
paulson@10602: %
paulson@11187: \begin{isabellebody}%
paulson@11187: \def\isabellecontext{Numbers}%
wenzelm@17056: %
wenzelm@17056: \isadelimtheory
wenzelm@17056: %
wenzelm@17056: \endisadelimtheory
wenzelm@17056: %
wenzelm@17056: \isatagtheory
wenzelm@17175: \isacommand{theory}\isamarkupfalse%
haftmann@27376: \ Numbers\isanewline
haftmann@27376: \isakeyword{imports}\ Complex{\isacharunderscore}Main\isanewline
haftmann@27376: \isakeyword{begin}%
wenzelm@17056: \endisatagtheory
wenzelm@17056: {\isafoldtheory}%
wenzelm@17056: %
wenzelm@17056: \isadelimtheory
paulson@10602: \isanewline
wenzelm@17056: %
wenzelm@17056: \endisadelimtheory
wenzelm@17056: %
wenzelm@17056: \isadelimML
wenzelm@17056: \isanewline
wenzelm@17056: %
wenzelm@17056: \endisadelimML
wenzelm@17056: %
wenzelm@17056: \isatagML
wenzelm@17175: \isacommand{ML}\isamarkupfalse%
wenzelm@36754: \ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
wenzelm@17175: \isacommand{ML}\isamarkupfalse%
wenzelm@37216: \ {\isachardoublequoteopen}Thy{\isacharunderscore}Output{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
wenzelm@17056: \endisatagML
wenzelm@17056: {\isafoldML}%
wenzelm@17056: %
wenzelm@17056: \isadelimML
wenzelm@17056: %
wenzelm@17056: \endisadelimML
wenzelm@11866: %
paulson@11187: \begin{isamarkuptext}%
paulson@10602: numeric literals; default simprules; can re-orient%
paulson@11187: \end{isamarkuptext}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17175: \isacommand{lemma}\isamarkupfalse%
wenzelm@17175: \ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m{\isachardoublequoteclose}%
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@17056: %
wenzelm@17056: \isatagproof
wenzelm@16353: %
wenzelm@16353: \begin{isamarkuptxt}%
wenzelm@16353: \begin{isabelle}%
wenzelm@16353: \ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m%
wenzelm@16353: \end{isabelle}%
wenzelm@16353: \end{isamarkuptxt}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17175: \isacommand{oops}\isamarkupfalse%
wenzelm@17175: %
wenzelm@17056: \endisatagproof
wenzelm@17056: {\isafoldproof}%
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@17056: \isanewline
paulson@15481: \isanewline
wenzelm@17175: \isacommand{consts}\isamarkupfalse%
wenzelm@17175: \ h\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
wenzelm@17175: \isacommand{recdef}\isamarkupfalse%
wenzelm@17175: \ h\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
wenzelm@17175: {\isachardoublequoteopen}h\ i\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isacharequal}\ {\isadigit{3}}\ then\ {\isadigit{2}}\ else\ i{\isacharparenright}{\isachardoublequoteclose}%
paulson@11187: \begin{isamarkuptext}%
wenzelm@11708: \isa{h\ {\isadigit{3}}\ {\isacharequal}\ {\isadigit{2}}}
paulson@11187: \isa{h\ i\ {\isacharequal}\ i}%
paulson@11187: \end{isamarkuptext}%
wenzelm@11866: \isamarkuptrue%
paulson@10878: %
paulson@11187: \begin{isamarkuptext}%
paulson@11187: \begin{isabelle}%
paulson@14387: Numeral{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}%
paulson@11187: \end{isabelle}
paulson@11174: \rulename{numeral_0_eq_0}
paulson@11187: 
paulson@11187: \begin{isabelle}%
paulson@14387: Numeral{\isadigit{1}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{numeral_1_eq_1}
paulson@10602: 
paulson@11187: \begin{isabelle}%
wenzelm@11708: {\isadigit{2}}\ {\isacharplus}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{add_2_eq_Suc}
paulson@10602: 
paulson@11187: \begin{isabelle}%
wenzelm@11708: n\ {\isacharplus}\ {\isadigit{2}}\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{add_2_eq_Suc'}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@14270: a\ {\isacharplus}\ b\ {\isacharplus}\ c\ {\isacharequal}\ a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{add_assoc}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@14270: a\ {\isacharplus}\ b\ {\isacharequal}\ b\ {\isacharplus}\ a%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{add_commute}
paulson@10602: 
paulson@11187: \begin{isabelle}%
nipkow@35103: b\ {\isacharplus}\ {\isacharparenleft}a\ {\isacharplus}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}%
paulson@10602: \end{isabelle}
paulson@11174: \rulename{add_left_commute}
paulson@10602: 
paulson@10602: these form add_ac; similarly there is mult_ac%
paulson@11187: \end{isamarkuptext}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17175: \isacommand{lemma}\isamarkupfalse%
wenzelm@17175: \ {\isachardoublequoteopen}Suc{\isacharparenleft}i\ {\isacharplus}\ j{\isacharasterisk}l{\isacharasterisk}k\ {\isacharplus}\ m{\isacharasterisk}n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n{\isacharasterisk}m\ {\isacharplus}\ i\ {\isacharplus}\ k{\isacharasterisk}j{\isacharasterisk}l{\isacharparenright}{\isachardoublequoteclose}%
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@17056: %
wenzelm@17056: \isatagproof
wenzelm@16353: %
wenzelm@16353: \begin{isamarkuptxt}%
wenzelm@16353: \begin{isabelle}%
wenzelm@16353: \ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ j\ {\isacharasterisk}\ l\ {\isacharasterisk}\ k\ {\isacharplus}\ m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n\ {\isacharasterisk}\ m\ {\isacharplus}\ i\ {\isacharplus}\ k\ {\isacharasterisk}\ j\ {\isacharasterisk}\ l{\isacharparenright}%
wenzelm@16353: \end{isabelle}%
wenzelm@16353: \end{isamarkuptxt}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17175: \isacommand{apply}\isamarkupfalse%
wenzelm@17175: \ {\isacharparenleft}simp\ add{\isacharcolon}\ add{\isacharunderscore}ac\ mult{\isacharunderscore}ac{\isacharparenright}%
wenzelm@16353: \begin{isamarkuptxt}%
wenzelm@16353: \begin{isabelle}%
wenzelm@16353: \ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
wenzelm@16353: \isaindent{\ {\isadigit{1}}{\isachardot}\ }f\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}%
wenzelm@16353: \end{isabelle}%
wenzelm@16353: \end{isamarkuptxt}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17175: \isacommand{oops}\isamarkupfalse%
wenzelm@17175: %
wenzelm@17056: \endisatagproof
wenzelm@17056: {\isafoldproof}%
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@11866: %
paulson@11187: \begin{isamarkuptext}%
paulson@11187: \begin{isabelle}%
paulson@11187: m\ {\isasymle}\ n\ {\isasymLongrightarrow}\ m\ div\ k\ {\isasymle}\ n\ div\ k%
paulson@11174: \end{isabelle}
paulson@11187: \rulename{div_le_mono}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11187: {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ {\isacharminus}\ n\ {\isacharasterisk}\ k%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{diff_mult_distrib}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11187: m\ mod\ n\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ mod\ {\isacharparenleft}n\ {\isacharasterisk}\ k{\isacharparenright}%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{mod_mult_distrib}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11187: P\ {\isacharparenleft}a\ {\isacharminus}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}a\ {\isacharless}\ b\ {\isasymlongrightarrow}\ P\ {\isadigit{0}}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}d{\isachardot}\ a\ {\isacharequal}\ b\ {\isacharplus}\ d\ {\isasymlongrightarrow}\ P\ d{\isacharparenright}{\isacharparenright}%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{nat_diff_split}%
paulson@11187: \end{isamarkuptext}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17175: \isacommand{lemma}\isamarkupfalse%
wenzelm@17175: \ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@17056: %
wenzelm@17056: \isatagproof
wenzelm@17175: \isacommand{apply}\isamarkupfalse%
wenzelm@17175: \ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split\ iff\ del{\isacharcolon}\ less{\isacharunderscore}Suc{\isadigit{0}}{\isacharparenright}\isanewline
wenzelm@16353: \ %
wenzelm@16353: \isamarkupcmt{\begin{isabelle}%
wenzelm@16353: \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ Suc\ {\isadigit{0}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ Suc\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%
wenzelm@16353: \end{isabelle}%
wenzelm@16353: }
wenzelm@16353: \isanewline
wenzelm@17175: \isacommand{apply}\isamarkupfalse%
wenzelm@17175: \ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{0}}{\isachardoublequoteclose}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline
wenzelm@17175: \isacommand{done}\isamarkupfalse%
wenzelm@17175: %
wenzelm@17056: \endisatagproof
wenzelm@17056: {\isafoldproof}%
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: \isanewline
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
paulson@12156: \isanewline
paulson@12156: \isanewline
wenzelm@17175: \isacommand{lemma}\isamarkupfalse%
wenzelm@17175: \ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@17056: %
wenzelm@17056: \isatagproof
wenzelm@17175: \isacommand{apply}\isamarkupfalse%
wenzelm@17175: \ {\isacharparenleft}simp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharcomma}\ clarify{\isacharparenright}\isanewline
wenzelm@16353: \ %
wenzelm@16353: \isamarkupcmt{\begin{isabelle}%
wenzelm@16353: \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ {\isadigit{4}}\ {\isacharplus}\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%
wenzelm@16353: \end{isabelle}%
wenzelm@16353: }
wenzelm@16353: \isanewline
wenzelm@17175: \isacommand{apply}\isamarkupfalse%
wenzelm@17175: \ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{0}}\ {\isacharbar}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequoteclose}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline
wenzelm@17175: \isacommand{done}\isamarkupfalse%
wenzelm@17175: %
wenzelm@17056: \endisatagproof
wenzelm@17056: {\isafoldproof}%
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@11866: %
paulson@11187: \begin{isamarkuptext}%
paulson@11187: \begin{isabelle}%
paulson@11187: m\ mod\ n\ {\isacharequal}\ {\isacharparenleft}if\ m\ {\isacharless}\ n\ then\ m\ else\ {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ mod\ n{\isacharparenright}%
paulson@11187: \end{isabelle}
paulson@11187: \rulename{mod_if}
paulson@10602: 
paulson@11187: \begin{isabelle}%
haftmann@27658: a\ div\ b\ {\isacharasterisk}\ b\ {\isacharplus}\ a\ mod\ b\ {\isacharequal}\ a%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{mod_div_equality}
paulson@10602: 
paulson@11187: 
paulson@11187: \begin{isabelle}%
paulson@11187: a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{div_mult1_eq}
paulson@11187: 
paulson@11187: \begin{isabelle}%
paulson@11187: a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c%
paulson@10602: \end{isabelle}
nipkow@30208: \rulename{mod_mult_right_eq}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11187: a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{div_mult2_eq}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11187: a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b%
paulson@11187: \end{isabelle}
paulson@11187: \rulename{mod_mult2_eq}
paulson@10602: 
paulson@11187: \begin{isabelle}%
haftmann@31678: c\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymLongrightarrow}\ c\ {\isacharasterisk}\ a\ div\ {\isacharparenleft}c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ a\ div\ b%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{div_mult_mult1}
paulson@10602: 
paulson@11187: \begin{isabelle}%
haftmann@27658: a\ div\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}%
paulson@10602: \end{isabelle}
haftmann@27658: \rulename{div_by_0}
paulson@10602: 
paulson@11187: \begin{isabelle}%
haftmann@27658: a\ mod\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ a%
paulson@10602: \end{isabelle}
haftmann@27658: \rulename{mod_by_0}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11187: {\isasymlbrakk}m\ dvd\ n{\isacharsemicolon}\ n\ dvd\ m{\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n%
paulson@10602: \end{isabelle}
nipkow@33750: \rulename{dvd_antisym}
paulson@10602: 
paulson@11187: \begin{isabelle}%
haftmann@27658: {\isasymlbrakk}a\ dvd\ b{\isacharsemicolon}\ a\ dvd\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ a\ dvd\ b\ {\isacharplus}\ c%
paulson@10602: \end{isabelle}
paulson@11174: \rulename{dvd_add}
paulson@10602: 
paulson@10602: For the integers, I'd list a few theorems that somehow involve negative 
paulson@13758: numbers.%
paulson@13758: \end{isamarkuptext}%
paulson@13758: \isamarkuptrue%
paulson@13758: %
paulson@13758: \begin{isamarkuptext}%
paulson@10602: Division, remainder of negatives
paulson@10602: 
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11870: {\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isasymle}\ a\ mod\ b%
paulson@11187: \end{isabelle}
paulson@11174: \rulename{pos_mod_sign}
paulson@11187: 
paulson@11187: \begin{isabelle}%
paulson@11870: {\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isacharless}\ b%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{pos_mod_bound}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11870: b\ {\isacharless}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isasymle}\ {\isadigit{0}}%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{neg_mod_sign}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11870: b\ {\isacharless}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ b\ {\isacharless}\ a\ mod\ b%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{neg_mod_bound}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11187: {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ div\ c\ {\isacharequal}\ a\ div\ c\ {\isacharplus}\ b\ div\ c\ {\isacharplus}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ div\ c%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{zdiv_zadd1_eq}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11187: {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ mod\ c\ {\isacharequal}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ mod\ c%
paulson@10602: \end{isabelle}
nipkow@30208: \rulename{mod_add_eq}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11187: a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{zdiv_zmult1_eq}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11187: a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{zmod_zmult1_eq}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11870: {\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c%
paulson@10602: \end{isabelle}
paulson@11187: \rulename{zdiv_zmult2_eq}
paulson@10602: 
paulson@11187: \begin{isabelle}%
paulson@11870: {\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b%
paulson@10602: \end{isabelle}
paulson@14400: \rulename{zmod_zmult2_eq}%
paulson@11187: \end{isamarkuptext}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17175: \isacommand{lemma}\isamarkupfalse%
wenzelm@17175: \ {\isachardoublequoteopen}abs\ {\isacharparenleft}x{\isacharplus}y{\isacharparenright}\ {\isasymle}\ abs\ x\ {\isacharplus}\ abs\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@17056: %
wenzelm@17056: \isatagproof
wenzelm@17175: \isacommand{by}\isamarkupfalse%
wenzelm@17175: \ arith%
wenzelm@17056: \endisatagproof
wenzelm@17056: {\isafoldproof}%
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: \isanewline
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
paulson@15481: \isanewline
wenzelm@17175: \isacommand{lemma}\isamarkupfalse%
wenzelm@17175: \ {\isachardoublequoteopen}abs\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}x{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ abs\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@17056: %
wenzelm@17056: \isatagproof
wenzelm@17175: \isacommand{by}\isamarkupfalse%
wenzelm@17175: \ {\isacharparenleft}simp\ add{\isacharcolon}\ abs{\isacharunderscore}if{\isacharparenright}%
wenzelm@17056: \endisatagproof
wenzelm@17056: {\isafoldproof}%
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@11866: %
paulson@11187: \begin{isamarkuptext}%
paulson@13758: Induction rules for the Integers
paulson@13758: 
paulson@13758: \begin{isabelle}%
paulson@13758: {\isasymlbrakk}k\ {\isasymle}\ i{\isacharsemicolon}\ P\ k{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}k\ {\isasymle}\ i{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i%
paulson@13758: \end{isabelle}
paulson@13758: \rulename{int_ge_induct}
paulson@13758: 
paulson@13758: \begin{isabelle}%
paulson@13758: {\isasymlbrakk}k\ {\isacharless}\ i{\isacharsemicolon}\ P\ {\isacharparenleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}k\ {\isacharless}\ i{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i%
paulson@13758: \end{isabelle}
paulson@13758: \rulename{int_gr_induct}
paulson@13758: 
paulson@13758: \begin{isabelle}%
paulson@13758: {\isasymlbrakk}i\ {\isasymle}\ k{\isacharsemicolon}\ P\ k{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}i\ {\isasymle}\ k{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i%
paulson@13758: \end{isabelle}
paulson@13758: \rulename{int_le_induct}
paulson@13758: 
paulson@13758: \begin{isabelle}%
paulson@13758: {\isasymlbrakk}i\ {\isacharless}\ k{\isacharsemicolon}\ P\ {\isacharparenleft}k\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}i\ {\isacharless}\ k{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i%
paulson@13758: \end{isabelle}
paulson@13758: \rulename{int_less_induct}%
paulson@13758: \end{isamarkuptext}%
paulson@13758: \isamarkuptrue%
paulson@13758: %
paulson@13758: \begin{isamarkuptext}%
paulson@14400: FIELDS
wenzelm@10776: 
paulson@11187: \begin{isabelle}%
wenzelm@25056: x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ {\isasymexists}z{\isachargreater}x{\isachardot}\ z\ {\isacharless}\ y%
wenzelm@10776: \end{isabelle}
paulson@14295: \rulename{dense}
paulson@11174: 
paulson@11187: \begin{isabelle}%
paulson@14288: a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c%
paulson@11174: \end{isabelle}
paulson@14288: \rulename{times_divide_eq_right}
wenzelm@10776: 
paulson@11187: \begin{isabelle}%
paulson@14288: b\ {\isacharslash}\ c\ {\isacharasterisk}\ a\ {\isacharequal}\ b\ {\isacharasterisk}\ a\ {\isacharslash}\ c%
wenzelm@10776: \end{isabelle}
paulson@14288: \rulename{times_divide_eq_left}
wenzelm@10776: 
paulson@11187: \begin{isabelle}%
paulson@14288: a\ {\isacharslash}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ c\ {\isacharslash}\ b%
wenzelm@10776: \end{isabelle}
paulson@14288: \rulename{divide_divide_eq_right}
wenzelm@10776: 
paulson@11187: \begin{isabelle}%
paulson@14288: a\ {\isacharslash}\ b\ {\isacharslash}\ c\ {\isacharequal}\ a\ {\isacharslash}\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}%
wenzelm@10776: \end{isabelle}
paulson@14288: \rulename{divide_divide_eq_left}
wenzelm@10776: 
paulson@11187: \begin{isabelle}%
paulson@14295: {\isacharminus}\ {\isacharparenleft}a\ {\isacharslash}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharminus}\ a\ {\isacharslash}\ b%
wenzelm@10776: \end{isabelle}
paulson@14295: \rulename{minus_divide_left}
wenzelm@10776: 
paulson@11187: \begin{isabelle}%
paulson@14295: {\isacharminus}\ {\isacharparenleft}a\ {\isacharslash}\ b{\isacharparenright}\ {\isacharequal}\ a\ {\isacharslash}\ {\isacharminus}\ b%
wenzelm@10776: \end{isabelle}
paulson@14295: \rulename{minus_divide_right}
wenzelm@10776: 
wenzelm@10776: This last NOT a simprule
wenzelm@10776: 
paulson@11187: \begin{isabelle}%
paulson@14295: {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharslash}\ c\ {\isacharequal}\ a\ {\isacharslash}\ c\ {\isacharplus}\ b\ {\isacharslash}\ c%
nipkow@10790: \end{isabelle}
paulson@14295: \rulename{add_divide_distrib}%
paulson@11187: \end{isamarkuptext}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17175: \isacommand{lemma}\isamarkupfalse%
wenzelm@17175: \ {\isachardoublequoteopen}{\isadigit{3}}{\isacharslash}{\isadigit{4}}\ {\isacharless}\ {\isacharparenleft}{\isadigit{7}}{\isacharslash}{\isadigit{8}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequoteclose}\isanewline
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@17056: %
wenzelm@17056: \isatagproof
wenzelm@17175: \isacommand{by}\isamarkupfalse%
wenzelm@17175: \ simp%
wenzelm@17056: \endisatagproof
wenzelm@17056: {\isafoldproof}%
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: \ \isanewline
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
paulson@11174: \isanewline
wenzelm@17175: \isacommand{lemma}\isamarkupfalse%
wenzelm@17175: \ {\isachardoublequoteopen}P\ {\isacharparenleft}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@17056: %
wenzelm@17056: \isatagproof
wenzelm@16353: %
wenzelm@16353: \begin{isamarkuptxt}%
wenzelm@16353: \begin{isabelle}%
wenzelm@16353: \ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isadigit{3}}\ {\isacharslash}\ {\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}\ {\isacharslash}\ {\isadigit{1}}{\isadigit{5}}{\isacharparenright}{\isacharparenright}%
wenzelm@16353: \end{isabelle}%
wenzelm@16353: \end{isamarkuptxt}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17175: \isacommand{apply}\isamarkupfalse%
wenzelm@17175: \ simp%
wenzelm@16353: \begin{isamarkuptxt}%
wenzelm@16353: \begin{isabelle}%
wenzelm@16353: \ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isadigit{2}}\ {\isacharslash}\ {\isadigit{5}}{\isacharparenright}%
wenzelm@16353: \end{isabelle}%
wenzelm@16353: \end{isamarkuptxt}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17175: \isacommand{oops}\isamarkupfalse%
wenzelm@17175: %
wenzelm@17056: \endisatagproof
wenzelm@17056: {\isafoldproof}%
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@17056: \isanewline
paulson@15481: \isanewline
wenzelm@17175: \isacommand{lemma}\isamarkupfalse%
wenzelm@17175: \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequoteclose}%
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
wenzelm@17056: %
wenzelm@17056: \isatagproof
wenzelm@16353: %
wenzelm@16353: \begin{isamarkuptxt}%
wenzelm@16353: \begin{isabelle}%
wenzelm@16353: \ {\isadigit{1}}{\isachardot}\ {\isadigit{3}}\ {\isacharslash}\ {\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}\ {\isacharslash}\ {\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ x%
wenzelm@16353: \end{isabelle}%
wenzelm@16353: \end{isamarkuptxt}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17175: \isacommand{apply}\isamarkupfalse%
wenzelm@17175: \ simp%
wenzelm@16353: \begin{isamarkuptxt}%
wenzelm@16353: \begin{isabelle}%
wenzelm@16353: \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharless}\ x\ {\isacharasterisk}\ {\isadigit{5}}%
wenzelm@16353: \end{isabelle}%
wenzelm@16353: \end{isamarkuptxt}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17175: \isacommand{oops}\isamarkupfalse%
wenzelm@17175: %
wenzelm@17056: \endisatagproof
wenzelm@17056: {\isafoldproof}%
wenzelm@17056: %
wenzelm@17056: \isadelimproof
wenzelm@17056: %
wenzelm@17056: \endisadelimproof
paulson@14400: %
paulson@14400: \begin{isamarkuptext}%
paulson@14400: Ring and Field
paulson@14400: 
paulson@14400: Requires a field, or else an ordered ring
paulson@14400: 
paulson@14400: \begin{isabelle}%
paulson@14400: {\isacharparenleft}a\ {\isacharasterisk}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}%
paulson@14400: \end{isabelle}
paulson@14400: \rulename{mult_eq_0_iff}
paulson@14400: 
paulson@14400: \begin{isabelle}%
paulson@14400: {\isacharparenleft}a\ {\isacharasterisk}\ c\ {\isacharequal}\ b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
paulson@14400: \end{isabelle}
paulson@14400: \rulename{mult_cancel_right}
paulson@14400: 
paulson@14400: \begin{isabelle}%
paulson@23504: {\isacharparenleft}c\ {\isacharasterisk}\ a\ {\isacharequal}\ c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
paulson@14400: \end{isabelle}
paulson@23504: \rulename{mult_cancel_left}%
paulson@14400: \end{isamarkuptext}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17056: %
paulson@14400: \begin{isamarkuptext}%
paulson@14400: effect of show sorts on the above
paulson@14400: 
paulson@14400: \begin{isabelle}%
wenzelm@32836: {\isacharparenleft}{\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharequal}\isanewline
wenzelm@32836: \isaindent{{\isacharparenleft}}c\ {\isacharasterisk}\ {\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
wenzelm@32836: {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
paulson@14400: \end{isabelle}
paulson@23504: \rulename{mult_cancel_left}%
paulson@14400: \end{isamarkuptext}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17056: %
paulson@14400: \begin{isamarkuptext}%
paulson@14400: absolute value
paulson@14400: 
paulson@14400: \begin{isabelle}%
paulson@14400: {\isasymbar}a\ {\isacharasterisk}\ b{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}b{\isasymbar}%
paulson@14400: \end{isabelle}
paulson@14400: \rulename{abs_mult}
paulson@14400: 
paulson@14400: \begin{isabelle}%
paulson@14400: {\isacharparenleft}{\isasymbar}a{\isasymbar}\ {\isasymle}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isasymle}\ b\ {\isasymand}\ {\isacharminus}\ a\ {\isasymle}\ b{\isacharparenright}%
paulson@14400: \end{isabelle}
paulson@14400: \rulename{abs_le_iff}
paulson@14400: 
paulson@14400: \begin{isabelle}%
paulson@14400: {\isasymbar}a\ {\isacharplus}\ b{\isasymbar}\ {\isasymle}\ {\isasymbar}a{\isasymbar}\ {\isacharplus}\ {\isasymbar}b{\isasymbar}%
paulson@14400: \end{isabelle}
paulson@14400: \rulename{abs_triangle_ineq}
paulson@14400: 
paulson@14400: \begin{isabelle}%
haftmann@31678: a\isactrlbsup m\ {\isacharplus}\ n\isactrlesup \ {\isacharequal}\ a\isactrlbsup m\isactrlesup \ {\isacharasterisk}\ a\isactrlbsup n\isactrlesup %
paulson@14400: \end{isabelle}
paulson@14400: \rulename{power_add}
paulson@14400: 
paulson@14400: \begin{isabelle}%
haftmann@31678: a\isactrlbsup m\ {\isacharasterisk}\ n\isactrlesup \ {\isacharequal}\ a\isactrlbsup m\isactrlesup \isactrlbsup n\isactrlesup %
paulson@14400: \end{isabelle}
paulson@14400: \rulename{power_mult}
paulson@14400: 
paulson@14400: \begin{isabelle}%
haftmann@31678: {\isasymbar}a\isactrlbsup n\isactrlesup {\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\isactrlbsup n\isactrlesup %
paulson@14400: \end{isabelle}
paulson@14400: \rulename{power_abs}%
paulson@14400: \end{isamarkuptext}%
wenzelm@17175: \isamarkuptrue%
wenzelm@17056: %
wenzelm@17056: \isadelimtheory
wenzelm@17056: %
wenzelm@17056: \endisadelimtheory
wenzelm@17056: %
wenzelm@17056: \isatagtheory
wenzelm@17175: \isacommand{end}\isamarkupfalse%
wenzelm@17175: %
wenzelm@17056: \endisatagtheory
wenzelm@17056: {\isafoldtheory}%
wenzelm@17056: %
wenzelm@17056: \isadelimtheory
wenzelm@17056: %
wenzelm@17056: \endisadelimtheory
wenzelm@17056: \isanewline
paulson@11187: \end{isabellebody}%
paulson@10602: %%% Local Variables:
paulson@10602: %%% mode: latex
paulson@10602: %%% TeX-master: "root"
paulson@10602: %%% End:




