%
\begin{isabellebody}%
\setisabellecontext{NonIsomorphicFamiliesImpl}%
%
\isamarkupsubsubsection{Implementation by sets represented by (sorted and distinct) lists%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ NonIsomorphicFamiliesImpl\isanewline
\isakeyword{imports}\ NonIsomorphicFamilies\isanewline
\ \ \ \ \ \ \ \ Combinatorics\isanewline
\ \ \ \ \ \ \ \ {\isachardoublequoteopen}HOL{\isacharminus}Library{\isachardot}List{\isacharunderscore}lexord{\isachardoublequoteclose}\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ list{\isacharunderscore}to{\isacharunderscore}fun\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}list{\isacharunderscore}to{\isacharunderscore}fun\ l\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}\ n{\isachardot}\ l\ {\isacharbang}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ permute{\isacharunderscore}set{\isacharunderscore}l\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ {\isasymRightarrow}\ nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}permute{\isacharunderscore}set{\isacharunderscore}l\ p\ A\ {\isacharequal}\ sort\ {\isacharparenleft}map\ {\isacharparenleft}list{\isacharunderscore}to{\isacharunderscore}fun\ p{\isacharparenright}\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{global{\isacharunderscore}interpretation}\isamarkupfalse%
\ SetPermutations{\isacharunderscore}lists{\isacharcolon}\ SetPermutations\ sd\ set\ list{\isacharunderscore}to{\isacharunderscore}fun\ permute{\isacharunderscore}set{\isacharunderscore}l\isanewline
\ \ \isakeyword{defines}\isanewline
\ \ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetPermutations{\isacharunderscore}lists{\isachardot}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ permute{\isacharunderscore}family{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetPermutations{\isacharunderscore}lists{\isachardot}permute{\isacharunderscore}family{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetPermutations{\isacharunderscore}lists{\isachardot}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}unfold{\isacharunderscore}locales{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ p\ s\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharparenleft}permute{\isacharunderscore}set{\isacharunderscore}l\ p\ s{\isacharparenright}\ {\isacharequal}\ list{\isacharunderscore}to{\isacharunderscore}fun\ p\ {\isacharbackquote}\ set\ s{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ permute{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ s{\isacharcolon}{\isacharcolon}{\isachardoublequoteopen}nat\ list{\isachardoublequoteclose}\ \isakeyword{and}\ p\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}sorted\ s\ {\isasymand}\ distinct\ s{\isachardoublequoteclose}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}list{\isacharunderscore}to{\isacharunderscore}fun\ p{\isacharparenright}\ {\isacharparenleft}set\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}sorted\ {\isacharparenleft}permute{\isacharunderscore}set{\isacharunderscore}l\ p\ s{\isacharparenright}\ {\isasymand}\ distinct\ {\isacharparenleft}permute{\isacharunderscore}set{\isacharunderscore}l\ p\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ permute{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}def\ list{\isacharunderscore}to{\isacharunderscore}fun{\isacharunderscore}def\ distinct{\isacharunderscore}map{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nat{\isacharunderscore}list{\isacharunderscore}to{\isacharunderscore}fun{\isacharunderscore}inj{\isacharunderscore}on{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ p{\isachardoublequoteclose}\ {\isachardoublequoteopen}p\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}X\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}length\ p{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}list{\isacharunderscore}to{\isacharunderscore}fun\ p{\isacharparenright}\ X{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}conv{\isacharunderscore}nth{\isacharbrackleft}of\ p{\isacharbrackright}\isanewline
\ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}to{\isacharunderscore}fun{\isacharunderscore}def\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}erule{\isacharunderscore}tac\ x{\isacharequal}x\ \isakeyword{in}\ allE{\isacharcomma}\ drule\ mp{\isacharcomma}\ force{\isacharparenright}\isanewline
\ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}erule{\isacharunderscore}tac\ x{\isacharequal}y\ \isakeyword{in}\ allE{\isacharcomma}\ drule\ mp{\isacharcomma}\ force{\isacharparenright}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nat{\isacharunderscore}list{\isacharunderscore}to{\isacharunderscore}fun{\isacharunderscore}inj{\isacharunderscore}on{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}\ p\ {\isasymin}\ set\ perms{\isachardot}\ p\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ fams{\isachardot}\ {\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}p{\isasymin}set\ perms{\isachardot}\ {\isasymforall}F{\isasymin}set\ fams{\isachardot}\ inj{\isacharunderscore}on\ {\isacharparenleft}list{\isacharunderscore}to{\isacharunderscore}fun\ p{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\ list{\isacharunderscore}to{\isacharunderscore}fun{\isacharunderscore}def\ SetImpl{\isacharunderscore}lists{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}auto{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ p\ F\ x\ y\ Ax\ Ay\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}p\ {\isasymin}\ set\ perms{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}F\ {\isasymin}\ set\ fams{\isachardoublequoteclose}\ {\isachardoublequoteopen}Ax\ {\isasymin}\ set\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ Ax{\isachardoublequoteclose}\ {\isachardoublequoteopen}Ay\ {\isasymin}\ set\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymin}\ set\ Ay{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ {\isachardoublequoteopen}p\ {\isacharbang}\ x\ {\isacharequal}\ p\ {\isacharbang}\ y{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ p{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}length\ p\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}p\ {\isasymin}\ set\ perms{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ perm{\isacharunderscore}distinct{\isacharunderscore}iff{\isacharbrackleft}of\ p\ {\isachardoublequoteopen}{\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ perm{\isacharunderscore}length{\isacharbrackleft}of\ p\ {\isachardoublequoteopen}{\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharless}\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isacharless}\ n{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ \ SetImpl{\isacharunderscore}lists{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ force{\isacharplus}\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}p\ {\isacharbang}\ x\ {\isacharequal}\ p\ {\isacharbang}\ y{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ nth{\isacharunderscore}eq{\isacharunderscore}iff{\isacharunderscore}index{\isacharunderscore}eq\ {\isacharbrackleft}of\ p\ x\ y{\isacharbrackright}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ iso{\isacharunderscore}permute{\isacharunderscore}family{\isacharunderscore}l{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}iso\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}sdf\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}sdf\ F{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}dm\ F\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}dm\ F{\isacharprime}\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}perms\ {\isacharequal}\ permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ p\ {\isasymin}\ set\ perms{\isachardot}\ set\ F{\isacharprime}\ {\isacharequal}\ set\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ assms\ \isacommand{obtain}\isamarkupfalse%
\ f\ \isakeyword{where}\ bij{\isacharcolon}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ f\ {\isacharparenleft}{\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharprime}\ {\isacharequal}\ op\ {\isacharbackquote}\ f\ {\isacharbackquote}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}\ {\isacharminus}\ {\isacharparenleft}{\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ card\ {\isacharparenleft}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}\ {\isacharminus}\ {\isacharparenleft}{\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ bij\ {\isacharbackquoteopen}dm\ F\ n{\isacharbackquoteclose}\ {\isacharbackquoteopen}dm\ F{\isacharprime}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ bij{\isacharunderscore}betw{\isacharunderscore}same{\isacharunderscore}card\ card{\isacharunderscore}Diff{\isacharunderscore}subset\ finite{\isacharunderscore}atLeastLessThan\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ f{\isacharprime}\ \isakeyword{where}\ bij{\isacharcolon}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ f{\isacharprime}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ {\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isachardot}\ f{\isacharprime}\ x\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}extend{\isacharbrackleft}OF\ bij{\isacharcomma}\ of\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}\ {\isacharminus}\ {\isacharparenleft}{\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}\ {\isacharminus}\ {\isacharparenleft}{\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}dm\ F{\isacharprime}\ n{\isacharbackquoteclose}\ {\isacharbackquoteopen}dm\ F\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}metis\ subset{\isacharunderscore}Un{\isacharunderscore}eq{\isacharparenright}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharprime}\ {\isacharequal}\ op\ {\isacharbackquote}\ f{\isacharprime}\ {\isacharbackquote}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ x\ {\isasymin}\ {\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isachardot}\ f{\isacharprime}\ x\ {\isacharequal}\ f\ x{\isacharbackquoteclose}\ {\isacharasterisk}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ map{\isacharunderscore}fam{\isacharunderscore}cong{\isacharparenright}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}perm\ {\isacharequal}\ {\isachardoublequoteopen}map\ f{\isacharprime}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}perm\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mset{\isacharunderscore}eq{\isacharunderscore}perm{\isacharbrackleft}symmetric{\isacharbrackright}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ set{\isacharunderscore}eq{\isacharunderscore}iff{\isacharunderscore}mset{\isacharunderscore}eq{\isacharunderscore}distinct{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}map\ f{\isacharprime}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}map{\isacharbrackleft}of\ f{\isacharprime}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ bij\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ bij{\isacharunderscore}betw{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharparenleft}map\ f{\isacharprime}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ set\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ bij\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharquery}perm{\isachardoublequoteclose}\ \isakeyword{in}\ bexI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}perm\ {\isasymin}\ set\ perms{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}perms\ {\isacharequal}\ permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isacharquery}perm\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ permute{\isacharunderscore}isPermutation{\isacharbrackleft}of\ {\isacharquery}perm\ {\isachardoublequoteopen}{\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ F{\isacharprime}\ {\isacharequal}\ set\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ {\isacharquery}perm\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ y\ \isakeyword{where}\ {\isachardoublequoteopen}y\ {\isasymin}\ set\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isacharasterisk}{\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}set\ x\ {\isacharequal}\ f{\isacharprime}\ {\isacharbackquote}\ set\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto{\isacharcomma}\ smt\ image{\isacharunderscore}eqI\ image{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ y\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymin}\ set\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}dm\ F\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ permute{\isacharunderscore}set{\isacharunderscore}l\ {\isacharquery}perm\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}map\ {\isacharparenleft}op\ {\isacharbang}\ {\isacharparenleft}FamilyImpl{\isachardot}map\ f{\isacharprime}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ y\ {\isacharequal}\ map\ f{\isacharprime}\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymin}\ set\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}dm\ F\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sd\ x{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymin}\ set\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}sdf\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isasymin}\ set\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}sdf\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ sort\ {\isacharparenleft}map\ f{\isacharprime}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}\ {\isacharbackquoteopen}set\ y\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}distinct{\isacharunderscore}set{\isacharunderscore}unique{\isacharbrackleft}of\ x\ {\isachardoublequoteopen}sort\ {\isacharparenleft}map\ f{\isacharprime}\ y{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ bij\ distinct{\isacharunderscore}map{\isacharbrackleft}of\ f{\isacharprime}\ y{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ subset{\isacharunderscore}inj{\isacharunderscore}on{\isacharbrackleft}of\ f{\isacharprime}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ y{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\ \isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ permute{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}def\ list{\isacharunderscore}to{\isacharunderscore}fun{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ metis\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ {\isacharquery}perm\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymin}\ set\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ SetPermutations{\isacharunderscore}lists{\isachardot}permute{\isacharunderscore}family{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ {\isacharquery}perm\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ y\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isacharequal}\ permute{\isacharunderscore}set{\isacharunderscore}l\ {\isacharquery}perm\ y{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymin}\ set\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ SetPermutations{\isacharunderscore}lists{\isachardot}permute{\isacharunderscore}family{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ sort\ {\isacharparenleft}map\ f{\isacharprime}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}map\ {\isacharparenleft}op\ {\isacharbang}\ {\isacharparenleft}FamilyImpl{\isachardot}map\ f{\isacharprime}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ y\ {\isacharequal}\ map\ f{\isacharprime}\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymin}\ set\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}dm\ F\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isacharequal}\ permute{\isacharunderscore}set{\isacharunderscore}l\ {\isacharquery}perm\ y{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ permute{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}def\ list{\isacharunderscore}to{\isacharunderscore}fun{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ metis\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ x\ {\isasymin}\ set\ {\isacharparenleft}map\ set\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymin}\ set\ F{\isacharbackquoteclose}\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ y{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ y\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}y\ {\isasymin}\ set\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}sdf\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}dm\ F\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}sd\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isacharequal}\ sort\ {\isacharparenleft}map\ f{\isacharprime}\ y{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}y\ {\isasymin}\ set\ F{\isacharbackquoteclose}\ distinct{\isacharunderscore}map{\isacharbrackleft}of\ f{\isacharprime}\ y{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ subset{\isacharunderscore}inj{\isacharunderscore}on{\isacharbrackleft}of\ f{\isacharprime}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ y{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ bij\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\ \isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sdf\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ SetImpl{\isacharunderscore}lists{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}def\ SetImpl{\isacharunderscore}lists{\isachardot}set{\isacharunderscore}set{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{lemmas}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}soundness\ {\isacharequal}\ SetPermutations{\isacharunderscore}lists{\isachardot}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharprime}{\isacharbrackleft}OF\ nat{\isacharunderscore}list{\isacharunderscore}to{\isacharunderscore}fun{\isacharunderscore}inj{\isacharunderscore}on{\isacharbrackright}\isanewline
\isacommand{lemmas}\isamarkupfalse%
\ permute{\isacharunderscore}set{\isacharunderscore}inv{\isacharunderscore}l\ {\isacharequal}\ SetPermutations{\isacharunderscore}lists{\isachardot}permute{\isacharunderscore}set{\isacharunderscore}inv{\isacharbrackleft}OF\ nat{\isacharunderscore}list{\isacharunderscore}to{\isacharunderscore}fun{\isacharunderscore}inj{\isacharunderscore}on{\isacharprime}{\isacharbrackright}\isanewline
\isacommand{lemmas}\isamarkupfalse%
\ iso{\isacharunderscore}representing{\isacharunderscore}subset{\isacharunderscore}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}l\ {\isacharequal}\ SetPermutations{\isacharunderscore}lists{\isachardot}generating{\isacharunderscore}subset{\isacharunderscore}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharbrackleft}OF\ nat{\isacharunderscore}list{\isacharunderscore}to{\isacharunderscore}fun{\isacharunderscore}inj{\isacharunderscore}on{\isacharbrackright}\isanewline
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
