:: Binary Arithmetics. Addition and Subtraction of Integers
:: by Yasuho Mizuhara and Takaya Nishiyama
::
:: Received March 18, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

Lm1:  for n being Nat
for p, q being Tuple of n, BOOLEAN st len p = n & len q = n & ( for i being Nat st i in Seg n holds
p /. i = q /. i ) holds
p = q
proofend;

definition
let n be Nat;
func Bin1 n ->  Tuple of n, BOOLEAN  means :Def1: :: BINARI_2:def 1
 for i being Nat st i in Seg n holds
it /. i = IFEQ (i,1,TRUE,FALSE);
existence
 ex b1 being Tuple of n, BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = IFEQ (i,1,TRUE,FALSE)
proofend;
uniqueness
 for b1, b2 being Tuple of n, BOOLEAN st ( for i being Nat st i in Seg n holds
b1 /. i = IFEQ (i,1,TRUE,FALSE) ) & ( for i being Nat st i in Seg n holds
b2 /. i = IFEQ (i,1,TRUE,FALSE) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Bin1 BINARI_2:def_1_:_
 for n being Nat
for b2 being Tuple of n, BOOLEAN holds
( b2 = Bin1 n iff for i being Nat st i in Seg n holds
b2 /. i = IFEQ (i,1,TRUE,FALSE) );

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

:: deftheorem  defines Neg2 BINARI_2:def_2_:_
 for n being non empty Nat
for x being Tuple of n, BOOLEAN holds Neg2 x = ('not' x) + (Bin1 n);

definition
let n be Nat;
let x be Tuple of n, BOOLEAN ;
func Intval x ->  Integer equals :Def3: :: BINARI_2:def 3
 Absval x if x /. n = FALSE
otherwise (Absval x) - (2 to_power n);
correctness
coherence
( ( x /. n = FALSE implies Absval x is Integer ) & ( not x /. n = FALSE implies (Absval x) - (2 to_power n) is Integer ) );
consistency
for b1 being Integer holds verum;
;
end;

:: deftheorem Def3 defines Intval BINARI_2:def_3_:_
 for n being Nat
for x being Tuple of n, BOOLEAN holds
( ( x /. n = FALSE implies Intval x = Absval x ) & ( not x /. n = FALSE implies Intval x = (Absval x) - (2 to_power n) ) );

definition
let n be non empty Nat;
let 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);
correctness
coherence
(('not' (z1 /. n)) '&' ('not' (z2 /. n))) '&' ((carry (z1,z2)) /. n) is Element of BOOLEAN ;
;
end;

:: deftheorem  defines Int_add_ovfl BINARI_2:def_4_:_
 for n being non empty Nat
for z1, z2 being Tuple of n, BOOLEAN holds Int_add_ovfl (z1,z2) = (('not' (z1 /. n)) '&' ('not' (z2 /. n))) '&' ((carry (z1,z2)) /. n);

definition
let n be non empty Nat;
let 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));
correctness
coherence
((z1 /. n) '&' (z2 /. n)) '&' ('not' ((carry (z1,z2)) /. n)) is Element of BOOLEAN ;
;
end;

:: deftheorem  defines Int_add_udfl BINARI_2:def_5_:_
 for n being non empty Nat
for z1, z2 being Tuple of n, BOOLEAN holds Int_add_udfl (z1,z2) = ((z1 /. n) '&' (z2 /. n)) '&' ('not' ((carry (z1,z2)) /. n));

theorem :: BINARI_2:1
for z1 being Tuple of 2, BOOLEAN st z1 = <*FALSE*> ^ <*FALSE*> holds
Intval z1 = 0
proofend;

theorem Th2: :: BINARI_2:2
for z1 being Tuple of 2, BOOLEAN st z1 = <*TRUE*> ^ <*FALSE*> holds
Intval z1 = 1
proofend;

theorem :: BINARI_2:3
for z1 being Tuple of 2, BOOLEAN st z1 = <*FALSE*> ^ <*TRUE*> holds
Intval z1 = - 2
proofend;

theorem :: BINARI_2:4
for z1 being Tuple of 2, BOOLEAN st z1 = <*TRUE*> ^ <*TRUE*> holds
Intval z1 = - 1
proofend;

theorem Th5: :: BINARI_2:5
for n, i being Nat st i in Seg n &amp; i = 1 holds
(Bin1 n) /. i = TRUE
proofend;

theorem Th6: :: BINARI_2:6
for n, i being Nat st i in Seg n &amp; i <> 1 holds
(Bin1 n) /. i = FALSE
proofend;

theorem Th7: :: BINARI_2:7
for m being non empty Nat holds Bin1 (m + 1) = (Bin1 m) ^ <*FALSE*>
proofend;

theorem Th8: :: BINARI_2:8
for m being non empty Nat holds Intval ((Bin1 m) ^ <*FALSE*>) = 1
proofend;

theorem Th9: :: BINARI_2:9
for m being non empty Nat
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds 'not' (z ^ <*d*>) = ('not' z) ^ <*('not' d)*>
proofend;

theorem Th10: :: BINARI_2:10
for m being non empty Nat
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)))
proofend;

theorem Th11: :: BINARI_2:11
for m being non empty Nat
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*>))
proofend;

theorem Th12: :: BINARI_2:12
for m being non empty Nat
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))))
proofend;

theorem Th13: :: BINARI_2:13
for m being non empty Nat
for x being Tuple of m, BOOLEAN holds Absval ('not' x) = ((- (Absval x)) + (2 to_power m)) - 1
proofend;

theorem Th14: :: BINARI_2:14
for m being non empty Nat
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))))*>
proofend;

theorem Th15: :: BINARI_2:15
for m being non empty Nat
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*>))
proofend;

theorem :: BINARI_2:16
for m being non empty Nat
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds Neg2 (Neg2 (z ^ <*d*>)) = z ^ <*d*>
proofend;

definition
let n be non empty Nat;
let x, y be Tuple of n, BOOLEAN ;
funcx - y ->  Tuple of n, BOOLEAN  means :Def6: :: BINARI_2:def 6
 for i being Nat st i in Seg n holds
it /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i);
existence
 ex b1 being Tuple of n, BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i)
proofend;
uniqueness
 for b1, b2 being Tuple of n, BOOLEAN st ( for i being Nat st i in Seg n holds
b1 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i) ) &amp; ( for i being Nat st i in Seg n holds
b2 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines - BINARI_2:def_6_:_
 for n being non empty Nat
for x, y, b4 being Tuple of n, BOOLEAN holds
( b4 = x - y iff for i being Nat st i in Seg n holds
b4 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i) );

theorem Th17: :: BINARI_2:17
for m being non empty Nat
for x, y being Tuple of m, BOOLEAN holds x - y = x + (Neg2 y)
proofend;

theorem :: BINARI_2:18
for m being non empty Nat
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))))*>
proofend;

theorem :: BINARI_2:19
for m being non empty Nat
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*>))
proofend;