src/Pure/drule.ML
changeset 1194 563ecd14c1d8
parent 952 9e10962866b0
child 1218 59ed8ef1a3a1
     1.1 --- a/src/Pure/drule.ML	Tue Jul 25 17:02:34 1995 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Jul 25 17:03:16 1995 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4    val flexpair_abs_elim_list: cterm list -> thm -> thm
     1.5    val forall_intr_list	: cterm list -> thm -> thm
     1.6    val forall_intr_frees	: thm -> thm
     1.7 +  val forall_intr_vars	: thm -> thm
     1.8    val forall_elim_list	: cterm list -> thm -> thm
     1.9    val forall_elim_var	: int -> thm -> thm
    1.10    val forall_elim_vars	: int -> thm -> thm
    1.11 @@ -644,6 +645,27 @@
    1.12  val size_of_thm = size_of_term o #prop o rep_thm;
    1.13  
    1.14  
    1.15 +(** Mark Staples's weaker version of eq_thm: ignores variable renaming and
    1.16 +    (some) type variable renaming **)
    1.17 +
    1.18 + (* Can't use term_vars, because it sorts the resulting list of variable names.
    1.19 +    We instead need the unique list noramlised by the order of appearance
    1.20 +    in the term. *)
    1.21 +fun term_vars' (t as Var(v,T)) = [t]
    1.22 +  | term_vars' (Abs(_,_,b)) = term_vars' b
    1.23 +  | term_vars' (f$a) = (term_vars' f) @ (term_vars' a)
    1.24 +  | term_vars' _ = [];
    1.25 +
    1.26 +fun forall_intr_vars th =
    1.27 +  let val {prop,sign,...} = rep_thm th;
    1.28 +      val vars = distinct (term_vars' prop);
    1.29 +  in forall_intr_list (map (cterm_of sign) vars) th end;
    1.30 +
    1.31 +fun weak_eq_thm (tha,thb) = 
    1.32 +    eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb));
    1.33 +
    1.34 +
    1.35 +
    1.36  (*** Meta-Rewriting Rules ***)
    1.37  
    1.38