95 val b = ctyp_of_term t; |
95 val b = ctyp_of_term t; |
96 val ty_insts = map SOME [b, a] |
96 val ty_insts = map SOME [b, a] |
97 val term_insts = map SOME [p, f, x] |
97 val term_insts = map SOME [p, f, x] |
98 in |
98 in |
99 if has_bad_head bad_hds trm |
99 if has_bad_head bad_hds trm |
100 then Conv.no_conv ctrm |
100 then Conv.all_conv ctrm |
101 else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
101 else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
102 end |
102 end |
103 | _ => Conv.no_conv ctrm |
103 | _ => Conv.no_conv ctrm |
104 |
104 |
105 (* conversion for lambdas *) |
105 (* conversion for lambdas *) |
113 if a permutation on a constant or application cannot be analysed *) |
113 if a permutation on a constant or application cannot be analysed *) |
114 fun progress_info_conv ctxt strict_flag bad_hds ctrm = |
114 fun progress_info_conv ctxt strict_flag bad_hds ctrm = |
115 let |
115 let |
116 fun msg trm = |
116 fun msg trm = |
117 let |
117 let |
118 val hd = head_of trm |
118 val hd = head_of trm |
119 in |
119 in |
120 if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then () |
120 if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then () |
121 else (if strict_flag then error else warning) |
121 else (if strict_flag then error else warning) |
122 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
122 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
123 end |
123 end |
124 |
124 |
125 val _ = case (term_of ctrm) of |
125 val _ = case (term_of ctrm) of |
126 Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
126 Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
127 | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
127 | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
128 | _ => () |
128 | _ => () |
129 in |
129 in |
130 Conv.all_conv ctrm |
130 Conv.all_conv ctrm |
131 end |
131 end |
132 |
132 |
133 (* main conversion *) |
133 (* main conversion *) |
134 fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm = |
134 fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm = |
135 let |
135 let |
136 val first_conv_wrapper = |
136 val first_conv_wrapper = |
137 if trace_enabled ctxt |
137 if trace_enabled ctxt |
138 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
138 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
148 More_Conv.rewrs_conv post_thms, |
148 More_Conv.rewrs_conv post_thms, |
149 progress_info_conv ctxt strict_flag bad_hds |
149 progress_info_conv ctxt strict_flag bad_hds |
150 ] ctrm |
150 ] ctrm |
151 end |
151 end |
152 |
152 |
|
153 (* the eqvt-tactics first eta-normalise goals in |
|
154 order to avoid problems with inductions in the |
|
155 equivaraince command. *) |
|
156 |
153 (* raises an error if some permutations cannot be eliminated *) |
157 (* raises an error if some permutations cannot be eliminated *) |
154 fun eqvt_strict_tac ctxt user_thms bad_hds = |
158 fun eqvt_strict_tac ctxt user_thms bad_hds = |
155 CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true user_thms bad_hds) ctxt) |
159 CONVERSION (More_Conv.top_conv |
|
160 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms bad_hds)) ctxt) |
156 |
161 |
157 (* prints a warning message if some permutations cannot be eliminated *) |
162 (* prints a warning message if some permutations cannot be eliminated *) |
158 fun eqvt_tac ctxt user_thms bad_hds = |
163 fun eqvt_tac ctxt user_thms bad_hds = |
159 CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false user_thms bad_hds) ctxt) |
164 CONVERSION (More_Conv.top_conv |
|
165 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms bad_hds)) ctxt) |
160 |
166 |
161 (* setup of the configuration value *) |
167 (* setup of the configuration value *) |
162 val setup = |
168 val setup = |
163 trace_eqvt_setup |
169 trace_eqvt_setup |
164 |
170 |
167 |
173 |
168 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; |
174 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; |
169 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
175 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
170 (Scan.repeat (Args.const true))) [] |
176 (Scan.repeat (Args.const true))) [] |
171 |
177 |
172 val args_parser = |
178 val args_parser = add_thms_parser -- exclude_consts_parser |
173 add_thms_parser -- exclude_consts_parser || |
|
174 exclude_consts_parser -- add_thms_parser >> swap |
|
175 |
179 |
176 fun perm_simp_meth (thms, consts) ctxt = |
180 fun perm_simp_meth (thms, consts) ctxt = |
177 SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts)) |
181 SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts)) |
178 |
182 |
179 fun perm_strict_simp_meth (thms, consts) ctxt = |
183 fun perm_strict_simp_meth (thms, consts) ctxt = |