:: Binary Arithmetics. Addition and Subtraction of Integers
:: by Yasuho Mizuhara and Takaya Nishiyama
::
:: Copyright (c) 1994-2018 Association of Mizar Users

Lm1: for n being Nat
for p, q being Tuple of n, BOOLEAN st len p = n & len q = n & ( for i being Nat st i in Seg n holds
p /. i = q /. i ) holds
p = q

proof end;

definition
let n be Nat;
func Bin1 n -> Tuple of n, BOOLEAN means :Def1: :: BINARI_2:def 1
for i being Nat st i in Seg n holds
it /. i = IFEQ (i,1,TRUE,FALSE);
existence
ex b1 being Tuple of n, BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = IFEQ (i,1,TRUE,FALSE)
proof end;
uniqueness
for b1, b2 being Tuple of n, BOOLEAN st ( for i being Nat st i in Seg n holds
b1 /. i = IFEQ (i,1,TRUE,FALSE) ) & ( for i being Nat st i in Seg n holds
b2 /. i = IFEQ (i,1,TRUE,FALSE) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Bin1 BINARI_2:def 1 :
for n being Nat
for b2 being Tuple of n, BOOLEAN holds
( b2 = Bin1 n iff for i being Nat st i in Seg n holds
b2 /. i = IFEQ (i,1,TRUE,FALSE) );

definition
let n be non zero Nat;
let x be Tuple of n, BOOLEAN ;
func Neg2 x -> Tuple of n, BOOLEAN equals :: BINARI_2:def 2
() + (Bin1 n);
correctness
coherence
() + (Bin1 n) is Tuple of n, BOOLEAN
;
;
end;

:: deftheorem defines Neg2 BINARI_2:def 2 :
for n being non zero Nat
for x being Tuple of n, BOOLEAN holds Neg2 x = () + (Bin1 n);

definition
let n be Nat;
let x be Tuple of n, BOOLEAN ;
func Intval x -> Integer equals :Def3: :: BINARI_2:def 3
Absval x if x /. n = FALSE
otherwise () - (2 to_power n);
correctness
coherence
( ( x /. n = FALSE implies Absval x is Integer ) & ( not x /. n = FALSE implies () - (2 to_power n) is Integer ) )
;
consistency
for b1 being Integer holds verum
;
;
end;

:: deftheorem Def3 defines Intval BINARI_2:def 3 :
for n being Nat
for x being Tuple of n, BOOLEAN holds
( ( x /. n = FALSE implies Intval x = Absval x ) & ( not x /. n = FALSE implies Intval x = () - (2 to_power n) ) );

definition
let n be non zero Nat;
let z1, z2 be Tuple of n, BOOLEAN ;
func Int_add_ovfl (z1,z2) -> Element of BOOLEAN equals :: BINARI_2:def 4
(('not' (z1 /. n)) '&' ('not' (z2 /. n))) '&' ((carry (z1,z2)) /. n);
correctness
coherence
(('not' (z1 /. n)) '&' ('not' (z2 /. n))) '&' ((carry (z1,z2)) /. n) is Element of BOOLEAN
;
;
end;

:: deftheorem defines Int_add_ovfl BINARI_2:def 4 :
for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN holds Int_add_ovfl (z1,z2) = (('not' (z1 /. n)) '&' ('not' (z2 /. n))) '&' ((carry (z1,z2)) /. n);

definition
let n be non zero Nat;
let z1, z2 be Tuple of n, BOOLEAN ;
func Int_add_udfl (z1,z2) -> Element of BOOLEAN equals :: BINARI_2:def 5
((z1 /. n) '&' (z2 /. n)) '&' ('not' ((carry (z1,z2)) /. n));
correctness
coherence
((z1 /. n) '&' (z2 /. n)) '&' ('not' ((carry (z1,z2)) /. n)) is Element of BOOLEAN
;
;
end;

:: deftheorem defines Int_add_udfl BINARI_2:def 5 :
for n being non zero Nat
for z1, z2 being Tuple of n, BOOLEAN holds Int_add_udfl (z1,z2) = ((z1 /. n) '&' (z2 /. n)) '&' ('not' ((carry (z1,z2)) /. n));

theorem :: BINARI_2:1
for z1 being Tuple of 2, BOOLEAN st z1 = ^ holds
Intval z1 = 0
proof end;

theorem Th2: :: BINARI_2:2
for z1 being Tuple of 2, BOOLEAN st z1 = ^ holds
Intval z1 = 1
proof end;

theorem :: BINARI_2:3
for z1 being Tuple of 2, BOOLEAN st z1 = ^ holds
Intval z1 = - 2
proof end;

theorem :: BINARI_2:4
for z1 being Tuple of 2, BOOLEAN st z1 = ^ holds
Intval z1 = - 1
proof end;

theorem Th5: :: BINARI_2:5
for n, i being Nat st i in Seg n & i = 1 holds
(Bin1 n) /. i = TRUE
proof end;

theorem Th6: :: BINARI_2:6
for n, i being Nat st i in Seg n & i <> 1 holds
(Bin1 n) /. i = FALSE
proof end;

theorem Th7: :: BINARI_2:7
for m being non zero Nat holds Bin1 (m + 1) = (Bin1 m) ^
proof end;

theorem Th8: :: BINARI_2:8
for m being non zero Nat holds Intval ((Bin1 m) ^ ) = 1
proof end;

theorem Th9: :: BINARI_2:9
for m being non zero Nat
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds 'not' (z ^ <*d*>) = () ^ <*()*>
proof end;

theorem Th10: :: BINARI_2:10
for m being non zero Nat
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds Intval (z ^ <*d*>) = () - (IFEQ (d,FALSE,0,(2 to_power m)))
proof end;

theorem Th11: :: BINARI_2:11
for m being non zero Nat
for z1, z2 being Tuple of m, BOOLEAN
for d1, d2 being Element of BOOLEAN holds ((Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + (IFEQ ((Int_add_ovfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))),FALSE,0,(2 to_power (m + 1))))) - (IFEQ ((Int_add_udfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))),FALSE,0,(2 to_power (m + 1)))) = (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))
proof end;

theorem Th12: :: BINARI_2:12
for m being non zero Nat
for z1, z2 being Tuple of m, BOOLEAN
for d1, d2 being Element of BOOLEAN holds Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>)) = (((Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>))) - (IFEQ ((Int_add_ovfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))),FALSE,0,(2 to_power (m + 1))))) + (IFEQ ((Int_add_udfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))),FALSE,0,(2 to_power (m + 1))))
proof end;

theorem Th13: :: BINARI_2:13
for m being non zero Nat
for x being Tuple of m, BOOLEAN holds Absval () = ((- ()) + (2 to_power m)) - 1
proof end;

theorem Th14: :: BINARI_2:14
for m being non zero Nat
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds Neg2 (z ^ <*d*>) = (Neg2 z) ^ <*(() 'xor' (add_ovfl ((),(Bin1 m))))*>
proof end;

theorem Th15: :: BINARI_2:15
for m being non zero Nat
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds (Intval (Neg2 (z ^ <*d*>))) + (IFEQ ((Int_add_ovfl (('not' (z ^ <*d*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = - (Intval (z ^ <*d*>))
proof end;

theorem :: BINARI_2:16
for m being non zero Nat
for z being Tuple of m, BOOLEAN
for d being Element of BOOLEAN holds Neg2 (Neg2 (z ^ <*d*>)) = z ^ <*d*>
proof end;

definition
let n be non zero Nat;
let x, y be Tuple of n, BOOLEAN ;
func x - y -> Tuple of n, BOOLEAN means :Def6: :: BINARI_2:def 6
for i being Nat st i in Seg n holds
it /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 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' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 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' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i) ) & ( for i being Nat st i in Seg n holds
b2 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines - BINARI_2:def 6 :
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' ((Neg2 y) /. i)) 'xor' ((carry (x,(Neg2 y))) /. i) );

theorem Th17: :: BINARI_2:17
for m being non zero Nat
for x, y being Tuple of m, BOOLEAN holds x - y = x + (Neg2 y)
proof end;

theorem :: BINARI_2:18
for m being non zero Nat
for z1, z2 being Tuple of m, BOOLEAN
for d1, d2 being Element of BOOLEAN holds (z1 ^ <*d1*>) - (z2 ^ <*d2*>) = (z1 + (Neg2 z2)) ^ <*(((d1 'xor' ('not' d2)) 'xor' (add_ovfl (('not' z2),(Bin1 m)))) 'xor' (add_ovfl (z1,(Neg2 z2))))*>
proof end;

theorem :: BINARI_2:19
for m being non zero Nat
for z1, z2 being Tuple of m, BOOLEAN
for d1, d2 being Element of BOOLEAN holds (((Intval ((z1 ^ <*d1*>) - (z2 ^ <*d2*>))) + (IFEQ ((Int_add_ovfl ((z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>)))),FALSE,0,(2 to_power (m + 1))))) - (IFEQ ((Int_add_udfl ((z1 ^ <*d1*>),(Neg2 (z2 ^ <*d2*>)))),FALSE,0,(2 to_power (m + 1))))) + (IFEQ ((Int_add_ovfl (('not' (z2 ^ <*d2*>)),(Bin1 (m + 1)))),FALSE,0,(2 to_power (m + 1)))) = (Intval (z1 ^ <*d1*>)) - (Intval (z2 ^ <*d2*>))
proof end;