# Re: [PVS-Help] Induction by a recursive function?

```It's not quite clear to me what you're trying to do; I'll assume you'd
like to induct on 's'. If that is the case, rather than running
(skosimp*) straightaway, you should run a (skolem!)/(flatten)
combination that isolates that (FORALL (s: SEQ) ...) after the
implication (so that FORALL is all you have in the consequent). Then
you can use the native PVS induction command on s: (induct "s" ...)

jerome

On Thu, Jul 16, 2009 at 03:57:21AM -0700, Ikram Ullah Lali wrote:
>
>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
>
>
>
>

```