|
1 (* Title: HOLCF/ssum1.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for theory ssum1.thy |
|
7 *) |
|
8 |
|
9 open Ssum1; |
|
10 |
|
11 local |
|
12 |
|
13 fun eq_left s1 s2 = |
|
14 ( |
|
15 (res_inst_tac [("s",s1),("t",s2)] (inject_Isinl RS subst) 1) |
|
16 THEN (rtac trans 1) |
|
17 THEN (atac 2) |
|
18 THEN (etac sym 1)); |
|
19 |
|
20 fun eq_right s1 s2 = |
|
21 ( |
|
22 (res_inst_tac [("s",s1),("t",s2)] (inject_Isinr RS subst) 1) |
|
23 THEN (rtac trans 1) |
|
24 THEN (atac 2) |
|
25 THEN (etac sym 1)); |
|
26 |
|
27 fun UU_left s1 = |
|
28 ( |
|
29 (res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct1 RS ssubst)1) |
|
30 THEN (rtac trans 1) |
|
31 THEN (atac 2) |
|
32 THEN (etac sym 1)); |
|
33 |
|
34 fun UU_right s1 = |
|
35 ( |
|
36 (res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct2 RS ssubst)1) |
|
37 THEN (rtac trans 1) |
|
38 THEN (atac 2) |
|
39 THEN (etac sym 1)) |
|
40 |
|
41 in |
|
42 |
|
43 val less_ssum1a = prove_goalw Ssum1.thy [less_ssum_def] |
|
44 "[|s1=Isinl(x); s2=Isinl(y)|] ==> less_ssum(s1,s2) = (x << y)" |
|
45 (fn prems => |
|
46 [ |
|
47 (cut_facts_tac prems 1), |
|
48 (rtac select_equality 1), |
|
49 (dtac conjunct1 2), |
|
50 (dtac spec 2), |
|
51 (dtac spec 2), |
|
52 (etac mp 2), |
|
53 (fast_tac HOL_cs 2), |
|
54 (rtac conjI 1), |
|
55 (strip_tac 1), |
|
56 (etac conjE 1), |
|
57 (eq_left "x" "u"), |
|
58 (eq_left "y" "xa"), |
|
59 (rtac refl 1), |
|
60 (rtac conjI 1), |
|
61 (strip_tac 1), |
|
62 (etac conjE 1), |
|
63 (UU_left "x"), |
|
64 (UU_right "v"), |
|
65 (simp_tac Cfun_ss 1), |
|
66 (rtac conjI 1), |
|
67 (strip_tac 1), |
|
68 (etac conjE 1), |
|
69 (eq_left "x" "u"), |
|
70 (UU_left "y"), |
|
71 (rtac iffI 1), |
|
72 (etac UU_I 1), |
|
73 (res_inst_tac [("s","x"),("t","UU")] subst 1), |
|
74 (atac 1), |
|
75 (rtac refl_less 1), |
|
76 (strip_tac 1), |
|
77 (etac conjE 1), |
|
78 (UU_left "x"), |
|
79 (UU_right "v"), |
|
80 (simp_tac Cfun_ss 1) |
|
81 ]); |
|
82 |
|
83 |
|
84 val less_ssum1b = prove_goalw Ssum1.thy [less_ssum_def] |
|
85 "[|s1=Isinr(x); s2=Isinr(y)|] ==> less_ssum(s1,s2) = (x << y)" |
|
86 (fn prems => |
|
87 [ |
|
88 (cut_facts_tac prems 1), |
|
89 (rtac select_equality 1), |
|
90 (dtac conjunct2 2), |
|
91 (dtac conjunct1 2), |
|
92 (dtac spec 2), |
|
93 (dtac spec 2), |
|
94 (etac mp 2), |
|
95 (fast_tac HOL_cs 2), |
|
96 (rtac conjI 1), |
|
97 (strip_tac 1), |
|
98 (etac conjE 1), |
|
99 (UU_right "x"), |
|
100 (UU_left "u"), |
|
101 (simp_tac Cfun_ss 1), |
|
102 (rtac conjI 1), |
|
103 (strip_tac 1), |
|
104 (etac conjE 1), |
|
105 (eq_right "x" "v"), |
|
106 (eq_right "y" "ya"), |
|
107 (rtac refl 1), |
|
108 (rtac conjI 1), |
|
109 (strip_tac 1), |
|
110 (etac conjE 1), |
|
111 (UU_right "x"), |
|
112 (UU_left "u"), |
|
113 (simp_tac Cfun_ss 1), |
|
114 (strip_tac 1), |
|
115 (etac conjE 1), |
|
116 (eq_right "x" "v"), |
|
117 (UU_right "y"), |
|
118 (rtac iffI 1), |
|
119 (etac UU_I 1), |
|
120 (res_inst_tac [("s","UU"),("t","x")] subst 1), |
|
121 (etac sym 1), |
|
122 (rtac refl_less 1) |
|
123 ]); |
|
124 |
|
125 |
|
126 val less_ssum1c = prove_goalw Ssum1.thy [less_ssum_def] |
|
127 "[|s1=Isinl(x); s2=Isinr(y)|] ==> less_ssum(s1,s2) = (x = UU)" |
|
128 (fn prems => |
|
129 [ |
|
130 (cut_facts_tac prems 1), |
|
131 (rtac select_equality 1), |
|
132 (rtac conjI 1), |
|
133 (strip_tac 1), |
|
134 (etac conjE 1), |
|
135 (eq_left "x" "u"), |
|
136 (UU_left "xa"), |
|
137 (rtac iffI 1), |
|
138 (res_inst_tac [("s","x"),("t","UU")] subst 1), |
|
139 (atac 1), |
|
140 (rtac refl_less 1), |
|
141 (etac UU_I 1), |
|
142 (rtac conjI 1), |
|
143 (strip_tac 1), |
|
144 (etac conjE 1), |
|
145 (UU_left "x"), |
|
146 (UU_right "v"), |
|
147 (simp_tac Cfun_ss 1), |
|
148 (rtac conjI 1), |
|
149 (strip_tac 1), |
|
150 (etac conjE 1), |
|
151 (eq_left "x" "u"), |
|
152 (rtac refl 1), |
|
153 (strip_tac 1), |
|
154 (etac conjE 1), |
|
155 (UU_left "x"), |
|
156 (UU_right "v"), |
|
157 (simp_tac Cfun_ss 1), |
|
158 (dtac conjunct2 1), |
|
159 (dtac conjunct2 1), |
|
160 (dtac conjunct1 1), |
|
161 (dtac spec 1), |
|
162 (dtac spec 1), |
|
163 (etac mp 1), |
|
164 (fast_tac HOL_cs 1) |
|
165 ]); |
|
166 |
|
167 |
|
168 val less_ssum1d = prove_goalw Ssum1.thy [less_ssum_def] |
|
169 "[|s1=Isinr(x); s2=Isinl(y)|] ==> less_ssum(s1,s2) = (x = UU)" |
|
170 (fn prems => |
|
171 [ |
|
172 (cut_facts_tac prems 1), |
|
173 (rtac select_equality 1), |
|
174 (dtac conjunct2 2), |
|
175 (dtac conjunct2 2), |
|
176 (dtac conjunct2 2), |
|
177 (dtac spec 2), |
|
178 (dtac spec 2), |
|
179 (etac mp 2), |
|
180 (fast_tac HOL_cs 2), |
|
181 (rtac conjI 1), |
|
182 (strip_tac 1), |
|
183 (etac conjE 1), |
|
184 (UU_right "x"), |
|
185 (UU_left "u"), |
|
186 (simp_tac Cfun_ss 1), |
|
187 (rtac conjI 1), |
|
188 (strip_tac 1), |
|
189 (etac conjE 1), |
|
190 (UU_right "ya"), |
|
191 (eq_right "x" "v"), |
|
192 (rtac iffI 1), |
|
193 (etac UU_I 2), |
|
194 (res_inst_tac [("s","UU"),("t","x")] subst 1), |
|
195 (etac sym 1), |
|
196 (rtac refl_less 1), |
|
197 (rtac conjI 1), |
|
198 (strip_tac 1), |
|
199 (etac conjE 1), |
|
200 (UU_right "x"), |
|
201 (UU_left "u"), |
|
202 (simp_tac HOL_ss 1), |
|
203 (strip_tac 1), |
|
204 (etac conjE 1), |
|
205 (eq_right "x" "v"), |
|
206 (rtac refl 1) |
|
207 ]) |
|
208 end; |
|
209 |
|
210 |
|
211 (* ------------------------------------------------------------------------ *) |
|
212 (* optimize lemmas about less_ssum *) |
|
213 (* ------------------------------------------------------------------------ *) |
|
214 |
|
215 val less_ssum2a = prove_goal Ssum1.thy |
|
216 "less_ssum(Isinl(x),Isinl(y)) = (x << y)" |
|
217 (fn prems => |
|
218 [ |
|
219 (rtac less_ssum1a 1), |
|
220 (rtac refl 1), |
|
221 (rtac refl 1) |
|
222 ]); |
|
223 |
|
224 val less_ssum2b = prove_goal Ssum1.thy |
|
225 "less_ssum(Isinr(x),Isinr(y)) = (x << y)" |
|
226 (fn prems => |
|
227 [ |
|
228 (rtac less_ssum1b 1), |
|
229 (rtac refl 1), |
|
230 (rtac refl 1) |
|
231 ]); |
|
232 |
|
233 val less_ssum2c = prove_goal Ssum1.thy |
|
234 "less_ssum(Isinl(x),Isinr(y)) = (x = UU)" |
|
235 (fn prems => |
|
236 [ |
|
237 (rtac less_ssum1c 1), |
|
238 (rtac refl 1), |
|
239 (rtac refl 1) |
|
240 ]); |
|
241 |
|
242 val less_ssum2d = prove_goal Ssum1.thy |
|
243 "less_ssum(Isinr(x),Isinl(y)) = (x = UU)" |
|
244 (fn prems => |
|
245 [ |
|
246 (rtac less_ssum1d 1), |
|
247 (rtac refl 1), |
|
248 (rtac refl 1) |
|
249 ]); |
|
250 |
|
251 |
|
252 (* ------------------------------------------------------------------------ *) |
|
253 (* less_ssum is a partial order on ++ *) |
|
254 (* ------------------------------------------------------------------------ *) |
|
255 |
|
256 val refl_less_ssum = prove_goal Ssum1.thy "less_ssum(p,p)" |
|
257 (fn prems => |
|
258 [ |
|
259 (res_inst_tac [("p","p")] IssumE2 1), |
|
260 (hyp_subst_tac 1), |
|
261 (rtac (less_ssum2a RS iffD2) 1), |
|
262 (rtac refl_less 1), |
|
263 (hyp_subst_tac 1), |
|
264 (rtac (less_ssum2b RS iffD2) 1), |
|
265 (rtac refl_less 1) |
|
266 ]); |
|
267 |
|
268 val antisym_less_ssum = prove_goal Ssum1.thy |
|
269 "[|less_ssum(p1,p2);less_ssum(p2,p1)|] ==> p1=p2" |
|
270 (fn prems => |
|
271 [ |
|
272 (cut_facts_tac prems 1), |
|
273 (res_inst_tac [("p","p1")] IssumE2 1), |
|
274 (hyp_subst_tac 1), |
|
275 (res_inst_tac [("p","p2")] IssumE2 1), |
|
276 (hyp_subst_tac 1), |
|
277 (res_inst_tac [("f","Isinl")] arg_cong 1), |
|
278 (rtac antisym_less 1), |
|
279 (etac (less_ssum2a RS iffD1) 1), |
|
280 (etac (less_ssum2a RS iffD1) 1), |
|
281 (hyp_subst_tac 1), |
|
282 (etac (less_ssum2d RS iffD1 RS ssubst) 1), |
|
283 (etac (less_ssum2c RS iffD1 RS ssubst) 1), |
|
284 (rtac strict_IsinlIsinr 1), |
|
285 (hyp_subst_tac 1), |
|
286 (res_inst_tac [("p","p2")] IssumE2 1), |
|
287 (hyp_subst_tac 1), |
|
288 (etac (less_ssum2c RS iffD1 RS ssubst) 1), |
|
289 (etac (less_ssum2d RS iffD1 RS ssubst) 1), |
|
290 (rtac (strict_IsinlIsinr RS sym) 1), |
|
291 (hyp_subst_tac 1), |
|
292 (res_inst_tac [("f","Isinr")] arg_cong 1), |
|
293 (rtac antisym_less 1), |
|
294 (etac (less_ssum2b RS iffD1) 1), |
|
295 (etac (less_ssum2b RS iffD1) 1) |
|
296 ]); |
|
297 |
|
298 val trans_less_ssum = prove_goal Ssum1.thy |
|
299 "[|less_ssum(p1,p2);less_ssum(p2,p3)|] ==> less_ssum(p1,p3)" |
|
300 (fn prems => |
|
301 [ |
|
302 (cut_facts_tac prems 1), |
|
303 (res_inst_tac [("p","p1")] IssumE2 1), |
|
304 (hyp_subst_tac 1), |
|
305 (res_inst_tac [("p","p3")] IssumE2 1), |
|
306 (hyp_subst_tac 1), |
|
307 (rtac (less_ssum2a RS iffD2) 1), |
|
308 (res_inst_tac [("p","p2")] IssumE2 1), |
|
309 (hyp_subst_tac 1), |
|
310 (rtac trans_less 1), |
|
311 (etac (less_ssum2a RS iffD1) 1), |
|
312 (etac (less_ssum2a RS iffD1) 1), |
|
313 (hyp_subst_tac 1), |
|
314 (etac (less_ssum2c RS iffD1 RS ssubst) 1), |
|
315 (rtac minimal 1), |
|
316 (hyp_subst_tac 1), |
|
317 (rtac (less_ssum2c RS iffD2) 1), |
|
318 (res_inst_tac [("p","p2")] IssumE2 1), |
|
319 (hyp_subst_tac 1), |
|
320 (rtac UU_I 1), |
|
321 (rtac trans_less 1), |
|
322 (etac (less_ssum2a RS iffD1) 1), |
|
323 (rtac (antisym_less_inverse RS conjunct1) 1), |
|
324 (etac (less_ssum2c RS iffD1) 1), |
|
325 (hyp_subst_tac 1), |
|
326 (etac (less_ssum2c RS iffD1) 1), |
|
327 (hyp_subst_tac 1), |
|
328 (res_inst_tac [("p","p3")] IssumE2 1), |
|
329 (hyp_subst_tac 1), |
|
330 (rtac (less_ssum2d RS iffD2) 1), |
|
331 (res_inst_tac [("p","p2")] IssumE2 1), |
|
332 (hyp_subst_tac 1), |
|
333 (etac (less_ssum2d RS iffD1) 1), |
|
334 (hyp_subst_tac 1), |
|
335 (rtac UU_I 1), |
|
336 (rtac trans_less 1), |
|
337 (etac (less_ssum2b RS iffD1) 1), |
|
338 (rtac (antisym_less_inverse RS conjunct1) 1), |
|
339 (etac (less_ssum2d RS iffD1) 1), |
|
340 (hyp_subst_tac 1), |
|
341 (rtac (less_ssum2b RS iffD2) 1), |
|
342 (res_inst_tac [("p","p2")] IssumE2 1), |
|
343 (hyp_subst_tac 1), |
|
344 (etac (less_ssum2d RS iffD1 RS ssubst) 1), |
|
345 (rtac minimal 1), |
|
346 (hyp_subst_tac 1), |
|
347 (rtac trans_less 1), |
|
348 (etac (less_ssum2b RS iffD1) 1), |
|
349 (etac (less_ssum2b RS iffD1) 1) |
|
350 ]); |
|
351 |
|
352 |
|
353 |