%
\begin{isabellebody}%
\setisabellecontext{MoreSet}%
%
\isamarkupsection{Auxiliary lemmas about (finite) sets%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ MoreSet\isanewline
\isakeyword{imports}\ Main\ MoreList\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ finiteUn{\isacharunderscore}iff{\isacharcolon}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}\ {\isasymlongleftrightarrow}\ finite\ F\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ S\ {\isasymin}\ F{\isachardot}\ finite\ S{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}auto\ dest{\isacharcolon}\ finite{\isacharunderscore}UnionD{\isacharparenright}\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ S\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}S\ {\isasymin}\ F{\isachardoublequoteclose}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}S\ {\isasymsubseteq}\ {\isasymUnion}\ F{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}finite\ S{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ card{\isacharunderscore}{\isadigit{1}}{\isacharunderscore}iff{\isacharunderscore}singleton{\isacharcolon}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ {\isadigit{1}}\ {\isasymlongleftrightarrow}\ {\isacharparenleft}{\isasymexists}\ a{\isachardot}\ A\ {\isacharequal}\ {\isacharbraceleft}a{\isacharbraceright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ a\ \isakeyword{where}\ {\isachardoublequoteopen}a\ {\isasymin}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isacharequal}\ {\isacharbraceleft}a{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}Diff{\isacharunderscore}singleton{\isacharbrackleft}of\ A\ a{\isacharbrackright}\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ {\isadigit{1}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}eq{\isacharbrackleft}of\ {\isachardoublequoteopen}A\ {\isacharminus}\ {\isacharbraceleft}a{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ card{\isacharunderscore}ge{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}finite{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymexists}\ a{\isachardot}\ A\ {\isacharequal}\ {\isacharbraceleft}a{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ card{\isacharunderscore}{\isadigit{2}}{\isacharunderscore}iff{\isacharunderscore}dubleton{\isacharcolon}\ \isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ {\isadigit{2}}\ {\isasymlongleftrightarrow}\ {\isacharparenleft}{\isasymexists}\ a\ b{\isachardot}\ A\ {\isacharequal}\ {\isacharbraceleft}a{\isacharcomma}\ b{\isacharbraceright}\ {\isasymand}\ a\ {\isasymnoteq}\ b{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isasymnoteq}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ a\ \isakeyword{where}\ {\isachardoublequoteopen}a\ {\isasymin}\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}card\ {\isacharparenleft}A\ {\isacharminus}\ {\isacharbraceleft}a{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}card\ A\ {\isacharequal}\ {\isadigit{2}}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}Diff{\isacharunderscore}singleton{\isacharbrackleft}of\ A\ a{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ card{\isacharunderscore}ge{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}finite{\isacharparenright}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ b\ \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isacharminus}\ {\isacharbraceleft}a{\isacharbraceright}\ {\isacharequal}\ {\isacharbraceleft}b{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}{\isadigit{1}}{\isacharunderscore}iff{\isacharunderscore}singleton{\isacharbrackleft}of\ {\isachardoublequoteopen}A\ {\isacharminus}\ {\isacharbraceleft}a{\isacharbraceright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}a\ {\isasymnoteq}\ b{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}A\ {\isacharequal}\ {\isacharbraceleft}a{\isacharcomma}\ b{\isacharbraceright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}a\ {\isasymin}\ A{\isacharbackquoteclose}\ {\isacharbackquoteopen}A\ {\isacharminus}\ {\isacharbraceleft}a{\isacharbraceright}\ {\isacharequal}\ {\isacharbraceleft}b{\isacharbraceright}{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymexists}\ a\ b{\isachardot}\ A\ {\isacharequal}\ {\isacharbraceleft}a{\isacharcomma}\ b{\isacharbraceright}\ {\isasymand}\ a\ {\isasymnoteq}\ b{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ subset{\isacharunderscore}eq{\isacharunderscore}card{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ \ {\isachardoublequoteopen}finite\ F{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}card\ F\ {\isasymge}\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ F{\isacharprime}{\isachardot}\ F{\isacharprime}\ {\isasymsubseteq}\ F\ {\isasymand}\ card\ F{\isacharprime}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ F\ rule{\isacharcolon}\ finite{\isacharunderscore}induct{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ empty\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}insert\ a\ F{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}n\ {\isasymle}\ card\ F{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ True\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ insert{\isacharparenleft}{\isadigit{3}}{\isacharparenright}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{case}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
\ {\isachardoublequoteopen}n\ {\isacharequal}\ card\ {\isacharparenleft}insert\ a\ F{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{using}\isamarkupfalse%
\ insert\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ card{\isacharunderscore}le{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}m\ {\isasymle}\ n{\isachardoublequoteclose}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ B{\isachardot}\ B\ {\isasymsubseteq}\ A\ {\isasymand}\ card\ B\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}eq{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}iff{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ subset{\isacharunderscore}eq{\isacharunderscore}card{\isacharbrackleft}of\ A\ m{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}cases\ {\isachardoublequoteopen}n\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}{\isacharparenright}\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\ \ \isanewline
\isacommand{lemma}\isamarkupfalse%
\ card{\isacharunderscore}Suc{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ A{\isacharprime}\ a{\isachardot}\ A\ {\isacharequal}\ A{\isacharprime}\ {\isasymunion}\ {\isacharbraceleft}a{\isacharbraceright}\ {\isasymand}\ a\ {\isasymnotin}\ A{\isacharprime}\ {\isasymand}\ card\ A{\isacharprime}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}metis\ card{\isacharunderscore}eq{\isacharunderscore}SucD{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ card{\isacharunderscore}Suc{\isacharprime}{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ k\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\ {\isachardoublequoteopen}a\ {\isasymin}\ A{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}card\ {\isacharparenleft}A\ {\isacharminus}\ {\isacharbraceleft}a{\isacharbraceright}{\isacharparenright}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ card{\isachardot}insert{\isacharbrackleft}of\ {\isachardoublequoteopen}A\ {\isacharminus}\ {\isacharbraceleft}a{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}a{\isachardoublequoteclose}{\isacharbrackright}\ card{\isacharunderscore}eq{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}iff{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ subset{\isacharunderscore}card{\isacharunderscore}eq{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymsubseteq}\ B{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ card\ B{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ B{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}A\ {\isacharequal}\ B{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ h\ \isakeyword{where}\ {\isachardoublequoteopen}bij{\isacharunderscore}betw\ h\ B\ A{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}same{\isacharunderscore}card{\isacharunderscore}bij{\isacharbrackleft}of\ B\ A{\isacharbrackright}\ assms\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ finite{\isacharunderscore}subset{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ bij{\isacharunderscore}betw{\isacharunderscore}def\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ endo{\isacharunderscore}inj{\isacharunderscore}surj{\isacharbrackleft}of\ B\ h{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymsubseteq}\ B{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ B{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ card{\isacharunderscore}n{\isacharunderscore}n{\isacharunderscore}aux{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymnoteq}\ B{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ card\ B{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}finite\ B{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}card\ {\isacharparenleft}A\ {\isasymunion}\ B{\isacharparenright}\ {\isasymnoteq}\ card\ A{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ subset{\isacharunderscore}card{\isacharunderscore}eq{\isacharbrackleft}of\ A\ {\isachardoublequoteopen}A\ {\isasymunion}\ B{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ subset{\isacharunderscore}card{\isacharunderscore}eq{\isacharbrackleft}of\ B\ A{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ card{\isacharunderscore}n{\isacharunderscore}n{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}card\ A\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}card\ B\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}n\ {\isachargreater}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}A\ {\isasymnoteq}\ B{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}n\ {\isacharless}\ card\ {\isacharparenleft}A\ {\isasymunion}\ B{\isacharparenright}\ {\isasymand}\ card\ {\isacharparenleft}A\ {\isasymunion}\ B{\isacharparenright}\ {\isasymle}\ {\isadigit{2}}{\isacharasterisk}n{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}mono{\isacharbrackleft}of\ A\ {\isachardoublequoteopen}A\ {\isasyminter}\ B{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}Un{\isacharunderscore}Int{\isacharbrackleft}of\ A\ B{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}gt{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}iff{\isacharbrackleft}of\ A{\isacharbrackright}\ \ card{\isacharunderscore}gt{\isacharunderscore}{\isadigit{0}}{\isacharunderscore}iff{\isacharbrackleft}of\ B{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ card{\isacharunderscore}n{\isacharunderscore}n{\isacharunderscore}aux{\isacharbrackleft}of\ A\ B{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
This should hold for every infinite type --- for our
applications, it suffices to consider only \isa{nat}.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ finite{\isacharunderscore}disjoint{\isacharunderscore}set{\isacharcolon}\isanewline
\ \ \isakeyword{fixes}\ X\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ Y{\isachardot}\ finite\ Y\ {\isasymand}\ card\ Y\ {\isacharequal}\ d\ {\isasymand}\ X\ {\isasyminter}\ Y\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharparenleft}induct\ d{\isacharparenright}\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isadigit{0}}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ force\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{case}\isamarkupfalse%
\ {\isacharparenleft}Suc\ d{\isacharparenright}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
\ Y\ \isakeyword{where}\ {\isachardoublequoteopen}card\ Y\ {\isacharequal}\ d{\isachardoublequoteclose}\ {\isachardoublequoteopen}X\ {\isasyminter}\ Y\ {\isacharequal}\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ Y{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{obtain}\isamarkupfalse%
\ a\ \isakeyword{where}\ {\isachardoublequoteopen}a\ {\isasymnotin}\ X\ {\isasymunion}\ Y{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ finite{\isacharunderscore}nat{\isacharunderscore}set{\isacharunderscore}iff{\isacharunderscore}bounded{\isacharbrackleft}of\ {\isachardoublequoteopen}X\ {\isasymunion}\ Y{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ {\isacharbackquoteopen}finite\ X{\isacharbackquoteclose}\ {\isacharbackquoteopen}finite\ Y{\isacharbackquoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isacharquery}case\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}Y\ {\isasymunion}\ {\isacharbraceleft}a{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ map{\isacharunderscore}fam{\isacharunderscore}cong{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}{\isasymforall}\ x\ {\isasymin}\ {\isacharparenleft}{\isasymUnion}\ F{\isacharparenright}{\isachardot}\ g{\isacharprime}\ x\ {\isacharequal}\ g\ x{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}op\ {\isacharbackquote}\ g\ {\isacharbackquote}\ F\ {\isacharequal}\ op\ {\isacharbackquote}\ g{\isacharprime}\ {\isacharbackquote}\ F{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{by}\isamarkupfalse%
\ auto\ {\isacharparenleft}metis\ {\isacharparenleft}lifting{\isacharparenright}\ image{\isacharunderscore}cong\ image{\isacharunderscore}iff{\isacharparenright}{\isacharplus}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Remove n-th element of an ordered set%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a{\isacharcolon}{\isacharcolon}linorder\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}set{\isacharunderscore}drop{\isacharunderscore}nth\ n\ s\ {\isacharequal}\ set\ {\isacharparenleft}drop{\isacharunderscore}nth\ n\ {\isacharparenleft}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ s{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}subset{\isacharcolon}\ \isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ X{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}set{\isacharunderscore}drop{\isacharunderscore}nth\ s\ X\ {\isasymsubseteq}\ X{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}def\ drop{\isacharunderscore}nth{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharbrackleft}of\ X{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}auto\ dest{\isacharcolon}\ in{\isacharunderscore}set{\isacharunderscore}takeD\ in{\isacharunderscore}set{\isacharunderscore}dropD{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ card{\isacharunderscore}set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}i\ {\isacharless}\ card\ S{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ S{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}card\ {\isacharparenleft}set{\isacharunderscore}drop{\isacharunderscore}nth\ i\ S{\isacharparenright}\ {\isacharequal}\ card\ S\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}card{\isacharbrackleft}of\ {\isachardoublequoteopen}drop{\isacharunderscore}nth\ i\ {\isacharparenleft}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ S{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}card{\isacharbrackleft}of\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ S{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}drop{\isacharunderscore}nth{\isacharbrackleft}of\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ S{\isachardoublequoteclose}\ i{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharbrackleft}of\ S{\isacharbrackright}\ length{\isacharunderscore}drop{\isacharunderscore}nth{\isacharbrackleft}of\ i\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ S{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}def\isanewline
\isacommand{by}\isamarkupfalse%
\ auto%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}drops{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}i\ {\isacharless}\ card\ S{\isachardoublequoteclose}\ {\isachardoublequoteopen}finite\ S{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}\ x\ {\isasymin}\ S{\isachardot}\ x\ {\isasymnotin}\ set{\isacharunderscore}drop{\isacharunderscore}nth\ i\ S{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}def\isanewline
\isacommand{using}\isamarkupfalse%
\ sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharbrackleft}of\ S{\isacharbrackright}\ length{\isacharunderscore}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharbrackleft}of\ S{\isacharbrackright}\ {\isacharbackquoteopen}finite\ S{\isacharbackquoteclose}\isanewline
\isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}distinct{\isacharbrackleft}of\ i\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ S{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{using}\isamarkupfalse%
\ in{\isacharunderscore}set{\isacharunderscore}conv{\isacharunderscore}nth{\isacharbrackleft}of\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ S\ {\isacharbang}\ i{\isachardoublequoteclose}\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ S{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}{\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ S\ {\isacharbang}\ i{\isachardoublequoteclose}\ \isakeyword{in}\ bexI{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ force%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}inj{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}finite\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}i\ {\isacharless}\ card\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}j\ {\isacharless}\ card\ A{\isachardoublequoteclose}\ {\isachardoublequoteopen}set{\isacharunderscore}drop{\isacharunderscore}nth\ i\ A\ {\isacharequal}\ set{\isacharunderscore}drop{\isacharunderscore}nth\ j\ A{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}i\ {\isacharequal}\ j{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{using}\isamarkupfalse%
\ assms\isanewline
\ \ \isacommand{unfolding}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}def\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}distinct{\isacharbrackleft}of\ {\isacharunderscore}\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ A{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ distinct{\isacharunderscore}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ nth{\isacharunderscore}eq{\isacharunderscore}iff{\isacharunderscore}index{\isacharunderscore}eq{\isacharbrackleft}of\ {\isachardoublequoteopen}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set\ A{\isachardoublequoteclose}{\isacharbrackright}\isanewline
\ \ \isacommand{using}\isamarkupfalse%
\ length{\isacharunderscore}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharbrackleft}of\ A{\isacharbrackright}\isanewline
\ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ insertE\ insert{\isacharunderscore}Diff\ nth{\isacharunderscore}mem\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}def\ set{\isacharunderscore}drop{\isacharunderscore}nth{\isacharunderscore}drops\ sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharparenright}%
\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:
