merged
authorhaftmann
Wed Aug 11 20:25:44 2010 +0200 (2010-08-11)
changeset 3838407c33be08476
parent 38354 fed4e71a8c0f
parent 38383 1ad96229b455
child 38385 60acf9470a9b
merged
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/IsaMakefile	Wed Aug 11 18:44:06 2010 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Wed Aug 11 20:25:44 2010 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4    Isar/auto_bind.ML					\
     1.5    Isar/calculation.ML					\
     1.6    Isar/class.ML						\
     1.7 -  Isar/class_target.ML					\
     1.8 +  Isar/class_declaration.ML				\
     1.9    Isar/code.ML						\
    1.10    Isar/constdefs.ML					\
    1.11    Isar/context_rules.ML					\
     2.1 --- a/src/Pure/Isar/class.ML	Wed Aug 11 18:44:06 2010 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Wed Aug 11 20:25:44 2010 +0200
     2.3 @@ -1,351 +1,640 @@
     2.4  (*  Title:      Pure/Isar/class.ML
     2.5      Author:     Florian Haftmann, TU Muenchen
     2.6  
     2.7 -Type classes derived from primitive axclasses and locales -- interfaces.
     2.8 +Type classes derived from primitive axclasses and locales.
     2.9  *)
    2.10  
    2.11  signature CLASS =
    2.12  sig
    2.13 -  include CLASS_TARGET
    2.14 -    (*FIXME the split into class_target.ML, named_target.ML and
    2.15 -      class.ML is artificial*)
    2.16 +  (*classes*)
    2.17 +  val is_class: theory -> class -> bool
    2.18 +  val these_params: theory -> sort -> (string * (class * (string * typ))) list
    2.19 +  val base_sort: theory -> class -> sort
    2.20 +  val rules: theory -> class -> thm option * thm
    2.21 +  val these_defs: theory -> sort -> thm list
    2.22 +  val these_operations: theory -> sort
    2.23 +    -> (string * (class * (typ * term))) list
    2.24 +  val print_classes: theory -> unit
    2.25 +  val init: class -> theory -> Proof.context
    2.26 +  val begin: class list -> sort -> Proof.context -> Proof.context
    2.27 +  val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory
    2.28 +  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
    2.29 +  val refresh_syntax: class -> Proof.context -> Proof.context
    2.30 +  val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
    2.31 +  val class_prefix: string -> string
    2.32 +  val register: class -> class list -> ((string * typ) * (string * typ)) list
    2.33 +    -> sort -> morphism -> morphism -> thm option -> thm option -> thm
    2.34 +    -> theory -> theory
    2.35  
    2.36 -  val class: binding -> class list -> Element.context_i list
    2.37 -    -> theory -> string * local_theory
    2.38 -  val class_cmd: binding -> xstring list -> Element.context list
    2.39 -    -> theory -> string * local_theory
    2.40 -  val prove_subclass: tactic -> class -> local_theory -> local_theory
    2.41 -  val subclass: class -> local_theory -> Proof.state
    2.42 -  val subclass_cmd: xstring -> local_theory -> Proof.state
    2.43 +  (*instances*)
    2.44 +  val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
    2.45 +  val instantiation_instance: (local_theory -> local_theory)
    2.46 +    -> local_theory -> Proof.state
    2.47 +  val prove_instantiation_instance: (Proof.context -> tactic)
    2.48 +    -> local_theory -> local_theory
    2.49 +  val prove_instantiation_exit: (Proof.context -> tactic)
    2.50 +    -> local_theory -> theory
    2.51 +  val prove_instantiation_exit_result: (morphism -> 'a -> 'b)
    2.52 +    -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
    2.53 +  val read_multi_arity: theory -> xstring list * xstring list * xstring
    2.54 +    -> string list * (string * sort) list * sort
    2.55 +  val type_name: string -> string
    2.56 +  val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
    2.57 +  val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
    2.58 +
    2.59 +  (*subclasses*)
    2.60 +  val classrel: class * class -> theory -> Proof.state
    2.61 +  val classrel_cmd: xstring * xstring -> theory -> Proof.state
    2.62 +  val register_subclass: class * class -> morphism option -> Element.witness option
    2.63 +    -> morphism -> theory -> theory
    2.64 +
    2.65 +  (*tactics*)
    2.66 +  val intro_classes_tac: thm list -> tactic
    2.67 +  val default_intro_tac: Proof.context -> thm list -> tactic
    2.68  end;
    2.69  
    2.70 -structure Class : CLASS =
    2.71 +structure Class: CLASS =
    2.72  struct
    2.73  
    2.74 -open Class_Target;
    2.75 +(** class data **)
    2.76 +
    2.77 +datatype class_data = ClassData of {
    2.78 +
    2.79 +  (* static part *)
    2.80 +  consts: (string * string) list
    2.81 +    (*locale parameter ~> constant name*),
    2.82 +  base_sort: sort,
    2.83 +  base_morph: morphism
    2.84 +    (*static part of canonical morphism*),
    2.85 +  export_morph: morphism,
    2.86 +  assm_intro: thm option,
    2.87 +  of_class: thm,
    2.88 +  axiom: thm option,
    2.89 +  
    2.90 +  (* dynamic part *)
    2.91 +  defs: thm list,
    2.92 +  operations: (string * (class * (typ * term))) list
    2.93 +
    2.94 +};
    2.95 +
    2.96 +fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
    2.97 +    (defs, operations)) =
    2.98 +  ClassData { consts = consts, base_sort = base_sort,
    2.99 +    base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
   2.100 +    of_class = of_class, axiom = axiom, defs = defs, operations = operations };
   2.101 +fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro,
   2.102 +    of_class, axiom, defs, operations }) =
   2.103 +  make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
   2.104 +    (defs, operations)));
   2.105 +fun merge_class_data _ (ClassData { consts = consts,
   2.106 +    base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
   2.107 +    of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
   2.108 +  ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
   2.109 +    of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
   2.110 +  make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
   2.111 +    (Thm.merge_thms (defs1, defs2),
   2.112 +      AList.merge (op =) (K true) (operations1, operations2)));
   2.113 +
   2.114 +structure ClassData = Theory_Data
   2.115 +(
   2.116 +  type T = class_data Graph.T
   2.117 +  val empty = Graph.empty;
   2.118 +  val extend = I;
   2.119 +  val merge = Graph.join merge_class_data;
   2.120 +);
   2.121 +
   2.122 +
   2.123 +(* queries *)
   2.124 +
   2.125 +fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class
   2.126 + of SOME (ClassData data) => SOME data
   2.127 +  | NONE => NONE;
   2.128 +
   2.129 +fun the_class_data thy class = case lookup_class_data thy class
   2.130 + of NONE => error ("Undeclared class " ^ quote class)
   2.131 +  | SOME data => data;
   2.132 +
   2.133 +val is_class = is_some oo lookup_class_data;
   2.134 +
   2.135 +val ancestry = Graph.all_succs o ClassData.get;
   2.136 +val heritage = Graph.all_preds o ClassData.get;
   2.137 +
   2.138 +fun these_params thy =
   2.139 +  let
   2.140 +    fun params class =
   2.141 +      let
   2.142 +        val const_typs = (#params o AxClass.get_info thy) class;
   2.143 +        val const_names = (#consts o the_class_data thy) class;
   2.144 +      in
   2.145 +        (map o apsnd)
   2.146 +          (fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names
   2.147 +      end;
   2.148 +  in maps params o ancestry thy end;
   2.149 +
   2.150 +val base_sort = #base_sort oo the_class_data;
   2.151 +
   2.152 +fun rules thy class =
   2.153 +  let val { axiom, of_class, ... } = the_class_data thy class
   2.154 +  in (axiom, of_class) end;
   2.155 +
   2.156 +fun all_assm_intros thy =
   2.157 +  Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm)
   2.158 +    (the_list assm_intro)) (ClassData.get thy) [];
   2.159 +
   2.160 +fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
   2.161 +fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
   2.162 +
   2.163 +val base_morphism = #base_morph oo the_class_data;
   2.164 +fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class])
   2.165 + of SOME eq_morph => base_morphism thy class $> eq_morph
   2.166 +  | NONE => base_morphism thy class;
   2.167 +val export_morphism = #export_morph oo the_class_data;
   2.168 +
   2.169 +fun print_classes thy =
   2.170 +  let
   2.171 +    val ctxt = ProofContext.init_global thy;
   2.172 +    val algebra = Sign.classes_of thy;
   2.173 +    val arities =
   2.174 +      Symtab.empty
   2.175 +      |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
   2.176 +           Symtab.map_default (class, []) (insert (op =) tyco)) arities)
   2.177 +             (Sorts.arities_of algebra);
   2.178 +    val the_arities = these o Symtab.lookup arities;
   2.179 +    fun mk_arity class tyco =
   2.180 +      let
   2.181 +        val Ss = Sorts.mg_domain algebra tyco [class];
   2.182 +      in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
   2.183 +    fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
   2.184 +      ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
   2.185 +    fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   2.186 +      (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
   2.187 +      (SOME o Pretty.block) [Pretty.str "supersort: ",
   2.188 +        (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
   2.189 +      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
   2.190 +          (Pretty.str "parameters:" :: ps)) o map mk_param
   2.191 +        o these o Option.map #params o try (AxClass.get_info thy)) class,
   2.192 +      (SOME o Pretty.block o Pretty.breaks) [
   2.193 +        Pretty.str "instances:",
   2.194 +        Pretty.list "" "" (map (mk_arity class) (the_arities class))
   2.195 +      ]
   2.196 +    ]
   2.197 +  in
   2.198 +    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "")
   2.199 +      o map mk_entry o Sorts.all_classes) algebra
   2.200 +  end;
   2.201 +
   2.202 +
   2.203 +(* updaters *)
   2.204 +
   2.205 +fun register class sups params base_sort base_morph export_morph
   2.206 +    axiom assm_intro of_class thy =
   2.207 +  let
   2.208 +    val operations = map (fn (v_ty as (_, ty), (c, _)) =>
   2.209 +      (c, (class, (ty, Free v_ty)))) params;
   2.210 +    val add_class = Graph.new_node (class,
   2.211 +        make_class_data (((map o pairself) fst params, base_sort,
   2.212 +          base_morph, export_morph, assm_intro, of_class, axiom), ([], operations)))
   2.213 +      #> fold (curry Graph.add_edge class) sups;
   2.214 +  in ClassData.map add_class thy end;
   2.215 +
   2.216 +fun activate_defs class thms thy = case Element.eq_morphism thy thms
   2.217 + of SOME eq_morph => fold (fn cls => fn thy =>
   2.218 +      Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
   2.219 +        (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
   2.220 +  | NONE => thy;
   2.221  
   2.222 -(** class definitions **)
   2.223 +fun register_operation class (c, (t, some_def)) thy =
   2.224 +  let
   2.225 +    val base_sort = base_sort thy class;
   2.226 +    val prep_typ = map_type_tfree
   2.227 +      (fn (v, sort) => if Name.aT = v
   2.228 +        then TFree (v, base_sort) else TVar ((v, 0), sort));
   2.229 +    val t' = map_types prep_typ t;
   2.230 +    val ty' = Term.fastype_of t';
   2.231 +  in
   2.232 +    thy
   2.233 +    |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
   2.234 +      (fn (defs, operations) =>
   2.235 +        (fold cons (the_list some_def) defs,
   2.236 +          (c, (class, (ty', t'))) :: operations))
   2.237 +    |> activate_defs class (the_list some_def)
   2.238 +  end;
   2.239 +
   2.240 +fun register_subclass (sub, sup) some_dep_morph some_wit export thy =
   2.241 +  let
   2.242 +    val intros = (snd o rules thy) sup :: map_filter I
   2.243 +      [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit,
   2.244 +        (fst o rules thy) sub];
   2.245 +    val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
   2.246 +    val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
   2.247 +      (K tac);
   2.248 +    val diff_sort = Sign.complete_sort thy [sup]
   2.249 +      |> subtract (op =) (Sign.complete_sort thy [sub])
   2.250 +      |> filter (is_class thy);
   2.251 +    val add_dependency = case some_dep_morph
   2.252 +     of SOME dep_morph => Locale.add_dependency sub
   2.253 +          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export
   2.254 +      | NONE => I
   2.255 +  in
   2.256 +    thy
   2.257 +    |> AxClass.add_classrel classrel
   2.258 +    |> ClassData.map (Graph.add_edge (sub, sup))
   2.259 +    |> activate_defs sub (these_defs thy diff_sort)
   2.260 +    |> add_dependency
   2.261 +  end;
   2.262 +
   2.263 +
   2.264 +(** classes and class target **)
   2.265 +
   2.266 +(* class context syntax *)
   2.267 +
   2.268 +fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
   2.269 +  o these_operations thy;
   2.270 +
   2.271 +fun redeclare_const thy c =
   2.272 +  let val b = Long_Name.base_name c
   2.273 +  in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
   2.274 +
   2.275 +fun synchronize_class_syntax sort base_sort ctxt =
   2.276 +  let
   2.277 +    val thy = ProofContext.theory_of ctxt;
   2.278 +    val algebra = Sign.classes_of thy;
   2.279 +    val operations = these_operations thy sort;
   2.280 +    fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
   2.281 +    val primary_constraints =
   2.282 +      (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
   2.283 +    val secondary_constraints =
   2.284 +      (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
   2.285 +    fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
   2.286 +     of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
   2.287 +         of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
   2.288 +             of SOME (_, ty' as TVar (vi, sort)) =>
   2.289 +                  if Type_Infer.is_param vi
   2.290 +                    andalso Sorts.sort_le algebra (base_sort, sort)
   2.291 +                      then SOME (ty', TFree (Name.aT, base_sort))
   2.292 +                      else NONE
   2.293 +              | _ => NONE)
   2.294 +          | NONE => NONE)
   2.295 +      | NONE => NONE)
   2.296 +    fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c);
   2.297 +    val unchecks = these_unchecks thy sort;
   2.298 +  in
   2.299 +    ctxt
   2.300 +    |> fold (redeclare_const thy o fst) primary_constraints
   2.301 +    |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
   2.302 +        (((improve, subst), true), unchecks)), false))
   2.303 +    |> Overloading.set_primary_constraints
   2.304 +  end;
   2.305 +
   2.306 +fun refresh_syntax class ctxt =
   2.307 +  let
   2.308 +    val thy = ProofContext.theory_of ctxt;
   2.309 +    val base_sort = base_sort thy class;
   2.310 +  in synchronize_class_syntax [class] base_sort ctxt end;
   2.311 +
   2.312 +fun redeclare_operations thy sort =
   2.313 +  fold (redeclare_const thy o fst) (these_operations thy sort);
   2.314 +
   2.315 +fun begin sort base_sort ctxt =
   2.316 +  ctxt
   2.317 +  |> Variable.declare_term
   2.318 +      (Logic.mk_type (TFree (Name.aT, base_sort)))
   2.319 +  |> synchronize_class_syntax sort base_sort
   2.320 +  |> Overloading.add_improvable_syntax;
   2.321 +
   2.322 +fun init class thy =
   2.323 +  thy
   2.324 +  |> Locale.init class
   2.325 +  |> begin [class] (base_sort thy class);
   2.326 +
   2.327 +
   2.328 +(* class target *)
   2.329 +
   2.330 +val class_prefix = Logic.const_of_class o Long_Name.base_name;
   2.331 +
   2.332 +fun declare class ((c, mx), (type_params, dict)) thy =
   2.333 +  let
   2.334 +    val morph = morphism thy class;
   2.335 +    val b = Morphism.binding morph c;
   2.336 +    val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b);
   2.337 +    val c' = Sign.full_name thy b;
   2.338 +    val dict' = Morphism.term morph dict;
   2.339 +    val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict';
   2.340 +    val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict')
   2.341 +      |> map_types Type.strip_sorts;
   2.342 +  in
   2.343 +    thy
   2.344 +    |> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
   2.345 +    |> snd
   2.346 +    |> Thm.add_def false false (b_def, def_eq)
   2.347 +    |>> apsnd Thm.varifyT_global
   2.348 +    |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm)
   2.349 +      #> snd
   2.350 +      #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
   2.351 +    |> Sign.add_const_constraint (c', SOME ty')
   2.352 +  end;
   2.353 +
   2.354 +fun abbrev class prmode ((c, mx), rhs) thy =
   2.355 +  let
   2.356 +    val morph = morphism thy class;
   2.357 +    val unchecks = these_unchecks thy [class];
   2.358 +    val b = Morphism.binding morph c;
   2.359 +    val c' = Sign.full_name thy b;
   2.360 +    val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
   2.361 +    val ty' = Term.fastype_of rhs';
   2.362 +    val rhs'' = map_types Logic.varifyT_global rhs';
   2.363 +  in
   2.364 +    thy
   2.365 +    |> Sign.add_abbrev (#1 prmode) (b, rhs'')
   2.366 +    |> snd
   2.367 +    |> Sign.add_const_constraint (c', SOME ty')
   2.368 +    |> Sign.notation true prmode [(Const (c', ty'), mx)]
   2.369 +    |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE))
   2.370 +  end;
   2.371 +
   2.372 +
   2.373 +(* simple subclasses *)
   2.374  
   2.375  local
   2.376  
   2.377 -(* calculating class-related rules including canonical interpretation *)
   2.378 -
   2.379 -fun calculate thy class sups base_sort param_map assm_axiom =
   2.380 -  let
   2.381 -    val empty_ctxt = ProofContext.init_global thy;
   2.382 -
   2.383 -    (* instantiation of canonical interpretation *)
   2.384 -    val aT = TFree (Name.aT, base_sort);
   2.385 -    val param_map_const = (map o apsnd) Const param_map;
   2.386 -    val param_map_inst = (map o apsnd)
   2.387 -      (Const o apsnd (map_atyps (K aT))) param_map;
   2.388 -    val const_morph = Element.inst_morphism thy
   2.389 -      (Symtab.empty, Symtab.make param_map_inst);
   2.390 -    val typ_morph = Element.inst_morphism thy
   2.391 -      (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty);
   2.392 -    val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt
   2.393 -      |> Expression.cert_goal_expression ([(class, (("", false),
   2.394 -           Expression.Named param_map_const))], []);
   2.395 -    val (props, inst_morph) = if null param_map
   2.396 -      then (raw_props |> map (Morphism.term typ_morph),
   2.397 -        raw_inst_morph $> typ_morph)
   2.398 -      else (raw_props, raw_inst_morph); (*FIXME proper handling in
   2.399 -        locale.ML / expression.ML would be desirable*)
   2.400 -
   2.401 -    (* witness for canonical interpretation *)
   2.402 -    val prop = try the_single props;
   2.403 -    val wit = Option.map (fn prop => let
   2.404 -        val sup_axioms = map_filter (fst o rules thy) sups;
   2.405 -        val loc_intro_tac = case Locale.intros_of thy class
   2.406 -          of (_, NONE) => all_tac
   2.407 -           | (_, SOME intro) => ALLGOALS (Tactic.rtac intro);
   2.408 -        val tac = loc_intro_tac
   2.409 -          THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom))
   2.410 -      in Element.prove_witness empty_ctxt prop tac end) prop;
   2.411 -    val axiom = Option.map Element.conclude_witness wit;
   2.412 -
   2.413 -    (* canonical interpretation *)
   2.414 -    val base_morph = inst_morph
   2.415 -      $> Morphism.binding_morphism (Binding.prefix false (class_prefix class))
   2.416 -      $> Element.satisfy_morphism (the_list wit);
   2.417 -    val eq_morph = Element.eq_morphism thy (these_defs thy sups);
   2.418 -
   2.419 -    (* assm_intro *)
   2.420 -    fun prove_assm_intro thm =
   2.421 -      let
   2.422 -        val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
   2.423 -        val const_eq_morph = case eq_morph
   2.424 -         of SOME eq_morph => const_morph $> eq_morph
   2.425 -          | NONE => const_morph
   2.426 -        val thm'' = Morphism.thm const_eq_morph thm';
   2.427 -        val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
   2.428 -      in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
   2.429 -    val assm_intro = Option.map prove_assm_intro
   2.430 -      (fst (Locale.intros_of thy class));
   2.431 -
   2.432 -    (* of_class *)
   2.433 -    val of_class_prop_concl = Logic.mk_of_class (aT, class);
   2.434 -    val of_class_prop = case prop of NONE => of_class_prop_concl
   2.435 -      | SOME prop => Logic.mk_implies (Morphism.term const_morph
   2.436 -          ((map_types o map_atyps) (K aT) prop), of_class_prop_concl);
   2.437 -    val sup_of_classes = map (snd o rules thy) sups;
   2.438 -    val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
   2.439 -    val axclass_intro = #intro (AxClass.get_info thy class);
   2.440 -    val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
   2.441 -    val tac = REPEAT (SOMEGOAL
   2.442 -      (Tactic.match_tac (axclass_intro :: sup_of_classes
   2.443 -         @ loc_axiom_intros @ base_sort_trivs)
   2.444 -           ORELSE' Tactic.assume_tac));
   2.445 -    val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac);
   2.446 -
   2.447 -  in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
   2.448 -
   2.449 -
   2.450 -(* reading and processing class specifications *)
   2.451 -
   2.452 -fun prep_class_elems prep_decl thy sups raw_elems =
   2.453 +fun gen_classrel mk_prop classrel thy =
   2.454    let
   2.455 -
   2.456 -    (* user space type system: only permits 'a type variable, improves towards 'a *)
   2.457 -    val algebra = Sign.classes_of thy;
   2.458 -    val inter_sort = curry (Sorts.inter_sort algebra);
   2.459 -    val proto_base_sort = if null sups then Sign.defaultS thy
   2.460 -      else fold inter_sort (map (base_sort thy) sups) [];
   2.461 -    val base_constraints = (map o apsnd)
   2.462 -      (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
   2.463 -        (these_operations thy sups);
   2.464 -    val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) =>
   2.465 -          if v = Name.aT then T
   2.466 -          else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
   2.467 -      | T => T);
   2.468 -    fun singleton_fixate Ts =
   2.469 -      let
   2.470 -        fun extract f = (fold o fold_atyps) f Ts [];
   2.471 -        val tfrees = extract
   2.472 -          (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
   2.473 -        val inferred_sort = extract
   2.474 -          (fn TVar (_, sort) => inter_sort sort | _ => I);
   2.475 -        val fixate_sort = if null tfrees then inferred_sort
   2.476 -          else case tfrees
   2.477 -           of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
   2.478 -                then inter_sort a_sort inferred_sort
   2.479 -                else error ("Type inference imposes additional sort constraint "
   2.480 -                  ^ Syntax.string_of_sort_global thy inferred_sort
   2.481 -                  ^ " of type parameter " ^ Name.aT ^ " of sort "
   2.482 -                  ^ Syntax.string_of_sort_global thy a_sort ^ ".")
   2.483 -            | _ => error "Multiple type variables in class specification.";
   2.484 -      in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
   2.485 -    fun add_typ_check level name f = Context.proof_map
   2.486 -      (Syntax.add_typ_check level name (fn xs => fn ctxt =>
   2.487 -        let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
   2.488 -
   2.489 -    (* preprocessing elements, retrieving base sort from type-checked elements *)
   2.490 -    val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
   2.491 -      #> redeclare_operations thy sups
   2.492 -      #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
   2.493 -      #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
   2.494 -    val raw_supexpr = (map (fn sup => (sup, (("", false),
   2.495 -      Expression.Positional []))) sups, []);
   2.496 -    val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy
   2.497 -      |> prep_decl raw_supexpr init_class_body raw_elems;
   2.498 -    fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
   2.499 -      | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
   2.500 -      | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
   2.501 -          fold_types f t #> (fold o fold_types) f ts) o snd) assms
   2.502 -      | fold_element_types f (Element.Defines _) =
   2.503 -          error ("\"defines\" element not allowed in class specification.")
   2.504 -      | fold_element_types f (Element.Notes _) =
   2.505 -          error ("\"notes\" element not allowed in class specification.");
   2.506 -    val base_sort = if null inferred_elems then proto_base_sort else
   2.507 -      case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
   2.508 -       of [] => error "No type variable in class specification"
   2.509 -        | [(_, sort)] => sort
   2.510 -        | _ => error "Multiple type variables in class specification";
   2.511 -    val supparams = map (fn ((c, T), _) =>
   2.512 -      (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams;
   2.513 -    val supparam_names = map fst supparams;
   2.514 -    fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c);
   2.515 -    val supexpr = (map (fn sup => (sup, (("", false),
   2.516 -      Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups,
   2.517 -        map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams);
   2.518 -
   2.519 -  in (base_sort, supparam_names, supexpr, inferred_elems) end;
   2.520 -
   2.521 -val cert_class_elems = prep_class_elems Expression.cert_declaration;
   2.522 -val read_class_elems = prep_class_elems Expression.cert_read_declaration;
   2.523 -
   2.524 -fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems =
   2.525 -  let
   2.526 -
   2.527 -    (* prepare import *)
   2.528 -    val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
   2.529 -    val sups = map (prep_class thy) raw_supclasses
   2.530 -      |> Sign.minimize_sort thy;
   2.531 -    val _ = case filter_out (is_class thy) sups
   2.532 -     of [] => ()
   2.533 -      | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
   2.534 -    val raw_supparams = (map o apsnd) (snd o snd) (these_params thy sups);
   2.535 -    val raw_supparam_names = map fst raw_supparams;
   2.536 -    val _ = if has_duplicates (op =) raw_supparam_names
   2.537 -      then error ("Duplicate parameter(s) in superclasses: "
   2.538 -        ^ (commas o map quote o duplicates (op =)) raw_supparam_names)
   2.539 -      else ();
   2.540 -
   2.541 -    (* infer types and base sort *)
   2.542 -    val (base_sort, supparam_names, supexpr, inferred_elems) =
   2.543 -      prep_class_elems thy sups raw_elems;
   2.544 -    val sup_sort = inter_sort base_sort sups;
   2.545 -
   2.546 -    (* process elements as class specification *)
   2.547 -    val class_ctxt = begin sups base_sort (ProofContext.init_global thy);
   2.548 -    val ((_, _, syntax_elems), _) = class_ctxt
   2.549 -      |> Expression.cert_declaration supexpr I inferred_elems;
   2.550 -    fun check_vars e vs = if null vs
   2.551 -      then error ("No type variable in part of specification element "
   2.552 -        ^ (Pretty.string_of o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
   2.553 -      else ();
   2.554 -    fun check_element (e as Element.Fixes fxs) =
   2.555 -          map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs
   2.556 -      | check_element (e as Element.Assumes assms) =
   2.557 -          maps (fn (_, ts_pss) => map
   2.558 -            (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms
   2.559 -      | check_element e = [()];
   2.560 -    val _ = map check_element syntax_elems;
   2.561 -    fun fork_syn (Element.Fixes xs) =
   2.562 -          fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
   2.563 -          #>> Element.Fixes
   2.564 -      | fork_syn x = pair x;
   2.565 -    val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
   2.566 -
   2.567 -  in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end;
   2.568 -
   2.569 -val cert_class_spec = prep_class_spec (K I) cert_class_elems;
   2.570 -val read_class_spec = prep_class_spec Sign.intern_class read_class_elems;
   2.571 -
   2.572 -
   2.573 -(* class establishment *)
   2.574 -
   2.575 -fun add_consts class base_sort sups supparam_names global_syntax thy =
   2.576 -  let
   2.577 -    (*FIXME simplify*)
   2.578 -    val supconsts = supparam_names
   2.579 -      |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
   2.580 -      |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
   2.581 -    val all_params = Locale.params_of thy class;
   2.582 -    val raw_params = (snd o chop (length supparam_names)) all_params;
   2.583 -    fun add_const ((raw_c, raw_ty), _) thy =
   2.584 -      let
   2.585 -        val b = Binding.name raw_c;
   2.586 -        val c = Sign.full_name thy b;
   2.587 -        val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
   2.588 -        val ty0 = Type.strip_sorts ty;
   2.589 -        val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
   2.590 -        val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
   2.591 -      in
   2.592 -        thy
   2.593 -        |> Sign.declare_const ((b, ty0), syn)
   2.594 -        |> snd
   2.595 -        |> pair ((Name.of_binding b, ty), (c, ty'))
   2.596 -      end;
   2.597 +    fun after_qed results =
   2.598 +      ProofContext.theory ((fold o fold) AxClass.add_classrel results);
   2.599    in
   2.600      thy
   2.601 -    |> Sign.add_path (class_prefix class)
   2.602 -    |> fold_map add_const raw_params
   2.603 -    ||> Sign.restore_naming thy
   2.604 -    |-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
   2.605 -  end;
   2.606 -
   2.607 -fun adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax thy =
   2.608 -  let
   2.609 -    (*FIXME simplify*)
   2.610 -    fun globalize param_map = map_aterms
   2.611 -      (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
   2.612 -        | t => t);
   2.613 -    val raw_pred = Locale.intros_of thy class
   2.614 -      |> fst
   2.615 -      |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of);
   2.616 -    fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
   2.617 -     of [] => NONE
   2.618 -      | [thm] => SOME thm;
   2.619 -  in
   2.620 -    thy
   2.621 -    |> add_consts class base_sort sups supparam_names global_syntax
   2.622 -    |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
   2.623 -          (map (fst o snd) params)
   2.624 -          [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
   2.625 -    #> snd
   2.626 -    #> `get_axiom
   2.627 -    #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
   2.628 -    #> pair (param_map, params, assm_axiom)))
   2.629 -  end;
   2.630 -
   2.631 -fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
   2.632 -  let
   2.633 -    val class = Sign.full_name thy b;
   2.634 -    val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
   2.635 -      prep_class_spec thy raw_supclasses raw_elems;
   2.636 -  in
   2.637 -    thy
   2.638 -    |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems
   2.639 -    |> snd |> Local_Theory.exit_global
   2.640 -    |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
   2.641 -    ||> Theory.checkpoint
   2.642 -    |-> (fn (param_map, params, assm_axiom) =>
   2.643 -       `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
   2.644 -    #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
   2.645 -       Context.theory_map (Locale.add_registration (class, base_morph)
   2.646 -         (Option.map (rpair true) eq_morph) export_morph)
   2.647 -    #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
   2.648 -    |> Named_Target.init (SOME class)
   2.649 -    |> pair class
   2.650 +    |> ProofContext.init_global
   2.651 +    |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
   2.652    end;
   2.653  
   2.654  in
   2.655  
   2.656 -val class = gen_class cert_class_spec;
   2.657 -val class_cmd = gen_class read_class_spec;
   2.658 +val classrel =
   2.659 +  gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel);
   2.660 +val classrel_cmd =
   2.661 +  gen_classrel (Logic.mk_classrel oo AxClass.read_classrel);
   2.662  
   2.663  end; (*local*)
   2.664  
   2.665  
   2.666 -(** subclass relations **)
   2.667 +(** instantiation target **)
   2.668 +
   2.669 +(* bookkeeping *)
   2.670 +
   2.671 +datatype instantiation = Instantiation of {
   2.672 +  arities: string list * (string * sort) list * sort,
   2.673 +  params: ((string * string) * (string * typ)) list
   2.674 +    (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
   2.675 +}
   2.676 +
   2.677 +structure Instantiation = Proof_Data
   2.678 +(
   2.679 +  type T = instantiation
   2.680 +  fun init _ = Instantiation { arities = ([], [], []), params = [] };
   2.681 +);
   2.682 +
   2.683 +fun mk_instantiation (arities, params) =
   2.684 +  Instantiation { arities = arities, params = params };
   2.685 +fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy)
   2.686 + of Instantiation data => data;
   2.687 +fun map_instantiation f = (Local_Theory.target o Instantiation.map)
   2.688 +  (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
   2.689  
   2.690 -local
   2.691 +fun the_instantiation lthy = case get_instantiation lthy
   2.692 + of { arities = ([], [], []), ... } => error "No instantiation target"
   2.693 +  | data => data;
   2.694 +
   2.695 +val instantiation_params = #params o get_instantiation;
   2.696 +
   2.697 +fun instantiation_param lthy b = instantiation_params lthy
   2.698 +  |> find_first (fn (_, (v, _)) => Binding.name_of b = v)
   2.699 +  |> Option.map (fst o fst);
   2.700  
   2.701 -fun gen_subclass prep_class do_proof raw_sup lthy =
   2.702 +fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
   2.703 +  let
   2.704 +    val ctxt = ProofContext.init_global thy;
   2.705 +    val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
   2.706 +      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
   2.707 +    val tycos = map #1 all_arities;
   2.708 +    val (_, sorts, sort) = hd all_arities;
   2.709 +    val vs = Name.names Name.context Name.aT sorts;
   2.710 +  in (tycos, vs, sort) end;
   2.711 +
   2.712 +
   2.713 +(* syntax *)
   2.714 +
   2.715 +fun synchronize_inst_syntax ctxt =
   2.716    let
   2.717 +    val Instantiation { params, ... } = Instantiation.get ctxt;
   2.718 +
   2.719 +    val lookup_inst_param = AxClass.lookup_inst_param
   2.720 +      (Sign.consts_of (ProofContext.theory_of ctxt)) params;
   2.721 +    fun subst (c, ty) = case lookup_inst_param (c, ty)
   2.722 +     of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
   2.723 +      | NONE => NONE;
   2.724 +    val unchecks =
   2.725 +      map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
   2.726 +  in
   2.727 +    ctxt
   2.728 +    |> Overloading.map_improvable_syntax
   2.729 +         (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
   2.730 +            (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
   2.731 +  end;
   2.732 +
   2.733 +fun resort_terms pp algebra consts constraints ts =
   2.734 +  let
   2.735 +    fun matchings (Const (c_ty as (c, _))) = (case constraints c
   2.736 +         of NONE => I
   2.737 +          | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
   2.738 +              (Consts.typargs consts c_ty) sorts)
   2.739 +      | matchings _ = I
   2.740 +    val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
   2.741 +      handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
   2.742 +    val inst = map_type_tvar
   2.743 +      (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
   2.744 +  in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
   2.745 +
   2.746 +
   2.747 +(* target *)
   2.748 +
   2.749 +val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*)
   2.750 +  let
   2.751 +    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
   2.752 +      orelse s = "'" orelse s = "_";
   2.753 +    val is_junk = not o is_valid andf Symbol.is_regular;
   2.754 +    val junk = Scan.many is_junk;
   2.755 +    val scan_valids = Symbol.scanner "Malformed input"
   2.756 +      ((junk |--
   2.757 +        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
   2.758 +        --| junk))
   2.759 +      ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
   2.760 +  in
   2.761 +    explode #> scan_valids #> implode
   2.762 +  end;
   2.763 +
   2.764 +val type_name = sanitize_name o Long_Name.base_name;
   2.765 +
   2.766 +fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.theory_result
   2.767 +    (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
   2.768 +  ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
   2.769 +  ##> Local_Theory.target synchronize_inst_syntax;
   2.770 +
   2.771 +fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   2.772 +  case instantiation_param lthy b
   2.773 +   of SOME c => if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
   2.774 +        else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
   2.775 +    | NONE => lthy |>
   2.776 +        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
   2.777 +
   2.778 +fun pretty lthy =
   2.779 +  let
   2.780 +    val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
   2.781      val thy = ProofContext.theory_of lthy;
   2.782 -    val proto_sup = prep_class thy raw_sup;
   2.783 -    val proto_sub = case Named_Target.peek lthy
   2.784 -     of {is_class = false, ...} => error "Not in a class context"
   2.785 -      | {target, ...} => target;
   2.786 -    val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
   2.787 +    fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
   2.788 +    fun pr_param ((c, _), (v, ty)) =
   2.789 +      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
   2.790 +        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
   2.791 +  in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end;
   2.792 +
   2.793 +fun conclude lthy =
   2.794 +  let
   2.795 +    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
   2.796 +    val thy = ProofContext.theory_of lthy;
   2.797 +    val _ = map (fn tyco => if Sign.of_sort thy
   2.798 +        (Type (tyco, map TFree vs), sort)
   2.799 +      then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
   2.800 +        tycos;
   2.801 +  in lthy end;
   2.802  
   2.803 -    val expr = ([(sup, (("", false), Expression.Positional []))], []);
   2.804 -    val (([props], deps, export), goal_ctxt) =
   2.805 -      Expression.cert_goal_expression expr lthy;
   2.806 -    val some_prop = try the_single props;
   2.807 -    val some_dep_morph = try the_single (map snd deps);
   2.808 -    fun after_qed some_wit =
   2.809 -      ProofContext.theory (register_subclass (sub, sup)
   2.810 -        some_dep_morph some_wit export)
   2.811 -      #> ProofContext.theory_of #> Named_Target.init (SOME sub);
   2.812 -  in do_proof after_qed some_prop goal_ctxt end;
   2.813 +fun instantiation (tycos, vs, sort) thy =
   2.814 +  let
   2.815 +    val _ = if null tycos then error "At least one arity must be given" else ();
   2.816 +    val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
   2.817 +    fun get_param tyco (param, (_, (c, ty))) =
   2.818 +      if can (AxClass.param_of_inst thy) (c, tyco)
   2.819 +      then NONE else SOME ((c, tyco),
   2.820 +        (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
   2.821 +    val params = map_product get_param tycos class_params |> map_filter I;
   2.822 +    val primary_constraints = map (apsnd
   2.823 +      (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
   2.824 +    val pp = Syntax.pp_global thy;
   2.825 +    val algebra = Sign.classes_of thy
   2.826 +      |> fold (fn tyco => Sorts.add_arities pp
   2.827 +            (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
   2.828 +    val consts = Sign.consts_of thy;
   2.829 +    val improve_constraints = AList.lookup (op =)
   2.830 +      (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
   2.831 +    fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts
   2.832 +     of NONE => NONE
   2.833 +      | SOME ts' => SOME (ts', ctxt);
   2.834 +    val lookup_inst_param = AxClass.lookup_inst_param consts params;
   2.835 +    val typ_instance = Type.typ_instance (Sign.tsig_of thy);
   2.836 +    fun improve (c, ty) = case lookup_inst_param (c, ty)
   2.837 +     of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE
   2.838 +      | NONE => NONE;
   2.839 +  in
   2.840 +    thy
   2.841 +    |> Theory.checkpoint
   2.842 +    |> ProofContext.init_global
   2.843 +    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
   2.844 +    |> fold (Variable.declare_typ o TFree) vs
   2.845 +    |> fold (Variable.declare_names o Free o snd) params
   2.846 +    |> (Overloading.map_improvable_syntax o apfst)
   2.847 +         (K ((primary_constraints, []), (((improve, K NONE), false), [])))
   2.848 +    |> Overloading.add_improvable_syntax
   2.849 +    |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
   2.850 +    |> synchronize_inst_syntax
   2.851 +    |> Local_Theory.init NONE ""
   2.852 +       {define = Generic_Target.define foundation,
   2.853 +        notes = Generic_Target.notes
   2.854 +          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
   2.855 +        abbrev = Generic_Target.abbrev
   2.856 +          (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
   2.857 +        declaration = K Generic_Target.theory_declaration,
   2.858 +        syntax_declaration = K Generic_Target.theory_declaration,
   2.859 +        pretty = pretty,
   2.860 +        exit = Local_Theory.target_of o conclude}
   2.861 +  end;
   2.862 +
   2.863 +fun instantiation_cmd arities thy =
   2.864 +  instantiation (read_multi_arity thy arities) thy;
   2.865 +
   2.866 +fun gen_instantiation_instance do_proof after_qed lthy =
   2.867 +  let
   2.868 +    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
   2.869 +    val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
   2.870 +    fun after_qed' results =
   2.871 +      Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
   2.872 +      #> after_qed;
   2.873 +  in
   2.874 +    lthy
   2.875 +    |> do_proof after_qed' arities_proof
   2.876 +  end;
   2.877  
   2.878 -fun user_proof after_qed some_prop =
   2.879 -  Element.witness_proof (after_qed o try the_single o the_single)
   2.880 -    [the_list some_prop];
   2.881 +val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
   2.882 +  Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
   2.883 +
   2.884 +fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
   2.885 +  fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
   2.886 +    (fn {context, ...} => tac context)) ts) lthy) I;
   2.887 +
   2.888 +fun prove_instantiation_exit tac = prove_instantiation_instance tac
   2.889 +  #> Local_Theory.exit_global;
   2.890  
   2.891 -fun tactic_proof tac after_qed some_prop ctxt =
   2.892 -  after_qed (Option.map
   2.893 -    (fn prop => Element.prove_witness ctxt prop tac) some_prop) ctxt;
   2.894 +fun prove_instantiation_exit_result f tac x lthy =
   2.895 +  let
   2.896 +    val morph = ProofContext.export_morphism lthy
   2.897 +      (ProofContext.init_global (ProofContext.theory_of lthy));
   2.898 +    val y = f morph x;
   2.899 +  in
   2.900 +    lthy
   2.901 +    |> prove_instantiation_exit (fn ctxt => tac ctxt y)
   2.902 +    |> pair y
   2.903 +  end;
   2.904 +
   2.905 +
   2.906 +(* simplified instantiation interface with no class parameter *)
   2.907  
   2.908 -in
   2.909 +fun instance_arity_cmd raw_arities thy =
   2.910 +  let
   2.911 +    val (tycos, vs, sort) = read_multi_arity thy raw_arities;
   2.912 +    val sorts = map snd vs;
   2.913 +    val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
   2.914 +    fun after_qed results = ProofContext.theory
   2.915 +      ((fold o fold) AxClass.add_arity results);
   2.916 +  in
   2.917 +    thy
   2.918 +    |> ProofContext.init_global
   2.919 +    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
   2.920 +  end;
   2.921 +
   2.922 +
   2.923 +(** tactics and methods **)
   2.924  
   2.925 -val subclass = gen_subclass (K I) user_proof;
   2.926 -fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
   2.927 -val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof;
   2.928 +fun intro_classes_tac facts st =
   2.929 +  let
   2.930 +    val thy = Thm.theory_of_thm st;
   2.931 +    val classes = Sign.all_classes thy;
   2.932 +    val class_trivs = map (Thm.class_triv thy) classes;
   2.933 +    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   2.934 +    val assm_intros = all_assm_intros thy;
   2.935 +  in
   2.936 +    Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
   2.937 +  end;
   2.938  
   2.939 -end; (*local*)
   2.940 +fun default_intro_tac ctxt [] =
   2.941 +      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
   2.942 +  | default_intro_tac _ _ = no_tac;
   2.943 +
   2.944 +fun default_tac rules ctxt facts =
   2.945 +  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   2.946 +    default_intro_tac ctxt facts;
   2.947 +
   2.948 +val _ = Context.>> (Context.map_theory
   2.949 + (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
   2.950 +    "back-chain introduction rules of classes" #>
   2.951 +  Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
   2.952 +    "apply some intro/elim rule"));
   2.953  
   2.954  end;
   2.955 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Aug 11 20:25:44 2010 +0200
     3.3 @@ -0,0 +1,345 @@
     3.4 +(*  Title:      Pure/Isar/class_declaration.ML
     3.5 +    Author:     Florian Haftmann, TU Muenchen
     3.6 +
     3.7 +Declaring classes and subclass relations.
     3.8 +*)
     3.9 +
    3.10 +signature CLASS_DECLARATION =
    3.11 +sig
    3.12 +  val class: binding -> class list -> Element.context_i list
    3.13 +    -> theory -> string * local_theory
    3.14 +  val class_cmd: binding -> xstring list -> Element.context list
    3.15 +    -> theory -> string * local_theory
    3.16 +  val prove_subclass: tactic -> class -> local_theory -> local_theory
    3.17 +  val subclass: class -> local_theory -> Proof.state
    3.18 +  val subclass_cmd: xstring -> local_theory -> Proof.state
    3.19 +end;
    3.20 +
    3.21 +structure Class_Declaration: CLASS_DECLARATION =
    3.22 +struct
    3.23 +
    3.24 +(** class definitions **)
    3.25 +
    3.26 +local
    3.27 +
    3.28 +(* calculating class-related rules including canonical interpretation *)
    3.29 +
    3.30 +fun calculate thy class sups base_sort param_map assm_axiom =
    3.31 +  let
    3.32 +    val empty_ctxt = ProofContext.init_global thy;
    3.33 +
    3.34 +    (* instantiation of canonical interpretation *)
    3.35 +    val aT = TFree (Name.aT, base_sort);
    3.36 +    val param_map_const = (map o apsnd) Const param_map;
    3.37 +    val param_map_inst = (map o apsnd)
    3.38 +      (Const o apsnd (map_atyps (K aT))) param_map;
    3.39 +    val const_morph = Element.inst_morphism thy
    3.40 +      (Symtab.empty, Symtab.make param_map_inst);
    3.41 +    val typ_morph = Element.inst_morphism thy
    3.42 +      (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty);
    3.43 +    val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt
    3.44 +      |> Expression.cert_goal_expression ([(class, (("", false),
    3.45 +           Expression.Named param_map_const))], []);
    3.46 +    val (props, inst_morph) = if null param_map
    3.47 +      then (raw_props |> map (Morphism.term typ_morph),
    3.48 +        raw_inst_morph $> typ_morph)
    3.49 +      else (raw_props, raw_inst_morph); (*FIXME proper handling in
    3.50 +        locale.ML / expression.ML would be desirable*)
    3.51 +
    3.52 +    (* witness for canonical interpretation *)
    3.53 +    val prop = try the_single props;
    3.54 +    val wit = Option.map (fn prop => let
    3.55 +        val sup_axioms = map_filter (fst o Class.rules thy) sups;
    3.56 +        val loc_intro_tac = case Locale.intros_of thy class
    3.57 +          of (_, NONE) => all_tac
    3.58 +           | (_, SOME intro) => ALLGOALS (Tactic.rtac intro);
    3.59 +        val tac = loc_intro_tac
    3.60 +          THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom))
    3.61 +      in Element.prove_witness empty_ctxt prop tac end) prop;
    3.62 +    val axiom = Option.map Element.conclude_witness wit;
    3.63 +
    3.64 +    (* canonical interpretation *)
    3.65 +    val base_morph = inst_morph
    3.66 +      $> Morphism.binding_morphism (Binding.prefix false (Class.class_prefix class))
    3.67 +      $> Element.satisfy_morphism (the_list wit);
    3.68 +    val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups);
    3.69 +
    3.70 +    (* assm_intro *)
    3.71 +    fun prove_assm_intro thm =
    3.72 +      let
    3.73 +        val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
    3.74 +        val const_eq_morph = case eq_morph
    3.75 +         of SOME eq_morph => const_morph $> eq_morph
    3.76 +          | NONE => const_morph
    3.77 +        val thm'' = Morphism.thm const_eq_morph thm';
    3.78 +        val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
    3.79 +      in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    3.80 +    val assm_intro = Option.map prove_assm_intro
    3.81 +      (fst (Locale.intros_of thy class));
    3.82 +
    3.83 +    (* of_class *)
    3.84 +    val of_class_prop_concl = Logic.mk_of_class (aT, class);
    3.85 +    val of_class_prop = case prop of NONE => of_class_prop_concl
    3.86 +      | SOME prop => Logic.mk_implies (Morphism.term const_morph
    3.87 +          ((map_types o map_atyps) (K aT) prop), of_class_prop_concl);
    3.88 +    val sup_of_classes = map (snd o Class.rules thy) sups;
    3.89 +    val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
    3.90 +    val axclass_intro = #intro (AxClass.get_info thy class);
    3.91 +    val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
    3.92 +    val tac = REPEAT (SOMEGOAL
    3.93 +      (Tactic.match_tac (axclass_intro :: sup_of_classes
    3.94 +         @ loc_axiom_intros @ base_sort_trivs)
    3.95 +           ORELSE' Tactic.assume_tac));
    3.96 +    val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac);
    3.97 +
    3.98 +  in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
    3.99 +
   3.100 +
   3.101 +(* reading and processing class specifications *)
   3.102 +
   3.103 +fun prep_class_elems prep_decl thy sups raw_elems =
   3.104 +  let
   3.105 +
   3.106 +    (* user space type system: only permits 'a type variable, improves towards 'a *)
   3.107 +    val algebra = Sign.classes_of thy;
   3.108 +    val inter_sort = curry (Sorts.inter_sort algebra);
   3.109 +    val proto_base_sort = if null sups then Sign.defaultS thy
   3.110 +      else fold inter_sort (map (Class.base_sort thy) sups) [];
   3.111 +    val base_constraints = (map o apsnd)
   3.112 +      (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
   3.113 +        (Class.these_operations thy sups);
   3.114 +    val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) =>
   3.115 +          if v = Name.aT then T
   3.116 +          else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
   3.117 +      | T => T);
   3.118 +    fun singleton_fixate Ts =
   3.119 +      let
   3.120 +        fun extract f = (fold o fold_atyps) f Ts [];
   3.121 +        val tfrees = extract
   3.122 +          (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
   3.123 +        val inferred_sort = extract
   3.124 +          (fn TVar (_, sort) => inter_sort sort | _ => I);
   3.125 +        val fixate_sort = if null tfrees then inferred_sort
   3.126 +          else case tfrees
   3.127 +           of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
   3.128 +                then inter_sort a_sort inferred_sort
   3.129 +                else error ("Type inference imposes additional sort constraint "
   3.130 +                  ^ Syntax.string_of_sort_global thy inferred_sort
   3.131 +                  ^ " of type parameter " ^ Name.aT ^ " of sort "
   3.132 +                  ^ Syntax.string_of_sort_global thy a_sort ^ ".")
   3.133 +            | _ => error "Multiple type variables in class specification.";
   3.134 +      in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
   3.135 +    fun add_typ_check level name f = Context.proof_map
   3.136 +      (Syntax.add_typ_check level name (fn xs => fn ctxt =>
   3.137 +        let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
   3.138 +
   3.139 +    (* preprocessing elements, retrieving base sort from type-checked elements *)
   3.140 +    val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
   3.141 +      #> Class.redeclare_operations thy sups
   3.142 +      #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
   3.143 +      #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
   3.144 +    val raw_supexpr = (map (fn sup => (sup, (("", false),
   3.145 +      Expression.Positional []))) sups, []);
   3.146 +    val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy
   3.147 +      |> prep_decl raw_supexpr init_class_body raw_elems;
   3.148 +    fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
   3.149 +      | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
   3.150 +      | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
   3.151 +          fold_types f t #> (fold o fold_types) f ts) o snd) assms
   3.152 +      | fold_element_types f (Element.Defines _) =
   3.153 +          error ("\"defines\" element not allowed in class specification.")
   3.154 +      | fold_element_types f (Element.Notes _) =
   3.155 +          error ("\"notes\" element not allowed in class specification.");
   3.156 +    val base_sort = if null inferred_elems then proto_base_sort else
   3.157 +      case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
   3.158 +       of [] => error "No type variable in class specification"
   3.159 +        | [(_, sort)] => sort
   3.160 +        | _ => error "Multiple type variables in class specification";
   3.161 +    val supparams = map (fn ((c, T), _) =>
   3.162 +      (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams;
   3.163 +    val supparam_names = map fst supparams;
   3.164 +    fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c);
   3.165 +    val supexpr = (map (fn sup => (sup, (("", false),
   3.166 +      Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups,
   3.167 +        map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams);
   3.168 +
   3.169 +  in (base_sort, supparam_names, supexpr, inferred_elems) end;
   3.170 +
   3.171 +val cert_class_elems = prep_class_elems Expression.cert_declaration;
   3.172 +val read_class_elems = prep_class_elems Expression.cert_read_declaration;
   3.173 +
   3.174 +fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems =
   3.175 +  let
   3.176 +
   3.177 +    (* prepare import *)
   3.178 +    val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
   3.179 +    val sups = map (prep_class thy) raw_supclasses
   3.180 +      |> Sign.minimize_sort thy;
   3.181 +    val _ = case filter_out (Class.is_class thy) sups
   3.182 +     of [] => ()
   3.183 +      | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
   3.184 +    val raw_supparams = (map o apsnd) (snd o snd) (Class.these_params thy sups);
   3.185 +    val raw_supparam_names = map fst raw_supparams;
   3.186 +    val _ = if has_duplicates (op =) raw_supparam_names
   3.187 +      then error ("Duplicate parameter(s) in superclasses: "
   3.188 +        ^ (commas o map quote o duplicates (op =)) raw_supparam_names)
   3.189 +      else ();
   3.190 +
   3.191 +    (* infer types and base sort *)
   3.192 +    val (base_sort, supparam_names, supexpr, inferred_elems) =
   3.193 +      prep_class_elems thy sups raw_elems;
   3.194 +    val sup_sort = inter_sort base_sort sups;
   3.195 +
   3.196 +    (* process elements as class specification *)
   3.197 +    val class_ctxt = Class.begin sups base_sort (ProofContext.init_global thy);
   3.198 +    val ((_, _, syntax_elems), _) = class_ctxt
   3.199 +      |> Expression.cert_declaration supexpr I inferred_elems;
   3.200 +    fun check_vars e vs = if null vs
   3.201 +      then error ("No type variable in part of specification element "
   3.202 +        ^ (Pretty.string_of o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
   3.203 +      else ();
   3.204 +    fun check_element (e as Element.Fixes fxs) =
   3.205 +          map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs
   3.206 +      | check_element (e as Element.Assumes assms) =
   3.207 +          maps (fn (_, ts_pss) => map
   3.208 +            (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms
   3.209 +      | check_element e = [()];
   3.210 +    val _ = map check_element syntax_elems;
   3.211 +    fun fork_syn (Element.Fixes xs) =
   3.212 +          fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
   3.213 +          #>> Element.Fixes
   3.214 +      | fork_syn x = pair x;
   3.215 +    val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
   3.216 +
   3.217 +  in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end;
   3.218 +
   3.219 +val cert_class_spec = prep_class_spec (K I) cert_class_elems;
   3.220 +val read_class_spec = prep_class_spec Sign.intern_class read_class_elems;
   3.221 +
   3.222 +
   3.223 +(* class establishment *)
   3.224 +
   3.225 +fun add_consts class base_sort sups supparam_names global_syntax thy =
   3.226 +  let
   3.227 +    (*FIXME simplify*)
   3.228 +    val supconsts = supparam_names
   3.229 +      |> AList.make (snd o the o AList.lookup (op =) (Class.these_params thy sups))
   3.230 +      |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
   3.231 +    val all_params = Locale.params_of thy class;
   3.232 +    val raw_params = (snd o chop (length supparam_names)) all_params;
   3.233 +    fun add_const ((raw_c, raw_ty), _) thy =
   3.234 +      let
   3.235 +        val b = Binding.name raw_c;
   3.236 +        val c = Sign.full_name thy b;
   3.237 +        val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
   3.238 +        val ty0 = Type.strip_sorts ty;
   3.239 +        val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
   3.240 +        val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
   3.241 +      in
   3.242 +        thy
   3.243 +        |> Sign.declare_const ((b, ty0), syn)
   3.244 +        |> snd
   3.245 +        |> pair ((Name.of_binding b, ty), (c, ty'))
   3.246 +      end;
   3.247 +  in
   3.248 +    thy
   3.249 +    |> Sign.add_path (Class.class_prefix class)
   3.250 +    |> fold_map add_const raw_params
   3.251 +    ||> Sign.restore_naming thy
   3.252 +    |-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
   3.253 +  end;
   3.254 +
   3.255 +fun adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax thy =
   3.256 +  let
   3.257 +    (*FIXME simplify*)
   3.258 +    fun globalize param_map = map_aterms
   3.259 +      (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
   3.260 +        | t => t);
   3.261 +    val raw_pred = Locale.intros_of thy class
   3.262 +      |> fst
   3.263 +      |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of);
   3.264 +    fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
   3.265 +     of [] => NONE
   3.266 +      | [thm] => SOME thm;
   3.267 +  in
   3.268 +    thy
   3.269 +    |> add_consts class base_sort sups supparam_names global_syntax
   3.270 +    |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
   3.271 +          (map (fst o snd) params)
   3.272 +          [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
   3.273 +    #> snd
   3.274 +    #> `get_axiom
   3.275 +    #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
   3.276 +    #> pair (param_map, params, assm_axiom)))
   3.277 +  end;
   3.278 +
   3.279 +fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
   3.280 +  let
   3.281 +    val class = Sign.full_name thy b;
   3.282 +    val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
   3.283 +      prep_class_spec thy raw_supclasses raw_elems;
   3.284 +  in
   3.285 +    thy
   3.286 +    |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems
   3.287 +    |> snd |> Local_Theory.exit_global
   3.288 +    |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
   3.289 +    ||> Theory.checkpoint
   3.290 +    |-> (fn (param_map, params, assm_axiom) =>
   3.291 +       `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
   3.292 +    #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
   3.293 +       Context.theory_map (Locale.add_registration (class, base_morph)
   3.294 +         (Option.map (rpair true) eq_morph) export_morph)
   3.295 +    #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
   3.296 +    |> Named_Target.init (SOME class)
   3.297 +    |> pair class
   3.298 +  end;
   3.299 +
   3.300 +in
   3.301 +
   3.302 +val class = gen_class cert_class_spec;
   3.303 +val class_cmd = gen_class read_class_spec;
   3.304 +
   3.305 +end; (*local*)
   3.306 +
   3.307 +
   3.308 +(** subclass relations **)
   3.309 +
   3.310 +local
   3.311 +
   3.312 +fun gen_subclass prep_class do_proof raw_sup lthy =
   3.313 +  let
   3.314 +    val thy = ProofContext.theory_of lthy;
   3.315 +    val proto_sup = prep_class thy raw_sup;
   3.316 +    val proto_sub = case Named_Target.peek lthy
   3.317 +     of {is_class = false, ...} => error "Not in a class context"
   3.318 +      | {target, ...} => target;
   3.319 +    val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
   3.320 +
   3.321 +    val expr = ([(sup, (("", false), Expression.Positional []))], []);
   3.322 +    val (([props], deps, export), goal_ctxt) =
   3.323 +      Expression.cert_goal_expression expr lthy;
   3.324 +    val some_prop = try the_single props;
   3.325 +    val some_dep_morph = try the_single (map snd deps);
   3.326 +    fun after_qed some_wit =
   3.327 +      ProofContext.theory (Class.register_subclass (sub, sup)
   3.328 +        some_dep_morph some_wit export)
   3.329 +      #> ProofContext.theory_of #> Named_Target.init (SOME sub);
   3.330 +  in do_proof after_qed some_prop goal_ctxt end;
   3.331 +
   3.332 +fun user_proof after_qed some_prop =
   3.333 +  Element.witness_proof (after_qed o try the_single o the_single)
   3.334 +    [the_list some_prop];
   3.335 +
   3.336 +fun tactic_proof tac after_qed some_prop ctxt =
   3.337 +  after_qed (Option.map
   3.338 +    (fn prop => Element.prove_witness ctxt prop tac) some_prop) ctxt;
   3.339 +
   3.340 +in
   3.341 +
   3.342 +val subclass = gen_subclass (K I) user_proof;
   3.343 +fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
   3.344 +val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof;
   3.345 +
   3.346 +end; (*local*)
   3.347 +
   3.348 +end;
     4.1 --- a/src/Pure/Isar/class_target.ML	Wed Aug 11 18:44:06 2010 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,659 +0,0 @@
     4.4 -(*  Title:      Pure/Isar/class_target.ML
     4.5 -    Author:     Florian Haftmann, TU Muenchen
     4.6 -
     4.7 -Type classes derived from primitive axclasses and locales -- mechanisms.
     4.8 -*)
     4.9 -
    4.10 -signature CLASS_TARGET =
    4.11 -sig
    4.12 -  (*classes*)
    4.13 -  val register: class -> class list -> ((string * typ) * (string * typ)) list
    4.14 -    -> sort -> morphism -> morphism -> thm option -> thm option -> thm
    4.15 -    -> theory -> theory
    4.16 -
    4.17 -  val is_class: theory -> class -> bool
    4.18 -  val base_sort: theory -> class -> sort
    4.19 -  val rules: theory -> class -> thm option * thm
    4.20 -  val these_params: theory -> sort -> (string * (class * (string * typ))) list
    4.21 -  val these_defs: theory -> sort -> thm list
    4.22 -  val these_operations: theory -> sort
    4.23 -    -> (string * (class * (typ * term))) list
    4.24 -  val print_classes: theory -> unit
    4.25 -
    4.26 -  val begin: class list -> sort -> Proof.context -> Proof.context
    4.27 -  val init: class -> theory -> Proof.context
    4.28 -  val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory
    4.29 -  val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
    4.30 -  val class_prefix: string -> string
    4.31 -  val refresh_syntax: class -> Proof.context -> Proof.context
    4.32 -  val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
    4.33 -
    4.34 -  (*instances*)
    4.35 -  val init_instantiation: string list * (string * sort) list * sort
    4.36 -    -> theory -> Proof.context
    4.37 -  val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
    4.38 -  val instantiation_instance: (local_theory -> local_theory)
    4.39 -    -> local_theory -> Proof.state
    4.40 -  val prove_instantiation_instance: (Proof.context -> tactic)
    4.41 -    -> local_theory -> local_theory
    4.42 -  val prove_instantiation_exit: (Proof.context -> tactic)
    4.43 -    -> local_theory -> theory
    4.44 -  val prove_instantiation_exit_result: (morphism -> 'a -> 'b)
    4.45 -    -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
    4.46 -  val conclude_instantiation: local_theory -> local_theory
    4.47 -  val instantiation_param: local_theory -> binding -> string option
    4.48 -  val confirm_declaration: binding -> local_theory -> local_theory
    4.49 -  val pretty_instantiation: local_theory -> Pretty.T
    4.50 -  val read_multi_arity: theory -> xstring list * xstring list * xstring
    4.51 -    -> string list * (string * sort) list * sort
    4.52 -  val type_name: string -> string
    4.53 -  val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
    4.54 -  val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
    4.55 -
    4.56 -  (*subclasses*)
    4.57 -  val register_subclass: class * class -> morphism option -> Element.witness option
    4.58 -    -> morphism -> theory -> theory
    4.59 -  val classrel: class * class -> theory -> Proof.state
    4.60 -  val classrel_cmd: xstring * xstring -> theory -> Proof.state
    4.61 -
    4.62 -  (*tactics*)
    4.63 -  val intro_classes_tac: thm list -> tactic
    4.64 -  val default_intro_tac: Proof.context -> thm list -> tactic
    4.65 -end;
    4.66 -
    4.67 -structure Class_Target : CLASS_TARGET =
    4.68 -struct
    4.69 -
    4.70 -(** class data **)
    4.71 -
    4.72 -datatype class_data = ClassData of {
    4.73 -
    4.74 -  (* static part *)
    4.75 -  consts: (string * string) list
    4.76 -    (*locale parameter ~> constant name*),
    4.77 -  base_sort: sort,
    4.78 -  base_morph: morphism
    4.79 -    (*static part of canonical morphism*),
    4.80 -  export_morph: morphism,
    4.81 -  assm_intro: thm option,
    4.82 -  of_class: thm,
    4.83 -  axiom: thm option,
    4.84 -  
    4.85 -  (* dynamic part *)
    4.86 -  defs: thm list,
    4.87 -  operations: (string * (class * (typ * term))) list
    4.88 -
    4.89 -};
    4.90 -
    4.91 -fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
    4.92 -    (defs, operations)) =
    4.93 -  ClassData { consts = consts, base_sort = base_sort,
    4.94 -    base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
    4.95 -    of_class = of_class, axiom = axiom, defs = defs, operations = operations };
    4.96 -fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro,
    4.97 -    of_class, axiom, defs, operations }) =
    4.98 -  make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
    4.99 -    (defs, operations)));
   4.100 -fun merge_class_data _ (ClassData { consts = consts,
   4.101 -    base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
   4.102 -    of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
   4.103 -  ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
   4.104 -    of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
   4.105 -  make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
   4.106 -    (Thm.merge_thms (defs1, defs2),
   4.107 -      AList.merge (op =) (K true) (operations1, operations2)));
   4.108 -
   4.109 -structure ClassData = Theory_Data
   4.110 -(
   4.111 -  type T = class_data Graph.T
   4.112 -  val empty = Graph.empty;
   4.113 -  val extend = I;
   4.114 -  val merge = Graph.join merge_class_data;
   4.115 -);
   4.116 -
   4.117 -
   4.118 -(* queries *)
   4.119 -
   4.120 -fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class
   4.121 - of SOME (ClassData data) => SOME data
   4.122 -  | NONE => NONE;
   4.123 -
   4.124 -fun the_class_data thy class = case lookup_class_data thy class
   4.125 - of NONE => error ("Undeclared class " ^ quote class)
   4.126 -  | SOME data => data;
   4.127 -
   4.128 -val is_class = is_some oo lookup_class_data;
   4.129 -
   4.130 -val ancestry = Graph.all_succs o ClassData.get;
   4.131 -val heritage = Graph.all_preds o ClassData.get;
   4.132 -
   4.133 -fun these_params thy =
   4.134 -  let
   4.135 -    fun params class =
   4.136 -      let
   4.137 -        val const_typs = (#params o AxClass.get_info thy) class;
   4.138 -        val const_names = (#consts o the_class_data thy) class;
   4.139 -      in
   4.140 -        (map o apsnd)
   4.141 -          (fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names
   4.142 -      end;
   4.143 -  in maps params o ancestry thy end;
   4.144 -
   4.145 -val base_sort = #base_sort oo the_class_data;
   4.146 -
   4.147 -fun rules thy class =
   4.148 -  let val { axiom, of_class, ... } = the_class_data thy class
   4.149 -  in (axiom, of_class) end;
   4.150 -
   4.151 -fun all_assm_intros thy =
   4.152 -  Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm)
   4.153 -    (the_list assm_intro)) (ClassData.get thy) [];
   4.154 -
   4.155 -fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
   4.156 -fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
   4.157 -
   4.158 -val base_morphism = #base_morph oo the_class_data;
   4.159 -fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class])
   4.160 - of SOME eq_morph => base_morphism thy class $> eq_morph
   4.161 -  | NONE => base_morphism thy class;
   4.162 -val export_morphism = #export_morph oo the_class_data;
   4.163 -
   4.164 -fun print_classes thy =
   4.165 -  let
   4.166 -    val ctxt = ProofContext.init_global thy;
   4.167 -    val algebra = Sign.classes_of thy;
   4.168 -    val arities =
   4.169 -      Symtab.empty
   4.170 -      |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
   4.171 -           Symtab.map_default (class, []) (insert (op =) tyco)) arities)
   4.172 -             (Sorts.arities_of algebra);
   4.173 -    val the_arities = these o Symtab.lookup arities;
   4.174 -    fun mk_arity class tyco =
   4.175 -      let
   4.176 -        val Ss = Sorts.mg_domain algebra tyco [class];
   4.177 -      in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
   4.178 -    fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
   4.179 -      ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
   4.180 -    fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   4.181 -      (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
   4.182 -      (SOME o Pretty.block) [Pretty.str "supersort: ",
   4.183 -        (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
   4.184 -      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
   4.185 -          (Pretty.str "parameters:" :: ps)) o map mk_param
   4.186 -        o these o Option.map #params o try (AxClass.get_info thy)) class,
   4.187 -      (SOME o Pretty.block o Pretty.breaks) [
   4.188 -        Pretty.str "instances:",
   4.189 -        Pretty.list "" "" (map (mk_arity class) (the_arities class))
   4.190 -      ]
   4.191 -    ]
   4.192 -  in
   4.193 -    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "")
   4.194 -      o map mk_entry o Sorts.all_classes) algebra
   4.195 -  end;
   4.196 -
   4.197 -
   4.198 -(* updaters *)
   4.199 -
   4.200 -fun register class sups params base_sort base_morph export_morph
   4.201 -    axiom assm_intro of_class thy =
   4.202 -  let
   4.203 -    val operations = map (fn (v_ty as (_, ty), (c, _)) =>
   4.204 -      (c, (class, (ty, Free v_ty)))) params;
   4.205 -    val add_class = Graph.new_node (class,
   4.206 -        make_class_data (((map o pairself) fst params, base_sort,
   4.207 -          base_morph, export_morph, assm_intro, of_class, axiom), ([], operations)))
   4.208 -      #> fold (curry Graph.add_edge class) sups;
   4.209 -  in ClassData.map add_class thy end;
   4.210 -
   4.211 -fun activate_defs class thms thy = case Element.eq_morphism thy thms
   4.212 - of SOME eq_morph => fold (fn cls => fn thy =>
   4.213 -      Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
   4.214 -        (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
   4.215 -  | NONE => thy;
   4.216 -
   4.217 -fun register_operation class (c, (t, some_def)) thy =
   4.218 -  let
   4.219 -    val base_sort = base_sort thy class;
   4.220 -    val prep_typ = map_type_tfree
   4.221 -      (fn (v, sort) => if Name.aT = v
   4.222 -        then TFree (v, base_sort) else TVar ((v, 0), sort));
   4.223 -    val t' = map_types prep_typ t;
   4.224 -    val ty' = Term.fastype_of t';
   4.225 -  in
   4.226 -    thy
   4.227 -    |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
   4.228 -      (fn (defs, operations) =>
   4.229 -        (fold cons (the_list some_def) defs,
   4.230 -          (c, (class, (ty', t'))) :: operations))
   4.231 -    |> activate_defs class (the_list some_def)
   4.232 -  end;
   4.233 -
   4.234 -fun register_subclass (sub, sup) some_dep_morph some_wit export thy =
   4.235 -  let
   4.236 -    val intros = (snd o rules thy) sup :: map_filter I
   4.237 -      [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit,
   4.238 -        (fst o rules thy) sub];
   4.239 -    val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
   4.240 -    val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
   4.241 -      (K tac);
   4.242 -    val diff_sort = Sign.complete_sort thy [sup]
   4.243 -      |> subtract (op =) (Sign.complete_sort thy [sub])
   4.244 -      |> filter (is_class thy);
   4.245 -    val add_dependency = case some_dep_morph
   4.246 -     of SOME dep_morph => Locale.add_dependency sub
   4.247 -          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export
   4.248 -      | NONE => I
   4.249 -  in
   4.250 -    thy
   4.251 -    |> AxClass.add_classrel classrel
   4.252 -    |> ClassData.map (Graph.add_edge (sub, sup))
   4.253 -    |> activate_defs sub (these_defs thy diff_sort)
   4.254 -    |> add_dependency
   4.255 -  end;
   4.256 -
   4.257 -
   4.258 -(** classes and class target **)
   4.259 -
   4.260 -(* class context syntax *)
   4.261 -
   4.262 -fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
   4.263 -  o these_operations thy;
   4.264 -
   4.265 -fun redeclare_const thy c =
   4.266 -  let val b = Long_Name.base_name c
   4.267 -  in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
   4.268 -
   4.269 -fun synchronize_class_syntax sort base_sort ctxt =
   4.270 -  let
   4.271 -    val thy = ProofContext.theory_of ctxt;
   4.272 -    val algebra = Sign.classes_of thy;
   4.273 -    val operations = these_operations thy sort;
   4.274 -    fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
   4.275 -    val primary_constraints =
   4.276 -      (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
   4.277 -    val secondary_constraints =
   4.278 -      (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
   4.279 -    fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
   4.280 -     of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
   4.281 -         of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
   4.282 -             of SOME (_, ty' as TVar (vi, sort)) =>
   4.283 -                  if Type_Infer.is_param vi
   4.284 -                    andalso Sorts.sort_le algebra (base_sort, sort)
   4.285 -                      then SOME (ty', TFree (Name.aT, base_sort))
   4.286 -                      else NONE
   4.287 -              | _ => NONE)
   4.288 -          | NONE => NONE)
   4.289 -      | NONE => NONE)
   4.290 -    fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c);
   4.291 -    val unchecks = these_unchecks thy sort;
   4.292 -  in
   4.293 -    ctxt
   4.294 -    |> fold (redeclare_const thy o fst) primary_constraints
   4.295 -    |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
   4.296 -        (((improve, subst), true), unchecks)), false))
   4.297 -    |> Overloading.set_primary_constraints
   4.298 -  end;
   4.299 -
   4.300 -fun refresh_syntax class ctxt =
   4.301 -  let
   4.302 -    val thy = ProofContext.theory_of ctxt;
   4.303 -    val base_sort = base_sort thy class;
   4.304 -  in synchronize_class_syntax [class] base_sort ctxt end;
   4.305 -
   4.306 -fun redeclare_operations thy sort =
   4.307 -  fold (redeclare_const thy o fst) (these_operations thy sort);
   4.308 -
   4.309 -fun begin sort base_sort ctxt =
   4.310 -  ctxt
   4.311 -  |> Variable.declare_term
   4.312 -      (Logic.mk_type (TFree (Name.aT, base_sort)))
   4.313 -  |> synchronize_class_syntax sort base_sort
   4.314 -  |> Overloading.add_improvable_syntax;
   4.315 -
   4.316 -fun init class thy =
   4.317 -  thy
   4.318 -  |> Locale.init class
   4.319 -  |> begin [class] (base_sort thy class);
   4.320 -
   4.321 -
   4.322 -(* class target *)
   4.323 -
   4.324 -val class_prefix = Logic.const_of_class o Long_Name.base_name;
   4.325 -
   4.326 -fun declare class ((c, mx), (type_params, dict)) thy =
   4.327 -  let
   4.328 -    val morph = morphism thy class;
   4.329 -    val b = Morphism.binding morph c;
   4.330 -    val b_def = Morphism.binding morph (Binding.suffix_name "_dict" b);
   4.331 -    val c' = Sign.full_name thy b;
   4.332 -    val dict' = Morphism.term morph dict;
   4.333 -    val ty' = map Term.fastype_of type_params ---> Term.fastype_of dict';
   4.334 -    val def_eq = Logic.mk_equals (list_comb (Const (c', ty'), type_params), dict')
   4.335 -      |> map_types Type.strip_sorts;
   4.336 -  in
   4.337 -    thy
   4.338 -    |> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
   4.339 -    |> snd
   4.340 -    |> Thm.add_def false false (b_def, def_eq)
   4.341 -    |>> apsnd Thm.varifyT_global
   4.342 -    |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm)
   4.343 -      #> snd
   4.344 -      #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
   4.345 -    |> Sign.add_const_constraint (c', SOME ty')
   4.346 -  end;
   4.347 -
   4.348 -fun abbrev class prmode ((c, mx), rhs) thy =
   4.349 -  let
   4.350 -    val morph = morphism thy class;
   4.351 -    val unchecks = these_unchecks thy [class];
   4.352 -    val b = Morphism.binding morph c;
   4.353 -    val c' = Sign.full_name thy b;
   4.354 -    val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
   4.355 -    val ty' = Term.fastype_of rhs';
   4.356 -    val rhs'' = map_types Logic.varifyT_global rhs';
   4.357 -  in
   4.358 -    thy
   4.359 -    |> Sign.add_abbrev (#1 prmode) (b, rhs'')
   4.360 -    |> snd
   4.361 -    |> Sign.add_const_constraint (c', SOME ty')
   4.362 -    |> Sign.notation true prmode [(Const (c', ty'), mx)]
   4.363 -    |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE))
   4.364 -  end;
   4.365 -
   4.366 -
   4.367 -(* simple subclasses *)
   4.368 -
   4.369 -local
   4.370 -
   4.371 -fun gen_classrel mk_prop classrel thy =
   4.372 -  let
   4.373 -    fun after_qed results =
   4.374 -      ProofContext.theory ((fold o fold) AxClass.add_classrel results);
   4.375 -  in
   4.376 -    thy
   4.377 -    |> ProofContext.init_global
   4.378 -    |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
   4.379 -  end;
   4.380 -
   4.381 -in
   4.382 -
   4.383 -val classrel =
   4.384 -  gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel);
   4.385 -val classrel_cmd =
   4.386 -  gen_classrel (Logic.mk_classrel oo AxClass.read_classrel);
   4.387 -
   4.388 -end; (*local*)
   4.389 -
   4.390 -
   4.391 -(** instantiation target **)
   4.392 -
   4.393 -(* bookkeeping *)
   4.394 -
   4.395 -datatype instantiation = Instantiation of {
   4.396 -  arities: string list * (string * sort) list * sort,
   4.397 -  params: ((string * string) * (string * typ)) list
   4.398 -    (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
   4.399 -}
   4.400 -
   4.401 -structure Instantiation = Proof_Data
   4.402 -(
   4.403 -  type T = instantiation
   4.404 -  fun init _ = Instantiation { arities = ([], [], []), params = [] };
   4.405 -);
   4.406 -
   4.407 -fun mk_instantiation (arities, params) =
   4.408 -  Instantiation { arities = arities, params = params };
   4.409 -fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy)
   4.410 - of Instantiation data => data;
   4.411 -fun map_instantiation f = (Local_Theory.target o Instantiation.map)
   4.412 -  (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
   4.413 -
   4.414 -fun the_instantiation lthy = case get_instantiation lthy
   4.415 - of { arities = ([], [], []), ... } => error "No instantiation target"
   4.416 -  | data => data;
   4.417 -
   4.418 -val instantiation_params = #params o get_instantiation;
   4.419 -
   4.420 -fun instantiation_param lthy b = instantiation_params lthy
   4.421 -  |> find_first (fn (_, (v, _)) => Binding.name_of b = v)
   4.422 -  |> Option.map (fst o fst);
   4.423 -
   4.424 -fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
   4.425 -  let
   4.426 -    val ctxt = ProofContext.init_global thy;
   4.427 -    val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
   4.428 -      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
   4.429 -    val tycos = map #1 all_arities;
   4.430 -    val (_, sorts, sort) = hd all_arities;
   4.431 -    val vs = Name.names Name.context Name.aT sorts;
   4.432 -  in (tycos, vs, sort) end;
   4.433 -
   4.434 -
   4.435 -(* syntax *)
   4.436 -
   4.437 -fun synchronize_inst_syntax ctxt =
   4.438 -  let
   4.439 -    val Instantiation { params, ... } = Instantiation.get ctxt;
   4.440 -
   4.441 -    val lookup_inst_param = AxClass.lookup_inst_param
   4.442 -      (Sign.consts_of (ProofContext.theory_of ctxt)) params;
   4.443 -    fun subst (c, ty) = case lookup_inst_param (c, ty)
   4.444 -     of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
   4.445 -      | NONE => NONE;
   4.446 -    val unchecks =
   4.447 -      map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
   4.448 -  in
   4.449 -    ctxt
   4.450 -    |> Overloading.map_improvable_syntax
   4.451 -         (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
   4.452 -            (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
   4.453 -  end;
   4.454 -
   4.455 -
   4.456 -(* target *)
   4.457 -
   4.458 -val sanitize_name = (*necessary as long as "dirty" type identifiers are permitted*)
   4.459 -  let
   4.460 -    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
   4.461 -      orelse s = "'" orelse s = "_";
   4.462 -    val is_junk = not o is_valid andf Symbol.is_regular;
   4.463 -    val junk = Scan.many is_junk;
   4.464 -    val scan_valids = Symbol.scanner "Malformed input"
   4.465 -      ((junk |--
   4.466 -        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
   4.467 -        --| junk))
   4.468 -      ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
   4.469 -  in
   4.470 -    explode #> scan_valids #> implode
   4.471 -  end;
   4.472 -
   4.473 -val type_name = sanitize_name o Long_Name.base_name;
   4.474 -
   4.475 -fun resort_terms pp algebra consts constraints ts =
   4.476 -  let
   4.477 -    fun matchings (Const (c_ty as (c, _))) = (case constraints c
   4.478 -         of NONE => I
   4.479 -          | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
   4.480 -              (Consts.typargs consts c_ty) sorts)
   4.481 -      | matchings _ = I
   4.482 -    val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
   4.483 -      handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
   4.484 -    val inst = map_type_tvar
   4.485 -      (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
   4.486 -  in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
   4.487 -
   4.488 -fun init_instantiation (tycos, vs, sort) thy =
   4.489 -  let
   4.490 -    val _ = if null tycos then error "At least one arity must be given" else ();
   4.491 -    val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
   4.492 -    fun get_param tyco (param, (_, (c, ty))) =
   4.493 -      if can (AxClass.param_of_inst thy) (c, tyco)
   4.494 -      then NONE else SOME ((c, tyco),
   4.495 -        (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
   4.496 -    val params = map_product get_param tycos class_params |> map_filter I;
   4.497 -    val primary_constraints = map (apsnd
   4.498 -      (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
   4.499 -    val pp = Syntax.pp_global thy;
   4.500 -    val algebra = Sign.classes_of thy
   4.501 -      |> fold (fn tyco => Sorts.add_arities pp
   4.502 -            (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
   4.503 -    val consts = Sign.consts_of thy;
   4.504 -    val improve_constraints = AList.lookup (op =)
   4.505 -      (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
   4.506 -    fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts
   4.507 -     of NONE => NONE
   4.508 -      | SOME ts' => SOME (ts', ctxt);
   4.509 -    val lookup_inst_param = AxClass.lookup_inst_param consts params;
   4.510 -    val typ_instance = Type.typ_instance (Sign.tsig_of thy);
   4.511 -    fun improve (c, ty) = case lookup_inst_param (c, ty)
   4.512 -     of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE
   4.513 -      | NONE => NONE;
   4.514 -  in
   4.515 -    thy
   4.516 -    |> Theory.checkpoint
   4.517 -    |> ProofContext.init_global
   4.518 -    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
   4.519 -    |> fold (Variable.declare_typ o TFree) vs
   4.520 -    |> fold (Variable.declare_names o Free o snd) params
   4.521 -    |> (Overloading.map_improvable_syntax o apfst)
   4.522 -         (K ((primary_constraints, []), (((improve, K NONE), false), [])))
   4.523 -    |> Overloading.add_improvable_syntax
   4.524 -    |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
   4.525 -    |> synchronize_inst_syntax
   4.526 -  end;
   4.527 -
   4.528 -fun confirm_declaration b = (map_instantiation o apsnd)
   4.529 -  (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
   4.530 -  #> Local_Theory.target synchronize_inst_syntax
   4.531 -
   4.532 -fun gen_instantiation_instance do_proof after_qed lthy =
   4.533 -  let
   4.534 -    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
   4.535 -    val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
   4.536 -    fun after_qed' results =
   4.537 -      Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
   4.538 -      #> after_qed;
   4.539 -  in
   4.540 -    lthy
   4.541 -    |> do_proof after_qed' arities_proof
   4.542 -  end;
   4.543 -
   4.544 -val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
   4.545 -  Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
   4.546 -
   4.547 -fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
   4.548 -  fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
   4.549 -    (fn {context, ...} => tac context)) ts) lthy) I;
   4.550 -
   4.551 -fun prove_instantiation_exit tac = prove_instantiation_instance tac
   4.552 -  #> Local_Theory.exit_global;
   4.553 -
   4.554 -fun prove_instantiation_exit_result f tac x lthy =
   4.555 -  let
   4.556 -    val morph = ProofContext.export_morphism lthy
   4.557 -      (ProofContext.init_global (ProofContext.theory_of lthy));
   4.558 -    val y = f morph x;
   4.559 -  in
   4.560 -    lthy
   4.561 -    |> prove_instantiation_exit (fn ctxt => tac ctxt y)
   4.562 -    |> pair y
   4.563 -  end;
   4.564 -
   4.565 -fun conclude_instantiation lthy =
   4.566 -  let
   4.567 -    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
   4.568 -    val thy = ProofContext.theory_of lthy;
   4.569 -    val _ = map (fn tyco => if Sign.of_sort thy
   4.570 -        (Type (tyco, map TFree vs), sort)
   4.571 -      then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
   4.572 -        tycos;
   4.573 -  in lthy end;
   4.574 -
   4.575 -fun pretty_instantiation lthy =
   4.576 -  let
   4.577 -    val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
   4.578 -    val thy = ProofContext.theory_of lthy;
   4.579 -    fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
   4.580 -    fun pr_param ((c, _), (v, ty)) =
   4.581 -      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
   4.582 -        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
   4.583 -  in
   4.584 -    (Pretty.block o Pretty.fbreaks)
   4.585 -      (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
   4.586 -  end;
   4.587 -
   4.588 -fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
   4.589 -
   4.590 -fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   4.591 -  case instantiation_param lthy b
   4.592 -   of SOME c => if mx <> NoSyn then syntax_error c
   4.593 -        else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
   4.594 -            ##>> AxClass.define_overloaded b_def (c, rhs))
   4.595 -          ||> confirm_declaration b
   4.596 -    | NONE => lthy |>
   4.597 -        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
   4.598 -
   4.599 -fun instantiation arities thy =
   4.600 -  thy
   4.601 -  |> init_instantiation arities
   4.602 -  |> Local_Theory.init NONE ""
   4.603 -     {define = Generic_Target.define instantiation_foundation,
   4.604 -      notes = Generic_Target.notes
   4.605 -        (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
   4.606 -      abbrev = Generic_Target.abbrev
   4.607 -        (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
   4.608 -      declaration = K Generic_Target.theory_declaration,
   4.609 -      syntax_declaration = K Generic_Target.theory_declaration,
   4.610 -      pretty = single o pretty_instantiation,
   4.611 -      reinit = instantiation arities o ProofContext.theory_of,
   4.612 -      exit = Local_Theory.target_of o conclude_instantiation};
   4.613 -
   4.614 -fun instantiation_cmd arities thy =
   4.615 -  instantiation (read_multi_arity thy arities) thy;
   4.616 -
   4.617 -
   4.618 -(* simplified instantiation interface with no class parameter *)
   4.619 -
   4.620 -fun instance_arity_cmd raw_arities thy =
   4.621 -  let
   4.622 -    val (tycos, vs, sort) = read_multi_arity thy raw_arities;
   4.623 -    val sorts = map snd vs;
   4.624 -    val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
   4.625 -    fun after_qed results = ProofContext.theory
   4.626 -      ((fold o fold) AxClass.add_arity results);
   4.627 -  in
   4.628 -    thy
   4.629 -    |> ProofContext.init_global
   4.630 -    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
   4.631 -  end;
   4.632 -
   4.633 -
   4.634 -(** tactics and methods **)
   4.635 -
   4.636 -fun intro_classes_tac facts st =
   4.637 -  let
   4.638 -    val thy = Thm.theory_of_thm st;
   4.639 -    val classes = Sign.all_classes thy;
   4.640 -    val class_trivs = map (Thm.class_triv thy) classes;
   4.641 -    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   4.642 -    val assm_intros = all_assm_intros thy;
   4.643 -  in
   4.644 -    Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
   4.645 -  end;
   4.646 -
   4.647 -fun default_intro_tac ctxt [] =
   4.648 -      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
   4.649 -  | default_intro_tac _ _ = no_tac;
   4.650 -
   4.651 -fun default_tac rules ctxt facts =
   4.652 -  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   4.653 -    default_intro_tac ctxt facts;
   4.654 -
   4.655 -val _ = Context.>> (Context.map_theory
   4.656 - (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
   4.657 -    "back-chain introduction rules of classes" #>
   4.658 -  Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
   4.659 -    "apply some intro/elim rule"));
   4.660 -
   4.661 -end;
   4.662 -
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 11 18:44:06 2010 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 11 20:25:44 2010 +0200
     5.3 @@ -462,11 +462,11 @@
     5.4     (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
     5.5      >> (fn ((name, (supclasses, elems)), begin) =>
     5.6          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
     5.7 -          (Class.class_cmd name supclasses elems #> snd)));
     5.8 +          (Class_Declaration.class_cmd name supclasses elems #> snd)));
     5.9  
    5.10  val _ =
    5.11    Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
    5.12 -    (Parse.xname >> Class.subclass_cmd);
    5.13 +    (Parse.xname >> Class_Declaration.subclass_cmd);
    5.14  
    5.15  val _ =
    5.16    Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
     6.1 --- a/src/Pure/Isar/local_theory.ML	Wed Aug 11 18:44:06 2010 +0200
     6.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Aug 11 20:25:44 2010 +0200
     6.3 @@ -50,7 +50,6 @@
     6.4    val const_alias: binding -> string -> local_theory -> local_theory
     6.5    val init: serial option -> string -> operations -> Proof.context -> local_theory
     6.6    val restore: local_theory -> local_theory
     6.7 -  val reinit: local_theory -> local_theory
     6.8    val exit: local_theory -> Proof.context
     6.9    val exit_global: local_theory -> theory
    6.10    val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
    6.11 @@ -75,7 +74,6 @@
    6.12    declaration: bool -> declaration -> local_theory -> local_theory,
    6.13    syntax_declaration: bool -> declaration -> local_theory -> local_theory,
    6.14    pretty: local_theory -> Pretty.T list,
    6.15 -  reinit: local_theory -> local_theory,
    6.16    exit: local_theory -> Proof.context};
    6.17  
    6.18  datatype lthy = LThy of
    6.19 @@ -260,8 +258,6 @@
    6.20    let val {naming, theory_prefix, operations, target} = get_lthy lthy
    6.21    in init (Name_Space.get_group naming) theory_prefix operations target end;
    6.22  
    6.23 -val reinit = checkpoint o operation #reinit;
    6.24 -
    6.25  
    6.26  (* exit *)
    6.27  
     7.1 --- a/src/Pure/Isar/named_target.ML	Wed Aug 11 18:44:06 2010 +0200
     7.2 +++ b/src/Pure/Isar/named_target.ML	Wed Aug 11 20:25:44 2010 +0200
     7.3 @@ -22,7 +22,13 @@
     7.4  fun make_target target is_locale is_class =
     7.5    Target {target = target, is_locale = is_locale, is_class = is_class};
     7.6  
     7.7 -val global_target = make_target "" false false;
     7.8 +val global_target = Target {target = "", is_locale = false, is_class = false};
     7.9 +
    7.10 +fun named_target _ NONE = global_target
    7.11 +  | named_target thy (SOME locale) =
    7.12 +      if Locale.defined thy locale
    7.13 +      then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale}
    7.14 +      else error ("No such locale: " ^ quote locale);
    7.15  
    7.16  structure Data = Proof_Data
    7.17  (
    7.18 @@ -63,7 +69,7 @@
    7.19      val is_canonical_class = is_class andalso
    7.20        (Binding.eq_name (b, b')
    7.21          andalso not (null prefix')
    7.22 -        andalso List.last prefix' = (Class_Target.class_prefix target, false)
    7.23 +        andalso List.last prefix' = (Class.class_prefix target, false)
    7.24        orelse same_shape);
    7.25    in
    7.26      not is_canonical_class ?
    7.27 @@ -82,7 +88,7 @@
    7.28  
    7.29  fun class_target (Target {target, ...}) f =
    7.30    Local_Theory.raw_theory f #>
    7.31 -  Local_Theory.target (Class_Target.refresh_syntax target);
    7.32 +  Local_Theory.target (Class.refresh_syntax target);
    7.33  
    7.34  
    7.35  (* define *)
    7.36 @@ -96,7 +102,7 @@
    7.37      (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    7.38    Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    7.39    #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
    7.40 -    #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
    7.41 +    #> class_target ta (Class.declare target ((b, mx), (type_params, lhs)))
    7.42      #> pair (lhs, def))
    7.43  
    7.44  fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
    7.45 @@ -135,7 +141,7 @@
    7.46    if is_locale
    7.47      then lthy
    7.48        |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
    7.49 -      |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t'))
    7.50 +      |> is_class ? class_target ta (Class.abbrev target prmode ((b, mx), t'))
    7.51      else lthy
    7.52        |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
    7.53  
    7.54 @@ -168,18 +174,18 @@
    7.55      pretty_thy ctxt target is_class;
    7.56  
    7.57  
    7.58 -(* init various targets *)
    7.59 +(* init *)
    7.60  
    7.61  local
    7.62  
    7.63 -fun init_data (Target {target, is_locale, is_class}) =
    7.64 +fun init_context (Target {target, is_locale, is_class}) =
    7.65    if not is_locale then ProofContext.init_global
    7.66    else if not is_class then Locale.init target
    7.67 -  else Class_Target.init target;
    7.68 +  else Class.init target;
    7.69  
    7.70  fun init_target (ta as Target {target, ...}) thy =
    7.71    thy
    7.72 -  |> init_data ta
    7.73 +  |> init_context ta
    7.74    |> Data.put ta
    7.75    |> Local_Theory.init NONE (Long_Name.base_name target)
    7.76       {define = Generic_Target.define (target_foundation ta),
    7.77 @@ -190,15 +196,8 @@
    7.78        syntax_declaration = fn pervasive => target_declaration ta
    7.79          { syntax = true, pervasive = pervasive },
    7.80        pretty = pretty ta,
    7.81 -      reinit = init_target ta o ProofContext.theory_of,
    7.82        exit = Local_Theory.target_of};
    7.83  
    7.84 -fun named_target _ NONE = global_target
    7.85 -  | named_target thy (SOME target) =
    7.86 -      if Locale.defined thy target
    7.87 -      then make_target target true (Class_Target.is_class thy target)
    7.88 -      else error ("No such locale: " ^ quote target);
    7.89 -
    7.90  in
    7.91  
    7.92  fun init target thy = init_target (named_target thy target) thy;
     8.1 --- a/src/Pure/Isar/overloading.ML	Wed Aug 11 18:44:06 2010 +0200
     8.2 +++ b/src/Pure/Isar/overloading.ML	Wed Aug 11 20:25:44 2010 +0200
     8.3 @@ -6,14 +6,6 @@
     8.4  
     8.5  signature OVERLOADING =
     8.6  sig
     8.7 -  val init: (string * (string * typ) * bool) list -> theory -> Proof.context
     8.8 -  val conclude: local_theory -> local_theory
     8.9 -  val declare: string * typ -> theory -> term * theory
    8.10 -  val confirm: binding -> local_theory -> local_theory
    8.11 -  val define: bool -> binding -> string * term -> theory -> thm * theory
    8.12 -  val operation: Proof.context -> binding -> (string * bool) option
    8.13 -  val pretty: Proof.context -> Pretty.T
    8.14 -
    8.15    type improvable_syntax
    8.16    val add_improvable_syntax: Proof.context -> Proof.context
    8.17    val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
    8.18 @@ -121,27 +113,22 @@
    8.19  
    8.20  (** overloading target **)
    8.21  
    8.22 -(* bookkeeping *)
    8.23 -
    8.24 -structure OverloadingData = Proof_Data
    8.25 +structure Data = Proof_Data
    8.26  (
    8.27    type T = ((string * typ) * (string * bool)) list;
    8.28    fun init _ = [];
    8.29  );
    8.30  
    8.31 -val get_overloading = OverloadingData.get o Local_Theory.target_of;
    8.32 -val map_overloading = Local_Theory.target o OverloadingData.map;
    8.33 +val get_overloading = Data.get o Local_Theory.target_of;
    8.34 +val map_overloading = Local_Theory.target o Data.map;
    8.35  
    8.36  fun operation lthy b = get_overloading lthy
    8.37    |> get_first (fn ((c, _), (v, checked)) =>
    8.38 -      if Binding.name_of b = v then SOME (c, checked) else NONE);
    8.39 -
    8.40 -
    8.41 -(* target *)
    8.42 +      if Binding.name_of b = v then SOME (c, (v, checked)) else NONE);
    8.43  
    8.44  fun synchronize_syntax ctxt =
    8.45    let
    8.46 -    val overloading = OverloadingData.get ctxt;
    8.47 +    val overloading = Data.get ctxt;
    8.48      fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
    8.49       of SOME (v, _) => SOME (ty, Free (v, ty))
    8.50        | NONE => NONE;
    8.51 @@ -152,38 +139,20 @@
    8.52      |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
    8.53    end
    8.54  
    8.55 -fun init raw_overloading thy =
    8.56 -  let
    8.57 -    val _ = if null raw_overloading then error "At least one parameter must be given" else ();
    8.58 -    val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
    8.59 -  in
    8.60 -    thy
    8.61 -    |> Theory.checkpoint
    8.62 -    |> ProofContext.init_global
    8.63 -    |> OverloadingData.put overloading
    8.64 -    |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
    8.65 -    |> add_improvable_syntax
    8.66 -    |> synchronize_syntax
    8.67 -  end;
    8.68 -
    8.69 -fun declare c_ty = pair (Const c_ty);
    8.70 +fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
    8.71 +  Local_Theory.theory_result
    8.72 +    (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
    8.73 +  ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
    8.74 +  ##> Local_Theory.target synchronize_syntax
    8.75 +  #-> (fn (_, def) => pair (Const (c, U), def))
    8.76  
    8.77 -fun define checked b (c, t) =
    8.78 -  Thm.add_def (not checked) true (b, Logic.mk_equals (Const (c, Term.fastype_of t), t))
    8.79 -  #>> snd;
    8.80 -
    8.81 -fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
    8.82 -  #> Local_Theory.target synchronize_syntax
    8.83 -
    8.84 -fun conclude lthy =
    8.85 -  let
    8.86 -    val overloading = get_overloading lthy;
    8.87 -    val _ = if null overloading then () else
    8.88 -      error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
    8.89 -        o Syntax.string_of_term lthy o Const o fst) overloading));
    8.90 -  in
    8.91 -    lthy
    8.92 -  end;
    8.93 +fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    8.94 +  case operation lthy b
    8.95 +   of SOME (c, (v, checked)) => if mx <> NoSyn
    8.96 +       then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
    8.97 +        else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
    8.98 +    | NONE => lthy |>
    8.99 +        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
   8.100  
   8.101  fun pretty lthy =
   8.102    let
   8.103 @@ -192,32 +161,32 @@
   8.104      fun pr_operation ((c, ty), (v, _)) =
   8.105        (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
   8.106          Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty];
   8.107 -  in
   8.108 -    (Pretty.block o Pretty.fbreaks)
   8.109 -      (Pretty.str "overloading" :: map pr_operation overloading)
   8.110 -  end;
   8.111 -
   8.112 -fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
   8.113 +  in Pretty.str "overloading" :: map pr_operation overloading end;
   8.114  
   8.115 -fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   8.116 -  case operation lthy b
   8.117 -   of SOME (c, checked) => if mx <> NoSyn then syntax_error c
   8.118 -        else lthy |> Local_Theory.theory_result (declare (c, U)
   8.119 -            ##>> define checked b_def (c, rhs))
   8.120 -          ||> confirm b
   8.121 -    | NONE => lthy |>
   8.122 -        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
   8.123 +fun conclude lthy =
   8.124 +  let
   8.125 +    val overloading = get_overloading lthy;
   8.126 +    val _ = if null overloading then () else
   8.127 +      error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
   8.128 +        o Syntax.string_of_term lthy o Const o fst) overloading));
   8.129 +  in lthy end;
   8.130  
   8.131 -fun gen_overloading prep_const raw_ops thy =
   8.132 +fun gen_overloading prep_const raw_overloading thy =
   8.133    let
   8.134      val ctxt = ProofContext.init_global thy;
   8.135 -    val ops = raw_ops |> map (fn (name, const, checked) =>
   8.136 -      (name, Term.dest_Const (prep_const ctxt const), checked));
   8.137 +    val _ = if null raw_overloading then error "At least one parameter must be given" else ();
   8.138 +    val overloading = raw_overloading |> map (fn (v, const, checked) =>
   8.139 +      (Term.dest_Const (prep_const ctxt const), (v, checked)));
   8.140    in
   8.141      thy
   8.142 -    |> init ops
   8.143 +    |> Theory.checkpoint
   8.144 +    |> ProofContext.init_global
   8.145 +    |> Data.put overloading
   8.146 +    |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
   8.147 +    |> add_improvable_syntax
   8.148 +    |> synchronize_syntax
   8.149      |> Local_Theory.init NONE ""
   8.150 -       {define = Generic_Target.define overloading_foundation,
   8.151 +       {define = Generic_Target.define foundation,
   8.152          notes = Generic_Target.notes
   8.153            (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
   8.154          abbrev = Generic_Target.abbrev
   8.155 @@ -225,8 +194,7 @@
   8.156              Generic_Target.theory_abbrev prmode ((b, mx), t)),
   8.157          declaration = K Generic_Target.theory_declaration,
   8.158          syntax_declaration = K Generic_Target.theory_declaration,
   8.159 -        pretty = single o pretty,
   8.160 -        reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
   8.161 +        pretty = pretty,
   8.162          exit = Local_Theory.target_of o conclude}
   8.163    end;
   8.164  
     9.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 11 18:44:06 2010 +0200
     9.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 11 20:25:44 2010 +0200
     9.3 @@ -111,8 +111,10 @@
     9.4  
     9.5  fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
     9.6    | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
     9.7 -  | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' =>
     9.8 -      Context.Proof (Local_Theory.reinit (Local_Theory.raw_theory (K (loc_exit lthy')) lthy));
     9.9 +  | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => let
    9.10 +        val target_name = #target (Named_Target.peek lthy);
    9.11 +        val target = if target_name = "" then NONE else SOME target_name;
    9.12 +      in Context.Proof (Named_Target.init target (loc_exit lthy')) end;
    9.13  
    9.14  
    9.15  (* datatype node *)
    10.1 --- a/src/Pure/ROOT.ML	Wed Aug 11 18:44:06 2010 +0200
    10.2 +++ b/src/Pure/ROOT.ML	Wed Aug 11 20:25:44 2010 +0200
    10.3 @@ -209,10 +209,10 @@
    10.4  use "Isar/generic_target.ML";
    10.5  use "Isar/overloading.ML";
    10.6  use "axclass.ML";
    10.7 -use "Isar/class_target.ML";
    10.8 +use "Isar/class.ML";
    10.9  use "Isar/named_target.ML";
   10.10  use "Isar/expression.ML";
   10.11 -use "Isar/class.ML";
   10.12 +use "Isar/class_declaration.ML";
   10.13  
   10.14  use "simplifier.ML";
   10.15  
    11.1 --- a/src/Pure/axclass.ML	Wed Aug 11 18:44:06 2010 +0200
    11.2 +++ b/src/Pure/axclass.ML	Wed Aug 11 20:25:44 2010 +0200
    11.3 @@ -406,7 +406,7 @@
    11.4    in
    11.5      thy
    11.6      |> Thm.add_def false false (b', prop)
    11.7 -    |>> (fn (_, thm) =>  Drule.transitive_thm OF [eq, thm])
    11.8 +    |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm])
    11.9    end;
   11.10  
   11.11