--- a/doc-src/Classes/Thy/Classes.thy Mon Feb 22 19:31:00 2010 +0100
+++ b/doc-src/Classes/Thy/Classes.thy Mon Feb 22 19:31:18 2010 +0100
@@ -362,17 +362,18 @@
text {*
\noindent The connection to the type system is done by means
- of a primitive axclass
+ of a primitive type class
*} (*<*)setup %invisible {* Sign.add_path "foo" *}
(*>*)
-axclass %quote idem < type
- idem: "f (f x) = f x" (*<*)setup %invisible {* Sign.parent_path *}(*>*)
+classes %quote idem < type
+(*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x"
+setup %invisible {* Sign.parent_path *}(*>*)
text {* \noindent together with a corresponding interpretation: *}
interpretation %quote idem_class:
idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
-proof qed (rule idem)
+(*<*)proof qed (rule idem)(*>*)
text {*
\noindent This gives you the full power of the Isabelle module system;
@@ -414,8 +415,7 @@
subsection {* Derived definitions *}
text {*
- Isabelle locales support a concept of local definitions
- in locales:
+ Isabelle locales are targets which support local definitions:
*}
primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
--- a/doc-src/Classes/Thy/document/Classes.tex Mon Feb 22 19:31:00 2010 +0100
+++ b/doc-src/Classes/Thy/document/Classes.tex Mon Feb 22 19:31:18 2010 +0100
@@ -641,7 +641,7 @@
%
\begin{isamarkuptext}%
\noindent The connection to the type system is done by means
- of a primitive axclass%
+ of a primitive type class%
\end{isamarkuptext}%
\isamarkuptrue%
\ %
@@ -663,9 +663,8 @@
\endisadelimquote
%
\isatagquote
-\isacommand{axclass}\isamarkupfalse%
-\ idem\ {\isacharless}\ type\isanewline
-\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ %
+\isacommand{classes}\isamarkupfalse%
+\ idem\ {\isacharless}\ type%
\endisatagquote
{\isafoldquote}%
%
@@ -698,10 +697,7 @@
\isatagquote
\isacommand{interpretation}\isamarkupfalse%
\ idem{\isacharunderscore}class{\isacharcolon}\isanewline
-\ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\ \isacommand{qed}\isamarkupfalse%
-\ {\isacharparenleft}rule\ idem{\isacharparenright}%
+\ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
--- a/doc-src/IsarRef/Thy/Spec.thy Mon Feb 22 19:31:00 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Mon Feb 22 19:31:18 2010 +0100
@@ -738,44 +738,6 @@
*}
-subsection {* Old-style axiomatic type classes \label{sec:axclass} *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"}
- \end{matharray}
-
- Axiomatic type classes are Isabelle/Pure's primitive
- interface to type classes. For practical
- applications, you should consider using classes
- (cf.~\secref{sec:classes}) which provide high level interface.
-
- \begin{rail}
- 'axclass' classdecl (axmdecl prop +)
- ;
- \end{rail}
-
- \begin{description}
-
- \item @{command "axclass"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n axms"} defines an
- axiomatic type class as the intersection of existing classes, with
- additional axioms holding. Class axioms may not contain more than
- one type variable. The class axioms (with implicit sort constraints
- added) are bound to the given names. Furthermore a class
- introduction rule is generated (being bound as @{text
- c_class.intro}); this rule is employed by method @{method
- intro_classes} to support instantiation proofs of this class.
-
- The ``class axioms'' (which are derived from the internal class
- definition) are stored as theorems according to the given name
- specifications; the name space prefix @{text "c_class"} is added
- here. The full collection of these facts is also stored as @{text
- c_class.axioms}.
-
- \end{description}
-*}
-
-
section {* Unrestricted overloading *}
text {*
@@ -962,8 +924,9 @@
\item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass
relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}.
- This is done axiomatically! The @{command_ref "instance"} command
- (see \secref{sec:axclass}) provides a way to introduce proven class
+ This is done axiomatically! The @{command_ref "instance"}
+ and @{command_ref "subclass"} command
+ (see \secref{sec:class}) provide a way to introduce proven class
relations.
\item @{command "defaultsort"}~@{text s} makes sort @{text s} the
@@ -1021,8 +984,8 @@
\item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
Isabelle's order-sorted signature of types by new type constructor
- arities. This is done axiomatically! The @{command_ref "instance"}
- command (see \secref{sec:axclass}) provides a way to introduce
+ arities. This is done axiomatically! The @{command_ref "instantiation"}
+ target (see \secref{sec:class}) provides a way to introduce
proven type arities.
\end{description}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Feb 22 19:31:00 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Feb 22 19:31:18 2010 +0100
@@ -755,43 +755,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Old-style axiomatic type classes \label{sec:axclass}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}}
- \end{matharray}
-
- Axiomatic type classes are Isabelle/Pure's primitive
- interface to type classes. For practical
- applications, you should consider using classes
- (cf.~\secref{sec:classes}) which provide high level interface.
-
- \begin{rail}
- 'axclass' classdecl (axmdecl prop +)
- ;
- \end{rail}
-
- \begin{description}
-
- \item \hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}} defines an
- axiomatic type class as the intersection of existing classes, with
- additional axioms holding. Class axioms may not contain more than
- one type variable. The class axioms (with implicit sort constraints
- added) are bound to the given names. Furthermore a class
- introduction rule is generated (being bound as \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class.
-
- The ``class axioms'' (which are derived from the internal class
- definition) are stored as theorems according to the given name
- specifications; the name space prefix \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} is added
- here. The full collection of these facts is also stored as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Unrestricted overloading%
}
\isamarkuptrue%
@@ -996,8 +959,9 @@
\item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} states subclass
relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
- This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command
- (see \secref{sec:axclass}) provides a way to introduce proven class
+ This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
+ and \indexref{}{command}{subclass}\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}} command
+ (see \secref{sec:class}) provide a way to introduce proven class
relations.
\item \hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s} makes sort \isa{s} the
@@ -1056,8 +1020,8 @@
\item \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s{\isachardoublequote}} augments
Isabelle's order-sorted signature of types by new type constructor
- arities. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
- command (see \secref{sec:axclass}) provides a way to introduce
+ arities. This is done axiomatically! The \indexref{}{command}{instantiation}\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
+ target (see \secref{sec:class}) provides a way to introduce
proven type arities.
\end{description}%
--- a/src/Provers/trancl.ML Mon Feb 22 19:31:00 2010 +0100
+++ b/src/Provers/trancl.ML Mon Feb 22 19:31:18 2010 +0100
@@ -541,9 +541,11 @@
val prems = flat (map_index (mkasm_trancl rel o swap) Hs);
val prfs = solveTrancl (prems, C);
in
- Subgoal.FOCUS (fn {prems, ...} =>
- let val thms = map (prove thy rel prems) prfs
- in rtac (prove thy rel thms prf) 1 end) ctxt n st
+ Subgoal.FOCUS (fn {prems, concl, ...} =>
+ let
+ val SOME (_, _, rel', _) = decomp (term_of concl);
+ val thms = map (prove thy rel' prems) prfs
+ in rtac (prove thy rel' thms prf) 1 end) ctxt n st
end
handle Cannot => Seq.empty);
@@ -558,9 +560,11 @@
val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
val prfs = solveRtrancl (prems, C);
in
- Subgoal.FOCUS (fn {prems, ...} =>
- let val thms = map (prove thy rel prems) prfs
- in rtac (prove thy rel thms prf) 1 end) ctxt n st
+ Subgoal.FOCUS (fn {prems, concl, ...} =>
+ let
+ val SOME (_, _, rel', _) = decomp (term_of concl);
+ val thms = map (prove thy rel' prems) prfs
+ in rtac (prove thy rel' thms prf) 1 end) ctxt n st
end
handle Cannot => Seq.empty | Subscript => Seq.empty);