[isabelle-dev] Isabelle/HOL axiom ext is redundant
makarius at sketis.net
Thu Nov 12 23:15:05 CET 2009
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
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.).
More information about the isabelle-dev