159 let val (ths1, ths2) = split_list thps |
159 let val (ths1, ths2) = split_list thps |
160 in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end |
160 in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end |
161 end |
161 end |
162 in get_first mk_thms eqs end; |
162 in get_first mk_thms eqs end; |
163 |
163 |
164 fun eqn_suc_preproc thy thms = |
164 fun eqn_suc_base_preproc thy thms = |
165 let |
165 let |
166 val dest = fst o Logic.dest_equals o prop_of; |
166 val dest = fst o Logic.dest_equals o prop_of; |
167 val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc}); |
167 val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc}); |
168 in |
168 in |
169 if forall (can dest) thms andalso exists (contains_suc o dest) thms |
169 if forall (can dest) thms andalso exists (contains_suc o dest) thms |
170 then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes |
170 then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes |
171 else NONE |
171 else NONE |
172 end; |
172 end; |
173 |
173 |
174 val eqn_suc_preproc1 = Code_Preproc.simple_functrans eqn_suc_preproc; |
174 val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc; |
175 |
|
176 fun eqn_suc_preproc2 thy thms = eqn_suc_preproc thy thms |
|
177 |> the_default thms; |
|
178 |
175 |
179 fun remove_suc_clause thy thms = |
176 fun remove_suc_clause thy thms = |
180 let |
177 let |
181 val vname = Name.variant (map fst |
178 val vname = Name.variant (map fst |
182 (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x"; |
179 (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x"; |
215 (map_filter (try dest) (concl_of th :: prems_of th))) ths |
212 (map_filter (try dest) (concl_of th :: prems_of th))) ths |
216 then remove_suc_clause thy ths else ths |
213 then remove_suc_clause thy ths else ths |
217 end; |
214 end; |
218 in |
215 in |
219 |
216 |
220 Codegen.add_preprocessor eqn_suc_preproc2 |
217 Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc) |
221 #> Codegen.add_preprocessor clause_suc_preproc |
218 #> Codegen.add_preprocessor clause_suc_preproc |
222 #> Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc1) |
|
223 |
219 |
224 end; |
220 end; |
225 *} |
221 *} |
226 (*>*) |
222 (*>*) |
227 |
223 |