From: Georgy Dunaev <georgedunaev@gmail.com>
Thanks for responses a lot! Just a quick question:
What if I try to declare some datatype, not in HOL, but if ZF?
theory Scratch imports ZF
begin
datatype simple = X1 | X2 | X3 | X4
end
That raises an error "Datatype set not previously declared as constant:
simple"
How can I do this in Isabelle? (declare "simple" to be a type constant)
( "typedecl simple" doesn't help in this particular problem, and the only
link that can be googled is
https://isabelle.in.tum.de/website-Isabelle2009/dist/library/ZF/datatype_package.ML.html
)
Yours sincerely,
Georgy Dunaev
From: Lawrence Paulson <lp15@cam.ac.uk>
If you want to use Isabelle/ZF, you should consult this (legacy) manual:
https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2019/doc/logics-ZF.pdf
For most people, Isabelle/HOL is a better choice with much more automation, in particular.
Note that in Isabelle/ZF, you do not introduce new types, ever. A “datatype” declaration actually introduces a set. Here is an example, from the manual mentioned above:
consts list :: "i=>i"
datatype "list(A)" = Nil | Cons ("a ∈ A", "l ∈ list(A)")
Larry Paulson
Last updated: Mar 28 2024 at 16:17 UTC