40 by (simp add: lub_below_iff) |
39 by (simp add: lub_below_iff) |
41 |
40 |
42 lemma below_lub: "\<lbrakk>chain S; x \<sqsubseteq> S i\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. S i)" |
41 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) |
42 by (erule below_trans, erule is_ub_thelub) |
44 |
43 |
45 lemma lub_range_mono: |
44 lemma lub_range_mono: "\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk> \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" |
46 "\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk> |
45 apply (erule lub_below) |
47 \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" |
46 apply (subgoal_tac "\<exists>j. X i = Y j") |
48 apply (erule lub_below) |
47 apply clarsimp |
49 apply (subgoal_tac "\<exists>j. X i = Y j") |
48 apply (erule is_ub_thelub) |
50 apply clarsimp |
49 apply auto |
51 apply (erule is_ub_thelub) |
50 done |
52 apply auto |
51 |
53 done |
52 lemma lub_range_shift: "chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)" |
54 |
53 apply (rule below_antisym) |
55 lemma lub_range_shift: |
54 apply (rule lub_range_mono) |
56 "chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)" |
55 apply fast |
57 apply (rule below_antisym) |
56 apply assumption |
58 apply (rule lub_range_mono) |
57 apply (erule chain_shift) |
59 apply fast |
58 apply (rule lub_below) |
60 apply assumption |
59 apply assumption |
61 apply (erule chain_shift) |
60 apply (rule_tac i="i" in below_lub) |
62 apply (rule lub_below) |
61 apply (erule chain_shift) |
63 apply assumption |
62 apply (erule chain_mono) |
64 apply (rule_tac i="i" in below_lub) |
63 apply (rule le_add1) |
65 apply (erule chain_shift) |
64 done |
66 apply (erule chain_mono) |
65 |
67 apply (rule le_add1) |
66 lemma maxinch_is_thelub: "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)" |
68 done |
67 apply (rule iffI) |
69 |
68 apply (fast intro!: lub_eqI lub_finch1) |
70 lemma maxinch_is_thelub: |
69 apply (unfold max_in_chain_def) |
71 "chain Y \<Longrightarrow> max_in_chain i Y = ((\<Squnion>i. Y i) = Y i)" |
70 apply (safe intro!: below_antisym) |
72 apply (rule iffI) |
71 apply (fast elim!: chain_mono) |
73 apply (fast intro!: lub_eqI lub_finch1) |
72 apply (drule sym) |
74 apply (unfold max_in_chain_def) |
73 apply (force elim!: is_ub_thelub) |
75 apply (safe intro!: below_antisym) |
74 done |
76 apply (fast elim!: chain_mono) |
|
77 apply (drule sym) |
|
78 apply (force elim!: is_ub_thelub) |
|
79 done |
|
80 |
75 |
81 text \<open>the \<open>\<sqsubseteq>\<close> relation between two chains is preserved by their lubs\<close> |
76 text \<open>the \<open>\<sqsubseteq>\<close> relation between two chains is preserved by their lubs\<close> |
82 |
77 |
83 lemma lub_mono: |
78 lemma lub_mono: "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" |
84 "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> |
79 by (fast elim: lub_below below_lub) |
85 \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" |
|
86 by (fast elim: lub_below below_lub) |
|
87 |
80 |
88 text \<open>the = relation between two chains is preserved by their lubs\<close> |
81 text \<open>the = relation between two chains is preserved by their lubs\<close> |
89 |
82 |
90 lemma lub_eq: |
83 lemma lub_eq: "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" |
91 "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" |
|
92 by simp |
84 by simp |
93 |
85 |
94 lemma ch2ch_lub: |
86 lemma ch2ch_lub: |
95 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" |
87 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" |
96 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" |
88 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" |
97 shows "chain (\<lambda>i. \<Squnion>j. Y i j)" |
89 shows "chain (\<lambda>i. \<Squnion>j. Y i j)" |
98 apply (rule chainI) |
90 apply (rule chainI) |
99 apply (rule lub_mono [OF 2 2]) |
91 apply (rule lub_mono [OF 2 2]) |
100 apply (rule chainE [OF 1]) |
92 apply (rule chainE [OF 1]) |
101 done |
93 done |
102 |
94 |
103 lemma diag_lub: |
95 lemma diag_lub: |
104 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" |
96 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" |
105 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" |
97 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" |
106 shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)" |
98 shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)" |
107 proof (rule below_antisym) |
99 proof (rule below_antisym) |
108 have 3: "chain (\<lambda>i. Y i i)" |
100 have 3: "chain (\<lambda>i. Y i i)" |
109 apply (rule chainI) |
101 apply (rule chainI) |
110 apply (rule below_trans) |
102 apply (rule below_trans) |
111 apply (rule chainE [OF 1]) |
103 apply (rule chainE [OF 1]) |
112 apply (rule chainE [OF 2]) |
104 apply (rule chainE [OF 2]) |
113 done |
105 done |
114 have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)" |
106 have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)" |
115 by (rule ch2ch_lub [OF 1 2]) |
107 by (rule ch2ch_lub [OF 1 2]) |
116 show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)" |
108 show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)" |
117 apply (rule lub_below [OF 4]) |
109 apply (rule lub_below [OF 4]) |
118 apply (rule lub_below [OF 2]) |
110 apply (rule lub_below [OF 2]) |
119 apply (rule below_lub [OF 3]) |
111 apply (rule below_lub [OF 3]) |
120 apply (rule below_trans) |
112 apply (rule below_trans) |
121 apply (rule chain_mono [OF 1 max.cobounded1]) |
113 apply (rule chain_mono [OF 1 max.cobounded1]) |
122 apply (rule chain_mono [OF 2 max.cobounded2]) |
114 apply (rule chain_mono [OF 2 max.cobounded2]) |
123 done |
115 done |
124 show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)" |
116 show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)" |
125 apply (rule lub_mono [OF 3 4]) |
117 apply (rule lub_mono [OF 3 4]) |
126 apply (rule is_ub_thelub [OF 2]) |
118 apply (rule is_ub_thelub [OF 2]) |
145 |
138 |
146 definition bottom :: "'a" ("\<bottom>") |
139 definition bottom :: "'a" ("\<bottom>") |
147 where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)" |
140 where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)" |
148 |
141 |
149 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x" |
142 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x" |
150 unfolding bottom_def |
143 unfolding bottom_def |
151 apply (rule the1I2) |
144 apply (rule the1I2) |
152 apply (rule ex_ex1I) |
145 apply (rule ex_ex1I) |
153 apply (rule least) |
146 apply (rule least) |
154 apply (blast intro: below_antisym) |
147 apply (blast intro: below_antisym) |
155 apply simp |
148 apply simp |
156 done |
149 done |
157 |
150 |
158 end |
151 end |
159 |
152 |
160 text \<open>Old "UU" syntax:\<close> |
153 text \<open>Old "UU" syntax:\<close> |
161 |
154 |
162 syntax UU :: logic |
155 syntax UU :: logic |
163 |
156 translations "UU" \<rightharpoonup> "CONST bottom" |
164 translations "UU" => "CONST bottom" |
|
165 |
157 |
166 text \<open>Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}.\<close> |
158 text \<open>Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}.\<close> |
167 |
159 setup \<open>Reorient_Proc.add (fn Const(\<^const_name>\<open>bottom\<close>, _) => true | _ => false)\<close> |
168 setup \<open> |
|
169 Reorient_Proc.add |
|
170 (fn Const(@{const_name bottom}, _) => true | _ => false) |
|
171 \<close> |
|
172 |
|
173 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc |
160 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc |
174 |
161 |
175 text \<open>useful lemmas about @{term \<bottom>}\<close> |
162 text \<open>useful lemmas about @{term \<bottom>}\<close> |
176 |
163 |
177 lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)" |
164 lemma below_bottom_iff [simp]: "x \<sqsubseteq> \<bottom> \<longleftrightarrow> x = \<bottom>" |
178 by (simp add: po_eq_conv) |
165 by (simp add: po_eq_conv) |
179 |
166 |
180 lemma eq_bottom_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)" |
167 lemma eq_bottom_iff: "x = \<bottom> \<longleftrightarrow> x \<sqsubseteq> \<bottom>" |
181 by simp |
168 by simp |
182 |
169 |
183 lemma bottomI: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>" |
170 lemma bottomI: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>" |
184 by (subst eq_bottom_iff) |
171 by (subst eq_bottom_iff) |
185 |
172 |
186 lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)" |
173 lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)" |
187 by (simp only: eq_bottom_iff lub_below_iff) |
174 by (simp only: eq_bottom_iff lub_below_iff) |
|
175 |
188 |
176 |
189 subsection \<open>Chain-finite and flat cpos\<close> |
177 subsection \<open>Chain-finite and flat cpos\<close> |
190 |
178 |
191 text \<open>further useful classes for HOLCF domains\<close> |
179 text \<open>further useful classes for HOLCF domains\<close> |
192 |
180 |
193 class chfin = po + |
181 class chfin = po + |
194 assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y" |
182 assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y" |
195 begin |
183 begin |
196 |
184 |
197 subclass cpo |
185 subclass cpo |
198 apply standard |
186 apply standard |
199 apply (frule chfin) |
187 apply (frule chfin) |
200 apply (blast intro: lub_finch1) |
188 apply (blast intro: lub_finch1) |
201 done |
189 done |
202 |
190 |
203 lemma chfin2finch: "chain Y \<Longrightarrow> finite_chain Y" |
191 lemma chfin2finch: "chain Y \<Longrightarrow> finite_chain Y" |
204 by (simp add: chfin finite_chain_def) |
192 by (simp add: chfin finite_chain_def) |
205 |
193 |
206 end |
194 end |
235 class discrete_cpo = below + |
222 class discrete_cpo = below + |
236 assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y" |
223 assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y" |
237 begin |
224 begin |
238 |
225 |
239 subclass po |
226 subclass po |
240 proof qed simp_all |
227 by standard simp_all |
241 |
228 |
242 text \<open>In a discrete cpo, every chain is constant\<close> |
229 text \<open>In a discrete cpo, every chain is constant\<close> |
243 |
230 |
244 lemma discrete_chain_const: |
231 lemma discrete_chain_const: |
245 assumes S: "chain S" |
232 assumes S: "chain S" |
246 shows "\<exists>x. S = (\<lambda>i. x)" |
233 shows "\<exists>x. S = (\<lambda>i. x)" |
247 proof (intro exI ext) |
234 proof (intro exI ext) |
248 fix i :: nat |
235 fix i :: nat |
249 have "S 0 \<sqsubseteq> S i" using S le0 by (rule chain_mono) |
236 from S le0 have "S 0 \<sqsubseteq> S i" by (rule chain_mono) |
250 hence "S 0 = S i" by simp |
237 then have "S 0 = S i" by simp |
251 thus "S i = S 0" by (rule sym) |
238 then show "S i = S 0" by (rule sym) |
252 qed |
239 qed |
253 |
240 |
254 subclass chfin |
241 subclass chfin |
255 proof |
242 proof |
256 fix S :: "nat \<Rightarrow> 'a" |
243 fix S :: "nat \<Rightarrow> 'a" |
257 assume S: "chain S" |
244 assume S: "chain S" |
258 hence "\<exists>x. S = (\<lambda>i. x)" by (rule discrete_chain_const) |
245 then have "\<exists>x. S = (\<lambda>i. x)" |
259 hence "max_in_chain 0 S" |
246 by (rule discrete_chain_const) |
260 unfolding max_in_chain_def by auto |
247 then have "max_in_chain 0 S" |
261 thus "\<exists>i. max_in_chain i S" .. |
248 by (auto simp: max_in_chain_def) |
|
249 then show "\<exists>i. max_in_chain i S" .. |
262 qed |
250 qed |
263 |
251 |
264 end |
252 end |
265 |
253 |
266 end |
254 end |