- Exported goals_conv and fconv_rule
authorberghofe
Fri Oct 12 16:57:07 2001 +0200 (2001-10-12)
changeset 11736da6fc37ed6fa
parent 11735 60c0fa10bfc2
child 11737 0ec18d3131b5
- Exported goals_conv and fconv_rule
- Added forall_conv
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Fri Oct 12 12:13:31 2001 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Fri Oct 12 16:57:07 2001 +0200
     1.3 @@ -41,6 +41,9 @@
     1.4    val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
     1.5    val rewrite_cterm: bool * bool * bool ->
     1.6      (meta_simpset -> thm -> thm option) -> meta_simpset -> cterm -> thm
     1.7 +  val goals_conv        : (int -> bool) -> (cterm -> thm) -> cterm -> thm
     1.8 +  val forall_conv       : (cterm -> thm) -> cterm -> thm
     1.9 +  val fconv_rule        : (cterm -> thm) -> thm -> thm
    1.10    val full_rewrite_cterm_aux: (meta_simpset -> thm -> thm option) -> thm list -> cterm -> cterm
    1.11    val rewrite_rule_aux  : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    1.12    val rewrite_thm       : bool * bool * bool
    1.13 @@ -931,6 +934,18 @@
    1.14          handle TERM _ => reflexive ct
    1.15    in gconv 1 end;
    1.16  
    1.17 +(* Rewrite A in !!x1,...x1. A *)
    1.18 +fun forall_conv cv ct =
    1.19 +  let val p as (ct1, ct2) = Thm.dest_comb ct
    1.20 +  in (case pairself term_of p of
    1.21 +      (Const ("all", _), Abs (s, _, _)) =>
    1.22 +         let val (v, ct') = Thm.dest_abs (Some "@") ct2;
    1.23 +         in Thm.combination (Thm.reflexive ct1)
    1.24 +           (Thm.abstract_rule s v (forall_conv cv ct'))
    1.25 +         end
    1.26 +    | _ => cv ct)
    1.27 +  end handle TERM _ => cv ct;
    1.28 +
    1.29  (*Use a conversion to transform a theorem*)
    1.30  fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
    1.31