:: 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

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

proof end;

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 b₁ being Tuple of n, BOOLEAN st
for i being Nat st i in Seg n holds
b₁ /. i = IFEQ (i,1,TRUE,FALSE)

proof end;

uniqueness
for b₁, b₂ being Tuple of n, BOOLEAN st ( for i being Nat st i in Seg n holds
b₁ /. i = IFEQ (i,1,TRUE,FALSE) ) & ( for i being Nat st i in Seg n holds
b₂ /. i = IFEQ (i,1,TRUE,FALSE) ) holds
b₁ = b₂

proof end;

end;

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

definition

let n be non zero 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 zero 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 b₁ 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 zero 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 zero 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 zero 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 zero 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

proof end;

theorem Th2: :: BINARI_2:2

for z1 being Tuple of 2, BOOLEAN st z1 = <*TRUE*> ^ <*FALSE*> holds
Intval z1 = 1

proof end;

theorem :: BINARI_2:3

for z1 being Tuple of 2, BOOLEAN st z1 = <*FALSE*> ^ <*TRUE*> holds
Intval z1 = - 2

proof end;

theorem :: BINARI_2:4

for z1 being Tuple of 2, BOOLEAN st z1 = <*TRUE*> ^ <*TRUE*> holds
Intval z1 = - 1

proof end;

theorem Th5: :: BINARI_2:5

for n, i being Nat st i in Seg n & i = 1 holds
(Bin1 n) /. i = TRUE

proof end;

theorem Th6: :: BINARI_2:6

for n, i being Nat st i in Seg n & i <> 1 holds
(Bin1 n) /. i = FALSE

proof end;

theorem Th7: :: BINARI_2:7

for m being non zero Nat holds Bin1 (m + 1) = (Bin1 m) ^ <*FALSE*>

proof end;

theorem Th8: :: BINARI_2:8

for m being non zero Nat holds Intval ((Bin1 m) ^ <*FALSE*>) = 1

proof end;

theorem Th9: :: BINARI_2:9

for m being non zero Nat
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds 'not' (z ^ <*d*>) = ('not' z) ^ <*('not' d)*>

proof end;

theorem Th10: :: BINARI_2:10

for m being non zero 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)))

proof end;

theorem Th11: :: BINARI_2:11

for m being non zero 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*>))

proof end;

theorem Th12: :: BINARI_2:12

for m being non zero 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))))

proof end;

theorem Th13: :: BINARI_2:13

for m being non zero Nat
for x being Tuple of m, BOOLEAN holds Absval ('not' x) = ((- (Absval x)) + (2 to_power m)) - 1

proof end;

theorem Th14: :: BINARI_2:14

for m being non zero 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))))*>

proof end;

theorem Th15: :: BINARI_2:15

for m being non zero 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*>))

proof end;

theorem :: BINARI_2:16

for m being non zero Nat
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds Neg2 (Neg2 (z ^ <*d*>)) = z ^ <*d*>

proof end;

definition

let n be non zero Nat;
let x, y be Tuple of n, BOOLEAN ;

func x - 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 b₁ being Tuple of n, BOOLEAN st
for i being Nat st i in Seg n holds
b₁ /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i)

proof end;

uniqueness
for b₁, b₂ being Tuple of n, BOOLEAN st ( for i being Nat st i in Seg n holds
b₁ /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i) ) & ( for i being Nat st i in Seg n holds
b₂ /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines - BINARI_2:def 6 :
for n being non zero Nat
for x, y, b₄ being Tuple of n, BOOLEAN holds
( b₄ = x - y iff for i being Nat st i in Seg n holds
b₄ /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i) );

theorem Th17: :: BINARI_2:17

for m being non zero Nat
for x, y being Tuple of m, BOOLEAN holds x - y = x + (Neg2 y)

proof end;

theorem :: BINARI_2:18

for m being non zero 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))))*>

proof end;

theorem :: BINARI_2:19

for m being non zero 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*>))

proof end;