BINARITH: Binary Arithmetics. Addition

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

proof end;

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines 'not' BINARITH:def 1 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines carry BINARITH:def 2 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Binary BINARITH:def 3 :

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 ;

end;

:: deftheorem defines Absval BINARITH:def 4 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines + BINARITH:def 5 :

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 ;

end;

:: deftheorem defines add_ovfl BINARITH:def 6 :

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 :

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

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;