%
\begin{isabellebody}%
\setisabellecontext{WeightsShares{\isacharunderscore}Frankl}%
%
\isamarkupsubsection{Frankl's families characterization using weights%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ WeightsShares{\isacharunderscore}Frankl\isanewline
\isakeyword{imports}\ Main\ WeightsShares\isanewline
\ \ \ \ \ \ \ \ More{\isachardot}MoreBigOperators\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ frankl{\isacharunderscore}weight{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ w\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ \isanewline
\ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub f\ F{\isacharparenright}\ {\isasymge}\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isacharasterisk}\ card\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ x{\isachardot}\ frankl{\isacharunderscore}element\ x\ F\ {\isasymand}\ w\ x\ {\isasymnoteq}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharquery}thesis{\isachardoublequoteclose}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}\ x{\isachardot}\ x\ {\isasymin}\ {\isasymUnion}\ F\ {\isasymand}\ w\ x\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ {\isadigit{2}}\ {\isacharasterisk}\ count\ x\ F\ {\isacharless}\ card\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ a{\isadigit{0}}\ \isakeyword{where}\ {\isachardoublequoteopen}a{\isadigit{0}}\ {\isasymin}\ {\isasymUnion}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}w\ a{\isadigit{0}}\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}a{\isasymin}{\isasymUnion}F{\isachardot}\ {\isadigit{0}}\ {\isasymle}\ w\ a{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ weight{\isacharunderscore}fun{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub f\ F{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}\ F{\isachardot}\ {\isacharparenleft}w\ a{\isacharparenright}{\isacharasterisk}\ {\isacharparenleft}count\ a\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ family{\isacharunderscore}weight{\isacharunderscore}lemma\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}\ F{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}w\ a{\isacharparenright}{\isacharasterisk}\ {\isacharparenleft}count\ a\ F{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}\ F{\isachardot}\ {\isacharparenleft}w\ a{\isacharparenright}\ {\isacharasterisk}\ card\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isacharunderscore}mono{\isacharunderscore}single{\isacharunderscore}lt{\isacharunderscore}nat{\isacharparenright}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
\ assms\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ a\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}F{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ w\ a\ {\isacharasterisk}\ {\isacharparenleft}count\ a\ F{\isacharparenright}\ {\isasymle}\ w\ a\ {\isacharasterisk}\ {\isacharparenleft}card\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}a{\isadigit{0}}\ {\isasymin}\ {\isasymUnion}F{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a{\isadigit{0}}\ {\isasymin}\ {\isasymUnion}F{\isacharbackquoteclose}\ \ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ w\ a{\isadigit{0}}\ {\isacharasterisk}\ {\isacharparenleft}count\ a{\isadigit{0}}\ F{\isacharparenright}\ {\isacharless}\ w\ a{\isadigit{0}}\ {\isacharasterisk}\ {\isacharparenleft}card\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharbackquoteopen}a{\isadigit{0}}\ {\isasymin}\ {\isasymUnion}F{\isacharbackquoteclose}\ {\isacharbackquoteopen}w\ a{\isadigit{0}}\ {\isachargreater}\ {\isadigit{0}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isacharasterisk}\ card\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sum{\isacharunderscore}distrib{\isacharunderscore}right{\isacharparenright}\isanewline
\ \ \isacommand{finally}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}\ F{\isachardot}\ {\isacharparenleft}w\ a{\isacharparenright}{\isacharasterisk}\ {\isacharparenleft}count\ a\ F{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}card\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sum{\isacharunderscore}distrib{\isacharunderscore}left\ mult{\isachardot}assoc{\isacharparenright}\isanewline
\ \ \isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}\ F{\isachardot}\ {\isacharparenleft}w\ a{\isacharparenright}{\isacharasterisk}\ {\isacharparenleft}count\ a\ F{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}card\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{2}}\ {\isacharasterisk}\ w\ {\isasymrhd}\isactrlsub f\ F\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}\ F{\isachardot}\ {\isacharparenleft}w\ a{\isacharparenright}{\isacharasterisk}\ {\isacharparenleft}count\ a\ F{\isacharparenright}{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{2}}\ {\isacharasterisk}\ w\ {\isasymrhd}\isactrlsub f\ F\ {\isasymge}\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}card\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ frankl{\isacharunderscore}weight{\isacharprime}{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}frankl\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}F\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ w{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}{\isachardot}\ weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isasymand}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub f\ F{\isacharparenright}\ {\isasymge}\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isacharasterisk}\ card\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}frankl\ F{\isacharbackquoteclose}\ \isacommand{obtain}\isamarkupfalse%
\ a\ \isakeyword{where}\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F\ {\isasymge}\ card\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ frankl{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}w\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ x{\isachardot}\ if\ x\ {\isacharequal}\ a\ then\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ else\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}{\isasymUnion}F\ {\isasyminter}\ {\isacharbraceleft}a{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymin}\ {\isasymUnion}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymin}\ {\isasymUnion}\ F{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sum{\isachardot}If{\isacharunderscore}cases{\isacharparenright}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ S\ {\isasymin}\ F{\isachardot}\ {\isacharquery}w\ {\isasymrhd}\isactrlsub s\ S\ {\isacharequal}\ {\isacharparenleft}if\ a\ {\isasymin}\ S\ then\ {\isadigit{1}}\ else\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sum{\isachardot}If{\isacharunderscore}cases\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}w\ {\isasymrhd}\isactrlsub f\ F\ {\isacharequal}\ count\ a\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ count{\isacharunderscore}def\ family{\isacharunderscore}weight{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sum{\isachardot}If{\isacharunderscore}cases\ Collect{\isacharunderscore}conj{\isacharunderscore}eq\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharquery}w\ {\isasymrhd}\isactrlsub f\ F{\isacharparenright}\ {\isasymge}\ card{\isacharparenleft}F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isadigit{2}}\ {\isacharasterisk}\ count\ a\ F\ {\isasymge}\ card\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharquery}w\ {\isasymrhd}\isactrlsub f\ F{\isacharparenright}\ {\isasymge}\ {\isacharparenleft}{\isacharquery}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isacharasterisk}\ card\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ {\isacharbackquoteopen}{\isacharquery}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isacharbackquoteclose}{\isacharparenright}\ simp\isanewline
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}weight{\isacharunderscore}fun\ {\isacharquery}w\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymin}\ {\isasymUnion}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ weight{\isacharunderscore}fun{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{theorem}\isamarkupfalse%
\ frankl{\isacharunderscore}weight{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}frankl\ F\ {\isasymlongleftrightarrow}\isanewline
\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}\ w{\isacharcolon}{\isacharcolon}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isachardot}\ weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isasymand}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub f\ F{\isacharparenright}\ {\isasymge}\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isacharasterisk}\ card\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}lhs\ {\isasymlongleftrightarrow}\ {\isacharquery}rhs{\isachardoublequoteclose}{\isacharparenright}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isacharquery}lhs\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}rhs\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ frankl{\isacharunderscore}weight{\isacharprime}{\isacharprime}{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isacharquery}rhs\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ w\ \isakeyword{where}\ {\isachardoublequoteopen}weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}w\ {\isasymrhd}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}\ {\isacharasterisk}\ card\ F\ {\isasymle}\ {\isadigit{2}}\ {\isacharasterisk}\ w\ {\isasymrhd}\isactrlsub f\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}lhs\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ frankl{\isacharunderscore}weight{\isacharprime}{\isacharbrackleft}of\ F\ w{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ frankl{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Frankl's families characterization using shares%
}
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ frankl{\isacharunderscore}share{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ a{\isachardot}\ frankl{\isacharunderscore}element\ a\ F\ {\isasymand}\ w\ a\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ frankl{\isacharunderscore}weight{\isacharprime}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
\ \isacommand{using}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}lemma{\isacharbrackleft}of\ F\ w\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \isacommand{by}\isamarkupfalse%
\ linarith%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ frankl{\isacharunderscore}share{\isacharprime}{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}frankl\ F{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ w{\isachardot}\ weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\ \isanewline
\isacommand{using}\isamarkupfalse%
\ frankl{\isacharunderscore}weight{\isacharprime}{\isacharprime}{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}lemma{\isacharbrackleft}of\ F\ {\isacharunderscore}\ {\isachardoublequoteopen}{\isasymUnion}F{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}smt\ of{\isacharunderscore}nat{\isacharunderscore}le{\isacharunderscore}iff{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Sufficient condition for Frankl using hypershares.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
\ frankl{\isacharunderscore}share{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}frankl\ F\ {\isasymlongleftrightarrow}\ {\isacharparenleft}{\isasymexists}\ w{\isachardot}\ weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\ frankl{\isacharunderscore}share{\isacharprime}{\isacharbrackleft}of\ F{\isacharbrackright}\ frankl{\isacharunderscore}share{\isacharprime}{\isacharprime}{\isacharbrackleft}of\ F{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ frankl{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ force%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{theorem}\isamarkupfalse%
\ frankl{\isacharunderscore}hyper{\isacharunderscore}share{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}F\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}weight{\isacharunderscore}fun\ w\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}K{\isacharprime}\ {\isasymunion}\ S\ {\isacharequal}\ {\isasymUnion}\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}K{\isacharprime}\ {\isasyminter}\ S\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ K\ {\isasymin}\ Pow\ K{\isacharprime}{\isachardot}\ \ {\isacharparenleft}w\ {\isasymodot}\isactrlsub f\isactrlsub \ K\ S\ F\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isasymge}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ a{\isachardot}\ frankl{\isacharunderscore}element\ a\ F\ {\isasymand}\ w\ a\ {\isasymnoteq}\ {\isadigit{0}}\ {\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ frankl{\isacharunderscore}share{\isacharprime}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
\isacommand{using}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}hyper{\isacharunderscore}share{\isacharbrackleft}of\ F\ K{\isacharprime}\ S{\isacharbrackright}\ sum{\isacharunderscore}nonneg\isanewline
\isacommand{by}\isamarkupfalse%
\ fastforce%
\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:
