*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] (i>0) & (int n = i) & P(n) ==> P(i)*From*: Jeremy Avigad <avigad at cmu.edu>*Date*: Tue, 09 Dec 2008 10:33:34 -0500*Cc*: Hauser Bruno <bhauser at student.ethz.ch>*In-reply-to*: <B902E52AFFC79B4CAD0A9A6F0134AA5717910F@EX6.d.ethz.ch>*References*: <B902E52AFFC79B4CAD0A9A6F0134AA5717910F@EX6.d.ethz.ch>*User-agent*: Thunderbird 2.0.0.18 (Windows/20081105)

Hauser Bruno wrote:

Is there a general way for proofing lemmas like: (i>0) & (int n = i) & P(n) ==> P(i) ?

Dear Bruno,

int n + int m = int (n + m) (int n) div (int m) = int (n div m) int n < int m = n < m

Jeremy

**References**:**[isabelle] (i>0) & (int n = i) & P(n) ==> P(i)***From:*Hauser Bruno

- Previous by Date: Re: [isabelle] (i>0) & (int n = i) & P(n) ==> P(i)
- Next by Date: [isabelle] CFP - 4th International Workshop on Systems Software Verification (SSV 09)
- Previous by Thread: Re: [isabelle] (i>0) & (int n = i) & P(n) ==> P(i)
- Next by Thread: [isabelle] Isabelle and Beamer
- Cl-isabelle-users December 2008 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