src/HOL/Transitive_Closure.thy
changeset 31690 cc37bf07f9bb
parent 31577 ce3721fa1e17
child 31970 ccaadfcf6941
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Jun 17 11:00:14 2009 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Jun 17 15:41:49 2009 +0200
     1.3 @@ -294,6 +294,20 @@
     1.4  lemma rtrancl_unfold: "r^* = Id Un r O r^*"
     1.5    by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
     1.6  
     1.7 +lemma rtrancl_Un_separatorE:
     1.8 +  "(a,b) : (P \<union> Q)^* \<Longrightarrow> \<forall>x y. (a,x) : P^* \<longrightarrow> (x,y) : Q \<longrightarrow> x=y \<Longrightarrow> (a,b) : P^*"
     1.9 +apply (induct rule:rtrancl.induct)
    1.10 + apply blast
    1.11 +apply (blast intro:rtrancl_trans)
    1.12 +done
    1.13 +
    1.14 +lemma rtrancl_Un_separator_converseE:
    1.15 +  "(a,b) : (P \<union> Q)^* \<Longrightarrow> \<forall>x y. (x,b) : P^* \<longrightarrow> (y,x) : Q \<longrightarrow> y=x \<Longrightarrow> (a,b) : P^*"
    1.16 +apply (induct rule:converse_rtrancl_induct)
    1.17 + apply blast
    1.18 +apply (blast intro:rtrancl_trans)
    1.19 +done
    1.20 +
    1.21  
    1.22  subsection {* Transitive closure *}
    1.23