%
\begin{isabellebody}%
\setisabellecontext{WeightsShares}%
%
\isamarkupsection{Weights and shares%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ WeightsShares\isanewline
\isakeyword{imports}\ Main\ Frankl\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsubsection{Weight functions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A technique, introduced by Poonen, used for analyzing Frankl's conjecture 
is based on the concept of weights and shares.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ weight{\isacharunderscore}fun\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharcolon}{\isacharcolon}{\isacharbraceleft}zero{\isacharcomma}ord{\isacharbraceright}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}weight{\isacharunderscore}fun\ w\ X\ {\isasymequiv}\ {\isacharparenleft}{\isasymforall}\ a\ {\isasymin}\ X{\isachardot}\ w\ a\ {\isasymge}\ {\isadigit{0}}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ a\ {\isasymin}\ X{\isachardot}\ w\ a\ {\isachargreater}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ set{\isacharunderscore}weight\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharcolon}{\isacharcolon}{\isacharbraceleft}comm{\isacharunderscore}monoid{\isacharunderscore}add{\isacharbraceright}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymrhd}\isactrlsub s{\isachardoublequoteclose}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}w\ {\isasymrhd}\isactrlsub s\ S\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}x{\isasymin}S{\isachardot}\ w\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ family{\isacharunderscore}weight\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharcolon}{\isacharcolon}{\isacharbraceleft}comm{\isacharunderscore}monoid{\isacharunderscore}add{\isacharbraceright}{\isacharparenright}\ {\isasymRightarrow}{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ \ {\isacharprime}b{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymrhd}\isactrlsub f{\isachardoublequoteclose}\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}w\ {\isasymrhd}\isactrlsub f\ F\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}S{\isasymin}F{\isachardot}\ w\ {\isasymrhd}\isactrlsub s\ S{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}cong{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ v\ {\isasymin}\ S{\isachardot}\ w\ v\ {\isacharequal}\ w{\isacharprime}\ v{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}w\ {\isasymrhd}\isactrlsub s\ S\ {\isacharequal}\ w{\isacharprime}\ {\isasymrhd}\isactrlsub s\ S{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}cong{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ family{\isacharunderscore}weight{\isacharunderscore}lemma{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}w\ {\isasymrhd}\isactrlsub f\ F\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}F{\isachardot}\ {\isacharparenleft}w\ a{\isacharparenright}\ {\isacharasterisk}\ count\ a\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}w\ {\isasymrhd}\isactrlsub f\ F\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}S{\isasymin}F{\isachardot}\ {\isasymSum}a{\isasymin}S{\isachardot}\ w\ a{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ family{\isacharunderscore}weight{\isacharunderscore}def\ set{\isacharunderscore}weight{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}\ F{\isachardot}\ {\isacharparenleft}w\ a{\isacharparenright}{\isacharasterisk}\ {\isacharparenleft}{\isasymSum}{\isacharunderscore}{\isasymin}{\isacharbraceleft}S\ {\isasymin}\ F{\isachardot}\ a\ {\isasymin}\ S{\isacharbraceright}{\isachardot}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ a{\isachardot}\ {\isacharbraceleft}S\ {\isasymin}\ F{\isachardot}\ a\ {\isasymin}\ S{\isacharbraceright}\ {\isasymtimes}\ {\isacharbraceleft}a{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}S{\isacharprime}\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ x{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}S{\isacharcomma}\ a{\isacharparenright}{\isachardot}\ S\ {\isasymin}\ F\ {\isasymand}\ a\ {\isasymin}\ S{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}CS\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharbackquote}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}S{\isasymin}F{\isachardot}\ {\isasymSum}a{\isasymin}S{\isachardot}\ w\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}{\isacharparenleft}S{\isacharcomma}\ a{\isacharparenright}{\isasymin}{\isacharparenleft}SIGMA\ S{\isacharcolon}F{\isachardot}\ S{\isacharparenright}{\isachardot}\ w\ a{\isacharparenright}{\isachardoublequoteclose}\ \isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ sum{\isachardot}Sigma\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}{\isacharparenleft}S{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ {\isacharquery}S{\isacharprime}\ a{\isachardot}\ w\ a{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ Collect{\isacharunderscore}case{\isacharunderscore}prod{\isacharunderscore}Sigma{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}\ x{\isachardot}\ x\ {\isasymin}\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymlambda}\ x\ y{\isachardot}\ y\ {\isasymin}\ x{\isachardoublequoteclose}{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}{\isacharparenleft}S{\isacharcomma}\ a{\isacharparenright}{\isasymin}{\isasymUnion}{\isacharquery}CS{\isachardot}\ w\ a{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}cong{\isacharparenright}\ auto\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}A{\isasymin}{\isacharquery}CS{\isachardot}\ {\isacharparenleft}{\isasymSum}x{\isasymin}A{\isachardot}\ w{\isacharparenleft}snd\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}Union{\isacharunderscore}disjoint{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ split{\isacharunderscore}def\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}\ F{\isachardot}\ {\isacharparenleft}{\isasymSum}x{\isasymin}{\isacharquery}S\ a{\isachardot}\ w\ {\isacharparenleft}snd\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}reindex{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}sum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ w\ {\isacharparenleft}snd\ x{\isacharparenright}{\isacharparenright}\ {\isasymcirc}\ {\isacharquery}S{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}\ F{\isachardot}\ sum\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ w\ {\isacharparenleft}snd\ x{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}{\isacharquery}S\ a{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}cong{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ a\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ w\ {\isacharparenleft}snd\ x{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}{\isacharquery}S\ a{\isacharparenright}\ {\isacharequal}\ sum\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ {\isacharparenleft}w\ a{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}{\isacharquery}S\ a{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}cong{\isacharparenright}\ auto\isanewline
\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}sum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ w\ {\isacharparenleft}snd\ x{\isacharparenright}{\isacharparenright}\ {\isasymcirc}\ {\isacharquery}S{\isacharparenright}\ a\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}x{\isasymin}{\isacharbraceleft}S\ {\isasymin}\ F{\isachardot}\ a\ {\isasymin}\ S{\isacharbraceright}\ {\isasymtimes}\ {\isacharbraceleft}a{\isacharbraceright}{\isachardot}\ w\ {\isacharparenleft}snd\ x{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ {\isacharbackquoteopen}a\ {\isasymin}\ {\isasymUnion}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharquery}S\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}F{\isachardot}\ w\ a\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}x{\isasymin}{\isacharbraceleft}S\ {\isasymin}\ F{\isachardot}\ a\ {\isasymin}\ S{\isacharbraceright}{\isachardot}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}cong{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ a\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymin}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ w\ {\isacharparenleft}snd\ x{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}{\isacharquery}S\ a{\isacharparenright}\ {\isacharequal}\ sum\ {\isacharparenleft}{\isasymlambda}\ x{\isachardot}\ {\isacharparenleft}w\ a{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}{\isacharquery}S\ a{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}cong{\isacharparenright}\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}x{\isasymin}{\isacharbraceleft}S\ {\isasymin}\ F{\isachardot}\ a\ {\isasymin}\ S{\isacharbraceright}\ {\isasymtimes}\ {\isacharbraceleft}a{\isacharbraceright}{\isachardot}\ w\ {\isacharparenleft}snd\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ w\ a\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}x{\isasymin}{\isacharbraceleft}S\ {\isasymin}\ F{\isachardot}\ a\ {\isasymin}\ S{\isacharbraceright}{\isachardot}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ count{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ {\isacharbackquoteopen}a\ {\isasymin}\ {\isasymUnion}\ F{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{finally}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}\ F{\isachardot}\ {\isacharparenleft}w\ a{\isacharparenright}{\isacharasterisk}\ {\isacharparenleft}count\ a\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ count{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{finally}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ sum{\isacharunderscore}card{\isacharunderscore}reorder{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}A{\isasymin}F{\isachardot}\ card\ A{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}a{\isasymin}{\isasymUnion}F{\isachardot}\ count\ a\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\ family{\isacharunderscore}weight{\isacharunderscore}lemma{\isacharbrackleft}of\ F\ {\isachardoublequoteopen}{\isasymlambda}\ {\isacharunderscore}{\isachardot}\ {\isadigit{1}}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ family{\isacharunderscore}weight{\isacharunderscore}def\ set{\isacharunderscore}weight{\isacharunderscore}def{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Shares%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ set{\isacharunderscore}share\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}set{\isacharunderscore}share\ S\ w\ X\ {\isasymequiv}\ {\isadigit{2}}\ {\isacharasterisk}\ int\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub s\ S{\isacharparenright}\ {\isacharminus}\ int\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub s\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{syntax}\isamarkupfalse%
\isanewline
\ \ {\isachardoublequoteopen}{\isacharunderscore}set{\isacharunderscore}share{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}\ {\isasymbowtie}\isactrlsub s\ {\isacharunderscore}\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{translations}\isamarkupfalse%
\ \isanewline
\ \ {\isachardoublequoteopen}w\ {\isasymbowtie}\isactrlsub s\ S\ X{\isachardoublequoteclose}\ {\isacharequal}{\isacharequal}\ {\isachardoublequoteopen}CONST\ set{\isacharunderscore}share\ S\ w\ X{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ family{\isacharunderscore}share\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}family{\isacharunderscore}share\ F\ w\ X\ {\isasymequiv}\ {\isacharparenleft}{\isasymSum}S\ {\isasymin}\ F{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ S\ X{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{syntax}\isamarkupfalse%
\isanewline
\ \ {\isachardoublequoteopen}{\isacharunderscore}family{\isacharunderscore}share{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}\ {\isasymbowtie}\isactrlsub f\ {\isacharunderscore}\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{translations}\isamarkupfalse%
\ \isanewline
\ \ {\isachardoublequoteopen}w\ {\isasymbowtie}\isactrlsub f\ F\ X{\isachardoublequoteclose}\ {\isacharequal}{\isacharequal}\ {\isachardoublequoteopen}CONST\ family{\isacharunderscore}share\ F\ w\ X{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}cong{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ v\ {\isasymin}\ X{\isachardot}\ w\ v\ {\isacharequal}\ w{\isacharprime}\ v{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymUnion}\ F\ {\isasymsubseteq}\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F\ X{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}w{\isacharprime}\ {\isasymbowtie}\isactrlsub f\ F\ \ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}w\ {\isasymrhd}\isactrlsub s\ X\ {\isacharequal}\ w{\isacharprime}\ {\isasymrhd}\isactrlsub s\ X{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}cong{\isacharbrackleft}of\ X\ w\ w{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ S\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}S\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}w\ {\isasymrhd}\isactrlsub s\ S\ {\isacharequal}\ \ w{\isacharprime}\ {\isasymrhd}\isactrlsub s\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}cong{\isacharbrackleft}of\ S\ w\ w{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}def\ set{\isacharunderscore}share{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}Pow{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ {\isacharparenleft}Pow\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}X\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}P\ {\isacharequal}\ {\isachardoublequoteopen}Pow\ {\isacharquery}X{\isachardoublequoteclose}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ S\ {\isasymin}\ {\isacharquery}P{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ S\ {\isacharquery}X{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}{\isacharquery}X\ {\isacharminus}\ S{\isacharparenright}\ {\isacharquery}X{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ S\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}S\ {\isasymin}\ {\isacharquery}P{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ S{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isacharquery}X\ {\isacharminus}\ S{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}S\ {\isasymunion}\ {\isasymUnion}\ F\ {\isacharequal}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ S\ {\isacharquery}X{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}{\isacharquery}X\ {\isacharminus}\ S{\isacharparenright}\ {\isacharquery}X{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}share{\isacharunderscore}def\ set{\isacharunderscore}weight{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sum{\isachardot}union{\isacharunderscore}disjoint{\isacharbrackleft}of\ {\isachardoublequoteopen}S{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharquery}X\ {\isacharminus}\ S{\isachardoublequoteclose}\ w{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ field{\isacharunderscore}simps{\isacharparenright}\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}S{\isasymin}{\isacharquery}P{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ S\ {\isacharquery}X{\isacharparenright}{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}{\isasymSum}S{\isasymin}{\isacharquery}P{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}{\isacharquery}X\ {\isacharminus}\ S{\isacharparenright}\ {\isacharquery}X{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymSum}S{\isasymin}{\isacharquery}P{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ S\ {\isacharquery}X{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}{\isacharquery}X\ {\isacharminus}\ S{\isacharparenright}\ {\isacharquery}X{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sum{\isachardot}distrib{\isacharparenright}\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}S{\isasymin}{\isacharquery}P{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ S\ {\isacharquery}X{\isacharparenright}{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}{\isasymSum}S{\isasymin}{\isacharquery}P{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}{\isacharquery}X\ {\isacharminus}\ S{\isacharparenright}\ {\isacharquery}X{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}S{\isasymin}{\isacharquery}P{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}{\isacharquery}X\ {\isacharminus}\ S{\isacharparenright}\ {\isacharquery}X{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}S{\isasymin}Pow\ {\isacharquery}X{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ S\ {\isacharquery}X{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}inj{\isacharunderscore}on\ {\isacharparenleft}op\ {\isacharminus}\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}{\isacharparenright}\ {\isacharquery}P{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ inj{\isacharunderscore}on{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isacharminus}\ {\isacharparenleft}{\isasymUnion}F{\isacharparenright}\ {\isacharbackquote}\ {\isacharquery}P\ {\isacharequal}\ {\isacharquery}P{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ sum{\isachardot}reindex{\isacharbrackleft}of\ {\isachardoublequoteopen}{\isasymlambda}\ S{\isachardot}\ {\isacharquery}X\ {\isacharminus}\ S{\isachardoublequoteclose}\ {\isachardoublequoteopen}Pow\ {\isacharquery}X{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymlambda}\ S{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ S\ {\isacharquery}X{\isacharparenright}{\isachardoublequoteclose}{\isacharcomma}\ THEN\ sym{\isacharbrackright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}S{\isasymin}{\isacharquery}P{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ S\ {\isacharquery}X{\isacharparenright}{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}{\isasymSum}S{\isasymin}{\isacharquery}P{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}{\isasymUnion}F\ {\isacharminus}\ S{\isacharparenright}\ {\isacharquery}X{\isacharparenright}{\isacharparenright}\ \ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}S{\isasymin}{\isacharquery}P{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ S\ {\isacharquery}X{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}lemma{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F\ X{\isacharparenright}\ {\isacharequal}\ int\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ w\ {\isasymrhd}\isactrlsub f\ F{\isacharparenright}\ {\isacharminus}\ int\ {\isacharparenleft}w\ {\isasymrhd}\isactrlsub s\ X\ {\isacharasterisk}\ {\isacharparenleft}card\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}def\ set{\isacharunderscore}share{\isacharunderscore}def\ family{\isacharunderscore}weight{\isacharunderscore}def\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ diff{\isacharunderscore}conv{\isacharunderscore}add{\isacharunderscore}uminus\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}distrib{\isacharcomma}\ subst\ sum{\isacharunderscore}distrib{\isacharunderscore}left{\isacharbrackleft}THEN\ sym{\isacharbrackright}{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ int{\isacharunderscore}sum{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Hypercube construction%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ hypercube\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set{\isachardoublequoteclose}\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}hypercube\ K\ S\ {\isasymequiv}\ {\isacharbraceleft}L{\isachardot}\ {\isacharparenleft}K\ {\isasymsubseteq}\ L{\isacharparenright}\ {\isasymand}\ L\ {\isasymsubseteq}\ {\isacharparenleft}K\ {\isasymunion}\ S{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\isacommand{syntax}\isamarkupfalse%
\isanewline
\ \ {\isachardoublequoteopen}{\isacharunderscore}hypercube{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymlangle}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isasymrangle}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{translations}\isamarkupfalse%
\ \isanewline
\ \ {\isachardoublequoteopen}{\isasymlangle}K{\isacharcomma}\ S{\isasymrangle}{\isachardoublequoteclose}\ {\isacharequal}{\isacharequal}\ {\isachardoublequoteopen}CONST\ hypercube\ K\ S{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ hypercube{\isacharunderscore}Pow{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlangle}K{\isacharcomma}\ S{\isasymrangle}\ {\isacharequal}\ {\isacharparenleft}op\ {\isasymunion}\ K{\isacharparenright}\ {\isacharbackquote}\ Pow\ S{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}H\ {\isacharequal}\ {\isacharquery}KP{\isachardoublequoteclose}{\isacharparenright}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}H\ {\isasymsubseteq}\ {\isacharquery}KP{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ M\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}M\ {\isasymin}\ {\isasymlangle}K{\isacharcomma}\ S{\isasymrangle}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ L\ \isakeyword{where}\ {\isachardoublequoteopen}L\ {\isasymsubseteq}\ S{\isachardoublequoteclose}\ {\isachardoublequoteopen}M\ {\isacharequal}\ K\ {\isasymunion}\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ hypercube{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}M\ {\isasymin}\ {\isacharquery}KP{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}KP\ {\isasymsubseteq}\ {\isacharquery}H{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ hypercube{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ hypercube{\isacharunderscore}inter{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}K{\isadigit{1}}\ {\isasymnoteq}\ K{\isadigit{2}}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}K{\isadigit{1}}\ {\isasyminter}\ S\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}K{\isadigit{2}}\ {\isasyminter}\ S\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymlangle}K{\isadigit{1}}{\isacharcomma}\ S{\isasymrangle}\ {\isasyminter}\ {\isasymlangle}K{\isadigit{2}}{\isacharcomma}\ S{\isasymrangle}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ hypercube{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ hypercube{\isacharunderscore}UN{\isacharunderscore}Pow{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymUnion}\ {\isacharparenleft}{\isacharparenleft}{\isasymlambda}\ K{\isachardot}\ {\isasymlangle}K{\isacharcomma}\ S{\isasymrangle}{\isacharparenright}\ {\isacharbackquote}\ {\isacharparenleft}Pow\ K{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Pow\ {\isacharparenleft}K\ {\isasymunion}\ S{\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{unfolding}\isamarkupfalse%
\ hypercube{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\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{show}\isamarkupfalse%
\ {\isachardoublequoteopen}X\ {\isasymin}\ {\isacharquery}lhs{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Kx\ {\isacharequal}\ {\isachardoublequoteopen}X\ {\isasyminter}\ K{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}Cx\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlangle}{\isacharquery}Kx{\isacharcomma}\ S{\isasymrangle}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}Kx\ {\isasymin}\ Pow\ K{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}X\ {\isasymin}\ {\isacharquery}Cx{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}X\ {\isasymin}\ {\isacharquery}rhs{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ hypercube{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{definition}\isamarkupfalse%
\ hyper{\isacharunderscore}share\ \isakeyword{where}\ \isanewline
\ \ {\isachardoublequoteopen}hyper{\isacharunderscore}share\ K\ S\ F\ w\ X\ {\isasymequiv}\ {\isacharparenleft}{\isasymSum}L\ {\isasymin}\ {\isasymlangle}K{\isacharcomma}\ S{\isasymrangle}\ {\isasyminter}\ F{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ L\ X{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{syntax}\isamarkupfalse%
\isanewline
\ \ {\isachardoublequoteopen}{\isacharunderscore}hyper{\isacharunderscore}share{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}\ {\isasymodot}\isactrlsub f\isactrlsub \ {\isacharunderscore}\ {\isacharunderscore}\ {\isacharunderscore}\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{translations}\isamarkupfalse%
\ \isanewline
\ \ {\isachardoublequoteopen}w\ {\isasymodot}\isactrlsub f\isactrlsub \ K\ S\ F\ X{\isachardoublequoteclose}\ {\isacharequal}{\isacharequal}\ {\isachardoublequoteopen}CONST\ hyper{\isacharunderscore}share\ K\ S\ F\ w\ X{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}hyper{\isacharunderscore}share{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}K{\isacharprime}\ {\isasymunion}\ S\ {\isacharequal}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}K{\isacharprime}\ {\isasyminter}\ S\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ F\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}K\ {\isasymin}\ Pow\ K{\isacharprime}{\isachardot}\ {\isacharparenleft}w\ {\isasymodot}\isactrlsub f\isactrlsub \ K\ S\ F\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}w\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}\ S{\isachardot}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ S\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}H\ {\isacharequal}\ {\isachardoublequoteopen}{\isasymlambda}K{\isachardot}\ {\isasymlangle}K{\isacharcomma}\ S{\isasymrangle}\ {\isasyminter}\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}K\ {\isacharequal}\ {\isachardoublequoteopen}Pow\ K{\isacharprime}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{let}\isamarkupfalse%
\ {\isacharquery}C\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharquery}H\ {\isacharbackquote}\ {\isacharquery}K{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymUnion}\ {\isacharquery}C\ {\isacharequal}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ hypercube{\isacharunderscore}UN{\isacharunderscore}Pow{\isacharbrackleft}of\ S\ K{\isacharprime}{\isacharbrackright}\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}K\ {\isasymin}\ {\isacharquery}K{\isachardot}\ {\isacharparenleft}w\ {\isasymodot}\isactrlsub f\isactrlsub \ K\ S\ F\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}L\ {\isasymin}\ {\isasymUnion}\ {\isacharquery}C{\isachardot}\ {\isacharquery}w\ L{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymSum}L\ {\isasymin}\ {\isasymUnion}\ {\isacharquery}C{\isachardot}\ {\isacharquery}w\ L{\isacharparenright}\ {\isacharequal}\ sum\ {\isacharparenleft}sum\ {\isacharquery}w{\isacharparenright}\ {\isacharquery}C{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}Union{\isacharunderscore}disjoint{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ L\ {\isasymin}\ {\isacharquery}C{\isachardot}\ finite\ L{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ finiteUn{\isacharunderscore}iff{\isacharparenright}\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}A{\isasymin}{\isacharquery}C{\isachardot}\ {\isasymforall}B{\isasymin}{\isacharquery}C{\isachardot}\ A\ {\isasymnoteq}\ B\ {\isasymlongrightarrow}\ A\ {\isasyminter}\ B\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ A\ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isacharquery}C{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Ka\ \isakeyword{where}\ {\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}Ka\ {\isasymin}\ {\isacharquery}K{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharquery}H\ Ka\ {\isacharequal}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}B{\isasymin}{\isacharquery}C{\isachardot}\ A\ {\isasymnoteq}\ B\ {\isasymlongrightarrow}\ A\ {\isasyminter}\ B\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ B\ \isacommand{assume}\isamarkupfalse%
\ \ {\isachardoublequoteopen}B\ {\isasymin}\ {\isacharquery}C{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Kb\ \isakeyword{where}\ {\isacharasterisk}{\isacharasterisk}{\isacharcolon}\ {\isachardoublequoteopen}Kb\ {\isasymin}\ {\isacharquery}K{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharquery}H\ Kb\ {\isacharequal}\ B{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymnoteq}\ B\ {\isasymlongrightarrow}\ A\ {\isasyminter}\ B\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymnoteq}\ B{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}Ka\ {\isasymnoteq}\ Kb{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}Ka\ {\isasyminter}\ S\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Kb\ {\isasyminter}\ S\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}Ka\ {\isasymin}\ {\isacharquery}K{\isacharbackquoteclose}\ {\isacharbackquoteopen}Kb\ {\isasymin}\ {\isacharquery}K{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymlangle}Ka{\isacharcomma}\ S{\isasymrangle}\ {\isasyminter}\ {\isasymlangle}Kb{\isacharcomma}\ S{\isasymrangle}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ hypercube{\isacharunderscore}inter{\isacharbrackleft}of\ Ka\ Kb\ S{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasyminter}\ B\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharasterisk}{\isacharasterisk}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{also}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}K{\isasymin}{\isacharquery}K{\isachardot}\ sum\ {\isacharquery}w\ {\isacharparenleft}{\isacharquery}H\ K{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}reindex{\isacharunderscore}nontrivial{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharquery}K{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}subset{\isacharbrackleft}of\ K{\isacharprime}\ {\isachardoublequoteopen}{\isasymUnion}\ F{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ Kx\ Ky\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}Kx\ {\isasymin}\ {\isacharquery}K{\isachardoublequoteclose}\ {\isachardoublequoteopen}Ky\ {\isasymin}\ {\isacharquery}K{\isachardoublequoteclose}\ {\isachardoublequoteopen}Kx\ {\isasymnoteq}\ Ky{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharquery}H\ Kx\ {\isacharequal}\ {\isacharquery}H\ Ky{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymlangle}Kx{\isacharcomma}\ S{\isasymrangle}\ {\isasyminter}\ {\isasymlangle}Ky{\isacharcomma}\ S{\isasymrangle}\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ hypercube{\isacharunderscore}inter{\isacharbrackleft}of\ Kx\ Ky\ S{\isacharbrackright}\ assms\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
\ {\isacharbackquoteopen}{\isacharquery}H\ Kx\ {\isacharequal}\ {\isacharquery}H\ Ky{\isacharbackquoteclose}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharquery}H\ Kx\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}sum\ {\isacharquery}w\ {\isacharparenleft}{\isacharquery}H\ Kx{\isacharparenright}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \isacommand{finally}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ hyper{\isacharunderscore}share{\isacharunderscore}def\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}def\ hyper{\isacharunderscore}share{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\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:
