src/Pure/Isar/element.ML
changeset 21481 025ab31286d8
parent 21440 807a39221a58
child 21497 4d330a487586
     1.1 --- a/src/Pure/Isar/element.ML	Thu Nov 23 00:52:11 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Thu Nov 23 00:52:15 2006 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4      var: string * mixfix -> string * mixfix,
     1.5      typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
     1.6      attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
     1.7 -  val map_ctxt_values: (typ -> typ) -> (term -> term) -> (thm -> thm) -> context_i -> context_i
     1.8 +  val morph_ctxt: morphism -> context_i -> context_i
     1.9    val params_of: context_i -> (string * typ) list
    1.10    val prems_of: context_i -> term list
    1.11    val facts_of: theory -> context_i ->
    1.12 @@ -35,6 +35,7 @@
    1.13    val pretty_statement: Proof.context -> string -> thm -> Pretty.T
    1.14    type witness
    1.15    val map_witness: (term * thm -> term * thm) -> witness -> witness
    1.16 +  val morph_witness: morphism -> witness -> witness
    1.17    val witness_prop: witness -> term
    1.18    val witness_hyps: witness -> term list
    1.19    val assume_witness: theory -> term -> witness
    1.20 @@ -49,20 +50,16 @@
    1.21    val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
    1.22    val rename_term: (string * (string * mixfix option)) list -> term -> term
    1.23    val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
    1.24 -  val rename_witness: (string * (string * mixfix option)) list -> witness -> witness
    1.25 -  val rename_ctxt: (string * (string * mixfix option)) list -> context_i -> context_i
    1.26 +  val rename_morphism: (string * (string * mixfix option)) list -> morphism
    1.27    val instT_type: typ Symtab.table -> typ -> typ
    1.28    val instT_term: typ Symtab.table -> term -> term
    1.29    val instT_thm: theory -> typ Symtab.table -> thm -> thm
    1.30 -  val instT_witness: theory -> typ Symtab.table -> witness -> witness
    1.31 -  val instT_ctxt: theory -> typ Symtab.table -> context_i -> context_i
    1.32 +  val instT_morphism: theory -> typ Symtab.table -> morphism
    1.33    val inst_term: typ Symtab.table * term Symtab.table -> term -> term
    1.34    val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm
    1.35 -  val inst_witness: theory -> typ Symtab.table * term Symtab.table -> witness -> witness
    1.36 -  val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i
    1.37 +  val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism
    1.38    val satisfy_thm: witness list -> thm -> thm
    1.39 -  val satisfy_witness: witness list -> witness -> witness
    1.40 -  val satisfy_ctxt: witness list -> context_i -> context_i
    1.41 +  val satisfy_morphism: witness list -> morphism
    1.42    val satisfy_facts: witness list ->
    1.43      ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.44      ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
    1.45 @@ -77,7 +74,6 @@
    1.46  structure Element: ELEMENT =
    1.47  struct
    1.48  
    1.49 -
    1.50  (** language elements **)
    1.51  
    1.52  (* statement *)
    1.53 @@ -113,9 +109,13 @@
    1.54     | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
    1.55        ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
    1.56  
    1.57 -fun map_ctxt_values typ term thm = map_ctxt
    1.58 -  {name = I, var = I, typ = typ, term = term, fact = map thm,
    1.59 -    attrib = Args.map_values I typ term thm};
    1.60 +fun morph_ctxt phi = map_ctxt
    1.61 + {name = Morphism.name phi,
    1.62 +  var = Morphism.var phi,
    1.63 +  typ = Morphism.typ phi,
    1.64 +  term = Morphism.term phi,
    1.65 +  fact = map (Morphism.thm phi),
    1.66 +  attrib = Args.morph_values phi};
    1.67  
    1.68  
    1.69  (* logical content *)
    1.70 @@ -272,6 +272,8 @@
    1.71  
    1.72  fun map_witness f (Witness witn) = Witness (f witn);
    1.73  
    1.74 +fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
    1.75 +
    1.76  fun witness_prop (Witness (t, _)) = t;
    1.77  fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
    1.78  
    1.79 @@ -369,12 +371,8 @@
    1.80      else th |> hyps_rule (instantiate_frees thy subst)
    1.81    end;
    1.82  
    1.83 -fun rename_witness ren =
    1.84 -  map_witness (fn (t, th) => (rename_term ren t, rename_thm ren th));
    1.85 -
    1.86 -fun rename_ctxt ren =
    1.87 -  map_ctxt_values I (rename_term ren) (rename_thm ren)
    1.88 -  #> map_ctxt {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren};
    1.89 +fun rename_morphism ren = Morphism.morphism
    1.90 +  {name = I, var = rename_var ren, typ = I, term = rename_term ren, thm = rename_thm ren};
    1.91  
    1.92  
    1.93  (* instantiate types *)
    1.94 @@ -399,11 +397,8 @@
    1.95      let val subst = instT_subst env th
    1.96      in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
    1.97  
    1.98 -fun instT_witness thy env =
    1.99 -  map_witness (fn (t, th) => (instT_term env t, instT_thm thy env th));
   1.100 -
   1.101 -fun instT_ctxt thy env =
   1.102 -  map_ctxt_values (instT_type env) (instT_term env) (instT_thm thy env);
   1.103 +fun instT_morphism thy env = Morphism.morphism
   1.104 +  {name = I, var = I, typ = instT_type env, term = instT_term env, thm = instT_thm thy env};
   1.105  
   1.106  
   1.107  (* instantiate types and terms *)
   1.108 @@ -445,11 +440,8 @@
   1.109          Drule.fconv_rule (Thm.beta_conversion true))
   1.110      end;
   1.111  
   1.112 -fun inst_witness thy envs =
   1.113 -  map_witness (fn (t, th) => (inst_term envs t, inst_thm thy envs th));
   1.114 -
   1.115 -fun inst_ctxt thy envs =
   1.116 -  map_ctxt_values (instT_type (#1 envs)) (inst_term envs) (inst_thm thy envs);
   1.117 +fun inst_morphism thy envs = Morphism.morphism
   1.118 +  {name = I, var = I, typ = instT_type (#1 envs), term = inst_term envs, thm = inst_thm thy envs};
   1.119  
   1.120  
   1.121  (* satisfy hypotheses *)
   1.122 @@ -460,12 +452,11 @@
   1.123      | SOME (Witness (_, th)) => Drule.implies_intr_protected [hyp] #> Goal.comp_hhf th))
   1.124    (#hyps (Thm.crep_thm thm));
   1.125  
   1.126 -fun satisfy_witness witns = map_witness (apsnd (satisfy_thm witns));
   1.127 -
   1.128 -fun satisfy_ctxt witns = map_ctxt_values I I (satisfy_thm witns);
   1.129 +fun satisfy_morphism witns = Morphism.morphism
   1.130 +  {name = I, var = I, typ = I, term = I, thm = satisfy_thm witns};
   1.131  
   1.132  fun satisfy_facts witns facts =
   1.133 -  satisfy_ctxt witns (Notes ("", facts)) |> (fn Notes (_, facts') => facts');
   1.134 +  morph_ctxt (satisfy_morphism witns) (Notes ("", facts)) |> (fn Notes (_, facts') => facts');
   1.135  
   1.136  
   1.137  (* generalize type/term parameters *)
   1.138 @@ -483,7 +474,9 @@
   1.139        singleton ((if std then ProofContext.export_standard else ProofContext.export) inner outer);
   1.140      val exp_term = Drule.term_rule thy exp_thm;
   1.141      val exp_typ = Logic.mk_type #> exp_term #> Logic.dest_type;
   1.142 -    val Notes (_, facts') = map_ctxt_values exp_typ exp_term exp_thm (Notes ("", facts));
   1.143 +    val exp_morphism =
   1.144 +      Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, thm = exp_thm};
   1.145 +    val Notes (_, facts') = morph_ctxt exp_morphism (Notes ("", facts));
   1.146    in facts' end;
   1.147  
   1.148  in