302 @ @{thms ho_all_prs ho_ex_prs} *} |
302 @ @{thms ho_all_prs ho_ex_prs} *} |
303 |
303 |
304 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
304 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
305 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
305 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
306 ML {* val consts = lookup_quot_consts defs *} |
306 ML {* val consts = lookup_quot_consts defs *} |
307 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
307 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *} |
308 |
308 |
309 lemma "IN x EMPTY = False" |
309 lemma "IN x EMPTY = False" |
310 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *}) |
310 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *}) |
311 |
311 |
312 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
312 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
332 (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)" |
332 (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)" |
333 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
333 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
334 done |
334 done |
335 |
335 |
336 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
336 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
337 apply(tactic {* Induct.fix_tac @{context} 0 [("x", @{typ "'b fset"}), ("xa", @{typ "'b fset"})] 1 *}) |
|
338 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
339 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
337 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
340 done |
338 done |
341 |
339 |
342 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
340 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
343 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
341 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
410 apply (auto simp add: FUN_REL_EQ) |
408 apply (auto simp add: FUN_REL_EQ) |
411 sorry |
409 sorry |
412 |
410 |
413 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
411 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
414 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
412 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
415 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
413 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *} |
416 |
414 |
417 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *} |
|
418 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
|
419 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
415 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
420 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
416 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
421 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) |
417 done |
422 apply (tactic {* (simp_tac (HOL_ss addsimps |
418 |
423 @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id})) 1 *}) |
|
424 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
|
425 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *}) |
|
426 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
|
427 done |
|
428 |
|
429 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.cases(2)})) *} |
|
430 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
|
431 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" |
419 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" |
432 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) |
420 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) |
433 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) |
|
434 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
|
435 done |
421 done |
436 |
422 |
437 lemma list_induct_part: |
423 lemma list_induct_part: |
438 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
424 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
439 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
425 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
450 |
436 |
451 |
437 |
452 |
438 |
453 (* Construction site starts here *) |
439 (* Construction site starts here *) |
454 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
440 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
455 apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *}) |
441 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *}) |
456 apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
442 apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
457 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
443 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
458 apply (rule FUN_QUOTIENT) |
444 apply (rule FUN_QUOTIENT) |
459 apply (rule FUN_QUOTIENT) |
445 apply (rule FUN_QUOTIENT) |
460 apply (rule IDENTITY_QUOTIENT) |
446 apply (rule IDENTITY_QUOTIENT) |
476 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
462 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
477 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
463 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
478 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
464 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
479 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
465 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
480 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
466 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
481 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
482 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
467 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
483 apply (rule IDENTITY_QUOTIENT) |
468 apply (rule IDENTITY_QUOTIENT) |
484 apply (rule FUN_QUOTIENT) |
469 apply (rule FUN_QUOTIENT) |
485 apply (rule QUOTIENT_fset) |
470 apply (rule QUOTIENT_fset) |
486 apply (rule IDENTITY_QUOTIENT) |
471 apply (rule IDENTITY_QUOTIENT) |
500 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
485 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
501 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
486 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
502 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
487 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
503 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
488 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
504 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
489 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
505 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
|
506 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
490 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
507 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
491 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
508 apply assumption |
492 apply assumption |
509 apply (rule refl) |
493 apply (rule refl) |
510 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
494 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
520 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
504 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
521 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
505 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
522 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
506 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
523 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
507 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
524 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
508 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
525 apply (simp only:map_id) |
509 apply (tactic {* clean_tac @{context} quot defs reps_same absrep [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *}) |
526 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
|
527 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
|
528 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *}) |
|
529 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
|
530 ML_prf {* val t = applic_prs @{context} rty qty absrep @{typ "('b \<Rightarrow> 'c list \<Rightarrow> bool)"} *} |
|
531 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] [t]) 1 *}) |
|
532 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
|
533 done |
510 done |
534 |
511 |
535 end |
512 end |