8 lemma "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}" |
8 lemma "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}" |
9 (is "lfp ?F = ?toA") |
9 (is "lfp ?F = ?toA") |
10 proof |
10 proof |
11 show "lfp ?F \<subseteq> ?toA" |
11 show "lfp ?F \<subseteq> ?toA" |
12 by (blast intro!: lfp_lowerbound intro: rtrancl_trans) |
12 by (blast intro!: lfp_lowerbound intro: rtrancl_trans) |
13 |
13 next |
14 show "?toA \<subseteq> lfp ?F" |
14 show "?toA \<subseteq> lfp ?F" |
15 proof |
15 proof |
16 fix s assume "s \<in> ?toA" |
16 fix s assume "s \<in> ?toA" |
17 then obtain t where stM: "(s,t) \<in> M\<^sup>*" and tA: "t \<in> A" |
17 then obtain t where stM: "(s,t) \<in> M\<^sup>*" and tA: "t \<in> A" |
18 by blast |
18 by blast |
19 from stM show "s \<in> lfp ?F" |
19 from stM show "s \<in> lfp ?F" |
20 proof (rule converse_rtrancl_induct) |
20 proof (rule converse_rtrancl_induct) |
21 from tA have "t \<in> ?F (lfp ?F)" by blast |
21 from tA have "t \<in> ?F (lfp ?F)" by blast |
22 with mono_ef show "t \<in> lfp ?F" .. |
22 with mono_ef show "t \<in> lfp ?F" .. |
|
23 next |
23 fix s s' assume "(s,s') \<in> M" and "(s',t) \<in> M\<^sup>*" |
24 fix s s' assume "(s,s') \<in> M" and "(s',t) \<in> M\<^sup>*" |
24 and "s' \<in> lfp ?F" |
25 and "s' \<in> lfp ?F" |
25 then have "s \<in> ?F (lfp ?F)" by blast |
26 then have "s \<in> ?F (lfp ?F)" by blast |
26 with mono_ef show "s \<in> lfp ?F" .. |
27 with mono_ef show "s \<in> lfp ?F" .. |
27 qed |
28 qed |