code cleanup

--- a/src/Pure/Isar/class.ML	Sat Jan 17 08:29:40 2009 +0100
+++ b/src/Pure/Isar/class.ML	Sat Jan 17 08:29:54 2009 +0100
@@ -45,7 +45,7 @@
         |> SOME
       end;
 
-fun raw_morphism thy class sups param_map some_axiom =
+fun calculate_morphism thy class sups param_map some_axiom =
   let
     val ctxt = ProofContext.init thy;
     val (([props], [(_, morph1)], export_morph), _) = ctxt
@@ -58,9 +58,8 @@
           $> Element.satisfy_morphism [(Element.prove_witness ctxt prop
                (ALLGOALS (ProofContext.fact_tac (the_list some_axiom))))]
         | [] => morph2;
-    (*FIXME generic amend operation for classes*)
-    val morph4 = morph3 $> eq_morph thy (these_defs thy sups);
-  in (morph4, export_morph) end;
+    val morph4 = morph3 $> Element.eq_morphism thy (these_defs thy sups);
+  in (morph3, morph4, export_morph) end;
 
 fun calculate_rules thy morph sups base_sort param_map axiom class =
   let
@@ -96,13 +95,6 @@
       |> Thm.close_derivation;
   in (assm_intro, of_class) end;
 
-fun note_assm_intro class assm_intro thy =
-  thy
-  |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN)
-  |> PureThy.store_thm (AxClass.introN, assm_intro)
-  |> snd
-  |> Sign.restore_naming thy;
-
 
 (** define classes **)
 
@@ -110,6 +102,7 @@
 
 fun gen_class_spec prep_class process_decl thy raw_supclasses raw_elems =
   let
+    (*FIXME 2009 simplify*)
     val supclasses = map (prep_class thy) raw_supclasses;
     val supsort = Sign.minimize_sort thy supclasses;
     val sups = filter (is_class thy) supsort;
@@ -127,7 +120,7 @@
       sups, []);
     val constrain = Element.Constrains ((map o apsnd o map_atyps)
       (K (TFree (Name.aT, base_sort))) supparams);
-      (*FIXME perhaps better: control type variable by explicit
+      (*FIXME 2009 perhaps better: control type variable by explicit
       parameter instantiation of import expression*)
     val begin_ctxt = begin sups base_sort
       #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
@@ -148,6 +141,7 @@
 
 fun add_consts bname class base_sort sups supparams global_syntax thy =
   let
+    (*FIXME 2009 simplify*)
     val supconsts = supparams
       |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
       |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
@@ -177,6 +171,7 @@
 
 fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
   let
+    (*FIXME 2009 simplify*)
     fun globalize param_map = map_aterms
       (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
         | t => t);
@@ -191,12 +186,12 @@
     |> add_consts bname class base_sort sups supparams global_syntax
     |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
           (map (fst o snd) params)
-          [(((*Binding.name (bname ^ "_" ^ AxClass.axiomsN*) Binding.empty, []),
+          [((Binding.empty, []),
             Option.map (globalize param_map) raw_pred |> the_list)]
     #> snd
     #> `get_axiom
     #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
-    #> pair (map (Const o snd) param_map, param_map, params, assm_axiom)))
+    #> pair (param_map, params, assm_axiom)))
   end;
 
 fun gen_class prep_spec bname raw_supclasses raw_elems thy =
@@ -204,32 +199,20 @@
     val class = Sign.full_bname thy bname;
     val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
       prep_spec thy raw_supclasses raw_elems;
-    (*val export_morph = (*FIXME how canonical is this?*)
-      Morphism.morphism { binding = I, var = I,
-        typ = Logic.varifyT,
-        term = (*map_types Logic.varifyT*) I,
-        fact = map Thm.varifyT
-      } $> Morphism.morphism { binding = I, var = I,
-        typ = Logic.type_map TermSubst.zero_var_indexes,
-        term = TermSubst.zero_var_indexes,
-        fact = Drule.zero_var_indexes_list o map Thm.strip_shyps
-      };*)
   in
     thy
     |> Expression.add_locale bname "" supexpr elems
     |> snd |> LocalTheory.exit_global
     |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
-    |-> (fn (inst, param_map, params, assm_axiom) =>
+    |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class)
     #-> (fn axiom =>
-       `(fn thy => raw_morphism thy class sups param_map axiom)
-    #-> (fn (morph, export_morph) => Locale.add_registration (class, (morph, export_morph))
+       `(fn thy => calculate_morphism thy class sups param_map axiom)
+    #-> (fn (raw_morph, morph, export_morph) => Locale.add_registration (class, (morph, export_morph))
     #>  Locale.activate_global_facts (class, morph $> export_morph)
     #> `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class)
     #-> (fn (assm_intro, of_class) =>
-        register class sups params base_sort inst
-          morph axiom assm_intro of_class
-    (*#> fold (note_assm_intro class) (the_list assm_intro*)))))
+        register class sups params base_sort raw_morph axiom assm_intro of_class))))
     |> TheoryTarget.init (SOME class)
     |> pair class
   end;
@@ -246,12 +229,6 @@
 
 local
 
-fun prove_sublocale tac (sub, expr) =
-  Expression.sublocale sub expr
-  #> Proof.global_terminal_proof
-      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
-  #> ProofContext.theory_of;
-
 fun gen_subclass prep_class do_proof raw_sup lthy =
   let
     val thy = ProofContext.theory_of lthy;
@@ -259,6 +236,7 @@
     val sub = case TheoryTarget.peek lthy
      of {is_class = false, ...} => error "Not a class context"
       | {target, ...} => target;
+
     val _ = if Sign.subsort thy ([sup], [sub])
       then error ("Class " ^ Syntax.string_of_sort lthy [sup]
         ^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub])
@@ -273,15 +251,21 @@
     val expr = ([(sup, (("", false), Expression.Positional []))], []);
     val (([props], _, _), goal_ctxt) =
       Expression.cert_goal_expression expr lthy;
-    val some_prop = try the_single props; (*FIXME*)
+    val some_prop = try the_single props;
+
+    fun tac some_thm = ALLGOALS (ProofContext.fact_tac (the_list some_thm));
+    fun prove_sublocale some_thm =
+      Expression.sublocale sub expr
+      #> Proof.global_terminal_proof
+          (Method.Basic (K (Method.SIMPLE_METHOD (tac some_thm)), Position.none), NONE)
+      #> ProofContext.theory_of;
     fun after_qed some_thm =
       LocalTheory.theory (register_subclass (sub, sup) some_thm)
-      #> is_some some_thm ? LocalTheory.theory
-        (prove_sublocale (ALLGOALS (ProofContext.fact_tac (the_list some_thm))) (sub, expr))
-      #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of);
-  in
-    do_proof after_qed some_prop lthy
-  end;
+      #> is_some some_thm ? LocalTheory.theory (prove_sublocale some_thm)
+          (*FIXME should also go to register_subclass*)
+      #> ProofContext.theory_of
+      #> TheoryTarget.init (SOME sub);
+  in do_proof after_qed some_prop lthy end;
 
 fun user_proof after_qed NONE =
       Proof.theorem_i NONE (K (after_qed NONE)) [[]]

--- a/src/Pure/Isar/class_target.ML	Sat Jan 17 08:29:40 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Sat Jan 17 08:29:54 2009 +0100
@@ -8,31 +8,27 @@
 sig
   (*classes*)
   val register: class -> class list -> ((string * typ) * (string * typ)) list
-    -> sort -> term list -> morphism
-    -> thm option -> thm option -> thm -> theory -> theory
+    -> sort -> morphism -> thm option -> thm option -> thm
+    -> theory -> theory
   val register_subclass: class * class -> thm option
     -> theory -> theory
 
+  val is_class: theory -> class -> bool
+  val base_sort: theory -> class -> sort
+  val rules: theory -> class -> thm option * thm
+  val these_params: theory -> sort -> (string * (class * (string * typ))) list
+  val these_defs: theory -> sort -> thm list
+  val print_classes: theory -> unit
+
   val begin: class list -> sort -> Proof.context -> Proof.context
   val init: class -> theory -> Proof.context
   val declare: class -> Properties.T
     -> (string * mixfix) * term -> theory -> theory
   val abbrev: class -> Syntax.mode -> Properties.T
     -> (string * mixfix) * term -> theory -> theory
+  val class_prefix: string -> string
   val refresh_syntax: class -> Proof.context -> Proof.context
 
-  val intro_classes_tac: thm list -> tactic
-  val default_intro_tac: Proof.context -> thm list -> tactic
-
-  val class_prefix: string -> string
-  val is_class: theory -> class -> bool
-  val these_params: theory -> sort -> (string * (class * (string * typ))) list
-  val these_defs: theory -> sort -> thm list
-  val eq_morph: theory -> thm list -> morphism
-  val base_sort: theory -> class -> sort
-  val rules: theory -> class -> thm option * thm
-  val print_classes: theory -> unit
-
   (*instances*)
   val init_instantiation: string list * (string * sort) list * sort
     -> theory -> local_theory
@@ -50,6 +46,9 @@
   val pretty_instantiation: local_theory -> Pretty.T
   val type_name: string -> string
 
+  val intro_classes_tac: thm list -> tactic
+  val default_intro_tac: Proof.context -> thm list -> tactic
+
   (*old axclass layer*)
   val axclass_cmd: bstring * xstring list
     -> (Attrib.binding * string list) list
@@ -116,8 +115,6 @@
   consts: (string * string) list
     (*locale parameter ~> constant name*),
   base_sort: sort,
-  inst: term list
-    (*canonical interpretation*),
   base_morph: Morphism.morphism
     (*static part of canonical morphism*),
   assm_intro: thm option,
@@ -130,22 +127,22 @@
 
 };
 
-fun rep_class_data (ClassData d) = d;
-fun mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
+fun rep_class_data (ClassData data) = data;
+fun mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
     (defs, operations)) =
-  ClassData { consts = consts, base_sort = base_sort, inst = inst,
+  ClassData { consts = consts, base_sort = base_sort,
     base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
     defs = defs, operations = operations };
-fun map_class_data f (ClassData { consts, base_sort, inst, base_morph, assm_intro,
+fun map_class_data f (ClassData { consts, base_sort, base_morph, assm_intro,
     of_class, axiom, defs, operations }) =
-  mk_class_data (f ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
+  mk_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
     (defs, operations)));
 fun merge_class_data _ (ClassData { consts = consts,
-    base_sort = base_sort, inst = inst, base_morph = base_morph, assm_intro = assm_intro,
+    base_sort = base_sort, base_morph = base_morph, assm_intro = assm_intro,
     of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
-  ClassData { consts = _, base_sort = _, inst = _, base_morph = _, assm_intro = _,
+  ClassData { consts = _, base_sort = _, base_morph = _, assm_intro = _,
     of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
-  mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
+  mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
     (Thm.merge_thms (defs1, defs2),
       AList.merge (op =) (K true) (operations1, operations2)));
 
@@ -170,11 +167,8 @@
 val is_class = is_some oo lookup_class_data;
 
 val ancestry = Graph.all_succs o ClassData.get;
-
 val heritage = Graph.all_preds o ClassData.get;
 
-fun the_inst thy = #inst o the_class_data thy;
-
 fun these_params thy =
   let
     fun params class =
@@ -187,34 +181,22 @@
       end;
   in maps params o ancestry thy end;
 
-fun these_assm_intros thy =
+val base_sort = #base_sort oo the_class_data;
+
+fun rules thy class =
+  let val { axiom, of_class, ... } = the_class_data thy class
+  in (axiom, of_class) end;
+
+fun all_assm_intros thy =
   Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
     ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
 
-fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
-
-fun these_operations thy =
-  maps (#operations o the_class_data thy) o ancestry thy;
-
-val base_sort = #base_sort oo the_class_data;
-
-fun rules thy class = let
-    val { axiom, of_class, ... } = the_class_data thy class
-  in (axiom, of_class) end;
+fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
+fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
 
-val class_prefix = Logic.const_of_class o Sign.base_name;
-
-fun class_binding_morph class =
-  Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
-
-fun eq_morph thy thms = (*FIXME how general is this?*)
-  Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms [])
-  $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms);
-
-fun morphism thy class =
-  let
-    val { base_morph, defs, ... } = the_class_data thy class;
-  in base_morph $> eq_morph thy defs end;
+val base_morphism = #base_morph oo the_class_data;
+fun morphism thy class = base_morphism thy class
+  $> Element.eq_morphism thy (these_defs thy [class]);
 
 fun print_classes thy =
   let
@@ -236,8 +218,6 @@
       (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
       (SOME o Pretty.block) [Pretty.str "supersort: ",
         (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
-      if is_class thy class then (SOME o Pretty.str)
-        ("locale: " ^ Locale.extern thy class) else NONE,
       ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
           (Pretty.str "parameters:" :: ps)) o map mk_param
         o these o Option.map #params o try (AxClass.get_info thy)) class,
@@ -254,18 +234,26 @@
 
 (* updaters *)
 
-fun register class superclasses params base_sort inst morph
+fun register class sups params base_sort morph
     axiom assm_intro of_class thy =
   let
     val operations = map (fn (v_ty as (_, ty), (c, _)) =>
       (c, (class, (ty, Free v_ty)))) params;
     val add_class = Graph.new_node (class,
         mk_class_data (((map o pairself) fst params, base_sort,
-          inst, morph, assm_intro, of_class, axiom), ([], operations)))
-      #> fold (curry Graph.add_edge class) superclasses;
+          morph, assm_intro, of_class, axiom), ([], operations)))
+      #> fold (curry Graph.add_edge class) sups;
   in ClassData.map add_class thy end;
 
+fun activate_defs class thms thy =
+  let
+    val eq_morph = Element.eq_morphism thy thms;
+    fun amend cls thy = Locale.amend_registration eq_morph
+      (cls, morphism thy cls) thy;
+  in fold amend (heritage thy [class]) thy end;
+
 fun register_operation class (c, (t, some_def)) thy =
+  (*FIXME 2009 does this still also work for abbrevs?*)
   let
     val base_sort = base_sort thy class;
     val prep_typ = map_type_tfree
@@ -279,12 +267,11 @@
       (fn (defs, operations) =>
         (fold cons (the_list some_def) defs,
           (c, (class, (ty', t'))) :: operations))
+    |> is_some some_def ? activate_defs class (the_list some_def)
   end;
 
-
-(** tactics and methods **)
-
 fun register_subclass (sub, sup) thms thy =
+  (*FIXME should also add subclass interpretation*)
   let
     val of_class = (snd o rules thy) sup;
     val intro = case thms
@@ -293,46 +280,15 @@
           ([], [sub])], []) of_class;
     val classrel = (intro OF (the_list o fst o rules thy) sub)
       |> Thm.close_derivation;
-    (*FIXME generic amend operation for classes*)
-    val amendments = map (fn class => (class, morphism thy class))
-      (heritage thy [sub]);
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub]);
-    val defs_morph = eq_morph thy (these_defs thy diff_sort);
   in
     thy
     |> AxClass.add_classrel classrel
     |> ClassData.map (Graph.add_edge (sub, sup))
-    |> fold (Locale.amend_registration defs_morph) amendments
-  end;
-
-fun intro_classes_tac facts st =
-  let
-    val thy = Thm.theory_of_thm st;
-    val classes = Sign.all_classes thy;
-    val class_trivs = map (Thm.class_triv thy) classes;
-    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
-    val assm_intros = these_assm_intros thy;
-  in
-    Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
+    |> activate_defs sub (these_defs thy diff_sort)
   end;
 
-fun default_intro_tac ctxt [] =
-      intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE
-      Locale.intro_locales_tac true ctxt []
-  | default_intro_tac _ _ = no_tac;
-
-fun default_tac rules ctxt facts =
-  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
-    default_intro_tac ctxt facts;
-
-val _ = Context.>> (Context.map_theory
-  (Method.add_methods
-   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
-      "back-chain introduction rules of classes"),
-    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
-      "apply some intro/elim rule")]));
-
 
 (** classes and class target **)
 
@@ -393,35 +349,33 @@
 
 (* class target *)
 
+val class_prefix = Logic.const_of_class o Sign.base_name;
+
 fun declare class pos ((c, mx), dict) thy =
   let
     val prfx = class_prefix class;
     val thy' = thy |> Sign.add_path prfx;
+      (*FIXME 2009 use proper name morphism*)
     val morph = morphism thy' class;
-    val inst = the_inst thy' class;
     val params = map (apsnd fst o snd) (these_params thy' [class]);
-    val amendments = map (fn class => (class, morphism thy' class))
-      (heritage thy' [class]);
 
     val c' = Sign.full_bname thy' c;
     val dict' = Morphism.term morph dict;
     val ty' = Term.fastype_of dict';
     val ty'' = Type.strip_sorts ty';
+      (*FIXME 2009 the tinkering with theorems here is a mess*)
     val def_eq = Logic.mk_equals (Const (c', ty'), dict');
-    (*FIXME a mess*)
-    fun amend def def' (class, morph) thy =
-      Locale.amend_registration (eq_morph thy [Thm.varifyT def])
-        (class, morph) thy;
     fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
   in
     thy'
     |> Sign.declare_const pos ((Binding.name c, ty''), mx) |> snd
-    |> Thm.add_def false false (c, def_eq)
+    |> Thm.add_def false false (c, def_eq) (*FIXME 2009 name of theorem*)
+      (*FIXME 2009 add_def should accept binding*)
     |>> Thm.symmetric
     ||>> get_axiom
     |-> (fn (def, def') => register_operation class (c', (dict', SOME (Thm.symmetric def')))
-      #> fold (amend def def') amendments
-      #> PureThy.store_thm (c ^ "_raw", def') (*FIXME name*)
+      #> PureThy.store_thm (c ^ "_raw", def') (*FIXME 2009 name of theorem*)
+         (*FIXME 2009 store_thm etc. should accept binding*)
       #> snd)
     |> Sign.restore_naming thy
     |> Sign.add_const_constraint (c', SOME ty')
@@ -522,7 +476,7 @@
 
 fun type_name "*" = "prod"
   | type_name "+" = "sum"
-  | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
+  | type_name s = sanatize_name (NameSpace.base s);
 
 fun resort_terms pp algebra consts constraints ts =
   let
@@ -638,5 +592,35 @@
       (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
   end;
 
+
+(** tactics and methods **)
+
+fun intro_classes_tac facts st =
+  let
+    val thy = Thm.theory_of_thm st;
+    val classes = Sign.all_classes thy;
+    val class_trivs = map (Thm.class_triv thy) classes;
+    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
+    val assm_intros = all_assm_intros thy;
+  in
+    Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
+  end;
+
+fun default_intro_tac ctxt [] =
+      intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE
+      Locale.intro_locales_tac true ctxt []
+  | default_intro_tac _ _ = no_tac;
+
+fun default_tac rules ctxt facts =
+  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
+    default_intro_tac ctxt facts;
+
+val _ = Context.>> (Context.map_theory
+  (Method.add_methods
+   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
+      "back-chain introduction rules of classes"),
+    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
+      "apply some intro/elim rule")]));
+
 end;