equal
deleted
inserted
replaced
31 (** equivariance tactics **) |
31 (** equivariance tactics **) |
32 |
32 |
33 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
33 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
34 let |
34 let |
35 val cpi = Thm.cterm_of ctxt pi |
35 val cpi = Thm.cterm_of ctxt pi |
36 val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} |
36 val pi_intro_rule = Thm.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} |
37 val eqvt_sconfig = eqvt_strict_config addexcls pred_names |
37 val eqvt_sconfig = eqvt_strict_config addexcls pred_names |
38 val simps1 = |
38 val simps1 = |
39 put_simpset HOL_basic_ss ctxt addsimps @{thms permute_fun_def permute_self split_paired_all} |
39 put_simpset HOL_basic_ss ctxt addsimps @{thms permute_fun_def permute_self split_paired_all} |
40 val simps2 = |
40 val simps2 = |
41 put_simpset HOL_basic_ss ctxt addsimps @{thms permute_bool_def permute_minus_cancel(2)} |
41 put_simpset HOL_basic_ss ctxt addsimps @{thms permute_bool_def permute_minus_cancel(2)} |
45 let |
45 let |
46 val prems' = map (transform_prem2 ctxt pred_names) prems |
46 val prems' = map (transform_prem2 ctxt pred_names) prems |
47 val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems' |
47 val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems' |
48 val prems''' = map (simplify simps2 o simplify simps1) prems'' |
48 val prems''' = map (simplify simps2 o simplify simps1) prems'' |
49 in |
49 in |
50 HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac ctxt (prems' @ prems'' @ prems''')) |
50 HEADGOAL (resolve_tac ctxt [intro] THEN_ALL_NEW |
|
51 resolve_tac ctxt (prems' @ prems'' @ prems''')) |
51 end) ctxt |
52 end) ctxt |
52 end |
53 end |
53 |
54 |
54 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
55 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
55 let |
56 let |
56 val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros |
57 val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros |
57 in |
58 in |
58 EVERY' ((DETERM o rtac induct) :: cases) |
59 EVERY' ((DETERM o resolve_tac ctxt [induct]) :: cases) |
59 end |
60 end |
60 |
61 |
61 |
62 |
62 (** equivariance procedure **) |
63 (** equivariance procedure **) |
63 |
64 |