:: Constructing Binary {H}uffman Tree
:: by Hiroyuki Okazaki , Yuichi Futa and Yasunari Shidama
::
:: Received June 18, 2013
:: Copyright (c) 2013-2018 Association of Mizar Users


registration
let D be non empty set ;
let x be Element of D;
cluster K453(x) -> binary ;
coherence
root-tree x is binary
by FUNCT_2:def 1;
end;

definition
func IndexedREAL -> set equals :: HUFFMAN1:def 1
[:NAT,REAL:];
correctness
coherence
[:NAT,REAL:] is set
;
;
end;

:: deftheorem defines IndexedREAL HUFFMAN1:def 1 :
IndexedREAL = [:NAT,REAL:];

registration
cluster IndexedREAL -> non empty ;
coherence
not IndexedREAL is empty
;
end;

definition
let D be non empty set ;
func BinFinTrees D -> DTree-set of D means :Def2: :: HUFFMAN1:def 2
for T being DecoratedTree of D holds
( ( dom T is finite & T is binary ) iff T in it );
existence
ex b1 being DTree-set of D st
for T being DecoratedTree of D holds
( ( dom T is finite & T is binary ) iff T in b1 )
proof end;
uniqueness
for b1, b2 being DTree-set of D st ( for T being DecoratedTree of D holds
( ( dom T is finite & T is binary ) iff T in b1 ) ) & ( for T being DecoratedTree of D holds
( ( dom T is finite & T is binary ) iff T in b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines BinFinTrees HUFFMAN1:def 2 :
for D being non empty set
for b2 being DTree-set of D holds
( b2 = BinFinTrees D iff for T being DecoratedTree of D holds
( ( dom T is finite & T is binary ) iff T in b2 ) );

definition
let D be non empty set ;
func BoolBinFinTrees D -> non empty Subset of (bool (BinFinTrees D)) equals :: HUFFMAN1:def 3
{ x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } ;
correctness
coherence
{ x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } is non empty Subset of (bool (BinFinTrees D))
;
proof end;
end;

:: deftheorem defines BoolBinFinTrees HUFFMAN1:def 3 :
for D being non empty set holds BoolBinFinTrees D = { x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } ;

definition
let SOURCE be non empty finite set ;
let p be Probability of Trivial-SigmaField SOURCE;
func Initial-Trees p -> non empty finite Subset of (BinFinTrees IndexedREAL) equals :: HUFFMAN1:def 4
{ T where T is Element of FinTrees IndexedREAL : ( T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) } ;
correctness
coherence
{ T where T is Element of FinTrees IndexedREAL : ( T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) } is non empty finite Subset of (BinFinTrees IndexedREAL)
;
proof end;
end;

:: deftheorem defines Initial-Trees HUFFMAN1:def 4 :
for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE holds Initial-Trees p = { T where T is Element of FinTrees IndexedREAL : ( T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) } ;

definition
let p be DecoratedTree of IndexedREAL ;
{} in dom p by TREES_1:22;
then p . {} in rng p by FUNCT_1:3;
then A1: ex x, y being object st
( x in NAT & y in REAL & p . {} = [x,y] ) by ZFMISC_1:def 2;
func Vrootr p -> Real equals :: HUFFMAN1:def 5
(p . {}) `2 ;
correctness
coherence
(p . {}) `2 is Real
;
by A1;
func Vrootl p -> Nat equals :: HUFFMAN1:def 6
(p . {}) `1 ;
correctness
coherence
(p . {}) `1 is Nat
;
by A1;
end;

:: deftheorem defines Vrootr HUFFMAN1:def 5 :
for p being DecoratedTree of IndexedREAL holds Vrootr p = (p . {}) `2 ;

:: deftheorem defines Vrootl HUFFMAN1:def 6 :
for p being DecoratedTree of IndexedREAL holds Vrootl p = (p . {}) `1 ;

definition
let T be finite binary DecoratedTree of IndexedREAL ;
let p be Element of dom T;
func Vtree p -> Real equals :: HUFFMAN1:def 7
(T . p) `2 ;
correctness
coherence
(T . p) `2 is Real
;
proof end;
end;

:: deftheorem defines Vtree HUFFMAN1:def 7 :
for T being finite binary DecoratedTree of IndexedREAL
for p being Element of dom T holds Vtree p = (T . p) `2 ;

definition
let p, q be finite binary DecoratedTree of IndexedREAL ;
let k be Nat;
func MakeTree (p,q,k) -> finite binary DecoratedTree of IndexedREAL equals :: HUFFMAN1:def 8
[k,((Vrootr p) + (Vrootr q))] -tree (p,q);
correctness
coherence
[k,((Vrootr p) + (Vrootr q))] -tree (p,q) is finite binary DecoratedTree of IndexedREAL
;
proof end;
end;

:: deftheorem defines MakeTree HUFFMAN1:def 8 :
for p, q being finite binary DecoratedTree of IndexedREAL
for k being Nat holds MakeTree (p,q,k) = [k,((Vrootr p) + (Vrootr q))] -tree (p,q);

definition
let X be non empty finite Subset of (BinFinTrees IndexedREAL);
func MaxVl X -> Nat means :Def9: :: HUFFMAN1:def 9
ex L being non empty finite Subset of NAT st
( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & it = max L );
existence
ex b1 being Nat ex L being non empty finite Subset of NAT st
( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b1 = max L )
proof end;
uniqueness
for b1, b2 being Nat st ex L being non empty finite Subset of NAT st
( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b1 = max L ) & ex L being non empty finite Subset of NAT st
( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b2 = max L ) holds
b1 = b2
;
end;

:: deftheorem Def9 defines MaxVl HUFFMAN1:def 9 :
for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for b2 being Nat holds
( b2 = MaxVl X iff ex L being non empty finite Subset of NAT st
( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b2 = max L ) );

theorem :: HUFFMAN1:1
for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for w being finite binary DecoratedTree of IndexedREAL st X = {w} holds
MaxVl X = Vrootl w
proof end;

theorem Th2: :: HUFFMAN1:2
for X, Y, Z being non empty finite Subset of (BinFinTrees IndexedREAL) st Z = X \/ Y holds
MaxVl Z = max ((MaxVl X),(MaxVl Y))
proof end;

theorem :: HUFFMAN1:3
for X, Z being non empty finite Subset of (BinFinTrees IndexedREAL)
for Y being set st Z = X \ Y holds
MaxVl Z <= MaxVl X
proof end;

theorem :: HUFFMAN1:4
for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for p being Element of BinFinTrees IndexedREAL st p in X holds
Vrootl p <= MaxVl X
proof end;

defpred S1[ non empty finite Subset of (BinFinTrees IndexedREAL), finite binary DecoratedTree of IndexedREAL ] means ( $2 in $1 & ( for q being finite binary DecoratedTree of IndexedREAL st q in $1 holds
Vrootr $2 <= Vrootr q ) );

definition
let X be non empty finite Subset of (BinFinTrees IndexedREAL);
mode MinValueTree of X -> finite binary DecoratedTree of IndexedREAL means :Def10: :: HUFFMAN1:def 10
( it in X & ( for q being finite binary DecoratedTree of IndexedREAL st q in X holds
Vrootr it <= Vrootr q ) );
existence
ex b1 being finite binary DecoratedTree of IndexedREAL st
( b1 in X & ( for q being finite binary DecoratedTree of IndexedREAL st q in X holds
Vrootr b1 <= Vrootr q ) )
proof end;
end;

:: deftheorem Def10 defines MinValueTree HUFFMAN1:def 10 :
for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for b2 being finite binary DecoratedTree of IndexedREAL holds
( b2 is MinValueTree of X iff ( b2 in X & ( for q being finite binary DecoratedTree of IndexedREAL st q in X holds
Vrootr b2 <= Vrootr q ) ) );

Lm1: for X being set
for x being object st ex u, v being object st
( u <> v & u in X & v in X ) holds
X \ {x} <> {}

proof end;

Lm2: for X, Y being set
for t, s, z being object st X c= Y & t in Y & s in Y & z in Y holds
(X \ {t,s}) \/ {z} c= Y

proof end;

Lm3: for X being finite set st 2 <= card X holds
ex u, v being object st
( u <> v & u in X & v in X )

proof end;

Lm4: for X being finite set st 1 = card X holds
ex u being object st X = {u}

proof end;

Lm5: for X being finite set
for t, s, z being object st t in X & s in X & t <> s & not z in X holds
card ((X \ {t,s}) \/ {z}) = (card X) - 1

proof end;

theorem Th5: :: HUFFMAN1:5
for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE holds card (Initial-Trees p) = card SOURCE
proof end;

theorem Th6: :: HUFFMAN1:6
for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for s, t being finite binary DecoratedTree of IndexedREAL holds not MakeTree (t,s,((MaxVl X) + 1)) in X
proof end;

definition
let X be set ;
func LeavesSet X -> Subset of (bool IndexedREAL) equals :: HUFFMAN1:def 11
{ (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } ;
correctness
coherence
{ (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } is Subset of (bool IndexedREAL)
;
proof end;
end;

:: deftheorem defines LeavesSet HUFFMAN1:def 11 :
for X being set holds LeavesSet X = { (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } ;

theorem Th7: :: HUFFMAN1:7
for X being finite binary DecoratedTree of IndexedREAL holds LeavesSet {X} = {(Leaves X)}
proof end;

theorem Th8: :: HUFFMAN1:8
for X, Y being set holds LeavesSet (X \/ Y) = (LeavesSet X) \/ (LeavesSet Y)
proof end;

theorem Th9: :: HUFFMAN1:9
for s, t being Tree holds not {} in Leaves (tree (t,s))
proof end;

theorem Th10: :: HUFFMAN1:10
for s, t being Tree holds Leaves (tree (t,s)) = { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s }
proof end;

theorem Th11: :: HUFFMAN1:11
for s, t being DecoratedTree
for x being object
for q being FinSequence of NAT st q in dom t holds
(x -tree (t,s)) . (<*0*> ^ q) = t . q
proof end;

theorem Th12: :: HUFFMAN1:12
for s, t being DecoratedTree
for x being object
for q being FinSequence of NAT st q in dom s holds
(x -tree (t,s)) . (<*1*> ^ q) = s . q
proof end;

theorem Th13: :: HUFFMAN1:13
for s, t being DecoratedTree
for x being object holds Leaves (x -tree (t,s)) = (Leaves t) \/ (Leaves s)
proof end;

theorem Th14: :: HUFFMAN1:14
for k being Nat
for s, t being finite binary DecoratedTree of IndexedREAL holds union (LeavesSet {s,t}) = union (LeavesSet {(MakeTree (t,s,k))})
proof end;

theorem Th15: :: HUFFMAN1:15
Leaves (elementary_tree 0) = elementary_tree 0
proof end;

theorem Th16: :: HUFFMAN1:16
for x being object
for D being non empty set
for T being finite binary DecoratedTree of D st T = root-tree x holds
Leaves T = {x}
proof end;

definition
let SOURCE be non empty finite set ;
let p be Probability of Trivial-SigmaField SOURCE;
let Tseq be FinSequence of BoolBinFinTrees IndexedREAL;
let q be FinSequence of NAT ;
pred Tseq,q,p is_constructingBinHuffmanTree means :Def12: :: HUFFMAN1:def 12
( Tseq . 1 = Initial-Trees p & len Tseq = card SOURCE & ( for i being Nat st 1 <= i & i < len Tseq holds
ex X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) ex s being MinValueTree of X ex t being MinValueTree of Y ex v being finite binary DecoratedTree of IndexedREAL st
( Tseq . i = X & Y = X \ {s} & v in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl