tuned interfaces of class module
authorhaftmann
Wed Nov 28 09:01:42 2007 +0100 (2007-11-28)
changeset 2548533840a854e63
parent 25484 4c98517601ce
child 25486 b944ef973109
tuned interfaces of class module
src/HOL/Tools/datatype_codegen.ML
src/Pure/Isar/class.ML
src/Pure/Isar/code.ML
src/Pure/Isar/code_unit.ML
src/Pure/Isar/instance.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/theory_target.ML
src/Tools/code/code_funcgr.ML
src/Tools/code/code_name.ML
src/Tools/code/code_package.ML
src/Tools/code/code_thingol.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Nov 28 09:01:40 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Nov 28 09:01:42 2007 +0100
     1.3 @@ -432,7 +432,7 @@
     1.4      |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
     1.5      |> Thm.implies_intr asm
     1.6      |> Thm.generalize ([], params) 0
     1.7 -    |> Conv.fconv_rule (Class.unoverload thy)
     1.8 +    |> Class.unoverload thy
     1.9      |> Thm.varifyT
    1.10    end;
    1.11  
    1.12 @@ -572,7 +572,7 @@
    1.13      fun add_eq_thms (dtco, (_, (vs, cs))) thy =
    1.14        let
    1.15          val thy_ref = Theory.check_thy thy;
    1.16 -        val const = Class.inst_const thy ("op =", dtco);
    1.17 +        val const = Class.param_of_inst thy ("op =", dtco);
    1.18          val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
    1.19        in
    1.20          Code.add_funcl (const, Susp.delay get_thms) thy
     2.1 --- a/src/Pure/Isar/class.ML	Wed Nov 28 09:01:40 2007 +0100
     2.2 +++ b/src/Pure/Isar/class.ML	Wed Nov 28 09:01:42 2007 +0100
     2.3 @@ -12,35 +12,42 @@
     2.4      -> string list -> theory -> string * Proof.context
     2.5    val class_cmd: bstring -> xstring list -> Element.context Locale.element list
     2.6      -> xstring list -> theory -> string * Proof.context
     2.7 -  val is_class: theory -> class -> bool
     2.8 -  val these_params: theory -> sort -> (string * (string * typ)) list
     2.9 +
    2.10    val init: class -> theory -> Proof.context
    2.11 -  val add_logical_const: string -> Markup.property list
    2.12 +  val logical_const: string -> Markup.property list
    2.13      -> (string * mixfix) * term -> theory -> theory
    2.14 -  val add_syntactic_const: string -> Syntax.mode -> Markup.property list
    2.15 +  val syntactic_const: string -> Syntax.mode -> Markup.property list
    2.16      -> (string * mixfix) * term -> theory -> theory
    2.17    val refresh_syntax: class -> Proof.context -> Proof.context
    2.18 +
    2.19    val intro_classes_tac: thm list -> tactic
    2.20    val default_intro_classes_tac: thm list -> tactic
    2.21    val prove_subclass: class * class -> thm list -> Proof.context
    2.22      -> theory -> theory
    2.23 +
    2.24 +  val class_prefix: string -> string
    2.25 +  val is_class: theory -> class -> bool
    2.26 +  val these_params: theory -> sort -> (string * (string * typ)) list
    2.27    val print_classes: theory -> unit
    2.28 -  val class_prefix: string -> string
    2.29  
    2.30    (*instances*)
    2.31 -  val declare_overloaded: string * typ * mixfix -> theory -> term * theory
    2.32 -  val define_overloaded: string -> string * term -> theory -> thm * theory
    2.33 -  val unoverload: theory -> conv
    2.34 -  val overload: theory -> conv
    2.35 +  val init_instantiation: arity list -> theory -> local_theory
    2.36 +  val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
    2.37 +  val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
    2.38 +  val conclude_instantiation: local_theory -> local_theory
    2.39 +
    2.40 +  val overloaded_const: string * typ * mixfix -> theory -> term * theory
    2.41 +  val overloaded_def: string -> string * term -> theory -> thm * theory
    2.42 +  val instantiation_param: Proof.context -> string -> string option
    2.43 +  val confirm_declaration: string -> local_theory -> local_theory
    2.44 +
    2.45 +  val unoverload: theory -> thm -> thm
    2.46 +  val overload: theory -> thm -> thm
    2.47 +  val unoverload_conv: theory -> conv
    2.48 +  val overload_conv: theory -> conv
    2.49    val unoverload_const: theory -> string * typ -> string
    2.50 -  val inst_const: theory -> string * string -> string
    2.51 -  val param_const: theory -> string -> (string * string) option
    2.52 -  val instantiation: arity list -> theory -> local_theory
    2.53 -  val proof_instantiation: (local_theory -> local_theory) -> local_theory -> Proof.state
    2.54 -  val prove_instantiation: (Proof.context -> tactic) -> local_theory -> local_theory
    2.55 -  val conclude_instantiation: local_theory -> local_theory
    2.56 -  val end_instantiation: local_theory -> Proof.context
    2.57 -  val instantiation_const: Proof.context -> string -> string option
    2.58 +  val param_of_inst: theory -> string * string -> string
    2.59 +  val inst_of_param: theory -> string -> (string * string) option
    2.60  
    2.61    (*old axclass layer*)
    2.62    val axclass_cmd: bstring * xstring list
    2.63 @@ -109,7 +116,7 @@
    2.64    end;
    2.65  
    2.66  
    2.67 -(** axclass command **)
    2.68 +(** primitive axclass and instance commands **)
    2.69  
    2.70  fun axclass_cmd (class, raw_superclasses) raw_specs thy =
    2.71    let
    2.72 @@ -175,26 +182,27 @@
    2.73  fun inst thy (c, tyco) =
    2.74    (the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
    2.75  
    2.76 -val inst_const = fst oo inst;
    2.77 +val param_of_inst = fst oo inst;
    2.78  
    2.79  fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
    2.80    (InstData.get thy) [];
    2.81  
    2.82 -val param_const = Symtab.lookup o snd o InstData.get;
    2.83 +val inst_of_param = Symtab.lookup o snd o InstData.get;
    2.84  
    2.85  fun add_inst (c, tyco) inst = (InstData.map o apfst
    2.86        o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
    2.87    #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
    2.88  
    2.89 -fun unoverload thy = MetaSimplifier.rewrite true (inst_thms thy);
    2.90 -fun overload thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
    2.91 +fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
    2.92 +fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
    2.93 +
    2.94 +fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
    2.95 +fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
    2.96  
    2.97  fun unoverload_const thy (c_ty as (c, _)) =
    2.98    case AxClass.class_of_param thy c
    2.99     of SOME class => (case inst_tyco thy c_ty
   2.100 -       of SOME tyco => (case try (inst thy) (c, tyco)
   2.101 -             of SOME (c, _) => c
   2.102 -              | NONE => c)
   2.103 +       of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
   2.104          | NONE => c)
   2.105      | NONE => c;
   2.106  
   2.107 @@ -205,18 +213,20 @@
   2.108    PureThy.note_thmss_i kind [((name, []), [([thm], [])])]
   2.109    #>> (fn [(_, [thm])] => thm);
   2.110  
   2.111 -fun declare_overloaded (c, ty, mx) thy =
   2.112 +fun overloaded_const (c, ty, mx) thy =
   2.113    let
   2.114 +    val _ = if mx <> NoSyn then
   2.115 +      error ("Illegal mixfix syntax for constant to be instantiated " ^ quote c)
   2.116 +      else ()
   2.117      val SOME class = AxClass.class_of_param thy c;
   2.118      val SOME tyco = inst_tyco thy (c, ty);
   2.119 -    val name_inst = NameSpace.base class ^ "_" ^ NameSpace.base tyco ^ "_inst";
   2.120 +    val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
   2.121      val c' = NameSpace.base c;
   2.122      val ty' = Type.strip_sorts ty;
   2.123    in
   2.124      thy
   2.125      |> Sign.sticky_prefix name_inst
   2.126      |> Sign.no_base_names
   2.127 -    |> Sign.notation true Syntax.mode_default [(Const (c, ty), mx)]
   2.128      |> Sign.declare_const [] (c', ty', NoSyn)
   2.129      |-> (fn const' as Const (c'', _) => Thm.add_def true
   2.130            (Thm.def_name c', Logic.mk_equals (Const (c, ty'), const'))
   2.131 @@ -228,22 +238,18 @@
   2.132      #> pair (Const (c, ty))))
   2.133    end;
   2.134  
   2.135 -fun define_overloaded name (c, t) thy =
   2.136 +fun overloaded_def name (c, t) thy =
   2.137    let
   2.138      val ty = Term.fastype_of t;
   2.139      val SOME tyco = inst_tyco thy (c, ty);
   2.140      val (c', eq) = inst thy (c, tyco);
   2.141 -    val [Type (_, tys)] = Sign.const_typargs thy (c, ty);
   2.142 -    val eq' = eq
   2.143 -      |> Drule.instantiate' (map (SOME o Thm.ctyp_of thy) tys) [];
   2.144 -          (*FIXME proper recover_sort mechanism*)
   2.145      val prop = Logic.mk_equals (Const (c', ty), t);
   2.146 -    val name' = if name = "" then
   2.147 -      Thm.def_name (NameSpace.base c ^ "_" ^ NameSpace.base tyco) else name;
   2.148 +    val name' = Thm.def_name_optional
   2.149 +      (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
   2.150    in
   2.151      thy
   2.152      |> Thm.add_def false (name', prop)
   2.153 -    |>> (fn thm => Thm.transitive eq' thm)
   2.154 +    |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
   2.155    end;
   2.156  
   2.157  
   2.158 @@ -911,9 +917,9 @@
   2.159  end; (*local*)
   2.160  
   2.161  
   2.162 -(* definition in class target *)
   2.163 +(* class target *)
   2.164  
   2.165 -fun add_logical_const class pos ((c, mx), dict) thy =
   2.166 +fun logical_const class pos ((c, mx), dict) thy =
   2.167    let
   2.168      val prfx = class_prefix class;
   2.169      val thy' = thy |> Sign.add_path prfx;
   2.170 @@ -928,7 +934,7 @@
   2.171    in
   2.172      thy'
   2.173      |> Sign.declare_const pos (c, ty'', mx) |> snd
   2.174 -    |> Thm.add_def false (c, def_eq)    (* FIXME PureThy.add_defs_i *)
   2.175 +    |> Thm.add_def false (c, def_eq)
   2.176      |>> Thm.symmetric
   2.177      |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
   2.178            #> register_operation class (c', (dict', SOME (Thm.varifyT def))))
   2.179 @@ -936,10 +942,7 @@
   2.180      |> Sign.add_const_constraint (c', SOME ty')
   2.181    end;
   2.182  
   2.183 -
   2.184 -(* abbreviation in class target *)
   2.185 -
   2.186 -fun add_syntactic_const class prmode pos ((c, mx), rhs) thy =
   2.187 +fun syntactic_const class prmode pos ((c, mx), rhs) thy =
   2.188    let
   2.189      val prfx = class_prefix class;
   2.190      val thy' = thy |> Sign.add_path prfx;
   2.191 @@ -974,51 +977,26 @@
   2.192    fun init _ = Instantiation { arities = [], params = [] };
   2.193  );
   2.194  
   2.195 -fun mk_instantiation (arities, params) = Instantiation {
   2.196 -    arities = arities, params = params
   2.197 -  };
   2.198 +fun mk_instantiation (arities, params) =
   2.199 +  Instantiation { arities = arities, params = params };
   2.200 +fun get_instantiation ctxt = case Instantiation.get ctxt
   2.201 + of Instantiation data => data;
   2.202  fun map_instantiation f (Instantiation { arities, params }) =
   2.203    mk_instantiation (f (arities, params));
   2.204  
   2.205 -fun the_instantiation ctxt = case Instantiation.get ctxt
   2.206 - of Instantiation { arities = [], ... } => error "No instantiation target"
   2.207 -  | Instantiation data => data;
   2.208 +fun the_instantiation ctxt = case get_instantiation ctxt
   2.209 + of { arities = [], ... } => error "No instantiation target"
   2.210 +  | data => data;
   2.211  
   2.212 -fun init_instantiation arities ctxt =
   2.213 -  let
   2.214 -    val thy = ProofContext.theory_of ctxt;
   2.215 -    val _ = if null arities then error "At least one arity must be given" else ();
   2.216 -    val _ = case (duplicates (op =) o map #1) arities
   2.217 -     of [] => ()
   2.218 -      | dupl_tycos => error ("Type constructors occur more than once in arities: "
   2.219 -          ^ commas_quote dupl_tycos);
   2.220 -    val ty_insts = map (fn (tyco, sorts, _) =>
   2.221 -        (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
   2.222 -      arities;
   2.223 -    val ty_inst = the o AList.lookup (op =) ty_insts;
   2.224 -    fun type_name "*" = "prod"
   2.225 -      | type_name "+" = "sum"
   2.226 -      | type_name s = NameSpace.base s; (*FIXME*)
   2.227 -    fun get_param tyco sorts (param, (c, ty)) =
   2.228 -      ((unoverload_const thy (c, ty), tyco),
   2.229 -        (param ^ "_" ^ type_name tyco,
   2.230 -          map_atyps (K (ty_inst tyco)) ty));
   2.231 -    fun get_params (tyco, sorts, sort) =
   2.232 -      map (get_param tyco sorts) (these_params thy sort)
   2.233 -    val params = maps get_params arities;
   2.234 -  in
   2.235 -    ctxt
   2.236 -    |> Instantiation.put (mk_instantiation (arities, params))
   2.237 -    |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts
   2.238 -    |> fold (Variable.declare_term o Free o snd) params
   2.239 -  end;
   2.240 +val instantiation_params = #params o get_instantiation;
   2.241  
   2.242 -val instantiation_params = #params o the_instantiation;
   2.243 -
   2.244 -fun instantiation_const ctxt v = instantiation_params ctxt
   2.245 +fun instantiation_param ctxt v = instantiation_params ctxt
   2.246    |> find_first (fn (_, (v', _)) => v = v')
   2.247    |> Option.map (fst o fst);
   2.248  
   2.249 +fun confirm_declaration c = (Instantiation.map o map_instantiation o apsnd)
   2.250 +  (filter_out (fn (_, (c', _)) => c' = c));
   2.251 +
   2.252  
   2.253  (* syntax *)
   2.254  
   2.255 @@ -1057,21 +1035,58 @@
   2.256  
   2.257  (* target *)
   2.258  
   2.259 -fun instantiation arities =
   2.260 -  ProofContext.init
   2.261 -  #> init_instantiation arities
   2.262 -  #> fold ProofContext.add_arity arities
   2.263 -  #> Context.proof_map (
   2.264 -      Syntax.add_term_check 0 "instance" inst_term_check
   2.265 -      #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck);
   2.266 +val sanatize_name = (*FIXME*)
   2.267 +  let
   2.268 +    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
   2.269 +    val is_junk = not o is_valid andf Symbol.is_regular;
   2.270 +    val junk = Scan.many is_junk;
   2.271 +    val scan_valids = Symbol.scanner "Malformed input"
   2.272 +      ((junk |--
   2.273 +        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
   2.274 +        --| junk))
   2.275 +      -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
   2.276 +  in
   2.277 +    explode #> scan_valids #> implode
   2.278 +  end;
   2.279 +
   2.280  
   2.281 -fun gen_proof_instantiation do_proof after_qed lthy =
   2.282 +fun init_instantiation arities thy =
   2.283    let
   2.284 -    (*FIXME should work on fresh context but continue local theory afterwards*)
   2.285 +    val _ = if null arities then error "At least one arity must be given" else ();
   2.286 +    val _ = case (duplicates (op =) o map #1) arities
   2.287 +     of [] => ()
   2.288 +      | dupl_tycos => error ("Type constructors occur more than once in arities: "
   2.289 +          ^ commas_quote dupl_tycos);
   2.290 +    val ty_insts = map (fn (tyco, sorts, _) =>
   2.291 +        (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
   2.292 +      arities;
   2.293 +    val ty_inst = the o AList.lookup (op =) ty_insts;
   2.294 +    fun type_name "*" = "prod"
   2.295 +      | type_name "+" = "sum"
   2.296 +      | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
   2.297 +    fun get_param tyco sorts (param, (c, ty)) =
   2.298 +      ((unoverload_const thy (c, ty), tyco),
   2.299 +        (param ^ "_" ^ type_name tyco,
   2.300 +          map_atyps (K (ty_inst tyco)) ty));
   2.301 +    fun get_params (tyco, sorts, sort) =
   2.302 +      map (get_param tyco sorts) (these_params thy sort)
   2.303 +    val params = maps get_params arities;
   2.304 +  in
   2.305 +    thy
   2.306 +    |> ProofContext.init
   2.307 +    |> Instantiation.put (mk_instantiation (arities, params))
   2.308 +    |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts
   2.309 +    |> fold ProofContext.add_arity arities
   2.310 +    |> Context.proof_map (
   2.311 +        Syntax.add_term_check 0 "instance" inst_term_check
   2.312 +        #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck)
   2.313 +  end;
   2.314 +
   2.315 +fun gen_instantiation_instance do_proof after_qed lthy =
   2.316 +  let
   2.317      val ctxt = LocalTheory.target_of lthy;
   2.318      val arities = (#arities o the_instantiation) ctxt;
   2.319 -    val arities_proof = maps
   2.320 -      (Logic.mk_arities o Sign.cert_arity (ProofContext.theory_of ctxt)) arities;
   2.321 +    val arities_proof = maps Logic.mk_arities arities;
   2.322      fun after_qed' results =
   2.323        LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
   2.324        #> after_qed;
   2.325 @@ -1080,16 +1095,16 @@
   2.326      |> do_proof after_qed' arities_proof
   2.327    end;
   2.328  
   2.329 -val proof_instantiation = gen_proof_instantiation (fn after_qed => fn ts =>
   2.330 +val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
   2.331    Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
   2.332  
   2.333 -fun prove_instantiation tac = gen_proof_instantiation (fn after_qed =>
   2.334 +fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
   2.335    fn ts => fn lthy => after_qed (Goal.prove_multi lthy [] [] ts
   2.336      (fn {context, ...} => tac context)) lthy) I;
   2.337  
   2.338  fun conclude_instantiation lthy =
   2.339    let
   2.340 -    val arities = (#arities o the_instantiation) lthy;
   2.341 +    val { arities, params } = the_instantiation lthy;
   2.342      val thy = ProofContext.theory_of lthy;
   2.343      (*val _ = map (fn (tyco, sorts, sort) =>
   2.344        if Sign.of_sort thy
   2.345 @@ -1101,20 +1116,21 @@
   2.346      val missing_params = arities
   2.347        |> maps (fn (tyco, _, sort) => params_of sort |> map (rpair tyco))
   2.348        |> filter_out (can (inst thy) o apfst fst);
   2.349 -    fun declare_missing ((c, ty), tyco) thy =
   2.350 +    fun declare_missing ((c, ty0), tyco) thy =
   2.351 +    (*fun declare_missing ((c, tyco), (_, ty)) thy =*)
   2.352        let
   2.353          val SOME class = AxClass.class_of_param thy c;
   2.354 -        val name_inst = NameSpace.base class ^ "_" ^ NameSpace.base tyco ^ "_inst";
   2.355 +        val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
   2.356 +        val c' = NameSpace.base c;
   2.357          val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []);
   2.358 -        val ty' = map_atyps (fn _ => Type (tyco, map TFree vs)) ty;
   2.359 -        val c' = NameSpace.base c;
   2.360 +        val ty = map_atyps (fn _ => Type (tyco, map TFree vs)) ty0;
   2.361        in
   2.362          thy
   2.363          |> Sign.sticky_prefix name_inst
   2.364          |> Sign.no_base_names
   2.365 -        |> Sign.declare_const [] (c', ty', NoSyn)
   2.366 +        |> Sign.declare_const [] (c', ty, NoSyn)
   2.367          |-> (fn const' as Const (c'', _) => Thm.add_def true
   2.368 -              (Thm.def_name c', Logic.mk_equals (const', Const (c, ty')))
   2.369 +              (Thm.def_name c', Logic.mk_equals (const', Const (c, ty)))
   2.370          #>> Thm.varifyT
   2.371          #-> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm)
   2.372          #> primitive_note Thm.internalK (c', thm)
   2.373 @@ -1126,6 +1142,4 @@
   2.374      |> LocalTheory.theory (fold declare_missing missing_params)
   2.375    end;
   2.376  
   2.377 -val end_instantiation = conclude_instantiation #> LocalTheory.target_of;
   2.378 -
   2.379  end;
     3.1 --- a/src/Pure/Isar/code.ML	Wed Nov 28 09:01:40 2007 +0100
     3.2 +++ b/src/Pure/Isar/code.ML	Wed Nov 28 09:01:42 2007 +0100
     3.3 @@ -3,7 +3,7 @@
     3.4      Author:     Florian Haftmann, TU Muenchen
     3.5  
     3.6  Abstract executable content of theory.  Management of data dependent on
     3.7 -executable content.  Cache assumes non-concurrent processing of a singly theory.
     3.8 +executable content.  Cache assumes non-concurrent processing of a single theory.
     3.9  *)
    3.10  
    3.11  signature CODE =
    3.12 @@ -24,7 +24,9 @@
    3.13    val del_post: thm -> theory -> theory
    3.14    val add_datatype: (string * typ) list -> theory -> theory
    3.15    val add_datatype_cmd: string list -> theory -> theory
    3.16 -  val type_interpretation: (string * string list -> theory -> theory) -> theory -> theory
    3.17 +  val type_interpretation:
    3.18 +    (string * ((string * sort) list * (string * typ list) list)
    3.19 +      -> theory -> theory) -> theory -> theory
    3.20    val add_case: thm -> theory -> theory
    3.21    val add_undefined: string -> theory -> theory
    3.22  
    3.23 @@ -546,7 +548,7 @@
    3.24      val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
    3.25      val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class;
    3.26      val funcs = classparams
    3.27 -      |> map_filter (fn c => try (Class.inst_const thy) (c, tyco))
    3.28 +      |> map_filter (fn c => try (Class.param_of_inst thy) (c, tyco))
    3.29        |> map (Symtab.lookup ((the_funcs o the_exec) thy))
    3.30        |> (map o Option.map) (Susp.force o fst o snd)
    3.31        |> maps these
    3.32 @@ -664,7 +666,7 @@
    3.33             ^ CodeUnit.string_of_typ thy ty_decl)
    3.34        end;
    3.35      fun check_typ (c, thm) =
    3.36 -      case Class.param_const thy c
    3.37 +      case Class.inst_of_param thy c
    3.38         of SOME (c, tyco) => check_typ_classparam tyco (c, thm)
    3.39          | NONE => check_typ_fun (c, thm);
    3.40    in check_typ (const_of_func thy thm, thm) end;
    3.41 @@ -777,8 +779,7 @@
    3.42  val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute
    3.43    (fn thm => Context.mapping (add_default_func thm) I));
    3.44  
    3.45 -structure TypeInterpretation = InterpretationFun(type T = string * string list val eq = op =);
    3.46 -val type_interpretation = TypeInterpretation.interpretation;
    3.47 +structure TypeInterpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
    3.48  
    3.49  fun add_datatype raw_cs thy =
    3.50    let
    3.51 @@ -792,9 +793,12 @@
    3.52      thy
    3.53      |> map_exec_purge purge_cs (map_dtyps (Symtab.update (tyco, vs_cos))
    3.54          #> map_funcs (fold (Symtab.delete_safe o fst) cs))
    3.55 -    |> TypeInterpretation.data (tyco, cs')
    3.56 +    |> TypeInterpretation.data (tyco, serial ())
    3.57    end;
    3.58  
    3.59 +fun type_interpretation f =  TypeInterpretation.interpretation
    3.60 +  (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
    3.61 +
    3.62  fun add_datatype_cmd raw_cs thy =
    3.63    let
    3.64      val cs = map (CodeUnit.read_bare_const thy) raw_cs;
    3.65 @@ -906,7 +910,7 @@
    3.66    |> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_thmproc o the_exec) thy)
    3.67  (*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
    3.68    |> common_typ_funcs
    3.69 -  |> map (Conv.fconv_rule (Class.unoverload thy));
    3.70 +  |> map (Class.unoverload thy);
    3.71  
    3.72  fun preprocess_conv ct =
    3.73    let
    3.74 @@ -916,7 +920,7 @@
    3.75      |> MetaSimplifier.rewrite false ((#inlines o the_thmproc o the_exec) thy)
    3.76      |> fold (fn (_, (_, f)) => rhs_conv (apply_inline_proc_cterm thy f))
    3.77          ((#inline_procs o the_thmproc o the_exec) thy)
    3.78 -    |> rhs_conv (Class.unoverload thy)
    3.79 +    |> rhs_conv (Class.unoverload_conv thy)
    3.80    end;
    3.81  
    3.82  fun preprocess_term thy = term_of_conv thy preprocess_conv;
    3.83 @@ -926,7 +930,7 @@
    3.84      val thy = Thm.theory_of_cterm ct;
    3.85    in
    3.86      ct
    3.87 -    |> Class.overload thy
    3.88 +    |> Class.overload_conv thy
    3.89      |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o the_exec) thy))
    3.90    end;
    3.91  
    3.92 @@ -934,7 +938,7 @@
    3.93  
    3.94  end; (*local*)
    3.95  
    3.96 -fun default_typ_proto thy c = case Class.param_const thy c
    3.97 +fun default_typ_proto thy c = case Class.inst_of_param thy c
    3.98   of SOME (c, tyco) => classparam_weakest_typ thy ((the o AxClass.class_of_param thy) c)
    3.99        (c, tyco) |> SOME
   3.100    | NONE => (case AxClass.class_of_param thy c
   3.101 @@ -965,7 +969,7 @@
   3.102  fun default_typ thy c = case default_typ_proto thy c
   3.103   of SOME ty => ty
   3.104    | NONE => (case get_funcs thy c
   3.105 -     of thm :: _ => snd (CodeUnit.head_func (Conv.fconv_rule (Class.unoverload thy) thm))
   3.106 +     of thm :: _ => snd (CodeUnit.head_func (Class.unoverload thy thm))
   3.107        | [] => Sign.the_const_type thy c);
   3.108  
   3.109  end; (*local*)
     4.1 --- a/src/Pure/Isar/code_unit.ML	Wed Nov 28 09:01:40 2007 +0100
     4.2 +++ b/src/Pure/Isar/code_unit.ML	Wed Nov 28 09:01:42 2007 +0100
     4.3 @@ -59,7 +59,7 @@
     4.4  fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
     4.5  
     4.6  fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
     4.7 -fun string_of_const thy c = case Class.param_const thy c
     4.8 +fun string_of_const thy c = case Class.inst_of_param thy c
     4.9   of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
    4.10    | NONE => Sign.extern_const thy c;
    4.11  
     5.1 --- a/src/Pure/Isar/instance.ML	Wed Nov 28 09:01:40 2007 +0100
     5.2 +++ b/src/Pure/Isar/instance.ML	Wed Nov 28 09:01:42 2007 +0100
     5.3 @@ -31,11 +31,11 @@
     5.4  fun instantiate arities f tac =
     5.5    TheoryTarget.instantiation arities
     5.6    #> f
     5.7 -  #> Class.prove_instantiation tac
     5.8 +  #> Class.prove_instantiation_instance tac
     5.9    #> LocalTheory.exit
    5.10    #> ProofContext.theory_of;
    5.11  
    5.12 -fun gen_instance prep_arity prep_attr prep_term do_proof raw_arities defs after_qed thy =
    5.13 +fun gen_instance prep_arity prep_attr parse_term do_proof raw_arities defs after_qed thy =
    5.14    let
    5.15      fun export_defs ctxt = 
    5.16        let
    5.17 @@ -48,8 +48,12 @@
    5.18      fun mk_def ctxt ((name, raw_attr), raw_t) =
    5.19        let
    5.20          val attr = map (prep_attr thy) raw_attr;
    5.21 -        val t = prep_term ctxt raw_t;
    5.22 +        val t = parse_term ctxt raw_t;
    5.23        in (NONE, ((name, attr), t)) end;
    5.24 +    fun define def ctxt =
    5.25 +      let
    5.26 +        val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
    5.27 +      in Specification.definition def' ctxt end;
    5.28      val arities = map (prep_arity thy) raw_arities;
    5.29    in
    5.30      thy
    5.31 @@ -64,12 +68,11 @@
    5.32    end;
    5.33  
    5.34  val instance = gen_instance Sign.cert_arity (K I) (K I)
    5.35 -  (fn _ => fn after_qed => Class.proof_instantiation (after_qed #> Class.conclude_instantiation));
    5.36 -val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src
    5.37 -  (fn ctxt => Syntax.parse_prop ctxt #> Syntax.check_prop ctxt)
    5.38 -  (fn _ => fn after_qed => Class.proof_instantiation (after_qed #> Class.conclude_instantiation));
    5.39 +  (fn _ => fn after_qed => Class.instantiation_instance (after_qed #> Class.conclude_instantiation));
    5.40 +val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src Syntax.parse_prop
    5.41 +  (fn _ => fn after_qed => Class.instantiation_instance (after_qed #> Class.conclude_instantiation));
    5.42  fun prove_instance tac arities defs = gen_instance Sign.cert_arity (K I) (K I)
    5.43 -  (fn defs => fn after_qed => Class.prove_instantiation (K tac)
    5.44 +  (fn defs => fn after_qed => Class.prove_instantiation_instance (K tac)
    5.45      #> after_qed #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs) arities defs (K I);
    5.46  
    5.47  end;
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Nov 28 09:01:40 2007 +0100
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 28 09:01:42 2007 +0100
     6.3 @@ -445,21 +445,20 @@
     6.4        Toplevel.print o Toplevel.local_theory_to_proof loc (Subclass.subclass_cmd class)));
     6.5  
     6.6  val _ =
     6.7 -  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
     6.8 -  ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
     6.9 -    P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    6.10 -      >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)))
    6.11 -    >> (Toplevel.print oo Toplevel.theory_to_proof));
    6.12 -
    6.13 -val _ =
    6.14    OuterSyntax.command "instantiation" "prove type arity" K.thy_decl
    6.15     (P.and_list1 P.arity --| P.begin
    6.16       >> (fn arities => Toplevel.print o
    6.17           Toplevel.begin_local_theory true (Instance.instantiation_cmd arities)));
    6.18  
    6.19 -val _ =  (* FIXME incorporate into "instance" *)
    6.20 -  OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal
    6.21 -    (Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.proof_instantiation I)));
    6.22 +val _ =
    6.23 +  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    6.24 +  ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
    6.25 +    P.$$$ "advanced" |-- P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    6.26 +      >> (fn (arities, defs) => Instance.instance_cmd arities defs (K I)) ||
    6.27 +    P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    6.28 +      >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)))
    6.29 +    >> (Toplevel.print oo Toplevel.theory_to_proof)
    6.30 +  || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
    6.31  
    6.32  
    6.33  (* code generation *)
     7.1 --- a/src/Pure/Isar/theory_target.ML	Wed Nov 28 09:01:40 2007 +0100
     7.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Nov 28 09:01:42 2007 +0100
     7.3 @@ -190,30 +190,29 @@
     7.4               Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
     7.5    end;
     7.6  
     7.7 -fun declare_const (ta as Target {target, is_locale, is_class, instantiation}) depends ((c, T), mx) lthy =
     7.8 +fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((c, T), mx) lthy =
     7.9    let
    7.10      val pos = ContextPosition.properties_of lthy;
    7.11      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    7.12      val U = map #2 xs ---> T;
    7.13      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    7.14 -    val declare_const = if null instantiation
    7.15 -      then Sign.declare_const pos (c, U, mx3)
    7.16 -      else case Class.instantiation_const lthy c
    7.17 -       of SOME c' => Class.declare_overloaded (c', U, mx3)
    7.18 -        | NONE => Sign.declare_const pos (c, U, mx3);
    7.19 -    val (const, lthy') = lthy |> LocalTheory.theory_result declare_const;
    7.20 +    val declare_const = case Class.instantiation_param lthy c
    7.21 +       of SOME c' => LocalTheory.theory_result (Class.overloaded_const (c', U, mx3))
    7.22 +            ##> Class.confirm_declaration c
    7.23 +        | NONE => LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3));
    7.24 +    val (const, lthy') = lthy |> declare_const;
    7.25      val t = Term.list_comb (const, map Free xs);
    7.26    in
    7.27      lthy'
    7.28      |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default pos ((c, mx2), t))
    7.29 -    |> is_class ? class_target ta (Class.add_logical_const target pos ((c, mx1), t))
    7.30 +    |> is_class ? class_target ta (Class.logical_const target pos ((c, mx1), t))
    7.31      |> LocalDefs.add_def ((c, NoSyn), t)
    7.32    end;
    7.33  
    7.34  
    7.35  (* abbrev *)
    7.36  
    7.37 -fun abbrev (ta as Target {target, is_locale, is_class, instantiation}) prmode ((c, mx), t) lthy =
    7.38 +fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((c, mx), t) lthy =
    7.39    let
    7.40      val pos = ContextPosition.properties_of lthy;
    7.41      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    7.42 @@ -232,7 +231,7 @@
    7.43          #-> (fn (lhs, _) =>
    7.44            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    7.45              term_syntax ta (locale_const ta prmode pos ((c, mx2), lhs')) #>
    7.46 -            is_class ? class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), t'))
    7.47 +            is_class ? class_target ta (Class.syntactic_const target prmode pos ((c, mx1), t'))
    7.48            end)
    7.49        else
    7.50          LocalTheory.theory
    7.51 @@ -245,7 +244,7 @@
    7.52  
    7.53  (* define *)
    7.54  
    7.55 -fun define (ta as Target {target, is_locale, is_class, instantiation})
    7.56 +fun define (ta as Target {target, is_locale, is_class, ...})
    7.57      kind ((c, mx), ((name, atts), rhs)) lthy =
    7.58    let
    7.59      val thy = ProofContext.theory_of lthy;
    7.60 @@ -262,18 +261,15 @@
    7.61      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
    7.62  
    7.63      (*def*)
    7.64 -    val is_instantiation = not (null instantiation)
    7.65 -      andalso is_some (Class.instantiation_const lthy c);
    7.66 -    val define_const = if not is_instantiation
    7.67 +    val define_const = if is_none (Class.instantiation_param lthy c)
    7.68        then (fn name => fn eq => Thm.add_def false (name, Logic.mk_equals eq))
    7.69 -      else (fn name => fn (Const (c, _), rhs) => Class.define_overloaded name (c, rhs));
    7.70 +      else (fn name => fn (Const (c, _), rhs) => Class.overloaded_def name (c, rhs));
    7.71      val (global_def, lthy3) = lthy2
    7.72        |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
    7.73 -    val def = if not is_instantiation then LocalDefs.trans_terms lthy3
    7.74 +    val def = LocalDefs.trans_terms lthy3
    7.75        [(*c == global.c xs*)     local_def,
    7.76         (*global.c xs == rhs'*)  global_def,
    7.77 -       (*rhs' == rhs*)          Thm.symmetric rhs_conv]
    7.78 -      else Thm.transitive local_def global_def;
    7.79 +       (*rhs' == rhs*)          Thm.symmetric rhs_conv];
    7.80  
    7.81      (*note*)
    7.82      val ([(res_name, [res])], lthy4) = lthy3
    7.83 @@ -294,7 +290,12 @@
    7.84      val global_consts = map (Term.dest_Const o Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
    7.85  
    7.86      (*axioms*)
    7.87 -    val hyps = map Thm.term_of (Assumption.assms_of lthy');
    7.88 +    val resubst_instparams = map_aterms (fn t as Free (v, T) =>
    7.89 +      (case Class.instantiation_param lthy' v
    7.90 +       of NONE => t
    7.91 +        | SOME c => Const (c, T)) | t => t)
    7.92 +    val hyps = map Thm.term_of (Assumption.assms_of lthy')
    7.93 +      |> map resubst_instparams;
    7.94      fun axiom ((name, atts), props) thy = thy
    7.95        |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
    7.96        |-> (fn ths => pair ((name, atts), [(ths, [])]));
    7.97 @@ -318,11 +319,10 @@
    7.98  fun init_instantiaton arities = make_target "" false false arities
    7.99  
   7.100  fun init_ctxt (Target {target, is_locale, is_class, instantiation}) =
   7.101 -  if null instantiation then
   7.102 -    if not is_locale then ProofContext.init
   7.103 -    else if not is_class then Locale.init target
   7.104 -    else Class.init target
   7.105 -  else Class.instantiation instantiation;
   7.106 +  if not (null instantiation) then Class.init_instantiation instantiation
   7.107 +  else if not is_locale then ProofContext.init
   7.108 +  else if not is_class then Locale.init target
   7.109 +  else Class.init target;
   7.110  
   7.111  fun init_lthy (ta as Target {target, instantiation, ...}) =
   7.112    Data.put ta #>
   7.113 @@ -336,7 +336,8 @@
   7.114      term_syntax = term_syntax ta,
   7.115      declaration = declaration ta,
   7.116      reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
   7.117 -    exit = if null instantiation then LocalTheory.target_of else Class.end_instantiation}
   7.118 +    exit = if null instantiation then LocalTheory.target_of
   7.119 +      else Class.conclude_instantiation #> LocalTheory.target_of}
   7.120  and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
   7.121  
   7.122  in
   7.123 @@ -347,8 +348,8 @@
   7.124  fun context "-" thy = init NONE thy
   7.125    | context target thy = init (SOME (Locale.intern thy target)) thy;
   7.126  
   7.127 -fun instantiation raw_arities thy =
   7.128 -  init_lthy_ctxt (init_instantiaton (map (Sign.cert_arity thy) raw_arities)) thy;
   7.129 +fun instantiation arities thy =
   7.130 +  init_lthy_ctxt (init_instantiaton arities) thy;
   7.131  
   7.132  end;
   7.133  
     8.1 --- a/src/Tools/code/code_funcgr.ML	Wed Nov 28 09:01:40 2007 +0100
     8.2 +++ b/src/Tools/code/code_funcgr.ML	Wed Nov 28 09:01:42 2007 +0100
     8.3 @@ -157,7 +157,7 @@
     8.4      val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
     8.5      fun all_classparams tyco class =
     8.6        these (try (#params o AxClass.get_info thy) class)
     8.7 -      |> map (fn (c, _) => Class.inst_const thy (c, tyco))
     8.8 +      |> map (fn (c, _) => Class.param_of_inst thy (c, tyco))
     8.9    in
    8.10      Symtab.empty
    8.11      |> fold (fn (tyco, class) =>
    8.12 @@ -211,7 +211,7 @@
    8.13        |> resort_funcss thy algebra funcgr
    8.14        |> filter_out (can (Graph.get_node funcgr) o fst);
    8.15      fun typ_func c [] = Code.default_typ thy c
    8.16 -      | typ_func c (thms as thm :: _) = case Class.param_const thy c
    8.17 +      | typ_func c (thms as thm :: _) = case Class.inst_of_param thy c
    8.18           of SOME (c', tyco) => 
    8.19                let
    8.20                  val (_, ty) = CodeUnit.head_func thm;
     9.1 --- a/src/Tools/code/code_name.ML	Wed Nov 28 09:01:40 2007 +0100
     9.2 +++ b/src/Tools/code/code_name.ML	Wed Nov 28 09:01:42 2007 +0100
     9.3 @@ -216,7 +216,7 @@
     9.4   of SOME dtco => SOME (thyname_of_tyco thy dtco)
     9.5    | NONE => (case AxClass.class_of_param thy c
     9.6       of SOME class => SOME (thyname_of_class thy class)
     9.7 -      | NONE => (case Class.param_const thy c
     9.8 +      | NONE => (case Class.inst_of_param thy c
     9.9           of SOME (c, tyco) => SOME (thyname_of_instance thy
    9.10                ((the o AxClass.class_of_param thy) c, tyco))
    9.11            | NONE => NONE));
    10.1 --- a/src/Tools/code/code_package.ML	Wed Nov 28 09:01:40 2007 +0100
    10.2 +++ b/src/Tools/code/code_package.ML	Wed Nov 28 09:01:42 2007 +0100
    10.3 @@ -33,7 +33,7 @@
    10.4        in
    10.5          gr
    10.6          |> Graph.subgraph (member (op =) select) 
    10.7 -        |> Graph.map_nodes ((apsnd o map) (Conv.fconv_rule (Class.overload thy)))
    10.8 +        |> Graph.map_nodes ((apsnd o map) (Class.overload thy))
    10.9        end;
   10.10  
   10.11  fun code_thms thy =
    11.1 --- a/src/Tools/code/code_thingol.ML	Wed Nov 28 09:01:40 2007 +0100
    11.2 +++ b/src/Tools/code/code_thingol.ML	Wed Nov 28 09:01:42 2007 +0100
    11.3 @@ -461,7 +461,7 @@
    11.4      fun exprgen_classparam_inst (c, ty) =
    11.5        let
    11.6          val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
    11.7 -        val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
    11.8 +        val thm = Class.unoverload_conv thy (Thm.cterm_of thy c_inst);
    11.9          val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
   11.10            o Logic.dest_equals o Thm.prop_of) thm;
   11.11        in