*To*: gottfried.barrow at gmx.com*Subject*: Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers*From*: Makarius <makarius at sketis.net>*Date*: Thu, 28 Jun 2012 23:29:29 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4FD21B37.8010304@gmx.com>*References*: <4FD21B37.8010304@gmx.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 8 Jun 2012, gottfried.barrow at gmx.com wrote:

In Krauss & Schropp's "A Mechanized Translation from Higher-Order Logic toSet Theory", page 5, <http://home.in.tum.de/~schropp/>, they say:In Isabelle, outermost quantiers and the [.]-embedding are not printed...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. (2) [.] is notation in the cited paper for Trueprop. 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

Makarius

**Follow-Ups**:**Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers***From:*Gottfried Barrow

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

- Previous by Date: Re: [isabelle] Referring to "this" in "from" and "using"
- Next by Date: Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- Previous by Thread: [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