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