# HG changeset patch
# User kleing
# Date 1007904858 -3600
# Node ID f3033eed309a931a4ef85f9e80c93881b2ce9b33
# Parent  37cfec8dfe8e0da7466c0aa4ce1f81cdedfbe47f
setup [trans] rules for calculational Isar reasoning

diff -r 37cfec8dfe8e -r f3033eed309a src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sat Dec 08 17:34:46 2001 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sun Dec 09 14:34:18 2001 +0100
@@ -95,6 +95,36 @@
  apply (auto)
  by (erule rev_mp, erule rtrancl_induct, auto)
 
+(* more about converse rtrancl and trancl, should be merged with main body *)
+
+lemma converse_rtrancl_into_rtrancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R^* \<Longrightarrow> (a,c) \<in> R^*"
+  by (erule rtrancl_induct) (fast intro: rtrancl_into_rtrancl)+
+
+lemma r_r_into_trancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R \<Longrightarrow> (a,c) \<in> R^+"
+  by (fast intro: trancl_trans)
+
+lemma trancl_into_trancl [rule_format]:
+  "(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r \<longrightarrow> (a,c) \<in> r\<^sup>+"
+  apply (erule trancl_induct)   
+   apply (fast intro: r_r_into_trancl)
+  apply (fast intro: r_r_into_trancl trancl_trans)
+  done
+
+lemma trancl_rtrancl_trancl:
+  "(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r\<^sup>* \<Longrightarrow> (a,c) \<in> r\<^sup>+"
+  apply (drule tranclD)
+  apply (erule exE, erule conjE)
+  apply (drule rtrancl_trans, assumption)
+  apply (drule rtrancl_into_trancl2, assumption)
+  apply assumption
+  done
+
+lemmas [trans] = r_r_into_trancl trancl_trans rtrancl_trans 
+                 trancl_into_trancl trancl_into_trancl2
+                 rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
+                 rtrancl_trancl_trancl trancl_rtrancl_trancl
+
+declare trancl_into_rtrancl [elim]
 
 declare rtrancl_induct [induct set: rtrancl]
 declare rtranclE [cases set: rtrancl]