equal
deleted
inserted
replaced
485 (* derives an abs_eq theorem of the form |
485 (* derives an abs_eq theorem of the form |
486 |
486 |
487 Exists q. [as].x = [p o as].(q o x) for non-recursive binders |
487 Exists q. [as].x = [p o as].(q o x) for non-recursive binders |
488 Exists q. [as].x = [q o as].(q o x) for recursive binders |
488 Exists q. [as].x = [q o as].(q o x) for recursive binders |
489 *) |
489 *) |
490 fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns |
490 fun abs_eq_thm ctxt fprops p parms bn_eqvt permute_bns (bclause as (BC (bmode, binders, bodies))) = |
491 (bclause as (BC (bmode, binders, bodies))) = |
|
492 case binders of |
491 case binders of |
493 [] => [] |
492 [] => [] |
494 | _ => |
493 | _ => |
495 let |
494 let |
496 val rec_flag = is_recursive_binder bclause |
495 val rec_flag = is_recursive_binder bclause |
508 |
507 |
509 val goal = HOLogic.mk_conj (abs_eq, peq) |
508 val goal = HOLogic.mk_conj (abs_eq, peq) |
510 |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |
509 |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |
511 |> HOLogic.mk_Trueprop |
510 |> HOLogic.mk_Trueprop |
512 |
511 |
513 val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt} |
512 val ss = fprops @ @{thms set.simps set_append union_eqvt} |
514 @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset |
513 @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset |
515 fresh_star_set} @ @{thms finite.intros finite_fset} |
514 fresh_star_set} |
516 |
515 |
517 val tac1 = |
516 val tac1 = |
518 if rec_flag |
517 if rec_flag |
519 then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} |
518 then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} |
520 else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} |
519 else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} |
546 (K (EVERY1 [etac exE, |
545 (K (EVERY1 [etac exE, |
547 full_simp_tac (HOL_basic_ss addsimps ss), |
546 full_simp_tac (HOL_basic_ss addsimps ss), |
548 REPEAT o (etac @{thm conjE})])) [fthm] ctxt |
547 REPEAT o (etac @{thm conjE})])) [fthm] ctxt |
549 |
548 |
550 val abs_eq_thms = flat |
549 val abs_eq_thms = flat |
551 (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses) |
550 (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_eqvt permute_bns) bclauses) |
552 |
551 |
553 val ((_, eqs), ctxt'') = Obtain.result |
552 val ((_, eqs), ctxt'') = Obtain.result |
554 (K (EVERY1 |
553 (K (EVERY1 |
555 [ REPEAT o (etac @{thm exE}), |
554 [ REPEAT o (etac @{thm exE}), |
556 REPEAT o (etac @{thm conjE}), |
555 REPEAT o (etac @{thm conjE}), |