:: Binary Arithmetics. Addition
:: by Takaya Nishiyama and Yasuho Mizuhara
::
:: Received October 8, 1993
:: Copyright (c) 1993-2021 Association of Mizar Users

theorem Th1: :: BINARITH:1

for i, n being Nat
for D being non empty set
for d being Element of D
for z being Tuple of n,D st i in Seg n holds
(z ^ <*d*>) /. i = z /. i

proof end;

theorem Th2: :: BINARITH:2

for n being Nat
for D being non empty set
for d being Element of D
for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d

proof end;

definition

let x, y be Element of BOOLEAN ;
:: original: 'or'
redefine func x 'or' y -> Element of BOOLEAN ;
correctness
coherence
x 'or' y is Element of BOOLEAN ;

proof end;

:: original: 'xor'
redefine func x 'xor' y -> Element of BOOLEAN ;
correctness
coherence
x 'xor' y is Element of BOOLEAN ;

proof end;

end;

theorem :: BINARITH:3

for x being boolean object holds x 'or' FALSE = x ;

theorem :: BINARITH:4

for x, y being boolean object holds 'not' (x '&' y) = ('not' x) 'or' ('not' y) ;

theorem :: BINARITH:5

for x, y being boolean object holds 'not' (x 'or' y) = ('not' x) '&' ('not' y) ;

theorem :: BINARITH:6

for x, y being boolean object holds x '&' y = 'not' (('not' x) 'or' ('not' y)) ;

theorem :: BINARITH:7

for x being boolean object holds TRUE 'xor' x = 'not' x ;

theorem :: BINARITH:8

for x being boolean object holds FALSE 'xor' x = x ;

theorem :: BINARITH:9

for x being boolean object holds x '&' x = x ;

theorem :: BINARITH:10

for x being boolean object holds x 'or' TRUE = TRUE ;

theorem :: BINARITH:11

for x, y, z being boolean object holds (x 'or' y) 'or' z = x 'or' (y 'or' z) ;

theorem :: BINARITH:12

for x being boolean object holds x 'or' x = x ;

theorem :: BINARITH:13

TRUE 'xor' FALSE = TRUE ;

definition

let n be Nat;
let x be Tuple of n, BOOLEAN ;

func 'not' x -> Tuple of n, BOOLEAN means :: BINARITH:def 1
for i being Nat st i in Seg n holds
it /. i = 'not' (x /. i);

existence
ex b₁ being Tuple of n, BOOLEAN st
for i being Nat st i in Seg n holds
b₁ /. i = 'not' (x /. 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 = 'not' (x /. i) ) & ( for i being Nat st i in Seg n holds
b₂ /. i = 'not' (x /. i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines 'not' BINARITH:def 1 :
for n being Nat
for x, b₃ being Tuple of n, BOOLEAN holds
( b₃ = 'not' x iff for i being Nat st i in Seg n holds
b₃ /. i = 'not' (x /. i) );

definition

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

func carry (x,y) -> Tuple of n, BOOLEAN means :Def2: :: 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)) ) );

existence
ex b₁ being Tuple of n, BOOLEAN st
( b₁ /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
b₁ /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b₁ /. i))) 'or' ((y /. i) '&' (b₁ /. i)) ) )

proof end;

uniqueness
for b₁, b₂ being Tuple of n, BOOLEAN st b₁ /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
b₁ /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b₁ /. i))) 'or' ((y /. i) '&' (b₁ /. i)) ) & b₂ /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
b₂ /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b₂ /. i))) 'or' ((y /. i) '&' (b₂ /. i)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines carry BINARITH:def 2 :
for n being non zero Nat
for x, y, b₄ being Tuple of n, BOOLEAN holds
( b₄ = carry (x,y) iff ( b₄ /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
b₄ /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b₄ /. i))) 'or' ((y /. i) '&' (b₄ /. i)) ) ) );

definition

let n be Nat;
let x be Tuple of n, BOOLEAN ;

func Binary x -> Tuple of n, NAT means :Def3: :: BINARITH:def 3
for i being Nat st i in Seg n holds
it /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1)));

existence
ex b₁ being Tuple of n, NAT st
for i being Nat st i in Seg n holds
b₁ /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1)))

proof end;

uniqueness
for b₁, b₂ being Tuple of n, NAT st ( for i being Nat st i in Seg n holds
b₁ /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) ) & ( for i being Nat st i in Seg n holds
b₂ /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Binary BINARITH:def 3 :
for n being Nat
for x being Tuple of n, BOOLEAN
for b₃ being Tuple of n, NAT holds
( b₃ = Binary x iff for i being Nat st i in Seg n holds
b₃ /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) );

definition

let n be Nat;
let x be Tuple of n, BOOLEAN ;

func Absval x -> Element of NAT equals :: BINARITH:def 4
addnat $$ (Binary x);

correctness
coherence
addnat $$ (Binary x) is Element of NAT ;
;

end;

:: deftheorem defines Absval BINARITH:def 4 :
for n being Nat
for x being Tuple of n, BOOLEAN holds Absval x = addnat $$ (Binary x);

definition

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

func x + y -> Tuple of n, BOOLEAN means :Def5: :: BINARITH:def 5
for i being Nat st i in Seg n holds
it /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,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' (y /. i)) 'xor' ((carry (x,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' (y /. i)) 'xor' ((carry (x,y)) /. i) ) & ( for i being Nat st i in Seg n holds
b₂ /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines + BINARITH:def 5 :
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' (y /. i)) 'xor' ((carry (x,y)) /. i) );

definition

let n be non zero Nat;
let z1, z2 be Tuple of n, BOOLEAN ;

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));

correctness
coherence
(((z1 /. n) '&' (z2 /. n)) 'or' ((z1 /. n) '&' ((carry (z1,z2)) /. n))) 'or' ((z2 /. n) '&' ((carry (z1,z2)) /. n)) is Element of BOOLEAN ;
;

end;

:: deftheorem defines add_ovfl BINARITH:def 6 :
for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN holds add_ovfl (z1,z2) = (((z1 /. n) '&' (z2 /. n)) 'or' ((z1 /. n) '&' ((carry (z1,z2)) /. n))) 'or' ((z2 /. n) '&' ((carry (z1,z2)) /. n));

definition

let n be non zero Nat;
let z1, z2 be Tuple of n, BOOLEAN ;

pred z1,z2 are_summable means :: BINARITH:def 7
add_ovfl (z1,z2) = FALSE ;

end;

:: deftheorem defines are_summable BINARITH:def 7 :
for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN holds
( z1,z2 are_summable iff add_ovfl (z1,z2) = FALSE );

theorem Th14: :: BINARITH:14

for z1 being Tuple of 1, BOOLEAN holds
( z1 = <*FALSE*> or z1 = <*TRUE*> )

proof end;

theorem Th15: :: BINARITH:15

for z1 being Tuple of 1, BOOLEAN st z1 = <*FALSE*> holds
Absval z1 = 0

proof end;

theorem Th16: :: BINARITH:16

for z1 being Tuple of 1, BOOLEAN st z1 = <*TRUE*> holds
Absval z1 = 1

proof end;

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;
:: original: ^
redefine func z1 ^ z2 -> Tuple of n1 + n2,D;
coherence
z1 ^ z2 is Tuple of n1 + n2,D by FINSEQ_2:107;

end;

definition

let D be non empty set ;
let d be Element of D;
:: original: <*
redefine func <*d*> -> Tuple of 1,D;
coherence
<*d*> is Tuple of 1,D

proof end;

end;

theorem Th17: :: BINARITH:17

for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN
for d1, d2 being Element of BOOLEAN
for i being Nat st i in Seg n holds
(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i

proof end;

theorem Th18: :: BINARITH:18

for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN
for d1, d2 being Element of BOOLEAN holds add_ovfl (z1,z2) = (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (n + 1)

proof end;

theorem Th19: :: BINARITH:19

for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN
for d1, d2 being Element of BOOLEAN holds (z1 ^ <*d1*>) + (z2 ^ <*d2*>) = (z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>

proof end;

theorem Th20: :: BINARITH:20

for n being non zero Nat
for z being Tuple of n, BOOLEAN
for d being Element of BOOLEAN holds Absval (z ^ <*d*>) = (Absval z) + (IFEQ (d,FALSE,0,(2 to_power n)))

proof end;

theorem Th21: :: BINARITH:21

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

proof end;

theorem :: BINARITH:22

for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN st z1,z2 are_summable holds
Absval (z1 + z2) = (Absval z1) + (Absval z2)

proof end;