%
\begin{isabellebody}%
\setisabellecontext{SomeShareNegative}%
%
\isamarkupsection{SomeShareNegative --- combinatorial search for union-closed extension with a negative share%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ SomeShareNegative\isanewline
\isakeyword{imports}\ Main\ WeightsShares{\isacharunderscore}FCFamily\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\begin{isamarkuptext}%
According to the theorem

%
\begin{isabelle}%
{\isasymlbrakk}weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}Fc{\isacharparenright}{\isacharsemicolon}\ {\isasymforall}F{\isacharprime}{\isasymin}{\isasymlbrace}Fc{\isasymrbrace}{\isachardot}\ {\isadigit{0}}\ {\isasymle}\ w\ {\isasymbowtie}\isactrlsub f\ F{\isacharprime}\ {\isasymUnion}Fc{\isasymrbrakk}\ {\isasymLongrightarrow}\ FC{\isacharunderscore}family\ Fc%
\end{isabelle}

to show that a family is an FC family, it suffices to show that there
is no member of union closed extension of a given family with a
negative share. The function \isa{some{\isacharunderscore}share{\isacharunderscore}negative} performs a
combinatorial enumeration of union closed extensions of a given family
and checks whether it contains a family with a negative share with
respect to the given weight function. We give a rather abstract
(nonexecutable) definition of this function and prove its main
properties. This function will be later refined and a more efficient,
executable implementation will be given.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{primrec}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set\ \ {\isasymRightarrow}\ {\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ {\isacharbrackleft}{\isacharbrackright}\ Ft\ Fc\ w\ X\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ Ft\ X{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ Ft\ Fc\ w\ X\ {\isacharequal}\ \isanewline
\ \ \ \ {\isacharparenleft}if\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ Ft\ X{\isacharparenright}\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ A\ X{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}\ then\isanewline
\ \ \ \ \ \ \ \ False\isanewline
\ \ \ \ \ else\ if\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ t\ Ft\ Fc\ w\ X\ then\isanewline
\ \ \ \ \ \ \ \ True\isanewline
\ \ \ \ \ else\ if\ h\ {\isasymin}\ Ft\ then\isanewline
\ \ \ \ \ \ \ \ False\isanewline
\ \ \ \ \ else\isanewline
\ \ \ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ t\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ h\ Ft\ Fc{\isacharparenright}\ Fc\ w\ X\isanewline
\ \ \ \ {\isacharparenright}\isanewline
{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}soundness{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ L\ Ft\ Fc\ w\ X\ {\isacharequal}\ False{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ set\ L{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ A\ X{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}distinct\ L{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}F\ {\isasymsupseteq}\ Ft{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ Fc{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ F\ {\isacharminus}\ Ft{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ A\ X{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ A\ {\isasymin}\ List{\isachardot}set\ L{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F\ X{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ L\ arbitrary{\isacharcolon}\ Ft{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}ss\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ A{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ A\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharquery}ss\ F\ {\isacharequal}\ sum\ {\isacharquery}ss\ {\isacharparenleft}Ft\ {\isasymunion}\ {\isacharparenleft}F\ {\isacharminus}\ Ft{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}cong{\isacharbrackleft}of\ F\ {\isachardoublequoteopen}Ft\ {\isasymunion}\ {\isacharparenleft}F\ {\isacharminus}\ Ft{\isacharparenright}{\isachardoublequoteclose}\ {\isacharquery}ss\ {\isacharquery}ss{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F\ {\isasymsupseteq}\ Ft{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ sum\ {\isacharquery}ss\ Ft\ {\isacharplus}\ sum\ {\isacharquery}ss\ {\isacharparenleft}F\ {\isacharminus}\ Ft{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}union{\isacharunderscore}disjoint{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}F\ {\isasymsupseteq}\ Ft{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \ \ \isacommand{finally}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharquery}ss\ F\ {\isacharequal}\ sum\ {\isacharquery}ss\ Ft\ {\isacharplus}\ sum\ {\isacharquery}ss\ {\isacharparenleft}F\ {\isacharminus}\ Ft{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharquery}ss\ {\isacharparenleft}F\ {\isacharminus}\ Ft{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isacharunderscore}nonneg{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}A{\isasymin}F\ {\isacharminus}\ Ft{\isachardot}\ set{\isacharunderscore}share\ A\ w\ X\ {\isacharless}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ A\ {\isasymin}\ set\ {\isacharbrackleft}{\isacharbrackright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharquery}ss\ Ft\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ {\isacharbrackleft}{\isacharbrackright}\ Ft\ Fc\ w\ X\ {\isacharequal}\ False{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ family{\isacharunderscore}share{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ family{\isacharunderscore}share{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ h\ t{\isacharparenright}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}ss\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ A{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ A\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}family{\isacharunderscore}share\ Ft\ w\ X\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharquery}ss\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Fp\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}A{\isachardot}\ A\ {\isasymin}\ F\ {\isacharminus}\ Ft\ {\isasymand}\ {\isacharquery}ss\ A\ {\isasymge}\ {\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Fn\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}A{\isachardot}\ A\ {\isasymin}\ F\ {\isacharminus}\ Ft\ {\isasymand}\ {\isacharquery}ss\ A\ {\isacharless}\ {\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}A{\isasymin}F{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isacharequal}\ \ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharparenleft}F\ {\isacharminus}\ Ft{\isacharparenright}\ {\isasymunion}\ Ft{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}cong{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Ft\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharparenleft}F\ {\isacharminus}\ Ft{\isacharparenright}{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}{\isasymSum}A{\isasymin}Ft{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}union{\isacharunderscore}disjoint{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}F\ {\isasymsupseteq}\ Ft{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \ \ \isacommand{finally}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}A{\isasymin}F{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharparenleft}F\ {\isacharminus}\ Ft{\isacharparenright}{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}{\isasymSum}A{\isasymin}Ft{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \ \ \isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharparenleft}F\ {\isacharminus}\ Ft{\isacharparenright}{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}Fp\ {\isasymunion}\ {\isacharquery}Fn{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}cong{\isacharparenright}\ auto\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}Fp{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}Fn{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}union{\isacharunderscore}disjoint{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{finally}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharparenleft}F\ {\isacharminus}\ Ft{\isacharparenright}{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}Fp{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}Fn{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}Fp{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isacharunderscore}nonneg{\isacharparenright}\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}A{\isasymin}F{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isasymge}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}Fn{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}{\isasymSum}A{\isasymin}Ft{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}L\ {\isacharequal}\ {\isachardoublequoteopen}set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharquery}ss\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}L{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}distinct\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ sum{\isacharunderscore}list{\isacharunderscore}distinct{\isacharunderscore}conv{\isacharunderscore}sum{\isacharunderscore}set{\isacharparenright}\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}L{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharparenleft}{\isacharquery}Fn\ {\isasymunion}\ {\isacharparenleft}{\isacharquery}L\ {\isacharminus}\ {\isacharquery}Fn{\isacharparenright}{\isacharparenright}{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}cong{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}A{\isasymin}F\ {\isacharminus}\ \ Ft{\isachardot}\ {\isacharquery}ss\ A\ {\isacharless}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ A\ {\isasymin}\ List{\isachardot}set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\ auto\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}Fn{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharparenleft}{\isacharquery}L\ {\isacharminus}\ {\isacharquery}Fn{\isacharparenright}{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}union{\isacharunderscore}disjoint{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isasymle}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}Fn{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharparenleft}{\isacharquery}L\ {\isacharminus}\ {\isacharquery}Fn{\isacharparenright}{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isasymle}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isacharunderscore}nonpos{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ A\ {\isasymin}\ set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isachardot}\ {\isacharquery}ss\ A\ {\isacharless}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{finally}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F\ X{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isacharparenleft}{\isasymSum}A{\isasymin}F{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isasymge}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}Fn{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}{\isasymSum}A{\isasymin}Ft{\isachardot}\ {\isacharquery}ss\ A{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ Ft\ X{\isacharparenright}\ {\isacharplus}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharquery}ss\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{note}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharequal}\ this\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ t\ Ft\ Fc\ w\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ Ft\ Fc\ w\ X\ {\isacharequal}\ False{\isacharbackquoteclose}\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{note}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharequal}\ {\isacharasterisk}\ this\isanewline
\ \ \ \ \isacommand{note}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharequal}\ {\isacharasterisk}\ {\isacharbackquoteopen}finite\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}Ft\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}A{\isasymin}set\ t{\isachardot}\ {\isacharquery}ss\ A\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}A{\isasymin}set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isachardot}\ {\isacharquery}ss\ A\ {\isacharless}\ {\isadigit{0}}{\isacharbackquoteclose}\ {\isacharbackquoteopen}distinct\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{note}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharequal}\ {\isacharasterisk}\ this\isanewline
\ \ \ \ \isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}h\ {\isasymin}\ Ft{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ Cons\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Ft{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ h\ Ft\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}s{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}family{\isacharunderscore}share\ {\isacharquery}Ft{\isacharprime}\ w\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}h\ {\isasymin}\ F{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ t\ {\isacharquery}Ft{\isacharprime}\ Fc\ w\ X\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}\ Ft\ Fc\ w\ X\ {\isacharequal}\ False{\isacharbackquoteclose}\ {\isacharasterisk}\ {\isacharbackquoteopen}h\ {\isasymnotin}\ Ft{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ A\ {\isasymin}\ F\ {\isacharminus}\ {\isacharquery}Ft{\isacharprime}{\isachardot}\ {\isacharquery}ss\ A\ {\isacharless}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ A\ {\isasymin}\ set\ t{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}\ A\ {\isasymin}\ F\ {\isacharminus}\ Ft{\isachardot}\ {\isacharquery}ss\ A\ {\isacharless}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ A\ {\isasymin}\ set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}h\ {\isasymnotin}\ Ft{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Ft{\isacharprime}\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Ft\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}h\ {\isasymin}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ union{\isacharunderscore}closed{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ {\isacharasterisk}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharparenright}\ {\isacharbackquoteopen}{\isasymforall}A{\isasymin}F\ {\isacharminus}\ Ft{\isachardot}\ {\isacharquery}ss\ A\ {\isacharless}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ \ A\ {\isasymin}\ set\ {\isacharparenleft}h\ {\isacharhash}\ t{\isacharparenright}{\isacharbackquoteclose}\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
{\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative\ Fc\ w\ {\isasymequiv}\isanewline
\ \ let\ X\ {\isacharequal}\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharsemicolon}\isanewline
\ \ \ \ \ \ P\ {\isacharequal}\ Pow\ X{\isacharsemicolon}\isanewline
\ \ \ \ \ \ Fc\ {\isacharequal}\ closure\ Fc{\isacharsemicolon}\isanewline
\ \ \ \ \ \ N\ {\isacharequal}\ {\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ P\ {\isasymand}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ x\ X{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isacharbraceright}{\isacharsemicolon}\ \isanewline
\ \ \ \ \ \ L\ {\isacharequal}\ {\isacharparenleft}SOME\ L{\isachardot}\ distinct\ L\ {\isasymand}\ set\ L\ {\isacharequal}\ N{\isacharparenright}\ in\isanewline
\ \ \ \ \ \ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ L\ {\isacharbraceleft}{\isacharbraceright}\ Fc\ w\ X{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}soundness{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative\ Fc\ w\ {\isacharequal}\ False{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}F\ {\isasymin}\ {\isasymlbrace}\ Fc\ {\isasymrbrace}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ \ \ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux{\isacharunderscore}soundness{\isacharparenright}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymUnion}\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}P\ {\isacharequal}\ {\isachardoublequoteopen}Pow\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Fc\ {\isacharequal}\ {\isachardoublequoteopen}closure\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}N\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ {\isacharquery}P\ {\isasymand}\ set{\isacharunderscore}share\ x\ w\ {\isacharquery}X\ {\isacharless}\ {\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}L\ {\isacharequal}\ {\isachardoublequoteopen}SOME\ L{\isachardot}\ distinct\ L\ {\isasymand}\ set\ L\ {\isacharequal}\ {\isacharquery}N{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}distinct\ {\isacharquery}L\ {\isasymand}\ set\ {\isacharquery}L\ {\isacharequal}\ {\isacharquery}N{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ someI{\isacharunderscore}ex{\isacharparenright}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharquery}N{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ L{\isachardot}\ distinct\ L\ {\isasymand}\ set\ L\ {\isacharequal}\ {\isacharquery}N{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ ex{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}aux\ {\isacharquery}L\ {\isacharbraceleft}{\isacharbraceright}\ {\isacharquery}Fc\ w\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}def\ Let{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ set\ {\isacharquery}L{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ a\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}distinct\ {\isacharquery}L{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a\ {\isasymin}\ F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceright}{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ a\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ a\ {\isasymin}\ set\ {\isacharquery}L{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F\ {\isasymin}\ {\isasymlbrace}\ Fc\ {\isasymrbrace}{\isacharbackquoteclose}\ {\isacharasterisk}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F\ {\isasymin}\ {\isasymlbrace}\ Fc\ {\isasymrbrace}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharbackquoteclose}\ \isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ {\isacharparenleft}closure\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}F\ {\isasymin}\ {\isasymlbrace}\ Fc\ {\isasymrbrace}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isacharbackquoteclose}\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}closure{\isacharbrackleft}of\ Fc\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ assms{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{theorem}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}soundness{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}some{\isacharunderscore}share{\isacharunderscore}negative\ Fc\ w\ {\isacharequal}\ False\ {\isasymLongrightarrow}\ uce{\isacharunderscore}shares{\isacharunderscore}nonneg\ Fc\ w{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}soundness{\isacharprime}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
