array2list[T:TYPE+] : THEORY
BEGIN

  IMPORTING listn[T], 
            more_list_props

  array2list_it(a:[nat->T],n:nat,i:upto(n)) : RECURSIVE 
    {l:listn(n-i) | FORALL (j:subrange(i,n-1)) : a(j) = nth(l,j-i)} =
    IF i = n THEN null
    ELSE cons(a(i),array2list_it(a,n,i+1))
    ENDIF
    MEASURE n-i

  array2list(n:nat)(a:[nat->T]) : 
    {l:listn(n) | FORALL (i:below(n)) : a(i) = nth(l,i)} =
    array2list_it(a,n,0)

  list2array(t:T)(l:list)(i:nat) : RECURSIVE T =
    IF null?(l) THEN t
    ELSIF i=0 THEN car(l)  
    ELSE list2array(t)(cdr(l))(i-1)
    ENDIF
  MEASURE l BY <<

  list2array_sound : LEMMA
    FORALL(l:list,t:T,i:nat) : 
      list2array(t)(l)(i) = 
        IF i < length(l) THEN nth(l,i)
        ELSE t
      ENDIF 

  default : T = choose({t:T|true})

  list2array_default(l:list) : MACRO [nat->T] =
    list2array(default)(l)

  array2list_inv : LEMMA
    FORALL (a:[nat->T],t:T,n:nat,i:below(n)) :      
      list2array(t)(array2list(n)(a))(i) = a(i)

  list2array_inv : LEMMA
    FORALL (l:list,t:T,i:below(length(l))) :      
      nth(array2list(length(l))(list2array(t)(l)),i) = nth(l,i)

  list2array_inv_ext : LEMMA
    FORALL (l:list,t:T) :
      array2list(length(l))(list2array(t)(l)) = l

  fill(t:T,n:nat) : 
    {l:listn(n) | FORALL (i:below(n)) : nth(l,i) = t} =
    array2list(n)(LAMBDA(n:nat):t)

END array2list