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