5 Automatic proofs for equivariance of inductive predicates. |
5 Automatic proofs for equivariance of inductive predicates. |
6 *) |
6 *) |
7 |
7 |
8 signature NOMINAL_EQVT = |
8 signature NOMINAL_EQVT = |
9 sig |
9 sig |
10 val equivariance: string -> Proof.context -> local_theory |
|
11 val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic |
10 val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic |
12 val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic |
11 val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic |
|
12 |
|
13 val equivariance: term list -> thm -> thm list -> Proof.context -> (string * thm list) list * local_theory |
|
14 val equivariance_cmd: string -> Proof.context -> local_theory |
13 end |
15 end |
14 |
16 |
15 structure Nominal_Eqvt : NOMINAL_EQVT = |
17 structure Nominal_Eqvt : NOMINAL_EQVT = |
16 struct |
18 struct |
17 |
19 |
125 (** equivariance procedure *) |
127 (** equivariance procedure *) |
126 |
128 |
127 (* sets up goal and makes sure parameters |
129 (* sets up goal and makes sure parameters |
128 are untouched PROBLEM: this violates the |
130 are untouched PROBLEM: this violates the |
129 form of eqvt lemmas *) |
131 form of eqvt lemmas *) |
130 fun prepare_goal params_no pi pred = |
132 fun prepare_goal pi pred = |
131 let |
133 let |
132 val (c, xs) = strip_comb pred; |
134 val (c, xs) = strip_comb pred; |
133 val (xs1, xs2) = chop params_no xs |
|
134 in |
135 in |
135 HOLogic.mk_imp (pred, list_comb (c, xs1 @ map (mk_perm pi) xs2)) |
136 HOLogic.mk_imp (pred, list_comb (c, map (mk_perm pi) xs)) |
136 end |
137 end |
137 |
138 |
138 (* stores thm under name.eqvt and adds [eqvt]-attribute *) |
139 (* stores thm under name.eqvt and adds [eqvt]-attribute *) |
139 fun note_named_thm (name, thm) ctxt = |
140 fun note_named_thm (name, thm) ctxt = |
140 let |
141 let |
143 val attr = Attrib.internal (K eqvt_add) |
144 val attr = Attrib.internal (K eqvt_add) |
144 in |
145 in |
145 Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
146 Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
146 end |
147 end |
147 |
148 |
148 fun equivariance pred_name ctxt = |
149 fun equivariance pred_trms raw_induct intrs ctxt = |
149 let |
150 let |
150 val thy = ProofContext.theory_of ctxt |
151 val pred_names = map (fst o dest_Const) pred_trms |
151 val ({names, ...}, {raw_induct, intrs, ...}) = |
152 val raw_induct' = atomize_induct ctxt raw_induct |
152 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
153 val intrs' = map atomize_intr intrs |
153 val raw_induct = atomize_induct ctxt raw_induct |
|
154 val intros = map atomize_intr intrs |
|
155 val params_no = length (Inductive.params_of raw_induct) |
|
156 val (([raw_concl], [raw_pi]), ctxt') = |
154 val (([raw_concl], [raw_pi]), ctxt') = |
157 ctxt |
155 ctxt |
158 |> Variable.import_terms false [concl_of raw_induct] |
156 |> Variable.import_terms false [concl_of raw_induct'] |
159 ||>> Variable.variant_fixes ["p"] |
157 ||>> Variable.variant_fixes ["p"] |
160 val pi = Free (raw_pi, @{typ perm}) |
158 val pi = Free (raw_pi, @{typ perm}) |
161 val preds = map (fst o HOLogic.dest_imp) |
159 val preds = map (fst o HOLogic.dest_imp) |
162 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
160 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
163 val goal = HOLogic.mk_Trueprop |
161 val goal = HOLogic.mk_Trueprop |
164 (foldr1 HOLogic.mk_conj (map (prepare_goal params_no pi) preds)) |
162 (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) |
165 val thms = Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] goal |
163 val thms = Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] goal |
166 (fn {context,...} => eqvt_rel_tac context names pi raw_induct intros 1) |
164 (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |
167 |> singleton (ProofContext.export ctxt' ctxt)) |
165 |> singleton (ProofContext.export ctxt' ctxt)) |
168 val thms' = map (fn th => zero_var_indexes (th RS mp)) thms |
166 val thms' = map (fn th => zero_var_indexes (th RS mp)) thms |
169 in |
167 in |
170 ctxt |> fold_map note_named_thm (names ~~ thms') |> snd |
168 ctxt |> fold_map note_named_thm (pred_names ~~ thms') |
171 end |
169 end |
172 |
170 |
|
171 fun equivariance_cmd pred_name ctxt = |
|
172 let |
|
173 val thy = ProofContext.theory_of ctxt |
|
174 val (_, {preds, raw_induct, intrs, ...}) = |
|
175 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
|
176 in |
|
177 equivariance preds raw_induct intrs ctxt |> snd |
|
178 end |
173 |
179 |
174 local structure P = OuterParse and K = OuterKeyword in |
180 local structure P = OuterParse and K = OuterKeyword in |
175 |
181 |
176 val _ = |
182 val _ = |
177 OuterSyntax.local_theory "equivariance" |
183 OuterSyntax.local_theory "equivariance" |
178 "Proves equivariance for inductive predicate involving nominal datatypes." |
184 "Proves equivariance for inductive predicate involving nominal datatypes." |
179 K.thy_decl (P.xname >> equivariance); |
185 K.thy_decl (P.xname >> equivariance_cmd); |
180 end; |
186 end; |
181 |
187 |
182 end (* structure *) |
188 end (* structure *) |