equal
deleted
inserted
replaced
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 cpi = Thm.cterm_of ctxt pi |
36 val cpi = Thm.cterm_of thy pi |
|
37 val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} |
36 val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} |
38 val eqvt_sconfig = eqvt_strict_config addexcls pred_names |
37 val eqvt_sconfig = eqvt_strict_config addexcls pred_names |
39 val simps1 = |
38 val simps1 = |
40 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} |
41 val simps2 = |
40 val simps2 = |
46 let |
45 let |
47 val prems' = map (transform_prem2 ctxt pred_names) prems |
46 val prems' = map (transform_prem2 ctxt pred_names) prems |
48 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' |
49 val prems''' = map (simplify simps2 o simplify simps1) prems'' |
48 val prems''' = map (simplify simps2 o simplify simps1) prems'' |
50 in |
49 in |
51 HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac (prems' @ prems'' @ prems''')) |
50 HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac ctxt (prems' @ prems'' @ prems''')) |
52 end) ctxt |
51 end) ctxt |
53 end |
52 end |
54 |
53 |
55 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
54 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
56 let |
55 let |
90 val raw_induct' = atomize_induct ctxt raw_induct |
89 val raw_induct' = atomize_induct ctxt raw_induct |
91 val intrs' = map (atomize_intr ctxt) intrs |
90 val intrs' = map (atomize_intr ctxt) intrs |
92 |
91 |
93 val (([raw_concl], [raw_pi]), ctxt') = |
92 val (([raw_concl], [raw_pi]), ctxt') = |
94 ctxt |
93 ctxt |
95 |> Variable.import_terms false [concl_of raw_induct'] |
94 |> Variable.import_terms false [Thm.concl_of raw_induct'] |
96 ||>> Variable.variant_fixes ["p"] |
95 ||>> Variable.variant_fixes ["p"] |
97 val pi = Free (raw_pi, @{typ perm}) |
96 val pi = Free (raw_pi, @{typ perm}) |
98 |
97 |
99 val preds_with_args = raw_concl |
98 val preds_with_args = raw_concl |
100 |> HOLogic.dest_Trueprop |
99 |> HOLogic.dest_Trueprop |
106 |> foldr1 HOLogic.mk_conj |
105 |> foldr1 HOLogic.mk_conj |
107 |> HOLogic.mk_Trueprop |
106 |> HOLogic.mk_Trueprop |
108 in |
107 in |
109 Goal.prove ctxt' [] [] goal |
108 Goal.prove ctxt' [] [] goal |
110 (fn {context, ...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |
109 (fn {context, ...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |
111 |> Datatype_Aux.split_conj_thm |
110 |> Old_Datatype_Aux.split_conj_thm |
112 |> Proof_Context.export ctxt' ctxt |
111 |> Proof_Context.export ctxt' ctxt |
113 |> map (fn th => th RS mp) |
112 |> map (fn th => th RS mp) |
114 |> map zero_var_indexes |
113 |> map zero_var_indexes |
115 end |
114 end |
116 |
115 |
138 in |
137 in |
139 fold_map note_named_thm (names ~~ thms) ctxt |> snd |
138 fold_map note_named_thm (names ~~ thms) ctxt |> snd |
140 end |
139 end |
141 |
140 |
142 val _ = |
141 val _ = |
143 Outer_Syntax.local_theory @{command_spec "equivariance"} |
142 Outer_Syntax.local_theory @{command_keyword equivariance} |
144 "Proves equivariance for inductive predicate involving nominal datatypes." |
143 "Proves equivariance for inductive predicate involving nominal datatypes." |
145 (Parse.const >> equivariance_cmd) |
144 (Parse.const >> equivariance_cmd) |
146 |
145 |
147 end (* structure *) |
146 end (* structure *) |