Theory Benchmark_Comparison

theory Benchmark_Comparison imports 
  Main
begin

fun gen_build :: "natural ⇒ nat ⇒ (natural set × Random.seed) ⇒ (natural set × 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) (insert x A, seed'))"

declare gen_build.simps [simp del]

fun gen_remove :: "natural ⇒ nat ⇒ (natural set × Random.seed) ⇒ (natural set × 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) (Set.remove x A, seed'))"

declare gen_remove.simps [simp del]

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

fun gen_lookup :: "natural ⇒ natural set ⇒ 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 x ∈ A then hits + 1 else hits, seed'))"

declare gen_lookup.simps [simp del]

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

definition test :: "natural set ⇒ (natural ⇒ bool) ⇒ nat"
where "test A P = card (A ∩ {x. P x})"

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

text ‹@{term complete'} is @{term complete} without iteration›

definition complete' :: "nat ⇒ Random.seed ⇒ (natural × nat)"
where "complete' n seed =
  (let (A, seed') = build n seed;
       (hits, seed'') = lookup n (A, seed')
   in (hits, 0))"

end