[isabelle-dev] Isabelle/HOL axiom ext is redundant
makarius at sketis.net
Thu Nov 12 21:07:28 CET 2009
On Thu, 12 Nov 2009, Brian Huffman wrote:
> On Thu, Nov 12, 2009 at 1:12 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>> Having just translated some lengthy, incomprehensible HOL proofs into
>> Isabelle, I appreciate more than ever the distinction between the meta-
>> and object- levels. HOL proofs are cluttered with extra steps to
>> manipulate implications because HOL has no other way to express the
>> dependence of a fact upon conditions.
> Right, having two kinds of implication (--> and ==>) is convenient
> because (==>) is used to encode subgoals with premises in apply-style
> Isabelle proofs. But this justification for having two implications is
> completely separate from the one you mentioned above, isn't it? With
> declarative Isar proofs, I don't think the distinction between --> and
> ==> is nearly as important, because users don't see so many subgoals
> encoded with (==>). HOL's problems with manipulating implications would
> probably be helped by having declarative Isar-style proofs too.
Isar depends a lot on Larry's rule calculus !! ==> and in fact makes it
really shine. On the other hand, less of this is visible in the text,
because native structured proof elements take over -- yet another layer on
top of all that. Thus Isar is a bit like a rich language like ML, where
raw lambda abstractions are relatively rare, but notbody would think of
removing the lambda.
Plain old HOL will have a hard time imitating Isar without Pure ND rules.
One would either have to reinvent it, or rethink the whole thing from the
Again: look at example of Isar calculations, to see where the rule
framework of Pure comes into place.
More information about the isabelle-dev