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

Re: trivial theorem



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