src/Pure/Isar/element.ML
changeset 20264 f09a4003e12d
parent 20233 ece639738db3
child 20304 500a3373c93c
     1.1 --- a/src/Pure/Isar/element.ML	Sun Jul 30 21:28:56 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Sun Jul 30 21:28:57 2006 +0200
     1.3 @@ -63,6 +63,12 @@
     1.4    val satisfy_thm: witness list -> thm -> thm
     1.5    val satisfy_witness: witness list -> witness -> witness
     1.6    val satisfy_ctxt: witness list -> context_i -> context_i
     1.7 +  val satisfy_facts: witness list ->
     1.8 +    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     1.9 +    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
    1.10 +  val generalize_facts: Proof.context -> Proof.context ->
    1.11 +    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    1.12 +    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
    1.13  end;
    1.14  
    1.15  structure Element: ELEMENT =
    1.16 @@ -453,4 +459,23 @@
    1.17  
    1.18  fun satisfy_ctxt witns = map_ctxt_values I I (satisfy_thm witns);
    1.19  
    1.20 +fun satisfy_facts witns facts =
    1.21 +  satisfy_ctxt witns (Notes facts) |> (fn Notes facts' => facts');
    1.22 +
    1.23 +
    1.24 +(* generalize type/term parameters *)
    1.25 +
    1.26 +val maxidx_atts = fold Args.maxidx_values;
    1.27 +
    1.28 +fun generalize_facts inner outer facts =
    1.29 +  let
    1.30 +    val thy = ProofContext.theory_of inner;
    1.31 +    val maxidx =
    1.32 +      fold (fn ((_, atts), bs) => maxidx_atts atts #> fold (maxidx_atts o #2) bs) facts ~1;
    1.33 +    val gen_thm = Thm.adjust_maxidx_thm maxidx #> singleton (Variable.export inner outer);
    1.34 +    val gen_term = Thm.cterm_of thy #> Drule.mk_term #> gen_thm #> Drule.dest_term #> Thm.term_of;
    1.35 +    val gen_typ = Logic.mk_type #> gen_term #> Logic.dest_type;
    1.36 +    val Notes facts' = map_ctxt_values gen_typ gen_term gen_thm (Notes facts);
    1.37 +  in facts' end;
    1.38 +
    1.39  end;