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

Re: Recursive declarations

Here's the mutually-recursive add1/2 example in PVS.  The "trick" is
to use a flag to switch the body of a single recursive function into
the appropriate one of the two cases.  You might find it instructive
to examine the TCCs (all are proved by M-x tcp) and to prove the lemmas.


delahaye: THEORY


adds(flag: subrange(1,2), n: nat): recursive nat =
  if flag=1 then
    if n=0 then 1 else 1+adds(2,n-1) endif
    if n=0 then 2 else 2+adds(1,n-1) endif
measure n

n, m: var nat
x: var subrange(1,2)

add1(n): nat = adds(1,n)
add2(n): nat = adds(2,n)

test1: lemma add2(4) = 8
test2: lemma add1(4) = 7
test3: lemma add2(5) = 9
test4: lemma add1(5) = 9

test_x: lemma adds(x,2*m) = x+3*m

test_a: lemma add2(2*m) = 2+3*m
test_b: lemma add1(2*m) = 1+3*m

test_d: lemma adds(x,2*m+1) = 3+3*m

END delahaye