Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to declare constants before datatype? (in ...


view this post on Zulip Email Gateway (Aug 23 2022 at 08:42):

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

view this post on Zulip Email Gateway (Aug 23 2022 at 08:43):

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