# HG changeset patch
# User wenzelm
# Date 1164239535 -3600
# Node ID 025ab31286d8219f65aee58aa726716759017038
# Parent  e2cc70e70b2f131f4f373f82f2662be569cdf42e
added morph_ctxt, morph_witness;
removed ctxt/witness in favour of general morphisms;

diff -r e2cc70e70b2f -r 025ab31286d8 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Nov 23 00:52:11 2006 +0100
+++ b/src/Pure/Isar/element.ML	Thu Nov 23 00:52:15 2006 +0100
@@ -25,7 +25,7 @@
     var: string * mixfix -> string * mixfix,
     typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
     attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
-  val map_ctxt_values: (typ -> typ) -> (term -> term) -> (thm -> thm) -> context_i -> context_i
+  val morph_ctxt: morphism -> context_i -> context_i
   val params_of: context_i -> (string * typ) list
   val prems_of: context_i -> term list
   val facts_of: theory -> context_i ->
@@ -35,6 +35,7 @@
   val pretty_statement: Proof.context -> string -> thm -> Pretty.T
   type witness
   val map_witness: (term * thm -> term * thm) -> witness -> witness
+  val morph_witness: morphism -> witness -> witness
   val witness_prop: witness -> term
   val witness_hyps: witness -> term list
   val assume_witness: theory -> term -> witness
@@ -49,20 +50,16 @@
   val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
   val rename_term: (string * (string * mixfix option)) list -> term -> term
   val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
-  val rename_witness: (string * (string * mixfix option)) list -> witness -> witness
-  val rename_ctxt: (string * (string * mixfix option)) list -> context_i -> context_i
+  val rename_morphism: (string * (string * mixfix option)) list -> morphism
   val instT_type: typ Symtab.table -> typ -> typ
   val instT_term: typ Symtab.table -> term -> term
   val instT_thm: theory -> typ Symtab.table -> thm -> thm
-  val instT_witness: theory -> typ Symtab.table -> witness -> witness
-  val instT_ctxt: theory -> typ Symtab.table -> context_i -> context_i
+  val instT_morphism: theory -> typ Symtab.table -> morphism
   val inst_term: typ Symtab.table * term Symtab.table -> term -> term
   val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm
-  val inst_witness: theory -> typ Symtab.table * term Symtab.table -> witness -> witness
-  val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i
+  val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism
   val satisfy_thm: witness list -> thm -> thm
-  val satisfy_witness: witness list -> witness -> witness
-  val satisfy_ctxt: witness list -> context_i -> context_i
+  val satisfy_morphism: witness list -> morphism
   val satisfy_facts: witness list ->
     ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
@@ -77,7 +74,6 @@
 structure Element: ELEMENT =
 struct
 
-
 (** language elements **)
 
 (* statement *)
@@ -113,9 +109,13 @@
    | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
       ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
 
-fun map_ctxt_values typ term thm = map_ctxt
-  {name = I, var = I, typ = typ, term = term, fact = map thm,
-    attrib = Args.map_values I typ term thm};
+fun morph_ctxt phi = map_ctxt
+ {name = Morphism.name phi,
+  var = Morphism.var phi,
+  typ = Morphism.typ phi,
+  term = Morphism.term phi,
+  fact = map (Morphism.thm phi),
+  attrib = Args.morph_values phi};
 
 
 (* logical content *)
@@ -272,6 +272,8 @@
 
 fun map_witness f (Witness witn) = Witness (f witn);
 
+fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
+
 fun witness_prop (Witness (t, _)) = t;
 fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
 
@@ -369,12 +371,8 @@
     else th |> hyps_rule (instantiate_frees thy subst)
   end;
 
-fun rename_witness ren =
-  map_witness (fn (t, th) => (rename_term ren t, rename_thm ren th));
-
-fun rename_ctxt ren =
-  map_ctxt_values I (rename_term ren) (rename_thm ren)
-  #> map_ctxt {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren};
+fun rename_morphism ren = Morphism.morphism
+  {name = I, var = rename_var ren, typ = I, term = rename_term ren, thm = rename_thm ren};
 
 
 (* instantiate types *)
@@ -399,11 +397,8 @@
     let val subst = instT_subst env th
     in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
 
-fun instT_witness thy env =
-  map_witness (fn (t, th) => (instT_term env t, instT_thm thy env th));
-
-fun instT_ctxt thy env =
-  map_ctxt_values (instT_type env) (instT_term env) (instT_thm thy env);
+fun instT_morphism thy env = Morphism.morphism
+  {name = I, var = I, typ = instT_type env, term = instT_term env, thm = instT_thm thy env};
 
 
 (* instantiate types and terms *)
@@ -445,11 +440,8 @@
         Drule.fconv_rule (Thm.beta_conversion true))
     end;
 
-fun inst_witness thy envs =
-  map_witness (fn (t, th) => (inst_term envs t, inst_thm thy envs th));
-
-fun inst_ctxt thy envs =
-  map_ctxt_values (instT_type (#1 envs)) (inst_term envs) (inst_thm thy envs);
+fun inst_morphism thy envs = Morphism.morphism
+  {name = I, var = I, typ = instT_type (#1 envs), term = inst_term envs, thm = inst_thm thy envs};
 
 
 (* satisfy hypotheses *)
@@ -460,12 +452,11 @@
     | SOME (Witness (_, th)) => Drule.implies_intr_protected [hyp] #> Goal.comp_hhf th))
   (#hyps (Thm.crep_thm thm));
 
-fun satisfy_witness witns = map_witness (apsnd (satisfy_thm witns));
-
-fun satisfy_ctxt witns = map_ctxt_values I I (satisfy_thm witns);
+fun satisfy_morphism witns = Morphism.morphism
+  {name = I, var = I, typ = I, term = I, thm = satisfy_thm witns};
 
 fun satisfy_facts witns facts =
-  satisfy_ctxt witns (Notes ("", facts)) |> (fn Notes (_, facts') => facts');
+  morph_ctxt (satisfy_morphism witns) (Notes ("", facts)) |> (fn Notes (_, facts') => facts');
 
 
 (* generalize type/term parameters *)
@@ -483,7 +474,9 @@
       singleton ((if std then ProofContext.export_standard else ProofContext.export) inner outer);
     val exp_term = Drule.term_rule thy exp_thm;
     val exp_typ = Logic.mk_type #> exp_term #> Logic.dest_type;
-    val Notes (_, facts') = map_ctxt_values exp_typ exp_term exp_thm (Notes ("", facts));
+    val exp_morphism =
+      Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, thm = exp_thm};
+    val Notes (_, facts') = morph_ctxt exp_morphism (Notes ("", facts));
   in facts' end;
 
 in