Changeset 2309


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

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