8 imports Bifinite |
8 imports Bifinite |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Ordering on sum type *} |
11 subsection {* Ordering on sum type *} |
12 |
12 |
13 instantiation "+" :: (below, below) below |
13 instantiation sum :: (below, below) below |
14 begin |
14 begin |
15 |
15 |
16 definition below_sum_def: |
16 definition below_sum_def: |
17 "x \<sqsubseteq> y \<equiv> case x of |
17 "x \<sqsubseteq> y \<equiv> case x of |
18 Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) | |
18 Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) | |
54 \<Longrightarrow> R" |
54 \<Longrightarrow> R" |
55 by (cases x, safe elim!: sum_below_elims, auto) |
55 by (cases x, safe elim!: sum_below_elims, auto) |
56 |
56 |
57 subsection {* Sum type is a complete partial order *} |
57 subsection {* Sum type is a complete partial order *} |
58 |
58 |
59 instance "+" :: (po, po) po |
59 instance sum :: (po, po) po |
60 proof |
60 proof |
61 fix x :: "'a + 'b" |
61 fix x :: "'a + 'b" |
62 show "x \<sqsubseteq> x" |
62 show "x \<sqsubseteq> x" |
63 by (induct x, simp_all) |
63 by (induct x, simp_all) |
64 next |
64 next |
115 apply (erule is_lub_lub) |
115 apply (erule is_lub_lub) |
116 apply (rule ub_rangeI) |
116 apply (rule ub_rangeI) |
117 apply (drule ub_rangeD, simp) |
117 apply (drule ub_rangeD, simp) |
118 done |
118 done |
119 |
119 |
120 instance "+" :: (cpo, cpo) cpo |
120 instance sum :: (cpo, cpo) cpo |
121 apply intro_classes |
121 apply intro_classes |
122 apply (erule sum_chain_cases, safe) |
122 apply (erule sum_chain_cases, safe) |
123 apply (rule exI) |
123 apply (rule exI) |
124 apply (rule is_lub_Inl) |
124 apply (rule is_lub_Inl) |
125 apply (erule cpo_lubI) |
125 apply (erule cpo_lubI) |
215 by (safe elim!: compact_Inl compact_Inl_rev) |
215 by (safe elim!: compact_Inl compact_Inl_rev) |
216 |
216 |
217 lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a" |
217 lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a" |
218 by (safe elim!: compact_Inr compact_Inr_rev) |
218 by (safe elim!: compact_Inr compact_Inr_rev) |
219 |
219 |
220 instance "+" :: (chfin, chfin) chfin |
220 instance sum :: (chfin, chfin) chfin |
221 apply intro_classes |
221 apply intro_classes |
222 apply (erule compact_imp_max_in_chain) |
222 apply (erule compact_imp_max_in_chain) |
223 apply (case_tac "\<Squnion>i. Y i", simp_all) |
223 apply (case_tac "\<Squnion>i. Y i", simp_all) |
224 done |
224 done |
225 |
225 |
226 instance "+" :: (finite_po, finite_po) finite_po .. |
226 instance sum :: (finite_po, finite_po) finite_po .. |
227 |
227 |
228 instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo |
228 instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo |
229 by intro_classes (simp add: below_sum_def split: sum.split) |
229 by intro_classes (simp add: below_sum_def split: sum.split) |
230 |
230 |
231 subsection {* Sum type is a bifinite domain *} |
231 subsection {* Sum type is a bifinite domain *} |
232 |
232 |
233 instantiation "+" :: (profinite, profinite) profinite |
233 instantiation sum :: (profinite, profinite) profinite |
234 begin |
234 begin |
235 |
235 |
236 definition |
236 definition |
237 approx_sum_def: "approx = |
237 approx_sum_def: "approx = |
238 (\<lambda>n. \<Lambda> x. case x of Inl a \<Rightarrow> Inl (approx n\<cdot>a) | Inr b \<Rightarrow> Inr (approx n\<cdot>b))" |
238 (\<lambda>n. \<Lambda> x. case x of Inl a \<Rightarrow> Inl (approx n\<cdot>a) | Inr b \<Rightarrow> Inr (approx n\<cdot>b))" |