[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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
>
>
>
>