--- 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)