34 (res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct2 RS ssubst)1) |
32 (res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct2 RS ssubst)1) |
35 THEN (rtac trans 1) |
33 THEN (rtac trans 1) |
36 THEN (atac 2) |
34 THEN (atac 2) |
37 THEN (etac sym 1)) |
35 THEN (etac sym 1)) |
38 |
36 |
39 in |
37 val prems = goalw thy [less_ssum_def] |
40 |
38 "[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"; |
41 val less_ssum1a = prove_goalw thy [less_ssum_def] |
39 by (cut_facts_tac prems 1); |
42 "[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)" |
40 by (rtac select_equality 1); |
43 (fn prems => |
41 by (dtac conjunct1 2); |
44 [ |
42 by (dtac spec 2); |
45 (cut_facts_tac prems 1), |
43 by (dtac spec 2); |
46 (rtac select_equality 1), |
44 by (etac mp 2); |
47 (dtac conjunct1 2), |
45 by (fast_tac HOL_cs 2); |
48 (dtac spec 2), |
46 by (rtac conjI 1); |
49 (dtac spec 2), |
47 by (strip_tac 1); |
50 (etac mp 2), |
48 by (etac conjE 1); |
51 (fast_tac HOL_cs 2), |
49 by (eq_left "x" "u"); |
52 (rtac conjI 1), |
50 by (eq_left "y" "xa"); |
53 (strip_tac 1), |
51 by (rtac refl 1); |
54 (etac conjE 1), |
52 by (rtac conjI 1); |
55 (eq_left "x" "u"), |
53 by (strip_tac 1); |
56 (eq_left "y" "xa"), |
54 by (etac conjE 1); |
57 (rtac refl 1), |
55 by (UU_left "x"); |
58 (rtac conjI 1), |
56 by (UU_right "v"); |
59 (strip_tac 1), |
57 by (Simp_tac 1); |
60 (etac conjE 1), |
58 by (rtac conjI 1); |
61 (UU_left "x"), |
59 by (strip_tac 1); |
62 (UU_right "v"), |
60 by (etac conjE 1); |
63 (Simp_tac 1), |
61 by (eq_left "x" "u"); |
64 (rtac conjI 1), |
62 by (UU_left "y"); |
65 (strip_tac 1), |
63 by (rtac iffI 1); |
66 (etac conjE 1), |
64 by (etac UU_I 1); |
67 (eq_left "x" "u"), |
65 by (res_inst_tac [("s","x"),("t","UU::'a")] subst 1); |
68 (UU_left "y"), |
66 by (atac 1); |
69 (rtac iffI 1), |
67 by (rtac refl_less 1); |
70 (etac UU_I 1), |
68 by (strip_tac 1); |
71 (res_inst_tac [("s","x"),("t","UU::'a")] subst 1), |
69 by (etac conjE 1); |
72 (atac 1), |
70 by (UU_left "x"); |
73 (rtac refl_less 1), |
71 by (UU_right "v"); |
74 (strip_tac 1), |
72 by (Simp_tac 1); |
75 (etac conjE 1), |
73 qed "less_ssum1a"; |
76 (UU_left "x"), |
74 |
77 (UU_right "v"), |
75 |
78 (Simp_tac 1) |
76 val prems = goalw thy [less_ssum_def] |
79 ]); |
77 "[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"; |
80 |
78 by (cut_facts_tac prems 1); |
81 |
79 by (rtac select_equality 1); |
82 val less_ssum1b = prove_goalw thy [less_ssum_def] |
80 by (dtac conjunct2 2); |
83 "[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)" |
81 by (dtac conjunct1 2); |
84 (fn prems => |
82 by (dtac spec 2); |
85 [ |
83 by (dtac spec 2); |
86 (cut_facts_tac prems 1), |
84 by (etac mp 2); |
87 (rtac select_equality 1), |
85 by (fast_tac HOL_cs 2); |
88 (dtac conjunct2 2), |
86 by (rtac conjI 1); |
89 (dtac conjunct1 2), |
87 by (strip_tac 1); |
90 (dtac spec 2), |
88 by (etac conjE 1); |
91 (dtac spec 2), |
89 by (UU_right "x"); |
92 (etac mp 2), |
90 by (UU_left "u"); |
93 (fast_tac HOL_cs 2), |
91 by (Simp_tac 1); |
94 (rtac conjI 1), |
92 by (rtac conjI 1); |
95 (strip_tac 1), |
93 by (strip_tac 1); |
96 (etac conjE 1), |
94 by (etac conjE 1); |
97 (UU_right "x"), |
95 by (eq_right "x" "v"); |
98 (UU_left "u"), |
96 by (eq_right "y" "ya"); |
99 (Simp_tac 1), |
97 by (rtac refl 1); |
100 (rtac conjI 1), |
98 by (rtac conjI 1); |
101 (strip_tac 1), |
99 by (strip_tac 1); |
102 (etac conjE 1), |
100 by (etac conjE 1); |
103 (eq_right "x" "v"), |
101 by (UU_right "x"); |
104 (eq_right "y" "ya"), |
102 by (UU_left "u"); |
105 (rtac refl 1), |
103 by (Simp_tac 1); |
106 (rtac conjI 1), |
104 by (strip_tac 1); |
107 (strip_tac 1), |
105 by (etac conjE 1); |
108 (etac conjE 1), |
106 by (eq_right "x" "v"); |
109 (UU_right "x"), |
107 by (UU_right "y"); |
110 (UU_left "u"), |
108 by (rtac iffI 1); |
111 (Simp_tac 1), |
109 by (etac UU_I 1); |
112 (strip_tac 1), |
110 by (res_inst_tac [("s","UU::'b"),("t","x")] subst 1); |
113 (etac conjE 1), |
111 by (etac sym 1); |
114 (eq_right "x" "v"), |
112 by (rtac refl_less 1); |
115 (UU_right "y"), |
113 qed "less_ssum1b"; |
116 (rtac iffI 1), |
114 |
117 (etac UU_I 1), |
115 |
118 (res_inst_tac [("s","UU::'b"),("t","x")] subst 1), |
116 val prems = goalw thy [less_ssum_def] |
119 (etac sym 1), |
117 "[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"; |
120 (rtac refl_less 1) |
118 by (cut_facts_tac prems 1); |
121 ]); |
119 by (rtac select_equality 1); |
122 |
120 by (rtac conjI 1); |
123 |
121 by (strip_tac 1); |
124 val less_ssum1c = prove_goalw thy [less_ssum_def] |
122 by (etac conjE 1); |
125 "[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)" |
123 by (eq_left "x" "u"); |
126 (fn prems => |
124 by (UU_left "xa"); |
127 [ |
125 by (rtac iffI 1); |
128 (cut_facts_tac prems 1), |
126 by (res_inst_tac [("s","x"),("t","UU::'a")] subst 1); |
129 (rtac select_equality 1), |
127 by (atac 1); |
130 (rtac conjI 1), |
128 by (rtac refl_less 1); |
131 (strip_tac 1), |
129 by (etac UU_I 1); |
132 (etac conjE 1), |
130 by (rtac conjI 1); |
133 (eq_left "x" "u"), |
131 by (strip_tac 1); |
134 (UU_left "xa"), |
132 by (etac conjE 1); |
135 (rtac iffI 1), |
133 by (UU_left "x"); |
136 (res_inst_tac [("s","x"),("t","UU::'a")] subst 1), |
134 by (UU_right "v"); |
137 (atac 1), |
135 by (Simp_tac 1); |
138 (rtac refl_less 1), |
136 by (rtac conjI 1); |
139 (etac UU_I 1), |
137 by (strip_tac 1); |
140 (rtac conjI 1), |
138 by (etac conjE 1); |
141 (strip_tac 1), |
139 by (eq_left "x" "u"); |
142 (etac conjE 1), |
140 by (rtac refl 1); |
143 (UU_left "x"), |
141 by (strip_tac 1); |
144 (UU_right "v"), |
142 by (etac conjE 1); |
145 (Simp_tac 1), |
143 by (UU_left "x"); |
146 (rtac conjI 1), |
144 by (UU_right "v"); |
147 (strip_tac 1), |
145 by (Simp_tac 1); |
148 (etac conjE 1), |
146 by (dtac conjunct2 1); |
149 (eq_left "x" "u"), |
147 by (dtac conjunct2 1); |
150 (rtac refl 1), |
148 by (dtac conjunct1 1); |
151 (strip_tac 1), |
149 by (dtac spec 1); |
152 (etac conjE 1), |
150 by (dtac spec 1); |
153 (UU_left "x"), |
151 by (etac mp 1); |
154 (UU_right "v"), |
152 by (fast_tac HOL_cs 1); |
155 (Simp_tac 1), |
153 qed "less_ssum1c"; |
156 (dtac conjunct2 1), |
154 |
157 (dtac conjunct2 1), |
155 |
158 (dtac conjunct1 1), |
156 val prems = goalw thy [less_ssum_def] |
159 (dtac spec 1), |
157 "[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"; |
160 (dtac spec 1), |
158 by (cut_facts_tac prems 1); |
161 (etac mp 1), |
159 by (rtac select_equality 1); |
162 (fast_tac HOL_cs 1) |
160 by (dtac conjunct2 2); |
163 ]); |
161 by (dtac conjunct2 2); |
164 |
162 by (dtac conjunct2 2); |
165 |
163 by (dtac spec 2); |
166 val less_ssum1d = prove_goalw thy [less_ssum_def] |
164 by (dtac spec 2); |
167 "[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)" |
165 by (etac mp 2); |
168 (fn prems => |
166 by (fast_tac HOL_cs 2); |
169 [ |
167 by (rtac conjI 1); |
170 (cut_facts_tac prems 1), |
168 by (strip_tac 1); |
171 (rtac select_equality 1), |
169 by (etac conjE 1); |
172 (dtac conjunct2 2), |
170 by (UU_right "x"); |
173 (dtac conjunct2 2), |
171 by (UU_left "u"); |
174 (dtac conjunct2 2), |
172 by (Simp_tac 1); |
175 (dtac spec 2), |
173 by (rtac conjI 1); |
176 (dtac spec 2), |
174 by (strip_tac 1); |
177 (etac mp 2), |
175 by (etac conjE 1); |
178 (fast_tac HOL_cs 2), |
176 by (UU_right "ya"); |
179 (rtac conjI 1), |
177 by (eq_right "x" "v"); |
180 (strip_tac 1), |
178 by (rtac iffI 1); |
181 (etac conjE 1), |
179 by (etac UU_I 2); |
182 (UU_right "x"), |
180 by (res_inst_tac [("s","UU"),("t","x")] subst 1); |
183 (UU_left "u"), |
181 by (etac sym 1); |
184 (Simp_tac 1), |
182 by (rtac refl_less 1); |
185 (rtac conjI 1), |
183 by (rtac conjI 1); |
186 (strip_tac 1), |
184 by (strip_tac 1); |
187 (etac conjE 1), |
185 by (etac conjE 1); |
188 (UU_right "ya"), |
186 by (UU_right "x"); |
189 (eq_right "x" "v"), |
187 by (UU_left "u"); |
190 (rtac iffI 1), |
188 by (Simp_tac 1); |
191 (etac UU_I 2), |
189 by (strip_tac 1); |
192 (res_inst_tac [("s","UU"),("t","x")] subst 1), |
190 by (etac conjE 1); |
193 (etac sym 1), |
191 by (eq_right "x" "v"); |
194 (rtac refl_less 1), |
192 by (rtac refl 1); |
195 (rtac conjI 1), |
193 qed "less_ssum1d"; |
196 (strip_tac 1), |
|
197 (etac conjE 1), |
|
198 (UU_right "x"), |
|
199 (UU_left "u"), |
|
200 (Simp_tac 1), |
|
201 (strip_tac 1), |
|
202 (etac conjE 1), |
|
203 (eq_right "x" "v"), |
|
204 (rtac refl 1) |
|
205 ]) |
|
206 end; |
|
207 |
194 |
208 |
195 |
209 (* ------------------------------------------------------------------------ *) |
196 (* ------------------------------------------------------------------------ *) |
210 (* optimize lemmas about less_ssum *) |
197 (* optimize lemmas about less_ssum *) |
211 (* ------------------------------------------------------------------------ *) |
198 (* ------------------------------------------------------------------------ *) |