%
\begin{isabellebody}%
\setisabellecontext{SomeShareNegativeImpl}%
%
\isamarkupsection{SomeShareNegative -- executable implementation%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ SomeShareNegativeImpl\isanewline
\isakeyword{imports}\ Main\isanewline
\ \ {\isachardoublequoteopen}HOL{\isacharminus}Library{\isachardot}List{\isacharunderscore}lexord{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}More{\isachardot}MoreMap{\isachardoublequoteclose}\isanewline
\ \ SomeShareNegative\ UnionClosedImpl\ WeightsSharesImpl\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\begin{isamarkuptext}%
In this section we define a refinement of the \isa{some{\isacharunderscore}share{\isacharunderscore}negative} function in several steps in order to obtain a
more efficient, executable implementation. Optimizations are
introduced gradually, through separate refinement steps.%
\end{isamarkuptext}\isamarkuptrue%
%
\isamarkupsubsection{Refinement of SomeShareNegativeFunction%
}
\isamarkuptrue%
\isacommand{locale}\isamarkupfalse%
\ SomeShareNegativeImpl\ {\isacharequal}\ \isanewline
\ \ SetWeightsSharesMapImpl\ inv\ to{\isacharunderscore}set\ set{\isacharunderscore}weight\ set{\isacharunderscore}weight{\isacharunderscore}map\ {\isacharplus}\isanewline
\ \ SetUnionImpl\ inv\ to{\isacharunderscore}set\ empty\ union\ pow\isanewline
\ \ \isakeyword{for}\ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{and}\ to{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequoteclose}\ \isakeyword{and}\ set{\isacharunderscore}weight\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{and}\ set{\isacharunderscore}weight{\isacharunderscore}map\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ nat{\isacharparenright}\ mapping\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s{\isachardoublequoteclose}\ \isakeyword{and}\ union\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}s{\isachardoublequoteclose}\ \isakeyword{and}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}s\ list{\isachardoublequoteclose}\isanewline
\isakeyword{begin}%
\isamarkupsubsubsection{Initial version%
}
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharprime}s\ list\ \ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ {\isacharbrackleft}{\isacharbrackright}\ F\ Init\ w\ X\ {\isacharequal}\ {\isacharparenleft}family{\isacharunderscore}share\ F\ w\ X\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ F\ Init\ w\ X\ {\isacharequal}\ \isanewline
\ \ \ \ {\isacharparenleft}if\ family{\isacharunderscore}share\ F\ w\ X\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}\ then\isanewline
\ \ \ \ \ \ \ \ False\isanewline
\ \ \ \ \ else\ if\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ t\ F\ Init\ w\ X\ then\isanewline
\ \ \ \ \ \ \ \ True\isanewline
\ \ \ \ \ else\ if\ h\ {\isasymin}\ set\ F\ then\isanewline
\ \ \ \ \ \ \ \ False\isanewline
\ \ \ \ \ else\isanewline
\ \ \ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ t\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ h\ F\ Init{\isacharparenright}\ Init\ w\ X\isanewline
\ \ \ \ \ {\isacharparenright}\isanewline
{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}{\isacharunderscore}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ F{\isachardot}\ inv\ l{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ L{\isachardot}\ inv\ l{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ Init{\isachardot}\ inv\ l{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}inv\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ L\ F\ Init\ w\ X\ {\isacharequal}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ {\isacharparenleft}map\ to{\isacharunderscore}set\ L{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Init{\isacharparenright}\ w\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ L\ arbitrary{\isacharcolon}\ F{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}set{\isacharbrackleft}of\ F\ X\ w{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ h\ t{\isacharparenright}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}family{\isacharunderscore}share\ F\ w\ X\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isacharparenright}\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ A\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}map\ to{\isacharunderscore}set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ A\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}map\ to{\isacharunderscore}set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}\ t\ {\isacharequal}\ map\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}to{\isacharunderscore}set\ x{\isacharparenright}\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isacharparenright}{\isacharparenright}\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}a{\isasymin}set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isachardot}\ inv\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}inv\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}share{\isacharunderscore}set\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}A{\isasymleftarrow}t{\isachardot}\ set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}x{\isasymleftarrow}t{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}to{\isacharunderscore}set\ x{\isacharparenright}\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ metis\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}a{\isasymin}set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isachardot}\ inv\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}inv\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ set{\isacharunderscore}share{\isacharunderscore}set\ comp{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}set{\isacharbrackleft}of\ F\ X\ w{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}a{\isasymin}set\ F{\isachardot}\ inv\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}inv\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}family{\isacharunderscore}share\ F\ w\ X\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ t\ F\ Init\ w\ X\ {\isacharequal}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ {\isacharparenleft}map\ to{\isacharunderscore}set\ t{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Init{\isacharparenright}\ w\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ t\ F\ Init\ w\ X{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ family{\isacharunderscore}share\ F\ w\ X\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ t\ F\ Init\ w\ X{\isacharbackquoteclose}\ {\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}{\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}h\ {\isasymin}\ set\ F{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}to{\isacharunderscore}set\ h\ {\isasymin}\ f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ set{\isacharunderscore}set{\isacharbrackleft}of\ F\ h{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}a{\isasymin}set\ F{\isachardot}\ inv\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}a{\isasymin}set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isachardot}\ inv\ a{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}h\ {\isasymin}\ set\ F{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ family{\isacharunderscore}share\ F\ w\ X\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ t\ F\ Init\ w\ X{\isacharbackquoteclose}\ {\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}h\ {\isasymin}\ set\ F{\isacharbackquoteclose}\ {\isacharasterisk}{\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ h\ F\ Init{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ t\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ h\ F\ Init{\isacharparenright}\ Init\ w\ X\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ {\isacharparenleft}map\ to{\isacharunderscore}set\ t{\isacharparenright}\ {\isacharparenleft}UnionClosed{\isachardot}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ {\isacharparenleft}to{\isacharunderscore}set\ h{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Init{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Init{\isacharparenright}\ w\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharquery}F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ insert{\isacharunderscore}sets{\isacharunderscore}distinct{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inv\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ t{\isachardot}\ inv\ l{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ Init{\isachardot}\ inv\ l{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inv\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isachardot}\ inv\ l{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ Init{\isachardot}\ inv\ l{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ {\isacharparenleft}set\ {\isacharquery}F{\isacharprime}{\isacharparenright}{\isachardot}\ inv\ l{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}a{\isasymin}set\ F{\isachardot}\ inv\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}a{\isasymin}set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isachardot}\ inv\ a{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}a{\isasymin}set\ Init{\isachardot}\ inv\ a{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ insert{\isacharunderscore}sets{\isacharunderscore}remdups\ union{\isacharunderscore}inv{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ {\isacharparenleft}map\ to{\isacharunderscore}set\ t{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ h\ F\ Init{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Init{\isacharparenright}\ w\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ {\isacharparenleft}map\ to{\isacharunderscore}set\ t{\isacharparenright}\ {\isacharparenleft}UnionClosed{\isachardot}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ {\isacharparenleft}to{\isacharunderscore}set\ h{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Init{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Init{\isacharparenright}\ w\isanewline
\ \ \ \ \ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}set\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ family{\isacharunderscore}share\ F\ w\ X\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ t\ F\ Init\ w\ X{\isacharbackquoteclose}\ {\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ h\ {\isasymin}\ set\ F{\isacharbackquoteclose}\ {\isacharasterisk}{\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Passing current family share as a parameter%
}
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}s\ {\isasymtimes}\ int{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}s\ list\ {\isasymtimes}\ int{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{2}}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ w\ X\ {\isacharequal}\ {\isacharparenleft}s\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{2}}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ w\ X\ {\isacharequal}\ \isanewline
\ \ \ \ {\isacharparenleft}if\ s\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ snd\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}\ then\isanewline
\ \ \ \ \ \ \ \ False\isanewline
\ \ \ \ \ else\ if\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{2}}\ t\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ w\ X\ then\isanewline
\ \ \ \ \ \ \ \ True\isanewline
\ \ \ \ \ else\ if\ fst\ h\ {\isasymin}\ set\ F\ then\isanewline
\ \ \ \ \ \ \ \ False\isanewline
\ \ \ \ \ else\isanewline
\ \ \ \ \ \ \ \ let\ F{\isacharprime}\ {\isacharequal}\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ {\isacharparenleft}fst\ h{\isacharparenright}\ F\ Init{\isacharsemicolon}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ s{\isacharprime}\ {\isacharequal}\ family{\isacharunderscore}share\ F{\isacharprime}\ w\ X\ in\isanewline
\ \ \ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{2}}\ t\ {\isacharparenleft}F{\isacharprime}{\isacharcomma}\ s{\isacharprime}{\isacharparenright}\ Init\ w\ X\isanewline
\ \ \ \ {\isacharparenright}\isanewline
{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{2}}{\isacharunderscore}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}L\ {\isacharequal}\ zip\ l\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ F{\isachardot}\ set{\isacharunderscore}share\ F\ w\ X{\isacharparenright}\ l{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}c\ {\isacharequal}\ family{\isacharunderscore}share\ F\ w\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{2}}\ \ L\ {\isacharparenleft}F{\isacharcomma}\ c{\isacharparenright}\ Init\ w\ X\ {\isacharequal}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}\ l\ F\ Init\ w\ X{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ arbitrary{\isacharcolon}\ F\ L\ c{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Caching set shares%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Instead of calculating set share every time from scratch when
calculating, family shares, we shall maintain a mapping from sets to
their shares.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{abbreviation}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}cached\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}s{\isacharcomma}\ int{\isacharparenright}\ mapping\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}family{\isacharunderscore}share{\isacharunderscore}cached\ F\ shares\ {\isasymequiv}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}the\ {\isasymcirc}\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ Mapping{\isachardot}lookup\ shares\ A{\isacharparenright}{\isacharparenright}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}cached{\isacharunderscore}family{\isacharunderscore}share{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ A{\isachardot}\ inv\ A\ {\isasymand}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S\ {\isasymlongrightarrow}\ Mapping{\isachardot}lookup\ shares\ A\ {\isacharequal}\ Some\ {\isacharparenleft}set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ set\ F{\isachardot}\ inv\ A\ {\isasymand}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}family{\isacharunderscore}share{\isacharunderscore}cached\ F\ shares\ {\isacharequal}\ family{\isacharunderscore}share\ F\ w\ X{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}map\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ the\ {\isacharparenleft}Mapping{\isachardot}lookup\ shares\ x{\isacharparenright}{\isacharparenright}\ F\ {\isacharequal}\ map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ local{\isachardot}set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}def\ comp{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ metis\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}cached{\isacharunderscore}cong{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}set\ F\ {\isacharequal}\ set\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}family{\isacharunderscore}share{\isacharunderscore}cached\ F\ shares\ {\isacharequal}\ family{\isacharunderscore}share{\isacharunderscore}cached\ F{\isacharprime}\ shares{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ sum{\isacharunderscore}list{\isacharunderscore}distinct{\isacharunderscore}conv{\isacharunderscore}sum{\isacharunderscore}set{\isacharbrackleft}of\ F\ {\isachardoublequoteopen}the\ {\isasymcirc}\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ Mapping{\isachardot}lookup\ shares\ A{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ sum{\isacharunderscore}list{\isacharunderscore}distinct{\isacharunderscore}conv{\isacharunderscore}sum{\isacharunderscore}set{\isacharbrackleft}of\ F{\isacharprime}\ {\isachardoublequoteopen}the\ {\isasymcirc}\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ Mapping{\isachardot}lookup\ shares\ A{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{fun}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}s\ {\isasymtimes}\ int{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}s\ list\ {\isasymtimes}\ int{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}s{\isacharcomma}\ int{\isacharparenright}\ mapping\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ {\isacharequal}\ {\isacharparenleft}s\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ {\isacharequal}\ \isanewline
\ \ \ \ {\isacharparenleft}if\ s\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ snd\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}\ then\isanewline
\ \ \ \ \ \ \ \ False\isanewline
\ \ \ \ \ else\ if\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}\ t\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ then\isanewline
\ \ \ \ \ \ \ \ True\isanewline
\ \ \ \ \ else\ if\ fst\ h\ {\isasymin}\ set\ F\ then\isanewline
\ \ \ \ \ \ \ \ False\isanewline
\ \ \ \ \ else\isanewline
\ \ \ \ \ \ \ \ let\ F{\isacharprime}\ {\isacharequal}\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ {\isacharparenleft}fst\ h{\isacharparenright}\ F\ Init{\isacharsemicolon}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ s{\isacharprime}\ {\isacharequal}\ family{\isacharunderscore}share{\isacharunderscore}cached\ F{\isacharprime}\ shares\ in\isanewline
\ \ \ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}\ t\ {\isacharparenleft}F{\isacharprime}{\isacharcomma}\ s{\isacharprime}{\isacharparenright}\ Init\ shares\isanewline
\ \ \ \ {\isacharparenright}\isanewline
{\isachardoublequoteclose}\isanewline
\isacommand{lemma}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}{\isacharunderscore}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{2}}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ A{\isachardot}\ inv\ A\ {\isasymand}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S\ {\isasymlongrightarrow}\ Mapping{\isachardot}lookup\ shares\ A\ {\isacharequal}\ Some\ {\isacharparenleft}set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ set\ F{\isachardot}\ inv\ A\ {\isasymand}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ set\ Init{\isachardot}\ inv\ A\ {\isasymand}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ set\ {\isacharparenleft}map\ fst\ l{\isacharparenright}{\isachardot}\ inv\ A\ {\isasymand}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}\ l\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ {\isacharequal}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{2}}\ l\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ w\ X{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ arbitrary{\isacharcolon}\ F\ s{\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{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}s\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ snd\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}fst\ h\ {\isasymin}\ set\ F{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ s\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ snd\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isacharbackquoteclose}\ Cons\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ {\isacharparenleft}fst\ h{\isacharparenright}\ F\ Init{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}s{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}family{\isacharunderscore}share{\isacharunderscore}cached\ {\isacharquery}F{\isacharprime}\ shares{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}s{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}family{\isacharunderscore}share\ {\isacharquery}F{\isacharprime}\ w\ X{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}A{\isasymin}set\ {\isacharquery}F{\isacharprime}{\isachardot}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ Cons{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}A{\isasymin}set\ {\isacharquery}F{\isacharprime}{\isachardot}\ inv\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}inv{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ Cons{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharquery}F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ insert{\isacharunderscore}sets{\isacharunderscore}distinct{\isacharparenright}\isanewline
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}s{\isacharprime}\ {\isacharequal}\ {\isacharquery}s{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ family{\isacharunderscore}share{\isacharunderscore}cached{\isacharunderscore}family{\isacharunderscore}share{\isacharbrackleft}of\ S\ shares\ w\ X\ {\isacharquery}F{\isacharprime}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}A{\isasymin}set\ {\isacharquery}F{\isacharprime}{\isachardot}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}A{\isasymin}set\ {\isacharquery}F{\isacharprime}{\isachardot}\ inv\ A{\isacharbackquoteclose}\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}\ t\ {\isacharparenleft}{\isacharquery}F{\isacharprime}{\isacharcomma}\ {\isacharquery}s{\isacharprime}{\isacharparenright}\ Init\ shares\ {\isacharequal}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{2}}\ t\ {\isacharparenleft}{\isacharquery}F{\isacharprime}{\isacharcomma}\ {\isacharquery}s{\isacharprime}{\isacharprime}{\isacharparenright}\ Init\ w\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ {\isacharquery}F{\isacharprime}\ {\isacharquery}s{\isacharprime}{\isacharbrackright}\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{5}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}A{\isasymin}set\ {\isacharquery}F{\isacharprime}{\isachardot}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}A{\isasymin}set\ {\isacharquery}F{\isacharprime}{\isachardot}\ inv\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ {\isacharquery}F{\isacharprime}{\isacharbackquoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ s\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ snd\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}fst\ h\ {\isasymnotin}\ set\ F{\isacharbackquoteclose}\ Cons\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}{\isacharunderscore}correct{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}\ L\ {\isacharparenleft}F{\isacharcomma}\ c{\isacharparenright}\ Init\ shares\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ set\ L{\isachardot}\ y\ {\isacharequal}\ set{\isacharunderscore}share\ x\ w\ X{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}c\ {\isacharequal}\ family{\isacharunderscore}share\ F\ w\ X{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}A{\isachardot}\ inv\ A\ {\isasymand}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S\ {\isasymlongrightarrow}\ Mapping{\isachardot}lookup\ shares\ A\ {\isacharequal}\ Some\ {\isacharparenleft}set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}A{\isasymin}set\ F{\isachardot}\ inv\ A\ {\isasymand}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}A{\isasymin}set\ Init{\isachardot}\ inv\ A\ {\isasymand}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}A{\isasymin}set\ {\isacharparenleft}map\ fst\ L{\isacharparenright}{\isachardot}\ inv\ A\ {\isasymand}\ to{\isacharunderscore}set\ A\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}inv\ X{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}A{\isasymin}set\ {\isacharparenleft}map\ fst\ L{\isacharparenright}{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}to{\isacharunderscore}set\ A{\isacharparenright}\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}finite\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}UnionClosed{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional\ F{\isacharprime}\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ Init{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ F\ {\isasymsubseteq}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}A{\isasymin}F{\isacharprime}\ {\isacharminus}\ f{\isacharunderscore}to{\isacharunderscore}set\ F{\isachardot}\ {\isacharparenleft}{\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ A\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ A\ {\isasymin}\ f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}map\ fst\ L{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}distinct\ L{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F{\isacharprime}\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ exists{\isacharunderscore}zip{\isacharbrackleft}of\ L\ {\isachardoublequoteopen}{\isasymlambda}\ x{\isachardot}\ set{\isacharunderscore}share\ x\ w\ X{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}{\isacharunderscore}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{2}}{\isacharbrackleft}of\ S\ shares\ w\ X{\isacharbrackright}{\isacharparenright}\isanewline
\isacommand{apply}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{2}}{\isacharunderscore}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}{\isacharbrackleft}of\ L\ {\isachardoublequoteopen}map\ fst\ L{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ comp{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharparenleft}asm{\isacharparenright}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{1}}{\isacharunderscore}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharparenright}\isanewline
\isacommand{apply}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}soundness{\isacharbrackleft}of\ {\isachardoublequoteopen}map\ to{\isacharunderscore}set\ {\isacharparenleft}map\ fst\ L{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}f{\isacharunderscore}to{\isacharunderscore}set\ Init{\isachardoublequoteclose}\ w\ {\isachardoublequoteopen}to{\isacharunderscore}set\ X{\isachardoublequoteclose}\ F{\isacharprime}{\isacharbrackright}{\isacharparenright}\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ comp{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}A{\isasymin}set\ L{\isachardot}\ inv\ {\isacharparenleft}fst\ A{\isacharparenright}\ {\isasymand}\ to{\isacharunderscore}set\ {\isacharparenleft}fst\ A{\isacharparenright}\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ L{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}x{\isasymin}set\ L{\isachardot}\ case\ x\ of\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymRightarrow}\ y\ {\isacharequal}\ set{\isacharunderscore}share\ x\ w\ X{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}a{\isasymin}set\ {\isacharparenleft}map\ fst\ L{\isacharparenright}{\isachardot}\ inv\ a{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}A{\isasymin}set\ L{\isachardot}\ inv\ {\isacharparenleft}fst\ A{\isacharparenright}\ {\isasymand}\ to{\isacharunderscore}set\ {\isacharparenleft}fst\ A{\isacharparenright}\ {\isasymsubseteq}\ S{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ to{\isacharunderscore}set\ {\isacharparenleft}set\ {\isacharparenleft}map\ fst\ L{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ to{\isacharunderscore}set{\isacharunderscore}inj{\isacharunderscore}on{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ to{\isacharunderscore}set\ {\isacharparenleft}fst\ x{\isacharparenright}{\isacharparenright}\ L{\isacharparenright}{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ comp{\isacharunderscore}inj{\isacharunderscore}on{\isacharunderscore}iff{\isacharbrackleft}of\ fst\ {\isachardoublequoteopen}set\ L{\isachardoublequoteclose}\ to{\isacharunderscore}set{\isacharbrackright}\ {\isacharasterisk}\ inj{\isacharunderscore}on{\isacharunderscore}fst{\isacharbrackleft}of\ L{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ distinct{\isacharunderscore}map\ comp{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Passing the sum of shares of elements in the current list as a parameter%
}
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}{\isacharprime}s\ {\isasymtimes}\ int{\isacharparenright}\ list\ {\isasymtimes}\ int{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}s\ list\ {\isasymtimes}\ int{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}s{\isacharcomma}\ int{\isacharparenright}\ mapping\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ {\isacharequal}\ {\isacharparenleft}s\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}{\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharcomma}\ ls{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ {\isacharequal}\ \isanewline
\ \ \ \ {\isacharparenleft}if\ s\ {\isacharplus}\ ls\ {\isasymge}\ {\isadigit{0}}\ then\isanewline
\ \ \ \ \ \ \ \ False\isanewline
\ \ \ \ \ else\ if\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ then\isanewline
\ \ \ \ \ \ \ \ True\isanewline
\ \ \ \ \ else\ if\ fst\ h\ {\isasymin}\ set\ F\ then\isanewline
\ \ \ \ \ \ \ \ False\isanewline
\ \ \ \ \ else\isanewline
\ \ \ \ \ \ \ \ let\ F{\isacharprime}\ {\isacharequal}\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ {\isacharparenleft}fst\ h{\isacharparenright}\ F\ Init{\isacharsemicolon}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ s{\isacharprime}\ {\isacharequal}\ family{\isacharunderscore}share{\isacharunderscore}cached\ F{\isacharprime}\ shares\ in\isanewline
\ \ \ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharprime}{\isacharcomma}\ s{\isacharprime}{\isacharparenright}\ Init\ shares\isanewline
\ \ \ \ {\isacharparenright}\isanewline
{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}{\isacharunderscore}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}l{\isacharcomma}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ snd\ l{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ {\isacharequal}\ \isanewline
\ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}\ l\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ arbitrary{\isacharcolon}\ F\ s{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}{\isacharunderscore}equal{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}set\ F\ {\isacharequal}\ set\ F{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}l{\isacharcomma}\ ls{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}l{\isacharcomma}\ ls{\isacharparenright}\ {\isacharparenleft}F{\isacharprime}{\isacharcomma}\ s{\isacharparenright}\ Init\ shares{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ arbitrary{\isacharcolon}\ F\ F{\isacharprime}\ s\ ls{\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{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}s\ {\isacharplus}\ ls\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ s\ {\isacharplus}\ ls\ {\isasymge}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ F\ F{\isacharprime}\ {\isachardoublequoteopen}ls\ {\isacharminus}\ snd\ h{\isachardoublequoteclose}\ s{\isacharbrackright}\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}fst\ h\ {\isasymin}\ set\ F{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ s\ {\isacharplus}\ ls\ {\isasymge}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ F\ F{\isacharprime}\ {\isachardoublequoteopen}ls\ {\isacharminus}\ snd\ h{\isachardoublequoteclose}\ s{\isacharbrackright}\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F\ {\isacharequal}\ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ {\isacharparenleft}fst\ h{\isacharparenright}\ F\ Init{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ {\isacharparenleft}fst\ h{\isacharparenright}\ F{\isacharprime}\ Init{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharquery}F\ {\isacharequal}\ set\ {\isacharquery}F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}set\ F\ {\isacharequal}\ set\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}distinct\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cong{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}family{\isacharunderscore}share{\isacharunderscore}cached\ {\isacharquery}F\ shares\ {\isacharequal}\ family{\isacharunderscore}share{\isacharunderscore}cached\ {\isacharquery}F{\isacharprime}\ shares{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}cached{\isacharunderscore}cong{\isacharbrackleft}of\ {\isacharquery}F\ {\isacharquery}F{\isacharprime}\ shares{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}distinct\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ insert{\isacharunderscore}sets{\isacharunderscore}distinct{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}fst\ h\ {\isasymnotin}\ set\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ s\ {\isacharplus}\ ls\ {\isasymge}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ F\ F{\isacharprime}\ {\isachardoublequoteopen}ls\ {\isacharminus}\ snd\ h{\isachardoublequoteclose}\ s{\isacharbrackright}\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{4}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}set\ {\isacharquery}F\ {\isacharequal}\ set\ {\isacharquery}F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ {\isacharquery}F\ {\isacharquery}F{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def\ insert{\isacharunderscore}sets{\isacharunderscore}distinct{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Incremental insert and close operation and calculation of share of the extended family%
}
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached\ A\ {\isacharparenleft}Ft{\isacharcomma}\ s{\isacharparenright}\ Fc\ shares\ {\isacharequal}\isanewline
\ \ \ \ \ \ {\isacharparenleft}let\ add\ {\isacharequal}\ {\isacharbrackleft}A{\isacharbrackright}\ {\isacharat}\ union{\isacharunderscore}with{\isacharunderscore}all\ A\ Ft\ {\isacharat}\ union{\isacharunderscore}with{\isacharunderscore}all\ A\ Fc{\isacharsemicolon}\isanewline
\ \ \ \ \ \ \ \ \ \ \ add\ {\isacharequal}\ filter\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ x\ {\isasymnotin}\ set\ Ft{\isacharparenright}\ {\isacharparenleft}remdups\ add{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ in\ {\isacharparenleft}add\ {\isacharat}\ Ft{\isacharcomma}\ s\ {\isacharplus}\ family{\isacharunderscore}share{\isacharunderscore}cached\ add\ shares{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached{\isacharunderscore}family{\isacharunderscore}share{\isacharunderscore}cached{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}let\ {\isacharparenleft}Ft{\isacharprime}{\isacharcomma}\ s{\isacharprime}{\isacharparenright}\ {\isacharequal}\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached\ A\ {\isacharparenleft}Ft{\isacharcomma}\ family{\isacharunderscore}share{\isacharunderscore}cached\ Ft\ shares{\isacharparenright}\ Fc\ shares\ \isanewline
\ \ \ \ \ \ \ \ \ \ in\ s{\isacharprime}\ {\isacharequal}\ family{\isacharunderscore}share{\isacharunderscore}cached\ Ft{\isacharprime}\ shares{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached{\isacharcolon}\isanewline
\isakeyword{assumes}\isanewline
\ \ {\isachardoublequoteopen}distinct\ Ft{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached\ A\ {\isacharparenleft}Ft{\isacharcomma}\ family{\isacharunderscore}share{\isacharunderscore}cached\ Ft\ shares{\isacharparenright}\ Fc\ shares\ {\isacharequal}\isanewline
\ \ \ {\isacharparenleft}Ft{\isacharprime}{\isacharcomma}\ s{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isakeyword{shows}\isanewline
\ \ {\isachardoublequoteopen}set\ Ft{\isacharprime}\ {\isacharequal}\ set\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ A\ Ft\ Fc{\isacharparenright}\ {\isasymand}\ \isanewline
\ \ \ s{\isacharprime}\ {\isacharequal}\ family{\isacharunderscore}share{\isacharunderscore}cached\ Ft{\isacharprime}\ shares{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}add\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbrackleft}A{\isacharbrackright}\ {\isacharat}\ union{\isacharunderscore}with{\isacharunderscore}all\ A\ Ft\ {\isacharat}\ union{\isacharunderscore}with{\isacharunderscore}all\ A\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}add\ {\isacharequal}\ {\isachardoublequoteopen}filter\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ x\ {\isasymnotin}\ set\ Ft{\isacharparenright}\ {\isacharparenleft}remdups\ {\isacharquery}add{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}Ft{\isacharprime}\ {\isacharequal}\ {\isacharquery}add\ {\isacharat}\ Ft{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ Ft{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ {\isachardoublequoteopen}s{\isacharprime}\ {\isacharequal}\ family{\isacharunderscore}share{\isacharunderscore}cached\ Ft\ shares\ {\isacharplus}\ family{\isacharunderscore}share{\isacharunderscore}cached\ {\isacharquery}add\ shares{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached\ A\ {\isacharparenleft}Ft{\isacharcomma}\ family{\isacharunderscore}share{\isacharunderscore}cached\ Ft\ shares{\isacharparenright}\ Fc\ shares\ {\isacharequal}\ {\isacharparenleft}Ft{\isacharprime}{\isacharcomma}\ s{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ Ft{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{function}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}{\isacharprime}s\ {\isasymtimes}\ int{\isacharparenright}\ list\ {\isasymtimes}\ int{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}s\ list\ {\isasymtimes}\ int{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}s{\isacharcomma}\ int{\isacharparenright}\ mapping\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ {\isacharparenleft}if\ s\ {\isacharless}\ {\isadigit{0}}\ then\ True\ else\ False{\isacharparenright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}\ {\isacharparenleft}{\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharcomma}\ ls{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ {\isacharequal}\ \isanewline
\ \ \ \ {\isacharparenleft}if\ s\ {\isacharplus}\ ls\ {\isasymge}\ {\isadigit{0}}\ then\isanewline
\ \ \ \ \ \ \ \ False\isanewline
\ \ \ \ \ else\ if\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ then\isanewline
\ \ \ \ \ \ \ \ True\isanewline
\ \ \ \ \ else\ if\ fst\ h\ {\isasymin}\ set\ F\ then\isanewline
\ \ \ \ \ \ \ \ False\isanewline
\ \ \ \ \ else\isanewline
\ \ \ \ \ \ \ \ let\ {\isacharparenleft}F{\isacharprime}{\isacharcomma}\ s{\isacharprime}{\isacharparenright}\ {\isacharequal}\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached\ {\isacharparenleft}fst\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ in\isanewline
\ \ \ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharprime}{\isacharcomma}\ s{\isacharprime}{\isacharparenright}\ Init\ shares\isanewline
\ \ \ \ {\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}{\isacharparenleft}L{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isacharcomma}\ {\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardot}\ length\ L{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}{\isacharunderscore}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}{\isacharcolon}\isanewline
\isakeyword{assumes}\ {\isachardoublequoteopen}s\ {\isacharequal}\ family{\isacharunderscore}share{\isacharunderscore}cached\ F\ shares{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\isanewline
\isakeyword{shows}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}\ {\isacharparenleft}L{\isacharcomma}\ ls{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ {\isacharequal}\ \isanewline
some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}L{\isacharcomma}\ ls{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ L\ arbitrary{\isacharcolon}\ F\ s\ ls{\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{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymle}\ s\ {\isacharplus}\ ls{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}{\isachardot}simps\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}{\isachardot}simps\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares\ {\isacharequal}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ s\ F\ {\isachardoublequoteopen}ls\ {\isacharminus}\ snd\ h{\isachardoublequoteclose}{\isacharbrackright}\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ Cons{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ {\isadigit{0}}\ {\isasymle}\ s\ {\isacharplus}\ ls{\isacharbackquoteclose}\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}fst\ h\ {\isasymin}\ set\ F{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ {\isadigit{0}}\ {\isasymle}\ s\ {\isacharplus}\ ls{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F{\isadigit{1}}s{\isadigit{1}}\ {\isacharequal}\ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached\ {\isacharparenleft}fst\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F{\isadigit{1}}\ {\isacharequal}\ {\isachardoublequoteopen}fst\ {\isacharquery}F{\isadigit{1}}s{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}s{\isadigit{1}}\ {\isacharequal}\ {\isachardoublequoteopen}snd\ {\isacharquery}F{\isadigit{1}}s{\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F{\isadigit{2}}\ {\isacharequal}\ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ {\isacharparenleft}fst\ h{\isacharparenright}\ F\ Init{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}s{\isadigit{2}}\ {\isacharequal}\ {\isachardoublequoteopen}family{\isacharunderscore}share{\isacharunderscore}cached\ {\isacharquery}F{\isadigit{2}}\ shares{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharquery}F{\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ {\isacharquery}F{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ insert{\isacharunderscore}sets{\isacharunderscore}distinct\ Let{\isacharunderscore}def{\isacharparenright}\isanewline
\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharquery}F{\isadigit{1}}\ {\isacharequal}\ set\ {\isacharquery}F{\isadigit{2}}\ {\isasymand}\ {\isacharquery}s{\isadigit{1}}\ {\isacharequal}\ {\isacharquery}s{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached{\isacharbrackleft}OF\ {\isacharbackquoteopen}distinct\ F{\isacharbackquoteclose}{\isacharcomma}\ of\ {\isachardoublequoteopen}fst\ h{\isachardoublequoteclose}\ shares\ Init\ {\isacharquery}F{\isadigit{1}}\ {\isacharquery}s{\isadigit{1}}{\isacharbrackright}\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ family{\isacharunderscore}share{\isacharunderscore}cached{\isacharunderscore}cong\ prod{\isachardot}collapse{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharquery}F{\isadigit{1}}\ {\isacharequal}\ set\ {\isacharquery}F{\isadigit{2}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharquery}s{\isadigit{1}}\ {\isacharequal}\ {\isacharquery}s{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ conjunct{\isadigit{1}}{\isacharcomma}\ rule\ conjunct{\isadigit{2}}{\isacharparenright}\isanewline
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}{\isacharquery}F{\isadigit{1}}{\isacharcomma}\ {\isacharquery}s{\isadigit{1}}{\isacharparenright}\ Init\ shares\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}{\isacharquery}F{\isadigit{2}}{\isacharcomma}\ {\isacharquery}s{\isadigit{2}}{\isacharparenright}\ Init\ shares{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}{\isacharunderscore}equal{\isacharunderscore}set{\isacharbrackleft}of\ {\isacharquery}F{\isadigit{1}}\ {\isacharquery}F{\isadigit{2}}\ t\ {\isachardoublequoteopen}ls\ {\isacharminus}\ snd\ h{\isachardoublequoteclose}\ {\isacharquery}s{\isadigit{1}}\ Init\ shares{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}set\ {\isacharquery}F{\isadigit{1}}\ {\isacharequal}\ set\ {\isacharquery}F{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharquery}F{\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ {\isacharquery}F{\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact{\isacharplus}\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}{\isacharquery}F{\isadigit{2}}{\isacharcomma}\ {\isacharquery}s{\isadigit{1}}{\isacharparenright}\ Init\ shares\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}{\isacharquery}F{\isadigit{2}}{\isacharcomma}\ {\isacharquery}s{\isadigit{2}}{\isacharparenright}\ Init\ shares{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharbackquoteopen}{\isacharquery}s{\isadigit{1}}\ {\isacharequal}\ {\isacharquery}s{\isadigit{2}}{\isacharbackquoteclose}{\isacharcomma}\ rule\ refl{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}{\isacharquery}F{\isadigit{1}}{\isacharcomma}\ {\isacharquery}s{\isadigit{1}}{\isacharparenright}\ Init\ shares\ {\isacharequal}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}{\isacharquery}F{\isadigit{1}}{\isacharcomma}\ {\isacharquery}s{\isadigit{1}}{\isacharparenright}\ Init\ shares{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackleft}of\ {\isacharquery}s{\isadigit{1}}\ {\isacharquery}F{\isadigit{1}}\ {\isachardoublequoteopen}ls\ {\isacharminus}\ snd\ h{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\ {\isacharbackquoteopen}distinct\ {\isacharquery}F{\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached{\isacharunderscore}family{\isacharunderscore}share{\isacharunderscore}cached{\isacharbrackleft}of\ {\isachardoublequoteopen}fst\ h{\isachardoublequoteclose}\ F\ shares\ Init{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Let{\isacharunderscore}def\ comp{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}fst\ h\ {\isasymnotin}\ set\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ {\isadigit{0}}\ {\isasymle}\ s\ {\isacharplus}\ ls{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymnot}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}\ {\isacharparenleft}t{\isacharcomma}\ ls\ {\isacharminus}\ snd\ h{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ s{\isacharparenright}\ Init\ shares{\isacharbackquoteclose}\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Final implementation%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ nat{\isacharparenright}\ mapping\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
{\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative\ A\ w\ {\isasymequiv}\isanewline
\ \ let\ S\ {\isacharequal}\ Union\ A{\isacharsemicolon}\isanewline
\ \ \ \ \ \ P\ {\isacharequal}\ pow\ S{\isacharsemicolon}\isanewline
\ \ \ \ \ \ A\ {\isacharequal}\ close\ A{\isacharsemicolon}\isanewline
\ \ \ \ \ \ U{\isacharprime}\ {\isacharequal}\ map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ set{\isacharunderscore}share{\isacharunderscore}map\ A\ w\ S{\isacharparenright}\ P{\isacharsemicolon}\isanewline
\ \ \ \ \ \ U\ {\isacharequal}\ sort{\isacharunderscore}key\ snd\ {\isacharparenleft}zip\ P\ U{\isacharprime}{\isacharparenright}{\isacharsemicolon}\isanewline
\ \ \ \ \ \ shares\ {\isacharequal}\ tabulate\ U{\isacharsemicolon}\isanewline
\ \ \ \ \ \ L\ {\isacharequal}\ \ takeWhile\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isachardot}\ b\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}\ U{\isacharsemicolon}\isanewline
\ \ \ \ \ \ F\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\isanewline
\ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}\ {\isacharparenleft}L{\isacharcomma}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ snd\ L{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}F{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ A\ shares{\isachardoublequoteclose}\isanewline
\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negativeFalse{\isacharunderscore}FamilyShare{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \isanewline
\ \ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative\ A\ w\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ A{\isachardot}\ inv\ l{\isachardoublequoteclose}\ \isanewline
\ \ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}UnionClosed{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ {\isacharparenleft}closure\ A{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ F{\isachardot}\ x\ {\isasymsubseteq}\ {\isasymUnion}\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ {\isasymUnion}A{\isacharprime}{\isachardot}\ Mapping{\isachardot}lookup\ w\ x\ {\isacharequal}\ Some\ {\isacharparenleft}w{\isacharprime}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}w{\isacharprime}\ {\isasymbowtie}\isactrlsub f\ F\ {\isacharparenleft}{\isasymUnion}\ A{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequoteopen}Union\ A{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}P\ {\isacharequal}\ {\isachardoublequoteopen}pow\ {\isacharquery}S{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}A\ {\isacharequal}\ {\isachardoublequoteopen}close\ A{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}U{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ set{\isacharunderscore}share{\isacharunderscore}map\ A\ w\ {\isacharquery}S{\isacharparenright}\ {\isacharquery}P{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}U\ {\isacharequal}\ {\isachardoublequoteopen}sort{\isacharunderscore}key\ snd\ {\isacharparenleft}zip\ {\isacharquery}P\ {\isacharquery}U{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}shares\ {\isacharequal}\ {\isachardoublequoteopen}tabulate\ {\isacharquery}U{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}L\ {\isacharequal}\ {\isachardoublequoteopen}takeWhile\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isachardot}\ b\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}\ {\isacharquery}U{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}F\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}inv\ {\isacharparenleft}Union\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ A{\isachardot}\ inv\ l{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ Union{\isacharunderscore}inv{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ set\ {\isacharquery}P{\isachardot}\ set{\isacharunderscore}share{\isacharunderscore}map\ x\ w\ {\isacharparenleft}Union\ A{\isacharparenright}\ {\isacharequal}\ set{\isacharunderscore}share\ x\ w{\isacharprime}\ {\isacharparenleft}Union\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ {\isacharquery}P{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}to{\isacharunderscore}set\ x\ {\isasymsubseteq}\ {\isasymUnion}\ A{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}inv\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pow{\isacharunderscore}set{\isacharbrackleft}of\ {\isachardoublequoteopen}Union\ A{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pow{\isacharunderscore}inv{\isacharbrackleft}of\ {\isachardoublequoteopen}Union\ A{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Union{\isacharunderscore}set{\isacharbrackleft}of\ A{\isacharbrackright}\ {\isacharbackquoteopen}inv\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharbackquoteclose}\ \ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ to{\isacharunderscore}set\ x{\isachardot}\ Mapping{\isachardot}lookup\ w\ a\ {\isacharequal}\ Some\ {\isacharparenleft}w{\isacharprime}\ a{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isasymUnion}A{\isacharprime}{\isachardot}\ Mapping{\isachardot}lookup\ w\ a\ {\isacharequal}\ Some\ {\isacharparenleft}w{\isacharprime}\ a{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}set{\isacharunderscore}share{\isacharunderscore}map\ x\ w\ {\isacharparenleft}Union\ A{\isacharparenright}\ {\isacharequal}\ set{\isacharunderscore}share\ x\ w{\isacharprime}\ {\isacharparenleft}Union\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharbrackleft}of\ x\ w\ w{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharbrackleft}of\ {\isachardoublequoteopen}Union\ A{\isachardoublequoteclose}\ w\ w{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isasymUnion}A{\isacharprime}{\isachardot}\ Mapping{\isachardot}lookup\ w\ a\ {\isacharequal}\ Some\ {\isacharparenleft}w{\isacharprime}\ a{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Union{\isacharunderscore}set{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inv\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}inv\ x{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ set{\isacharunderscore}share{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharbackquoteclose}{\isacharcomma}\ subst\ Union{\isacharunderscore}set{\isacharbrackleft}THEN\ sym{\isacharbrackright}{\isacharcomma}\ rule\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}{\isacharunderscore}correct{\isacharbrackleft}of\ {\isacharquery}L\ {\isacharquery}F\ {\isadigit{0}}\ {\isacharquery}A\ {\isacharquery}shares{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}\ {\isacharquery}L\ {\isacharparenleft}{\isacharquery}F{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharquery}A\ {\isacharquery}shares\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}some{\isacharunderscore}share{\isacharunderscore}negative\ A\ w\ {\isacharequal}\ False{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}def\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}{\isacharunderscore}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{3}}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}{\isacharunderscore}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{4}}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ set\ {\isacharquery}L{\isachardot}\ y\ {\isacharequal}\ set{\isacharunderscore}share\ x\ w{\isacharprime}\ {\isacharparenleft}Union\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ dest{\isacharbang}{\isacharcolon}\ set{\isacharunderscore}takeWhileD\ simp\ add{\isacharcolon}\ set{\isacharunderscore}zip{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharequal}\ family{\isacharunderscore}share\ {\isacharbrackleft}{\isacharbrackright}\ w{\isacharprime}\ {\isacharparenleft}Union\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ family{\isacharunderscore}share{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A{\isacharprime}{\isachardot}\ inv\ A{\isacharprime}\ {\isasymand}\ to{\isacharunderscore}set\ A{\isacharprime}\ {\isasymsubseteq}\ to{\isacharunderscore}set\ {\isacharquery}S\ {\isasymlongrightarrow}\ Mapping{\isachardot}lookup\ {\isacharquery}shares\ A{\isacharprime}\ {\isacharequal}\ Some\ {\isacharparenleft}set{\isacharunderscore}share\ A{\isacharprime}\ w{\isacharprime}\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharquery}P{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inv\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ pow{\isacharunderscore}distinct{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharparenleft}map\ fst\ {\isacharquery}U{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}fst{\isacharbrackleft}of\ {\isacharquery}U{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}force\ simp\ add{\isacharcolon}\ distinct{\isacharunderscore}map\ distinct{\isacharunderscore}zipI{\isadigit{1}}\ set{\isacharunderscore}zip{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ {\isacharquery}P{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inv\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ subset{\isacharunderscore}in{\isacharunderscore}pow\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ tabulate{\isacharunderscore}map{\isacharunderscore}of{\isacharbrackleft}of\ {\isacharquery}U{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ tabulate{\isacharunderscore}map{\isacharunderscore}of\ map{\isacharunderscore}of{\isacharunderscore}sort{\isacharunderscore}key\ map{\isacharunderscore}of{\isacharunderscore}zip{\isacharunderscore}map\ Mapping{\isachardot}lookup{\isachardot}abs{\isacharunderscore}eq{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A{\isacharprime}\ {\isasymin}\ set\ {\isacharparenleft}close\ A{\isacharparenright}{\isachardot}\ inv\ A{\isacharprime}\ {\isasymand}\ to{\isacharunderscore}set\ A{\isacharprime}\ {\isasymsubseteq}\ to{\isacharunderscore}set\ {\isacharparenleft}Union\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ close{\isacharunderscore}inv{\isacharbrackleft}of\ A{\isacharbrackright}\ {\isacharbackquoteopen}{\isasymforall}l{\isasymin}set\ A{\isachardot}\ inv\ l{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ close{\isacharunderscore}subset{\isacharbrackleft}of\ A\ {\isachardoublequoteopen}to{\isacharunderscore}set\ {\isacharparenleft}Union\ A{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Union{\isacharunderscore}set{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A{\isacharprime}\ {\isasymin}\ set\ {\isacharparenleft}map\ fst\ {\isacharquery}L{\isacharparenright}{\isachardot}\ inv\ A{\isacharprime}\ {\isasymand}\ to{\isacharunderscore}set\ A{\isacharprime}\ {\isasymsubseteq}\ to{\isacharunderscore}set\ {\isacharparenleft}Union\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pow{\isacharunderscore}inv{\isacharbrackleft}of\ {\isachardoublequoteopen}Union\ A{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{using}\isamarkupfalse%
\ pow{\isacharunderscore}set{\isacharbrackleft}of\ {\isachardoublequoteopen}Union\ A{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}inv\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ dest{\isacharbang}{\isacharcolon}\ set{\isacharunderscore}takeWhileD\ set{\isacharunderscore}zip{\isacharunderscore}leftD{\isacharparenright}\ force\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inv\ {\isacharparenleft}Union\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}A{\isacharprime}{\isasymin}set\ {\isacharparenleft}map\ fst\ {\isacharquery}L{\isacharparenright}{\isachardot}\ {\isacharparenleft}w{\isacharprime}\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}to{\isacharunderscore}set\ A{\isacharprime}{\isacharparenright}\ {\isacharparenleft}to{\isacharunderscore}set\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\ \isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ a\ b\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ set\ {\isacharparenleft}zip\ {\isacharquery}P\ {\isacharquery}U{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}b\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ set\ {\isacharquery}P{\isachardoublequoteclose}\ {\isachardoublequoteopen}set{\isacharunderscore}share{\isacharunderscore}map\ a\ w\ {\isacharparenleft}Union\ A{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ set{\isacharunderscore}zip{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}w{\isacharprime}\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}to{\isacharunderscore}set\ a{\isacharparenright}\ {\isacharparenleft}to{\isacharunderscore}set\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ set{\isacharunderscore}share{\isacharunderscore}set{\isacharbrackleft}of\ a\ {\isachardoublequoteopen}Union\ A{\isachardoublequoteclose}\ w{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inv\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pow{\isacharunderscore}inv{\isacharbrackleft}of\ {\isachardoublequoteopen}Union\ A{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ dest{\isacharbang}{\isacharcolon}\ set{\isacharunderscore}takeWhileD{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}UnionClosed{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}close\ A{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}UnionClosed{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ {\isacharparenleft}closure\ A{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ close{\isacharunderscore}set{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}x{\isasymin}F\ {\isacharminus}\ f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharbrackleft}{\isacharbrackright}{\isachardot}\ {\isacharparenleft}{\isacharparenleft}w{\isacharprime}\ {\isasymbowtie}\isactrlsub s\ x\ {\isacharparenleft}to{\isacharunderscore}set\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ \isanewline
\ \ \ \ \ \ x\ {\isasymin}\ f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}map\ fst\ {\isacharquery}L{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}w{\isacharprime}\ {\isasymbowtie}\isactrlsub s\ x\ {\isacharparenleft}to{\isacharunderscore}set\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymsubseteq}\ to{\isacharunderscore}set\ {\isacharparenleft}Union\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ x\ {\isasymin}\ F{\isachardot}\ x\ {\isasymsubseteq}\ {\isasymUnion}\ A{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isasymin}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Union{\isacharunderscore}set{\isacharbrackleft}of\ A{\isacharbrackright}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharquery}P{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pow{\isacharunderscore}set{\isacharbrackleft}of\ {\isachardoublequoteopen}Union\ A{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ x{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isacharequal}\ to{\isacharunderscore}set\ x{\isacharprime}{\isachardoublequoteclose}\ {\isachardoublequoteopen}x{\isacharprime}\ {\isasymin}\ set\ {\isacharquery}P{\isachardoublequoteclose}\ {\isachardoublequoteopen}inv\ x{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ pow{\isacharunderscore}inv{\isacharbrackleft}of\ {\isachardoublequoteopen}Union\ A{\isachardoublequoteclose}{\isacharbrackright}\ {\isacharbackquoteopen}inv\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharprime}{\isacharcomma}\ set{\isacharunderscore}share{\isacharunderscore}map\ x{\isacharprime}\ w\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharparenright}\ {\isasymin}\ set\ {\isacharquery}L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ sorted{\isacharunderscore}takeWhile{\isacharunderscore}snd{\isacharunderscore}neg{\isacharbrackleft}of\ {\isacharquery}U\ {\isacharquery}P{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x{\isacharprime}\ {\isasymin}\ set\ {\isacharquery}P{\isacharbackquoteclose}\ {\isacharbackquoteopen}x\ {\isacharequal}\ to{\isacharunderscore}set\ x{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isacharparenleft}w{\isacharprime}\ {\isasymbowtie}\isactrlsub s\ x\ {\isacharparenleft}to{\isacharunderscore}set\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}inv\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}inv\ x{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}share{\isacharunderscore}set\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}map\ fst\ {\isacharquery}L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isacharequal}\ to{\isacharunderscore}set\ x{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}force\ simp\ add{\isacharcolon}\ comp{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}distinct\ {\isacharquery}L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}inv\ {\isacharparenleft}Union\ A{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ intro{\isacharbang}{\isacharcolon}\ distinct{\isacharunderscore}takeWhile\ distinct{\isacharunderscore}zipI{\isadigit{1}}\ pow{\isacharunderscore}distinct{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negativeSound{\isacharcolon}\isanewline
\isakeyword{assumes}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}l{\isasymin}set\ A{\isachardot}\ inv\ l{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}x{\isasymin}A{\isacharprime}{\isachardot}\ finite\ x{\isachardoublequoteclose}\isanewline
\ \ {\isachardoublequoteopen}{\isasymforall}x{\isasymin}{\isasymUnion}A{\isacharprime}{\isachardot}\ Mapping{\isachardot}lookup\ w\ x\ {\isacharequal}\ Some\ {\isacharparenleft}w{\isacharprime}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative\ A\ w\ {\isacharequal}\ False\ {\isasymLongrightarrow}\ uce{\isacharunderscore}shares{\isacharunderscore}nonneg\ A{\isacharprime}\ w{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ F\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative\ A\ w\ {\isacharequal}\ False{\isachardoublequoteclose}\ {\isachardoublequoteopen}F\ {\isasymin}\ {\isasymlbrace}A{\isacharprime}{\isasymrbrace}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}UnionClosed{\isachardot}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}F\ {\isasymsubseteq}\ Pow\ {\isacharparenleft}{\isasymUnion}\ A{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}{\isasymforall}A{\isacharprime}{\isacharprime}{\isasymin}F{\isachardot}\ op\ {\isasymunion}\ A{\isacharprime}{\isacharprime}\ {\isacharbackquote}\ A{\isacharprime}\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ F{\isachardot}\ finite\ x{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F\ {\isasymsubseteq}\ Pow\ {\isacharparenleft}{\isasymUnion}\ A{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ X\ {\isasymin}\ A{\isacharprime}{\isachardot}\ finite\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymle}\ {\isacharparenleft}w{\isacharprime}\ {\isasymbowtie}\isactrlsub f\ F\ {\isacharparenleft}{\isasymUnion}A{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharbackquoteclose}{\isacharcomma}\ rule\ some{\isacharunderscore}share{\isacharunderscore}negativeFalse{\isacharunderscore}FamilyShare{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative\ A\ w\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}UnionClosed{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ {\isacharparenleft}closure\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharbackquoteclose}{\isacharbrackleft}THEN\ sym{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}UnionClosed{\isachardot}union{\isacharunderscore}closed\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}auto{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A{\isacharprime}{\isacharprime}\ x\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A{\isacharprime}{\isacharprime}\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}x\ {\isasymin}\ closure\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymunion}\ A{\isacharprime}{\isacharprime}\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}UnionClosed{\isachardot}union{\isacharunderscore}closed\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}{\isasymforall}\ A{\isacharprime}{\isacharprime}\ {\isasymin}\ F{\isachardot}\ image\ {\isacharparenleft}op\ {\isasymunion}\ A{\isacharprime}{\isacharprime}{\isacharparenright}\ A{\isacharprime}\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}additional{\isacharunderscore}set{\isacharbrackleft}of\ A{\isacharprime}\ x\ A{\isacharprime}{\isacharprime}\ F{\isacharbrackright}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}A{\isacharprime}{\isacharprime}\ {\isasymunion}\ x\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ Un{\isacharunderscore}commute{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}l{\isasymin}set\ A{\isachardot}\ inv\ l{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ F{\isachardot}\ x\ {\isasymsubseteq}\ {\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F\ {\isasymsubseteq}\ Pow\ {\isacharparenleft}{\isasymUnion}\ A{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ {\isasymUnion}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isachardot}\ Mapping{\isachardot}lookup\ w\ a\ {\isacharequal}\ Some\ {\isacharparenleft}w{\isacharprime}\ a{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ x\ {\isasymin}\ {\isasymUnion}\ A{\isacharprime}{\isachardot}\ Mapping{\isachardot}lookup\ w\ x\ {\isacharequal}\ Some\ {\isacharparenleft}w{\isacharprime}\ x{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A{\isacharprime}\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{end}\isamarkupfalse%
%
\isamarkupsubsection{Interpretations%
}
\isamarkuptrue%
%
\isamarkupsubsubsection{Representation of sets by lists%
}
\isamarkuptrue%
\isacommand{global{\isacharunderscore}interpretation}\isamarkupfalse%
\ SomeShareNegativeImpl{\isacharunderscore}lists{\isacharcolon}\isanewline
\ \ SomeShareNegativeImpl\ {\isachardoublequoteopen}{\isasymlambda}\ {\isacharparenleft}l{\isacharcolon}{\isacharcolon}nat\ list{\isacharparenright}{\isachardot}\ sorted\ l\ {\isasymand}\ distinct\ l{\isachardoublequoteclose}\ List{\isachardot}set\ set{\isacharunderscore}weight{\isacharunderscore}l\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}l\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ merge\ Pow{\isacharunderscore}l\ \ \isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ \isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Representation of sets by natural numbers%
}
\isamarkuptrue%
\isacommand{global{\isacharunderscore}interpretation}\isamarkupfalse%
\ SomeShareNegativeImpl{\isacharunderscore}nats{\isacharcolon}\isanewline
\ \ SomeShareNegativeImpl\ {\isachardoublequoteopen}{\isasymlambda}\ n{\isachardot}\ True{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isachardoublequoteclose}\ set{\isacharunderscore}weight{\isacharunderscore}n\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}n\ {\isadigit{0}}\ bitor\ pow{\isacharunderscore}n\ \isanewline
\ \ \isakeyword{defines}\isanewline
\ \ \ \ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SomeShareNegativeImpl{\isacharunderscore}nats{\isachardot}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional{\isacharunderscore}cached{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SomeShareNegativeImpl{\isacharunderscore}nats{\isachardot}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}{\isadigit{5}}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}n\ {\isacharequal}\ {\isachardoublequoteopen}SomeShareNegativeImpl{\isacharunderscore}nats{\isachardot}some{\isacharunderscore}share{\isacharunderscore}negative{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}unfold{\isacharunderscore}locales{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative\ A\ w\ {\isasymequiv}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}n\ {\isacharparenleft}map\ list{\isadigit{2}}nat\ A{\isacharparenright}\ w{\isachardoublequoteclose}\isanewline
\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}soundness{\isacharunderscore}nats{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ X\ {\isasymin}\ A{\isachardot}\ finite\ X{\isachardoublequoteclose}\ \isanewline
\ \ \ \ {\isachardoublequoteopen}set\ {\isacharparenleft}map\ set\ A{\isacharprime}{\isacharparenright}\ {\isacharequal}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ X\ {\isasymin}\ set\ A{\isacharprime}{\isachardot}\ distinct\ X\ {\isasymand}\ sorted\ X{\isachardoublequoteclose}\ \isanewline
\ \ \ \ {\isachardoublequoteopen}w{\isacharprime}\ {\isacharequal}\ Mapping{\isachardot}tabulate\ {\isacharparenleft}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ {\isacharparenleft}{\isasymUnion}\ A{\isacharparenright}{\isacharparenright}\ w{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative\ A{\isacharprime}\ w{\isacharprime}\ {\isacharequal}\ False\ {\isasymLongrightarrow}\ uce{\isacharunderscore}shares{\isacharunderscore}nonneg\ A\ w{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ SomeShareNegativeImpl{\isacharunderscore}nats{\isachardot}some{\isacharunderscore}share{\isacharunderscore}negativeSound{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isacharequal}\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}n\ {\isacharparenleft}map\ list{\isadigit{2}}nat\ A{\isacharprime}{\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\ A{\isacharprime}\ {\isacharequal}\ set\ {\isacharbackquote}\ set\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ X\ {\isasymin}\ set\ A{\isacharprime}{\isachardot}\ distinct\ X\ {\isasymand}\ sorted\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ nat{\isadigit{2}}list{\isacharunderscore}list{\isadigit{2}}nat\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}set\ {\isacharparenleft}map\ set\ A{\isacharprime}{\isacharparenright}\ {\isacharequal}\ A{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}x{\isasymin}{\isasymUnion}A{\isachardot}\ Mapping{\isachardot}lookup\ w{\isacharprime}\ x\ {\isacharequal}\ Some\ {\isacharparenleft}w\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}w{\isacharprime}\ {\isacharequal}\ Mapping{\isachardot}tabulate\ {\isacharparenleft}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ {\isacharparenleft}{\isasymUnion}\ A{\isacharparenright}{\isacharparenright}\ w{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isacharequal}\ SetImpl{\isacharunderscore}nats{\isachardot}f{\isacharunderscore}to{\isacharunderscore}set\ {\isacharparenleft}map\ list{\isadigit{2}}nat\ A{\isacharprime}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ assms\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ weights{\isadigit{2}}map\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}weights{\isadigit{2}}map\ l\ {\isacharequal}\ foldl\ {\isacharparenleft}{\isasymlambda}\ w\ {\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}{\isachardot}\ w\ {\isacharparenleft}k\ {\isacharcolon}{\isacharequal}\ v{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}\ {\isacharunderscore}{\isachardot}\ {\isadigit{0}}{\isacharparenright}\ l{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ weights{\isadigit{2}}map{\isacharunderscore}snoc{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}weights{\isadigit{2}}map\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}weights{\isadigit{2}}map\ xs{\isacharparenright}\ {\isacharparenleft}fst\ x\ {\isacharcolon}{\isacharequal}\ snd\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ weights{\isadigit{2}}map{\isacharunderscore}def\ split{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ ssn\ \isakeyword{where}\isanewline
{\isachardoublequoteopen}ssn\ f\ w\ {\isacharequal}\ some{\isacharunderscore}share{\isacharunderscore}negative\ f\ {\isacharparenleft}tabulate\ w{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isanewline
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
