Theory Benchmark_ICF

theory Benchmark_ICF 
imports 
  Benchmark_Comparison
  Collections.CollectionsV1
  "HOL-Library.Code_Target_Nat"
begin

locale benchmark_base = 
  fixes empty :: "unit ⇒ 's"
  and memb :: "natural ⇒ 's ⇒ bool"
  and ins :: "natural ⇒ 's ⇒ 's"
  and rem :: "natural ⇒ 's => 's"
  and size :: "'s ⇒ nat"
  and filter :: "(natural ⇒ bool) ⇒ 's ⇒ 's"
begin

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

declare gen_build.simps [simp del]

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

declare gen_remove.simps [simp del]

definition build :: "nat ⇒ Random.seed ⇒ ('s × Random.seed)"
where "build n seed = (let bound = of_nat n * 2 in gen_remove bound n (gen_build bound n (empty (), seed)))"

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

declare gen_lookup.simps [simp del]

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

definition test :: "'s ⇒ (natural ⇒ bool) ⇒ nat"
where "test A P = size (filter P A)"

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

end

lemmas [code] =
  benchmark_base.gen_build.simps
  benchmark_base.gen_remove.simps
  benchmark_base.build_def
  benchmark_base.gen_lookup.simps
  benchmark_base.lookup.simps
  benchmark_base.test_def
  benchmark_base.complete_def

locale benchmark = 
  benchmark_base empty memb ins rem size filter +
  set α invar +
  set_empty α invar empty +
  set_memb α invar memb +
  set_ins α invar ins +
  set_delete α invar rem +
  set_size α invar size +
  set_filter α invar α invar filter
  for α :: "'s ⇒ natural set"
  and invar :: "'s ⇒ bool"
  and empty :: "unit ⇒ 's"
  and memb :: "natural ⇒ 's ⇒ bool"
  and ins :: "natural ⇒ 's ⇒ 's"
  and rem :: "natural ⇒ 's ⇒ 's"
  and size :: "'s ⇒ nat"
  and filter :: "(natural ⇒ bool) ⇒ 's ⇒ 's"
begin

lemma gen_build_invar: "invar (fst As) ⟹ invar (fst (gen_build bound n As))"
apply(induct bound n As rule: gen_build.induct)
apply(subst gen_build.simps)
apply(simp add: split_beta ins_correct)
done

lemma α_gen_build: "invar (fst As) ⟹ apfst α (gen_build bound n As) = Benchmark_Comparison.gen_build bound n (apfst α As)"
apply(induct bound n As rule: gen_build.induct)
apply simp
apply(subst gen_build.simps)
apply(subst Benchmark_Comparison.gen_build.simps)
apply(simp add: split_beta ins_correct)
done

lemma gen_remove_invar: "invar (fst As) ⟹ invar (fst (gen_remove bound n As))"
apply(induct bound n As rule: gen_remove.induct)
apply(subst gen_remove.simps)
apply(simp add: split_beta delete_correct)
done

lemma α_gen_remove: "invar (fst As) ⟹ apfst α (gen_remove bound n As) = Benchmark_Comparison.gen_remove bound n (apfst α As)"
apply(induct bound n As rule: gen_remove.induct)
apply simp
apply(subst gen_remove.simps)
apply(subst Benchmark_Comparison.gen_remove.simps)
apply(simp add: split_beta delete_correct Set.remove_def)
done

lemma build_invar: "invar (fst (build n seed))"
by(simp add: build_def gen_build_invar gen_remove_invar Let_def empty_correct)

lemma α_build: "apfst α (build n seed) = Benchmark_Comparison.build n seed"
by(simp add: build_def Benchmark_Comparison.build_def empty_correct α_gen_build α_gen_remove gen_build_invar Let_def)

lemma α_gen_lookup: "invar A ⟹ gen_lookup bound A n hs = Benchmark_Comparison.gen_lookup bound (α A) n hs"
apply(induct A n hs rule: gen_lookup.induct)
apply(subst gen_lookup.simps)
apply(subst Benchmark_Comparison.gen_lookup.simps)
apply(simp add: split_beta memb_correct)
done

lemma α_lookup: "invar A ⟹ lookup n (A, seed) = Benchmark_Comparison.lookup n (α A, seed)"
by(simp add: α_gen_lookup)

lemma α_test: "invar A ⟹ test A P = Benchmark_Comparison.test (α A) P"
apply(simp only: test_def Benchmark_Comparison.test_def size_correct filter_correct)
apply(rule arg_cong[where f=card])
apply auto
done

lemma apfst_fst: "apfst f x = (f (fst x), snd x)"
by(cases x) simp

lemma case_prod_apfst: "(case (apfst f z) of (x, y) ⇒ g x y) = (case z of (x, y) ⇒ g (f x) y)"
by(cases z) simp

lemma α_complete: "complete n seed = Benchmark_Comparison.complete n seed"
apply(simp add: complete_def Benchmark_Comparison.complete_def α_test α_gen_lookup build_invar α_build[symmetric] α_gen_lookup[symmetric])
apply(simp add: split_beta α_gen_lookup[symmetric] build_invar α_test)
done

end

setup Locale_Code.open_block
interpretation gen_rr: g_set_xy_loc rs_ops rs_ops by unfold_locales
setup Locale_Code.close_block


definition rs_filter where "rs_filter = iflt_filter gen_rr.g_inj_image_filter"
lemmas rs_filter_impl = iflt_filter_correct[OF gen_rr.g_inj_image_filter_impl, folded rs_filter_def]
interpretation rs: set_filter rs_α rs_invar rs_α rs_invar rs_filter using rs_filter_impl .

interpretation rs: benchmark rs_α rs_invar rs_empty rs_memb rs_ins rs_delete rs_size rs_filter
by(unfold_locales)

definition complete where "complete = rs.complete"

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

end