# HG changeset patch
# User haftmann
# Date 1189877264 -7200
# Node ID d3fca349736c3f1cfe45e87c769cfacbd051dcf5
# Parent  ed9a1254d6748b89f4039b299844c13572daa7ff
clarified class interfaces and internals

diff -r ed9a1254d674 -r d3fca349736c src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sat Sep 15 19:27:43 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Sep 15 19:27:44 2007 +0200
@@ -427,7 +427,7 @@
         val n = Sign.arity_number thy tyco;
       in
         thy
-        |> Class.prove_instance_arity (Class.intro_classes_tac [])
+        |> Class.prove_instance (Class.intro_classes_tac [])
             [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
         |> snd
       end
diff -r ed9a1254d674 -r d3fca349736c src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Sat Sep 15 19:27:43 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Sat Sep 15 19:27:44 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/datatype_codegen.ML
+(*  Title:      HOL/Tools/datatype_codegen.ML
     ID:         $Id$
     Author:     Stefan Berghofer & Florian Haftmann, TU Muenchen
 
@@ -590,7 +590,7 @@
         |> not (null arities) ? (
             f arities css
             #-> (fn defs =>
-              Class.prove_instance_arity tac arities defs
+              Class.prove_instance tac arities defs
             #-> (fn defs =>
               after_qed arities css defs)))
       end;
diff -r ed9a1254d674 -r d3fca349736c src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sat Sep 15 19:27:43 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Sat Sep 15 19:27:44 2007 +0200
@@ -565,7 +565,7 @@
         val n = Sign.arity_number thy tyco;
       in
         thy
-        |> Class.prove_instance_arity (Class.intro_classes_tac [])
+        |> Class.prove_instance (Class.intro_classes_tac [])
             [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
         |> snd
       end
diff -r ed9a1254d674 -r d3fca349736c src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Sep 15 19:27:43 2007 +0200
+++ b/src/Pure/Isar/class.ML	Sat Sep 15 19:27:44 2007 +0200
@@ -10,23 +10,32 @@
   val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix
 
   val axclass_cmd: bstring * xstring list
-    -> ((bstring * Attrib.src list) * string list) list -> theory -> class * theory
+    -> ((bstring * Attrib.src list) * string list) list
+    -> theory -> class * theory
+  val classrel_cmd: xstring * xstring -> theory -> Proof.state
   val class: bstring -> class list -> Element.context_i Locale.element list
     -> string list -> theory -> string * Proof.context
-  val class_cmd: bstring -> string list -> Element.context Locale.element list
-    -> string list -> theory -> string * Proof.context
-  val class_of_locale: theory -> string -> class option
+  val class_cmd: bstring -> xstring list -> Element.context Locale.element list
+    -> xstring list -> theory -> string * Proof.context
   val add_const_in_class: string -> (string * term) * Syntax.mixfix
     -> theory -> theory
+  val interpretation_in_class: class * class -> theory -> Proof.state
+  val interpretation_in_class_cmd: xstring * xstring -> theory -> Proof.state
+  val prove_interpretation_in_class: tactic -> class * class -> theory -> theory
+  val intro_classes_tac: thm list -> tactic
+  val default_intro_classes_tac: thm list -> tactic
+  val class_of_locale: theory -> string -> class option
+  val print_classes: theory -> unit
 
-  val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list
+  val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
+  val instance: arity list -> ((bstring * Attrib.src list) * term) list
     -> (thm list -> theory -> theory)
     -> theory -> Proof.state
-  val instance_arity_cmd: (bstring * string list * string) list
-    -> ((bstring * Attrib.src list) * string) list
+  val instance_cmd: (bstring * xstring list * xstring) list
+    -> ((bstring * Attrib.src list) * xstring) list
     -> (thm list -> theory -> theory)
     -> theory -> Proof.state
-  val prove_instance_arity: tactic -> arity list
+  val prove_instance: tactic -> arity list
     -> ((bstring * Attrib.src list) * term) list
     -> theory -> thm list * theory
   val unoverload: theory -> conv
@@ -35,16 +44,6 @@
   val inst_const: theory -> string * string -> string
   val param_const: theory -> string -> (string * string) option
   val params_of_sort: theory -> sort -> (string * (string * typ)) list
-  val intro_classes_tac: thm list -> tactic
-  val default_intro_classes_tac: thm list -> tactic
-
-  val instance_class: class * class -> theory -> Proof.state
-  val instance_class_cmd: string * string -> theory -> Proof.state
-  val instance_sort: class * sort -> theory -> Proof.state
-  val instance_sort_cmd: string * string -> theory -> Proof.state
-  val prove_instance_sort: tactic -> class * sort -> theory -> theory
-
-  val print_classes: theory -> unit
 end;
 
 structure Class : CLASS =
@@ -60,20 +59,55 @@
     val mx_local = if is_loc then mx else NoSyn;
   in (mx_global, mx_local) end;
 
+fun prove_interpretation tac prfx_atts expr insts =
+  Locale.interpretation_i I prfx_atts expr insts
+  #> Proof.global_terminal_proof
+      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
+  #> ProofContext.theory_of;
+
+fun prove_interpretation_in tac after_qed (name, expr) =
+  Locale.interpretation_in_locale
+      (ProofContext.theory after_qed) (name, expr)
+  #> Proof.global_terminal_proof
+      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
+  #> ProofContext.theory_of;
+
+fun OF_LAST thm1 thm2 =
+  let
+    val n = (length o Logic.strip_imp_prems o prop_of) thm2;
+  in (thm1 RSN (n, thm2)) end;
+
+fun strip_all_ofclass thy sort =
+  let
+    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
+    fun prem_inclass t =
+      case Logic.strip_imp_prems t
+       of ofcls :: _ => try Logic.dest_inclass ofcls
+        | [] => NONE;
+    fun strip_ofclass class thm =
+      thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
+    fun strip thm = case (prem_inclass o Thm.prop_of) thm
+     of SOME (_, class) => thm |> strip_ofclass class |> strip
+      | NONE => thm;
+  in strip end;
+
+
+(** axclass command **)
+
 fun axclass_cmd (class, raw_superclasses) raw_specs thy =
   let
     val ctxt = ProofContext.init thy;
     val superclasses = map (Sign.read_class thy) raw_superclasses;
-    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) raw_specs;
-    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) raw_specs)
+    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
+      raw_specs;
+    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
+          raw_specs)
       |> snd
       |> (map o map) fst;
-  in AxClass.define_class (class, superclasses) [] (name_atts ~~ axiomss) thy end;
-
-
-(** axclasses with implicit parameter handling **)
-
-(* axclass instances *)
+  in
+    AxClass.define_class (class, superclasses) []
+      (name_atts ~~ axiomss) thy
+  end;
 
 local
 
@@ -84,54 +118,25 @@
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts)
+    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])])
+        o maps (mk_prop thy)) insts)
   end;
 
 in
 
-val axclass_instance_arity =
+val instance_arity =
   gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
-val axclass_instance_sort =
+val classrel =
   gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
     AxClass.add_classrel I o single;
+val classrel_cmd =
+  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel))
+    AxClass.add_classrel I o single;
 
 end; (*local*)
 
 
-(* introducing axclasses with implicit parameter handling *)
-
-fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
-  let
-    val superclasses = map (Sign.certify_class thy) raw_superclasses;
-    val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
-    val prefix = Logic.const_of_class name;
-    fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix)
-      (Sign.full_name thy c);
-    fun add_const ((c, ty), syn) =
-      Sign.add_consts_authentic [(c, ty, syn)]
-      #> pair (mk_const_name c, ty);
-    fun mk_axioms cs thy =
-      raw_dep_axioms thy cs
-      |> (map o apsnd o map) (Sign.cert_prop thy)
-      |> rpair thy;
-    fun add_constraint class (c, ty) =
-      Sign.add_const_constraint_i (c, SOME
-        (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
-  in
-    thy
-    |> Theory.add_path prefix
-    |> fold_map add_const consts
-    ||> Theory.restore_naming thy
-    |-> (fn cs => mk_axioms cs
-    #-> (fn axioms_prop => AxClass.define_class (name, superclasses)
-           (map fst cs @ other_consts) axioms_prop
-    #-> (fn class => `(fn thy => AxClass.get_definition thy class)
-    #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
-    #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))
-  end;
-
-
-(* explicit constants for overloaded definitions *)
+(** explicit constants for overloaded definitions **)
 
 structure InstData = TheoryDataFun
 (
@@ -146,22 +151,22 @@
       Symtab.merge (K true) (tabb1, tabb2));
 );
 
-fun inst_thms f thy =
-  (Symtab.fold (Symtab.fold (cons o f o snd o snd) o snd) o fst) (InstData.get thy) [];
-fun add_inst (c, tyco) inst = (InstData.map o apfst o Symtab.map_default (c, Symtab.empty))
-  (Symtab.update_new (tyco, inst))
+fun inst_thms f thy = (Symtab.fold (Symtab.fold (cons o f o snd o snd) o snd) o fst)
+    (InstData.get thy) [];
+fun add_inst (c, tyco) inst = (InstData.map o apfst
+      o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
   #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
 
-fun unoverload thy thm = MetaSimplifier.rewrite false (inst_thms I thy) thm;
-fun overload thy thm = MetaSimplifier.rewrite false (inst_thms symmetric thy) thm;
+fun unoverload thy = MetaSimplifier.rewrite false (inst_thms I thy);
+fun overload thy = MetaSimplifier.rewrite false (inst_thms symmetric thy);
 
 fun inst_const thy (c, tyco) =
   (fst o the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
 fun unoverload_const thy (c_ty as (c, _)) =
   case AxClass.class_of_param thy c
    of SOME class => (case Sign.const_typargs thy c_ty
-       of [Type (tyco, _)] =>
-            (case Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c) tyco
+       of [Type (tyco, _)] => (case Symtab.lookup
+           ((the o Symtab.lookup (fst (InstData.get thy))) c) tyco
              of SOME (c, _) => c
               | NONE => c)
         | [_] => c)
@@ -192,7 +197,8 @@
 
 fun add_def ((class, tyco), ((name, prop), atts)) thy =
   let
-    val ((lhs as Const (c, ty), args), rhs) = (apfst Term.strip_comb o Logic.dest_equals) prop;
+    val ((lhs as Const (c, ty), args), rhs) =
+      (apfst Term.strip_comb o Logic.dest_equals) prop;
     fun add_inst' def ([], (Const (c_inst, ty))) =
           if forall (fn TFree _ => true | _ => false) (Sign.const_typargs thy (c_inst, ty))
           then add_inst (c, tyco) (c_inst, def)
@@ -205,7 +211,7 @@
   end;
 
 
-(* instances with implicit parameter handling *)
+(** instances with implicit parameter handling **)
 
 local
 
@@ -223,7 +229,7 @@
 fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm;
 fun read_def thy = gen_read_def thy (K I) (K I);
 
-fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
+fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
   let
     val arities = map (prep_arity theory) raw_arities;
     val _ = if null arities then error "at least one arity must be given" else ();
@@ -231,7 +237,8 @@
      of [] => ()
       | dupl_tycos => error ("type constructors occur more than once in arities: "
           ^ (commas o map quote) dupl_tycos);
-    val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory
+    val super_sort =
+      (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory;
     fun get_consts_class tyco ty class =
       let
         val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class;
@@ -241,7 +248,8 @@
       end;
     fun get_consts_sort (tyco, asorts, sort) =
       let
-        val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.names Name.context "'a" asorts))
+        val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort))
+          (Name.names Name.context "'a" asorts))
       in maps (get_consts_class tyco ty) (super_sort sort) end;
     val cs = maps get_consts_sort arities;
     fun mk_typnorm thy (ty, ty_sc) =
@@ -288,8 +296,6 @@
     |-> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs)
   end;
 
-fun instance_arity_cmd' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof;
-fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof;
 fun tactic_proof tac f arities defs =
   fold (fn arity => AxClass.prove_arity arity tac) arities
   #> f
@@ -297,26 +303,27 @@
 
 in
 
-val instance_arity_cmd = instance_arity_cmd'
-  (fn f => fn arities => fn defs => axclass_instance_arity f arities);
-val instance_arity = instance_arity'
-  (fn f => fn arities => fn defs => axclass_instance_arity f arities);
-fun prove_instance_arity tac arities defs =
-  instance_arity' (tactic_proof tac) arities defs (K I);
+val instance = gen_instance Sign.cert_arity read_def
+  (fn f => fn arities => fn defs => instance_arity f arities);
+val instance_cmd = gen_instance Sign.read_arity read_def_cmd
+  (fn f => fn arities => fn defs => instance_arity f arities);
+fun prove_instance tac arities defs =
+  gen_instance Sign.cert_arity read_def
+    (tactic_proof tac) arities defs (K I);
 
 end; (*local*)
 
 
 
-(** combining locales and axclasses **)
-
-(* theory data *)
+(** class data **)
 
 datatype class_data = ClassData of {
   locale: string,
   consts: (string * string) list
     (*locale parameter ~> toplevel theory constant*),
   v: string option,
+  inst: typ Symtab.table * term Symtab.table
+    (*canonical interpretation*),
   intro: thm
 } * thm list (*derived defs*);
 
@@ -336,13 +343,13 @@
 
 (* queries *)
 
-val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o fst o ClassData.get;
+val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node
+  o fst o ClassData.get;
 fun class_of_locale thy = Symtab.lookup ((snd o ClassData.get) thy);
 
-fun the_class_data thy class =
-  case lookup_class_data thy class
-    of NONE => error ("undeclared class " ^ quote class)
-     | SOME data => data;
+fun the_class_data thy class = case lookup_class_data thy class
+ of NONE => error ("undeclared class " ^ quote class)
+  | SOME data => data;
 
 val ancestry = Graph.all_succs o fst o ClassData.get;
 
@@ -391,18 +398,18 @@
       ]
     ]
   in
-    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.all_classes)
-      algebra
+    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "")
+      o map mk_entry o Sorts.all_classes) algebra
   end;
 
 
 (* updaters *)
 
-fun add_class_data ((class, superclasses), (locale, consts, v, intro)) =
+fun add_class_data ((class, superclasses), (locale, consts, v, inst, intro)) =
   ClassData.map (fn (gr, tab) => (
     gr
     |> Graph.new_node (class, ClassData ({ locale = locale, consts = consts,
-         v = v, intro = intro }, []))
+         v = v, inst = inst, intro = intro }, []))
     |> fold (curry Graph.add_edge class) superclasses,
     tab
     |> Symtab.update (locale, class)
@@ -411,7 +418,65 @@
 fun add_class_const_thm (class, thm) = (ClassData.map o apfst o Graph.map_node class)
   (fn ClassData (data, thms) => ClassData (data, thm :: thms));
 
-(* tactics and methods *)
+
+(** rule calculation, tactics and methods **)
+
+fun class_intro thy locale class sups =
+  let
+    fun class_elim class =
+      case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class
+       of [thm] => SOME thm
+        | [] => NONE;
+    val pred_intro = case Locale.intros thy locale
+     of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME
+      | ([intro], []) => SOME intro
+      | ([], [intro]) => SOME intro
+      | _ => NONE;
+    val pred_intro' = pred_intro
+      |> Option.map (fn intro => intro OF map_filter class_elim sups);
+    val class_intro = (#intro o AxClass.get_definition thy) class;
+    val raw_intro = case pred_intro'
+     of SOME pred_intro => class_intro |> OF_LAST pred_intro
+      | NONE => class_intro;
+    val sort = Sign.super_classes thy class;
+    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
+    val defs = these_defs thy sups;
+  in
+    raw_intro
+    |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] []
+    |> strip_all_ofclass thy sort
+    |> Thm.strip_shyps
+    |> MetaSimplifier.rewrite_rule defs
+    |> Drule.unconstrainTs
+  end;
+
+fun class_interpretation class facts defs thy =
+  let
+    val ({ locale, inst, ... }, _) = the_class_data thy class;
+    val tac = (ALLGOALS o ProofContext.fact_tac) facts;
+    val prfx = Logic.const_of_class (NameSpace.base class);
+  in
+    prove_interpretation tac ((false, prfx), []) (Locale.Locale locale)
+      (inst, defs) thy
+  end;
+
+fun interpretation_in_rule thy (class1, class2) =
+  let
+    fun mk_axioms class =
+      let
+        val ({ locale, inst = (_, insttab), ... }, _) = the_class_data thy class;
+      in
+        Locale.global_asms_of thy locale
+        |> maps snd
+        |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup insttab) s | t => t)
+        |> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1]) | T => T)
+        |> map (ObjectLogic.ensure_propT thy)
+      end;
+    val (prems, concls) = pairself mk_axioms (class1, class2);
+  in
+    Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls)
+      (Locale.intro_locales_tac true (ProofContext.init thy))
+  end;
 
 fun intro_classes_tac facts st =
   let
@@ -443,102 +508,9 @@
     "apply some intro/elim rule")]);
 
 
-(* tactical interfaces to locale commands *)
-
-fun prove_interpretation tac prfx_atts expr insts thy =
-  thy
-  |> Locale.interpretation_i I prfx_atts expr insts
-  |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
-  |> ProofContext.theory_of;
-
-fun prove_interpretation_in tac after_qed (name, expr) thy =
-  thy
-  |> Locale.interpretation_in_locale (ProofContext.theory after_qed) (name, expr)
-  |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
-  |> ProofContext.theory_of;
-
-
-(* constructing class introduction and other rules from axclass and locale rules *)
-
-fun mk_instT class = Symtab.empty
-  |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
-
-fun mk_inst class param_names cs =
-  Symtab.empty
-  |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
-       (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
-
-fun OF_LAST thm1 thm2 =
-  let
-    val n = (length o Logic.strip_imp_prems o prop_of) thm2;
-  in (thm1 RSN (n, thm2)) end;
-
-fun strip_all_ofclass thy sort =
-  let
-    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
-    fun prem_inclass t =
-      case Logic.strip_imp_prems t
-       of ofcls :: _ => try Logic.dest_inclass ofcls
-        | [] => NONE;
-    fun strip_ofclass class thm =
-      thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
-    fun strip thm = case (prem_inclass o Thm.prop_of) thm
-     of SOME (_, class) => thm |> strip_ofclass class |> strip
-      | NONE => thm;
-  in strip end;
+(** classes and class target **)
 
-fun class_intro thy locale class sups =
-  let
-    fun class_elim class =
-      case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class
-       of [thm] => SOME thm
-        | [] => NONE;
-    val pred_intro = case Locale.intros thy locale
-     of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME
-      | ([intro], []) => SOME intro
-      | ([], [intro]) => SOME intro
-      | _ => NONE;
-    val pred_intro' = pred_intro
-      |> Option.map (fn intro => intro OF map_filter class_elim sups);
-    val class_intro = (#intro o AxClass.get_definition thy) class;
-    val raw_intro = case pred_intro'
-     of SOME pred_intro => class_intro |> OF_LAST pred_intro
-      | NONE => class_intro;
-    val sort = Sign.super_classes thy class;
-    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
-    val defs = these_defs thy sups;
-  in
-    raw_intro
-    |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] []
-    |> strip_all_ofclass thy sort
-    |> Thm.strip_shyps
-    |> MetaSimplifier.rewrite_rule defs
-    |> Drule.unconstrainTs
-  end;
-
-fun interpretation_in_rule thy (class1, class2) =
-  let
-    val (params, consts) = split_list (params_of_sort thy [class1]);
-    (*FIXME also remember this at add_class*)
-    fun mk_axioms class =
-      let
-        val name_locale = (#locale o fst o the_class_data thy) class;
-        val inst = mk_inst class params consts;
-      in
-        Locale.global_asms_of thy name_locale
-        |> maps snd
-        |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup inst) s | t => t)
-        |> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1]) | T => T)
-        |> map (ObjectLogic.ensure_propT thy)
-      end;
-    val (prems, concls) = pairself mk_axioms (class1, class2);
-  in
-    Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls)
-      (Locale.intro_locales_tac true (ProofContext.init thy))
-  end;
-
-
-(* classes *)
+(* class definition *)
 
 local
 
@@ -553,11 +525,18 @@
 fun gen_class add_locale prep_class prep_param bname
     raw_supclasses raw_elems raw_other_consts thy =
   let
+    fun mk_instT class = Symtab.empty
+      |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
+    fun mk_inst class param_names cs =
+      Symtab.empty
+      |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
+           (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
     (*FIXME need proper concept for reading locale statements*)
     fun subst_classtyvar (_, _) =
           TFree (AxClass.param_tyvarname, [])
       | subst_classtyvar (v, sort) =
-          error ("Sort constraint illegal in type class, for type variable " ^ v ^ "::" ^ Sign.string_of_sort thy sort);
+          error ("Sort constraint illegal in type class, for type variable "
+            ^ v ^ "::" ^ Sign.string_of_sort thy sort);
     (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,
       typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)
     val other_consts = map (prep_param thy) raw_other_consts;
@@ -602,7 +581,7 @@
         val super_defs = these_defs thy sups;
         fun prep_asm ((name, atts), ts) =
           ((NameSpace.base name, map (Attrib.attribute thy) atts),
-            (map o map_aterms) ((*MetaSimplifier.rewrite_term thy super_defs [] o *)subst) ts);
+            (map o map_aterms) subst ts);
       in
         Locale.global_asms_of thy name_locale
         |> map prep_asm
@@ -617,21 +596,17 @@
     |-> (fn name_locale => ProofContext.theory_result (
       `(fn thy => extract_params thy name_locale)
       #-> (fn (v, (param_names, params)) =>
-        axclass_params (bname, supsort) params (extract_assumes name_locale params) other_consts
-      #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
+        AxClass.define_class_params (bname, supsort) params
+          (extract_assumes name_locale params) other_consts
+      #-> (fn (name_axclass, (consts, axioms)) =>
         `(fn thy => class_intro thy name_locale name_axclass sups)
       #-> (fn class_intro =>
         add_class_data ((name_axclass, sups),
           (name_locale, map (fst o fst) params ~~ map fst consts, v,
-            class_intro))
-        (*FIXME: class_data should already contain data relevant
-          for interpretation; use this later for class target*)
-        (*FIXME: general export_fixes which may be parametrized
-          with pieces of an emerging class*)
+            (mk_instT name_axclass, mk_inst name_axclass param_names
+              (map snd supconsts @ consts)), class_intro))
       #> note_intro name_axclass class_intro
-      #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
-          ((false, Logic.const_of_class bname), []) (Locale.Locale name_locale)
-          ((mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts)), [])
+      #> class_interpretation name_axclass axioms []
       #> pair name_axclass
       )))))
   end;
@@ -643,73 +618,8 @@
 
 end; (*local*)
 
-local
 
-fun instance_subclass (class1, class2) thy  =
-  let
-    val interp = interpretation_in_rule thy (class1, class2);
-    val ax = #axioms (AxClass.get_definition thy class1);
-    val intro = #intro (AxClass.get_definition thy class2)
-      |> Drule.instantiate' [SOME (Thm.ctyp_of thy
-          (TVar ((AxClass.param_tyvarname, 0), [class1])))] [];
-    val thm = 
-      intro
-      |> OF_LAST (interp OF ax)
-      |> strip_all_ofclass thy (Sign.super_classes thy class2);
-  in
-    thy |> AxClass.add_classrel thm
-  end;
-
-fun instance_subsort (class, sort) thy =
-  let
-    val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra
-      o Sign.classes_of) thy sort;
-    val classes = filter_out (fn class' => Sign.subsort thy ([class], [class']))
-      (rev super_sort);
-  in
-    thy |> fold (curry instance_subclass class) classes
-  end;
-
-fun instance_sort' do_proof (class, sort) theory =
-  let
-    val loc_name = (#locale o fst o the_class_data theory) class;
-    val loc_expr =
-      (Locale.Merge o map (Locale.Locale o #locale o fst o the_class_data theory)) sort;
-  in
-    theory
-    |> do_proof (instance_subsort (class, sort)) (loc_name, loc_expr)
-  end;
-
-fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory =
-  let
-    val class = prep_class theory raw_class;
-    val sort = prep_sort theory raw_sort;
-  in
-    theory
-    |> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort)
-  end;
-
-fun gen_instance_class prep_class (raw_class, raw_superclass) theory =
-  let
-    val class = prep_class theory raw_class;
-    val superclass = prep_class theory raw_superclass;
-  in
-    theory
-    |> axclass_instance_sort (class, superclass)
-  end;
-
-in
-
-val instance_sort_cmd = gen_instance_sort Sign.read_class Syntax.global_read_sort;
-val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort;
-val prove_instance_sort = instance_sort' o prove_interpretation_in;
-val instance_class_cmd = gen_instance_class Sign.read_class;
-val instance_class = gen_instance_class Sign.certify_class;
-
-end; (*local*)
-
-
-(** class target **)
+(* definition in class target *)
 
 fun export_fixes thy class =
   let
@@ -740,14 +650,10 @@
     val (syn', _) = fork_mixfix true NONE syn;
     fun interpret def =
       let
-        val def' = symmetric def
-        val tac = (ALLGOALS o ProofContext.fact_tac) [def'];
-        val name_locale = (#locale o fst o the_class_data thy) class;
+        val def' = symmetric def;
         val def_eq = Thm.prop_of def';
-        val (params, consts) = split_list (params_of_sort thy [class]);
       in
-        prove_interpretation tac ((false, prfx), []) (Locale.Locale name_locale)
-          ((mk_instT class, mk_inst class params consts), [def_eq])
+        class_interpretation class [def'] [def_eq]
         #> add_class_const_thm (class, def')
       end;
   in
@@ -762,4 +668,53 @@
     |> Sign.restore_naming thy
   end;
 
+
+(* interpretation in class target *)
+
+local
+
+fun gen_interpretation_in_class prep_class do_proof (raw_class, raw_superclass) theory =
+  let
+    val class = prep_class theory raw_class;
+    val superclass = prep_class theory raw_superclass;
+    val loc_name = (#locale o fst o the_class_data theory) class;
+    val loc_expr = (Locale.Locale o #locale o fst o the_class_data theory) superclass;
+    fun prove_classrel (class, superclass) thy =
+      let
+        val classes = (Graph.all_succs o #classes o Sorts.rep_algebra
+              o Sign.classes_of) thy [superclass]
+          |> filter_out (fn class' => Sign.subsort thy ([class], [class']));
+        fun instance_subclass (class1, class2) thy  =
+          let
+            val interp = interpretation_in_rule thy (class1, class2);
+            val ax = #axioms (AxClass.get_definition thy class1);
+            val intro = #intro (AxClass.get_definition thy class2)
+              |> Drule.instantiate' [SOME (Thm.ctyp_of thy
+                  (TVar ((AxClass.param_tyvarname, 0), [class1])))] [];
+            val thm = 
+              intro
+              |> OF_LAST (interp OF ax)
+              |> strip_all_ofclass thy (Sign.super_classes thy class2);
+          in
+            thy |> AxClass.add_classrel thm
+          end;
+      in
+        thy |> fold_rev (curry instance_subclass class) classes
+      end;
+  in
+    theory
+    |> do_proof (prove_classrel (class, superclass)) (loc_name, loc_expr)
+  end;
+
+in
+
+val interpretation_in_class = gen_interpretation_in_class Sign.certify_class
+  (Locale.interpretation_in_locale o ProofContext.theory);
+val interpretation_in_class_cmd = gen_interpretation_in_class Sign.read_class
+  (Locale.interpretation_in_locale o ProofContext.theory);
+val prove_interpretation_in_class = gen_interpretation_in_class Sign.certify_class
+  o prove_interpretation_in;
+
+end; (*local*)
+
 end;
diff -r ed9a1254d674 -r d3fca349736c src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Sep 15 19:27:43 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Sep 15 19:27:44 2007 +0200
@@ -427,13 +427,24 @@
 val instanceP =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
       P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
-           >> Class.instance_class_cmd
+           >> Class.classrel_cmd
       || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
-           >> Class.instance_sort_cmd
+           >> Class.interpretation_in_class_cmd
       || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
-           >> (fn (arities, defs) => Class.instance_arity_cmd arities defs (fold (Code.add_func false)))
+           >> (fn (arities, defs) => Class.instance_cmd arities defs (fold (Code.add_func false)))
     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
 
+val instantiationP =
+  OuterSyntax.command "instantiation" "prove type arity" K.thy_decl (
+      P.and_list1 P.arity -- P.opt_begin
+           >> (fn (arities, begin) => (begin ? Toplevel.print)
+            o Toplevel.begin_local_theory begin
+                (Instance.begin_instantiation_cmd arities)));
+
+val instance_proofP =
+  OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal
+      (Scan.succeed ((Toplevel.print oo Toplevel.local_theory_to_proof NONE) Instance.proof_instantiation));
+
 end;
 
 
@@ -993,7 +1004,7 @@
   simproc_setupP, parse_ast_translationP, parse_translationP,
   print_translationP, typed_print_translationP,
   print_ast_translationP, token_translationP, oracleP, contextP,
-  localeP, classP, instanceP, code_datatypeP,
+  localeP, classP, instanceP, instantiationP, instance_proofP, code_datatypeP,
   (*proof commands*)
   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
diff -r ed9a1254d674 -r d3fca349736c src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Sep 15 19:27:43 2007 +0200
+++ b/src/Pure/axclass.ML	Sat Sep 15 19:27:44 2007 +0200
@@ -8,6 +8,16 @@
 
 signature AX_CLASS =
 sig
+  val define_class: bstring * class list -> string list ->
+    ((bstring * attribute list) * term list) list -> theory -> class * theory
+  val define_class_params: bstring * class list -> ((bstring * typ) * mixfix) list ->
+    (theory -> (string * typ) list -> ((bstring * attribute list) * term list) list) ->
+    string list -> theory ->
+    (class * ((string * typ) list * thm list)) * theory
+  val add_classrel: thm -> theory -> theory
+  val add_arity: thm -> theory -> theory
+  val prove_classrel: class * class -> tactic -> theory -> theory
+  val prove_arity: string * sort list * sort -> tactic -> theory -> theory
   val get_definition: theory -> class -> {def: thm, intro: thm, axioms: thm list,
     params: (string * typ) list}
   val class_intros: theory -> thm list
@@ -17,12 +27,6 @@
   val print_axclasses: theory -> unit
   val cert_classrel: theory -> class * class -> class * class
   val read_classrel: theory -> xstring * xstring -> class * class
-  val add_classrel: thm -> theory -> theory
-  val add_arity: thm -> theory -> theory
-  val prove_classrel: class * class -> tactic -> theory -> theory
-  val prove_arity: string * sort list * sort -> tactic -> theory -> theory
-  val define_class: bstring * class list -> string list ->
-    ((bstring * attribute list) * term list) list -> theory -> class * theory
   val axiomatize_class: bstring * xstring list -> theory -> theory
   val axiomatize_class_i: bstring * class list -> theory -> theory
   val axiomatize_classrel: (xstring * xstring) list -> theory -> theory
@@ -359,6 +363,40 @@
 
 
 
+(** axclasses with implicit parameter handling **)
+
+fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
+  let
+    val superclasses = map (Sign.certify_class thy) raw_superclasses;
+    val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
+    val prefix = Logic.const_of_class name;
+    fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix)
+      (Sign.full_name thy c);
+    fun add_const ((c, ty), syn) =
+      Sign.add_consts_authentic [(c, ty, syn)]
+      #> pair (mk_const_name c, ty);
+    fun mk_axioms cs thy =
+      raw_dep_axioms thy cs
+      |> (map o apsnd o map) (Sign.cert_prop thy)
+      |> rpair thy;
+    fun add_constraint class (c, ty) =
+      Sign.add_const_constraint_i (c, SOME
+        (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
+  in
+    thy
+    |> Theory.add_path prefix
+    |> fold_map add_const consts
+    ||> Theory.restore_naming thy
+    |-> (fn cs => mk_axioms cs
+    #-> (fn axioms_prop => define_class (name, superclasses)
+           (map fst cs @ other_consts) axioms_prop
+    #-> (fn class => `(fn thy => get_definition thy class)
+    #-> (fn {axioms, ...} => fold (add_constraint class) cs
+    #> pair (class, (cs, axioms))))))
+  end;
+
+
+
 (** axiomatizations **)
 
 local