equal
deleted
inserted
replaced
400 |
400 |
401 |
401 |
402 text {* More about converse @{text rtrancl} and @{text trancl}, should |
402 text {* More about converse @{text rtrancl} and @{text trancl}, should |
403 be merged with main body. *} |
403 be merged with main body. *} |
404 |
404 |
|
405 lemma single_valued_confluent: |
|
406 "\<lbrakk> single_valued r; (x,y) \<in> r^*; (x,z) \<in> r^* \<rbrakk> |
|
407 \<Longrightarrow> (y,z) \<in> r^* \<or> (z,y) \<in> r^*" |
|
408 apply(erule rtrancl_induct) |
|
409 apply simp |
|
410 apply(erule disjE) |
|
411 apply(blast elim:converse_rtranclE dest:single_valuedD) |
|
412 apply(blast intro:rtrancl_trans) |
|
413 done |
|
414 |
405 lemma r_r_into_trancl: "(a, b) \<in> R ==> (b, c) \<in> R ==> (a, c) \<in> R^+" |
415 lemma r_r_into_trancl: "(a, b) \<in> R ==> (b, c) \<in> R ==> (a, c) \<in> R^+" |
406 by (fast intro: trancl_trans) |
416 by (fast intro: trancl_trans) |
407 |
417 |
408 lemma trancl_into_trancl [rule_format]: |
418 lemma trancl_into_trancl [rule_format]: |
409 "(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r --> (a,c) \<in> r\<^sup>+" |
419 "(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r --> (a,c) \<in> r\<^sup>+" |