:: by Hiroyuki Okazaki , Yuichi Futa and Yasunari Shidama

::

:: Received June 18, 2013

:: Copyright (c) 2013-2018 Association of Mizar Users

registration
end;

definition

let D be non empty set ;

ex b_{1} being DTree-set of D st

for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in b_{1} )

for b_{1}, b_{2} being DTree-set of D st ( for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in b_{1} ) ) & ( for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in b_{2} ) ) holds

b_{1} = b_{2}

end;
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 for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in it );

ex b

for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in b

proof end;

uniqueness for b

( ( dom T is finite & T is binary ) iff T in b

( ( dom T is finite & T is binary ) iff T in b

b

proof end;

:: deftheorem Def2 defines BinFinTrees HUFFMAN1:def 2 :

for D being non empty set

for b_{2} being DTree-set of D holds

( b_{2} = BinFinTrees D iff for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in b_{2} ) );

for D being non empty set

for b

( b

( ( dom T is finite & T is binary ) iff T in b

definition

let D be non empty set ;

coherence

{ x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } is non empty Subset of (bool (BinFinTrees D));

end;
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 { x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } ;

coherence

{ x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } is non empty Subset of (bool (BinFinTrees D));

proof 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 <> {} ) } ;

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;

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

end;
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 { 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})] ) } ;

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;

:: 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})] ) } ;

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;

correctness

coherence

(p . {}) `2 is Real;

by A1;

correctness

coherence

(p . {}) `1 is Nat;

by A1;

end;
{} 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;

correctness

coherence

(p . {}) `2 is Real;

by A1;

correctness

coherence

(p . {}) `1 is Nat;

by A1;

:: deftheorem defines Vrootr HUFFMAN1:def 5 :

for p being DecoratedTree of IndexedREAL holds Vrootr p = (p . {}) `2 ;

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 ;

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;

correctness

coherence

(T . p) `2 is Real;

end;
let p be Element of dom T;

correctness

coherence

(T . p) `2 is Real;

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

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;

coherence

[k,((Vrootr p) + (Vrootr q))] -tree (p,q) is finite binary DecoratedTree of IndexedREAL ;

end;
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 [k,((Vrootr p) + (Vrootr q))] -tree (p,q);

coherence

[k,((Vrootr p) + (Vrootr q))] -tree (p,q) is finite binary DecoratedTree of IndexedREAL ;

proof 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);

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

ex b_{1} 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 } & b_{1} = max L )

for b_{1}, b_{2} 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 } & b_{1} = 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 } & b_{2} = max L ) holds

b_{1} = b_{2}
;

end;
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 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 );

ex b

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b

proof end;

uniqueness for b

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b

b

:: deftheorem Def9 defines MaxVl HUFFMAN1:def 9 :

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for b_{2} being Nat holds

( b_{2} = 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 } & b_{2} = max L ) );

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for b

( b

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b

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

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

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

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

for p being Element of BinFinTrees IndexedREAL st p in X holds

Vrootl p <= MaxVl X

proof end;

defpred S

Vrootr $2 <= Vrootr q ) );

definition

let X be non empty finite Subset of (BinFinTrees IndexedREAL);

ex b_{1} being finite binary DecoratedTree of IndexedREAL st

( b_{1} in X & ( for q being finite binary DecoratedTree of IndexedREAL st q in X holds

Vrootr b_{1} <= Vrootr q ) )

end;
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 ( it in X & ( for q being finite binary DecoratedTree of IndexedREAL st q in X holds

Vrootr it <= Vrootr q ) );

ex b

( b

Vrootr b

proof end;

:: deftheorem Def10 defines MinValueTree HUFFMAN1:def 10 :

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for b_{2} being finite binary DecoratedTree of IndexedREAL holds

( b_{2} is MinValueTree of X iff ( b_{2} in X & ( for q being finite binary DecoratedTree of IndexedREAL st q in X holds

Vrootr b_{2} <= Vrootr q ) ) );

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for b

( b

Vrootr b

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

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

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 ;

coherence

{ (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } is Subset of (bool IndexedREAL);

end;
func LeavesSet X -> Subset of (bool IndexedREAL) equals :: HUFFMAN1:def 11

{ (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } ;

correctness { (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } ;

coherence

{ (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } is Subset of (bool IndexedREAL);

proof 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 } ;

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

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

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

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)

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

for s, t being finite binary DecoratedTree of IndexedREAL holds union (LeavesSet {s,t}) = union (LeavesSet {(MakeTree (t,s,k))})

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}

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 ;

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

( 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