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

begin

theorem :: BINARITH:1

canceled;

theorem Th2: :: BINARITH:2

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 Th3: :: BINARITH:3

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

canceled;

theorem :: BINARITH:5

canceled;

theorem :: BINARITH:6

canceled;

theorem :: BINARITH:7

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

theorem :: BINARITH:8

canceled;

theorem :: BINARITH:9

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

theorem :: BINARITH:10

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

theorem :: BINARITH:11

canceled;

theorem :: BINARITH:12

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

theorem :: BINARITH:13

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

theorem :: BINARITH:14

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

theorem :: BINARITH:15

canceled;

theorem :: BINARITH:16

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

theorem :: BINARITH:17

canceled;

theorem :: BINARITH:18

canceled;

theorem :: BINARITH:19

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

theorem :: BINARITH:20

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

theorem :: BINARITH:21

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

theorem :: BINARITH:22

canceled;

theorem :: BINARITH:23

canceled;

theorem :: BINARITH:24

canceled;

theorem :: BINARITH:25

canceled;

theorem :: BINARITH:26

canceled;

theorem :: BINARITH:27

canceled;

theorem :: BINARITH:28

canceled;

theorem :: BINARITH:29

canceled;

theorem :: BINARITH:30

canceled;

theorem :: BINARITH:31

canceled;

theorem :: BINARITH:32

canceled;

theorem :: BINARITH:33

TRUE 'xor' FALSE = TRUE ;

theorem :: BINARITH:34

canceled;

theorem :: BINARITH:35

canceled;

theorem :: BINARITH:36

canceled;

theorem :: BINARITH:37

canceled;

theorem :: BINARITH:38

canceled;

theorem :: BINARITH:39

canceled;

definition

canceled;
canceled;
canceled;
let n be Nat;
let x be Tuple of n, BOOLEAN ;
func 'not' x -> Tuple of n, BOOLEAN means :: BINARITH:def 4
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 BINARITH:def 1 :
canceled;

:: deftheorem BINARITH:def 2 :
canceled;

:: deftheorem BINARITH:def 3 :
canceled;

:: deftheorem defines 'not' BINARITH:def 4 :
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 empty Nat;
let x, y be Tuple of n, BOOLEAN ;
func carry (x,y) -> Tuple of n, BOOLEAN means :Def5: :: BINARITH:def 5
( 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 Def5 defines carry BINARITH:def 5 :
for n being non empty 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 :Def6: :: BINARITH:def 6
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 Def6 defines Binary BINARITH:def 6 :
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 7
addnat $$ (Binary x);
correctness
coherence
addnat $$ (Binary x) is Element of NAT ;
;

end;

:: deftheorem defines Absval BINARITH:def 7 :
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 :Def8: :: BINARITH:def 8
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 Def8 defines + BINARITH:def 8 :
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 9
(((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 9 :
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 :Def10: :: BINARITH:def 10
add_ovfl (z1,z2) = FALSE ;

end;

:: deftheorem Def10 defines are_summable BINARITH:def 10 :
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 Th40: :: BINARITH:40

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

proof end;

theorem Th41: :: BINARITH:41

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

proof end;

theorem Th42: :: BINARITH:42

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

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 Th43: :: BINARITH:43

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 Th44: :: BINARITH:44

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 Th45: :: BINARITH:45

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 Th46: :: BINARITH:46

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 Th47: :: BINARITH:47

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

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;