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



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

In Krauss & Schropp's "A Mechanized Translation from Higher-Order Logic to Set 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


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


	Makarius


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