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



But then, looking at the revised version, the problem still seems to be caused by the language.
The first line ("consts" â) seems to be a declaration, and the third line ("defs" â) a definition.
Declarations like this allow the declared constant to practically behave like a variable, since the constant can be specified (defined) much later.

In Q0/R0 there are no such declarations.
If one would try to express the same in the language of R0, only one possibility would be left.
The definition ("defs" â) could not be placed first, since it requires tau, which would be introduced by the latter type definition ("typedef" â) not available at the beginning.
Hence first type tau has to be defined (being a mere abbreviation) on the basis of a variable "c" as:
	tau := [\x:bool  .  x=T \/ x=c:bool]
Proving tau_T (i.e., T is element of tau; '_' denotes lambda application) then makes tau a type (being non-empty).
Finally,
	c = ~(AL x,y:tau  .  x=y)
could be introduced as a hypothesis. Since it leads to a contradiction, it is shown to be false (hence, c != ~(AL x,y:tau  .  x=y) ), which is the desired result.
In summary, the solution would be not allowing declarations in the mathematical language, but only definitions, like in Q0/R0.

Concerning the question of definitions, they shouldn't be part of the kernel, since non-logical axioms should be avoided as discussed in section 3 at
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00069.html
Also, implementing definitions within the logical core contradicts to the LCF philosophy of a small trusted kernel.
For this reason, definitions in R0 are mere abbreviations located outside of the logical kernel.
They also can be removed at any time (and re-introduced again) without modifying the theorems already obtained.

Ken Kubota


> Am 21.08.2016 um 21:17 schrieb OndÅej KunÄar <kuncar at in.tum.de>:
> 
> On 08/21/2016 07:35 PM, Ken Kubota wrote:
>> Dear Andrei,
>> 
>> Thank you for the quick answer, and also thanks to Larry Paulson and Makarius Wenzel.
>> 
>> I had read the abbreviated notation with the forall quantifier too quickly, but still the third restriction specified at
>>        http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf (p. 33) or at [Gordon/Melham, 1993, p. 220].
>> seems to be violated, as the type variable sigma occurs in the definiens, but not in (the type of) the definiendum.
> 
> That's a typo, that type should be tau, the type that was defined on the previous line. I've already uploaded an updated version of the draft.
> 
> Btw, we usually use alpha, beta, gamma for type variables, not sigma. But this is not mentioned until page 7.
> 
> Ondrej

____________________

Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100





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