Re: [isabelle] frustrated by blast and instantiation
You are right that the meta-level form of a theorem (using !! and
==>) is generally best, but it depends on various factors. You really
need to use an Isar structured proof to take advantage of this
format. Here is a nice version of your proof:
lemma foo3: "!!i. EX! n. n < c & f n = i"
lemma foo4: "(ALL k. P k) = (ALL i. i < c --> P (f i))"
assume "ALL i<c. P (f i)"
with foo3 [of k]
show "P k" by blast
The problem with the straight-line version is that k is a bound
variable, and instantiation by of/where (which is really intended for
structured proofs only) inserts a free variable. With the structured
proof above, k becomes a free variable.
On 16 Jan 2007, at 03:52, Michael Norrish wrote:
I am currently trying to prove what feels like a trivial lemma and
becoming frustrated by meta-level quantifiers and blast, and no doubt
any number of sophisticated considerations that I'm not aware of.
Here is a miniature theory that illustrates a stripped down version of
This archive was generated by a fusion of
Pipermail (Mailman edition) and