1 (* Title: HOL/BCV/Err.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2000 TUM |
|
5 *) |
|
6 |
|
7 Goalw [lesub_def] "e1 <=_(le r) e2 == le r e1 e2"; |
|
8 by (Simp_tac 1); |
|
9 qed "unfold_lesub_err"; |
|
10 |
|
11 Goalw [lesub_def,Err.le_def] "!x. x <=_r x ==> e <=_(Err.le r) e"; |
|
12 by (asm_simp_tac (simpset() addsplits [err.split]) 1); |
|
13 qed "le_err_refl"; |
|
14 |
|
15 Goalw [unfold_lesub_err,le_def] "order r ==> \ |
|
16 \ e1 <=_(le r) e2 --> e2 <=_(le r) e3 --> e1 <=_(le r) e3"; |
|
17 by (simp_tac (simpset() addsplits [err.split]) 1); |
|
18 by (blast_tac (claset() addIs [order_trans]) 1); |
|
19 qed_spec_mp "le_err_trans"; |
|
20 |
|
21 Goalw [unfold_lesub_err,le_def] |
|
22 "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e1 --> e1=e2"; |
|
23 by (simp_tac (simpset() addsplits [err.split]) 1); |
|
24 by (blast_tac (claset() addIs [order_antisym]) 1); |
|
25 qed_spec_mp "le_err_antisym"; |
|
26 |
|
27 |
|
28 Goalw [unfold_lesub_err,le_def] |
|
29 "(OK x <=_(le r) OK y) = (x <=_r y)"; |
|
30 by (Simp_tac 1); |
|
31 qed "OK_le_err_OK"; |
|
32 |
|
33 |
|
34 Goal "order(le r) = order r"; |
|
35 by (rtac iffI 1); |
|
36 by (stac order_def 1); |
|
37 by (blast_tac (claset() addDs [order_antisym,OK_le_err_OK RS iffD2] |
|
38 addIs [order_trans,OK_le_err_OK RS iffD1]) 1); |
|
39 by (stac order_def 1); |
|
40 by (blast_tac (claset() addIs [le_err_refl,le_err_trans,le_err_antisym] |
|
41 addDs [order_refl]) 1); |
|
42 qed "order_le_err"; |
|
43 AddIffs [order_le_err]; |
|
44 |
|
45 |
|
46 Goalw [unfold_lesub_err,le_def] |
|
47 "e <=_(le r) Err"; |
|
48 by (Simp_tac 1); |
|
49 qed "le_Err"; |
|
50 AddIffs [le_Err]; |
|
51 |
|
52 Goalw [unfold_lesub_err,le_def] |
|
53 "Err <=_(le r) e = (e = Err)"; |
|
54 by (simp_tac (simpset() addsplits [err.split]) 1); |
|
55 qed "Err_le_conv"; |
|
56 AddIffs [Err_le_conv]; |
|
57 |
|
58 Goalw [unfold_lesub_err,le_def] |
|
59 "e <=_(le r) OK x = (? y. e = OK y & y <=_r x)"; |
|
60 by (simp_tac (simpset() addsplits [err.split]) 1); |
|
61 qed "le_OK_conv"; |
|
62 AddIffs [le_OK_conv]; |
|
63 |
|
64 Goalw [unfold_lesub_err,le_def] |
|
65 "OK x <=_(le r) e = (e = Err | (? y. e = OK y & x <=_r y))"; |
|
66 by (simp_tac (simpset() addsplits [err.split]) 1); |
|
67 qed "OK_le_conv"; |
|
68 |
|
69 Goalw [top_def] "top (le r) Err"; |
|
70 by (Simp_tac 1); |
|
71 qed "top_Err"; |
|
72 AddIffs [top_Err]; |
|
73 |
|
74 Goalw [lesssub_def,lesub_def,le_def] |
|
75 "OK x <_(le r) e = (e=Err | (? y. e = OK y & x <_r y))"; |
|
76 by (simp_tac (simpset() addsplits [err.split]) 1); |
|
77 qed_spec_mp "OK_less_conv"; |
|
78 AddIffs [OK_less_conv]; |
|
79 |
|
80 Goalw [lesssub_def,lesub_def,le_def] "~(Err <_(le r) x)"; |
|
81 by (simp_tac (simpset() addsplits [err.split]) 1); |
|
82 qed_spec_mp "not_Err_less"; |
|
83 AddIffs [not_Err_less]; |
|
84 |
|
85 |
|
86 Goalw |
|
87 [semilat_Def,closed_def,plussub_def,lesub_def,lift2_def,Err.le_def,err_def] |
|
88 "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"; |
|
89 by (asm_full_simp_tac (simpset() addsplits [err.split]) 1); |
|
90 qed "semilat_errI"; |
|
91 |
|
92 Goalw [sl_def,esl_def] |
|
93 "!!L. semilat L ==> err_semilat(esl L)"; |
|
94 by (split_all_tac 1); |
|
95 by (asm_full_simp_tac (simpset() addsimps [semilat_errI]) 1); |
|
96 qed "err_semilat_eslI"; |
|
97 |
|
98 Goalw [acc_def,lesub_def,le_def,lesssub_def] |
|
99 "acc r ==> acc(le r)"; |
|
100 by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal] addsplits [err.split]) 1); |
|
101 by (Clarify_tac 1); |
|
102 by (case_tac "Err : Q" 1); |
|
103 by (Blast_tac 1); |
|
104 by (eres_inst_tac [("x","{a . OK a : Q}")] allE 1); |
|
105 by (case_tac "x" 1); |
|
106 by (Fast_tac 1); |
|
107 by (Blast_tac 1); |
|
108 qed "acc_err"; |
|
109 Addsimps [acc_err]; |
|
110 AddSIs [acc_err]; |
|
111 |
|
112 Goalw [err_def] "Err : err A"; |
|
113 by (Simp_tac 1); |
|
114 qed "Err_in_err"; |
|
115 AddIffs [Err_in_err]; |
|
116 |
|
117 Goalw [err_def] "(OK x : err A) = (x:A)"; |
|
118 by (Auto_tac); |
|
119 qed "OK_in_err"; |
|
120 AddIffs [OK_in_err]; |
|
121 |
|
122 |
|
123 (** lift **) |
|
124 |
|
125 Goalw [lift_def] |
|
126 "[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S"; |
|
127 by (asm_simp_tac (simpset() addsplits [err.split]) 1); |
|
128 by (Blast_tac 1); |
|
129 qed "lift_in_errI"; |
|
130 |
|
131 (** lift2 **) |
|
132 |
|
133 Goalw [lift2_def,plussub_def] "Err +_(lift2 f) x = Err"; |
|
134 by (Simp_tac 1); |
|
135 qed "Err_lift2"; |
|
136 |
|
137 Goalw [lift2_def,plussub_def] "x +_(lift2 f) Err = Err"; |
|
138 by (simp_tac (simpset() addsplits [err.split]) 1); |
|
139 qed "lift2_Err"; |
|
140 |
|
141 Goalw [lift2_def,plussub_def] "OK x +_(lift2 f) OK y = x +_f y"; |
|
142 by (simp_tac (simpset() addsplits [err.split]) 1); |
|
143 qed "OK_lift2_OK"; |
|
144 |
|
145 Addsimps [Err_lift2,lift2_Err,OK_lift2_OK]; |
|
146 |
|
147 (** sup **) |
|
148 |
|
149 Goalw [plussub_def,Err.sup_def,Err.lift2_def] "Err +_(Err.sup f) x = Err"; |
|
150 by (Simp_tac 1); |
|
151 qed "Err_sup_Err"; |
|
152 |
|
153 Goalw [plussub_def,Err.sup_def,Err.lift2_def] "x +_(Err.sup f) Err = Err"; |
|
154 by (simp_tac (simpset() addsplits [err.split]) 1); |
|
155 qed "Err_sup_Err2"; |
|
156 |
|
157 Goalw [plussub_def,Err.sup_def,Err.lift2_def] |
|
158 "OK x +_(Err.sup f) OK y = OK(x +_f y)"; |
|
159 by (Simp_tac 1); |
|
160 qed "Err_sup_OK"; |
|
161 |
|
162 Addsimps [Err_sup_Err,Err_sup_Err2,Err_sup_OK]; |
|
163 |
|
164 Goalw [Err.sup_def,lift2_def,plussub_def] |
|
165 "(Err.sup f ex ey = OK z) = (? x y. ex = OK x & ey = OK y & f x y = z)"; |
|
166 by (rtac iffI 1); |
|
167 by (Clarify_tac 2); |
|
168 by (Asm_simp_tac 2); |
|
169 by (asm_full_simp_tac (simpset() addsplits [err.split_asm]) 1); |
|
170 qed "Err_sup_eq_OK_conv"; |
|
171 AddIffs [Err_sup_eq_OK_conv]; |
|
172 |
|
173 Goalw [Err.sup_def,lift2_def,plussub_def] |
|
174 "(Err.sup f ex ey = Err) = (ex=Err | ey=Err)"; |
|
175 by (simp_tac (simpset() addsplits [err.split]) 1); |
|
176 qed "Err_sup_eq_Err"; |
|
177 AddIffs [Err_sup_eq_Err]; |
|
178 |
|
179 |
|
180 (*** semilat (err A) (le r) f ***) |
|
181 |
|
182 Goal "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err"; |
|
183 by (blast_tac (claset() addIs [le_iff_plus_unchanged RS iffD1,le_iff_plus_unchanged2 RS iffD1]) 1); |
|
184 qed "semilat_le_err_Err_plus"; |
|
185 |
|
186 Goal "[| x: err A; semilat(err A, le r, f) |] ==> x +_f Err = Err"; |
|
187 by (blast_tac (claset() addIs [le_iff_plus_unchanged RS iffD1,le_iff_plus_unchanged2 RS iffD1]) 1); |
|
188 qed "semilat_le_err_plus_Err"; |
|
189 |
|
190 Addsimps [semilat_le_err_Err_plus,semilat_le_err_plus_Err]; |
|
191 |
|
192 Goal "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] \ |
|
193 \ ==> x <=_r z"; |
|
194 by (rtac (OK_le_err_OK RS iffD1) 1); |
|
195 by (etac subst 1); |
|
196 by (Asm_simp_tac 1); |
|
197 qed "semilat_le_err_OK1"; |
|
198 |
|
199 Goal "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] \ |
|
200 \ ==> y <=_r z"; |
|
201 by (rtac (OK_le_err_OK RS iffD1) 1); |
|
202 by (etac subst 1); |
|
203 by (Asm_simp_tac 1); |
|
204 qed "semilat_le_err_OK2"; |
|
205 |
|
206 Goalw [order_def] "[| x=y; order r |] ==> x <=_r y"; |
|
207 by (Blast_tac 1); |
|
208 qed "eq_order_le"; |
|
209 |
|
210 Goal |
|
211 "[| x:A; y:A; semilat(err A, le r, fe) |] ==> \ |
|
212 \ ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"; |
|
213 by (rtac iffI 1); |
|
214 by (Clarify_tac 1); |
|
215 by (dtac (OK_le_err_OK RS iffD2) 1); |
|
216 by (dtac (OK_le_err_OK RS iffD2) 1); |
|
217 by (dtac semilat_lub 1); |
|
218 by (assume_tac 1); |
|
219 by (assume_tac 1); |
|
220 by (Asm_simp_tac 1); |
|
221 by (Asm_simp_tac 1); |
|
222 by (Asm_simp_tac 1); |
|
223 by (Asm_full_simp_tac 1); |
|
224 by (case_tac "(OK x) +_fe (OK y)" 1); |
|
225 by (assume_tac 1); |
|
226 by (rename_tac "z" 1); |
|
227 by (subgoal_tac "OK z: err A" 1); |
|
228 by (dtac eq_order_le 1); |
|
229 by (Blast_tac 1); |
|
230 by (blast_tac (claset() addDs [rotate_prems 3 (plus_le_conv RS iffD1)]) 1); |
|
231 by (etac subst 1); |
|
232 by (blast_tac (claset() addIs [closedD]) 1); |
|
233 qed "OK_plus_OK_eq_Err_conv"; |
|
234 Addsimps [OK_plus_OK_eq_Err_conv]; |
|
235 |
|
236 (*** semilat (err(Union AS)) ***) |
|
237 |
|
238 (* FIXME? *) |
|
239 Goal "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))"; |
|
240 by (Blast_tac 1); |
|
241 qed "all_bex_swap_lemma"; |
|
242 AddIffs [all_bex_swap_lemma]; |
|
243 |
|
244 Goalw [closed_def,err_def] |
|
245 "[| !A:AS. closed (err A) (lift2 f); AS ~= {}; \ |
|
246 \ !A:AS.!B:AS. A~=B --> (!a:A.!b:B. a +_f b = Err) |] \ |
|
247 \ ==> closed (err(Union AS)) (lift2 f)"; |
|
248 by (Asm_full_simp_tac 1); |
|
249 by (Clarify_tac 1); |
|
250 by (Asm_full_simp_tac 1); |
|
251 by (Fast_tac 1); |
|
252 qed "closed_err_Union_lift2I"; |
|
253 |
|
254 (* If AS = {} the thm collapses to |
|
255 order r & closed {Err} f & Err +_f Err = Err |
|
256 which may not hold *) |
|
257 Goalw [semilat_def,sl_def] |
|
258 "[| !A:AS. err_semilat(A, r, f); AS ~= {}; \ |
|
259 \ !A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |] \ |
|
260 \ ==> err_semilat(Union AS, r, f)"; |
|
261 by (asm_full_simp_tac (simpset() addsimps [closed_err_Union_lift2I]) 1); |
|
262 by (rtac conjI 1); |
|
263 by (Blast_tac 1); |
|
264 by (asm_full_simp_tac (simpset() addsimps [err_def]) 1); |
|
265 by (rtac conjI 1); |
|
266 by (Clarify_tac 1); |
|
267 by (rename_tac "A a u B b" 1); |
|
268 by (case_tac "A = B" 1); |
|
269 by (Asm_full_simp_tac 1); |
|
270 by (Asm_full_simp_tac 1); |
|
271 by (rtac conjI 1); |
|
272 by (Clarify_tac 1); |
|
273 by (rename_tac "A a u B b" 1); |
|
274 by (case_tac "A = B" 1); |
|
275 by (Asm_full_simp_tac 1); |
|
276 by (Asm_full_simp_tac 1); |
|
277 by (Clarify_tac 1); |
|
278 by (rename_tac "A ya yb B yd z C c a b" 1); |
|
279 by (case_tac "A = B" 1); |
|
280 by (case_tac "A = C" 1); |
|
281 by (Asm_full_simp_tac 1); |
|
282 by (rotate_tac ~1 1); |
|
283 by (Asm_full_simp_tac 1); |
|
284 by (rotate_tac ~1 1); |
|
285 by (case_tac "B = C" 1); |
|
286 by (Asm_full_simp_tac 1); |
|
287 by (rotate_tac ~1 1); |
|
288 by (Asm_full_simp_tac 1); |
|
289 qed "err_semilat_UnionI"; |
|