diff -r b161604f0c8d -r 7bf8868ab3e4 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Jan 17 09:52:54 2007 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Jan 17 09:53:50 2007 +0100
@@ -108,6 +108,12 @@
   apply (erule asm_rl exE disjE conjE cases)+
   done
 
+lemma rtrancl_Int_subset: "[| Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s|] ==> r^* \<subseteq> s"
+  apply (rule subsetI)
+  apply (rule_tac p="x" in PairE, clarify)
+  apply (erule rtrancl_induct, auto) 
+  done
+
 lemma converse_rtrancl_into_rtrancl:
   "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
   by (rule rtrancl_trans) iprover+
@@ -263,6 +269,12 @@
 
 inductive_cases tranclE: "(a, b) : r^+"
 
+lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s"
+  apply (rule subsetI)
+  apply (rule_tac p="x" in PairE, clarify)
+  apply (erule trancl_induct, auto) 
+  done
+
 lemma trancl_unfold: "r^+ = r Un r O r^+"
   by (auto intro: trancl_into_trancl elim: tranclE)