HUFFMAN1: Constructing Binary {H}uffman Tree

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

registration

let D be non empty set ;
let x be Element of D;

cluster root-tree x -> binary ;

coherence ;

end;

definition

func IndexedREAL -> set equals :: HUFFMAN1:def 1
[:NAT,REAL:];

correctness ;

end;

:: deftheorem defines IndexedREAL HUFFMAN1:def 1 :

registration

cluster IndexedREAL -> non empty ;

coherence ;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines BinFinTrees HUFFMAN1:def 2 :

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

proof end;

end;

:: deftheorem defines BoolBinFinTrees HUFFMAN1:def 3 :

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

proof end;

end;

:: deftheorem defines Initial-Trees HUFFMAN1:def 4 :

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 by A1;

func Vrootl p -> Nat equals :: HUFFMAN1:def 6
(p . {}) `1 ;

correctness by A1;

end;

:: deftheorem defines Vrootr HUFFMAN1:def 5 :

:: deftheorem defines Vrootl HUFFMAN1:def 6 :

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

proof end;

end;

:: deftheorem defines Vtree HUFFMAN1:def 7 :

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

proof end;

end;

:: deftheorem defines MakeTree HUFFMAN1:def 8 :

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

proof end;

uniqueness ;

end;

:: deftheorem Def9 defines MaxVl HUFFMAN1:def 9 :

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 S₁[ 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

proof end;

end;

:: deftheorem Def10 defines MinValueTree HUFFMAN1:def 10 :

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

proof end;

end;

:: deftheorem defines LeavesSet HUFFMAN1:def 11 :

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 X) + 1)))} & Tseq . (i + 1) = (X \ {t,s}) \/ {v} ) ) & ex T being finite binary DecoratedTree of IndexedREAL st {T} = Tseq . (len Tseq) & dom q = Seg (card SOURCE) & ( for k being Nat st k in Seg (card SOURCE) holds
( q . k = card (Tseq . k) & q . k <> 0 ) ) & ( for k being Nat st k < card SOURCE holds
q . (k + 1) = (q . 1) - k ) & ( for k being Nat st 1 <= k & k < card SOURCE holds
2 <= q . k ) );

end;

:: deftheorem Def12 defines is_constructingBinHuffmanTree HUFFMAN1:def 12 :

theorem Th17: :: HUFFMAN1:17

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree

proof end;

definition

let SOURCE be non empty finite set ;
let p be Probability of Trivial-SigmaField SOURCE;

mode BinHuffmanTree of p -> finite binary DecoratedTree of IndexedREAL means :Def13: :: HUFFMAN1:def 13
ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st
( Tseq,q,p is_constructingBinHuffmanTree & {it} = Tseq . (len Tseq) );

existence

proof end;

end;

:: deftheorem Def13 defines BinHuffmanTree HUFFMAN1:def 13 :

theorem Th18: :: HUFFMAN1:18

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE holds union (LeavesSet (Initial-Trees p)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }

proof end;

theorem Th19: :: HUFFMAN1:19

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat st 1 <= i & i <= len Tseq holds
union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }

proof end;

theorem :: HUFFMAN1:20

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for T being BinHuffmanTree of p holds Leaves T = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }

proof end;

theorem Th21: :: HUFFMAN1:21

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat
for T being finite binary DecoratedTree of IndexedREAL
for t, s, r being Element of dom T st T in Tseq . i & t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)

proof end;

theorem :: HUFFMAN1:22

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for T being BinHuffmanTree of p
for t, s, r being Element of dom T st t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)

proof end;

theorem Th23: :: HUFFMAN1:23

for X being non empty finite Subset of (BinFinTrees IndexedREAL) st ( for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X ) holds
for s, t, w being finite binary DecoratedTree of IndexedREAL st s in X & t in X & w = MakeTree (t,s,((MaxVl X) + 1)) holds
for p being Element of dom w
for r being Element of NAT st r = (w . p) `1 holds
r <= (MaxVl X) + 1

proof end;

theorem Th24: :: HUFFMAN1:24

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat st 1 <= i & i < len Tseq holds
for X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & Y = Tseq . (i + 1) holds
MaxVl Y = (MaxVl X) + 1

proof end;

theorem :: HUFFMAN1:25

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i holds
for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X

proof end;

theorem Th26: :: HUFFMAN1:26

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i holds
for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X

proof end;

theorem Th27: :: HUFFMAN1:27

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat
for s, t being finite binary DecoratedTree of IndexedREAL
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & s in X & t in X holds
for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z

proof end;

registration

let x be object ;

cluster root-tree x -> one-to-one ;

coherence

proof end;

end;

theorem Th28: :: HUFFMAN1:28

for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for s, t, w being finite binary DecoratedTree of IndexedREAL st ( for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X ) & ( for p, q being finite binary DecoratedTree of IndexedREAL st p in X & q in X & p <> q holds
(rng p) /\ (rng q) = {} ) & s in X & t in X & s <> t & w in X \ {s,t} holds
(rng (MakeTree (t,s,((MaxVl X) + 1)))) /\ (rng w) = {}

proof end;

theorem Th29: :: HUFFMAN1:29

proof end;

theorem Th30: :: HUFFMAN1:30

for X being non empty finite Subset of (BinFinTrees IndexedREAL)
for s, t being finite binary DecoratedTree of IndexedREAL st s is one-to-one & t is one-to-one & t in X & s in X & (rng s) /\ (rng t) = {} & ( for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z ) holds
MakeTree (t,s,((MaxVl X) + 1)) is one-to-one

proof end;

theorem Th31: :: HUFFMAN1:31

proof end;

registration

let SOURCE be non empty finite set ;
let p be Probability of Trivial-SigmaField SOURCE;

cluster -> one-to-one for BinHuffmanTree of p;

coherence

proof end;

end;