16 "[| is_chain(Y); x~= UU; lub(range(Y))~= UU |] ==>\ |
16 "[| is_chain(Y); x~= UU; lub(range(Y))~= UU |] ==>\ |
17 \ Ispair (lub(range Y)) x =\ |
17 \ Ispair (lub(range Y)) x =\ |
18 \ Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) \ |
18 \ Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) \ |
19 \ (lub(range(%i. Issnd(Ispair(Y i) x))))" |
19 \ (lub(range(%i. Issnd(Ispair(Y i) x))))" |
20 (fn prems => |
20 (fn prems => |
21 [ |
21 [ |
22 (cut_facts_tac prems 1), |
22 (cut_facts_tac prems 1), |
23 (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1), |
23 (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1), |
24 (rtac lub_equal 1), |
24 (rtac lub_equal 1), |
25 (atac 1), |
25 (atac 1), |
26 (rtac (monofun_Isfst RS ch2ch_monofun) 1), |
26 (rtac (monofun_Isfst RS ch2ch_monofun) 1), |
27 (rtac ch2ch_fun 1), |
27 (rtac ch2ch_fun 1), |
28 (rtac (monofun_Ispair1 RS ch2ch_monofun) 1), |
28 (rtac (monofun_Ispair1 RS ch2ch_monofun) 1), |
29 (atac 1), |
29 (atac 1), |
30 (rtac allI 1), |
30 (rtac allI 1), |
31 (asm_simp_tac Sprod0_ss 1), |
31 (asm_simp_tac Sprod0_ss 1), |
32 (rtac sym 1), |
32 (rtac sym 1), |
33 (rtac lub_chain_maxelem 1), |
33 (rtac lub_chain_maxelem 1), |
34 (res_inst_tac [("P","%j.~Y(j)=UU")] exE 1), |
34 (res_inst_tac [("P","%j.~Y(j)=UU")] exE 1), |
35 (rtac (notall2ex RS iffD1) 1), |
35 (rtac (notall2ex RS iffD1) 1), |
36 (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1), |
36 (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1), |
37 (atac 1), |
37 (atac 1), |
38 (rtac chain_UU_I_inverse 1), |
38 (rtac chain_UU_I_inverse 1), |
39 (atac 1), |
39 (atac 1), |
40 (rtac exI 1), |
40 (rtac exI 1), |
41 (etac Issnd2 1), |
41 (etac Issnd2 1), |
42 (rtac allI 1), |
42 (rtac allI 1), |
43 (res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1), |
43 (res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1), |
44 (asm_simp_tac Sprod0_ss 1), |
44 (asm_simp_tac Sprod0_ss 1), |
45 (rtac refl_less 1), |
45 (rtac refl_less 1), |
46 (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1), |
46 (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1), |
47 (etac sym 1), |
47 (etac sym 1), |
48 (asm_simp_tac Sprod0_ss 1), |
48 (asm_simp_tac Sprod0_ss 1), |
49 (rtac minimal 1) |
49 (rtac minimal 1) |
50 ]); |
50 ]); |
51 |
51 |
52 qed_goal "sprod3_lemma2" Sprod3.thy |
52 qed_goal "sprod3_lemma2" Sprod3.thy |
53 "[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\ |
53 "[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\ |
54 \ Ispair (lub(range Y)) x =\ |
54 \ Ispair (lub(range Y)) x =\ |
55 \ Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))\ |
55 \ Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))\ |
56 \ (lub(range(%i. Issnd(Ispair(Y i) x))))" |
56 \ (lub(range(%i. Issnd(Ispair(Y i) x))))" |
57 (fn prems => |
57 (fn prems => |
58 [ |
58 [ |
59 (cut_facts_tac prems 1), |
59 (cut_facts_tac prems 1), |
60 (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1), |
60 (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1), |
61 (atac 1), |
61 (atac 1), |
62 (rtac trans 1), |
62 (rtac trans 1), |
63 (rtac strict_Ispair1 1), |
63 (rtac strict_Ispair1 1), |
64 (rtac (strict_Ispair RS sym) 1), |
64 (rtac (strict_Ispair RS sym) 1), |
65 (rtac disjI1 1), |
65 (rtac disjI1 1), |
66 (rtac chain_UU_I_inverse 1), |
66 (rtac chain_UU_I_inverse 1), |
67 (rtac allI 1), |
67 (rtac allI 1), |
68 (asm_simp_tac Sprod0_ss 1), |
68 (asm_simp_tac Sprod0_ss 1), |
69 (etac (chain_UU_I RS spec) 1), |
69 (etac (chain_UU_I RS spec) 1), |
70 (atac 1) |
70 (atac 1) |
71 ]); |
71 ]); |
72 |
72 |
73 |
73 |
74 qed_goal "sprod3_lemma3" Sprod3.thy |
74 qed_goal "sprod3_lemma3" Sprod3.thy |
75 "[| is_chain(Y); x = UU |] ==>\ |
75 "[| is_chain(Y); x = UU |] ==>\ |
76 \ Ispair (lub(range Y)) x =\ |
76 \ Ispair (lub(range Y)) x =\ |
77 \ Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))\ |
77 \ Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))\ |
78 \ (lub(range(%i. Issnd(Ispair (Y i) x))))" |
78 \ (lub(range(%i. Issnd(Ispair (Y i) x))))" |
79 (fn prems => |
79 (fn prems => |
80 [ |
80 [ |
81 (cut_facts_tac prems 1), |
81 (cut_facts_tac prems 1), |
82 (res_inst_tac [("s","UU"),("t","x")] ssubst 1), |
82 (res_inst_tac [("s","UU"),("t","x")] ssubst 1), |
83 (atac 1), |
83 (atac 1), |
84 (rtac trans 1), |
84 (rtac trans 1), |
85 (rtac strict_Ispair2 1), |
85 (rtac strict_Ispair2 1), |
86 (rtac (strict_Ispair RS sym) 1), |
86 (rtac (strict_Ispair RS sym) 1), |
87 (rtac disjI1 1), |
87 (rtac disjI1 1), |
88 (rtac chain_UU_I_inverse 1), |
88 (rtac chain_UU_I_inverse 1), |
89 (rtac allI 1), |
89 (rtac allI 1), |
90 (simp_tac Sprod0_ss 1) |
90 (simp_tac Sprod0_ss 1) |
91 ]); |
91 ]); |
92 |
92 |
93 |
93 |
94 qed_goal "contlub_Ispair1" Sprod3.thy "contlub(Ispair)" |
94 qed_goal "contlub_Ispair1" Sprod3.thy "contlub(Ispair)" |
95 (fn prems => |
95 (fn prems => |
96 [ |
96 [ |
97 (rtac contlubI 1), |
97 (rtac contlubI 1), |
98 (strip_tac 1), |
98 (strip_tac 1), |
99 (rtac (expand_fun_eq RS iffD2) 1), |
99 (rtac (expand_fun_eq RS iffD2) 1), |
100 (strip_tac 1), |
100 (strip_tac 1), |
101 (rtac (lub_fun RS thelubI RS ssubst) 1), |
101 (rtac (lub_fun RS thelubI RS ssubst) 1), |
102 (etac (monofun_Ispair1 RS ch2ch_monofun) 1), |
102 (etac (monofun_Ispair1 RS ch2ch_monofun) 1), |
103 (rtac trans 1), |
103 (rtac trans 1), |
104 (rtac (thelub_sprod RS sym) 2), |
104 (rtac (thelub_sprod RS sym) 2), |
105 (rtac ch2ch_fun 2), |
105 (rtac ch2ch_fun 2), |
106 (etac (monofun_Ispair1 RS ch2ch_monofun) 2), |
106 (etac (monofun_Ispair1 RS ch2ch_monofun) 2), |
107 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
107 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
108 (res_inst_tac |
108 (res_inst_tac |
109 [("Q","lub(range(Y))=UU")] (excluded_middle RS disjE) 1), |
109 [("Q","lub(range(Y))=UU")] (excluded_middle RS disjE) 1), |
110 (etac sprod3_lemma1 1), |
110 (etac sprod3_lemma1 1), |
111 (atac 1), |
111 (atac 1), |
112 (atac 1), |
112 (atac 1), |
113 (etac sprod3_lemma2 1), |
113 (etac sprod3_lemma2 1), |
114 (atac 1), |
114 (atac 1), |
115 (atac 1), |
115 (atac 1), |
116 (etac sprod3_lemma3 1), |
116 (etac sprod3_lemma3 1), |
117 (atac 1) |
117 (atac 1) |
118 ]); |
118 ]); |
119 |
119 |
120 qed_goal "sprod3_lemma4" Sprod3.thy |
120 qed_goal "sprod3_lemma4" Sprod3.thy |
121 "[| is_chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\ |
121 "[| is_chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\ |
122 \ Ispair x (lub(range Y)) =\ |
122 \ Ispair x (lub(range Y)) =\ |
123 \ Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\ |
123 \ Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\ |
124 \ (lub(range(%i. Issnd (Ispair x (Y i)))))" |
124 \ (lub(range(%i. Issnd (Ispair x (Y i)))))" |
125 (fn prems => |
125 (fn prems => |
126 [ |
126 [ |
127 (cut_facts_tac prems 1), |
127 (cut_facts_tac prems 1), |
128 (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1), |
128 (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1), |
129 (rtac sym 1), |
129 (rtac sym 1), |
130 (rtac lub_chain_maxelem 1), |
130 (rtac lub_chain_maxelem 1), |
131 (res_inst_tac [("P","%j.Y(j)~=UU")] exE 1), |
131 (res_inst_tac [("P","%j.Y(j)~=UU")] exE 1), |
132 (rtac (notall2ex RS iffD1) 1), |
132 (rtac (notall2ex RS iffD1) 1), |
133 (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1), |
133 (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1), |
134 (atac 1), |
134 (atac 1), |
135 (rtac chain_UU_I_inverse 1), |
135 (rtac chain_UU_I_inverse 1), |
136 (atac 1), |
136 (atac 1), |
137 (rtac exI 1), |
137 (rtac exI 1), |
138 (etac Isfst2 1), |
138 (etac Isfst2 1), |
139 (rtac allI 1), |
139 (rtac allI 1), |
140 (res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1), |
140 (res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1), |
141 (asm_simp_tac Sprod0_ss 1), |
141 (asm_simp_tac Sprod0_ss 1), |
142 (rtac refl_less 1), |
142 (rtac refl_less 1), |
143 (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1), |
143 (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1), |
144 (etac sym 1), |
144 (etac sym 1), |
145 (asm_simp_tac Sprod0_ss 1), |
145 (asm_simp_tac Sprod0_ss 1), |
146 (rtac minimal 1), |
146 (rtac minimal 1), |
147 (rtac lub_equal 1), |
147 (rtac lub_equal 1), |
148 (atac 1), |
148 (atac 1), |
149 (rtac (monofun_Issnd RS ch2ch_monofun) 1), |
149 (rtac (monofun_Issnd RS ch2ch_monofun) 1), |
150 (rtac (monofun_Ispair2 RS ch2ch_monofun) 1), |
150 (rtac (monofun_Ispair2 RS ch2ch_monofun) 1), |
151 (atac 1), |
151 (atac 1), |
152 (rtac allI 1), |
152 (rtac allI 1), |
153 (asm_simp_tac Sprod0_ss 1) |
153 (asm_simp_tac Sprod0_ss 1) |
154 ]); |
154 ]); |
155 |
155 |
156 qed_goal "sprod3_lemma5" Sprod3.thy |
156 qed_goal "sprod3_lemma5" Sprod3.thy |
157 "[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\ |
157 "[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\ |
158 \ Ispair x (lub(range Y)) =\ |
158 \ Ispair x (lub(range Y)) =\ |
159 \ Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))\ |
159 \ Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))\ |
160 \ (lub(range(%i. Issnd(Ispair x (Y i)))))" |
160 \ (lub(range(%i. Issnd(Ispair x (Y i)))))" |
161 (fn prems => |
161 (fn prems => |
162 [ |
162 [ |
163 (cut_facts_tac prems 1), |
163 (cut_facts_tac prems 1), |
164 (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1), |
164 (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1), |
165 (atac 1), |
165 (atac 1), |
166 (rtac trans 1), |
166 (rtac trans 1), |
167 (rtac strict_Ispair2 1), |
167 (rtac strict_Ispair2 1), |
168 (rtac (strict_Ispair RS sym) 1), |
168 (rtac (strict_Ispair RS sym) 1), |
169 (rtac disjI2 1), |
169 (rtac disjI2 1), |
170 (rtac chain_UU_I_inverse 1), |
170 (rtac chain_UU_I_inverse 1), |
171 (rtac allI 1), |
171 (rtac allI 1), |
172 (asm_simp_tac Sprod0_ss 1), |
172 (asm_simp_tac Sprod0_ss 1), |
173 (etac (chain_UU_I RS spec) 1), |
173 (etac (chain_UU_I RS spec) 1), |
174 (atac 1) |
174 (atac 1) |
175 ]); |
175 ]); |
176 |
176 |
177 qed_goal "sprod3_lemma6" Sprod3.thy |
177 qed_goal "sprod3_lemma6" Sprod3.thy |
178 "[| is_chain(Y); x = UU |] ==>\ |
178 "[| is_chain(Y); x = UU |] ==>\ |
179 \ Ispair x (lub(range Y)) =\ |
179 \ Ispair x (lub(range Y)) =\ |
180 \ Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\ |
180 \ Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\ |
181 \ (lub(range(%i. Issnd (Ispair x (Y i)))))" |
181 \ (lub(range(%i. Issnd (Ispair x (Y i)))))" |
182 (fn prems => |
182 (fn prems => |
183 [ |
183 [ |
184 (cut_facts_tac prems 1), |
184 (cut_facts_tac prems 1), |
185 (res_inst_tac [("s","UU"),("t","x")] ssubst 1), |
185 (res_inst_tac [("s","UU"),("t","x")] ssubst 1), |
186 (atac 1), |
186 (atac 1), |
187 (rtac trans 1), |
187 (rtac trans 1), |
188 (rtac strict_Ispair1 1), |
188 (rtac strict_Ispair1 1), |
189 (rtac (strict_Ispair RS sym) 1), |
189 (rtac (strict_Ispair RS sym) 1), |
190 (rtac disjI1 1), |
190 (rtac disjI1 1), |
191 (rtac chain_UU_I_inverse 1), |
191 (rtac chain_UU_I_inverse 1), |
192 (rtac allI 1), |
192 (rtac allI 1), |
193 (simp_tac Sprod0_ss 1) |
193 (simp_tac Sprod0_ss 1) |
194 ]); |
194 ]); |
195 |
195 |
196 qed_goal "contlub_Ispair2" Sprod3.thy "contlub(Ispair(x))" |
196 qed_goal "contlub_Ispair2" Sprod3.thy "contlub(Ispair(x))" |
197 (fn prems => |
197 (fn prems => |
198 [ |
198 [ |
199 (rtac contlubI 1), |
199 (rtac contlubI 1), |
200 (strip_tac 1), |
200 (strip_tac 1), |
201 (rtac trans 1), |
201 (rtac trans 1), |
202 (rtac (thelub_sprod RS sym) 2), |
202 (rtac (thelub_sprod RS sym) 2), |
203 (etac (monofun_Ispair2 RS ch2ch_monofun) 2), |
203 (etac (monofun_Ispair2 RS ch2ch_monofun) 2), |
204 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
204 (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), |
205 (res_inst_tac [("Q","lub(range(Y))=UU")] |
205 (res_inst_tac [("Q","lub(range(Y))=UU")] |
206 (excluded_middle RS disjE) 1), |
206 (excluded_middle RS disjE) 1), |
207 (etac sprod3_lemma4 1), |
207 (etac sprod3_lemma4 1), |
208 (atac 1), |
208 (atac 1), |
209 (atac 1), |
209 (atac 1), |
210 (etac sprod3_lemma5 1), |
210 (etac sprod3_lemma5 1), |
211 (atac 1), |
211 (atac 1), |
212 (atac 1), |
212 (atac 1), |
213 (etac sprod3_lemma6 1), |
213 (etac sprod3_lemma6 1), |
214 (atac 1) |
214 (atac 1) |
215 ]); |
215 ]); |
216 |
216 |
217 |
217 |
218 qed_goal "cont_Ispair1" Sprod3.thy "cont(Ispair)" |
218 qed_goal "cont_Ispair1" Sprod3.thy "cont(Ispair)" |
219 (fn prems => |
219 (fn prems => |
220 [ |
220 [ |
221 (rtac monocontlub2cont 1), |
221 (rtac monocontlub2cont 1), |
222 (rtac monofun_Ispair1 1), |
222 (rtac monofun_Ispair1 1), |
223 (rtac contlub_Ispair1 1) |
223 (rtac contlub_Ispair1 1) |
224 ]); |
224 ]); |
225 |
225 |
226 |
226 |
227 qed_goal "cont_Ispair2" Sprod3.thy "cont(Ispair(x))" |
227 qed_goal "cont_Ispair2" Sprod3.thy "cont(Ispair(x))" |
228 (fn prems => |
228 (fn prems => |
229 [ |
229 [ |
230 (rtac monocontlub2cont 1), |
230 (rtac monocontlub2cont 1), |
231 (rtac monofun_Ispair2 1), |
231 (rtac monofun_Ispair2 1), |
232 (rtac contlub_Ispair2 1) |
232 (rtac contlub_Ispair2 1) |
233 ]); |
233 ]); |
234 |
234 |
235 qed_goal "contlub_Isfst" Sprod3.thy "contlub(Isfst)" |
235 qed_goal "contlub_Isfst" Sprod3.thy "contlub(Isfst)" |
236 (fn prems => |
236 (fn prems => |
237 [ |
237 [ |
238 (rtac contlubI 1), |
238 (rtac contlubI 1), |
239 (strip_tac 1), |
239 (strip_tac 1), |
240 (rtac (lub_sprod RS thelubI RS ssubst) 1), |
240 (rtac (lub_sprod RS thelubI RS ssubst) 1), |
241 (atac 1), |
241 (atac 1), |
242 (res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")] |
242 (res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")] |
243 (excluded_middle RS disjE) 1), |
243 (excluded_middle RS disjE) 1), |
244 (asm_simp_tac Sprod0_ss 1), |
244 (asm_simp_tac Sprod0_ss 1), |
245 (res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")] |
245 (res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")] |
246 ssubst 1), |
246 ssubst 1), |
247 (atac 1), |
247 (atac 1), |
248 (rtac trans 1), |
248 (rtac trans 1), |
249 (asm_simp_tac Sprod0_ss 1), |
249 (asm_simp_tac Sprod0_ss 1), |
250 (rtac sym 1), |
250 (rtac sym 1), |
251 (rtac chain_UU_I_inverse 1), |
251 (rtac chain_UU_I_inverse 1), |
252 (rtac allI 1), |
252 (rtac allI 1), |
253 (rtac strict_Isfst 1), |
253 (rtac strict_Isfst 1), |
254 (rtac swap 1), |
254 (rtac swap 1), |
255 (etac (defined_IsfstIssnd RS conjunct2) 2), |
255 (etac (defined_IsfstIssnd RS conjunct2) 2), |
256 (rtac notnotI 1), |
256 (rtac notnotI 1), |
257 (rtac (chain_UU_I RS spec) 1), |
257 (rtac (chain_UU_I RS spec) 1), |
258 (rtac (monofun_Issnd RS ch2ch_monofun) 1), |
258 (rtac (monofun_Issnd RS ch2ch_monofun) 1), |
259 (atac 1), |
259 (atac 1), |
260 (atac 1) |
260 (atac 1) |
261 ]); |
261 ]); |
262 |
262 |
263 |
263 |
264 qed_goal "contlub_Issnd" Sprod3.thy "contlub(Issnd)" |
264 qed_goal "contlub_Issnd" Sprod3.thy "contlub(Issnd)" |
265 (fn prems => |
265 (fn prems => |
266 [ |
266 [ |
267 (rtac contlubI 1), |
267 (rtac contlubI 1), |
268 (strip_tac 1), |
268 (strip_tac 1), |
269 (rtac (lub_sprod RS thelubI RS ssubst) 1), |
269 (rtac (lub_sprod RS thelubI RS ssubst) 1), |
270 (atac 1), |
270 (atac 1), |
271 (res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")] |
271 (res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")] |
272 (excluded_middle RS disjE) 1), |
272 (excluded_middle RS disjE) 1), |
273 (asm_simp_tac Sprod0_ss 1), |
273 (asm_simp_tac Sprod0_ss 1), |
274 (res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")] |
274 (res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")] |
275 ssubst 1), |
275 ssubst 1), |
276 (atac 1), |
276 (atac 1), |
277 (asm_simp_tac Sprod0_ss 1), |
277 (asm_simp_tac Sprod0_ss 1), |
278 (rtac sym 1), |
278 (rtac sym 1), |
279 (rtac chain_UU_I_inverse 1), |
279 (rtac chain_UU_I_inverse 1), |
280 (rtac allI 1), |
280 (rtac allI 1), |
281 (rtac strict_Issnd 1), |
281 (rtac strict_Issnd 1), |
282 (rtac swap 1), |
282 (rtac swap 1), |
283 (etac (defined_IsfstIssnd RS conjunct1) 2), |
283 (etac (defined_IsfstIssnd RS conjunct1) 2), |
284 (rtac notnotI 1), |
284 (rtac notnotI 1), |
285 (rtac (chain_UU_I RS spec) 1), |
285 (rtac (chain_UU_I RS spec) 1), |
286 (rtac (monofun_Isfst RS ch2ch_monofun) 1), |
286 (rtac (monofun_Isfst RS ch2ch_monofun) 1), |
287 (atac 1), |
287 (atac 1), |
288 (atac 1) |
288 (atac 1) |
289 ]); |
289 ]); |
290 |
290 |
291 |
291 |
292 qed_goal "cont_Isfst" Sprod3.thy "cont(Isfst)" |
292 qed_goal "cont_Isfst" Sprod3.thy "cont(Isfst)" |
293 (fn prems => |
293 (fn prems => |
294 [ |
294 [ |
295 (rtac monocontlub2cont 1), |
295 (rtac monocontlub2cont 1), |
296 (rtac monofun_Isfst 1), |
296 (rtac monofun_Isfst 1), |
297 (rtac contlub_Isfst 1) |
297 (rtac contlub_Isfst 1) |
298 ]); |
298 ]); |
299 |
299 |
300 qed_goal "cont_Issnd" Sprod3.thy "cont(Issnd)" |
300 qed_goal "cont_Issnd" Sprod3.thy "cont(Issnd)" |
301 (fn prems => |
301 (fn prems => |
302 [ |
302 [ |
303 (rtac monocontlub2cont 1), |
303 (rtac monocontlub2cont 1), |
304 (rtac monofun_Issnd 1), |
304 (rtac monofun_Issnd 1), |
305 (rtac contlub_Issnd 1) |
305 (rtac contlub_Issnd 1) |
306 ]); |
306 ]); |
307 |
307 |
308 (* |
308 (* |
309 -------------------------------------------------------------------------- |
309 -------------------------------------------------------------------------- |
310 more lemmas for Sprod3.thy |
310 more lemmas for Sprod3.thy |
311 |
311 |
312 -------------------------------------------------------------------------- |
312 -------------------------------------------------------------------------- |
313 *) |
313 *) |
314 |
314 |
315 qed_goal "spair_eq" Sprod3.thy "[|x1=x2;y1=y2|] ==> (|x1,y1|) = (|x2,y2|)" |
315 qed_goal "spair_eq" Sprod3.thy "[|x1=x2;y1=y2|] ==> (|x1,y1|) = (|x2,y2|)" |
316 (fn prems => |
316 (fn prems => |
317 [ |
317 [ |
318 (cut_facts_tac prems 1), |
318 (cut_facts_tac prems 1), |
319 (fast_tac HOL_cs 1) |
319 (fast_tac HOL_cs 1) |
320 ]); |
320 ]); |
321 |
321 |
322 (* ------------------------------------------------------------------------ *) |
322 (* ------------------------------------------------------------------------ *) |
323 (* convert all lemmas to the continuous versions *) |
323 (* convert all lemmas to the continuous versions *) |
324 (* ------------------------------------------------------------------------ *) |
324 (* ------------------------------------------------------------------------ *) |
325 |
325 |
326 qed_goalw "beta_cfun_sprod" Sprod3.thy [spair_def] |
326 qed_goalw "beta_cfun_sprod" Sprod3.thy [spair_def] |
327 "(LAM x y.Ispair x y)`a`b = Ispair a b" |
327 "(LAM x y.Ispair x y)`a`b = Ispair a b" |
328 (fn prems => |
328 (fn prems => |
329 [ |
329 [ |
330 (rtac (beta_cfun RS ssubst) 1), |
330 (rtac (beta_cfun RS ssubst) 1), |
331 (cont_tac 1), |
331 (cont_tac 1), |
332 (rtac cont_Ispair2 1), |
332 (rtac cont_Ispair2 1), |
333 (rtac cont2cont_CF1L 1), |
333 (rtac cont2cont_CF1L 1), |
334 (rtac cont_Ispair1 1), |
334 (rtac cont_Ispair1 1), |
335 (rtac (beta_cfun RS ssubst) 1), |
335 (rtac (beta_cfun RS ssubst) 1), |
336 (rtac cont_Ispair2 1), |
336 (rtac cont_Ispair2 1), |
337 (rtac refl 1) |
337 (rtac refl 1) |
338 ]); |
338 ]); |
339 |
339 |
340 qed_goalw "inject_spair" Sprod3.thy [spair_def] |
340 qed_goalw "inject_spair" Sprod3.thy [spair_def] |
341 "[| aa~=UU ; ba~=UU ; (|a,b|)=(|aa,ba|) |] ==> a=aa & b=ba" |
341 "[| aa~=UU ; ba~=UU ; (|a,b|)=(|aa,ba|) |] ==> a=aa & b=ba" |
342 (fn prems => |
342 (fn prems => |
343 [ |
343 [ |
344 (cut_facts_tac prems 1), |
344 (cut_facts_tac prems 1), |
345 (etac inject_Ispair 1), |
345 (etac inject_Ispair 1), |
346 (atac 1), |
346 (atac 1), |
347 (etac box_equals 1), |
347 (etac box_equals 1), |
348 (rtac beta_cfun_sprod 1), |
348 (rtac beta_cfun_sprod 1), |
349 (rtac beta_cfun_sprod 1) |
349 (rtac beta_cfun_sprod 1) |
350 ]); |
350 ]); |
351 |
351 |
352 qed_goalw "inst_sprod_pcpo2" Sprod3.thy [spair_def] "UU = (|UU,UU|)" |
352 qed_goalw "inst_sprod_pcpo2" Sprod3.thy [spair_def] "UU = (|UU,UU|)" |
353 (fn prems => |
353 (fn prems => |
354 [ |
354 [ |
355 (rtac sym 1), |
355 (rtac sym 1), |
356 (rtac trans 1), |
356 (rtac trans 1), |
357 (rtac beta_cfun_sprod 1), |
357 (rtac beta_cfun_sprod 1), |
358 (rtac sym 1), |
358 (rtac sym 1), |
359 (rtac inst_sprod_pcpo 1) |
359 (rtac inst_sprod_pcpo 1) |
360 ]); |
360 ]); |
361 |
361 |
362 qed_goalw "strict_spair" Sprod3.thy [spair_def] |
362 qed_goalw "strict_spair" Sprod3.thy [spair_def] |
363 "(a=UU | b=UU) ==> (|a,b|)=UU" |
363 "(a=UU | b=UU) ==> (|a,b|)=UU" |
364 (fn prems => |
364 (fn prems => |
365 [ |
365 [ |
366 (cut_facts_tac prems 1), |
366 (cut_facts_tac prems 1), |
367 (rtac trans 1), |
367 (rtac trans 1), |
368 (rtac beta_cfun_sprod 1), |
368 (rtac beta_cfun_sprod 1), |
369 (rtac trans 1), |
369 (rtac trans 1), |
370 (rtac (inst_sprod_pcpo RS sym) 2), |
370 (rtac (inst_sprod_pcpo RS sym) 2), |
371 (etac strict_Ispair 1) |
371 (etac strict_Ispair 1) |
372 ]); |
372 ]); |
373 |
373 |
374 qed_goalw "strict_spair1" Sprod3.thy [spair_def] "(|UU,b|) = UU" |
374 qed_goalw "strict_spair1" Sprod3.thy [spair_def] "(|UU,b|) = UU" |
375 (fn prems => |
375 (fn prems => |
376 [ |
376 [ |
377 (rtac (beta_cfun_sprod RS ssubst) 1), |
377 (rtac (beta_cfun_sprod RS ssubst) 1), |
378 (rtac trans 1), |
378 (rtac trans 1), |
379 (rtac (inst_sprod_pcpo RS sym) 2), |
379 (rtac (inst_sprod_pcpo RS sym) 2), |
380 (rtac strict_Ispair1 1) |
380 (rtac strict_Ispair1 1) |
381 ]); |
381 ]); |
382 |
382 |
383 qed_goalw "strict_spair2" Sprod3.thy [spair_def] "(|a,UU|) = UU" |
383 qed_goalw "strict_spair2" Sprod3.thy [spair_def] "(|a,UU|) = UU" |
384 (fn prems => |
384 (fn prems => |
385 [ |
385 [ |
386 (rtac (beta_cfun_sprod RS ssubst) 1), |
386 (rtac (beta_cfun_sprod RS ssubst) 1), |
387 (rtac trans 1), |
387 (rtac trans 1), |
388 (rtac (inst_sprod_pcpo RS sym) 2), |
388 (rtac (inst_sprod_pcpo RS sym) 2), |
389 (rtac strict_Ispair2 1) |
389 (rtac strict_Ispair2 1) |
390 ]); |
390 ]); |
391 |
391 |
392 qed_goalw "strict_spair_rev" Sprod3.thy [spair_def] |
392 qed_goalw "strict_spair_rev" Sprod3.thy [spair_def] |
393 "(|x,y|)~=UU ==> ~x=UU & ~y=UU" |
393 "(|x,y|)~=UU ==> ~x=UU & ~y=UU" |
394 (fn prems => |
394 (fn prems => |
395 [ |
395 [ |
396 (cut_facts_tac prems 1), |
396 (cut_facts_tac prems 1), |
397 (rtac strict_Ispair_rev 1), |
397 (rtac strict_Ispair_rev 1), |
398 (rtac (beta_cfun_sprod RS subst) 1), |
398 (rtac (beta_cfun_sprod RS subst) 1), |
399 (rtac (inst_sprod_pcpo RS subst) 1), |
399 (rtac (inst_sprod_pcpo RS subst) 1), |
400 (atac 1) |
400 (atac 1) |
401 ]); |
401 ]); |
402 |
402 |
403 qed_goalw "defined_spair_rev" Sprod3.thy [spair_def] |
403 qed_goalw "defined_spair_rev" Sprod3.thy [spair_def] |
404 "(|a,b|) = UU ==> (a = UU | b = UU)" |
404 "(|a,b|) = UU ==> (a = UU | b = UU)" |
405 (fn prems => |
405 (fn prems => |
406 [ |
406 [ |
407 (cut_facts_tac prems 1), |
407 (cut_facts_tac prems 1), |
408 (rtac defined_Ispair_rev 1), |
408 (rtac defined_Ispair_rev 1), |
409 (rtac (beta_cfun_sprod RS subst) 1), |
409 (rtac (beta_cfun_sprod RS subst) 1), |
410 (rtac (inst_sprod_pcpo RS subst) 1), |
410 (rtac (inst_sprod_pcpo RS subst) 1), |
411 (atac 1) |
411 (atac 1) |
412 ]); |
412 ]); |
413 |
413 |
414 qed_goalw "defined_spair" Sprod3.thy [spair_def] |
414 qed_goalw "defined_spair" Sprod3.thy [spair_def] |
415 "[|a~=UU; b~=UU|] ==> (|a,b|) ~= UU" |
415 "[|a~=UU; b~=UU|] ==> (|a,b|) ~= UU" |
416 (fn prems => |
416 (fn prems => |
417 [ |
417 [ |
418 (cut_facts_tac prems 1), |
418 (cut_facts_tac prems 1), |
419 (rtac (beta_cfun_sprod RS ssubst) 1), |
419 (rtac (beta_cfun_sprod RS ssubst) 1), |
420 (rtac (inst_sprod_pcpo RS ssubst) 1), |
420 (rtac (inst_sprod_pcpo RS ssubst) 1), |
421 (etac defined_Ispair 1), |
421 (etac defined_Ispair 1), |
422 (atac 1) |
422 (atac 1) |
423 ]); |
423 ]); |
424 |
424 |
425 qed_goalw "Exh_Sprod2" Sprod3.thy [spair_def] |
425 qed_goalw "Exh_Sprod2" Sprod3.thy [spair_def] |
426 "z=UU | (? a b. z=(|a,b|) & a~=UU & b~=UU)" |
426 "z=UU | (? a b. z=(|a,b|) & a~=UU & b~=UU)" |
427 (fn prems => |
427 (fn prems => |
428 [ |
428 [ |
429 (rtac (Exh_Sprod RS disjE) 1), |
429 (rtac (Exh_Sprod RS disjE) 1), |
430 (rtac disjI1 1), |
430 (rtac disjI1 1), |
431 (rtac (inst_sprod_pcpo RS ssubst) 1), |
431 (rtac (inst_sprod_pcpo RS ssubst) 1), |
432 (atac 1), |
432 (atac 1), |
433 (rtac disjI2 1), |
433 (rtac disjI2 1), |
434 (etac exE 1), |
434 (etac exE 1), |
435 (etac exE 1), |
435 (etac exE 1), |
436 (rtac exI 1), |
436 (rtac exI 1), |
437 (rtac exI 1), |
437 (rtac exI 1), |
438 (rtac conjI 1), |
438 (rtac conjI 1), |
439 (rtac (beta_cfun_sprod RS ssubst) 1), |
439 (rtac (beta_cfun_sprod RS ssubst) 1), |
440 (fast_tac HOL_cs 1), |
440 (fast_tac HOL_cs 1), |
441 (fast_tac HOL_cs 1) |
441 (fast_tac HOL_cs 1) |
442 ]); |
442 ]); |
443 |
443 |
444 |
444 |
445 qed_goalw "sprodE" Sprod3.thy [spair_def] |
445 qed_goalw "sprodE" Sprod3.thy [spair_def] |
446 "[|p=UU ==> Q;!!x y. [|p=(|x,y|);x~=UU ; y~=UU|] ==> Q|] ==> Q" |
446 "[|p=UU ==> Q;!!x y. [|p=(|x,y|);x~=UU ; y~=UU|] ==> Q|] ==> Q" |
447 (fn prems => |
447 (fn prems => |
448 [ |
448 [ |
449 (rtac IsprodE 1), |
449 (rtac IsprodE 1), |
450 (resolve_tac prems 1), |
450 (resolve_tac prems 1), |
451 (rtac (inst_sprod_pcpo RS ssubst) 1), |
451 (rtac (inst_sprod_pcpo RS ssubst) 1), |
452 (atac 1), |
452 (atac 1), |
453 (resolve_tac prems 1), |
453 (resolve_tac prems 1), |
454 (atac 2), |
454 (atac 2), |
455 (atac 2), |
455 (atac 2), |
456 (rtac (beta_cfun_sprod RS ssubst) 1), |
456 (rtac (beta_cfun_sprod RS ssubst) 1), |
457 (atac 1) |
457 (atac 1) |
458 ]); |
458 ]); |
459 |
459 |
460 |
460 |
461 qed_goalw "strict_sfst" Sprod3.thy [sfst_def] |
461 qed_goalw "strict_sfst" Sprod3.thy [sfst_def] |
462 "p=UU==>sfst`p=UU" |
462 "p=UU==>sfst`p=UU" |
463 (fn prems => |
463 (fn prems => |
464 [ |
464 [ |
465 (cut_facts_tac prems 1), |
465 (cut_facts_tac prems 1), |
466 (rtac (beta_cfun RS ssubst) 1), |
466 (rtac (beta_cfun RS ssubst) 1), |
467 (rtac cont_Isfst 1), |
467 (rtac cont_Isfst 1), |
468 (rtac strict_Isfst 1), |
468 (rtac strict_Isfst 1), |
469 (rtac (inst_sprod_pcpo RS subst) 1), |
469 (rtac (inst_sprod_pcpo RS subst) 1), |
470 (atac 1) |
470 (atac 1) |
471 ]); |
471 ]); |
472 |
472 |
473 qed_goalw "strict_sfst1" Sprod3.thy [sfst_def,spair_def] |
473 qed_goalw "strict_sfst1" Sprod3.thy [sfst_def,spair_def] |
474 "sfst`(|UU,y|) = UU" |
474 "sfst`(|UU,y|) = UU" |
475 (fn prems => |
475 (fn prems => |
476 [ |
476 [ |
477 (rtac (beta_cfun_sprod RS ssubst) 1), |
477 (rtac (beta_cfun_sprod RS ssubst) 1), |
478 (rtac (beta_cfun RS ssubst) 1), |
478 (rtac (beta_cfun RS ssubst) 1), |
479 (rtac cont_Isfst 1), |
479 (rtac cont_Isfst 1), |
480 (rtac strict_Isfst1 1) |
480 (rtac strict_Isfst1 1) |
481 ]); |
481 ]); |
482 |
482 |
483 qed_goalw "strict_sfst2" Sprod3.thy [sfst_def,spair_def] |
483 qed_goalw "strict_sfst2" Sprod3.thy [sfst_def,spair_def] |
484 "sfst`(|x,UU|) = UU" |
484 "sfst`(|x,UU|) = UU" |
485 (fn prems => |
485 (fn prems => |
486 [ |
486 [ |
487 (rtac (beta_cfun_sprod RS ssubst) 1), |
487 (rtac (beta_cfun_sprod RS ssubst) 1), |
488 (rtac (beta_cfun RS ssubst) 1), |
488 (rtac (beta_cfun RS ssubst) 1), |
489 (rtac cont_Isfst 1), |
489 (rtac cont_Isfst 1), |
490 (rtac strict_Isfst2 1) |
490 (rtac strict_Isfst2 1) |
491 ]); |
491 ]); |
492 |
492 |
493 qed_goalw "strict_ssnd" Sprod3.thy [ssnd_def] |
493 qed_goalw "strict_ssnd" Sprod3.thy [ssnd_def] |
494 "p=UU==>ssnd`p=UU" |
494 "p=UU==>ssnd`p=UU" |
495 (fn prems => |
495 (fn prems => |
496 [ |
496 [ |
497 (cut_facts_tac prems 1), |
497 (cut_facts_tac prems 1), |
498 (rtac (beta_cfun RS ssubst) 1), |
498 (rtac (beta_cfun RS ssubst) 1), |
499 (rtac cont_Issnd 1), |
499 (rtac cont_Issnd 1), |
500 (rtac strict_Issnd 1), |
500 (rtac strict_Issnd 1), |
501 (rtac (inst_sprod_pcpo RS subst) 1), |
501 (rtac (inst_sprod_pcpo RS subst) 1), |
502 (atac 1) |
502 (atac 1) |
503 ]); |
503 ]); |
504 |
504 |
505 qed_goalw "strict_ssnd1" Sprod3.thy [ssnd_def,spair_def] |
505 qed_goalw "strict_ssnd1" Sprod3.thy [ssnd_def,spair_def] |
506 "ssnd`(|UU,y|) = UU" |
506 "ssnd`(|UU,y|) = UU" |
507 (fn prems => |
507 (fn prems => |
508 [ |
508 [ |
509 (rtac (beta_cfun_sprod RS ssubst) 1), |
509 (rtac (beta_cfun_sprod RS ssubst) 1), |
510 (rtac (beta_cfun RS ssubst) 1), |
510 (rtac (beta_cfun RS ssubst) 1), |
511 (rtac cont_Issnd 1), |
511 (rtac cont_Issnd 1), |
512 (rtac strict_Issnd1 1) |
512 (rtac strict_Issnd1 1) |
513 ]); |
513 ]); |
514 |
514 |
515 qed_goalw "strict_ssnd2" Sprod3.thy [ssnd_def,spair_def] |
515 qed_goalw "strict_ssnd2" Sprod3.thy [ssnd_def,spair_def] |
516 "ssnd`(|x,UU|) = UU" |
516 "ssnd`(|x,UU|) = UU" |
517 (fn prems => |
517 (fn prems => |
518 [ |
518 [ |
519 (rtac (beta_cfun_sprod RS ssubst) 1), |
519 (rtac (beta_cfun_sprod RS ssubst) 1), |
520 (rtac (beta_cfun RS ssubst) 1), |
520 (rtac (beta_cfun RS ssubst) 1), |
521 (rtac cont_Issnd 1), |
521 (rtac cont_Issnd 1), |
522 (rtac strict_Issnd2 1) |
522 (rtac strict_Issnd2 1) |
523 ]); |
523 ]); |
524 |
524 |
525 qed_goalw "sfst2" Sprod3.thy [sfst_def,spair_def] |
525 qed_goalw "sfst2" Sprod3.thy [sfst_def,spair_def] |
526 "y~=UU ==>sfst`(|x,y|)=x" |
526 "y~=UU ==>sfst`(|x,y|)=x" |
527 (fn prems => |
527 (fn prems => |
528 [ |
528 [ |
529 (cut_facts_tac prems 1), |
529 (cut_facts_tac prems 1), |
530 (rtac (beta_cfun_sprod RS ssubst) 1), |
530 (rtac (beta_cfun_sprod RS ssubst) 1), |
531 (rtac (beta_cfun RS ssubst) 1), |
531 (rtac (beta_cfun RS ssubst) 1), |
532 (rtac cont_Isfst 1), |
532 (rtac cont_Isfst 1), |
533 (etac Isfst2 1) |
533 (etac Isfst2 1) |
534 ]); |
534 ]); |
535 |
535 |
536 qed_goalw "ssnd2" Sprod3.thy [ssnd_def,spair_def] |
536 qed_goalw "ssnd2" Sprod3.thy [ssnd_def,spair_def] |
537 "x~=UU ==>ssnd`(|x,y|)=y" |
537 "x~=UU ==>ssnd`(|x,y|)=y" |
538 (fn prems => |
538 (fn prems => |
539 [ |
539 [ |
540 (cut_facts_tac prems 1), |
540 (cut_facts_tac prems 1), |
541 (rtac (beta_cfun_sprod RS ssubst) 1), |
541 (rtac (beta_cfun_sprod RS ssubst) 1), |
542 (rtac (beta_cfun RS ssubst) 1), |
542 (rtac (beta_cfun RS ssubst) 1), |
543 (rtac cont_Issnd 1), |
543 (rtac cont_Issnd 1), |
544 (etac Issnd2 1) |
544 (etac Issnd2 1) |
545 ]); |
545 ]); |
546 |
546 |
547 |
547 |
548 qed_goalw "defined_sfstssnd" Sprod3.thy [sfst_def,ssnd_def,spair_def] |
548 qed_goalw "defined_sfstssnd" Sprod3.thy [sfst_def,ssnd_def,spair_def] |
549 "p~=UU ==> sfst`p ~=UU & ssnd`p ~=UU" |
549 "p~=UU ==> sfst`p ~=UU & ssnd`p ~=UU" |
550 (fn prems => |
550 (fn prems => |
551 [ |
551 [ |
552 (cut_facts_tac prems 1), |
552 (cut_facts_tac prems 1), |
553 (rtac (beta_cfun RS ssubst) 1), |
553 (rtac (beta_cfun RS ssubst) 1), |
554 (rtac cont_Issnd 1), |
554 (rtac cont_Issnd 1), |
555 (rtac (beta_cfun RS ssubst) 1), |
555 (rtac (beta_cfun RS ssubst) 1), |
556 (rtac cont_Isfst 1), |
556 (rtac cont_Isfst 1), |
557 (rtac defined_IsfstIssnd 1), |
557 (rtac defined_IsfstIssnd 1), |
558 (rtac (inst_sprod_pcpo RS subst) 1), |
558 (rtac (inst_sprod_pcpo RS subst) 1), |
559 (atac 1) |
559 (atac 1) |
560 ]); |
560 ]); |
561 |
561 |
562 |
562 |
563 qed_goalw "surjective_pairing_Sprod2" Sprod3.thy |
563 qed_goalw "surjective_pairing_Sprod2" Sprod3.thy |
564 [sfst_def,ssnd_def,spair_def] "(|sfst`p , ssnd`p|) = p" |
564 [sfst_def,ssnd_def,spair_def] "(|sfst`p , ssnd`p|) = p" |
565 (fn prems => |
565 (fn prems => |
566 [ |
566 [ |
567 (rtac (beta_cfun_sprod RS ssubst) 1), |
567 (rtac (beta_cfun_sprod RS ssubst) 1), |
568 (rtac (beta_cfun RS ssubst) 1), |
568 (rtac (beta_cfun RS ssubst) 1), |
569 (rtac cont_Issnd 1), |
569 (rtac cont_Issnd 1), |
570 (rtac (beta_cfun RS ssubst) 1), |
570 (rtac (beta_cfun RS ssubst) 1), |
571 (rtac cont_Isfst 1), |
571 (rtac cont_Isfst 1), |
572 (rtac (surjective_pairing_Sprod RS sym) 1) |
572 (rtac (surjective_pairing_Sprod RS sym) 1) |
573 ]); |
573 ]); |
574 |
574 |
575 |
575 |
576 qed_goalw "less_sprod5b" Sprod3.thy [sfst_def,ssnd_def,spair_def] |
576 qed_goalw "less_sprod5b" Sprod3.thy [sfst_def,ssnd_def,spair_def] |
577 "p1~=UU ==> (p1<<p2) = (sfst`p1<<sfst`p2 & ssnd`p1<<ssnd`p2)" |
577 "p1~=UU ==> (p1<<p2) = (sfst`p1<<sfst`p2 & ssnd`p1<<ssnd`p2)" |
578 (fn prems => |
578 (fn prems => |
579 [ |
579 [ |
580 (cut_facts_tac prems 1), |
580 (cut_facts_tac prems 1), |
581 (rtac (beta_cfun RS ssubst) 1), |
581 (rtac (beta_cfun RS ssubst) 1), |
582 (rtac cont_Issnd 1), |
582 (rtac cont_Issnd 1), |
583 (rtac (beta_cfun RS ssubst) 1), |
583 (rtac (beta_cfun RS ssubst) 1), |
584 (rtac cont_Issnd 1), |
584 (rtac cont_Issnd 1), |
585 (rtac (beta_cfun RS ssubst) 1), |
585 (rtac (beta_cfun RS ssubst) 1), |
586 (rtac cont_Isfst 1), |
586 (rtac cont_Isfst 1), |
587 (rtac (beta_cfun RS ssubst) 1), |
587 (rtac (beta_cfun RS ssubst) 1), |
588 (rtac cont_Isfst 1), |
588 (rtac cont_Isfst 1), |
589 (rtac less_sprod3b 1), |
589 (rtac less_sprod3b 1), |
590 (rtac (inst_sprod_pcpo RS subst) 1), |
590 (rtac (inst_sprod_pcpo RS subst) 1), |
591 (atac 1) |
591 (atac 1) |
592 ]); |
592 ]); |
593 |
593 |
594 |
594 |
595 qed_goalw "less_sprod5c" Sprod3.thy [sfst_def,ssnd_def,spair_def] |
595 qed_goalw "less_sprod5c" Sprod3.thy [sfst_def,ssnd_def,spair_def] |
596 "[|(|xa,ya|) << (|x,y|);xa~=UU;ya~=UU;x~=UU;y~=UU|] ==>xa<<x & ya << y" |
596 "[|(|xa,ya|) << (|x,y|);xa~=UU;ya~=UU;x~=UU;y~=UU|] ==>xa<<x & ya << y" |
597 (fn prems => |
597 (fn prems => |
598 [ |
598 [ |
599 (cut_facts_tac prems 1), |
599 (cut_facts_tac prems 1), |
600 (rtac less_sprod4c 1), |
600 (rtac less_sprod4c 1), |
601 (REPEAT (atac 2)), |
601 (REPEAT (atac 2)), |
602 (rtac (beta_cfun_sprod RS subst) 1), |
602 (rtac (beta_cfun_sprod RS subst) 1), |
603 (rtac (beta_cfun_sprod RS subst) 1), |
603 (rtac (beta_cfun_sprod RS subst) 1), |
604 (atac 1) |
604 (atac 1) |
605 ]); |
605 ]); |
606 |
606 |
607 qed_goalw "lub_sprod2" Sprod3.thy [sfst_def,ssnd_def,spair_def] |
607 qed_goalw "lub_sprod2" Sprod3.thy [sfst_def,ssnd_def,spair_def] |
608 "[|is_chain(S)|] ==> range(S) <<| \ |
608 "[|is_chain(S)|] ==> range(S) <<| \ |
609 \ (| lub(range(%i.sfst`(S i))), lub(range(%i.ssnd`(S i))) |)" |
609 \ (| lub(range(%i.sfst`(S i))), lub(range(%i.ssnd`(S i))) |)" |
610 (fn prems => |
610 (fn prems => |
611 [ |
611 [ |
612 (cut_facts_tac prems 1), |
612 (cut_facts_tac prems 1), |
613 (rtac (beta_cfun_sprod RS ssubst) 1), |
613 (rtac (beta_cfun_sprod RS ssubst) 1), |
614 (rtac (beta_cfun RS ext RS ssubst) 1), |
614 (rtac (beta_cfun RS ext RS ssubst) 1), |
615 (rtac cont_Issnd 1), |
615 (rtac cont_Issnd 1), |
616 (rtac (beta_cfun RS ext RS ssubst) 1), |
616 (rtac (beta_cfun RS ext RS ssubst) 1), |
617 (rtac cont_Isfst 1), |
617 (rtac cont_Isfst 1), |
618 (rtac lub_sprod 1), |
618 (rtac lub_sprod 1), |
619 (resolve_tac prems 1) |
619 (resolve_tac prems 1) |
620 ]); |
620 ]); |
621 |
621 |
622 |
622 |
623 val thelub_sprod2 = (lub_sprod2 RS thelubI); |
623 val thelub_sprod2 = (lub_sprod2 RS thelubI); |
624 (* |
624 (* |
625 "is_chain ?S1 ==> |
625 "is_chain ?S1 ==> |
626 lub (range ?S1) = |
626 lub (range ?S1) = |
627 (|lub (range (%i. sfst`(?S1 i))), lub (range (%i. ssnd`(?S1 i)))|)" : thm |
627 (|lub (range (%i. sfst`(?S1 i))), lub (range (%i. ssnd`(?S1 i)))|)" : thm |
628 *) |
628 *) |
629 |
629 |
630 qed_goalw "ssplit1" Sprod3.thy [ssplit_def] |
630 qed_goalw "ssplit1" Sprod3.thy [ssplit_def] |
631 "ssplit`f`UU=UU" |
631 "ssplit`f`UU=UU" |
632 (fn prems => |
632 (fn prems => |
633 [ |
633 [ |
634 (rtac (beta_cfun RS ssubst) 1), |
634 (rtac (beta_cfun RS ssubst) 1), |
635 (cont_tacR 1), |
635 (cont_tacR 1), |
636 (rtac (strictify1 RS ssubst) 1), |
636 (rtac (strictify1 RS ssubst) 1), |
637 (rtac refl 1) |
637 (rtac refl 1) |
638 ]); |
638 ]); |
639 |
639 |
640 qed_goalw "ssplit2" Sprod3.thy [ssplit_def] |
640 qed_goalw "ssplit2" Sprod3.thy [ssplit_def] |
641 "[|x~=UU;y~=UU|] ==> ssplit`f`(|x,y|)= f`x`y" |
641 "[|x~=UU;y~=UU|] ==> ssplit`f`(|x,y|)= f`x`y" |
642 (fn prems => |
642 (fn prems => |
643 [ |
643 [ |
644 (rtac (beta_cfun RS ssubst) 1), |
644 (rtac (beta_cfun RS ssubst) 1), |
645 (cont_tacR 1), |
645 (cont_tacR 1), |
646 (rtac (strictify2 RS ssubst) 1), |
646 (rtac (strictify2 RS ssubst) 1), |
647 (rtac defined_spair 1), |
647 (rtac defined_spair 1), |
648 (resolve_tac prems 1), |
648 (resolve_tac prems 1), |
649 (resolve_tac prems 1), |
649 (resolve_tac prems 1), |
650 (rtac (beta_cfun RS ssubst) 1), |
650 (rtac (beta_cfun RS ssubst) 1), |
651 (cont_tacR 1), |
651 (cont_tacR 1), |
652 (rtac (sfst2 RS ssubst) 1), |
652 (rtac (sfst2 RS ssubst) 1), |
653 (resolve_tac prems 1), |
653 (resolve_tac prems 1), |
654 (rtac (ssnd2 RS ssubst) 1), |
654 (rtac (ssnd2 RS ssubst) 1), |
655 (resolve_tac prems 1), |
655 (resolve_tac prems 1), |
656 (rtac refl 1) |
656 (rtac refl 1) |
657 ]); |
657 ]); |
658 |
658 |
659 |
659 |
660 qed_goalw "ssplit3" Sprod3.thy [ssplit_def] |
660 qed_goalw "ssplit3" Sprod3.thy [ssplit_def] |
661 "ssplit`spair`z=z" |
661 "ssplit`spair`z=z" |
662 (fn prems => |
662 (fn prems => |
663 [ |
663 [ |
664 (rtac (beta_cfun RS ssubst) 1), |
664 (rtac (beta_cfun RS ssubst) 1), |
665 (cont_tacR 1), |
665 (cont_tacR 1), |
666 (res_inst_tac [("Q","z=UU")] classical2 1), |
666 (res_inst_tac [("Q","z=UU")] classical2 1), |
667 (hyp_subst_tac 1), |
667 (hyp_subst_tac 1), |
668 (rtac strictify1 1), |
668 (rtac strictify1 1), |
669 (rtac trans 1), |
669 (rtac trans 1), |
670 (rtac strictify2 1), |
670 (rtac strictify2 1), |
671 (atac 1), |
671 (atac 1), |
672 (rtac (beta_cfun RS ssubst) 1), |
672 (rtac (beta_cfun RS ssubst) 1), |
673 (cont_tacR 1), |
673 (cont_tacR 1), |
674 (rtac surjective_pairing_Sprod2 1) |
674 (rtac surjective_pairing_Sprod2 1) |
675 ]); |
675 ]); |
676 |
676 |
677 |
677 |
678 (* ------------------------------------------------------------------------ *) |
678 (* ------------------------------------------------------------------------ *) |
679 (* install simplifier for Sprod *) |
679 (* install simplifier for Sprod *) |
680 (* ------------------------------------------------------------------------ *) |
680 (* ------------------------------------------------------------------------ *) |
681 |
681 |
682 val Sprod_rews = [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2, |
682 val Sprod_rews = [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2, |
683 strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair, |
683 strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair, |
684 ssplit1,ssplit2]; |
684 ssplit1,ssplit2]; |
685 |
685 |
686 Addsimps [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2, |
686 Addsimps [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2, |
687 strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair, |
687 strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair, |
688 ssplit1,ssplit2]; |
688 ssplit1,ssplit2]; |