--- 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
--- 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}
--- 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}
--- 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}.
--- 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}.
--- /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: "\<lbrakk> x <<= y; y <<= z \<rbrakk> \<Longrightarrow> x <<= z"
+antisym: "\<lbrakk> x <<= y; y <<= x \<rbrakk> \<Longrightarrow> x = y"
+less_le: "x << y = (x <<= y \<and> x \<noteq> 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 \<Longrightarrow> (\<not> y << x) = True";
+
+txt{*\noindent
+The conclusion is not simply @{prop"\<not> 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 \<Longrightarrow> \<not>(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 \<or> 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 "\<And>x::'a::linord. x<<y \<or> x=y \<or> y<<x";
+apply(simp add: less_le);
+apply(insert total);
+apply blast;
+done
+
+text{*
+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.
+*}
+
+subsubsection{*Strict orders*}
+
+text{*
+An alternative axiomatization of partial orders takes @{text"<<"} rather than
+@{text"<<="} as the primary concept. The result is a \emph{strict} order:
+*}
+
+axclass strord < ordrel
+irrefl: "\<not> x << x"
+less_trans: "\<lbrakk> x << y; y << z \<rbrakk> \<Longrightarrow> x << z"
+le_less: "x <<= y = (x << y \<or> 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"\<le>"} 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 \<noteq> x";
+
+lemma "False";
+by(rule notE[OF false HOL.refl]);
+*)
+(*<*)end(*>*)
--- 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)
--- 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 \<Rightarrow> '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 \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and @{typ"'b \<Rightarrow>
-'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 \<Rightarrow> 'a"} --- this merely supresses warnings to that effect.
--- 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"\<le>"} and @{text"<"} in theory @{text
+been chosen to avoid clashes with @{text"<"} and @{text"\<le>"} 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) \<Rightarrow> 'a \<Rightarrow> bool" (infixl 50)
- "<<=" :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl 50)
+consts less :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<" 50)
+ le :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> 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 \<equiv> P \<longrightarrow> Q"
less_bool_def: "P << Q \<equiv> \<not>P \<and> 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
--- 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) \<equiv>
size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)"
-text{*
+text{*\noindent
+The infix function @{text"!"} 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.
-*}
-(*<*)end(*>*)
-
+%Note: only one definition because based on name.
+*}(*<*)end(*>*)
--- /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:
--- 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
--- 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.
--- 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
--- 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
--- 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|)}
--- 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$\<Longrightarrow>$ \\
-\indexboldpos{\isasymAnd}{$IsaAnd} &
+\isasymAnd\index{$IsaAnd@\isasymAnd|bold}&
\texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
\verb$\<And>$ \\
\indexboldpos{\isasymequiv}{$IsaEq} &
@@ -80,10 +80,10 @@
\indexboldpos{\isasyminter}{$HOL3Set1}&
\ttindexbold{Int} &
\verb$\<inter>$\\
-\indexboldpos{\isasymUnion}{$HOL3Set2}&
+\isasymUnion\index{$HOL3Set2@\isasymUnion|bold}&
\ttindexbold{UN}, \ttindexbold{Union} &
\verb$\<Union>$\\
-\indexboldpos{\isasymInter}{$HOL3Set2}&
+\isasymInter\index{$HOL3Set2@\isasymInter|bold}&
\ttindexbold{INT}, \ttindexbold{Inter} &
\verb$\<Inter>$\\
\hline