Theory Optimal_BST_Examples

(* Author: Tobias Nipkow *)

theory Optimal_BST_Examples
imports "HOL-Library.Tree"
begin

text ‹Example by Mehlhorn:›

definition a_ex1 :: "int ⇒ nat" where
"a_ex1 i = [4,0,0,3,10] ! nat i"

definition b_ex1 :: "int ⇒ nat" where
"b_ex1 i = [1,3,3,0] ! nat i"

definition t_opt_ex1 :: "int tree" where
"t_opt_ex1 = ⟨⟨⟨⟩, 0, ⟨⟨⟩, 1, ⟨⟩⟩⟩, 2, ⟨⟨⟩, 3, ⟨⟩⟩⟩"

text ‹Example by Knuth:›

definition a_ex2 :: "int ⇒ nat" where
"a_ex2 i = 0"

definition b_ex2 :: "int ⇒ nat" where
"b_ex2 i = [32,7,69,13,6,15,10,8,64,142,22,79,18,9] ! nat i"

definition t_opt_ex2 :: "int tree" where
"t_opt_ex2 =
  ⟨
   ⟨
    ⟨⟨⟩, 0, ⟨⟨⟩, 1, ⟨⟩⟩⟩,
    2,
    ⟨
     ⟨
      ⟨⟨⟩, 3, ⟨⟨⟩, 4, ⟨⟩⟩⟩,
      5,
      ⟨⟨⟩, 6, ⟨⟨⟩, 7, ⟨⟩⟩⟩
     ⟩,
     8,
     ⟨⟩
    ⟩
   ⟩,
   9,
   ⟨⟨⟨⟩, 10, ⟨⟩⟩,
    11,
    ⟨⟨⟩, 12, ⟨⟨⟩, 13, ⟨⟩⟩
    ⟩
   ⟩
  ⟩"

end