The abstract of the Mizar article:

Binary Arithmetics, Addition and Subtraction of Integers

by

Yasuho Mizuhara, and

Takaya Nishiyama

Received March 18, 1994

MML identifier: BINARI_2

[ Mizar article, MML identifier index ]

environ

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


begin

definition let X be non empty set; let D be non empty Subset of X;
 let x,y be set, a,b be Element of D;
 redefine func IFEQ(x,y,a,b) -> Element of D;
end;

 reserve i,j,n for Nat;
 reserve m for non empty Nat;
 reserve p,q for Tuple of n, BOOLEAN;
 reserve d,d1,d2 for Element of BOOLEAN;

definition let n be Nat;
  func Bin1 (n) -> Tuple of n, BOOLEAN means
:: BINARI_2:def 1
  for i st i in Seg n holds it/.i = IFEQ(i,1,TRUE,FALSE);
end;

definition let n be non empty Nat, x be Tuple of n, BOOLEAN;
  func Neg2 (x) -> Tuple of n,BOOLEAN equals
:: BINARI_2:def 2
   'not' x + Bin1 (n);
end;

definition let n be Nat, x be Tuple of n, BOOLEAN;
  func Intval (x) -> Integer equals
:: BINARI_2:def 3
   Absval (x) if x/.n = FALSE
    otherwise Absval (x) - 2 to_power n;
end;

definition let n be non empty Nat, z1,z2 be Tuple of n, BOOLEAN;
  func Int_add_ovfl(z1,z2) -> Element of BOOLEAN equals
:: BINARI_2:def 4
   'not' (z1/.n) '&' 'not' (z2/.n) '&' (carry(z1,z2)/.n);
end;

definition let n be non empty Nat, z1,z2 be Tuple of n, BOOLEAN;
  func Int_add_udfl(z1,z2) -> Element of BOOLEAN equals
:: BINARI_2:def 5
   (z1/.n) '&' (z2/.n) '&' 'not' (carry(z1,z2)/.n);
end;

canceled 2;

theorem :: BINARI_2:3
    for z1 being Tuple of 2, BOOLEAN holds
   z1=<*FALSE*>^<*FALSE*> implies Intval(z1) = 0;

theorem :: BINARI_2:4
  for z1 being Tuple of 2, BOOLEAN holds
   z1=<*TRUE*>^<*FALSE*> implies Intval(z1) = 1;

theorem :: BINARI_2:5
    for z1 being Tuple of 2, BOOLEAN holds
   z1=<*FALSE*>^<*TRUE*> implies Intval(z1) = -2;

theorem :: BINARI_2:6
    for z1 being Tuple of 2, BOOLEAN holds
   z1=<*TRUE*>^<*TRUE*> implies Intval(z1) = -1;

theorem :: BINARI_2:7
  for i st i in Seg n & i = 1 holds (Bin1(n))/.i = TRUE;

theorem :: BINARI_2:8
  for i st i in Seg n & i <> 1 holds (Bin1(n))/.i = FALSE;

theorem :: BINARI_2:9
  Bin1 (m+1) = Bin1 (m)^<*FALSE*>;

theorem :: BINARI_2:10
  for m holds Intval (Bin1(m)^<*FALSE*>) = 1;

theorem :: BINARI_2:11
  for z being Tuple of m, BOOLEAN
  for d being Element of BOOLEAN holds
  'not' (z^<* d *>) = 'not' z^<* 'not' d *>;

theorem :: BINARI_2:12
  for z being Tuple of m, BOOLEAN
  for d being Element of BOOLEAN holds
   Intval(z^<*d*>) = Absval(z)-(IFEQ(d,FALSE,0,2 to_power(m)) qua Nat);

theorem :: BINARI_2:13
  for z1,z2 being Tuple of m, BOOLEAN
  for d1,d2 being Element of BOOLEAN holds
   Intval(z1^<*d1*>+z2^<*d2*>)
            + IFEQ(Int_add_ovfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1))
            - IFEQ(Int_add_udfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1))
    = Intval(z1^<*d1*>) + Intval(z2^<*d2*>);

theorem :: BINARI_2:14
  for z1,z2 being Tuple of m, BOOLEAN
  for d1,d2 being Element of BOOLEAN holds
   Intval(z1^<*d1*>+z2^<*d2*>)
  = Intval(z1^<*d1*>) + Intval(z2^<*d2*>)
       - IFEQ(Int_add_ovfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1))
       + IFEQ(Int_add_udfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1));

theorem :: BINARI_2:15
  for m for x being Tuple of m, BOOLEAN holds
   Absval('not' x) = - Absval(x) + 2 to_power m - 1;

theorem :: BINARI_2:16
  for z being Tuple of m, BOOLEAN
   for d being Element of BOOLEAN holds
  Neg2(z^<*d*>) = Neg2(z)^<*'not' d 'xor' add_ovfl('not' z,Bin1(m))*>;

theorem :: BINARI_2:17
  for z being Tuple of m, BOOLEAN
   for d being Element of BOOLEAN holds
  Intval(Neg2(z^<*d*>))
       + IFEQ(Int_add_ovfl('not' (z^<*d*>),Bin1(m+1)),FALSE,0,2 to_power(m+1))
     = - Intval(z^<*d*>);

theorem :: BINARI_2:18
    for m for z being Tuple of m, BOOLEAN
        for d being Element of BOOLEAN holds
          Neg2(Neg2(z^<*d*>)) = z^<*d*>;

definition let n be non empty Nat, x, y be Tuple of n, BOOLEAN;
  func x - y -> Tuple of n, BOOLEAN means
:: BINARI_2:def 6
  for i st i in Seg n holds
    it/.i = (x/.i) 'xor' ((Neg2(y))/.i) 'xor' ((carry(x,Neg2(y)))/.i);
end;

theorem :: BINARI_2:19
  for x,y being Tuple of m, BOOLEAN holds x - y = x + Neg2(y);

theorem :: BINARI_2:20
    for z1,z2 being Tuple of m, BOOLEAN
   for d1,d2 being Element of BOOLEAN holds
     z1^<*d1*> - z2^<*d2*>
          = (z1 + Neg2(z2))^<*d1 'xor' 'not' d2 'xor' add_ovfl('not'
          z2,Bin1(m)) 'xor' add_ovfl(z1,Neg2(z2))*>;

theorem :: BINARI_2:21
    for z1,z2 being Tuple of m, BOOLEAN
        for d1,d2 being Element of BOOLEAN holds
  Intval(z1^<*d1*>-z2^<*d2*>)
  + IFEQ(Int_add_ovfl(z1^<*d1*>,Neg2(z2^<*d2*>)),FALSE,0,2 to_power(m+1))
  - IFEQ(Int_add_udfl(z1^<*d1*>,Neg2(z2^<*d2*>)),FALSE,0,2 to_power(m+1))
  + IFEQ(Int_add_ovfl('not' (z2^<*d2*>),Bin1(m+1)),FALSE,0,2 to_power(m+1))
    = Intval(z1^<*d1*>) - Intval(z2^<*d2*>);