47 apply (fast intro: antisym_less) |
47 apply (fast intro: antisym_less) |
48 done |
48 done |
49 |
49 |
50 lemma trans_less_cprod: "\<lbrakk>(p1::'a*'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p3\<rbrakk> \<Longrightarrow> p1 \<sqsubseteq> p3" |
50 lemma trans_less_cprod: "\<lbrakk>(p1::'a*'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p3\<rbrakk> \<Longrightarrow> p1 \<sqsubseteq> p3" |
51 apply (unfold less_cprod_def) |
51 apply (unfold less_cprod_def) |
52 apply (rule conjI) |
|
53 apply (fast intro: trans_less) |
|
54 apply (fast intro: trans_less) |
52 apply (fast intro: trans_less) |
55 done |
53 done |
56 |
54 |
57 instance "*" :: (cpo, cpo) po |
55 instance "*" :: (cpo, cpo) po |
58 by intro_classes |
56 by intro_classes |
62 subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *} |
60 subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *} |
63 |
61 |
64 text {* Pair @{text "(_,_)"} is monotone in both arguments *} |
62 text {* Pair @{text "(_,_)"} is monotone in both arguments *} |
65 |
63 |
66 lemma monofun_pair1: "monofun (\<lambda>x. (x, y))" |
64 lemma monofun_pair1: "monofun (\<lambda>x. (x, y))" |
67 by (simp add: monofun less_cprod_def) |
65 by (simp add: monofun_def less_cprod_def) |
68 |
66 |
69 lemma monofun_pair2: "monofun (\<lambda>y. (x, y))" |
67 lemma monofun_pair2: "monofun (\<lambda>y. (x, y))" |
70 by (simp add: monofun less_cprod_def) |
68 by (simp add: monofun_def less_cprod_def) |
71 |
69 |
72 lemma monofun_pair: |
70 lemma monofun_pair: |
73 "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)" |
71 "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)" |
74 by (simp add: less_cprod_def) |
72 by (simp add: less_cprod_def) |
75 |
73 |
76 text {* @{term fst} and @{term snd} are monotone *} |
74 text {* @{term fst} and @{term snd} are monotone *} |
77 |
75 |
78 lemma monofun_fst: "monofun fst" |
76 lemma monofun_fst: "monofun fst" |
79 by (simp add: monofun less_cprod_def) |
77 by (simp add: monofun_def less_cprod_def) |
80 |
78 |
81 lemma monofun_snd: "monofun snd" |
79 lemma monofun_snd: "monofun snd" |
82 by (simp add: monofun less_cprod_def) |
80 by (simp add: monofun_def less_cprod_def) |
83 |
81 |
84 subsection {* Type @{typ "'a * 'b"} is a cpo *} |
82 subsection {* Type @{typ "'a * 'b"} is a cpo *} |
85 |
83 |
86 lemma lub_cprod: |
84 lemma lub_cprod: |
87 "chain S \<Longrightarrow> range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
85 "chain S \<Longrightarrow> range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
88 apply (rule is_lubI) |
86 apply (rule is_lubI) |
89 apply (rule ub_rangeI) |
87 apply (rule ub_rangeI) |
90 apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst]) |
88 apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst]) |
91 apply (rule monofun_pair) |
89 apply (rule monofun_pair) |
92 apply (rule is_ub_thelub) |
90 apply (rule is_ub_thelub) |
133 |
131 |
134 |
132 |
135 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} |
133 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} |
136 |
134 |
137 lemma contlub_pair1: "contlub (\<lambda>x. (x,y))" |
135 lemma contlub_pair1: "contlub (\<lambda>x. (x,y))" |
138 apply (rule contlubI [rule_format]) |
136 apply (rule contlubI) |
139 apply (subst thelub_cprod) |
137 apply (subst thelub_cprod) |
140 apply (erule monofun_pair1 [THEN ch2ch_monofun]) |
138 apply (erule monofun_pair1 [THEN ch2ch_monofun]) |
141 apply (simp add: thelub_const) |
139 apply (simp add: thelub_const) |
142 done |
140 done |
143 |
141 |
144 lemma contlub_pair2: "contlub (\<lambda>y. (x, y))" |
142 lemma contlub_pair2: "contlub (\<lambda>y. (x, y))" |
145 apply (rule contlubI [rule_format]) |
143 apply (rule contlubI) |
146 apply (subst thelub_cprod) |
144 apply (subst thelub_cprod) |
147 apply (erule monofun_pair2 [THEN ch2ch_monofun]) |
145 apply (erule monofun_pair2 [THEN ch2ch_monofun]) |
148 apply (simp add: thelub_const) |
146 apply (simp add: thelub_const) |
149 done |
147 done |
150 |
148 |
159 apply (rule monofun_pair2) |
157 apply (rule monofun_pair2) |
160 apply (rule contlub_pair2) |
158 apply (rule contlub_pair2) |
161 done |
159 done |
162 |
160 |
163 lemma contlub_fst: "contlub fst" |
161 lemma contlub_fst: "contlub fst" |
164 apply (rule contlubI [rule_format]) |
162 apply (rule contlubI) |
165 apply (simp add: lub_cprod [THEN thelubI]) |
163 apply (simp add: thelub_cprod) |
166 done |
164 done |
167 |
165 |
168 lemma contlub_snd: "contlub snd" |
166 lemma contlub_snd: "contlub snd" |
169 apply (rule contlubI [rule_format]) |
167 apply (rule contlubI) |
170 apply (simp add: lub_cprod [THEN thelubI]) |
168 apply (simp add: thelub_cprod) |
171 done |
169 done |
172 |
170 |
173 lemma cont_fst: "cont fst" |
171 lemma cont_fst: "cont fst" |
174 apply (rule monocontlub2cont) |
172 apply (rule monocontlub2cont) |
175 apply (rule monofun_fst) |
173 apply (rule monofun_fst) |
252 by (simp add: cpair_eq_pair) |
250 by (simp add: cpair_eq_pair) |
253 |
251 |
254 lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')" |
252 lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')" |
255 by (simp add: cpair_eq_pair less_cprod_def) |
253 by (simp add: cpair_eq_pair less_cprod_def) |
256 |
254 |
|
255 lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>" |
|
256 by (simp add: cpair_eq_pair inst_cprod_pcpo) |
|
257 |
257 lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>" |
258 lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>" |
258 by (simp add: cpair_eq_pair inst_cprod_pcpo) |
259 by (simp add: cpair_eq_pair inst_cprod_pcpo) |
259 |
260 |
260 lemma defined_cpair_rev: |
261 lemma defined_cpair_rev: |
261 "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>" |
262 "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>" |
265 by (simp add: cpair_eq_pair) |
266 by (simp add: cpair_eq_pair) |
266 |
267 |
267 lemma cprodE: "\<lbrakk>\<And>x y. p = <x, y> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
268 lemma cprodE: "\<lbrakk>\<And>x y. p = <x, y> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
268 by (cut_tac Exh_Cprod2, auto) |
269 by (cut_tac Exh_Cprod2, auto) |
269 |
270 |
270 lemma cfst2 [simp]: "cfst\<cdot><x, y> = x" |
271 lemma cfst_cpair [simp]: "cfst\<cdot><x, y> = x" |
271 by (simp add: cpair_eq_pair cfst_def cont_fst) |
272 by (simp add: cpair_eq_pair cfst_def cont_fst) |
272 |
273 |
273 lemma csnd2 [simp]: "csnd\<cdot><x, y> = y" |
274 lemma csnd_cpair [simp]: "csnd\<cdot><x, y> = y" |
274 by (simp add: cpair_eq_pair csnd_def cont_snd) |
275 by (simp add: cpair_eq_pair csnd_def cont_snd) |
275 |
276 |
276 lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>" |
277 lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>" |
277 by (simp add: inst_cprod_pcpo2) |
278 by (simp add: inst_cprod_pcpo2) |
278 |
279 |