Email Gateway (Aug 18 2022 at 11:14): Email Gateway (Aug 18 2022 at 11:14):From: Michael Anthony Smith <m.a.smith72@btinternet.com>
I am a new user, just starting to experiment with Isabelle (and machine assisted theorem proving).
I expected to be able to evaluate the contents of an "inbuilt set" in a similar manner to that of the "inbuilt list". However, when I issue the command
value "{}::(int set)"
I get the following error/warning message
*** Unable to generate code for term:
*** {x. False}
*** required by:
*** {}, <Top>
*** At command "value".
Any ideas?
Anthony.
PS: I was trying to validate some set functions that I had written, by evaluating concrete examples. Eventually, I discovered that I could not even evaluate the empty set.
PPS: Example Proof Script - illustrating above issue
theory MyTheory
imports Main
begin
value "3::int"
lemma "{a,b} \<union> {c,d} = {a,b,c,d}"
by blast
lemma "{} = {}"
by blast
value "[]::(int list)" -- "Everything works up to and incl. this line"
value "{}::(int set)" -- "Unable to generate code for this line!"
end
Email Gateway (Aug 18 2022 at 11:14):From: Tobias Nipkow <nipkow@in.tum.de>
A priory, sets are not computable because they could be infinite or
involve comprehensions. But if you also import Executable_Set,
operations like {}, union etc, but not comprehensions, become executable.
Tobias
Michael Anthony Smith wrote:
Email Gateway (Aug 18 2022 at 11:14):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Michael,
you can import theory "Executable_Set" in the header of your theory
file, this will make an implementation of finite sets available for "value".
Hope this helps
Florian
signature.asc
Last updated: May 03 2024 at 12:27 UTC