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


begin

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

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

definition
let x, y be Element of BOOLEAN ;
:: original:'or'
redefine funcx 'or' y ->  Element of BOOLEAN ;
correctness
coherence
x 'or' y is Element of BOOLEAN ;
proofend;
:: original:'xor'
redefine funcx 'xor' y ->  Element of BOOLEAN ;
correctness
coherence
x 'xor' y is Element of BOOLEAN ;
proofend;
end;

theorem :: BINARITH:3
for x being boolean set holds x 'or' FALSE = x ;

theorem :: BINARITH:4
for x, y being boolean set holds 'not' (x '&amp;' y) = ('not' x) 'or' ('not' y) ;

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

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

theorem :: BINARITH:7
for x being boolean set holds TRUE 'xor' x = 'not' x ;

theorem :: BINARITH:8
for x being boolean set holds FALSE 'xor' x = x ;

theorem :: BINARITH:9
for x being boolean set holds x '&amp;' x = x ;

theorem :: BINARITH:10
for x being boolean set holds x 'or' TRUE = TRUE ;

theorem :: BINARITH:11
for x, y, z being boolean set holds (x 'or' y) 'or' z = x 'or' (y 'or' z) ;

theorem :: BINARITH:12
for x being boolean set 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 b1 being Tuple of n, BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = 'not' (x /. i)
proofend;
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) ) &amp; ( for i being Nat st i in Seg n holds
b2 /. i = 'not' (x /. i) ) holds
b1 = b2
proofend;
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 empty 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 &amp; ( for i being Nat st 1 <= i &amp; i < n holds
it /. (i + 1) = (((x /. i) '&amp;' (y /. i)) 'or' ((x /. i) '&amp;' (it /. i))) 'or' ((y /. i) '&amp;' (it /. i)) ) );
existence
 ex b1 being Tuple of n, BOOLEAN st
( b1 /. 1 = FALSE &amp; ( for i being Nat st 1 <= i &amp; i < n holds
b1 /. (i + 1) = (((x /. i) '&amp;' (y /. i)) 'or' ((x /. i) '&amp;' (b1 /. i))) 'or' ((y /. i) '&amp;' (b1 /. i)) ) )
proofend;
uniqueness
 for b1, b2 being Tuple of n, BOOLEAN st b1 /. 1 = FALSE &amp; ( for i being Nat st 1 <= i &amp; i < n holds
b1 /. (i + 1) = (((x /. i) '&amp;' (y /. i)) 'or' ((x /. i) '&amp;' (b1 /. i))) 'or' ((y /. i) '&amp;' (b1 /. i)) ) &amp; b2 /. 1 = FALSE &amp; ( for i being Nat st 1 <= i &amp; i < n holds
b2 /. (i + 1) = (((x /. i) '&amp;' (y /. i)) 'or' ((x /. i) '&amp;' (b2 /. i))) 'or' ((y /. i) '&amp;' (b2 /. i)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines carry BINARITH:def_2_:_
 for n being non empty Nat
for x, y, b4 being Tuple of n, BOOLEAN holds
( b4 = carry (x,y) iff ( b4 /. 1 = FALSE &amp; ( for i being Nat st 1 <= i &amp; i < n holds
b4 /. (i + 1) = (((x /. i) '&amp;' (y /. i)) 'or' ((x /. i) '&amp;' (b4 /. i))) 'or' ((y /. i) '&amp;' (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)))
proofend;
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))) ) &amp; ( 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
proofend;
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 $$ (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 ;
funcx + 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)
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' (y /. i)) 'xor' ((carry (x,y)) /. i) ) &amp; ( 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
proofend;
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) '&amp;' (z2 /. n)) 'or' ((z1 /. n) '&amp;' ((carry (z1,z2)) /. n))) 'or' ((z2 /. n) '&amp;' ((carry (z1,z2)) /. n));
correctness
coherence
(((z1 /. n) '&amp;' (z2 /. n)) 'or' ((z1 /. n) '&amp;' ((carry (z1,z2)) /. n))) 'or' ((z2 /. n) '&amp;' ((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) '&amp;' (z2 /. n)) 'or' ((z1 /. n) '&amp;' ((carry (z1,z2)) /. n))) 'or' ((z2 /. n) '&amp;' ((carry (z1,z2)) /. n));

definition
let n be non zero Nat;
let z1, z2 be Tuple of n, BOOLEAN ;
predz1,z2 are_summable  means :Def7: :: BINARITH:def 7
 add_ovfl (z1,z2) = FALSE ;
end;

:: deftheorem Def7 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*> )
proofend;

theorem Th15: :: BINARITH:15
for z1 being Tuple of 1, BOOLEAN st z1 = <*FALSE*> holds
Absval z1 = 0
proofend;

theorem Th16: :: BINARITH:16
for z1 being Tuple of 1, BOOLEAN st z1 = <*TRUE*> holds
Absval z1 = 1
proofend;

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 funcz1 ^ 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
proofend;
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
proofend;

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

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

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

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

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