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

[Makarius]

On Thu, 12 Nov 2009, Lucas Dixon wrote:

>> 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.
>
> this is interesting to me: I don't understand why you couldn't just use 
> the --> and ALL of HOL to do exactly what ==> and !! are doing? Isn't 
> that what SPL by Zammit did? The dependencies (in Isabelle, stored in 
> hyps) can all be recorded outside the logic (as they are in SPL). If 
> done correctly, like Isar, the final theorems can be re-constructed 
> easily enough from the recorded structure of the proof text... or so it 
> seems to me. :)

The hyps are not involved at this point.  This is about what I've called 
"the visible part of ND reasoning" before.  The nice thing of explicitly 
outlined ND rules via ==> and !! is that the system knows how to combine 
them from their shape.  It is not about "two versions" of certain 
connectives, but a ND rule calculus that is used together with a fully 
featured object-logic.

For example, Isar calculations (via 'also' and 'finally') work via a 
collection of "trans" rules declared in the library. The system merely 
applies them in canonical fashion, using the resolution principle in 
forward manner.  Thus the machinery can work with mixed =, <, <= etc. 
subsitution wrt. =, subsitution wrt. < and <= within a monotonic context. 
In the latter case, side conditions are accumulated and propagated 
monotonically through the chain of reasoning -- the final proof after 
'finally' can solve them.  All of this is done by Larry's Pure calculus, 
with very little intervention from my side (Pure/Isar/calculation.ML is 
one of the smaller files.).


 	Makarius