136 |
136 |
137 lemma contlub_pair1: "contlub (\<lambda>x. (x,y))" |
137 lemma contlub_pair1: "contlub (\<lambda>x. (x,y))" |
138 apply (rule contlubI [rule_format]) |
138 apply (rule contlubI [rule_format]) |
139 apply (subst thelub_cprod) |
139 apply (subst thelub_cprod) |
140 apply (erule monofun_pair1 [THEN ch2ch_monofun]) |
140 apply (erule monofun_pair1 [THEN ch2ch_monofun]) |
141 apply (simp add: lub_const [THEN thelubI]) |
141 apply (simp add: thelub_const) |
142 done |
142 done |
143 |
143 |
144 lemma contlub_pair2: "contlub (\<lambda>y. (x, y))" |
144 lemma contlub_pair2: "contlub (\<lambda>y. (x, y))" |
145 apply (rule contlubI [rule_format]) |
145 apply (rule contlubI [rule_format]) |
146 apply (subst thelub_cprod) |
146 apply (subst thelub_cprod) |
147 apply (erule monofun_pair2 [THEN ch2ch_monofun]) |
147 apply (erule monofun_pair2 [THEN ch2ch_monofun]) |
148 apply (simp add: lub_const [THEN thelubI]) |
148 apply (simp add: thelub_const) |
149 done |
149 done |
150 |
150 |
151 lemma cont_pair1: "cont (\<lambda>x. (x, y))" |
151 lemma cont_pair1: "cont (\<lambda>x. (x, y))" |
152 apply (rule monocontlub2cont) |
152 apply (rule monocontlub2cont) |
153 apply (rule monofun_pair1) |
153 apply (rule monofun_pair1) |