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
    by transfer (simp add: bit_eq_iff, auto simp add: bit_simps)

  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
    by transfer (simp add: bit_eq_iff, auto simp add: bit_simps)

  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
    by transfer (simp add: bit_eq_iff, auto simp add: bit_simps)

  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
    by transfer (simp add: bit_eq_iff, auto simp add: bit_simps)

  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
    by transfer (simp add: bit_eq_iff, auto simp add: bit_simps)

  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
    by transfer (simp add: bit_eq_iff, auto simp add: bit_simps)

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 AND bin_mask (i - 1) = s" by (simp add: int_and_mask `s≥0`)
    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
    by (smt bin_mask_ge0 bin_mask_p1_conv_shift)


  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"
    by (simp add: shiftl_int_def)

  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)
    apply (simp_all add: bs_set_rel_def br_def)

  proof (clarsimp)



  definition 

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

  end"


*)


end