7 |
7 |
8 signature NOMINAL_EQVT = |
8 signature NOMINAL_EQVT = |
9 sig |
9 sig |
10 val equivariance: string -> Proof.context -> local_theory |
10 val equivariance: string -> Proof.context -> local_theory |
11 val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic |
11 val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic |
12 val eqvt_rel_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic |
12 val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic |
13 end |
13 end |
14 |
14 |
15 structure Nominal_Eqvt : NOMINAL_EQVT = |
15 structure Nominal_Eqvt : NOMINAL_EQVT = |
16 struct |
16 struct |
17 |
17 |
25 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 |
25 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 |
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 (** |
29 (** |
30 proves F[f t] from F[t] which is the given theorem |
30 given the theorem F[t]; proves the theorem F[f t] |
|
31 |
31 - F needs to be monotone |
32 - F needs to be monotone |
32 - f returns either SOME for a term it fires |
33 - f returns either SOME for a term it fires on |
33 and NONE elsewhere |
34 and NONE elsewhere |
34 **) |
35 **) |
35 fun map_term f t = |
36 fun map_term f t = |
36 (case f t of |
37 (case f t of |
37 NONE => map_term' f t |
38 NONE => map_term' f t |
88 |
89 |
89 val perm_boolE = @{thm permute_boolE} |
90 val perm_boolE = @{thm permute_boolE} |
90 val perm_cancel = @{thms permute_minus_cancel(2)} |
91 val perm_cancel = @{thms permute_minus_cancel(2)} |
91 val perm_expand_bool = @{thms permute_fun_def minus_minus permute_bool_def} |
92 val perm_expand_bool = @{thms permute_fun_def minus_minus permute_bool_def} |
92 |
93 |
93 fun eqvt_rel_case_tac ctxt pred_names pi intro = |
94 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
94 let |
95 let |
95 val thy = ProofContext.theory_of ctxt |
96 val thy = ProofContext.theory_of ctxt |
96 val cpi = Thm.cterm_of thy (mk_minus pi) |
97 val cpi = Thm.cterm_of thy (mk_minus pi) |
97 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
98 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
98 val simps = HOL_basic_ss addsimps perm_expand_bool |
99 val simps = HOL_basic_ss addsimps perm_expand_bool |
148 val ({names, ...}, {raw_induct, intrs, ...}) = |
149 val ({names, ...}, {raw_induct, intrs, ...}) = |
149 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
150 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
150 val raw_induct = atomize_induct ctxt raw_induct |
151 val raw_induct = atomize_induct ctxt raw_induct |
151 val intros = map atomize_intr intrs |
152 val intros = map atomize_intr intrs |
152 val params_no = length (Inductive.params_of raw_induct) |
153 val params_no = length (Inductive.params_of raw_induct) |
153 val (([raw_concl], [raw_pi]), ctxt') = ctxt |
154 val (([raw_concl], [raw_pi]), ctxt') = |
154 |> Variable.import_terms false [concl_of raw_induct] |
155 ctxt |
155 ||>> Variable.variant_fixes ["p"] |
156 |> Variable.import_terms false [concl_of raw_induct] |
|
157 ||>> Variable.variant_fixes ["p"] |
156 val pi = Free (raw_pi, @{typ perm}) |
158 val pi = Free (raw_pi, @{typ perm}) |
157 val preds = map (fst o HOLogic.dest_imp) |
159 val preds = map (fst o HOLogic.dest_imp) |
158 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
160 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
159 val goal = HOLogic.mk_Trueprop |
161 val goal = HOLogic.mk_Trueprop |
160 (foldr1 HOLogic.mk_conj (map (prepare_goal params_no pi) preds)) |
162 (foldr1 HOLogic.mk_conj (map (prepare_goal params_no pi) preds)) |