# HG changeset patch
# User wenzelm
# Date 1166106681 -3600
# Node ID e10b8bd7a886f60613b87ae33193c96f6f49911e
# Parent  2015be1b6a03dac59d25ada99a2af8094f8aabcf
added trans_terms/props;

diff -r 2015be1b6a03 -r e10b8bd7a886 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Dec 14 15:31:20 2006 +0100
+++ b/src/Pure/Isar/local_defs.ML	Thu Dec 14 15:31:21 2006 +0100
@@ -15,6 +15,8 @@
   val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     (term * (bstring * thm)) list * Proof.context
   val export: Proof.context -> Proof.context -> thm -> thm list * thm
+  val trans_terms: Proof.context -> thm list -> thm
+  val trans_props: Proof.context -> thm list -> thm
   val print_rules: Proof.context -> unit
   val defn_add: attribute
   val defn_del: attribute
@@ -111,6 +113,28 @@
   in (map Drule.abs_def defs, th') end;
 
 
+(* basic transitivity reasoning -- modulo beta-eta *)
+
+local
+
+val is_trivial = Pattern.aeconv o Logic.dest_equals o Thm.prop_of;
+
+fun trans_list _ _ [] = raise Empty
+  | trans_list trans ctxt (th :: raw_eqs) =
+      (case filter_out is_trivial raw_eqs of
+        [] => th
+      | eqs =>
+          let val ((_, th' :: eqs'), ctxt') = Variable.import true (th :: eqs) ctxt
+          in singleton (Variable.export ctxt' ctxt) (fold trans eqs' th') end);
+
+in
+
+val trans_terms = trans_list (fn eq2 => fn eq1 => eq2 COMP (eq1 COMP Drule.transitive_thm));
+val trans_props = trans_list (fn eq => fn th => th COMP (eq COMP Drule.equal_elim_rule1));
+
+end;
+
+
 
 (** defived definitions **)