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

[PVS-Help] Re: help to prove my first theorem



M Raghuram <raghu_megh@yahoo.com> wrote:
>      I am new to PVS. I wrote my first theorem and I
> am not able to prove it using PVS. I have read the
> documentation abt the prover but I am not able to do
> it. May be its trivial but not yet for me. The
> following is my first theory.
> 
> First : Theory
> 
> Begin
>    m : Var nat
> 
> Th1 : Theorem Forall (m1: bvec[m]): exists
> (m2:bvec[m]): (xor(m1,m2) = m1) => (m2=nat2bv(0))
> 
> End First

Your specification is a bit confused.  You are saying, "Give me any
bitvector m1.  I can then produce an m2 such that, if it so happens that
xor(m1,m2) = m1, then m2 is nat2bv(0)."  I suspect you really mean one
of the following:

First: THEORY
 BEGIN

  m: VAR nat

  Th1: THEOREM
    FORALL (m1, m2: bvec[m]): XOR(m1, m2) = m1 IFF bv2nat(m2) = 0

  Th2: THEOREM FORALL (m1: bvec[m]): EXISTS (m2: bvec[m]): XOR(m1, m2) = m1

 END First

Both of those theorems can be proved with a little effort.  Read up on
the decompose-equality strategy; you'll need it.  Also, by changing your
use of nat2bv into a use of bv2nat instead, I've made it possible to use
the bv2nat_fill_F and bv2nat_eq0 lemmas from the prelude.  See what
those two lemmas say and think about how they might be used.

Good luck!
-- 
Jerry James
http://www.ittc.ku.edu/~james/