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: