1.1 --- a/doc-src/TutorialI/Types/Numbers.thy Thu Feb 19 16:44:21 2004 +0100
1.2 +++ b/doc-src/TutorialI/Types/Numbers.thy Thu Feb 19 17:57:54 2004 +0100
1.3 @@ -60,18 +60,10 @@
1.4 oops
1.5
1.6 text{*
1.7 -@{thm[display] mult_le_mono[no_vars]}
1.8 -\rulename{mult_le_mono}
1.9 -
1.10 -@{thm[display] mult_less_mono1[no_vars]}
1.11 -\rulename{mult_less_mono1}
1.12
1.13 @{thm[display] div_le_mono[no_vars]}
1.14 \rulename{div_le_mono}
1.15
1.16 -@{thm[display] add_mult_distrib[no_vars]}
1.17 -\rulename{add_mult_distrib}
1.18 -
1.19 @{thm[display] diff_mult_distrib[no_vars]}
1.20 \rulename{diff_mult_distrib}
1.21
1.22 @@ -168,9 +160,6 @@
1.23
1.24 @{thm[display] zmod_zmult2_eq[no_vars]}
1.25 \rulename{zmod_zmult2_eq}
1.26 -
1.27 -@{thm[display] abs_mult[no_vars]}
1.28 -\rulename{abs_mult}
1.29 *}
1.30
1.31 lemma "abs (x+y) \<le> abs x + abs (y :: int)"
1.32 @@ -195,14 +184,11 @@
1.33 \rulename{int_less_induct}
1.34 *}
1.35
1.36 -text {*REALS
1.37 +text {*FIELDS
1.38
1.39 @{thm[display] dense[no_vars]}
1.40 \rulename{dense}
1.41
1.42 -@{thm[display] power_abs[no_vars]}
1.43 -\rulename{power_abs}
1.44 -
1.45 @{thm[display] times_divide_eq_right[no_vars]}
1.46 \rulename{times_divide_eq_right}
1.47
1.48 @@ -254,6 +240,59 @@
1.49 apply simp
1.50 oops
1.51
1.52 +text{*
1.53 +Ring and Field
1.54 +
1.55 +Requires a field, or else an ordered ring
1.56 +
1.57 +@{thm[display] mult_eq_0_iff[no_vars]}
1.58 +\rulename{mult_eq_0_iff}
1.59 +
1.60 +@{thm[display] field_mult_eq_0_iff[no_vars]}
1.61 +\rulename{field_mult_eq_0_iff}
1.62 +
1.63 +@{thm[display] mult_cancel_right[no_vars]}
1.64 +\rulename{mult_cancel_right}
1.65 +
1.66 +@{thm[display] field_mult_cancel_right[no_vars]}
1.67 +\rulename{field_mult_cancel_right}
1.68 +*}
1.69 +
1.70 +ML{*set show_sorts*}
1.71 +
1.72 +text{*
1.73 +effect of show sorts on the above
1.74 +
1.75 +@{thm[display] field_mult_cancel_right[no_vars]}
1.76 +\rulename{field_mult_cancel_right}
1.77 +*}
1.78 +
1.79 +ML{*reset show_sorts*}
1.80 +
1.81 +
1.82 +text{*
1.83 +absolute value
1.84 +
1.85 +@{thm[display] abs_mult[no_vars]}
1.86 +\rulename{abs_mult}
1.87 +
1.88 +@{thm[display] abs_le_iff[no_vars]}
1.89 +\rulename{abs_le_iff}
1.90 +
1.91 +@{thm[display] abs_triangle_ineq[no_vars]}
1.92 +\rulename{abs_triangle_ineq}
1.93 +
1.94 +@{thm[display] power_add[no_vars]}
1.95 +\rulename{power_add}
1.96 +
1.97 +@{thm[display] power_mult[no_vars]}
1.98 +\rulename{power_mult}
1.99 +
1.100 +@{thm[display] power_abs[no_vars]}
1.101 +\rulename{power_abs}
1.102 +
1.103 +
1.104 +*}
1.105
1.106
1.107 end
2.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex Thu Feb 19 16:44:21 2004 +0100
2.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Thu Feb 19 17:57:54 2004 +0100
2.3 @@ -95,26 +95,11 @@
2.4 %
2.5 \begin{isamarkuptext}%
2.6 \begin{isabelle}%
2.7 -{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ k\ {\isasymle}\ l{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isasymle}\ j\ {\isacharasterisk}\ l%
2.8 -\end{isabelle}
2.9 -\rulename{mult_le_mono}
2.10 -
2.11 -\begin{isabelle}%
2.12 -{\isasymlbrakk}i\ {\isacharless}\ j{\isacharsemicolon}\ {\isadigit{0}}\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharasterisk}\ k\ {\isacharless}\ j\ {\isacharasterisk}\ k%
2.13 -\end{isabelle}
2.14 -\rulename{mult_less_mono1}
2.15 -
2.16 -\begin{isabelle}%
2.17 m\ {\isasymle}\ n\ {\isasymLongrightarrow}\ m\ div\ k\ {\isasymle}\ n\ div\ k%
2.18 \end{isabelle}
2.19 \rulename{div_le_mono}
2.20
2.21 \begin{isabelle}%
2.22 -{\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ {\isacharplus}\ n\ {\isacharasterisk}\ k%
2.23 -\end{isabelle}
2.24 -\rulename{add_mult_distrib}
2.25 -
2.26 -\begin{isabelle}%
2.27 {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ {\isacharminus}\ n\ {\isacharasterisk}\ k%
2.28 \end{isabelle}
2.29 \rulename{diff_mult_distrib}
2.30 @@ -274,12 +259,7 @@
2.31 \begin{isabelle}%
2.32 {\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%
2.33 \end{isabelle}
2.34 -\rulename{zmod_zmult2_eq}
2.35 -
2.36 -\begin{isabelle}%
2.37 -{\isasymbar}a\ {\isacharasterisk}\ b{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}b{\isasymbar}%
2.38 -\end{isabelle}
2.39 -\rulename{abs_mult}%
2.40 +\rulename{zmod_zmult2_eq}%
2.41 \end{isamarkuptext}%
2.42 \isamarkuptrue%
2.43 \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}x{\isacharplus}y{\isacharparenright}\ {\isasymle}\ abs\ x\ {\isacharplus}\ abs\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline
2.44 @@ -317,7 +297,7 @@
2.45 \isamarkuptrue%
2.46 %
2.47 \begin{isamarkuptext}%
2.48 -REALS
2.49 +FIELDS
2.50
2.51 \begin{isabelle}%
2.52 a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b%
2.53 @@ -325,11 +305,6 @@
2.54 \rulename{dense}
2.55
2.56 \begin{isabelle}%
2.57 -{\isasymbar}a\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharcircum}\ n%
2.58 -\end{isabelle}
2.59 -\rulename{power_abs}
2.60 -
2.61 -\begin{isabelle}%
2.62 a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c%
2.63 \end{isabelle}
2.64 \rulename{times_divide_eq_right}
2.65 @@ -414,11 +389,82 @@
2.66 \isamarkupfalse%
2.67 \isacommand{apply}\ simp\ \isanewline
2.68 \isamarkupfalse%
2.69 -\isacommand{oops}\isanewline
2.70 -\isanewline
2.71 -\isanewline
2.72 -\isanewline
2.73 -\isamarkupfalse%
2.74 +\isacommand{oops}\isamarkupfalse%
2.75 +%
2.76 +\begin{isamarkuptext}%
2.77 +Ring and Field
2.78 +
2.79 +Requires a field, or else an ordered ring
2.80 +
2.81 +\begin{isabelle}%
2.82 +{\isacharparenleft}a\ {\isacharasterisk}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}%
2.83 +\end{isabelle}
2.84 +\rulename{mult_eq_0_iff}
2.85 +
2.86 +\begin{isabelle}%
2.87 +{\isacharparenleft}a\ {\isacharasterisk}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}%
2.88 +\end{isabelle}
2.89 +\rulename{field_mult_eq_0_iff}
2.90 +
2.91 +\begin{isabelle}%
2.92 +{\isacharparenleft}a\ {\isacharasterisk}\ c\ {\isacharequal}\ b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
2.93 +\end{isabelle}
2.94 +\rulename{mult_cancel_right}
2.95 +
2.96 +\begin{isabelle}%
2.97 +{\isacharparenleft}a\ {\isacharasterisk}\ c\ {\isacharequal}\ b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
2.98 +\end{isabelle}
2.99 +\rulename{field_mult_cancel_right}%
2.100 +\end{isamarkuptext}%
2.101 +\isamarkuptrue%
2.102 +\isacommand{ML}{\isacharbraceleft}{\isacharasterisk}set\ show{\isacharunderscore}sorts{\isacharasterisk}{\isacharbraceright}\isamarkupfalse%
2.103 +%
2.104 +\begin{isamarkuptext}%
2.105 +effect of show sorts on the above
2.106 +
2.107 +\begin{isabelle}%
2.108 +{\isacharparenleft}{\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}field{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}field{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}field{\isacharparenright}\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\isanewline
2.109 +{\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}field{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
2.110 +\end{isabelle}
2.111 +\rulename{field_mult_cancel_right}%
2.112 +\end{isamarkuptext}%
2.113 +\isamarkuptrue%
2.114 +\isacommand{ML}{\isacharbraceleft}{\isacharasterisk}reset\ show{\isacharunderscore}sorts{\isacharasterisk}{\isacharbraceright}\isamarkupfalse%
2.115 +%
2.116 +\begin{isamarkuptext}%
2.117 +absolute value
2.118 +
2.119 +\begin{isabelle}%
2.120 +{\isasymbar}a\ {\isacharasterisk}\ b{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}b{\isasymbar}%
2.121 +\end{isabelle}
2.122 +\rulename{abs_mult}
2.123 +
2.124 +\begin{isabelle}%
2.125 +{\isacharparenleft}{\isasymbar}a{\isasymbar}\ {\isasymle}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isasymle}\ b\ {\isasymand}\ {\isacharminus}\ a\ {\isasymle}\ b{\isacharparenright}%
2.126 +\end{isabelle}
2.127 +\rulename{abs_le_iff}
2.128 +
2.129 +\begin{isabelle}%
2.130 +{\isasymbar}a\ {\isacharplus}\ b{\isasymbar}\ {\isasymle}\ {\isasymbar}a{\isasymbar}\ {\isacharplus}\ {\isasymbar}b{\isasymbar}%
2.131 +\end{isabelle}
2.132 +\rulename{abs_triangle_ineq}
2.133 +
2.134 +\begin{isabelle}%
2.135 +a\ {\isacharcircum}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}\ {\isacharequal}\ a\ {\isacharcircum}\ m\ {\isacharasterisk}\ a\ {\isacharcircum}\ n%
2.136 +\end{isabelle}
2.137 +\rulename{power_add}
2.138 +
2.139 +\begin{isabelle}%
2.140 +a\ {\isacharcircum}\ {\isacharparenleft}m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharcircum}\ m{\isacharparenright}\ {\isacharcircum}\ n%
2.141 +\end{isabelle}
2.142 +\rulename{power_mult}
2.143 +
2.144 +\begin{isabelle}%
2.145 +{\isasymbar}a\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharcircum}\ n%
2.146 +\end{isabelle}
2.147 +\rulename{power_abs}%
2.148 +\end{isamarkuptext}%
2.149 +\isamarkuptrue%
2.150 \isacommand{end}\isanewline
2.151 \isamarkupfalse%
2.152 \end{isabellebody}%
3.1 --- a/doc-src/TutorialI/Types/numerics.tex Thu Feb 19 16:44:21 2004 +0100
3.2 +++ b/doc-src/TutorialI/Types/numerics.tex Thu Feb 19 17:57:54 2004 +0100
3.3 @@ -10,16 +10,19 @@
3.4 zero and successor, so it works well with inductive proofs and primitive
3.5 recursive function definitions. HOL also provides the type
3.6 \isa{int} of \textbf{integers}, which lack induction but support true
3.7 -subtraction. The integers are preferable to the natural numbers for reasoning about
3.8 -complicated arithmetic expressions, even for some expressions whose
3.9 -value is non-negative. The logic HOL-Complex also has the types
3.10 -\isa{real} and \isa{complex}: the real and complex numbers. Isabelle has no
3.11 +subtraction. With subtraction, arithmetic reasoning is easier, which makes
3.12 +the integers preferable to the natural numbers for
3.13 +complicated arithmetic expressions, even if they are non-negative. The logic HOL-Complex also has the types
3.14 +\isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers. Isabelle has no
3.15 subtyping, so the numeric
3.16 types are distinct and there are functions to convert between them.
3.17 -Fortunately most numeric operations are overloaded: the same symbol can be
3.18 +Most numeric operations are overloaded: the same symbol can be
3.19 used at all numeric types. Table~\ref{tab:overloading} in the appendix
3.20 shows the most important operations, together with the priorities of the
3.21 -infix symbols.
3.22 +infix symbols. Algebraic properties are organized using type classes
3.23 +around algebraic concepts such as rings and fields;
3.24 +a property such as the commutativity of addition is a single theorem
3.25 +(\isa{add_commute}) that applies to all numeric types.
3.26
3.27 \index{linear arithmetic}%
3.28 Many theorems involving numeric types can be proved automatically by
3.29 @@ -29,8 +32,7 @@
3.30 are regarded as variables. The procedure can be slow, especially if the
3.31 subgoal to be proved involves subtraction over type \isa{nat}, which
3.32 causes case splits. On types \isa{nat} and \isa{int}, \methdx{arith}
3.33 -can deal with quantifiers (this is known as ``Presburger Arithmetic''),
3.34 -whereas on type \isa{real} it cannot.
3.35 +can deal with quantifiers---this is known as Presburger arithmetic---whereas on type \isa{real} it cannot.
3.36
3.37 The simplifier reduces arithmetic expressions in other
3.38 ways, such as dividing through by common factors. For problems that lie
3.39 @@ -46,16 +48,13 @@
3.40 \index{numeric literals|(}%
3.41 The constants \cdx{0} and \cdx{1} are overloaded. They denote zero and one,
3.42 respectively, for all numeric types. Other values are expressed by numeric
3.43 -literals, which consist of one or more decimal digits optionally preceeded by
3.44 -a minus sign (\isa{-}). Examples are \isa{2}, \isa{-3} and
3.45 -\isa{441223334678}. Literals are available for the types of natural numbers,
3.46 -integers and reals; they denote integer values of arbitrary size.
3.47 +literals, which consist of one or more decimal digits optionally preceeded by a minus sign (\isa{-}). Examples are \isa{2}, \isa{-3} and
3.48 \isa{441223334678}. Literals are available for the types of natural
3.49 numbers, integers, rationals, reals, etc.; they denote integer values of
3.50 arbitrary size.
3.51
3.52 Literals look like constants, but they abbreviate
3.53 terms representing the number in a two's complement binary notation.
3.54 Isabelle performs arithmetic on literals by rewriting rather
3.55 than using the hardware arithmetic. In most cases arithmetic
3.56 -is fast enough, even for large numbers. The arithmetic operations
3.57 +is fast enough, even for numbers in the millions. The arithmetic operations
3.58 provided for literals include addition, subtraction, multiplication,
3.59 integer division and remainder. Fractions of literals (expressed using
3.60 division) are reduced to lowest terms.
3.61 @@ -98,14 +97,14 @@
3.62 \end{warn}
3.63
3.64
3.65 -
3.66 \subsection{The Type of Natural Numbers, {\tt\slshape nat}}
3.67
3.68 \index{natural numbers|(}\index{*nat (type)|(}%
3.69 This type requires no introduction: we have been using it from the
3.70 beginning. Hundreds of theorems about the natural numbers are
3.71 -proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}. Only
3.72 -in exceptional circumstances should you resort to induction.
3.73 +proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}.
3.74 +Basic properties of addition and multiplication are available through the
3.75 +axiomatic type class for semirings (\S\ref{sec:numeric-axclasses}).
3.76
3.77 \subsubsection{Literals}
3.78 \index{numeric literals!for type \protect\isa{nat}}%
3.79 @@ -134,30 +133,6 @@
3.80 the simplifier will normally reverse this transformation. Novices should
3.81 express natural numbers using \isa{0} and \isa{Suc} only.
3.82
3.83 -\subsubsection{Typical lemmas}
3.84 -Inequalities involving addition and subtraction alone can be proved
3.85 -automatically. Lemmas such as these can be used to prove inequalities
3.86 -involving multiplication and division:
3.87 -\begin{isabelle}
3.88 -\isasymlbrakk i\ \isasymle \ j;\ k\ \isasymle \ l\isasymrbrakk \ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ l%
3.89 -\rulename{mult_le_mono}\isanewline
3.90 -\isasymlbrakk i\ <\ j;\ 0\ <\ k\isasymrbrakk \ \isasymLongrightarrow \ i\
3.91 -*\ k\ <\ j\ *\ k%
3.92 -\rulename{mult_less_mono1}\isanewline
3.93 -m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
3.94 -\rulename{div_le_mono}
3.95 -\end{isabelle}
3.96 -%
3.97 -Various distributive laws concerning multiplication are available:
3.98 -\begin{isabelle}
3.99 -(m\ +\ n)\ *\ k\ =\ m\ *\ k\ +\ n\ *\ k%
3.100 -\rulenamedx{add_mult_distrib}\isanewline
3.101 -(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
3.102 -\rulenamedx{diff_mult_distrib}\isanewline
3.103 -(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
3.104 -\rulenamedx{mod_mult_distrib}
3.105 -\end{isabelle}
3.106 -
3.107 \subsubsection{Division}
3.108 \index{division!for type \protect\isa{nat}}%
3.109 The infix operators \isa{div} and \isa{mod} are overloaded.
3.110 @@ -182,7 +157,11 @@
3.111 a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
3.112 \rulename{mod_mult2_eq}\isanewline
3.113 0\ <\ c\ \isasymLongrightarrow \ (c\ *\ a)\ div\ (c\ *\ b)\ =\ a\ div\ b%
3.114 -\rulename{div_mult_mult1}
3.115 +\rulename{div_mult_mult1}\isanewline
3.116 +(m\ mod\ n)\ *\ k\ =\ (m\ *\ k)\ mod\ (n\ *\ k)
3.117 +\rulenamedx{mod_mult_distrib}\isanewline
3.118 +m\ \isasymle \ n\ \isasymLongrightarrow \ m\ div\ k\ \isasymle \ n\ div\ k%
3.119 +\rulename{div_le_mono}
3.120 \end{isabelle}
3.121
3.122 Surprisingly few of these results depend upon the
3.123 @@ -196,8 +175,7 @@
3.124 a\ mod\ 0\ =\ a%
3.125 \rulename{DIVISION_BY_ZERO_MOD}
3.126 \end{isabelle}
3.127 -As a concession to convention, these equations are not installed as default
3.128 -simplification rules. In \isa{div_mult_mult1} above, one of
3.129 +In \isa{div_mult_mult1} above, one of
3.130 the two divisors (namely~\isa{c}) must still be nonzero.
3.131
3.132 The \textbf{divides} relation\index{divides relation}
3.133 @@ -217,19 +195,26 @@
3.134 \rulenamedx{dvd_add}
3.135 \end{isabelle}
3.136
3.137 -\subsubsection{Simplifier Tricks}
3.138 -The rule \isa{diff_mult_distrib} shown above is one of the few facts
3.139 +\subsubsection{Subtraction}
3.140 +
3.141 +There are no negative natural numbers, so \isa{m\ -\ n} equals zero unless
3.142 +\isa{m} exceeds~\isa{n}. The following is one of the few facts
3.143 about \isa{m\ -\ n} that is not subject to
3.144 -the condition \isa{n\ \isasymle \ m}. Natural number subtraction has few
3.145 +the condition \isa{n\ \isasymle \ m}.
3.146 +\begin{isabelle}
3.147 +(m\ -\ n)\ *\ k\ =\ m\ *\ k\ -\ n\ *\ k%
3.148 +\rulenamedx{diff_mult_distrib}
3.149 +\end{isabelle}
3.150 +Natural number subtraction has few
3.151 nice properties; often you should remove it by simplifying with this split
3.152 -rule:
3.153 +rule.
3.154 \begin{isabelle}
3.155 P(a-b)\ =\ ((a<b\ \isasymlongrightarrow \ P\
3.156 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
3.157 d))
3.158 \rulename{nat_diff_split}
3.159 \end{isabelle}
3.160 -For example, splitting helps to prove the following fact:
3.161 +For example, splitting helps to prove the following fact.
3.162 \begin{isabelle}
3.163 \isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline
3.164 \isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline
3.165 @@ -241,66 +226,18 @@
3.166 \begin{isabelle}
3.167 \isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
3.168 \isacommand{done}
3.169 -\end{isabelle}
3.170 -
3.171 -Suppose that two expressions are equal, differing only in
3.172 -associativity and commutativity of addition. Simplifying with the
3.173 -following equations sorts the terms and groups them to the right, making
3.174 -the two expressions identical:
3.175 -\begin{isabelle}
3.176 -m\ +\ n\ +\ k\ =\ m\ +\ (n\ +\ k)
3.177 -\rulenamedx{add_assoc}\isanewline
3.178 -m\ +\ n\ =\ n\ +\ m%
3.179 -\rulenamedx{add_commute}\isanewline
3.180 -x\ +\ (y\ +\ z)\ =\ y\ +\ (x\
3.181 -+\ z)
3.182 -\rulename{add_left_commute}
3.183 -\end{isabelle}
3.184 -The name \isa{add_ac}\index{*add_ac (theorems)}
3.185 -refers to the list of all three theorems; similarly
3.186 -there is \isa{mult_ac}.\index{*mult_ac (theorems)}
3.187 -Here is an example of the sorting effect. Start
3.188 -with this goal:
3.189 -\begin{isabelle}
3.190 -\ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
3.191 -f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
3.192 -\end{isabelle}
3.193 -%
3.194 -Simplify using \isa{add_ac} and \isa{mult_ac}:
3.195 -\begin{isabelle}
3.196 -\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
3.197 -\end{isabelle}
3.198 -%
3.199 -Here is the resulting subgoal:
3.200 -\begin{isabelle}
3.201 -\ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
3.202 -=\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
3.203 -\end{isabelle}%
3.204 +\end{isabelle}%%%%%%
3.205 \index{natural numbers|)}\index{*nat (type)|)}
3.206
3.207
3.208 -
3.209 \subsection{The Type of Integers, {\tt\slshape int}}
3.210
3.211 \index{integers|(}\index{*int (type)|(}%
3.212 -Reasoning methods resemble those for the natural numbers, but induction and
3.213 -the constant \isa{Suc} are not available. HOL provides many lemmas
3.214 -for proving inequalities involving integer multiplication and division,
3.215 -similar to those shown above for type~\isa{nat}.
3.216 +Reasoning methods for the integers resemble those for the natural numbers,
3.217 +but induction and
3.218 the constant \isa{Suc} are not available. HOL provides many lemmas for
3.219 proving inequalities involving integer multiplication and division, similar
3.220 to those shown above for type~\isa{nat}. The laws of addition, subtraction
3.221 and multiplication are available through the axiomatic type class for rings
3.222 (\S\ref{sec:numeric-axclasses}).
3.223
3.224 -The \rmindex{absolute value} function \cdx{abs} is overloaded for the numeric types.
3.225 -It is defined for the integers; we have for example the obvious law
3.226 -\begin{isabelle}
3.227 -\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
3.228 -\rulename{abs_mult}
3.229 -\end{isabelle}
3.230 -
3.231 -\begin{warn}
3.232 -The absolute value bars shown above cannot be typed on a keyboard. They
3.233 -can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to
3.234 -get \isa{\isasymbar x\isasymbar}.
3.235 -\end{warn}
3.236 -
3.237 +The \rmindex{absolute value} function \cdx{abs} is overloaded, and is
3.238 +defined for all types that involve negative numbers, including the integers.
3.239 The \isa{arith} method can prove facts about \isa{abs} automatically,
3.240 though as it does so by case analysis, the cost can be exponential.
3.241 \begin{isabelle}
3.242 @@ -308,16 +245,6 @@
3.243 \isacommand{by}\ arith
3.244 \end{isabelle}
3.245
3.246 -Concerning simplifier tricks, we have no need to eliminate subtraction: it
3.247 -is well-behaved. As with the natural numbers, the simplifier can sort the
3.248 -operands of sums and products. The name \isa{zadd_ac}\index{*zadd_ac (theorems)}
3.249 -refers to the
3.250 -associativity and commutativity theorems for integer addition, while
3.251 -\isa{zmult_ac}\index{*zmult_ac (theorems)}
3.252 -has the analogous theorems for multiplication. The
3.253 -prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
3.254 -denote the set of integers.
3.255 -
3.256 For division and remainder,\index{division!by negative numbers}
3.257 the treatment of negative divisors follows
3.258 mathematical practice: the sign of the remainder follows that
3.259 @@ -363,7 +290,9 @@
3.260 \isa{c} to be zero. However, \isa{c} cannot be negative: a counterexample
3.261 is
3.262 $\isa{a} = 7$, $\isa{b} = 2$ and $\isa{c} = -3$, when the left-hand side of
3.263 -\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
3.264 +\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.
3.265 +The prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
3.266 +denote the set of integers.%
3.267 \index{integers|)}\index{*int (type)|)}
3.268
3.269 Induction is less important for integers than it is for the natural numbers, but it can be valuable if the range of integers has a lower or upper bound. There are four rules for integer induction, corresponding to the possible relations of the bound ($\geq$, $>$, $\leq$ and $<$):
3.270 @@ -379,27 +308,147 @@
3.271 \end{isabelle}
3.272
3.273
3.274 -\subsection{The Type of Real Numbers, {\tt\slshape real}}
3.275 +\subsection{The Types of Rational, Real and Complex Numbers}
3.276
3.277 +\index{rational numbers|(}\index{*rat (type)|(}%
3.278 \index{real numbers|(}\index{*real (type)|(}%
3.279 -The real numbers enjoy two significant properties that the integers lack.
3.280 -They are
3.281 -\textbf{dense}: between every two distinct real numbers there lies another.
3.282 -This property follows from the division laws, since if $x<y$ then between
3.283 -them lies $(x+y)/2$. The second property is that they are
3.284 -\textbf{complete}: every set of reals that is bounded above has a least
3.285 -upper bound. Completeness distinguishes the reals from the rationals, for
3.286 -which the set $\{x\mid x^2<2\}$ has no least upper bound. (It could only be
3.287 -$\surd2$, which is irrational.)
3.288 -The formalization of completeness is complicated; rather than
3.289 -reproducing it here, we refer you to the theory \texttt{RComplete} in
3.290 -directory \texttt{Real}.
3.291 -Density, however, is trivial to express:
3.292 +\index{complex numbers|(}\index{*complex (type)|(}%
3.293 +These types provide true division, the overloaded operator \isa{/},
3.294 +which differs from the operator \isa{div} of the
3.295 +natural numbers and integers. The rationals and reals are
3.296 +\textbf{dense}: between every two distinct numbers lies another.
3.297 +This property follows from the division laws, since if $x\not=y$ then $(x+y)/2$ lies between them:
3.298 \begin{isabelle}
3.299 -x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
3.300 +a\ <\ b\ \isasymLongrightarrow \ \isasymexists r.\ a\ <\ r\ \isasymand \ r\ <\ b%
3.301 \rulename{dense}
3.302 \end{isabelle}
3.303
3.304 +The real numbers are, moreover, \textbf{complete}: every set of reals that
3.305 is bounded above has a least upper bound. Completeness distinguishes the
3.306 reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least
3.307 upper bound. (It could only be $\surd2$, which is irrational. The
3.308 formalization of completeness, which is complicated,
3.309 +can be found in theory \texttt{RComplete} of directory
3.310 \texttt{Real}.
3.311 +
3.312 +Numeric literals\index{numeric literals!for type \protect\isa{real}}
3.313 +for type \isa{real} have the same syntax as those for type
3.314 +\isa{int} and only express integral values. Fractions expressed
3.315 +using the division operator are automatically simplified to lowest terms:
3.316 +\begin{isabelle}
3.317 +\ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
3.318 +\isacommand{apply} simp\isanewline
3.319 +\ 1.\ P\ (2\ /\ 5)
3.320 +\end{isabelle}
3.321 +Exponentiation can express floating-point values such as
3.322 +\isa{2 * 10\isacharcircum6}, but at present no special simplification
3.323 +is performed.
3.324 +
3.325 +\begin{warn}
3.326 +Type \isa{real} is only available in the logic HOL-Complex, which
3.327 +is HOL extended with a definitional development of the real and complex
3.328 +numbers. Base your theory upon theory
3.329 +\thydx{Complex_Main}, not the usual \isa{Main}.%
3.330 +\index{real numbers|)}\index{*real (type)|)}
3.331 +Launch Isabelle using the command
3.332 +\begin{verbatim}
3.333 +Isabelle -l HOL-Complex
3.334 +\end{verbatim}
3.335 +\end{warn}
3.336 +
3.337 +Also available in HOL-Complex is the
3.338 +theory \isa{Hyperreal}, which define the type \tydx{hypreal} of
3.339 +\rmindex{non-standard reals}. These
3.340 +\textbf{hyperreals} include infinitesimals, which represent infinitely
3.341 +small and infinitely large quantities; they facilitate proofs
3.342 +about limits, differentiation and integration~\cite{fleuriot-jcm}. The
3.343 +development defines an infinitely large number, \isa{omega} and an
3.344 +infinitely small positive number, \isa{epsilon}. The
3.345 +relation $x\approx y$ means ``$x$ is infinitely close to~$y$.''
3.346 +Theory \isa{Hyperreal} also defines transcendental functions such as sine,
3.347 +cosine, exponential and logarithm --- even the versions for type
3.348 +\isa{real}, because they are defined using nonstandard limits.%
3.349 +\index{rational numbers|)}\index{*rat (type)|)}%
3.350 +\index{real numbers|)}\index{*real (type)|)}%
3.351 +\index{complex numbers|)}\index{*complex (type)|)}
3.352 +
3.353 +
3.354 +\subsection{The Numeric Type Classes}\label{sec:numeric-axclasses}
3.355 +
3.356 +Isabelle/HOL organises its numeric theories using axiomatic type classes.
3.357 +Hundreds of basic properties are proved in the theory \isa{Ring_and_Field}.
3.358 +These lemmas are available (as simprules if they were declared as such)
3.359 +for all numeric types satisfying the necessary axioms. The theory defines
3.360 +the following type classes:
3.361 +\begin{itemize}
3.362 +\item
3.363 +\tcdx{semiring} and \tcdx{ordered_semiring}: a \emph{semiring}
3.364 provides the operators \isa{+} and~\isa{*}, which are commutative and
3.365 associative, with the usual distributive law and with \isa{0} and~\isa{1}
3.366 as their respective identities. An \emph{ordered semiring} is also linearly
3.367 ordered, with addition and multiplication respecting the ordering. Type \isa{nat} is an ordered semiring.
3.368 +\item
3.369 +\tcdx{ring} and \tcdx{ordered_ring}: a \emph{ring} extends a semiring
3.370 with unary minus (the additive inverse) and subtraction (both
3.371 denoted~\isa{-}). An \emph{ordered ring} includes the absolute value
3.372 function, \cdx{abs}. Type \isa{int} is an ordered ring.
3.373 +\item
3.374 +\tcdx{field} and \tcdx{ordered_field}: a field extends a ring with the
3.375 multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/}).
3.376 An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field.
3.377 +\item
3.378 +\tcdx{division_by_zero} includes all types where \isa{inverse 0 = 0}
3.379 +and \isa{a / 0 = 0}. These include all of Isabelle's standard numeric types.
3.380 +However, the basic properties of fields are derived without assuming
3.381 +division by zero.
3.382 \end{itemize}
3.383 +
3.384 +Theory \thydx{Ring_and_Field} proves over 250 lemmas, each of which
3.385 holds for all types in the corresponding type class. In most
3.386 cases, it is obvious whether a property is valid for a particular type. All
3.387 abstract properties involving subtraction require a ring, and therefore do
3.388 not hold for type \isa{nat}, although we have theorems such as
3.389 \isa{diff_mult_distrib} proved specifically about subtraction on
3.390 type~\isa{nat}. All abstract properties involving division require a field.
3.391 Obviously, all properties involving orderings required an ordered
3.392 structure.
3.393 +
3.394 +The following two theorems are less obvious. Although they
3.395 +mention no ordering, they require an ordered ring. However, if we have a
3.396 +field, then an ordering is no longer required.
3.397 +\begin{isabelle}
3.398 +(a\ *\ b\ =\ (0::'a))\ =\ (a\ =\ (0::'a)\ \isasymor \ b\ =\ (0::'a))
3.399 +\rulename{mult_eq_0_iff}\isanewline
3.400 +(a\ *\ c\ =\ b\ *\ c)\ =\ (c\ =\ (0::'a)\ \isasymor \ a\ =\ b)
3.401 +\rulename{mult_cancel_right}
3.402 +\end{isabelle}
3.403 +Theorems \isa{field_mult_eq_0_iff} and \isa{field_mult_cancel_right}
3.404 +express the same properties, only for fields. When working with such
3.405 +theorems, setting the \texttt{show_sorts}\index{*show_sorts (flag)}
3.406 +flag will display the type classes of all type variables. Here is how the
3.407 +theorem \isa{field_mult_cancel_right} appears with the flag set.
3.408 +\begin{isabelle}
3.409 +((a::'a::field)\ *\ (c::'a::field)\ =\ (b::'a::field)\ *\ c)\ =\isanewline
3.410 +(c\ =\ (0::'a::field)\ \isasymor \ a\ =\ b)
3.411 +\end{isabelle}
3.412 +
3.413 +
3.414 +\subsubsection{Simplifying with the AC-Laws}
3.415 +Suppose that two expressions are equal, differing only in
3.416 +associativity and commutativity of addition. Simplifying with the
3.417 +following equations sorts the terms and groups them to the right, making
3.418 +the two expressions identical.
3.419 +\begin{isabelle}
3.420 +a\ +\ b\ +\ c\ =\ a\ +\ (b\ +\ c)
3.421 +\rulenamedx{add_assoc}\isanewline
3.422 +a\ +\ b\ =\ b\ +\ a%
3.423 +\rulenamedx{add_commute}\isanewline
3.424 +a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c)
3.425 +\rulename{add_left_commute}
3.426 +\end{isabelle}
3.427 +The name \isa{add_ac}\index{*add_ac (theorems)}
3.428 +refers to the list of all three theorems; similarly
3.429 +there is \isa{mult_ac}.\index{*mult_ac (theorems)}
3.430 +They are all proved for semirings and therefore hold for all numeric types.
3.431 +
3.432 +Here is an example of the sorting effect. Start
3.433 +with this goal, which involves type \isa{nat}.
3.434 +\begin{isabelle}
3.435 +\ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
3.436 +f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l)
3.437 +\end{isabelle}
3.438 +%
3.439 +Simplify using \isa{add_ac} and \isa{mult_ac}.
3.440 +\begin{isabelle}
3.441 +\isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac)
3.442 +\end{isabelle}
3.443 +%
3.444 +Here is the resulting subgoal.
3.445 +\begin{isabelle}
3.446 +\ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\
3.447 +=\ f\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))%
3.448 +\end{isabelle}
3.449 +
3.450 +
3.451 +\subsubsection{Division Laws for Fields}
3.452 +
3.453 Here is a selection of rules about the division operator. The following
3.454 are installed as default simplification rules in order to express
3.455 combinations of products and quotients as rational expressions:
3.456 @@ -430,56 +479,41 @@
3.457 \rulename{add_divide_distrib}
3.458 \end{isabelle}
3.459
3.460 -As with the other numeric types, the simplifier can sort the operands of
3.461 -addition and multiplication. The name \isa{real_add_ac} refers to the
3.462 -associativity and commutativity theorems for addition, while similarly
3.463 -\isa{real_mult_ac} contains those properties for multiplication.
3.464
3.465 -The absolute value function \isa{abs} is
3.466 -defined for the reals, along with many theorems such as this one about
3.467 -exponentiation:
3.468 +\subsubsection{Absolute Value}
3.469 +
3.470 +The \rmindex{absolute value} function \cdx{abs} is available for all
3.471 +ordered rings, including types \isa{int}, \isa{rat} and \isa{real}.
3.472 +It satisfies many properties,
3.473 +such as the following:
3.474 \begin{isabelle}
3.475 -\isasymbar a\ \isacharcircum \ n\isasymbar\ =\
3.476 -\isasymbar a\isasymbar \ \isacharcircum \ n
3.477 -\rulename{power_abs}
3.478 +\isasymbar x\ *\ y\isasymbar \ =\ \isasymbar x\isasymbar \ *\ \isasymbar y\isasymbar
3.479 +\rulename{abs_mult}\isanewline
3.480 +(\isasymbar a\isasymbar \ \isasymle \ b)\ =\ (a\ \isasymle \ b\ \isasymand \ -\ a\ \isasymle \ b)
3.481 +\rulename{abs_le_iff}\isanewline
3.482 +\isasymbar a\ +\ b\isasymbar \ \isasymle \ \isasymbar a\isasymbar \ +\ \isasymbar b\isasymbar
3.483 +\rulename{abs_triangle_ineq}
3.484 \end{isabelle}
3.485
3.486 -Numeric literals\index{numeric literals!for type \protect\isa{real}}
3.487 -for type \isa{real} have the same syntax as those for type
3.488 -\isa{int} and only express integral values. Fractions expressed
3.489 -using the division operator are automatically simplified to lowest terms:
3.490 -\begin{isabelle}
3.491 -\ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
3.492 -\isacommand{apply} simp\isanewline
3.493 -\ 1.\ P\ (2\ /\ 5)
3.494 -\end{isabelle}
3.495 -Exponentiation can express floating-point values such as
3.496 -\isa{2 * 10\isacharcircum6}, but at present no special simplification
3.497 -is performed.
3.498 -
3.499 -
3.500 \begin{warn}
3.501 -Type \isa{real} is only available in the logic HOL-Complex, which
3.502 -is HOL extended with a definitional development of the real and complex
3.503 -numbers. Base your theory upon theory
3.504 -\thydx{Complex_Main}, not the usual \isa{Main}.%
3.505 -\index{real numbers|)}\index{*real (type)|)}
3.506 -Launch Isabelle using the command
3.507 -\begin{verbatim}
3.508 -Isabelle -l HOL-Complex
3.509 -\end{verbatim}
3.510 +The absolute value bars shown above cannot be typed on a keyboard. They
3.511 +can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to
3.512 +get \isa{\isasymbar x\isasymbar}.
3.513 \end{warn}
3.514
3.515 -Also available in HOL-Complex is the
3.516 -theory \isa{Hyperreal}, which define the type \tydx{hypreal} of
3.517 -\rmindex{non-standard reals}. These
3.518 -\textbf{hyperreals} include infinitesimals, which represent infinitely
3.519 -small and infinitely large quantities; they facilitate proofs
3.520 -about limits, differentiation and integration~\cite{fleuriot-jcm}. The
3.521 -development defines an infinitely large number, \isa{omega} and an
3.522 -infinitely small positive number, \isa{epsilon}. The
3.523 -relation $x\approx y$ means ``$x$ is infinitely close to~$y$.''
3.524 -Theory \isa{Hyperreal} also defines transcendental functions such as sine,
3.525 -cosine, exponential and logarithm --- even the versions for type
3.526 -\isa{real}, because they are defined using nonstandard limits.%
3.527 +
3.528 +\subsubsection{Raising to a Power}
3.529 +
3.530 +Another type class, \tcdx{ringppower}, specifies rings that also have
3.531 +exponentation to a natural number power, defined using the obvious primitive
3.532 +recursion. Theory \thydx{Power} proves various theorems, such as the
3.533 +following.
3.534 +\begin{isabelle}
3.535 +a\ \isacharcircum \ (m\ +\ n)\ =\ a\ \isacharcircum \ m\ *\ a\ \isacharcircum \ n%
3.536 +\rulename{power_add}\isanewline
3.537 +a\ \isacharcircum \ (m\ *\ n)\ =\ (a\ \isacharcircum \ m)\ \isacharcircum \ n%
3.538 +\rulename{power_mult}\isanewline
3.539 +\isasymbar a\ \isacharcircum \ n\isasymbar \ =\ \isasymbar a\isasymbar \ \isacharcircum \ n%
3.540 +\rulename{power_abs}
3.541 +\end{isabelle}%%%%%%%%%%%%%%%%%%%%%%%%%
3.542 \index{numbers|)}
4.1 --- a/doc-src/TutorialI/Types/types.tex Thu Feb 19 16:44:21 2004 +0100
4.2 +++ b/doc-src/TutorialI/Types/types.tex Thu Feb 19 17:57:54 2004 +0100
4.3 @@ -6,37 +6,29 @@
4.4 (\isacommand{datatype}). This chapter will introduce more
4.5 advanced material:
4.6 \begin{itemize}
4.7 -\item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs
4.8 - ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to
4.9 - reason about them.
4.10 +\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
4.11 and how to reason about them.
4.12 \item Type classes: how to specify and reason about axiomatic collections of
4.13 - types ({\S}\ref{sec:axclass}).
4.14 -\item Introducing your own types: how to introduce new types that
4.15 + types ({\S}\ref{sec:axclass}). This section leads on to a discussion of
4.16 + Isabelle's numeric types ({\S}\ref{sec:numbers}).
4.17 +\item Introducing your own types: how to define types that
4.18 cannot be constructed with any of the basic methods
4.19 ({\S}\ref{sec:adv-typedef}).
4.20 \end{itemize}
4.21
4.22 -The material in this section goes beyond the needs of most novices. Serious
4.23 -users should at least skim the sections on basic types and on type classes.
4.24 -The latter material is fairly advanced; read the beginning to understand what
4.25 -it is
4.26 -about, but consult the rest only when necessary.
4.27 -
4.28 -\input{Types/numerics}
4.29 +The material in this section goes beyond the needs of most novices.
4.30 Serious users should at least skim the sections as far as type classes.
4.31 That material is fairly advanced; read the beginning to understand what it
4.32 is about, but consult the rest only when necessary.
4.33
4.34 \index{pairs and tuples|(}
4.35 -\input{Types/document/Pairs}
4.36 +\input{Types/document/Pairs} %%%Section "Pairs and Tuples"
4.37 \index{pairs and tuples|)}
4.38
4.39 -\input{Types/document/Records}
4.40 +\input{Types/document/Records} %%%Section "Records"
4.41
4.42
4.43 -\section{Axiomatic Type Classes}
4.44 +\section{Axiomatic Type Classes} %%%Section
4.45 \label{sec:axclass}
4.46 \index{axiomatic type classes|(}
4.47 \index{*axclass|(}
4.48
4.49 -
4.50 The programming language Haskell has popularized the notion of type classes.
4.51 In its simplest form, a type class is a set of types with a common interface:
4.52 all types in that class must provide the functions in the interface.
4.53 @@ -67,5 +59,6 @@
4.54 \index{axiomatic type classes|)}
4.55 \index{*axclass|)}
4.56
4.57 +\input{Types/numerics} %%%Section "Numbers"
4.58
4.59 -\input{Types/document/Typedefs}
4.60 +\input{Types/document/Typedefs} %%%Section "Introducing New Types"
5.1 --- a/doc-src/TutorialI/tutorial.sty Thu Feb 19 16:44:21 2004 +0100
5.2 +++ b/doc-src/TutorialI/tutorial.sty Thu Feb 19 17:57:54 2004 +0100
5.3 @@ -34,6 +34,7 @@
5.4
5.5 \newcommand\cldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (class)}}
5.6 \newcommand\tydx[1]{\isa{#1}\index{#1@\protect\isa{#1} (type)}}
5.7 +\newcommand\tcdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (type class)}}
5.8 \newcommand\thydx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theory)}}
5.9
5.10 \newcommand\attrdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (attribute)}}
6.1 --- a/doc-src/TutorialI/tutorial.tex Thu Feb 19 16:44:21 2004 +0100
6.2 +++ b/doc-src/TutorialI/tutorial.tex Thu Feb 19 17:57:54 2004 +0100
6.3 @@ -1,4 +1,5 @@
6.4 \documentclass{article}
6.5 +%%\includeonly{Types/types} %%UNCOMMENT to process only selected chapters
6.6 \usepackage{cl2emono-modified,isabelle,isabellesym}
6.7 \usepackage{../proof,amsmath,amsfonts}
6.8 \usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment}
6.9 @@ -52,26 +53,26 @@
6.10 \vspace*{\fill}
6.11 \vspace*{\fill}
6.12 \newpage
6.13 -\input{preface}
6.14 +\include{preface}
6.15
6.16 \tableofcontents
6.17
6.18 \cleardoublepage\pagenumbering{arabic}
6.19
6.20 \part{Elementary Techniques}
6.21 -\input{basics}
6.22 -\input{fp}
6.23 -\input{Documents/documents}
6.24 +\include{basics}
6.25 +\include{fp}
6.26 +\include{Documents/documents}
6.27
6.28 \part{Logic and Sets}
6.29 -\input{Rules/rules}
6.30 -\input{Sets/sets}\input{CTL/ctl} %these constitute ONE chapter
6.31 -\input{Inductive/inductive}
6.32 +\include{Rules/rules}
6.33 +\include{Sets/sets}
6.34 +\include{Inductive/inductive}
6.35
6.36 \part{Advanced Material}
6.37 -\input{Types/types}
6.38 -\input{Advanced/advanced}
6.39 -\input{Protocol/protocol}
6.40 +\include{Types/types}
6.41 +\include{Advanced/advanced}
6.42 +\include{Protocol/protocol}
6.43
6.44 \markboth{}{}
6.45 \cleardoublepage
6.46 @@ -85,9 +86,12 @@
6.47 \vspace*{\fill}
6.48 \vspace*{\fill}
6.49
6.50 -\input{appendix}
6.51 +\underscoreoff
6.52 +
6.53 +\include{appendix}
6.54
6.55 \bibliographystyle{plain}
6.56 \bibliography{../manual}
6.57 +\underscoreoff
6.58 \printindex
6.59 \end{document}