%
\begin{isabellebody}%
\setisabellecontext{FamilyImpl}%
%
\isamarkupsection{Executable implementations of set families%
}
\isamarkuptrue%
%
\isamarkupsubsection{Abstract representation of sets and families%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ FamilyImpl\isanewline
\isakeyword{imports}\ Family\isanewline
\ \ \ \ \ \ \ \ Frankl\ \isanewline
\ \ \ \ \ \ \ \ More{\isachardot}MoreSet\ ListNat\isanewline
\ \ \ \ \ \ \ \ {\isachardoublequoteopen}HOL{\isacharminus}Library{\isachardot}List{\isacharunderscore}lexord{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ {\isachardoublequoteopen}HOL{\isacharminus}Library{\isachardot}Code{\isacharunderscore}Target{\isacharunderscore}Nat{\isachardoublequoteclose}\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ map\ \isakeyword{where}\ {\isachardoublequoteopen}map\ {\isasymequiv}\ List{\isachardot}map{\isachardoublequoteclose}%
\begin{isamarkuptext}%
Set operations are specified in the following locale. Families are
always represented as (distinct) lists of sets.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{locale}\isamarkupfalse%
\ SetImpl\ {\isacharequal}\ \isanewline
\ \ \isakeyword{fixes}\ to{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{fixes}\ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ to{\isacharunderscore}set{\isacharunderscore}inj{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}inv\ s{\isadigit{1}}{\isacharsemicolon}\ inv\ s{\isadigit{2}}{\isacharsemicolon}\ to{\isacharunderscore}set\ s{\isadigit{1}}\ {\isacharequal}\ to{\isacharunderscore}set\ s{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ s{\isadigit{1}}\ {\isacharequal}\ s{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ to{\isacharunderscore}set{\isacharunderscore}ex{\isacharcolon}\ {\isachardoublequoteopen}finite\ a\ {\isasymLongrightarrow}\ {\isasymexists}\ s{\isachardot}\ a\ {\isacharequal}\ to{\isacharunderscore}set\ s\ {\isasymand}\ inv\ s{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ to{\isacharunderscore}set{\isacharunderscore}finite{\isacharcolon}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}to{\isacharunderscore}set\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ F\ {\isacharequal}\ set\ {\isacharparenleft}map\ to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ fs{\isacharunderscore}to{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set\ set{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymcircle}{\isachardoublequoteclose}{\isacharparenright}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}{\isasymcircle}\ FF\ {\isasymequiv}\ set\ {\isacharparenleft}map\ f{\isacharunderscore}to{\isacharunderscore}set\ FF{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ to{\isacharunderscore}set{\isacharunderscore}inj{\isacharunderscore}on{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ set\ A{\isachardot}\ inv\ a\ {\isasymLongrightarrow}\ inj{\isacharunderscore}on\ to{\isacharunderscore}set\ {\isacharparenleft}set\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ to{\isacharunderscore}set{\isacharunderscore}inj{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}set{\isacharcolon}\ \isanewline
\ \ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}a{\isasymin}set\ A{\isachardot}\ inv\ a{\isacharsemicolon}\ inv\ h{\isasymrbrakk}\ {\isasymLongrightarrow}\ \isanewline
\ \ \ \ \ h\ {\isasymin}\ set\ A\ {\isasymlongleftrightarrow}\ to{\isacharunderscore}set\ h\ {\isasymin}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ to{\isacharunderscore}set{\isacharunderscore}inj\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}ex{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ Fl{\isachardot}\ F\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ Fl\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ A\ {\isasymin}\ set\ Fl{\isachardot}\ inv\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ F{\isachardot}\ finite\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ F{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ empty\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}insert\ A\ F{\isacharparenright}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Fl\ Al\ \isakeyword{where}\ {\isachardoublequoteopen}F\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ Fl\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ A\ {\isasymin}\ set\ Fl{\isachardot}\ inv\ A{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isacharequal}\ to{\isacharunderscore}set\ Al\ {\isasymand}\ inv\ Al{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ to{\isacharunderscore}set{\isacharunderscore}ex{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}Al\ {\isacharhash}\ Fl{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ contains\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}contains\ a\ S\ {\isasymequiv}\ a\ {\isasymin}\ to{\isacharunderscore}set\ S{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ count\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}count\ a\ F\ {\isacharequal}\ length\ {\isacharparenleft}filter\ {\isacharparenleft}contains\ a{\isacharparenright}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ count{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ set\ F{\isachardot}\ inv\ x{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}count\ a\ F\ {\isacharequal}\ Family{\isachardot}count\ a\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}to{\isacharunderscore}set\ {\isacharbackquote}\ {\isacharbraceleft}x\ {\isasymin}\ set\ F{\isachardot}\ a\ {\isasymin}\ to{\isacharunderscore}set\ x{\isacharbraceright}\ {\isacharequal}\ {\isacharbraceleft}S\ {\isasymin}\ to{\isacharunderscore}set\ {\isacharbackquote}\ set\ F{\isachardot}\ a\ {\isasymin}\ S{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ to{\isacharunderscore}set\ {\isacharbraceleft}x\ {\isasymin}\ set\ F{\isachardot}\ a\ {\isasymin}\ to{\isacharunderscore}set\ x{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ to{\isacharunderscore}set{\isacharunderscore}inj\ {\isacharbackquoteopen}{\isasymforall}\ x\ {\isasymin}\ set\ F{\isachardot}\ inv\ x{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharbraceleft}x\ {\isasymin}\ set\ F{\isachardot}\ a\ {\isasymin}\ to{\isacharunderscore}set\ x{\isacharbraceright}\ {\isacharequal}\ card\ {\isacharbraceleft}S\ {\isasymin}\ to{\isacharunderscore}set\ {\isacharbackquote}\ set\ F{\isachardot}\ a\ {\isasymin}\ S{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}image{\isacharbrackleft}of\ to{\isacharunderscore}set\ {\isachardoublequoteopen}{\isacharbraceleft}x\ {\isasymin}\ set\ F{\isachardot}\ a\ {\isasymin}\ to{\isacharunderscore}set\ x{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ distinct{\isacharunderscore}card{\isacharbrackleft}of\ {\isachardoublequoteopen}filter\ {\isacharparenleft}contains\ a{\isacharparenright}\ F{\isachardoublequoteclose}{\isacharcomma}\ symmetric{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ count{\isacharunderscore}def\ Family{\isachardot}count{\isacharunderscore}def\ contains{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ frankl{\isacharunderscore}fun\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ x\ F\ {\isasymequiv}\ {\isadigit{2}}\ {\isacharasterisk}\ int\ {\isacharparenleft}count\ x\ F{\isacharparenright}\ {\isacharminus}\ int\ {\isacharparenleft}length\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ frankl{\isacharunderscore}fun{\isacharunderscore}set{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ Fs{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ set\ Fs{\isachardot}\ inv\ A{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ a\ Fs\ {\isacharequal}\ Frankl{\isachardot}frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Fs{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ to{\isacharunderscore}set\ {\isacharparenleft}set\ Fs{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ to{\isacharunderscore}set{\isacharunderscore}inj\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}to{\isacharunderscore}set\ {\isacharbackquote}\ set\ Fs{\isacharparenright}\ {\isacharequal}\ card\ {\isacharparenleft}set\ Fs{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ card{\isacharunderscore}image{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}card{\isacharbrackleft}OF\ assms{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ count{\isacharunderscore}set{\isacharbrackleft}OF\ assms{\isacharcomma}\ of\ a{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ frankl{\isacharunderscore}fun{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{end}\isamarkupfalse%
%
\isamarkupsubsubsection{Implementation of sets by sorted and distinct lists%
}
\isamarkuptrue%
\isacommand{abbreviation}\isamarkupfalse%
\ sd\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}sd\ A\ {\isasymequiv}\ sorted\ A\ {\isasymand}\ distinct\ A{\isachardoublequoteclose}\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ sdf\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}sdf\ F\ {\isasymequiv}\ {\isasymforall}\ A\ {\isasymin}\ set\ F{\isachardot}\ sd\ A{\isachardoublequoteclose}\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ sdff\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}sdff\ {\isasymF}\ {\isasymequiv}\ {\isasymforall}\ F\ {\isasymin}\ set\ {\isasymF}{\isachardot}\ sdf\ F{\isachardoublequoteclose}%
\begin{isamarkuptext}%
For example, the family \isa{{\isacharbraceleft}{\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharbraceright}} is represented
by \isa{{\isacharbrackleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharbrackright}{\isacharbrackright}}.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{global{\isacharunderscore}interpretation}\isamarkupfalse%
\ SetImpl{\isacharunderscore}lists{\isacharcolon}\ SetImpl\ {\isachardoublequoteopen}set\ {\isacharcolon}{\isacharcolon}\ nat\ list\ {\isasymRightarrow}\ nat\ set{\isachardoublequoteclose}\ {\isachardoublequoteopen}sd{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{defines}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetImpl{\isacharunderscore}lists{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ count{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetImpl{\isacharunderscore}lists{\isachardot}count{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ frankl{\isacharunderscore}fun{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetImpl{\isacharunderscore}lists{\isachardot}frankl{\isacharunderscore}fun{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}unfold{\isacharunderscore}locales{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ a\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ a{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}s{\isachardot}\ a\ {\isacharequal}\ set\ s\ {\isasymand}\ sd\ s{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ a{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sorted{\isacharunderscore}distinct{\isacharunderscore}set{\isacharunderscore}unique{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ dm\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}dm\ F\ n\ {\isasymequiv}\ {\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ dmf\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}dmf\ FF\ n\ {\isasymequiv}\ {\isasymforall}\ F\ {\isasymin}\ set\ FF{\isachardot}\ dm\ F\ n{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}fs{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F\ {\isasymequiv}\ set\ {\isacharparenleft}map\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ F{\isacharparenright}{\isachardoublequoteclose}%
\isamarkupsubsubsection{Implementation of sets of nats by nats%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
For example, the family \isa{{\isacharbraceleft}{\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharbraceright}} is represented
by \isa{{\isacharbrackleft}{\isadigit{1}}{\isadigit{4}}{\isacharcomma}\ {\isadigit{2}}{\isadigit{8}}{\isacharbrackright}}. Encoding and decoding funcions are defined in 
the theory ListNat.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{global{\isacharunderscore}interpretation}\isamarkupfalse%
\ SetImpl{\isacharunderscore}nats{\isacharcolon}\ SetImpl\ {\isachardoublequoteopen}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymlambda}\ n{\isachardot}\ True{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{defines}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SetImpl{\isacharunderscore}nats{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ count{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SetImpl{\isacharunderscore}nats{\isachardot}count{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ frankl{\isacharunderscore}fun{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SetImpl{\isacharunderscore}nats{\isachardot}frankl{\isacharunderscore}fun{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}unfold{\isacharunderscore}locales{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ s{\isadigit{1}}\ s{\isadigit{2}}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isacharparenright}\ s{\isadigit{1}}\ {\isacharequal}\ {\isacharparenleft}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isacharparenright}\ s{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}s{\isadigit{1}}\ {\isacharequal}\ s{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}nat{\isadigit{2}}list{\isacharbrackleft}of\ s{\isadigit{1}}{\isacharbrackright}\ sorted{\isacharunderscore}nat{\isadigit{2}}list{\isacharbrackleft}of\ s{\isadigit{2}}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}nat{\isadigit{2}}list{\isacharbrackleft}of\ s{\isadigit{1}}{\isacharbrackright}\ distinct{\isacharunderscore}nat{\isadigit{2}}list{\isacharbrackleft}of\ s{\isadigit{2}}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}distinct{\isacharunderscore}set{\isacharunderscore}unique{\isacharbrackleft}of\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ s{\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ s{\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}nat{\isadigit{2}}list\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ a\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ a{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ s{\isachardot}\ a\ {\isacharequal}\ {\isacharparenleft}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isacharparenright}\ s\ {\isasymand}\ True{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}list{\isadigit{2}}nat\ {\isacharparenleft}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ a{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}list{\isadigit{2}}nat{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
\ simp{\isacharunderscore}all%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isadelimML
\isanewline
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
{\isacharverbatimopen}\isanewline
\isanewline
{\isacharparenleft}{\isacharasterisk}\ Converts\ a\ term\ that\ represents\ a\ family\ {\isacharparenleft}set\ of\ sets{\isacharparenright}\ to\ a\ corresponding\ list\ of\ lists{\isachardot}\ If\ the\isanewline
term\ represents\ a\ list\ of\ families{\isacharcomma}\ then\ the\ the\ transformation\ is\ applied\ to\ each\ family\ in\ the\isanewline
list\ and\ the\ term\ that\ represents\ the\ corresponding\ list\ of\ lists\ of\ lists\ is\ returned{\isachardot}\ {\isacharasterisk}{\isacharparenright}\isanewline
\isanewline
fun\ sets{\isacharunderscore}to{\isacharunderscore}lists\ F\ {\isacharequal}\isanewline
\ \ let\isanewline
\ \ \ \ val\ c{\isadigit{1}}\ {\isacharequal}\ Const\ {\isacharparenleft}{\isachardoublequote}List{\isachardot}list{\isachardot}Cons{\isachardoublequote}{\isacharcomma}\ %
\isaantiq
typ\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequote}{}%
\endisaantiq
{\isacharparenright}\isanewline
\ \ \ \ val\ c{\isadigit{2}}\ {\isacharequal}\ Const\ {\isacharparenleft}{\isachardoublequote}Set{\isachardot}insert{\isachardoublequote}{\isacharcomma}\ %
\isaantiq
typ\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ set\ {\isasymRightarrow}\ nat\ set{\isachardoublequote}{}%
\endisaantiq
{\isacharparenright}\isanewline
\ \ \ \ val\ c{\isadigit{1}}{\isacharprime}\ {\isacharequal}\ Const\ {\isacharparenleft}{\isachardoublequote}List{\isachardot}list{\isachardot}Cons{\isachardoublequote}{\isacharcomma}\ %
\isaantiq
typ\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ nat\ list\ list\ {\isasymRightarrow}\ nat\ list\ list{\isachardoublequote}{}%
\endisaantiq
{\isacharparenright}\isanewline
\ \ \ \ val\ c{\isadigit{2}}{\isacharprime}\ {\isacharequal}\ Const\ {\isacharparenleft}{\isachardoublequote}Set{\isachardot}insert{\isachardoublequote}{\isacharcomma}\ %
\isaantiq
typ\ {\isachardoublequote}nat\ set\ {\isasymRightarrow}\ nat\ set\ set\ {\isasymRightarrow}\ nat\ set\ set{\isachardoublequote}{}%
\endisaantiq
{\isacharparenright}\isanewline
\ \ \ \ val\ c{\isadigit{3}}\ {\isacharequal}\ Const\ {\isacharparenleft}{\isachardoublequote}List{\isachardot}list{\isachardot}Cons{\isachardoublequote}{\isacharcomma}\ %
\isaantiq
typ\ {\isachardoublequote}nat\ set\ set\ {\isasymRightarrow}\ nat\ set\ set\ list\ {\isasymRightarrow}\ nat\ set\ set\ list{\isachardoublequote}{}%
\endisaantiq
{\isacharparenright}\isanewline
\ \ \ \ val\ c{\isadigit{3}}{\isacharprime}\ {\isacharequal}\ Const\ {\isacharparenleft}{\isachardoublequote}List{\isachardot}list{\isachardot}Cons{\isachardoublequote}{\isacharcomma}\ %
\isaantiq
typ\ {\isachardoublequote}nat\ list\ list\ {\isasymRightarrow}\ nat\ list\ list\ list\ {\isasymRightarrow}\ nat\ list\ list\ list{\isachardoublequote}{}%
\endisaantiq
{\isacharparenright}\isanewline
\ \ \ \ val\ sub{\isadigit{1}}\ {\isacharequal}\ {\isacharparenleft}c{\isadigit{2}}{\isacharcomma}\ c{\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ val\ sub{\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}c{\isadigit{2}}{\isacharprime}{\isacharcomma}\ c{\isadigit{1}}{\isacharprime}{\isacharparenright}\isanewline
\ \ \ \ val\ sub{\isadigit{3}}\ {\isacharequal}\ {\isacharparenleft}c{\isadigit{3}}{\isacharcomma}\ c{\isadigit{3}}{\isacharprime}{\isacharparenright}\isanewline
\ \ \ \ val\ sub{\isadigit{4}}\ {\isacharequal}\ {\isacharparenleft}%
\isaantiq
term\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isacharcolon}{\isacharcolon}nat\ set{\isachardoublequote}{}%
\endisaantiq
{\isacharcomma}\ %
\isaantiq
term\ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isacharcolon}{\isacharcolon}nat\ list{\isachardoublequote}{}%
\endisaantiq
{\isacharparenright}\isanewline
\ \ \ \ val\ sub{\isadigit{5}}\ {\isacharequal}\ {\isacharparenleft}%
\isaantiq
term\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isacharcolon}{\isacharcolon}nat\ set\ set{\isachardoublequote}{}%
\endisaantiq
{\isacharcomma}\ %
\isaantiq
term\ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isacharcolon}{\isacharcolon}nat\ list\ list{\isachardoublequote}{}%
\endisaantiq
{\isacharparenright}\isanewline
\ \ \ \ val\ sub{\isadigit{6}}\ {\isacharequal}\ {\isacharparenleft}%
\isaantiq
term\ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isacharcolon}{\isacharcolon}nat\ set\ set\ list{\isachardoublequote}{}%
\endisaantiq
{\isacharcomma}\ %
\isaantiq
term\ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isacharcolon}{\isacharcolon}nat\ list\ list\ list{\isachardoublequote}{}%
\endisaantiq
{\isacharparenright}\isanewline
\ \ in\isanewline
\ \ \ \ subst{\isacharunderscore}free\ {\isacharbrackleft}sub{\isadigit{1}}{\isacharcomma}\ sub{\isadigit{2}}{\isacharcomma}\ sub{\isadigit{3}}{\isacharcomma}\ sub{\isadigit{4}}{\isacharcomma}\ sub{\isadigit{5}}{\isacharcomma}\ sub{\isadigit{6}}{\isacharbrackright}\ F\isanewline
\ \ end{\isacharsemicolon}\isanewline
\isanewline
{\isacharparenleft}{\isacharasterisk}\ Given\ a\ term\ that\ represents\ a\ family\ returns\ a\ theorem\ stating\ that\ it\ is\ obtained\isanewline
by\ applying\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ to\ the\ corresponding\ list\ of\ list\ representation{\isachardot}\ \isanewline
E{\isachardot}g{\isachardot}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}thm\ %
\isaantiq
term\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceleft}{\isadigit{1}}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isacharbraceright}{\isacharcolon}{\isacharcolon}nat\ set\ set{\isachardoublequote}{}%
\endisaantiq
\ returns\isanewline
\ \ \ \ \ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceleft}{\isadigit{1}}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isacharbraceright}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharbrackleft}{\isacharbrackleft}{\isadigit{1}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}{\isacharbrackright}{\isachardoublequote}{\isacharcolon}\ thm\isanewline
{\isacharasterisk}{\isacharparenright}\isanewline
\isanewline
fun\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}thm\ F\ {\isacharequal}\isanewline
let\isanewline
\ \ \ \ fun\ mk{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}thm\ F\ {\isacharequal}\isanewline
\ \ \ \ let\ \isanewline
\ \ \ \ \ \ \ val\ term{\isacharunderscore}eq\ {\isacharequal}\ %
\isaantiq
term\ {\isachardoublequote}HOL{\isachardot}eq\ {\isacharcolon}{\isacharcolon}\ nat\ set\ set\ {\isasymRightarrow}\ \ nat\ set\ set\ {\isasymRightarrow}\ bool{\isachardoublequote}{}%
\endisaantiq
\isanewline
\ \ \ \ \ \ \ val\ term{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharequal}\ %
\isaantiq
term\ {\isachardoublequote}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharcolon}{\isacharcolon}\ nat\ list\ list\ {\isasymRightarrow}\ nat\ set\ set{\isachardoublequote}{}%
\endisaantiq
\isanewline
\ \ \ \ in\isanewline
\ \ \ \ \ \ \ HOLogic{\isachardot}mk{\isacharunderscore}Trueprop\ {\isacharparenleft}list{\isacharunderscore}comb\ {\isacharparenleft}term{\isacharunderscore}eq{\isacharcomma}\ {\isacharbrackleft}F{\isacharcomma}\ term{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set\ {\isachardollar}\ sets{\isacharunderscore}to{\isacharunderscore}lists\ F{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
\ \ \ \ end\isanewline
in\isanewline
\ \ Goal{\isachardot}prove\ %
\isaantiq
context{}%
\endisaantiq
\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}mk{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}thm\ F{\isacharparenright}\ {\isacharparenleft}fn\ {\isacharunderscore}\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}simp{\isacharunderscore}tac\ %
\isaantiq
context{}%
\endisaantiq
\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}\isanewline
end\isanewline
\isanewline
{\isacharparenleft}{\isacharasterisk}\ Similar\ as\ the\ previous\ one{\isacharcomma}\ except\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ is\ applied\ to\ every\ family\ i\ the\ given\isanewline
\ \ list{\isachardot}\isanewline
\ \ E{\isachardot}g{\isachardot}\ list{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}thm\ %
\isaantiq
term\ {\isachardoublequote}{\isacharbrackleft}{\isacharbraceleft}{\isacharbraceleft}{\isadigit{1}}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isadigit{2}}{\isacharbraceright}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{3}}{\isacharbraceright}{\isacharbraceright}{\isacharbrackright}{\isacharcolon}{\isacharcolon}nat\ set\ set\ list{\isachardoublequote}{}%
\endisaantiq
\ returns\isanewline
\ \ \ {\isachardoublequote}{\isacharbrackleft}{\isacharbraceleft}{\isacharbraceleft}{\isadigit{1}}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isadigit{2}}{\isacharbraceright}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{3}}{\isacharbraceright}{\isacharbraceright}{\isacharbrackright}\ {\isacharequal}\ map\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackleft}{\isadigit{1}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharbrackright}{\isacharbrackright}{\isachardoublequote}\ {\isacharcolon}\ thm\isanewline
{\isacharasterisk}{\isacharparenright}\isanewline
\isanewline
fun\ list{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}thm\ F\ {\isacharequal}\isanewline
let\isanewline
\ \ fun\ mk{\isacharunderscore}list{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}thm\ FF\ {\isacharequal}\isanewline
\ \ let\isanewline
\ \ \ \ \ val\ term{\isacharunderscore}eq\ {\isacharequal}\ %
\isaantiq
term\ {\isachardoublequote}HOL{\isachardot}eq\ {\isacharcolon}{\isacharcolon}\ nat\ set\ set\ list\ {\isasymRightarrow}\ \ nat\ set\ set\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}{}%
\endisaantiq
\isanewline
\ \ \ \ \ val\ term{\isacharunderscore}map{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharequal}\ %
\isaantiq
term\ {\isachardoublequote}map\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isacharcolon}{\isacharcolon}\ nat\ list\ list\ list\ {\isasymRightarrow}\ nat\ set\ set\ list{\isachardoublequote}{}%
\endisaantiq
\isanewline
\ \ in\isanewline
\ \ \ \ \ HOLogic{\isachardot}mk{\isacharunderscore}Trueprop\ {\isacharparenleft}list{\isacharunderscore}comb\ {\isacharparenleft}term{\isacharunderscore}eq{\isacharcomma}\ {\isacharbrackleft}FF{\isacharcomma}\ term{\isacharunderscore}map{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ {\isachardollar}\ sets{\isacharunderscore}to{\isacharunderscore}lists\ FF{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
\ \ end\isanewline
in\isanewline
\ \ Goal{\isachardot}prove\ %
\isaantiq
context{}%
\endisaantiq
\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}mk{\isacharunderscore}list{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}thm\ F{\isacharparenright}\ {\isacharparenleft}fn\ {\isacharunderscore}\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}simp{\isacharunderscore}tac\ %
\isaantiq
context{}%
\endisaantiq
\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}\isanewline
end\isanewline
\isanewline
{\isacharparenleft}{\isacharasterisk}\ Converts\ a\ term\ that\ represents\ a\ family\ {\isacharparenleft}set\ of\ sets{\isacharparenright}\ to\ a\ corresponding\ list\ of\ nats{\isachardot}\ {\isacharasterisk}{\isacharparenright}\isanewline
\isanewline
fun\ sets{\isacharunderscore}to{\isacharunderscore}nats\ t\ {\isacharequal}\ \isanewline
\ \ let\isanewline
\ \ \ \ val\ cons{\isacharunderscore}list\ {\isacharequal}\ Const\ {\isacharparenleft}{\isachardoublequote}List{\isachardot}list{\isachardot}Cons{\isachardoublequote}{\isacharcomma}\ %
\isaantiq
typ\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequote}{}%
\endisaantiq
{\isacharparenright}\isanewline
\ \ \ \ val\ insert{\isacharunderscore}list\ {\isacharequal}\ Const\ {\isacharparenleft}{\isachardoublequote}Set{\isachardot}insert{\isachardoublequote}{\isacharcomma}\ %
\isaantiq
typ\ {\isachardoublequote}nat\ set\ {\isasymRightarrow}\ nat\ set\ set\ {\isasymRightarrow}\ nat\ set\ set{\isachardoublequote}{}%
\endisaantiq
{\isacharparenright}\isanewline
\ \ in\isanewline
\ \ case\ t\ of\ insert{\isacharunderscore}list\ {\isachardollar}\ S\ {\isachardollar}\ L\ {\isacharequal}{\isachargreater}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ cons{\isacharunderscore}list\ {\isachardollar}\ {\isacharparenleft}%
\isaantiq
term\ {\isachardoublequote}list{\isadigit{2}}nat{\isachardoublequote}{}%
\endisaantiq
\ {\isachardollar}\ sets{\isacharunderscore}to{\isacharunderscore}lists\ S{\isacharparenright}\ {\isachardollar}\ sets{\isacharunderscore}to{\isacharunderscore}nats\ L\ \isanewline
\ \ \ \ \ \ \ \ \ \ {\isacharbar}\ %
\isaantiq
term\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isacharcolon}{\isacharcolon}nat\ set\ set{\isachardoublequote}{}%
\endisaantiq
\ {\isacharequal}{\isachargreater}\ %
\isaantiq
term\ {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isacharcolon}{\isacharcolon}\ nat\ list{\isachardoublequote}{}%
\endisaantiq
\isanewline
\ \ \ \ \ \ \ \ \ \ {\isacharbar}\ {\isacharunderscore}\ {\isacharequal}{\isachargreater}\ raise\ Fail\ {\isacharparenleft}{\isachardoublequote}pattern\ not\ matched{\isachardoublequote}{\isacharparenright}\isanewline
\ \ end\isanewline
\isanewline
{\isacharparenleft}{\isacharasterisk}\ Given\ a\ term\ that\ represents\ a\ family\ returns\ a\ theorem\ stating\ that\ it\ is\ obtained\isanewline
by\ applying\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}n\ to\ the\ corresponding\ list\ of\ nats\ representation{\isachardot}\ \isanewline
E{\isachardot}g{\isachardot}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}n{\isacharunderscore}thm\ %
\isaantiq
term\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceleft}{\isadigit{1}}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isacharbraceright}{\isacharcolon}{\isacharcolon}nat\ set\ set{\isachardoublequote}{}%
\endisaantiq
\ returns\isanewline
\ \ \ \ \ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceleft}{\isadigit{1}}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isacharbraceright}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}n\ {\isacharbrackleft}list{\isadigit{2}}nat\ {\isacharbrackleft}{\isadigit{1}}{\isacharbrackright}{\isacharcomma}\ list{\isadigit{2}}nat\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}{\isacharbrackright}{\isachardoublequote}{\isacharcolon}\ thm\isanewline
{\isacharasterisk}{\isacharparenright}\isanewline
\isanewline
fun\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}n{\isacharunderscore}thm\ F\ {\isacharequal}\isanewline
let\isanewline
\ \ \ \ fun\ mk{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}n{\isacharunderscore}thm\ F\ {\isacharequal}\isanewline
\ \ \ \ let\ \isanewline
\ \ \ \ \ \ \ val\ term{\isacharunderscore}eq\ {\isacharequal}\ %
\isaantiq
term\ {\isachardoublequote}HOL{\isachardot}eq\ {\isacharcolon}{\isacharcolon}\ nat\ set\ set\ {\isasymRightarrow}\ \ nat\ set\ set\ {\isasymRightarrow}\ bool{\isachardoublequote}{}%
\endisaantiq
\isanewline
\ \ \ \ \ \ \ val\ term{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharequal}\ %
\isaantiq
term\ {\isachardoublequote}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}n\ {\isacharcolon}{\isacharcolon}\ nat\ list\ \ {\isasymRightarrow}\ nat\ set\ set{\isachardoublequote}{}%
\endisaantiq
\isanewline
\ \ \ \ in\isanewline
\ \ \ \ \ \ \ HOLogic{\isachardot}mk{\isacharunderscore}Trueprop\ {\isacharparenleft}list{\isacharunderscore}comb\ {\isacharparenleft}term{\isacharunderscore}eq{\isacharcomma}\ {\isacharbrackleft}F{\isacharcomma}\ term{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set\ {\isachardollar}\ sets{\isacharunderscore}to{\isacharunderscore}nats\ F{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
\ \ \ \ end\isanewline
\ \ \ \ val\ ss\ {\isacharequal}\ put{\isacharunderscore}simpset\ HOL{\isacharunderscore}ss\ %
\isaantiq
context{}%
\endisaantiq
\ addsimps\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isacharbrackleft}%
\isaantiq
thm\ nat{\isadigit{2}}list{\isacharunderscore}list{\isadigit{2}}nat{}%
\endisaantiq
{\isacharcomma}\ %
\isaantiq
thm\ SetImpl{\isacharunderscore}nats{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}def{}%
\endisaantiq
{\isacharbrackright}\ {\isacharat}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ %
\isaantiq
thms\ List{\isachardot}list{\isachardot}map{}%
\endisaantiq
\ {\isacharat}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbrackleft}%
\isaantiq
thm\ comp{\isacharunderscore}apply{}%
\endisaantiq
{\isacharbrackright}\ {\isacharat}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ %
\isaantiq
thms\ distinct{\isachardot}simps{}%
\endisaantiq
\ {\isacharat}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ %
\isaantiq
thms\ List{\isachardot}list{\isachardot}set{}%
\endisaantiq
\ {\isacharat}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbrackleft}%
\isaantiq
thm\ empty{\isacharunderscore}iff{}%
\endisaantiq
{\isacharcomma}\ %
\isaantiq
thm\ insert{\isacharunderscore}iff{}%
\endisaantiq
{\isacharbrackright}\ {\isacharat}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ %
\isaantiq
thms\ eq{\isacharunderscore}numeral{\isacharunderscore}simps{}%
\endisaantiq
\ {\isacharat}\ {\isacharbrackleft}%
\isaantiq
thm\ zero{\isacharunderscore}neq{\isacharunderscore}one{}%
\endisaantiq
{\isacharbrackright}\ {\isacharat}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ %
\isaantiq
thms\ Num{\isachardot}num{\isachardot}distinct{}%
\endisaantiq
\ {\isacharat}\ %
\isaantiq
thms\ num{\isachardot}inject{}%
\endisaantiq
\ {\isacharat}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbrackleft}%
\isaantiq
thm\ sorted{\isachardot}Nil{}%
\endisaantiq
{\isacharcomma}\ %
\isaantiq
thm\ sorted{\isacharunderscore}single{}%
\endisaantiq
{\isacharcomma}\ %
\isaantiq
thm\ sorted{\isacharunderscore}many{}%
\endisaantiq
{\isacharbrackright}\ {\isacharat}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ %
\isaantiq
thms\ le{\isacharunderscore}numeral{\isacharunderscore}simps{}%
\endisaantiq
\ {\isacharat}\ %
\isaantiq
thms\ le{\isacharunderscore}num{\isacharunderscore}simps{}%
\endisaantiq
\ {\isacharat}\ %
\isaantiq
thms\ less{\isacharunderscore}num{\isacharunderscore}simps{}%
\endisaantiq
\ {\isacharat}\ {\isacharbrackleft}%
\isaantiq
thm\ le{\isadigit{0}}{}%
\endisaantiq
{\isacharbrackright}{\isacharparenright}\isanewline
in\isanewline
\ \ Goal{\isachardot}prove\ %
\isaantiq
context{}%
\endisaantiq
\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}mk{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}n{\isacharunderscore}thm\ F{\isacharparenright}\ {\isacharparenleft}fn\ {\isacharunderscore}\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}asm{\isacharunderscore}full{\isacharunderscore}simp{\isacharunderscore}tac\ ss\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}\isanewline
end\isanewline
{\isacharverbatimclose}%
\endisatagML
{\isafoldML}%
%
\isadelimML
\isanewline
%
\endisadelimML
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
