%
\begin{isabellebody}%
\setisabellecontext{MoreMap}%
%
\isamarkupsection{Auxiliary lemmas about mappings%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ MoreMap\isanewline
\isakeyword{imports}\ {\isachardoublequoteopen}HOL{\isacharminus}Library{\isachardot}Mapping{\isachardoublequoteclose}\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\ tabulate\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ mapping{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}tabulate\ l\ {\isacharequal}\ foldl\ {\isacharparenleft}{\isasymlambda}\ m\ a{\isachardot}\ Mapping{\isachardot}update\ {\isacharparenleft}fst\ a{\isacharparenright}\ {\isacharparenleft}snd\ a{\isacharparenright}\ m{\isacharparenright}\ Mapping{\isachardot}empty\ l{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ tabulate{\isacharunderscore}map{\isacharunderscore}of{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}distinct\ {\isacharparenleft}map\ fst\ l{\isacharparenright}\ {\isasymLongrightarrow}\ tabulate\ l\ {\isacharequal}\ Mapping{\isachardot}Mapping\ {\isacharparenleft}map{\isacharunderscore}of\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{unfolding}\isamarkupfalse%
\ tabulate{\isacharunderscore}def\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}induct\ l\ rule{\isacharcolon}\ rev{\isacharunderscore}induct{\isacharparenright}\isanewline
\isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Mapping{\isachardot}empty{\isacharunderscore}def\ Mapping{\isachardot}update{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}metis\ dom{\isacharunderscore}map{\isacharunderscore}of{\isacharunderscore}conv{\isacharunderscore}image{\isacharunderscore}fst\ empty{\isacharunderscore}map{\isacharunderscore}add\ lookup{\isachardot}abs{\isacharunderscore}eq\ lookup{\isachardot}rep{\isacharunderscore}eq\ map{\isacharunderscore}add{\isacharunderscore}upd{\isacharunderscore}left{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{find{\isacharunderscore}theorems}\isamarkupfalse%
\ Mapping{\isachardot}lookup\ Mapping{\isachardot}tabulate\isanewline
\isanewline
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ lookup{\isacharunderscore}tabulate\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}Mapping{\isachardot}lookup\ {\isacharparenleft}Mapping{\isachardot}tabulate\ ks\ f{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ o\ f{\isacharparenright}\ {\isacharbar}{\isacharbackquote}\ set\ ks{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ %
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ ks{\isacharparenright}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Mapping{\isachardot}tabulate{\isachardot}abs{\isacharunderscore}eq\ Mapping{\isachardot}lookup{\isachardot}abs{\isacharunderscore}eq\ restrict{\isacharunderscore}map{\isacharunderscore}def\ fun{\isacharunderscore}eq{\isacharunderscore}iff{\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:
