lemma, equation between rtrancl and trancl
authorkleing
Tue Jun 21 11:08:31 2005 +0200 (2005-06-21)
changeset 16514090c6a98c704
parent 16513 f38693aad717
child 16515 7896ea4f3a87
lemma, equation between rtrancl and trancl
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Transitive_Closure.thy	Tue Jun 21 09:51:59 2005 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Jun 21 11:08:31 2005 +0200
     1.3 @@ -384,6 +384,9 @@
     1.4  lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+"
     1.5    by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
     1.6  
     1.7 +lemma rtrancl_eq_or_trancl:
     1.8 +  "(x,y) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> R\<^sup>+)"
     1.9 +  by (fast elim: trancl_into_rtrancl dest: rtranclD)
    1.10  
    1.11  text {* @{text Domain} and @{text Range} *}
    1.12