Re: [isabelle] Definition in (and of) Isabelle/HOL



Makarius,

Thanks again for that. My current plan for the paper is to not to exclude Isabelle/HOL, but to discuss it alongside the other implementations. Perhaps you could let me know if you there is anything wrong with the following outline of my understanding, based on your reply below.

Isabelle/HOl was first implemented in the early ‘90s after the unsoundness problem with type variables appearing on the right-hand side of a definition, c = t, but not on the left-hand side was known, so it never suffered from that problem. Its internal mechanisms for doing definitions have involved over the years, but the current position for type definitions is quite like HOL Light when you look right under the covers, i.e., new_specification is emulated using an equational definition and Hilbert choice. However, Isabelle has information-hiding mechanisms that are more powerful than HOL Light’s, so this is not so problematic in practice. I think it is also fair to say that locales in Isabelle/HOL provide an alternative abstraction mechanism that can be used as a replacement for the kind of abstraction offered by new_specification, in that it lets you identify the abstract properties needed to carry out a given set of proofs without requiring you to be explicit about the actual types and constants that satisfy those properties. Locales (or a slight variant of them) would perhaps give you a nice way of implementing the generalised new_specification proposed in my paper.

Do you do anything to avoid the potential problem whereby two calls of new_specification with the same predicate will result in provably equal constants if you implement new_specification naively with Hilbert choice. E.g., ?x.1 < x < 10 used to define c and d?  This is addressed in HOL Light along the following lines: it defines a function on the natural numbers such that 1 < x(n) < 10 for all n, and then defines c = x(42) and d = x(43), assuming that c is the 42nd constant that HOL Light has been asked to define.

What you say about type definitions in Isabelle/HOL sounds interesting and is reminiscent of what we do in ProofPower to allow users to defer consistency proofs.

Regards,

Rob.

On 31 Mar 2014, at 16:00, Makarius <makarius at sketis.net> wrote:

> On Sat, 29 Mar 2014, Rob Arthan wrote:
> 
>> I am trying to address a comment to this short paper proposing an improved method of constant specification in the non-Isabelle implementations of HOL: http://www.lemma-one.com/papers/hcddr.pdf. The comment is asking me to say more about Isabelle/HOL. My reason for excluding Isabelle/HOL when I first wrote the paper, was that I believed, based on hearsay and guesswork, that all the mechanisms for defining constants in Isabelle/HOL are founded on a primitive that is part of the logical framework and that supports definition via (non-recursive) equations.
> 
> There is a long story behind that, started by Larry some decades ago, but it continously changed according to new requirements.
> 
> The original Pure logical framework by Larry merely had axiomatic specifications, which were introduced as 'types', 'consts', 'rules' (similar to LF).
> 
> In the mid-1990-ies we added a slightly restricted version of 'rules' that was called 'defs', with a few local checks, but no global guarantees of the well-formedness of the theory.
> 
> When I introduced the Isar theory syntax in 1998/1999, I renamed 'rules' to 'axioms'.  Later the 'defs' became a bit more serious, with some non-local checks, to track dependencies of overloaded and non-overloaded constants more explicitly.  This was substantially refined in 2005, and 2007/2008.
> 
> Later the 'axioms' became 'axiomatization', with some explicit dependency tracking of which constants are supposed to be axiomatized.  The 'defs' were also de-emphasized in favour of the Local_Theory.define abstraction, which merely uses a restricted 'defs' form at the bottom: just c == t for closed terms, and no longer any pre-conditions that were still allowed in 'defs'.
> 
> 
> Isabelle/HOL relies on constant definitions of Isabelle/Pure in the above form, but invents its own axiom schemes, notably 'typedef' (which is not quite definitional as we all know).
> 
> Our current version of typedef is notable, since it does not depend on a proven non-emptiness theorem in advance, it merely needs that to turn a conditional axiomatization into an actual one.  That formal trick makes the constant definitions independent on the typedefs, because the "meaning" of consts is not needed to introduce new typedefs.
> 
> 
>> So anything like the HOL4 new_specification would be implemented under the covers using the Hilbert choice function. Is that correct?
> 
> There is indeed an Isabelle/HOL emulation of HOL4 new_specification called 'specification', which uses Hilbert choice + definition.  It has an alternative axiomatic personality without the Hilbert Choice, but that was actually never used and is already deleted for the coming Isabelle release.
> 
> In Isabelle2013-2 documentation http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/isar-ref.pdf there is still a description of ax_specification, but its worries about exposing the definition to the user are actually obsolete: with Local_Theory.define the kernel produces a precise definition c == @x. ... at the very bottom, but that is only for foundational purposes.  After the next renovation of the 'specification' element, it will just refrain from exposing that definition to the normal fact name space, and the user will have a hard time to come across it accidentally.
> 
> This is analogous to something that is "private" in Java.  Normally inaccesible and not to be worried about, but with some tricks you can get it from the low-level JVM environment, because it is there for foundational purposes
> 
> This separation of Local_Theory primitives vs. theory foundations at the bottom circumvents some old problems, although it introduces new complexity to be dealt with.
> 
> 
> 	Makarius
> 
> 




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