# HG changeset patch
# User nipkow
# Date 1245246109 -7200
# Node ID cc37bf07f9bb375cd372b8b50a9b1db2f28972b5
# Parent  358cdcdf56d2f2ce48183740e6f90c8ec7b990b8
rtrancl lemmas

diff -r 358cdcdf56d2 -r cc37bf07f9bb src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Jun 17 11:00:14 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy	Wed Jun 17 15:41:49 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 *}