equal
deleted
inserted
replaced
106 prefer 2 apply blast |
106 prefer 2 apply blast |
107 prefer 2 apply blast |
107 prefer 2 apply blast |
108 apply (erule asm_rl exE disjE conjE cases)+ |
108 apply (erule asm_rl exE disjE conjE cases)+ |
109 done |
109 done |
110 |
110 |
|
111 lemma rtrancl_Int_subset: "[| Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s|] ==> r^* \<subseteq> s" |
|
112 apply (rule subsetI) |
|
113 apply (rule_tac p="x" in PairE, clarify) |
|
114 apply (erule rtrancl_induct, auto) |
|
115 done |
|
116 |
111 lemma converse_rtrancl_into_rtrancl: |
117 lemma converse_rtrancl_into_rtrancl: |
112 "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*" |
118 "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*" |
113 by (rule rtrancl_trans) iprover+ |
119 by (rule rtrancl_trans) iprover+ |
114 |
120 |
115 text {* |
121 text {* |
260 shows "P x y" |
266 shows "P x y" |
261 -- {* Another induction rule for trancl, incorporating transitivity *} |
267 -- {* Another induction rule for trancl, incorporating transitivity *} |
262 by (iprover intro: r_into_trancl major [THEN trancl_induct] cases) |
268 by (iprover intro: r_into_trancl major [THEN trancl_induct] cases) |
263 |
269 |
264 inductive_cases tranclE: "(a, b) : r^+" |
270 inductive_cases tranclE: "(a, b) : r^+" |
|
271 |
|
272 lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s" |
|
273 apply (rule subsetI) |
|
274 apply (rule_tac p="x" in PairE, clarify) |
|
275 apply (erule trancl_induct, auto) |
|
276 done |
265 |
277 |
266 lemma trancl_unfold: "r^+ = r Un r O r^+" |
278 lemma trancl_unfold: "r^+ = r Un r O r^+" |
267 by (auto intro: trancl_into_trancl elim: tranclE) |
279 by (auto intro: trancl_into_trancl elim: tranclE) |
268 |
280 |
269 lemma trans_trancl[simp]: "trans(r^+)" |
281 lemma trans_trancl[simp]: "trans(r^+)" |