%
\begin{isabellebody}%
\setisabellecontext{Frankl}%
%
\isamarkupsection{Frankl's condition%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Frankl\isanewline
\isakeyword{imports}\ Family\ UnionClosed\ More{\isachardot}MoreSet\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsubsection{Frankl's condition%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Note that, in order to avoid using rational numbers, the
following condition is not formulated as \isa{count\ x\ F\ {\isasymge}\ {\isacharparenleft}card\ F{\isacharparenright}\ {\isacharslash}\ {\isadigit{2}}}, what would be more expected.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{abbreviation}\isamarkupfalse%
\ frankl{\isacharunderscore}element\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}frankl{\isacharunderscore}element\ x\ F\ {\isasymequiv}\ x\ {\isasymin}\ {\isasymUnion}\ F\ {\isasymand}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ x\ F\ {\isasymge}\ card\ F{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ frankl\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}frankl\ F\ {\isasymequiv}\ {\isacharparenleft}{\isasymexists}\ x{\isachardot}\ frankl{\isacharunderscore}element\ x\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ obtain{\isacharunderscore}frankl{\isacharunderscore}element{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}frankl\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{obtains}\ x\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ x\ F\ {\isasymge}\ card\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ frankl{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Frankl's function%
}
\isamarkuptrue%
\isacommand{abbreviation}\isamarkupfalse%
\ frankl{\isacharunderscore}fun\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ x\ F\ {\isasymequiv}\ {\isadigit{2}}\ {\isacharasterisk}\ int\ {\isacharparenleft}count\ x\ F{\isacharparenright}\ {\isacharminus}\ int\ {\isacharparenleft}card\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}frankl{\isacharunderscore}element\ x\ F\ {\isasymlongleftrightarrow}\ {\isacharparenleft}x\ {\isasymin}\ {\isasymUnion}\ F\ {\isasymand}\ frankl{\isacharunderscore}fun\ x\ F\ {\isasymge}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ frankl{\isacharunderscore}fun{\isacharunderscore}Un{\isacharunderscore}disjoint{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasyminter}\ B\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ B{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}A\ {\isasymunion}\ B{\isacharparenright}\ {\isacharequal}\ frankl{\isacharunderscore}fun\ a\ A\ {\isacharplus}\ frankl{\isacharunderscore}fun\ a\ B{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}A\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}S{\isachardot}\ S\ {\isasymin}\ A\ {\isasymand}\ a\ {\isasymin}\ S{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isacharquery}B\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}S{\isachardot}\ S\ {\isasymin}\ B\ {\isasymand}\ a\ {\isasymin}\ S{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharbraceleft}S{\isachardot}\ {\isacharparenleft}S\ {\isasymin}\ A\ {\isasymunion}\ B{\isacharparenright}\ {\isasymand}\ a\ {\isasymin}\ S{\isacharbraceright}\ {\isacharequal}\ {\isacharquery}A\ {\isasymunion}\ {\isacharquery}B{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharquery}A\ {\isasyminter}\ {\isacharquery}B\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharbraceleft}S{\isachardot}\ {\isacharparenleft}S\ {\isasymin}\ A\ {\isasymunion}\ B{\isacharparenright}\ {\isasymand}\ a\ {\isasymin}\ S{\isacharbraceright}\ {\isacharequal}\ card\ {\isacharquery}A\ {\isacharplus}\ card\ {\isacharquery}B{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}Un{\isacharunderscore}disjoint{\isacharbrackleft}of\ {\isacharquery}A\ {\isacharquery}B{\isacharbrackright}\ \isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ count{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ card{\isacharunderscore}Un{\isacharunderscore}disjoint{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ frankl{\isacharunderscore}fun{\isacharunderscore}Un{\isacharunderscore}disjoint{\isacharunderscore}{\isadigit{3}}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ B{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ C{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}A\ {\isasyminter}\ B\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}A\ {\isasyminter}\ C\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}B\ {\isasyminter}\ C\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ i\ {\isacharparenleft}A\ {\isasymunion}\ B\ {\isasymunion}\ C{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ \ frankl{\isacharunderscore}fun\ i\ A\ {\isacharplus}\ frankl{\isacharunderscore}fun\ i\ B\ {\isacharplus}\ frankl{\isacharunderscore}fun\ i\ C{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\ frankl{\isacharunderscore}fun{\isacharunderscore}Un{\isacharunderscore}disjoint{\isacharbrackleft}of\ {\isachardoublequoteopen}A\ {\isasymunion}\ B{\isachardoublequoteclose}\ {\isachardoublequoteopen}C{\isachardoublequoteclose}\ i{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ assms\ frankl{\isacharunderscore}fun{\isacharunderscore}Un{\isacharunderscore}disjoint{\isacharbrackleft}of\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\ i{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ frankl{\isacharunderscore}fun{\isacharunderscore}UN{\isacharunderscore}disjoint{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ set\ l{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymforall}\ i\ j{\isachardot}\ i\ {\isacharless}\ length\ l\ {\isasymand}\ j\ {\isacharless}\ length\ l\ {\isasymand}\ i\ {\isasymnoteq}\ j\ {\isasymlongrightarrow}\ l\ {\isacharbang}\ i\ {\isasyminter}\ l\ {\isacharbang}\ j\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ i\ {\isacharparenleft}{\isasymUnion}\ set\ l{\isacharparenright}\ {\isacharequal}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}frankl{\isacharunderscore}fun\ i{\isacharparenright}\ \ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ l{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ Nil\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ count{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Cons\ a\ l{\isacharprime}{\isacharparenright}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}i\ j{\isachardot}\ i\ {\isacharless}\ length\ l{\isacharprime}\ {\isasymand}\ j\ {\isacharless}\ length\ l{\isacharprime}\ {\isasymand}\ i\ {\isasymnoteq}\ j\ {\isasymlongrightarrow}\ l{\isacharprime}\ {\isacharbang}\ i\ {\isasyminter}\ l{\isacharprime}\ {\isacharbang}\ j\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ i\ {\isacharparenleft}{\isasymUnion}\ set\ {\isacharparenleft}a\ {\isacharhash}\ l{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ frankl{\isacharunderscore}fun\ i\ {\isacharparenleft}a\ {\isasymunion}\ {\isacharparenleft}{\isasymUnion}\ set\ l{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ frankl{\isacharunderscore}fun\ i\ a\ {\isacharplus}\ frankl{\isacharunderscore}fun\ i\ {\isacharparenleft}{\isasymUnion}\ set\ l{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ frankl{\isacharunderscore}fun{\isacharunderscore}Un{\isacharunderscore}disjoint{\isacharbrackleft}of\ a\ {\isachardoublequoteopen}{\isasymUnion}\ {\isacharparenleft}set\ l{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\ i{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasyminter}\ {\isasymUnion}\ set\ l{\isacharprime}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ nth{\isacharunderscore}Cons{\isacharparenright}\ {\isacharparenleft}metis\ Suc{\isacharunderscore}less{\isacharunderscore}eq\ Zero{\isacharunderscore}not{\isacharunderscore}Suc\ disjoint{\isacharunderscore}iff{\isacharunderscore}not{\isacharunderscore}equal\ in{\isacharunderscore}set{\isacharunderscore}conv{\isacharunderscore}nth\ nth{\isachardot}simps\ nth{\isacharunderscore}Cons{\isacharunderscore}{\isadigit{0}}\ nth{\isacharunderscore}Cons{\isacharunderscore}Suc\ zero{\isacharunderscore}less{\isacharunderscore}Suc{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\ {\isacharparenleft}insert\ Cons{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isacharcomma}\ auto{\isacharparenright}\isanewline
\ \ \ \ \isacommand{finally}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Cons{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ frankl{\isacharunderscore}fun{\isacharunderscore}Pow{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}a\ {\isasymin}\ A{\isachardoublequoteclose}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}frankl{\isacharunderscore}fun\ a\ {\isacharparenleft}Pow\ A{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ A{\isacharprime}{\isachardot}\ A\ {\isacharequal}\ A{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}a{\isacharbraceright}\ {\isasymand}\ a\ {\isasymnotin}\ A{\isacharprime}\ {\isasymand}\ finite\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}A\ {\isacharminus}\ {\isacharbraceleft}a{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ auto\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ A{\isacharprime}\ \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isacharequal}\ A{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}a{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}a\ {\isasymnotin}\ A{\isacharprime}{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}finite\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}PA{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}Pow\ A{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isacharquery}aPA{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}op\ {\isasymunion}\ {\isacharbraceleft}a{\isacharbraceright}{\isacharparenright}\ {\isacharbackquote}\ Pow\ A{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}Pow\ A\ {\isacharequal}\ {\isacharquery}PA{\isacharprime}\ {\isasymunion}\ {\isacharquery}aPA{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ Pow{\isacharunderscore}insert{\isacharbrackleft}of\ a\ A{\isacharprime}{\isacharbrackright}\ {\isacharbackquoteopen}A\ {\isacharequal}\ A{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}a{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ image{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}PA{\isacharprime}\ {\isasyminter}\ {\isacharquery}aPA{\isacharprime}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymnotin}\ A{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}count\ a\ {\isacharparenleft}Pow\ A{\isacharparenright}\ {\isacharequal}\ count\ a\ {\isacharquery}PA{\isacharprime}\ {\isacharplus}\ count\ a\ {\isacharquery}aPA{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ A{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ count{\isacharunderscore}Un{\isacharunderscore}disjoint{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharbraceleft}S{\isachardot}\ S\ {\isasymsubseteq}\ A{\isacharprime}\ {\isasymand}\ a\ {\isasymin}\ S{\isacharbraceright}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymnotin}\ A{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}count\ a\ {\isacharquery}PA{\isacharprime}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ A{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ count{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}count\ a\ {\isacharquery}aPA{\isacharprime}\ {\isacharequal}\ card\ {\isacharquery}PA{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharbraceleft}S\ {\isasymin}\ op\ {\isasymunion}\ {\isacharbraceleft}a{\isacharbraceright}\ {\isacharbackquote}\ Pow\ A{\isacharprime}{\isachardot}\ a\ {\isasymin}\ S{\isacharbraceright}\ {\isacharequal}\ op\ {\isasymunion}\ {\isacharbraceleft}a{\isacharbraceright}\ {\isacharbackquote}\ Pow\ A{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}count\ a\ {\isacharparenleft}op\ {\isasymunion}\ {\isacharbraceleft}a{\isacharbraceright}\ {\isacharbackquote}\ Pow\ A{\isacharprime}{\isacharparenright}\ {\isacharequal}\ card\ {\isacharparenleft}op\ {\isasymunion}\ {\isacharbraceleft}a{\isacharbraceright}\ {\isacharbackquote}\ Pow\ A{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ count{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ card\ {\isacharparenleft}Pow\ A{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymnotin}\ A{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ card{\isacharunderscore}image{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ inj{\isacharunderscore}on{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{finally}\isamarkupfalse%
\ \isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isacharequal}\ A{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}a{\isacharbraceright}{\isacharbackquoteclose}\ {\isacharbackquoteopen}a\ {\isasymnotin}\ A{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ A{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ card{\isacharunderscore}Pow{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{FC Families%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ FC{\isacharunderscore}family\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc\ {\isasymequiv}\ \isanewline
\ \ \ \ {\isasymforall}\ F{\isachardot}\ F\ {\isasymsupseteq}\ Fc\ {\isasymand}\ finite{\isacharunderscore}union{\isacharunderscore}closed\ F\ {\isasymlongrightarrow}\isanewline
\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}\ a\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F\ {\isasymge}\ card\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}frankl{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}Fc\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite{\isacharunderscore}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}frankl\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ Fc\ {\isasymsubseteq}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}def\ frankl{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}mono{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}Fc\ {\isasymsubseteq}\ Fc{\isacharprime}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc{\isacharprime}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}def\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ F\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}Fc{\isacharprime}\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}Fc\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ \ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ Fc{\isacharprime}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ a\ \isakeyword{where}\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ F\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}FC{\isacharunderscore}family\ Fc{\isacharbackquoteclose}\ {\isacharbackquoteopen}union{\isacharunderscore}closed\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}a{\isasymin}{\isasymUnion}Fc{\isacharprime}{\isachardot}\ card\ F\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Fc\ {\isasymsubseteq}\ Fc{\isacharprime}{\isacharbackquoteclose}\ {\isacharbackquoteopen}Fc{\isacharprime}\ {\isasymsubseteq}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}empty{\isacharunderscore}set{\isacharunderscore}remove{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc\ {\isasymlongleftrightarrow}\ FC{\isacharunderscore}family\ {\isacharparenleft}Fc\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ {\isacharparenleft}Fc\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}def\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}safe{\isacharparenright}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ F\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}Fc\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}\ {\isasymsubseteq}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}union{\isacharunderscore}closed\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}Fc\ {\isasymsubseteq}\ F\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite{\isacharunderscore}union{\isacharunderscore}closed\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ union{\isacharunderscore}closed{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ a\ \isakeyword{where}\ {\isachardoublequoteopen}a{\isasymin}{\isasymUnion}Fc{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}FC{\isacharunderscore}family\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ F\ {\isasymle}\ card\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff\ card{\isacharunderscore}insert{\isacharunderscore}le{\isacharparenright}\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharbraceleft}A{\isachardot}\ {\isacharparenleft}A\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}\ {\isasymor}\ A\ {\isasymin}\ F{\isacharparenright}\ {\isasymand}\ a\ {\isasymin}\ A{\isacharbraceright}\ {\isacharequal}\ {\isacharbraceleft}A\ {\isasymin}\ F{\isachardot}\ a\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ count\ a\ {\isacharparenleft}F\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ count{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ F\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}{\isacharparenleft}Fc\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}a{\isasymin}{\isasymUnion}{\isacharparenleft}Fc\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardot}\ card\ F\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ {\isacharparenleft}Fc\ {\isacharminus}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}empty{\isacharunderscore}set{\isacharunderscore}insert{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ {\isacharparenleft}Fc\ {\isasymunion}\ {\isacharbraceleft}{\isacharbraceleft}{\isacharbraceright}{\isacharbraceright}{\isacharparenright}\ {\isasymlongleftrightarrow}\ FC{\isacharunderscore}family\ Fc{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ FC{\isacharunderscore}family{\isacharunderscore}empty{\isacharunderscore}set{\isacharunderscore}remove\ Diff{\isacharunderscore}insert{\isacharunderscore}absorb\ Un{\isacharunderscore}empty{\isacharunderscore}right\ Un{\isacharunderscore}insert{\isacharunderscore}right\ insert{\isacharunderscore}absorb{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}closure{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc\ {\isasymlongleftrightarrow}\ FC{\isacharunderscore}family\ {\isacharparenleft}closure\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc{\isachardoublequoteclose}\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}Fc\ {\isasymsubseteq}\ closure\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ closure{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ {\isacharparenleft}closure\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ {\isacharparenleft}closure\ Fc{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}FC{\isacharunderscore}family\ Fc{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ FC{\isacharunderscore}family{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ closure{\isacharunderscore}min{\isacharunderscore}closed{\isacharbrackleft}of\ Fc{\isacharbrackright}\ {\isacharbackquoteopen}finite\ Fc{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\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:
