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: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory |
13 val raw_equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory |
|
14 val equivariance: string -> Proof.context -> (thm list * local_theory) |
14 val equivariance_cmd: string -> Proof.context -> local_theory |
15 val equivariance_cmd: string -> Proof.context -> local_theory |
15 end |
16 end |
16 |
17 |
17 structure Nominal_Eqvt : NOMINAL_EQVT = |
18 structure Nominal_Eqvt : NOMINAL_EQVT = |
18 struct |
19 struct |
83 val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
84 val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
84 in |
85 in |
85 (thm', ctxt') |
86 (thm', ctxt') |
86 end |
87 end |
87 |
88 |
88 fun equivariance note_flag pred_trms raw_induct intrs ctxt = |
89 fun get_name (Const (a, _)) = a |
|
90 | get_name (Free (a, _)) = a |
|
91 |
|
92 fun raw_equivariance note_flag pred_trms raw_induct intrs ctxt = |
89 let |
93 let |
90 val is_already_eqvt = |
94 val is_already_eqvt = |
91 filter (is_eqvt ctxt) pred_trms |
95 filter (is_eqvt ctxt) pred_trms |
92 |> map (Syntax.string_of_term ctxt) |
96 |> map (Syntax.string_of_term ctxt) |
93 val _ = if null is_already_eqvt then () |
97 val _ = if null is_already_eqvt then () |
94 else error ("Already equivariant: " ^ commas is_already_eqvt) |
98 else error ("Already equivariant: " ^ commas is_already_eqvt) |
95 |
99 |
96 val pred_names = map (fst o dest_Const) pred_trms |
100 val pred_names = map get_name pred_trms |
97 val raw_induct' = atomize_induct ctxt raw_induct |
101 val raw_induct' = atomize_induct ctxt raw_induct |
98 val intrs' = map atomize_intr intrs |
102 val intrs' = map atomize_intr intrs |
99 |
103 |
100 val (([raw_concl], [raw_pi]), ctxt') = |
104 val (([raw_concl], [raw_pi]), ctxt') = |
101 ctxt |
105 ctxt |
119 if note_flag |
123 if note_flag |
120 then fold_map note_named_thm (pred_names ~~ thms) ctxt |
124 then fold_map note_named_thm (pred_names ~~ thms) ctxt |
121 else (thms, ctxt) |
125 else (thms, ctxt) |
122 end |
126 end |
123 |
127 |
|
128 fun equivariance pred_name ctxt = |
|
129 let |
|
130 val thy = ProofContext.theory_of ctxt |
|
131 val (_, {preds, raw_induct, intrs, ...}) = |
|
132 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
|
133 in |
|
134 raw_equivariance false preds raw_induct intrs ctxt |
|
135 end |
|
136 |
124 fun equivariance_cmd pred_name ctxt = |
137 fun equivariance_cmd pred_name ctxt = |
125 let |
138 let |
126 val thy = ProofContext.theory_of ctxt |
139 val thy = ProofContext.theory_of ctxt |
127 val (_, {preds, raw_induct, intrs, ...}) = |
140 val (_, {preds, raw_induct, intrs, ...}) = |
128 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
141 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
129 in |
142 in |
130 equivariance true preds raw_induct intrs ctxt |> snd |
143 raw_equivariance true preds raw_induct intrs ctxt |> snd |
131 end |
144 end |
132 |
145 |
133 local structure P = Parse and K = Keyword in |
146 local structure P = Parse and K = Keyword in |
134 |
147 |
135 val _ = |
148 val _ = |