%
\begin{isabellebody}%
\setisabellecontext{CoveringImpl}%
%
\isamarkupsubsubsection{FC and nonFC covering implementation%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ CoveringImpl\isanewline
\ \ \isakeyword{imports}\isanewline
\ \ \ Covering\isanewline
\ \ \ FamilyImpl\ UnionClosedImpl\ NonIsomorphicFamiliesImpl\isanewline
\ \ \ More{\isachardot}MoreBinomial\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}l\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ list\ {\isasymRightarrow}\ nat\ list\ list\ {\isasymRightarrow}\ nat\ list\ list\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}FC{\isacharunderscore}covered{\isacharunderscore}l\ Fc\ F\ perms\ {\isasymlongleftrightarrow}\ list{\isacharunderscore}ex\ {\isacharparenleft}{\isasymlambda}\ Fc{\isacharprime}{\isachardot}\ set\ Fc{\isacharprime}\ {\isasymsubseteq}\ set\ {\isacharparenleft}close{\isacharunderscore}l\ F{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ p{\isachardot}\ permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc{\isacharparenright}\ perms{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}soundness{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ p\ {\isasymin}\ set\ perms{\isachardot}\ p\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}dm\ Fc\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}FC{\isacharunderscore}covered{\isacharunderscore}l\ Fc\ F\ perms{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}FC{\isacharunderscore}covered\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ p\ \isakeyword{where}\ {\isachardoublequoteopen}p\ {\isasymin}\ set\ perms{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc{\isacharparenright}\ {\isasymsubseteq}\ set\ {\isacharparenleft}close{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}ex{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ rule{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isacharparenright}\ {\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}list{\isacharunderscore}to{\isacharunderscore}fun\ p{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isacharparenright}{\isachardoublequoteclose}\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
\ \ \ \ \ \ \ \ \ \ {\isacharbackquoteopen}p\ {\isasymin}\ set\ perms{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isacharunderscore}list{\isacharunderscore}to{\isacharunderscore}fun{\isacharunderscore}inj{\isacharunderscore}on{\isacharprime}{\isacharbrackleft}of\ p\ n\ {\isachardoublequoteopen}{\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ SetPermutations{\isacharunderscore}lists{\isachardot}permute{\isacharunderscore}family{\isacharunderscore}inj{\isacharunderscore}embed{\isacharbrackleft}of\ p\ Fc{\isacharbrackright}\ inj{\isacharunderscore}embed{\isacharunderscore}iso{\isacharbrackleft}of\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\ iso{\isacharunderscore}sym\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc{\isacharparenright}\ {\isasymsubseteq}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}set\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc{\isacharparenright}\ {\isasymsubseteq}\ set\ {\isacharparenleft}close{\isacharunderscore}l\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ SetUnionImpl{\isacharunderscore}lists{\isachardot}close{\isacharunderscore}set{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}completeness{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sdf\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}sdf\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}dm\ Fc\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}dm\ F\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}perms\ {\isacharequal}\ permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}FC{\isacharunderscore}covered\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}FC{\isacharunderscore}covered{\isacharunderscore}l\ Fc\ F\ perms{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ Fc{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}iso\ Fc{\isacharprime}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isacharparenright}{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}Fc{\isacharprime}\ {\isasymsubseteq}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ Fc{\isacharprime}\ {\isasymsubseteq}\ {\isasymUnion}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fc{\isacharprime}\ {\isasymsubseteq}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ Union{\isacharunderscore}mono{\isacharparenright}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ Fc{\isacharprime}\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}dm\ F\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}iso\ Fc{\isacharprime}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isacharparenright}{\isacharbackquoteclose}\ bij{\isacharunderscore}betw{\isacharunderscore}finite\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ iso{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Fc{\isacharprime}l\ \isakeyword{where}\ {\isachardoublequoteopen}Fc{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isacharprime}l{\isachardoublequoteclose}\ {\isachardoublequoteopen}sdf\ Fc{\isacharprime}l{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ SetImpl{\isacharunderscore}lists{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}ex{\isacharbrackleft}of\ Fc{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ p\ \isakeyword{where}\ {\isachardoublequoteopen}p{\isasymin}set\ perms{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ Fc{\isacharprime}l\ {\isacharequal}\ set\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}iso\ Fc{\isacharprime}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isacharparenright}{\isacharbackquoteclose}\ iso{\isacharunderscore}permute{\isacharunderscore}family{\isacharunderscore}l{\isacharbrackleft}of\ Fc\ Fc{\isacharprime}l\ n\ perms{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}dm\ Fc\ n{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymUnion}\ Fc{\isacharprime}\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbackquoteclose}\ \ {\isacharbackquoteopen}perms\ {\isacharequal}\ permute\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}sdf\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ iso{\isacharunderscore}sym{\isacharbrackleft}of\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isacharprime}l{\isachardoublequoteclose}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ list{\isacharunderscore}ex{\isacharunderscore}iff{\isacharcomma}\ rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc{\isachardoublequoteclose}\ \isakeyword{in}\ bexI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc\ {\isasymin}\ set\ {\isacharparenleft}FamilyImpl{\isachardot}map\ {\isacharparenleft}{\isasymlambda}p{\isachardot}\ permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc{\isacharparenright}\ perms{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}p\ {\isasymin}\ set\ perms{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc{\isacharparenright}\ {\isasymsubseteq}\ set\ {\isacharparenleft}close{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ Fc{\isacharprime}l\ {\isasymsubseteq}\ set\ {\isacharparenleft}close{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ Fc{\isacharprime}l{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}close{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ SetUnionImpl{\isacharunderscore}lists{\isachardot}close{\isacharunderscore}completeness{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}sorted\ A\ {\isasymand}\ distinct\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ A\ {\isasymin}\ set\ Fc{\isacharprime}l{\isachardot}\ sorted\ A\ {\isasymand}\ distinct\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isasymin}\ set\ Fc{\isacharprime}l{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}a{\isasymin}set\ F{\isachardot}\ sorted\ a\ {\isasymand}\ distinct\ a{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ A\ {\isasymin}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymin}\ set\ Fc{\isacharprime}l{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fc{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fc{\isacharprime}l{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fc{\isacharprime}\ {\isasymsubseteq}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}set\ Fc{\isacharprime}l\ {\isacharequal}\ set\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Fc{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ FCs{\isacharunderscore}covered{\isacharunderscore}l\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}FCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymF}\ F\ perms\ {\isasymlongleftrightarrow}\ list{\isacharunderscore}ex\ {\isacharparenleft}{\isasymlambda}\ Fc{\isachardot}\ FC{\isacharunderscore}covered{\isacharunderscore}l\ Fc\ F\ perms{\isacharparenright}\ {\isasymF}{\isachardoublequoteclose}\isanewline
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}l\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered{\isacharunderscore}l\ Nc\ F\ perms\ {\isasymlongleftrightarrow}\ \isanewline
\ \ \ \ list{\isacharunderscore}ex\ {\isacharparenleft}{\isasymlambda}\ Nc{\isacharprime}{\isachardot}\ set\ {\isacharparenleft}close{\isacharunderscore}l\ F{\isacharparenright}\ {\isasymsubseteq}\ set\ Nc{\isacharprime}{\isacharparenright}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ p{\isachardot}\ {\isacharparenleft}close{\isacharunderscore}insert{\isacharunderscore}empty{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Nc{\isacharparenright}{\isacharparenright}{\isacharparenright}\ perms{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}soundness{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ p\ {\isasymin}\ set\ perms{\isachardot}\ p\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}dm\ Nc\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered{\isacharunderscore}l\ Nc\ F\ perms{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Nc{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ p\ \isakeyword{where}\ {\isachardoublequoteopen}p\ {\isasymin}\ set\ perms{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ {\isacharparenleft}close{\isacharunderscore}insert{\isacharunderscore}empty{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Nc{\isacharparenright}{\isacharparenright}\ {\isasymsupseteq}\ set\ {\isacharparenleft}close{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}ex{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Nc{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ rule{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}iso\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Nc{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Nc{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}list{\isacharunderscore}to{\isacharunderscore}fun\ p{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Nc{\isacharparenright}{\isachardoublequoteclose}\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
\ \ \ \ \ \ \ \ \ \ {\isacharbackquoteopen}p\ {\isasymin}\ set\ perms{\isacharbackquoteclose}\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isacharunderscore}list{\isacharunderscore}to{\isacharunderscore}fun{\isacharunderscore}inj{\isacharunderscore}on{\isacharprime}{\isacharbrackleft}of\ p\ n\ {\isachardoublequoteopen}{\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Nc{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ SetPermutations{\isacharunderscore}lists{\isachardot}permute{\isacharunderscore}family{\isacharunderscore}inj{\isacharunderscore}embed{\isacharbrackleft}of\ p\ Nc{\isacharbrackright}\ inj{\isacharunderscore}embed{\isacharunderscore}iso{\isacharbrackleft}of\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Nc{\isachardoublequoteclose}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Nc{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\ iso{\isacharunderscore}sym\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}\ {\isasymsubseteq}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Nc{\isacharparenright}{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}set\ {\isacharparenleft}close{\isacharunderscore}insert{\isacharunderscore}empty{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Nc{\isacharparenright}{\isacharparenright}\ {\isasymsupseteq}\ set\ {\isacharparenleft}close{\isacharunderscore}l\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ SetUnionImpl{\isacharunderscore}lists{\isachardot}close{\isacharunderscore}set{\isacharbrackleft}of\ F{\isacharcomma}\ symmetric{\isacharbrackright}\ SetUnionImpl{\isacharunderscore}lists{\isachardot}close{\isacharunderscore}and{\isacharunderscore}insert{\isacharunderscore}empty{\isacharunderscore}set{\isacharbrackleft}symmetric{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ nonFCs{\isacharunderscore}covered{\isacharunderscore}l\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}nonFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymN}\ F\ perms\ {\isasymlongleftrightarrow}\ \isanewline
\ \ \ \ list{\isacharunderscore}ex\ {\isacharparenleft}{\isasymlambda}\ Nc{\isachardot}\ nonFC{\isacharunderscore}covered{\isacharunderscore}l\ Nc\ F\ perms{\isacharparenright}\ {\isasymN}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nonFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}soundness{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}p{\isasymin}set\ perms{\isachardot}\ p\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}dmf\ {\isasymN}\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}nonFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymN}\ F\ perms{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}nonFCs{\isacharunderscore}covered\ {\isacharparenleft}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isasymN}{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ nonFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}soundness{\isacharbrackleft}of\ perms\ n{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}ex{\isacharunderscore}iff{\isacharparenright}\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}Nc{\isachardoublequoteclose}\ \isakeyword{in}\ bexI{\isacharcomma}\ auto{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list\ list\ list\ {\isasymRightarrow}\ nat\ list\ list\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}nonFC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ Nc{\isacharunderscore}perms\ F\ {\isasymlongleftrightarrow}\ \isanewline
\ \ \ \ list{\isacharunderscore}ex\ {\isacharparenleft}{\isasymlambda}\ Nc{\isacharprime}{\isachardot}\ set\ {\isacharparenleft}close{\isacharunderscore}l\ F{\isacharparenright}\ {\isasymsubseteq}\ set\ Nc{\isacharprime}{\isacharparenright}\ Nc{\isacharunderscore}perms{\isachardoublequoteclose}\isanewline
\isacommand{definition}\isamarkupfalse%
\ nonFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}nonFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymN}{\isacharunderscore}perms\ F\ {\isasymlongleftrightarrow}\ \isanewline
\ \ \ \ list{\isacharunderscore}ex\ {\isacharparenleft}{\isasymlambda}\ Nc{\isachardot}\ nonFC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ Nc\ F{\isacharparenright}\ {\isasymN}{\isacharunderscore}perms{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ nonFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymN}{\isacharunderscore}perms\ {\isacharequal}\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ Nc{\isachardot}\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ p{\isachardot}\ close{\isacharunderscore}insert{\isacharunderscore}empty{\isacharunderscore}l\ {\isacharparenleft}permute{\isacharunderscore}family{\isacharunderscore}l\ p\ Nc{\isacharparenright}{\isacharparenright}\ perms{\isacharparenright}{\isacharparenright}\ {\isasymN}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}nonFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt\ {\isasymN}{\isacharunderscore}perms\ F\ {\isasymlongleftrightarrow}\ nonFCs{\isacharunderscore}covered{\isacharunderscore}l\ {\isasymN}\ F\ perms{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ nonFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ nonFCs{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharunderscore}def\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ nonFC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}def\ nonFC{\isacharunderscore}covered{\isacharunderscore}l{\isacharunderscore}opt{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}ex{\isacharunderscore}iff{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
