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

beginner's problem



I'm sure this is something very basic.
Here are some definitions in my pvs file.

   factorial(x:nat): RECURSIVE nat = 
	   IF x = 0 THEN 1 ELSE x * factorial(x-1) ENDIF
		   MEASURE x 

   fac_loop(x:nat, y:nat): RECURSIVE nat =
    IF x = 0 THEN y ELSE fac_loop(x - 1, x * y) ENDIF
    MEASURE x

I could prove this theorem:

   fact_thm3: THEOREM
         (FORALL (m:nat, n:nat): fac_loop(m, n) = n * fac_loop(m, 1)

But when I added this theorem...

   fact_thm4: THEOREM (FORALL (m:nat): factorial(m) = fact_loop(m, 1))

I get this parse-error message:

   Expecting an expression
   No resolution for fact_loop with arguments of types:
     m : naturalnumbers.nat
     1 : integers.posint

I've spent quite a while trying to figure out what's going on, but
can't.  Please advise.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Steven D. Johnson               net: sjohnson@cs.indiana.edu
Computer Science Department     tel: 812-855-2567
Indiana University              fax: 812-855-4829
Bloomington, IN 47405-4101      www: via http://www.cs.indiana.edu
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~