Quelle  listn.pvs

listn[T:TYPE] : THEORY
BEGIN

  IMPORTING list[T]

  listn?(n:nat)(l:list) : MACRO bool = length(l)=n

  listn(n:nat) : TYPE = (listn?(n))

  listn_ext : LEMMA
    FORALL(n:nat,l1:listn(n),l2:listn(n)):
      (FORALL (i:below(n)): nth(l1,i) = nth(l2,i)) IMPLIES l1 = l2

  listn_0 : JUDGEMENT
    null HAS_TYPE listn(0)

  setnth(l:list,n:nat,f:[T->T]) : RECURSIVE 
    {sl : listn(length(l)) | 
          FORALL (i:below(length(l))) : IF i=n THEN nth(sl,i) = f(nth(l,i)) 
                                        ELSE nth(sl,i) = nth(l,i)
                                        ENDIF} =
    CASES l OF
      null : null,
      cons(a,r) : IF n=0 THEN cons(f(a),r)
                  ELSE cons(a,setnth(r,n-1,f))
                  ENDIF
    ENDCASES
  MEASURE l BY <<

  finseqn?(n:nat)(f:finseq[T]) : MACRO bool = f`length = n

  Finseqn(n:nat) : TYPE = (finseqn?(n))

  normalize_fseq(f:finseq[T]): {fsn: Finseqn(f`length)|fsn = f} =
    LET fslist = finseq2list(f)
    IN  list2finseq(fslist)

  normalize_fseq_def: LEMMA FORALL (f:finseq[T]): normalize_fseq(f) = f


END listn