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



On 6/28/2012 4:29 PM, Makarius wrote:
On Fri, 8 Jun 2012, gottfried.barrow at gmx.com wrote:
QUESTION 1: Is there a command to show these hidden meta-logic
quantifiers, or any other such hidden meta-logic? I suppose not.

There two different things here:

(1) Outermost quantifiers are circumvented, by writing things with fixed
variables instead ("eigen context") and then make them arbitrary in
the result.

If you do write explicit quantifiers, which are escpecially required
for things nested on the LHS (e.g. in assumptions), there is an
explicit core inference that removes the quantifiers and expresses the
generality in terms of schematic variables.

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.

To summarize, I'm pretty sure that what you're saying is, "There's a lot that goes on under the hood of the engine."

This discussion ties into the thread "Free variables vs schematic variables":

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00048.html

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. I guess that's related to what you're talking about above.

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.

(2) [.] is notation in the cited paper for Trueprop.

I missed understanding what that meant, so thanks for the clarification.

But the meaning of [.], along with your discussion above, brings up their statement again from page 5 of holzf.pdf:

    In Isabelle, outermost quantifiers and the [.]-embedding are not
    printed.

In particular, they give as an example [edited by me],

    \<And>P::'a => bool.(\<And>x::'a. [P x]) ==> [\<forall>x. P x]

where the square brackets is the application of Trueprop, and they say that this will be shown in HOL as

   (\<And>x::'a. P x) ==> \<forall>x. P x

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.

But to summarize again, there's a lot going on under the hood, or the bonnet, which is a good enough explanation for me right now.

Here is a
copy-paste from an explanation that I have given in some Isabelle
course at some point:

text {*
The object-logic is embedded into the Pure framework via an implicit
derivability judgment @{term "Trueprop :: bool ⇒ prop"}.

Thus any HOL formulae appears atomic to the Pure framework, while
the rule structure outlines the corresponding proof pattern.

This can be made explicit as follows:
*}

notepad
begin
write Trueprop ("Tr")

thm conjI
thm impI
thm nat.induct
end

I found that in your 2010 and 2012 LRI tutorials, in the .thy's for natural deduction:

   http://www.lri.fr/~wenzel/

It's on my agenda to look at those tutorials, but it's also on my agenda to look more at "Isabelle/Isar --- a versatile environment...":

   http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html

Especially after reading "Twenty Ways to Prove A /\ B --> B /\ A" in sections 4.2.3 and 4.2.4. The new "prog-prove.pdf" by Tobias is good, but it only recently surfaced; I gave up some time back trying to learn all this in a linear manner.

Above you can also use a global 'notation' command, but making
everything local is more fun.

So you say, but the commands

    notation Trueprop ("Tr")
    notation all  ("AllStuff")

are providing sufficient fun for the moment. I don't see "all" showing up anywhere that it's not explicitly used.

I tried

   notation prop ("Pr")

to see how prop is being used, but that gives an error. You can only have so much fun in a day.

This is good information. I naively thought that every bool gets mapped to prop, but no, it's not that simple, as shown by "P x" above; "notation Truepropr ("Tr")" is giving me what I asked for.

Thanks,
GB









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