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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extralib.ma
r2178 r2309 46 46 47 47 (* bool *) 48 49 definition xorb : bool → bool → bool ≝ 50 λx,y. match x with [ false ⇒ y  true ⇒ notb y ]. 51 52 53 54 48 49 lemma xorb_neg : ∀a,b. notb (xorb a b) = xorb a (notb b). * * @refl qed. 50 lemma xorb_false : ∀a. xorb a false = a. * @refl qed. 51 lemma xorb_true : ∀a. xorb a true = (¬a). * @refl qed. 52 lemma xorb_comm : ∀a,b. xorb a b = xorb b a. * * @refl qed. 53 lemma xorb_assoc : ∀a,b,c. xorb a (xorb b c) = xorb (xorb a b) c. * * * @refl qed. 54 lemma xorb_lneg : ∀a,b. xorb (¬a) b = (¬xorb a b). * * @refl qed. 55 lemma xorb_rneg : ∀a,b. xorb a (¬b) = (¬xorb a b). * * @refl qed. 56 lemma xorb_inj : ∀a,b,c. xorb a b = xorb a c ↔ b = c. * * * @conj try // normalize try // qed. 57 58 59 55 60 (* should be proved in nat.ma, but it's not! *) 56 61 (* Paolo: there is eqb_elim which does something very similar *)
Note: See TracChangeset
for help on using the changeset viewer.