equal
deleted
inserted
replaced
60 apply auto |
60 apply auto |
61 apply (case_tac "xa") |
61 apply (case_tac "xa") |
62 apply auto |
62 apply auto |
63 done |
63 done |
64 |
64 |
65 (* context (theory "Transitive_Closure") *) |
65 (* irrefl_tranclI in Transitive_Closure.thy is more general *) |
66 lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+" |
66 lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+" |
67 apply (rule allI) |
67 by(blast elim: tranclE dest: trancl_into_rtrancl) |
68 apply (erule irrefl_tranclI) |
68 |
69 done |
|
70 |
69 |
71 lemma trancl_rtrancl_trancl: |
70 lemma trancl_rtrancl_trancl: |
72 "\<lbrakk>(x,y)\<in>r^+; (y,z)\<in>r^*\<rbrakk> \<Longrightarrow> (x,z)\<in>r^+" |
71 "\<lbrakk>(x,y)\<in>r^+; (y,z)\<in>r^*\<rbrakk> \<Longrightarrow> (x,z)\<in>r^+" |
73 by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2) |
72 by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2) |
74 |
73 |