:: Binary Representation of Natural Numbers
:: by Hiroyuki Okazaki
::
:: Received September 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users


theorem LM000: :: BINARI_6:1
for x being Nat ex m being Nat st x < 2 to_power m
proof end;

theorem LM001: :: BINARI_6:2
for x being Nat st x <> 0 holds
ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) )
proof end;

theorem LM002: :: BINARI_6:3
for x, n1, n2 being Nat st 2 to_power n1 <= x & x < 2 to_power (n1 + 1) & 2 to_power n2 <= x & x < 2 to_power (n2 + 1) holds
n1 = n2
proof end;

theorem LM0020: :: BINARI_6:4
<*0*> = 0* 1 by FINSEQ_2:59;

theorem :: BINARI_6:5
for n1, n2 being Nat holds (0* n1) ^ (0* n2) = 0* (n1 + n2) by FINSEQ_2:123;

definition
let x be Nat;
func LenBSeq x -> non zero Nat means :Def1: :: BINARI_6:def 1
it = 1 if x = 0
otherwise ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & it = n + 1 );
existence
( ( x = 0 implies ex b1 being non zero Nat st b1 = 1 ) & ( not x = 0 implies ex b1 being non zero Nat ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & b1 = n + 1 ) ) )
proof end;
uniqueness
for b1, b2 being non zero Nat holds
( ( x = 0 & b1 = 1 & b2 = 1 implies b1 = b2 ) & ( not x = 0 & ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & b1 = n + 1 ) & ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & b2 = n + 1 ) implies b1 = b2 ) )
by LM002;
consistency
for b1 being non zero Nat holds verum
;
end;

:: deftheorem Def1 defines LenBSeq BINARI_6:def 1 :
for x being Nat
for b2 being non zero Nat holds
( ( x = 0 implies ( b2 = LenBSeq x iff b2 = 1 ) ) & ( not x = 0 implies ( b2 = LenBSeq x iff ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & b2 = n + 1 ) ) ) );

theorem LM006: :: BINARI_6:6
for x being Nat holds x < 2 to_power (LenBSeq x)
proof end;

theorem LM007: :: BINARI_6:7
for x being Nat holds x = Absval ((LenBSeq x) -BinarySequence x)
proof end;

theorem LM0071: :: BINARI_6:8
for n being Nat
for x being Tuple of n + 1, BOOLEAN st x . (n + 1) = 1 holds
( 2 to_power n <= Absval x & Absval x < 2 to_power (n + 1) )
proof end;

theorem :: BINARI_6:9
ex F being Function of (BOOLEAN *),NAT st
for x being Element of BOOLEAN * ex x0 being Tuple of len x, BOOLEAN st
( x = x0 & F . x = Absval x0 )
proof end;

LM020: ex F being Function of NAT,(BOOLEAN *) st
for x being Element of NAT holds F . x = (LenBSeq x) -BinarySequence x

proof end;

LM030: for F being Function of NAT,(BOOLEAN *) st ( for x being Element of NAT holds F . x = (LenBSeq x) -BinarySequence x ) holds
F is one-to-one

proof end;

definition
func Nat2BL -> Function of NAT,(BOOLEAN *) means :Def2: :: BINARI_6:def 2
for x being Element of NAT holds it . x = (LenBSeq x) -BinarySequence x;
existence
ex b1 being Function of NAT,(BOOLEAN *) st
for x being Element of NAT holds b1 . x = (LenBSeq x) -BinarySequence x
by LM020;
uniqueness
for b1, b2 being Function of NAT,(BOOLEAN *) st ( for x being Element of NAT holds b1 . x = (LenBSeq x) -BinarySequence x ) & ( for x being Element of NAT holds b2 . x = (LenBSeq x) -BinarySequence x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Nat2BL BINARI_6:def 2 :
for b1 being Function of NAT,(BOOLEAN *) holds
( b1 = Nat2BL iff for x being Element of NAT holds b1 . x = (LenBSeq x) -BinarySequence x );

theorem :: BINARI_6:10
for x being Element of NAT
for y being Tuple of LenBSeq x, BOOLEAN st Nat2BL . x = y holds
Absval y = x
proof end;

theorem LM031: :: BINARI_6:11
rng Nat2BL = { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>}
proof end;

theorem :: BINARI_6:12
Nat2BL is one-to-one
proof end;

definition
let x, y be Element of BOOLEAN * ;
assume AS: ( len x <> 0 & len y <> 0 ) ;
func LenMax (x,y) -> non zero Nat equals :Def15: :: BINARI_6:def 3
max ((len x),(len y));
correctness
coherence
max ((len x),(len y)) is non zero Nat
;
by XXREAL_0:16, AS;
end;

:: deftheorem Def15 defines LenMax BINARI_6:def 3 :
for x, y being Element of BOOLEAN * st len x <> 0 & len y <> 0 holds
LenMax (x,y) = max ((len x),(len y));

definition
let K be Nat;
let x be Element of BOOLEAN * ;
func ExtBit (x,K) -> Tuple of K, BOOLEAN equals :Def20: :: BINARI_6:def 4
x ^ (0* (K -' (len x))) if len x <= K
otherwise x | K;
coherence
( ( len x <= K implies x ^ (0* (K -' (len x))) is Tuple of K, BOOLEAN ) & ( not len x <= K implies x | K is Tuple of K, BOOLEAN ) )
proof end;
consistency
for b1 being Tuple of K, BOOLEAN holds verum
;
end;

:: deftheorem Def20 defines ExtBit BINARI_6:def 4 :
for K being Nat
for x being Element of BOOLEAN * holds
( ( len x <= K implies ExtBit (x,K) = x ^ (0* (K -' (len x))) ) & ( not len x <= K implies ExtBit (x,K) = x | K ) );

theorem LMExtBit1: :: BINARI_6:13
for K being Nat
for x being Element of BOOLEAN * st len x <= K holds
ExtBit (x,(K + 1)) = (ExtBit (x,K)) ^ <*0*>
proof end;

theorem LMExtBit8: :: BINARI_6:14
for K being non zero Nat
for x being Element of BOOLEAN * st len x = K holds
ExtBit (x,K) = x
proof end;

theorem LMExtBit2: :: BINARI_6:15
for K being non zero Nat
for x, y being Tuple of K, BOOLEAN
for x1, y1 being Tuple of K + 1, BOOLEAN st x1 = x ^ <*0*> & y1 = y ^ <*0*> holds
x1,y1 are_summable
proof end;

theorem LMExtBit4: :: BINARI_6:16
for K being non zero Nat
for y being Tuple of K, BOOLEAN st y = 0* K holds
for n being non zero Nat st n <= K holds
y /. n = 0
proof end;

theorem LMExtBit501: :: BINARI_6:17
for K being non zero Nat
for x, y being Tuple of K, BOOLEAN holds carry (x,y) = carry (y,x)
proof end;

theorem LMExtBit3: :: BINARI_6:18
for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st y = 0* K holds
for n being non zero Nat st n <= K holds
( (carry (x,y)) /. n = 0 & (carry (y,x)) /. n = 0 )
proof end;

theorem LMExtBit500: :: BINARI_6:19
for K being non zero Nat
for x, y being Tuple of K, BOOLEAN holds x + y = y + x
proof end;

theorem LMExtBit5: :: BINARI_6:20
for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st y = 0* K holds
( x + y = x & y + x = x )
proof end;

theorem LMExtBit9: :: BINARI_6:21
for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st x . (len x) = 1 & y . (len y) = 1 holds
not x,y are_summable
proof end;

LMExtBit60: for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st x,y are_summable & x . (len x) = 1 holds
(x + y) . (len (x + y)) = 1

proof end;

theorem LMExtBit61: :: BINARI_6:22
for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st x,y are_summable holds
y,x are_summable
proof end;

theorem LMExtBit6: :: BINARI_6:23
for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st x,y are_summable & ( x . (len x) = 1 or y . (len y) = 1 ) holds
(x + y) . (len (x + y)) = 1
proof end;

theorem LMExtBit7: :: BINARI_6:24
for K being non zero Nat
for x, y being Tuple of K, BOOLEAN
for x1, y1 being Tuple of K + 1, BOOLEAN st not x,y are_summable & x1 = x ^ <*0*> & y1 = y ^ <*0*> holds
(x1 + y1) . (len (x1 + y1)) = 1
proof end;

definition
let x, y be Element of BOOLEAN * ;
func x + y -> Element of BOOLEAN * equals :Def3: :: BINARI_6:def 5
y if len x = 0
x if len y = 0
(ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) if ( ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 )
otherwise (ExtBit (x,((LenMax (x,y)) + 1))) + (ExtBit (y,((LenMax (x,y)) + 1)));
coherence
( ( len x = 0 implies y is Element of BOOLEAN * ) & ( len y = 0 implies x is Element of BOOLEAN * ) & ( ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 implies (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) is Element of BOOLEAN * ) & ( not len x = 0 & not len y = 0 & ( not ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable or not len x <> 0 or not len y <> 0 ) implies (ExtBit (x,((LenMax (x,y)) + 1))) + (ExtBit (y,((LenMax (x,y)) + 1))) is Element of BOOLEAN * ) )
by FINSEQ_1:def 11;
consistency
for b1 being Element of BOOLEAN * holds
( ( len x = 0 & len y = 0 implies ( b1 = y iff b1 = x ) ) & ( len x = 0 & ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 implies ( b1 = y iff b1 = (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) ) ) & ( len y = 0 & ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 implies ( b1 = x iff b1 = (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) ) ) )
;
end;

:: deftheorem Def3 defines + BINARI_6:def 5 :
for x, y being Element of BOOLEAN * holds
( ( len x = 0 implies x + y = y ) & ( len y = 0 implies x + y = x ) & ( ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable & len x <> 0 & len y <> 0 implies x + y = (ExtBit (x,(LenMax (x,y)))) + (ExtBit (y,(LenMax (x,y)))) ) & ( not len x = 0 & not len y = 0 & ( not ExtBit (x,(LenMax (x,y))), ExtBit (y,(LenMax (x,y))) are_summable or not len x <> 0 or not len y <> 0 ) implies x + y = (ExtBit (x,((LenMax (x,y)) + 1))) + (ExtBit (y,((LenMax (x,y)) + 1))) ) );

definition
let F be Function of NAT,(BOOLEAN *);
let x be Element of NAT ;
:: original: .
redefine func F . x -> Element of BOOLEAN * ;
correctness
coherence
F . x is Element of BOOLEAN *
;
by FUNCT_2:5;
end;

theorem LM0710: :: BINARI_6:25
for x being Element of BOOLEAN * st x in rng Nat2BL holds
1 <= len x
proof end;

theorem LM071: :: BINARI_6:26
for x, y being Element of BOOLEAN * st x in rng Nat2BL & y in rng Nat2BL holds
x + y in rng Nat2BL
proof end;

theorem LM080: :: BINARI_6:27
for n being non zero Nat
for x being Tuple of n, BOOLEAN
for m, l being Nat
for y being Tuple of l, BOOLEAN st y = x ^ (0* m) holds
Absval y = Absval x
proof end;

theorem LM090: :: BINARI_6:28
for n being Nat
for x being Element of NAT
for y being Tuple of n, BOOLEAN st y = Nat2BL . x holds
( n = LenBSeq x & Absval y = x & Nat2BL . (Absval y) = y )
proof end;

theorem LM100: :: BINARI_6:29
for x, y being Element of NAT holds Nat2BL . (x + y) = (Nat2BL . x) + (Nat2BL . y)
proof end;

theorem :: BINARI_6:30
for x, y being Element of BOOLEAN * st x in rng Nat2BL & y in rng Nat2BL holds
x + y = y + x
proof end;

theorem :: BINARI_6:31
for x, y, z being Element of BOOLEAN * st x in rng Nat2BL & y in rng Nat2BL & z in rng Nat2BL holds
(x + y) + z = x + (y + z)
proof end;

definition
let x be Element of BOOLEAN * ;
func ExAbsval x -> Nat means :Def100: :: BINARI_6:def 6
ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & it = Absval y );
existence
ex b1, n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & b1 = Absval y )
proof end;
uniqueness
for b1, b2 being Nat st ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & b1 = Absval y ) & ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & b2 = Absval y ) holds
b1 = b2
proof end;
end;

:: deftheorem Def100 defines ExAbsval BINARI_6:def 6 :
for x being Element of BOOLEAN *
for b2 being Nat holds
( b2 = ExAbsval x iff ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & b2 = Absval y ) );

D100: for x being Element of BOOLEAN * st len x = 0 holds
ExAbsval x = 0

proof end;

theorem LM210: :: BINARI_6:32
ex F being Function of (BOOLEAN *),NAT st
for x being Element of BOOLEAN * holds F . x = ExAbsval x
proof end;

definition
func BL2Nat -> Function of (BOOLEAN *),NAT means :Def110: :: BINARI_6:def 7
for x being Element of BOOLEAN * holds it . x = ExAbsval x;
existence
ex b1 being Function of (BOOLEAN *),NAT st
for x being Element of BOOLEAN * holds b1 . x = ExAbsval x
by LM210;
uniqueness
for b1, b2 being Function of (BOOLEAN *),NAT st ( for x being Element of BOOLEAN * holds b1 . x = ExAbsval x ) & ( for x being Element of BOOLEAN * holds b2 . x = ExAbsval x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def110 defines BL2Nat BINARI_6:def 7 :
for b1 being Function of (BOOLEAN *),NAT holds
( b1 = BL2Nat iff for x being Element of BOOLEAN * holds b1 . x = ExAbsval x );

definition
let F be Function of (BOOLEAN *),NAT;
let x be Element of BOOLEAN * ;
:: original: .
redefine func F . x -> Element of NAT ;
correctness
coherence
F . x is Element of NAT
;
by FUNCT_2:5;
end;

LM220: for F being Function of (BOOLEAN *),NAT st ( for x being Element of BOOLEAN * holds F . x = ExAbsval x ) holds
F is onto

proof end;

registration
cluster BL2Nat -> onto ;
coherence
BL2Nat is onto
proof end;
end;

theorem LM230: :: BINARI_6:33
for x being Element of BOOLEAN *
for K being Nat st len x <> 0 & len x <= K holds
ExAbsval x = Absval (ExtBit (x,K))
proof end;

theorem LM240: :: BINARI_6:34
for x, y being Element of BOOLEAN * holds BL2Nat . (x + y) = (BL2Nat . x) + (BL2Nat . y)
proof end;

definition
func EqBL2Nat -> Equivalence_Relation of (BOOLEAN *) means :Def300: :: BINARI_6:def 8
for x, y being object holds
( [x,y] in it iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) );
existence
ex b1 being Equivalence_Relation of (BOOLEAN *) st
for x, y being object holds
( [x,y] in b1 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of (BOOLEAN *) st ( for x, y being object holds
( [x,y] in b1 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) ) & ( for x, y being object holds
( [x,y] in b2 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def300 defines EqBL2Nat BINARI_6:def 8 :
for b1 being Equivalence_Relation of (BOOLEAN *) holds
( b1 = EqBL2Nat iff for x, y being object holds
( [x,y] in b1 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) );

definition
func QuBL2Nat -> Function of (Class EqBL2Nat),NAT means :Def400: :: BINARI_6:def 9
for A being Element of Class EqBL2Nat ex x being object st
( x in A & it . A = BL2Nat . x );
existence
ex b1 being Function of (Class EqBL2Nat),NAT st
for A being Element of Class EqBL2Nat ex x being object st
( x in A & b1 . A = BL2Nat . x )
proof end;
uniqueness
for b1, b2 being Function of (Class EqBL2Nat),NAT st ( for A being Element of Class EqBL2Nat ex x being object st
( x in A & b1 . A = BL2Nat . x ) ) & ( for A being Element of Class EqBL2Nat ex x being object st
( x in A & b2 . A = BL2Nat . x ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def400 defines QuBL2Nat BINARI_6:def 9 :
for b1 being Function of (Class EqBL2Nat),NAT holds
( b1 = QuBL2Nat iff for A being Element of Class EqBL2Nat ex x being object st
( x in A & b1 . A = BL2Nat . x ) );

LemmaQU: QuBL2Nat is onto
proof end;

LM600: QuBL2Nat is one-to-one
proof end;

registration
cluster QuBL2Nat -> one-to-one onto ;
coherence
( QuBL2Nat is one-to-one & QuBL2Nat is onto )
by LemmaQU, LM600;
end;

theorem LM700: :: BINARI_6:35
for x being Element of BOOLEAN * holds QuBL2Nat . (Class (EqBL2Nat,x)) = BL2Nat . x
proof end;

definition
let A, B be Element of Class EqBL2Nat;
func A + B -> Element of Class EqBL2Nat means :Def500: :: BINARI_6:def 10
ex x, y being Element of BOOLEAN * st
( x in A & y in B & it = Class (EqBL2Nat,(x + y)) );
existence
ex b1 being Element of Class EqBL2Nat ex x, y being Element of BOOLEAN * st
( x in A & y in B & b1 = Class (EqBL2Nat,(x + y)) )
proof end;
uniqueness
for b1, b2 being Element of Class EqBL2Nat st ex x, y being Element of BOOLEAN * st
( x in A & y in B & b1 = Class (EqBL2Nat,(x + y)) ) & ex x, y being Element of BOOLEAN * st
( x in A & y in B & b2 = Class (EqBL2Nat,(x + y)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def500 defines + BINARI_6:def 10 :
for A, B, b3 being Element of Class EqBL2Nat holds
( b3 = A + B iff ex x, y being Element of BOOLEAN * st
( x in A & y in B & b3 = Class (EqBL2Nat,(x + y)) ) );

theorem LM800: :: BINARI_6:36
for A, B being Element of Class EqBL2Nat
for x, y being Element of BOOLEAN * st x in A & y in B holds
A + B = Class (EqBL2Nat,(x + y))
proof end;

theorem :: BINARI_6:37
for A, B being Element of Class EqBL2Nat holds QuBL2Nat . (A + B) = (QuBL2Nat . A) + (QuBL2Nat . B)
proof end;

theorem LM910: :: BINARI_6:38
for A, B being Element of Class EqBL2Nat holds A + B = B + A
proof end;

theorem :: BINARI_6:39
for A, B, C being Element of Class EqBL2Nat holds (A + B) + C = A + (B + C)
proof end;

theorem LM930: :: BINARI_6:40
for n being Nat
for z, z1 being Element of BOOLEAN * st z = <*> BOOLEAN & z1 = 0* n holds
Class (EqBL2Nat,z) = Class (EqBL2Nat,z1)
proof end;

theorem :: BINARI_6:41
for A, Z being Element of Class EqBL2Nat
for n being Nat
for z being Element of BOOLEAN * st Z = Class (EqBL2Nat,z) & z = 0* n holds
( A + Z = A & Z + A = A )
proof end;