:: 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
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, FINSEQ_1, FUNCT_1, XXREAL_0, ORDINAL4,
      RELAT_1, TREES_1, XBOOLE_0, FINSET_1, TARSKI, TREES_2, FUNCT_2, CARD_1,
      ZFMISC_1, MCART_1, NAT_1, ARYTM_3, TREES_A, ARYTM_1, TREES_3, REAL_1,
      BINTREE1, ORDINAL1, TREES_4, HUFFMAN1, PROB_1, RANDOM_1, UPROOTS;
 notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
      ORDINAL1, RELSET_1, FUNCT_2, DOMAIN_1, FUNCOP_1, FINSET_1, CARD_1,
      NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, XXREAL_2,
      FINSEQ_1, TREES_1, RVSUM_1, TREES_2, TREES_3, TREES_4, PROB_1, BINTREE1,
      RANDOM_1;
 constructors DOMAIN_1, XXREAL_2, RELSET_1, WELLORD2, BINTREE1, RVSUM_1,
      RANDOM_1, ARYTM_1, TREES_4, RFINSEQ2;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, TREES_3,
      FINSET_1, XREAL_0, NAT_1, FINSEQ_1, TREES_1, TREES_2, CARD_1, RELSET_1,
      MEMBERED, BINTREE1, XTUPLE_0, VALUED_0, NUMBERS, FRAENKEL, XXREAL_2,
      FUNCOP_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Constructing Binary Decoded Trees

registration
  let D be non empty set, x be Element of D;
  cluster root-tree x -> binary;
end;

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

registration
  cluster IndexedREAL -> non empty;
end;

definition
let D be non empty set;
func BinFinTrees D -> DTree-set of D means
:: HUFFMAN1:def 2
for T being DecoratedTree of D holds
 dom T is finite & T is binary iff T in it;
end;

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

reserve SOURCE for non empty finite set,
 p for Probability of Trivial-SigmaField SOURCE,
 Tseq for FinSequence of BoolBinFinTrees IndexedREAL,
 q for FinSequence of NAT;

definition
let SOURCE,p;
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 be Element of SOURCE st
 T = root-tree [ (canFS SOURCE)".x, p.{x} ] };
end;

definition
let p be DecoratedTree of IndexedREAL;
func Vrootr p -> Real equals
:: HUFFMAN1:def 5
 (p.{}) `2;
func Vrootl p -> Nat equals
:: HUFFMAN1:def 6
 (p.{}) `1;
end;

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

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

definition
  let X be non empty finite Subset of BinFinTrees IndexedREAL;
  func MaxVl(X) -> Nat means
:: HUFFMAN1:def 9

 ex L be non empty finite Subset of NAT
 st L = {Vrootl p where p is Element of BinFinTrees IndexedREAL: p in X }
 & it = max L;
end;

theorem :: HUFFMAN1:1
for X be non empty finite Subset of BinFinTrees IndexedREAL,
    w be finite binary DecoratedTree of IndexedREAL st X = {w}
holds MaxVl X = Vrootl w;

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

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

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

definition
  let X be non empty finite Subset of BinFinTrees IndexedREAL;
  mode MinValueTree of X -> finite binary DecoratedTree of IndexedREAL means
:: HUFFMAN1:def 10

  it in X & for q be finite binary DecoratedTree of IndexedREAL
  st q in X holds Vrootr it <= Vrootr q;
end;

theorem :: HUFFMAN1:5
  card (Initial-Trees(p)) = card SOURCE;

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

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

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

theorem :: HUFFMAN1:8
 for X,Y be set
 holds LeavesSet(X \/ Y ) = LeavesSet(X) \/ LeavesSet(Y);

theorem :: HUFFMAN1:9
 for s,t be Tree holds not {} in Leaves (tree (t,s));

theorem :: HUFFMAN1:10
 for s,t be 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};

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

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

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

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

theorem :: HUFFMAN1:15
 Leaves (elementary_tree 0 ) = elementary_tree 0;

theorem :: HUFFMAN1:16
 for x be object, D be non empty set,
 T be finite binary DecoratedTree of D st T = root-tree x holds
 Leaves (T) = {x};

begin :: Binary Huffman Tree

definition
  let SOURCE,p,Tseq,q;
  pred Tseq,q,p is_constructingBinHuffmanTree means
:: HUFFMAN1:def 12

 Tseq.1 = Initial-Trees(p) &
 len Tseq = card SOURCE &
 ( for i be Nat st 1<= i & i < len Tseq
 ex X,Y being non empty finite Subset of BinFinTrees IndexedREAL,
    s being MinValueTree of X,
    t being MinValueTree of Y,
    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 be finite binary DecoratedTree of IndexedREAL
 st { T } = Tseq.(len Tseq)) &
 dom q = Seg card SOURCE
 & (for k be Nat st k in Seg card SOURCE
 holds q.k = card(Tseq.k) & q.k <> 0)
 & (for k be Nat holds (k < card SOURCE implies q.(k+1) = q.1 - k))
 & (for k be Nat st 1<=k & k < card SOURCE holds 2 <= q.k);
end;

theorem :: HUFFMAN1:17
 ex Tseq,q st Tseq,q,p is_constructingBinHuffmanTree;

definition
  let SOURCE,p;
  mode BinHuffmanTree of p -> finite binary DecoratedTree of IndexedREAL means
:: HUFFMAN1:def 13

  ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL,
        q being FinSequence of NAT
  st Tseq,q,p is_constructingBinHuffmanTree &
  {it} = Tseq.(len Tseq);
end;

reserve T for BinHuffmanTree of p;

theorem :: HUFFMAN1:18
union LeavesSet(Initial-Trees p) = { z where z is Element of [:NAT,REAL:]
 :ex x be Element of SOURCE st z =[(canFS SOURCE)".x,p.{x}] };

theorem :: HUFFMAN1:19
 Tseq,q,p is_constructingBinHuffmanTree implies
 for i be Nat st 1 <= i & i <= len Tseq holds
 union LeavesSet(Tseq.i) = { z where z is Element of [:NAT,REAL:]
 :ex x be Element of SOURCE
 st z =[(canFS SOURCE)".x,p.{x}] };

theorem :: HUFFMAN1:20
 Leaves T ={ z where z is Element of [:NAT,REAL:]
 :ex x be Element of SOURCE
 st z =[(canFS SOURCE)".x,p.{x}] };

theorem :: HUFFMAN1:21
 Tseq,q,p is_constructingBinHuffmanTree implies
 for i be Nat
 for T be finite binary DecoratedTree of IndexedREAL
 for t,s,r be 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);

theorem :: HUFFMAN1:22
 for t,s,r be 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);

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

theorem :: HUFFMAN1:24
 Tseq,q,p is_constructingBinHuffmanTree implies
 for i be Nat st 1 <=i & i < len Tseq
 for X,Y be non empty finite Subset of BinFinTrees IndexedREAL
 st X=Tseq.i & Y = Tseq.(i+1) holds
 MaxVl(Y)=MaxVl(X) + 1;

theorem :: HUFFMAN1:25
 Tseq,q,p is_constructingBinHuffmanTree implies
 for i be Nat
 for X be non empty finite Subset of BinFinTrees IndexedREAL
 st X=Tseq.i holds
 for T be finite binary DecoratedTree of IndexedREAL st T in X holds
 for p be Element of (dom T), r be Element of NAT
 st r = (T.p) `1 holds r <= MaxVl(X);

theorem :: HUFFMAN1:26
 Tseq,q,p is_constructingBinHuffmanTree implies
 for i be Nat
 for X be non empty finite Subset of BinFinTrees IndexedREAL
 st X=Tseq.i
 for T be finite binary DecoratedTree of IndexedREAL st T in X
 for p be Element of (dom T), r be Element of NAT st r = (T.p) `1
 holds r <= MaxVl(X);

theorem :: HUFFMAN1:27
 Tseq,q,p is_constructingBinHuffmanTree implies
 for i be Nat
 for s,t be finite binary DecoratedTree of IndexedREAL
 for X be non empty finite Subset of BinFinTrees IndexedREAL
 st X=Tseq.i & s in X & t in X
 for z be finite binary DecoratedTree of IndexedREAL st z in X holds
 not [(MaxVl(X) + 1),(Vrootr t) +(Vrootr s)] in rng z;

registration
 let x be object;
 cluster root-tree x -> one-to-one;
end;

theorem :: HUFFMAN1:28
 for X be non empty finite Subset of BinFinTrees IndexedREAL,
 s,t,w be finite binary DecoratedTree of IndexedREAL st
 ( for T be finite binary DecoratedTree of IndexedREAL st T in X holds
 for p be Element of (dom T), r be Element of NAT st r = (T.p) `1
 holds r <= MaxVl(X) ) &
 ( for p,q be 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 = {};

theorem :: HUFFMAN1:29
 Tseq,q,p is_constructingBinHuffmanTree implies
 for i be Nat
 for T,S be finite binary DecoratedTree of IndexedREAL
 st T in Tseq.i & S in Tseq.i & T <> S
 holds rng T /\ rng S = {};

theorem :: HUFFMAN1:30
 for X be non empty finite Subset of BinFinTrees IndexedREAL,
 s,t be 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 be 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;

theorem :: HUFFMAN1:31
 Tseq,q,p is_constructingBinHuffmanTree implies
 for i be Nat
 for T be finite binary DecoratedTree of IndexedREAL
 st T in Tseq.i
 holds T is one-to-one;

registration
  let SOURCE,p;
  cluster -> one-to-one for BinHuffmanTree of p;
end;