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



On 11.09.2012 22:07, Gottfried Barrow wrote:
Hello,
Like two months ago, I specifically asked, in a fairly precise way,
"What's the difference between free variables and universally quantified
variables, and is there a reason I shouldn't use free variables?"
[...]
For a free variable a not bound in any enclosing context, 'lemma "P a"'
is always equivalent to 'lemma "!a. P a"' in that each of these lemmas can be derived from the other.

But the implicit all quantification happens on the outermost level of the term, which explains your examples below. They can be simplified as follows:

theorem
"~((A --> B --> A) --> (A <-> B))"

"!a b. ~(P a b)"

theorem
"(A --> B --> A) --> (A <-> B)"

"!a b. P a b"

theorem
"~(!A. !B.(A --> B --> A) --> (A <-> B))"

"~(!a b. P a b)"

  -- Lars





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