equal
deleted
inserted
replaced
102 |
102 |
103 lemma diamond_rtrancl: "diamond(r) ==> diamond(r^*)" |
103 lemma diamond_rtrancl: "diamond(r) ==> diamond(r^*)" |
104 apply (simp (no_asm_simp) add: diamond_def) |
104 apply (simp (no_asm_simp) add: diamond_def) |
105 apply (rule impI [THEN allI, THEN allI]) |
105 apply (rule impI [THEN allI, THEN allI]) |
106 apply (erule rtrancl_induct, blast) |
106 apply (erule rtrancl_induct, blast) |
107 apply (best intro: rtrancl_trans [OF _ r_into_rtrancl] |
107 apply (meson rtrancl_trans r_into_rtrancl diamond_strip_lemmaE) |
108 elim: diamond_strip_lemmaE [THEN exE]) |
|
109 done |
108 done |
110 |
109 |
111 |
110 |
112 subsection {* Non-contraction results *} |
111 subsection {* Non-contraction results *} |
113 |
112 |