Re: [isabelle] frustrated by blast and instantiation
Lawrence Paulson wrote:
> 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))"
> proof auto
> fix k
> 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.
Thanks. I think I appreciate the distinction between the different
sorts of variables a bit better now. I was misled by or misunderstood
the Tutorial's description of "insert", which uses of in an
apply-style proof, and doesn't seem to run into any issues with
Until I figure out Isar's declarative language, I'll use meta_allE for
the moment (thanks, Tobias).
This archive was generated by a fusion of
Pipermail (Mailman edition) and