# HG changeset patch
# User haftmann
# Date 1231679912 -3600
# Node ID 7b09624f6bc1416b1f590e6ffc8bfac0c213f651
# Parent  4848cb75d5ea64395566ce3e90e1aef84021f8f6# Parent  28d7d7572b812732793ca87bd4cb551ae5d1fb33
merged

diff -r 4848cb75d5ea -r 7b09624f6bc1 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Jan 11 13:48:11 2009 +0100
+++ b/src/Pure/Isar/class.ML	Sun Jan 11 14:18:32 2009 +0100
@@ -7,8 +7,8 @@
 signature CLASS =
 sig
   include CLASS_TARGET
-    (*FIXME the split in class_target.ML, theory_target.ML and
-      ML is artificial*)
+    (*FIXME the split into class_target.ML, theory_target.ML and
+      class.ML is artificial*)
 
   val class: bstring -> class list -> Element.context_i list
     -> theory -> string * local_theory
@@ -45,7 +45,25 @@
         |> SOME
       end;
 
-fun calculate_rules thy phi sups base_sort param_map axiom class =
+fun raw_morphism thy class param_map some_axiom =
+  let
+    val ctxt = ProofContext.init thy;
+    val some_wit = case some_axiom
+     of SOME axiom => SOME (Element.prove_witness ctxt
+          (Logic.unvarify (Thm.prop_of axiom))
+            (ALLGOALS (ProofContext.fact_tac [axiom])))
+      | NONE => NONE;
+    val instT = Symtab.empty |> Symtab.update ("'a", TFree ("'a", [class]));
+    val inst = Symtab.make ((map o apsnd) Const param_map);
+  in case some_wit
+   of SOME wit => Element.inst_morphism thy (instT, inst)
+        $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class))
+        $> Element.satisfy_morphism [wit]
+    | NONE => Element.inst_morphism thy (instT, inst)
+        $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class))
+  end;
+
+fun calculate_rules thy morph sups base_sort param_map axiom class =
   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)
@@ -200,14 +218,13 @@
     #-> (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 thy => raw_morphism thy class param_map axiom)
+    #-> (fn 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
-          morphism axiom assm_intro of_class
-    #> fold (note_assm_intro class) (the_list assm_intro))))))
+          morph axiom assm_intro of_class
+    #> fold (note_assm_intro class) (the_list assm_intro)))))
     |> TheoryTarget.init (SOME class)
     |> pair class
   end;
diff -r 4848cb75d5ea -r 7b09624f6bc1 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sun Jan 11 13:48:11 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Sun Jan 11 14:18:32 2009 +0100
@@ -7,9 +7,8 @@
 signature CLASS_TARGET =
 sig
   (*classes*)
-  type raw_morphism = morphism * ((typ Vartab.table * typ list) *  (term Vartab.table * term list));
   val register: class -> class list -> ((string * typ) * (string * typ)) list
-    -> sort -> term list -> raw_morphism
+    -> sort -> term list -> morphism
     -> thm option -> thm option -> thm -> theory -> theory
 
   val begin: class list -> sort -> Proof.context -> Proof.context
@@ -22,10 +21,8 @@
 
   val intro_classes_tac: thm list -> tactic
   val default_intro_tac: Proof.context -> thm list -> tactic
-  val activate_class_morphism: theory -> class -> term list
-    -> raw_morphism -> morphism
   val prove_class_interpretation: class -> term list -> (class * string) list
-    -> thm list -> thm list -> theory -> raw_morphism * theory
+    -> thm list -> thm list -> theory -> theory
   val prove_subclass_relation: class * class -> thm option -> theory -> theory
 
   val class_prefix: string -> string
@@ -97,19 +94,6 @@
 end;
 
 
-(** auxiliary **)
-
-val class_prefix = Logic.const_of_class o Sign.base_name;
-
-fun class_name_morphism class =
-  Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
-
-type raw_morphism = morphism * ((typ Vartab.table * typ list) *  (term Vartab.table * term list));
-
-fun activate_class_morphism thy class inst morphism =
-  Locale_Layer.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;
-
-
 (** primitive axclass and instance commands **)
 
 fun axclass_cmd (class, raw_superclasses) raw_specs thy =
@@ -164,8 +148,8 @@
   base_sort: sort,
   inst: term list
     (*canonical interpretation*),
-  morphism: Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))
-    (*morphism cookie of canonical interpretation*),
+  base_morph: Morphism.morphism
+    (*static part of canonical morphism*),
   assm_intro: thm option,
   of_class: thm,
   axiom: thm option,
@@ -177,21 +161,21 @@
 };
 
 fun rep_class_data (ClassData d) = d;
-fun mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
+fun mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
     (defs, operations)) =
   ClassData { consts = consts, base_sort = base_sort, inst = inst,
-    morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
+    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, morphism, assm_intro,
+fun map_class_data f (ClassData { consts, base_sort, inst, base_morph, assm_intro,
     of_class, axiom, defs, operations }) =
-  mk_class_data (f ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
+  mk_class_data (f ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
     (defs, operations)));
 fun merge_class_data _ (ClassData { consts = consts,
-    base_sort = base_sort, inst = inst, morphism = morphism, assm_intro = assm_intro,
+    base_sort = base_sort, inst = inst, base_morph = base_morph, assm_intro = assm_intro,
     of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
-  ClassData { consts = _, base_sort = _, inst = _, morphism = _, assm_intro = _,
+  ClassData { consts = _, base_sort = _, inst = _, base_morph = _, assm_intro = _,
     of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
-  mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
+  mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
     (Thm.merge_thms (defs1, defs2),
       AList.merge (op =) (K true) (operations1, operations2)));
 
@@ -246,10 +230,19 @@
     val { axiom, of_class, ... } = the_class_data thy class
   in (axiom, of_class) end;
 
+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 morphism thy class =
   let
-    val { inst, morphism, ... } = the_class_data thy class;
-  in activate_class_morphism thy class inst morphism end;
+    val { base_morph, defs, ... } = the_class_data thy class;
+  in
+    base_morph 
+    $> Morphism.term_morphism (MetaSimplifier.rewrite_term thy defs [])
+    $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule defs)
+  end;
 
 fun print_classes thy =
   let
@@ -289,23 +282,23 @@
 
 (* updaters *)
 
-fun register class superclasses params base_sort inst phi
+fun register class superclasses params base_sort inst 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, phi, assm_intro, of_class, axiom), ([], operations)))
+          inst, morph, assm_intro, of_class, axiom), ([], operations)))
       #> fold (curry Graph.add_edge class) superclasses;
   in ClassData.map add_class thy end;
 
 fun register_operation class (c, (t, some_def)) thy =
   let
     val base_sort = base_sort thy class;
-    val prep_typ = map_type_tvar
-      (fn (vi as (v, _), sort) => if Name.aT = v
-        then TFree (v, base_sort) else TVar (vi, sort));
+    val prep_typ = map_type_tfree
+      (fn (v, sort) => if Name.aT = v
+        then TFree (v, base_sort) else TVar ((v, 0), sort));
     val t' = map_types prep_typ t;
     val ty' = Term.fastype_of t';
   in
@@ -331,9 +324,10 @@
   in
     thy
     |> fold2 add_constraint (map snd consts) no_constraints
-    |> Locale_Layer.prove_interpretation tac (class_name_morphism class) (Locale_Layer.Locale class)
+    |> Locale_Layer.prove_interpretation tac (class_binding_morph class) (Locale_Layer.Locale class)
           (map SOME inst, map (pair (Attrib.empty_binding) o Thm.prop_of) def_facts)
-    ||> fold2 add_constraint (map snd consts) constraints
+    |> snd
+    |> fold2 add_constraint (map snd consts) constraints
   end;
 
 fun prove_subclass_relation (sub, sup) some_thm thy =
@@ -444,16 +438,15 @@
   let
     val prfx = class_prefix class;
     val thy' = thy |> Sign.add_path prfx;
-    val phi = morphism thy' class;
+    val morph = morphism thy' class;
     val inst = the_inst thy' class;
     val params = map (apsnd fst o snd) (these_params thy' [class]);
 
     val c' = Sign.full_bname thy' c;
-    val dict' = Morphism.term phi dict;
-    val dict_def = map_types Logic.unvarifyT dict';
-    val ty' = Term.fastype_of dict_def;
+    val dict' = Morphism.term morph dict;
+    val ty' = Term.fastype_of dict';
     val ty'' = Type.strip_sorts ty';
-    val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
+    val def_eq = Logic.mk_equals (Const (c', ty'), dict');
     fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
   in
     thy'
@@ -462,9 +455,6 @@
     |>> Thm.symmetric
     ||>> get_axiom
     |-> (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)
@@ -649,9 +639,9 @@
 
 fun prove_instantiation_exit_result f tac x lthy =
   let
-    val phi = ProofContext.export_morphism lthy
+    val morph = ProofContext.export_morphism lthy
       (ProofContext.init (ProofContext.theory_of lthy));
-    val y = f phi x;
+    val y = f morph x;
   in
     lthy
     |> prove_instantiation_exit (fn ctxt => tac ctxt y)
diff -r 4848cb75d5ea -r 7b09624f6bc1 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Jan 11 13:48:11 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Jan 11 14:18:32 2009 +0100
@@ -12,10 +12,10 @@
   type expression = string expr * (Binding.T * string option * mixfix) list;
 
   (* Processing of context statements *)
+  val cert_statement: Element.context_i list -> (term * term list) list list ->
+    Proof.context -> (term * term list) list list * Proof.context;
   val read_statement: Element.context list -> (string * string list) list list ->
     Proof.context ->  (term * term list) list list * Proof.context;
-  val cert_statement: Element.context_i list -> (term * term list) list list ->
-    Proof.context -> (term * term list) list list * Proof.context;
 
   (* Declaring locales *)
   val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
@@ -24,6 +24,9 @@
     theory -> string * local_theory;
 
   (* Interpretation *)
+  val cert_goal_expression: expression_i -> Proof.context ->
+    (term list list * (string * morphism) list * morphism) * Proof.context;
+
   val sublocale: string -> expression_i -> theory -> Proof.state;
   val sublocale_cmd: string -> expression -> theory -> Proof.state;
   val interpretation: expression_i -> (Attrib.binding * term) list ->
@@ -740,10 +743,11 @@
       map_filter (fn Notes notes => SOME notes | _ => NONE);
 
     val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
+    val axioms = map Element.conclude_witness b_axioms;
 
     val loc_ctxt = thy'
       |> Locale.register_locale bname (extraTs, params)
-          (asm, rev defs) ([], [])
+          (asm, rev defs) (a_intro, b_intro) axioms ([], []) 
           (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev)
       |> TheoryTarget.init (SOME name)
       |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
@@ -816,12 +820,54 @@
     val ctxt = ProofContext.init thy;
 
     val ((propss, regs, export), expr_ctxt) = prep_expr expression ctxt;
-    
+
     val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
     val eq_attns = map ((apsnd o map) (prep_attr thy) o fst) equations;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     val export' = Variable.export_morphism goal_ctxt expr_ctxt;
 
+    (*** alternative code -- unclear why it does not work yet ***)
+    fun store_reg ((name, morph), thms) thy =
+      let
+        val thms' = map (Element.morph_witness export') thms;
+        val morph' = morph $> Element.satisfy_morphism thms';
+      in
+        thy
+        |> Locale.add_registration (name, (morph', export))
+        |> pair (name, morph')
+      end;
+
+    fun store_eqns_activate regs [] thy =
+          thy
+          |> fold (fn (name, morph) =>
+               Locale.activate_global_facts (name, morph $> export)) regs
+      | store_eqns_activate regs thms thys =
+          let
+            val thms' = thms |> map (Element.conclude_witness #>
+              Morphism.thm (export' $> export) #>
+              LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
+              Drule.abs_def);
+            val eq_morph =
+              Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $>
+              Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms');
+            val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
+          in
+            thy
+            |> fold (fn (name, morph) =>
+                Locale.amend_registration eq_morph (name, morph) #>
+                Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs
+            |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn th => [([th], [])]) thms')
+            |> snd
+          end;
+
+    fun after_qed results =
+      let
+        val (wits_reg, wits_eq) = split_last (prep_result (propss @ [eqns]) results);
+      in ProofContext.theory (fold_map store_reg (regs ~~ wits_reg)
+        #-> (fn regs => store_eqns_activate regs wits_eq))
+      end;
+    (*** alternative code end ***)
+
     fun store (Reg (name, morph), thms) (regs, thy) =
         let
           val thms' = map (Element.morph_witness export') thms;
diff -r 4848cb75d5ea -r 7b09624f6bc1 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sun Jan 11 13:48:11 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Sun Jan 11 14:18:32 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/local_defs.ML
-    ID:         $Id$
     Author:     Makarius
 
 Local definitions.
diff -r 4848cb75d5ea -r 7b09624f6bc1 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Jan 11 13:48:11 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Jan 11 14:18:32 2009 +0100
@@ -34,6 +34,7 @@
   val register_locale: bstring ->
     (string * sort) list * (Binding.T * typ option * mixfix) list ->
     term option * term list ->
+    thm option * thm option -> thm list ->
     (declaration * stamp) list * (declaration * stamp) list ->
     ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
     ((string * Morphism.morphism) * stamp) list -> theory -> theory
@@ -45,6 +46,8 @@
   (* Specification *)
   val defined: theory -> string -> bool
   val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
+  val intros_of: theory -> string -> thm option * thm option
+  val axioms_of: theory -> string -> thm list
   val instance_of: theory -> string -> Morphism.morphism -> term list
   val specification_of: theory -> string -> term option * term list
   val declarations_of: theory -> string -> declaration list * declaration list
@@ -118,6 +121,8 @@
     (* type and term parameters *)
   spec: term option * term list,
     (* assumptions (as a single predicate expression) and defines *)
+  intros: thm option * thm option,
+  axioms: thm list,
   (** dynamic part **)
   decls: (declaration * stamp) list * (declaration * stamp) list,
     (* type and term syntax declarations *)
@@ -127,17 +132,18 @@
     (* locale dependencies (sublocale relation) *)
 };
 
-fun mk_locale ((parameters, spec), ((decls, notes), dependencies)) =
-  Loc {parameters = parameters, spec = spec, decls = decls,
-    notes = notes, dependencies = dependencies};
-fun map_locale f (Loc {parameters, spec, decls, notes, dependencies}) =
-  mk_locale (f ((parameters, spec), ((decls, notes), dependencies)));
-fun merge_locale (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
-  Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
-    mk_locale ((parameters, spec),
-      (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
-        merge (eq_snd op =) (notes, notes')),
-          merge (eq_snd op =) (dependencies, dependencies')));
+fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
+  Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
+    decls = decls, notes = notes, dependencies = dependencies};
+fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
+  mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
+fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
+  notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
+    dependencies = dependencies', ...}) = mk_locale
+      ((parameters, spec, intros, axioms),
+        (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
+          merge (eq_snd op =) (notes, notes')),
+            merge (eq_snd op =) (dependencies, dependencies')));
 
 structure LocalesData = TheoryDataFun
 (
@@ -159,9 +165,9 @@
  of SOME (Loc loc) => loc
   | NONE => error ("Unknown locale " ^ quote name);
 
-fun register_locale bname parameters spec decls notes dependencies thy =
+fun register_locale bname parameters spec intros axioms decls notes dependencies thy =
   thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
-    mk_locale ((parameters, spec), ((decls, notes), dependencies))) #> snd);
+    mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies))) #> snd);
 
 fun change_locale name =
   LocalesData.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
@@ -175,6 +181,10 @@
 
 fun params_of thy = snd o #parameters o the_locale thy;
 
+fun intros_of thy = #intros o the_locale thy;
+
+fun axioms_of thy = #axioms o the_locale thy;
+
 fun instance_of thy name morph = params_of thy name |>
   map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);