Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers



On Fri, 29 Jun 2012, Gottfried Barrow wrote:

Examples:

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 Trueprop.

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 inferences.


I tried

  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 http://isabelle.in.tum.de/dist/Isabelle2012/doc/implementation.pdf for 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.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.