Brian Huffman wrote:
I would consider this as an implementation detail, and not worry about
it any further.
Tools that operate on the level of proof terms can then eliminate
eq_reflection, as was pointed out first by Stefan Berghofer some years ago,
IIRC. (I also learned from him that it is
Thanks for this interesting and enlightening discussion.
I have always had an intuitive appreciation of the meta-logic in
Isabelle. I find it clarifies the both the modeling and proof
activities profoundly.
I would be interested also in a discussion of an important place where
the
Makarius wrote:
On Thu, 12 Nov 2009, Lucas Dixon wrote:
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
This sort of discussion is analogous to suggesting that we get rid of
and/or/not/implies and write all formulas using the Scheffer stroke
(NAND), or that Gentzen's sequent calculus should be replaced by the
much simpler Hilbert system. It can be done, but who would want to do
it?
Larry
I was really wondering what the principle was that makes -- and ALL
fail (or be inappropriately convoluted) than using the meta-level
connectives: is there a small example that illustrates it?
My own understanding was that the meta-level of Isabelle, and the use of
it by Isar, facilitated the
On Fri, 13 Nov 2009, Lucas Dixon wrote:
I was really wondering what the principle was that makes -- and ALL
fail (or be inappropriately convoluted) than using the meta-level
connectives: is there a small example that illustrates it?
My own understanding was that the meta-level of Isabelle,
On Thu, Nov 12, 2009 at 2:06 PM, Andreas Schropp schropp at in.tum.de wrote:
In a sense, eq_reflection is a meta-thereom, but Pure is not a meta-logic,
so it cannot be proven within the system. ?Thus we need to add it as an
axiom.
But we can prove all instances of the eq_reflection
Anyway, since eq_reflection actually *is* an axiom, and (=) actually
*does* mean the same thing as (==), then I really don't see any reason
why we need to have both (or separate bool and prop types, for that
matter). I don't know of any other HOL provers that do.
Even if we got rid of the
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
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
Hello all,
This morning I was looking at the following comment from HOL.thy:
ext:(!!x::'a. (f x ::'b) = g x) == (%x. f x) = (%x. g x)
-- {*Extensionality is built into the meta-logic, and this rule expresses
a related property. It is an eta-expanded version of the
In the translation to ZF which Andy and I am developing, such
strange proofs actually caused some weird problems at some point.
This sounds interesting :-) Is there more information on this
translation available?
Best,
Steven
PS: For those of you who a) speak German b) play Skat c) have
15 matches
Mail list logo
