Changeset 2309

Timestamp:

Aug 31, 2012, 11:35:25 AM (7 years ago)

Author:

garnier

Message:

Removed the superfluous xorb definition and move some basic properties of xorb to switchRemoval.ma to extralib.ma

File:

• src/utilities/extralib.ma (modified) (1 diff)

src/utilities/extralib.ma

@@ -46 +46 @@
 
 (* bool *)
-
-definition xorb : bool → bool → bool ≝
-  λx,y. match x with [ false ⇒ y | true ⇒ notb y ].
-  
-  
-  
-
+  
+lemma xorb_neg : ∀a,b. notb (xorb a b) = xorb a (notb b). * * @refl qed.
+lemma xorb_false : ∀a. xorb a false = a. * @refl qed.
+lemma xorb_true : ∀a. xorb a true = (¬a). * @refl qed.
+lemma xorb_comm : ∀a,b. xorb a b = xorb b a. * * @refl qed.
+lemma xorb_assoc : ∀a,b,c. xorb a (xorb b c) = xorb (xorb a b) c. * * * @refl qed.
+lemma xorb_lneg : ∀a,b. xorb (¬a) b = (¬xorb a b). * * @refl qed.
+lemma xorb_rneg : ∀a,b. xorb a (¬b) = (¬xorb a b). * * @refl qed.
+lemma xorb_inj : ∀a,b,c. xorb a b = xorb a c ↔ b = c. * * * @conj try // normalize try // qed.  
+  
+  
+  
 (* should be proved in nat.ma, but it's not! *)
 (* Paolo: there is eqb_elim which does something very similar *)