equal
deleted
inserted
replaced
301 | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) |
301 | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) |
302 |
302 |
303 |
303 |
304 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
304 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
305 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |
305 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |
306 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def |
306 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_def permute_prod_def |
307 prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI} |
307 prod.rec prod.case prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI} |
308 |
308 |
309 fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps |
309 fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps |
310 fv_bn_eqvts qinduct bclausess ctxt = |
310 fv_bn_eqvts qinduct bclausess ctxt = |
311 let |
311 let |
312 val goals1 = map mk_fvs_goals fvs |
312 val goals1 = map mk_fvs_goals fvs |
353 (arg_ty, fn x => finite $ (to_set (qbn $ x))) |
353 (arg_ty, fn x => finite $ (to_set (qbn $ x))) |
354 end |
354 end |
355 |
355 |
356 val props = map mk_goal qbns |
356 val props = map mk_goal qbns |
357 val ss_tac = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (qbn_simps @ |
357 val ss_tac = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (qbn_simps @ |
358 @{thms set.simps set_append finite_insert finite.emptyI finite_Un})) |
358 @{thms set_simps set_append finite_insert finite.emptyI finite_Un})) |
359 in |
359 in |
360 induct_prove qtys props qinduct (K ss_tac) ctxt |
360 induct_prove qtys props qinduct (K ss_tac) ctxt |
361 end |
361 end |
362 |
362 |
363 |
363 |
530 |
530 |
531 val goal = HOLogic.mk_conj (abs_eq, peq) |
531 val goal = HOLogic.mk_conj (abs_eq, peq) |
532 |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |
532 |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |
533 |> HOLogic.mk_Trueprop |
533 |> HOLogic.mk_Trueprop |
534 |
534 |
535 val ss = fprops @ @{thms set.simps set_append union_eqvt} |
535 val ss = fprops @ @{thms set_simps set_append union_eqvt} |
536 @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset |
536 @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset |
537 fresh_star_set} |
537 fresh_star_set} |
538 |
538 |
539 val tac1 = |
539 val tac1 = |
540 if rec_flag |
540 if rec_flag |
578 (fn ctxt'' => EVERY1 |
578 (fn ctxt'' => EVERY1 |
579 [ REPEAT o (etac @{thm exE}), |
579 [ REPEAT o (etac @{thm exE}), |
580 REPEAT o (etac @{thm conjE}), |
580 REPEAT o (etac @{thm conjE}), |
581 REPEAT o (dtac setify), |
581 REPEAT o (dtac setify), |
582 full_simp_tac (put_simpset HOL_basic_ss ctxt'' |
582 full_simp_tac (put_simpset HOL_basic_ss ctxt'' |
583 addsimps @{thms set_append set.simps})]) abs_eq_thms ctxt' |
583 addsimps @{thms set_append set_simps})]) abs_eq_thms ctxt' |
584 |
584 |
585 val (abs_eqs, peqs) = split_filter is_abs_eq eqs |
585 val (abs_eqs, peqs) = split_filter is_abs_eq eqs |
586 |
586 |
587 val fprops' = |
587 val fprops' = |
588 map (eqvt_rule ctxt'' (eqvt_strict_config addpres permute_bns)) fprops |
588 map (eqvt_rule ctxt'' (eqvt_strict_config addpres permute_bns)) fprops |