:: by Takaya Nishiyama and Yasuho Mizuhara
::
:: Copyright (c) 1993-2019 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) = () 'or' () ;

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

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

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

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 b1 being Tuple of n, BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = 'not' (x /. i)
proof end;
uniqueness
for b1, b2 being Tuple of n, BOOLEAN st ( for i being Nat st i in Seg n holds
b1 /. i = 'not' (x /. i) ) & ( for i being Nat st i in Seg n holds
b2 /. i = 'not' (x /. i) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines 'not' BINARITH:def 1 :
for n being Nat
for x, b3 being Tuple of n, BOOLEAN holds
( b3 = 'not' x iff for i being Nat st i in Seg n holds
b3 /. 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 b1 being Tuple of n, BOOLEAN st
( b1 /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
b1 /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b1 /. i))) 'or' ((y /. i) '&' (b1 /. i)) ) )
proof end;
uniqueness
for b1, b2 being Tuple of n, BOOLEAN st b1 /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
b1 /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b1 /. i))) 'or' ((y /. i) '&' (b1 /. i)) ) & b2 /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
b2 /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b2 /. i))) 'or' ((y /. i) '&' (b2 /. i)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines carry BINARITH:def 2 :
for n being non zero Nat
for x, y, b4 being Tuple of n, BOOLEAN holds
( b4 = carry (x,y) iff ( b4 /. 1 = FALSE & ( for i being Nat st 1 <= i & i < n holds
b4 /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (b4 /. i))) 'or' ((y /. i) '&' (b4 /. 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 b1 being Tuple of n, NAT st
for i being Nat st i in Seg n holds
b1 /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1)))
proof end;
uniqueness
for b1, b2 being Tuple of n, NAT st ( for i being Nat st i in Seg n holds
b1 /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) ) & ( for i being Nat st i in Seg n holds
b2 /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Binary BINARITH:def 3 :
for n being Nat
for x being Tuple of n, BOOLEAN
for b3 being Tuple of n, NAT holds
( b3 = Binary x iff for i being Nat st i in Seg n holds
b3 /. 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 $$(); correctness coherence addnat$$ () 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  ();

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 b1 being Tuple of n, BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i)
proof end;
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' (y /. i)) 'xor' ((carry (x,y)) /. i) ) & ( for i being Nat st i in Seg n holds
b2 /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines + BINARITH:def 5 :
for n being non zero 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' (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
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 = or z1 = )
proof end;

theorem Th15: :: BINARITH:15
for z1 being Tuple of 1, BOOLEAN st z1 = holds
Absval z1 = 0
proof end;

theorem Th16: :: BINARITH:16
for z1 being Tuple of 1, BOOLEAN st z1 = 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*>) = () + (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;