# HG changeset patch # User nipkow # Date 972491073 -7200 # Node ID bf33cbd76c050991ece116e46ff646135749052c # Parent 19214ac381cf45210f580f40c68e6e32bffa6aa8 *** empty log message *** diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/IsaMakefile --- a/doc-src/TutorialI/IsaMakefile Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/IsaMakefile Wed Oct 25 18:24:33 2000 +0200 @@ -4,7 +4,7 @@ ## targets -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 +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 images: test: all: default @@ -138,6 +138,16 @@ @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive @rm -f tutorial.dvi +## HOL-Types + +HOL-Types: HOL $(LOG)/HOL-Types.gz + +$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \ + Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \ + Types/Overloading.thy Types/Axioms.thy + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Types + @rm -f tutorial.dvi + ## HOL-Misc HOL-Misc: HOL $(LOG)/HOL-Misc.gz @@ -154,4 +164,4 @@ ## clean clean: - @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 + @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 diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Misc/AdvancedInd.thy --- a/doc-src/TutorialI/Misc/AdvancedInd.thy Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Wed Oct 25 18:24:33 2000 +0200 @@ -57,6 +57,7 @@ text{*\noindent This time, induction leaves us with the following base case +%{goals[goals_limit=1,display]} \begin{isabelle} \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] \end{isabelle} diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Misc/document/AdvancedInd.tex --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Oct 25 18:24:33 2000 +0200 @@ -54,6 +54,7 @@ \begin{isamarkuptext}% \noindent This time, induction leaves us with the following base case +%{goals[goals_limit=1,display]} \begin{isabelle} \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] \end{isabelle} diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/ToyList/ToyList.thy --- a/doc-src/TutorialI/ToyList/ToyList.thy Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Wed Oct 25 18:24:33 2000 +0200 @@ -184,8 +184,8 @@ The induction step is an example of the general format of a subgoal: \begin{isabelle} -~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} -\end{isabelle} +~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} +\end{isabelle}\index{$IsaAnd@\isasymAnd|bold} The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be ignored most of the time, or simply treated as a list of variables local to this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}. diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Oct 25 18:24:33 2000 +0200 @@ -179,8 +179,8 @@ The induction step is an example of the general format of a subgoal: \begin{isabelle} -~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} -\end{isabelle} +~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} +\end{isabelle}\index{$IsaAnd@\isasymAnd|bold} The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be ignored most of the time, or simply treated as a list of variables local to this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}. diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Types/Axioms.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Types/Axioms.thy Wed Oct 25 18:24:33 2000 +0200 @@ -0,0 +1,202 @@ +(*<*)theory Axioms = Overloading:(*>*) + +subsection{*Axioms*} + + +text{*Now we want to attach axioms to our classes. Then we can reason on the +level of classes and the results will be applicable to all types in a class, +just as in axiomatic mathematics. These ideas are demonstrated by means of +our above ordering relations. +*} + +subsubsection{*Partial orders*} + +text{* +A \emph{partial order} is a subclass of @{text ordrel} +where certain axioms need to hold: +*} + +axclass parord < ordrel +refl: "x <<= x" +trans: "\ x <<= y; y <<= z \ \ x <<= z" +antisym: "\ x <<= y; y <<= x \ \ x = y" +less_le: "x << y = (x <<= y \ x \ y)" + +text{*\noindent +The first three axioms are the familiar ones, and the final one +requires that @{text"<<"} and @{text"<<="} are related as expected. +Note that behind the scenes, Isabelle has restricted the axioms to class +@{text parord}. For example, this is what @{thm[source]refl} really looks like: +@{thm[show_types]refl}. + +We can now prove simple theorems in this abstract setting, for example +that @{text"<<"} is not symmetric: +*} + +lemma [simp]: "(x::'a::parord) << y \ (\ y << x) = True"; + +txt{*\noindent +The conclusion is not simply @{prop"\ y << x"} because the preprocessor +of the simplifier would turn this into @{prop"y << x = False"}, thus yielding +a nonterminating rewrite rule. In the above form it is a generally useful +rule. +The type constraint is necessary because otherwise Isabelle would only assume +@{text"'a::ordrel"} (as required in the type of @{text"<<"}), in +which case the proposition is not a theorem. The proof is easy: +*} + +by(simp add:less_le antisym); + +text{* We could now continue in this vein and develop a whole theory of +results about partial orders. Eventually we will want to apply these results +to concrete types, namely the instances of the class. Thus we first need to +prove that the types in question, for example @{typ bool}, are indeed +instances of @{text parord}:*} + +instance bool :: parord +apply intro_classes; + +txt{*\noindent +This time @{text intro_classes} leaves us with the four axioms, +specialized to type @{typ bool}, as subgoals: +@{goals[display,show_types,indent=0]} +Fortunately, the proof is easy for blast, once we have unfolded the definitions +of @{text"<<"} and @{text"<<="} at @{typ bool}: +*} + +apply(simp_all (no_asm_use) only: le_bool_def less_bool_def); +by(blast, blast, blast, blast); + +text{*\noindent +Can you figure out why we have to include @{text"(no_asm_use)"}? + +We can now apply our single lemma above in the context of booleans: +*} + +lemma "(P::bool) << Q \ \(Q << P)"; +by simp; + +text{*\noindent +The effect is not stunning but demonstrates the principle. It also shows +that tools like the simplifier can deal with generic rules as well. Moreover, +it should be clear that the main advantage of the axiomatic method is that +theorems can be proved in the abstract and one does not need to repeat the +proof for each instance. +*} + +subsubsection{*Linear orders*} + +text{* If any two elements of a partial order are comparable it is a +\emph{linear} or \emph{total} order: *} + +axclass linord < parord +total: "x <<= y \ y <<= x" + +text{*\noindent +By construction, @{text linord} inherits all axioms from @{text parord}. +Therefore we can show that totality can be expressed in terms of @{text"<<"} +as follows: +*} + +lemma "\x::'a::linord. x< x=y \ y< x << x" +less_trans: "\ x << y; y << z \ \ x << z" +le_less: "x <<= y = (x << y \ x = y)" + +text{*\noindent +It is well known that partial orders are the same as strict orders. Let us +prove one direction, namely that partial orders are a subclass of strict +orders. The proof follows the ususal pattern: *} + +instance parord < strord +apply intro_classes; +apply(simp_all (no_asm_use) add:less_le); + apply(blast intro: trans antisym); + apply(blast intro: refl); +done + +text{*\noindent +The result is the following subclass diagram: +\[ +\begin{array}{c} +\isa{term}\\ +|\\ +\isa{ordrel}\\ +|\\ +\isa{strord}\\ +|\\ +\isa{parord} +\end{array} +\] + +In general, the subclass diagram must be acyclic. Therefore Isabelle will +complain if you also prove the relationship @{text"strord < parord"}. +Multiple inheritance is however permitted. + +This finishes our demonstration of type classes based on orderings. We +remind our readers that \isa{Main} contains a much more developed theory of +orderings phrased in terms of the usual @{text"\"} and @{text"<"}. +It is recommended that, if possible, +you base your own ordering relations on this theory. +*} + +(* +instance strord < parord +apply intro_classes; +apply(simp_all (no_asm_use) add:le_less); +apply(blast intro: less_trans); +apply(erule disjE); +apply(erule disjE); +apply(rule irrefl[THEN notE]); +apply(rule less_trans, assumption, assumption); +apply blast;apply blast; +apply(blast intro: irrefl[THEN notE]); +done +*) + +subsubsection{*Inconsistencies*} + +text{* The reader may be wondering what happens if we, maybe accidentally, +attach an inconsistent set of axioms to a class. So far we have always +avoided to add new axioms to HOL for fear of inconsistencies and suddenly it +seems that we are throwing all caution to the wind. So why is there no +problem? + +The point is that by construction, all type variables in the axioms of an +\isacommand{axclass} are automatically constrained with the class being +defined (as shown for axiom @{thm[source]refl} above). These constraints are +always carried around and Isabelle takes care that they are never lost, +unless the type variable is instantiated with a type that has been shown to +belong to that class. Thus you may be able to prove @{prop False} +from your axioms, but Isabelle will remind you that this +theorem has the hidden hypothesis that the class is non-empty. +*} + +(* +axclass false<"term" +false: "x \ x"; + +lemma "False"; +by(rule notE[OF false HOL.refl]); +*) +(*<*)end(*>*) diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Types/Overloading.thy --- a/doc-src/TutorialI/Types/Overloading.thy Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/Types/Overloading.thy Wed Oct 25 18:24:33 2000 +0200 @@ -3,8 +3,12 @@ by intro_classes text{*\noindent -This means. Of course we should also define the meaning of @{text <<=} and -@{text <<} on lists. +This \isacommand{instance} declaration can be read like the declaration of +a function on types: the constructor @{text list} maps types of class @{text +term}, i.e.\ all HOL types, to types of class @{text ordrel}, i.e.\ +if @{text"ty :: term"} then @{text"ty list :: ordrel"}. +Of course we should also define the meaning of @{text <<=} and +@{text <<} on lists: *} defs (overloaded) diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Types/Overloading0.thy --- a/doc-src/TutorialI/Types/Overloading0.thy Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/Types/Overloading0.thy Wed Oct 25 18:24:33 2000 +0200 @@ -1,11 +1,13 @@ (*<*)theory Overloading0 = Main:(*>*) +text{* We start with a concept that is required for type classes but already +useful on its own: \emph{overloading}. Isabelle allows overloading: a +constant may have multiple definitions at non-overlapping types. *} + subsubsection{*An initial example*} -text{* We start with a concept that is required for type classes but already -useful on its own: \emph{overloading}. Isabelle allows overloading: a -constant may have multiple definitions at non-overlapping types. For example, -if we want to introduce the notion of an \emph{inverse} at arbitrary types we +text{* +If we want to introduce the notion of an \emph{inverse} for arbitrary types we give it a polymorphic type *} consts inverse :: "'a \ 'a" @@ -25,7 +27,7 @@ common instance. What is more, the recursion in @{thm[source]inverse_pair} is benign because the type of @{term inverse} becomes smaller: on the left it is @{typ"'a \ 'b \ 'a \ 'b"} but on the right @{typ"'a \ 'a"} and @{typ"'b \ -'b"}. The @{text"(overloaded)"} tells Isabelle that the definitions do +'b"}. The annotation @{text"(overloaded)"} tells Isabelle that the definitions do intentionally define @{term inverse} only at instances of its declared type @{typ"'a \ 'a"} --- this merely supresses warnings to that effect. diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Types/Overloading1.thy --- a/doc-src/TutorialI/Types/Overloading1.thy Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/Types/Overloading1.thy Wed Oct 25 18:24:33 2000 +0200 @@ -5,7 +5,7 @@ text{* We now start with the theory of ordering relations, which we want to phrase in terms of the two binary symbols @{text"<<"} and @{text"<<="}: they have -been chosen to avoid clashes with @{text"\"} and @{text"<"} in theory @{text +been chosen to avoid clashes with @{text"<"} and @{text"\"} in theory @{text Main}. To restrict the application of @{text"<<"} and @{text"<<="} we introduce the class @{text ordrel}: *} @@ -13,27 +13,52 @@ axclass ordrel < "term" text{*\noindent +This introduces a new class @{text ordrel} and makes it a subclass of +the predefined class @{text term}\footnote{The quotes around @{text term} +simply avoid the clash with the command \isacommand{term}.}; @{text term} +is the class of all HOL types, like ``Object'' in Java. This is a degenerate form of axiomatic type class without any axioms. Its sole purpose is to restrict the use of overloaded constants to meaningful instances: *} -consts - "<<" :: "('a::ordrel) \ 'a \ bool" (infixl 50) - "<<=" :: "('a::ordrel) \ 'a \ bool" (infixl 50) +consts less :: "('a::ordrel) \ 'a \ bool" (infixl "<<" 50) + le :: "('a::ordrel) \ 'a \ bool" (infixl "<<=" 50) + +text{*\noindent +So far there is not a single type of class @{text ordrel}. To breathe life +into @{text ordrel} we need to declare a type to be an \bfindex{instance} of +@{text ordrel}: +*} instance bool :: ordrel + +txt{*\noindent +Command \isacommand{instance} actually starts a proof, namely that +@{typ bool} satisfies all axioms of @{text ordrel}. +There are none, but we still need to finish that proof, which we do +by invoking a fixed predefined method: +*} + by intro_classes +text{*\noindent +More interesting \isacommand{instance} proofs will arise below +in the context of proper axiomatic type classes. + +Althoug terms like @{prop"False <<= P"} are now legal, we still need to say +what the relation symbols actually mean at type @{typ bool}: +*} + defs (overloaded) le_bool_def: "P <<= Q \ P \ Q" less_bool_def: "P << Q \ \P \ Q" -text{* -Now @{prop"False <<= False"} is provable +text{*\noindent +Now @{prop"False <<= P"} is provable *} -lemma "False <<= False" +lemma "False <<= P" by(simp add: le_bool_def) text{*\noindent diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Types/Overloading2.thy --- a/doc-src/TutorialI/Types/Overloading2.thy Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/Types/Overloading2.thy Wed Oct 25 18:24:33 2000 +0200 @@ -2,7 +2,9 @@ text{* Of course this is not the only possible definition of the two relations. -Componentwise +Componentwise comparison of lists of equal length also makes sense. This time +the elements of the list must also be of class @{text ordrel} to permit their +comparison: *} instance list :: (ordrel)ordrel @@ -12,10 +14,8 @@ le_list_def: "xs <<= (ys::'a::ordrel list) \ size xs = size ys \ (\i*) - +%Note: only one definition because based on name. +*}(*<*)end(*>*) diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Types/document/Axioms.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Types/document/Axioms.tex Wed Oct 25 18:24:33 2000 +0200 @@ -0,0 +1,186 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Axioms}% +% +\isamarkupsubsection{Axioms} +% +\begin{isamarkuptext}% +Now we want to attach axioms to our classes. Then we can reason on the +level of classes and the results will be applicable to all types in a class, +just as in axiomatic mathematics. These ideas are demonstrated by means of +our above ordering relations.% +\end{isamarkuptext}% +% +\isamarkupsubsubsection{Partial orders} +% +\begin{isamarkuptext}% +A \emph{partial order} is a subclass of \isa{ordrel} +where certain axioms need to hold:% +\end{isamarkuptext}% +\isacommand{axclass}\ parord\ {\isacharless}\ ordrel\isanewline +refl{\isacharcolon}\ \ \ \ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}\isanewline +trans{\isacharcolon}\ \ \ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isachardoublequote}\isanewline +antisym{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequote}\isanewline +less{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequote}% +\begin{isamarkuptext}% +\noindent +The first three axioms are the familiar ones, and the final one +requires that \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} are related as expected. +Note that behind the scenes, Isabelle has restricted the axioms to class +\isa{parord}. For example, this is what \isa{refl} really looks like: +\isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}. + +We can now prove simple theorems in this abstract setting, for example +that \isa{{\isacharless}{\isacharless}} is not symmetric:% +\end{isamarkuptext}% +\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}% +\begin{isamarkuptxt}% +\noindent +The conclusion is not simply \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the preprocessor +of the simplifier would turn this into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, thus yielding +a nonterminating rewrite rule. In the above form it is a generally useful +rule. +The type constraint is necessary because otherwise Isabelle would only assume +\isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}), in +which case the proposition is not a theorem. The proof is easy:% +\end{isamarkuptxt}% +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}less{\isacharunderscore}le\ antisym{\isacharparenright}% +\begin{isamarkuptext}% +We could now continue in this vein and develop a whole theory of +results about partial orders. Eventually we will want to apply these results +to concrete types, namely the instances of the class. Thus we first need to +prove that the types in question, for example \isa{bool}, are indeed +instances of \isa{parord}:% +\end{isamarkuptext}% +\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ parord\isanewline +\isacommand{apply}\ intro{\isacharunderscore}classes% +\begin{isamarkuptxt}% +\noindent +This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms, +specialized to type \isa{bool}, as subgoals: +\begin{isabelle}% +OFCLASS{\isacharparenleft}bool{\isacharcomma}\ parord{\isacharunderscore}class{\isacharparenright}\isanewline +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline +\ {\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 +\ {\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 +\ {\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}% +\end{isabelle} +Fortunately, the proof is easy for blast, once we have unfolded the definitions +of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at \isa{bool}:% +\end{isamarkuptxt}% +\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 +\isacommand{by}{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}% +\begin{isamarkuptext}% +\noindent +Can you figure out why we have to include \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}? + +We can now apply our single lemma above in the context of booleans:% +\end{isamarkuptext}% +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{by}\ simp% +\begin{isamarkuptext}% +\noindent +The effect is not stunning but demonstrates the principle. It also shows +that tools like the simplifier can deal with generic rules as well. Moreover, +it should be clear that the main advantage of the axiomatic method is that +theorems can be proved in the abstract and one does not need to repeat the +proof for each instance.% +\end{isamarkuptext}% +% +\isamarkupsubsubsection{Linear orders} +% +\begin{isamarkuptext}% +If any two elements of a partial order are comparable it is a +\emph{linear} or \emph{total} order:% +\end{isamarkuptext}% +\isacommand{axclass}\ linord\ {\isacharless}\ parord\isanewline +total{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}% +\begin{isamarkuptext}% +\noindent +By construction, \isa{linord} inherits all axioms from \isa{parord}. +Therefore we can show that totality can be expressed in terms of \isa{{\isacharless}{\isacharless}} +as follows:% +\end{isamarkuptext}% +\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 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}insert\ total{\isacharparenright}\isanewline +\isacommand{apply}\ blast\isanewline +\isacommand{done}% +\begin{isamarkuptext}% +Linear orders are an example of subclassing by construction, which is the most +common case. It is also possible to prove additional subclass relationships +later on, i.e.\ subclassing by proof. This is the topic of the following +section.% +\end{isamarkuptext}% +% +\isamarkupsubsubsection{Strict orders} +% +\begin{isamarkuptext}% +An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than +\isa{{\isacharless}{\isacharless}{\isacharequal}} as the primary concept. The result is a \emph{strict} order:% +\end{isamarkuptext}% +\isacommand{axclass}\ strord\ {\isacharless}\ ordrel\isanewline +irrefl{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isasymnot}\ x\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline +less{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z{\isachardoublequote}\isanewline +le{\isacharunderscore}less{\isacharcolon}\ \ \ \ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}% +\begin{isamarkuptext}% +\noindent +It is well known that partial orders are the same as strict orders. Let us +prove one direction, namely that partial orders are a subclass of strict +orders. The proof follows the ususal pattern:% +\end{isamarkuptext}% +\isacommand{instance}\ parord\ {\isacharless}\ strord\isanewline +\isacommand{apply}\ intro{\isacharunderscore}classes\isanewline +\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}less{\isacharunderscore}le{\isacharparenright}\isanewline +\ \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline +\isacommand{done}% +\begin{isamarkuptext}% +\noindent +The result is the following subclass diagram: +\[ +\begin{array}{c} +\isa{term}\\ +|\\ +\isa{ordrel}\\ +|\\ +\isa{strord}\\ +|\\ +\isa{parord} +\end{array} +\] + +In general, the subclass diagram must be acyclic. Therefore Isabelle will +complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}. +Multiple inheritance is however permitted. + +This finishes our demonstration of type classes based on orderings. We +remind our readers that \isa{Main} contains a much more developed theory of +orderings phrased in terms of the usual \isa{{\isasymle}} and \isa{{\isacharless}}. +It is recommended that, if possible, +you base your own ordering relations on this theory.% +\end{isamarkuptext}% +% +\isamarkupsubsubsection{Inconsistencies} +% +\begin{isamarkuptext}% +The reader may be wondering what happens if we, maybe accidentally, +attach an inconsistent set of axioms to a class. So far we have always +avoided to add new axioms to HOL for fear of inconsistencies and suddenly it +seems that we are throwing all caution to the wind. So why is there no +problem? + +The point is that by construction, all type variables in the axioms of an +\isacommand{axclass} are automatically constrained with the class being +defined (as shown for axiom \isa{refl} above). These constraints are +always carried around and Isabelle takes care that they are never lost, +unless the type variable is instantiated with a type that has been shown to +belong to that class. Thus you may be able to prove \isa{False} +from your axioms, but Isabelle will remind you that this +theorem has the hidden hypothesis that the class is non-empty.% +\end{isamarkuptext}% +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Types/document/Overloading.tex --- a/doc-src/TutorialI/Types/document/Overloading.tex Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/Types/document/Overloading.tex Wed Oct 25 18:24:33 2000 +0200 @@ -5,8 +5,11 @@ \isacommand{by}\ intro{\isacharunderscore}classes% \begin{isamarkuptext}% \noindent -This means. Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and -\isa{{\isacharless}{\isacharless}} on lists.% +This \isacommand{instance} declaration can be read like the declaration of +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.\ +if \isa{ty\ {\isacharcolon}{\isacharcolon}\ term} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}. +Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and +\isa{{\isacharless}{\isacharless}} on lists:% \end{isamarkuptext}% \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline prefix{\isacharunderscore}def{\isacharcolon}\isanewline diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Types/document/Overloading0.tex --- a/doc-src/TutorialI/Types/document/Overloading0.tex Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/Types/document/Overloading0.tex Wed Oct 25 18:24:33 2000 +0200 @@ -2,13 +2,16 @@ \begin{isabellebody}% \def\isabellecontext{Overloading{\isadigit{0}}}% % +\begin{isamarkuptext}% +We start with a concept that is required for type classes but already +useful on its own: \emph{overloading}. Isabelle allows overloading: a +constant may have multiple definitions at non-overlapping types.% +\end{isamarkuptext}% +% \isamarkupsubsubsection{An initial example} % \begin{isamarkuptext}% -We start with a concept that is required for type classes but already -useful on its own: \emph{overloading}. Isabelle allows overloading: a -constant may have multiple definitions at non-overlapping types. For example, -if we want to introduce the notion of an \emph{inverse} at arbitrary types we +If we want to introduce the notion of an \emph{inverse} for arbitrary types we give it a polymorphic type% \end{isamarkuptext}% \isacommand{consts}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}% @@ -26,7 +29,7 @@ two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is benign because the type of \isa{inverse} becomes smaller: on the left it is -\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 +\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 intentionally define \isa{inverse} only at instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses warnings to that effect. diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Types/document/Overloading1.tex --- a/doc-src/TutorialI/Types/document/Overloading1.tex Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/Types/document/Overloading1.tex Wed Oct 25 18:24:33 2000 +0200 @@ -7,30 +7,53 @@ \begin{isamarkuptext}% We now start with the theory of ordering relations, which we want to phrase in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}: they have -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 +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 introduce the class \isa{ordrel}:% \end{isamarkuptext}% \isacommand{axclass}\ ordrel\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}% \begin{isamarkuptext}% \noindent +This introduces a new class \isa{ordrel} and makes it a subclass of +the predefined class \isa{term}\footnote{The quotes around \isa{term} +simply avoid the clash with the command \isacommand{term}.}; \isa{term} +is the class of all HOL types, like ``Object'' in Java. This is a degenerate form of axiomatic type class without any axioms. Its sole purpose is to restrict the use of overloaded constants to meaningful instances:% \end{isamarkuptext}% -\isacommand{consts}\isanewline -\ \ {\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 -\ \ {\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 -\isanewline -\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel\isanewline -\isacommand{by}\ intro{\isacharunderscore}classes\isanewline -\isanewline +\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 +\ \ \ \ \ \ \ 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}% +\begin{isamarkuptext}% +\noindent +So far there is not a single type of class \isa{ordrel}. To breathe life +into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of +\isa{ordrel}:% +\end{isamarkuptext}% +\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel% +\begin{isamarkuptxt}% +\noindent +Command \isacommand{instance} actually starts a proof, namely that +\isa{bool} satisfies all axioms of \isa{ordrel}. +There are none, but we still need to finish that proof, which we do +by invoking a fixed predefined method:% +\end{isamarkuptxt}% +\isacommand{by}\ intro{\isacharunderscore}classes% +\begin{isamarkuptext}% +\noindent +More interesting \isacommand{instance} proofs will arise below +in the context of proper axiomatic type classes. + +Althoug terms like \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} are now legal, we still need to say +what the relation symbols actually mean at type \isa{bool}:% +\end{isamarkuptext}% \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline le{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}P\ {\isacharless}{\isacharless}{\isacharequal}\ Q\ {\isasymequiv}\ P\ {\isasymlongrightarrow}\ Q{\isachardoublequote}\isanewline less{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequote}% \begin{isamarkuptext}% -Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ False} is provable% +\noindent +Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable% \end{isamarkuptext}% -\isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ False{\isachardoublequote}\isanewline +\isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequote}\isanewline \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptext}% \noindent diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Types/document/Overloading2.tex --- a/doc-src/TutorialI/Types/document/Overloading2.tex Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex Wed Oct 25 18:24:33 2000 +0200 @@ -4,7 +4,9 @@ % \begin{isamarkuptext}% Of course this is not the only possible definition of the two relations. -Componentwise% +Componentwise comparison of lists of equal length also makes sense. This time +the elements of the list must also be of class \isa{ordrel} to permit their +comparison:% \end{isamarkuptext}% \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline \isacommand{by}\ intro{\isacharunderscore}classes\isanewline @@ -13,11 +15,11 @@ le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% +\noindent +The infix function \isa{{\isacharbang}} yields the nth element of a list. %However, we retract the componetwise comparison of lists and return - -Note: only one definition because based on name.% +%Note: only one definition because based on name.% \end{isamarkuptext}% -\isanewline \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/Types/types.tex --- a/doc-src/TutorialI/Types/types.tex Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/Types/types.tex Wed Oct 25 18:24:33 2000 +0200 @@ -42,10 +42,7 @@ \index{overloading|)} -Finally we should remind our readers that \isa{Main} contains a much more -developed theory of orderings phrased in terms of the usual $\leq$ and -\isa{<}. It is recommended that, if possible, you base your own -ordering relations on this theory. +\input{Types/document/Axioms} \index{axiomatic type class|)} \index{*axclass|)} diff -r 19214ac381cf -r bf33cbd76c05 doc-src/TutorialI/appendix.tex --- a/doc-src/TutorialI/appendix.tex Wed Oct 25 17:44:59 2000 +0200 +++ b/doc-src/TutorialI/appendix.tex Wed Oct 25 18:24:33 2000 +0200 @@ -16,7 +16,7 @@ \indexboldpos{\isasymImp}{$IsaImp} & \ttindexboldpos{==>}{$IsaImp} & \verb$\$ \\ -\indexboldpos{\isasymAnd}{$IsaAnd} & +\isasymAnd\index{$IsaAnd@\isasymAnd|bold}& \texttt{!!}\index{$IsaAnd@\ttAnd|bold} & \verb$\$ \\ \indexboldpos{\isasymequiv}{$IsaEq} & @@ -80,10 +80,10 @@ \indexboldpos{\isasyminter}{$HOL3Set1}& \ttindexbold{Int} & \verb$\$\\ -\indexboldpos{\isasymUnion}{$HOL3Set2}& +\isasymUnion\index{$HOL3Set2@\isasymUnion|bold}& \ttindexbold{UN}, \ttindexbold{Union} & \verb$\$\\ -\indexboldpos{\isasymInter}{$HOL3Set2}& +\isasymInter\index{$HOL3Set2@\isasymInter|bold}& \ttindexbold{INT}, \ttindexbold{Inter} & \verb$\$\\ \hline