The abstract of the Mizar article:

Binary Arithmetics

by

Takaya Nishiyama, and

Yasuho Mizuhara

Received October 8, 1993

MML identifier: BINARITH

[ Mizar article, MML identifier index ]

environ

 vocabulary MONOID_0, FUNCT_1, VECTSP_1, RELAT_1, MIDSP_3, FINSEQ_1, MARGREL1,
      ZF_LANG, ORDINAL2, ARYTM_1, CQC_LANG, POWER, SETWISEO, BOOLE, FINSEQ_2,
      BINARITH, FINSEQ_4, ARYTM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS,
      XCMPLX_0, XREAL_0, REAL_1, NAT_1, MARGREL1, RELAT_1, FUNCT_1, FUNCT_2,
      BINOP_1, MONOID_0, SETWOP_2, SERIES_1, VECTSP_1, CQC_LANG, FINSEQ_1,
      FINSEQ_2, FINSEQ_4, MIDSP_3;
 constructors REAL_1, NAT_1, MARGREL1, BINOP_1, MONOID_0, SETWISEO, SERIES_1,
      CQC_LANG, FINSOP_1, FINSEQ_4, MEMBERED, XBOOLE_0;
 clusters INT_1, FUNCT_1, RELSET_1, MARGREL1, NAT_1, MEMBERED, ZFMISC_1,
      XBOOLE_0, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

definition
  cluster non empty Nat;
end;

  theorem :: BINARITH:1
    for i,j being Nat holds addnat.(i,j) = i + j;

  theorem :: BINARITH:2
    for i,n being Nat,
        D being non empty set,
        d being Element of D,
        z being Tuple of n,D st i in Seg n holds
    (z^<*d*>)/.i=z/.i;

  theorem :: BINARITH:3
    for n being Nat,
        D being non empty set,
        d being Element of D,
        z being Tuple of n,D holds
    (z^<*d*>)/.(n+1)=d;

canceled;

  theorem :: BINARITH:5
     for i,n being Nat holds
      i in Seg n implies i is non empty;

  definition
    let x, y be boolean set;
    func x 'or' y equals
:: BINARITH:def 1

     'not'('not' x '&' 'not' y);
    commutativity;
  end;

  definition
    let x, y be boolean set;
    func x 'xor' y equals
:: BINARITH:def 2

     ('not' x '&' y) 'or' (x '&' 'not' y);
    commutativity;
  end;

  definition
    let x, y be boolean set;
    cluster x 'or' y -> boolean;
  end;

  definition
    let x, y be boolean set;
    cluster x 'xor' y -> boolean;
  end;

  definition
    let x, y be Element of BOOLEAN;
    redefine func x 'or' y -> Element of BOOLEAN;
    func x 'xor' y -> Element of BOOLEAN;
  end;

  reserve x,y,z for boolean set;

canceled;

  theorem :: BINARITH:7
  x 'or' FALSE = x;

canceled;

  theorem :: BINARITH:9
  'not' (x '&' y) = 'not' x 'or' 'not' y;

  theorem :: BINARITH:10
  'not' (x 'or' y) = 'not' x '&' 'not' y;

canceled;

  theorem :: BINARITH:12
    x '&' y = 'not' ('not' x 'or' 'not' y);

  theorem :: BINARITH:13
    TRUE 'xor' x = 'not' x;

  theorem :: BINARITH:14
    FALSE 'xor' x = x;

  theorem :: BINARITH:15
  x 'xor' x = FALSE;

  theorem :: BINARITH:16
  x '&' x = x;

  theorem :: BINARITH:17
  x 'xor' 'not' x = TRUE;

  theorem :: BINARITH:18
  x 'or' 'not' x = TRUE;

  theorem :: BINARITH:19
  x 'or' TRUE = TRUE;

  theorem :: BINARITH:20
  (x 'or' y) 'or' z = x 'or' (y 'or' z);

  theorem :: BINARITH:21
  x 'or' x = x;

  theorem :: BINARITH:22
  x '&' (y 'or' z) = x '&' y 'or' x '&' z;

  theorem :: BINARITH:23
  x 'or' y '&' z = (x 'or' y) '&' (x 'or' z);

  theorem :: BINARITH:24
    x 'or' x '&' y = x;

  theorem :: BINARITH:25
  x '&' (x 'or' y) = x;

  theorem :: BINARITH:26
  x 'or' 'not' x '&' y = x 'or' y;

  theorem :: BINARITH:27
    x '&' ('not' x 'or' y) = x '&' y;

canceled 5;

  theorem :: BINARITH:33
  TRUE 'xor' FALSE = TRUE;

  theorem :: BINARITH:34
  (x 'xor' y) 'xor' z = x 'xor' (y 'xor' z);

  theorem :: BINARITH:35
      x 'xor' 'not' x '&' y = x 'or' y;

  theorem :: BINARITH:36
      x 'or' (x 'xor' y) = x 'or' y;

  theorem :: BINARITH:37
      x 'or' ('not' x 'xor' y) = x 'or' 'not' y;

  theorem :: BINARITH:38
    x '&' (y 'xor' z) = (x '&' y) 'xor' (x '&' z);

  definition let i,j be natural number;
  func i -' j -> Nat equals
:: BINARITH:def 3
      i - j if i - j >= 0 otherwise 0;
  end;

  theorem :: BINARITH:39
  for i,j being natural number holds i + j -' j = i;

  reserve i,j,k for Nat;
  reserve n for non empty Nat;
  reserve x,y,z1,z2 for Tuple of n, BOOLEAN;

  definition let n be Nat, x be Tuple of n, BOOLEAN;
  func 'not' x -> Tuple of n, BOOLEAN means
:: BINARITH:def 4
      for i st i in Seg n holds it/.i = 'not' (x/.i);
 end;

  definition let n be non empty Nat, x, y be Tuple of n, BOOLEAN;
  func carry(x, y) -> Tuple of n, BOOLEAN means
:: BINARITH:def 5

    it/.1 = FALSE &
      for i st 1 <= i & i < n holds it/.(i+1) = (x/.i) '&' (y/.i) 'or'
        (x/.i) '&' (it/.i) 'or' (y/.i) '&' (it/.i);
  end;

  definition let n be Nat, x be Tuple of n, BOOLEAN;
  func Binary(x) -> Tuple of n, NAT means
:: BINARITH:def 6
    for i st i in Seg n holds
                  it/.i = IFEQ(x/.i,FALSE,0,2 to_power(i-'1));
   end;

  definition let n be Nat, x be Tuple of n, BOOLEAN;
  func Absval (x) -> Nat equals
:: BINARITH:def 7
  addnat $$ Binary (x);
  end;

  definition let n, x, y;
  func x + y -> Tuple of n, BOOLEAN means
:: BINARITH:def 8
    for i st i in Seg n holds it/.i =
                     (x/.i) 'xor' (y/.i) 'xor' (carry(x,y)/.i);
  end;

  definition let n,z1,z2;
  func add_ovfl(z1,z2) -> Element of BOOLEAN equals
:: BINARITH:def 9
     (z1/.n) '&' (z2/.n) 'or'
        (z1/.n) '&' (carry(z1,z2)/.n) 'or' (z2/.n) '&' (carry(z1,z2)/.n);
  end;

 scheme Ind_from_1 { P[Nat] } :
 for k being non empty Nat holds P[k]
   provided
    P[1] and
    for k being non empty Nat st P[k] holds P[k + 1];

definition let n,z1,z2;
  pred z1,z2 are_summable means
:: BINARITH:def 10
      add_ovfl(z1,z2) = FALSE;
end;

  theorem :: BINARITH:40
   for z1 being Tuple of 1,BOOLEAN holds
     z1= <*FALSE*> or z1=<*TRUE*>;

  theorem :: BINARITH:41
   for z1 being Tuple of 1,BOOLEAN holds
   z1=<*FALSE*> implies Absval(z1) = 0;

  theorem :: BINARITH:42
   for z1 being Tuple of 1,BOOLEAN holds
   z1=<*TRUE*> implies Absval(z1)=1;

  definition
    let n1 be non empty Nat;
    let n2 be Nat;
    let D  be non empty set;
    let z1 be Tuple of n1,D;
    let z2 be Tuple of n2,D;
    redefine func z1 ^ z2 -> Tuple of n1+n2,D;
  end;

  definition
    let D be non empty set;
    let d be Element of D;
    redefine func <* d *> -> Tuple of 1,D;
  end;

  theorem :: BINARITH:43
    for z1,z2 being Tuple of n,BOOLEAN holds
    for d1,d2 being Element of BOOLEAN holds
    for i being Nat holds
    i in Seg n implies
     carry(z1^<*d1*>,z2^<*d2*>)/.i = carry(z1,z2)/.i;

  theorem :: BINARITH:44
    for z1,z2 being Tuple of n,BOOLEAN,
              d1,d2 being Element of BOOLEAN holds
    add_ovfl(z1,z2) = carry(z1^<*d1*>,z2^<*d2*>)/.(n+1);

  theorem :: BINARITH:45
   for z1,z2 being Tuple of n,BOOLEAN,
             d1,d2 being Element of BOOLEAN holds
     z1^<*d1*> + z2^<*d2*> = (z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,z2)*>;

  theorem :: BINARITH:46
    for z being Tuple of n,BOOLEAN,
              d being Element of BOOLEAN holds
    Absval(z^<*d*>) = Absval(z)+IFEQ(d,FALSE,0,2 to_power n);

  theorem :: BINARITH:47
   for n for z1,z2 being Tuple of n,BOOLEAN holds
   Absval(z1+z2) + IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n)) =
                   Absval(z1) + Absval(z2);

  theorem :: BINARITH:48
      for z1,z2 being Tuple of n,BOOLEAN holds
    z1,z2 are_summable implies
    Absval(z1+z2) = Absval(z1) + Absval(z2);