://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20091112/66863895/attachment.htm
If you do these things, you put an end to all Isabelle logics other
than Isabelle/HOL. Remember, an object logic does not need to possess
an equality symbol or even an implication symbol.
Having just translated some lengthy, incomprehensible HOL proofs into
Isabelle, I appreciate more than
On Wed, 11 Nov 2009, Brian Huffman wrote:
On Wed, Nov 11, 2009 at 1:46 PM, Alexander Krauss krauss at in.tum.de wrote:
in essence, ext and subst etc. are the real axioms, and eq_reflection
is an admissible rule which exists for technical reasons, but not a
first-class citizen.
So
Brian Huffman wrote:
On Thu, Nov 12, 2009 at 4:52 AM, Makarius makarius at sketis.net wrote:
Anyway, can you still derive iff from a more conventional classical rule
without equality?
I just had a go at this, and I don't think it's possible.
Using the classical axiom P | ~ P, the proof
On Thu, Nov 12, 2009 at 1:12 AM, Lawrence Paulson lp15 at cam.ac.uk wrote:
If you do these things, you put an end to all Isabelle logics other than
Isabelle/HOL. Remember, an object logic does not need to possess an equality
symbol or even an implication symbol.
OK, good point. All the
Makarius wrote:
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
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
