1 (* Title: nominal_eqvt.ML |
|
2 Author: Stefan Berghofer (original code) |
|
3 Author: Christian Urban |
|
4 |
|
5 Automatic proofs for equivariance of inductive predicates. |
|
6 *) |
|
7 |
|
8 signature NOMINAL_EQVT = |
|
9 sig |
|
10 val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic |
|
11 val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic |
|
12 |
|
13 val equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory |
|
14 val equivariance_cmd: string -> Proof.context -> local_theory |
|
15 end |
|
16 |
|
17 structure Nominal_Eqvt : NOMINAL_EQVT = |
|
18 struct |
|
19 |
|
20 open Nominal_Permeq; |
|
21 open Nominal_ThmDecls; |
|
22 |
|
23 val atomize_conv = |
|
24 MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) |
|
25 (HOL_basic_ss addsimps @{thms induct_atomize}); |
|
26 val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); |
|
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)); |
|
29 |
|
30 |
|
31 (** equivariance tactics **) |
|
32 |
|
33 val perm_boolE = @{thm permute_boolE} |
|
34 val perm_cancel = @{thms permute_minus_cancel(2)} |
|
35 |
|
36 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
|
37 let |
|
38 val thy = ProofContext.theory_of ctxt |
|
39 val cpi = Thm.cterm_of thy (mk_minus pi) |
|
40 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
|
41 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} |
|
42 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} |
|
43 in |
|
44 eqvt_strict_tac ctxt [] pred_names THEN' |
|
45 SUBPROOF (fn {prems, context as ctxt, ...} => |
|
46 let |
|
47 val prems' = map (transform_prem2 ctxt pred_names) prems |
|
48 val tac1 = resolve_tac prems' |
|
49 val tac2 = EVERY' [ rtac pi_intro_rule, |
|
50 eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] |
|
51 val tac3 = EVERY' [ rtac pi_intro_rule, |
|
52 eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, |
|
53 simp_tac simps2, resolve_tac prems'] |
|
54 in |
|
55 (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 |
|
56 end) ctxt |
|
57 end |
|
58 |
|
59 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
|
60 let |
|
61 val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros |
|
62 in |
|
63 EVERY' (rtac induct :: cases) |
|
64 end |
|
65 |
|
66 |
|
67 (** equivariance procedure *) |
|
68 |
|
69 fun prepare_goal pi pred = |
|
70 let |
|
71 val (c, xs) = strip_comb pred; |
|
72 in |
|
73 HOLogic.mk_imp (pred, list_comb (c, map (mk_perm pi) xs)) |
|
74 end |
|
75 |
|
76 (* stores thm under name.eqvt and adds [eqvt]-attribute *) |
|
77 |
|
78 fun note_named_thm (name, thm) ctxt = |
|
79 let |
|
80 val thm_name = Binding.qualified_name |
|
81 (Long_Name.qualify (Long_Name.base_name name) "eqvt") |
|
82 val attr = Attrib.internal (K eqvt_add) |
|
83 val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
|
84 in |
|
85 (thm', ctxt') |
|
86 end |
|
87 |
|
88 fun equivariance note_flag pred_trms raw_induct intrs ctxt = |
|
89 let |
|
90 val is_already_eqvt = |
|
91 filter (is_eqvt ctxt) pred_trms |
|
92 |> map (Syntax.string_of_term ctxt) |
|
93 val _ = if null is_already_eqvt then () |
|
94 else error ("Already equivariant: " ^ commas is_already_eqvt) |
|
95 |
|
96 val pred_names = map (fst o dest_Const) pred_trms |
|
97 val raw_induct' = atomize_induct ctxt raw_induct |
|
98 val intrs' = map atomize_intr intrs |
|
99 |
|
100 val (([raw_concl], [raw_pi]), ctxt') = |
|
101 ctxt |
|
102 |> Variable.import_terms false [concl_of raw_induct'] |
|
103 ||>> Variable.variant_fixes ["p"] |
|
104 val pi = Free (raw_pi, @{typ perm}) |
|
105 |
|
106 val preds = map (fst o HOLogic.dest_imp) |
|
107 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
|
108 |
|
109 val goal = HOLogic.mk_Trueprop |
|
110 (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) |
|
111 |
|
112 val thms = Goal.prove ctxt' [] [] goal |
|
113 (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |
|
114 |> Datatype_Aux.split_conj_thm |
|
115 |> ProofContext.export ctxt' ctxt |
|
116 |> map (fn th => th RS mp) |
|
117 |> map zero_var_indexes |
|
118 in |
|
119 if note_flag |
|
120 then fold_map note_named_thm (pred_names ~~ thms) ctxt |
|
121 else (thms, ctxt) |
|
122 end |
|
123 |
|
124 fun equivariance_cmd pred_name ctxt = |
|
125 let |
|
126 val thy = ProofContext.theory_of ctxt |
|
127 val (_, {preds, raw_induct, intrs, ...}) = |
|
128 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
|
129 in |
|
130 equivariance true preds raw_induct intrs ctxt |> snd |
|
131 end |
|
132 |
|
133 local structure P = Parse and K = Keyword in |
|
134 |
|
135 val _ = |
|
136 Outer_Syntax.local_theory "equivariance" |
|
137 "Proves equivariance for inductive predicate involving nominal datatypes." |
|
138 K.thy_decl (P.xname >> equivariance_cmd); |
|
139 |
|
140 end; |
|
141 |
|
142 end (* structure *) |
|