# HG changeset patch
# User haftmann
# Date 1245227642 -7200
# Node ID 127e8a8b8cde6806beb8efc1ea373572d6aa493b
# Parent  614a8c4c9c0f870f617fe23c78f5243821a4e580
refined section concerning classes

diff -r 614a8c4c9c0f -r 127e8a8b8cde doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Wed Jun 17 10:11:33 2009 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Jun 17 10:34:02 2009 +0200
@@ -585,6 +585,7 @@
     @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -599,8 +600,12 @@
     ;
     'instance'
     ;
+    'instance' nameref '::' arity
+    ;
     'subclass' target? nameref
     ;
+    'instance' nameref ('<' | subseteq) nameref
+    ;
     'print\_classes'
     ;
     'class\_deps'
@@ -649,12 +654,24 @@
   the type classes involved.  After finishing the proof, the
   background theory will be augmented by the proven type arities.
 
+  On the theory level, @{command "instance"}~@{text "t :: (s\<^sub>1, \<dots>,
+  s\<^sub>n)s"} provides a convenient way to instantiate a type class with no
+  need to specifify operations: one can continue with the
+  instantiation proof immediately.
+
   \item @{command "subclass"}~@{text c} in a class context for class
   @{text d} sets up a goal stating that class @{text c} is logically
   contained in class @{text d}.  After finishing the proof, class
   @{text d} is proven to be subclass @{text c} and the locale @{text
   c} is interpreted into @{text d} simultaneously.
 
+  A weakend form of this is available through a further variant of
+  @{command instance}:  @{command instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} opens
+  a proof that class @{text "c\<^isub>2"} implies @{text "c\<^isub>1"} without reference
+  to the underlying locales;  this is useful if the properties to prove
+  the logical connection are not sufficent on the locale level but on
+  the theory level.
+
   \item @{command "print_classes"} prints all classes in the current
   theory.
 
@@ -703,20 +720,17 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
+    @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"}
   \end{matharray}
 
   Axiomatic type classes are Isabelle/Pure's primitive
-  \emph{definitional} interface to type classes.  For practical
+  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 +)
     ;
-    'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
-    ;
   \end{rail}
 
   \begin{description}
@@ -736,14 +750,6 @@
   here.  The full collection of these facts is also stored as @{text
   c_class.axioms}.
   
-  \item @{command "instance"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} and @{command
-  "instance"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} setup a goal stating a class
-  relation or type arity.  The proof would usually proceed by @{method
-  intro_classes}, and then establish the characteristic theorems of
-  the type classes involved.  After finishing the proof, the theory
-  will be augmented by a type signature declaration corresponding to
-  the resulting theorem.
-
   \end{description}
 *}
 
diff -r 614a8c4c9c0f -r 127e8a8b8cde doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Jun 17 10:11:33 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Jun 17 10:34:02 2009 +0200
@@ -599,6 +599,7 @@
     \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
+    \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
     \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
@@ -613,8 +614,12 @@
     ;
     'instance'
     ;
+    'instance' nameref '::' arity
+    ;
     'subclass' target? nameref
     ;
+    'instance' nameref ('<' | subseteq) nameref
+    ;
     'print\_classes'
     ;
     'class\_deps'
@@ -656,11 +661,22 @@
   the type classes involved.  After finishing the proof, the
   background theory will be augmented by the proven type arities.
 
+  On the theory level, \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s{\isachardoublequote}} provides a convenient way to instantiate a type class with no
+  need to specifify operations: one can continue with the
+  instantiation proof immediately.
+
   \item \hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c} in a class context for class
   \isa{d} sets up a goal stating that class \isa{c} is logically
   contained in class \isa{d}.  After finishing the proof, class
   \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
 
+  A weakend form of this is available through a further variant of
+  \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}:  \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} opens
+  a proof that class \isa{{\isachardoublequote}c\isactrlisub {\isadigit{2}}{\isachardoublequote}} implies \isa{{\isachardoublequote}c\isactrlisub {\isadigit{1}}{\isachardoublequote}} without reference
+  to the underlying locales;  this is useful if the properties to prove
+  the logical connection are not sufficent on the locale level but on
+  the theory level.
+
   \item \hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}} prints all classes in the current
   theory.
 
@@ -713,8 +729,7 @@
 %
 \begin{isamarkuptext}%
 \begin{matharray}{rcl}
-    \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
-    \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
+    \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
@@ -725,8 +740,6 @@
   \begin{rail}
     'axclass' classdecl (axmdecl prop +)
     ;
-    'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
-    ;
   \end{rail}
 
   \begin{description}
@@ -743,12 +756,6 @@
   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}.
   
-  \item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s{\isachardoublequote}} setup a goal stating a class
-  relation or type arity.  The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of
-  the type classes involved.  After finishing the proof, the theory
-  will be augmented by a type signature declaration corresponding to
-  the resulting theorem.
-
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%