|
1 (* Title: HOLCF/Pcpo.thy |
|
2 Author: Franz Regensburger |
|
3 *) |
|
4 |
|
5 header {* Classes cpo and pcpo *} |
|
6 |
|
7 theory Pcpo |
|
8 imports Porder |
|
9 begin |
|
10 |
|
11 subsection {* Complete partial orders *} |
|
12 |
|
13 text {* The class cpo of chain complete partial orders *} |
|
14 |
|
15 class cpo = po + |
|
16 assumes cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x" |
|
17 begin |
|
18 |
|
19 text {* in cpo's everthing equal to THE lub has lub properties for every chain *} |
|
20 |
|
21 lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)" |
|
22 by (fast dest: cpo elim: is_lub_lub) |
|
23 |
|
24 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l" |
|
25 by (blast dest: cpo intro: is_lub_lub) |
|
26 |
|
27 text {* Properties of the lub *} |
|
28 |
|
29 lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)" |
|
30 by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1]) |
|
31 |
|
32 lemma is_lub_thelub: |
|
33 "\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x" |
|
34 by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2]) |
|
35 |
|
36 lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)" |
|
37 by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def) |
|
38 |
|
39 lemma lub_below: "\<lbrakk>chain S; \<And>i. S i \<sqsubseteq> x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x" |
|
40 by (simp add: lub_below_iff) |
|
41 |
|
42 lemma below_lub: "\<lbrakk>chain S; x \<sqsubseteq> S i\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. S i)" |
|
43 by (erule below_trans, erule is_ub_thelub) |
|
44 |
|
45 lemma lub_range_mono: |
|
46 "\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk> |
|
47 \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" |
|
48 apply (erule lub_below) |
|
49 apply (subgoal_tac "\<exists>j. X i = Y j") |
|
50 apply clarsimp |
|
51 apply (erule is_ub_thelub) |
|
52 apply auto |
|
53 done |
|
54 |
|
55 lemma lub_range_shift: |
|
56 "chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)" |
|
57 apply (rule below_antisym) |
|
58 apply (rule lub_range_mono) |
|
59 apply fast |
|
60 apply assumption |
|
61 apply (erule chain_shift) |
|
62 apply (rule lub_below) |
|
63 apply assumption |
|
64 apply (rule_tac i="i" in below_lub) |
|
65 apply (erule chain_shift) |
|
66 apply (erule chain_mono) |
|
67 apply (rule le_add1) |
|
68 done |
|
69 |
|
70 lemma maxinch_is_thelub: |
|
71 "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)" |
|
72 apply (rule iffI) |
|
73 apply (fast intro!: lub_eqI lub_finch1) |
|
74 apply (unfold max_in_chain_def) |
|
75 apply (safe intro!: below_antisym) |
|
76 apply (fast elim!: chain_mono) |
|
77 apply (drule sym) |
|
78 apply (force elim!: is_ub_thelub) |
|
79 done |
|
80 |
|
81 text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *} |
|
82 |
|
83 lemma lub_mono: |
|
84 "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> |
|
85 \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" |
|
86 by (fast elim: lub_below below_lub) |
|
87 |
|
88 text {* the = relation between two chains is preserved by their lubs *} |
|
89 |
|
90 lemma lub_eq: |
|
91 "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" |
|
92 by simp |
|
93 |
|
94 lemma ch2ch_lub: |
|
95 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" |
|
96 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" |
|
97 shows "chain (\<lambda>i. \<Squnion>j. Y i j)" |
|
98 apply (rule chainI) |
|
99 apply (rule lub_mono [OF 2 2]) |
|
100 apply (rule chainE [OF 1]) |
|
101 done |
|
102 |
|
103 lemma diag_lub: |
|
104 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" |
|
105 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" |
|
106 shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)" |
|
107 proof (rule below_antisym) |
|
108 have 3: "chain (\<lambda>i. Y i i)" |
|
109 apply (rule chainI) |
|
110 apply (rule below_trans) |
|
111 apply (rule chainE [OF 1]) |
|
112 apply (rule chainE [OF 2]) |
|
113 done |
|
114 have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)" |
|
115 by (rule ch2ch_lub [OF 1 2]) |
|
116 show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)" |
|
117 apply (rule lub_below [OF 4]) |
|
118 apply (rule lub_below [OF 2]) |
|
119 apply (rule below_lub [OF 3]) |
|
120 apply (rule below_trans) |
|
121 apply (rule chain_mono [OF 1 le_maxI1]) |
|
122 apply (rule chain_mono [OF 2 le_maxI2]) |
|
123 done |
|
124 show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)" |
|
125 apply (rule lub_mono [OF 3 4]) |
|
126 apply (rule is_ub_thelub [OF 2]) |
|
127 done |
|
128 qed |
|
129 |
|
130 lemma ex_lub: |
|
131 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" |
|
132 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" |
|
133 shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>j. \<Squnion>i. Y i j)" |
|
134 by (simp add: diag_lub 1 2) |
|
135 |
|
136 end |
|
137 |
|
138 subsection {* Pointed cpos *} |
|
139 |
|
140 text {* The class pcpo of pointed cpos *} |
|
141 |
|
142 class pcpo = cpo + |
|
143 assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y" |
|
144 begin |
|
145 |
|
146 definition UU :: 'a where |
|
147 "UU = (THE x. \<forall>y. x \<sqsubseteq> y)" |
|
148 |
|
149 notation (xsymbols) |
|
150 UU ("\<bottom>") |
|
151 |
|
152 text {* derive the old rule minimal *} |
|
153 |
|
154 lemma UU_least: "\<forall>z. \<bottom> \<sqsubseteq> z" |
|
155 apply (unfold UU_def) |
|
156 apply (rule theI') |
|
157 apply (rule ex_ex1I) |
|
158 apply (rule least) |
|
159 apply (blast intro: below_antisym) |
|
160 done |
|
161 |
|
162 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x" |
|
163 by (rule UU_least [THEN spec]) |
|
164 |
|
165 end |
|
166 |
|
167 text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *} |
|
168 |
|
169 setup {* |
|
170 Reorient_Proc.add |
|
171 (fn Const(@{const_name UU}, _) => true | _ => false) |
|
172 *} |
|
173 |
|
174 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc |
|
175 |
|
176 context pcpo |
|
177 begin |
|
178 |
|
179 text {* useful lemmas about @{term \<bottom>} *} |
|
180 |
|
181 lemma below_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)" |
|
182 by (simp add: po_eq_conv) |
|
183 |
|
184 lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)" |
|
185 by simp |
|
186 |
|
187 lemma UU_I: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>" |
|
188 by (subst eq_UU_iff) |
|
189 |
|
190 lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)" |
|
191 by (simp only: eq_UU_iff lub_below_iff) |
|
192 |
|
193 lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = \<bottom>" |
|
194 by (simp add: lub_eq_bottom_iff) |
|
195 |
|
196 lemma chain_UU_I_inverse: "\<forall>i::nat. Y i = \<bottom> \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom>" |
|
197 by simp |
|
198 |
|
199 lemma chain_UU_I_inverse2: "(\<Squnion>i. Y i) \<noteq> \<bottom> \<Longrightarrow> \<exists>i::nat. Y i \<noteq> \<bottom>" |
|
200 by (blast intro: chain_UU_I_inverse) |
|
201 |
|
202 lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>" |
|
203 by (blast intro: UU_I) |
|
204 |
|
205 end |
|
206 |
|
207 subsection {* Chain-finite and flat cpos *} |
|
208 |
|
209 text {* further useful classes for HOLCF domains *} |
|
210 |
|
211 class chfin = po + |
|
212 assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y" |
|
213 begin |
|
214 |
|
215 subclass cpo |
|
216 apply default |
|
217 apply (frule chfin) |
|
218 apply (blast intro: lub_finch1) |
|
219 done |
|
220 |
|
221 lemma chfin2finch: "chain Y \<Longrightarrow> finite_chain Y" |
|
222 by (simp add: chfin finite_chain_def) |
|
223 |
|
224 end |
|
225 |
|
226 class flat = pcpo + |
|
227 assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y" |
|
228 begin |
|
229 |
|
230 subclass chfin |
|
231 apply default |
|
232 apply (unfold max_in_chain_def) |
|
233 apply (case_tac "\<forall>i. Y i = \<bottom>") |
|
234 apply simp |
|
235 apply simp |
|
236 apply (erule exE) |
|
237 apply (rule_tac x="i" in exI) |
|
238 apply clarify |
|
239 apply (blast dest: chain_mono ax_flat) |
|
240 done |
|
241 |
|
242 lemma flat_below_iff: |
|
243 shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)" |
|
244 by (safe dest!: ax_flat) |
|
245 |
|
246 lemma flat_eq: "a \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)" |
|
247 by (safe dest!: ax_flat) |
|
248 |
|
249 end |
|
250 |
|
251 subsection {* Discrete cpos *} |
|
252 |
|
253 class discrete_cpo = below + |
|
254 assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y" |
|
255 begin |
|
256 |
|
257 subclass po |
|
258 proof qed simp_all |
|
259 |
|
260 text {* In a discrete cpo, every chain is constant *} |
|
261 |
|
262 lemma discrete_chain_const: |
|
263 assumes S: "chain S" |
|
264 shows "\<exists>x. S = (\<lambda>i. x)" |
|
265 proof (intro exI ext) |
|
266 fix i :: nat |
|
267 have "S 0 \<sqsubseteq> S i" using S le0 by (rule chain_mono) |
|
268 hence "S 0 = S i" by simp |
|
269 thus "S i = S 0" by (rule sym) |
|
270 qed |
|
271 |
|
272 subclass chfin |
|
273 proof |
|
274 fix S :: "nat \<Rightarrow> 'a" |
|
275 assume S: "chain S" |
|
276 hence "\<exists>x. S = (\<lambda>i. x)" by (rule discrete_chain_const) |
|
277 hence "max_in_chain 0 S" |
|
278 unfolding max_in_chain_def by auto |
|
279 thus "\<exists>i. max_in_chain i S" .. |
|
280 qed |
|
281 |
|
282 end |
|
283 |
|
284 end |