diff -r 0c86acc069ad -r 5deda0549f97 doc-src/TutorialI/document/Numbers.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/Numbers.tex	Thu Jul 26 17:16:02 2012 +0200
@@ -0,0 +1,611 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Numbers}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Numbers\isanewline
+\isakeyword{imports}\ Complex{\isaliteral{5F}{\isacharunderscore}}Main\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}Pretty{\isaliteral{2E}{\isachardot}}margin{\isaliteral{5F}{\isacharunderscore}}default\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{6}}{\isadigit{4}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+\isacommand{declare}\isamarkupfalse%
+\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}thy{\isaliteral{5F}{\isacharunderscore}}output{\isaliteral{5F}{\isacharunderscore}}indent\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}%
+\begin{isamarkuptext}%
+numeric literals; default simprules; can re-orient%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ m\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{2B}{\isacharplus}}\ m{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ m\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{2B}{\isacharplus}}\ m%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{oops}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{fun}\isamarkupfalse%
+\ h\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}h\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ then\ {\isadigit{2}}\ else\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\isa{h\ {\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}}
+\isa{h\ i\ {\isaliteral{3D}{\isacharequal}}\ i}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{isabelle}%
+Numeral{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{numeral_1_eq_1}
+
+\begin{isabelle}%
+{\isadigit{2}}\ {\isaliteral{2B}{\isacharplus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{add_2_eq_Suc}
+
+\begin{isabelle}%
+n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{add_2_eq_Suc'}
+
+\begin{isabelle}%
+a\ {\isaliteral{2B}{\isacharplus}}\ b\ {\isaliteral{2B}{\isacharplus}}\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2B}{\isacharplus}}\ c{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{add_assoc}
+
+\begin{isabelle}%
+a\ {\isaliteral{2B}{\isacharplus}}\ b\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2B}{\isacharplus}}\ a%
+\end{isabelle}
+\rulename{add_commute}
+
+\begin{isabelle}%
+b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2B}{\isacharplus}}\ c{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{add_left_commute}
+
+these form add_ac; similarly there is mult_ac%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}Suc{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ j{\isaliteral{2A}{\isacharasterisk}}l{\isaliteral{2A}{\isacharasterisk}}k\ {\isaliteral{2B}{\isacharplus}}\ m{\isaliteral{2A}{\isacharasterisk}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2A}{\isacharasterisk}}m\ {\isaliteral{2B}{\isacharplus}}\ i\ {\isaliteral{2B}{\isacharplus}}\ k{\isaliteral{2A}{\isacharasterisk}}j{\isaliteral{2A}{\isacharasterisk}}l{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ j\ {\isaliteral{2A}{\isacharasterisk}}\ l\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{2B}{\isacharplus}}\ m\ {\isaliteral{2A}{\isacharasterisk}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2A}{\isacharasterisk}}\ m\ {\isaliteral{2B}{\isacharplus}}\ i\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{2A}{\isacharasterisk}}\ j\ {\isaliteral{2A}{\isacharasterisk}}\ l{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ add{\isaliteral{5F}{\isacharunderscore}}ac\ mult{\isaliteral{5F}{\isacharunderscore}}ac{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{2B}{\isacharplus}}\ j\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2A}{\isacharasterisk}}\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ }f\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{2B}{\isacharplus}}\ j\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2A}{\isacharasterisk}}\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{oops}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\begin{isabelle}%
+m\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ m\ div\ k\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n\ div\ k%
+\end{isabelle}
+\rulename{div_le_mono}
+
+\begin{isabelle}%
+{\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2D}{\isacharminus}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{2D}{\isacharminus}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ k%
+\end{isabelle}
+\rulename{diff_mult_distrib}
+
+\begin{isabelle}%
+a\ mod\ b\ {\isaliteral{2A}{\isacharasterisk}}\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ c\ mod\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{mult_mod_left}
+
+\begin{isabelle}%
+P\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2D}{\isacharminus}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{3C}{\isacharless}}\ b\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}d{\isaliteral{2E}{\isachardot}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2B}{\isacharplus}}\ d\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ d{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{nat_diff_split}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}clarsimp\ split{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}diff{\isaliteral{5F}{\isacharunderscore}}split\ iff\ del{\isaliteral{3A}{\isacharcolon}}\ less{\isaliteral{5F}{\isacharunderscore}}Suc{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ %
+\isamarkupcmt{\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}d{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{3C}{\isacharless}}\ Suc\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ d{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ d\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}%
+\end{isabelle}%
+}
+\isanewline
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{22}{\isachardoublequoteopen}}n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ force{\isaliteral{2C}{\isacharcomma}}\ arith{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ split{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}diff{\isaliteral{5F}{\isacharunderscore}}split{\isaliteral{2C}{\isacharcomma}}\ clarify{\isaliteral{29}{\isacharparenright}}\isanewline
+\ %
+\isamarkupcmt{\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}d{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ d{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ d\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}%
+\end{isabelle}%
+}
+\isanewline
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{22}{\isachardoublequoteopen}}n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ n{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ force{\isaliteral{2C}{\isacharcomma}}\ arith{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\begin{isabelle}%
+m\ mod\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ m\ {\isaliteral{3C}{\isacharless}}\ n\ then\ m\ else\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2D}{\isacharminus}}\ n{\isaliteral{29}{\isacharparenright}}\ mod\ n{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{mod_if}
+
+\begin{isabelle}%
+a\ div\ b\ {\isaliteral{2A}{\isacharasterisk}}\ b\ {\isaliteral{2B}{\isacharplus}}\ a\ mod\ b\ {\isaliteral{3D}{\isacharequal}}\ a%
+\end{isabelle}
+\rulename{mod_div_equality}
+
+
+\begin{isabelle}%
+a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ div\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ div\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ div\ c%
+\end{isabelle}
+\rulename{div_mult1_eq}
+
+\begin{isabelle}%
+a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ mod\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ mod\ c%
+\end{isabelle}
+\rulename{mod_mult_right_eq}
+
+\begin{isabelle}%
+a\ div\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ b\ div\ c%
+\end{isabelle}
+\rulename{div_mult2_eq}
+
+\begin{isabelle}%
+a\ mod\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}a\ div\ b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ a\ mod\ b%
+\end{isabelle}
+\rulename{mod_mult2_eq}
+
+\begin{isabelle}%
+c\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ c\ {\isaliteral{2A}{\isacharasterisk}}\ a\ div\ {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ b%
+\end{isabelle}
+\rulename{div_mult_mult1}
+
+\begin{isabelle}%
+a\ div\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{div_by_0}
+
+\begin{isabelle}%
+a\ mod\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a%
+\end{isabelle}
+\rulename{mod_by_0}
+
+\begin{isabelle}%
+{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}m\ dvd\ n{\isaliteral{3B}{\isacharsemicolon}}\ n\ dvd\ m{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ m\ {\isaliteral{3D}{\isacharequal}}\ n%
+\end{isabelle}
+\rulename{dvd_antisym}
+
+\begin{isabelle}%
+{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}a\ dvd\ b{\isaliteral{3B}{\isacharsemicolon}}\ a\ dvd\ c{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ dvd\ b\ {\isaliteral{2B}{\isacharplus}}\ c%
+\end{isabelle}
+\rulename{dvd_add}
+
+For the integers, I'd list a few theorems that somehow involve negative 
+numbers.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Division, remainder of negatives
+
+
+\begin{isabelle}%
+{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ b\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{0}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ a\ mod\ b%
+\end{isabelle}
+\rulename{pos_mod_sign}
+
+\begin{isabelle}%
+{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ b\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ mod\ b\ {\isaliteral{3C}{\isacharless}}\ b%
+\end{isabelle}
+\rulename{pos_mod_bound}
+
+\begin{isabelle}%
+b\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ mod\ b\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isadigit{0}}%
+\end{isabelle}
+\rulename{neg_mod_sign}
+
+\begin{isabelle}%
+b\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ b\ {\isaliteral{3C}{\isacharless}}\ a\ mod\ b%
+\end{isabelle}
+\rulename{neg_mod_bound}
+
+\begin{isabelle}%
+{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{29}{\isacharparenright}}\ div\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ c\ {\isaliteral{2B}{\isacharplus}}\ b\ div\ c\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}a\ mod\ c\ {\isaliteral{2B}{\isacharplus}}\ b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ div\ c%
+\end{isabelle}
+\rulename{zdiv_zadd1_eq}
+
+\begin{isabelle}%
+{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{29}{\isacharparenright}}\ mod\ c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a\ mod\ c\ {\isaliteral{2B}{\isacharplus}}\ b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ mod\ c%
+\end{isabelle}
+\rulename{mod_add_eq}
+
+\begin{isabelle}%
+a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ div\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ div\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ div\ c%
+\end{isabelle}
+\rulename{zdiv_zmult1_eq}
+
+\begin{isabelle}%
+a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ mod\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ mod\ c%
+\end{isabelle}
+\rulename{mod_mult_right_eq}
+
+\begin{isabelle}%
+{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ div\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ b\ div\ c%
+\end{isabelle}
+\rulename{zdiv_zmult2_eq}
+
+\begin{isabelle}%
+{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ mod\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}a\ div\ b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ a\ mod\ b%
+\end{isabelle}
+\rulename{zmod_zmult2_eq}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}abs\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2B}{\isacharplus}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ abs\ x\ {\isaliteral{2B}{\isacharplus}}\ abs\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ arith%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}abs\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2A}{\isacharasterisk}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ abs\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ abs{\isaliteral{5F}{\isacharunderscore}}if{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Induction rules for the Integers
+
+\begin{isabelle}%
+{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}k\ {\isaliteral{5C3C6C653E}{\isasymle}}\ i{\isaliteral{3B}{\isacharsemicolon}}\ P\ k{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}k\ {\isaliteral{5C3C6C653E}{\isasymle}}\ i{\isaliteral{3B}{\isacharsemicolon}}\ P\ i{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ i%
+\end{isabelle}
+\rulename{int_ge_induct}
+
+\begin{isabelle}%
+{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}k\ {\isaliteral{3C}{\isacharless}}\ i{\isaliteral{3B}{\isacharsemicolon}}\ P\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}k\ {\isaliteral{3C}{\isacharless}}\ i{\isaliteral{3B}{\isacharsemicolon}}\ P\ i{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ i%
+\end{isabelle}
+\rulename{int_gr_induct}
+
+\begin{isabelle}%
+{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ P\ k{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ P\ i{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ i%
+\end{isabelle}
+\rulename{int_le_induct}
+
+\begin{isabelle}%
+{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}i\ {\isaliteral{3C}{\isacharless}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ P\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}i\ {\isaliteral{3C}{\isacharless}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ P\ i{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ i%
+\end{isabelle}
+\rulename{int_less_induct}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIELDS
+
+\begin{isabelle}%
+x\ {\isaliteral{3C}{\isacharless}}\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}z{\isaliteral{3E}{\isachargreater}}x{\isaliteral{2E}{\isachardot}}\ z\ {\isaliteral{3C}{\isacharless}}\ y%
+\end{isabelle}
+\rulename{dense}
+
+\begin{isabelle}%
+a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2F}{\isacharslash}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ {\isaliteral{2F}{\isacharslash}}\ c%
+\end{isabelle}
+\rulename{times_divide_eq_right}
+
+\begin{isabelle}%
+b\ {\isaliteral{2F}{\isacharslash}}\ c\ {\isaliteral{2A}{\isacharasterisk}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ a\ {\isaliteral{2F}{\isacharslash}}\ c%
+\end{isabelle}
+\rulename{times_divide_eq_left}
+
+\begin{isabelle}%
+a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2F}{\isacharslash}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ c\ {\isaliteral{2F}{\isacharslash}}\ b%
+\end{isabelle}
+\rulename{divide_divide_eq_right}
+
+\begin{isabelle}%
+a\ {\isaliteral{2F}{\isacharslash}}\ b\ {\isaliteral{2F}{\isacharslash}}\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{divide_divide_eq_left}
+
+\begin{isabelle}%
+{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2F}{\isacharslash}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}\ a\ {\isaliteral{2F}{\isacharslash}}\ b%
+\end{isabelle}
+\rulename{minus_divide_left}
+
+\begin{isabelle}%
+{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2F}{\isacharslash}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{2D}{\isacharminus}}\ b%
+\end{isabelle}
+\rulename{minus_divide_right}
+
+This last NOT a simprule
+
+\begin{isabelle}%
+{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2F}{\isacharslash}}\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ c\ {\isaliteral{2B}{\isacharplus}}\ b\ {\isaliteral{2F}{\isacharslash}}\ c%
+\end{isabelle}
+\rulename{add_divide_distrib}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{3}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{7}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ real{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\ \isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{8}}{\isaliteral{2F}{\isacharslash}}{\isadigit{1}}{\isadigit{5}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{8}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+\ simp%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{5}}{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{oops}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{8}}{\isaliteral{2F}{\isacharslash}}{\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ real{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{8}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ x%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}\isamarkupfalse%
+\ simp%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isadigit{2}}\ {\isaliteral{3C}{\isacharless}}\ x\ {\isaliteral{2A}{\isacharasterisk}}\ {\isadigit{5}}%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{oops}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Ring and Field
+
+Requires a field, or else an ordered ring
+
+\begin{isabelle}%
+{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ b\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{mult_eq_0_iff}
+
+\begin{isabelle}%
+{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2A}{\isacharasterisk}}\ c\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{mult_cancel_right}
+
+\begin{isabelle}%
+{\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{2A}{\isacharasterisk}}\ a\ {\isaliteral{3D}{\isacharequal}}\ c\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{mult_cancel_left}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+effect of show sorts on the above
+
+\begin{isabelle}%
+{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ring{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}zero{\isaliteral{5F}{\isacharunderscore}}divisors{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ring{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}zero{\isaliteral{5F}{\isacharunderscore}}divisors{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\isaindent{{\isaliteral{28}{\isacharparenleft}}}c\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ring{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}zero{\isaliteral{5F}{\isacharunderscore}}divisors{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
+{\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ring{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}zero{\isaliteral{5F}{\isacharunderscore}}divisors{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{mult_cancel_left}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+absolute value
+
+\begin{isabelle}%
+{\isaliteral{5C3C6261723E}{\isasymbar}}a\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}a{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}b{\isaliteral{5C3C6261723E}{\isasymbar}}%
+\end{isabelle}
+\rulename{abs_mult}
+
+\begin{isabelle}%
+{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6261723E}{\isasymbar}}a{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{5C3C6C653E}{\isasymle}}\ b\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{2D}{\isacharminus}}\ a\ {\isaliteral{5C3C6C653E}{\isasymle}}\ b{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+\rulename{abs_le_iff}
+
+\begin{isabelle}%
+{\isaliteral{5C3C6261723E}{\isasymbar}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}a{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}b{\isaliteral{5C3C6261723E}{\isasymbar}}%
+\end{isabelle}
+\rulename{abs_triangle_ineq}
+
+\begin{isabelle}%
+a\isaliteral{5C3C5E627375703E}{}\isactrlbsup m\ {\isaliteral{2B}{\isacharplus}}\ n\isaliteral{5C3C5E657375703E}{}\isactrlesup \ {\isaliteral{3D}{\isacharequal}}\ a\isaliteral{5C3C5E627375703E}{}\isactrlbsup m\isaliteral{5C3C5E657375703E}{}\isactrlesup \ {\isaliteral{2A}{\isacharasterisk}}\ a\isaliteral{5C3C5E627375703E}{}\isactrlbsup n\isaliteral{5C3C5E657375703E}{}\isactrlesup %
+\end{isabelle}
+\rulename{power_add}
+
+\begin{isabelle}%
+a\isaliteral{5C3C5E627375703E}{}\isactrlbsup m\ {\isaliteral{2A}{\isacharasterisk}}\ n\isaliteral{5C3C5E657375703E}{}\isactrlesup \ {\isaliteral{3D}{\isacharequal}}\ a\isaliteral{5C3C5E627375703E}{}\isactrlbsup m\isaliteral{5C3C5E657375703E}{}\isactrlesup \isaliteral{5C3C5E627375703E}{}\isactrlbsup n\isaliteral{5C3C5E657375703E}{}\isactrlesup %
+\end{isabelle}
+\rulename{power_mult}
+
+\begin{isabelle}%
+{\isaliteral{5C3C6261723E}{\isasymbar}}a\isaliteral{5C3C5E627375703E}{}\isactrlbsup n\isaliteral{5C3C5E657375703E}{}\isactrlesup {\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}a{\isaliteral{5C3C6261723E}{\isasymbar}}\isaliteral{5C3C5E627375703E}{}\isactrlbsup n\isaliteral{5C3C5E657375703E}{}\isactrlesup %
+\end{isabelle}
+\rulename{power_abs}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: