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
"!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
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"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and