11 (* ------------------------------------------------------------------------ *) |
11 (* ------------------------------------------------------------------------ *) |
12 (* access to less_ssum in class po *) |
12 (* access to less_ssum in class po *) |
13 (* ------------------------------------------------------------------------ *) |
13 (* ------------------------------------------------------------------------ *) |
14 |
14 |
15 qed_goal "less_ssum3a" Ssum2.thy |
15 qed_goal "less_ssum3a" Ssum2.thy |
16 "(Isinl(x) << Isinl(y)) = (x << y)" |
16 "(Isinl(x) << Isinl(y)) = (x << y)" |
17 (fn prems => |
17 (fn prems => |
18 [ |
18 [ |
19 (rtac (inst_ssum_po RS ssubst) 1), |
19 (rtac (inst_ssum_po RS ssubst) 1), |
20 (rtac less_ssum2a 1) |
20 (rtac less_ssum2a 1) |
21 ]); |
21 ]); |
22 |
22 |
23 qed_goal "less_ssum3b" Ssum2.thy |
23 qed_goal "less_ssum3b" Ssum2.thy |
24 "(Isinr(x) << Isinr(y)) = (x << y)" |
24 "(Isinr(x) << Isinr(y)) = (x << y)" |
25 (fn prems => |
25 (fn prems => |
26 [ |
26 [ |
27 (rtac (inst_ssum_po RS ssubst) 1), |
27 (rtac (inst_ssum_po RS ssubst) 1), |
28 (rtac less_ssum2b 1) |
28 (rtac less_ssum2b 1) |
29 ]); |
29 ]); |
30 |
30 |
31 qed_goal "less_ssum3c" Ssum2.thy |
31 qed_goal "less_ssum3c" Ssum2.thy |
32 "(Isinl(x) << Isinr(y)) = (x = UU)" |
32 "(Isinl(x) << Isinr(y)) = (x = UU)" |
33 (fn prems => |
33 (fn prems => |
34 [ |
34 [ |
35 (rtac (inst_ssum_po RS ssubst) 1), |
35 (rtac (inst_ssum_po RS ssubst) 1), |
36 (rtac less_ssum2c 1) |
36 (rtac less_ssum2c 1) |
37 ]); |
37 ]); |
38 |
38 |
39 qed_goal "less_ssum3d" Ssum2.thy |
39 qed_goal "less_ssum3d" Ssum2.thy |
40 "(Isinr(x) << Isinl(y)) = (x = UU)" |
40 "(Isinr(x) << Isinl(y)) = (x = UU)" |
41 (fn prems => |
41 (fn prems => |
42 [ |
42 [ |
43 (rtac (inst_ssum_po RS ssubst) 1), |
43 (rtac (inst_ssum_po RS ssubst) 1), |
44 (rtac less_ssum2d 1) |
44 (rtac less_ssum2d 1) |
45 ]); |
45 ]); |
46 |
46 |
47 |
47 |
48 (* ------------------------------------------------------------------------ *) |
48 (* ------------------------------------------------------------------------ *) |
49 (* type ssum ++ is pointed *) |
49 (* type ssum ++ is pointed *) |
50 (* ------------------------------------------------------------------------ *) |
50 (* ------------------------------------------------------------------------ *) |
51 |
51 |
52 qed_goal "minimal_ssum" Ssum2.thy "Isinl(UU) << s" |
52 qed_goal "minimal_ssum" Ssum2.thy "Isinl(UU) << s" |
53 (fn prems => |
53 (fn prems => |
54 [ |
54 [ |
55 (res_inst_tac [("p","s")] IssumE2 1), |
55 (res_inst_tac [("p","s")] IssumE2 1), |
56 (hyp_subst_tac 1), |
56 (hyp_subst_tac 1), |
57 (rtac (less_ssum3a RS iffD2) 1), |
57 (rtac (less_ssum3a RS iffD2) 1), |
58 (rtac minimal 1), |
58 (rtac minimal 1), |
59 (hyp_subst_tac 1), |
59 (hyp_subst_tac 1), |
60 (rtac (strict_IsinlIsinr RS ssubst) 1), |
60 (rtac (strict_IsinlIsinr RS ssubst) 1), |
61 (rtac (less_ssum3b RS iffD2) 1), |
61 (rtac (less_ssum3b RS iffD2) 1), |
62 (rtac minimal 1) |
62 (rtac minimal 1) |
63 ]); |
63 ]); |
64 |
64 |
65 |
65 |
66 (* ------------------------------------------------------------------------ *) |
66 (* ------------------------------------------------------------------------ *) |
67 (* Isinl, Isinr are monotone *) |
67 (* Isinl, Isinr are monotone *) |
68 (* ------------------------------------------------------------------------ *) |
68 (* ------------------------------------------------------------------------ *) |
69 |
69 |
70 qed_goalw "monofun_Isinl" Ssum2.thy [monofun] "monofun(Isinl)" |
70 qed_goalw "monofun_Isinl" Ssum2.thy [monofun] "monofun(Isinl)" |
71 (fn prems => |
71 (fn prems => |
72 [ |
72 [ |
73 (strip_tac 1), |
73 (strip_tac 1), |
74 (etac (less_ssum3a RS iffD2) 1) |
74 (etac (less_ssum3a RS iffD2) 1) |
75 ]); |
75 ]); |
76 |
76 |
77 qed_goalw "monofun_Isinr" Ssum2.thy [monofun] "monofun(Isinr)" |
77 qed_goalw "monofun_Isinr" Ssum2.thy [monofun] "monofun(Isinr)" |
78 (fn prems => |
78 (fn prems => |
79 [ |
79 [ |
80 (strip_tac 1), |
80 (strip_tac 1), |
81 (etac (less_ssum3b RS iffD2) 1) |
81 (etac (less_ssum3b RS iffD2) 1) |
82 ]); |
82 ]); |
83 |
83 |
84 |
84 |
85 (* ------------------------------------------------------------------------ *) |
85 (* ------------------------------------------------------------------------ *) |
86 (* Iwhen is monotone in all arguments *) |
86 (* Iwhen is monotone in all arguments *) |
87 (* ------------------------------------------------------------------------ *) |
87 (* ------------------------------------------------------------------------ *) |
88 |
88 |
89 |
89 |
90 qed_goalw "monofun_Iwhen1" Ssum2.thy [monofun] "monofun(Iwhen)" |
90 qed_goalw "monofun_Iwhen1" Ssum2.thy [monofun] "monofun(Iwhen)" |
91 (fn prems => |
91 (fn prems => |
92 [ |
92 [ |
93 (strip_tac 1), |
93 (strip_tac 1), |
94 (rtac (less_fun RS iffD2) 1), |
94 (rtac (less_fun RS iffD2) 1), |
95 (strip_tac 1), |
95 (strip_tac 1), |
96 (rtac (less_fun RS iffD2) 1), |
96 (rtac (less_fun RS iffD2) 1), |
97 (strip_tac 1), |
97 (strip_tac 1), |
98 (res_inst_tac [("p","xb")] IssumE 1), |
98 (res_inst_tac [("p","xb")] IssumE 1), |
99 (hyp_subst_tac 1), |
99 (hyp_subst_tac 1), |
100 (asm_simp_tac Ssum0_ss 1), |
100 (asm_simp_tac Ssum0_ss 1), |
101 (asm_simp_tac Ssum0_ss 1), |
101 (asm_simp_tac Ssum0_ss 1), |
102 (etac monofun_cfun_fun 1), |
102 (etac monofun_cfun_fun 1), |
103 (asm_simp_tac Ssum0_ss 1) |
103 (asm_simp_tac Ssum0_ss 1) |
104 ]); |
104 ]); |
105 |
105 |
106 qed_goalw "monofun_Iwhen2" Ssum2.thy [monofun] "monofun(Iwhen(f))" |
106 qed_goalw "monofun_Iwhen2" Ssum2.thy [monofun] "monofun(Iwhen(f))" |
107 (fn prems => |
107 (fn prems => |
108 [ |
108 [ |
109 (strip_tac 1), |
109 (strip_tac 1), |
110 (rtac (less_fun RS iffD2) 1), |
110 (rtac (less_fun RS iffD2) 1), |
111 (strip_tac 1), |
111 (strip_tac 1), |
112 (res_inst_tac [("p","xa")] IssumE 1), |
112 (res_inst_tac [("p","xa")] IssumE 1), |
113 (hyp_subst_tac 1), |
113 (hyp_subst_tac 1), |
114 (asm_simp_tac Ssum0_ss 1), |
114 (asm_simp_tac Ssum0_ss 1), |
115 (asm_simp_tac Ssum0_ss 1), |
115 (asm_simp_tac Ssum0_ss 1), |
116 (asm_simp_tac Ssum0_ss 1), |
116 (asm_simp_tac Ssum0_ss 1), |
117 (etac monofun_cfun_fun 1) |
117 (etac monofun_cfun_fun 1) |
118 ]); |
118 ]); |
119 |
119 |
120 qed_goalw "monofun_Iwhen3" Ssum2.thy [monofun] "monofun(Iwhen(f)(g))" |
120 qed_goalw "monofun_Iwhen3" Ssum2.thy [monofun] "monofun(Iwhen(f)(g))" |
121 (fn prems => |
121 (fn prems => |
122 [ |
122 [ |
123 (strip_tac 1), |
123 (strip_tac 1), |
124 (res_inst_tac [("p","x")] IssumE 1), |
124 (res_inst_tac [("p","x")] IssumE 1), |
125 (hyp_subst_tac 1), |
125 (hyp_subst_tac 1), |
126 (asm_simp_tac Ssum0_ss 1), |
126 (asm_simp_tac Ssum0_ss 1), |
127 (hyp_subst_tac 1), |
127 (hyp_subst_tac 1), |
128 (res_inst_tac [("p","y")] IssumE 1), |
128 (res_inst_tac [("p","y")] IssumE 1), |
129 (hyp_subst_tac 1), |
129 (hyp_subst_tac 1), |
130 (asm_simp_tac Ssum0_ss 1), |
130 (asm_simp_tac Ssum0_ss 1), |
131 (res_inst_tac [("P","xa=UU")] notE 1), |
131 (res_inst_tac [("P","xa=UU")] notE 1), |
132 (atac 1), |
132 (atac 1), |
133 (rtac UU_I 1), |
133 (rtac UU_I 1), |
134 (rtac (less_ssum3a RS iffD1) 1), |
134 (rtac (less_ssum3a RS iffD1) 1), |
135 (atac 1), |
135 (atac 1), |
136 (hyp_subst_tac 1), |
136 (hyp_subst_tac 1), |
137 (asm_simp_tac Ssum0_ss 1), |
137 (asm_simp_tac Ssum0_ss 1), |
138 (rtac monofun_cfun_arg 1), |
138 (rtac monofun_cfun_arg 1), |
139 (etac (less_ssum3a RS iffD1) 1), |
139 (etac (less_ssum3a RS iffD1) 1), |
140 (hyp_subst_tac 1), |
140 (hyp_subst_tac 1), |
141 (res_inst_tac [("s","UU"),("t","xa")] subst 1), |
141 (res_inst_tac [("s","UU"),("t","xa")] subst 1), |
142 (etac (less_ssum3c RS iffD1 RS sym) 1), |
142 (etac (less_ssum3c RS iffD1 RS sym) 1), |
143 (asm_simp_tac Ssum0_ss 1), |
143 (asm_simp_tac Ssum0_ss 1), |
144 (hyp_subst_tac 1), |
144 (hyp_subst_tac 1), |
145 (res_inst_tac [("p","y")] IssumE 1), |
145 (res_inst_tac [("p","y")] IssumE 1), |
146 (hyp_subst_tac 1), |
146 (hyp_subst_tac 1), |
147 (res_inst_tac [("s","UU"),("t","ya")] subst 1), |
147 (res_inst_tac [("s","UU"),("t","ya")] subst 1), |
148 (etac (less_ssum3d RS iffD1 RS sym) 1), |
148 (etac (less_ssum3d RS iffD1 RS sym) 1), |
149 (asm_simp_tac Ssum0_ss 1), |
149 (asm_simp_tac Ssum0_ss 1), |
150 (hyp_subst_tac 1), |
150 (hyp_subst_tac 1), |
151 (res_inst_tac [("s","UU"),("t","ya")] subst 1), |
151 (res_inst_tac [("s","UU"),("t","ya")] subst 1), |
152 (etac (less_ssum3d RS iffD1 RS sym) 1), |
152 (etac (less_ssum3d RS iffD1 RS sym) 1), |
153 (asm_simp_tac Ssum0_ss 1), |
153 (asm_simp_tac Ssum0_ss 1), |
154 (hyp_subst_tac 1), |
154 (hyp_subst_tac 1), |
155 (asm_simp_tac Ssum0_ss 1), |
155 (asm_simp_tac Ssum0_ss 1), |
156 (rtac monofun_cfun_arg 1), |
156 (rtac monofun_cfun_arg 1), |
157 (etac (less_ssum3b RS iffD1) 1) |
157 (etac (less_ssum3b RS iffD1) 1) |
158 ]); |
158 ]); |
159 |
159 |
160 |
160 |
161 |
161 |
162 |
162 |
163 (* ------------------------------------------------------------------------ *) |
163 (* ------------------------------------------------------------------------ *) |
166 |
166 |
167 |
167 |
168 qed_goal "ssum_lemma1" Ssum2.thy |
168 qed_goal "ssum_lemma1" Ssum2.thy |
169 "[|~(!i.? x.Y(i::nat)=Isinl(x))|] ==> (? i.! x.Y(i)~=Isinl(x))" |
169 "[|~(!i.? x.Y(i::nat)=Isinl(x))|] ==> (? i.! x.Y(i)~=Isinl(x))" |
170 (fn prems => |
170 (fn prems => |
171 [ |
171 [ |
172 (cut_facts_tac prems 1), |
172 (cut_facts_tac prems 1), |
173 (fast_tac HOL_cs 1) |
173 (fast_tac HOL_cs 1) |
174 ]); |
174 ]); |
175 |
175 |
176 qed_goal "ssum_lemma2" Ssum2.thy |
176 qed_goal "ssum_lemma2" Ssum2.thy |
177 "[|(? i.!x.(Y::nat => 'a++'b)(i::nat)~=Isinl(x::'a))|] ==>\ |
177 "[|(? i.!x.(Y::nat => 'a++'b)(i::nat)~=Isinl(x::'a))|] ==>\ |
178 \ (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & y~=UU)" |
178 \ (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & y~=UU)" |
179 (fn prems => |
179 (fn prems => |
180 [ |
180 [ |
181 (cut_facts_tac prems 1), |
181 (cut_facts_tac prems 1), |
182 (etac exE 1), |
182 (etac exE 1), |
183 (res_inst_tac [("p","Y(i)")] IssumE 1), |
183 (res_inst_tac [("p","Y(i)")] IssumE 1), |
184 (dtac spec 1), |
184 (dtac spec 1), |
185 (contr_tac 1), |
185 (contr_tac 1), |
186 (dtac spec 1), |
186 (dtac spec 1), |
187 (contr_tac 1), |
187 (contr_tac 1), |
188 (fast_tac HOL_cs 1) |
188 (fast_tac HOL_cs 1) |
189 ]); |
189 ]); |
190 |
190 |
191 |
191 |
192 qed_goal "ssum_lemma3" Ssum2.thy |
192 qed_goal "ssum_lemma3" Ssum2.thy |
193 "[|is_chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\ |
193 "[|is_chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\ |
194 \ (!i.? y.Y(i)=Isinr(y))" |
194 \ (!i.? y.Y(i)=Isinr(y))" |
195 (fn prems => |
195 (fn prems => |
196 [ |
196 [ |
197 (cut_facts_tac prems 1), |
197 (cut_facts_tac prems 1), |
198 (etac exE 1), |
198 (etac exE 1), |
199 (etac exE 1), |
199 (etac exE 1), |
200 (rtac allI 1), |
200 (rtac allI 1), |
201 (res_inst_tac [("p","Y(ia)")] IssumE 1), |
201 (res_inst_tac [("p","Y(ia)")] IssumE 1), |
202 (rtac exI 1), |
202 (rtac exI 1), |
203 (rtac trans 1), |
203 (rtac trans 1), |
204 (rtac strict_IsinlIsinr 2), |
204 (rtac strict_IsinlIsinr 2), |
205 (atac 1), |
205 (atac 1), |
206 (etac exI 2), |
206 (etac exI 2), |
207 (etac conjE 1), |
207 (etac conjE 1), |
208 (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1), |
208 (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1), |
209 (hyp_subst_tac 2), |
209 (hyp_subst_tac 2), |
210 (etac exI 2), |
210 (etac exI 2), |
211 (eres_inst_tac [("P","x=UU")] notE 1), |
211 (eres_inst_tac [("P","x=UU")] notE 1), |
212 (rtac (less_ssum3d RS iffD1) 1), |
212 (rtac (less_ssum3d RS iffD1) 1), |
213 (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1), |
213 (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1), |
214 (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1), |
214 (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1), |
215 (etac (chain_mono RS mp) 1), |
215 (etac (chain_mono RS mp) 1), |
216 (atac 1), |
216 (atac 1), |
217 (eres_inst_tac [("P","xa=UU")] notE 1), |
217 (eres_inst_tac [("P","xa=UU")] notE 1), |
218 (rtac (less_ssum3c RS iffD1) 1), |
218 (rtac (less_ssum3c RS iffD1) 1), |
219 (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1), |
219 (eres_inst_tac [("s","Y(i)"),("t","Isinr(x)::'a++'b")] subst 1), |
220 (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1), |
220 (eres_inst_tac [("s","Y(ia)"),("t","Isinl(xa)::'a++'b")] subst 1), |
221 (etac (chain_mono RS mp) 1), |
221 (etac (chain_mono RS mp) 1), |
222 (atac 1) |
222 (atac 1) |
223 ]); |
223 ]); |
224 |
224 |
225 qed_goal "ssum_lemma4" Ssum2.thy |
225 qed_goal "ssum_lemma4" Ssum2.thy |
226 "is_chain(Y) ==> (!i.? x.Y(i)=Isinl(x))|(!i.? y.Y(i)=Isinr(y))" |
226 "is_chain(Y) ==> (!i.? x.Y(i)=Isinl(x))|(!i.? y.Y(i)=Isinr(y))" |
227 (fn prems => |
227 (fn prems => |
228 [ |
228 [ |
229 (cut_facts_tac prems 1), |
229 (cut_facts_tac prems 1), |
230 (rtac classical2 1), |
230 (rtac classical2 1), |
231 (etac disjI1 1), |
231 (etac disjI1 1), |
232 (rtac disjI2 1), |
232 (rtac disjI2 1), |
233 (etac ssum_lemma3 1), |
233 (etac ssum_lemma3 1), |
234 (rtac ssum_lemma2 1), |
234 (rtac ssum_lemma2 1), |
235 (etac ssum_lemma1 1) |
235 (etac ssum_lemma1 1) |
236 ]); |
236 ]); |
237 |
237 |
238 |
238 |
239 (* ------------------------------------------------------------------------ *) |
239 (* ------------------------------------------------------------------------ *) |
240 (* restricted surjectivity of Isinl *) |
240 (* restricted surjectivity of Isinl *) |
241 (* ------------------------------------------------------------------------ *) |
241 (* ------------------------------------------------------------------------ *) |
242 |
242 |
243 qed_goal "ssum_lemma5" Ssum2.thy |
243 qed_goal "ssum_lemma5" Ssum2.thy |
244 "z=Isinl(x)==> Isinl((Iwhen (LAM x.x) (LAM y.UU))(z)) = z" |
244 "z=Isinl(x)==> Isinl((Iwhen (LAM x.x) (LAM y.UU))(z)) = z" |
245 (fn prems => |
245 (fn prems => |
246 [ |
246 [ |
247 (cut_facts_tac prems 1), |
247 (cut_facts_tac prems 1), |
248 (hyp_subst_tac 1), |
248 (hyp_subst_tac 1), |
249 (res_inst_tac [("Q","x=UU")] classical2 1), |
249 (res_inst_tac [("Q","x=UU")] classical2 1), |
250 (asm_simp_tac Ssum0_ss 1), |
250 (asm_simp_tac Ssum0_ss 1), |
251 (asm_simp_tac Ssum0_ss 1) |
251 (asm_simp_tac Ssum0_ss 1) |
252 ]); |
252 ]); |
253 |
253 |
254 (* ------------------------------------------------------------------------ *) |
254 (* ------------------------------------------------------------------------ *) |
255 (* restricted surjectivity of Isinr *) |
255 (* restricted surjectivity of Isinr *) |
256 (* ------------------------------------------------------------------------ *) |
256 (* ------------------------------------------------------------------------ *) |
257 |
257 |
258 qed_goal "ssum_lemma6" Ssum2.thy |
258 qed_goal "ssum_lemma6" Ssum2.thy |
259 "z=Isinr(x)==> Isinr((Iwhen (LAM y.UU) (LAM x.x))(z)) = z" |
259 "z=Isinr(x)==> Isinr((Iwhen (LAM y.UU) (LAM x.x))(z)) = z" |
260 (fn prems => |
260 (fn prems => |
261 [ |
261 [ |
262 (cut_facts_tac prems 1), |
262 (cut_facts_tac prems 1), |
263 (hyp_subst_tac 1), |
263 (hyp_subst_tac 1), |
264 (res_inst_tac [("Q","x=UU")] classical2 1), |
264 (res_inst_tac [("Q","x=UU")] classical2 1), |
265 (asm_simp_tac Ssum0_ss 1), |
265 (asm_simp_tac Ssum0_ss 1), |
266 (asm_simp_tac Ssum0_ss 1) |
266 (asm_simp_tac Ssum0_ss 1) |
267 ]); |
267 ]); |
268 |
268 |
269 (* ------------------------------------------------------------------------ *) |
269 (* ------------------------------------------------------------------------ *) |
270 (* technical lemmas *) |
270 (* technical lemmas *) |
271 (* ------------------------------------------------------------------------ *) |
271 (* ------------------------------------------------------------------------ *) |
272 |
272 |
273 qed_goal "ssum_lemma7" Ssum2.thy |
273 qed_goal "ssum_lemma7" Ssum2.thy |
274 "[|Isinl(x) << z; x~=UU|] ==> ? y.z=Isinl(y) & y~=UU" |
274 "[|Isinl(x) << z; x~=UU|] ==> ? y.z=Isinl(y) & y~=UU" |
275 (fn prems => |
275 (fn prems => |
276 [ |
276 [ |
277 (cut_facts_tac prems 1), |
277 (cut_facts_tac prems 1), |
278 (res_inst_tac [("p","z")] IssumE 1), |
278 (res_inst_tac [("p","z")] IssumE 1), |
279 (hyp_subst_tac 1), |
279 (hyp_subst_tac 1), |
280 (etac notE 1), |
280 (etac notE 1), |
281 (rtac antisym_less 1), |
281 (rtac antisym_less 1), |
282 (etac (less_ssum3a RS iffD1) 1), |
282 (etac (less_ssum3a RS iffD1) 1), |
283 (rtac minimal 1), |
283 (rtac minimal 1), |
284 (fast_tac HOL_cs 1), |
284 (fast_tac HOL_cs 1), |
285 (hyp_subst_tac 1), |
285 (hyp_subst_tac 1), |
286 (rtac notE 1), |
286 (rtac notE 1), |
287 (etac (less_ssum3c RS iffD1) 2), |
287 (etac (less_ssum3c RS iffD1) 2), |
288 (atac 1) |
288 (atac 1) |
289 ]); |
289 ]); |
290 |
290 |
291 qed_goal "ssum_lemma8" Ssum2.thy |
291 qed_goal "ssum_lemma8" Ssum2.thy |
292 "[|Isinr(x) << z; x~=UU|] ==> ? y.z=Isinr(y) & y~=UU" |
292 "[|Isinr(x) << z; x~=UU|] ==> ? y.z=Isinr(y) & y~=UU" |
293 (fn prems => |
293 (fn prems => |
294 [ |
294 [ |
295 (cut_facts_tac prems 1), |
295 (cut_facts_tac prems 1), |
296 (res_inst_tac [("p","z")] IssumE 1), |
296 (res_inst_tac [("p","z")] IssumE 1), |
297 (hyp_subst_tac 1), |
297 (hyp_subst_tac 1), |
298 (etac notE 1), |
298 (etac notE 1), |
299 (etac (less_ssum3d RS iffD1) 1), |
299 (etac (less_ssum3d RS iffD1) 1), |
300 (hyp_subst_tac 1), |
300 (hyp_subst_tac 1), |
301 (rtac notE 1), |
301 (rtac notE 1), |
302 (etac (less_ssum3d RS iffD1) 2), |
302 (etac (less_ssum3d RS iffD1) 2), |
303 (atac 1), |
303 (atac 1), |
304 (fast_tac HOL_cs 1) |
304 (fast_tac HOL_cs 1) |
305 ]); |
305 ]); |
306 |
306 |
307 (* ------------------------------------------------------------------------ *) |
307 (* ------------------------------------------------------------------------ *) |
308 (* the type 'a ++ 'b is a cpo in three steps *) |
308 (* the type 'a ++ 'b is a cpo in three steps *) |
309 (* ------------------------------------------------------------------------ *) |
309 (* ------------------------------------------------------------------------ *) |
310 |
310 |
311 qed_goal "lub_ssum1a" Ssum2.thy |
311 qed_goal "lub_ssum1a" Ssum2.thy |
312 "[|is_chain(Y);(!i.? x.Y(i)=Isinl(x))|] ==>\ |
312 "[|is_chain(Y);(!i.? x.Y(i)=Isinl(x))|] ==>\ |
313 \ range(Y) <<|\ |
313 \ range(Y) <<|\ |
314 \ Isinl(lub(range(%i.(Iwhen (LAM x.x) (LAM y.UU))(Y i))))" |
314 \ Isinl(lub(range(%i.(Iwhen (LAM x.x) (LAM y.UU))(Y i))))" |
315 (fn prems => |
315 (fn prems => |
316 [ |
316 [ |
317 (cut_facts_tac prems 1), |
317 (cut_facts_tac prems 1), |
318 (rtac is_lubI 1), |
318 (rtac is_lubI 1), |
319 (rtac conjI 1), |
319 (rtac conjI 1), |
320 (rtac ub_rangeI 1), |
320 (rtac ub_rangeI 1), |
321 (rtac allI 1), |
321 (rtac allI 1), |
322 (etac allE 1), |
322 (etac allE 1), |
323 (etac exE 1), |
323 (etac exE 1), |
324 (res_inst_tac [("t","Y(i)")] (ssum_lemma5 RS subst) 1), |
324 (res_inst_tac [("t","Y(i)")] (ssum_lemma5 RS subst) 1), |
325 (atac 1), |
325 (atac 1), |
326 (rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1), |
326 (rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1), |
327 (rtac is_ub_thelub 1), |
327 (rtac is_ub_thelub 1), |
328 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
328 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
329 (strip_tac 1), |
329 (strip_tac 1), |
330 (res_inst_tac [("p","u")] IssumE2 1), |
330 (res_inst_tac [("p","u")] IssumE2 1), |
331 (res_inst_tac [("t","u")] (ssum_lemma5 RS subst) 1), |
331 (res_inst_tac [("t","u")] (ssum_lemma5 RS subst) 1), |
332 (atac 1), |
332 (atac 1), |
333 (rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1), |
333 (rtac (monofun_Isinl RS monofunE RS spec RS spec RS mp) 1), |
334 (rtac is_lub_thelub 1), |
334 (rtac is_lub_thelub 1), |
335 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
335 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
336 (etac (monofun_Iwhen3 RS ub2ub_monofun) 1), |
336 (etac (monofun_Iwhen3 RS ub2ub_monofun) 1), |
337 (hyp_subst_tac 1), |
337 (hyp_subst_tac 1), |
338 (rtac (less_ssum3c RS iffD2) 1), |
338 (rtac (less_ssum3c RS iffD2) 1), |
339 (rtac chain_UU_I_inverse 1), |
339 (rtac chain_UU_I_inverse 1), |
340 (rtac allI 1), |
340 (rtac allI 1), |
341 (res_inst_tac [("p","Y(i)")] IssumE 1), |
341 (res_inst_tac [("p","Y(i)")] IssumE 1), |
342 (asm_simp_tac Ssum0_ss 1), |
342 (asm_simp_tac Ssum0_ss 1), |
343 (asm_simp_tac Ssum0_ss 2), |
343 (asm_simp_tac Ssum0_ss 2), |
344 (etac notE 1), |
344 (etac notE 1), |
345 (rtac (less_ssum3c RS iffD1) 1), |
345 (rtac (less_ssum3c RS iffD1) 1), |
346 (res_inst_tac [("t","Isinl(x)")] subst 1), |
346 (res_inst_tac [("t","Isinl(x)")] subst 1), |
347 (atac 1), |
347 (atac 1), |
348 (etac (ub_rangeE RS spec) 1) |
348 (etac (ub_rangeE RS spec) 1) |
349 ]); |
349 ]); |
350 |
350 |
351 |
351 |
352 qed_goal "lub_ssum1b" Ssum2.thy |
352 qed_goal "lub_ssum1b" Ssum2.thy |
353 "[|is_chain(Y);(!i.? x.Y(i)=Isinr(x))|] ==>\ |
353 "[|is_chain(Y);(!i.? x.Y(i)=Isinr(x))|] ==>\ |
354 \ range(Y) <<|\ |
354 \ range(Y) <<|\ |
355 \ Isinr(lub(range(%i.(Iwhen (LAM y.UU) (LAM x.x))(Y i))))" |
355 \ Isinr(lub(range(%i.(Iwhen (LAM y.UU) (LAM x.x))(Y i))))" |
356 (fn prems => |
356 (fn prems => |
357 [ |
357 [ |
358 (cut_facts_tac prems 1), |
358 (cut_facts_tac prems 1), |
359 (rtac is_lubI 1), |
359 (rtac is_lubI 1), |
360 (rtac conjI 1), |
360 (rtac conjI 1), |
361 (rtac ub_rangeI 1), |
361 (rtac ub_rangeI 1), |
362 (rtac allI 1), |
362 (rtac allI 1), |
363 (etac allE 1), |
363 (etac allE 1), |
364 (etac exE 1), |
364 (etac exE 1), |
365 (res_inst_tac [("t","Y(i)")] (ssum_lemma6 RS subst) 1), |
365 (res_inst_tac [("t","Y(i)")] (ssum_lemma6 RS subst) 1), |
366 (atac 1), |
366 (atac 1), |
367 (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1), |
367 (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1), |
368 (rtac is_ub_thelub 1), |
368 (rtac is_ub_thelub 1), |
369 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
369 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
370 (strip_tac 1), |
370 (strip_tac 1), |
371 (res_inst_tac [("p","u")] IssumE2 1), |
371 (res_inst_tac [("p","u")] IssumE2 1), |
372 (hyp_subst_tac 1), |
372 (hyp_subst_tac 1), |
373 (rtac (less_ssum3d RS iffD2) 1), |
373 (rtac (less_ssum3d RS iffD2) 1), |
374 (rtac chain_UU_I_inverse 1), |
374 (rtac chain_UU_I_inverse 1), |
375 (rtac allI 1), |
375 (rtac allI 1), |
376 (res_inst_tac [("p","Y(i)")] IssumE 1), |
376 (res_inst_tac [("p","Y(i)")] IssumE 1), |
377 (asm_simp_tac Ssum0_ss 1), |
377 (asm_simp_tac Ssum0_ss 1), |
378 (asm_simp_tac Ssum0_ss 1), |
378 (asm_simp_tac Ssum0_ss 1), |
379 (etac notE 1), |
379 (etac notE 1), |
380 (rtac (less_ssum3d RS iffD1) 1), |
380 (rtac (less_ssum3d RS iffD1) 1), |
381 (res_inst_tac [("t","Isinr(y)")] subst 1), |
381 (res_inst_tac [("t","Isinr(y)")] subst 1), |
382 (atac 1), |
382 (atac 1), |
383 (etac (ub_rangeE RS spec) 1), |
383 (etac (ub_rangeE RS spec) 1), |
384 (res_inst_tac [("t","u")] (ssum_lemma6 RS subst) 1), |
384 (res_inst_tac [("t","u")] (ssum_lemma6 RS subst) 1), |
385 (atac 1), |
385 (atac 1), |
386 (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1), |
386 (rtac (monofun_Isinr RS monofunE RS spec RS spec RS mp) 1), |
387 (rtac is_lub_thelub 1), |
387 (rtac is_lub_thelub 1), |
388 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
388 (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
389 (etac (monofun_Iwhen3 RS ub2ub_monofun) 1) |
389 (etac (monofun_Iwhen3 RS ub2ub_monofun) 1) |
390 ]); |
390 ]); |
391 |
391 |
392 |
392 |
393 val thelub_ssum1a = lub_ssum1a RS thelubI; |
393 val thelub_ssum1a = lub_ssum1a RS thelubI; |
394 (* |
394 (* |
395 [| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==> |
395 [| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==> |