*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.9010601@gmx.com>*References*: <4FD21B37.8010304@gmx.com> <alpine.LNX.2.00.1206282323070.13196@macbroy21.informatik.tu-muenchen.de> <4FED54BA.9010601@gmx.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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 areshown in the step 0 output.

I have declare[[show_consts=true]], and this discussion is making somesense of the constants that show up, which I talk about below inrelation to Trueprop.Okay, all of this helps make sense of the mystery constants that show up inthe 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 notexplicitly, then I'm guessing it should show up in the output, likeTrueprop.

I tried notation prop ("Pr") to see how prop is being used, but that gives an error.

I naively thought that every bool gets mapped to prop, but no, it's notthat simple, as shown by "P x" above;

Makarius

- Previous by Date: Re: [isabelle] variable in Isar?
- Next by Date: [isabelle] HOLCF equality
- Previous by Thread: Re: [isabelle] variable in Isar?
- Next by Thread: [isabelle] HOLCF equality
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list