code cleanup
authorhaftmann
Sat Jan 17 08:29:54 2009 +0100 (2009-01-17)
changeset 295260b32c8b84d3e
parent 29525 ad7991d7b5bb
child 29527 7178c11b6bc1
code cleanup
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
     1.1 --- a/src/Pure/Isar/class.ML	Sat Jan 17 08:29:40 2009 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Jan 17 08:29:54 2009 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4          |> SOME
     1.5        end;
     1.6  
     1.7 -fun raw_morphism thy class sups param_map some_axiom =
     1.8 +fun calculate_morphism thy class sups param_map some_axiom =
     1.9    let
    1.10      val ctxt = ProofContext.init thy;
    1.11      val (([props], [(_, morph1)], export_morph), _) = ctxt
    1.12 @@ -58,9 +58,8 @@
    1.13            $> Element.satisfy_morphism [(Element.prove_witness ctxt prop
    1.14                 (ALLGOALS (ProofContext.fact_tac (the_list some_axiom))))]
    1.15          | [] => morph2;
    1.16 -    (*FIXME generic amend operation for classes*)
    1.17 -    val morph4 = morph3 $> eq_morph thy (these_defs thy sups);
    1.18 -  in (morph4, export_morph) end;
    1.19 +    val morph4 = morph3 $> Element.eq_morphism thy (these_defs thy sups);
    1.20 +  in (morph3, morph4, export_morph) end;
    1.21  
    1.22  fun calculate_rules thy morph sups base_sort param_map axiom class =
    1.23    let
    1.24 @@ -96,13 +95,6 @@
    1.25        |> Thm.close_derivation;
    1.26    in (assm_intro, of_class) end;
    1.27  
    1.28 -fun note_assm_intro class assm_intro thy =
    1.29 -  thy
    1.30 -  |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN)
    1.31 -  |> PureThy.store_thm (AxClass.introN, assm_intro)
    1.32 -  |> snd
    1.33 -  |> Sign.restore_naming thy;
    1.34 -
    1.35  
    1.36  (** define classes **)
    1.37  
    1.38 @@ -110,6 +102,7 @@
    1.39  
    1.40  fun gen_class_spec prep_class process_decl thy raw_supclasses raw_elems =
    1.41    let
    1.42 +    (*FIXME 2009 simplify*)
    1.43      val supclasses = map (prep_class thy) raw_supclasses;
    1.44      val supsort = Sign.minimize_sort thy supclasses;
    1.45      val sups = filter (is_class thy) supsort;
    1.46 @@ -127,7 +120,7 @@
    1.47        sups, []);
    1.48      val constrain = Element.Constrains ((map o apsnd o map_atyps)
    1.49        (K (TFree (Name.aT, base_sort))) supparams);
    1.50 -      (*FIXME perhaps better: control type variable by explicit
    1.51 +      (*FIXME 2009 perhaps better: control type variable by explicit
    1.52        parameter instantiation of import expression*)
    1.53      val begin_ctxt = begin sups base_sort
    1.54        #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
    1.55 @@ -148,6 +141,7 @@
    1.56  
    1.57  fun add_consts bname class base_sort sups supparams global_syntax thy =
    1.58    let
    1.59 +    (*FIXME 2009 simplify*)
    1.60      val supconsts = supparams
    1.61        |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
    1.62        |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
    1.63 @@ -177,6 +171,7 @@
    1.64  
    1.65  fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
    1.66    let
    1.67 +    (*FIXME 2009 simplify*)
    1.68      fun globalize param_map = map_aterms
    1.69        (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
    1.70          | t => t);
    1.71 @@ -191,12 +186,12 @@
    1.72      |> add_consts bname class base_sort sups supparams global_syntax
    1.73      |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
    1.74            (map (fst o snd) params)
    1.75 -          [(((*Binding.name (bname ^ "_" ^ AxClass.axiomsN*) Binding.empty, []),
    1.76 +          [((Binding.empty, []),
    1.77              Option.map (globalize param_map) raw_pred |> the_list)]
    1.78      #> snd
    1.79      #> `get_axiom
    1.80      #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
    1.81 -    #> pair (map (Const o snd) param_map, param_map, params, assm_axiom)))
    1.82 +    #> pair (param_map, params, assm_axiom)))
    1.83    end;
    1.84  
    1.85  fun gen_class prep_spec bname raw_supclasses raw_elems thy =
    1.86 @@ -204,32 +199,20 @@
    1.87      val class = Sign.full_bname thy bname;
    1.88      val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
    1.89        prep_spec thy raw_supclasses raw_elems;
    1.90 -    (*val export_morph = (*FIXME how canonical is this?*)
    1.91 -      Morphism.morphism { binding = I, var = I,
    1.92 -        typ = Logic.varifyT,
    1.93 -        term = (*map_types Logic.varifyT*) I,
    1.94 -        fact = map Thm.varifyT
    1.95 -      } $> Morphism.morphism { binding = I, var = I,
    1.96 -        typ = Logic.type_map TermSubst.zero_var_indexes,
    1.97 -        term = TermSubst.zero_var_indexes,
    1.98 -        fact = Drule.zero_var_indexes_list o map Thm.strip_shyps
    1.99 -      };*)
   1.100    in
   1.101      thy
   1.102      |> Expression.add_locale bname "" supexpr elems
   1.103      |> snd |> LocalTheory.exit_global
   1.104      |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
   1.105 -    |-> (fn (inst, param_map, params, assm_axiom) =>
   1.106 +    |-> (fn (param_map, params, assm_axiom) =>
   1.107         `(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class)
   1.108      #-> (fn axiom =>
   1.109 -       `(fn thy => raw_morphism thy class sups param_map axiom)
   1.110 -    #-> (fn (morph, export_morph) => Locale.add_registration (class, (morph, export_morph))
   1.111 +       `(fn thy => calculate_morphism thy class sups param_map axiom)
   1.112 +    #-> (fn (raw_morph, morph, export_morph) => Locale.add_registration (class, (morph, export_morph))
   1.113      #>  Locale.activate_global_facts (class, morph $> export_morph)
   1.114      #> `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class)
   1.115      #-> (fn (assm_intro, of_class) =>
   1.116 -        register class sups params base_sort inst
   1.117 -          morph axiom assm_intro of_class
   1.118 -    (*#> fold (note_assm_intro class) (the_list assm_intro*)))))
   1.119 +        register class sups params base_sort raw_morph axiom assm_intro of_class))))
   1.120      |> TheoryTarget.init (SOME class)
   1.121      |> pair class
   1.122    end;
   1.123 @@ -246,12 +229,6 @@
   1.124  
   1.125  local
   1.126  
   1.127 -fun prove_sublocale tac (sub, expr) =
   1.128 -  Expression.sublocale sub expr
   1.129 -  #> Proof.global_terminal_proof
   1.130 -      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   1.131 -  #> ProofContext.theory_of;
   1.132 -
   1.133  fun gen_subclass prep_class do_proof raw_sup lthy =
   1.134    let
   1.135      val thy = ProofContext.theory_of lthy;
   1.136 @@ -259,6 +236,7 @@
   1.137      val sub = case TheoryTarget.peek lthy
   1.138       of {is_class = false, ...} => error "Not a class context"
   1.139        | {target, ...} => target;
   1.140 +
   1.141      val _ = if Sign.subsort thy ([sup], [sub])
   1.142        then error ("Class " ^ Syntax.string_of_sort lthy [sup]
   1.143          ^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub])
   1.144 @@ -273,15 +251,21 @@
   1.145      val expr = ([(sup, (("", false), Expression.Positional []))], []);
   1.146      val (([props], _, _), goal_ctxt) =
   1.147        Expression.cert_goal_expression expr lthy;
   1.148 -    val some_prop = try the_single props; (*FIXME*)
   1.149 +    val some_prop = try the_single props;
   1.150 +
   1.151 +    fun tac some_thm = ALLGOALS (ProofContext.fact_tac (the_list some_thm));
   1.152 +    fun prove_sublocale some_thm =
   1.153 +      Expression.sublocale sub expr
   1.154 +      #> Proof.global_terminal_proof
   1.155 +          (Method.Basic (K (Method.SIMPLE_METHOD (tac some_thm)), Position.none), NONE)
   1.156 +      #> ProofContext.theory_of;
   1.157      fun after_qed some_thm =
   1.158        LocalTheory.theory (register_subclass (sub, sup) some_thm)
   1.159 -      #> is_some some_thm ? LocalTheory.theory
   1.160 -        (prove_sublocale (ALLGOALS (ProofContext.fact_tac (the_list some_thm))) (sub, expr))
   1.161 -      #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of);
   1.162 -  in
   1.163 -    do_proof after_qed some_prop lthy
   1.164 -  end;
   1.165 +      #> is_some some_thm ? LocalTheory.theory (prove_sublocale some_thm)
   1.166 +          (*FIXME should also go to register_subclass*)
   1.167 +      #> ProofContext.theory_of
   1.168 +      #> TheoryTarget.init (SOME sub);
   1.169 +  in do_proof after_qed some_prop lthy end;
   1.170  
   1.171  fun user_proof after_qed NONE =
   1.172        Proof.theorem_i NONE (K (after_qed NONE)) [[]]
     2.1 --- a/src/Pure/Isar/class_target.ML	Sat Jan 17 08:29:40 2009 +0100
     2.2 +++ b/src/Pure/Isar/class_target.ML	Sat Jan 17 08:29:54 2009 +0100
     2.3 @@ -8,31 +8,27 @@
     2.4  sig
     2.5    (*classes*)
     2.6    val register: class -> class list -> ((string * typ) * (string * typ)) list
     2.7 -    -> sort -> term list -> morphism
     2.8 -    -> thm option -> thm option -> thm -> theory -> theory
     2.9 +    -> sort -> morphism -> thm option -> thm option -> thm
    2.10 +    -> theory -> theory
    2.11    val register_subclass: class * class -> thm option
    2.12      -> theory -> theory
    2.13  
    2.14 +  val is_class: theory -> class -> bool
    2.15 +  val base_sort: theory -> class -> sort
    2.16 +  val rules: theory -> class -> thm option * thm
    2.17 +  val these_params: theory -> sort -> (string * (class * (string * typ))) list
    2.18 +  val these_defs: theory -> sort -> thm list
    2.19 +  val print_classes: theory -> unit
    2.20 +
    2.21    val begin: class list -> sort -> Proof.context -> Proof.context
    2.22    val init: class -> theory -> Proof.context
    2.23    val declare: class -> Properties.T
    2.24      -> (string * mixfix) * term -> theory -> theory
    2.25    val abbrev: class -> Syntax.mode -> Properties.T
    2.26      -> (string * mixfix) * term -> theory -> theory
    2.27 +  val class_prefix: string -> string
    2.28    val refresh_syntax: class -> Proof.context -> Proof.context
    2.29  
    2.30 -  val intro_classes_tac: thm list -> tactic
    2.31 -  val default_intro_tac: Proof.context -> thm list -> tactic
    2.32 -
    2.33 -  val class_prefix: string -> string
    2.34 -  val is_class: theory -> class -> bool
    2.35 -  val these_params: theory -> sort -> (string * (class * (string * typ))) list
    2.36 -  val these_defs: theory -> sort -> thm list
    2.37 -  val eq_morph: theory -> thm list -> morphism
    2.38 -  val base_sort: theory -> class -> sort
    2.39 -  val rules: theory -> class -> thm option * thm
    2.40 -  val print_classes: theory -> unit
    2.41 -
    2.42    (*instances*)
    2.43    val init_instantiation: string list * (string * sort) list * sort
    2.44      -> theory -> local_theory
    2.45 @@ -50,6 +46,9 @@
    2.46    val pretty_instantiation: local_theory -> Pretty.T
    2.47    val type_name: string -> string
    2.48  
    2.49 +  val intro_classes_tac: thm list -> tactic
    2.50 +  val default_intro_tac: Proof.context -> thm list -> tactic
    2.51 +
    2.52    (*old axclass layer*)
    2.53    val axclass_cmd: bstring * xstring list
    2.54      -> (Attrib.binding * string list) list
    2.55 @@ -116,8 +115,6 @@
    2.56    consts: (string * string) list
    2.57      (*locale parameter ~> constant name*),
    2.58    base_sort: sort,
    2.59 -  inst: term list
    2.60 -    (*canonical interpretation*),
    2.61    base_morph: Morphism.morphism
    2.62      (*static part of canonical morphism*),
    2.63    assm_intro: thm option,
    2.64 @@ -130,22 +127,22 @@
    2.65  
    2.66  };
    2.67  
    2.68 -fun rep_class_data (ClassData d) = d;
    2.69 -fun mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
    2.70 +fun rep_class_data (ClassData data) = data;
    2.71 +fun mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    2.72      (defs, operations)) =
    2.73 -  ClassData { consts = consts, base_sort = base_sort, inst = inst,
    2.74 +  ClassData { consts = consts, base_sort = base_sort,
    2.75      base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
    2.76      defs = defs, operations = operations };
    2.77 -fun map_class_data f (ClassData { consts, base_sort, inst, base_morph, assm_intro,
    2.78 +fun map_class_data f (ClassData { consts, base_sort, base_morph, assm_intro,
    2.79      of_class, axiom, defs, operations }) =
    2.80 -  mk_class_data (f ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
    2.81 +  mk_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    2.82      (defs, operations)));
    2.83  fun merge_class_data _ (ClassData { consts = consts,
    2.84 -    base_sort = base_sort, inst = inst, base_morph = base_morph, assm_intro = assm_intro,
    2.85 +    base_sort = base_sort, base_morph = base_morph, assm_intro = assm_intro,
    2.86      of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
    2.87 -  ClassData { consts = _, base_sort = _, inst = _, base_morph = _, assm_intro = _,
    2.88 +  ClassData { consts = _, base_sort = _, base_morph = _, assm_intro = _,
    2.89      of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
    2.90 -  mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
    2.91 +  mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    2.92      (Thm.merge_thms (defs1, defs2),
    2.93        AList.merge (op =) (K true) (operations1, operations2)));
    2.94  
    2.95 @@ -170,11 +167,8 @@
    2.96  val is_class = is_some oo lookup_class_data;
    2.97  
    2.98  val ancestry = Graph.all_succs o ClassData.get;
    2.99 -
   2.100  val heritage = Graph.all_preds o ClassData.get;
   2.101  
   2.102 -fun the_inst thy = #inst o the_class_data thy;
   2.103 -
   2.104  fun these_params thy =
   2.105    let
   2.106      fun params class =
   2.107 @@ -187,34 +181,22 @@
   2.108        end;
   2.109    in maps params o ancestry thy end;
   2.110  
   2.111 -fun these_assm_intros thy =
   2.112 +val base_sort = #base_sort oo the_class_data;
   2.113 +
   2.114 +fun rules thy class =
   2.115 +  let val { axiom, of_class, ... } = the_class_data thy class
   2.116 +  in (axiom, of_class) end;
   2.117 +
   2.118 +fun all_assm_intros thy =
   2.119    Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
   2.120      ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
   2.121  
   2.122 -fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
   2.123 -
   2.124 -fun these_operations thy =
   2.125 -  maps (#operations o the_class_data thy) o ancestry thy;
   2.126 -
   2.127 -val base_sort = #base_sort oo the_class_data;
   2.128 -
   2.129 -fun rules thy class = let
   2.130 -    val { axiom, of_class, ... } = the_class_data thy class
   2.131 -  in (axiom, of_class) end;
   2.132 +fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
   2.133 +fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
   2.134  
   2.135 -val class_prefix = Logic.const_of_class o Sign.base_name;
   2.136 -
   2.137 -fun class_binding_morph class =
   2.138 -  Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
   2.139 -
   2.140 -fun eq_morph thy thms = (*FIXME how general is this?*)
   2.141 -  Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms [])
   2.142 -  $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms);
   2.143 -
   2.144 -fun morphism thy class =
   2.145 -  let
   2.146 -    val { base_morph, defs, ... } = the_class_data thy class;
   2.147 -  in base_morph $> eq_morph thy defs end;
   2.148 +val base_morphism = #base_morph oo the_class_data;
   2.149 +fun morphism thy class = base_morphism thy class
   2.150 +  $> Element.eq_morphism thy (these_defs thy [class]);
   2.151  
   2.152  fun print_classes thy =
   2.153    let
   2.154 @@ -236,8 +218,6 @@
   2.155        (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
   2.156        (SOME o Pretty.block) [Pretty.str "supersort: ",
   2.157          (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
   2.158 -      if is_class thy class then (SOME o Pretty.str)
   2.159 -        ("locale: " ^ Locale.extern thy class) else NONE,
   2.160        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
   2.161            (Pretty.str "parameters:" :: ps)) o map mk_param
   2.162          o these o Option.map #params o try (AxClass.get_info thy)) class,
   2.163 @@ -254,18 +234,26 @@
   2.164  
   2.165  (* updaters *)
   2.166  
   2.167 -fun register class superclasses params base_sort inst morph
   2.168 +fun register class sups params base_sort morph
   2.169      axiom assm_intro of_class thy =
   2.170    let
   2.171      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
   2.172        (c, (class, (ty, Free v_ty)))) params;
   2.173      val add_class = Graph.new_node (class,
   2.174          mk_class_data (((map o pairself) fst params, base_sort,
   2.175 -          inst, morph, assm_intro, of_class, axiom), ([], operations)))
   2.176 -      #> fold (curry Graph.add_edge class) superclasses;
   2.177 +          morph, assm_intro, of_class, axiom), ([], operations)))
   2.178 +      #> fold (curry Graph.add_edge class) sups;
   2.179    in ClassData.map add_class thy end;
   2.180  
   2.181 +fun activate_defs class thms thy =
   2.182 +  let
   2.183 +    val eq_morph = Element.eq_morphism thy thms;
   2.184 +    fun amend cls thy = Locale.amend_registration eq_morph
   2.185 +      (cls, morphism thy cls) thy;
   2.186 +  in fold amend (heritage thy [class]) thy end;
   2.187 +
   2.188  fun register_operation class (c, (t, some_def)) thy =
   2.189 +  (*FIXME 2009 does this still also work for abbrevs?*)
   2.190    let
   2.191      val base_sort = base_sort thy class;
   2.192      val prep_typ = map_type_tfree
   2.193 @@ -279,12 +267,11 @@
   2.194        (fn (defs, operations) =>
   2.195          (fold cons (the_list some_def) defs,
   2.196            (c, (class, (ty', t'))) :: operations))
   2.197 +    |> is_some some_def ? activate_defs class (the_list some_def)
   2.198    end;
   2.199  
   2.200 -
   2.201 -(** tactics and methods **)
   2.202 -
   2.203  fun register_subclass (sub, sup) thms thy =
   2.204 +  (*FIXME should also add subclass interpretation*)
   2.205    let
   2.206      val of_class = (snd o rules thy) sup;
   2.207      val intro = case thms
   2.208 @@ -293,46 +280,15 @@
   2.209            ([], [sub])], []) of_class;
   2.210      val classrel = (intro OF (the_list o fst o rules thy) sub)
   2.211        |> Thm.close_derivation;
   2.212 -    (*FIXME generic amend operation for classes*)
   2.213 -    val amendments = map (fn class => (class, morphism thy class))
   2.214 -      (heritage thy [sub]);
   2.215      val diff_sort = Sign.complete_sort thy [sup]
   2.216        |> subtract (op =) (Sign.complete_sort thy [sub]);
   2.217 -    val defs_morph = eq_morph thy (these_defs thy diff_sort);
   2.218    in
   2.219      thy
   2.220      |> AxClass.add_classrel classrel
   2.221      |> ClassData.map (Graph.add_edge (sub, sup))
   2.222 -    |> fold (Locale.amend_registration defs_morph) amendments
   2.223 -  end;
   2.224 -
   2.225 -fun intro_classes_tac facts st =
   2.226 -  let
   2.227 -    val thy = Thm.theory_of_thm st;
   2.228 -    val classes = Sign.all_classes thy;
   2.229 -    val class_trivs = map (Thm.class_triv thy) classes;
   2.230 -    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   2.231 -    val assm_intros = these_assm_intros thy;
   2.232 -  in
   2.233 -    Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
   2.234 +    |> activate_defs sub (these_defs thy diff_sort)
   2.235    end;
   2.236  
   2.237 -fun default_intro_tac ctxt [] =
   2.238 -      intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE
   2.239 -      Locale.intro_locales_tac true ctxt []
   2.240 -  | default_intro_tac _ _ = no_tac;
   2.241 -
   2.242 -fun default_tac rules ctxt facts =
   2.243 -  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   2.244 -    default_intro_tac ctxt facts;
   2.245 -
   2.246 -val _ = Context.>> (Context.map_theory
   2.247 -  (Method.add_methods
   2.248 -   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   2.249 -      "back-chain introduction rules of classes"),
   2.250 -    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   2.251 -      "apply some intro/elim rule")]));
   2.252 -
   2.253  
   2.254  (** classes and class target **)
   2.255  
   2.256 @@ -393,35 +349,33 @@
   2.257  
   2.258  (* class target *)
   2.259  
   2.260 +val class_prefix = Logic.const_of_class o Sign.base_name;
   2.261 +
   2.262  fun declare class pos ((c, mx), dict) thy =
   2.263    let
   2.264      val prfx = class_prefix class;
   2.265      val thy' = thy |> Sign.add_path prfx;
   2.266 +      (*FIXME 2009 use proper name morphism*)
   2.267      val morph = morphism thy' class;
   2.268 -    val inst = the_inst thy' class;
   2.269      val params = map (apsnd fst o snd) (these_params thy' [class]);
   2.270 -    val amendments = map (fn class => (class, morphism thy' class))
   2.271 -      (heritage thy' [class]);
   2.272  
   2.273      val c' = Sign.full_bname thy' c;
   2.274      val dict' = Morphism.term morph dict;
   2.275      val ty' = Term.fastype_of dict';
   2.276      val ty'' = Type.strip_sorts ty';
   2.277 +      (*FIXME 2009 the tinkering with theorems here is a mess*)
   2.278      val def_eq = Logic.mk_equals (Const (c', ty'), dict');
   2.279 -    (*FIXME a mess*)
   2.280 -    fun amend def def' (class, morph) thy =
   2.281 -      Locale.amend_registration (eq_morph thy [Thm.varifyT def])
   2.282 -        (class, morph) thy;
   2.283      fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
   2.284    in
   2.285      thy'
   2.286      |> Sign.declare_const pos ((Binding.name c, ty''), mx) |> snd
   2.287 -    |> Thm.add_def false false (c, def_eq)
   2.288 +    |> Thm.add_def false false (c, def_eq) (*FIXME 2009 name of theorem*)
   2.289 +      (*FIXME 2009 add_def should accept binding*)
   2.290      |>> Thm.symmetric
   2.291      ||>> get_axiom
   2.292      |-> (fn (def, def') => register_operation class (c', (dict', SOME (Thm.symmetric def')))
   2.293 -      #> fold (amend def def') amendments
   2.294 -      #> PureThy.store_thm (c ^ "_raw", def') (*FIXME name*)
   2.295 +      #> PureThy.store_thm (c ^ "_raw", def') (*FIXME 2009 name of theorem*)
   2.296 +         (*FIXME 2009 store_thm etc. should accept binding*)
   2.297        #> snd)
   2.298      |> Sign.restore_naming thy
   2.299      |> Sign.add_const_constraint (c', SOME ty')
   2.300 @@ -522,7 +476,7 @@
   2.301  
   2.302  fun type_name "*" = "prod"
   2.303    | type_name "+" = "sum"
   2.304 -  | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
   2.305 +  | type_name s = sanatize_name (NameSpace.base s);
   2.306  
   2.307  fun resort_terms pp algebra consts constraints ts =
   2.308    let
   2.309 @@ -638,5 +592,35 @@
   2.310        (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
   2.311    end;
   2.312  
   2.313 +
   2.314 +(** tactics and methods **)
   2.315 +
   2.316 +fun intro_classes_tac facts st =
   2.317 +  let
   2.318 +    val thy = Thm.theory_of_thm st;
   2.319 +    val classes = Sign.all_classes thy;
   2.320 +    val class_trivs = map (Thm.class_triv thy) classes;
   2.321 +    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
   2.322 +    val assm_intros = all_assm_intros thy;
   2.323 +  in
   2.324 +    Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
   2.325 +  end;
   2.326 +
   2.327 +fun default_intro_tac ctxt [] =
   2.328 +      intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE
   2.329 +      Locale.intro_locales_tac true ctxt []
   2.330 +  | default_intro_tac _ _ = no_tac;
   2.331 +
   2.332 +fun default_tac rules ctxt facts =
   2.333 +  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   2.334 +    default_intro_tac ctxt facts;
   2.335 +
   2.336 +val _ = Context.>> (Context.map_theory
   2.337 +  (Method.add_methods
   2.338 +   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   2.339 +      "back-chain introduction rules of classes"),
   2.340 +    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   2.341 +      "apply some intro/elim rule")]));
   2.342 +
   2.343  end;
   2.344