*** empty log message ***
authornipkow
Wed Oct 25 18:24:33 2000 +0200 (2000-10-25)
changeset 10328bf33cbd76c05
parent 10327 19214ac381cf
child 10329 a9898d89a634
*** empty log message ***
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Misc/AdvancedInd.thy
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/Types/Axioms.thy
doc-src/TutorialI/Types/Overloading.thy
doc-src/TutorialI/Types/Overloading0.thy
doc-src/TutorialI/Types/Overloading1.thy
doc-src/TutorialI/Types/Overloading2.thy
doc-src/TutorialI/Types/document/Axioms.tex
doc-src/TutorialI/Types/document/Overloading.tex
doc-src/TutorialI/Types/document/Overloading0.tex
doc-src/TutorialI/Types/document/Overloading1.tex
doc-src/TutorialI/Types/document/Overloading2.tex
doc-src/TutorialI/Types/types.tex
doc-src/TutorialI/appendix.tex
     1.1 --- a/doc-src/TutorialI/IsaMakefile	Wed Oct 25 17:44:59 2000 +0200
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Wed Oct 25 18:24:33 2000 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  ## targets
     1.6  
     1.7 -default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Misc styles
     1.8 +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Types HOL-Misc styles
     1.9  images:
    1.10  test:
    1.11  all: default
    1.12 @@ -138,6 +138,16 @@
    1.13  	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive
    1.14  	@rm -f tutorial.dvi
    1.15  
    1.16 +## HOL-Types
    1.17 +
    1.18 +HOL-Types: HOL $(LOG)/HOL-Types.gz
    1.19 +
    1.20 +$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
    1.21 +  Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
    1.22 +  Types/Overloading.thy Types/Axioms.thy
    1.23 +	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Types
    1.24 +	@rm -f tutorial.dvi
    1.25 +
    1.26  ## HOL-Misc
    1.27  
    1.28  HOL-Misc: HOL $(LOG)/HOL-Misc.gz
    1.29 @@ -154,4 +164,4 @@
    1.30  ## clean
    1.31  
    1.32  clean:
    1.33 -	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz
    1.34 +	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz
     2.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Wed Oct 25 17:44:59 2000 +0200
     2.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Wed Oct 25 18:24:33 2000 +0200
     2.3 @@ -57,6 +57,7 @@
     2.4  
     2.5  text{*\noindent
     2.6  This time, induction leaves us with the following base case
     2.7 +%{goals[goals_limit=1,display]}
     2.8  \begin{isabelle}
     2.9  \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
    2.10  \end{isabelle}
     3.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Oct 25 17:44:59 2000 +0200
     3.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Oct 25 18:24:33 2000 +0200
     3.3 @@ -54,6 +54,7 @@
     3.4  \begin{isamarkuptext}%
     3.5  \noindent
     3.6  This time, induction leaves us with the following base case
     3.7 +%{goals[goals_limit=1,display]}
     3.8  \begin{isabelle}
     3.9  \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
    3.10  \end{isabelle}
     4.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Wed Oct 25 17:44:59 2000 +0200
     4.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Wed Oct 25 18:24:33 2000 +0200
     4.3 @@ -184,8 +184,8 @@
     4.4  
     4.5  The induction step is an example of the general format of a subgoal:
     4.6  \begin{isabelle}
     4.7 -~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
     4.8 -\end{isabelle}
     4.9 +~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
    4.10 +\end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
    4.11  The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
    4.12  ignored most of the time, or simply treated as a list of variables local to
    4.13  this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
     5.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Oct 25 17:44:59 2000 +0200
     5.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Oct 25 18:24:33 2000 +0200
     5.3 @@ -179,8 +179,8 @@
     5.4  
     5.5  The induction step is an example of the general format of a subgoal:
     5.6  \begin{isabelle}
     5.7 -~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
     5.8 -\end{isabelle}
     5.9 +~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
    5.10 +\end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
    5.11  The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
    5.12  ignored most of the time, or simply treated as a list of variables local to
    5.13  this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/doc-src/TutorialI/Types/Axioms.thy	Wed Oct 25 18:24:33 2000 +0200
     6.3 @@ -0,0 +1,202 @@
     6.4 +(*<*)theory Axioms = Overloading:(*>*)
     6.5 +
     6.6 +subsection{*Axioms*}
     6.7 +
     6.8 +
     6.9 +text{*Now we want to attach axioms to our classes. Then we can reason on the
    6.10 +level of classes and the results will be applicable to all types in a class,
    6.11 +just as in axiomatic mathematics. These ideas are demonstrated by means of
    6.12 +our above ordering relations.
    6.13 +*}
    6.14 +
    6.15 +subsubsection{*Partial orders*}
    6.16 +
    6.17 +text{*
    6.18 +A \emph{partial order} is a subclass of @{text ordrel}
    6.19 +where certain axioms need to hold:
    6.20 +*}
    6.21 +
    6.22 +axclass parord < ordrel
    6.23 +refl:    "x <<= x"
    6.24 +trans:   "\<lbrakk> x <<= y; y <<= z \<rbrakk> \<Longrightarrow> x <<= z"
    6.25 +antisym: "\<lbrakk> x <<= y; y <<= x \<rbrakk> \<Longrightarrow> x = y"
    6.26 +less_le: "x << y = (x <<= y \<and> x \<noteq> y)"
    6.27 +
    6.28 +text{*\noindent
    6.29 +The first three axioms are the familiar ones, and the final one
    6.30 +requires that @{text"<<"} and @{text"<<="} are related as expected.
    6.31 +Note that behind the scenes, Isabelle has restricted the axioms to class
    6.32 +@{text parord}. For example, this is what @{thm[source]refl} really looks like:
    6.33 +@{thm[show_types]refl}.
    6.34 +
    6.35 +We can now prove simple theorems in this abstract setting, for example
    6.36 +that @{text"<<"} is not symmetric:
    6.37 +*}
    6.38 +
    6.39 +lemma [simp]: "(x::'a::parord) << y \<Longrightarrow> (\<not> y << x) = True";
    6.40 +
    6.41 +txt{*\noindent
    6.42 +The conclusion is not simply @{prop"\<not> y << x"} because the preprocessor
    6.43 +of the simplifier would turn this into @{prop"y << x = False"}, thus yielding
    6.44 +a nonterminating rewrite rule. In the above form it is a generally useful
    6.45 +rule.
    6.46 +The type constraint is necessary because otherwise Isabelle would only assume
    6.47 +@{text"'a::ordrel"} (as required in the type of @{text"<<"}), in
    6.48 +which case the proposition is not a theorem.  The proof is easy:
    6.49 +*}
    6.50 +
    6.51 +by(simp add:less_le antisym);
    6.52 +
    6.53 +text{* We could now continue in this vein and develop a whole theory of
    6.54 +results about partial orders. Eventually we will want to apply these results
    6.55 +to concrete types, namely the instances of the class. Thus we first need to
    6.56 +prove that the types in question, for example @{typ bool}, are indeed
    6.57 +instances of @{text parord}:*}
    6.58 +
    6.59 +instance bool :: parord
    6.60 +apply intro_classes;
    6.61 +
    6.62 +txt{*\noindent
    6.63 +This time @{text intro_classes} leaves us with the four axioms,
    6.64 +specialized to type @{typ bool}, as subgoals:
    6.65 +@{goals[display,show_types,indent=0]}
    6.66 +Fortunately, the proof is easy for blast, once we have unfolded the definitions
    6.67 +of @{text"<<"} and @{text"<<="} at @{typ bool}:
    6.68 +*}
    6.69 +
    6.70 +apply(simp_all (no_asm_use) only: le_bool_def less_bool_def);
    6.71 +by(blast, blast, blast, blast);
    6.72 +
    6.73 +text{*\noindent
    6.74 +Can you figure out why we have to include @{text"(no_asm_use)"}?
    6.75 +
    6.76 +We can now apply our single lemma above in the context of booleans:
    6.77 +*}
    6.78 +
    6.79 +lemma "(P::bool) << Q \<Longrightarrow> \<not>(Q << P)";
    6.80 +by simp;
    6.81 +
    6.82 +text{*\noindent
    6.83 +The effect is not stunning but demonstrates the principle.  It also shows
    6.84 +that tools like the simplifier can deal with generic rules as well. Moreover,
    6.85 +it should be clear that the main advantage of the axiomatic method is that
    6.86 +theorems can be proved in the abstract and one does not need to repeat the
    6.87 +proof for each instance.
    6.88 +*}
    6.89 +
    6.90 +subsubsection{*Linear orders*}
    6.91 +
    6.92 +text{* If any two elements of a partial order are comparable it is a
    6.93 +\emph{linear} or \emph{total} order: *}
    6.94 +
    6.95 +axclass linord < parord
    6.96 +total: "x <<= y \<or> y <<= x"
    6.97 +
    6.98 +text{*\noindent
    6.99 +By construction, @{text linord} inherits all axioms from @{text parord}.
   6.100 +Therefore we can show that totality can be expressed in terms of @{text"<<"}
   6.101 +as follows:
   6.102 +*}
   6.103 +
   6.104 +lemma "\<And>x::'a::linord. x<<y \<or> x=y \<or> y<<x";
   6.105 +apply(simp add: less_le);
   6.106 +apply(insert total);
   6.107 +apply blast;
   6.108 +done
   6.109 +
   6.110 +text{*
   6.111 +Linear orders are an example of subclassing by construction, which is the most
   6.112 +common case. It is also possible to prove additional subclass relationships
   6.113 +later on, i.e.\ subclassing by proof. This is the topic of the following
   6.114 +section.
   6.115 +*}
   6.116 +
   6.117 +subsubsection{*Strict orders*}
   6.118 +
   6.119 +text{*
   6.120 +An alternative axiomatization of partial orders takes @{text"<<"} rather than
   6.121 +@{text"<<="} as the primary concept. The result is a \emph{strict} order:
   6.122 +*}
   6.123 +
   6.124 +axclass strord < ordrel
   6.125 +irrefl:     "\<not> x << x"
   6.126 +less_trans: "\<lbrakk> x << y; y << z \<rbrakk> \<Longrightarrow> x << z"
   6.127 +le_less:    "x <<= y = (x << y \<or> x = y)"
   6.128 +
   6.129 +text{*\noindent
   6.130 +It is well known that partial orders are the same as strict orders. Let us
   6.131 +prove one direction, namely that partial orders are a subclass of strict
   6.132 +orders. The proof follows the ususal pattern: *}
   6.133 +
   6.134 +instance parord < strord
   6.135 +apply intro_classes;
   6.136 +apply(simp_all (no_asm_use) add:less_le);
   6.137 +  apply(blast intro: trans antisym);
   6.138 + apply(blast intro: refl);
   6.139 +done
   6.140 +
   6.141 +text{*\noindent
   6.142 +The result is the following subclass diagram:
   6.143 +\[
   6.144 +\begin{array}{c}
   6.145 +\isa{term}\\
   6.146 +|\\
   6.147 +\isa{ordrel}\\
   6.148 +|\\
   6.149 +\isa{strord}\\
   6.150 +|\\
   6.151 +\isa{parord}
   6.152 +\end{array}
   6.153 +\]
   6.154 +
   6.155 +In general, the subclass diagram must be acyclic. Therefore Isabelle will
   6.156 +complain if you also prove the relationship @{text"strord < parord"}.
   6.157 +Multiple inheritance is however permitted.
   6.158 +
   6.159 +This finishes our demonstration of type classes based on orderings.  We
   6.160 +remind our readers that \isa{Main} contains a much more developed theory of
   6.161 +orderings phrased in terms of the usual @{text"\<le>"} and @{text"<"}.
   6.162 +It is recommended that, if possible,
   6.163 +you base your own ordering relations on this theory.
   6.164 +*}
   6.165 +
   6.166 +(*
   6.167 +instance strord < parord
   6.168 +apply intro_classes;
   6.169 +apply(simp_all (no_asm_use) add:le_less);
   6.170 +apply(blast intro: less_trans);
   6.171 +apply(erule disjE);
   6.172 +apply(erule disjE);
   6.173 +apply(rule irrefl[THEN notE]);
   6.174 +apply(rule less_trans, assumption, assumption);
   6.175 +apply blast;apply blast;
   6.176 +apply(blast intro: irrefl[THEN notE]);
   6.177 +done
   6.178 +*)
   6.179 +
   6.180 +subsubsection{*Inconsistencies*}
   6.181 +
   6.182 +text{* The reader may be wondering what happens if we, maybe accidentally,
   6.183 +attach an inconsistent set of axioms to a class. So far we have always
   6.184 +avoided to add new axioms to HOL for fear of inconsistencies and suddenly it
   6.185 +seems that we are throwing all caution to the wind. So why is there no
   6.186 +problem?
   6.187 +
   6.188 +The point is that by construction, all type variables in the axioms of an
   6.189 +\isacommand{axclass} are automatically constrained with the class being
   6.190 +defined (as shown for axiom @{thm[source]refl} above). These constraints are
   6.191 +always carried around and Isabelle takes care that they are never lost,
   6.192 +unless the type variable is instantiated with a type that has been shown to
   6.193 +belong to that class. Thus you may be able to prove @{prop False}
   6.194 +from your axioms, but Isabelle will remind you that this
   6.195 +theorem has the hidden hypothesis that the class is non-empty.
   6.196 +*}
   6.197 +
   6.198 +(*
   6.199 +axclass false<"term"
   6.200 +false: "x \<noteq> x";
   6.201 +
   6.202 +lemma "False";
   6.203 +by(rule notE[OF false HOL.refl]);
   6.204 +*)
   6.205 +(*<*)end(*>*)
     7.1 --- a/doc-src/TutorialI/Types/Overloading.thy	Wed Oct 25 17:44:59 2000 +0200
     7.2 +++ b/doc-src/TutorialI/Types/Overloading.thy	Wed Oct 25 18:24:33 2000 +0200
     7.3 @@ -3,8 +3,12 @@
     7.4  by intro_classes
     7.5  
     7.6  text{*\noindent
     7.7 -This means. Of course we should also define the meaning of @{text <<=} and
     7.8 -@{text <<} on lists.
     7.9 +This \isacommand{instance} declaration can be read like the declaration of
    7.10 +a function on types: the constructor @{text list} maps types of class @{text
    7.11 +term}, i.e.\ all HOL types, to types of class @{text ordrel}, i.e.\
    7.12 +if @{text"ty :: term"} then @{text"ty list :: ordrel"}.
    7.13 +Of course we should also define the meaning of @{text <<=} and
    7.14 +@{text <<} on lists:
    7.15  *}
    7.16  
    7.17  defs (overloaded)
     8.1 --- a/doc-src/TutorialI/Types/Overloading0.thy	Wed Oct 25 17:44:59 2000 +0200
     8.2 +++ b/doc-src/TutorialI/Types/Overloading0.thy	Wed Oct 25 18:24:33 2000 +0200
     8.3 @@ -1,11 +1,13 @@
     8.4  (*<*)theory Overloading0 = Main:(*>*)
     8.5  
     8.6 +text{* We start with a concept that is required for type classes but already
     8.7 +useful on its own: \emph{overloading}. Isabelle allows overloading: a
     8.8 +constant may have multiple definitions at non-overlapping types. *}
     8.9 +
    8.10  subsubsection{*An initial example*}
    8.11  
    8.12 -text{* We start with a concept that is required for type classes but already
    8.13 -useful on its own: \emph{overloading}. Isabelle allows overloading: a
    8.14 -constant may have multiple definitions at non-overlapping types. For example,
    8.15 -if we want to introduce the notion of an \emph{inverse} at arbitrary types we
    8.16 +text{*
    8.17 +If we want to introduce the notion of an \emph{inverse} for arbitrary types we
    8.18  give it a polymorphic type *}
    8.19  
    8.20  consts inverse :: "'a \<Rightarrow> 'a"
    8.21 @@ -25,7 +27,7 @@
    8.22  common instance. What is more, the recursion in @{thm[source]inverse_pair} is
    8.23  benign because the type of @{term inverse} becomes smaller: on the left it is
    8.24  @{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and @{typ"'b \<Rightarrow>
    8.25 -'b"}. The @{text"(overloaded)"} tells Isabelle that the definitions do
    8.26 +'b"}. The annotation @{text"(overloaded)"} tells Isabelle that the definitions do
    8.27  intentionally define @{term inverse} only at instances of its declared type
    8.28  @{typ"'a \<Rightarrow> 'a"} --- this merely supresses warnings to that effect.
    8.29  
     9.1 --- a/doc-src/TutorialI/Types/Overloading1.thy	Wed Oct 25 17:44:59 2000 +0200
     9.2 +++ b/doc-src/TutorialI/Types/Overloading1.thy	Wed Oct 25 18:24:33 2000 +0200
     9.3 @@ -5,7 +5,7 @@
     9.4  text{*
     9.5  We now start with the theory of ordering relations, which we want to phrase
     9.6  in terms of the two binary symbols @{text"<<"} and @{text"<<="}: they have
     9.7 -been chosen to avoid clashes with @{text"\<le>"} and @{text"<"} in theory @{text
     9.8 +been chosen to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text
     9.9  Main}. To restrict the application of @{text"<<"} and @{text"<<="} we
    9.10  introduce the class @{text ordrel}:
    9.11  *}
    9.12 @@ -13,27 +13,52 @@
    9.13  axclass ordrel < "term"
    9.14  
    9.15  text{*\noindent
    9.16 +This introduces a new class @{text ordrel} and makes it a subclass of
    9.17 +the predefined class @{text term}\footnote{The quotes around @{text term}
    9.18 +simply avoid the clash with the command \isacommand{term}.}; @{text term}
    9.19 +is the class of all HOL types, like ``Object'' in Java.
    9.20  This is a degenerate form of axiomatic type class without any axioms.
    9.21  Its sole purpose is to restrict the use of overloaded constants to meaningful
    9.22  instances:
    9.23  *}
    9.24  
    9.25 -consts
    9.26 -  "<<"        :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"             (infixl 50)
    9.27 -  "<<="       :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"             (infixl 50)
    9.28 +consts less :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"     (infixl "<<"  50)
    9.29 +       le   :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"     (infixl "<<=" 50)
    9.30 +
    9.31 +text{*\noindent
    9.32 +So far there is not a single type of class @{text ordrel}. To breathe life
    9.33 +into @{text ordrel} we need to declare a type to be an \bfindex{instance} of
    9.34 +@{text ordrel}:
    9.35 +*}
    9.36  
    9.37  instance bool :: ordrel
    9.38 +
    9.39 +txt{*\noindent
    9.40 +Command \isacommand{instance} actually starts a proof, namely that
    9.41 +@{typ bool} satisfies all axioms of @{text ordrel}.
    9.42 +There are none, but we still need to finish that proof, which we do
    9.43 +by invoking a fixed predefined method:
    9.44 +*}
    9.45 +
    9.46  by intro_classes
    9.47  
    9.48 +text{*\noindent
    9.49 +More interesting \isacommand{instance} proofs will arise below
    9.50 +in the context of proper axiomatic type classes.
    9.51 +
    9.52 +Althoug terms like @{prop"False <<= P"} are now legal, we still need to say
    9.53 +what the relation symbols actually mean at type @{typ bool}:
    9.54 +*}
    9.55 +
    9.56  defs (overloaded)
    9.57  le_bool_def:  "P <<= Q \<equiv> P \<longrightarrow> Q"
    9.58  less_bool_def: "P << Q \<equiv> \<not>P \<and> Q"
    9.59  
    9.60 -text{*
    9.61 -Now @{prop"False <<= False"} is provable
    9.62 +text{*\noindent
    9.63 +Now @{prop"False <<= P"} is provable
    9.64  *}
    9.65  
    9.66 -lemma "False <<= False"
    9.67 +lemma "False <<= P"
    9.68  by(simp add: le_bool_def)
    9.69  
    9.70  text{*\noindent
    10.1 --- a/doc-src/TutorialI/Types/Overloading2.thy	Wed Oct 25 17:44:59 2000 +0200
    10.2 +++ b/doc-src/TutorialI/Types/Overloading2.thy	Wed Oct 25 18:24:33 2000 +0200
    10.3 @@ -2,7 +2,9 @@
    10.4  
    10.5  text{*
    10.6  Of course this is not the only possible definition of the two relations.
    10.7 -Componentwise
    10.8 +Componentwise comparison of lists of equal length also makes sense. This time
    10.9 +the elements of the list must also be of class @{text ordrel} to permit their
   10.10 +comparison:
   10.11  *}
   10.12  
   10.13  instance list :: (ordrel)ordrel
   10.14 @@ -12,10 +14,8 @@
   10.15  le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv>
   10.16                size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)"
   10.17  
   10.18 -text{*
   10.19 +text{*\noindent
   10.20 +The infix function @{text"!"} yields the nth element of a list.
   10.21  %However, we retract the componetwise comparison of lists and return
   10.22 -
   10.23 -Note: only one definition because based on name.
   10.24 -*}
   10.25 -(*<*)end(*>*)
   10.26 -
   10.27 +%Note: only one definition because based on name.
   10.28 +*}(*<*)end(*>*)
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/doc-src/TutorialI/Types/document/Axioms.tex	Wed Oct 25 18:24:33 2000 +0200
    11.3 @@ -0,0 +1,186 @@
    11.4 +%
    11.5 +\begin{isabellebody}%
    11.6 +\def\isabellecontext{Axioms}%
    11.7 +%
    11.8 +\isamarkupsubsection{Axioms}
    11.9 +%
   11.10 +\begin{isamarkuptext}%
   11.11 +Now we want to attach axioms to our classes. Then we can reason on the
   11.12 +level of classes and the results will be applicable to all types in a class,
   11.13 +just as in axiomatic mathematics. These ideas are demonstrated by means of
   11.14 +our above ordering relations.%
   11.15 +\end{isamarkuptext}%
   11.16 +%
   11.17 +\isamarkupsubsubsection{Partial orders}
   11.18 +%
   11.19 +\begin{isamarkuptext}%
   11.20 +A \emph{partial order} is a subclass of \isa{ordrel}
   11.21 +where certain axioms need to hold:%
   11.22 +\end{isamarkuptext}%
   11.23 +\isacommand{axclass}\ parord\ {\isacharless}\ ordrel\isanewline
   11.24 +refl{\isacharcolon}\ \ \ \ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}\isanewline
   11.25 +trans{\isacharcolon}\ \ \ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isachardoublequote}\isanewline
   11.26 +antisym{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequote}\isanewline
   11.27 +less{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequote}%
   11.28 +\begin{isamarkuptext}%
   11.29 +\noindent
   11.30 +The first three axioms are the familiar ones, and the final one
   11.31 +requires that \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} are related as expected.
   11.32 +Note that behind the scenes, Isabelle has restricted the axioms to class
   11.33 +\isa{parord}. For example, this is what \isa{refl} really looks like:
   11.34 +\isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
   11.35 +
   11.36 +We can now prove simple theorems in this abstract setting, for example
   11.37 +that \isa{{\isacharless}{\isacharless}} is not symmetric:%
   11.38 +\end{isamarkuptext}%
   11.39 +\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}parord{\isacharparenright}\ {\isacharless}{\isacharless}\ y\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}%
   11.40 +\begin{isamarkuptxt}%
   11.41 +\noindent
   11.42 +The conclusion is not simply \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the preprocessor
   11.43 +of the simplifier would turn this into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, thus yielding
   11.44 +a nonterminating rewrite rule. In the above form it is a generally useful
   11.45 +rule.
   11.46 +The type constraint is necessary because otherwise Isabelle would only assume
   11.47 +\isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}), in
   11.48 +which case the proposition is not a theorem.  The proof is easy:%
   11.49 +\end{isamarkuptxt}%
   11.50 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}less{\isacharunderscore}le\ antisym{\isacharparenright}%
   11.51 +\begin{isamarkuptext}%
   11.52 +We could now continue in this vein and develop a whole theory of
   11.53 +results about partial orders. Eventually we will want to apply these results
   11.54 +to concrete types, namely the instances of the class. Thus we first need to
   11.55 +prove that the types in question, for example \isa{bool}, are indeed
   11.56 +instances of \isa{parord}:%
   11.57 +\end{isamarkuptext}%
   11.58 +\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ parord\isanewline
   11.59 +\isacommand{apply}\ intro{\isacharunderscore}classes%
   11.60 +\begin{isamarkuptxt}%
   11.61 +\noindent
   11.62 +This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms,
   11.63 +specialized to type \isa{bool}, as subgoals:
   11.64 +\begin{isabelle}%
   11.65 +OFCLASS{\isacharparenleft}bool{\isacharcomma}\ parord{\isacharunderscore}class{\isacharparenright}\isanewline
   11.66 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline
   11.67 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}\ z{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z\isanewline
   11.68 +\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline
   11.69 +\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}%
   11.70 +\end{isabelle}
   11.71 +Fortunately, the proof is easy for blast, once we have unfolded the definitions
   11.72 +of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at \isa{bool}:%
   11.73 +\end{isamarkuptxt}%
   11.74 +\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ only{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def\ less{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
   11.75 +\isacommand{by}{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}%
   11.76 +\begin{isamarkuptext}%
   11.77 +\noindent
   11.78 +Can you figure out why we have to include \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}?
   11.79 +
   11.80 +We can now apply our single lemma above in the context of booleans:%
   11.81 +\end{isamarkuptext}%
   11.82 +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequote}\isanewline
   11.83 +\isacommand{by}\ simp%
   11.84 +\begin{isamarkuptext}%
   11.85 +\noindent
   11.86 +The effect is not stunning but demonstrates the principle.  It also shows
   11.87 +that tools like the simplifier can deal with generic rules as well. Moreover,
   11.88 +it should be clear that the main advantage of the axiomatic method is that
   11.89 +theorems can be proved in the abstract and one does not need to repeat the
   11.90 +proof for each instance.%
   11.91 +\end{isamarkuptext}%
   11.92 +%
   11.93 +\isamarkupsubsubsection{Linear orders}
   11.94 +%
   11.95 +\begin{isamarkuptext}%
   11.96 +If any two elements of a partial order are comparable it is a
   11.97 +\emph{linear} or \emph{total} order:%
   11.98 +\end{isamarkuptext}%
   11.99 +\isacommand{axclass}\ linord\ {\isacharless}\ parord\isanewline
  11.100 +total{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}%
  11.101 +\begin{isamarkuptext}%
  11.102 +\noindent
  11.103 +By construction, \isa{linord} inherits all axioms from \isa{parord}.
  11.104 +Therefore we can show that totality can be expressed in terms of \isa{{\isacharless}{\isacharless}}
  11.105 +as follows:%
  11.106 +\end{isamarkuptext}%
  11.107 +\isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}linord{\isachardot}\ x{\isacharless}{\isacharless}y\ {\isasymor}\ x{\isacharequal}y\ {\isasymor}\ y{\isacharless}{\isacharless}x{\isachardoublequote}\isanewline
  11.108 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline
  11.109 +\isacommand{apply}{\isacharparenleft}insert\ total{\isacharparenright}\isanewline
  11.110 +\isacommand{apply}\ blast\isanewline
  11.111 +\isacommand{done}%
  11.112 +\begin{isamarkuptext}%
  11.113 +Linear orders are an example of subclassing by construction, which is the most
  11.114 +common case. It is also possible to prove additional subclass relationships
  11.115 +later on, i.e.\ subclassing by proof. This is the topic of the following
  11.116 +section.%
  11.117 +\end{isamarkuptext}%
  11.118 +%
  11.119 +\isamarkupsubsubsection{Strict orders}
  11.120 +%
  11.121 +\begin{isamarkuptext}%
  11.122 +An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than
  11.123 +\isa{{\isacharless}{\isacharless}{\isacharequal}} as the primary concept. The result is a \emph{strict} order:%
  11.124 +\end{isamarkuptext}%
  11.125 +\isacommand{axclass}\ strord\ {\isacharless}\ ordrel\isanewline
  11.126 +irrefl{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isasymnot}\ x\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline
  11.127 +less{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z{\isachardoublequote}\isanewline
  11.128 +le{\isacharunderscore}less{\isacharcolon}\ \ \ \ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}%
  11.129 +\begin{isamarkuptext}%
  11.130 +\noindent
  11.131 +It is well known that partial orders are the same as strict orders. Let us
  11.132 +prove one direction, namely that partial orders are a subclass of strict
  11.133 +orders. The proof follows the ususal pattern:%
  11.134 +\end{isamarkuptext}%
  11.135 +\isacommand{instance}\ parord\ {\isacharless}\ strord\isanewline
  11.136 +\isacommand{apply}\ intro{\isacharunderscore}classes\isanewline
  11.137 +\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}less{\isacharunderscore}le{\isacharparenright}\isanewline
  11.138 +\ \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline
  11.139 +\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline
  11.140 +\isacommand{done}%
  11.141 +\begin{isamarkuptext}%
  11.142 +\noindent
  11.143 +The result is the following subclass diagram:
  11.144 +\[
  11.145 +\begin{array}{c}
  11.146 +\isa{term}\\
  11.147 +|\\
  11.148 +\isa{ordrel}\\
  11.149 +|\\
  11.150 +\isa{strord}\\
  11.151 +|\\
  11.152 +\isa{parord}
  11.153 +\end{array}
  11.154 +\]
  11.155 +
  11.156 +In general, the subclass diagram must be acyclic. Therefore Isabelle will
  11.157 +complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.
  11.158 +Multiple inheritance is however permitted.
  11.159 +
  11.160 +This finishes our demonstration of type classes based on orderings.  We
  11.161 +remind our readers that \isa{Main} contains a much more developed theory of
  11.162 +orderings phrased in terms of the usual \isa{{\isasymle}} and \isa{{\isacharless}}.
  11.163 +It is recommended that, if possible,
  11.164 +you base your own ordering relations on this theory.%
  11.165 +\end{isamarkuptext}%
  11.166 +%
  11.167 +\isamarkupsubsubsection{Inconsistencies}
  11.168 +%
  11.169 +\begin{isamarkuptext}%
  11.170 +The reader may be wondering what happens if we, maybe accidentally,
  11.171 +attach an inconsistent set of axioms to a class. So far we have always
  11.172 +avoided to add new axioms to HOL for fear of inconsistencies and suddenly it
  11.173 +seems that we are throwing all caution to the wind. So why is there no
  11.174 +problem?
  11.175 +
  11.176 +The point is that by construction, all type variables in the axioms of an
  11.177 +\isacommand{axclass} are automatically constrained with the class being
  11.178 +defined (as shown for axiom \isa{refl} above). These constraints are
  11.179 +always carried around and Isabelle takes care that they are never lost,
  11.180 +unless the type variable is instantiated with a type that has been shown to
  11.181 +belong to that class. Thus you may be able to prove \isa{False}
  11.182 +from your axioms, but Isabelle will remind you that this
  11.183 +theorem has the hidden hypothesis that the class is non-empty.%
  11.184 +\end{isamarkuptext}%
  11.185 +\end{isabellebody}%
  11.186 +%%% Local Variables:
  11.187 +%%% mode: latex
  11.188 +%%% TeX-master: "root"
  11.189 +%%% End:
    12.1 --- a/doc-src/TutorialI/Types/document/Overloading.tex	Wed Oct 25 17:44:59 2000 +0200
    12.2 +++ b/doc-src/TutorialI/Types/document/Overloading.tex	Wed Oct 25 18:24:33 2000 +0200
    12.3 @@ -5,8 +5,11 @@
    12.4  \isacommand{by}\ intro{\isacharunderscore}classes%
    12.5  \begin{isamarkuptext}%
    12.6  \noindent
    12.7 -This means. Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
    12.8 -\isa{{\isacharless}{\isacharless}} on lists.%
    12.9 +This \isacommand{instance} declaration can be read like the declaration of
   12.10 +a function on types: the constructor \isa{list} maps types of class \isa{term}, i.e.\ all HOL types, to types of class \isa{ordrel}, i.e.\
   12.11 +if \isa{ty\ {\isacharcolon}{\isacharcolon}\ term} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}.
   12.12 +Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
   12.13 +\isa{{\isacharless}{\isacharless}} on lists:%
   12.14  \end{isamarkuptext}%
   12.15  \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
   12.16  prefix{\isacharunderscore}def{\isacharcolon}\isanewline
    13.1 --- a/doc-src/TutorialI/Types/document/Overloading0.tex	Wed Oct 25 17:44:59 2000 +0200
    13.2 +++ b/doc-src/TutorialI/Types/document/Overloading0.tex	Wed Oct 25 18:24:33 2000 +0200
    13.3 @@ -2,13 +2,16 @@
    13.4  \begin{isabellebody}%
    13.5  \def\isabellecontext{Overloading{\isadigit{0}}}%
    13.6  %
    13.7 +\begin{isamarkuptext}%
    13.8 +We start with a concept that is required for type classes but already
    13.9 +useful on its own: \emph{overloading}. Isabelle allows overloading: a
   13.10 +constant may have multiple definitions at non-overlapping types.%
   13.11 +\end{isamarkuptext}%
   13.12 +%
   13.13  \isamarkupsubsubsection{An initial example}
   13.14  %
   13.15  \begin{isamarkuptext}%
   13.16 -We start with a concept that is required for type classes but already
   13.17 -useful on its own: \emph{overloading}. Isabelle allows overloading: a
   13.18 -constant may have multiple definitions at non-overlapping types. For example,
   13.19 -if we want to introduce the notion of an \emph{inverse} at arbitrary types we
   13.20 +If we want to introduce the notion of an \emph{inverse} for arbitrary types we
   13.21  give it a polymorphic type%
   13.22  \end{isamarkuptext}%
   13.23  \isacommand{consts}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}%
   13.24 @@ -26,7 +29,7 @@
   13.25  two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a
   13.26  common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is
   13.27  benign because the type of \isa{inverse} becomes smaller: on the left it is
   13.28 -\isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and \isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that the definitions do
   13.29 +\isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and \isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that the definitions do
   13.30  intentionally define \isa{inverse} only at instances of its declared type
   13.31  \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses warnings to that effect.
   13.32  
    14.1 --- a/doc-src/TutorialI/Types/document/Overloading1.tex	Wed Oct 25 17:44:59 2000 +0200
    14.2 +++ b/doc-src/TutorialI/Types/document/Overloading1.tex	Wed Oct 25 18:24:33 2000 +0200
    14.3 @@ -7,30 +7,53 @@
    14.4  \begin{isamarkuptext}%
    14.5  We now start with the theory of ordering relations, which we want to phrase
    14.6  in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}: they have
    14.7 -been chosen to avoid clashes with \isa{{\isasymle}} and \isa{{\isacharless}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we
    14.8 +been chosen to avoid clashes with \isa{{\isacharless}} and \isa{{\isasymle}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we
    14.9  introduce the class \isa{ordrel}:%
   14.10  \end{isamarkuptext}%
   14.11  \isacommand{axclass}\ ordrel\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}%
   14.12  \begin{isamarkuptext}%
   14.13  \noindent
   14.14 +This introduces a new class \isa{ordrel} and makes it a subclass of
   14.15 +the predefined class \isa{term}\footnote{The quotes around \isa{term}
   14.16 +simply avoid the clash with the command \isacommand{term}.}; \isa{term}
   14.17 +is the class of all HOL types, like ``Object'' in Java.
   14.18  This is a degenerate form of axiomatic type class without any axioms.
   14.19  Its sole purpose is to restrict the use of overloaded constants to meaningful
   14.20  instances:%
   14.21  \end{isamarkuptext}%
   14.22 -\isacommand{consts}\isanewline
   14.23 -\ \ {\isachardoublequote}{\isacharless}{\isacharless}{\isachardoublequote}\ \ \ \ \ \ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
   14.24 -\ \ {\isachardoublequote}{\isacharless}{\isacharless}{\isacharequal}{\isachardoublequote}\ \ \ \ \ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
   14.25 -\isanewline
   14.26 -\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel\isanewline
   14.27 -\isacommand{by}\ intro{\isacharunderscore}classes\isanewline
   14.28 -\isanewline
   14.29 +\isacommand{consts}\ less\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharless}{\isacharless}{\isachardoublequote}\ \ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
   14.30 +\ \ \ \ \ \ \ le\ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharless}{\isacharless}{\isacharequal}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
   14.31 +\begin{isamarkuptext}%
   14.32 +\noindent
   14.33 +So far there is not a single type of class \isa{ordrel}. To breathe life
   14.34 +into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of
   14.35 +\isa{ordrel}:%
   14.36 +\end{isamarkuptext}%
   14.37 +\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel%
   14.38 +\begin{isamarkuptxt}%
   14.39 +\noindent
   14.40 +Command \isacommand{instance} actually starts a proof, namely that
   14.41 +\isa{bool} satisfies all axioms of \isa{ordrel}.
   14.42 +There are none, but we still need to finish that proof, which we do
   14.43 +by invoking a fixed predefined method:%
   14.44 +\end{isamarkuptxt}%
   14.45 +\isacommand{by}\ intro{\isacharunderscore}classes%
   14.46 +\begin{isamarkuptext}%
   14.47 +\noindent
   14.48 +More interesting \isacommand{instance} proofs will arise below
   14.49 +in the context of proper axiomatic type classes.
   14.50 +
   14.51 +Althoug terms like \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} are now legal, we still need to say
   14.52 +what the relation symbols actually mean at type \isa{bool}:%
   14.53 +\end{isamarkuptext}%
   14.54  \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
   14.55  le{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}P\ {\isacharless}{\isacharless}{\isacharequal}\ Q\ {\isasymequiv}\ P\ {\isasymlongrightarrow}\ Q{\isachardoublequote}\isanewline
   14.56  less{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequote}%
   14.57  \begin{isamarkuptext}%
   14.58 -Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ False} is provable%
   14.59 +\noindent
   14.60 +Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable%
   14.61  \end{isamarkuptext}%
   14.62 -\isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ False{\isachardoublequote}\isanewline
   14.63 +\isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequote}\isanewline
   14.64  \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}%
   14.65  \begin{isamarkuptext}%
   14.66  \noindent
    15.1 --- a/doc-src/TutorialI/Types/document/Overloading2.tex	Wed Oct 25 17:44:59 2000 +0200
    15.2 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Wed Oct 25 18:24:33 2000 +0200
    15.3 @@ -4,7 +4,9 @@
    15.4  %
    15.5  \begin{isamarkuptext}%
    15.6  Of course this is not the only possible definition of the two relations.
    15.7 -Componentwise%
    15.8 +Componentwise comparison of lists of equal length also makes sense. This time
    15.9 +the elements of the list must also be of class \isa{ordrel} to permit their
   15.10 +comparison:%
   15.11  \end{isamarkuptext}%
   15.12  \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
   15.13  \isacommand{by}\ intro{\isacharunderscore}classes\isanewline
   15.14 @@ -13,11 +15,11 @@
   15.15  le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline
   15.16  \ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}%
   15.17  \begin{isamarkuptext}%
   15.18 +\noindent
   15.19 +The infix function \isa{{\isacharbang}} yields the nth element of a list.
   15.20  %However, we retract the componetwise comparison of lists and return
   15.21 -
   15.22 -Note: only one definition because based on name.%
   15.23 +%Note: only one definition because based on name.%
   15.24  \end{isamarkuptext}%
   15.25 -\isanewline
   15.26  \end{isabellebody}%
   15.27  %%% Local Variables:
   15.28  %%% mode: latex
    16.1 --- a/doc-src/TutorialI/Types/types.tex	Wed Oct 25 17:44:59 2000 +0200
    16.2 +++ b/doc-src/TutorialI/Types/types.tex	Wed Oct 25 18:24:33 2000 +0200
    16.3 @@ -42,10 +42,7 @@
    16.4  
    16.5  \index{overloading|)}
    16.6  
    16.7 -Finally we should remind our readers that \isa{Main} contains a much more
    16.8 -developed theory of orderings phrased in terms of the usual $\leq$ and
    16.9 -\isa{<}. It is recommended that, if possible, you base your own
   16.10 -ordering relations on this theory.
   16.11 +\input{Types/document/Axioms}
   16.12  
   16.13  \index{axiomatic type class|)}
   16.14  \index{*axclass|)}
    17.1 --- a/doc-src/TutorialI/appendix.tex	Wed Oct 25 17:44:59 2000 +0200
    17.2 +++ b/doc-src/TutorialI/appendix.tex	Wed Oct 25 18:24:33 2000 +0200
    17.3 @@ -16,7 +16,7 @@
    17.4  \indexboldpos{\isasymImp}{$IsaImp} &
    17.5  \ttindexboldpos{==>}{$IsaImp} &
    17.6  \verb$\<Longrightarrow>$ \\
    17.7 -\indexboldpos{\isasymAnd}{$IsaAnd} &
    17.8 +\isasymAnd\index{$IsaAnd@\isasymAnd|bold}&
    17.9  \texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
   17.10  \verb$\<And>$ \\
   17.11  \indexboldpos{\isasymequiv}{$IsaEq} &
   17.12 @@ -80,10 +80,10 @@
   17.13  \indexboldpos{\isasyminter}{$HOL3Set1}&
   17.14  \ttindexbold{Int} &
   17.15  \verb$\<inter>$\\
   17.16 -\indexboldpos{\isasymUnion}{$HOL3Set2}&
   17.17 +\isasymUnion\index{$HOL3Set2@\isasymUnion|bold}&
   17.18  \ttindexbold{UN}, \ttindexbold{Union} &
   17.19  \verb$\<Union>$\\
   17.20 -\indexboldpos{\isasymInter}{$HOL3Set2}&
   17.21 +\isasymInter\index{$HOL3Set2@\isasymInter|bold}&
   17.22  \ttindexbold{INT}, \ttindexbold{Inter} &
   17.23  \verb$\<Inter>$\\
   17.24  \hline