Theory Benchmark_Set

theory Benchmark_Set
imports
  "HOL-Library.Word"
  "HOL-Library.Cardinality"
begin

instantiation word :: (len) card_UNIV begin
definition "finite_UNIV = Phantom('a word) True"
definition "card_UNIV = Phantom('a word) (2 ^ LENGTH('a))"
instance by(intro_classes)(simp_all add: card_UNIV_word_def card_word finite_UNIV_word_def)
end

definition word_of_integer :: "integer ⇒ 'a::len word"
where "word_of_integer = word_of_int ∘ int_of_integer"

lemma word_of_integer_code [code]:
  "word_of_integer k = 
  (if k < 0 then - word_of_integer (- k)
   else if k = 0 then 0
   else let (q, r) = divmod_integer k 2
        in if r = 0 then 2 * word_of_integer q else 2 * word_of_integer q + 1)"
  apply (unfold word_of_integer_def)
  apply transfer
  apply (auto simp add: not_less comp_def split_beta)
  apply (subst int_of_integer_code)
  apply (clarsimp simp add: divmod_integer_def)
  done

definition word_of :: "natural ⇒ 'a::len word"
where "word_of = word_of_integer o integer_of_natural"

text ‹randomly generate a set of (up to) n elements drawn from 0 to bound›

fun gen_build1 :: "natural ⇒ nat ⇒ (32 word set × Random.seed) ⇒ (32 word set × Random.seed)"
where 
  "gen_build1 bound n (A, seed) =
  (if n = 0 then (A, seed) 
   else let (x, seed') = Random.range bound seed in gen_build1 bound (n - 1) (insert (word_of x) A, seed'))"

declare gen_build1.simps[simp del]

definition build1 :: "natural ⇒ Random.seed ⇒ (32 word set × Random.seed)"
where 
  "build1 bound seed =
  (let (n', seed') = Random.range bound seed;
       (compl, seed'') = Random.range 2 seed;
       (x, seed''') = gen_build1 bound (Code_Numeral.nat_of_natural n') ({}, seed'')
   in (if compl = 0 then x else - x, seed'''))"

text ‹randomly generate a set of (up to) n sets each with a random number between 0 and bound of elements between 0 and bound›

fun gen_build2 :: "natural ⇒ nat ⇒ (32 word set set × Random.seed) ⇒ (32 word set set × Random.seed)"
where
  "gen_build2 bound n (A, seed) =
  (if n = 0 then (A, seed)
   else let (x, seed') = build1 bound seed
        in gen_build2 bound (n - 1) (insert x A, seed'))"

declare gen_build2.simps[simp del]

definition build :: "nat ⇒ nat ⇒ Random.seed ⇒ 32 word set set × Random.seed"
where "build n m seed = gen_build2 (of_nat m) n ({}, seed)"

fun gen_lookup :: "32 word set set ⇒ natural ⇒ nat ⇒ (nat × Random.seed) ⇒ (nat × Random.seed)"
where
  "gen_lookup A bound n (hits, seed) =
  (if n = 0 then (hits, seed)
   else let (x, seed') = build1 bound seed
        in gen_lookup A bound (n - 1) (if x : A then hits + 1 else hits, seed'))"

declare gen_lookup.simps [simp del]

primrec lookup :: "nat ⇒ nat ⇒ (32 word set set × Random.seed) ⇒ (nat × Random.seed)"
where "lookup n m (A, seed) = gen_lookup A (of_nat m) 100 (0, seed)"

definition covered :: "32 word set set ⇒ nat"
where "covered A = card (⋃A)"

definition complete :: "nat ⇒ nat ⇒ Random.seed ⇒ (nat × nat)"
where "complete n m seed = (let (A, seed') = build n m seed in (fst (lookup n m (A, seed)), covered A))"

end