%
\begin{isabellebody}%
\setisabellecontext{NonIsomorphicFamilies}%
%
\isamarkupsubsection{Non-isomorphic families of sets%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ NonIsomorphicFamilies\isanewline
\isakeyword{imports}\ Main\ \isanewline
\ \ IsomorphicFamilies\isanewline
\ \ FamilyImpl\ \isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\begin{isamarkuptext}%
In this section we define a combinatorial algorithm
(implemented by a function \isa{non{\isacharunderscore}isomorphic{\isacharunderscore}families}) that
computes non isomorphic families of sets. Two uniform families (over
the same domain) are called isomorphic if one can be obtained from the
other by permuting elements of the domain. This function is used to
remove symmetric cases in verification of FC families.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{locale}\isamarkupfalse%
\ Mapping\ {\isacharequal}\ \isanewline
\ \ \isakeyword{fixes}\ to{\isacharunderscore}fun\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}m\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{locale}\isamarkupfalse%
\ SetPermutations\ {\isacharequal}\ SetImpl\ to{\isacharunderscore}set\ inv\ {\isacharplus}\ Mapping\ to{\isacharunderscore}fun\ \isakeyword{for}\isanewline
\ \ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s{\isacharcolon}{\isacharcolon}linorder\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{and}\ to{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s{\isacharcolon}{\isacharcolon}linorder\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequoteclose}\ \isakeyword{and}\ to{\isacharunderscore}fun\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}m\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardoublequoteclose}\ {\isacharplus}\isanewline
\ \ \isakeyword{fixes}\ permute{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}m\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}s{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ permute{\isacharunderscore}set{\isacharunderscore}set{\isacharcolon}\ {\isachardoublequoteopen}to{\isacharunderscore}set\ {\isacharparenleft}permute{\isacharunderscore}set\ p\ s{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}to{\isacharunderscore}fun\ p{\isacharparenright}\ {\isacharbackquote}\ {\isacharparenleft}to{\isacharunderscore}set\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ permute{\isacharunderscore}set{\isacharunderscore}inv{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}inj{\isacharunderscore}on\ {\isacharparenleft}to{\isacharunderscore}fun\ p{\isacharparenright}\ {\isacharparenleft}to{\isacharunderscore}set\ s{\isacharparenright}{\isacharsemicolon}\ inv\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ inv\ {\isacharparenleft}permute{\isacharunderscore}set\ p\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ permute{\isacharunderscore}family\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}m\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}permute{\isacharunderscore}family\ p\ F\ {\isacharequal}\ map\ {\isacharparenleft}permute{\isacharunderscore}set\ p{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ permute{\isacharunderscore}family{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}permute{\isacharunderscore}family\ p\ F{\isacharparenright}\ {\isacharequal}\ op\ {\isacharbackquote}\ {\isacharparenleft}to{\isacharunderscore}fun\ p{\isacharparenright}\ {\isacharbackquote}\ f{\isacharunderscore}to{\isacharunderscore}set\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ permute{\isacharunderscore}family{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ permute{\isacharunderscore}set{\isacharunderscore}set\isanewline
\isacommand{by}\isamarkupfalse%
\ force%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ permute{\isacharunderscore}family{\isacharunderscore}inj{\isacharunderscore}embed{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}to{\isacharunderscore}fun\ p{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}permute{\isacharunderscore}family\ p\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\ permute{\isacharunderscore}family{\isacharunderscore}set\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}to{\isacharunderscore}fun\ p{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{function}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux\ perms\ fams\ res\ {\isacharequal}\isanewline
\ \ {\isacharparenleft}case\ fams\ of\ \isanewline
\ \ \ \ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ res\isanewline
\ \ {\isacharbar}\ h\ {\isacharhash}\ t\ {\isasymRightarrow}\ \isanewline
\ \ \ \ let\ hp\ {\isacharequal}\ remdups\ {\isacharparenleft}h\ {\isacharhash}\ map\ {\isacharparenleft}{\isasymlambda}\ p{\isachardot}\ permute{\isacharunderscore}family\ p\ h{\isacharparenright}\ perms{\isacharparenright}\ in\isanewline
\ \ \ \ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux\ perms\ {\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}\ l{\isachardot}\ sort\ l\ {\isasymnotin}\ set\ {\isacharparenleft}map\ sort\ hp{\isacharparenright}{\isacharparenright}\ fams{\isacharparenright}\ {\isacharparenleft}h\ {\isacharhash}\ res{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isacommand{termination}\isamarkupfalse%
\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}p{\isacharcomma}\ f{\isacharcomma}\ r{\isacharparenright}{\isachardot}\ length\ f{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isacommand{declare}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families\ \isakeyword{where}\isanewline
\ \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}non{\isacharunderscore}isomorphic{\isacharunderscore}families\ perms\ fams\ {\isacharequal}\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux\ perms\ fams\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isacharunderscore}res{\isacharunderscore}mono{\isacharcolon}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set\ res\ {\isasymsubseteq}\ set\ {\isacharparenleft}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux\ perms\ fams\ res{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ perms\ fams\ res\ rule{\isacharcolon}\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ perms\ fams\ res{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ fams{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ a\ fams{\isacharprime}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ perms\ fams\ res{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharbrackleft}of\ a\ fams{\isacharprime}\ {\isachardoublequoteopen}remdups\ {\isacharparenleft}a\ {\isacharhash}\ FamilyImpl{\isachardot}map\ {\isacharparenleft}{\isasymlambda}p{\isachardot}\ permute{\isacharunderscore}family\ p\ a{\isacharparenright}\ perms{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isacharunderscore}subset{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F\ {\isasymsupseteq}\ set\ res{\isachardoublequoteclose}\ {\isachardoublequoteopen}F\ {\isasymsupseteq}\ set\ fams{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}F\ {\isasymsupseteq}\ set\ {\isacharparenleft}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux\ perms\ fams\ res{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ perms\ fams\ res\ rule{\isacharcolon}\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ perms\ fams\ res{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ fams{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ a\ fams{\isacharprime}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}hp\ {\isacharequal}\ {\isachardoublequoteopen}remdups\ {\isacharparenleft}a\ {\isacharhash}\ FamilyImpl{\isachardot}map\ {\isacharparenleft}{\isasymlambda}p{\isachardot}\ permute{\isacharunderscore}family\ p\ a{\isacharparenright}\ perms{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharparenleft}let\ hp\ {\isacharequal}\ {\isacharquery}hp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ in\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux\ perms\ {\isacharbrackleft}l{\isasymleftarrow}fams\ {\isachardot}\ sort\ l\ {\isasymnotin}\ set\ {\isacharparenleft}map\ sort\ hp{\isacharparenright}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}a\ {\isacharhash}\ res{\isacharparenright}{\isacharparenright}\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ a\ fams{\isacharprime}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ Cons\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ perms\ fams\ res{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}subset{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set\ {\isacharparenleft}non{\isacharunderscore}isomorphic{\isacharunderscore}families\ perms\ F{\isacharparenright}\ {\isasymsubseteq}\ set\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isacharunderscore}subset{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ p\ {\isasymin}\ set\ perms{\isachardot}\ {\isasymforall}\ F\ {\isasymin}\ set\ fams{\isachardot}\ inj{\isacharunderscore}on\ {\isacharparenleft}to{\isacharunderscore}fun\ p{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ fams{\isachardot}\ {\isasymexists}\ F{\isacharprime}\ {\isasymin}\ set\ {\isacharparenleft}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux\ perms\ fams\ res{\isacharparenright}{\isachardot}\ inj{\isacharunderscore}embed\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ perms\ fams\ res\ rule{\isacharcolon}\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ perms\ fams\ res{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}fams{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ F\ fams{\isacharprime}{\isacharparenright}\isanewline
\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}nefams\ {\isacharequal}\ {\isachardoublequoteopen}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux\ perms\ fams\ res{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}hp\ {\isacharequal}\ {\isachardoublequoteopen}remdups\ {\isacharparenleft}F\ {\isacharhash}\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ p{\isachardot}\ permute{\isacharunderscore}family\ p\ F{\isacharparenright}\ perms{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}filt\ {\isacharequal}\ {\isachardoublequoteopen}filter\ {\isacharparenleft}{\isasymlambda}\ l{\isachardot}\ sort\ l\ {\isasymnotin}\ set\ {\isacharparenleft}map\ sort\ {\isacharquery}hp{\isacharparenright}{\isacharparenright}\ fams{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}nef\ {\isacharequal}\ {\isachardoublequoteopen}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux\ perms\ {\isacharquery}filt\ {\isacharparenleft}F\ {\isacharhash}\ res{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}nefams\ {\isacharequal}\ {\isacharquery}nef{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ perms\ fams\ res{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ballI{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ Fa\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}Fa\ {\isasymin}\ set\ fams{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}a{\isasymin}set\ {\isacharquery}nefams{\isachardot}\ inj{\isacharunderscore}embed\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Fa{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ a{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}sort\ Fa\ {\isacharequal}\ sort\ F{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}F\ \isakeyword{in}\ bexI{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}F\ {\isasymin}\ set\ {\isacharparenleft}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux\ perms\ fams\ res{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isacharquery}nefams\ {\isacharequal}\ {\isacharquery}nef{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isacharunderscore}res{\isacharunderscore}mono{\isacharbrackleft}of\ {\isachardoublequoteopen}F\ {\isacharhash}\ res{\isachardoublequoteclose}\ perms\ {\isacharquery}filt{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Fa{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sort\ Fa\ {\isacharequal}\ sort\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}def\ image{\isacharunderscore}set\ inj{\isacharunderscore}embed{\isacharunderscore}refl\ set{\isacharunderscore}sort{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}Fa\ {\isasymin}\ set\ fams{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons\ {\isacharbackquoteopen}Fa\ {\isasymin}\ set\ fams{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}sort\ Fa\ {\isasymin}\ set\ {\isacharparenleft}map\ sort\ {\isacharquery}hp{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons\ {\isacharbackquoteopen}Fa\ {\isasymin}\ set\ fams{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ F\ fams{\isacharprime}\ {\isacharquery}hp{\isacharbrackright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isacharquery}nefams\ {\isacharequal}\ {\isacharquery}nef{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ p\ \isakeyword{where}\ {\isachardoublequoteopen}p\ {\isasymin}\ set\ {\isacharparenleft}perms{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}sort\ Fa\ {\isacharequal}\ sort\ {\isacharparenleft}permute{\isacharunderscore}family\ p\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}to{\isacharunderscore}fun\ p{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sort\ Fa\ {\isasymnoteq}\ sort\ F{\isacharbackquoteclose}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ Cons\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ split{\isacharcolon}\ if{\isacharunderscore}split{\isacharunderscore}asm{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Fa{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ permute{\isacharunderscore}family{\isacharunderscore}inj{\isacharunderscore}embed{\isacharbrackleft}of\ p\ F{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}def\ image{\isacharunderscore}set\ set{\isacharunderscore}sort{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}F\ {\isasymin}\ set\ {\isacharquery}nefams{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isacharquery}nefams\ {\isacharequal}\ {\isacharquery}nef{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux{\isacharunderscore}res{\isacharunderscore}mono{\isacharbrackleft}of\ {\isachardoublequoteopen}F\ {\isacharhash}\ res{\isachardoublequoteclose}\ perms\ {\isacharquery}filt{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}embed{\isacharunderscore}sym{\isacharbrackleft}of\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ Fa{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ p\ {\isasymin}\ set\ perms{\isachardot}\ {\isasymforall}\ F\ {\isasymin}\ set\ fams{\isachardot}\ inj{\isacharunderscore}on\ {\isacharparenleft}to{\isacharunderscore}fun\ p{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ fams{\isachardot}\ {\isasymexists}\ F{\isacharprime}\ {\isasymin}\ set\ {\isacharparenleft}non{\isacharunderscore}isomorphic{\isacharunderscore}families\ perms\ fams{\isacharparenright}{\isachardot}\ inj{\isacharunderscore}embed\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}aux\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ generating{\isacharunderscore}subset{\isacharunderscore}non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}p{\isasymin}set\ perms{\isachardot}\ {\isasymforall}F{\isasymin}set\ FF{\isachardot}\ inj{\isacharunderscore}on\ {\isacharparenleft}to{\isacharunderscore}fun\ p{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}{\isasymcircle}FF{\isacharparenright}\ FF{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}{\isasymcircle}{\isacharparenleft}non{\isacharunderscore}isomorphic{\isacharunderscore}families\ perms\ FF{\isacharparenright}{\isacharparenright}\ FF{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymcircle}\ {\isacharparenleft}non{\isacharunderscore}isomorphic{\isacharunderscore}families\ perms\ FF{\isacharparenright}\ {\isasymsubseteq}\ FF{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}{\isasymcircle}FF{\isacharparenright}\ FF{\isacharprime}{\isacharbackquoteclose}\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharunderscore}subset{\isacharbrackleft}of\ perms{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso{\isacharunderscore}represents\ {\isacharparenleft}{\isasymcircle}\ {\isacharparenleft}non{\isacharunderscore}isomorphic{\isacharunderscore}families\ perms\ FF{\isacharparenright}{\isacharparenright}\ FF{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}represents{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ F{\isacharprime}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymin}\ FF{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F\ \isakeyword{where}\ {\isachardoublequoteopen}F\ {\isasymin}\ {\isacharparenleft}{\isasymcircle}FF{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}iso\ F{\isacharprime}\ F{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}iso{\isacharunderscore}representing{\isacharunderscore}subset\ {\isacharparenleft}{\isasymcircle}FF{\isacharparenright}\ FF{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}represents{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Fl\ \isakeyword{where}\ {\isachardoublequoteopen}Fl\ {\isasymin}\ set\ FF{\isachardoublequoteclose}\ {\isachardoublequoteopen}F\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ Fl{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ F{\isacharprime}{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}F{\isacharprime}{\isacharprime}\ {\isasymin}{\isasymcircle}{\isacharparenleft}non{\isacharunderscore}isomorphic{\isacharunderscore}families\ perms\ FF{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}inj{\isacharunderscore}embed\ F\ F{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ non{\isacharunderscore}isomorphic{\isacharunderscore}families{\isacharprime}{\isacharbrackleft}of\ perms\ FF{\isacharcomma}\ OF\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}metis\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}def\ imageI\ image{\isacharunderscore}set{\isacharparenright}\ \isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}Bex\ {\isacharparenleft}{\isasymcircle}\ {\isacharparenleft}non{\isacharunderscore}isomorphic{\isacharunderscore}families\ perms\ FF{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}iso\ F{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}iso\ F{\isacharprime}\ F{\isacharbackquoteclose}\ iso{\isacharunderscore}trans\ inj{\isacharunderscore}embed{\isacharunderscore}iso\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{end}\isamarkupfalse%
\ \isanewline
\isanewline
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
