Theory Benchmark_RBT

theory Benchmark_RBT 
imports 
  Benchmark_Comparison
  "HOL-Library.RBT_Impl"
  "HOL-Library.Code_Target_Nat"
begin

fun gen_build :: "natural ⇒ nat ⇒ ((natural, unit) rbt × Random.seed) ⇒ ((natural, unit) rbt × Random.seed)"
where 
  "gen_build bound n (A, seed) =
  (if n = 0 then (A, seed) 
   else let (x, seed') = Random.range bound seed in gen_build bound (n - 1) (rbt_insert x () A, seed'))"

declare gen_build.simps [simp del]

fun gen_remove :: "natural ⇒ nat ⇒ ((natural, unit) rbt × Random.seed) ⇒ ((natural, unit) rbt × Random.seed)"
where
  "gen_remove bound n (A, seed) =
  (if n = 0 then (A, seed)
   else let (x, seed') = Random.range bound seed in gen_remove bound (n - 1) (rbt_delete x A, seed'))"

declare gen_remove.simps [simp del]

definition build :: "nat ⇒ Random.seed ⇒ ((natural, unit) rbt × Random.seed)"
where "build n seed = (let bound = of_nat n * 2 in gen_remove bound n (gen_build bound n (rbt.Empty, seed)))"

fun gen_lookup :: "natural ⇒ (natural, unit) rbt ⇒ nat ⇒ (natural × Random.seed) ⇒ (natural × Random.seed)"
where
  "gen_lookup bound A n (hits, seed) =
  (if n = 0 then (hits, seed)
   else let (x, seed') = Random.range bound seed in gen_lookup bound A (n - 1) (if rbt_lookup A x = Some () then hits + 1 else hits, seed'))"

declare gen_lookup.simps [simp del]

primrec lookup :: "nat ⇒ ((natural, unit) rbt × Random.seed) ⇒ (natural × Random.seed)"
where "lookup n (A, seed) = gen_lookup (of_nat n * 2) A n (0, seed)"

definition test :: "(natural, unit) rbt ⇒ (natural ⇒ bool) ⇒ nat"
where "test A P = RBT_Impl.fold (λx _ i. if P x then i + 1 else i) A 0"

definition complete :: "nat ⇒ Random.seed ⇒ (natural × nat)"
where 
  "complete n seed =
  (let (A, seed') = build n seed;
       (hits, seed'') = lookup n (A, seed');
       less = test A (λx. x ≤ of_nat n)
   in (hits, less))"

notepad begin
  have "complete 200 (12345, 67889) = (48, 50)" by eval
end

end