tuned interfaces of class module

--- a/src/HOL/Tools/datatype_codegen.ML	Wed Nov 28 09:01:40 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Nov 28 09:01:42 2007 +0100
@@ -432,7 +432,7 @@
     |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
     |> Thm.implies_intr asm
     |> Thm.generalize ([], params) 0
-    |> Conv.fconv_rule (Class.unoverload thy)
+    |> Class.unoverload thy
     |> Thm.varifyT
   end;
 
@@ -572,7 +572,7 @@
     fun add_eq_thms (dtco, (_, (vs, cs))) thy =
       let
         val thy_ref = Theory.check_thy thy;
-        val const = Class.inst_const thy ("op =", dtco);
+        val const = Class.param_of_inst thy ("op =", dtco);
         val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
       in
         Code.add_funcl (const, Susp.delay get_thms) thy

--- a/src/Pure/Isar/class.ML	Wed Nov 28 09:01:40 2007 +0100
+++ b/src/Pure/Isar/class.ML	Wed Nov 28 09:01:42 2007 +0100
@@ -12,35 +12,42 @@
     -> string list -> theory -> string * Proof.context
   val class_cmd: bstring -> xstring list -> Element.context Locale.element list
     -> xstring list -> theory -> string * Proof.context
-  val is_class: theory -> class -> bool
-  val these_params: theory -> sort -> (string * (string * typ)) list
+
   val init: class -> theory -> Proof.context
-  val add_logical_const: string -> Markup.property list
+  val logical_const: string -> Markup.property list
     -> (string * mixfix) * term -> theory -> theory
-  val add_syntactic_const: string -> Syntax.mode -> Markup.property list
+  val syntactic_const: string -> Syntax.mode -> Markup.property list
     -> (string * mixfix) * term -> theory -> theory
   val refresh_syntax: class -> Proof.context -> Proof.context
+
   val intro_classes_tac: thm list -> tactic
   val default_intro_classes_tac: thm list -> tactic
   val prove_subclass: class * class -> thm list -> Proof.context
     -> theory -> theory
+
+  val class_prefix: string -> string
+  val is_class: theory -> class -> bool
+  val these_params: theory -> sort -> (string * (string * typ)) list
   val print_classes: theory -> unit
-  val class_prefix: string -> string
 
   (*instances*)
-  val declare_overloaded: string * typ * mixfix -> theory -> term * theory
-  val define_overloaded: string -> string * term -> theory -> thm * theory
-  val unoverload: theory -> conv
-  val overload: theory -> conv
+  val init_instantiation: arity list -> theory -> local_theory
+  val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
+  val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
+  val conclude_instantiation: local_theory -> local_theory
+
+  val overloaded_const: string * typ * mixfix -> theory -> term * theory
+  val overloaded_def: string -> string * term -> theory -> thm * theory
+  val instantiation_param: Proof.context -> string -> string option
+  val confirm_declaration: string -> local_theory -> local_theory
+
+  val unoverload: theory -> thm -> thm
+  val overload: theory -> thm -> thm
+  val unoverload_conv: theory -> conv
+  val overload_conv: theory -> conv
   val unoverload_const: theory -> string * typ -> string
-  val inst_const: theory -> string * string -> string
-  val param_const: theory -> string -> (string * string) option
-  val instantiation: arity list -> theory -> local_theory
-  val proof_instantiation: (local_theory -> local_theory) -> local_theory -> Proof.state
-  val prove_instantiation: (Proof.context -> tactic) -> local_theory -> local_theory
-  val conclude_instantiation: local_theory -> local_theory
-  val end_instantiation: local_theory -> Proof.context
-  val instantiation_const: Proof.context -> string -> string option
+  val param_of_inst: theory -> string * string -> string
+  val inst_of_param: theory -> string -> (string * string) option
 
   (*old axclass layer*)
   val axclass_cmd: bstring * xstring list
@@ -109,7 +116,7 @@
   end;
 
 
-(** axclass command **)
+(** primitive axclass and instance commands **)
 
 fun axclass_cmd (class, raw_superclasses) raw_specs thy =
   let
@@ -175,26 +182,27 @@
 fun inst thy (c, tyco) =
   (the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
 
-val inst_const = fst oo inst;
+val param_of_inst = fst oo inst;
 
 fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
   (InstData.get thy) [];
 
-val param_const = Symtab.lookup o snd o InstData.get;
+val inst_of_param = Symtab.lookup o snd o InstData.get;
 
 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 = MetaSimplifier.rewrite true (inst_thms thy);
-fun overload thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
+fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
+fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
+
+fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
+fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
 
 fun unoverload_const thy (c_ty as (c, _)) =
   case AxClass.class_of_param thy c
    of SOME class => (case inst_tyco thy c_ty
-       of SOME tyco => (case try (inst thy) (c, tyco)
-             of SOME (c, _) => c
-              | NONE => c)
+       of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
         | NONE => c)
     | NONE => c;
 
@@ -205,18 +213,20 @@
   PureThy.note_thmss_i kind [((name, []), [([thm], [])])]
   #>> (fn [(_, [thm])] => thm);
 
-fun declare_overloaded (c, ty, mx) thy =
+fun overloaded_const (c, ty, mx) thy =
   let
+    val _ = if mx <> NoSyn then
+      error ("Illegal mixfix syntax for constant to be instantiated " ^ quote c)
+      else ()
     val SOME class = AxClass.class_of_param thy c;
     val SOME tyco = inst_tyco thy (c, ty);
-    val name_inst = NameSpace.base class ^ "_" ^ NameSpace.base tyco ^ "_inst";
+    val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
     val c' = NameSpace.base c;
     val ty' = Type.strip_sorts ty;
   in
     thy
     |> Sign.sticky_prefix name_inst
     |> Sign.no_base_names
-    |> Sign.notation true Syntax.mode_default [(Const (c, ty), mx)]
     |> Sign.declare_const [] (c', ty', NoSyn)
     |-> (fn const' as Const (c'', _) => Thm.add_def true
           (Thm.def_name c', Logic.mk_equals (Const (c, ty'), const'))
@@ -228,22 +238,18 @@
     #> pair (Const (c, ty))))
   end;
 
-fun define_overloaded name (c, t) thy =
+fun overloaded_def name (c, t) thy =
   let
     val ty = Term.fastype_of t;
     val SOME tyco = inst_tyco thy (c, ty);
     val (c', eq) = inst thy (c, tyco);
-    val [Type (_, tys)] = Sign.const_typargs thy (c, ty);
-    val eq' = eq
-      |> Drule.instantiate' (map (SOME o Thm.ctyp_of thy) tys) [];
-          (*FIXME proper recover_sort mechanism*)
     val prop = Logic.mk_equals (Const (c', ty), t);
-    val name' = if name = "" then
-      Thm.def_name (NameSpace.base c ^ "_" ^ NameSpace.base tyco) else name;
+    val name' = Thm.def_name_optional
+      (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
   in
     thy
     |> Thm.add_def false (name', prop)
-    |>> (fn thm => Thm.transitive eq' thm)
+    |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
   end;
 
 
@@ -911,9 +917,9 @@
 end; (*local*)
 
 
-(* definition in class target *)
+(* class target *)
 
-fun add_logical_const class pos ((c, mx), dict) thy =
+fun logical_const class pos ((c, mx), dict) thy =
   let
     val prfx = class_prefix class;
     val thy' = thy |> Sign.add_path prfx;
@@ -928,7 +934,7 @@
   in
     thy'
     |> Sign.declare_const pos (c, ty'', mx) |> snd
-    |> Thm.add_def false (c, def_eq)    (* FIXME PureThy.add_defs_i *)
+    |> Thm.add_def false (c, def_eq)
     |>> Thm.symmetric
     |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
           #> register_operation class (c', (dict', SOME (Thm.varifyT def))))
@@ -936,10 +942,7 @@
     |> Sign.add_const_constraint (c', SOME ty')
   end;
 
-
-(* abbreviation in class target *)
-
-fun add_syntactic_const class prmode pos ((c, mx), rhs) thy =
+fun syntactic_const class prmode pos ((c, mx), rhs) thy =
   let
     val prfx = class_prefix class;
     val thy' = thy |> Sign.add_path prfx;
@@ -974,51 +977,26 @@
   fun init _ = Instantiation { arities = [], params = [] };
 );
 
-fun mk_instantiation (arities, params) = Instantiation {
-    arities = arities, params = params
-  };
+fun mk_instantiation (arities, params) =
+  Instantiation { arities = arities, params = params };
+fun get_instantiation ctxt = case Instantiation.get ctxt
+ of Instantiation data => data;
 fun map_instantiation f (Instantiation { arities, params }) =
   mk_instantiation (f (arities, params));
 
-fun the_instantiation ctxt = case Instantiation.get ctxt
- of Instantiation { arities = [], ... } => error "No instantiation target"
-  | Instantiation data => data;
+fun the_instantiation ctxt = case get_instantiation ctxt
+ of { arities = [], ... } => error "No instantiation target"
+  | data => data;
 
-fun init_instantiation arities ctxt =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    val _ = if null arities then error "At least one arity must be given" else ();
-    val _ = case (duplicates (op =) o map #1) arities
-     of [] => ()
-      | dupl_tycos => error ("Type constructors occur more than once in arities: "
-          ^ commas_quote dupl_tycos);
-    val ty_insts = map (fn (tyco, sorts, _) =>
-        (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
-      arities;
-    val ty_inst = the o AList.lookup (op =) ty_insts;
-    fun type_name "*" = "prod"
-      | type_name "+" = "sum"
-      | type_name s = NameSpace.base s; (*FIXME*)
-    fun get_param tyco sorts (param, (c, ty)) =
-      ((unoverload_const thy (c, ty), tyco),
-        (param ^ "_" ^ type_name tyco,
-          map_atyps (K (ty_inst tyco)) ty));
-    fun get_params (tyco, sorts, sort) =
-      map (get_param tyco sorts) (these_params thy sort)
-    val params = maps get_params arities;
-  in
-    ctxt
-    |> Instantiation.put (mk_instantiation (arities, params))
-    |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts
-    |> fold (Variable.declare_term o Free o snd) params
-  end;
+val instantiation_params = #params o get_instantiation;
 
-val instantiation_params = #params o the_instantiation;
-
-fun instantiation_const ctxt v = instantiation_params ctxt
+fun instantiation_param ctxt v = instantiation_params ctxt
   |> find_first (fn (_, (v', _)) => v = v')
   |> Option.map (fst o fst);
 
+fun confirm_declaration c = (Instantiation.map o map_instantiation o apsnd)
+  (filter_out (fn (_, (c', _)) => c' = c));
+
 
 (* syntax *)
 
@@ -1057,21 +1035,58 @@
 
 (* target *)
 
-fun instantiation arities =
-  ProofContext.init
-  #> init_instantiation arities
-  #> fold ProofContext.add_arity arities
-  #> Context.proof_map (
-      Syntax.add_term_check 0 "instance" inst_term_check
-      #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck);
+val sanatize_name = (*FIXME*)
+  let
+    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
+    val is_junk = not o is_valid andf Symbol.is_regular;
+    val junk = Scan.many is_junk;
+    val scan_valids = Symbol.scanner "Malformed input"
+      ((junk |--
+        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
+        --| junk))
+      -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
+  in
+    explode #> scan_valids #> implode
+  end;
+
 
-fun gen_proof_instantiation do_proof after_qed lthy =
+fun init_instantiation arities thy =
   let
-    (*FIXME should work on fresh context but continue local theory afterwards*)
+    val _ = if null arities then error "At least one arity must be given" else ();
+    val _ = case (duplicates (op =) o map #1) arities
+     of [] => ()
+      | dupl_tycos => error ("Type constructors occur more than once in arities: "
+          ^ commas_quote dupl_tycos);
+    val ty_insts = map (fn (tyco, sorts, _) =>
+        (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
+      arities;
+    val ty_inst = the o AList.lookup (op =) ty_insts;
+    fun type_name "*" = "prod"
+      | type_name "+" = "sum"
+      | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
+    fun get_param tyco sorts (param, (c, ty)) =
+      ((unoverload_const thy (c, ty), tyco),
+        (param ^ "_" ^ type_name tyco,
+          map_atyps (K (ty_inst tyco)) ty));
+    fun get_params (tyco, sorts, sort) =
+      map (get_param tyco sorts) (these_params thy sort)
+    val params = maps get_params arities;
+  in
+    thy
+    |> ProofContext.init
+    |> Instantiation.put (mk_instantiation (arities, params))
+    |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts
+    |> fold ProofContext.add_arity arities
+    |> Context.proof_map (
+        Syntax.add_term_check 0 "instance" inst_term_check
+        #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck)
+  end;
+
+fun gen_instantiation_instance do_proof after_qed lthy =
+  let
     val ctxt = LocalTheory.target_of lthy;
     val arities = (#arities o the_instantiation) ctxt;
-    val arities_proof = maps
-      (Logic.mk_arities o Sign.cert_arity (ProofContext.theory_of ctxt)) arities;
+    val arities_proof = maps Logic.mk_arities arities;
     fun after_qed' results =
       LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
       #> after_qed;
@@ -1080,16 +1095,16 @@
     |> do_proof after_qed' arities_proof
   end;
 
-val proof_instantiation = gen_proof_instantiation (fn after_qed => fn ts =>
+val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
   Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
 
-fun prove_instantiation tac = gen_proof_instantiation (fn after_qed =>
+fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
   fn ts => fn lthy => after_qed (Goal.prove_multi lthy [] [] ts
     (fn {context, ...} => tac context)) lthy) I;
 
 fun conclude_instantiation lthy =
   let
-    val arities = (#arities o the_instantiation) lthy;
+    val { arities, params } = the_instantiation lthy;
     val thy = ProofContext.theory_of lthy;
     (*val _ = map (fn (tyco, sorts, sort) =>
       if Sign.of_sort thy
@@ -1101,20 +1116,21 @@
     val missing_params = arities
       |> maps (fn (tyco, _, sort) => params_of sort |> map (rpair tyco))
       |> filter_out (can (inst thy) o apfst fst);
-    fun declare_missing ((c, ty), tyco) thy =
+    fun declare_missing ((c, ty0), tyco) thy =
+    (*fun declare_missing ((c, tyco), (_, ty)) thy =*)
       let
         val SOME class = AxClass.class_of_param thy c;
-        val name_inst = NameSpace.base class ^ "_" ^ NameSpace.base tyco ^ "_inst";
+        val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
+        val c' = NameSpace.base c;
         val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []);
-        val ty' = map_atyps (fn _ => Type (tyco, map TFree vs)) ty;
-        val c' = NameSpace.base c;
+        val ty = map_atyps (fn _ => Type (tyco, map TFree vs)) ty0;
       in
         thy
         |> Sign.sticky_prefix name_inst
         |> Sign.no_base_names
-        |> Sign.declare_const [] (c', ty', NoSyn)
+        |> Sign.declare_const [] (c', ty, NoSyn)
         |-> (fn const' as Const (c'', _) => Thm.add_def true
-              (Thm.def_name c', Logic.mk_equals (const', Const (c, ty')))
+              (Thm.def_name c', Logic.mk_equals (const', Const (c, ty)))
         #>> Thm.varifyT
         #-> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm)
         #> primitive_note Thm.internalK (c', thm)
@@ -1126,6 +1142,4 @@
     |> LocalTheory.theory (fold declare_missing missing_params)
   end;
 
-val end_instantiation = conclude_instantiation #> LocalTheory.target_of;
-
 end;

--- a/src/Pure/Isar/code.ML	Wed Nov 28 09:01:40 2007 +0100
+++ b/src/Pure/Isar/code.ML	Wed Nov 28 09:01:42 2007 +0100
@@ -3,7 +3,7 @@
     Author:     Florian Haftmann, TU Muenchen
 
 Abstract executable content of theory.  Management of data dependent on
-executable content.  Cache assumes non-concurrent processing of a singly theory.
+executable content.  Cache assumes non-concurrent processing of a single theory.
 *)
 
 signature CODE =
@@ -24,7 +24,9 @@
   val del_post: thm -> theory -> theory
   val add_datatype: (string * typ) list -> theory -> theory
   val add_datatype_cmd: string list -> theory -> theory
-  val type_interpretation: (string * string list -> theory -> theory) -> theory -> theory
+  val type_interpretation:
+    (string * ((string * sort) list * (string * typ list) list)
+      -> theory -> theory) -> theory -> theory
   val add_case: thm -> theory -> theory
   val add_undefined: string -> theory -> theory
 
@@ -546,7 +548,7 @@
     val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
     val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class;
     val funcs = classparams
-      |> map_filter (fn c => try (Class.inst_const thy) (c, tyco))
+      |> map_filter (fn c => try (Class.param_of_inst thy) (c, tyco))
       |> map (Symtab.lookup ((the_funcs o the_exec) thy))
       |> (map o Option.map) (Susp.force o fst o snd)
       |> maps these
@@ -664,7 +666,7 @@
            ^ CodeUnit.string_of_typ thy ty_decl)
       end;
     fun check_typ (c, thm) =
-      case Class.param_const thy c
+      case Class.inst_of_param thy c
        of SOME (c, tyco) => check_typ_classparam tyco (c, thm)
         | NONE => check_typ_fun (c, thm);
   in check_typ (const_of_func thy thm, thm) end;
@@ -777,8 +779,7 @@
 val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute
   (fn thm => Context.mapping (add_default_func thm) I));
 
-structure TypeInterpretation = InterpretationFun(type T = string * string list val eq = op =);
-val type_interpretation = TypeInterpretation.interpretation;
+structure TypeInterpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
 
 fun add_datatype raw_cs thy =
   let
@@ -792,9 +793,12 @@
     thy
     |> map_exec_purge purge_cs (map_dtyps (Symtab.update (tyco, vs_cos))
         #> map_funcs (fold (Symtab.delete_safe o fst) cs))
-    |> TypeInterpretation.data (tyco, cs')
+    |> TypeInterpretation.data (tyco, serial ())
   end;
 
+fun type_interpretation f =  TypeInterpretation.interpretation
+  (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
+
 fun add_datatype_cmd raw_cs thy =
   let
     val cs = map (CodeUnit.read_bare_const thy) raw_cs;
@@ -906,7 +910,7 @@
   |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o the_exec) thy)
 (*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
   |> common_typ_funcs
-  |> map (Conv.fconv_rule (Class.unoverload thy));
+  |> map (Class.unoverload thy);
 
 fun preprocess_conv ct =
   let
@@ -916,7 +920,7 @@
     |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o the_exec) thy)
     |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
         ((#inline_procs o the_thmproc o the_exec) thy)
-    |> rhs_conv (Class.unoverload thy)
+    |> rhs_conv (Class.unoverload_conv thy)
   end;
 
 fun preprocess_term thy = term_of_conv thy preprocess_conv;
@@ -926,7 +930,7 @@
     val thy = Thm.theory_of_cterm ct;
   in
     ct
-    |> Class.overload thy
+    |> Class.overload_conv thy
     |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o the_exec) thy))
   end;
 
@@ -934,7 +938,7 @@
 
 end; (*local*)
 
-fun default_typ_proto thy c = case Class.param_const thy c
+fun default_typ_proto thy c = case Class.inst_of_param thy c
  of SOME (c, tyco) => classparam_weakest_typ thy ((the o AxClass.class_of_param thy) c)
       (c, tyco) |> SOME
   | NONE => (case AxClass.class_of_param thy c
@@ -965,7 +969,7 @@
 fun default_typ thy c = case default_typ_proto thy c
  of SOME ty => ty
   | NONE => (case get_funcs thy c
-     of thm :: _ => snd (CodeUnit.head_func (Conv.fconv_rule (Class.unoverload thy) thm))
+     of thm :: _ => snd (CodeUnit.head_func (Class.unoverload thy thm))
       | [] => Sign.the_const_type thy c);
 
 end; (*local*)

--- a/src/Pure/Isar/code_unit.ML	Wed Nov 28 09:01:40 2007 +0100
+++ b/src/Pure/Isar/code_unit.ML	Wed Nov 28 09:01:42 2007 +0100
@@ -59,7 +59,7 @@
 fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
 
 fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
-fun string_of_const thy c = case Class.param_const thy c
+fun string_of_const thy c = case Class.inst_of_param thy c
  of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
   | NONE => Sign.extern_const thy c;
 

--- a/src/Pure/Isar/instance.ML	Wed Nov 28 09:01:40 2007 +0100
+++ b/src/Pure/Isar/instance.ML	Wed Nov 28 09:01:42 2007 +0100
@@ -31,11 +31,11 @@
 fun instantiate arities f tac =
   TheoryTarget.instantiation arities
   #> f
-  #> Class.prove_instantiation tac
+  #> Class.prove_instantiation_instance tac
   #> LocalTheory.exit
   #> ProofContext.theory_of;
 
-fun gen_instance prep_arity prep_attr prep_term do_proof raw_arities defs after_qed thy =
+fun gen_instance prep_arity prep_attr parse_term do_proof raw_arities defs after_qed thy =
   let
     fun export_defs ctxt = 
       let
@@ -48,8 +48,12 @@
     fun mk_def ctxt ((name, raw_attr), raw_t) =
       let
         val attr = map (prep_attr thy) raw_attr;
-        val t = prep_term ctxt raw_t;
+        val t = parse_term ctxt raw_t;
       in (NONE, ((name, attr), t)) end;
+    fun define def ctxt =
+      let
+        val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
+      in Specification.definition def' ctxt end;
     val arities = map (prep_arity thy) raw_arities;
   in
     thy
@@ -64,12 +68,11 @@
   end;
 
 val instance = gen_instance Sign.cert_arity (K I) (K I)
-  (fn _ => fn after_qed => Class.proof_instantiation (after_qed #> Class.conclude_instantiation));
-val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src
-  (fn ctxt => Syntax.parse_prop ctxt #> Syntax.check_prop ctxt)
-  (fn _ => fn after_qed => Class.proof_instantiation (after_qed #> Class.conclude_instantiation));
+  (fn _ => fn after_qed => Class.instantiation_instance (after_qed #> Class.conclude_instantiation));
+val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src Syntax.parse_prop
+  (fn _ => fn after_qed => Class.instantiation_instance (after_qed #> Class.conclude_instantiation));
 fun prove_instance tac arities defs = gen_instance Sign.cert_arity (K I) (K I)
-  (fn defs => fn after_qed => Class.prove_instantiation (K tac)
+  (fn defs => fn after_qed => Class.prove_instantiation_instance (K tac)
     #> after_qed #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs) arities defs (K I);
 
 end;

--- a/src/Pure/Isar/isar_syn.ML	Wed Nov 28 09:01:40 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 28 09:01:42 2007 +0100
@@ -445,21 +445,20 @@
       Toplevel.print o Toplevel.local_theory_to_proof loc (Subclass.subclass_cmd class)));
 
 val _ =
-  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
-  ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
-    P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
-      >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)))
-    >> (Toplevel.print oo Toplevel.theory_to_proof));
-
-val _ =
   OuterSyntax.command "instantiation" "prove type arity" K.thy_decl
    (P.and_list1 P.arity --| P.begin
      >> (fn arities => Toplevel.print o
          Toplevel.begin_local_theory true (Instance.instantiation_cmd arities)));
 
-val _ =  (* FIXME incorporate into "instance" *)
-  OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal
-    (Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.proof_instantiation I)));
+val _ =
+  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
+  ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
+    P.$$$ "advanced" |-- P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
+      >> (fn (arities, defs) => Instance.instance_cmd arities defs (K I)) ||
+    P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
+      >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)))
+    >> (Toplevel.print oo Toplevel.theory_to_proof)
+  || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
 
 
 (* code generation *)

--- a/src/Pure/Isar/theory_target.ML	Wed Nov 28 09:01:40 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML	Wed Nov 28 09:01:42 2007 +0100
@@ -190,30 +190,29 @@
              Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   end;
 
-fun declare_const (ta as Target {target, is_locale, is_class, instantiation}) depends ((c, T), mx) lthy =
+fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((c, T), mx) lthy =
   let
     val pos = ContextPosition.properties_of lthy;
     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
     val U = map #2 xs ---> T;
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
-    val declare_const = if null instantiation
-      then Sign.declare_const pos (c, U, mx3)
-      else case Class.instantiation_const lthy c
-       of SOME c' => Class.declare_overloaded (c', U, mx3)
-        | NONE => Sign.declare_const pos (c, U, mx3);
-    val (const, lthy') = lthy |> LocalTheory.theory_result declare_const;
+    val declare_const = case Class.instantiation_param lthy c
+       of SOME c' => LocalTheory.theory_result (Class.overloaded_const (c', U, mx3))
+            ##> Class.confirm_declaration c
+        | NONE => LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3));
+    val (const, lthy') = lthy |> declare_const;
     val t = Term.list_comb (const, map Free xs);
   in
     lthy'
     |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default pos ((c, mx2), t))
-    |> is_class ? class_target ta (Class.add_logical_const target pos ((c, mx1), t))
+    |> is_class ? class_target ta (Class.logical_const target pos ((c, mx1), t))
     |> LocalDefs.add_def ((c, NoSyn), t)
   end;
 
 
 (* abbrev *)
 
-fun abbrev (ta as Target {target, is_locale, is_class, instantiation}) prmode ((c, mx), t) lthy =
+fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((c, mx), t) lthy =
   let
     val pos = ContextPosition.properties_of lthy;
     val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
@@ -232,7 +231,7 @@
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
             term_syntax ta (locale_const ta prmode pos ((c, mx2), lhs')) #>
-            is_class ? class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), t'))
+            is_class ? class_target ta (Class.syntactic_const target prmode pos ((c, mx1), t'))
           end)
       else
         LocalTheory.theory
@@ -245,7 +244,7 @@
 
 (* define *)
 
-fun define (ta as Target {target, is_locale, is_class, instantiation})
+fun define (ta as Target {target, is_locale, is_class, ...})
     kind ((c, mx), ((name, atts), rhs)) lthy =
   let
     val thy = ProofContext.theory_of lthy;
@@ -262,18 +261,15 @@
     val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
 
     (*def*)
-    val is_instantiation = not (null instantiation)
-      andalso is_some (Class.instantiation_const lthy c);
-    val define_const = if not is_instantiation
+    val define_const = if is_none (Class.instantiation_param lthy c)
       then (fn name => fn eq => Thm.add_def false (name, Logic.mk_equals eq))
-      else (fn name => fn (Const (c, _), rhs) => Class.define_overloaded name (c, rhs));
+      else (fn name => fn (Const (c, _), rhs) => Class.overloaded_def name (c, rhs));
     val (global_def, lthy3) = lthy2
       |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
-    val def = if not is_instantiation then LocalDefs.trans_terms lthy3
+    val def = LocalDefs.trans_terms lthy3
       [(*c == global.c xs*)     local_def,
        (*global.c xs == rhs'*)  global_def,
-       (*rhs' == rhs*)          Thm.symmetric rhs_conv]
-      else Thm.transitive local_def global_def;
+       (*rhs' == rhs*)          Thm.symmetric rhs_conv];
 
     (*note*)
     val ([(res_name, [res])], lthy4) = lthy3
@@ -294,7 +290,12 @@
     val global_consts = map (Term.dest_Const o Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
 
     (*axioms*)
-    val hyps = map Thm.term_of (Assumption.assms_of lthy');
+    val resubst_instparams = map_aterms (fn t as Free (v, T) =>
+      (case Class.instantiation_param lthy' v
+       of NONE => t
+        | SOME c => Const (c, T)) | t => t)
+    val hyps = map Thm.term_of (Assumption.assms_of lthy')
+      |> map resubst_instparams;
     fun axiom ((name, atts), props) thy = thy
       |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
       |-> (fn ths => pair ((name, atts), [(ths, [])]));
@@ -318,11 +319,10 @@
 fun init_instantiaton arities = make_target "" false false arities
 
 fun init_ctxt (Target {target, is_locale, is_class, instantiation}) =
-  if null instantiation then
-    if not is_locale then ProofContext.init
-    else if not is_class then Locale.init target
-    else Class.init target
-  else Class.instantiation instantiation;
+  if not (null instantiation) then Class.init_instantiation instantiation
+  else if not is_locale then ProofContext.init
+  else if not is_class then Locale.init target
+  else Class.init target;
 
 fun init_lthy (ta as Target {target, instantiation, ...}) =
   Data.put ta #>
@@ -336,7 +336,8 @@
     term_syntax = term_syntax ta,
     declaration = declaration ta,
     reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
-    exit = if null instantiation then LocalTheory.target_of else Class.end_instantiation}
+    exit = if null instantiation then LocalTheory.target_of
+      else Class.conclude_instantiation #> LocalTheory.target_of}
 and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
 
 in
@@ -347,8 +348,8 @@
 fun context "-" thy = init NONE thy
   | context target thy = init (SOME (Locale.intern thy target)) thy;
 
-fun instantiation raw_arities thy =
-  init_lthy_ctxt (init_instantiaton (map (Sign.cert_arity thy) raw_arities)) thy;
+fun instantiation arities thy =
+  init_lthy_ctxt (init_instantiaton arities) thy;
 
 end;
 

--- a/src/Tools/code/code_funcgr.ML	Wed Nov 28 09:01:40 2007 +0100
+++ b/src/Tools/code/code_funcgr.ML	Wed Nov 28 09:01:42 2007 +0100
@@ -157,7 +157,7 @@
     val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
     fun all_classparams tyco class =
       these (try (#params o AxClass.get_info thy) class)
-      |> map (fn (c, _) => Class.inst_const thy (c, tyco))
+      |> map (fn (c, _) => Class.param_of_inst thy (c, tyco))
   in
     Symtab.empty
     |> fold (fn (tyco, class) =>
@@ -211,7 +211,7 @@
       |> resort_funcss thy algebra funcgr
       |> filter_out (can (Graph.get_node funcgr) o fst);
     fun typ_func c [] = Code.default_typ thy c
-      | typ_func c (thms as thm :: _) = case Class.param_const thy c
+      | typ_func c (thms as thm :: _) = case Class.inst_of_param thy c
          of SOME (c', tyco) => 
               let
                 val (_, ty) = CodeUnit.head_func thm;

--- a/src/Tools/code/code_name.ML	Wed Nov 28 09:01:40 2007 +0100
+++ b/src/Tools/code/code_name.ML	Wed Nov 28 09:01:42 2007 +0100
@@ -216,7 +216,7 @@
  of SOME dtco => SOME (thyname_of_tyco thy dtco)
   | NONE => (case AxClass.class_of_param thy c
      of SOME class => SOME (thyname_of_class thy class)
-      | NONE => (case Class.param_const thy c
+      | NONE => (case Class.inst_of_param thy c
          of SOME (c, tyco) => SOME (thyname_of_instance thy
               ((the o AxClass.class_of_param thy) c, tyco))
           | NONE => NONE));

--- a/src/Tools/code/code_package.ML	Wed Nov 28 09:01:40 2007 +0100
+++ b/src/Tools/code/code_package.ML	Wed Nov 28 09:01:42 2007 +0100
@@ -33,7 +33,7 @@
       in
         gr
         |> Graph.subgraph (member (op =) select) 
-        |> Graph.map_nodes ((apsnd o map) (Conv.fconv_rule (Class.overload thy)))
+        |> Graph.map_nodes ((apsnd o map) (Class.overload thy))
       end;
 
 fun code_thms thy =

--- a/src/Tools/code/code_thingol.ML	Wed Nov 28 09:01:40 2007 +0100
+++ b/src/Tools/code/code_thingol.ML	Wed Nov 28 09:01:42 2007 +0100
@@ -461,7 +461,7 @@
     fun exprgen_classparam_inst (c, ty) =
       let
         val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
-        val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
+        val thm = Class.unoverload_conv thy (Thm.cterm_of thy c_inst);
         val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
           o Logic.dest_equals o Thm.prop_of) thm;
       in