# HG changeset patch
# User paulson
# Date 1160037612 -7200
# Node ID fd0e33caeb3bf47f14104233962dfcea92c5bbfd
# Parent  1a8efd618190a5ccca314c60263029bcb04ae8a4
a few new functions on thms and cterms

diff -r 1a8efd618190 -r fd0e33caeb3b src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Oct 05 05:46:32 2006 +0200
+++ b/src/Pure/drule.ML	Thu Oct 05 10:40:12 2006 +0200
@@ -89,6 +89,8 @@
   val list_comb: cterm * cterm list -> cterm
   val strip_comb: cterm -> cterm * cterm list
   val strip_type: ctyp -> ctyp list * ctyp
+  val clhs_of: thm -> cterm
+  val crhs_of: thm -> cterm
   val beta_conv: cterm -> cterm -> cterm
   val plain_prop_of: thm -> term
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
@@ -107,6 +109,7 @@
   val imp_cong_rule: thm -> thm -> thm
   val beta_eta_conversion: cterm -> thm
   val eta_long_conversion: cterm -> thm
+  val eta_contraction_rule: thm -> thm
   val forall_conv: int -> (cterm -> thm) -> cterm -> thm
   val concl_conv: int -> (cterm -> thm) -> cterm -> thm
   val prems_conv: int -> (int -> cterm -> thm) -> cterm -> thm
@@ -213,6 +216,18 @@
       in (cT1 :: cTs, cT') end
   | _ => ([], cT));
 
+fun clhs_of th =
+  case strip_comb (cprop_of th) of
+      (f, [x, _]) =>
+          (case term_of f of Const ("==", _) => x | _ => raise THM ("clhs_of", 0, [th]))
+    | _ => raise THM ("clhs_of", 1, [th]);
+
+fun crhs_of th =
+  case strip_comb (cprop_of th) of
+      (f, [_, x]) =>
+          (case term_of f of Const ("==", _) => x | _ => raise THM ("crhs_of", 0, [th]))
+    | _ => raise THM ("crhs_of", 1, [th]);
+
 (*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs
   of the meta-equality returned by the beta_conversion rule.*)
 fun beta_conv x y =
@@ -657,6 +672,10 @@
 fun eta_long_conversion ct = transitive (beta_eta_conversion ct)
   (symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct)));
 
+(*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
+fun eta_contraction_rule th =
+  equal_elim (eta_conversion (cprop_of th)) th;
+
 val abs_def =
   let
     fun contract_lhs th =