[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