elements.why 1.72 KB
Newer Older
1 2
theory Elements

3 4
use int.Int
use bag.Bag
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
5
use export map.Map
6

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
7
type array 'a = map int 'a
8 9 10 11

(* [elements a i j] is the bag of elements in a[i..j[ *)
function elements (a:array 'a) (i j:int) : bag 'a

12
axiom Elements_empty : forall a:array 'a, i j:int.
13 14
     i >= j -> (elements a i j) = empty_bag

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
15
axiom Elements_add : forall a:array 'a, i j :int.
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
16
       i < j ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
17
       (elements a i j) = (add a[j-1] (elements a i (j-1)))
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
18 19

lemma Elements_singleton : forall a:array 'a, i j:int.
20
     j = i + 1 ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
21
       (elements a i j) = (singleton a[i])
22

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
23
lemma Elements_union : forall a:array 'a, i j k:int.
24 25 26
     i <= j <= k  ->
      (elements a i k) = (union (elements a i j) (elements a j k))

Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
27
lemma Elements_add1 : forall a:array 'a, i j :int.
28
      i < j ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
29
      (elements a i j) = (add a[i] (elements a (i+1) j))
30

31 32
lemma Elements_remove_last: forall a:array 'a, i j :int.
      i < j-1 ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
33
      (elements a i (j-1)) = diff (elements a i j) (singleton a[j-1])
34 35 36 37 38

lemma Occ_elements: forall a:array 'a, i j n:int.
       i <= j < n ->
         nb_occ a[j] (elements a i n) > 0

39 40 41 42 43 44
let rec lemma elements_set_outside (a:array 'a) (i j:int)
  requires { i <= j }
  variant { j - i }
  ensures { forall k : int. (k < i || k >= j) ->
            forall e:'a. (elements (a[k <- e]) i j) = (elements a i j) }
= if j > i then elements_set_outside a i (j-1)
45

46 47
lemma Elements_set_inside : forall a:array 'a, i j n: int, e:'a, b:bag 'a.
       i <= j < n ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
48 49
       (elements a i n) = add a[j] b ->
       (elements (a[j <- e]) i n) = add e b
50

51 52
lemma Elements_set_inside2 : forall a:array 'a, i j n: int, e:'a.
       i <= j < n ->
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
53
       elements a[j <- e] i n =
54 55
          add e (diff (elements a i n) (singleton (a[j])))

56 57 58 59
end

(*
Local Variables:
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
60
compile-command: "why3ide -I . elements"
61
End:
Asma Tafat-Bouzid's avatar
Asma Tafat-Bouzid committed
62
*)