:: Binary Arithmetics. Addition :: by Takaya Nishiyama and Yasuho Mizuhara :: :: Received October 8, 1993 :: Copyright (c) 1993-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_2, FINSEQ_1, ORDINAL4, PARTFUN1, RELAT_1, ARYTM_3, CARD_1, MARGREL1, XBOOLEAN, XCMPLX_0, FUNCT_1, XXREAL_0, ARYTM_1, FUNCOP_1, POWER, BINOP_2, SETWISEO, REAL_1, BINARITH; notations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XBOOLEAN, MARGREL1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, BINOP_2, SETWISEO, FUNCOP_1, SETWOP_2, SERIES_1, FINSEQ_1, FINSEQ_2, XXREAL_0, NAT_1, NAT_D, TREES_3; constructors BINOP_1, SETWISEO, XXREAL_0, NAT_1, INT_1, BINOP_2, MARGREL1, PARTFUN1, FINSOP_1, SERIES_1, RFINSEQ, REAL_1, NAT_D, RELSET_1, FINSEQ_2, TREES_3, FUNCOP_1; registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2, XBOOLEAN, MARGREL1, FINSEQ_2, CARD_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin theorem :: BINARITH:1 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:2 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; definition let x, y be Element of BOOLEAN; redefine func x 'or' y -> Element of BOOLEAN; redefine func x 'xor' y -> Element of BOOLEAN; end; reserve x,y,z for boolean object; theorem :: BINARITH:3 x 'or' FALSE = x; theorem :: BINARITH:4 'not' (x '&' y) = 'not' x 'or' 'not' y; theorem :: BINARITH:5 'not' (x 'or' y) = 'not' x '&' 'not' y; theorem :: BINARITH:6 x '&' y = 'not' ('not' x 'or' 'not' y); theorem :: BINARITH:7 TRUE 'xor' x = 'not' x; theorem :: BINARITH:8 FALSE 'xor' x = x; theorem :: BINARITH:9 x '&' x = x; theorem :: BINARITH:10 x 'or' TRUE = TRUE; theorem :: BINARITH:11 (x 'or' y) 'or' z = x 'or' (y 'or' z); theorem :: BINARITH:12 x 'or' x = x; theorem :: BINARITH:13 TRUE 'xor' FALSE = TRUE; reserve i,j,k for Nat; reserve n for non zero 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 1 for i st i in Seg n holds it/.i = 'not' (x/.i); end; definition let n be non zero Nat, x, y be Tuple of n, BOOLEAN; func carry(x, y) -> Tuple of n, BOOLEAN means :: BINARITH:def 2 it/.1 = FALSE & for i being Nat 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 3 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) -> Element of NAT equals :: BINARITH:def 4 addnat $$ Binary (x); end; definition let n, x, y; func x + y -> Tuple of n, BOOLEAN means :: BINARITH:def 5 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 6 (z1/.n) '&' (z2/.n) 'or' ( z1/.n) '&' (carry(z1,z2)/.n) 'or' (z2/.n) '&' (carry(z1,z2)/.n); end; definition let n,z1,z2; pred z1,z2 are_summable means :: BINARITH:def 7 add_ovfl(z1,z2) = FALSE; end; theorem :: BINARITH:14 for z1 being Tuple of 1,BOOLEAN holds z1= <*FALSE*> or z1=<*TRUE *>; theorem :: BINARITH:15 for z1 being Tuple of 1,BOOLEAN holds z1=<*FALSE*> implies Absval(z1) = 0; theorem :: BINARITH:16 for z1 being Tuple of 1,BOOLEAN st z1=<*TRUE*> holds Absval(z1)= 1; definition let n1,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:17 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:18 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:19 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:20 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:21 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:22 for z1,z2 being Tuple of n,BOOLEAN st z1,z2 are_summable holds Absval( z1+z2) = Absval(z1) + Absval(z2);