merged
authorwenzelm
Wed, 17 Jun 2009 17:24:34 +0200
changeset 31692 57715a08e4b6
parent 31690 cc37bf07f9bb (diff)
parent 31689 84a14d2dc868 (current diff)
child 31693 8d1861721887
merged
--- a/src/HOL/Transitive_Closure.thy	Wed Jun 17 17:07:26 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy	Wed Jun 17 17:24:34 2009 +0200
@@ -294,6 +294,20 @@
 lemma rtrancl_unfold: "r^* = Id Un r O r^*"
   by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
 
+lemma rtrancl_Un_separatorE:
+  "(a,b) : (P \<union> Q)^* \<Longrightarrow> \<forall>x y. (a,x) : P^* \<longrightarrow> (x,y) : Q \<longrightarrow> x=y \<Longrightarrow> (a,b) : P^*"
+apply (induct rule:rtrancl.induct)
+ apply blast
+apply (blast intro:rtrancl_trans)
+done
+
+lemma rtrancl_Un_separator_converseE:
+  "(a,b) : (P \<union> Q)^* \<Longrightarrow> \<forall>x y. (x,b) : P^* \<longrightarrow> (y,x) : Q \<longrightarrow> y=x \<Longrightarrow> (a,b) : P^*"
+apply (induct rule:converse_rtrancl_induct)
+ apply blast
+apply (blast intro:rtrancl_trans)
+done
+
 
 subsection {* Transitive closure *}