Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- From: Makarius <makarius at sketis.net>
- Date: Fri, 6 Jul 2012 14:19:10 +0200 (CEST)
- Cc: Gottfried Barrow <gottfried.barrow at gmx.com>
- In-reply-to: <4FED54BA.firstname.lastname@example.org>
- References: <4FD21B37.email@example.com> <alpine.LNX.firstname.lastname@example.org> <4FED54BA.email@example.com>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Fri, 29 Jun 2012, Gottfried Barrow wrote:
theorem "x = y ==> y = z ==> x = z" by (rule trans)
theorem "⋀x y z. x = y ==> y = z ==> x = z" by (rule trans)
Note that this stripping of outermost quantifiers looses some
information, but it is convenient, and quite essential for the
implicit rule composition scheme of Isabelle.
But I typed in your 2 theorems above. For the first, in the output of step 0,
it shows x, y, and z as variables. For the second theorem, no variables are
shown in the step 0 output.
That is because the second statement has all variables bound, so the goal
formula is closed and there are no free variables to display here.
I have declare[[show_consts=true]], and this discussion is making some
sense of the constants that show up, which I talk about below in
relation to Trueprop.
Okay, all of this helps make sense of the mystery constants that show up in
the output window:
prop :: prop => prop, and
HOL.Trueprop :: HOL.bool => prop.
They're being used, but it doesn't show explicitly how they're being used.
Well, if the constant quantifier \<And> is really being used, but not
explicitly, then I'm guessing it should show up in the output, like
This is a misunderstanding inherited from the holzf.pdf that was cited
earlier on this thread. The Pure "all" quantifier is always explicitly
visible by the !! or \<And> notation when it is there. The system
explicitly strips outermost quantifiers from result theorems, not by
suppression in the syntax, but by changing the theorem via some
notation prop ("Pr")
to see how prop is being used, but that gives an error.
You need to quote the "prop" above, to prevent its interpretation as
command keyword (as highlighted by Isabelle/jEdit).
The "prop" constant is a bit more esoteric than Trueprop. It normally
does not show up in user applications at all. See section 2.3.2 of
some bits of explanations on it.
I naively thought that every bool gets mapped to prop, but no, it's not
that simple, as shown by "P x" above;
Then there would be no reason to have Trueprop at all. The purpose of it
is to indicate the boundary between the Pure framework (with its native
language of natural deduction rules over \<And> and ==>) and the
object-logic with its diversity of connectives.
This archive was generated by a fusion of
Pipermail (Mailman edition) and