--- a/doc-src/TutorialI/Types/Axioms.thy Wed Jun 17 10:07:23 2009 +0200
+++ b/doc-src/TutorialI/Types/Axioms.thy Wed Jun 17 10:07:25 2009 +0200
@@ -1,258 +1,262 @@
-(*<*)theory Axioms imports Overloading begin(*>*)
+(*<*)theory Axioms imports Overloading Setup begin(*>*)
+
+subsection {* Axioms *}
+
+text {* Attaching axioms to our classes lets us reason on the level of
+classes. The results will be applicable to all types in a class, just
+as in axiomatic mathematics.
+
+\begin{warn}
+Proofs in this section use structured \emph{Isar} proofs, which are not
+covered in this tutorial; but see \cite{Nipkow-TYPES02}.%
+\end{warn} *}
+
+subsubsection {* Semigroups *}
+
+text{* We specify \emph{semigroups} as subclass of @{class plus}
+where certain axioms need to hold: *}
+
+class semigroup = plus +
+ assumes assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
+
+text {* \noindent This @{command class} specification requires that
+all instances of @{class semigroup} obey @{fact "assoc:"}~@{prop
+[source] "\<And>x y z \<Colon> 'a\<Colon>semigroup. (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"}.
-subsection{*Axioms*}
+We can use this class axiom to derive further abstract theorems
+relative to class @{class semigroup}: *}
+
+lemma assoc_left:
+ fixes x y z :: "'a\<Colon>semigroup"
+ shows "x \<oplus> (y \<oplus> z) = (x \<oplus> y) \<oplus> z"
+ using assoc by (rule sym)
+
+text {* \noindent The @{class semigroup} constraint on type @{typ
+"'a"} restricts instantiations of @{typ "'a"} to types of class
+@{class semigroup} and during the proof enables us to use the fact
+@{fact assoc} whose type parameter is itself constrained to class
+@{class semigroup}. The main advantage is that theorems can be proved
+in the abstract and freely reused for each instance.
+
+On instantiation, we have to give a proof that the given operations
+obey the class axioms: *}
+
+instantiation nat :: semigroup
+begin
+
+instance proof
+
+txt {* \noindent The proof opens with a default proof step, which for
+instance judgements invokes method @{method intro_classes}. *}
-text{*Attaching axioms to our classes lets us reason on the
-level of classes. The results will be applicable to all types in a class,
-just as in axiomatic mathematics. These ideas are demonstrated by means of
-our ordering relations.
-*}
-
-subsubsection{*Partial Orders*}
+ fix m n q :: nat
+ show "(m \<oplus> n) \<oplus> q = m \<oplus> (n \<oplus> q)"
+ by (induct m) simp_all
+qed
-text{*
-A \emph{partial order} is a subclass of @{text ordrel}
-where certain axioms need to hold:
-*}
+end
-axclass parord < ordrel
-refl: "x <<= x"
-trans: "\<lbrakk> x <<= y; y <<= z \<rbrakk> \<Longrightarrow> x <<= z"
-antisym: "\<lbrakk> x <<= y; y <<= x \<rbrakk> \<Longrightarrow> x = y"
-lt_le: "x << y = (x <<= y \<and> x \<noteq> y)"
+text {* \noindent Again, the interesting things enter the stage with
+parametric types: *}
+
+instantiation * :: (semigroup, semigroup) semigroup
+begin
-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, the axiom @{thm[source]refl} really is
-@{thm[show_sorts]refl}.
+instance proof
+ fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup"
+ show "p\<^isub>1 \<oplus> p\<^isub>2 \<oplus> p\<^isub>3 = p\<^isub>1 \<oplus> (p\<^isub>2 \<oplus> p\<^isub>3)"
+ by (cases p\<^isub>1, cases p\<^isub>2, cases p\<^isub>3) (simp add: assoc)
-We have not made @{thm[source] lt_le} a global definition because it would
-fix once and for all that @{text"<<"} is defined in terms of @{text"<<="} and
-never the other way around. Below you will see why we want to avoid this
-asymmetry. The drawback of our choice is that
-we need to define both @{text"<<="} and @{text"<<"} for each instance.
+txt {* \noindent Associativity of product semigroups is established
+using the hypothetical associativity @{fact assoc} of the type
+components, which holds due to the @{class semigroup} constraints
+imposed on the type components by the @{command instance} proposition.
+Indeed, this pattern often occurs with parametric types and type
+classes. *}
-We can now prove simple theorems in this abstract setting, for example
-that @{text"<<"} is not symmetric:
-*}
+qed
-lemma [simp]: "(x::'a::parord) << y \<Longrightarrow> (\<not> y << x) = True";
+end
+
+subsubsection {* Monoids *}
-txt{*\noindent
-The conclusion is not just @{prop"\<not> y << x"} because the
-simplifier's preprocessor (see \S\ref{sec:simp-preprocessor})
-would turn it into @{prop"y << x = False"}, yielding
-a nonterminating rewrite rule.
-(It would be used to try to prove its own precondition \emph{ad
- infinitum}.)
-In the form above, the rule is useful.
-The type constraint is necessary because otherwise Isabelle would only assume
-@{text"'a::ordrel"} (as required in the type of @{text"<<"}),
-when the proposition is not a theorem. The proof is easy:
-*}
+text {* We define a subclass @{text monoidl} (a semigroup with a
+left-hand neutral) by extending @{class semigroup} with one additional
+parameter @{text neutral} together with its property: *}
-by(simp add: lt_le antisym);
+class monoidl = semigroup +
+ fixes neutral :: "'a" ("\<zero>")
+ assumes neutl: "\<zero> \<oplus> x = x"
-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}:*}
+text {* \noindent Again, we prove some instances, by providing
+suitable parameter definitions and proofs for the additional
+specifications. *}
-instance bool :: parord
-apply intro_classes;
+instantiation nat :: monoidl
+begin
-txt{*\noindent
-This time @{text intro_classes} leaves us with the four axioms,
-specialized to type @{typ bool}, as subgoals:
-@{subgoals[display,show_types,indent=0]}
-Fortunately, the proof is easy for \isa{blast}
-once we have unfolded the definitions
-of @{text"<<"} and @{text"<<="} at type @{typ bool}:
-*}
-
-apply(simp_all (no_asm_use) only: le_bool_def lt_bool_def);
-by(blast, blast, blast, blast);
+definition
+ neutral_nat_def: "\<zero> = (0\<Colon>nat)"
-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:
-*}
+instance proof
+ fix n :: nat
+ show "\<zero> \<oplus> n = n"
+ unfolding neutral_nat_def by simp
+qed
-lemma "(P::bool) << Q \<Longrightarrow> \<not>(Q << P)";
-by simp;
+end
-text{*\noindent
-The effect is not stunning, but it demonstrates the principle. It also shows
-that tools like the simplifier can deal with generic rules.
-The main advantage of the axiomatic method is that
-theorems can be proved in the abstract and freely reused for each instance.
+text {* \noindent Unless in the above examples, we here have both
+specification of class operations and a non-trivial instance proof.
+
+This covers products as well:
*}
-subsubsection{*Linear Orders*}
+instantiation * :: (monoidl, monoidl) monoidl
+begin
-text{* If any two elements of a partial order are comparable it is a
-\textbf{linear} or \textbf{total} order: *}
-
-axclass linord < parord
-linear: "x <<= y \<or> y <<= x"
+definition
+ neutral_prod_def: "\<zero> = (\<zero>, \<zero>)"
-text{*\noindent
-By construction, @{text linord} inherits all axioms from @{text parord}.
-Therefore we can show that linearity can be expressed in terms of @{text"<<"}
-as follows:
-*}
+instance proof
+ fix p :: "'a\<Colon>monoidl \<times> 'b\<Colon>monoidl"
+ show "\<zero> \<oplus> p = p"
+ by (cases p) (simp add: neutral_prod_def neutl)
+qed
-lemma "\<And>x::'a::linord. x << y \<or> x = y \<or> y << x";
-apply(simp add: lt_le);
-apply(insert linear);
-apply blast;
-done
+end
-text{*
-Linear orders are an example of subclassing\index{subclasses}
-by construction, which is the most
-common case. Subclass relationships can also be proved.
-This is the topic of the following
-paragraph.
-*}
+text {* \noindent Fully-fledged monoids are modelled by another
+subclass which does not add new parameters but tightens the
+specification: *}
-subsubsection{*Strict Orders*}
+class monoid = monoidl +
+ assumes neutr: "x \<oplus> \<zero> = x"
-text{*
-An alternative axiomatization of partial orders takes @{text"<<"} rather than
-@{text"<<="} as the primary concept. The result is a \textbf{strict} order:
-*}
+text {* \noindent Corresponding instances for @{typ nat} and products
+are left as an exercise to the reader. *}
+
+subsubsection {* Groups *}
-axclass strord < ordrel
-irrefl: "\<not> x << x"
-lt_trans: "\<lbrakk> x << y; y << z \<rbrakk> \<Longrightarrow> x << z"
-le_less: "x <<= y = (x << y \<or> x = y)"
+text {* \noindent To finish our small algebra example, we add a @{text
+group} class: *}
-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. *}
-
-instance parord < strord
-apply intro_classes;
+class group = monoidl +
+ fixes inv :: "'a \<Rightarrow> 'a" ("\<div> _" [81] 80)
+ assumes invl: "\<div> x \<oplus> x = \<zero>"
-txt{*\noindent
-@{subgoals[display,show_sorts]}
-Because of @{text"'a :: parord"}, the three axioms of class @{text strord}
-are easily proved:
-*}
+text {* \noindent We continue with a further example for abstract
+proofs relative to type classes: *}
- apply(simp_all (no_asm_use) add: lt_le);
- apply(blast intro: trans antisym);
-apply(blast intro: refl);
-done
-
-text{*
-The subclass relation must always be acyclic. Therefore Isabelle will
-complain if you also prove the relationship @{text"strord < parord"}.
-*}
-
+lemma left_cancel:
+ fixes x y z :: "'a\<Colon>group"
+ shows "x \<oplus> y = x \<oplus> z \<longleftrightarrow> y = z"
+proof
+ assume "x \<oplus> y = x \<oplus> z"
+ then have "\<div> x \<oplus> (x \<oplus> y) = \<div> x \<oplus> (x \<oplus> z)" by simp
+ then have "(\<div> x \<oplus> x) \<oplus> y = (\<div> x \<oplus> x) \<oplus> z" by (simp add: assoc)
+ then show "y = z" by (simp add: invl neutl)
+next
+ assume "y = z"
+ then show "x \<oplus> y = x \<oplus> z" by simp
+qed
-(*
-instance strord < parord
-apply intro_classes;
-apply(simp_all (no_asm_use) add: le_lt);
-apply(blast intro: lt_trans);
-apply(erule disjE);
-apply(erule disjE);
-apply(rule irrefl[THEN notE]);
-apply(rule lt_trans, assumption, assumption);
-apply blast;apply blast;
-apply(blast intro: irrefl[THEN notE]);
-done
-*)
+text {* \noindent Any @{text "group"} is also a @{text "monoid"}; this
+can be made explicit by claiming an additional subclass relation,
+together with a proof of the logical difference: *}
-subsubsection{*Multiple Inheritance and Sorts*}
-
-text{*
-A class may inherit from more than one direct superclass. This is called
-\bfindex{multiple inheritance}. For example, we could define
-the classes of well-founded orderings and well-orderings:
-*}
+instance group \<subseteq> monoid
+proof
+ fix x
+ from invl have "\<div> x \<oplus> x = \<zero>" .
+ then have "\<div> x \<oplus> (x \<oplus> \<zero>) = \<div> x \<oplus> x"
+ by (simp add: neutl invl assoc [symmetric])
+ then show "x \<oplus> \<zero> = x" by (simp add: left_cancel)
+qed
-axclass wford < parord
-wford: "wf {(y,x). y << x}"
-
-axclass wellord < linord, wford
-
-text{*\noindent
-The last line expresses the usual definition: a well-ordering is a linear
-well-founded ordering. The result is the subclass diagram in
+text {* \noindent The proof result is propagated to the type system,
+making @{text group} an instance of @{text monoid} by adding an
+additional edge to the graph of subclass relation; see also
Figure~\ref{fig:subclass}.
\begin{figure}[htbp]
-\[
-\begin{array}{r@ {}r@ {}c@ {}l@ {}l}
-& & \isa{type}\\
-& & |\\
-& & \isa{ordrel}\\
-& & |\\
-& & \isa{strord}\\
-& & |\\
-& & \isa{parord} \\
-& / & & \backslash \\
-\isa{linord} & & & & \isa{wford} \\
-& \backslash & & / \\
-& & \isa{wellord}
-\end{array}
-\]
-\caption{Subclass Diagram}
-\label{fig:subclass}
+ \begin{center}
+ \small
+ \unitlength 0.6mm
+ \begin{picture}(40,60)(0,0)
+ \put(20,60){\makebox(0,0){@{text semigroup}}}
+ \put(20,40){\makebox(0,0){@{text monoidl}}}
+ \put(00,20){\makebox(0,0){@{text monoid}}}
+ \put(40,00){\makebox(0,0){@{text group}}}
+ \put(20,55){\vector(0,-1){10}}
+ \put(15,35){\vector(-1,-1){10}}
+ \put(25,35){\vector(1,-3){10}}
+ \end{picture}
+ \hspace{8em}
+ \begin{picture}(40,60)(0,0)
+ \put(20,60){\makebox(0,0){@{text semigroup}}}
+ \put(20,40){\makebox(0,0){@{text monoidl}}}
+ \put(00,20){\makebox(0,0){@{text monoid}}}
+ \put(40,00){\makebox(0,0){@{text group}}}
+ \put(20,55){\vector(0,-1){10}}
+ \put(15,35){\vector(-1,-1){10}}
+ \put(05,15){\vector(3,-1){30}}
+ \end{picture}
+ \caption{Subclass relationship of monoids and groups:
+ before and after establishing the relationship
+ @{text "group \<subseteq> monoid"}; transitive edges are left out.}
+ \label{fig:subclass}
+ \end{center}
\end{figure}
-
-Since class @{text wellord} does not introduce any new axioms, it can simply
-be viewed as the intersection of the two classes @{text linord} and @{text
-wford}. Such intersections need not be given a new name but can be created on
-the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
-represents the intersection of the $C@i$. Such an expression is called a
-\textbf{sort},\index{sorts} and sorts can appear in most places where we have only shown
-classes so far, for example in type constraints: @{text"'a::{linord,wford}"}.
-In fact, @{text"'a::C"} is short for @{text"'a::{C}"}.
-However, we do not pursue this rarefied concept further.
-
-This concludes our demonstration of type classes based on orderings. We
-remind our readers that \isa{Main} contains a theory of
-orderings phrased in terms of the usual @{text"\<le>"} and @{text"<"}.
-If possible, base your own ordering relations on this theory.
*}
-subsubsection{*Inconsistencies*}
+subsubsection {* Inconsistencies *}
-text{* The reader may be wondering what happens if we
-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
+text {* The reader may be wondering what happens if we 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.
+The point is that by construction, all type variables in the axioms of
+a \isacommand{class} 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.
+
+Even if each individual class is consistent, intersections of
+(unrelated) classes readily become inconsistent in practice. Now we
+know this need not worry us. *}
+
+
+subsubsection{* Syntactic Classes and Predefined Overloading *}
-Even if each individual class is consistent, intersections of (unrelated)
-classes readily become inconsistent in practice. Now we know this need not
-worry us.
-*}
+text {* In our algebra example, we have started with a \emph{syntactic
+class} @{class plus} which only specifies operations but no axioms; it
+would have been also possible to start immediately with class @{class
+semigroup}, specifying the @{text "\<oplus>"} operation and associativity at
+the same time.
-(*
-axclass false<"term"
-false: "x \<noteq> x";
+Which approach is more appropriate depends. Usually it is more
+convenient to introduce operations and axioms in the same class: then
+the type checker will automatically insert the corresponding class
+constraints whenever the operations occur, reducing the need of manual
+annotations. However, when operations are decorated with popular
+syntax, syntactic classes can be an option to re-use the syntax in
+different contexts; this is indeed the way most overloaded constants
+in HOL are introduced, of which the most important are listed in
+Table~\ref{tab:overloading} in the appendix. Section
+\ref{sec:numeric-classes} covers a range of corresponding classes
+\emph{with} axioms.
-lemma "False";
-by(rule notE[OF false HOL.refl]);
-*)
+Further note that classes may contain axioms but \emph{no} operations.
+An example is class @{class finite} from theory @{theory Finite_Set}
+which specifies a type to be finite: @{lemma [source] "finite (UNIV \<Colon> 'a\<Colon>finite
+set)" by (fact finite_UNIV)}. *}
+
(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/Overloading.thy Wed Jun 17 10:07:23 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(*<*)theory Overloading imports Overloading1 begin(*>*)
-instance list :: (type)ordrel
-by intro_classes
-
-text{*\noindent
-This \isacommand{instance} declaration can be read like the declaration of
-a function on types. The constructor @{text list} maps types of class @{text
-type} (all HOL types), to types of class @{text ordrel};
-in other words,
-if @{text"ty :: type"} then @{text"ty list :: ordrel"}.
-Of course we should also define the meaning of @{text <<=} and
-@{text <<} on lists:
-*}
-
-defs (overloaded)
-prefix_def:
- "xs <<= (ys::'a list) \<equiv> \<exists>zs. ys = xs@zs"
-strict_prefix_def:
- "xs << (ys::'a list) \<equiv> xs <<= ys \<and> xs \<noteq> ys"
-
-(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/Overloading0.thy Wed Jun 17 10:07:23 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*<*)theory Overloading0 imports Main begin(*>*)
-
-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{*
-If we want to introduce the notion of an \emph{inverse} for arbitrary types we
-give it a polymorphic type *}
-
-consts inverse :: "'a \<Rightarrow> 'a"
-
-text{*\noindent
-and provide different definitions at different instances:
-*}
-
-defs (overloaded)
-inverse_bool: "inverse(b::bool) \<equiv> \<not> b"
-inverse_set: "inverse(A::'a set) \<equiv> -A"
-inverse_pair: "inverse(p) \<equiv> (inverse(fst p), inverse(snd p))"
-
-text{*\noindent
-Isabelle will not complain because the three definitions do not overlap: no
-two of the three types @{typ bool}, @{typ"'a set"} and @{typ"'a \<times> 'b"} have a
-common instance. What is more, the recursion in @{thm[source]inverse_pair} is
-benign because the type of @{term[source]inverse} becomes smaller: on the
-left it is @{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and
-@{typ"'b \<Rightarrow> 'b"}. The annotation @{text"("}\isacommand{overloaded}@{text")"} tells Isabelle that
-the definitions do intentionally define @{term[source]inverse} only at
-instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely suppresses
-warnings to that effect.
-
-However, there is nothing to prevent the user from forming terms such as
-@{text"inverse []"} and proving theorems such as @{text"inverse []
-= inverse []"} when inverse is not defined on lists. Proving theorems about
-unspecified constants does not endanger soundness, but it is pointless.
-To prevent such terms from even being formed requires the use of type classes.
-*}
-(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/Overloading1.thy Wed Jun 17 10:07:23 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-(*<*)theory Overloading1 imports Main begin(*>*)
-
-subsubsection{*Controlled Overloading with Type Classes*}
-
-text{*
-We now start with the theory of ordering relations, which we shall phrase
-in terms of the two binary symbols @{text"<<"} and @{text"<<="}
-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}:
-*}
-
-axclass ordrel < type
-
-text{*\noindent
-This introduces a new class @{text ordrel} and makes it a subclass of
-the predefined class @{text type}, which
-is the class of all HOL types.
-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 lt :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<" 50)
- le :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<=" 50)
-
-text{*\noindent
-Note that only one occurrence of a type variable in a type needs to be
-constrained with a class; the constraint is propagated to the other
-occurrences automatically.
-
-So far there are no types 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 the \methdx{intro_classes} method:
-*}
-
-by intro_classes
-
-text{*\noindent
-More interesting \isacommand{instance} proofs will arise below
-in the context of proper axiomatic type classes.
-
-Although 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 \<equiv> P \<longrightarrow> Q"
-lt_bool_def: "P << Q \<equiv> \<not>P \<and> Q"
-
-text{*\noindent
-Now @{prop"False <<= P"} is provable:
-*}
-
-lemma "False <<= P"
-by(simp add: le_bool_def)
-
-text{*\noindent
-At this point, @{text"[] <<= []"} is not even well-typed.
-To make it well-typed,
-we need to make lists a type of class @{text ordrel}:*}(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/Overloading2.thy Wed Jun 17 10:07:23 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*<*)theory Overloading2 imports Overloading1 begin(*>*)
-
-text{*
-Of course this is not the only possible definition of the two relations.
-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
-by intro_classes
-
-defs (overloaded)
-le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv>
- size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)"
-
-text{*\noindent
-The infix function @{text"!"} yields the nth element of a list, starting with 0.
-
-\begin{warn}
-A type constructor can be instantiated in only one way to
-a given type class. For example, our two instantiations of @{text list} must
-reside in separate theories with disjoint scopes.
-\end{warn}
-*}
-
-subsubsection{*Predefined Overloading*}
-
-text{*
-HOL comes with a number of overloaded constants and corresponding classes.
-The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
-defined on all numeric types and sometimes on other types as well, for example
-$-$ and @{text"\<le>"} on sets.
-
-In addition there is a special syntax for bounded quantifiers:
-\begin{center}
-\begin{tabular}{lcl}
-@{prop"\<forall>x \<le> y. P x"} & @{text"\<rightleftharpoons>"} & @{prop [source] "\<forall>x. x \<le> y \<longrightarrow> P x"} \\
-@{prop"\<exists>x \<le> y. P x"} & @{text"\<rightleftharpoons>"} & @{prop [source] "\<exists>x. x \<le> y \<and> P x"}
-\end{tabular}
-\end{center}
-And analogously for @{text"<"} instead of @{text"\<le>"}.
-*}(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/ROOT.ML Wed Jun 17 10:07:23 2009 +0200
+++ b/doc-src/TutorialI/Types/ROOT.ML Wed Jun 17 10:07:25 2009 +0200
@@ -1,9 +1,10 @@
-(* ID: $Id$ *)
+
+no_document use_thy "Setup";
+
use "../settings.ML";
use_thy "Numbers";
use_thy "Pairs";
use_thy "Records";
use_thy "Typedefs";
-use_thy "Overloading0";
-use_thy "Overloading2";
+use_thy "Overloading";
use_thy "Axioms";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/Setup.thy Wed Jun 17 10:07:25 2009 +0200
@@ -0,0 +1,8 @@
+theory Setup
+imports Main
+uses
+ "../../antiquote_setup.ML"
+ "../../more_antiquote.ML"
+begin
+
+end
\ No newline at end of file
--- a/doc-src/TutorialI/Types/document/Axioms.tex Wed Jun 17 10:07:23 2009 +0200
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Wed Jun 17 10:07:25 2009 +0200
@@ -20,70 +20,50 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Attaching axioms to our classes lets us reason on the
-level of classes. The results will be applicable to all types in a class,
-just as in axiomatic mathematics. These ideas are demonstrated by means of
-our ordering relations.%
+Attaching axioms to our classes lets us reason on the level of
+classes. The results will be applicable to all types in a class, just
+as in axiomatic mathematics.
+
+\begin{warn}
+Proofs in this section use structured \emph{Isar} proofs, which are not
+covered in this tutorial; but see \cite{Nipkow-TYPES02}.%
+\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Partial Orders%
+\isamarkupsubsubsection{Semigroups%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A \emph{partial order} is a subclass of \isa{ordrel}
+We specify \emph{semigroups} as subclass of \isa{plus}
where certain axioms need to hold:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ parord\ {\isacharless}\ ordrel\isanewline
-refl{\isacharcolon}\ \ \ \ {\isachardoublequoteopen}x\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-trans{\isacharcolon}\ \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isachardoublequoteclose}\isanewline
-antisym{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
-lt{\isacharunderscore}le{\isacharcolon}\ \ \ {\isachardoublequoteopen}x\ {\isacharless}{\isacharless}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}%
+\isacommand{class}\isamarkupfalse%
+\ semigroup\ {\isacharequal}\ plus\ {\isacharplus}\isanewline
+\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}%
\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, the axiom \isa{refl} really is
-\isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isasymColon}parord{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
+\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification requires that
+all instances of \isa{semigroup} obey \hyperlink{fact.assoc:}{\mbox{\isa{assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isacharprime}a{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}}.
-We have not made \isa{lt{\isacharunderscore}le} a global definition because it would
-fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
-never the other way around. Below you will see why we want to avoid this
-asymmetry. The drawback of our choice is that
-we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance.
-
-We can now prove simple theorems in this abstract setting, for example
-that \isa{{\isacharless}{\isacharless}} is not symmetric:%
+We can use this class axiom to derive further abstract theorems
+relative to class \isa{semigroup}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}parord{\isacharparenright}\ {\isacharless}{\isacharless}\ y\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}%
+\ assoc{\isacharunderscore}left{\isacharcolon}\isanewline
+\ \ \isakeyword{fixes}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z{\isachardoublequoteclose}\isanewline
+%
\isadelimproof
-%
+\ \ %
\endisadelimproof
%
\isatagproof
-%
-\begin{isamarkuptxt}%
-\noindent
-The conclusion is not just \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the
-simplifier's preprocessor (see \S\ref{sec:simp-preprocessor})
-would turn it into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, yielding
-a nonterminating rewrite rule.
-(It would be used to try to prove its own precondition \emph{ad
- infinitum}.)
-In the form above, the rule is useful.
-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}}),
-when the proposition is not a theorem. The proof is easy:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{by}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}\ lt{\isacharunderscore}le\ antisym{\isacharparenright}%
+\isacommand{using}\isamarkupfalse%
+\ assoc\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ sym{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
@@ -92,116 +72,262 @@
\endisadelimproof
%
\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}:%
+\noindent The \isa{semigroup} constraint on type \isa{{\isacharprime}a} restricts instantiations of \isa{{\isacharprime}a} to types of class
+\isa{semigroup} and during the proof enables us to use the fact
+\hyperlink{fact.assoc}{\mbox{\isa{assoc}}} whose type parameter is itself constrained to class
+\isa{semigroup}. The main advantage is that theorems can be proved
+in the abstract and freely reused for each instance.
+
+On instantiation, we have to give a proof that the given operations
+obey the class axioms:%
\end{isamarkuptext}%
\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
\isacommand{instance}\isamarkupfalse%
-\ bool\ {\isacharcolon}{\isacharcolon}\ parord\isanewline
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent The proof opens with a default proof step, which for
+instance judgements invokes method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{fix}\isamarkupfalse%
+\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharparenleft}m\ {\isasymoplus}\ n{\isacharparenright}\ {\isasymoplus}\ q\ {\isacharequal}\ m\ {\isasymoplus}\ {\isacharparenleft}n\ {\isasymoplus}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ m{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent Again, the interesting things enter the stage with
+parametric types:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
%
\isatagproof
-\isacommand{apply}\isamarkupfalse%
-\ intro{\isacharunderscore}classes%
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymoplus}\ p\isactrlisub {\isadigit{2}}\ {\isasymoplus}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymoplus}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymoplus}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}cases\ p\isactrlisub {\isadigit{1}}{\isacharcomma}\ cases\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ cases\ p\isactrlisub {\isadigit{3}}{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}%
\begin{isamarkuptxt}%
-\noindent
-This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms,
-specialized to type \isa{bool}, as subgoals:
-\begin{isabelle}%
-\ {\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 \isa{blast}
-once we have unfolded the definitions
-of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at type \isa{bool}:%
+\noindent Associativity of product semigroups is established
+using the hypothetical associativity \hyperlink{fact.assoc}{\mbox{\isa{assoc}}} of the type
+components, which holds due to the \isa{semigroup} constraints
+imposed on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
+Indeed, this pattern often occurs with parametric types and type
+classes.%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ only{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def\ lt{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
-\isacommand{by}\isamarkupfalse%
-{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}%
+\isacommand{qed}\isamarkupfalse%
+%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\isamarkupsubsubsection{Monoids%
+}
+\isamarkuptrue%
%
\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:%
+We define a subclass \isa{monoidl} (a semigroup with a
+left-hand neutral) by extending \isa{semigroup} with one additional
+parameter \isa{neutral} together with its property:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{class}\isamarkupfalse%
+\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
+\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymzero}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymzero}\ {\isasymoplus}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent Again, we prove some instances, by providing
+suitable parameter definitions and proofs for the additional
+specifications.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymzero}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
%
\isadelimproof
-%
+\ %
\endisadelimproof
%
\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ simp%
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymzero}\ {\isasymoplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
-\noindent
-The effect is not stunning, but it demonstrates the principle. It also shows
-that tools like the simplifier can deal with generic rules.
-The main advantage of the axiomatic method is that
-theorems can be proved in the abstract and freely reused for each instance.%
+\noindent Unless in the above examples, we here have both
+specification of class operations and a non-trivial instance proof.
+
+This covers products as well:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymzero}\ {\isacharequal}\ {\isacharparenleft}{\isasymzero}{\isacharcomma}\ {\isasymzero}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoidl\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymzero}\ {\isasymoplus}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}cases\ p{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ neutl{\isacharparenright}\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent Fully-fledged monoids are modelled by another
+subclass which does not add new parameters but tightens the
+specification:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{class}\isamarkupfalse%
+\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
+\ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymoplus}\ {\isasymzero}\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent Corresponding instances for \isa{nat} and products
+are left as an exercise to the reader.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Linear Orders%
+\isamarkupsubsubsection{Groups%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-If any two elements of a partial order are comparable it is a
-\textbf{linear} or \textbf{total} order:%
+\noindent To finish our small algebra example, we add a \isa{group} class:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ linord\ {\isacharless}\ parord\isanewline
-linear{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequoteclose}%
+\isacommand{class}\isamarkupfalse%
+\ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
+\ \ \isakeyword{fixes}\ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymdiv}\ {\isacharunderscore}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{1}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymdiv}\ x\ {\isasymoplus}\ x\ {\isacharequal}\ {\isasymzero}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-\noindent
-By construction, \isa{linord} inherits all axioms from \isa{parord}.
-Therefore we can show that linearity can be expressed in terms of \isa{{\isacharless}{\isacharless}}
-as follows:%
+\noindent We continue with a further example for abstract
+proofs relative to type classes:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymAnd}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}linord{\isachardot}\ x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}\ x{\isachardoublequoteclose}\isanewline
+\ left{\isacharunderscore}cancel{\isacharcolon}\isanewline
+\ \ \isakeyword{fixes}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isasymoplus}\ y\ {\isacharequal}\ x\ {\isasymoplus}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}\ lt{\isacharunderscore}le{\isacharparenright}\isanewline
-\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}insert\ linear{\isacharparenright}\isanewline
-\isacommand{apply}\isamarkupfalse%
-\ blast\isanewline
-\isacommand{done}\isamarkupfalse%
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymoplus}\ y\ {\isacharequal}\ x\ {\isasymoplus}\ z{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymdiv}\ x\ {\isasymoplus}\ {\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isacharequal}\ {\isasymdiv}\ x\ {\isasymoplus}\ {\isacharparenleft}x\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymdiv}\ x\ {\isasymoplus}\ x{\isacharparenright}\ {\isasymoplus}\ y\ {\isacharequal}\ {\isacharparenleft}{\isasymdiv}\ x\ {\isasymoplus}\ x{\isacharparenright}\ {\isasymoplus}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ invl\ neutl{\isacharparenright}\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymoplus}\ y\ {\isacharequal}\ x\ {\isasymoplus}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -211,65 +337,37 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-Linear orders are an example of subclassing\index{subclasses}
-by construction, which is the most
-common case. Subclass relationships can also be proved.
-This is the topic of the following
-paragraph.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Strict Orders%
-}
-\isamarkuptrue%
-%
-\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 \textbf{strict} order:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ strord\ {\isacharless}\ ordrel\isanewline
-irrefl{\isacharcolon}\ \ \ \ \ {\isachardoublequoteopen}{\isasymnot}\ x\ {\isacharless}{\isacharless}\ x{\isachardoublequoteclose}\isanewline
-lt{\isacharunderscore}trans{\isacharcolon}\ \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z{\isachardoublequoteclose}\isanewline
-le{\isacharunderscore}less{\isacharcolon}\ \ \ \ {\isachardoublequoteopen}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequoteclose}%
-\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.%
+\noindent Any \isa{group} is also a \isa{monoid}; this
+can be made explicit by claiming an additional subclass relation,
+together with a proof of the logical difference:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{instance}\isamarkupfalse%
-\ parord\ {\isacharless}\ strord\isanewline
+\ group\ {\isasymsubseteq}\ monoid\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
-\isacommand{apply}\isamarkupfalse%
-\ intro{\isacharunderscore}classes%
-\begin{isamarkuptxt}%
-\noindent
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymnot}\ x\ {\isacharless}{\isacharless}\ x\isanewline
-\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}{\isacharprime}a{\isacharparenright}\ z{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z\isanewline
-\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}a{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}\isanewline
-type\ variables{\isacharcolon}\isanewline
-\isaindent{\ \ }{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord%
-\end{isabelle}
-Because of \isa{{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord}, the three axioms of class \isa{strord}
-are easily proved:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\ \ \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}\ lt{\isacharunderscore}le{\isacharparenright}\isanewline
-\ \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline
-\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline
-\isacommand{done}\isamarkupfalse%
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ x\isanewline
+\ \ \isacommand{from}\isamarkupfalse%
+\ invl\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymdiv}\ x\ {\isasymoplus}\ x\ {\isacharequal}\ {\isasymzero}{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymdiv}\ x\ {\isasymoplus}\ {\isacharparenleft}x\ {\isasymoplus}\ {\isasymzero}{\isacharparenright}\ {\isacharequal}\ {\isasymdiv}\ x\ {\isasymoplus}\ x{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl\ invl\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymoplus}\ {\isasymzero}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ left{\isacharunderscore}cancel{\isacharparenright}\isanewline
+\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -279,66 +377,40 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-The subclass relation must always be acyclic. Therefore Isabelle will
-complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Multiple Inheritance and Sorts%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-A class may inherit from more than one direct superclass. This is called
-\bfindex{multiple inheritance}. For example, we could define
-the classes of well-founded orderings and well-orderings:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ wford\ {\isacharless}\ parord\isanewline
-wford{\isacharcolon}\ {\isachardoublequoteopen}wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharless}{\isacharless}\ x{\isacharbraceright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ wellord\ {\isacharless}\ linord{\isacharcomma}\ wford%
-\begin{isamarkuptext}%
-\noindent
-The last line expresses the usual definition: a well-ordering is a linear
-well-founded ordering. The result is the subclass diagram in
+\noindent The proof result is propagated to the type system,
+making \isa{group} an instance of \isa{monoid} by adding an
+additional edge to the graph of subclass relation; see also
Figure~\ref{fig:subclass}.
\begin{figure}[htbp]
-\[
-\begin{array}{r@ {}r@ {}c@ {}l@ {}l}
-& & \isa{type}\\
-& & |\\
-& & \isa{ordrel}\\
-& & |\\
-& & \isa{strord}\\
-& & |\\
-& & \isa{parord} \\
-& / & & \backslash \\
-\isa{linord} & & & & \isa{wford} \\
-& \backslash & & / \\
-& & \isa{wellord}
-\end{array}
-\]
-\caption{Subclass Diagram}
-\label{fig:subclass}
-\end{figure}
-
-Since class \isa{wellord} does not introduce any new axioms, it can simply
-be viewed as the intersection of the two classes \isa{linord} and \isa{wford}. Such intersections need not be given a new name but can be created on
-the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
-represents the intersection of the $C@i$. Such an expression is called a
-\textbf{sort},\index{sorts} and sorts can appear in most places where we have only shown
-classes so far, for example in type constraints: \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}linord{\isacharcomma}wford{\isacharbraceright}}.
-In fact, \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}C} is short for \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}C{\isacharbraceright}}.
-However, we do not pursue this rarefied concept further.
-
-This concludes our demonstration of type classes based on orderings. We
-remind our readers that \isa{Main} contains a theory of
-orderings phrased in terms of the usual \isa{{\isasymle}} and \isa{{\isacharless}}.
-If possible, base your own ordering relations on this theory.%
+ \begin{center}
+ \small
+ \unitlength 0.6mm
+ \begin{picture}(40,60)(0,0)
+ \put(20,60){\makebox(0,0){\isa{semigroup}}}
+ \put(20,40){\makebox(0,0){\isa{monoidl}}}
+ \put(00,20){\makebox(0,0){\isa{monoid}}}
+ \put(40,00){\makebox(0,0){\isa{group}}}
+ \put(20,55){\vector(0,-1){10}}
+ \put(15,35){\vector(-1,-1){10}}
+ \put(25,35){\vector(1,-3){10}}
+ \end{picture}
+ \hspace{8em}
+ \begin{picture}(40,60)(0,0)
+ \put(20,60){\makebox(0,0){\isa{semigroup}}}
+ \put(20,40){\makebox(0,0){\isa{monoidl}}}
+ \put(00,20){\makebox(0,0){\isa{monoid}}}
+ \put(40,00){\makebox(0,0){\isa{group}}}
+ \put(20,55){\vector(0,-1){10}}
+ \put(15,35){\vector(-1,-1){10}}
+ \put(05,15){\vector(3,-1){30}}
+ \end{picture}
+ \caption{Subclass relationship of monoids and groups:
+ before and after establishing the relationship
+ \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges are left out.}
+ \label{fig:subclass}
+ \end{center}
+\end{figure}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -347,24 +419,53 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The reader may be wondering what happens if we
-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
+The reader may be wondering what happens if we 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.
+The point is that by construction, all type variables in the axioms of
+a \isacommand{class} 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.
-Even if each individual class is consistent, intersections of (unrelated)
-classes readily become inconsistent in practice. Now we know this need not
-worry us.%
+Even if each individual class is consistent, intersections of
+(unrelated) classes readily become inconsistent in practice. Now we
+know this need not worry us.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Syntactic Classes and Predefined Overloading%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In our algebra example, we have started with a \emph{syntactic
+class} \isa{plus} which only specifies operations but no axioms; it
+would have been also possible to start immediately with class \isa{semigroup}, specifying the \isa{{\isasymoplus}} operation and associativity at
+the same time.
+
+Which approach is more appropriate depends. Usually it is more
+convenient to introduce operations and axioms in the same class: then
+the type checker will automatically insert the corresponding class
+constraints whenever the operations occur, reducing the need of manual
+annotations. However, when operations are decorated with popular
+syntax, syntactic classes can be an option to re-use the syntax in
+different contexts; this is indeed the way most overloaded constants
+in HOL are introduced, of which the most important are listed in
+Table~\ref{tab:overloading} in the appendix. Section
+\ref{sec:numeric-classes} covers a range of corresponding classes
+\emph{with} axioms.
+
+Further note that classes may contain axioms but \emph{no} operations.
+An example is class \isa{finite} from theory \hyperlink{theory.Finite-Set}{\mbox{\isa{Finite{\isacharunderscore}Set}}}
+which specifies a type to be finite: \isa{{\isachardoublequote}finite\ {\isacharparenleft}UNIV\ {\isasymColon}\ {\isacharprime}a{\isasymColon}finite\ set{\isacharparenright}{\isachardoublequote}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/TutorialI/Types/document/Numbers.tex Wed Jun 17 10:07:23 2009 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Wed Jun 17 10:07:25 2009 +0200
@@ -257,7 +257,7 @@
\rulename{mod_mult2_eq}
\begin{isabelle}%
-{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ c\ {\isacharasterisk}\ a\ div\ {\isacharparenleft}c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ a\ div\ b%
+c\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymLongrightarrow}\ c\ {\isacharasterisk}\ a\ div\ {\isacharparenleft}c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ a\ div\ b%
\end{isabelle}
\rulename{div_mult_mult1}
@@ -607,17 +607,17 @@
\rulename{abs_triangle_ineq}
\begin{isabelle}%
-a\ {\isacharcircum}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}\ {\isacharequal}\ a\ {\isacharcircum}\ m\ {\isacharasterisk}\ a\ {\isacharcircum}\ n%
+a\isactrlbsup m\ {\isacharplus}\ n\isactrlesup \ {\isacharequal}\ a\isactrlbsup m\isactrlesup \ {\isacharasterisk}\ a\isactrlbsup n\isactrlesup %
\end{isabelle}
\rulename{power_add}
\begin{isabelle}%
-a\ {\isacharcircum}\ {\isacharparenleft}m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharcircum}\ m{\isacharparenright}\ {\isacharcircum}\ n%
+a\isactrlbsup m\ {\isacharasterisk}\ n\isactrlesup \ {\isacharequal}\ a\isactrlbsup m\isactrlesup \isactrlbsup n\isactrlesup %
\end{isabelle}
\rulename{power_mult}
\begin{isabelle}%
-{\isasymbar}a\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharcircum}\ n%
+{\isasymbar}a\isactrlbsup n\isactrlesup {\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\isactrlbsup n\isactrlesup %
\end{isabelle}
\rulename{power_abs}%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Types/document/Overloading.tex Wed Jun 17 10:07:23 2009 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading.tex Wed Jun 17 10:07:25 2009 +0200
@@ -14,16 +14,69 @@
\isadelimtheory
%
\endisadelimtheory
+%
+\begin{isamarkuptext}%
+Type classes allow \emph{overloading}; thus a constant may
+have multiple definitions at non-overlapping types.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Overloading%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+We can introduce a binary infix addition operator \isa{{\isasymotimes}}
+for arbitrary types by means of a type class:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{class}\isamarkupfalse%
+\ plus\ {\isacharequal}\isanewline
+\ \ \isakeyword{fixes}\ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent This introduces a new class \isa{plus},
+along with a constant \isa{plus} with nice infix syntax.
+\isa{plus} is also named \emph{class operation}. The type
+of \isa{plus} carries a sort constraint \isa{{\isachardoublequote}{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ plus{\isachardoublequote}} on its type variable, meaning that only types of class
+\isa{plus} can be instantiated for \isa{{\isachardoublequote}{\isacharprime}a{\isachardoublequote}}.
+To breathe life into \isa{plus} we need to declare a type
+to be an \bfindex{instance} of \isa{plus}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ nat\ {\isacharcolon}{\isacharcolon}\ plus\isanewline
+\isakeyword{begin}%
+\begin{isamarkuptext}%
+\noindent Command \isacommand{instantiation} opens a local
+theory context. Here we can now instantiate \isa{plus} on
+\isa{nat}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{primrec}\isamarkupfalse%
+\ plus{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymoplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymoplus}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymoplus}\ n{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent Note that the name \isa{plus} carries a
+suffix \isa{{\isacharunderscore}nat}; by default, the local name of a class operation
+\isa{f} to be instantiated on type constructor \isa{{\isasymkappa}} is mangled
+as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty, these names may be inspected
+using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command or the corresponding
+ProofGeneral button.
+
+Although class \isa{plus} has no axioms, the instantiation must be
+formally concluded by a (trivial) instantiation proof ``..'':%
+\end{isamarkuptext}%
+\isamarkuptrue%
\isacommand{instance}\isamarkupfalse%
-\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}ordrel\isanewline
%
\isadelimproof
-%
+\ %
\endisadelimproof
%
\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ intro{\isacharunderscore}classes%
+\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
\endisatagproof
{\isafoldproof}%
%
@@ -32,21 +85,60 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent
-This \isacommand{instance} declaration can be read like the declaration of
-a function on types. The constructor \isa{list} maps types of class \isa{type} (all HOL types), to types of class \isa{ordrel};
-in other words,
-if \isa{ty\ {\isacharcolon}{\isacharcolon}\ type} 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:%
+\noindent More interesting \isacommand{instance} proofs will
+arise below.
+
+The instantiation is finished by an explicit%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{end}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent From now on, terms like \isa{Suc\ {\isacharparenleft}m\ {\isasymoplus}\ {\isadigit{2}}{\isacharparenright}} are
+legal.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}plus{\isacharcomma}\ plus{\isacharparenright}\ plus\isanewline
+\isakeyword{begin}%
+\begin{isamarkuptext}%
+\noindent Here we instantiate the product type \isa{{\isacharasterisk}} to
+class \isa{plus}, given that its type arguments are of
+class \isa{plus}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-prefix{\isacharunderscore}def{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequoteclose}\isanewline
-strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequoteclose}\isanewline
+\isacommand{fun}\isamarkupfalse%
+\ plus{\isacharunderscore}prod\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymoplus}\ {\isacharparenleft}w{\isacharcomma}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymoplus}\ w{\isacharcomma}\ y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent Obviously, overloaded specifications may include
+recursion over the syntactic structure of types.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instance}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent This way we have encoded the canonical lifting of
+binary operations to products by means of type classes.%
+\end{isamarkuptext}%
+\isamarkuptrue%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Wed Jun 17 10:07:23 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Overloading{\isadigit{0}}}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\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}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{An Initial Example%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If we want to introduce the notion of an \emph{inverse} for arbitrary types we
-give it a polymorphic type%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-and provide different definitions at different instances:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-inverse{\isacharunderscore}bool{\isacharcolon}\ {\isachardoublequoteopen}inverse{\isacharparenleft}b{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isasymequiv}\ {\isasymnot}\ b{\isachardoublequoteclose}\isanewline
-inverse{\isacharunderscore}set{\isacharcolon}\ \ {\isachardoublequoteopen}inverse{\isacharparenleft}A{\isacharcolon}{\isacharcolon}{\isacharprime}a\ set{\isacharparenright}\ {\isasymequiv}\ {\isacharminus}A{\isachardoublequoteclose}\isanewline
-inverse{\isacharunderscore}pair{\isacharcolon}\ {\isachardoublequoteopen}inverse{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}inverse{\isacharparenleft}fst\ p{\isacharparenright}{\isacharcomma}\ inverse{\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-Isabelle will not complain because the three definitions do not overlap: no
-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 annotation \isa{{\isacharparenleft}}\isacommand{overloaded}\isa{{\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 suppresses
-warnings to that effect.
-
-However, there is nothing to prevent the user from forming terms such as
-\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}} when inverse is not defined on lists. Proving theorems about
-unspecified constants does not endanger soundness, but it is pointless.
-To prevent such terms from even being formed requires the use of type classes.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Types/document/Overloading1.tex Wed Jun 17 10:07:23 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,139 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Overloading{\isadigit{1}}}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsubsubsection{Controlled Overloading with Type Classes%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-We now start with the theory of ordering relations, which we shall phrase
-in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}
-to avoid clashes with \isa{{\isacharless}} and \isa{{\isacharless}{\isacharequal}} 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}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ ordrel\ {\isacharless}\ type%
-\begin{isamarkuptext}%
-\noindent
-This introduces a new class \isa{ordrel} and makes it a subclass of
-the predefined class \isa{type}, which
-is the class of all HOL types.
-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}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ lt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharless}{\isacharless}{\isachardoublequoteclose}\ \ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \ le\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharless}{\isacharless}{\isacharequal}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
-Note that only one occurrence of a type variable in a type needs to be
-constrained with a class; the constraint is propagated to the other
-occurrences automatically.
-
-So far there are no types 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}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\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 the \methdx{intro_classes} method:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{by}\isamarkupfalse%
-\ intro{\isacharunderscore}classes%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-More interesting \isacommand{instance} proofs will arise below
-in the context of proper axiomatic type classes.
-
-Although 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}%
-\isamarkuptrue%
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-le{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}P\ {\isacharless}{\isacharless}{\isacharequal}\ Q\ {\isasymequiv}\ P\ {\isasymlongrightarrow}\ Q{\isachardoublequoteclose}\isanewline
-lt{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-At this point, \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed.
-To make it well-typed,
-we need to make lists a type of class \isa{ordrel}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Wed Jun 17 10:07:23 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Overloading{\isadigit{2}}}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-Of course this is not the only possible definition of the two relations.
-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}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ intro{\isacharunderscore}classes%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-\isanewline
-%
-\endisadelimproof
-\isanewline
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}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}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-The infix function \isa{{\isacharbang}} yields the nth element of a list, starting with 0.
-
-\begin{warn}
-A type constructor can be instantiated in only one way to
-a given type class. For example, our two instantiations of \isa{list} must
-reside in separate theories with disjoint scopes.
-\end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Predefined Overloading%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-HOL comes with a number of overloaded constants and corresponding classes.
-The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
-defined on all numeric types and sometimes on other types as well, for example
-$-$ and \isa{{\isasymle}} on sets.
-
-In addition there is a special syntax for bounded quantifiers:
-\begin{center}
-\begin{tabular}{lcl}
-\isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}} \\
-\isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x{\isachardoublequote}}
-\end{tabular}
-\end{center}
-And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Types/numerics.tex Wed Jun 17 10:07:23 2009 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex Wed Jun 17 10:07:25 2009 +0200
@@ -12,7 +12,7 @@
\isa{int} of \textbf{integers}, which lack induction but support true
subtraction. With subtraction, arithmetic reasoning is easier, which makes
the integers preferable to the natural numbers for
-complicated arithmetic expressions, even if they are non-negative. The logic HOL-Complex also has the types
+complicated arithmetic expressions, even if they are non-negative. There are also the types
\isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers. Isabelle has no
subtyping, so the numeric
types are distinct and there are functions to convert between them.
@@ -107,7 +107,7 @@
beginning. Hundreds of theorems about the natural numbers are
proved in the theories \isa{Nat} and \isa{Divides}.
Basic properties of addition and multiplication are available through the
-axiomatic type class for semirings (\S\ref{sec:numeric-axclasses}).
+axiomatic type class for semirings (\S\ref{sec:numeric-classes}).
\subsubsection{Literals}
\index{numeric literals!for type \protect\isa{nat}}%
@@ -242,7 +242,7 @@
proving inequalities involving integer multiplication and division, similar
to those shown above for type~\isa{nat}. The laws of addition, subtraction
and multiplication are available through the axiomatic type class for rings
-(\S\ref{sec:numeric-axclasses}).
+(\S\ref{sec:numeric-classes}).
The \rmindex{absolute value} function \cdx{abs} is overloaded, and is
defined for all types that involve negative numbers, including the integers.
@@ -337,8 +337,7 @@
reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least
upper bound. (It could only be $\surd2$, which is irrational.) The
formalization of completeness, which is complicated,
-can be found in theory \texttt{RComplete} of directory
-\texttt{Real}.
+can be found in theory \texttt{RComplete}.
Numeric literals\index{numeric literals!for type \protect\isa{real}}
for type \isa{real} have the same syntax as those for type
@@ -354,15 +353,13 @@
is performed.
\begin{warn}
-Type \isa{real} is only available in the logic HOL-Complex, which is
-HOL extended with a definitional development of the real and complex
+Types \isa{rat}, \isa{real} and \isa{complex} are provided by theory HOL-Complex, which is
+Main extended with a definitional development of the rational, real and complex
numbers. Base your theory upon theory \thydx{Complex_Main}, not the
-usual \isa{Main}, and set the Proof General menu item \pgmenu{Isabelle} $>$
-\pgmenu{Logics} $>$ \pgmenu{HOL-Complex}.%
-\index{real numbers|)}\index{*real (type)|)}
+usual \isa{Main}.%
\end{warn}
-Also available in HOL-Complex is the
+Available in the logic HOL-NSA is the
theory \isa{Hyperreal}, which define the type \tydx{hypreal} of
\rmindex{non-standard reals}. These
\textbf{hyperreals} include infinitesimals, which represent infinitely
@@ -379,7 +376,7 @@
\index{complex numbers|)}\index{*complex (type)|)}
-\subsection{The Numeric Type Classes}\label{sec:numeric-axclasses}
+\subsection{The Numeric Type Classes}\label{sec:numeric-classes}
Isabelle/HOL organises its numeric theories using axiomatic type classes.
Hundreds of basic properties are proved in the theory \isa{Ring_and_Field}.
--- a/doc-src/TutorialI/Types/types.tex Wed Jun 17 10:07:23 2009 +0200
+++ b/doc-src/TutorialI/Types/types.tex Wed Jun 17 10:07:25 2009 +0200
@@ -6,7 +6,8 @@
(\isacommand{datatype}). This chapter will introduce more
advanced material:
\begin{itemize}
-\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
and how to reason about them.
+\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
+and how to reason about them.
\item Type classes: how to specify and reason about axiomatic collections of
types ({\S}\ref{sec:axclass}). This section leads on to a discussion of
Isabelle's numeric types ({\S}\ref{sec:numbers}).
@@ -15,7 +16,10 @@
({\S}\ref{sec:adv-typedef}).
\end{itemize}
-The material in this section goes beyond the needs of most novices.
Serious users should at least skim the sections as far as type classes.
That material is fairly advanced; read the beginning to understand what it
is about, but consult the rest only when necessary.
+The material in this section goes beyond the needs of most novices.
+Serious users should at least skim the sections as far as type classes.
+That material is fairly advanced; read the beginning to understand what it
+is about, but consult the rest only when necessary.
\index{pairs and tuples|(}
\input{Types/document/Pairs} %%%Section "Pairs and Tuples"
@@ -24,48 +28,41 @@
\input{Types/document/Records} %%%Section "Records"
-\section{Axiomatic Type Classes} %%%Section
+\section{Type Classes} %%%Section
\label{sec:axclass}
\index{axiomatic type classes|(}
\index{*axclass|(}
-The programming language Haskell has popularized the notion of type classes.
-In its simplest form, a type class is a set of types with a common interface:
-all types in that class must provide the functions in the interface.
-Isabelle offers the related concept of an \textbf{axiomatic type class}.
-Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\
-an axiomatic specification of a class of types. Thus we can talk about a type
-$\tau$ being in a class $C$, which is written $\tau :: C$. This is the case if
-$\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
-organized in a hierarchy. Thus there is the notion of a class $D$ being a
-\textbf{subclass}\index{subclasses}
-of a class $C$, written $D < C$. This is the case if all
-axioms of $C$ are also provable in $D$. We introduce these concepts
-by means of a running example, ordering relations.
+The programming language Haskell has popularized the notion of type
+classes: a type class is a set of types with a
+common interface: all types in that class must provide the functions
+in the interface. Isabelle offers a similar type class concept: in
+addition, properties (\emph{class axioms}) can be specified which any
+instance of this type class must obey. Thus we can talk about a type
+$\tau$ being in a class $C$, which is written $\tau :: C$. This is the case
+if $\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
+organized in a hierarchy. Thus there is the notion of a class $D$
+being a subclass\index{subclasses} of a class $C$, written $D
+< C$. This is the case if all axioms of $C$ are also provable in $D$.
-\begin{warn}
-The material in this section describes a low-level approach to type classes.
-It is recommended to use the new \isacommand{class} command instead.
-For details see the appropriate tutorial~\cite{isabelle-classes} and the
-related article~\cite{Haftmann-Wenzel:2006:classes}.
-\end{warn}
-
+In this section we introduce the most important concepts behind type
+classes by means of a running example from algebra. This should give
+you an intuition how to use type classes and to understand
+specifications involving type classes. Type classes are covered more
+deeply in a separate tutorial \cite{isabelle-classes}.
\subsection{Overloading}
\label{sec:overloading}
\index{overloading|(}
-\input{Types/document/Overloading0}
-\input{Types/document/Overloading1}
\input{Types/document/Overloading}
-\input{Types/document/Overloading2}
\index{overloading|)}
\input{Types/document/Axioms}
-\index{axiomatic type classes|)}
-\index{*axclass|)}
+\index{type classes|)}
+\index{*class|)}
\input{Types/numerics} %%%Section "Numbers"