# Re: [isabelle] Thanks Nitpick for actually answering a former, simple question

On Wed, 12 Sep 2012, Gottfried Barrow wrote:

On 9/11/2012 3:51 PM, Lars Noschinski wrote:

`But the implicit all quantification happens on the outermost level of the
``term, which explains your examples below. They can be simplified as
``follows:
`"!a b. ~(P a b)"
"!a b. P a b"
"~(!a b. P a b)"

`And Makarius had talked some about outermost quantifiers in an email,
``and how they get stripped away.
`

`This was about the Pure connectives !! and ==> which are not the same as
``HOL ! and --> (and more), even though sometimes people prefer to smash
``that distinction. The point of Pure connectives is to describe the
``structure of a rule statement declaratively, so that the system knows what
``is meant and how to compose the rules (by back-chaining and unification).
`

`This is in contrast to the usual FOL view on logic with many connectives,
``and application-specific operations (set-theory, lattices etc.).
``Automated tools turn all this object-logic material *and* the Pure !! and
``==> into hash-brown, and try to serve that to the user. This often works,
``but is no longer Pure logic, the one underlying Isar proofs.
`
So when you state
lemma "!x y. A x --> B y"

`your result is again compact "!x y. A x --> B y" (with its implicit
``Trueprop wrapping).
`
But when you state
lemma "!!x y. A x ==> B y"

`your result is schematic "A ?x ==> B ?y". You can get the same rule by
``writing the statement with explicit "eigen-context" as follows:
`
lemma fixes x y assumes "A x" shows "B y"
or
lemma assumes "A x" shows "B y"

`in most situations, where x and y are implicitly free and thus ready to be
``fixed at the outermost level.
`

`In the latter two forms, the resulting rules emerge naturally, without
``navigating through logical connectives first.
`
Makarius

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