*To*: Michael Norrish <michael.norrish at nicta.com.au>*Subject*: Re: [isabelle] frustrated by blast and instantiation*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 16 Jan 2007 13:39:28 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <45AC4BF1.50909@nicta.com.au>*References*: <45AC4BF1.50909@nicta.com.au>

Michael,

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

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.

**Follow-Ups**:**Re: [isabelle] frustrated by blast and instantiation***From:*Michael Norrish

**References**:**[isabelle] frustrated by blast and instantiation***From:*Michael Norrish

- Previous by Date: Re: [isabelle] Questions about number representation in Isabelle
- Next by Date: Re: [isabelle] frustrated by blast and instantiation
- Previous by Thread: Re: [isabelle] frustrated by blast and instantiation
- Next by Thread: Re: [isabelle] frustrated by blast and instantiation
- Cl-isabelle-users January 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list