new-style numerals without leading #, along with generic 0 and 1
authorpaulson
Mon Nov 12 10:56:38 2001 +0100 (2001-11-12)
changeset 12156d2758965362e
parent 12155 13c5469b4bb3
child 12157 59307bf77215
new-style numerals without leading #, along with generic 0 and 1
doc-src/TutorialI/Inductive/Advanced.thy
doc-src/TutorialI/Inductive/document/Advanced.tex
doc-src/TutorialI/Rules/Forward.thy
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/Types/Numbers.thy
doc-src/TutorialI/Types/Records.thy
doc-src/TutorialI/Types/document/Numbers.tex
doc-src/TutorialI/Types/numerics.tex
doc-src/TutorialI/Types/records.tex
     1.1 --- a/doc-src/TutorialI/Inductive/Advanced.thy	Mon Nov 12 10:44:55 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/Advanced.thy	Mon Nov 12 10:56:38 2001 +0100
     1.3 @@ -76,6 +76,7 @@
     1.4  by (blast intro!: mono_Int monoI gterms_mono)
     1.5  
     1.6  
     1.7 +text{*the following declaration isn't actually used*}
     1.8  consts integer_arity :: "integer_op \<Rightarrow> nat"
     1.9  primrec
    1.10  "integer_arity (Number n)        = 0"
     2.1 --- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Nov 12 10:44:55 2001 +0100
     2.2 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Nov 12 10:56:38 2001 +0100
     2.3 @@ -112,10 +112,12 @@
     2.4  \isacommand{lemma}\ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
     2.5  \ \ \ \ \ {\isachardoublequote}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequote}\isanewline
     2.6  \isamarkupfalse%
     2.7 -\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isanewline
     2.8 -\isanewline
     2.9 -\isanewline
    2.10 -\isamarkupfalse%
    2.11 +\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isamarkupfalse%
    2.12 +%
    2.13 +\begin{isamarkuptext}%
    2.14 +the following declaration isn't actually used%
    2.15 +\end{isamarkuptext}%
    2.16 +\isamarkuptrue%
    2.17  \isacommand{consts}\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    2.18  \isamarkupfalse%
    2.19  \isacommand{primrec}\isanewline
     3.1 --- a/doc-src/TutorialI/Rules/Forward.thy	Mon Nov 12 10:44:55 2001 +0100
     3.2 +++ b/doc-src/TutorialI/Rules/Forward.thy	Mon Nov 12 10:56:38 2001 +0100
     3.3 @@ -33,15 +33,6 @@
     3.4  as far as HERE.
     3.5  *}
     3.6  
     3.7 -
     3.8 -text {*
     3.9 -@{thm[display] gcd_1}
    3.10 -\rulename{gcd_1}
    3.11 -
    3.12 -@{thm[display] gcd_1_left}
    3.13 -\rulename{gcd_1_left}
    3.14 -*};
    3.15 -
    3.16  text{*\noindent
    3.17  SKIP THIS PROOF
    3.18  *}
     4.1 --- a/doc-src/TutorialI/Rules/rules.tex	Mon Nov 12 10:44:55 2001 +0100
     4.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Mon Nov 12 10:56:38 2001 +0100
     4.3 @@ -1818,7 +1818,7 @@
     4.4  appearance from left to right.  In this case, the variables  are \isa{?k}, \isa{?m}
     4.5  and~\isa{?n}. So, the expression
     4.6  \hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m}
     4.7 -by~\isa{1}.\REMARK{which 1 do we use?? (right the way down)}
     4.8 +by~\isa{1}.
     4.9  \begin{isabelle}
    4.10  \isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1]
    4.11  \end{isabelle}
    4.12 @@ -1890,8 +1890,7 @@
    4.13  \end{isabelle}
    4.14  %
    4.15  Normally we would never name the intermediate theorems
    4.16 -such as \isa{gcd_mult_0} and
    4.17 -\isa{gcd_mult_1} but would combine
    4.18 +such as \isa{gcd_mult_0} and \isa{gcd_mult_1} but would combine
    4.19  the three forward steps: 
    4.20  \begin{isabelle}
    4.21  \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]%
    4.22 @@ -1959,7 +1958,7 @@
    4.23  First, we
    4.24  prove an instance of its first premise:
    4.25  \begin{isabelle}
    4.26 -\isacommand{lemma}\ relprime_20_81:\ "gcd(\#20,\#81)\ =\ 1"\isanewline
    4.27 +\isacommand{lemma}\ relprime_20_81:\ "gcd(20,81)\ =\ 1"\isanewline
    4.28  \isacommand{by}\ (simp\ add:\ gcd.simps)
    4.29  \end{isabelle}
    4.30  We have evaluated an application of the \isa{gcd} function by
    4.31 @@ -1973,7 +1972,7 @@
    4.32  \end{isabelle}
    4.33  yields the theorem
    4.34  \begin{isabelle}
    4.35 -\ \ \ \ \ \#20\ dvd\ (?m\ *\ \#81)\ \isasymLongrightarrow\ \#20\ dvd\ ?m%
    4.36 +\ \ \ \ \ 20\ dvd\ (?m\ *\ 81)\ \isasymLongrightarrow\ 20\ dvd\ ?m%
    4.37  \end{isabelle}
    4.38  %
    4.39  \isa{OF} takes any number of operands.  Consider 
    4.40 @@ -2048,10 +2047,10 @@
    4.41  
    4.42  For example, let us prove a fact about divisibility in the natural numbers:
    4.43  \begin{isabelle}
    4.44 -\isacommand{lemma}\ "\#2\ \isasymle \ u\ \isasymLongrightarrow \ u*m\ \isasymnoteq
    4.45 +\isacommand{lemma}\ "2\ \isasymle \ u\ \isasymLongrightarrow \ u*m\ \isasymnoteq
    4.46  \ Suc(u*n)"\isanewline
    4.47  \isacommand{apply}\ intro\isanewline
    4.48 -\ 1.\ \isasymlbrakk \#2\ \isasymle \ u;\ u\ *\ m\ =\ Suc\ (u\ *\ n)\isasymrbrakk \ \isasymLongrightarrow \ False%
    4.49 +\ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ =\ Suc\ (u\ *\ n)\isasymrbrakk \ \isasymLongrightarrow \ False%
    4.50  \end{isabelle}
    4.51  %
    4.52  The key step is to apply the function \ldots\isa{mod\ u} to both sides of the
    4.53 @@ -2060,7 +2059,7 @@
    4.54  \begin{isabelle}
    4.55  \isacommand{apply}\ (drule_tac\ f="\isasymlambda x.\ x\ mod\ u"\ \isakeyword{in}\
    4.56  arg_cong)\isanewline
    4.57 -\ 1.\ \isasymlbrakk \#2\ \isasymle \ u;\ u\ *\ m\ mod\ u\ =\ Suc\ (u\ *\ n)\ mod\
    4.58 +\ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ mod\ u\ =\ Suc\ (u\ *\ n)\ mod\
    4.59  u\isasymrbrakk \ \isasymLongrightarrow \ False
    4.60  \end{isabelle}
    4.61  %
    4.62 @@ -2175,13 +2174,13 @@
    4.63  
    4.64  Look at the following example. 
    4.65  \begin{isabelle}
    4.66 -\isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ \#37;\ \#66\ <\ \#2*z;\ z*z\
    4.67 -\isasymnoteq\ \#1225;\ Q(\#34);\ Q(\#36)\isasymrbrakk\isanewline
    4.68 +\isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ 37;\ 66\ <\ 2*z;\ z*z\
    4.69 +\isasymnoteq\ 1225;\ Q(34);\ Q(36)\isasymrbrakk\isanewline
    4.70  \ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ Q(z)"\isanewline
    4.71 -\isacommand{apply}\ (subgoal_tac\ "z\ =\ \#34\ \isasymor\ z\ =\
    4.72 -\#36")\isanewline
    4.73 +\isacommand{apply}\ (subgoal_tac\ "z\ =\ 34\ \isasymor\ z\ =\
    4.74 +36")\isanewline
    4.75  \isacommand{apply}\ blast\isanewline
    4.76 -\isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ \#35")\isanewline
    4.77 +\isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ 35")\isanewline
    4.78  \isacommand{apply}\ arith\isanewline
    4.79  \isacommand{apply}\ force\isanewline
    4.80  \isacommand{done}
    4.81 @@ -2196,25 +2195,25 @@
    4.82  step is to claim that \isa{z} is either 34 or 36. The resulting proof 
    4.83  state gives us two subgoals: 
    4.84  \begin{isabelle}
    4.85 -%\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\
    4.86 -%Q\ \#34;\ Q\ \#36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline
    4.87 -\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
    4.88 -\ \ \ \ \ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isasymrbrakk\isanewline
    4.89 +%\isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\
    4.90 +%Q\ 34;\ Q\ 36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline
    4.91 +\ 1.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36;\isanewline
    4.92 +\ \ \ \ \ z\ =\ 34\ \isasymor\ z\ =\ 36\isasymrbrakk\isanewline
    4.93  \ \ \ \ \isasymLongrightarrow\ Q\ z\isanewline
    4.94 -\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
    4.95 -\ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36
    4.96 +\ 2.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36\isasymrbrakk\isanewline
    4.97 +\ \ \ \ \isasymLongrightarrow\ z\ =\ 34\ \isasymor\ z\ =\ 36
    4.98  \end{isabelle}
    4.99  The first subgoal is trivial (\isa{blast}), but for the second Isabelle needs help to eliminate
   4.100  the case
   4.101  \isa{z}=35.  The second invocation  of {\isa{subgoal_tac}} leaves two
   4.102  subgoals: 
   4.103  \begin{isabelle}
   4.104 -\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\
   4.105 -\#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
   4.106 -\ \ \ \ \ z\ \isasymnoteq\ \#35\isasymrbrakk\isanewline
   4.107 -\ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isanewline
   4.108 -\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
   4.109 -\ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35
   4.110 +\ 1.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\
   4.111 +1225;\ Q\ 34;\ Q\ 36;\isanewline
   4.112 +\ \ \ \ \ z\ \isasymnoteq\ 35\isasymrbrakk\isanewline
   4.113 +\ \ \ \ \isasymLongrightarrow\ z\ =\ 34\ \isasymor\ z\ =\ 36\isanewline
   4.114 +\ 2.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36\isasymrbrakk\isanewline
   4.115 +\ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ 35
   4.116  \end{isabelle}
   4.117  
   4.118  Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic
   4.119 @@ -2286,8 +2285,8 @@
   4.120  implications in which most of the antecedents are proved by assumption, but one is
   4.121  proved by arithmetic:
   4.122  \begin{isabelle}
   4.123 -\isacommand{lemma}\ "\isasymlbrakk Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ x<\#5\isasymlongrightarrow P;\
   4.124 -Suc\ x\ <\ \#5\isasymrbrakk \ \isasymLongrightarrow \ R"\ \isanewline
   4.125 +\isacommand{lemma}\ "\isasymlbrakk Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ x<5\isasymlongrightarrow P;\
   4.126 +Suc\ x\ <\ 5\isasymrbrakk \ \isasymLongrightarrow \ R"\ \isanewline
   4.127  \isacommand{by}\ (drule\ mp,\ (assumption|arith))+
   4.128  \end{isabelle}
   4.129  The \isa{arith}
     5.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Mon Nov 12 10:44:55 2001 +0100
     5.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Mon Nov 12 10:56:38 2001 +0100
     5.3 @@ -83,8 +83,15 @@
     5.4  *}
     5.5  
     5.6  
     5.7 +lemma "(n - 1) * (n + 1) = n * n - (1::nat)"
     5.8 +apply (clarsimp split: nat_diff_split)
     5.9 + --{* @{subgoals[display,indent=0,margin=65]} *}
    5.10 +apply (subgoal_tac "n=0", force, arith)
    5.11 +done
    5.12 +
    5.13 +
    5.14  lemma "(n - 2) * (n + 2) = n * n - (4::nat)"
    5.15 -apply (clarsimp split: nat_diff_split)
    5.16 +apply (simp split: nat_diff_split, clarify)
    5.17   --{* @{subgoals[display,indent=0,margin=65]} *}
    5.18  apply (subgoal_tac "n=0 | n=1", force, arith)
    5.19  done
     6.1 --- a/doc-src/TutorialI/Types/Records.thy	Mon Nov 12 10:44:55 2001 +0100
     6.2 +++ b/doc-src/TutorialI/Types/Records.thy	Mon Nov 12 10:56:38 2001 +0100
     6.3 @@ -112,7 +112,6 @@
     6.4    @{text [display]
     6.5  "    point = (| Xcoord :: int, Ycoord :: int |)
     6.6      'a point_scheme = (| Xcoord :: int, Ycoord :: int, ... :: 'a |)"}
     6.7 -  Extensions `...' must be in type class @{text more}.
     6.8  *}
     6.9  
    6.10  constdefs
     7.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Mon Nov 12 10:44:55 2001 +0100
     7.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Mon Nov 12 10:56:38 2001 +0100
     7.3 @@ -130,9 +130,25 @@
     7.4  \rulename{nat_diff_split}%
     7.5  \end{isamarkuptext}%
     7.6  \isamarkuptrue%
     7.7 +\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
     7.8 +\isamarkupfalse%
     7.9 +\isacommand{apply}\ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
    7.10 +\ %
    7.11 +\isamarkupcmt{\begin{isabelle}%
    7.12 +\ {\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}}%
    7.13 +\end{isabelle}%
    7.14 +}
    7.15 +\isanewline
    7.16 +\isamarkupfalse%
    7.17 +\isacommand{apply}\ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}n{\isacharequal}{\isadigit{0}}{\isachardoublequote}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline
    7.18 +\isamarkupfalse%
    7.19 +\isacommand{done}\isanewline
    7.20 +\isanewline
    7.21 +\isanewline
    7.22 +\isamarkupfalse%
    7.23  \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
    7.24  \isamarkupfalse%
    7.25 -\isacommand{apply}\ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
    7.26 +\isacommand{apply}\ {\isacharparenleft}simp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharcomma}\ clarify{\isacharparenright}\isanewline
    7.27  \ %
    7.28  \isamarkupcmt{\begin{isabelle}%
    7.29  \ {\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}}%
     8.1 --- a/doc-src/TutorialI/Types/numerics.tex	Mon Nov 12 10:44:55 2001 +0100
     8.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Mon Nov 12 10:56:38 2001 +0100
     8.3 @@ -41,15 +41,15 @@
     8.4  \label{sec:numerals}
     8.5  
     8.6  \index{numeric literals|(}%
     8.7 -Literals are available for the types of natural numbers, integers 
     8.8 -and reals and denote integer values of arbitrary size. 
     8.9 -They begin 
    8.10 -with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and 
    8.11 -then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3} 
    8.12 -and \isa{\#441223334678}.\REMARK{will need updating?}
    8.13 +The constants \cdx{0} and \cdx{1} are overloaded.  They denote zero and one,
    8.14 +respectively, for all numeric types.  Other values are expressed by numeric
    8.15 +literals, which consist of one or more decimal digits optionally preceeded by
    8.16 +a minus sign (\isa{-}).  Examples are \isa{2}, \isa{-3} and
    8.17 +\isa{441223334678}.  Literals are available for the types of natural numbers,
    8.18 +integers and reals; they denote integer values of arbitrary size.
    8.19  
    8.20  Literals look like constants, but they abbreviate 
    8.21 -terms, representing the number in a two's complement binary notation. 
    8.22 +terms representing the number in a two's complement binary notation. 
    8.23  Isabelle performs arithmetic on literals by rewriting rather 
    8.24  than using the hardware arithmetic. In most cases arithmetic 
    8.25  is fast enough, even for large numbers. The arithmetic operations 
    8.26 @@ -64,14 +64,14 @@
    8.27  type constraints.  Here is an example of what can go wrong:
    8.28  \par
    8.29  \begin{isabelle}
    8.30 -\isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"
    8.31 +\isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m"
    8.32  \end{isabelle}
    8.33  %
    8.34  Carefully observe how Isabelle displays the subgoal:
    8.35  \begin{isabelle}
    8.36 -\ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m
    8.37 +\ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m
    8.38  \end{isabelle}
    8.39 -The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric
    8.40 +The type \isa{'a} given for the literal \isa{2} warns us that no numeric
    8.41  type has been specified.  The problem is underspecified.  Given a type
    8.42  constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
    8.43  \end{warn}
    8.44 @@ -83,13 +83,13 @@
    8.45  rejected:
    8.46  \begin{isabelle}
    8.47  \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
    8.48 -"h\ \#3\ =\ \#2"\isanewline
    8.49 +"h\ 3\ =\ 2"\isanewline
    8.50  "h\ i\ \ =\ i"
    8.51  \end{isabelle}
    8.52  
    8.53  You should use a conditional expression instead:
    8.54  \begin{isabelle}
    8.55 -"h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)"
    8.56 +"h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)"
    8.57  \end{isabelle}
    8.58  \index{numeric literals|)}
    8.59  \end{warn}
    8.60 @@ -106,29 +106,30 @@
    8.61  
    8.62  \subsubsection{Literals}
    8.63  \index{numeric literals!for type \protect\isa{nat}}%
    8.64 -The notational options for the natural numbers are confusing.  The 
    8.65 -constant \cdx{0} is overloaded to serve as the neutral value 
    8.66 -in a variety of additive types. The symbols \sdx{1} and \sdx{2} are 
    8.67 -not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},
    8.68 -respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2}  are
    8.69 -syntactically different from \isa{0}, \isa{1} and \isa{2}. You  will\REMARK{will need updating?}
    8.70 -sometimes prefer one notation to the other. Literals are  obviously
    8.71 -necessary to express large values, while \isa{0} and \isa{Suc}  are needed
    8.72 -in order to match many theorems, including the rewrite  rules for primitive
    8.73 -recursive functions. The following default  simplification rules replace
    8.74 +The notational options for the natural  numbers are confusing.  Recall that an
    8.75 +overloaded constant can be defined independently for each type; the definition
    8.76 +of \cdx{1} for type \isa{nat} is
    8.77 +\begin{isabelle}
    8.78 +1\ \isasymequiv\ Suc\ 0
    8.79 +\rulename{One_nat_def}
    8.80 +\end{isabelle}
    8.81 +This is installed as a simplification rule, so the simplifier will replace
    8.82 +every occurrence of \isa{1::nat} by \isa{Suc\ 0}.  Literals are obviously
    8.83 +better than nested \isa{Suc}s at expressing large values.  But many theorems,
    8.84 +including the rewrite rules for primitive recursive functions, can only be
    8.85 +applied to terms of the form \isa{Suc\ $n$}.
    8.86 +
    8.87 +The following default  simplification rules replace
    8.88  small literals by zero and successor: 
    8.89  \begin{isabelle}
    8.90 -\#0\ =\ 0
    8.91 -\rulename{numeral_0_eq_0}\isanewline
    8.92 -\#1\ =\ 1
    8.93 -\rulename{numeral_1_eq_1}\isanewline
    8.94 -\#2\ +\ n\ =\ Suc\ (Suc\ n)
    8.95 +2\ +\ n\ =\ Suc\ (Suc\ n)
    8.96  \rulename{add_2_eq_Suc}\isanewline
    8.97 -n\ +\ \#2\ =\ Suc\ (Suc\ n)
    8.98 +n\ +\ 2\ =\ Suc\ (Suc\ n)
    8.99  \rulename{add_2_eq_Suc'}
   8.100  \end{isabelle}
   8.101 -In special circumstances, you may wish to remove or reorient 
   8.102 -these rules. 
   8.103 +It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and
   8.104 +the simplifier will normally reverse this transformation.  Novices should
   8.105 +express natural numbers using \isa{0} and \isa{Suc} only.
   8.106  
   8.107  \subsubsection{Typical lemmas}
   8.108  Inequalities involving addition and subtraction alone can be proved
   8.109 @@ -225,11 +226,17 @@
   8.110  d))
   8.111  \rulename{nat_diff_split}
   8.112  \end{isabelle}
   8.113 -For example, this splitting proves the following fact, which lies outside the scope of
   8.114 -linear arithmetic:\REMARK{replace by new example!}
   8.115 +For example, splitting helps to prove the following fact:
   8.116  \begin{isabelle}
   8.117 -\isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline
   8.118 -\isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline
   8.119 +\isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline
   8.120 +\isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline
   8.121 +\ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0
   8.122 +\end{isabelle}
   8.123 +The result lies outside the scope of linear arithmetic, but
   8.124 + it is easily found
   8.125 +if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:
   8.126 +\begin{isabelle}
   8.127 +\isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
   8.128  \isacommand{done}
   8.129  \end{isabelle}
   8.130  
   8.131 @@ -313,13 +320,13 @@
   8.132  mathematical practice: the sign of the remainder follows that
   8.133  of the divisor:
   8.134  \begin{isabelle}
   8.135 -\#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b%
   8.136 +0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b%
   8.137  \rulename{pos_mod_sign}\isanewline
   8.138 -\#0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
   8.139 +0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
   8.140  \rulename{pos_mod_bound}\isanewline
   8.141 -b\ <\ \#0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ \#0
   8.142 +b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0
   8.143  \rulename{neg_mod_sign}\isanewline
   8.144 -b\ <\ \#0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
   8.145 +b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
   8.146  \rulename{neg_mod_bound}
   8.147  \end{isabelle}
   8.148  ML treats negative divisors in the same way, but most computer hardware
   8.149 @@ -342,9 +349,9 @@
   8.150  \end{isabelle}
   8.151  
   8.152  \begin{isabelle}
   8.153 -\#0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
   8.154 +0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
   8.155  \rulename{zdiv_zmult2_eq}\isanewline
   8.156 -\#0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
   8.157 +0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
   8.158  c)\ +\ a\ mod\ b%
   8.159  \rulename{zmod_zmult2_eq}
   8.160  \end{isabelle}
   8.161 @@ -426,18 +433,18 @@
   8.162  \isa{int} and only express integral values.  Fractions expressed
   8.163  using the division operator are automatically simplified to lowest terms:
   8.164  \begin{isabelle}
   8.165 -\ 1.\ P\ ((\#3\ /\ \#4)\ *\ (\#8\ /\ \#15))\isanewline
   8.166 +\ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
   8.167  \isacommand{apply} simp\isanewline
   8.168 -\ 1.\ P\ (\#2\ /\ \#5)
   8.169 +\ 1.\ P\ (2\ /\ 5)
   8.170  \end{isabelle}
   8.171  Exponentiation can express floating-point values such as
   8.172 -\isa{\#2 * \#10\isacharcircum\#6}, but at present no special simplification
   8.173 +\isa{2 * 10\isacharcircum6}, but at present no special simplification
   8.174  is performed.
   8.175  
   8.176  
   8.177  \begin{warn}
   8.178  Type \isa{real} is only available in the logic HOL-Real, which
   8.179 -is  HOL extended with the rather substantial development of the real
   8.180 +is  HOL extended with a definitional development of the real
   8.181  numbers.  Base your theory upon theory
   8.182  \thydx{Real}, not the usual \isa{Main}.%
   8.183  \index{real numbers|)}\index{*real (type)|)}
     9.1 --- a/doc-src/TutorialI/Types/records.tex	Mon Nov 12 10:44:55 2001 +0100
     9.2 +++ b/doc-src/TutorialI/Types/records.tex	Mon Nov 12 10:56:38 2001 +0100
     9.3 @@ -36,7 +36,7 @@
     9.4  \isa{point}:
     9.5  \begin{isabelle}
     9.6  \isacommand{constdefs}\ \ \ pt1\ ::\ point\isanewline
     9.7 -\ \ \ \ \ \ \ \ \ \ \ \ "pt1\ ==\ (|\ Xcoord\ =\ \#999,\ Ycoord\ =\ \#23\ |)"
     9.8 +\ \ \ \ \ \ \ \ \ \ \ \ "pt1\ ==\ (|\ Xcoord\ =\ 999,\ Ycoord\ =\ 23\ |)"
     9.9  \end{isabelle}
    9.10  We see above the ASCII notation for record brackets.  You can also use
    9.11  the symbolic brackets \isa{\isasymlparr} and  \isa{\isasymrparr}.
    9.12 @@ -45,7 +45,7 @@
    9.13  \begin{isabelle}
    9.14  \isacommand{constdefs}\ \ \ pt2\ ::\ "(|\ Xcoord\ ::\ int,\ Ycoord\ ::\ int\
    9.15  |)"\ \isanewline
    9.16 -\ \ \ \ \ \ \ \ \ \ \ \ "pt2\ ==\ (|\ Xcoord\ =\ \#-45,\ Ycoord\ =\ \#97\ |)"
    9.17 +\ \ \ \ \ \ \ \ \ \ \ \ "pt2\ ==\ (|\ Xcoord\ =\ -45,\ Ycoord\ =\ 97\ |)"
    9.18  \end{isabelle}
    9.19  
    9.20  For each field, there is a \emph{selector} function of the same name.  For
    9.21 @@ -57,12 +57,12 @@
    9.22  \isacommand{by}\ simp
    9.23  \end{isabelle}
    9.24  The \emph{update} operation is functional.  For example,
    9.25 -\isa{p\isasymlparr Xcoord:=\#0\isasymrparr} is a record whose \isa{Xcoord} value
    9.26 +\isa{p\isasymlparr Xcoord:=0\isasymrparr} is a record whose \isa{Xcoord} value
    9.27  is zero and whose
    9.28  \isa{Ycoord} value is copied from~\isa{p}.  Updates are also simplified
    9.29  automatically:
    9.30  \begin{isabelle}
    9.31 -\isacommand{lemma}\ "(|\ Xcoord\ =\ a,\ Ycoord\ =\ b\ |)\ (|\ Xcoord:=\ \#0\ |)\
    9.32 +\isacommand{lemma}\ "(|\ Xcoord\ =\ a,\ Ycoord\ =\ b\ |)\ (|\ Xcoord:=\ 0\ |)\
    9.33  =\isanewline
    9.34  \ \ \ \ \ \ \ \ (|\ Xcoord\ =\ 0,\ Ycoord\ =\ b\ |)"\isanewline
    9.35  \isacommand{by}\ simp
    9.36 @@ -94,7 +94,7 @@
    9.37  order:
    9.38  \begin{isabelle}
    9.39  \isacommand{constdefs}\ \ \ cpt1\ ::\ cpoint\isanewline
    9.40 -\ \ \ \ \ \ \ \ \ \ \ \ "cpt1\ ==\ (|\ Xcoord\ =\ \#999,\ Ycoord\ =\ \#23,\ col\
    9.41 +\ \ \ \ \ \ \ \ \ \ \ \ "cpt1\ ==\ (|\ Xcoord\ =\ 999,\ Ycoord\ =\ 23,\ col\
    9.42  =\ Green\ |)"
    9.43  \end{isabelle}
    9.44  
    9.45 @@ -141,14 +141,11 @@
    9.46  comprises all possible extensions to those two fields.  For example,
    9.47  let us define two operations --- methods, if we regard records as
    9.48  objects --- to get and set any point's
    9.49 -\isa{Xcoord} field.  The sort constraint in \isa{'a::more} is
    9.50 -required, since all extensions must belong to the type class
    9.51 -\isa{more}.%
    9.52 -\REMARK{Why, and what does this imply in practice?}
    9.53 +\isa{Xcoord} field. 
    9.54  \begin{isabelle}
    9.55 -\ \ getX\ ::\ "('a::more)\ point_scheme\ \isasymRightarrow \ int"\isanewline
    9.56 +\ \ getX\ ::\ "'a\ point_scheme\ \isasymRightarrow \ int"\isanewline
    9.57  \ \ \ "getX\ r\ ==\ Xcoord\ r"\isanewline
    9.58 -\ \ setX\ ::\ "[('a::more)\ point_scheme,\ int]\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
    9.59 +\ \ setX\ ::\ "['a\ point_scheme,\ int]\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
    9.60  \ \ \ "setX\ r\ a\ ==\ r\ (|\ Xcoord\ :=\ a\ |)"
    9.61  \end{isabelle}
    9.62  
    9.63 @@ -158,9 +155,8 @@
    9.64  extensions, such as \isa{cpoint}:
    9.65  \begin{isabelle}
    9.66  \isacommand{constdefs}\isanewline
    9.67 -\ \ incX\ ::\ "('a::more)\ point_scheme\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
    9.68 -\ \ "incX\ r\ ==\ \isasymlparr Xcoord\ =\ (Xcoord\ r)\ +\
    9.69 -\#1,\isanewline
    9.70 +\ \ incX\ ::\ "'a\ point_scheme\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
    9.71 +\ \ "incX\ r\ ==\ \isasymlparr Xcoord\ =\ (Xcoord\ r)\ +\ 1,\isanewline
    9.72  \ \ \ \ \ \ \ \ \ \ \ \ \ \ Ycoord\ =\ Ycoord\ r,\isanewline
    9.73  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymdots \ =\ point.more\
    9.74  r\isasymrparr"
    9.75 @@ -169,7 +165,7 @@
    9.76  Generic theorems can be proved about generic methods.  This trivial
    9.77  lemma relates \isa{incX} to \isa{getX} and \isa{setX}:
    9.78  \begin{isabelle}
    9.79 -\isacommand{lemma}\ "incX\ r\ =\ setX\ r\ ((getX\ r)\ +\ \#1)"\isanewline
    9.80 +\isacommand{lemma}\ "incX\ r\ =\ setX\ r\ ((getX\ r)\ +\ 1)"\isanewline
    9.81  \isacommand{by}\ (simp\ add:\ getX_def\ setX_def\ incX_def)
    9.82  \end{isabelle}
    9.83