152 upper_pd.extension_mono PDPlus_upper_mono) |
152 upper_pd.extension_mono PDPlus_upper_mono) |
153 |
153 |
154 interpretation upper_add: semilattice upper_add proof |
154 interpretation upper_add: semilattice upper_add proof |
155 fix xs ys zs :: "'a upper_pd" |
155 fix xs ys zs :: "'a upper_pd" |
156 show "(xs \<union>\<sharp> ys) \<union>\<sharp> zs = xs \<union>\<sharp> (ys \<union>\<sharp> zs)" |
156 show "(xs \<union>\<sharp> ys) \<union>\<sharp> zs = xs \<union>\<sharp> (ys \<union>\<sharp> zs)" |
157 apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp) |
157 apply (induct xs rule: upper_pd.principal_induct, simp) |
158 apply (rule_tac x=zs in upper_pd.principal_induct, simp) |
158 apply (induct ys rule: upper_pd.principal_induct, simp) |
|
159 apply (induct zs rule: upper_pd.principal_induct, simp) |
159 apply (simp add: PDPlus_assoc) |
160 apply (simp add: PDPlus_assoc) |
160 done |
161 done |
161 show "xs \<union>\<sharp> ys = ys \<union>\<sharp> xs" |
162 show "xs \<union>\<sharp> ys = ys \<union>\<sharp> xs" |
162 apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp) |
163 apply (induct xs rule: upper_pd.principal_induct, simp) |
|
164 apply (induct ys rule: upper_pd.principal_induct, simp) |
163 apply (simp add: PDPlus_commute) |
165 apply (simp add: PDPlus_commute) |
164 done |
166 done |
165 show "xs \<union>\<sharp> xs = xs" |
167 show "xs \<union>\<sharp> xs = xs" |
166 apply (induct xs rule: upper_pd.principal_induct, simp) |
168 apply (induct xs rule: upper_pd.principal_induct, simp) |
167 apply (simp add: PDPlus_absorb) |
169 apply (simp add: PDPlus_absorb) |
181 text {* Useful for @{text "simp only: upper_plus_aci"} *} |
183 text {* Useful for @{text "simp only: upper_plus_aci"} *} |
182 lemmas upper_plus_aci = |
184 lemmas upper_plus_aci = |
183 upper_plus_ac upper_plus_absorb upper_plus_left_absorb |
185 upper_plus_ac upper_plus_absorb upper_plus_left_absorb |
184 |
186 |
185 lemma upper_plus_below1: "xs \<union>\<sharp> ys \<sqsubseteq> xs" |
187 lemma upper_plus_below1: "xs \<union>\<sharp> ys \<sqsubseteq> xs" |
186 apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp) |
188 apply (induct xs rule: upper_pd.principal_induct, simp) |
|
189 apply (induct ys rule: upper_pd.principal_induct, simp) |
187 apply (simp add: PDPlus_upper_le) |
190 apply (simp add: PDPlus_upper_le) |
188 done |
191 done |
189 |
192 |
190 lemma upper_plus_below2: "xs \<union>\<sharp> ys \<sqsubseteq> ys" |
193 lemma upper_plus_below2: "xs \<union>\<sharp> ys \<sqsubseteq> ys" |
191 by (subst upper_plus_commute, rule upper_plus_below1) |
194 by (subst upper_plus_commute, rule upper_plus_below1) |
238 lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>" |
241 lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>" |
239 unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff) |
242 unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff) |
240 |
243 |
241 lemma upper_plus_bottom_iff [simp]: |
244 lemma upper_plus_bottom_iff [simp]: |
242 "xs \<union>\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>" |
245 "xs \<union>\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>" |
243 apply (rule iffI) |
246 apply (induct xs rule: upper_pd.principal_induct, simp) |
244 apply (erule rev_mp) |
247 apply (induct ys rule: upper_pd.principal_induct, simp) |
245 apply (rule upper_pd.principal_induct2 [where x=xs and y=ys], simp, simp) |
|
246 apply (simp add: inst_upper_pd_pcpo upper_pd.principal_eq_iff |
248 apply (simp add: inst_upper_pd_pcpo upper_pd.principal_eq_iff |
247 upper_le_PDPlus_PDUnit_iff) |
249 upper_le_PDPlus_PDUnit_iff) |
248 apply auto |
|
249 done |
250 done |
250 |
251 |
251 lemma compact_upper_unit: "compact x \<Longrightarrow> compact {x}\<sharp>" |
252 lemma compact_upper_unit: "compact x \<Longrightarrow> compact {x}\<sharp>" |
252 by (auto dest!: compact_basis.compact_imp_principal) |
253 by (auto dest!: compact_basis.compact_imp_principal) |
253 |
254 |
350 "upper_bind\<cdot>{x}\<sharp>\<cdot>f = f\<cdot>x" |
351 "upper_bind\<cdot>{x}\<sharp>\<cdot>f = f\<cdot>x" |
351 by (induct x rule: compact_basis.principal_induct, simp, simp) |
352 by (induct x rule: compact_basis.principal_induct, simp, simp) |
352 |
353 |
353 lemma upper_bind_plus [simp]: |
354 lemma upper_bind_plus [simp]: |
354 "upper_bind\<cdot>(xs \<union>\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f \<union>\<sharp> upper_bind\<cdot>ys\<cdot>f" |
355 "upper_bind\<cdot>(xs \<union>\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f \<union>\<sharp> upper_bind\<cdot>ys\<cdot>f" |
355 by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp) |
356 by (induct xs rule: upper_pd.principal_induct, simp, |
|
357 induct ys rule: upper_pd.principal_induct, simp, simp) |
356 |
358 |
357 lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>" |
359 lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>" |
358 unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit) |
360 unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit) |
359 |
361 |
360 lemma upper_bind_bind: |
362 lemma upper_bind_bind: |