\<^loc>\ x = \<^loc>\" 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 \ int \ \\group \ \\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 \ \\group \ \\group" where "pow_nat 0 x = \" | "pow_nat (Suc n) x = x \ pow_nat n x" @@ -493,7 +493,7 @@ pow_int :: "int \ \\group \ \\group" where "pow_int k x = (if k >= 0 then pow_nat (nat k) x - else (pow_nat (nat (- k)) x)\

)" + else (pow_nat (nat (- k)) x)\

)"*) definition example :: int where diff -r b924fac38eec -r c6f5cc939c29 doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs --- 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; diff -r b924fac38eec -r c6f5cc939c29 doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML --- 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); diff -r b924fac38eec -r c6f5cc939c29 doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex --- 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 diff -r b924fac38eec -r c6f5cc939c29 doc-src/IsarRef/generic.tex --- 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. diff -r b924fac38eec -r c6f5cc939c29 doc-src/isar.sty --- 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}