Quelle  more_list_props.pvs

more_list_props[T: TYPE]: THEORY
BEGIN
  x: VAR T
  l1, l2, l3: VAR list[T]
  P, Q: VAR PRED[T]
  i: VAR nat

  append1(l1, x): list[T] = append(l1, cons(x, null))

  length_parm: LEMMA
     FORALL (pl: list[(P)]):
      length[(P)](pl) = length[T](pl)

  nth_parm: LEMMA
     FORALL (pl: list[(P)], (n:below[length(pl)])):
      nth[(P)](pl, n) = nth[T](pl, n)

  every_parm: LEMMA
     FORALL (pl: list[(P)]):
      every[(P)](Q)(pl) = every[T](Q)(pl)

  append_parm: LEMMA
     FORALL (l1, l2: list[(P)]):
      append[(P)](l1, l2) = append[T](l1, l2)
       

  append_append_cons: LEMMA
    append(l1, cons(x, l2)) = append(append(l1, cons(x, null)), l2)

  append_equal_null: LEMMA append(l1, l2) = l2 => l1 = null

  nth_append_below: LEMMA
    i < length(l1) => nth(append(l1, l2), i) = nth(l1, i)

  nth_append_above: LEMMA
    i >= length(l1) and i < length(append(l1, l2)) => nth(append(l1, l2), i) = nth(l2, i - length(l1))

  tail?(l1, l2): recursive bool =
    if null?(l1)
    then null?(l2)
    else l1 = l2 or tail?(cdr(l1), l2)
    endif
   measure l1 by <<

  tail_append: lemma tail?(append(l1, l2), l2)

  ldiff(l1, (l2 | tail?(l1, l2))): recursive list[T] =
    if l1 = l2
    then null
    else cons(car(l1), ldiff(cdr(l1), l2))
    endif
   measure l1 by <<

  ldiff_append: lemma forall (l1, l2): ldiff(append(l1, l2), l2) = l1

END more_list_props