sum.mlw 868 Bytes
Newer Older
1

2 3
(** {1 Sum of the elements of an indexed container} *)

4
module Sum
5

6
  use int.Int
7 8 9

  type container

Andrei Paskevich's avatar
Andrei Paskevich committed
10
  function f container int : int
11
  (** `f c i` is the `i`-th element in the container `c` *)
12

Andrei Paskevich's avatar
Andrei Paskevich committed
13
  function sum container int int : int
14
  (** `sum c i j` is the sum `\sum_{i <= k < j} f c k` *)
15 16 17 18 19 20 21 22

  axiom Sum_def_empty :
    forall c : container, i j : int. j <= i -> sum c i j = 0

  axiom Sum_def_non_empty :
    forall c: container, i j : int. i < j -> sum c i j = f c i + sum c (i+1) j

  lemma Sum_right_extension:
23
    forall c : container, i j : int.
24 25 26 27 28 29 30
    i < j -> sum c i j = sum c i (j-1) + f c (j-1)

  lemma Sum_transitivity :
    forall c : container, i k j : int. i <= k <= j ->
    sum c i j = sum c i k + sum c k j

  lemma Sum_eq :
31
    forall c1 c2 : container, i j : int.
32 33 34
    (forall k : int. i <= k < j -> f c1 k = f c2 k) -> sum c1 i j = sum c2 i j

end