equal
deleted
inserted
replaced
80 |
80 |
81 text {* |
81 text {* |
82 First of all, we use the de-Morgan property of fixed points |
82 First of all, we use the de-Morgan property of fixed points |
83 *} |
83 *} |
84 |
84 |
85 lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))" |
85 lemma lfp_gfp: "lfp f = - gfp (\<lambda>s::'a set. - (f (- s)))" |
86 proof |
86 proof |
87 show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))" |
87 show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))" |
88 proof |
88 proof |
89 fix x assume l: "x \<in> lfp f" |
89 fix x assume l: "x \<in> lfp f" |
90 show "x \<in> - gfp (\<lambda>s. - f (- s))" |
90 show "x \<in> - gfp (\<lambda>s. - f (- s))" |
91 proof |
91 proof |
92 assume "x \<in> gfp (\<lambda>s. - f (- s))" |
92 assume "x \<in> gfp (\<lambda>s. - f (- s))" |
93 then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)" by (unfold gfp_def) auto |
93 then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)" |
|
94 by (auto simp add: gfp_def Join_set_eq) |
94 then have "f (- u) \<subseteq> - u" by auto |
95 then have "f (- u) \<subseteq> - u" by auto |
95 then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound) |
96 then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound) |
96 from l and this have "x \<notin> u" by auto |
97 from l and this have "x \<notin> u" by auto |
97 then show False by contradiction |
98 then show False by contradiction |
98 qed |
99 qed |
105 then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound) |
106 then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound) |
106 then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto |
107 then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto |
107 qed |
108 qed |
108 qed |
109 qed |
109 |
110 |
110 lemma lfp_gfp': "- lfp f = gfp (\<lambda>s. - (f (- s)))" |
111 lemma lfp_gfp': "- lfp f = gfp (\<lambda>s::'a set. - (f (- s)))" |
111 by (simp add: lfp_gfp) |
112 by (simp add: lfp_gfp) |
112 |
113 |
113 lemma gfp_lfp': "- gfp f = lfp (\<lambda>s. - (f (- s)))" |
114 lemma gfp_lfp': "- gfp f = lfp (\<lambda>s::'a set. - (f (- s)))" |
114 by (simp add: lfp_gfp) |
115 by (simp add: lfp_gfp) |
115 |
116 |
116 text {* |
117 text {* |
117 in order to give dual fixed point representations of @{term "AF p"} |
118 in order to give dual fixed point representations of @{term "AF p"} |
118 and @{term "AG p"}: |
119 and @{term "AG p"}: |