%
\begin{isabellebody}%
\setisabellecontext{UnionClosedImpl}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ UnionClosedImpl\isanewline
\isakeyword{imports}\ UnionClosed\ FamilyImpl\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsubsection{Abstract representation of union closed families%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Sets that support empty set, unions and powerset.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{locale}\isamarkupfalse%
\ SetUnionImpl\ {\isacharequal}\ SetImpl\ to{\isacharunderscore}set\ \isakeyword{for}\ to{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequoteclose}\ {\isacharplus}\isanewline
\ \ \isakeyword{fixes}\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ empty{\isacharunderscore}set{\isacharcolon}\ {\isachardoublequoteopen}to{\isacharunderscore}set\ empty\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ empty{\isacharunderscore}inv{\isacharcolon}\ {\isachardoublequoteopen}inv\ empty{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isakeyword{fixes}\ union\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}s{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isachardoublequoteclose}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}\isanewline
\ \ \isakeyword{assumes}\ union{\isacharunderscore}set{\isacharcolon}\ {\isachardoublequoteopen}to{\isacharunderscore}set\ {\isacharparenleft}s{\isadigit{1}}\ {\isasymsqunion}\ s{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ to{\isacharunderscore}set\ s{\isadigit{1}}\ {\isasymunion}\ to{\isacharunderscore}set\ s{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ union{\isacharunderscore}inv{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}inv\ s{\isadigit{1}}{\isacharsemicolon}\ inv\ s{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ inv\ {\isacharparenleft}s{\isadigit{1}}\ {\isasymsqunion}\ s{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isakeyword{fixes}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}s\ list{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ pow{\isacharunderscore}set{\isacharcolon}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}pow\ s{\isacharparenright}\ {\isacharequal}\ Pow\ {\isacharparenleft}to{\isacharunderscore}set\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ pow{\isacharunderscore}inv{\isacharcolon}\ {\isachardoublequoteopen}inv\ s\ {\isasymLongrightarrow}\ {\isasymforall}\ A\ {\isasymin}\ set\ {\isacharparenleft}pow\ s{\isacharparenright}{\isachardot}\ inv\ A{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ pow{\isacharunderscore}distinct{\isacharcolon}\ {\isachardoublequoteopen}inv\ s\ {\isasymLongrightarrow}\ distinct\ {\isacharparenleft}pow\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ subset{\isacharunderscore}in{\isacharunderscore}pow{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inv\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}inv\ S{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ to{\isacharunderscore}set\ S{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}pow\ S{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}to{\isacharunderscore}set\ A\ {\isasymin}\ f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}pow\ S{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ to{\isacharunderscore}set\ S{\isacharbackquoteclose}\ pow{\isacharunderscore}set{\isacharbrackleft}of\ S{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inv\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}inv\ S{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ pow{\isacharunderscore}inv\ to{\isacharunderscore}set{\isacharunderscore}inj\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ Union\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
{\isachardoublequoteopen}Union\ F\ {\isacharequal}\ foldl\ union\ empty\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ Union{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}to{\isacharunderscore}set\ {\isacharparenleft}Union\ F{\isacharparenright}\ {\isacharequal}\ {\isasymUnion}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ F\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Union{\isacharunderscore}def\ empty{\isacharunderscore}set\ union{\isacharunderscore}set{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ Union{\isacharunderscore}inv{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ set\ F{\isachardot}\ inv\ A\ {\isasymLongrightarrow}\ inv\ {\isacharparenleft}Union\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ Union{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ F\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ empty{\isacharunderscore}inv\ union{\isacharunderscore}inv{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ union{\isacharunderscore}with{\isacharunderscore}all\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}union{\isacharunderscore}with{\isacharunderscore}all\ A\ F\ {\isasymequiv}\ {\isacharparenleft}map\ {\isacharparenleft}op\ {\isasymsqunion}\ A{\isacharparenright}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ union{\isacharunderscore}with{\isacharunderscore}all{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}map\ to{\isacharunderscore}set\ {\isacharparenleft}union{\isacharunderscore}with{\isacharunderscore}all\ A\ F{\isacharparenright}\ {\isacharequal}\ map\ {\isacharparenleft}op\ {\isasymunion}\ {\isacharparenleft}to{\isacharunderscore}set\ A{\isacharparenright}\ {\isasymcirc}\ to{\isacharunderscore}set{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ comp{\isacharunderscore}def\ union{\isacharunderscore}set{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ union{\isacharunderscore}with{\isacharunderscore}all{\isacharunderscore}set{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}to{\isacharunderscore}set\ {\isacharbackquote}\ {\isacharparenleft}op\ {\isasymsqunion}\ A\ {\isacharbackquote}\ set\ F{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}op\ {\isasymunion}\ {\isacharparenleft}to{\isacharunderscore}set\ A{\isacharparenright}\ {\isacharbackquote}\ to{\isacharunderscore}set\ {\isacharbackquote}\ set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharparenleft}map\ to{\isacharunderscore}set\ {\isacharparenleft}union{\isacharunderscore}with{\isacharunderscore}all\ A\ F{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ set\ {\isacharparenleft}map\ {\isacharparenleft}op\ {\isasymunion}\ {\isacharparenleft}to{\isacharunderscore}set\ A{\isacharparenright}\ {\isasymcirc}\ to{\isacharunderscore}set{\isacharparenright}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ union{\isacharunderscore}with{\isacharunderscore}all{\isacharunderscore}set{\isacharbrackleft}of\ A\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ comp{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ image{\isacharunderscore}comp{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ insert{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}insert{\isacharunderscore}set\ A\ F\ {\isasymequiv}\ {\isacharparenleft}if\ A\ {\isasymin}\ set\ F\ then\ F\ else\ A\ {\isacharhash}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ insert{\isacharunderscore}set{\isacharunderscore}set\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set\ {\isacharparenleft}insert{\isacharunderscore}set\ A\ F{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}A{\isacharbraceright}\ {\isasymunion}\ set\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ insert{\isacharunderscore}set{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ insert{\isacharunderscore}sets\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}insert{\isacharunderscore}sets\ l\ F\ {\isacharequal}\ foldl\ {\isacharparenleft}{\isasymlambda}\ F{\isacharprime}\ a{\isachardot}\ insert{\isacharunderscore}set\ a\ F{\isacharprime}{\isacharparenright}\ F\ l{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ insert{\isacharunderscore}sets{\isacharunderscore}set\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set\ {\isacharparenleft}insert{\isacharunderscore}sets\ l\ F{\isacharparenright}\ {\isacharequal}\ set\ l\ {\isasymunion}\ set\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ insert{\isacharunderscore}sets{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ insert{\isacharunderscore}sets{\isacharunderscore}remdups{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}distinct\ F\ {\isasymLongrightarrow}\ insert{\isacharunderscore}sets\ l\ F\ {\isacharequal}\ remdups\ {\isacharparenleft}rev\ l\ {\isacharat}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ insert{\isacharunderscore}sets{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ insert{\isacharunderscore}set{\isacharunderscore}def\ distinct{\isacharunderscore}remdups{\isacharunderscore}id{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ insert{\isacharunderscore}sets{\isacharunderscore}distinct{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}distinct\ F\ {\isasymLongrightarrow}\ distinct\ {\isacharparenleft}insert{\isacharunderscore}sets\ l\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ insert{\isacharunderscore}sets{\isacharunderscore}remdups{\isacharbrackleft}of\ F\ l{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close\ A\ F\ {\isasymequiv}\ insert{\isacharunderscore}sets\ {\isacharparenleft}{\isacharbrackleft}A{\isacharbrackright}\ {\isacharat}\ union{\isacharunderscore}with{\isacharunderscore}all\ A\ F{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close\ h\ F{\isacharparenright}\ {\isacharequal}\ UnionClosed{\isachardot}insert{\isacharunderscore}and{\isacharunderscore}close\ {\isacharparenleft}to{\isacharunderscore}set\ h{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ insert{\isacharunderscore}sets{\isacharunderscore}remdups\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ union{\isacharunderscore}with{\isacharunderscore}all{\isacharunderscore}set{\isacharprime}{\isacharbrackleft}of\ h\ F{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ \ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}inv{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ F{\isachardot}\ inv\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}inv\ h{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close\ h\ F{\isacharparenright}{\isachardot}\ inv\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ insert{\isacharunderscore}sets{\isacharunderscore}remdups\ union{\isacharunderscore}inv{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ \ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}subset{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ F{\isachardot}\ to{\isacharunderscore}set\ l\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}to{\isacharunderscore}set\ h\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close\ h\ F{\isacharparenright}{\isachardot}\ to{\isacharunderscore}set\ l\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\ l\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}l\ {\isasymin}\ set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close\ h\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymin}\ to{\isacharunderscore}set\ l{\isachardoublequoteclose}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close\ h\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ {\isacharparenleft}UnionClosed{\isachardot}insert{\isacharunderscore}and{\isacharunderscore}close\ {\isacharparenleft}to{\isacharunderscore}set\ h{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}set{\isacharbrackleft}of\ F\ h{\isacharcomma}\ THEN\ sym{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ split{\isacharcolon}\ if{\isacharunderscore}split{\isacharunderscore}asm{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ A\ F\ Fc\ {\isasymequiv}\ insert{\isacharunderscore}sets\ {\isacharparenleft}{\isacharbrackleft}A{\isacharbrackright}\ {\isacharat}\ union{\isacharunderscore}with{\isacharunderscore}all\ A\ F\ {\isacharat}\ union{\isacharunderscore}with{\isacharunderscore}all\ A\ Fc{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ A\ F\ Fc{\isacharparenright}\ {\isacharequal}\ UnionClosed{\isachardot}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ {\isacharparenleft}to{\isacharunderscore}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ insert{\isacharunderscore}sets{\isacharunderscore}remdups\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ union{\isacharunderscore}with{\isacharunderscore}all{\isacharunderscore}set{\isacharprime}{\isacharbrackleft}of\ A\ F{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ union{\isacharunderscore}with{\isacharunderscore}all{\isacharunderscore}set{\isacharprime}{\isacharbrackleft}of\ A\ Fc{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ \ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}subset{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ F{\isachardot}\ to{\isacharunderscore}set\ l\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ Fc{\isachardot}\ to{\isacharunderscore}set\ l\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ A\ F\ Fc{\isacharparenright}{\isachardot}\ to{\isacharunderscore}set\ l\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\ l\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}l\ {\isasymin}\ set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ A\ F\ Fc{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymin}\ to{\isacharunderscore}set\ l{\isachardoublequoteclose}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ A\ F\ Fc{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ {\isacharparenleft}UnionClosed{\isachardot}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ {\isacharparenleft}to{\isacharunderscore}set\ A{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Fc{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}set{\isacharbrackleft}of\ F\ A\ Fc{\isacharcomma}\ THEN\ sym{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ split{\isacharcolon}\ if{\isacharunderscore}split{\isacharunderscore}asm{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ \ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}inv{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inv\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ F{\isachardot}\ inv\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ Fc{\isachardot}\ inv\ l{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ A\ F\ Fc{\isacharparenright}{\isachardot}\ inv\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ insert{\isacharunderscore}sets{\isacharunderscore}remdups\ union{\isacharunderscore}inv{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cong{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}set\ F\ {\isacharequal}\ set\ F{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ A\ F\ Fc{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ \ set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ A\ F{\isacharprime}\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ insert{\isacharunderscore}sets{\isacharunderscore}remdups{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ close\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}close\ F\ {\isacharequal}\ foldl\ {\isacharparenleft}{\isasymlambda}\ F\ A{\isachardot}\ insert{\isacharunderscore}and{\isacharunderscore}close\ A\ F{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ close{\isacharunderscore}snoc{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}close\ {\isacharparenleft}F\ {\isacharat}\ {\isacharbrackleft}A{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ insert{\isacharunderscore}and{\isacharunderscore}close\ A\ {\isacharparenleft}close\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ close{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ close{\isacharunderscore}distinct{\isacharcolon}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}close\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ close{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ A\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ insert{\isacharunderscore}sets{\isacharunderscore}distinct{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ close{\isacharunderscore}set{\isacharcolon}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}close\ A{\isacharparenright}\ {\isacharequal}\ UnionClosed{\isachardot}closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ A\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}snoc\ l\ a{\isacharparenright}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}L\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ x{\isachardot}\ foldl\ {\isacharparenleft}{\isasymlambda}F\ A{\isachardot}\ local{\isachardot}insert{\isacharunderscore}and{\isacharunderscore}close\ A\ F{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ x{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ close{\isacharunderscore}distinct{\isacharbrackleft}of\ a{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}set{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isacharquery}L\ a{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}insert{\isacharbrackleft}of\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ a{\isachardoublequoteclose}\ {\isachardoublequoteopen}to{\isacharunderscore}set\ l{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ snoc{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ close{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ close{\isacharunderscore}def\ closure{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ close{\isacharunderscore}completeness{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inv\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ set\ F{\isachardot}\ inv\ a{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}to{\isacharunderscore}set\ A\ {\isasymin}\ UnionClosed{\isachardot}closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}A\ {\isasymin}\ set\ {\isacharparenleft}close\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ F\ arbitrary{\isacharcolon}\ A\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ closure{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}snoc\ a\ l{\isacharparenright}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}to{\isacharunderscore}set\ A\ {\isasymin}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}l\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}to{\isacharunderscore}set\ A\ {\isacharequal}\ to{\isacharunderscore}set\ a\ {\isasymor}\ to{\isacharunderscore}set\ A\ {\isasymin}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ l{\isacharparenright}\ {\isasymor}\ to{\isacharunderscore}set\ A\ {\isasymin}\ op\ {\isasymunion}\ {\isacharparenleft}to{\isacharunderscore}set\ a{\isacharparenright}\ {\isacharbackquote}\ closure\ {\isacharparenleft}to{\isacharunderscore}set\ {\isacharbackquote}\ set\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}insert{\isacharbrackleft}of\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ l{\isachardoublequoteclose}\ {\isachardoublequoteopen}to{\isacharunderscore}set\ a{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}to{\isacharunderscore}set\ A\ {\isacharequal}\ to{\isacharunderscore}set\ a{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ snoc{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ snoc{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ to{\isacharunderscore}set{\isacharunderscore}inj\ close{\isacharunderscore}snoc{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}to{\isacharunderscore}set\ A\ {\isasymin}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ l{\isacharparenright}\ {\isasymor}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ to{\isacharunderscore}set\ A\ {\isasymin}\ op\ {\isasymunion}\ {\isacharparenleft}to{\isacharunderscore}set\ a{\isacharparenright}\ {\isacharbackquote}\ closure\ {\isacharparenleft}to{\isacharunderscore}set\ {\isacharbackquote}\ set\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}to{\isacharunderscore}set\ A\ {\isasymin}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ snoc{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ snoc{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ snoc{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ close{\isacharunderscore}snoc{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}to{\isacharunderscore}set\ A\ {\isasymin}\ op\ {\isasymunion}\ {\isacharparenleft}to{\isacharunderscore}set\ a{\isacharparenright}\ {\isacharbackquote}\ closure\ {\isacharparenleft}to{\isacharunderscore}set\ {\isacharbackquote}\ set\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ X\ \isakeyword{where}\ {\isachardoublequoteopen}X\ {\isasymin}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ l{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}to{\isacharunderscore}set\ A\ {\isacharequal}\ to{\isacharunderscore}set\ a\ {\isasymunion}\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ finiteUn{\isacharunderscore}iff{\isacharbrackleft}of\ {\isachardoublequoteopen}closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ l{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}closure{\isacharbrackleft}of\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ l{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ to{\isacharunderscore}set{\isacharunderscore}finite{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Y\ \isakeyword{where}\ {\isachardoublequoteopen}X\ {\isacharequal}\ to{\isacharunderscore}set\ Y{\isachardoublequoteclose}\ {\isachardoublequoteopen}inv\ Y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ to{\isacharunderscore}set{\isacharunderscore}ex{\isacharbrackleft}of\ X{\isacharbrackright}\ \isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}Y\ {\isasymin}\ set\ {\isacharparenleft}close\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ snoc{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ Y{\isacharbrackright}\ {\isacharbackquoteopen}X\ {\isasymin}\ closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ l{\isacharparenright}{\isacharbackquoteclose}\ snoc{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isacharequal}\ a\ {\isasymsqunion}\ Y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}to{\isacharunderscore}set\ A\ {\isacharequal}\ to{\isacharunderscore}set\ a\ {\isasymunion}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}X\ {\isacharequal}\ to{\isacharunderscore}set\ Y{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ snoc{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ snoc{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ {\isacharbackquoteopen}inv\ Y{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ union{\isacharunderscore}set\ union{\isacharunderscore}inv\ to{\isacharunderscore}set{\isacharunderscore}inj{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ op\ {\isasymsqunion}\ a\ {\isacharbackquote}\ set\ {\isacharparenleft}close\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Y\ {\isasymin}\ set\ {\isacharparenleft}close\ l{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ close{\isacharunderscore}snoc{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ close{\isacharunderscore}inv{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ F{\isachardot}\ inv\ l{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ {\isacharparenleft}close\ F{\isacharparenright}{\isachardot}\ inv\ l{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ F\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}snoc\ a\ l{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ close{\isacharunderscore}distinct{\isacharbrackleft}of\ l{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ close{\isacharunderscore}def\ insert{\isacharunderscore}sets{\isacharunderscore}remdups\ union{\isacharunderscore}inv{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ close{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ close{\isacharunderscore}subset{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ F{\isachardot}\ to{\isacharunderscore}set\ l\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ {\isacharparenleft}close\ F{\isacharparenright}{\isachardot}\ to{\isacharunderscore}set\ l\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ F\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}snoc\ a\ l{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}subset{\isacharbrackleft}of\ {\isachardoublequoteopen}close\ l{\isachardoublequoteclose}\ S\ a{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ close{\isacharunderscore}distinct{\isacharbrackleft}of\ l{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ close{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ close{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ close{\isacharunderscore}and{\isacharunderscore}insert{\isacharunderscore}empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}close{\isacharunderscore}and{\isacharunderscore}insert{\isacharunderscore}empty\ F\ {\isasymequiv}\isanewline
\ \ \ \ \ let\ X\ {\isacharequal}\ close\ F\isanewline
\ \ \ \ \ \ in\ {\isacharparenleft}if\ empty\ {\isasymin}\ set\ X\ then\ X\ else\ empty\ {\isacharhash}\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ close{\isacharunderscore}and{\isacharunderscore}insert{\isacharunderscore}empty{\isacharunderscore}set{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set\ {\isacharparenleft}close{\isacharunderscore}and{\isacharunderscore}insert{\isacharunderscore}empty\ F{\isacharparenright}\ {\isacharequal}\ set\ {\isacharparenleft}close\ F{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}empty{\isacharbraceright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Let{\isacharunderscore}def\ close{\isacharunderscore}and{\isacharunderscore}insert{\isacharunderscore}empty{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ close{\isacharunderscore}and{\isacharunderscore}insert{\isacharunderscore}empty{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}close{\isacharunderscore}and{\isacharunderscore}insert{\isacharunderscore}empty\ F{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ \ {\isacharparenleft}UnionClosed{\isachardot}closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}to{\isacharunderscore}set\ {\isacharbackquote}\ set\ {\isacharparenleft}close\ F{\isacharparenright}\ {\isacharequal}\ closure\ {\isacharparenleft}to{\isacharunderscore}set\ {\isacharbackquote}\ set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}def\ close{\isacharunderscore}set\ image{\isacharunderscore}set{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ close{\isacharunderscore}and{\isacharunderscore}insert{\isacharunderscore}empty{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ empty{\isacharunderscore}set\ Let{\isacharunderscore}def{\isacharparenright}\ {\isacharparenleft}metis\ empty{\isacharunderscore}set\ image{\isacharunderscore}eqI{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{primrec}\isamarkupfalse%
\ union{\isacharunderscore}closed\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}union{\isacharunderscore}closed\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}list{\isacharunderscore}all\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ h\ {\isasymsqunion}\ x\ {\isasymin}\ set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ t\ {\isasymand}\ union{\isacharunderscore}closed\ t{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F\ {\isasymLongrightarrow}\ UnionClosed{\isachardot}union{\isacharunderscore}closed\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ F{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ UnionClosed{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ h\ t{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}insert{\isacharbrackleft}of\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ t{\isachardoublequoteclose}\ {\isachardoublequoteopen}to{\isacharunderscore}set\ h{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ list{\isacharunderscore}all{\isacharunderscore}iff{\isacharparenright}\ {\isacharparenleft}metis\ imageI\ union{\isacharunderscore}set{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{primrec}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharprime}\ F\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharprime}\ F\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}list{\isacharunderscore}all\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ h\ {\isasymsqunion}\ x\ {\isasymin}\ set\ F{\isacharparenright}\ F\ {\isasymand}\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharprime}\ F\ t{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharprime}{\isacharunderscore}set{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharprime}\ F\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ f{\isacharunderscore}to{\isacharunderscore}set\ Fc{\isachardot}\ {\isasymforall}\ B\ {\isasymin}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardot}\ A\ {\isasymunion}\ B\ {\isasymin}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ Fc{\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{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ list{\isacharunderscore}all{\isacharunderscore}iff{\isacharparenright}\ {\isacharparenleft}metis\ union{\isacharunderscore}set\ imageI{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}additional\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ Fc\ {\isasymlongleftrightarrow}\ union{\isacharunderscore}closed\ F\ {\isasymand}\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharprime}\ F\ Fc{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}UnionClosed{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}set{\isacharbrackleft}of\ F{\isacharbrackright}\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharprime}{\isacharunderscore}set{\isacharbrackleft}of\ F\ Fc{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto{\isacharparenright}\ {\isacharparenleft}metis\ sup{\isacharunderscore}commute{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{end}\isamarkupfalse%
%
\isamarkupsubsubsection{Implementation by sorted and distinct lists%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Power set of a list%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{primrec}\isamarkupfalse%
\ Pow{\isacharunderscore}l\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}Pow{\isacharunderscore}l\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackleft}{\isacharbrackright}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}Pow{\isacharunderscore}l\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ {\isacharequal}\ \isanewline
\ \ \ \ \ {\isacharparenleft}let\ X\ {\isacharequal}\ Pow{\isacharunderscore}l\ t\isanewline
\ \ \ \ \ \ \ in\ X\ {\isacharat}\ map\ {\isacharparenleft}op\ {\isacharhash}\ h{\isacharparenright}\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set\ {\isacharparenleft}map\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ X{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Pow\ {\isacharparenleft}set\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ X{\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\ l{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharbrackleft}THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Let{\isacharunderscore}def\ comp{\isacharunderscore}def\ Pow{\isacharunderscore}insert{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}distinct{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}distinct\ A\ {\isasymLongrightarrow}\ distinct\ {\isacharparenleft}Pow{\isacharunderscore}l\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ A{\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\ A{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Let{\isacharunderscore}def\ distinct{\isacharunderscore}map\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymnotin}\ set\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isacharhash}\ x\ {\isasymin}\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharparenleft}a\ {\isacharhash}\ x{\isacharparenright}\ {\isasymin}\ Pow\ {\isacharparenleft}set\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}set{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ del{\isacharcolon}\ set{\isacharunderscore}simps{\isacharparenright}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymnotin}\ set\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}elems{\isacharunderscore}distinct{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}distinct\ x{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ A\ arbitrary{\isacharcolon}\ x{\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{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ t{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ y\ \isakeyword{where}\ {\isachardoublequoteopen}y\ {\isasymin}\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ t{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isacharequal}\ h\ {\isacharhash}\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}set{\isacharbrackleft}of\ t{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}elems{\isacharunderscore}sorted{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sorted\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}sorted\ x{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ A\ arbitrary{\isacharcolon}\ x{\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\ t\ h{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ t{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ y\ \isakeyword{where}\ {\isachardoublequoteopen}y\ {\isasymin}\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ t{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isacharequal}\ h\ {\isacharhash}\ y{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}set{\isacharbrackleft}of\ t{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}Cons{\isacharbrackleft}of\ h\ y{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}no{\isacharunderscore}perms{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}sorted\ A{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ A{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}y\ {\isasymin}\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}set\ x\ {\isacharequal}\ set\ y{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}elems{\isacharunderscore}sorted{\isacharbrackleft}of\ A\ x{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}elems{\isacharunderscore}distinct{\isacharbrackleft}of\ A\ x{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}elems{\isacharunderscore}sorted{\isacharbrackleft}of\ A\ y{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}elems{\isacharunderscore}distinct{\isacharbrackleft}of\ A\ y{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ sorted{\isacharunderscore}distinct{\isacharunderscore}set{\isacharunderscore}unique{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Merging two sorted lists%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ merge\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isacharcolon}{\isacharcolon}linorder\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isacharcolon}{\isacharcolon}linorder\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isacharcolon}{\isacharcolon}linorder\ list{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isachardoublequoteclose}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}merge\ {\isacharbrackleft}{\isacharbrackright}\ l\ {\isacharequal}\ l{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}merge\ l\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ l{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}merge\ {\isacharparenleft}h{\isadigit{1}}\ {\isacharhash}\ t{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}h{\isadigit{2}}\ {\isacharhash}\ t{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ \isanewline
\ \ \ \ \ {\isacharparenleft}if\ h{\isadigit{1}}\ {\isacharless}\ h{\isadigit{2}}\ then\ \isanewline
\ \ \ \ \ \ \ \ \ \ h{\isadigit{1}}\ {\isacharhash}\ merge\ t{\isadigit{1}}\ {\isacharparenleft}h{\isadigit{2}}\ {\isacharhash}\ t{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ else\ if\ h{\isadigit{1}}\ {\isachargreater}\ h{\isadigit{2}}\ then\isanewline
\ \ \ \ \ \ \ \ \ \ h{\isadigit{2}}\ {\isacharhash}\ merge\ {\isacharparenleft}h{\isadigit{1}}\ {\isacharhash}\ t{\isadigit{1}}{\isacharparenright}\ t{\isadigit{2}}\isanewline
\ \ \ \ \ \ else\isanewline
\ \ \ \ \ \ \ \ \ \ h{\isadigit{1}}\ {\isacharhash}\ merge\ t{\isadigit{1}}\ t{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ merge{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set\ {\isacharparenleft}l{\isadigit{1}}\ {\isasymsqunion}\ l{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ set\ l{\isadigit{1}}\ {\isasymunion}\ set\ l{\isadigit{2}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ l{\isadigit{1}}\ l{\isadigit{2}}\ rule{\isacharcolon}\ merge{\isachardot}induct{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ merge{\isacharunderscore}sorted{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}sorted\ l{\isadigit{1}}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}sorted\ l{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}sorted\ {\isacharparenleft}l{\isadigit{1}}\ {\isasymsqunion}\ l{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ l{\isadigit{1}}\ l{\isadigit{2}}\ rule{\isacharcolon}\ merge{\isachardot}induct{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sorted{\isacharunderscore}Cons\ merge{\isacharunderscore}set{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ merge{\isacharunderscore}distinct{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ l{\isadigit{1}}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}distinct\ l{\isadigit{2}}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}sorted\ l{\isadigit{1}}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}sorted\ l{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}l{\isadigit{1}}\ {\isasymsqunion}\ l{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ l{\isadigit{1}}\ l{\isadigit{2}}\ rule{\isacharcolon}\ merge{\isachardot}induct{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sorted{\isacharunderscore}Cons\ merge{\isacharunderscore}set{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{global{\isacharunderscore}interpretation}\isamarkupfalse%
\ SetUnionImpl{\isacharunderscore}lists{\isacharcolon}\ SetUnionImpl\ {\isachardoublequoteopen}{\isasymlambda}\ {\isacharparenleft}l{\isacharcolon}{\isacharcolon}nat\ list{\isacharparenright}{\isachardot}\ sorted\ l\ {\isasymand}\ distinct\ l{\isachardoublequoteclose}\ set\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ merge\ Pow{\isacharunderscore}l\isanewline
\ \ \isakeyword{defines}\isanewline
\ \ close{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}lists{\isachardot}close{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ insert{\isacharunderscore}set{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}lists{\isachardot}insert{\isacharunderscore}set{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ insert{\isacharunderscore}sets{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}lists{\isachardot}insert{\isacharunderscore}sets{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}lists{\isachardot}insert{\isacharunderscore}and{\isacharunderscore}close{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ Union{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}lists{\isachardot}Union{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ close{\isacharunderscore}insert{\isacharunderscore}empty{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}lists{\isachardot}close{\isacharunderscore}and{\isacharunderscore}insert{\isacharunderscore}empty{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ union{\isacharunderscore}closed{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}lists{\isachardot}union{\isacharunderscore}closed{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharprime}{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}lists{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}l\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}lists{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}unfold{\isacharunderscore}locales{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ s\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ list{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}SetImpl{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ s{\isacharparenright}\ {\isacharequal}\ Pow\ {\isacharparenleft}set\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}def{\isacharbrackleft}symmetric{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ SetImpl{\isacharunderscore}lists{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}def{\isacharbrackleft}of\ {\isachardoublequoteopen}Pow{\isacharunderscore}l\ s{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ Pow{\isacharunderscore}l{\isacharunderscore}set{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Pow{\isacharunderscore}l{\isacharunderscore}elems{\isacharunderscore}sorted\ Pow{\isacharunderscore}l{\isacharunderscore}elems{\isacharunderscore}distinct\ merge{\isacharunderscore}set\ merge{\isacharunderscore}sorted\ merge{\isacharunderscore}distinct\ sorted{\isacharunderscore}distinct{\isacharunderscore}set{\isacharunderscore}unique\ Pow{\isacharunderscore}l{\isacharunderscore}distinct{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Implementation by sets represented as natural numbers%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
For example, the family \isa{{\isacharbraceleft}{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isacharcomma}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbraceright}{\isacharbraceright}} is represented
as \isa{{\isacharbrackleft}{\isadigit{7}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{4}}{\isacharbrackright}}.%
\end{isamarkuptext}\isamarkuptrue%
%
\begin{isamarkuptext}%
Powerset%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ pow{\isacharunderscore}n\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
{\isachardoublequoteopen}pow{\isacharunderscore}n\ n\ {\isacharequal}\ map\ list{\isadigit{2}}nat\ {\isacharparenleft}Pow{\isacharunderscore}l\ {\isacharparenleft}nat{\isadigit{2}}list\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
Union is obtained by bitwise disjunction -- this is a naive implementation%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{function}\isamarkupfalse%
\ bitor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}bitor\ x\ y\ {\isacharequal}\ \isanewline
\ \ {\isacharparenleft}if\ x\ {\isacharequal}\ {\isadigit{0}}\ then\ y\isanewline
\ \ \ else\ if\ y\ {\isacharequal}\ {\isadigit{0}}\ then\ x\ else\isanewline
\ \ \ let\ {\isacharparenleft}xd{\isacharcomma}\ xm{\isacharparenright}\ {\isacharequal}\ Divides{\isachardot}divmod{\isacharunderscore}nat\ x\ {\isadigit{2}}{\isacharsemicolon}\isanewline
\ \ \ \ \ \ \ {\isacharparenleft}yd{\isacharcomma}\ ym{\isacharparenright}\ {\isacharequal}\ Divides{\isachardot}divmod{\isacharunderscore}nat\ y\ {\isadigit{2}}\ in\isanewline
\ \ \ if\ {\isacharparenleft}xm\ {\isacharequal}\ {\isadigit{1}}\ {\isacharbar}\ ym\ {\isacharequal}\ {\isadigit{1}}{\isacharparenright}\isanewline
\ \ \ then\ {\isadigit{1}}\ {\isacharplus}\ {\isadigit{2}}\ {\isacharasterisk}\ bitor\ xd\ yd\isanewline
\ \ \ else\ {\isadigit{2}}\ {\isacharasterisk}\ bitor\ xd\ yd{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ pat{\isacharunderscore}completeness\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isacommand{termination}\isamarkupfalse%
\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ \ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}x{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardot}\ x{\isacharparenright}{\isachardoublequoteclose}{\isacharcomma}\ auto\ simp\ add{\isacharcolon}\ divmod{\isacharunderscore}nat{\isacharunderscore}div{\isacharunderscore}mod{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isacommand{declare}\isamarkupfalse%
\ bitor{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ bitor{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}bitor\ x\ y{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ set\ {\isacharparenleft}nat{\isadigit{2}}list\ x{\isacharparenright}\ {\isasymunion}\ set\ {\isacharparenleft}nat{\isadigit{2}}list\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ x\ y\ rule{\isacharcolon}\ bitor{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}{\isadigit{1}}\ x{\isacharprime}\ y{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}x{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ bitor{\isachardot}simps\ nat{\isadigit{2}}list{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}y{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x{\isacharprime}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ bitor{\isachardot}simps\ nat{\isadigit{2}}list{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}x{\isacharprime}\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ Suc\ {\isadigit{0}}\ {\isasymand}\ y{\isacharprime}\ mod\ {\isadigit{2}}\ {\isasymnoteq}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}bitor\ x{\isacharprime}\ y{\isacharprime}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ bitor\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x{\isacharprime}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}y{\isacharprime}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ bitor{\isachardot}simps{\isacharbrackleft}of\ x{\isacharprime}\ y{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}def\ Let{\isacharunderscore}def\ div{\isacharunderscore}nat{\isacharunderscore}def{\isacharbrackleft}THEN\ sym{\isacharbrackright}\ mod{\isacharunderscore}nat{\isacharunderscore}def{\isacharbrackleft}THEN\ sym{\isacharbrackright}\ split{\isacharcolon}\ if{\isacharunderscore}split{\isacharunderscore}asm{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ {\isacharparenleft}bitor\ x{\isacharprime}\ y{\isacharprime}{\isacharparenright}\ {\isacharequal}\ map\ {\isacharparenleft}op\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}bitor\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}even{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}bitor\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ set\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}\ {\isasymunion}\ set\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharbrackleft}of\ {\isachardoublequoteopen}Divides{\isachardot}divmod{\isacharunderscore}nat\ x{\isacharprime}\ {\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x{\isacharprime}\ div\ {\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x{\isacharprime}\ mod\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}Divides{\isachardot}divmod{\isacharunderscore}nat\ y{\isacharprime}\ {\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}y{\isacharprime}\ div\ {\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}y{\isacharprime}\ mod\ {\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x{\isacharprime}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}y{\isacharprime}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ True\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ div{\isacharunderscore}nat{\isacharunderscore}def\ mod{\isacharunderscore}nat{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ divmod{\isacharunderscore}nat{\isacharunderscore}div{\isacharunderscore}mod{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}y{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isacharprime}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}y{\isacharprime}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ \ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ x{\isacharprime}\ {\isacharequal}\ map\ {\isacharparenleft}op\ {\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}nat{\isadigit{2}}list\ y{\isacharprime}\ {\isacharequal}\ map\ {\isacharparenleft}op\ {\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}even{\isacharbrackleft}of\ {\isachardoublequoteopen}x{\isacharprime}\ div\ {\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\ nat{\isadigit{2}}list{\isacharunderscore}even{\isacharbrackleft}of\ {\isachardoublequoteopen}y{\isacharprime}\ div\ {\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}bitor\ x{\isacharprime}\ y{\isacharprime}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ bitor\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x{\isacharprime}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}y{\isacharprime}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ bitor{\isachardot}simps{\isacharbrackleft}of\ x{\isacharprime}\ y{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}def\ Let{\isacharunderscore}def\ div{\isacharunderscore}nat{\isacharunderscore}def{\isacharbrackleft}THEN\ sym{\isacharbrackright}\ mod{\isacharunderscore}nat{\isacharunderscore}def{\isacharbrackleft}THEN\ sym{\isacharbrackright}\ split{\isacharcolon}\ if{\isacharunderscore}split{\isacharunderscore}asm{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ {\isacharparenleft}bitor\ x{\isacharprime}\ y{\isacharprime}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}\ {\isacharhash}\ map\ {\isacharparenleft}op\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}bitor\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}odd\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}bitor\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ set\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}\ {\isasymunion}\ set\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isadigit{1}}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ {\isachardoublequoteopen}Divides{\isachardot}divmod{\isacharunderscore}nat\ x{\isacharprime}\ {\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x{\isacharprime}\ div\ {\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x{\isacharprime}\ mod\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}Divides{\isachardot}divmod{\isacharunderscore}nat\ y{\isacharprime}\ {\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}y{\isacharprime}\ div\ {\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}y{\isacharprime}\ mod\ {\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x{\isacharprime}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}y{\isacharprime}\ {\isasymnoteq}\ {\isadigit{0}}{\isacharbackquoteclose}\ False\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\ {\isacharparenleft}simp\ add{\isacharcolon}\ divmod{\isacharunderscore}nat{\isacharunderscore}div{\isacharunderscore}mod{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}x{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}\ {\isasymand}\ y{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ x{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymand}\ y{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}\ {\isasymor}\ x{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymand}\ y{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharparenleft}nat{\isadigit{2}}list\ x{\isacharprime}{\isacharparenright}\ {\isasymunion}\ set\ {\isacharparenleft}nat{\isadigit{2}}list\ y{\isacharprime}{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}{\isadigit{0}}{\isacharbraceright}\ {\isasymunion}\ {\isacharparenleft}op\ {\isacharplus}{\isadigit{1}}\ {\isacharbackquote}\ {\isacharparenleft}set\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}\ {\isasymunion}\ set\ {\isacharparenleft}nat{\isadigit{2}}list\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}\ {\isasymand}\ y{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isacharprime}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}\ {\isasymand}\ y{\isacharprime}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ mod{\isacharunderscore}mult{\isacharunderscore}div{\isacharunderscore}eq{\isacharbrackleft}of\ y{\isacharprime}\ {\isadigit{2}}{\isacharcomma}\ THEN\ sym{\isacharbrackright}\ mod{\isacharunderscore}mult{\isacharunderscore}div{\isacharunderscore}eq{\isacharbrackleft}of\ x{\isacharprime}\ {\isadigit{2}}{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}even{\isacharbrackleft}of\ {\isachardoublequoteopen}x{\isacharprime}\ div\ {\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\ nat{\isadigit{2}}list{\isacharunderscore}odd{\isacharbrackleft}of\ {\isachardoublequoteopen}y{\isacharprime}\ div\ {\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymand}\ y{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isacharprime}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymand}\ y{\isacharprime}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ mod{\isacharunderscore}mult{\isacharunderscore}div{\isacharunderscore}eq{\isacharbrackleft}of\ y{\isacharprime}\ {\isadigit{2}}{\isacharcomma}\ THEN\ sym{\isacharbrackright}\ mod{\isacharunderscore}mult{\isacharunderscore}div{\isacharunderscore}eq{\isacharbrackleft}of\ x{\isacharprime}\ {\isadigit{2}}{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}even{\isacharbrackleft}of\ {\isachardoublequoteopen}y{\isacharprime}\ div\ {\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\ nat{\isadigit{2}}list{\isacharunderscore}odd{\isacharbrackleft}of\ {\isachardoublequoteopen}x{\isacharprime}\ div\ {\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}\ {\isasymand}\ y{\isacharprime}\ mod\ {\isadigit{2}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isacharprime}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}x{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymand}\ y{\isacharprime}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}y{\isacharprime}\ div\ {\isadigit{2}}{\isacharparenright}\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ mod{\isacharunderscore}mult{\isacharunderscore}div{\isacharunderscore}eq{\isacharbrackleft}of\ y{\isacharprime}\ {\isadigit{2}}{\isacharcomma}\ THEN\ sym{\isacharbrackright}\ mod{\isacharunderscore}mult{\isacharunderscore}div{\isacharunderscore}eq{\isacharbrackleft}of\ x{\isacharprime}\ {\isadigit{2}}{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}odd{\isacharbrackleft}of\ {\isachardoublequoteopen}x{\isacharprime}\ div\ {\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\ nat{\isadigit{2}}list{\isacharunderscore}odd{\isacharbrackleft}of\ {\isachardoublequoteopen}y{\isacharprime}\ div\ {\isadigit{2}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\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
\isanewline
\isacommand{global{\isacharunderscore}interpretation}\isamarkupfalse%
\ SetUnionImpl{\isacharunderscore}nats{\isacharcolon}\ SetUnionImpl\ {\isachardoublequoteopen}{\isasymlambda}\ n{\isachardot}\ True{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isachardoublequoteclose}\ {\isadigit{0}}\ bitor\ pow{\isacharunderscore}n\ \isanewline
\ \ \isakeyword{defines}\isanewline
\ \ close{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}nats{\isachardot}close{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ insert{\isacharunderscore}set{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}nats{\isachardot}insert{\isacharunderscore}set{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ insert{\isacharunderscore}sets{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}nats{\isachardot}insert{\isacharunderscore}sets{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}nats{\isachardot}insert{\isacharunderscore}and{\isacharunderscore}close{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ Union{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}nats{\isachardot}Union{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ close{\isacharunderscore}and{\isacharunderscore}insert{\isacharunderscore}empty{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}nats{\isachardot}close{\isacharunderscore}and{\isacharunderscore}insert{\isacharunderscore}empty{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ union{\isacharunderscore}closed{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}nats{\isachardot}union{\isacharunderscore}closed{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharprime}{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}nats{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SetUnionImpl{\isacharunderscore}nats{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}unfold{\isacharunderscore}locales{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isacharparenright}\ {\isadigit{0}}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ nat{\isadigit{2}}list{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ s{\isadigit{1}}\ s{\isadigit{2}}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isacharparenright}\ {\isacharparenleft}bitor\ s{\isadigit{1}}\ s{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isacharparenright}\ s{\isadigit{1}}\ {\isasymunion}\ {\isacharparenleft}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isacharparenright}\ s{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ bitor{\isacharunderscore}set\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ s\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}SetImpl{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isacharparenright}\ {\isacharparenleft}pow{\isacharunderscore}n\ s{\isacharparenright}\ {\isacharequal}\ Pow\ {\isacharparenleft}{\isacharparenleft}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isacharparenright}\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}set\ {\isasymcirc}\ nat{\isadigit{2}}list\ {\isasymcirc}\ list{\isadigit{2}}nat{\isacharparenright}\ {\isacharbackquote}\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ {\isacharparenleft}nat{\isadigit{2}}list\ s{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ set\ {\isacharbackquote}\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ {\isacharparenleft}nat{\isadigit{2}}list\ s{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ image{\isacharunderscore}cong{\isacharcomma}\ simp{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ {\isacharparenleft}Pow{\isacharunderscore}l\ {\isacharparenleft}nat{\isadigit{2}}list\ s{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}set\ {\isasymcirc}\ nat{\isadigit{2}}list\ {\isasymcirc}\ list{\isadigit{2}}nat{\isacharparenright}\ x\ {\isacharequal}\ set\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}nat{\isadigit{2}}list{\isacharbrackleft}of\ s{\isacharbrackright}\ distinct{\isacharunderscore}nat{\isadigit{2}}list{\isacharbrackleft}of\ s{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}list{\isadigit{2}}nat{\isacharbrackleft}of\ x{\isacharbrackright}\ Pow{\isacharunderscore}l{\isacharunderscore}elems{\isacharunderscore}sorted{\isacharbrackleft}of\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ s{\isachardoublequoteclose}\ x{\isacharbrackright}\ Pow{\isacharunderscore}l{\isacharunderscore}elems{\isacharunderscore}distinct{\isacharbrackleft}of\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ s{\isachardoublequoteclose}\ x{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}n{\isacharunderscore}def{\isacharbrackleft}symmetric{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ SetImpl{\isacharunderscore}nats{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ pow{\isacharunderscore}n{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Pow{\isacharunderscore}l{\isacharunderscore}set{\isacharbrackleft}of\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ s{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ s\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}pow{\isacharunderscore}n\ s{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ pow{\isacharunderscore}n{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ distinct{\isacharunderscore}map\ distinct{\isacharunderscore}nat{\isadigit{2}}list\ Pow{\isacharunderscore}l{\isacharunderscore}distinct\ \isanewline
\ \ \ \ \ \ \ \ inj{\isacharunderscore}on{\isacharunderscore}def\ inj{\isacharunderscore}list{\isadigit{2}}nat\ \isanewline
\ \ \ \ \ \ \ \ Pow{\isacharunderscore}l{\isacharunderscore}elems{\isacharunderscore}sorted{\isacharbrackleft}of\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ s{\isachardoublequoteclose}{\isacharbrackright}\ sorted{\isacharunderscore}nat{\isadigit{2}}list\isanewline
\ \ \ \ \ \ \ \ Pow{\isacharunderscore}l{\isacharunderscore}elems{\isacharunderscore}distinct{\isacharbrackleft}of\ {\isachardoublequoteopen}nat{\isadigit{2}}list\ s{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
\ simp{\isacharunderscore}all%
\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:
