# HG changeset patch
# User blanchet
# Date 1266863478 -3600
# Node ID 40da65ef68e3e7b4a13aeccae0261f4b85a69bd7
# Parent  9edc2bd6d2bdc2aadccdc0185793776d3abdbc09# Parent  8fd9d555d04dbb2f0acfe8407c9593367ac061f8
merge

diff -r 9edc2bd6d2bd -r 40da65ef68e3 doc-src/Classes/Thy/Classes.thy
--- 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
diff -r 9edc2bd6d2bd -r 40da65ef68e3 doc-src/Classes/Thy/document/Classes.tex
--- 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}%
 %
diff -r 9edc2bd6d2bd -r 40da65ef68e3 doc-src/IsarRef/Thy/Spec.thy
--- 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}
diff -r 9edc2bd6d2bd -r 40da65ef68e3 doc-src/IsarRef/Thy/document/Spec.tex
--- 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}%
diff -r 9edc2bd6d2bd -r 40da65ef68e3 src/Provers/trancl.ML
--- 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);