--- 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 \<in> even \<Longrightarrow> Suc n \<in> 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 \<in> even \<longrightarrow> ?P ?x) \<and> (?y \<in> odd \<longrightarrow> ?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 \<in> even \<longrightarrow> 2 dvd m) \<and> (n \<in> odd \<longrightarrow> 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(*>*)
--- 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}%
--- 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) \<longrightarrow> (k dvd n) \<longrightarrow> k dvd gcd(m,n)"
+ "k dvd m \<longrightarrow> k dvd n \<longrightarrow> 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:
- "\<lbrakk> gcd(k,n)=1; k dvd (m*n) \<rbrakk> \<Longrightarrow> k dvd m";
+ "\<lbrakk> gcd(k,n)=1; k dvd m*n \<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> k dvd (m*n) = k dvd m";
+lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
apply (blast intro: relprime_dvd_mult dvd_trans)
done
--- 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}
--- 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}
--- 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}%