238 by (Blast_tac 1); |
238 by (Blast_tac 1); |
239 by (thin_tac "? x xs. ?P x xs" 1); |
239 by (thin_tac "? x xs. ?P x xs" 1); |
240 by (Clarify_tac 1); |
240 by (Clarify_tac 1); |
241 by (rename_tac "maxA xs" 1); |
241 by (rename_tac "maxA xs" 1); |
242 by (eres_inst_tac [("x","{ys. size ys = size xs & maxA#ys : M}")] allE 1); |
242 by (eres_inst_tac [("x","{ys. size ys = size xs & maxA#ys : M}")] allE 1); |
243 be impE 1; |
243 by (etac impE 1); |
244 by(Blast_tac 1); |
244 by (Blast_tac 1); |
245 by (Clarify_tac 1); |
245 by (Clarify_tac 1); |
246 by (thin_tac "m : M" 1); |
246 by (thin_tac "m : M" 1); |
247 by (thin_tac "maxA#xs : M" 1); |
247 by (thin_tac "maxA#xs : M" 1); |
248 by (rtac bexI 1); |
248 by (rtac bexI 1); |
249 ba 2; |
249 by (assume_tac 2); |
250 by (Clarify_tac 1); |
250 by (Clarify_tac 1); |
251 by(Asm_full_simp_tac 1); |
251 by (Asm_full_simp_tac 1); |
252 by(Blast_tac 1); |
252 by (Blast_tac 1); |
253 qed "acc_le_listI"; |
253 qed "acc_le_listI"; |
254 AddSIs [acc_le_listI]; |
254 AddSIs [acc_le_listI]; |
255 |
255 |
256 |
256 |
257 Goalw [closed_def] |
257 Goalw [closed_def] |
258 "closed S f ==> closed (list n S) (map2 f)"; |
258 "closed S f ==> closed (list n S) (map2 f)"; |
259 by(induct_tac "n" 1); |
259 by (induct_tac "n" 1); |
260 by(Simp_tac 1); |
260 by (Simp_tac 1); |
261 by(Clarify_tac 1); |
261 by (Clarify_tac 1); |
262 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
262 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
263 by(Clarify_tac 1); |
263 by (Clarify_tac 1); |
264 by(Simp_tac 1); |
264 by (Simp_tac 1); |
265 by (Blast_tac 1); |
265 by (Blast_tac 1); |
266 qed "closed_listI"; |
266 qed "closed_listI"; |
267 |
267 |
268 |
268 |
269 Goalw [Listn.sl_def] |
269 Goalw [Listn.sl_def] |
270 "!!L. semilat L ==> semilat (Listn.sl n L)"; |
270 "!!L. semilat L ==> semilat (Listn.sl n L)"; |
271 by(split_all_tac 1); |
271 by (split_all_tac 1); |
272 by(simp_tac (HOL_basic_ss addsimps [semilat_Def,split]) 1); |
272 by (simp_tac (HOL_basic_ss addsimps [semilat_Def,split]) 1); |
273 br conjI 1; |
273 by (rtac conjI 1); |
274 by(Asm_simp_tac 1); |
274 by (Asm_simp_tac 1); |
275 br conjI 1; |
275 by (rtac conjI 1); |
276 by(asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_listI]) 1); |
276 by (asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_listI]) 1); |
277 by(simp_tac (HOL_basic_ss addsimps [list_def]) 1); |
277 by (simp_tac (HOL_basic_ss addsimps [list_def]) 1); |
278 by (asm_simp_tac (simpset() addsimps [plus_list_ub1,plus_list_ub2,plus_list_lub]) 1); |
278 by (asm_simp_tac (simpset() addsimps [plus_list_ub1,plus_list_ub2,plus_list_lub]) 1); |
279 qed "semilat_Listn_sl"; |
279 qed "semilat_Listn_sl"; |
280 |
280 |
281 |
281 |
282 Goal "!xes. xes : list n (err A) --> coalesce xes : err(list n A)"; |
282 Goal "!xes. xes : list n (err A) --> coalesce xes : err(list n A)"; |
283 by(induct_tac "n" 1); |
283 by (induct_tac "n" 1); |
284 by(Simp_tac 1); |
284 by (Simp_tac 1); |
285 by(Clarify_tac 1); |
285 by (Clarify_tac 1); |
286 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
286 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
287 by(Clarify_tac 1); |
287 by (Clarify_tac 1); |
288 by (simp_tac (simpset() addsimps [plussub_def,Err.sup_def,lift2_def] addsplits [err.split]) 1); |
288 by (simp_tac (simpset() addsimps [plussub_def,Err.sup_def,lift2_def] addsplits [err.split]) 1); |
289 by(Force_tac 1); |
289 by (Force_tac 1); |
290 qed_spec_mp "coalesce_in_err_list"; |
290 qed_spec_mp "coalesce_in_err_list"; |
291 |
291 |
292 |
292 |
293 Goal "x +_(op #) xs = x#xs"; |
293 Goal "x +_(op #) xs = x#xs"; |
294 by (simp_tac (simpset() addsimps [plussub_def]) 1); |
294 by (simp_tac (simpset() addsimps [plussub_def]) 1); |
296 |
296 |
297 Goal |
297 Goal |
298 "semilat(err A, Err.le r, lift2 f) ==> \ |
298 "semilat(err A, Err.le r, lift2 f) ==> \ |
299 \ !xs. xs : list n A --> (!ys. ys : list n A --> \ |
299 \ !xs. xs : list n A --> (!ys. ys : list n A --> \ |
300 \ (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))"; |
300 \ (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))"; |
301 by(induct_tac "n" 1); |
301 by (induct_tac "n" 1); |
302 by(Simp_tac 1); |
302 by (Simp_tac 1); |
303 by(Clarify_tac 1); |
303 by (Clarify_tac 1); |
304 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
304 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
305 by(Clarify_tac 1); |
305 by (Clarify_tac 1); |
306 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1); |
306 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1); |
307 by(force_tac (claset(), simpset() addsimps [semilat_le_err_OK1]) 1); |
307 by (force_tac (claset(), simpset() addsimps [semilat_le_err_OK1]) 1); |
308 qed_spec_mp "coalesce_eq_OK1_D"; |
308 qed_spec_mp "coalesce_eq_OK1_D"; |
309 |
309 |
310 Goal |
310 Goal |
311 "semilat(err A, Err.le r, lift2 f) ==> \ |
311 "semilat(err A, Err.le r, lift2 f) ==> \ |
312 \ !xs. xs : list n A --> (!ys. ys : list n A --> \ |
312 \ !xs. xs : list n A --> (!ys. ys : list n A --> \ |
313 \ (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))"; |
313 \ (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))"; |
314 by(induct_tac "n" 1); |
314 by (induct_tac "n" 1); |
315 by(Simp_tac 1); |
315 by (Simp_tac 1); |
316 by(Clarify_tac 1); |
316 by (Clarify_tac 1); |
317 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
317 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
318 by(Clarify_tac 1); |
318 by (Clarify_tac 1); |
319 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1); |
319 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1); |
320 by(force_tac (claset(), simpset() addsimps [semilat_le_err_OK2]) 1); |
320 by (force_tac (claset(), simpset() addsimps [semilat_le_err_OK2]) 1); |
321 qed_spec_mp "coalesce_eq_OK2_D"; |
321 qed_spec_mp "coalesce_eq_OK2_D"; |
322 |
322 |
323 Goalw [semilat_Def,plussub_def,err_def] |
323 Goalw [semilat_Def,plussub_def,err_def] |
324 "[| semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; \ |
324 "[| semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; \ |
325 \ u:A; x <=_r u; y <=_r u |] ==> z <=_r u"; |
325 \ u:A; x <=_r u; y <=_r u |] ==> z <=_r u"; |
326 by(asm_full_simp_tac (simpset() addsimps [lift2_def]) 1); |
326 by (asm_full_simp_tac (simpset() addsimps [lift2_def]) 1); |
327 by(Clarify_tac 1); |
327 by (Clarify_tac 1); |
328 by(rotate_tac ~3 1); |
328 by (rotate_tac ~3 1); |
329 by(etac thin_rl 1); |
329 by (etac thin_rl 1); |
330 by(etac thin_rl 1); |
330 by (etac thin_rl 1); |
331 by(Force_tac 1); |
331 by (Force_tac 1); |
332 qed "lift2_le_ub"; |
332 qed "lift2_le_ub"; |
333 |
333 |
334 Goal |
334 Goal |
335 "semilat(err A, Err.le r, lift2 f) ==> \ |
335 "semilat(err A, Err.le r, lift2 f) ==> \ |
336 \ !xs. xs : list n A --> (!ys. ys : list n A --> \ |
336 \ !xs. xs : list n A --> (!ys. ys : list n A --> \ |
337 \ (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us \ |
337 \ (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us \ |
338 \ & us : list n A --> zs <=[r] us))"; |
338 \ & us : list n A --> zs <=[r] us))"; |
339 by(induct_tac "n" 1); |
339 by (induct_tac "n" 1); |
340 by(Simp_tac 1); |
340 by (Simp_tac 1); |
341 by(Clarify_tac 1); |
341 by (Clarify_tac 1); |
342 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
342 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
343 by(Clarify_tac 1); |
343 by (Clarify_tac 1); |
344 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1); |
344 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1); |
345 by(Clarify_tac 1); |
345 by (Clarify_tac 1); |
346 br conjI 1; |
346 by (rtac conjI 1); |
347 by(Blast_tac 2); |
347 by (Blast_tac 2); |
348 by(blast_tac (claset() addIs [lift2_le_ub]) 1); |
348 by (blast_tac (claset() addIs [lift2_le_ub]) 1); |
349 qed_spec_mp "coalesce_eq_OK_ub_D"; |
349 qed_spec_mp "coalesce_eq_OK_ub_D"; |
350 |
350 |
351 Goal |
351 Goal |
352 "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A |] \ |
352 "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A |] \ |
353 \ ==> ~(? u:A. x <=_r u & y <=_r u)"; |
353 \ ==> ~(? u:A. x <=_r u & y <=_r u)"; |
354 by(asm_simp_tac (simpset() addsimps [OK_plus_OK_eq_Err_conv RS iffD1]) 1); |
354 by (asm_simp_tac (simpset() addsimps [OK_plus_OK_eq_Err_conv RS iffD1]) 1); |
355 qed "lift2_eq_ErrD"; |
355 qed "lift2_eq_ErrD"; |
356 |
356 |
357 Goal |
357 Goal |
358 "[| semilat(err A, Err.le r, lift2 f) \ |
358 "[| semilat(err A, Err.le r, lift2 f) \ |
359 \ |] ==> !xs. xs:list n A --> (!ys. ys:list n A --> \ |
359 \ |] ==> !xs. xs:list n A --> (!ys. ys:list n A --> \ |
360 \ coalesce (xs +[f] ys) = Err --> \ |
360 \ coalesce (xs +[f] ys) = Err --> \ |
361 \ ~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))"; |
361 \ ~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))"; |
362 by(induct_tac "n" 1); |
362 by (induct_tac "n" 1); |
363 by(Simp_tac 1); |
363 by (Simp_tac 1); |
364 by(Clarify_tac 1); |
364 by (Clarify_tac 1); |
365 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
365 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
366 by(Clarify_tac 1); |
366 by (Clarify_tac 1); |
367 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1); |
367 by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1); |
368 by(blast_tac (claset() addDs [lift2_eq_ErrD]) 1); |
368 by (blast_tac (claset() addDs [lift2_eq_ErrD]) 1); |
369 by(Blast_tac 1); |
369 by (Blast_tac 1); |
370 qed_spec_mp "coalesce_eq_Err_D"; |
370 qed_spec_mp "coalesce_eq_Err_D"; |
371 |
371 |
372 |
372 |
373 Goalw [closed_def] |
373 Goalw [closed_def] |
374 "closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)"; |
374 "closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)"; |
375 by(simp_tac (simpset() addsimps [err_def]) 1); |
375 by (simp_tac (simpset() addsimps [err_def]) 1); |
376 qed "closed_err_lift2_conv"; |
376 qed "closed_err_lift2_conv"; |
377 |
377 |
378 Goalw [map2_def] |
378 Goalw [map2_def] |
379 "closed (err A) (lift2 f) ==> \ |
379 "closed (err A) (lift2 f) ==> \ |
380 \ !xs. xs : list n A --> (!ys. ys : list n A --> \ |
380 \ !xs. xs : list n A --> (!ys. ys : list n A --> \ |
381 \ map2 f xs ys : list n (err A))"; |
381 \ map2 f xs ys : list n (err A))"; |
382 by(induct_tac "n" 1); |
382 by (induct_tac "n" 1); |
383 by(Simp_tac 1); |
383 by (Simp_tac 1); |
384 by(Clarify_tac 1); |
384 by (Clarify_tac 1); |
385 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
385 by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); |
386 by(Clarify_tac 1); |
386 by (Clarify_tac 1); |
387 by (full_simp_tac (simpset() addsimps [plussub_def,closed_err_lift2_conv]) 1); |
387 by (full_simp_tac (simpset() addsimps [plussub_def,closed_err_lift2_conv]) 1); |
388 by(Blast_tac 1); |
388 by (Blast_tac 1); |
389 qed_spec_mp "closed_map2_list"; |
389 qed_spec_mp "closed_map2_list"; |
390 |
390 |
391 Goal |
391 Goal |
392 "closed (err A) (lift2 f) ==> \ |
392 "closed (err A) (lift2 f) ==> \ |
393 \ closed (err (list n A)) (lift2 (sup f))"; |
393 \ closed (err (list n A)) (lift2 (sup f))"; |
394 by(fast_tac (claset() addss (simpset() addsimps |
394 by (fast_tac (claset() addss (simpset() addsimps |
395 [closed_def,plussub_def,sup_def,lift2_def, |
395 [closed_def,plussub_def,sup_def,lift2_def, |
396 coalesce_in_err_list,closed_map2_list] |
396 coalesce_in_err_list,closed_map2_list] |
397 addsplits [err.split])) 1); |
397 addsplits [err.split])) 1); |
398 qed "closed_lift2_sup"; |
398 qed "closed_lift2_sup"; |
399 |
399 |
400 Goalw [Err.sl_def] |
400 Goalw [Err.sl_def] |
401 "err_semilat (A,r,f) ==> \ |
401 "err_semilat (A,r,f) ==> \ |
402 \ err_semilat (list n A, Listn.le r, sup f)"; |
402 \ err_semilat (list n A, Listn.le r, sup f)"; |
403 by(asm_full_simp_tac (HOL_basic_ss addsimps [split]) 1); |
403 by (asm_full_simp_tac (HOL_basic_ss addsimps [split]) 1); |
404 by(simp_tac (HOL_basic_ss addsimps [semilat_Def,plussub_def]) 1); |
404 by (simp_tac (HOL_basic_ss addsimps [semilat_Def,plussub_def]) 1); |
405 by(asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_lift2_sup]) 1); |
405 by (asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_lift2_sup]) 1); |
406 br conjI 1; |
406 by (rtac conjI 1); |
407 bd semilatDorderI 1; |
407 by (dtac semilatDorderI 1); |
408 by(Asm_full_simp_tac 1); |
408 by (Asm_full_simp_tac 1); |
409 by(simp_tac (HOL_basic_ss addsimps |
409 by (simp_tac (HOL_basic_ss addsimps |
410 [unfold_lesub_err,Err.le_def,err_def,sup_def,lift2_def]) 1); |
410 [unfold_lesub_err,Err.le_def,err_def,sup_def,lift2_def]) 1); |
411 by (asm_simp_tac (simpset() addsimps |
411 by (asm_simp_tac (simpset() addsimps |
412 [coalesce_eq_OK1_D,coalesce_eq_OK2_D] addsplits [err.split]) 1); |
412 [coalesce_eq_OK1_D,coalesce_eq_OK2_D] addsplits [err.split]) 1); |
413 by(blast_tac (claset()addIs[coalesce_eq_OK_ub_D] addDs [coalesce_eq_Err_D]) 1); |
413 by (blast_tac (claset()addIs[coalesce_eq_OK_ub_D] addDs [coalesce_eq_Err_D]) 1); |
414 qed "err_semilat_sup"; |
414 qed "err_semilat_sup"; |
415 |
415 |
416 Goalw [Listn.upto_esl_def] |
416 Goalw [Listn.upto_esl_def] |
417 "!!L. err_semilat L ==> err_semilat(upto_esl m L)"; |
417 "!!L. err_semilat L ==> err_semilat(upto_esl m L)"; |
418 by(split_all_tac 1); |
418 by (split_all_tac 1); |
419 by(Asm_full_simp_tac 1); |
419 by (Asm_full_simp_tac 1); |
420 by(fast_tac (claset() |
420 by (fast_tac (claset() |
421 addSIs [err_semilat_UnionI,err_semilat_sup] |
421 addSIs [err_semilat_UnionI,err_semilat_sup] |
422 addDs [lesub_list_impl_same_size] addss (simpset() |
422 addDs [lesub_list_impl_same_size] addss (simpset() |
423 addsimps [plussub_def,Listn.sup_def])) 1); |
423 addsimps [plussub_def,Listn.sup_def])) 1); |
424 qed "err_semilat_upto_esl"; |
424 qed "err_semilat_upto_esl"; |