added two new ops in settheory, updated realizations.

Makefile.in

@@ -932,12 +932,24 @@ depend: $(COQVD)
 clean::
 	rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
 
-update-coq: bin/why3 drivers/coq-realizations.aux
+update-coq: update-coq-int update-coq-real update-coq-number update-coq-set update-coq-settheory update-coq-fp
+
+update-coq-int: bin/why3 drivers/coq-realizations.aux theories/int.why
 	for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
+
+update-coq-real: bin/why3 drivers/coq-realizations.aux theories/real.why
 	for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
+
+update-coq-number: bin/why3 drivers/coq-realizations.aux theories/number.why
 	for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
+
+update-coq-set: bin/why3 drivers/coq-realizations.aux theories/set.why
 	for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done
+
+update-coq-settheory: bin/why3 drivers/coq-realizations.aux theories/settheory.why
 	for f in $(COQLIBS_SETTHEORY_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T settheory.$$f -o lib/coq/settheory/; done
+
+update-coq-fp: bin/why3 drivers/coq-realizations.aux theories/floating_point.why
 	for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
 
 else

lib/coq/floating_point/Double.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require Import Rbasic_fun.

lib/coq/floating_point/DoubleFormat.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/floating_point/Rounding.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/floating_point/Single.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require Import Rbasic_fun.

lib/coq/floating_point/SingleFormat.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/int/Abs.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/int/ComputerDivision.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require Import ZOdiv.

lib/coq/int/Div2.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/int/EuclideanDivision.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/int/Exponentiation.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/int/Int.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/int/MinMax.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/int/Power.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/number/Divisibility.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require Import ZOdiv.

lib/coq/number/Gcd.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require Import ZOdiv.

lib/coq/number/Parity.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/number/Prime.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require Import ZOdiv.

lib/coq/real/Abs.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require Import Rbasic_fun.

lib/coq/real/ExpLog.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require Import Rtrigo_def.

lib/coq/real/FromInt.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/real/MinMax.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/real/PowerInt.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require Import Rfunctions.

lib/coq/real/Real.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/real/RealInfix.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/real/Square.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require Import R_sqrt.

lib/coq/set/Set.v

@@ -82,6 +82,13 @@ intros a a_WT.
 unfold is_empty; intuition.
 Qed.
 
+(* Why3 goal *)
+Lemma mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
+  (empty :(set a))).
+intros a a_WT x.
+auto.
+Qed.
+
 (* Why3 goal *)
 Definition add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
 intros a a_WT x s.

lib/coq/settheory/Function.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.
@@ -114,12 +114,10 @@ Lemma mem_total_functions : forall {a:Type} {a_WT:WhyType a}
   {b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
   (s:(set.Set.set a)) (t:(set.Set.set b)), (set.Set.mem f (infix_mnmngt s
   t)) <-> ((set.Set.mem f (infix_plmngt s t)) /\
-  (set.Set.infix_eqeq (settheory.InverseDomRan.dom f) s)).
+  ((settheory.InverseDomRan.dom f) = s)).
 intros a a_WT b b_WT f s t.
 unfold infix_mnmngt, mem.
 intuition.
-now subst s.
-apply predicate_extensionality; assumption.
 Qed.
 
 (* Why3 goal *)
@@ -132,6 +130,36 @@ unfold infix_mnmngt, mem in h1.
 unfold mem; tauto.
 Qed.
 
+(* Why3 goal *)
+Lemma singleton_is_function : forall {a:Type} {a_WT:WhyType a}
+  {b:Type} {b_WT:WhyType b}, forall (x:a) (y:b), (set.Set.mem (set.Set.add (
+  x, y) (set.Set.empty :(set.Set.set (a* b)%type)))
+  (infix_mnmngt (set.Set.add x (set.Set.empty :(set.Set.set a)))
+  (set.Set.add y (set.Set.empty :(set.Set.set b))))).
+intros a a_WT b b_WT x y.
+rewrite mem_total_functions.
+split.
+
+rewrite mem_function.
+split.
+
+intros x' y'.
+repeat rewrite set.Set.add_def1.
+(*
+repeat rewrite set.Set.mem_empty.
+Anomaly: unknown meta ?1230. Please report.
+*)
+intuition; inversion H0; auto.
+
+intros x0 y1 y2.
+repeat rewrite set.Set.add_def1.
+intuition; inversion H; inversion H0; auto.
+
+rewrite dom_add.
+rewrite dom_empty; auto.
+
+Qed.
+
 Require Import ClassicalEpsilon.
 
 (* Why3 goal *)
@@ -143,14 +171,16 @@ exact (epsilon i (fun y:b => mem x (dom f) -> mem (x,y) f)).
 Defined.
 
 (* Why3 goal *)
-Lemma apply_def1 : forall {a:Type} {a_WT:WhyType a}
+Lemma apply_def0 : forall {a:Type} {a_WT:WhyType a}
   {b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
-  (s:(set.Set.set a)) (t:(set.Set.set b)) (a1:a), ((set.Set.mem a1 s) /\
-  (set.Set.mem f (infix_mnmngt s t))) -> (set.Set.mem (a1, (apply f a1)) f).
-intros a a_WT b b_WT f s t a1 (h1 & h2 & h3).
+  (s:(set.Set.set a)) (t:(set.Set.set b)) (a1:a), ((set.Set.mem f
+  (infix_plmngt s t)) /\ (set.Set.mem a1 (settheory.InverseDomRan.dom f))) ->
+  (set.Set.mem (a1, (apply f a1)) f).
+intros a a_WT b b_WT f s t a1 (h1,h2).
 unfold apply.
 unfold mem.
-cut (dom f a1). 
+unfold mem in h2.
+generalize h2.
 apply epsilon_spec.
 destruct (classic (dom f a1)).
 destruct H as (x, h).
@@ -159,25 +189,37 @@ intro.
 apply h.
 exists b_WT.
 tauto.
-rewrite h3.
-now apply h1.
+Qed.
+
+(* Why3 goal *)
+Lemma apply_def1 : forall {a:Type} {a_WT:WhyType a}
+  {b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
+  (s:(set.Set.set a)) (t:(set.Set.set b)) (a1:a), ((set.Set.mem f
+  (infix_mnmngt s t)) /\ (set.Set.mem a1 s)) -> (set.Set.mem (a1, (apply f
+  a1)) f).
+intros a a_WT b b_WT f s t a1 (h1 & h2).
+eapply apply_def0.
+split.
+apply total_function_is_function; eauto.
+destruct h1.
+subst s; auto.
 Qed.
 
 (* Why3 goal *)
 Lemma apply_def2 : forall {a:Type} {a_WT:WhyType a}
   {b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
   (s:(set.Set.set a)) (t:(set.Set.set b)) (a1:a) (b1:b), ((set.Set.mem f
-  (infix_mnmngt s t)) /\ (set.Set.mem (a1, b1) f)) -> (b1 = (apply f a1)).
+  (infix_plmngt s t)) /\ (set.Set.mem (a1, b1) f)) -> ((apply f a1) = b1).
 intros a a_WT b b_WT f s t a1 b1 (h1,h2).
-generalize h1; intros (h3 & h4).
-destruct h3 as (h5 & h6 & h7).
-apply h7 with a1.
+generalize h1; intro h1'.
+rewrite mem_function in h1.
+destruct h1 as (_ & h).
+apply h with (x:=a1).
 split; auto.
-apply apply_def1 with s t.
-split; auto.
-rewrite <- h4.
-unfold dom, mem.
-now exists b1.
+eapply apply_def0; split.
+eauto.
+rewrite dom_def.
+exists b1; auto.
 Qed.
 
 (* Why3 goal *)
@@ -198,4 +240,87 @@ unfold inverse, mem.
 apply apply_def1 with s t; tauto.
 Qed.
 
+(* Why3 goal *)
+Lemma apply_singleton : forall {a:Type} {a_WT:WhyType a}
+  {b:Type} {b_WT:WhyType b}, forall (x:a) (y:b), ((apply (set.Set.add (x, y)
+  (set.Set.empty :(set.Set.set (a* b)%type))) x) = y).
+intros a a_WT b b_WT x y.
+rewrite apply_def2 with (s:=(add x empty)) 
+  (t:=(add y empty)) (b1 := y); auto.
+split.
+apply total_function_is_function.
+apply singleton_is_function.
+apply add_def1; auto.
+Qed.
+
+(* Why3 goal *)
+Definition semicolon: forall {a:Type} {a_WT:WhyType a}
+  {b:Type} {b_WT:WhyType b} {c:Type} {c_WT:WhyType c}, (set.Set.set (a*
+  b)%type) -> (set.Set.set (b* c)%type) -> (set.Set.set (a* c)%type).
+intros a a_WT b b_WT c c_WT f g.
+exact (fun p => match p with 
+  (x,z) => exists y:b, f (x,y) /\ g (y,z) end).
+Defined.
+
+(* Why3 goal *)
+Lemma semicolon_def : forall {a:Type} {a_WT:WhyType a}
+  {b:Type} {b_WT:WhyType b} {c:Type} {c_WT:WhyType c}, forall (x:a) (z:c)
+  (p:(set.Set.set (a* b)%type)) (q:(set.Set.set (b* c)%type)), (set.Set.mem (
+  x, z) (semicolon p q)) <-> exists y:b, (set.Set.mem (x, y) p) /\
+  (set.Set.mem (y, z) q).
+intros a a_WT b b_WT c c_WT x z p q.
+tauto.
+Qed.
+
+(* Why3 goal *)
+Lemma semicolon_is_function : forall {a:Type} {a_WT:WhyType a}
+  {b:Type} {b_WT:WhyType b} {c:Type} {c_WT:WhyType c}, forall (f:(set.Set.set
+  (a* b)%type)) (g:(set.Set.set (b* c)%type)) (s:(set.Set.set a))
+  (t:(set.Set.set b)) (u:(set.Set.set c)), ((set.Set.mem f (infix_plmngt s
+  t)) /\ (set.Set.mem g (infix_plmngt t u))) -> (set.Set.mem (semicolon f g)
+  (infix_plmngt s u)).
+intros a a_WT b b_WT c c_WT f g s t u ((f1&f2&f3),(g1&g2&g3)).
+rewrite mem_function.
+split.
+intros x z (y & h1 & h2).
+split.
+apply f1; exists y; auto.
+apply g2; exists y; auto.
+intros x y1 y2 ((h1&h2&h3)&(i1&i2&i3)).
+eapply g3.
+split. apply h3.
+assert (h1=i1).
+eapply f3.
+split. apply h2. apply i2.
+subst i1.
+apply i3.
+Qed.
+
+(* Why3 goal *)
+Lemma apply_compose : forall {a:Type} {a_WT:WhyType a}
+  {b:Type} {b_WT:WhyType b} {c:Type} {c_WT:WhyType c}, forall (x:a)
+  (f:(set.Set.set (a* b)%type)) (g:(set.Set.set (b* c)%type)) (s:(set.Set.set
+  a)) (t:(set.Set.set b)) (u:(set.Set.set c)), ((set.Set.mem f
+  (infix_plmngt s t)) /\ ((set.Set.mem g (infix_plmngt t u)) /\
+  ((set.Set.mem x (settheory.InverseDomRan.dom f)) /\ (set.Set.mem (apply f
+  x) (settheory.InverseDomRan.dom g))))) -> ((apply (semicolon f g)
+  x) = (apply g (apply f x))).
+intros a a_WT b b_WT c c_WT x f g s t u (h1 & h2 & h3 & h4).
+eapply apply_def2.
+split.
+eapply semicolon_is_function.
+split; eauto.
+rewrite semicolon_def.
+exists (apply f x).
+split.
+eapply apply_def0.
+split.
+eauto.
+assumption.
+eapply apply_def0.
+split.
+eauto.
+assumption.
+Qed.
+
 

lib/coq/settheory/Identity.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/settheory/Image.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/settheory/Interval.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.
@@ -59,3 +59,8 @@ unfold mk, add, mem; intuition; omega.
 Qed.
 
 
+(* Unused content named mem_interval_1
+intros x a b (h1,h2).
+
+Qed.
+ *)

lib/coq/settheory/InverseDomRan.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.
@@ -54,4 +54,38 @@ intros a a_WT b b_WT r y.
 unfold ran; intuition.
 Qed.
 
+(* Why3 goal *)
+Lemma dom_empty : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  ((dom (set.Set.empty :(set.Set.set (a*
+  b)%type))) = (set.Set.empty :(set.Set.set a))).
+intros a a_WT b b_WT.
+apply extensionality; intro x.
+rewrite dom_def.
+split.
+intros (y,h); auto.
+unfold mem, empty; intuition.
+Qed.
+
+(* Why3 goal *)
+Lemma dom_add : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  forall (f:(set.Set.set (a* b)%type)) (x:a) (y:b), ((dom (set.Set.add (x, y)
+  f)) = (set.Set.add x (dom f))).
+intros a a_WT b b_WT f x y.
+apply extensionality.
+intro z.
+rewrite add_def1.
+do 2 rewrite dom_def.
+split.
+intro H; destruct H.
+rewrite add_def1 in H.
+destruct H.
+inversion H; intuition.
+right; exists x0; auto.
+intro H; destruct H.
+subst z.
+exists y; rewrite add_def1; auto.
+destruct H.
+exists x0; rewrite add_def1; auto.
+Qed.
+
 

lib/coq/settheory/PowerSet.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

lib/coq/settheory/Relation.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq-realize driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.

theories/set.why

@@ -32,6 +32,8 @@ theory SetGen
 
   axiom empty_def1: is_empty (empty : set 'a)
 
+  lemma mem_empty: forall x:'a. mem x empty <-> false
+
   (** addition *)
   function add 'a (set 'a) : set 'a
 

theories/settheory.why

@@ -78,30 +78,23 @@ theory Relation
 
 end
 
-(** {2 Image}
+(** {2 Composition}
 
-Image by a relation
+Composition of relations
 
 *)
 
-theory Image
-
-  use export Relation
+theory Composition
 
-  function image (r : rel 'a 'b) (dom : set 'a) : set 'b
+  use import Relation
 
-  axiom mem_image:
-    forall r : rel 'a 'b, dom : set 'a, y : 'b [mem y (image r dom)].
-    mem y (image r dom) <-> exists x: 'a. mem x dom /\ mem (x,y) r
+  function semicolon (rel 'a 'b) (rel 'b 'c) : (rel 'a 'c)
 
-  lemma image_union:
-    forall r : rel 'a 'b, s t: set 'a.
-    image r (union s t) = union (image r s) (image r t)
+  axiom semicolon_def:
+    forall x:'a, z:'c, p:rel 'a 'b, q:rel 'b 'c.
+    mem (x,z) (semicolon p q) <->
+      exists y:'b. mem (x,y) p /\ mem (y,z) q
 
-  lemma image_add:
-    forall r : rel 'a 'b, dom : set 'a, x:'a.
-    image r (add x dom) = union (image r (singleton x))
-                                        (image r dom)
 end
 
 (** {2 Domain, Range, Inverse} 
@@ -132,8 +125,44 @@ theory InverseDomRan
     forall r : rel 'a 'b. forall y : 'b.
       mem y (ran r) <-> exists x : 'a. mem (x,y) r
 
+  lemma dom_empty:
+    dom (empty : rel 'a 'b) = (empty : set 'a)
+
+  lemma dom_add:
+    forall f:rel 'a 'b, x:'a, y:'b.
+      dom (add (x,y) f) = add x (dom f) 
+
 end
 
+(** {2 Image}
+
+Image by a relation
+
+*)
+
+theory Image
+
+  use export Relation
+
+  function image (r : rel 'a 'b) (dom : set 'a) : set 'b
+
+  axiom mem_image:
+    forall r : rel 'a 'b, dom : set 'a, y : 'b [mem y (image r dom)].
+    mem y (image r dom) <-> exists x: 'a. mem x dom /\ mem (x,y) r
+
+  lemma image_union:
+    forall r : rel 'a 'b, s t: set 'a.
+    image r (union s t) = union (image r s) (image r t)
+
+  lemma image_add:
+    forall r : rel 'a 'b, dom : set 'a, x:'a.
+    image r (add x dom) = union (image r (singleton x))
+                                        (image r dom)
+end
+
+
+
+
 (** {2 Functions}
 
 Partial functions as relations
@@ -183,21 +212,29 @@ theory Function
 
   axiom mem_total_functions:
     forall f:rel 'a 'b, s:set 'a, t:set 'b.
-      mem f (s --> t) <-> mem f (s +-> t) /\ dom f == s
+      mem f (s --> t) <-> mem f (s +-> t) /\ dom f = s
 
   lemma total_function_is_fun