Email Gateway (Aug 23 2022 at 09:15): Email Gateway (Aug 23 2022 at 09:15):From: Christopher Hoskin <christopher.hoskin@gmail.com>
Isabelle accepts:
definition test :: "nat ⇒ nat set"
where "test y == {x. x>y}"
and I presume this to mean that "test 3" will be all the natural
numbers strictly greater than 3.
However, if I write
definition testb :: "nat ⇒ (nat set) set"
where "testb z = {(test y). (y>z)}"
meaning the set of sets of natural numbers greater than y for each
natural number greater than z, then Isabelle says
Inner syntax error⌂
Failed to parse prop
How should something like this be formulated.
<Digression>
Despite several years experience with both mathematics and various
programming languages, I find the Isabelle syntax quite opaque. Most
of the literature on the subject appears to be written for people with
a deep background in computer science or mathematical logic rather
than the "working mathematician". The only article I've found that's
integigable to someone like me is Grechuk's "Isabelle Primer for
Mathematicians". Slightly out of date now, but invaluable.
I'd be curious to know if there were other Mathematicians who'd
managed to self-tutor themselves in Isabelle, and if so, how they went
about it. Are there any plans to try to make Isabelle more accessible
to a wider mathematical community?
</Digression>
Christopher
Email Gateway (Aug 23 2022 at 09:15):From: marco caminati via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Il mercoledì 24 giugno 2020, 16:47:00 GMT+1, Christopher Hoskin <christopher.hoskin@gmail.com> ha scritto:
How should something like this be formulated.
Hello Christopher,
you could try
testb z = {(test y)| y. (y>z)}
This has to do with how the corresponding syntaxes are defined in src/HOL/Set.thy and yes, it can be confusing.
Kind regards,
Marco Caminati
Email Gateway (Aug 23 2022 at 09:15):From: Christopher Hoskin <christopher.hoskin@gmail.com>
Dear Marco,
Thank you - that seems to work (at least Isabelle accepts the
definition without a syntax error).
Best wishes,
Christopher
Last updated: Apr 23 2024 at 20:15 UTC