*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Fri, 29 Jun 2012 02:09:46 -0500*In-reply-to*: <alpine.LNX.2.00.1206282323070.13196@macbroy21.informatik.tu-muenchen.de>*References*: <4FD21B37.8010304@gmx.com> <alpine.LNX.2.00.1206282323070.13196@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

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.

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

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

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

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]

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

prop :: prop => prop, and HOL.Trueprop :: HOL.bool => prop. They're being used, but it doesn't show explicitly how they're being used.

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

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

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

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")

I tried notation prop ("Pr")

Thanks, GB

**References**:**[isabelle] "Proof terms" section of isar-ref; Outermost quantifiers***From:*gottfried . barrow

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

- Previous by Date: Re: [isabelle] HOLCF
- Next by Date: Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- Previous by Thread: Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- Next by Thread: Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- Cl-isabelle-users June 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