8 signature NOMINAL_EQVT = |
8 signature NOMINAL_EQVT = |
9 sig |
9 sig |
10 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 |
11 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 |
12 |
13 val equivariance: term list -> thm -> thm list -> Proof.context -> thm list * local_theory |
13 val equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory |
14 val equivariance_cmd: string -> Proof.context -> local_theory |
14 val equivariance_cmd: string -> Proof.context -> local_theory |
15 end |
15 end |
16 |
16 |
17 structure Nominal_Eqvt : NOMINAL_EQVT = |
17 structure Nominal_Eqvt : NOMINAL_EQVT = |
18 struct |
18 struct |
145 val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
145 val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
146 in |
146 in |
147 (thm', ctxt') |
147 (thm', ctxt') |
148 end |
148 end |
149 |
149 |
150 fun equivariance pred_trms raw_induct intrs ctxt = |
150 fun equivariance note_flag pred_trms raw_induct intrs ctxt = |
151 let |
151 let |
152 val is_already_eqvt = |
152 val is_already_eqvt = |
153 filter (is_eqvt ctxt) pred_trms |
153 filter (is_eqvt ctxt) pred_trms |
154 |> map (Syntax.string_of_term ctxt) |
154 |> map (Syntax.string_of_term ctxt) |
155 val _ = if null is_already_eqvt then () |
155 val _ = if null is_already_eqvt then () |
170 val thms = Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] goal |
170 val thms = Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] goal |
171 (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |
171 (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |
172 |> singleton (ProofContext.export ctxt' ctxt)) |
172 |> singleton (ProofContext.export ctxt' ctxt)) |
173 val thms' = map (fn th => zero_var_indexes (th RS mp)) thms |
173 val thms' = map (fn th => zero_var_indexes (th RS mp)) thms |
174 in |
174 in |
175 ctxt |> fold_map note_named_thm (pred_names ~~ thms') |
175 if note_flag |
|
176 then ctxt |> fold_map note_named_thm (pred_names ~~ thms') |
|
177 else (thms', ctxt) |
176 end |
178 end |
177 |
179 |
178 fun equivariance_cmd pred_name ctxt = |
180 fun equivariance_cmd pred_name ctxt = |
179 let |
181 let |
180 val thy = ProofContext.theory_of ctxt |
182 val thy = ProofContext.theory_of ctxt |
181 val (_, {preds, raw_induct, intrs, ...}) = |
183 val (_, {preds, raw_induct, intrs, ...}) = |
182 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
184 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
183 in |
185 in |
184 equivariance preds raw_induct intrs ctxt |> snd |
186 equivariance true preds raw_induct intrs ctxt |> snd |
185 end |
187 end |
186 |
188 |
187 local structure P = Parse and K = Keyword in |
189 local structure P = Parse and K = Keyword in |
188 |
190 |
189 val _ = |
191 val _ = |