Email Gateway (Dec 21 2021 at 11:08): Email Gateway (Dec 21 2021 at 11:08):From: Leo Freitas <leo.freitas@newcastle.ac.uk>
Hello,
I am trying to find a scheme for certain recursive functions over specific structured (non-data) types. Namely, recursion over sets, integers, etc.
For example, sum over elements of a set of nat
function
sum :: "nat set ⇒ nat"
where
"sum {} = 0"
| "x ∉ s ⟹ sum ({x} ∪ s) = x + (sum s)"
This leads to more involved pattern/termination proofs than I was hoping for.
I wonder whether are there examples of recursive function definitions over such structured (non-data) types?
Best regards,
Leo
Email Gateway (Dec 21 2021 at 11:29):From: Tobias Nipkow <nipkow@in.tum.de>
Hi Leo,
Patter matching doesn't really work on non-free types. For integers, you can
just write your function as you would in any programming language, e.g. with
"-1" on the rhs. For sets see this thread:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2008-November/msg00024.html
Essentially: use Finite_Set.fold
You find some examples in HOL/Relation.thy.
Tobias
smime.p7s
Last updated: Jan 04 2025 at 20:18 UTC