30 by intro_classes simp |
30 by intro_classes simp |
31 |
31 |
32 |
32 |
33 subsection {* Product type is a partial order *} |
33 subsection {* Product type is a partial order *} |
34 |
34 |
35 instantiation "*" :: (below, below) below |
35 instantiation prod :: (below, below) below |
36 begin |
36 begin |
37 |
37 |
38 definition |
38 definition |
39 below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)" |
39 below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)" |
40 |
40 |
41 instance .. |
41 instance .. |
42 end |
42 end |
43 |
43 |
44 instance "*" :: (po, po) po |
44 instance prod :: (po, po) po |
45 proof |
45 proof |
46 fix x :: "'a \<times> 'b" |
46 fix x :: "'a \<times> 'b" |
47 show "x \<sqsubseteq> x" |
47 show "x \<sqsubseteq> x" |
48 unfolding below_prod_def by simp |
48 unfolding below_prod_def by simp |
49 next |
49 next |
146 lemma thelub_cprod: |
146 lemma thelub_cprod: |
147 "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo) |
147 "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo) |
148 \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
148 \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
149 by (rule lub_cprod [THEN thelubI]) |
149 by (rule lub_cprod [THEN thelubI]) |
150 |
150 |
151 instance "*" :: (cpo, cpo) cpo |
151 instance prod :: (cpo, cpo) cpo |
152 proof |
152 proof |
153 fix S :: "nat \<Rightarrow> ('a \<times> 'b)" |
153 fix S :: "nat \<Rightarrow> ('a \<times> 'b)" |
154 assume "chain S" |
154 assume "chain S" |
155 hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
155 hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
156 by (rule lub_cprod) |
156 by (rule lub_cprod) |
157 thus "\<exists>x. range S <<| x" .. |
157 thus "\<exists>x. range S <<| x" .. |
158 qed |
158 qed |
159 |
159 |
160 instance "*" :: (finite_po, finite_po) finite_po .. |
160 instance prod :: (finite_po, finite_po) finite_po .. |
161 |
161 |
162 instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo |
162 instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo |
163 proof |
163 proof |
164 fix x y :: "'a \<times> 'b" |
164 fix x y :: "'a \<times> 'b" |
165 show "x \<sqsubseteq> y \<longleftrightarrow> x = y" |
165 show "x \<sqsubseteq> y \<longleftrightarrow> x = y" |
166 unfolding below_prod_def Pair_fst_snd_eq |
166 unfolding below_prod_def Pair_fst_snd_eq |
167 by simp |
167 by simp |
170 subsection {* Product type is pointed *} |
170 subsection {* Product type is pointed *} |
171 |
171 |
172 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p" |
172 lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p" |
173 by (simp add: below_prod_def) |
173 by (simp add: below_prod_def) |
174 |
174 |
175 instance "*" :: (pcpo, pcpo) pcpo |
175 instance prod :: (pcpo, pcpo) pcpo |
176 by intro_classes (fast intro: minimal_cprod) |
176 by intro_classes (fast intro: minimal_cprod) |
177 |
177 |
178 lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)" |
178 lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)" |
179 by (rule minimal_cprod [THEN UU_I, symmetric]) |
179 by (rule minimal_cprod [THEN UU_I, symmetric]) |
180 |
180 |
295 apply (safe intro!: compact_Pair) |
295 apply (safe intro!: compact_Pair) |
296 apply (drule compact_fst, simp) |
296 apply (drule compact_fst, simp) |
297 apply (drule compact_snd, simp) |
297 apply (drule compact_snd, simp) |
298 done |
298 done |
299 |
299 |
300 instance "*" :: (chfin, chfin) chfin |
300 instance prod :: (chfin, chfin) chfin |
301 apply intro_classes |
301 apply intro_classes |
302 apply (erule compact_imp_max_in_chain) |
302 apply (erule compact_imp_max_in_chain) |
303 apply (case_tac "\<Squnion>i. Y i", simp) |
303 apply (case_tac "\<Squnion>i. Y i", simp) |
304 done |
304 done |
305 |
305 |