[isabelle-dev] Isabelle/HOL axiom ext is redundant

[Makarius]

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 
ground up.

Again: look at example of Isar calculations, to see where the rule 
framework of Pure comes into place.


 	Makarius