equal
deleted
inserted
replaced
167 end; |
167 end; |
168 |
168 |
169 fun eqn_suc_preproc thy ths = |
169 fun eqn_suc_preproc thy ths = |
170 let |
170 let |
171 val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of; |
171 val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of; |
172 fun contains_suc t = member (op =) (OldTerm.term_consts t) @{const_name Suc}; |
172 val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc}); |
173 in |
173 in |
174 if forall (can dest) ths andalso |
174 if forall (can dest) ths andalso |
175 exists (contains_suc o dest) ths |
175 exists (contains_suc o dest) ths |
176 then remove_suc thy ths else ths |
176 then remove_suc thy ths else ths |
177 end; |
177 end; |
209 fun clause_suc_preproc thy ths = |
209 fun clause_suc_preproc thy ths = |
210 let |
210 let |
211 val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop |
211 val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop |
212 in |
212 in |
213 if forall (can (dest o concl_of)) ths andalso |
213 if forall (can (dest o concl_of)) ths andalso |
214 exists (fn th => member (op =) (foldr OldTerm.add_term_consts |
214 exists (fn th => exists (exists_Const (fn (c, _) => c = @{const_name Suc})) |
215 [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths |
215 (map_filter (try dest) (concl_of th :: prems_of th))) ths |
216 then remove_suc_clause thy ths else ths |
216 then remove_suc_clause thy ths else ths |
217 end; |
217 end; |
218 |
218 |
219 fun lift f thy eqns1 = |
219 fun lift f thy eqns1 = |
220 let |
220 let |