3 Author: Brian Huffman |
3 Author: Brian Huffman |
4 *) |
4 *) |
5 |
5 |
6 signature NOMINAL_PERMEQ = |
6 signature NOMINAL_PERMEQ = |
7 sig |
7 sig |
|
8 val eqvt_rule: Proof.context -> thm list -> string list -> thm -> thm |
|
9 val eqvt_strict_rule: Proof.context -> thm list -> string list -> thm -> thm |
|
10 |
8 val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic |
11 val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic |
9 val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic |
12 val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic |
10 |
13 |
11 val perm_simp_meth: thm list * string list -> Proof.context -> Method.method |
14 val perm_simp_meth: thm list * string list -> Proof.context -> Method.method |
12 val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method |
15 val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method |
114 in |
117 in |
115 Conv.all_conv ctrm |
118 Conv.all_conv ctrm |
116 end |
119 end |
117 |
120 |
118 (* main conversion *) |
121 (* main conversion *) |
119 fun eqvt_conv ctxt strict_flag user_thms excluded ctrm = |
122 fun main_eqvt_conv ctxt strict_flag user_thms excluded ctrm = |
120 let |
123 let |
121 val first_conv_wrapper = |
124 val first_conv_wrapper = |
122 if trace_enabled ctxt |
125 if trace_enabled ctxt |
123 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
126 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
124 else Conv.first_conv |
127 else Conv.first_conv |
135 ] ctrm |
138 ] ctrm |
136 end |
139 end |
137 |
140 |
138 (* the eqvt-tactics first eta-normalise goals in |
141 (* the eqvt-tactics first eta-normalise goals in |
139 order to avoid problems with inductions in the |
142 order to avoid problems with inductions in the |
140 equivaraince command. *) |
143 equivariance command. *) |
141 |
144 |
142 (* raises an error if some permutations cannot be eliminated *) |
145 (* raises an error if some permutations cannot be eliminated *) |
143 fun eqvt_strict_tac ctxt user_thms excluded = |
146 fun eqvt_strict_conv ctxt user_thms excluded = |
144 CONVERSION (Conv.top_conv |
147 Conv.top_conv |
145 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt) |
148 (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt true user_thms excluded)) ctxt |
146 |
149 |
147 (* prints a warning message if some permutations cannot be eliminated *) |
150 (* prints a warning message if some permutations cannot be eliminated *) |
|
151 fun eqvt_conv ctxt user_thms excluded = |
|
152 Conv.top_conv |
|
153 (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt false user_thms excluded)) ctxt |
|
154 |
|
155 |
|
156 (* thms rewriters *) |
|
157 fun eqvt_strict_rule ctxt user_thms excluded = |
|
158 Conv.fconv_rule (eqvt_strict_conv ctxt user_thms excluded) |
|
159 |
|
160 fun eqvt_rule ctxt user_thms excluded = |
|
161 Conv.fconv_rule (eqvt_conv ctxt user_thms excluded) |
|
162 |
|
163 (* tactics *) |
|
164 fun eqvt_strict_tac ctxt user_thms excluded = |
|
165 CONVERSION (eqvt_strict_conv ctxt user_thms excluded) |
|
166 |
148 fun eqvt_tac ctxt user_thms excluded = |
167 fun eqvt_tac ctxt user_thms excluded = |
149 CONVERSION (Conv.top_conv |
168 CONVERSION (eqvt_conv ctxt user_thms excluded) |
150 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt) |
|
151 |
169 |
152 (* setup of the configuration value *) |
170 (* setup of the configuration value *) |
153 val setup = |
171 val setup = |
154 trace_eqvt_setup |
172 trace_eqvt_setup |
155 |
173 |