16 struct |
16 struct |
17 |
17 |
18 open Nominal_Permeq; |
18 open Nominal_Permeq; |
19 open Nominal_ThmDecls; |
19 open Nominal_ThmDecls; |
20 |
20 |
21 val atomize_conv = |
21 fun atomize_conv ctxt = |
22 Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) |
22 Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) |
23 (HOL_basic_ss addsimps @{thms induct_atomize}) |
23 (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize}) |
24 |
24 |
25 val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv) |
25 fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt)) |
26 |
26 |
27 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 |
27 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 |
28 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)) |
28 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 (atomize_conv ctxt))) ctxt)) |
29 |
29 |
30 |
30 |
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 thy = Proof_Context.theory_of ctxt |
35 val thy = Proof_Context.theory_of ctxt |
36 val cpi = Thm.cterm_of thy pi |
36 val cpi = Thm.cterm_of thy pi |
37 val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} |
37 val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} |
38 val eqvt_sconfig = eqvt_strict_config addexcls pred_names |
38 val eqvt_sconfig = eqvt_strict_config addexcls pred_names |
39 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def permute_self split_paired_all} |
39 val simps1 = |
40 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def permute_minus_cancel(2)} |
40 put_simpset HOL_basic_ss ctxt addsimps @{thms permute_fun_def permute_self split_paired_all} |
|
41 val simps2 = |
|
42 put_simpset HOL_basic_ss ctxt addsimps @{thms permute_bool_def permute_minus_cancel(2)} |
41 in |
43 in |
42 eqvt_tac ctxt eqvt_sconfig THEN' |
44 eqvt_tac ctxt eqvt_sconfig THEN' |
43 SUBPROOF (fn {prems, context as ctxt, ...} => |
45 SUBPROOF (fn {prems, context as ctxt, ...} => |
44 let |
46 let |
45 val prems' = map (transform_prem2 ctxt pred_names) prems |
47 val prems' = map (transform_prem2 ctxt pred_names) prems |
84 else error ("Already equivariant: " ^ commas |
86 else error ("Already equivariant: " ^ commas |
85 (map (Syntax.string_of_term ctxt) is_already_eqvt)) |
87 (map (Syntax.string_of_term ctxt) is_already_eqvt)) |
86 |
88 |
87 val pred_names = map (name_of o head_of) preds |
89 val pred_names = map (name_of o head_of) preds |
88 val raw_induct' = atomize_induct ctxt raw_induct |
90 val raw_induct' = atomize_induct ctxt raw_induct |
89 val intrs' = map atomize_intr intrs |
91 val intrs' = map (atomize_intr ctxt) intrs |
90 |
92 |
91 val (([raw_concl], [raw_pi]), ctxt') = |
93 val (([raw_concl], [raw_pi]), ctxt') = |
92 ctxt |
94 ctxt |
93 |> Variable.import_terms false [concl_of raw_induct'] |
95 |> Variable.import_terms false [concl_of raw_induct'] |
94 ||>> Variable.variant_fixes ["p"] |
96 ||>> Variable.variant_fixes ["p"] |