equal
deleted
inserted
replaced
382 by (rule subst [OF reflcl_trancl]) simp |
382 by (rule subst [OF reflcl_trancl]) simp |
383 |
383 |
384 lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+" |
384 lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+" |
385 by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl) |
385 by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl) |
386 |
386 |
|
387 lemma rtrancl_eq_or_trancl: |
|
388 "(x,y) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> R\<^sup>+)" |
|
389 by (fast elim: trancl_into_rtrancl dest: rtranclD) |
387 |
390 |
388 text {* @{text Domain} and @{text Range} *} |
391 text {* @{text Domain} and @{text Range} *} |
389 |
392 |
390 lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV" |
393 lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV" |
391 by blast |
394 by blast |