equal
deleted
inserted
replaced
306 "(a,b) : (P \<union> Q)^* \<Longrightarrow> \<forall>x y. (x,b) : P^* \<longrightarrow> (y,x) : Q \<longrightarrow> y=x \<Longrightarrow> (a,b) : P^*" |
306 "(a,b) : (P \<union> Q)^* \<Longrightarrow> \<forall>x y. (x,b) : P^* \<longrightarrow> (y,x) : Q \<longrightarrow> y=x \<Longrightarrow> (a,b) : P^*" |
307 apply (induct rule:converse_rtrancl_induct) |
307 apply (induct rule:converse_rtrancl_induct) |
308 apply blast |
308 apply blast |
309 apply (blast intro:rtrancl_trans) |
309 apply (blast intro:rtrancl_trans) |
310 done |
310 done |
|
311 |
|
312 lemma Image_closed_trancl: |
|
313 assumes "r `` X \<subseteq> X" shows "r\<^sup>* `` X = X" |
|
314 proof - |
|
315 from assms have **: "{y. \<exists>x\<in>X. (x, y) \<in> r} \<subseteq> X" by auto |
|
316 have "\<And>x y. (y, x) \<in> r\<^sup>* \<Longrightarrow> y \<in> X \<Longrightarrow> x \<in> X" |
|
317 proof - |
|
318 fix x y |
|
319 assume *: "y \<in> X" |
|
320 assume "(y, x) \<in> r\<^sup>*" |
|
321 then show "x \<in> X" |
|
322 proof induct |
|
323 case base show ?case by (fact *) |
|
324 next |
|
325 case step with ** show ?case by auto |
|
326 qed |
|
327 qed |
|
328 then show ?thesis by auto |
|
329 qed |
311 |
330 |
312 |
331 |
313 subsection {* Transitive closure *} |
332 subsection {* Transitive closure *} |
314 |
333 |
315 lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+" |
334 lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+" |