8 |
8 |
9 (* ------------------------------------------------------------------------ *) |
9 (* ------------------------------------------------------------------------ *) |
10 (* A non-emptyness result for Sssum *) |
10 (* A non-emptyness result for Sssum *) |
11 (* ------------------------------------------------------------------------ *) |
11 (* ------------------------------------------------------------------------ *) |
12 |
12 |
13 qed_goalw "SsumIl" Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum" |
13 val prems = goalw Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum"; |
14 (fn prems => |
14 by (rtac CollectI 1); |
15 [ |
15 by (rtac disjI1 1); |
16 (rtac CollectI 1), |
16 by (rtac exI 1); |
17 (rtac disjI1 1), |
17 by (rtac refl 1); |
18 (rtac exI 1), |
18 qed "SsumIl"; |
19 (rtac refl 1) |
19 |
20 ]); |
20 val prems = goalw Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum"; |
21 |
21 by (rtac CollectI 1); |
22 qed_goalw "SsumIr" Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum" |
22 by (rtac disjI2 1); |
23 (fn prems => |
23 by (rtac exI 1); |
24 [ |
24 by (rtac refl 1); |
25 (rtac CollectI 1), |
25 qed "SsumIr"; |
26 (rtac disjI2 1), |
|
27 (rtac exI 1), |
|
28 (rtac refl 1) |
|
29 ]); |
|
30 |
26 |
31 Goal "inj_on Abs_Ssum Ssum"; |
27 Goal "inj_on Abs_Ssum Ssum"; |
32 by (rtac inj_on_inverseI 1); |
28 by (rtac inj_on_inverseI 1); |
33 by (etac Abs_Ssum_inverse 1); |
29 by (etac Abs_Ssum_inverse 1); |
34 qed "inj_on_Abs_Ssum"; |
30 qed "inj_on_Abs_Ssum"; |
35 |
31 |
36 (* ------------------------------------------------------------------------ *) |
32 (* ------------------------------------------------------------------------ *) |
37 (* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr *) |
33 (* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr *) |
38 (* ------------------------------------------------------------------------ *) |
34 (* ------------------------------------------------------------------------ *) |
39 |
35 |
40 qed_goalw "strict_SinlSinr_Rep" Ssum0.thy [Sinr_Rep_def,Sinl_Rep_def] |
36 val prems = goalw Ssum0.thy [Sinr_Rep_def,Sinl_Rep_def] |
41 "Sinl_Rep(UU) = Sinr_Rep(UU)" |
37 "Sinl_Rep(UU) = Sinr_Rep(UU)"; |
42 (fn prems => |
38 by (rtac ext 1); |
43 [ |
39 by (rtac ext 1); |
44 (rtac ext 1), |
40 by (rtac ext 1); |
45 (rtac ext 1), |
41 by (fast_tac HOL_cs 1); |
46 (rtac ext 1), |
42 qed "strict_SinlSinr_Rep"; |
47 (fast_tac HOL_cs 1) |
43 |
48 ]); |
44 val prems = goalw Ssum0.thy [Isinl_def,Isinr_def] |
49 |
45 "Isinl(UU) = Isinr(UU)"; |
50 qed_goalw "strict_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def] |
46 by (rtac (strict_SinlSinr_Rep RS arg_cong) 1); |
51 "Isinl(UU) = Isinr(UU)" |
47 qed "strict_IsinlIsinr"; |
52 (fn prems => |
|
53 [ |
|
54 (rtac (strict_SinlSinr_Rep RS arg_cong) 1) |
|
55 ]); |
|
56 |
48 |
57 |
49 |
58 (* ------------------------------------------------------------------------ *) |
50 (* ------------------------------------------------------------------------ *) |
59 (* distinctness of Sinl_Rep, Sinr_Rep and Isinl, Isinr *) |
51 (* distinctness of Sinl_Rep, Sinr_Rep and Isinl, Isinr *) |
60 (* ------------------------------------------------------------------------ *) |
52 (* ------------------------------------------------------------------------ *) |
61 |
53 |
62 qed_goalw "noteq_SinlSinr_Rep" Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def] |
54 val prems = goalw Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def] |
63 "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU" |
55 "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"; |
64 (fn prems => |
56 by (rtac conjI 1); |
65 [ |
57 by (case_tac "a=UU" 1); |
66 (rtac conjI 1), |
58 by (atac 1); |
67 (case_tac "a=UU" 1), |
59 by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 RS mp RS conjunct1 RS sym) 1); |
68 (atac 1), |
60 by (fast_tac HOL_cs 1); |
69 (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 |
61 by (atac 1); |
70 RS mp RS conjunct1 RS sym) 1), |
62 by (case_tac "b=UU" 1); |
71 (fast_tac HOL_cs 1), |
63 by (atac 1); |
72 (atac 1), |
64 by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1 RS mp RS conjunct1 RS sym) 1); |
73 (case_tac "b=UU" 1), |
65 by (fast_tac HOL_cs 1); |
74 (atac 1), |
66 by (atac 1); |
75 (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1 |
67 qed "noteq_SinlSinr_Rep"; |
76 RS mp RS conjunct1 RS sym) 1), |
68 |
77 (fast_tac HOL_cs 1), |
69 |
78 (atac 1) |
70 val prems = goalw Ssum0.thy [Isinl_def,Isinr_def] |
79 ]); |
71 "Isinl(a)=Isinr(b) ==> a=UU & b=UU"; |
80 |
72 by (cut_facts_tac prems 1); |
81 |
73 by (rtac noteq_SinlSinr_Rep 1); |
82 qed_goalw "noteq_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def] |
74 by (etac (inj_on_Abs_Ssum RS inj_onD) 1); |
83 "Isinl(a)=Isinr(b) ==> a=UU & b=UU" |
75 by (rtac SsumIl 1); |
84 (fn prems => |
76 by (rtac SsumIr 1); |
85 [ |
77 qed "noteq_IsinlIsinr"; |
86 (cut_facts_tac prems 1), |
|
87 (rtac noteq_SinlSinr_Rep 1), |
|
88 (etac (inj_on_Abs_Ssum RS inj_onD) 1), |
|
89 (rtac SsumIl 1), |
|
90 (rtac SsumIr 1) |
|
91 ]); |
|
92 |
78 |
93 |
79 |
94 |
80 |
95 (* ------------------------------------------------------------------------ *) |
81 (* ------------------------------------------------------------------------ *) |
96 (* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr *) |
82 (* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr *) |
97 (* ------------------------------------------------------------------------ *) |
83 (* ------------------------------------------------------------------------ *) |
98 |
84 |
99 qed_goalw "inject_Sinl_Rep1" Ssum0.thy [Sinl_Rep_def] |
85 val prems = goalw Ssum0.thy [Sinl_Rep_def] |
100 "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU" |
86 "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"; |
101 (fn prems => |
87 by (case_tac "a=UU" 1); |
102 [ |
88 by (atac 1); |
103 (case_tac "a=UU" 1), |
89 by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 RS mp RS conjunct1 RS sym) 1); |
104 (atac 1), |
90 by (fast_tac HOL_cs 1); |
105 (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong |
91 by (atac 1); |
106 RS iffD2 RS mp RS conjunct1 RS sym) 1), |
92 qed "inject_Sinl_Rep1"; |
107 (fast_tac HOL_cs 1), |
93 |
108 (atac 1) |
94 val prems = goalw Ssum0.thy [Sinr_Rep_def] |
109 ]); |
95 "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"; |
110 |
96 by (case_tac "b=UU" 1); |
111 qed_goalw "inject_Sinr_Rep1" Ssum0.thy [Sinr_Rep_def] |
97 by (atac 1); |
112 "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU" |
98 by (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 RS mp RS conjunct1 RS sym) 1); |
113 (fn prems => |
99 by (fast_tac HOL_cs 1); |
114 [ |
100 by (atac 1); |
115 (case_tac "b=UU" 1), |
101 qed "inject_Sinr_Rep1"; |
116 (atac 1), |
102 |
117 (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong |
103 val prems = goalw Ssum0.thy [Sinl_Rep_def] |
118 RS iffD2 RS mp RS conjunct1 RS sym) 1), |
104 "[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2"; |
119 (fast_tac HOL_cs 1), |
105 by (rtac ((nth_elem (2,prems)) RS fun_cong RS fun_cong RS fun_cong RS iffD1 RS mp RS conjunct1) 1); |
120 (atac 1) |
106 by (fast_tac HOL_cs 1); |
121 ]); |
107 by (resolve_tac prems 1); |
122 |
108 qed "inject_Sinl_Rep2"; |
123 qed_goalw "inject_Sinl_Rep2" Ssum0.thy [Sinl_Rep_def] |
109 |
124 "[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2" |
110 val prems = goalw Ssum0.thy [Sinr_Rep_def] |
125 (fn prems => |
111 "[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2"; |
126 [ |
112 by (rtac ((nth_elem (2,prems)) RS fun_cong RS fun_cong RS fun_cong RS iffD1 RS mp RS conjunct1) 1); |
127 (rtac ((nth_elem (2,prems)) RS fun_cong RS fun_cong RS fun_cong |
113 by (fast_tac HOL_cs 1); |
128 RS iffD1 RS mp RS conjunct1) 1), |
114 by (resolve_tac prems 1); |
129 (fast_tac HOL_cs 1), |
115 qed "inject_Sinr_Rep2"; |
130 (resolve_tac prems 1) |
|
131 ]); |
|
132 |
|
133 qed_goalw "inject_Sinr_Rep2" Ssum0.thy [Sinr_Rep_def] |
|
134 "[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2" |
|
135 (fn prems => |
|
136 [ |
|
137 (rtac ((nth_elem (2,prems)) RS fun_cong RS fun_cong RS fun_cong |
|
138 RS iffD1 RS mp RS conjunct1) 1), |
|
139 (fast_tac HOL_cs 1), |
|
140 (resolve_tac prems 1) |
|
141 ]); |
|
142 |
116 |
143 Goal "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2"; |
117 Goal "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2"; |
144 by (case_tac "a1=UU" 1); |
118 by (case_tac "a1=UU" 1); |
145 by (hyp_subst_tac 1); |
119 by (hyp_subst_tac 1); |
146 by (rtac (inject_Sinl_Rep1 RS sym) 1); |
120 by (rtac (inject_Sinl_Rep1 RS sym) 1); |
164 by (etac inject_Sinr_Rep2 1); |
138 by (etac inject_Sinr_Rep2 1); |
165 by (atac 1); |
139 by (atac 1); |
166 by (atac 1); |
140 by (atac 1); |
167 qed "inject_Sinr_Rep"; |
141 qed "inject_Sinr_Rep"; |
168 |
142 |
169 qed_goalw "inject_Isinl" Ssum0.thy [Isinl_def] |
143 val prems = goalw Ssum0.thy [Isinl_def] |
170 "Isinl(a1)=Isinl(a2)==> a1=a2" |
144 "Isinl(a1)=Isinl(a2)==> a1=a2"; |
171 (fn prems => |
145 by (cut_facts_tac prems 1); |
172 [ |
146 by (rtac inject_Sinl_Rep 1); |
173 (cut_facts_tac prems 1), |
147 by (etac (inj_on_Abs_Ssum RS inj_onD) 1); |
174 (rtac inject_Sinl_Rep 1), |
148 by (rtac SsumIl 1); |
175 (etac (inj_on_Abs_Ssum RS inj_onD) 1), |
149 by (rtac SsumIl 1); |
176 (rtac SsumIl 1), |
150 qed "inject_Isinl"; |
177 (rtac SsumIl 1) |
151 |
178 ]); |
152 val prems = goalw Ssum0.thy [Isinr_def] |
179 |
153 "Isinr(b1)=Isinr(b2) ==> b1=b2"; |
180 qed_goalw "inject_Isinr" Ssum0.thy [Isinr_def] |
154 by (cut_facts_tac prems 1); |
181 "Isinr(b1)=Isinr(b2) ==> b1=b2" |
155 by (rtac inject_Sinr_Rep 1); |
182 (fn prems => |
156 by (etac (inj_on_Abs_Ssum RS inj_onD) 1); |
183 [ |
157 by (rtac SsumIr 1); |
184 (cut_facts_tac prems 1), |
158 by (rtac SsumIr 1); |
185 (rtac inject_Sinr_Rep 1), |
159 qed "inject_Isinr"; |
186 (etac (inj_on_Abs_Ssum RS inj_onD) 1), |
|
187 (rtac SsumIr 1), |
|
188 (rtac SsumIr 1) |
|
189 ]); |
|
190 |
160 |
191 Goal "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"; |
161 Goal "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"; |
192 by (rtac contrapos 1); |
162 by (rtac contrapos 1); |
193 by (etac inject_Isinl 2); |
163 by (etac inject_Isinl 2); |
194 by (atac 1); |
164 by (atac 1); |
203 (* ------------------------------------------------------------------------ *) |
173 (* ------------------------------------------------------------------------ *) |
204 (* Exhaustion of the strict sum ++ *) |
174 (* Exhaustion of the strict sum ++ *) |
205 (* choice of the bottom representation is arbitrary *) |
175 (* choice of the bottom representation is arbitrary *) |
206 (* ------------------------------------------------------------------------ *) |
176 (* ------------------------------------------------------------------------ *) |
207 |
177 |
208 qed_goalw "Exh_Ssum" Ssum0.thy [Isinl_def,Isinr_def] |
178 val prems = goalw Ssum0.thy [Isinl_def,Isinr_def] |
209 "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)" |
179 "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)"; |
210 (fn prems => |
180 by (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1); |
211 [ |
181 by (etac disjE 1); |
212 (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1), |
182 by (etac exE 1); |
213 (etac disjE 1), |
183 by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1); |
214 (etac exE 1), |
184 by (etac disjI1 1); |
215 (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1), |
185 by (rtac disjI2 1); |
216 (etac disjI1 1), |
186 by (rtac disjI1 1); |
217 (rtac disjI2 1), |
187 by (rtac exI 1); |
218 (rtac disjI1 1), |
188 by (rtac conjI 1); |
219 (rtac exI 1), |
189 by (rtac (Rep_Ssum_inverse RS sym RS trans) 1); |
220 (rtac conjI 1), |
190 by (etac arg_cong 1); |
221 (rtac (Rep_Ssum_inverse RS sym RS trans) 1), |
191 by (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos 1); |
222 (etac arg_cong 1), |
192 by (etac arg_cong 2); |
223 (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos 1), |
193 by (etac contrapos 1); |
224 (etac arg_cong 2), |
194 by (rtac (Rep_Ssum_inverse RS sym RS trans) 1); |
225 (etac contrapos 1), |
195 by (rtac trans 1); |
226 (rtac (Rep_Ssum_inverse RS sym RS trans) 1), |
196 by (etac arg_cong 1); |
227 (rtac trans 1), |
197 by (etac arg_cong 1); |
228 (etac arg_cong 1), |
198 by (etac exE 1); |
229 (etac arg_cong 1), |
199 by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1); |
230 (etac exE 1), |
200 by (etac disjI1 1); |
231 (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1), |
201 by (rtac disjI2 1); |
232 (etac disjI1 1), |
202 by (rtac disjI2 1); |
233 (rtac disjI2 1), |
203 by (rtac exI 1); |
234 (rtac disjI2 1), |
204 by (rtac conjI 1); |
235 (rtac exI 1), |
205 by (rtac (Rep_Ssum_inverse RS sym RS trans) 1); |
236 (rtac conjI 1), |
206 by (etac arg_cong 1); |
237 (rtac (Rep_Ssum_inverse RS sym RS trans) 1), |
207 by (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos 1); |
238 (etac arg_cong 1), |
208 by (hyp_subst_tac 2); |
239 (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos 1), |
209 by (rtac (strict_SinlSinr_Rep RS sym) 2); |
240 (hyp_subst_tac 2), |
210 by (etac contrapos 1); |
241 (rtac (strict_SinlSinr_Rep RS sym) 2), |
211 by (rtac (Rep_Ssum_inverse RS sym RS trans) 1); |
242 (etac contrapos 1), |
212 by (rtac trans 1); |
243 (rtac (Rep_Ssum_inverse RS sym RS trans) 1), |
213 by (etac arg_cong 1); |
244 (rtac trans 1), |
214 by (etac arg_cong 1); |
245 (etac arg_cong 1), |
215 qed "Exh_Ssum"; |
246 (etac arg_cong 1) |
|
247 ]); |
|
248 |
216 |
249 (* ------------------------------------------------------------------------ *) |
217 (* ------------------------------------------------------------------------ *) |
250 (* elimination rules for the strict sum ++ *) |
218 (* elimination rules for the strict sum ++ *) |
251 (* ------------------------------------------------------------------------ *) |
219 (* ------------------------------------------------------------------------ *) |
252 |
220 |
280 |
248 |
281 (* ------------------------------------------------------------------------ *) |
249 (* ------------------------------------------------------------------------ *) |
282 (* rewrites for Iwhen *) |
250 (* rewrites for Iwhen *) |
283 (* ------------------------------------------------------------------------ *) |
251 (* ------------------------------------------------------------------------ *) |
284 |
252 |
285 qed_goalw "Iwhen1" Ssum0.thy [Iwhen_def] |
253 val prems = goalw Ssum0.thy [Iwhen_def] |
286 "Iwhen f g (Isinl UU) = UU" |
254 "Iwhen f g (Isinl UU) = UU"; |
287 (fn prems => |
255 by (rtac select_equality 1); |
288 [ |
256 by (rtac conjI 1); |
289 (rtac select_equality 1), |
257 by (fast_tac HOL_cs 1); |
290 (rtac conjI 1), |
258 by (rtac conjI 1); |
291 (fast_tac HOL_cs 1), |
259 by (strip_tac 1); |
292 (rtac conjI 1), |
260 by (res_inst_tac [("P","a=UU")] notE 1); |
293 (strip_tac 1), |
261 by (fast_tac HOL_cs 1); |
294 (res_inst_tac [("P","a=UU")] notE 1), |
262 by (rtac inject_Isinl 1); |
295 (fast_tac HOL_cs 1), |
263 by (rtac sym 1); |
296 (rtac inject_Isinl 1), |
264 by (fast_tac HOL_cs 1); |
297 (rtac sym 1), |
265 by (strip_tac 1); |
298 (fast_tac HOL_cs 1), |
266 by (res_inst_tac [("P","b=UU")] notE 1); |
299 (strip_tac 1), |
267 by (fast_tac HOL_cs 1); |
300 (res_inst_tac [("P","b=UU")] notE 1), |
268 by (rtac inject_Isinr 1); |
301 (fast_tac HOL_cs 1), |
269 by (rtac sym 1); |
302 (rtac inject_Isinr 1), |
270 by (rtac (strict_IsinlIsinr RS subst) 1); |
303 (rtac sym 1), |
271 by (fast_tac HOL_cs 1); |
304 (rtac (strict_IsinlIsinr RS subst) 1), |
272 by (fast_tac HOL_cs 1); |
305 (fast_tac HOL_cs 1), |
273 qed "Iwhen1"; |
306 (fast_tac HOL_cs 1) |
274 |
307 ]); |
275 |
308 |
276 val prems = goalw Ssum0.thy [Iwhen_def] |
309 |
277 "x~=UU ==> Iwhen f g (Isinl x) = f`x"; |
310 qed_goalw "Iwhen2" Ssum0.thy [Iwhen_def] |
278 by (cut_facts_tac prems 1); |
311 "x~=UU ==> Iwhen f g (Isinl x) = f`x" |
279 by (rtac select_equality 1); |
312 (fn prems => |
280 by (fast_tac HOL_cs 2); |
313 [ |
281 by (rtac conjI 1); |
314 (cut_facts_tac prems 1), |
282 by (strip_tac 1); |
315 (rtac select_equality 1), |
283 by (res_inst_tac [("P","x=UU")] notE 1); |
316 (fast_tac HOL_cs 2), |
284 by (atac 1); |
317 (rtac conjI 1), |
285 by (rtac inject_Isinl 1); |
318 (strip_tac 1), |
286 by (atac 1); |
319 (res_inst_tac [("P","x=UU")] notE 1), |
287 by (rtac conjI 1); |
320 (atac 1), |
288 by (strip_tac 1); |
321 (rtac inject_Isinl 1), |
289 by (rtac cfun_arg_cong 1); |
322 (atac 1), |
290 by (rtac inject_Isinl 1); |
323 (rtac conjI 1), |
291 by (fast_tac HOL_cs 1); |
324 (strip_tac 1), |
292 by (strip_tac 1); |
325 (rtac cfun_arg_cong 1), |
293 by (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1); |
326 (rtac inject_Isinl 1), |
294 by (fast_tac HOL_cs 2); |
327 (fast_tac HOL_cs 1), |
295 by (rtac contrapos 1); |
328 (strip_tac 1), |
296 by (etac noteq_IsinlIsinr 2); |
329 (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1), |
297 by (fast_tac HOL_cs 1); |
330 (fast_tac HOL_cs 2), |
298 qed "Iwhen2"; |
331 (rtac contrapos 1), |
299 |
332 (etac noteq_IsinlIsinr 2), |
300 val prems = goalw Ssum0.thy [Iwhen_def] |
333 (fast_tac HOL_cs 1) |
301 "y~=UU ==> Iwhen f g (Isinr y) = g`y"; |
334 ]); |
302 by (cut_facts_tac prems 1); |
335 |
303 by (rtac select_equality 1); |
336 qed_goalw "Iwhen3" Ssum0.thy [Iwhen_def] |
304 by (fast_tac HOL_cs 2); |
337 "y~=UU ==> Iwhen f g (Isinr y) = g`y" |
305 by (rtac conjI 1); |
338 (fn prems => |
306 by (strip_tac 1); |
339 [ |
307 by (res_inst_tac [("P","y=UU")] notE 1); |
340 (cut_facts_tac prems 1), |
308 by (atac 1); |
341 (rtac select_equality 1), |
309 by (rtac inject_Isinr 1); |
342 (fast_tac HOL_cs 2), |
310 by (rtac (strict_IsinlIsinr RS subst) 1); |
343 (rtac conjI 1), |
311 by (atac 1); |
344 (strip_tac 1), |
312 by (rtac conjI 1); |
345 (res_inst_tac [("P","y=UU")] notE 1), |
313 by (strip_tac 1); |
346 (atac 1), |
314 by (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1); |
347 (rtac inject_Isinr 1), |
315 by (fast_tac HOL_cs 2); |
348 (rtac (strict_IsinlIsinr RS subst) 1), |
316 by (rtac contrapos 1); |
349 (atac 1), |
317 by (etac (sym RS noteq_IsinlIsinr) 2); |
350 (rtac conjI 1), |
318 by (fast_tac HOL_cs 1); |
351 (strip_tac 1), |
319 by (strip_tac 1); |
352 (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1), |
320 by (rtac cfun_arg_cong 1); |
353 (fast_tac HOL_cs 2), |
321 by (rtac inject_Isinr 1); |
354 (rtac contrapos 1), |
322 by (fast_tac HOL_cs 1); |
355 (etac (sym RS noteq_IsinlIsinr) 2), |
323 qed "Iwhen3"; |
356 (fast_tac HOL_cs 1), |
|
357 (strip_tac 1), |
|
358 (rtac cfun_arg_cong 1), |
|
359 (rtac inject_Isinr 1), |
|
360 (fast_tac HOL_cs 1) |
|
361 ]); |
|
362 |
324 |
363 (* ------------------------------------------------------------------------ *) |
325 (* ------------------------------------------------------------------------ *) |
364 (* instantiate the simplifier *) |
326 (* instantiate the simplifier *) |
365 (* ------------------------------------------------------------------------ *) |
327 (* ------------------------------------------------------------------------ *) |
366 |
328 |