[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: trivial theorem

To: mandrio5@ipmel3 (Stud. D. Mandrioli)
Subject: Re: trivial theorem
From: Darrell Kindred <dkindred@cmu.edu>
Date: Mon, 28 Jul 1997 21:09:54 -0400
Cc: pvs-help@csl.sri.com, mandrio5@elet.polimi.it
In-Reply-To: <9707282211.AA23880@ipmel3.>
Organization: Carnegie Mellon University School of Computer Science
References: <9707282211.AA23880@ipmel3.>

Stud. D. Mandrioli writes:
 > I can't prove this:
 >   bah : LEMMA FORALL (r:real, k1,k2:int) : NOT ( r>0 AND r<1 AND k1+r=k2)

Here's one proof.  A cleaner one may be possible.

  (""
   (SKOSIMP*)
   (CASE "r!1 = k2!1 - k1!1")
   (("1"
     (CASE "integer?(r!1)")
     (("1"
       (CASE "FORALL (i:int): NOT (i > 0 AND i < 1)")
       (("1" (GRIND)) ("2" (GRIND))))
      ("2" (GRIND))))
    ("2" (GROUND))))

This proves that "r" must be an integer, and then that no
integers exist between 0 and 1.  You might choose to state
a general case of the latter as a separate lemma:

    no_ints_between_consecutive_ints : LEMMA
      FORALL (i,j:int): NOT (j > i AND j < i+1)

(This is proved with one "grind".)  The proof above then becomes

  (""
   (SKOSIMP*)
   (USE "no_ints_between_consecutive_ints")
   (("1" (ASSERT))
    ("2" (CASE "r!1 = k2!1 - k1!1") (("1" (GROUND)) ("2" (GROUND))))))

- Darrell

References:
- trivial theorem
  - From: mandrio5@ipmel3 (Stud. D. Mandrioli)

Prev by Date: trivial theorem
Next by Date: Re: Getting Help
Prev by thread: trivial theorem
Next by thread: lemma,inst? and replace
Index(es):
- Date
- Thread