Theory Impl_Bit_Set

```section "Bitvector based Sets of Naturals"
theory Impl_Bit_Set
imports
"../../Iterator/Iterator"
"../Intf/Intf_Set"
Native_Word.Code_Target_Integer_Bit
begin
text ‹
Based on the Native-Word library, using bit-operations on arbitrary
precision integers. Fast for sets of small numbers,
direct and fast implementations of equal, union, inter, diff.

Note: On Poly/ML 5.5.1, bit-operations on arbitrary precision integers are
rather inefficient. Use MLton instead, here they are efficiently implemented.
›

type_synonym bitset = integer

definition bs_α :: "bitset ⇒ nat set" where "bs_α s ≡ { n . bit s n}"

context
includes integer.lifting bit_operations_syntax
begin

definition bs_empty :: "unit ⇒ bitset" where "bs_empty ≡ λ_. 0"

lemma bs_empty_correct: "bs_α (bs_empty ()) = {}"
unfolding bs_α_def bs_empty_def
apply transfer
by auto

definition bs_isEmpty :: "bitset ⇒ bool" where "bs_isEmpty s ≡ s=0"

lemma bs_isEmpty_correct: "bs_isEmpty s ⟷ bs_α s = {}"
unfolding bs_isEmpty_def bs_α_def
by transfer (auto simp: bit_eq_iff)

term set_bit
definition bs_insert :: "nat ⇒ bitset ⇒ bitset" where
"bs_insert i s ≡ set_bit s i True"

lemma bs_insert_correct: "bs_α (bs_insert i s) = insert i (bs_α s)"
unfolding bs_α_def bs_insert_def
by transfer (auto simp add: bit_simps)

definition bs_delete :: "nat ⇒ bitset ⇒ bitset" where
"bs_delete i s ≡ set_bit s i False"

lemma bs_delete_correct: "bs_α (bs_delete i s) = (bs_α s) - {i}"
unfolding bs_α_def bs_delete_def
by transfer (auto simp add: bit_simps split: if_splits)

definition bs_mem :: "nat ⇒ bitset ⇒ bool" where
"bs_mem i s ≡ bit s i"

lemma bs_mem_correct: "bs_mem i s ⟷ i∈bs_α s"
unfolding bs_mem_def bs_α_def by transfer auto

definition bs_eq :: "bitset ⇒ bitset ⇒ bool" where
"bs_eq s1 s2 ≡ (s1=s2)"

lemma bs_eq_correct: "bs_eq s1 s2 ⟷ bs_α s1 = bs_α s2"
unfolding bs_eq_def bs_α_def
including integer.lifting
by transfer (simp add: bit_eq_iff set_eq_iff)

definition bs_subset_eq :: "bitset ⇒ bitset ⇒ bool" where
"bs_subset_eq s1 s2 ≡ s1 AND NOT s2 = 0"

lemma bs_subset_eq_correct: "bs_subset_eq s1 s2 ⟷ bs_α s1 ⊆ bs_α s2"
unfolding bs_α_def bs_subset_eq_def

definition bs_disjoint :: "bitset ⇒ bitset ⇒ bool" where
"bs_disjoint s1 s2 ≡ s1 AND s2 = 0"

lemma bs_disjoint_correct: "bs_disjoint s1 s2 ⟷ bs_α s1 ∩ bs_α s2 = {}"
unfolding bs_α_def bs_disjoint_def

definition bs_union :: "bitset ⇒ bitset ⇒ bitset" where
"bs_union s1 s2 = s1 OR s2"

lemma bs_union_correct: "bs_α (bs_union s1 s2) = bs_α s1 ∪ bs_α s2"
unfolding bs_α_def bs_union_def

definition bs_inter :: "bitset ⇒ bitset ⇒ bitset" where
"bs_inter s1 s2 = s1 AND s2"

lemma bs_inter_correct: "bs_α (bs_inter s1 s2) = bs_α s1 ∩ bs_α s2"
unfolding bs_α_def bs_inter_def

definition bs_diff :: "bitset ⇒ bitset ⇒ bitset" where
"bs_diff s1 s2 = s1 AND NOT s2"

lemma bs_diff_correct: "bs_α (bs_diff s1 s2) = bs_α s1 - bs_α s2"
unfolding bs_α_def bs_diff_def

definition bs_UNIV :: "unit ⇒ bitset" where "bs_UNIV ≡ λ_. -1"

lemma bs_UNIV_correct: "bs_α (bs_UNIV ()) = UNIV"
unfolding bs_α_def bs_UNIV_def
by transfer (auto)

definition bs_complement :: "bitset ⇒ bitset" where
"bs_complement s = NOT s"

lemma bs_complement_correct: "bs_α (bs_complement s) = - bs_α s"
unfolding bs_α_def bs_complement_def

end

lemmas bs_correct[simp] =
bs_empty_correct
bs_isEmpty_correct
bs_insert_correct
bs_delete_correct
bs_mem_correct
bs_eq_correct
bs_subset_eq_correct
bs_disjoint_correct
bs_union_correct
bs_inter_correct
bs_diff_correct
bs_UNIV_correct
bs_complement_correct

subsection ‹Autoref Setup›

definition bs_set_rel_def_internal:
"bs_set_rel Rk ≡
if Rk=nat_rel then br bs_α (λ_. True) else {}"
lemma bs_set_rel_def:
"⟨nat_rel⟩bs_set_rel ≡ br bs_α (λ_. True)"
unfolding bs_set_rel_def_internal relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of "bs_set_rel" i_set]

lemma bs_set_rel_sv[relator_props]: "single_valued (⟨nat_rel⟩bs_set_rel)"
unfolding bs_set_rel_def by auto

term bs_empty

lemma [autoref_rules]: "(bs_empty (),{})∈⟨nat_rel⟩bs_set_rel"
by (auto simp: bs_set_rel_def br_def)

lemma [autoref_rules]: "(bs_UNIV (),UNIV)∈⟨nat_rel⟩bs_set_rel"
by (auto simp: bs_set_rel_def br_def)

lemma [autoref_rules]: "(bs_isEmpty,op_set_isEmpty)∈⟨nat_rel⟩bs_set_rel → bool_rel"
by (auto simp: bs_set_rel_def br_def)

term insert
lemma [autoref_rules]: "(bs_insert,insert)∈nat_rel → ⟨nat_rel⟩bs_set_rel → ⟨nat_rel⟩bs_set_rel"
by (auto simp: bs_set_rel_def br_def)

term op_set_delete
lemma [autoref_rules]: "(bs_delete,op_set_delete)∈nat_rel → ⟨nat_rel⟩bs_set_rel → ⟨nat_rel⟩bs_set_rel"
by (auto simp: bs_set_rel_def br_def)

lemma [autoref_rules]: "(bs_mem,(∈))∈nat_rel → ⟨nat_rel⟩bs_set_rel → bool_rel"
by (auto simp: bs_set_rel_def br_def)

lemma [autoref_rules]: "(bs_eq,(=))∈⟨nat_rel⟩bs_set_rel → ⟨nat_rel⟩bs_set_rel → bool_rel"
by (auto simp: bs_set_rel_def br_def)

lemma [autoref_rules]: "(bs_subset_eq,(⊆))∈⟨nat_rel⟩bs_set_rel → ⟨nat_rel⟩bs_set_rel → bool_rel"
by (auto simp: bs_set_rel_def br_def)

lemma [autoref_rules]: "(bs_union,(∪))∈⟨nat_rel⟩bs_set_rel → ⟨nat_rel⟩bs_set_rel → ⟨nat_rel⟩bs_set_rel"
by (auto simp: bs_set_rel_def br_def)

lemma [autoref_rules]: "(bs_inter,(∩))∈⟨nat_rel⟩bs_set_rel → ⟨nat_rel⟩bs_set_rel → ⟨nat_rel⟩bs_set_rel"
by (auto simp: bs_set_rel_def br_def)

lemma [autoref_rules]: "(bs_diff,(-))∈⟨nat_rel⟩bs_set_rel → ⟨nat_rel⟩bs_set_rel → ⟨nat_rel⟩bs_set_rel"
by (auto simp: bs_set_rel_def br_def)

lemma [autoref_rules]: "(bs_complement,uminus)∈⟨nat_rel⟩bs_set_rel → ⟨nat_rel⟩bs_set_rel"
by (auto simp: bs_set_rel_def br_def)

lemma [autoref_rules]: "(bs_disjoint,op_set_disjoint)∈⟨nat_rel⟩bs_set_rel → ⟨nat_rel⟩bs_set_rel → bool_rel"
by (auto simp: bs_set_rel_def br_def)

export_code
bs_empty
bs_isEmpty
bs_insert
bs_delete
bs_mem
bs_eq
bs_subset_eq
bs_disjoint
bs_union
bs_inter
bs_diff
bs_UNIV
bs_complement
in SML

(*

TODO: Iterator

definition "maxbi s ≡ GREATEST i. s!!i"

lemma cmp_BIT_append_conv[simp]: "i < i BIT b ⟷ ((i≥0 ∧ b=1) ∨ i>0)"
by (cases b) (auto simp: Bit_B0 Bit_B1)

lemma BIT_append_cmp_conv[simp]: "i BIT b < i ⟷ ((i<0 ∧ (i=-1 ⟶ b=0)))"
by (cases b) (auto simp: Bit_B0 Bit_B1)

lemma BIT_append_eq[simp]: fixes i :: int shows "i BIT b = i ⟷ (i=0 ∧ b=0) ∨ (i=-1 ∧ b=1)"
by (cases b) (auto simp: Bit_B0 Bit_B1)

lemma int_no_bits_eq_zero[simp]:
fixes s::int shows "(∀i. ¬s!!i) ⟷ s=0"
apply clarsimp
by (metis bin_eqI bin_nth_code(1))

lemma int_obtain_bit:
fixes s::int
assumes "s≠0"
obtains i where "s!!i"
by (metis assms int_no_bits_eq_zero)

lemma int_bit_bound:
fixes s::int
assumes "s≥0" and "s!!i"
shows "i ≤ Bits_Integer.log2 s"
proof (rule ccontr)
assume "¬i≤Bits_Integer.log2 s"
hence "i>Bits_Integer.log2 s" by simp
hence "i - 1 ≥ Bits_Integer.log2 s" by simp
hence "¬ (s!!i)"
by clarsimp (metis Nat.diff_le_self bin_nth_mask bin_nth_ops(1) leD)
thus False using `s!!i` ..
qed

lemma int_bit_bound':
fixes s::int
assumes "s≥0" and "s!!i"
shows "i < Bits_Integer.log2 s + 1"
using assms int_bit_bound by smt

lemma int_obtain_bit_pos:
fixes s::int
assumes "s>0"
obtains i where "s!!i" "i < Bits_Integer.log2 s + 1"
by (metis assms int_bit_bound' int_no_bits_eq_zero less_imp_le less_irrefl)

lemma maxbi_set: fixes s::int shows "s>0 ⟹ s!!maxbi s"
unfolding maxbi_def
apply (rule int_obtain_bit_pos, assumption)
apply (rule GreatestI_nat, assumption)
apply (intro allI impI)
apply (rule int_bit_bound'[rotated], assumption)
by auto

lemma maxbi_max: fixes s::int shows "i>maxbi s ⟹ ¬ s!!i"
oops

function get_maxbi :: "nat ⇒ int ⇒ nat" where
"get_maxbi n s = (let
b = 1<<n
in
if b≤s then get_maxbi (n+1) s
else n
)"
by pat_completeness auto

termination
apply (rule "termination"[of "measure (λ(n,s). nat (s + 1 - (1<<n)))"])
apply simp
apply auto

partial_function (tailrec)
bs_iterate_aux :: "nat ⇒ bitset ⇒ ('σ ⇒ bool) ⇒ (nat ⇒ 'σ ⇒ 'σ) ⇒ 'σ ⇒ 'σ"
where "bs_iterate_aux i s c f σ = (
if s < 1 << i then σ
else if ¬c σ then σ
else if test_bit s i then bs_iterate_aux (i+1) s c f (f i σ)
else bs_iterate_aux (i+1) s c f σ
)"

definition bs_iteratei :: "bitset ⇒ (nat,'σ) set_iterator" where
"bs_iteratei s = bs_iterate_aux 0 s"

definition bs_set_rel_def_internal:
"bs_set_rel Rk ≡
if Rk=nat_rel then br bs_α (λ_. True) else {}"
lemma bs_set_rel_def:
"⟨nat_rel⟩bs_set_rel ≡ br bs_α (λ_. True)"
unfolding bs_set_rel_def_internal relAPP_def by simp

definition "bs_to_list ≡ it_to_list bs_iteratei"

lemma "(1::int)<<i = 2^i"

lemma
fixes s :: int
assumes "s≥0"
shows "s < 1<<i ⟷ Bits_Integer.log2 s ≤ i"
using assms
proof (induct i arbitrary: s)
case 0 thus ?case by auto
next
case (Suc i)
note GE=`0≤s`
show ?case proof
assume "s < 1 << Suc i"

have "s ≤ (s >> 1) BIT 1"

hence "(s >> 1) < (1<<i)" using GE apply auto
with Suc.hyps[of "s div 2"]

apply auto

lemma "distinct (bs_to_list s)"
unfolding bs_to_list_def it_to_list_def bs_iteratei_def[abs_def]
proof -
{
fix l i
assume "distinct l"
show "distinct (bs_iterate_aux 0 s (λ_. True) (λx l. l @ [x]) [])"

}

apply auto

lemma "set (bs_to_list s) = bs_α s"

lemma autoref_iam_is_iterator[autoref_ga_rules]:
shows "is_set_to_list nat_rel bs_set_rel bs_to_list"
unfolding is_set_to_list_def is_set_to_sorted_list_def
apply clarsimp
unfolding it_to_sorted_list_def
apply (refine_rcg refine_vcg)

proof (clarsimp)

definition

"iterate s c f σ ≡ let
i=0;
b=0;
(_,_,s) = while
in

end"

*)

end
```