--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Thu Oct 11 23:03:51 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Fri Oct 12 08:20:43 2007 +0200
@@ -2,7 +2,7 @@
(*<*)
theory Classes
-imports Main Pretty_Int
+imports Main Code_Integer
begin
ML {*
@@ -110,7 +110,7 @@
From a software enigineering point of view, type classes
correspond to interfaces in object-oriented languages like Java;
so, it is naturally desirable that type classes do not only
- provide functions (class operations) but also state specifications
+ provide functions (class parameters) but also state specifications
implementations must obey. For example, the @{text "class eq"}
above could be given the following specification, demanding that
@{text "class eq"} is an equivalence relation obeying reflexivity,
@@ -130,9 +130,9 @@
all those aspects together:
\begin{enumerate}
- \item specifying abstract operations togehter with
+ \item specifying abstract parameters together with
corresponding specifications,
- \item instantating those abstract operations by a particular
+ \item instantating those abstract parameters by a particular
type
\item in connection with a ``less ad-hoc'' approach to overloading,
\item with a direct link to the Isabelle module system
@@ -159,7 +159,7 @@
text {*
Depending on an arbitrary type @{text "\<alpha>"}, class @{text
- "semigroup"} introduces a binary operation @{text "\<circ>"} that is
+ "semigroup"} introduces a binary operator @{text "\<otimes>"} that is
assumed to be associative:
*}
@@ -169,11 +169,11 @@
text {*
\noindent This @{text "\<CLASS>"} specification consists of two
- parts: the \qn{operational} part names the class operation (@{text
+ parts: the \qn{operational} part names the class parameter (@{text
"\<FIXES>"}), the \qn{logical} part specifies properties on them
(@{text "\<ASSUMES>"}). The local @{text "\<FIXES>"} and @{text
"\<ASSUMES>"} are lifted to the theory toplevel, yielding the global
- operation @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
+ parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
global theorem @{text "semigroup.assoc:"}~@{prop [source] "\<And>x y
z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
*}
@@ -183,7 +183,7 @@
text {*
The concrete type @{text "int"} is made a @{text "semigroup"}
- instance by providing a suitable definition for the class operation
+ instance by providing a suitable definition for the class parameter
@{text "mult"} and a proof for the specification of @{text "assoc"}.
*}
@@ -217,7 +217,7 @@
text {*
\noindent Also @{text "list"}s form a semigroup with @{const "op @"} as
- operation:
+ parameter:
*}
instance list :: (type) semigroup
@@ -237,7 +237,7 @@
text {*
We define a subclass @{text "monoidl"} (a semigroup with a left-hand neutral)
by extending @{text "semigroup"}
- with one additional operation @{text "neutral"} together
+ with one additional parameter @{text "neutral"} together
with its property:
*}
@@ -247,7 +247,7 @@
text {*
\noindent Again, we make some instances, by
- providing suitable operation definitions and proofs for the
+ providing suitable parameter definitions and proofs for the
additional specifications.
*}
@@ -279,7 +279,7 @@
text {*
\noindent Fully-fledged monoids are modelled by another subclass
- which does not add new operations but tightens the specification:
+ which does not add new parameters but tightens the specification:
*}
class monoid = monoidl +
@@ -429,7 +429,7 @@
*}
-(*subsection {* Additional subclass relations *}
+subsection {* Additional subclass relations *}
text {*
Any @{text "group"} is also a @{text "monoid"}; this
@@ -437,7 +437,7 @@
together with a proof of the logical difference:
*}
- instance advanced group < monoid
+ subclass (in group) monoid
proof unfold_locales
fix x
from invl have "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>" by simp
@@ -452,7 +452,7 @@
open to proof to the user. After the proof it is propagated
to the type system, making @{text group} an instance of
@{text monoid}. For illustration, a derived definition
- in @{text group} which uses @{text of_nat}:
+ in @{text group} which uses @{text pow_nat}:
*}
definition (in group)
@@ -465,7 +465,7 @@
yields the global definition of
@{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"}
with the corresponding theorem @{thm pow_int_def [no_vars]}.
-*} *)
+*}
section {* Further issues *}
@@ -484,7 +484,7 @@
For example, lets go back to the power function:
*}
- fun
+(* fun
pow_nat :: "nat \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group" where
"pow_nat 0 x = \<one>"
| "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
@@ -493,7 +493,7 @@
pow_int :: "int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group" where
"pow_int k x = (if k >= 0
then pow_nat (nat k) x
- else (pow_nat (nat (- k)) x)\<div>)"
+ else (pow_nat (nat (- k)) x)\<div>)"*)
definition
example :: int where
--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Thu Oct 11 23:03:51 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Fri Oct 12 08:20:43 2007 +0200
@@ -20,7 +20,10 @@
neutral :: a;
};
-class (Classes.Monoidl a) => Group a where {
+class (Classes.Monoidl a) => Monoid a where {
+};
+
+class (Classes.Monoid a) => Group a where {
inverse :: a -> a;
};
@@ -41,11 +44,14 @@
neutral = Classes.neutral_int;
};
+instance Classes.Monoid Integer where {
+};
+
instance Classes.Group Integer where {
inverse = Classes.inverse_int;
};
-pow_nat :: (Classes.Group b) => Classes.Nat -> b -> b;
+pow_nat :: (Classes.Monoid a) => Classes.Nat -> a -> a;
pow_nat (Classes.Suc n) x = Classes.mult x (Classes.pow_nat n x);
pow_nat Classes.Zero_nat x = Classes.neutral;
--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Thu Oct 11 23:03:51 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML Fri Oct 12 08:20:43 2007 +0200
@@ -19,8 +19,11 @@
fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;
fun neutral (A_:'a monoidl) = #neutral A_;
-type 'a group = {Classes__monoidl_group : 'a monoidl, inverse : 'a -> 'a};
-fun monoidl_group (A_:'a group) = #Classes__monoidl_group A_;
+type 'a monoid = {Classes__monoidl_monoid : 'a monoidl};
+fun monoidl_monoid (A_:'a monoid) = #Classes__monoidl_monoid A_;
+
+type 'a group = {Classes__monoid_group : 'a monoid, inverse : 'a -> 'a};
+fun monoid_group (A_:'a group) = #Classes__monoid_group A_;
fun inverse (A_:'a group) = #inverse A_;
fun inverse_int i = IntInf.~ i;
@@ -35,17 +38,21 @@
{Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :
IntInf.int monoidl;
+val monoid_int = {Classes__monoidl_monoid = monoidl_int} :
+ IntInf.int monoid;
+
val group_int =
- {Classes__monoidl_group = monoidl_int, inverse = inverse_int} :
+ {Classes__monoid_group = monoid_int, inverse = inverse_int} :
IntInf.int group;
-fun pow_nat B_ (Suc n) x =
- mult ((semigroup_monoidl o monoidl_group) B_) x (pow_nat B_ n x)
- | pow_nat B_ Zero_nat x = neutral (monoidl_group B_);
+fun pow_nat A_ (Suc n) x =
+ mult ((semigroup_monoidl o monoidl_monoid) A_) x (pow_nat A_ n x)
+ | pow_nat A_ Zero_nat x = neutral (monoidl_monoid A_);
fun pow_int A_ k x =
- (if IntInf.<= ((0 : IntInf.int), k) then pow_nat A_ (nat k) x
- else inverse A_ (pow_nat A_ (nat (IntInf.~ k)) x));
+ (if IntInf.<= ((0 : IntInf.int), k)
+ then pow_nat (monoid_group A_) (nat k) x
+ else inverse A_ (pow_nat (monoid_group A_) (nat (IntInf.~ k)) x));
val example : IntInf.int =
pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Thu Oct 11 23:03:51 2007 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Fri Oct 12 08:20:43 2007 +0200
@@ -89,7 +89,7 @@
From a software enigineering point of view, type classes
correspond to interfaces in object-oriented languages like Java;
so, it is naturally desirable that type classes do not only
- provide functions (class operations) but also state specifications
+ provide functions (class parameters) but also state specifications
implementations must obey. For example, the \isa{class\ eq}
above could be given the following specification, demanding that
\isa{class\ eq} is an equivalence relation obeying reflexivity,
@@ -109,9 +109,9 @@
all those aspects together:
\begin{enumerate}
- \item specifying abstract operations togehter with
+ \item specifying abstract parameters togehter with
corresponding specifications,
- \item instantating those abstract operations by a particular
+ \item instantating those abstract parameters by a particular
type
\item in connection with a ``less ad-hoc'' approach to overloading,
\item with a direct link to the Isabelle module system
@@ -142,7 +142,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operation \isa{{\isasymcirc}} that is
+Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isasymotimes}} that is
assumed to be associative:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -152,9 +152,9 @@
\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}y\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent This \isa{{\isasymCLASS}} specification consists of two
- parts: the \qn{operational} part names the class operation (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
+ parts: the \qn{operational} part names the class parameter (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
(\isa{{\isasymASSUMES}}). The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
- operation \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
+ parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -165,7 +165,7 @@
%
\begin{isamarkuptext}%
The concrete type \isa{int} is made a \isa{semigroup}
- instance by providing a suitable definition for the class operation
+ instance by providing a suitable definition for the class parameter
\isa{mult} and a proof for the specification of \isa{assoc}.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -240,7 +240,7 @@
%
\begin{isamarkuptext}%
\noindent Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as
- operation:%
+ parameter:%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \ \ \isacommand{instance}\isamarkupfalse%
@@ -285,7 +285,7 @@
\begin{isamarkuptext}%
We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
by extending \isa{semigroup}
- with one additional operation \isa{neutral} together
+ with one additional parameter \isa{neutral} together
with its property:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -295,7 +295,7 @@
\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}\isactrlloc {\isasymone}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent Again, we make some instances, by
- providing suitable operation definitions and proofs for the
+ providing suitable parameter definitions and proofs for the
additional specifications.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -396,7 +396,7 @@
%
\begin{isamarkuptext}%
\noindent Fully-fledged monoids are modelled by another subclass
- which does not add new operations but tightens the specification:%
+ which does not add new parameters but tightens the specification:%
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \ \ \isacommand{class}\isamarkupfalse%
@@ -691,6 +691,72 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Additional subclass relations%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+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{subclass}\isamarkupfalse%
+\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline
+%
+\isadelimproof
+\ \ \ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ unfold{\isacharunderscore}locales\isanewline
+\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ x\isanewline
+\ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
+\ invl\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
+\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
+\ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \ \ \isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+The logical proof is carried out on the locale level
+ and thus conveniently is opened using the \isa{unfold{\isacharunderscore}locales}
+ method which only leaves the logical differences still
+ open to proof to the user. After the proof it is propagated
+ to the type system, making \isa{group} an instance of
+ \isa{monoid}. For illustration, a derived definition
+ in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ \ \ \isacommand{definition}\isamarkupfalse%
+\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\isanewline
+\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
+\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
+\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}\isactrlloc {\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+yields the global definition of
+ \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
+ with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Further issues%
}
\isamarkuptrue%
@@ -711,19 +777,6 @@
For example, lets go back to the power function:%
\end{isamarkuptext}%
\isamarkuptrue%
-\ \ \ \ \isacommand{fun}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline
-\isanewline
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
-\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
-\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
\ \ \ \ \isacommand{definition}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
--- a/doc-src/IsarRef/generic.tex Thu Oct 11 23:03:51 2007 +0200
+++ b/doc-src/IsarRef/generic.tex Fri Oct 12 08:20:43 2007 +0200
@@ -519,24 +519,21 @@
\indexisarcmd{instance}\indexisarcmd{class}\indexisarcmd{print-classes}
\begin{matharray}{rcl}
\isarcmd{class} & : & \isartrans{theory}{local{\dsh}theory} \\
+ \isarcmd{subclass} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
\isarcmd{print_classes}^* & : & \isarkeep{theory~|~proof} \\
\end{matharray}
\begin{rail}
- 'class' name '=' classexpr 'begin'?
+ 'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) 'begin'?
;
- 'instance' (instarity | instsubsort)
+ 'subclass' target? nameref
+ ;
+ 'instance' (nameref '::' arity + 'and') (axmdecl prop +)?
;
'print\_classes'
;
- classexpr: ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+))
- ;
- instarity: (nameref '::' arity + 'and') (axmdecl prop +)?
- ;
- instsubsort: nameref ('<' | subseteq) sort
- ;
superclassexpr: nameref | (nameref '+' superclassexpr)
;
\end{rail}
@@ -555,12 +552,12 @@
constraining
the free type variable to sort $c$.
-\item [$\INSTANCE~a: \vec{arity}~\vec{defs}$]
+\item [$\INSTANCE~~t :: (\vec s)s \vec{defs}$]
sets up a goal stating type arities. The proof would usually
proceed by $intro_classes$, and then establish the characteristic theorems
of the type classes involved.
The $defs$, if given, must correspond to the class parameters
- involved in the $arities$ and are introduces in the theory
+ involved in the $arities$ and are introduced in the theory
before proof.
After finishing the proof, the theory will be
augmented by a type signature declaration corresponding to the
@@ -568,12 +565,10 @@
This $\isarcmd{instance}$ command is actually an extension
of primitive axclass $\isarcmd{instance}$ (see \ref{sec:axclass}).
-\item [$\INSTANCE~c \subseteq \vec{c}$] sets up a
- goal stating
- the interpretation of the locale corresponding to $c$
- in the merge of all locales corresponding to $\vec{c}$.
- After finishing the proof, it is automatically lifted to
- prove the additional class relation $c \subseteq \vec{c}$.
+\item [$\SUBCLASS~c$] in a class context for class $d$
+ sets up a goal stating that class $c$ is logically
+ contained in class $d$. After finishing the proof, class $d$ is proven
+ to be subclass $c$ and the locale $c$ is interpreted into $d$ simultaneously.
\item [$\isarkeyword{print_classes}$] prints all classes
in the current theory.
--- a/doc-src/isar.sty Thu Oct 11 23:03:51 2007 +0200
+++ b/doc-src/isar.sty Fri Oct 12 08:20:43 2007 +0200
@@ -83,6 +83,7 @@
\newcommand{\THEOREMS}{\isarkeyword{theorems}}
\newcommand{\LOCALE}{\isarkeyword{locale}}
\newcommand{\CLASS}{\isarkeyword{class}}
+\newcommand{\SUBCLASS}{\isarkeyword{subclass}}
\newcommand{\TEXT}{\isarkeyword{text}}
\newcommand{\TXT}{\isarkeyword{txt}}
\newcommand{\NOTE}[2]{\NOTENAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2}