How to study Isabelle/ZF?

[Victor Porton]

What documents I need to read to become acquainted with Isabelle/ZF?

I quickly (not in detail) read "Tutorial on Isabelle/HOL" (http://
isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf) but afterwards
found that it is specific with HOL and does not present ZF.

"Isabelle's Logics: FOL and ZF" (http://isabelle.in.tum.de/dist/
Isabelle/doc/logics-ZF.pdf) seems being not enough detailed about core
Isabelle/Isar telling almost only ZF-specific things.

So what to read? I want to get all features which may be needed for ZF
based theory development with Isabelle.

[Slawomir Kolodynski]

> What documents I need to read to become acquainted with
> Isabelle/ZF?

The fact of life is that there is no tutorial on writing Isabelle/ZF proofs in Isar. The best sources for study are Tutorial on Isar and Tutorial on Locales from Isabelle documentation page http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html, just skip everything that uses double colon (::) or talks about induction. And of course you can look at existing examples.

Slawekk

IsarMathLib (formalmath.org)
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)

[Victor Porton]

23.02.09, 01:01, "Slawomir Kolodynski" <skok...@yahoo.com>:

> > What documents I need to read to become acquainted with
> > Isabelle/ZF?
> The fact of life is that there is no tutorial on writing Isabelle/ZF proofs in Isar. The best sources for study are Tutorial on Isar and Tutorial on Locales from Isabelle documentation page http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html, just skip everything that uses double colon (::) or talks about induction. And of course you can look at existing examples.

But what if I want to use induction with ZF? AFAIK, the axiom of induction is provable for natural numbers represented as ordinals in ZF. What if I want to use this axiom (actually a theorem in ZF)?

[Victor Porton]

On Feb 23, 12:01 am, Slawomir Kolodynski <skoko...@yahoo.com> wrote:
> > What documents I need to read to become acquainted with
> > Isabelle/ZF?
>

> The fact of life is that there is no tutorial on writing Isabelle/ZF proofs in Isar. The best sources for study are Tutorial on Isar and Tutorial on Locales from Isabelle documentation pagehttp://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html, just skip everything that uses double colon (::) or talks about induction. And of course you can look at existing examples.

What will happen if I would indeed use :: in a ZF-based theory? Will
it be a compilation error?

[slawekk]

> >skip everything that uses double colon (::) or talks about induction.

These are just simple ways to recognize parts that are most likely
specific to HOL. You can of course do proofs by induction in ZF (see
lemma nat_induct at http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/Nat_ZF.html
or ind_on_nat in http://www.nongnu.org/isarmathlib/IsarMathLib/outline.pdf
).

As for "::" you can use it in Isabelle/ZF, but unlike in HOL you don't
have to. ZF uses only two types: "i" (set) and "o" (logical, true-
false). In ZF Isabelle is able to do full type inference from the
context and in my experience type specifications with :: are not
needed. An expert in Isabelle internals might be able to come up with
a counterexample though.

Slawekk

[Victor Porton]

23.02.09, 19:52, "slawekk" <skok...@yahoo.com>:

Is it possible to define new datatypes in Isabelle/ZF? Will it work smoothly?

[slawekk]

> Is it possible to define new datatypes in Isabelle/ZF? Will it work smoothly?

It is possible, see for example http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/Finite.html
.

However, if you need datatypes you would be probably better of with
some other foundation based on type theory (like HOL) rather than
(untyped) set theory. Isabelle/ZF is great for formalized mathematics
based on standard set theory. Datatypes, records, structs etc. can be
probably simulated, but do not belong here.