26 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); |
26 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); |
27 |
27 |
28 |
28 |
29 (** equivariance tactics **) |
29 (** equivariance tactics **) |
30 |
30 |
31 val perm_boolE = @{thm permute_boolE} |
|
32 |
|
33 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
31 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
34 let |
32 let |
35 val thy = Proof_Context.theory_of ctxt |
33 val thy = Proof_Context.theory_of ctxt |
36 val cpi = Thm.cterm_of thy (mk_minus pi) |
34 val cpi = Thm.cterm_of thy pi |
37 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
35 val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} |
38 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} |
36 val eqvt_sconfig = eqvt_strict_config addexcls pred_names |
39 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} |
37 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def permute_self split_paired_all} |
40 val eqvt_sconfig = |
38 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def permute_minus_cancel(2)} |
41 eqvt_strict_config addpres @{thms permute_minus_cancel(2)} addexcls pred_names |
|
42 in |
39 in |
43 eqvt_tac ctxt (eqvt_strict_config addexcls pred_names) THEN' |
40 eqvt_tac ctxt eqvt_sconfig THEN' |
44 SUBPROOF (fn {prems, context as ctxt, ...} => |
41 SUBPROOF (fn {prems, context as ctxt, ...} => |
45 let |
42 let |
46 val prems' = map (transform_prem2 ctxt pred_names) prems |
43 val prems' = map (transform_prem2 ctxt pred_names) prems |
47 val tac1 = resolve_tac prems' |
44 val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems' |
48 val tac2 = EVERY' [ rtac pi_intro_rule, |
45 val prems''' = map (simplify simps2 o simplify simps1) prems'' |
49 eqvt_tac ctxt eqvt_sconfig, resolve_tac prems' ] |
46 |
50 val tac3 = EVERY' [ rtac pi_intro_rule, |
|
51 eqvt_tac ctxt eqvt_sconfig, simp_tac simps1, |
|
52 simp_tac simps2, resolve_tac prems'] |
|
53 in |
47 in |
54 (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 |
48 HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac (prems' @ prems'' @ prems''')) |
55 end) ctxt |
49 end) ctxt |
56 end |
50 end |
57 |
51 |
58 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
52 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
59 let |
53 let |