Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Recursive functions over non datatype input


view this post on Zulip 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

view this post on Zulip 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: Jul 15 2022 at 23:21 UTC