*To*: Nicole Rauch <rauch at informatik.uni-kl.de>*Subject*: Re: [isabelle] Metalogical "spec" not resolved automatically*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 19 Oct 2005 10:43:40 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <36FFDE13-EBEA-4BCC-830E-734107354DC5@informatik.uni-kl.de>*References*: <36FFDE13-EBEA-4BCC-830E-734107354DC5@informatik.uni-kl.de>*Sender*: "L. Paulson" <lp15 at hermes.cam.ac.uk>

Larry Paulson On 19 Oct 2005, at 09:20, Nicole Rauch wrote:

I'm stuck with a logical problem and I don't see why it is nottrivial to Isabelle. These are my two subgoals:1. !! N. [| 0 < N; P N |] ==> P (Suc 0) 2. !! N. [| 0 < N; P N; 0 < M |] ==> P MIf P holds for all arguments greater than zero, then it should holdfor a fixed argument which is greater than zero. This is basicallyHOL's spec lemma, just with metalogical quantification instead ofHOL quantification. But Isabelle refuses to accept this. What am Ioverlooking here?

**References**:**[isabelle] Metalogical "spec" not resolved automatically***From:*Nicole Rauch

- Previous by Date: Re: [isabelle] recdef tuple for 2 args, infix syntax possible?
- Next by Date: Re: [isabelle] Metalogical "spec" not resolved automatically
- Previous by Thread: Re: [isabelle] Metalogical "spec" not resolved automatically
- Next by Thread: Re: [isabelle] Metalogical "spec" not resolved automatically
- Cl-isabelle-users October 2005 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