mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
62 lines
1.7 KiB
Plaintext
62 lines
1.7 KiB
Plaintext
theory Elements
|
|
|
|
use int.Int
|
|
use bag.Bag
|
|
use export map.Map
|
|
|
|
type array 'a = map int 'a
|
|
|
|
(* [elements a i j] is the bag of elements in a[i..j[ *)
|
|
function elements (a:array 'a) (i j:int) : bag 'a
|
|
|
|
axiom Elements_empty : forall a:array 'a, i j:int.
|
|
i >= j -> (elements a i j) = empty_bag
|
|
|
|
axiom Elements_add : forall a:array 'a, i j :int.
|
|
i < j ->
|
|
(elements a i j) = (add a[j-1] (elements a i (j-1)))
|
|
|
|
lemma Elements_singleton : forall a:array 'a, i j:int.
|
|
j = i + 1 ->
|
|
(elements a i j) = (singleton a[i])
|
|
|
|
lemma Elements_union : forall a:array 'a, i j k:int.
|
|
i <= j <= k ->
|
|
(elements a i k) = (union (elements a i j) (elements a j k))
|
|
|
|
lemma Elements_add1 : forall a:array 'a, i j :int.
|
|
i < j ->
|
|
(elements a i j) = (add a[i] (elements a (i+1) j))
|
|
|
|
lemma Elements_remove_last: forall a:array 'a, i j :int.
|
|
i < j-1 ->
|
|
(elements a i (j-1)) = diff (elements a i j) (singleton a[j-1])
|
|
|
|
lemma Occ_elements: forall a:array 'a, i j n:int.
|
|
i <= j < n ->
|
|
nb_occ a[j] (elements a i n) > 0
|
|
|
|
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)
|
|
|
|
lemma Elements_set_inside : forall a:array 'a, i j n: int, e:'a, b:bag 'a.
|
|
i <= j < n ->
|
|
(elements a i n) = add a[j] b ->
|
|
(elements (a[j <- e]) i n) = add e b
|
|
|
|
lemma Elements_set_inside2 : forall a:array 'a, i j n: int, e:'a.
|
|
i <= j < n ->
|
|
elements a[j <- e] i n =
|
|
add e (diff (elements a i n) (singleton (a[j])))
|
|
|
|
end
|
|
|
|
(*
|
|
Local Variables:
|
|
compile-command: "why3ide -I . elements"
|
|
End:
|
|
*) |