# HG changeset patch # User nipkow # Date 978704200 -3600 # Node ID 520dd8696927da6ff34fc3063719eba05add45c0 # Parent 260fa2c67e3e9a60c3e013abf580fb3ccd542449 *** empty log message *** diff -r 260fa2c67e3e -r 520dd8696927 doc-src/TutorialI/Inductive/Mutual.thy --- a/doc-src/TutorialI/Inductive/Mutual.thy Fri Jan 05 14:28:10 2001 +0100 +++ b/doc-src/TutorialI/Inductive/Mutual.thy Fri Jan 05 15:16:40 2001 +0100 @@ -1,10 +1,11 @@ (*<*)theory Mutual = Main:(*>*) -subsection{*Mutual inductive definitions*} +subsection{*Mutually inductive definitions*} text{* Just as there are datatypes defined by mutual recursion, there are sets defined -by mutual induction. As a trivial example we consider the even and odd natural numbers: +by mutual induction. As a trivial example we consider the even and odd +natural numbers: *} consts even :: "nat set" @@ -17,22 +18,23 @@ oddI: "n \ even \ Suc n \ odd" text{*\noindent -The simultaneous inductive definition of multiple sets is no different from that -of a single set, except for induction: just as for mutually recursive datatypes, -induction needs to involve all the simultaneously defined sets. In the above case, -the induction rule is called @{thm[source]even_odd.induct} (simply concenate the names -of the sets involved) and has the conclusion +The mutually inductive definition of multiple sets is no different from +that of a single set, except for induction: just as for mutually recursive +datatypes, induction needs to involve all the simultaneously defined sets. In +the above case, the induction rule is called @{thm[source]even_odd.induct} +(simply concatenate the names of the sets involved) and has the conclusion @{text[display]"(?x \ even \ ?P ?x) \ (?y \ odd \ ?Q ?y)"} -If we want to prove that all even numbers are divisible by 2, we have to generalize -the statement as follows: +If we want to prove that all even numbers are divisible by 2, we have to +generalize the statement as follows: *} lemma "(m \ even \ 2 dvd m) \ (n \ odd \ 2 dvd (Suc n))" txt{*\noindent -The proof is by rule induction. Because of the form of the induction theorem, it is -applied by @{text rule} rather than @{text erule} as for ordinary inductive definitions: +The proof is by rule induction. Because of the form of the induction theorem, +it is applied by @{text rule} rather than @{text erule} as for ordinary +inductive definitions: *} apply(rule even_odd.induct) @@ -56,4 +58,4 @@ (* Exercise: 1 : odd *) -(*<*)end(*>*) \ No newline at end of file +(*<*)end(*>*) diff -r 260fa2c67e3e -r 520dd8696927 doc-src/TutorialI/Inductive/document/Mutual.tex --- a/doc-src/TutorialI/Inductive/document/Mutual.tex Fri Jan 05 14:28:10 2001 +0100 +++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Fri Jan 05 15:16:40 2001 +0100 @@ -2,12 +2,13 @@ \begin{isabellebody}% \def\isabellecontext{Mutual}% % -\isamarkupsubsection{Mutual inductive definitions% +\isamarkupsubsection{Mutually inductive definitions% } % \begin{isamarkuptext}% Just as there are datatypes defined by mutual recursion, there are sets defined -by mutual induction. As a trivial example we consider the even and odd natural numbers:% +by mutual induction. As a trivial example we consider the even and odd +natural numbers:% \end{isamarkuptext}% \isacommand{consts}\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline \ \ \ \ \ \ \ odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline @@ -19,23 +20,24 @@ oddI{\isacharcolon}\ \ {\isachardoublequote}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ odd{\isachardoublequote}% \begin{isamarkuptext}% \noindent -The simultaneous inductive definition of multiple sets is no different from that -of a single set, except for induction: just as for mutually recursive datatypes, -induction needs to involve all the simultaneously defined sets. In the above case, -the induction rule is called \isa{even{\isacharunderscore}odd{\isachardot}induct} (simply concenate the names -of the sets involved) and has the conclusion +The mutually inductive definition of multiple sets is no different from +that of a single set, except for induction: just as for mutually recursive +datatypes, induction needs to involve all the simultaneously defined sets. In +the above case, the induction rule is called \isa{even{\isacharunderscore}odd{\isachardot}induct} +(simply concatenate the names of the sets involved) and has the conclusion \begin{isabelle}% \ \ \ \ \ {\isacharparenleft}{\isacharquery}x\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isacharquery}P\ {\isacharquery}x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isacharquery}y\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isacharquery}Q\ {\isacharquery}y{\isacharparenright}% \end{isabelle} -If we want to prove that all even numbers are divisible by 2, we have to generalize -the statement as follows:% +If we want to prove that all even numbers are divisible by 2, we have to +generalize the statement as follows:% \end{isamarkuptext}% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}m\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ m{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent -The proof is by rule induction. Because of the form of the induction theorem, it is -applied by \isa{rule} rather than \isa{erule} as for ordinary inductive definitions:% +The proof is by rule induction. Because of the form of the induction theorem, +it is applied by \isa{rule} rather than \isa{erule} as for ordinary +inductive definitions:% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}rule\ even{\isacharunderscore}odd{\isachardot}induct{\isacharparenright}% \begin{isamarkuptxt}% diff -r 260fa2c67e3e -r 520dd8696927 doc-src/TutorialI/Rules/Primes.thy --- a/doc-src/TutorialI/Rules/Primes.thy Fri Jan 05 14:28:10 2001 +0100 +++ b/doc-src/TutorialI/Rules/Primes.thy Fri Jan 05 15:16:40 2001 +0100 @@ -77,7 +77,7 @@ (*Maximality: for all m,n,k naturals, if k divides m and k divides n then k divides gcd(m,n)*) lemma gcd_greatest [rule_format]: - "(k dvd m) \ (k dvd n) \ k dvd gcd(m,n)" + "k dvd m \ k dvd n \ k dvd gcd(m,n)" apply (induct_tac m n rule: gcd.induct) apply (case_tac "n=0") apply (simp_all add: dvd_mod); @@ -266,7 +266,7 @@ done lemma relprime_dvd_mult: - "\ gcd(k,n)=1; k dvd (m*n) \ \ k dvd m"; + "\ gcd(k,n)=1; k dvd m*n \ \ k dvd m"; apply (insert gcd_mult_distrib2 [of m k n]) apply (simp) apply (erule_tac t="m" in ssubst); @@ -287,7 +287,7 @@ apply (simp) done -lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \ k dvd (m*n) = k dvd m"; +lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \ (k dvd m*n) = (k dvd m)"; apply (blast intro: relprime_dvd_mult dvd_trans) done diff -r 260fa2c67e3e -r 520dd8696927 doc-src/TutorialI/ToyList/ToyList.thy --- a/doc-src/TutorialI/ToyList/ToyList.thy Fri Jan 05 14:28:10 2001 +0100 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Fri Jan 05 15:16:40 2001 +0100 @@ -48,8 +48,8 @@ In contrast to ML, Isabelle insists on explicit declarations of all functions (keyword \isacommand{consts}). (Apart from the declaration-before-use restriction, the order of items in a theory file is unconstrained.) Function -@{term"app"} is annotated with concrete syntax too. Instead of the prefix -syntax \isa{app xs ys} the infix +@{text"app"} is annotated with concrete syntax too. Instead of the +prefix syntax @{text"app xs ys"} the infix @{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred form. Both functions are defined recursively: *} @@ -64,10 +64,10 @@ text{* \noindent -The equations for @{term"app"} and @{term"rev"} hardly need comments: -@{term"app"} appends two lists and @{term"rev"} reverses a list. The keyword -\isacommand{primrec}\index{*primrec} indicates that the recursion is of a -particularly primitive kind where each recursive call peels off a datatype +The equations for @{text"app"} and @{term"rev"} hardly need comments: +@{text"app"} appends two lists and @{term"rev"} reverses a list. The +keyword \isacommand{primrec}\index{*primrec} indicates that the recursion is +of a particularly primitive kind where each recursive call peels off a datatype constructor from one of the arguments. Thus the recursion always terminates, i.e.\ the function is \textbf{total}. \index{total function} diff -r 260fa2c67e3e -r 520dd8696927 doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jan 05 14:28:10 2001 +0100 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jan 05 15:16:40 2001 +0100 @@ -48,8 +48,8 @@ In contrast to ML, Isabelle insists on explicit declarations of all functions (keyword \isacommand{consts}). (Apart from the declaration-before-use restriction, the order of items in a theory file is unconstrained.) Function -\isa{op\ {\isacharat}} is annotated with concrete syntax too. Instead of the prefix -syntax \isa{app xs ys} the infix +\isa{app} is annotated with concrete syntax too. Instead of the +prefix syntax \isa{app\ xs\ ys} the infix \isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred form. Both functions are defined recursively:% \end{isamarkuptext}% @@ -62,10 +62,10 @@ {\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent -The equations for \isa{op\ {\isacharat}} and \isa{rev} hardly need comments: -\isa{op\ {\isacharat}} appends two lists and \isa{rev} reverses a list. The keyword -\isacommand{primrec}\index{*primrec} indicates that the recursion is of a -particularly primitive kind where each recursive call peels off a datatype +The equations for \isa{app} and \isa{rev} hardly need comments: +\isa{app} appends two lists and \isa{rev} reverses a list. The +keyword \isacommand{primrec}\index{*primrec} indicates that the recursion is +of a particularly primitive kind where each recursive call peels off a datatype constructor from one of the arguments. Thus the recursion always terminates, i.e.\ the function is \textbf{total}. \index{total function} diff -r 260fa2c67e3e -r 520dd8696927 doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Fri Jan 05 14:28:10 2001 +0100 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Fri Jan 05 15:16:40 2001 +0100 @@ -4,7 +4,8 @@ \isanewline \isacommand{theory}\ Numbers\ {\isacharequal}\ Real{\isacharcolon}\isanewline \isanewline -\isacommand{ML}\ {\isachardoublequote}Pretty{\isachardot}setmargin\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequote}% +\isacommand{ML}\ {\isachardoublequote}Pretty{\isachardot}setmargin\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequote}\isanewline +\isacommand{ML}\ {\isachardoublequote}IsarOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequote}% \begin{isamarkuptext}% numeric literals; default simprules; can re-orient% \end{isamarkuptext}% @@ -19,37 +20,37 @@ \begin{isabelle}% -\ \ \ \ \ {\isacharhash}{\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}% +{\isacharhash}{\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}% \end{isabelle} \rulename{numeral_0_eq_0} \begin{isabelle}% -\ \ \ \ \ {\isacharhash}{\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}% +{\isacharhash}{\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}% \end{isabelle} \rulename{numeral_1_eq_1} \begin{isabelle}% -\ \ \ \ \ {\isacharhash}{\isadigit{2}}\ {\isacharplus}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% +{\isacharhash}{\isadigit{2}}\ {\isacharplus}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% \end{isabelle} \rulename{add_2_eq_Suc} \begin{isabelle}% -\ \ \ \ \ n\ {\isacharplus}\ {\isacharhash}{\isadigit{2}}\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% +n\ {\isacharplus}\ {\isacharhash}{\isadigit{2}}\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% \end{isabelle} \rulename{add_2_eq_Suc'} \begin{isabelle}% -\ \ \ \ \ m\ {\isacharplus}\ n\ {\isacharplus}\ k\ {\isacharequal}\ m\ {\isacharplus}\ {\isacharparenleft}n\ {\isacharplus}\ k{\isacharparenright}% +m\ {\isacharplus}\ n\ {\isacharplus}\ k\ {\isacharequal}\ m\ {\isacharplus}\ {\isacharparenleft}n\ {\isacharplus}\ k{\isacharparenright}% \end{isabelle} \rulename{add_assoc} \begin{isabelle}% -\ \ \ \ \ m\ {\isacharplus}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m% +m\ {\isacharplus}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m% \end{isabelle} \rulename{add_commute} \begin{isabelle}% -\ \ \ \ \ x\ {\isacharplus}\ {\isacharparenleft}y\ {\isacharplus}\ z{\isacharparenright}\ {\isacharequal}\ y\ {\isacharplus}\ {\isacharparenleft}x\ {\isacharplus}\ z{\isacharparenright}% +x\ {\isacharplus}\ {\isacharparenleft}y\ {\isacharplus}\ z{\isacharparenright}\ {\isacharequal}\ y\ {\isacharplus}\ {\isacharparenleft}x\ {\isacharplus}\ z{\isacharparenright}% \end{isabelle} \rulename{add_left_commute} @@ -75,37 +76,37 @@ % \begin{isamarkuptext}% \begin{isabelle}% -\ \ \ \ \ {\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ k\ {\isasymle}\ l{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isasymle}\ j\ {\isacharasterisk}\ l% +{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ k\ {\isasymle}\ l{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isasymle}\ j\ {\isacharasterisk}\ l% \end{isabelle} \rulename{mult_le_mono} \begin{isabelle}% -\ \ \ \ \ {\isasymlbrakk}i\ {\isacharless}\ j{\isacharsemicolon}\ {\isadigit{0}}\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isacharless}\ j\ {\isacharasterisk}\ k% +{\isasymlbrakk}i\ {\isacharless}\ j{\isacharsemicolon}\ {\isadigit{0}}\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isacharless}\ j\ {\isacharasterisk}\ k% \end{isabelle} \rulename{mult_less_mono1} \begin{isabelle}% -\ \ \ \ \ m\ {\isasymle}\ n\ {\isasymLongrightarrow}\ m\ div\ k\ {\isasymle}\ n\ div\ k% +m\ {\isasymle}\ n\ {\isasymLongrightarrow}\ m\ div\ k\ {\isasymle}\ n\ div\ k% \end{isabelle} \rulename{div_le_mono} \begin{isabelle}% -\ \ \ \ \ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ {\isacharplus}\ n\ {\isacharasterisk}\ k% +{\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ {\isacharplus}\ n\ {\isacharasterisk}\ k% \end{isabelle} \rulename{add_mult_distrib} \begin{isabelle}% -\ \ \ \ \ {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ {\isacharminus}\ n\ {\isacharasterisk}\ k% +{\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ {\isacharminus}\ n\ {\isacharasterisk}\ k% \end{isabelle} \rulename{diff_mult_distrib} \begin{isabelle}% -\ \ \ \ \ m\ mod\ n\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ mod\ {\isacharparenleft}n\ {\isacharasterisk}\ k{\isacharparenright}% +m\ mod\ n\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ mod\ {\isacharparenleft}n\ {\isacharasterisk}\ k{\isacharparenright}% \end{isabelle} \rulename{mod_mult_distrib} \begin{isabelle}% -\ \ \ \ \ 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}% +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}% \end{isabelle} \rulename{nat_diff_split}% \end{isamarkuptext}% @@ -114,58 +115,58 @@ \isacommand{done}% \begin{isamarkuptext}% \begin{isabelle}% -\ \ \ \ \ m\ mod\ n\ {\isacharequal}\ {\isacharparenleft}if\ m\ {\isacharless}\ n\ then\ m\ else\ {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ mod\ n{\isacharparenright}% +m\ mod\ n\ {\isacharequal}\ {\isacharparenleft}if\ m\ {\isacharless}\ n\ then\ m\ else\ {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ mod\ n{\isacharparenright}% \end{isabelle} \rulename{mod_if} \begin{isabelle}% -\ \ \ \ \ m\ div\ n\ {\isacharasterisk}\ n\ {\isacharplus}\ m\ mod\ n\ {\isacharequal}\ m% +m\ div\ n\ {\isacharasterisk}\ n\ {\isacharplus}\ m\ mod\ n\ {\isacharequal}\ m% \end{isabelle} \rulename{mod_div_equality} \begin{isabelle}% -\ \ \ \ \ a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c% +a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c% \end{isabelle} \rulename{div_mult1_eq} \begin{isabelle}% -\ \ \ \ \ a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c% +a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c% \end{isabelle} \rulename{mod_mult1_eq} \begin{isabelle}% -\ \ \ \ \ a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c% +a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c% \end{isabelle} \rulename{div_mult2_eq} \begin{isabelle}% -\ \ \ \ \ a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b% +a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b% \end{isabelle} \rulename{mod_mult2_eq} \begin{isabelle}% -\ \ \ \ \ {\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ c\ {\isacharasterisk}\ a\ div\ {\isacharparenleft}c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ a\ div\ b% +{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ c\ {\isacharasterisk}\ a\ div\ {\isacharparenleft}c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ a\ div\ b% \end{isabelle} \rulename{div_mult_mult1} \begin{isabelle}% -\ \ \ \ \ a\ div\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}% +a\ div\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}% \end{isabelle} \rulename{DIVISION_BY_ZERO_DIV} \begin{isabelle}% -\ \ \ \ \ a\ mod\ {\isadigit{0}}\ {\isacharequal}\ a% +a\ mod\ {\isadigit{0}}\ {\isacharequal}\ a% \end{isabelle} \rulename{DIVISION_BY_ZERO_MOD} \begin{isabelle}% -\ \ \ \ \ {\isasymlbrakk}m\ dvd\ n{\isacharsemicolon}\ n\ dvd\ m{\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n% +{\isasymlbrakk}m\ dvd\ n{\isacharsemicolon}\ n\ dvd\ m{\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n% \end{isabelle} \rulename{dvd_anti_sym} \begin{isabelle}% -\ \ \ \ \ {\isasymlbrakk}k\ dvd\ m{\isacharsemicolon}\ k\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ k\ dvd\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}% +{\isasymlbrakk}k\ dvd\ m{\isacharsemicolon}\ k\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ k\ dvd\ m\ {\isacharplus}\ n% \end{isabelle} \rulename{dvd_add} @@ -176,58 +177,57 @@ \begin{isabelle}% -\ \ \ \ \ {\isacharhash}{\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{0}}\ {\isasymle}\ a\ mod\ b% +{\isacharhash}{\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isacharhash}{\isadigit{0}}\ {\isasymle}\ a\ mod\ b% \end{isabelle} \rulename{pos_mod_sign} \begin{isabelle}% -\ \ \ \ \ {\isacharhash}{\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isacharless}\ b% +{\isacharhash}{\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isacharless}\ b% \end{isabelle} \rulename{pos_mod_bound} \begin{isabelle}% -\ \ \ \ \ b\ {\isacharless}\ {\isacharhash}{\isadigit{0}}\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isasymle}\ {\isacharhash}{\isadigit{0}}% +b\ {\isacharless}\ {\isacharhash}{\isadigit{0}}\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isasymle}\ {\isacharhash}{\isadigit{0}}% \end{isabelle} \rulename{neg_mod_sign} \begin{isabelle}% -\ \ \ \ \ b\ {\isacharless}\ {\isacharhash}{\isadigit{0}}\ {\isasymLongrightarrow}\ b\ {\isacharless}\ a\ mod\ b% +b\ {\isacharless}\ {\isacharhash}{\isadigit{0}}\ {\isasymLongrightarrow}\ b\ {\isacharless}\ a\ mod\ b% \end{isabelle} \rulename{neg_mod_bound} \begin{isabelle}% -\ \ \ \ \ {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ div\ c\ {\isacharequal}\isanewline -\ \ \ \ \ a\ div\ c\ {\isacharplus}\ b\ div\ c\ {\isacharplus}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ div\ c% +{\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% \end{isabelle} \rulename{zdiv_zadd1_eq} \begin{isabelle}% -\ \ \ \ \ {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ mod\ c\ {\isacharequal}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ mod\ c% +{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ mod\ c\ {\isacharequal}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ mod\ c% \end{isabelle} \rulename{zmod_zadd1_eq} \begin{isabelle}% -\ \ \ \ \ a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c% +a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c% \end{isabelle} \rulename{zdiv_zmult1_eq} \begin{isabelle}% -\ \ \ \ \ a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c% +a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c% \end{isabelle} \rulename{zmod_zmult1_eq} \begin{isabelle}% -\ \ \ \ \ {\isacharhash}{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c% +{\isacharhash}{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c% \end{isabelle} \rulename{zdiv_zmult2_eq} \begin{isabelle}% -\ \ \ \ \ {\isacharhash}{\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% +{\isacharhash}{\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% \end{isabelle} \rulename{zmod_zmult2_eq} \begin{isabelle}% -\ \ \ \ \ {\isasymbar}x\ {\isacharasterisk}\ y{\isasymbar}\ {\isacharequal}\ {\isasymbar}x{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}y{\isasymbar}% +{\isasymbar}x\ {\isacharasterisk}\ y{\isasymbar}\ {\isacharequal}\ {\isasymbar}x{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}y{\isasymbar}% \end{isabelle} \rulename{abs_mult}% \end{isamarkuptext}% @@ -236,53 +236,56 @@ REALS \begin{isabelle}% -\ \ \ \ \ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n\ {\isacharequal}\ {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}% +{\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n\ {\isacharequal}\ {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}% \end{isabelle} \rulename{realpow_abs} \begin{isabelle}% -\ \ \ \ \ x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ x\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ y% +x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ x\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ y% \end{isabelle} \rulename{real_dense} \begin{isabelle}% -\ \ \ \ \ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n\ {\isacharequal}\ {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}% +{\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n\ {\isacharequal}\ {\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}% \end{isabelle} \rulename{realpow_abs} \begin{isabelle}% -\ \ \ \ \ x\ {\isacharasterisk}\ {\isacharparenleft}y\ {\isacharslash}\ z{\isacharparenright}\ {\isacharequal}\ x\ {\isacharasterisk}\ y\ {\isacharslash}\ z% +x\ {\isacharasterisk}\ {\isacharparenleft}y\ {\isacharslash}\ z{\isacharparenright}\ {\isacharequal}\ x\ {\isacharasterisk}\ y\ {\isacharslash}\ z% \end{isabelle} \rulename{real_times_divide1_eq} \begin{isabelle}% -\ \ \ \ \ y\ {\isacharslash}\ z\ {\isacharasterisk}\ x\ {\isacharequal}\ y\ {\isacharasterisk}\ x\ {\isacharslash}\ z% +y\ {\isacharslash}\ z\ {\isacharasterisk}\ x\ {\isacharequal}\ y\ {\isacharasterisk}\ x\ {\isacharslash}\ z% \end{isabelle} \rulename{real_times_divide2_eq} \begin{isabelle}% -\ \ \ \ \ x\ {\isacharslash}\ {\isacharparenleft}y\ {\isacharslash}\ z{\isacharparenright}\ {\isacharequal}\ x\ {\isacharasterisk}\ z\ {\isacharslash}\ y% +x\ {\isacharslash}\ {\isacharparenleft}y\ {\isacharslash}\ z{\isacharparenright}\ {\isacharequal}\ x\ {\isacharasterisk}\ z\ {\isacharslash}\ y% \end{isabelle} \rulename{real_divide_divide1_eq} \begin{isabelle}% -\ \ \ \ \ x\ {\isacharslash}\ y\ {\isacharslash}\ z\ {\isacharequal}\ x\ {\isacharslash}\ {\isacharparenleft}y\ {\isacharasterisk}\ z{\isacharparenright}% +x\ {\isacharslash}\ y\ {\isacharslash}\ z\ {\isacharequal}\ x\ {\isacharslash}\ {\isacharparenleft}y\ {\isacharasterisk}\ z{\isacharparenright}% \end{isabelle} \rulename{real_divide_divide2_eq} \begin{isabelle}% -\ \ \ \ \ {\isacharminus}\ x\ {\isacharslash}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}% +{\isacharminus}\ x\ {\isacharslash}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}% \end{isabelle} \rulename{real_minus_divide_eq} \begin{isabelle}% -\ \ \ \ \ x\ {\isacharslash}\ {\isacharminus}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}% +x\ {\isacharslash}\ {\isacharminus}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}% \end{isabelle} \rulename{real_divide_minus_eq} This last NOT a simprule -real_add_divide_distrib% +\begin{isabelle}% +{\isacharparenleft}x\ {\isacharplus}\ y{\isacharparenright}\ {\isacharslash}\ z\ {\isacharequal}\ x\ {\isacharslash}\ z\ {\isacharplus}\ y\ {\isacharslash}\ z% +\end{isabelle} +\rulename{real_add_divide_distrib}% \end{isamarkuptext}% \isacommand{end}\isanewline \end{isabellebody}%