[isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu

Dear Isabelle Developers,

Concerning the type definitions in Isabelle and the article by OndÅej KunÄar and Andrei Popescu, I have some questions.

1. Which restriction was introduced in Isabelle (2016) in order to avoid the inconsistency of earlier versions revealed by KunÄar/Popescu? See
	http://www21.in.tum.de/~kuncar/kuncar-popescu-jar2016.pdf (p. 3)
The definition of the constant c contains a free variable y.
Constant definitions in Gordon's original HOL do not allow free variables, but only "a closed term" [Gordon/Melham, 1993, p. 220; or
	http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf (p. 33)].

2. Are all types still constructed via the "typedef" mechanism?
The following formulation allows two interpretations: a mechanism on top of "typedef",
or a new mechanism at the same (basic) level as and in addition to "typedef":
"In the postâIsabelle 2012 development version, we have converted the numeric types int, rat, and real to use Lifting and Transfer. (Previously they were constructed as quotients with typedef, in the style of Paulson [6].)"
	http://www21.in.tum.de/~kuncar/documents/huffman-kuncar-itp2012.pdf (p. 17)

3. The main questions is, whether in Isabelle still all new types are (besides being tested for non-emptiness)
introduced with an axiom stating a mapping, like in Gordon's original HOL,
where for each new type an axiom is asserted saying that the new type is isomorphic to the defined (sub)set, cf.
	http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf (p. 39).

Let me remark that the section "8.5.2 Defining New Types" in
	http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/tutorial.pdf (pp. 173 ff.)
explaining "typedef" is quite hidden.
It would be desirable to have it in a separate logic manual like in the HOL4 logic part linked above.

4. Why should "dependent types" be "to a large extent incompatible with the HOL philosophy of keeping all types non-empty" as claimed at
	http://www21.in.tum.de/~kuncar/kuncar-popescu-jar2016.pdf (p. 4)?
My R0 implementation is a dependent type theory, and there are no empty types in it.

Kind regards,

Ken Kubota


Ken Kubota
doi: 10.4444/100

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.