|
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
[ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
]
|
