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"
> sorry

> 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
> qed

> 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
its quantifiers.

Until I figure out Isar's declarative language, I'll use meta_allE for
the moment (thanks, Tobias).

Regards,
Michael.







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