Re: [isabelle] frustrated by blast and instantiation



Michael,

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

Larry


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
my problem.






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