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

[PVS-Help] Proof by induction fails with geenric and library



Hi all

I am trying to prove a theorem by induction but I got a problem.
Not sure it is a bug, I did not succeed isolating the problem so I need some hints
or better the solution.

I have some specifications, mainly a datatype World which is used in another
library.
In the second library I can type-check and even prove but induction is failing
at the lisp level

The critical part is enclosed:

Test[S,W:TYPE] : THEORY
BEGIN
	IMPORTING BASE@TheoryWorld[S, W]

	 % does not work (but succeed in the BASE library)
size_theorem2 : THEOREM FORALL (w:World[S,W]): size(w) > 0

	     % BUGS ?
END Test

Launching the prover I got the following message

pvs(1): 
pvs(2): 
Installing rewrite rule sets.singleton_rew (all instances)

size_theorem2 :  

  |-------
{1}   FORALL (w: World[S, W]): b2n(size(w)) > 0

Rule? (induct "w")
Error: No methods applicable for generic function
       #<standard-generic-function add-usings-to-context*> with args
       (nil ListMonitors[S, W]) of classes (null full-modname)
  [condition type: program-error]

I suspect some problems with library, data type induction and parameter types.
But may be it is a mistake in my specifications.
regards

Jean-Claude.Royer@mines-nantes.fr
ASCOLA, Mines de Nantes - INRIA
+ 33 2 51 85 82 05