%
\begin{isabellebody}%
\setisabellecontext{UnionClosed}%
%
\isamarkupsection{Union closed families%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ UnionClosed\isanewline
\isakeyword{imports}\ Main\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsubsection{Union closed families%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ sum{\isacharunderscore}family\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymuplus}{\isachardoublequoteclose}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}A\ {\isasymuplus}\ B\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isachardot}\ a\ {\isasymunion}\ b{\isacharparenright}\ {\isacharbackquote}\ {\isacharbraceleft}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isachardot}\ a\ {\isasymin}\ A\ {\isasymand}\ b\ {\isasymin}\ B{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ union{\isacharunderscore}closed\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F\ {\isasymequiv}\ {\isasymforall}\ A\ B{\isachardot}\ A\ {\isasymin}\ F\ {\isasymand}\ B\ {\isasymin}\ F\ {\isasymlongrightarrow}\ A\ {\isasymunion}\ B\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F\ {\isasymlongleftrightarrow}\ F\ {\isasymuplus}\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\ sum{\isacharunderscore}family{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\ \ \isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ finite{\isacharunderscore}union{\isacharunderscore}closed\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}finite{\isacharunderscore}union{\isacharunderscore}closed\ F\ {\isasymequiv}\ union{\isacharunderscore}closed\ F\ {\isasymand}\ finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}n{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}F{\isacharprime}\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isacharprime}\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ F{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ empty\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}insert\ a\ F{\isacharprime}{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ insert\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}F{\isacharprime}{\isacharprime}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ union{\isacharunderscore}closed{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}insert{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ B\ {\isasymin}\ F{\isachardot}\ A\ {\isasymunion}\ B\ {\isasymin}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Un{\isacharunderscore}commute{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Closure -- minimal union closed family containing F%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ closure\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}closure\ F\ {\isacharequal}\ Union\ {\isacharbackquote}\ {\isacharparenleft}Pow\ F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ closure{\isacharunderscore}closed{\isacharcolon}\ \isanewline
\ \ {\isachardoublequoteopen}union{\isacharunderscore}closed\ {\isacharparenleft}closure\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}{\isacharparenleft}rule\ allI{\isacharparenright}{\isacharplus}\ {\isacharcomma}\ rule\ impI{\isacharcomma}\ erule\ conjE{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ A\ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set{\isachardoublequoteclose}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ xa\ xb\ \isakeyword{where}\isanewline
\ \ \ \ {\isachardoublequoteopen}A\ {\isacharequal}\ {\isasymUnion}\ xa{\isachardoublequoteclose}\ {\isachardoublequoteopen}xa\ {\isasymin}\ Pow\ F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ {\isachardoublequoteopen}B\ {\isacharequal}\ {\isasymUnion}\ xb{\isachardoublequoteclose}\ {\isachardoublequoteopen}xb\ {\isasymin}\ Pow\ F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ closure{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}xa\ {\isasymunion}\ {\isasymUnion}xb\ {\isacharequal}\ {\isasymUnion}\ {\isacharparenleft}xa\ {\isasymunion}\ xb{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}xa\ {\isasymunion}\ xb\ {\isasymin}\ Pow\ F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}xa\ {\isasymin}\ Pow\ F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}xb\ {\isasymin}\ Pow\ F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ B\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isacharequal}\ {\isasymUnion}\ xa{\isacharbackquoteclose}\ {\isacharbackquoteopen}B\ {\isacharequal}\ {\isasymUnion}\ xb{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ closure{\isacharunderscore}min{\isacharunderscore}closed{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}F\ {\isasymsubseteq}\ F{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}closure\ F\ {\isasymsubseteq}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ S\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isacharequal}\ {\isasymUnion}\ S{\isachardoublequoteclose}\ {\isachardoublequoteopen}S\ {\isasymin}\ Pow\ F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}n{\isacharbrackleft}of\ S\ F{\isacharprime}{\isacharbrackright}\ {\isacharbackquoteopen}union{\isacharunderscore}closed\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}F\ {\isasymsubseteq}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}subset\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ closure{\isacharunderscore}union{\isacharunderscore}closed{\isacharunderscore}id{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}closure\ F\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\ closure{\isacharunderscore}min{\isacharunderscore}closed{\isacharbrackleft}of\ F\ F{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ closure{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymUnion}\ {\isacharparenleft}closure\ F{\isacharparenright}\ {\isacharequal}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ finite{\isacharunderscore}closure{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ {\isacharparenleft}closure\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ closure{\isacharunderscore}mono{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F\ {\isasymsubseteq}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}closure\ F\ {\isasymsubseteq}\ closure\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Iterative closure: insert set to closed family and close.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{abbreviation}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close\ A\ F\ {\isasymequiv}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}\ {\isasymunion}\ {\isacharparenleft}op\ {\isasymunion}\ A{\isacharparenright}\ {\isacharbackquote}\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ {\isacharparenleft}insert{\isacharunderscore}and{\isacharunderscore}close\ A\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ \ closure{\isacharunderscore}insert{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}closure\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ insert{\isacharunderscore}and{\isacharunderscore}close\ A\ {\isacharparenleft}closure\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isacharequal}\ {\isacharquery}rhs{\isachardoublequoteclose}{\isacharparenright}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isasymsubseteq}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ union{\isacharunderscore}closed{\isacharunderscore}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharbrackleft}of\ {\isachardoublequoteopen}closure\ F{\isachardoublequoteclose}\ A{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}closed{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}min{\isacharunderscore}closed{\isacharbrackleft}of\ {\isachardoublequoteopen}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}\ {\isacharquery}rhs{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ closure{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}rhs\ {\isasymsubseteq}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}rhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ closure\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}\ {\isasymor}\ x\ {\isasymin}\ op\ {\isasymunion}\ A\ {\isacharbackquote}\ {\isacharparenleft}closure\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ closure\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ closure\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ closure{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ op\ {\isasymunion}\ A\ {\isacharbackquote}\ {\isacharparenleft}closure\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ y\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isacharequal}\ y\ {\isasymunion}\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ k\ \isakeyword{where}\ {\isachardoublequoteopen}k\ {\isasymin}\ Pow\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isacharequal}\ {\isasymUnion}\ k{\isachardoublequoteclose}\ {\isachardoublequoteopen}k\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ rev{\isacharunderscore}image{\isacharunderscore}eqI{\isacharbrackleft}of\ {\isachardoublequoteopen}k\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}x\ {\isacharequal}\ y\ {\isasymunion}\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}y\ {\isacharequal}\ {\isasymUnion}\ k{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}k\ {\isasymin}\ Pow\ F{\isacharbackquoteclose}\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%
\ closure{\isacharunderscore}subset{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}F\ {\isasymsubseteq}\ closure\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ closure{\isacharunderscore}empty{\isacharcolon}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}\ {\isasymin}\ closure\ F\ {\isasymlongleftrightarrow}\ {\isacharbraceleft}{\isacharbraceright}\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}subset{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ force%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}empty{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close\ {\isacharbraceleft}{\isacharbraceright}\ F\ {\isacharequal}\ F\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\ \isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ closure{\isacharunderscore}remove{\isacharunderscore}empty{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}closure\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ closure\ F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}\ {\isasymin}\ F{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}F\ {\isacharequal}\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}closure\ F\ {\isacharequal}\ closure\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharbackquoteopen}F\ {\isacharequal}\ {\isacharparenleft}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharbackquoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ closure{\isacharunderscore}insert{\isacharbrackleft}of\ {\isachardoublequoteopen}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ assms{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}empty{\isacharparenright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ True\ closure{\isacharunderscore}empty{\isacharbrackleft}of\ {\isachardoublequoteopen}F\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}empty{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}closure{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}closure\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ insert{\isacharunderscore}and{\isacharunderscore}close\ A\ F{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isacharequal}\ {\isacharquery}rhs{\isachardoublequoteclose}{\isacharparenright}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}insert{\isacharbrackleft}of\ F\ A{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}union{\isacharunderscore}closed{\isacharunderscore}id{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ simp%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Union closed families closed to unions with an additional family%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}additional\ \isakeyword{where}\ \isanewline
\ \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ Fc\ {\isasymequiv}\isanewline
\ \ \ \ \ \ \ \ \ \ \ union{\isacharunderscore}closed\ F\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ A\ {\isasymin}\ F{\isachardot}\ {\isacharparenleft}op\ {\isasymunion}\ A{\isacharparenright}\ {\isacharbackquote}\ Fc\ {\isasymsubseteq}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ Fc\ {\isasymlongleftrightarrow}\ F\ {\isasymuplus}\ F\ {\isacharequal}\ F\ {\isasymand}\ F\ {\isasymuplus}\ Fc\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}def\ union{\isacharunderscore}closed{\isacharunderscore}def\ sum{\isacharunderscore}family{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto\ force%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\ \ \isanewline
\isacommand{lemma}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharcolon}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymforall}\ A\ {\isasymin}\ F{\isachardot}\ {\isasymforall}\ Ai\ {\isasymin}\ Fc{\isachardot}\ A\ {\isasymunion}\ Ai\ {\isasymin}\ F{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}\ A\ {\isasymin}\ F{\isachardot}\ {\isacharparenleft}op\ {\isasymunion}\ A{\isacharparenright}\ {\isacharbackquote}\ Fc\ {\isasymsubseteq}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}insert{\isacharunderscore}and{\isacharunderscore}close{\isacharunderscore}additional\ A\ F\ Fc\ {\isasymequiv}\ F\ {\isasymunion}\ {\isacharbraceleft}A{\isacharbraceright}\ {\isasymunion}\ {\isacharparenleft}{\isacharparenleft}op\ {\isasymunion}\ A{\isacharparenright}\ {\isacharbackquote}\ F{\isacharparenright}\ {\isasymunion}\ {\isacharparenleft}{\isacharparenleft}op\ {\isasymunion}\ A{\isacharparenright}\ {\isacharbackquote}\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ closure{\isacharunderscore}additional{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}A\ {\isasymin}\ closure\ F{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ {\isachardoublequoteopen}A{\isacharprime}\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ A{\isacharprime}\ {\isasymin}\ F{\isacharprime}{\isachardot}\ op\ {\isasymunion}\ A{\isacharprime}\ {\isacharbackquote}\ F\ {\isasymsubseteq}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}A\ {\isasymunion}\ A{\isacharprime}\ {\isasymin}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isasymunion}\ A{\isacharprime}\ {\isacharbackquote}\ F\ {\isasymsubseteq}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isasymforall}A{\isacharprime}{\isasymin}F{\isacharprime}{\isachardot}\ image\ {\isacharparenleft}op\ {\isasymunion}\ A{\isacharprime}{\isacharparenright}\ F\ {\isasymsubseteq}\ F{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}A{\isacharprime}\ {\isasymin}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ X\ \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isacharequal}\ {\isasymUnion}\ X{\isachardoublequoteclose}\ {\isachardoublequoteopen}X\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}X\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymin}\ closure\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ closure{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymunion}\ A{\isacharprime}\ {\isacharequal}\ {\isasymUnion}\ {\isacharparenleft}{\isacharparenleft}op\ {\isasymunion}\ A{\isacharprime}{\isacharparenright}\ {\isacharbackquote}\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isacharequal}\ {\isasymUnion}\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}X\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharbackquoteopen}A\ {\isasymunion}\ A{\isacharprime}\ {\isacharequal}\ {\isasymUnion}\ image\ {\isacharparenleft}op\ {\isasymunion}\ A{\isacharprime}{\isacharparenright}\ X{\isacharbackquoteclose}{\isacharcomma}\ rule\ union{\isacharunderscore}closed{\isacharunderscore}n{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}op\ {\isasymunion}\ A{\isacharprime}\ {\isacharbackquote}\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isasymunion}\ A{\isacharprime}\ {\isacharbackquote}\ X\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}X\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isasymunion}\ A{\isacharprime}\ {\isacharbackquote}\ X\ {\isasymsubseteq}\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}image\ {\isacharparenleft}op\ {\isasymunion}\ A{\isacharprime}{\isacharparenright}\ F\ {\isasymsubseteq}\ F{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}X\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ fact\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}closure{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ Fc{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ {\isacharparenleft}closure\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\ y\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}y\ {\isasymin}\ closure\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymunion}\ y\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}additional{\isacharunderscore}set{\isacharbrackleft}of\ Fc\ y\ x\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ Fc{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Un{\isacharunderscore}commute{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Union closed extensions%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ union{\isacharunderscore}closed{\isacharunderscore}extensions\ \isakeyword{where}\isanewline
\ \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}union{\isacharunderscore}closed{\isacharunderscore}extensions\ Fc\ {\isasymequiv}\isanewline
\ \ \ \ \ \ \ \ \ \ \ {\isacharbraceleft}F{\isachardot}\ F\ {\isasymsubseteq}\ Pow\ {\isacharparenleft}{\isasymUnion}\ Fc{\isacharparenright}\ {\isasymand}\ union{\isacharunderscore}closed{\isacharunderscore}additional\ F\ Fc{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{syntax}\isamarkupfalse%
\isanewline
\ \ {\isachardoublequoteopen}{\isacharunderscore}union{\isacharunderscore}closed{\isacharunderscore}extensions{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set\ set{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymlbrace}{\isacharunderscore}{\isasymrbrace}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{translations}\isamarkupfalse%
\ \isanewline
\ \ {\isachardoublequoteopen}{\isasymlbrace}Fc{\isasymrbrace}{\isachardoublequoteclose}\ {\isacharequal}{\isacharequal}\ {\isachardoublequoteopen}CONST\ union{\isacharunderscore}closed{\isacharunderscore}extensions\ Fc{\isachardoublequoteclose}\isanewline
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
