%
\begin{isabellebody}%
\setisabellecontext{Combinatorics}%
%
\isamarkupsection{Combinatorics%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Combinatorics\isanewline
\isakeyword{imports}\ Main\isanewline
\ \ {\isachardoublequoteopen}HOL{\isacharminus}Library{\isachardot}Permutation{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}HOL{\isacharminus}Library{\isachardot}List{\isacharunderscore}lexord{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}More{\isachardot}MoreList{\isachardoublequoteclose}\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsubsection{Generating all permutations%
}
\isamarkuptrue%
\isacommand{primrec}\isamarkupfalse%
\ interleave\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}interleave\ x\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackleft}x{\isacharbrackright}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}interleave\ x\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isacharhash}\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ l{\isachardot}\ h\ {\isacharhash}\ l{\isacharparenright}\ {\isacharparenleft}interleave\ x\ t{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
For example, \isa{interleave\ {\isadigit{1}}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{4}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}{\isacharbrackright}}.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{primrec}\isamarkupfalse%
\ permute\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}permute\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}permute\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ {\isacharequal}\ concat\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ l{\isachardot}\ interleave\ h\ l{\isacharparenright}\ {\isacharparenleft}permute\ t{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
For example, \isa{permute\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{3}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{3}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{1}}{\isacharbrackright}{\isacharbrackright}}.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ multiset{\isacharunderscore}interleave{\isacharcolon}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}p\ {\isasymin}\ set\ {\isacharparenleft}interleave\ h\ a{\isacharparenright}\ {\isasymLongrightarrow}\ mset\ p\ {\isacharequal}\ mset\ a\ {\isacharplus}\ {\isacharbraceleft}{\isacharhash}h{\isacharhash}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ a\ arbitrary{\isacharcolon}\ p{\isacharparenright}\ \isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ h{\isacharprime}\ t{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ add{\isachardot}commute{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharhash}h{\isacharhash}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharhash}h{\isacharprime}{\isacharhash}{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ add{\isachardot}assoc\ {\isacharbrackleft}of\ {\isachardoublequoteopen}mset\ t{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharhash}h{\isacharhash}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharhash}h{\isacharprime}{\isacharhash}{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ add{\isachardot}assoc\ {\isacharbrackleft}of\ {\isachardoublequoteopen}mset\ t{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharhash}h{\isacharprime}{\isacharhash}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharhash}h{\isacharhash}{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ interleave{\isacharunderscore}hd\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}h\ {\isacharhash}\ t\ {\isasymin}\ set\ {\isacharparenleft}interleave\ h\ t{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}t{\isachardoublequoteclose}{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ interleave{\isacharunderscore}append\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}t{\isadigit{1}}\ {\isacharat}\ {\isacharbrackleft}h{\isacharbrackright}\ {\isacharat}\ t{\isadigit{2}}\ {\isasymin}\ set\ {\isacharparenleft}interleave\ h\ {\isacharparenleft}t{\isadigit{1}}\ {\isacharat}\ t{\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ t{\isadigit{1}}{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ isPermutation{\isacharunderscore}permute{\isacharcolon}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}p\ {\isasymin}\ set\ {\isacharparenleft}permute\ l{\isacharparenright}\ {\isasymLongrightarrow}\ p\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ arbitrary{\isacharcolon}\ p{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ mset{\isacharunderscore}eq{\isacharunderscore}perm{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ h\ t{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mset{\isacharunderscore}eq{\isacharunderscore}perm{\isacharbrackleft}THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ multiset{\isacharunderscore}interleave{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ mset{\isacharunderscore}append{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}mset\ p\ {\isacharequal}\ mset\ t\ {\isacharplus}\ {\isacharbraceleft}{\isacharhash}h{\isacharhash}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ t{\isadigit{1}}\ t{\isadigit{2}}{\isachardot}\ p\ {\isacharequal}\ t{\isadigit{1}}\ {\isacharat}\ {\isacharbrackleft}h{\isacharbrackright}\ {\isacharat}\ t{\isadigit{2}}\ {\isasymand}\ mset\ t\ {\isacharequal}\ mset\ t{\isadigit{1}}\ {\isacharplus}\ mset\ t{\isadigit{2}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ p\ arbitrary{\isacharcolon}\ t{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ a\ p{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}a\ {\isacharequal}\ h{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}h\ {\isasymin}{\isacharhash}\ mset\ p{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ insert{\isacharunderscore}noteq{\isacharunderscore}member{\isacharbrackleft}of\ a\ {\isachardoublequoteopen}mset\ p{\isacharprime}{\isachardoublequoteclose}{\isacharbrackright}\ \isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}mset\ p{\isacharprime}\ {\isacharequal}\ mset\ p{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}{\isacharhash}h{\isacharhash}{\isacharbraceright}\ {\isacharplus}\ {\isacharbraceleft}{\isacharhash}h{\isacharhash}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ insert{\isacharunderscore}DiffM{\isadigit{2}}{\isacharbrackleft}of\ h\ {\isachardoublequoteopen}mset\ p{\isacharprime}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ {\isachardoublequoteopen}remove{\isadigit{1}}\ h\ p{\isacharprime}{\isachardoublequoteclose}{\isacharbrackright}\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto{\isacharcomma}\ rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}a{\isacharhash}t{\isadigit{1}}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ auto{\isacharparenright}\ \isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ permute{\isacharunderscore}isPermutation{\isacharcolon}\ \isanewline
\ \ {\isachardoublequoteopen}p\ {\isacharless}{\isachartilde}{\isachartilde}{\isachargreater}\ l\ {\isasymLongrightarrow}\ p\ {\isasymin}\ set\ {\isacharparenleft}permute\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ arbitrary{\isacharcolon}\ p{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ h\ t{\isacharparenright}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ t{\isadigit{1}}\ t{\isadigit{2}}\ \isakeyword{where}\ {\isachardoublequoteopen}p\ {\isacharequal}\ t{\isadigit{1}}\ {\isacharat}\ {\isacharbrackleft}h{\isacharbrackright}\ {\isacharat}\ t{\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}mset\ t\ {\isacharequal}\ mset\ t{\isadigit{1}}\ {\isacharplus}\ mset\ t{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mset{\isacharunderscore}eq{\isacharunderscore}perm{\isacharbrackleft}THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ mset{\isacharunderscore}append{\isacharbrackleft}of\ p\ t\ h{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ {\isachardoublequoteopen}t{\isadigit{1}}\ {\isacharat}\ t{\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ add{\isachardot}assoc\ {\isacharbrackleft}of\ {\isachardoublequoteopen}mset\ t{\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}mset\ t{\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharhash}h{\isacharhash}{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ interleave{\isacharunderscore}append{\isacharbrackleft}of\ t{\isadigit{1}}\ h\ t{\isadigit{2}}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mset{\isacharunderscore}eq{\isacharunderscore}perm{\isacharbrackleft}THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ permute{\isacharunderscore}bij{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}p\ {\isasymin}\ set\ {\isacharparenleft}permute\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ f{\isachardot}\ bij{\isacharunderscore}betw\ f\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}length\ p{\isacharbraceright}\ {\isacharbraceleft}{\isachardot}{\isachardot}{\isacharless}length\ l{\isacharbraceright}\ {\isasymand}\isanewline
\ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}\ i{\isacharless}length\ p{\isachardot}\ p\ {\isacharbang}\ i\ {\isacharequal}\ l\ {\isacharbang}\ {\isacharparenleft}f\ i{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ isPermutation{\isacharunderscore}permute{\isacharbrackleft}of\ p\ l{\isacharbrackright}\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ permutation{\isacharunderscore}Ex{\isacharunderscore}bij{\isacharbrackleft}of\ p\ l{\isacharbrackright}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Generating all combinations%
}
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ combine{\isacharunderscore}aux\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}combine{\isacharunderscore}aux\ l\ n\ k\ {\isacharequal}\ \isanewline
\ \ \ \ \ {\isacharparenleft}if\ k\ {\isacharequal}\ {\isadigit{0}}\ then\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}\ else\ \isanewline
\ \ \ \ \ \ if\ k\ {\isacharequal}\ n\ then\ {\isacharbrackleft}l{\isacharbrackright}\ else\isanewline
\ \ \ \ \ \ {\isacharparenleft}case\ l\ of\ \isanewline
\ \ \ \ \ \ \ \ \ \ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
\ \ \ \ \ \ {\isacharbar}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ {\isasymRightarrow}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ l{\isacharprime}{\isachardot}\ h\ {\isacharhash}\ l{\isacharprime}{\isacharparenright}\ {\isacharparenleft}combine{\isacharunderscore}aux\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}k{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharat}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ combine{\isacharunderscore}aux\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ k{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{declare}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isacharunderscore}induct{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \isanewline
\ \ {\isachardoublequoteopen}{\isasymAnd}\ l\ n{\isachardot}\ P\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}\ l\ n\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymAnd}\ l\ n{\isachardot}\ {\isadigit{0}}\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ {\isacharbrackleft}l{\isacharbrackright}\ l\ n\ n{\isachardoublequoteclose}\ \isanewline
\ \ {\isachardoublequoteopen}{\isasymAnd}\ k\ n{\isachardot}\ {\isasymlbrakk}{\isadigit{0}}\ {\isacharless}\ k{\isacharsemicolon}\ k\ {\isasymnoteq}\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}\ n\ k{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymAnd}\ h\ t\ n\ k{\isachardot}\ {\isasymlbrakk}\isanewline
\ \ \ \ \ P\ {\isacharparenleft}combine{\isacharunderscore}aux\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}k{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isacharparenright}\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}k{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
\ \ \ \ \ P\ {\isacharparenleft}combine{\isacharunderscore}aux\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ k{\isacharparenright}\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ \isanewline
\ \ \ \ \ P\ {\isacharparenleft}map\ {\isacharparenleft}op\ {\isacharhash}\ h{\isacharparenright}\ {\isacharparenleft}combine{\isacharunderscore}aux\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}k{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharat}\isanewline
\ \ \ \ \ \ \ \ \ \ combine{\isacharunderscore}aux\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ k{\isacharparenright}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ n\ k{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}P\ {\isacharparenleft}combine{\isacharunderscore}aux\ l\ n\ k{\isacharparenright}\ l\ n\ k{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ n\ k\ rule{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ l\ n\ k{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k{\isacharequal}{\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k\ {\isacharequal}\ n{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}l\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ h\ t\ \isakeyword{where}\ {\isachardoublequoteopen}l\ {\isacharequal}\ h\ {\isacharhash}\ t{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ neq{\isacharunderscore}Nil{\isacharunderscore}conv{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}l{\isadigit{1}}\ {\isacharequal}\ {\isachardoublequoteopen}combine{\isacharunderscore}aux\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}k{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}l{\isadigit{2}}\ {\isacharequal}\ {\isachardoublequoteopen}combine{\isacharunderscore}aux\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}P\ {\isacharquery}l{\isadigit{1}}\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}k{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ h\ t{\isacharbrackright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharminus}{\isadigit{6}}{\isacharparenright}\ \ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\ {\isacharbackquoteopen}l\ {\isacharequal}\ h\ {\isacharhash}\ t{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}P\ {\isacharquery}l{\isadigit{2}}\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharbrackleft}of\ h\ t{\isacharbrackright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharminus}{\isadigit{6}}{\isacharparenright}\ \ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\ {\isacharbackquoteopen}l\ {\isacharequal}\ h\ {\isacharhash}\ t{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}l\ {\isacharequal}\ h\ {\isacharhash}\ t{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ l\ n\ k{\isacharbrackright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{6}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ combine\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ list{\isachardoublequoteclose}\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}combine\ l\ k\ {\isacharequal}\ combine{\isacharunderscore}aux\ l\ {\isacharparenleft}length\ l{\isacharparenright}\ k{\isachardoublequoteclose}%
\begin{isamarkuptext}%
For example, \isa{combine\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}\ {\isadigit{2}}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharbrackright}}.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isacharunderscore}subset{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ A{\isachardot}\ A\ {\isasymin}\ set\ {\isacharparenleft}combine{\isacharunderscore}aux\ l\ n\ k{\isacharparenright}\ {\isasymlongrightarrow}\ set\ A\ {\isasymsubseteq}\ set\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ combine{\isacharunderscore}aux{\isacharunderscore}induct{\isacharparenright}\ {\isacharparenleft}auto{\isacharcomma}\ force{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ combine{\isacharunderscore}subset{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}combine\ l\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set\ A\ {\isasymsubseteq}\ set\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isacharunderscore}subset{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ of\ A\ l\ {\isachardoublequoteopen}length\ l{\isachardoublequoteclose}\ k{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ combine{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isacharunderscore}sublist{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ A{\isachardot}\ A\ {\isasymsubseteq}\ set\ L\ {\isasymand}\ n\ {\isacharequal}\ length\ L\ {\isasymand}\ m\ {\isacharequal}\ card\ A\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}x{\isasymin}set\ {\isacharparenleft}combine{\isacharunderscore}aux\ L\ n\ m{\isacharparenright}{\isachardot}\ A\ {\isacharequal}\ set\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ combine{\isacharunderscore}aux{\isacharunderscore}induct{\isacharbrackleft}\isakeyword{where}\ P\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ c\ l\ n\ m{\isachardot}\ {\isacharparenleft}{\isasymforall}\ A{\isachardot}\ A\ {\isasymsubseteq}\ set\ l\ {\isasymand}\ n\ {\isacharequal}\ length\ l\ {\isasymand}\ m\ {\isacharequal}\ card\ A\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}x\ {\isasymin}\ set\ c{\isachardot}\ A\ {\isacharequal}\ set\ x{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ l\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{and}\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}A{\isachardot}\ A\ {\isasymsubseteq}\ set\ l\ {\isasymand}\ n\ {\isacharequal}\ length\ l\ {\isasymand}\ {\isadigit{0}}\ {\isacharequal}\ card\ A\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}x{\isasymin}set\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}{\isachardot}\ A\ {\isacharequal}\ set\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ card{\isacharunderscore}eq{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}iff\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ l\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{and}\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}n\ {\isachargreater}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}A{\isachardot}\ A\ {\isasymsubseteq}\ set\ l\ {\isasymand}\ n\ {\isacharequal}\ length\ l\ {\isasymand}\ n\ {\isacharequal}\ card\ A\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}x{\isasymin}set\ {\isacharbrackleft}l{\isacharbrackright}{\isachardot}\ A\ {\isacharequal}\ set\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ subset{\isacharunderscore}card{\isacharunderscore}length\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ h\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{and}\ t\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{and}\ n\ {\isacharcolon}{\isacharcolon}\ nat\ \isakeyword{and}\ k\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}l{\isadigit{1}}\ {\isacharequal}\ {\isachardoublequoteopen}combine{\isacharunderscore}aux\ t\ {\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}k\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ {\isacharquery}l{\isadigit{2}}\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharparenleft}combine{\isacharunderscore}aux\ t\ {\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}A{\isachardot}\ A\ {\isasymsubseteq}\ set\ t\ {\isasymand}\ n\ {\isacharminus}\ {\isadigit{1}}\ {\isacharequal}\ length\ t\ {\isasymand}\ k\ {\isacharminus}\ {\isadigit{1}}\ {\isacharequal}\ card\ A\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}x{\isasymin}set\ {\isacharquery}l{\isadigit{1}}{\isachardot}\ A\ {\isacharequal}\ set\ x{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ {\isacharasterisk}{\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}A{\isachardot}\ A\ {\isasymsubseteq}\ set\ t\ {\isasymand}\ n\ {\isacharminus}\ {\isadigit{1}}\ {\isacharequal}\ length\ t\ {\isasymand}\ k\ {\isacharequal}\ card\ A\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}x{\isasymin}set\ {\isacharquery}l{\isadigit{2}}{\isachardot}\ A\ {\isacharequal}\ set\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}A{\isachardot}\ A\ {\isasymsubseteq}\ set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ {\isasymand}\ n\ {\isacharequal}\ length\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ {\isasymand}\ k\ {\isacharequal}\ card\ A\ {\isasymlongrightarrow}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}x{\isasymin}set\ {\isacharparenleft}map\ {\isacharparenleft}op\ {\isacharhash}\ h{\isacharparenright}\ {\isacharparenleft}{\isacharquery}l{\isadigit{1}}{\isacharparenright}\ {\isacharat}\ {\isacharquery}l{\isadigit{2}}{\isacharparenright}{\isachardot}\ A\ {\isacharequal}\ set\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ allI{\isacharcomma}\ rule\ impI{\isacharcomma}\ {\isacharparenleft}erule\ conjE{\isacharparenright}{\isacharplus}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A{\isacharprime}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymsubseteq}\ set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}n\ {\isacharequal}\ length\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}k\ {\isacharequal}\ card\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}x{\isasymin}set\ {\isacharparenleft}map\ {\isacharparenleft}op\ {\isacharhash}\ h{\isacharparenright}\ {\isacharparenleft}{\isacharquery}l{\isadigit{1}}{\isacharparenright}\ {\isacharat}\ {\isacharquery}l{\isadigit{2}}{\isacharparenright}{\isachardot}\ A{\isacharprime}\ {\isacharequal}\ set\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}h\ {\isasymin}\ A{\isacharprime}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymsubseteq}\ set\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymsubseteq}\ set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ of\ A{\isacharprime}{\isacharbrackright}\ {\isacharbackquoteopen}n\ {\isacharequal}\ length\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isacharequal}\ card\ A{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}x{\isasymin}set\ {\isacharquery}l{\isadigit{1}}{\isachardot}\ {\isacharparenleft}A{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}h{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ set\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ of\ {\isachardoublequoteopen}A{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}h{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\ \ {\isacharbackquoteopen}n\ {\isacharequal}\ length\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isacharequal}\ card\ A{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymsubseteq}\ set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}Diff{\isacharunderscore}singleton{\isacharbrackleft}of\ A{\isacharprime}\ h{\isacharbrackright}\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ A{\isacharprime}\ {\isachardoublequoteopen}set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ x\ \isakeyword{where}\ {\isachardoublequoteopen}x{\isasymin}set\ {\isacharquery}l{\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}A{\isacharprime}\ {\isacharminus}\ {\isacharbraceleft}h{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ set\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}h\ {\isasymin}\ A{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}h\ {\isacharhash}\ x{\isachardoublequoteclose}\ \isakeyword{in}\ bexI{\isacharparenright}\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ combine{\isacharunderscore}sublist{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ set\ L{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}x{\isasymin}set\ {\isacharparenleft}combine\ L\ {\isacharparenleft}card\ A{\isacharparenright}{\isacharparenright}{\isachardot}\ A\ {\isacharequal}\ set\ x{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isacharunderscore}sublist{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ of\ A\ L\ {\isachardoublequoteopen}length\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ A{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ combine{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isacharunderscore}combines{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sorted\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}n\ {\isacharequal}\ length\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}combine{\isacharunderscore}aux\ l\ n\ k{\isacharparenright}\ {\isasymlongleftrightarrow}\ sorted\ A\ {\isasymand}\ distinct\ A\ {\isasymand}\ length\ A\ {\isacharequal}\ k\ {\isasymand}\ set\ A\ {\isasymsubseteq}\ set\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\ \isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ n\ k\ \ arbitrary{\isacharcolon}\ A\ rule{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ l\ n\ k{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k\ {\isacharequal}\ n{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}sorted\ l{\isacharbackquoteclose}\ {\isacharbackquoteopen}distinct\ l{\isacharbackquoteclose}\ {\isacharbackquoteopen}n\ {\isacharequal}\ length\ l{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}card{\isacharbrackleft}of\ l{\isacharbrackright}\ distinct{\isacharunderscore}card{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}seteq{\isacharbrackleft}of\ {\isachardoublequoteopen}set\ l{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ A{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}distinct{\isacharunderscore}set{\isacharunderscore}unique{\isacharbrackleft}of\ A\ l{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}l\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ h\ t\ \isakeyword{where}\ {\isachardoublequoteopen}l\ {\isacharequal}\ h\ {\isacharhash}\ t{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ neq{\isacharunderscore}Nil{\isacharunderscore}conv{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}l{\isadigit{1}}\ {\isacharequal}\ {\isachardoublequoteopen}combine{\isacharunderscore}aux\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}k{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}l{\isadigit{2}}\ {\isacharequal}\ {\isachardoublequoteopen}combine{\isacharunderscore}aux\ t\ {\isacharparenleft}n{\isacharminus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sorted\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isacharbackquoteopen}l\ {\isacharequal}\ h\ {\isacharhash}\ t{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sorted{\isacharunderscore}Cons{\isacharparenright}\isanewline
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}combine{\isacharunderscore}aux\ l\ n\ k{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}A\ {\isasymin}\ set\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ l{\isacharprime}{\isachardot}\ h\ {\isacharhash}\ l{\isacharprime}{\isacharparenright}\ {\isacharquery}l{\isadigit{1}}{\isacharparenright}\ {\isasymor}\ A\ {\isasymin}\ set\ {\isacharquery}l{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\ {\isacharbackquoteopen}l\ {\isacharequal}\ h\ {\isacharhash}\ t{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharquery}l{\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}sorted\ A\ {\isasymand}\ distinct\ A\ {\isasymand}\ length\ A\ {\isacharequal}\ k\ {\isasymand}\ set\ A\ {\isasymsubseteq}\ set\ t{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharbrackleft}of\ h\ t\ A{\isacharbrackright}\ \ \ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\ {\isacharbackquoteopen}l\ {\isacharequal}\ h\ {\isacharhash}\ t{\isacharbackquoteclose}\ {\isacharbackquoteopen}sorted\ t{\isacharbackquoteclose}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ l{\isacharprime}{\isachardot}\ h\ {\isacharhash}\ l{\isacharprime}{\isacharparenright}\ {\isacharquery}l{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}sorted\ A\ {\isasymand}\ distinct\ A\ {\isasymand}\ length\ A\ {\isacharequal}\ k\ {\isasymand}\ {\isasymnot}\ set\ A\ {\isasymsubseteq}\ set\ t\ {\isasymand}\ set\ A\ {\isasymsubseteq}\ set\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}tl\ A\ {\isasymin}\ set\ {\isacharquery}l{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}sorted\ {\isacharparenleft}tl\ A{\isacharparenright}\ {\isasymand}\ distinct\ {\isacharparenleft}tl\ A{\isacharparenright}\ {\isasymand}\ length\ {\isacharparenleft}tl\ A{\isacharparenright}\ {\isacharequal}\ k\ {\isacharminus}\ {\isadigit{1}}\ {\isasymand}\ set\ {\isacharparenleft}tl\ A{\isacharparenright}\ {\isasymsubseteq}\ set\ t{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ h\ t\ {\isachardoublequoteopen}tl\ A{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}l\ {\isacharequal}\ h\ {\isacharhash}\ t{\isacharbackquoteclose}\ {\isacharbackquoteopen}sorted\ t{\isacharbackquoteclose}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ l{\isacharprime}{\isachardot}\ h\ {\isacharhash}\ l{\isacharprime}{\isacharparenright}\ {\isacharquery}l{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}A\ {\isacharequal}\ h\ {\isacharhash}\ {\isacharparenleft}tl\ A{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}tl\ A\ {\isasymin}\ set\ {\isacharquery}l{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ set\ t{\isachardot}\ h\ {\isasymle}\ x{\isachardoublequoteclose}\ {\isachardoublequoteopen}h\ {\isasymnotin}\ set\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sorted\ l{\isacharbackquoteclose}\ {\isacharbackquoteopen}distinct\ l{\isacharbackquoteclose}\ {\isacharbackquoteopen}l\ {\isacharequal}\ h\ {\isacharhash}\ t{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sorted{\isacharunderscore}Cons{\isacharparenright}\isanewline
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}A\ {\isacharequal}\ h\ {\isacharhash}\ tl\ A\ {\isasymand}\ sorted\ {\isacharparenleft}tl\ A{\isacharparenright}\ {\isasymand}\ distinct\ {\isacharparenleft}tl\ A{\isacharparenright}\ {\isasymand}\ length\ A\ {\isacharminus}\ {\isadigit{1}}\ {\isacharequal}\ k\ {\isacharminus}\ {\isadigit{1}}\ {\isasymand}\ set\ {\isacharparenleft}tl\ A{\isacharparenright}\ {\isasymsubseteq}\ set\ t{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}sorted\ A\ {\isasymand}\ distinct\ A\ {\isasymand}\ length\ A\ {\isacharequal}\ k\ {\isasymand}\ {\isasymnot}\ set\ A\ {\isasymsubseteq}\ set\ t\ {\isasymand}\ set\ A\ {\isasymsubseteq}\ insert\ h\ {\isacharparenleft}set\ t{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isacharequal}\ {\isacharquery}rhs{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ iffI{\isacharcomma}\ {\isacharparenleft}erule{\isacharunderscore}tac{\isacharbrackleft}{\isacharbang}{\isacharbrackright}\ conjE{\isacharparenright}{\isacharplus}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isacharequal}\ h\ {\isacharhash}\ tl\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}sorted\ {\isacharparenleft}tl\ A{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}tl\ A{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}length\ A\ {\isacharminus}\ {\isadigit{1}}\ {\isacharequal}\ k\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ {\isacharparenleft}tl\ A{\isacharparenright}\ {\isasymsubseteq}\ set\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}rhs\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ A\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ A\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isacharequal}\ h\ {\isacharhash}\ tl\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ A\ {\isacharminus}\ {\isadigit{1}}\ {\isacharequal}\ k\ {\isacharminus}\ {\isadigit{1}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}length\ A\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ arith\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}sorted\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharbackquoteopen}A\ {\isacharequal}\ h\ {\isacharhash}\ tl\ A{\isacharbackquoteclose}{\isacharcomma}\ subst\ sorted{\isacharunderscore}Cons{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sorted\ {\isacharparenleft}tl\ A{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}set\ {\isacharparenleft}tl\ A{\isacharparenright}\ {\isasymsubseteq}\ set\ t{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ x\ {\isasymin}\ set\ t{\isachardot}\ h\ {\isasymle}\ x{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharbackquoteopen}A\ {\isacharequal}\ h\ {\isacharhash}\ tl\ A{\isacharbackquoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ {\isacharparenleft}tl\ A{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}h\ {\isasymnotin}\ set\ t{\isacharbackquoteclose}\ {\isacharbackquoteopen}set\ {\isacharparenleft}tl\ A{\isacharparenright}\ {\isasymsubseteq}\ set\ t{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ A\ {\isasymsubseteq}\ set\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}False{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ {\isacharbackquoteopen}A\ {\isacharequal}\ h\ {\isacharhash}\ tl\ A{\isacharbackquoteclose}{\isacharparenright}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}h\ {\isasymnotin}\ set\ t{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymnotin}\ set\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isacharequal}\ h{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ {\isacharbackquoteopen}A\ {\isacharequal}\ h\ {\isacharhash}\ tl\ A{\isacharbackquoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}set\ {\isacharparenleft}tl\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharparenleft}set\ t{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}sorted\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}length\ A\ {\isacharequal}\ k{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymnot}\ set\ A\ {\isasymsubseteq}\ set\ t{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ A\ {\isasymsubseteq}\ insert\ h\ {\isacharparenleft}set\ t{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}sorted\ {\isacharparenleft}tl\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sorted\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ linorder{\isacharunderscore}class{\isachardot}sorted{\isacharunderscore}tl{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}tl\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ distinct{\isacharunderscore}tl{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isacharequal}\ h\ {\isacharhash}\ tl\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}h\ {\isasymin}\ set\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ set\ A\ {\isasymsubseteq}\ set\ t{\isacharbackquoteclose}\ {\isacharbackquoteopen}set\ A\ {\isasymsubseteq}\ insert\ h\ {\isacharparenleft}set\ t{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isacharequal}\ hd\ A\ {\isacharhash}\ tl\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}hd\ A\ {\isacharequal}\ h{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}h\ {\isasymin}\ set\ A{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}h\ {\isacharequal}\ hd\ A\ {\isasymor}\ h\ {\isasymin}\ set\ {\isacharparenleft}tl\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ {\isacharbackquoteopen}A\ {\isacharequal}\ hd\ A\ {\isacharhash}\ tl\ A{\isacharbackquoteclose}{\isacharparenright}\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}h\ {\isasymin}\ set\ {\isacharparenleft}tl\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}hd\ A\ {\isasymnoteq}\ h{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}hd\ A\ {\isacharless}\ h{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}sorted\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ {\isacharbackquoteopen}A\ {\isacharequal}\ hd\ A\ {\isacharhash}\ tl\ A{\isacharbackquoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}h\ {\isasymin}\ set\ {\isacharparenleft}tl\ A{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}hd\ A\ {\isasymnoteq}\ h{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sorted{\isacharunderscore}Cons{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}hd\ A\ {\isasymin}\ set\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}set\ A\ {\isasymsubseteq}\ insert\ h\ {\isacharparenleft}set\ t{\isacharparenright}{\isacharbackquoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ {\isacharbackquoteopen}A\ {\isacharequal}\ hd\ A\ {\isacharhash}\ tl\ A{\isacharbackquoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}hd\ A\ {\isasymnoteq}\ h{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}h\ {\isasymle}\ hd\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ x\ {\isasymin}\ set\ t{\isachardot}\ h\ {\isasymle}\ x{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ {\isacharparenleft}tl\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymin}\ set\ {\isacharparenleft}tl\ A{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharbackquoteopen}A\ {\isacharequal}\ h\ {\isacharhash}\ tl\ A{\isacharbackquoteclose}{\isacharparenright}\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ insert\ h\ {\isacharparenleft}set\ t{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}set\ A\ {\isasymsubseteq}\ insert\ h\ {\isacharparenleft}set\ t{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymnoteq}\ h{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ {\isacharbackquoteopen}A\ {\isacharequal}\ h\ {\isacharhash}\ tl\ A{\isacharbackquoteclose}{\isacharparenright}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}x\ {\isasymin}\ set\ {\isacharparenleft}tl\ A{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isasymin}\ insert\ h\ {\isacharparenleft}set\ t{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isasymnoteq}\ h{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}length\ A\ {\isacharminus}\ {\isadigit{1}}\ {\isacharequal}\ k\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}length\ A\ {\isacharequal}\ k{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}l\ {\isacharequal}\ h\ {\isacharhash}\ t{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}l\ {\isacharequal}\ h\ {\isacharhash}\ t{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\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%
\ combine{\isacharunderscore}combines{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \isanewline
\ \ {\isachardoublequoteopen}sorted\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\isanewline
\ \ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}combine\ l\ k{\isacharparenright}\ \ {\isasymlongleftrightarrow}\ {\isacharparenleft}sorted\ A\ {\isasymand}\ distinct\ A\ {\isasymand}\ length\ A\ {\isacharequal}\ k\ {\isasymand}\ set\ A\ {\isasymsubseteq}\ set\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ combine{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isacharunderscore}combines{\isacharbrackleft}of\ l\ {\isachardoublequoteopen}length\ l{\isachardoublequoteclose}\ A\ k{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isacharunderscore}length{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}combine{\isacharunderscore}aux\ l\ n\ k{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}length\ l\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}length\ A\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ n\ k\ arbitrary{\isacharcolon}\ A\ rule{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ l\ n\ k{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k\ {\isacharequal}\ n{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ l{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ h\ t{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ l\ n\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ h\ t\ {\isachardoublequoteopen}tl\ A{\isachardoublequoteclose}{\isacharbrackright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharbrackleft}of\ h\ t\ A{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\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%
\ combine{\isacharunderscore}length{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}combine\ l\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}length\ A\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isacharunderscore}length{\isacharbrackleft}of\ A\ l\ {\isachardoublequoteopen}length\ l{\isachardoublequoteclose}\ k{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ combine{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\ \ \isanewline
\isacommand{lemma}\isamarkupfalse%
\ distinct{\isacharunderscore}combine{\isacharunderscore}aux{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}n\ {\isacharequal}\ length\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}combine{\isacharunderscore}aux\ l\ n\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ n\ k\ rule{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ l\ n\ k{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k\ {\isacharequal}\ n{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ l{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ h\ t{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ l\ n\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ h\ t{\isacharbrackright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharbrackleft}of\ h\ t{\isacharbrackright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ distinct{\isacharunderscore}map\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isacharunderscore}subset{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ of\ {\isacharunderscore}\ t\ {\isachardoublequoteopen}length\ t{\isachardoublequoteclose}\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\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%
\ distinct{\isacharunderscore}combine{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}combine\ l\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}combine{\isacharunderscore}aux{\isacharbrackleft}of\ {\isachardoublequoteopen}length\ l{\isachardoublequoteclose}\ l\ k{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ combine{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}prepend{\isacharcolon}\ {\isachardoublequoteopen}sorted\ l\ {\isacharequal}\ sorted\ {\isacharparenleft}map\ {\isacharparenleft}op\ {\isacharhash}\ h{\isacharparenright}\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ l{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sorted{\isacharunderscore}Cons{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}combine{\isacharunderscore}aux{\isacharunderscore}lemma{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ h\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isacharcolon}{\isacharcolon}linorder{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}x{\isasymin}set\ t{\isachardot}\ h\ {\isasymle}\ x{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}h\ {\isasymnotin}\ set\ t{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}set\ l{\isacharprime}\ {\isasymsubseteq}\ set\ t{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}l{\isacharprime}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}h\ {\isacharhash}\ l\ {\isasymle}\ l{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}hd\ l{\isacharprime}\ {\isasymin}\ set\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}l{\isacharprime}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}set\ l{\isacharprime}\ {\isasymsubseteq}\ set\ t{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}h\ {\isacharless}\ hd\ l{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}x{\isasymin}set\ t{\isachardot}\ h\ {\isasymle}\ x{\isacharbackquoteclose}\ {\isacharbackquoteopen}h\ {\isasymnotin}\ set\ t{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}h\ {\isacharequal}\ hd\ l{\isacharprime}{\isachardoublequoteclose}{\isacharparenright}\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}l{\isacharprime}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\ Cons{\isacharunderscore}le{\isacharunderscore}Cons{\isacharbrackleft}of\ h\ l\ {\isachardoublequoteopen}hd\ l{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}tl\ l{\isacharprime}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sorted{\isacharunderscore}combine{\isacharunderscore}aux{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}n\ {\isacharequal}\ length\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}sorted\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}sorted\ {\isacharparenleft}combine{\isacharunderscore}aux\ l\ n\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ n\ k\ rule{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ l\ n\ k{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}k\ {\isacharequal}\ n{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ l{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ h\ t{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ n{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isachardot}simps{\isacharbrackleft}of\ l\ n\ k{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ h\ t{\isacharbrackright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharbrackleft}of\ h\ t{\isacharbrackright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ {\isadigit{1}}{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ distinct{\isacharunderscore}map\ inj{\isacharunderscore}on{\isacharunderscore}def\ sorted{\isacharunderscore}Cons\ sorted{\isacharunderscore}append{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ sorted{\isacharunderscore}prepend{\isacharbrackleft}THEN\ sym{\isacharbrackright}{\isacharcomma}\ simp{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ sorted{\isacharunderscore}combine{\isacharunderscore}aux{\isacharunderscore}lemma{\isacharbrackleft}of\ t{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ combine{\isacharunderscore}aux{\isacharunderscore}subset{\isacharparenright}{\isacharplus}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ length{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}conv{\isacharbrackleft}THEN\ sym{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}aux{\isacharunderscore}length\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\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%
\ sorted{\isacharunderscore}combine{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sorted\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}sorted\ {\isacharparenleft}combine\ l\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}combine{\isacharunderscore}aux{\isacharbrackleft}of\ {\isachardoublequoteopen}length\ l{\isachardoublequoteclose}\ l\ k{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ combine{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Generating all nonempty subsets%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ all{\isacharunderscore}nonempty{\isacharunderscore}subsets\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}all{\isacharunderscore}nonempty{\isacharunderscore}subsets\ F\ {\isacharequal}\ concat\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ k{\isachardot}\ combine\ F\ k{\isacharparenright}\ {\isacharbrackleft}{\isadigit{1}}{\isachardot}{\isachardot}{\isacharless}length\ F\ {\isacharplus}\ {\isadigit{1}}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ all{\isacharunderscore}subs{\isacharunderscore}set{\isacharcolon}\ {\isachardoublequoteopen}set\ {\isacharparenleft}all{\isacharunderscore}nonempty{\isacharunderscore}subsets\ l{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}A{\isachardot}\ set\ A\ {\isasymsubseteq}\ set\ l\ {\isasymand}\ length\ A\ {\isasymge}\ {\isadigit{1}}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ all{\isacharunderscore}nonempty{\isacharunderscore}subsets{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}subset\ combine{\isacharunderscore}length\isanewline
\isacommand{by}\isamarkupfalse%
\ force%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Generating all m-elements subsets of n-element set%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ all{\isacharunderscore}mn{\isacharunderscore}subsets\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m\ {\isacharequal}\ combine\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}\ m{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}set\ {\isacharparenleft}map\ set\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}A{\isachardot}\ card\ A\ {\isacharequal}\ m\ {\isasymand}\ A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isacharequal}\ {\isacharquery}rhs{\isachardoublequoteclose}{\isacharparenright}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ combine{\isacharunderscore}combines{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharunderscore}\ m{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ distinct{\isacharunderscore}card{\isacharparenright}\ {\isacharparenleft}metis\ distinct{\isacharunderscore}card\ finite{\isacharunderscore}atLeastLessThan\ finite{\isacharunderscore}sorted{\isacharunderscore}distinct{\isacharunderscore}unique\ image{\isacharunderscore}iff\ rev{\isacharunderscore}finite{\isacharunderscore}subset{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharunderscore}completeness{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ m{\isachardoublequoteclose}\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ Al\ {\isasymin}\ set\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isachardot}\ set\ Al\ {\isacharequal}\ A{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ assms\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}map\ set\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharbrackleft}of\ n\ m{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharunderscore}sorted{\isacharunderscore}distinct{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}sorted\ A\ {\isasymand}\ distinct\ A{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ combine{\isacharunderscore}combines\ distinct{\isacharunderscore}upt\ sorted{\isacharunderscore}upt{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}all{\isacharunderscore}mn{\isacharunderscore}subsets\ n\ m{\isacharparenright}\ {\isasymLongrightarrow}\ set\ A\ {\isasymsubseteq}\ {\isacharbraceleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ all{\isacharunderscore}mn{\isacharunderscore}subsets{\isacharbrackleft}of\ n\ m{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\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:
