:: Binary Arithmetics. Addition and Subtraction of Integers :: by Yasuho Mizuhara and Takaya Nishiyama :: :: Received March 18, 1994 :: Copyright (c) 1994-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, FINSEQ_2, MARGREL1, SUBSET_1, FINSEQ_1, PARTFUN1, RELAT_1, FUNCT_1, FUNCOP_1, XBOOLEAN, ARYTM_3, INT_1, BINARITH, ARYTM_1, POWER, ORDINAL4, CARD_1, TARSKI, BINOP_2, SETWISEO, BINARI_2, XCMPLX_0; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, NUMBERS, FUNCT_1, NAT_1, NAT_D, INT_1, PARTFUN1, BINOP_1, SETWOP_2, SERIES_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, BINOP_2, XBOOLEAN, MARGREL1, BINARITH; constructors PARTFUN1, BINOP_1, SETWISEO, XXREAL_0, NAT_1, INT_1, FINSEQ_4, FINSOP_1, SERIES_1, BINARITH, BINOP_2, NAT_D, RELSET_1, TREES_3, FUNCOP_1; registrations ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, BINOP_2, XBOOLEAN, MARGREL1, FINSEQ_2, CARD_1; requirements REAL, NUMERALS, SUBSET, ARITHM; begin reserve i,n for Nat; reserve m for non zero 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 zero 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 zero 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 zero 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; theorem :: BINARI_2:1 for z1 being Tuple of 2, BOOLEAN holds z1=<*FALSE*>^<*FALSE*> implies Intval(z1) = 0; theorem :: BINARI_2:2 for z1 being Tuple of 2, BOOLEAN holds z1=<*TRUE*>^<*FALSE*> implies Intval(z1) = 1; theorem :: BINARI_2:3 for z1 being Tuple of 2, BOOLEAN holds z1=<*FALSE*>^<*TRUE*> implies Intval(z1) = -2; theorem :: BINARI_2:4 for z1 being Tuple of 2, BOOLEAN holds z1=<*TRUE*>^<*TRUE*> implies Intval(z1) = -1; theorem :: BINARI_2:5 for i st i in Seg n & i = 1 holds (Bin1(n))/.i = TRUE; theorem :: BINARI_2:6 for i st i in Seg n & i <> 1 holds (Bin1(n))/.i = FALSE; theorem :: BINARI_2:7 Bin1 (m+1) = Bin1 (m)^<*FALSE*>; theorem :: BINARI_2:8 for m holds Intval (Bin1(m)^<*FALSE*>) = 1; theorem :: BINARI_2:9 for z being Tuple of m, BOOLEAN for d being Element of BOOLEAN holds 'not' (z^<* d *>) = 'not' z^<* 'not' d *>; theorem :: BINARI_2:10 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:11 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:12 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:13 for m for x being Tuple of m, BOOLEAN holds Absval('not' x) = - Absval(x) + 2 to_power m - 1; theorem :: BINARI_2:14 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:15 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:16 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 zero 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:17 for x,y being Tuple of m, BOOLEAN holds x - y = x + Neg2(y); theorem :: BINARI_2:18 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:19 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*>);