equal
deleted
inserted
replaced
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 -> (string * thm list) list * local_theory |
13 val equivariance: 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 |
140 fun note_named_thm (name, thm) ctxt = |
140 fun note_named_thm (name, thm) ctxt = |
141 let |
141 let |
142 val thm_name = Binding.qualified_name |
142 val thm_name = Binding.qualified_name |
143 (Long_Name.qualify (Long_Name.base_name name) "eqvt") |
143 (Long_Name.qualify (Long_Name.base_name name) "eqvt") |
144 val attr = Attrib.internal (K eqvt_add) |
144 val attr = Attrib.internal (K eqvt_add) |
|
145 val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
145 in |
146 in |
146 Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
147 (thm', ctxt') |
147 end |
148 end |
148 |
149 |
149 fun equivariance pred_trms raw_induct intrs ctxt = |
150 fun equivariance pred_trms raw_induct intrs ctxt = |
150 let |
151 let |
151 val pred_names = map (fst o dest_Const) pred_trms |
152 val pred_names = map (fst o dest_Const) pred_trms |