# HG changeset patch
# User haftmann
# Date 1225958988 -3600
# Node ID 238f9966c80eb12d24ca9c4938fba872727fed44
# Parent  1992553cccfed69abc652da2677feb63633c5caf
class morphism stemming from locale interpretation

diff -r 1992553cccfe -r 238f9966c80e src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Nov 03 14:15:25 2008 +0100
+++ b/src/Pure/Isar/class.ML	Thu Nov 06 09:09:48 2008 +0100
@@ -18,10 +18,6 @@
     -> (string * mixfix) * term -> theory -> theory
   val abbrev: class -> Syntax.mode -> Properties.T
     -> (string * mixfix) * term -> theory -> theory
-  val note: class -> string
-    -> (Attrib.binding * (thm list * Attrib.src list) list) list
-    -> theory -> (bstring * thm list) list * theory
-  val declaration: class -> declaration -> theory -> theory
   val refresh_syntax: class -> Proof.context -> Proof.context
 
   val intro_classes_tac: thm list -> tactic
@@ -67,10 +63,10 @@
 (** auxiliary **)
 
 fun prove_interpretation tac prfx_atts expr inst =
-  Locale.interpretation_i I prfx_atts expr inst #> snd
-  #> Proof.global_terminal_proof
+  Locale.interpretation_i I prfx_atts expr inst
+  ##> Proof.global_terminal_proof
       (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
-  #> ProofContext.theory_of;
+  ##> ProofContext.theory_of;
 
 fun prove_interpretation_in tac after_qed (name, expr) =
   Locale.interpretation_in_locale
@@ -79,6 +75,28 @@
       (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   #> ProofContext.theory_of;
 
+val class_prefix = Logic.const_of_class o Sign.base_name;
+
+fun activate_class_morphism thy class inst morphism =
+  Locale.get_interpret_morph thy (class_prefix class) "" morphism class inst;
+
+fun prove_class_interpretation class inst consts hyp_facts def_facts thy =
+  let
+    val constraints = map (fn (class, c) => map_atyps (K (TFree (Name.aT,
+      [class]))) (Sign.the_const_type thy c)) consts;
+    val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
+    fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
+    fun tac ctxt = ALLGOALS (ProofContext.fact_tac (hyp_facts @ def_facts)
+      ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n));
+    val prfx = class_prefix class;
+  in
+    thy
+    |> fold2 add_constraint (map snd consts) no_constraints
+    |> prove_interpretation tac (false, prfx) (Locale.Locale class)
+          (map SOME inst, map (pair (Attrib.no_binding) o Thm.prop_of) def_facts)
+    ||> fold2 add_constraint (map snd consts) constraints
+  end;
+
 
 (** primitive axclass and instance commands **)
 
@@ -127,18 +145,23 @@
 (** class data **)
 
 datatype class_data = ClassData of {
+
+  (* static part *)
   consts: (string * string) list
     (*locale parameter ~> constant name*),
   base_sort: sort,
-  inst: term option list
+  inst: term list
     (*canonical interpretation*),
-  morphism: theory -> thm list -> morphism,
-    (*partial morphism of canonical interpretation*)
+  morphism: Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))
+    (*morphism cookie of canonical interpretation*),
   assm_intro: thm option,
   of_class: thm,
   axiom: thm option,
+  
+  (* dynamic part *)
   defs: thm list,
   operations: (string * (class * (typ * term))) list
+
 };
 
 fun rep_class_data (ClassData d) = d;
@@ -147,8 +170,8 @@
   ClassData { consts = consts, base_sort = base_sort, inst = inst,
     morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
     defs = defs, operations = operations };
-fun map_class_data f (ClassData { consts, base_sort, inst, morphism,
-    assm_intro, of_class, axiom, defs, operations }) =
+fun map_class_data f (ClassData { consts, base_sort, inst, morphism, assm_intro,
+    of_class, axiom, defs, operations }) =
   mk_class_data (f ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
     (defs, operations)));
 fun merge_class_data _ (ClassData { consts = consts,
@@ -182,6 +205,8 @@
 
 val ancestry = Graph.all_succs o ClassData.get;
 
+fun the_inst thy = #inst o the_class_data thy;
+
 fun these_params thy =
   let
     fun params class =
@@ -194,17 +219,20 @@
       end;
   in maps params o ancestry thy end;
 
-fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
-
-fun morphism thy class = #morphism (the_class_data thy class) thy (these_defs thy [class]);
-
 fun these_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;
 
+fun morphism thy class =
+  let
+    val { inst, morphism, ... } = the_class_data thy class;
+  in activate_class_morphism thy class inst morphism end;
+
 fun print_classes thy =
   let
     val ctxt = ProofContext.init thy;
@@ -250,7 +278,7 @@
       (c, (class, (ty, Free v_ty)))) params;
     val add_class = Graph.new_node (class,
         mk_class_data (((map o pairself) fst params, base_sort,
-          map (SOME o Const) inst, phi, assm_intro, of_class, axiom), ([], operations)))
+          inst, phi, assm_intro, of_class, axiom), ([], operations)))
       #> fold (curry Graph.add_edge class) superclasses;
   in ClassData.map add_class thy end;
 
@@ -273,65 +301,38 @@
 
 (** rule calculation, tactics and methods **)
 
-val class_prefix = Logic.const_of_class o Sign.base_name;
+fun calculate_axiom thy sups base_sort assm_axiom param_map class =
+  case Locale.intros thy class
+   of (_, []) => assm_axiom
+    | (_, [intro]) =>
+      let
+        fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
+          (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
+            (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
+              Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
+        val axiom_premises = map_filter (#axiom o the_class_data thy) sups
+          @ the_list assm_axiom;
+      in intro
+        |> instantiate thy [class]
+        |> (fn thm => thm OF axiom_premises)
+        |> Drule.standard'
+        |> Thm.close_derivation
+        |> SOME
+      end;
 
-fun calculate sups base_sort assm_axiom param_map class thy =
+fun calculate_rules thy phi sups base_sort param_map axiom class =
   let
-    (*static parts of morphism*)
-    val subst_typ = map_type_tfree (fn (v, sort) =>
-          if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort));
-    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) param_map v
-         of SOME (c, _) => Const (c, ty)
-          | NONE => t)
-      | subst_aterm t = t;
     fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
       (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
         (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
           Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
-    (*fun inst thy sort thm = (tracing (makestring thm); instantiate thy sort thm);
-    val instantiate = inst;*)
-    val (proto_assm_intro, locale_intro) = Locale.intros thy class
-      |> pairself (try the_single);
-    val axiom_premises = map_filter (#axiom o the_class_data thy) sups
-      @ the_list assm_axiom;
-    val axiom = locale_intro
-      |> Option.map (Thm.close_derivation o Drule.standard' o (fn thm => thm OF axiom_premises) o instantiate thy [class])
-      |> (fn x as SOME _ => x | NONE => assm_axiom);
-    val lift_axiom = case axiom
-     of SOME axiom => (fn thm => ((*tracing "-(morphism)-";
-          tracing (makestring thm);
-          tracing (makestring axiom);*)
-          Thm.implies_elim thm axiom))
-      | NONE => I;
-
-    (*dynamic parts of morphism*)
-    fun avoid_a thy thm =
-      let
-        val tvars = Term.add_tvars (Thm.prop_of thm) [];
-        val thm' = case AList.lookup (op =) tvars (Name.aT, 0)
-         of SOME sort => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o rpair sort o rpair 0)
-              (Name.aT, Name.variant (map (fst o fst) tvars) Name.aT)], []) thm
-          | NONE => thm;
-      in thm' end;
-    fun rew_term thy defs = Pattern.rewrite_term thy
-      (map (Logic.dest_equals o Thm.prop_of) defs) [];
-    fun subst_term thy defs = map_aterms subst_aterm #> rew_term thy defs
-      #> map_types subst_typ;
-    fun subst_thm thy defs = Drule.zero_var_indexes #> avoid_a thy
-      #> Drule.standard' #> instantiate thy [class] #> lift_axiom
-      #> MetaSimplifier.rewrite_rule defs;
-    fun morphism thy defs =
-      Morphism.typ_morphism subst_typ
-      $> Morphism.term_morphism (subst_term thy defs)
-      $> Morphism.thm_morphism (subst_thm thy defs);
-
-    (*class rules*)
     val defs = these_defs thy sups;
-    val assm_intro = proto_assm_intro
-      |> Option.map (instantiate thy base_sort)
-      |> Option.map (MetaSimplifier.rewrite_rule defs)
-      |> Option.map Thm.close_derivation;
-    val class_intro = (#intro o AxClass.get_info thy) class;
+    val assm_intro = Locale.intros thy class
+      |> fst
+      |> map (instantiate thy base_sort)
+      |> map (MetaSimplifier.rewrite_rule defs)
+      |> map Thm.close_derivation
+      |> try the_single;
     val fixate = Thm.instantiate
       (map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)),
         (TVar ((Name.aT, 0), base_sort), TFree (Name.aT, base_sort))], [])
@@ -348,39 +349,11 @@
         |> (map_types o map_atyps o K) (TFree (Name.aT, base_sort))
         |> (Thm.assume o Thm.cterm_of thy)
         |> replicate num_trivs;
-    val of_class = (fixate class_intro OF of_class_sups OF locale_dests OF pred_trivs)
+    val axclass_intro = (#intro o AxClass.get_info thy) class;
+    val of_class = (fixate axclass_intro OF of_class_sups OF locale_dests OF pred_trivs)
       |> Drule.standard'
       |> Thm.close_derivation;
-    val this_intro = assm_intro |> the_default class_intro;
-  in
-    thy
-    |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN)
-    |> PureThy.store_thm (AxClass.introN, this_intro)
-    |> snd
-    |> Sign.restore_naming thy
-    |> pair (morphism, axiom, assm_intro, of_class)
-  end;
-
-fun class_interpretation class facts defs thy = thy;
-
-fun class_interpretation class facts defs thy =
-  let
-    val consts = map (apsnd fst o snd) (these_params thy [class]);
-    val constraints = map (fn (class, c) => map_atyps (K (TFree (Name.aT,
-      [class]))) (Sign.the_const_type thy c)) consts;
-    val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
-    fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
-    val inst = (#inst o the_class_data thy) class;
-    fun tac ctxt = ALLGOALS (ProofContext.fact_tac facts
-      ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n));
-    val prfx = class_prefix class;
-  in
-    thy
-    |> fold2 add_constraint (map snd consts) no_constraints
-    |> prove_interpretation tac (false, prfx) (Locale.Locale class)
-          (inst, map (fn def => (Attrib.no_binding, def)) defs)
-    |> fold2 add_constraint (map snd consts) constraints
-  end;
+  in (assm_intro, of_class) end;
 
 fun prove_subclass (sub, sup) some_thm thy =
   let
@@ -399,6 +372,13 @@
     |> ClassData.map (Graph.add_edge (sub, sup))
   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;
+
 fun intro_classes_tac facts st =
   let
     val thy = Thm.theory_of_thm st;
@@ -490,6 +470,8 @@
     val prfx = class_prefix class;
     val thy' = thy |> Sign.add_path prfx;
     val phi = morphism thy' class;
+    val inst = the_inst thy' class;
+    val params = map (apsnd fst o snd) (these_params thy' [class]);
 
     val c' = Sign.full_name thy' c;
     val dict' = Morphism.term phi dict;
@@ -504,7 +486,10 @@
     |> Thm.add_def false false (c, def_eq)
     |>> Thm.symmetric
     ||>> get_axiom
-    |-> (fn (def, def') => class_interpretation class [def] [Thm.prop_of def]
+    |-> (fn (def, def') => prove_class_interpretation class inst params [] [def]
+      #> snd
+        (*assumption: interpretation cookie does not change
+          by adding equations to interpretation*)
       #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
       #> PureThy.store_thm (c ^ "_raw", def')
       #> snd)
@@ -532,22 +517,6 @@
     |> Sign.restore_naming thy
   end;
 
-fun note class kind facts thy =
-  let
-    val phi = morphism thy class;
-    val facts' = facts
-      |> PureThy.map_facts (Morphism.thm phi) 
-      |> Attrib.map_facts (Attrib.attribute_i thy);
-  in
-    thy
-    |> Sign.add_path (class_prefix class)
-    |> PureThy.note_thmss kind facts'
-    ||> Sign.restore_naming thy
-  end;
-
-fun declaration class decl thy =
-  Context.theory_map (decl (morphism thy class)) thy;
-
 
 (* class definition *)
 
@@ -593,12 +562,13 @@
 val read_class_spec = gen_class_spec Sign.intern_class Locale.read_expr;
 val check_class_spec = gen_class_spec (K I) Locale.cert_expr;
 
-fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
+fun add_consts bname class base_sort sups supparams global_syntax thy =
   let
     val supconsts = map fst 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]);
     val all_params = map fst (Locale.parameters_of thy class);
+    val raw_params = (snd o chop (length supparams)) all_params;
     fun add_const (v, raw_ty) thy =
       let
         val c = Sign.full_name thy v;
@@ -612,12 +582,16 @@
         |> snd
         |> pair ((v, ty), (c, ty'))
       end;
-    fun add_consts raw_params thy =
-      thy
-      |> Sign.add_path (Logic.const_of_class bname)
-      |> fold_map add_const raw_params
-      ||> Sign.restore_naming thy
-      |-> (fn params => pair (supconsts @ (map o apfst) fst params, params));
+  in
+    thy
+    |> Sign.add_path (Logic.const_of_class bname)
+    |> fold_map add_const raw_params
+    ||> Sign.restore_naming thy
+    |-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
+  end;
+
+fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
+  let
     fun globalize param_map = map_aterms
       (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
         | t => t);
@@ -629,14 +603,14 @@
       | [thm] => SOME thm;
   in
     thy
-    |> add_consts ((snd o chop (length supparams)) all_params)
+    |> add_consts bname class base_sort sups supparams global_syntax
     |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
           (map (fst o snd) params)
           [((Name.binding (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)]
     #> snd
     #> `get_axiom
     #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
-    #> pair (param_map, params, assm_axiom)))
+    #> pair (map (Const o snd) param_map, param_map, params, assm_axiom)))
   end;
 
 fun gen_class prep_spec bname raw_supclasses raw_elems thy =
@@ -644,21 +618,26 @@
     val class = Sign.full_name thy bname;
     val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) =
       prep_spec thy raw_supclasses raw_elems;
+    val supconsts = map (apsnd fst o snd) (these_params thy sups);
   in
     thy
     |> Locale.add_locale_i "" bname mergeexpr elems
     |> snd
     |> ProofContext.theory_of
     |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
-    |-> (fn (param_map, params, assm_axiom) =>
-        calculate sups base_sort assm_axiom param_map class
-    #-> (fn (morphism, axiom, assm_intro, of_class) =>
-        add_class_data ((class, sups), (params, base_sort,
-          map snd param_map, morphism, axiom, assm_intro, of_class))
-    (*#> `(fn thy => Locale.facts_of thy class)
-    #-> (fn facts => fold_map (note class Thm.assumptionK) facts
-    #> snd*)
-    #> class_interpretation class (the_list axiom) []))
+    |-> (fn (inst, param_map, params, assm_axiom) =>
+        `(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class)
+    #-> (fn axiom =>
+        prove_class_interpretation class inst
+          (supconsts @ map (pair class o fst o snd) params) (the_list axiom) []
+    #-> (fn morphism =>
+        `(fn thy => activate_class_morphism thy class inst morphism)
+    #-> (fn phi =>
+        `(fn thy => calculate_rules thy phi sups base_sort param_map axiom class)
+    #-> (fn (assm_intro, of_class) =>
+        add_class_data ((class, sups), (params, base_sort, inst,
+          morphism, axiom, assm_intro, of_class))
+    #> fold (note_assm_intro class) (the_list assm_intro))))))
     |> init class
     |> pair class
   end;