Theory Benchmark_Set_LC

theory Benchmark_Set_LC
imports 
  Benchmark_Set
  Containers.Set_Impl
  "HOL-Library.Code_Target_Nat"
begin

instantiation word :: (len) ceq begin
definition "CEQ('a word) = Some (=)"
instance by(intro_classes)(simp add: ceq_word_def)
end

instantiation word :: (len) compare begin
definition "compare_word = (comparator_of :: 'a word comparator)"
instance by(intro_classes)(simp add: compare_word_def comparator_of)
end

instantiation word :: (len) ccompare begin
definition "CCOMPARE('a word) = Some compare"
instance by(intro_classes)(simp add: ccompare_word_def comparator_compare)
end

instantiation word :: (len) set_impl begin
definition "SET_IMPL('a word) = Phantom('a word) set_RBT"
instance ..
end

instantiation word :: (len) proper_interval begin

fun proper_interval_word :: "'a word option ⇒ 'a word option ⇒ bool"
where
  "proper_interval_word None None = True"
| "proper_interval_word None (Some y) = (y ≠ 0)"
| "proper_interval_word (Some x) None = (x ≠ - 1)"
| "proper_interval_word (Some x) (Some y) = (x < y ∧ x ≠ y - 1)"

instance
proof
  let ?pi = "proper_interval :: 'a word proper_interval"
  show "?pi None None = True" by simp
  fix y
  show "?pi None (Some y) = (∃z. z < y)"
    using word_neq_0_conv [of y] by auto
  fix x
  show "?pi (Some x) None = (∃z. x < z)"
    using word_order.not_eq_extremum [of x] by auto

  have "(x < y ∧ x ≠ y - 1) = (∃z>x. z < y)" (is "?lhs ⟷ ?rhs")
  proof
    assume ?lhs
    then obtain "x < y" "x ≠ y - 1" ..
    have "0 ≤ uint x" by simp
    also have "… < uint y" using ‹x < y› by(simp add: word_less_def)
    finally have "0 < uint y" .
    then have "y - 1 < y" by(simp add: word_less_def uint_sub_if' not_le)
    moreover from ‹0 < uint y› ‹x < y› ‹x ≠ y - 1›
    have "x < y - 1" by(simp add: word_less_def uint_sub_if' uint_arith_simps(3))
    ultimately show ?rhs by blast
  next
    assume ?rhs
    then obtain z where z: "x < z" "z < y" by blast
    have "0 ≤ uint z" by simp
    also have "… < uint y" using ‹z < y› by(simp add: word_less_def)
    finally show ?lhs using z by(auto simp add: word_less_def uint_sub_if')
  qed
  thus "?pi (Some x) (Some y) = (∃z>x. z < y)" by simp
qed

end

instantiation word :: (len) cproper_interval begin
definition "cproper_interval = (proper_interval :: 'a word proper_interval)"
instance by( intro_classes, simp add: cproper_interval_word_def ccompare_word_def 
  compare_word_def le_lt_comparator_of ID_Some proper_interval_class.axioms)
end

instantiation word :: (len) cenum begin
definition "CENUM('a word) = None"
instance by(intro_classes)(simp_all add: cEnum_word_def)
end

notepad begin
  have "Benchmark_Set.complete 30 40 (12345, 67899) = (32, 4294967296)" by eval
end

end