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

[PVS-Help] Induction by a recursive function?




Dear All,
         While working with finseq, i came accross a problem. I have a finseq[finseq[T]] and a finseq[T], first I divide finseq[T] and get finseq[finseq[T]] and then try to construct the finseq[T] from it. My theory is as below:

In lemma, i use induction on length of finseq[T] and in induction step, when I need to initialize but this may be another recursive function. How can I do so? Can some help me?

example[T: TYPE] : THEORY
BEGIN
  importing seqown
% in finseq own, i ve parent and last, parent returns all the ancestors
% and last returns last seq.
  SEQ: TYPE = finseq[T]
  t : VAR T
  fs:VAR finseq[finseq[T]]
  s:VAR SEQ
  i,j : VAR nat

  extrt(s,i):SEQ=
    IF i< s`length THEN 
    LET len = s`length IN
        (#length :=len, 
         seq := (LAMBDA (n:below[len]) :
	   	         seq(s)(n))#) 
   ELSE
     empty_seq
   ENDIF  

  extr(s): finseq[SEQ]=
   IF s`length>0 THEN
    LET len = s`length IN
      (#length := len,
        seq := (LAMBDA (i:below[len]):
                            extrt(s,i))#) 
   ELSE empty_seq ENDIF 

  concat(fs):RECURSIVE finseq[T]=   
   IF length(fs) = 0 THEN empty_seq
   ELSE
      concat(parent(fs)) o last(fs)
   ENDIF
   MEASURE length(fs) 
  
  concat_Extr:LEMMA
   FORALL j: j= length(extr(s)) AND ne_seq?(concat(extr(s))) 
         IMPLIES s=concat(extr(s))

 END example
-----------

{1}   FORALL (j_1: nat):
        (FORALL (s: SEQ):
           j_1 = length(extr(s)) AND length(s) > 0 IMPLIES
            s = concat(extr(s)))
         IMPLIES
         (FORALL (s: SEQ):
            j_1 + 1 = length(extr(s)) AND length(s) > 0 IMPLIES
             s = concat(extr(s)))



Rule? (skosimp*)
Repeatedly Skolemizing and flattening,
this simplifies to: 
concat_Extr.2 :  

{-1}  FORALL (s: SEQ):
        j!1 = length(extr(s)) AND length(s) > 0 IMPLIES s = concat(extr(s))
{-2}  j!1 + 1 = length(extr(s!1))
{-3}  length(s!1) > 0
  |-------
{1}   s!1 = concat(extr(s!1))



Rule? (expand "concat" +)
Expanding the definition of concat,
this simplifies to: 
concat_Extr.2 :  

[-1]  FORALL (s: SEQ):
        j!1 = length(extr(s)) AND length(s) > 0 IMPLIES s = concat(extr(s))
[-2]  j!1 + 1 = length(extr(s!1))
[-3]  length(s!1) > 0
  |-------
{1}   s!1 =
       IF length(extr(s!1)) = 0 THEN empty_seq
       ELSE concat(parent(extr(s!1))) o last(extr(s!1))
       ENDIF



Rule? (lift-if )
Lifting IF-conditions to the top level,
this simplifies to: 
concat_Extr.2 :  

[-1]  FORALL (s: SEQ):
        j!1 = length(extr(s)) AND length(s) > 0 IMPLIES s = concat(extr(s))
[-2]  j!1 + 1 = length(extr(s!1))
[-3]  length(s!1) > 0
  |-------
{1}   IF length(extr(s!1)) = 0 THEN s!1 = empty_seq
      ELSE s!1 = concat(parent(extr(s!1))) o last(extr(s!1))
      ENDIF



Rule? (assert)
Simplifying, rewriting, and recording with decision procedures,
this simplifies to: 
concat_Extr.2 :  

[-1]  FORALL (s: SEQ):
        j!1 = length(extr(s)) AND length(s) > 0 IMPLIES s = concat(extr(s))
{-2}  1 + j!1 = length(extr(s!1))
[-3]  length(s!1) > 0
  |-------
{1}   s!1 = concat(parent(extr(s!1))) o last(extr(s!1))



Rule? (inst - "concat(parent(extr(s!1)))")
Instantiating the top quantifier in - with the terms: 
 concat(parent(extr(s!1))),
this simplifies to: 
concat_Extr.2 :  

{-1}  j!1 = length(extr(concat(parent(extr(s!1))))) AND
       length(concat(parent(extr(s!1)))) > 0
       IMPLIES
       concat(parent(extr(s!1))) = concat(extr(concat(parent(extr(s!1)))))
[-2]  1 + j!1 = length(extr(s!1))
[-3]  length(s!1) > 0
  |-------
[1]   s!1 = concat(parent(extr(s!1))) o last(extr(s!1))



Rule? (assert)
Simplifying, rewriting, and recording with decision procedures,
this simplifies to: 
concat_Extr.2 :  

[-1]  j!1 = length(extr(concat(parent(extr(s!1))))) AND
       length(concat(parent(extr(s!1)))) > 0
       IMPLIES
       concat(parent(extr(s!1))) = concat(extr(concat(parent(extr(s!1)))))
[-2]  1 + j!1 = length(extr(s!1))
[-3]  length(s!1) > 0
  |-------
[1]   s!1 = concat(parent(extr(s!1))) o last(extr(s!1))



Rule? (prop)
Applying propositional simplification,
this yields  3 subgoals: 
concat_Extr.2.1 :  

{-1}  concat(parent(extr(s!1))) = concat(extr(concat(parent(extr(s!1)))))
[-2]  1 + j!1 = length(extr(s!1))
[-3]  length(s!1) > 0
  |-------
[1]   s!1 = concat(parent(extr(s!1))) o last(extr(s!1))



Rule? (assert)
Simplifying, rewriting, and recording with decision procedures,
this simplifies to: 
concat_Extr.2.1 :  

[-1]  concat(parent(extr(s!1))) = concat(extr(concat(parent(extr(s!1)))))
[-2]  1 + j!1 = length(extr(s!1))
[-3]  length(s!1) > 0
  |-------
[1]   s!1 = concat(parent(extr(s!1))) o last(extr(s!1))


Rule? 



Best Regards,

M Ikram