--- a/doc-src/TutorialI/Inductive/Advanced.thy Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Inductive/Advanced.thy Mon Nov 12 10:56:38 2001 +0100
@@ -76,6 +76,7 @@
by (blast intro!: mono_Int monoI gterms_mono)
+text{*the following declaration isn't actually used*}
consts integer_arity :: "integer_op \<Rightarrow> nat"
primrec
"integer_arity (Number n) = 0"
--- a/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Nov 12 10:56:38 2001 +0100
@@ -112,10 +112,12 @@
\isacommand{lemma}\ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
\ \ \ \ \ {\isachardoublequote}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isanewline
-\isanewline
-\isanewline
-\isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+the following declaration isn't actually used%
+\end{isamarkuptext}%
+\isamarkuptrue%
\isacommand{consts}\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{primrec}\isanewline
--- a/doc-src/TutorialI/Rules/Forward.thy Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Rules/Forward.thy Mon Nov 12 10:56:38 2001 +0100
@@ -33,15 +33,6 @@
as far as HERE.
*}
-
-text {*
-@{thm[display] gcd_1}
-\rulename{gcd_1}
-
-@{thm[display] gcd_1_left}
-\rulename{gcd_1_left}
-*};
-
text{*\noindent
SKIP THIS PROOF
*}
--- a/doc-src/TutorialI/Rules/rules.tex Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Mon Nov 12 10:56:38 2001 +0100
@@ -1818,7 +1818,7 @@
appearance from left to right. In this case, the variables are \isa{?k}, \isa{?m}
and~\isa{?n}. So, the expression
\hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m}
-by~\isa{1}.\REMARK{which 1 do we use?? (right the way down)}
+by~\isa{1}.
\begin{isabelle}
\isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1]
\end{isabelle}
@@ -1890,8 +1890,7 @@
\end{isabelle}
%
Normally we would never name the intermediate theorems
-such as \isa{gcd_mult_0} and
-\isa{gcd_mult_1} but would combine
+such as \isa{gcd_mult_0} and \isa{gcd_mult_1} but would combine
the three forward steps:
\begin{isabelle}
\isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]%
@@ -1959,7 +1958,7 @@
First, we
prove an instance of its first premise:
\begin{isabelle}
-\isacommand{lemma}\ relprime_20_81:\ "gcd(\#20,\#81)\ =\ 1"\isanewline
+\isacommand{lemma}\ relprime_20_81:\ "gcd(20,81)\ =\ 1"\isanewline
\isacommand{by}\ (simp\ add:\ gcd.simps)
\end{isabelle}
We have evaluated an application of the \isa{gcd} function by
@@ -1973,7 +1972,7 @@
\end{isabelle}
yields the theorem
\begin{isabelle}
-\ \ \ \ \ \#20\ dvd\ (?m\ *\ \#81)\ \isasymLongrightarrow\ \#20\ dvd\ ?m%
+\ \ \ \ \ 20\ dvd\ (?m\ *\ 81)\ \isasymLongrightarrow\ 20\ dvd\ ?m%
\end{isabelle}
%
\isa{OF} takes any number of operands. Consider
@@ -2048,10 +2047,10 @@
For example, let us prove a fact about divisibility in the natural numbers:
\begin{isabelle}
-\isacommand{lemma}\ "\#2\ \isasymle \ u\ \isasymLongrightarrow \ u*m\ \isasymnoteq
+\isacommand{lemma}\ "2\ \isasymle \ u\ \isasymLongrightarrow \ u*m\ \isasymnoteq
\ Suc(u*n)"\isanewline
\isacommand{apply}\ intro\isanewline
-\ 1.\ \isasymlbrakk \#2\ \isasymle \ u;\ u\ *\ m\ =\ Suc\ (u\ *\ n)\isasymrbrakk \ \isasymLongrightarrow \ False%
+\ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ =\ Suc\ (u\ *\ n)\isasymrbrakk \ \isasymLongrightarrow \ False%
\end{isabelle}
%
The key step is to apply the function \ldots\isa{mod\ u} to both sides of the
@@ -2060,7 +2059,7 @@
\begin{isabelle}
\isacommand{apply}\ (drule_tac\ f="\isasymlambda x.\ x\ mod\ u"\ \isakeyword{in}\
arg_cong)\isanewline
-\ 1.\ \isasymlbrakk \#2\ \isasymle \ u;\ u\ *\ m\ mod\ u\ =\ Suc\ (u\ *\ n)\ mod\
+\ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ mod\ u\ =\ Suc\ (u\ *\ n)\ mod\
u\isasymrbrakk \ \isasymLongrightarrow \ False
\end{isabelle}
%
@@ -2175,13 +2174,13 @@
Look at the following example.
\begin{isabelle}
-\isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ \#37;\ \#66\ <\ \#2*z;\ z*z\
-\isasymnoteq\ \#1225;\ Q(\#34);\ Q(\#36)\isasymrbrakk\isanewline
+\isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ 37;\ 66\ <\ 2*z;\ z*z\
+\isasymnoteq\ 1225;\ Q(34);\ Q(36)\isasymrbrakk\isanewline
\ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ Q(z)"\isanewline
-\isacommand{apply}\ (subgoal_tac\ "z\ =\ \#34\ \isasymor\ z\ =\
-\#36")\isanewline
+\isacommand{apply}\ (subgoal_tac\ "z\ =\ 34\ \isasymor\ z\ =\
+36")\isanewline
\isacommand{apply}\ blast\isanewline
-\isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ \#35")\isanewline
+\isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ 35")\isanewline
\isacommand{apply}\ arith\isanewline
\isacommand{apply}\ force\isanewline
\isacommand{done}
@@ -2196,25 +2195,25 @@
step is to claim that \isa{z} is either 34 or 36. The resulting proof
state gives us two subgoals:
\begin{isabelle}
-%\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\
-%Q\ \#34;\ Q\ \#36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline
-\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
-\ \ \ \ \ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isasymrbrakk\isanewline
+%\isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\
+%Q\ 34;\ Q\ 36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline
+\ 1.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36;\isanewline
+\ \ \ \ \ z\ =\ 34\ \isasymor\ z\ =\ 36\isasymrbrakk\isanewline
\ \ \ \ \isasymLongrightarrow\ Q\ z\isanewline
-\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
-\ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36
+\ 2.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36\isasymrbrakk\isanewline
+\ \ \ \ \isasymLongrightarrow\ z\ =\ 34\ \isasymor\ z\ =\ 36
\end{isabelle}
The first subgoal is trivial (\isa{blast}), but for the second Isabelle needs help to eliminate
the case
\isa{z}=35. The second invocation of {\isa{subgoal_tac}} leaves two
subgoals:
\begin{isabelle}
-\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\
-\#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
-\ \ \ \ \ z\ \isasymnoteq\ \#35\isasymrbrakk\isanewline
-\ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isanewline
-\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
-\ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35
+\ 1.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\
+1225;\ Q\ 34;\ Q\ 36;\isanewline
+\ \ \ \ \ z\ \isasymnoteq\ 35\isasymrbrakk\isanewline
+\ \ \ \ \isasymLongrightarrow\ z\ =\ 34\ \isasymor\ z\ =\ 36\isanewline
+\ 2.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36\isasymrbrakk\isanewline
+\ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ 35
\end{isabelle}
Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic
@@ -2286,8 +2285,8 @@
implications in which most of the antecedents are proved by assumption, but one is
proved by arithmetic:
\begin{isabelle}
-\isacommand{lemma}\ "\isasymlbrakk Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ x<\#5\isasymlongrightarrow P;\
-Suc\ x\ <\ \#5\isasymrbrakk \ \isasymLongrightarrow \ R"\ \isanewline
+\isacommand{lemma}\ "\isasymlbrakk Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ x<5\isasymlongrightarrow P;\
+Suc\ x\ <\ 5\isasymrbrakk \ \isasymLongrightarrow \ R"\ \isanewline
\isacommand{by}\ (drule\ mp,\ (assumption|arith))+
\end{isabelle}
The \isa{arith}
--- a/doc-src/TutorialI/Types/Numbers.thy Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy Mon Nov 12 10:56:38 2001 +0100
@@ -83,8 +83,15 @@
*}
+lemma "(n - 1) * (n + 1) = n * n - (1::nat)"
+apply (clarsimp split: nat_diff_split)
+ --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (subgoal_tac "n=0", force, arith)
+done
+
+
lemma "(n - 2) * (n + 2) = n * n - (4::nat)"
-apply (clarsimp split: nat_diff_split)
+apply (simp split: nat_diff_split, clarify)
--{* @{subgoals[display,indent=0,margin=65]} *}
apply (subgoal_tac "n=0 | n=1", force, arith)
done
--- a/doc-src/TutorialI/Types/Records.thy Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Types/Records.thy Mon Nov 12 10:56:38 2001 +0100
@@ -112,7 +112,6 @@
@{text [display]
" point = (| Xcoord :: int, Ycoord :: int |)
'a point_scheme = (| Xcoord :: int, Ycoord :: int, ... :: 'a |)"}
- Extensions `...' must be in type class @{text more}.
*}
constdefs
--- a/doc-src/TutorialI/Types/document/Numbers.tex Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Mon Nov 12 10:56:38 2001 +0100
@@ -130,9 +130,25 @@
\rulename{nat_diff_split}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
+\ %
+\isamarkupcmt{\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ Suc\ {\isadigit{0}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ Suc\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%
+\end{isabelle}%
+}
+\isanewline
+\isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}n{\isacharequal}{\isadigit{0}}{\isachardoublequote}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isacommand{done}\isanewline
+\isanewline
+\isanewline
+\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{apply}\ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
+\isacommand{apply}\ {\isacharparenleft}simp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharcomma}\ clarify{\isacharparenright}\isanewline
\ %
\isamarkupcmt{\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ {\isadigit{4}}\ {\isacharplus}\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%
--- a/doc-src/TutorialI/Types/numerics.tex Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Mon Nov 12 10:56:38 2001 +0100
@@ -41,15 +41,15 @@
\label{sec:numerals}
\index{numeric literals|(}%
-Literals are available for the types of natural numbers, integers
-and reals and denote integer values of arbitrary size.
-They begin
-with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and
-then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3}
-and \isa{\#441223334678}.\REMARK{will need updating?}
+The constants \cdx{0} and \cdx{1} are overloaded. They denote zero and one,
+respectively, for all numeric types. Other values are expressed by numeric
+literals, which consist of one or more decimal digits optionally preceeded by
+a minus sign (\isa{-}). Examples are \isa{2}, \isa{-3} and
+\isa{441223334678}. Literals are available for the types of natural numbers,
+integers and reals; they denote integer values of arbitrary size.
Literals look like constants, but they abbreviate
-terms, representing the number in a two's complement binary notation.
+terms representing the number in a two's complement binary notation.
Isabelle performs arithmetic on literals by rewriting rather
than using the hardware arithmetic. In most cases arithmetic
is fast enough, even for large numbers. The arithmetic operations
@@ -64,14 +64,14 @@
type constraints. Here is an example of what can go wrong:
\par
\begin{isabelle}
-\isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"
+\isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m"
\end{isabelle}
%
Carefully observe how Isabelle displays the subgoal:
\begin{isabelle}
-\ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m
+\ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m
\end{isabelle}
-The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric
+The type \isa{'a} given for the literal \isa{2} warns us that no numeric
type has been specified. The problem is underspecified. Given a type
constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
\end{warn}
@@ -83,13 +83,13 @@
rejected:
\begin{isabelle}
\isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
-"h\ \#3\ =\ \#2"\isanewline
+"h\ 3\ =\ 2"\isanewline
"h\ i\ \ =\ i"
\end{isabelle}
You should use a conditional expression instead:
\begin{isabelle}
-"h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)"
+"h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)"
\end{isabelle}
\index{numeric literals|)}
\end{warn}
@@ -106,29 +106,30 @@
\subsubsection{Literals}
\index{numeric literals!for type \protect\isa{nat}}%
-The notational options for the natural numbers are confusing. The
-constant \cdx{0} is overloaded to serve as the neutral value
-in a variety of additive types. The symbols \sdx{1} and \sdx{2} are
-not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},
-respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2} are
-syntactically different from \isa{0}, \isa{1} and \isa{2}. You will\REMARK{will need updating?}
-sometimes prefer one notation to the other. Literals are obviously
-necessary to express large values, while \isa{0} and \isa{Suc} are needed
-in order to match many theorems, including the rewrite rules for primitive
-recursive functions. The following default simplification rules replace
+The notational options for the natural numbers are confusing. Recall that an
+overloaded constant can be defined independently for each type; the definition
+of \cdx{1} for type \isa{nat} is
+\begin{isabelle}
+1\ \isasymequiv\ Suc\ 0
+\rulename{One_nat_def}
+\end{isabelle}
+This is installed as a simplification rule, so the simplifier will replace
+every occurrence of \isa{1::nat} by \isa{Suc\ 0}. Literals are obviously
+better than nested \isa{Suc}s at expressing large values. But many theorems,
+including the rewrite rules for primitive recursive functions, can only be
+applied to terms of the form \isa{Suc\ $n$}.
+
+The following default simplification rules replace
small literals by zero and successor:
\begin{isabelle}
-\#0\ =\ 0
-\rulename{numeral_0_eq_0}\isanewline
-\#1\ =\ 1
-\rulename{numeral_1_eq_1}\isanewline
-\#2\ +\ n\ =\ Suc\ (Suc\ n)
+2\ +\ n\ =\ Suc\ (Suc\ n)
\rulename{add_2_eq_Suc}\isanewline
-n\ +\ \#2\ =\ Suc\ (Suc\ n)
+n\ +\ 2\ =\ Suc\ (Suc\ n)
\rulename{add_2_eq_Suc'}
\end{isabelle}
-In special circumstances, you may wish to remove or reorient
-these rules.
+It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and
+the simplifier will normally reverse this transformation. Novices should
+express natural numbers using \isa{0} and \isa{Suc} only.
\subsubsection{Typical lemmas}
Inequalities involving addition and subtraction alone can be proved
@@ -225,11 +226,17 @@
d))
\rulename{nat_diff_split}
\end{isabelle}
-For example, this splitting proves the following fact, which lies outside the scope of
-linear arithmetic:\REMARK{replace by new example!}
+For example, splitting helps to prove the following fact:
\begin{isabelle}
-\isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline
-\isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline
+\isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline
+\isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline
+\ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0
+\end{isabelle}
+The result lies outside the scope of linear arithmetic, but
+ it is easily found
+if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:
+\begin{isabelle}
+\isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
\isacommand{done}
\end{isabelle}
@@ -313,13 +320,13 @@
mathematical practice: the sign of the remainder follows that
of the divisor:
\begin{isabelle}
-\#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b%
+0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b%
\rulename{pos_mod_sign}\isanewline
-\#0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
+0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
\rulename{pos_mod_bound}\isanewline
-b\ <\ \#0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ \#0
+b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0
\rulename{neg_mod_sign}\isanewline
-b\ <\ \#0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
+b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
\rulename{neg_mod_bound}
\end{isabelle}
ML treats negative divisors in the same way, but most computer hardware
@@ -342,9 +349,9 @@
\end{isabelle}
\begin{isabelle}
-\#0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
+0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
\rulename{zdiv_zmult2_eq}\isanewline
-\#0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
+0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
c)\ +\ a\ mod\ b%
\rulename{zmod_zmult2_eq}
\end{isabelle}
@@ -426,18 +433,18 @@
\isa{int} and only express integral values. Fractions expressed
using the division operator are automatically simplified to lowest terms:
\begin{isabelle}
-\ 1.\ P\ ((\#3\ /\ \#4)\ *\ (\#8\ /\ \#15))\isanewline
+\ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
\isacommand{apply} simp\isanewline
-\ 1.\ P\ (\#2\ /\ \#5)
+\ 1.\ P\ (2\ /\ 5)
\end{isabelle}
Exponentiation can express floating-point values such as
-\isa{\#2 * \#10\isacharcircum\#6}, but at present no special simplification
+\isa{2 * 10\isacharcircum6}, but at present no special simplification
is performed.
\begin{warn}
Type \isa{real} is only available in the logic HOL-Real, which
-is HOL extended with the rather substantial development of the real
+is HOL extended with a definitional development of the real
numbers. Base your theory upon theory
\thydx{Real}, not the usual \isa{Main}.%
\index{real numbers|)}\index{*real (type)|)}
--- a/doc-src/TutorialI/Types/records.tex Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Types/records.tex Mon Nov 12 10:56:38 2001 +0100
@@ -36,7 +36,7 @@
\isa{point}:
\begin{isabelle}
\isacommand{constdefs}\ \ \ pt1\ ::\ point\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ "pt1\ ==\ (|\ Xcoord\ =\ \#999,\ Ycoord\ =\ \#23\ |)"
+\ \ \ \ \ \ \ \ \ \ \ \ "pt1\ ==\ (|\ Xcoord\ =\ 999,\ Ycoord\ =\ 23\ |)"
\end{isabelle}
We see above the ASCII notation for record brackets. You can also use
the symbolic brackets \isa{\isasymlparr} and \isa{\isasymrparr}.
@@ -45,7 +45,7 @@
\begin{isabelle}
\isacommand{constdefs}\ \ \ pt2\ ::\ "(|\ Xcoord\ ::\ int,\ Ycoord\ ::\ int\
|)"\ \isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ "pt2\ ==\ (|\ Xcoord\ =\ \#-45,\ Ycoord\ =\ \#97\ |)"
+\ \ \ \ \ \ \ \ \ \ \ \ "pt2\ ==\ (|\ Xcoord\ =\ -45,\ Ycoord\ =\ 97\ |)"
\end{isabelle}
For each field, there is a \emph{selector} function of the same name. For
@@ -57,12 +57,12 @@
\isacommand{by}\ simp
\end{isabelle}
The \emph{update} operation is functional. For example,
-\isa{p\isasymlparr Xcoord:=\#0\isasymrparr} is a record whose \isa{Xcoord} value
+\isa{p\isasymlparr Xcoord:=0\isasymrparr} is a record whose \isa{Xcoord} value
is zero and whose
\isa{Ycoord} value is copied from~\isa{p}. Updates are also simplified
automatically:
\begin{isabelle}
-\isacommand{lemma}\ "(|\ Xcoord\ =\ a,\ Ycoord\ =\ b\ |)\ (|\ Xcoord:=\ \#0\ |)\
+\isacommand{lemma}\ "(|\ Xcoord\ =\ a,\ Ycoord\ =\ b\ |)\ (|\ Xcoord:=\ 0\ |)\
=\isanewline
\ \ \ \ \ \ \ \ (|\ Xcoord\ =\ 0,\ Ycoord\ =\ b\ |)"\isanewline
\isacommand{by}\ simp
@@ -94,7 +94,7 @@
order:
\begin{isabelle}
\isacommand{constdefs}\ \ \ cpt1\ ::\ cpoint\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ "cpt1\ ==\ (|\ Xcoord\ =\ \#999,\ Ycoord\ =\ \#23,\ col\
+\ \ \ \ \ \ \ \ \ \ \ \ "cpt1\ ==\ (|\ Xcoord\ =\ 999,\ Ycoord\ =\ 23,\ col\
=\ Green\ |)"
\end{isabelle}
@@ -141,14 +141,11 @@
comprises all possible extensions to those two fields. For example,
let us define two operations --- methods, if we regard records as
objects --- to get and set any point's
-\isa{Xcoord} field. The sort constraint in \isa{'a::more} is
-required, since all extensions must belong to the type class
-\isa{more}.%
-\REMARK{Why, and what does this imply in practice?}
+\isa{Xcoord} field.
\begin{isabelle}
-\ \ getX\ ::\ "('a::more)\ point_scheme\ \isasymRightarrow \ int"\isanewline
+\ \ getX\ ::\ "'a\ point_scheme\ \isasymRightarrow \ int"\isanewline
\ \ \ "getX\ r\ ==\ Xcoord\ r"\isanewline
-\ \ setX\ ::\ "[('a::more)\ point_scheme,\ int]\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
+\ \ setX\ ::\ "['a\ point_scheme,\ int]\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
\ \ \ "setX\ r\ a\ ==\ r\ (|\ Xcoord\ :=\ a\ |)"
\end{isabelle}
@@ -158,9 +155,8 @@
extensions, such as \isa{cpoint}:
\begin{isabelle}
\isacommand{constdefs}\isanewline
-\ \ incX\ ::\ "('a::more)\ point_scheme\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
-\ \ "incX\ r\ ==\ \isasymlparr Xcoord\ =\ (Xcoord\ r)\ +\
-\#1,\isanewline
+\ \ incX\ ::\ "'a\ point_scheme\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
+\ \ "incX\ r\ ==\ \isasymlparr Xcoord\ =\ (Xcoord\ r)\ +\ 1,\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ Ycoord\ =\ Ycoord\ r,\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymdots \ =\ point.more\
r\isasymrparr"
@@ -169,7 +165,7 @@
Generic theorems can be proved about generic methods. This trivial
lemma relates \isa{incX} to \isa{getX} and \isa{setX}:
\begin{isabelle}
-\isacommand{lemma}\ "incX\ r\ =\ setX\ r\ ((getX\ r)\ +\ \#1)"\isanewline
+\isacommand{lemma}\ "incX\ r\ =\ setX\ r\ ((getX\ r)\ +\ 1)"\isanewline
\isacommand{by}\ (simp\ add:\ getX_def\ setX_def\ incX_def)
\end{isabelle}