equal
deleted
inserted
replaced
232 proc = cancel_int_nat_simproc, identifier = [] }] |
232 proc = cancel_int_nat_simproc, identifier = [] }] |
233 |
233 |
234 fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss) |
234 fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss) |
235 |
235 |
236 val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat})) |
236 val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat})) |
|
237 val uses_nat_int = |
|
238 Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}]) |
237 in |
239 in |
238 fun nat_as_int ctxt thms = |
240 fun nat_as_int ctxt thms = |
239 let |
241 let |
240 fun norm thm uses_nat = |
242 fun norm thm = thm |
241 if not (uses_nat_type (Thm.prop_of thm)) then (thm, uses_nat) |
243 |> uses_nat_type (Thm.prop_of thm) ? Conv.fconv_rule (conv ctxt) |
242 else (Conv.fconv_rule (conv ctxt) thm, true) |
244 val thms' = map norm thms |
243 val (thms', uses_nat) = fold_map norm thms false |
245 in |
244 in if uses_nat then nat_embedding @ thms' else thms' end |
246 if exists (uses_nat_int o Thm.prop_of) thms' then nat_embedding @ thms' |
|
247 else thms' |
|
248 end |
245 end |
249 end |
246 |
250 |
247 |
251 |
248 (* include additional rules *) |
252 (* include additional rules *) |
249 |
253 |