# HG changeset patch
# User wenzelm
# Date 1164239543 -3600
# Node ID e4be91feca5086de21efe43b87b10cfaf12d7739
# Parent  7bb5de80917fa71b52e8fd74467e53afa69e792d
replaced Args.map_values/Element.map_ctxt_values by general morphism application;

diff -r 7bb5de80917f -r e4be91feca50 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Nov 23 00:52:19 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Nov 23 00:52:23 2006 +0100
@@ -212,20 +212,21 @@
     let
       val t = termify ts;
       val subs = subsumers thy t regs;
-    in (case subs of
+    in
+      (case subs of
         [] => NONE
-      | ((t', (attn, thms)) :: _) => let
+      | ((t', (attn, thms)) :: _) =>
+          let
             val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
             (* thms contain Frees, not Vars *)
-            val tinst' = tinst |> Vartab.dest
+            val tinst' = tinst |> Vartab.dest   (* FIXME Symtab.map (!?) *)
                  |> map (fn ((x, 0), (_, T)) => (x, Logic.legacy_unvarifyT T))
                  |> Symtab.make;
             val inst' = inst |> Vartab.dest
                  |> map (fn ((x, 0), (_, t)) => (x, Logic.legacy_unvarify t))
                  |> Symtab.make;
-          in
-            SOME (attn, map (Element.inst_witness thy (tinst', inst')) thms)
-          end)
+            val inst_witness = Element.morph_witness (Element.inst_morphism thy (tinst', inst'));
+          in SOME (attn, map inst_witness thms) end)
     end;
 
   (* add registration if not subsumed by ones already present,
@@ -607,12 +608,13 @@
   | unify_elemss ctxt fixed_parms elemss =
       let
         val thy = ProofContext.theory_of ctxt;
-        val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss);
-        fun inst ((((name, ps), mode), elems), env) =
-          (((name, map (apsnd (Option.map (Element.instT_type env))) ps),
-              map_mode (map (Element.instT_witness thy env)) mode),
-            map (Element.instT_ctxt thy env) elems);
-      in map inst (elemss ~~ envs) end;
+        val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss)
+          |> map (Element.instT_morphism thy);
+        fun inst ((((name, ps), mode), elems), phi) =
+          (((name, map (apsnd (Option.map (Morphism.typ phi))) ps),
+              map_mode (map (Element.morph_witness phi)) mode),
+            map (Element.morph_ctxt phi) elems);
+      in map inst (elemss ~~ phis) end;
 
 
 fun renaming xs parms = zip_options parms xs
@@ -722,7 +724,7 @@
         ((name, map (Element.rename ren) ps),
          if top
          then (map (Element.rename ren) parms,
-               map_mode (map (Element.rename_witness ren)) mode)
+               map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode)
          else (parms, mode));
 
     (* add (name, ps) and its registrations, recursively; adjust hyps of witnesses *)
@@ -744,11 +746,14 @@
                  map (Element.transfer_witness thy) wits)) regs;
             val new_regs = regs';
             val new_ids = map fst new_regs;
-            val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
+            val new_idTs =
+              map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
 
             val new_wits = new_regs |> map (#2 #> map
-              (Element.instT_witness thy env #> Element.rename_witness ren #>
-                Element.satisfy_witness wits));
+              (Element.morph_witness
+                (Element.instT_morphism thy env $>
+                  Element.rename_morphism ren $>
+                  Element.satisfy_morphism wits)));
             val new_ids' = map (fn (id, wits) =>
                 (id, ([], Derived wits))) (new_ids ~~ new_wits);
             val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
@@ -827,12 +832,12 @@
         val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
         val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
         val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
-        val elems' = elems
-              |> map (Element.rename_ctxt ren)
-              |> map (Element.map_ctxt {var = I, typ = I, term = I, fact = I, attrib = I,
-                   name = NameSpace.qualified (space_implode "_" params)})
-              |> map (Element.instT_ctxt thy env)
-      in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
+        val eval_elem =
+           Element.morph_ctxt (Element.rename_morphism ren) #>
+           Element.map_ctxt {var = I, typ = I, term = I, fact = I, attrib = I,
+             name = NameSpace.qualified (space_implode "_" params)} #>
+           Element.morph_ctxt (Element.instT_morphism thy env);
+      in (((name, map (apsnd SOME) locale_params'), mode'), map eval_elem elems) end;
 
     (* parameters, their types and syntax *)
     val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
@@ -1083,7 +1088,7 @@
 (* for finish_elems (Int),
    remove redundant elements of derived identifiers,
    turn assumptions and definitions into facts,
-   adjust hypotheses of facts using witnesses *)
+   satisfy hypotheses of facts *)
 
 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
   | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
@@ -1092,17 +1097,17 @@
 
   | finish_derived _ _ (Derived _) (Fixes _) = NONE
   | finish_derived _ _ (Derived _) (Constrains _) = NONE
-  | finish_derived sign wits (Derived _) (Assumes asms) = asms
+  | finish_derived sign satisfy (Derived _) (Assumes asms) = asms
       |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
       |> pair Thm.assumptionK |> Notes
-      |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
-  | finish_derived sign wits (Derived _) (Defines defs) = defs
+      |> Element.morph_ctxt satisfy |> SOME
+  | finish_derived sign satisfy (Derived _) (Defines defs) = defs
       |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
       |> pair Thm.definitionK |> Notes
-      |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
+      |> Element.morph_ctxt satisfy |> SOME
 
-  | finish_derived _ wits _ (Notes facts) = Notes facts
-      |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME;
+  | finish_derived _ satisfy _ (Notes facts) = Notes facts
+      |> Element.morph_ctxt satisfy |> SOME;
 
 (* CB: for finish_elems (Ext) *)
 
@@ -1148,7 +1153,7 @@
         val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
         val text' = fold (eval_text ctxt id' false) es text;
         val es' = map_filter
-              (finish_derived (ProofContext.theory_of ctxt) wits' mode) es;
+          (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es;
       in ((text', wits'), (id', map Int es')) end
   | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
       let
@@ -1282,7 +1287,7 @@
   else name;
 
 fun prep_facts _ _ _ ctxt (Int elem) =
-      Element.map_ctxt_values I I (Thm.transfer (ProofContext.theory_of ctxt)) elem
+      Element.morph_ctxt (Morphism.transfer (ProofContext.theory_of ctxt)) elem
   | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
      {var = I, typ = I, term = I,
       name = prep_name,
@@ -1506,9 +1511,7 @@
       let
         val (insts, prems) = collect_global_witnesses thy parms ids vts;
         val attrib = Attrib.attribute_i thy;
-        val inst_atts =
-          Args.map_values I (Element.instT_type (#1 insts))
-            (Element.inst_term insts) (Element.inst_thm thy insts);
+        val inst_atts = Args.morph_values (Element.inst_morphism thy insts);
         val inst_thm =
           Drule.standard o Element.satisfy_thm prems o Element.inst_thm thy insts;
         val args' = args |> map (fn ((name, atts), bs) =>
@@ -1645,9 +1648,9 @@
 
 fun change_assumes_elemss axioms elemss =
   let
+    val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
     fun change (id as ("", _), es) =
-          fold_map assumes_to_notes
-            (map (Element.map_ctxt_values I I (Element.satisfy_thm axioms)) es)
+          fold_map assumes_to_notes (map satisfy es)
           #-> (fn es' => pair (id, es'))
       | change e = pair e;
   in
@@ -1658,9 +1661,8 @@
 
 fun change_elemss_hyps axioms elemss =
   let
-    fun change (id as ("", _), es) =
-        (id, map (fn e as Notes _ => Element.map_ctxt_values I I (Element.satisfy_thm axioms) e
-                   | e => e) es)
+    val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms);
+    fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es)
       | change e = e;
   in map change elemss end;
 
@@ -1880,9 +1882,11 @@
     let
       fun activate_elem disch (prfx, atts) (Notes (kind, facts)) thy_ctxt =
           let
+            val disch_morphism = Morphism.morphism
+              {name = I, var = I, typ = I, term = I, thm = disch};
             val facts' = facts
               (* discharge hyps in attributes *)
-              |> Attrib.map_facts (attrib thy_ctxt o Args.map_values I I I disch)
+              |> Attrib.map_facts (attrib thy_ctxt o Args.morph_values disch_morphism)
               (* append interpretation attributes *)
               |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
               (* discharge hyps *)
@@ -1908,13 +1912,14 @@
       val prems = flat (map_filter
             (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id)
               | ((_, Derived _), _) => NONE) all_elemss);
+      val satisfy = Element.satisfy_morphism prems;
       val thy_ctxt'' = thy_ctxt'
         (* add witnesses of Derived elements *)
-        |> fold (fn (id, thms) => fold (add_wit id o Element.satisfy_witness prems) thms)
+        |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness satisfy) thms)
            (map_filter (fn ((_, Assumed _), _) => NONE
               | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
 
-      val disch' = std o Element.satisfy_thm prems;  (* FIXME *)
+      val disch' = std o Morphism.thm satisfy;  (* FIXME *)
     in
       thy_ctxt''
         (* add facts to theory or context *)
@@ -2004,6 +2009,7 @@
       in Symtab.update_new (p, d) inst end;
     val inst = fold add_def not_given inst;
     val insts = (tinst, inst);
+    val inst_morphism = Element.inst_morphism thy insts;
     (* Note: insts contain no vars. *)
 
 
@@ -2016,9 +2022,9 @@
     val (_, all_elemss') = chop (length raw_params_elemss) all_elemss
     (* instantiate ids and elements *)
     val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) =>
-      ((n, map (Element.inst_term insts) ps),
-        map (fn Int e => Element.inst_ctxt thy insts e) elems)
-      |> apfst (fn id => (id, map_mode (map (Element.inst_witness thy insts)) mode)));
+      ((n, map (Morphism.term inst_morphism) ps),
+        map (fn Int e => Element.morph_ctxt inst_morphism e) elems)
+      |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
 
     (* remove fragments already registered with theory or context *)
     val new_inst_elemss = filter (fn ((id, _), _) =>
@@ -2088,7 +2094,8 @@
                 |> fold (add_witness_in_locale target id) thms
           | activate_id _ thy = thy;
 
-        fun activate_reg (vts, ((prfx, atts2), _)) thy = let
+        fun activate_reg (vts, ((prfx, atts2), _)) thy =
+          let
             val (insts, wits) = collect_global_witnesses thy fixed t_ids vts;
             fun inst_parms ps = map
                   (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
@@ -2104,7 +2111,7 @@
                 else thy
                   |> put_global_registration (name, ps') (prfx, atts2)
                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
-                     (Element.inst_witness thy insts witn) thy) thms
+                     (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
               end;
 
             fun activate_derived_id ((_, Assumed _), _) thy = thy
@@ -2123,11 +2130,11 @@
 
             fun activate_elem (Notes (kind, facts)) thy =
                 let
+                  val att_morphism = Morphism.morphism {var = I, name = I,
+                    typ = Element.instT_type (#1 insts), term = Element.inst_term insts,
+                    thm = disch o Element.inst_thm thy insts o satisfy};
                   val facts' = facts
-                      |> Attrib.map_facts (Attrib.attribute_i thy o
-                         Args.map_values I (Element.instT_type (#1 insts))
-                           (Element.inst_term insts)
-                           (disch o Element.inst_thm thy insts o satisfy))
+                      |> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism)
                       |> map (apfst (apsnd (fn a => a @ map (Attrib.attribute thy) atts2)))
                       |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
                 in
diff -r 7bb5de80917f -r e4be91feca50 src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Thu Nov 23 00:52:19 2006 +0100
+++ b/src/Pure/Tools/invoke.ML	Thu Nov 23 00:52:23 2006 +0100
@@ -67,8 +67,9 @@
 
           val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;
           val params'' = map (Thm.term_of o Drule.dest_term) res_params;
-          val elems' = elems |> map (Element.inst_ctxt thy
+          val inst = Element.morph_ctxt (Element.inst_morphism thy
             (Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params'')));
+          val elems' = map inst elems;
           val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
           val notes =
             maps (Element.facts_of thy) elems'