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.