Commit f5583575 authored by MARCHE Claude's avatar MARCHE Claude

proof of heap_implem.insert

parent d9caac0a
......@@ -44,6 +44,9 @@ lemma Union_assoc : forall a b c:bag 'a.
lemma bag_simpl : forall a b c: bag 'a.
(union a b) = (union c b) -> a = c
lemma bag_simpl_left : forall a b c: bag 'a.
(union a b) = (union a c) -> b = c
(* add operation *)
function add (x : 'a) (b: bag 'a) : bag 'a = union (singleton x) b
......
......@@ -10,38 +10,43 @@ type array 'a = A.map int 'a
function elements (a:array 'a) (i j:int) : bag 'a
axiom Elements_empty : forall a:array int, i j:int.
axiom Elements_empty : forall a:array 'a, i j:int.
i >= j -> (elements a i j) = empty_bag
axiom Elements_singleton : forall a:array int, i j:int.
axiom Elements_singleton : forall a:array 'a, i j:int.
j = i + 1 ->
(elements a i j) = (singleton (A.get a i))
axiom Elements_union : forall a:array int, i j k:int.
axiom 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_union1 : forall a:array int, i j :int.
lemma Elements_union1 : forall a:array 'a, i j :int.
i < j ->
(elements a i j) = (add (A.get a i) (elements a (i+1) j))
lemma Elements_union2 : forall a:array int, i j :int.
lemma Elements_union2 : forall a:array 'a, i j :int.
i < j ->
(elements a i j) = (add (A.get a (j-1)) (elements a i (j-1)))
lemma Elements_set : forall a:array int, i j:int.
lemma Elements_set_outside : forall a:array 'a, i j:int.
i <= j -> forall k : int. (k < i || k >= j) ->
forall e:int. (elements (A.set a k e) i j) = (elements a i j)
forall e:'a. (elements (A.set a k e) i j) = (elements a i j)
lemma Elements_union3 : forall a:array int, i j k:int.
lemma Elements_union3 : forall a:array 'a, i j:int, e:'a.
i <= j ->
(add k (elements a i j)) = (elements (A.set a j k) i (j+1))
(add e (elements a i j)) = (elements (A.set a j e) i (j+1))
lemma Elements_set2 : forall a:array int, i j k:int.
lemma Elements_set2 : forall a:array 'a, i j k:int.
i <= k < j ->
forall e:int. (add (A.get a k) (elements (A.set a k e) i j)) =
forall e:'a. (add (A.get a k) (elements (A.set a k e) i j)) =
(add e (elements a i j))
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.get a j) b ->
(elements (A.set a j e) i n) = add e b
end
(*
......
......@@ -44,15 +44,14 @@ let insert (this : ref logic_heap) (e : int) : unit =
let p = A.get !arr parent in
if (e >= p) then raise Break;
arr := A.set !arr !i p;
i := parent;
assert { is_heap_array !arr 0 (n + 1) }
i := parent
done
with Break -> ()
end;
arr := A.set !arr !i e;
this := (!arr, n + 1);
assert { !i = n -> is_heap !this };
assert { !i < n -> is_heap !this }
assert { 0 < !i < n -> is_heap !this };
assert { !i < n -> model !this = add e (model (a,n)) }
{ is_heap !this /\
model !this = add e (model (old !this)) }
......
......@@ -75,6 +75,10 @@ Axiom Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
Axiom Union_assoc : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 (union b c)) = (union (union a1 b) c)).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem bag_simpl : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union c b)) -> (a1 = c).
(* YOU MAY EDIT THE PROOF BELOW *)
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Axiom Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
Axiom Union_assoc : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 (union b c)) = (union (union a1 b) c)).
Axiom bag_simpl : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union c b)) -> (a1 = c).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem bag_simpl_left : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union a1 c)) -> (b = c).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X a b c H_union.
apply bag_extensionality; intro x.
assert (h: (get (union a b) x) = (get (union a c) x))
by (rewrite H_union; auto).
do 2 rewrite occ_union in h; auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -109,44 +109,51 @@ Parameter elements: forall (a:Type), (map Z a) -> Z -> Z -> (map a Z).
Implicit Arguments elements.
Axiom Elements_empty : forall (a:(map Z Z)) (i:Z) (j:Z), (j <= i)%Z ->
((elements a i j) = (empty_bag:(map Z Z))).
Axiom Elements_empty : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
(j <= i)%Z -> ((elements a1 i j) = (empty_bag:(map a Z))).
Axiom Elements_singleton : forall (a:(map Z Z)) (i:Z) (j:Z),
(j = (i + 1%Z)%Z) -> ((elements a i j) = (set (empty_bag:(map Z Z)) (get a
i) 1%Z)).
Axiom Elements_singleton : forall (a:Type), forall (a1:(map Z a)) (i:Z)
(j:Z), (j = (i + 1%Z)%Z) -> ((elements a1 i j) = (set (empty_bag:(map a Z))
(get a1 i) 1%Z)).
Axiom Elements_union : forall (a:(map Z Z)) (i:Z) (j:Z) (k:Z), ((i <= j)%Z /\
(j <= k)%Z) -> ((elements a i k) = (union (elements a i j) (elements a j
k))).
Axiom Elements_union : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z)
(k:Z), ((i <= j)%Z /\ (j <= k)%Z) -> ((elements a1 i
k) = (union (elements a1 i j) (elements a1 j k))).
Axiom Elements_union1 : forall (a:(map Z Z)) (i:Z) (j:Z), (i < j)%Z ->
((elements a i j) = (add (get a i) (elements a (i + 1%Z)%Z j))).
Axiom Elements_union1 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
(i < j)%Z -> ((elements a1 i j) = (add (get a1 i) (elements a1 (i + 1%Z)%Z
j))).
Axiom Elements_union2 : forall (a:(map Z Z)) (i:Z) (j:Z), (i < j)%Z ->
((elements a i j) = (add (get a (j - 1%Z)%Z) (elements a i (j - 1%Z)%Z))).
Axiom Elements_union2 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
(i < j)%Z -> ((elements a1 i j) = (add (get a1 (j - 1%Z)%Z) (elements a1 i
(j - 1%Z)%Z))).
Axiom Elements_set : forall (a:(map Z Z)) (i:Z) (j:Z), (i <= j)%Z ->
forall (k:Z), ((k < i)%Z \/ (j <= k)%Z) -> forall (e:Z), ((elements (set a
k e) i j) = (elements a i j)).
Axiom Elements_set_outside : forall (a:Type), forall (a1:(map Z a)) (i:Z)
(j:Z), (i <= j)%Z -> forall (k:Z), ((k < i)%Z \/ (j <= k)%Z) ->
forall (e:a), ((elements (set a1 k e) i j) = (elements a1 i j)).
Axiom Elements_union3 : forall (a:(map Z Z)) (i:Z) (j:Z) (k:Z), (i <= j)%Z ->
((add k (elements a i j)) = (elements (set a j k) i (j + 1%Z)%Z)).
Axiom Elements_union3 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z)
(e:a), (i <= j)%Z -> ((add e (elements a1 i j)) = (elements (set a1 j e) i
(j + 1%Z)%Z)).
Theorem Elements_set2 : forall (a:(map Z Z)) (i:Z) (j:Z) (k:Z),
((i <= k)%Z /\ (k < j)%Z) -> forall (e:Z), ((add (get a k)
(elements (set a k e) i j)) = (add e (elements a i j))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem Elements_set2 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z)
(k:Z), ((i <= k)%Z /\ (k < j)%Z) -> forall (e:a), ((add (get a1 k)
(elements (set a1 k e) i j)) = (add e (elements a1 i j))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros.
intros A a i j k Hijk e.
pattern (elements (set a k e) i j);
rewrite Elements_union with (j := k); auto with zarith.
pattern (elements (set a k e) i k);
rewrite Elements_set; auto with zarith.
rewrite Elements_set_outside; auto with zarith.
pattern (elements (set a k e) k j);
rewrite Elements_union1; auto with zarith.
pattern (get (set a k e) k); rewrite Select_eq; auto.
pattern (elements (set a k e) (k + 1) j);
rewrite Elements_set; auto with zarith.
rewrite Elements_set_outside; auto with zarith.
unfold add.
pattern (union (elements a i k)
(union (set empty_bag e 1%Z)
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Axiom Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
Axiom Union_assoc : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 (union b c)) = (union (union a1 b) c)).
Axiom bag_simpl : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union c b)) -> (a1 = c).
Axiom bag_simpl_left : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union a1 c)) -> (b = c).
Definition add (a:Type)(x:a) (b:(map a Z)): (map a Z) :=
(union (set (empty_bag:(map a Z)) x 1%Z) b).
Implicit Arguments add.
Axiom occ_add_eq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(x = y) -> ((get (add x b) x) = ((get b x) + 1%Z)%Z).
Axiom occ_add_neq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(~ (x = y)) -> ((get (add x b) y) = (get b y)).
Parameter card: forall (a:Type), (map a Z) -> Z.
Implicit Arguments card.
Axiom Card_empty : forall (a:Type), ((card (empty_bag:(map a Z))) = 0%Z).
Axiom Card_singleton : forall (a:Type), forall (x:a),
((card (set (empty_bag:(map a Z)) x 1%Z)) = 1%Z).
Axiom Card_union : forall (a:Type), forall (x:(map a Z)) (y:(map a Z)),
((card (union x y)) = ((card x) + (card y))%Z).
Axiom Card_zero_empty : forall (a:Type), forall (x:(map a Z)),
((card x) = 0%Z) -> (x = (empty_bag:(map a Z))).
Definition array (a:Type) := (map Z a).
Parameter elements: forall (a:Type), (map Z a) -> Z -> Z -> (map a Z).
Implicit Arguments elements.
Axiom Elements_empty : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
(j <= i)%Z -> ((elements a1 i j) = (empty_bag:(map a Z))).
Axiom Elements_singleton : forall (a:Type), forall (a1:(map Z a)) (i:Z)
(j:Z), (j = (i + 1%Z)%Z) -> ((elements a1 i j) = (set (empty_bag:(map a Z))
(get a1 i) 1%Z)).
Axiom Elements_union : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z)
(k:Z), ((i <= j)%Z /\ (j <= k)%Z) -> ((elements a1 i
k) = (union (elements a1 i j) (elements a1 j k))).
Axiom Elements_union1 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
(i < j)%Z -> ((elements a1 i j) = (add (get a1 i) (elements a1 (i + 1%Z)%Z
j))).
Axiom Elements_union2 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z),
(i < j)%Z -> ((elements a1 i j) = (add (get a1 (j - 1%Z)%Z) (elements a1 i
(j - 1%Z)%Z))).
Axiom Elements_set_outside : forall (a:Type), forall (a1:(map Z a)) (i:Z)
(j:Z), (i <= j)%Z -> forall (k:Z), ((k < i)%Z \/ (j <= k)%Z) ->
forall (e:a), ((elements (set a1 k e) i j) = (elements a1 i j)).
Axiom Elements_union3 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z)
(e:a), (i <= j)%Z -> ((add e (elements a1 i j)) = (elements (set a1 j e) i
(j + 1%Z)%Z)).
Axiom Elements_set2 : forall (a:Type), forall (a1:(map Z a)) (i:Z) (j:Z)
(k:Z), ((i <= k)%Z /\ (k < j)%Z) -> forall (e:a), ((add (get a1 k)
(elements (set a1 k e) i j)) = (add e (elements a1 i j))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem Elements_set_inside : forall (a:Type), forall (a1:(map Z a)) (i:Z)
(j:Z) (n:Z) (e:a) (b:(map a Z)), ((i <= j)%Z /\ (j < n)%Z) ->
(((elements a1 i n) = (add (get a1 j) b)) -> ((elements (set a1 j e) i
n) = (add e b))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X a i j n e b Hi H.
apply bag_simpl_left with (a1:=(add (get a j) empty_bag)).
replace (add e b) with (union b (add e empty_bag)).
2: rewrite Union_comm ; unfold add ; rewrite Union_identity; auto.
rewrite Union_assoc.
unfold add; rewrite Union_identity.
unfold add in H; rewrite <- H; clear H.
rewrite Elements_union with (j:=j); auto with zarith.
rewrite Elements_set_outside; auto with zarith.
pattern (elements (set a j e) j n); rewrite Elements_union1; auto with zarith.
rewrite Select_eq; auto.
rewrite Elements_set_outside; auto with zarith.
rewrite Elements_union with (i:=i) (j:=j) (k:=n); auto with zarith.
pattern (elements a j n); rewrite Elements_union1; auto with zarith.
(* AC1 equality *)
rewrite Union_identity.
rewrite Union_assoc.
pattern (union (set empty_bag (get a j) 1%Z) (elements a i j)); rewrite Union_comm.
rewrite <- Union_assoc.
rewrite <- Union_assoc.
apply f_equal.
unfold add.
rewrite <- Union_assoc.
apply f_equal.
apply Union_comm.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Axiom Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
Axiom Union_assoc : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 (union b c)) = (union (union a1 b) c)).
Axiom bag_simpl : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union c b)) -> (a1 = c).
Definition add (a:Type)(x:a) (b:(map a Z)): (map a Z) :=
(union (set (empty_bag:(map a Z)) x 1%Z) b).
Implicit Arguments add.
Axiom occ_add_eq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(x = y) -> ((get (add x b) x) = ((get b x) + 1%Z)%Z).
Axiom occ_add_neq : forall (a:Type), forall (b:(map a Z)) (x:a) (y:a),
(~ (x = y)) -> ((get (add x b) y) = (get b y)).
Parameter card: forall (a:Type), (map a Z) -> Z.
Implicit Arguments card.
Axiom Card_empty : forall (a:Type), ((card (empty_bag:(map a Z))) = 0%Z).
Axiom Card_singleton : forall (a:Type), forall (x:a),
((card (set (empty_bag:(map a Z)) x 1%Z)) = 1%Z).
Axiom Card_union : forall (a:Type), forall (x:(map a Z)) (y:(map a Z)),
((card (union x y)) = ((card x) + (card y))%Z).
Axiom Card_zero_empty : forall (a:Type), forall (x:(map a Z)),
((card x) = 0%Z) -> (x = (empty_bag:(map a Z))).
Definition array (a:Type) := (map Z a).
Parameter elements: forall (a:Type), (map Z a) -> Z -> Z -> (map a Z).
Implicit Arguments elements.