%
\begin{isabellebody}%
\setisabellecontext{WeightsSharesImpl}%
%
\isamarkupsubsection{Abstract representation of sets and families with weights and shares%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ WeightsSharesImpl\isanewline
\isakeyword{imports}\ WeightsShares\ FamilyImpl\isanewline
\ \ \ \ \ \ \ \ {\isachardoublequoteopen}HOL{\isacharminus}Library{\isachardot}Mapping{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ {\isachardoublequoteopen}HOL{\isacharminus}Library{\isachardot}RBT{\isacharunderscore}Mapping{\isachardoublequoteclose}\ {\isachardoublequoteopen}HOL{\isacharminus}Library{\isachardot}RBT{\isacharunderscore}Impl{\isachardoublequoteclose}\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{locale}\isamarkupfalse%
\ SetWeightsSharesImpl\ {\isacharequal}\ SetImpl\ to{\isacharunderscore}set\ inv\ \isakeyword{for}\ \isanewline
\ \ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{and}\ to{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequoteclose}\ {\isacharplus}\isanewline
\ \ \isakeyword{fixes}\ set{\isacharunderscore}weight\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ set{\isacharunderscore}weight{\isacharunderscore}set{\isacharcolon}\ {\isachardoublequoteopen}inv\ A\ {\isasymLongrightarrow}\ set{\isacharunderscore}weight\ w\ A\ {\isacharequal}\ w\ {\isasymrhd}\isactrlsub s\ to{\isacharunderscore}set\ A{\isachardoublequoteclose}\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ set{\isacharunderscore}share\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}set{\isacharunderscore}share\ A\ w\ X\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ int\ {\isacharparenleft}set{\isacharunderscore}weight\ w\ A{\isacharparenright}\ {\isacharminus}\ int\ {\isacharparenleft}set{\isacharunderscore}weight\ w\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ family{\isacharunderscore}share\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}family{\isacharunderscore}share\ F\ w\ X\ {\isacharequal}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ A{\isachardot}\ set{\isacharunderscore}share\ A\ w\ X{\isacharparenright}\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}share{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}inv\ x{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}inv\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set{\isacharunderscore}share\ x\ w\ X\ {\isacharequal}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub s\ {\isacharparenleft}to{\isacharunderscore}set\ x{\isacharparenright}\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ WeightsShares{\isachardot}set{\isacharunderscore}share{\isacharunderscore}def\ set{\isacharunderscore}share{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ set{\isacharunderscore}weight{\isacharunderscore}set{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isasymforall}\ l\ {\isasymin}\ set\ F{\isachardot}\ inv\ l{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}inv\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}family{\isacharunderscore}share\ F\ w\ X\ {\isacharequal}\ {\isacharparenleft}w\ {\isasymbowtie}\isactrlsub f\ {\isacharparenleft}f{\isacharunderscore}to{\isacharunderscore}set\ F{\isacharparenright}\ {\isacharparenleft}to{\isacharunderscore}set\ X{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ family{\isacharunderscore}share{\isacharunderscore}def\ WeightsShares{\isachardot}family{\isacharunderscore}share{\isacharunderscore}def\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isacharunderscore}list{\isacharunderscore}distinct{\isacharunderscore}conv{\isacharunderscore}sum{\isacharunderscore}set{\isacharparenright}\isanewline
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{apply}\isamarkupfalse%
\ simp{\isacharunderscore}all\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isachardot}reindex{\isacharparenright}\isanewline
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ to{\isacharunderscore}set{\isacharunderscore}inj{\isacharunderscore}on{\isacharparenright}\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ sum{\isachardot}cong{\isacharparenright}\isanewline
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ set{\isacharunderscore}share{\isacharunderscore}set{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{end}\isamarkupfalse%
%
\isamarkupsubsubsection{Implementation by sorted and distinct lists%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}l\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isakeyword{where}\isanewline
\ {\isachardoublequoteopen}set{\isacharunderscore}weight{\isacharunderscore}l\ w\ S\ {\isacharequal}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ w\ S{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}l{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}distinct\ A{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set{\isacharunderscore}weight{\isacharunderscore}l\ w\ A\ {\isacharequal}\ w\ {\isasymrhd}\isactrlsub s\ set\ A{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}l{\isacharunderscore}def\ set{\isacharunderscore}weight{\isacharunderscore}def\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isacharunderscore}list{\isacharunderscore}distinct{\isacharunderscore}conv{\isacharunderscore}sum{\isacharunderscore}set{\isacharparenright}\isanewline
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ simp{\isacharunderscore}all%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{global{\isacharunderscore}interpretation}\isamarkupfalse%
\ SetWeightsSharesImpl{\isacharunderscore}lists{\isacharcolon}\ SetWeightsSharesImpl\ {\isachardoublequoteopen}{\isasymlambda}\ {\isacharparenleft}l{\isacharcolon}{\isacharcolon}nat\ list{\isacharparenright}{\isachardot}\ sorted\ l\ {\isasymand}\ distinct\ l{\isachardoublequoteclose}\ set\ set{\isacharunderscore}weight{\isacharunderscore}l\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}unfold{\isacharunderscore}locales{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}\ set{\isacharunderscore}weight{\isacharunderscore}l{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Implementation by natural numbers%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}n\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}set{\isacharunderscore}weight{\isacharunderscore}n\ w\ n\ {\isacharequal}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ w\ {\isacharparenleft}nat{\isadigit{2}}list\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}n{\isacharcolon}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set{\isacharunderscore}weight{\isacharunderscore}n\ w\ A\ {\isacharequal}\ w\ {\isasymrhd}\isactrlsub s\ set\ {\isacharparenleft}nat{\isadigit{2}}list\ A{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}n{\isacharunderscore}def\ set{\isacharunderscore}weight{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}subst\ sum{\isacharunderscore}list{\isacharunderscore}distinct{\isacharunderscore}conv{\isacharunderscore}sum{\isacharunderscore}set{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ distinct{\isacharunderscore}nat{\isadigit{2}}list{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{global{\isacharunderscore}interpretation}\isamarkupfalse%
\ SetWeightsSharesImpl{\isacharunderscore}nats{\isacharcolon}\ SetWeightsSharesImpl\ {\isachardoublequoteopen}{\isasymlambda}\ {\isacharunderscore}{\isachardot}\ True{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isachardoublequoteclose}\ set{\isacharunderscore}weight{\isacharunderscore}n\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}unfold{\isacharunderscore}locales{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}\ set{\isacharunderscore}weight{\isacharunderscore}n{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsection{Weight functions implemented by mappings%
}
\isamarkuptrue%
\isacommand{locale}\isamarkupfalse%
\ SetWeightsSharesMapImpl\ {\isacharequal}\ SetWeightsSharesImpl\ inv\ to{\isacharunderscore}set\ set{\isacharunderscore}weight\ \isakeyword{for}\ \isanewline
\ \ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{and}\ to{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequoteclose}\ \isakeyword{and}\ set{\isacharunderscore}weight\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ {\isacharplus}\ \isanewline
\ \ \isanewline
\ \ \isakeyword{fixes}\ set{\isacharunderscore}weight{\isacharunderscore}map\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ nat{\isacharparenright}\ mapping\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharcolon}\ \isanewline
\ \ {\isachardoublequoteopen}{\isasymlbrakk}inv\ A{\isacharsemicolon}\ {\isasymforall}\ x\ {\isasymin}\ to{\isacharunderscore}set\ A{\isachardot}\ Mapping{\isachardot}lookup\ wm\ x\ {\isacharequal}\ Some\ {\isacharparenleft}w\ x{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \isanewline
\ \ \ \ \ \ set{\isacharunderscore}weight{\isacharunderscore}map\ wm\ A\ {\isacharequal}\ set{\isacharunderscore}weight\ w\ A{\isachardoublequoteclose}\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{abbreviation}\isamarkupfalse%
\ set{\isacharunderscore}share{\isacharunderscore}map\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}s\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ nat{\isacharparenright}\ mapping\ {\isasymRightarrow}\ {\isacharprime}s\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ {\isachardoublequoteopen}set{\isacharunderscore}share{\isacharunderscore}map\ A\ w\ X\ {\isasymequiv}\ {\isadigit{2}}\ {\isacharasterisk}\ int{\isacharparenleft}set{\isacharunderscore}weight{\isacharunderscore}map\ w\ A{\isacharparenright}\ {\isacharminus}\ int\ {\isacharparenleft}set{\isacharunderscore}weight{\isacharunderscore}map\ w\ X{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
%
\isamarkupsubsubsection{Representation of sets by lists%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}l\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ nat{\isacharparenright}\ mapping\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}l\ w\ S\ {\isacharequal}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}the\ {\isasymcirc}\ {\isacharparenleft}Mapping{\isachardot}lookup\ w{\isacharparenright}{\isacharparenright}\ S{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}l{\isacharcolon}\ \isanewline
\ \ {\isachardoublequoteopen}{\isasymlbrakk}distinct\ A{\isacharsemicolon}\ {\isasymforall}\ x\ {\isasymin}\ set\ A{\isachardot}\ Mapping{\isachardot}lookup\ wm\ x\ {\isacharequal}\ Some\ {\isacharparenleft}w\ x{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \isanewline
\ \ \ \ \ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}l\ wm\ A\ {\isacharequal}\ set{\isacharunderscore}weight{\isacharunderscore}l\ w\ A{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}l{\isacharunderscore}def\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}l{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ sum{\isacharunderscore}list{\isacharunderscore}distinct{\isacharunderscore}conv{\isacharunderscore}sum{\isacharunderscore}set{\isacharbrackleft}of\ A\ w{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ sum{\isacharunderscore}list{\isacharunderscore}distinct{\isacharunderscore}conv{\isacharunderscore}sum{\isacharunderscore}set{\isacharbrackleft}of\ A\ {\isachardoublequoteopen}the\ {\isasymcirc}\ {\isacharparenleft}Mapping{\isachardot}lookup\ wm{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{global{\isacharunderscore}interpretation}\isamarkupfalse%
\ SetWeightsSharesMapImpl{\isacharunderscore}lists{\isacharcolon}\isanewline
\ \ SetWeightsSharesMapImpl\ {\isachardoublequoteopen}{\isasymlambda}\ {\isacharparenleft}l{\isacharcolon}{\isacharcolon}nat\ list{\isacharparenright}{\isachardot}\ sorted\ l\ {\isasymand}\ distinct\ l{\isachardoublequoteclose}\ List{\isachardot}set\ set{\isacharunderscore}weight{\isacharunderscore}l\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}l\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}unfold{\isacharunderscore}locales{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ A\ \isakeyword{and}\ wm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}linorder{\isacharcomma}\ nat{\isacharparenright}\ mapping{\isachardoublequoteclose}\ \isakeyword{and}\ w\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}sorted\ A\ {\isasymand}\ distinct\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}x{\isasymin}set\ A{\isachardot}\ Mapping{\isachardot}lookup\ wm\ x\ {\isacharequal}\ Some\ {\isacharparenleft}w\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}l\ wm\ A\ {\isacharequal}\ set{\isacharunderscore}weight{\isacharunderscore}l\ w\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}l{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isamarkupsubsubsection{Representation of sets by natural numbers%
}
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}n\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ Mapping{\isachardot}mapping\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}n\ w\ n\ {\isacharequal}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}the\ {\isasymcirc}\ {\isacharparenleft}Mapping{\isachardot}lookup\ w{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}nat{\isadigit{2}}list\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{global{\isacharunderscore}interpretation}\isamarkupfalse%
\ SetWeightsSharesCachedImpl{\isacharunderscore}nats{\isacharcolon}\isanewline
\ \ SetWeightsSharesMapImpl\ {\isachardoublequoteopen}{\isasymlambda}\ {\isacharunderscore}{\isachardot}\ True{\isachardoublequoteclose}\ {\isachardoublequoteopen}List{\isachardot}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isachardoublequoteclose}\ set{\isacharunderscore}weight{\isacharunderscore}n\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}n\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ A\ wm\ \isakeyword{and}\ w\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}x{\isasymin}{\isacharparenleft}set\ {\isasymcirc}\ nat{\isadigit{2}}list{\isacharparenright}\ A{\isachardot}\ Mapping{\isachardot}lookup\ wm\ x\ {\isacharequal}\ Some\ {\isacharparenleft}w\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}n\ wm\ A\ {\isacharequal}\ set{\isacharunderscore}weight{\isacharunderscore}n\ w\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}weight{\isacharunderscore}n{\isacharunderscore}def\ set{\isacharunderscore}weight{\isacharunderscore}map{\isacharunderscore}n{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}nat{\isadigit{2}}list{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ sum{\isacharunderscore}list{\isacharunderscore}distinct{\isacharunderscore}conv{\isacharunderscore}sum{\isacharunderscore}set{\isacharparenright}\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:
