Theory Impl_Uv_Set

theory Impl_Uv_Set
imports
  "../../Iterator/Iterator"
  "../Intf/Intf_Set"
  Native_Word.Uint
begin

  subsection ‹Bit-Vectors as Lists of Words›

  subsubsection ‹Lookup›

  primrec lookup :: "nat ⇒ ('a::len) word list ⇒ bool" where
    "lookup _ [] ⟷ False"
  | "lookup n (w#ws)
      ⟷ (if n<LENGTH('a) then bit w n else lookup (n-LENGTH('a)) ws)"

  lemma lookup_append[simp]: "lookup n (w1@w2 :: 'a::len word list)
    ⟷ (
      if n < LENGTH('a) * length w1 then
        lookup n w1
      else lookup (n - LENGTH('a) * length w1) w2)"
    by (induction w1 arbitrary: n) auto

  lemma lookup_zeroes[simp]: "lookup i (replicate n (0::'a::len word)) = False"
    by (induction n arbitrary: i) auto

  lemma lookup_out_of_bound:
    fixes uv :: "'a::len word list"
    assumes "¬ i < LENGTH('a::len) * length uv"
    shows "¬ lookup i uv"
    using assms
    by (induction uv arbitrary: i) auto


  subsubsection ‹Empty›

  definition empty :: "'a::len word list" where "empty = []"

  subsubsection ‹Set and Reset Bit›

  function single_bit :: "nat ⇒ ('a::len) word list"
    where "single_bit n = (
      if (n<LENGTH('a)) then
        [set_bit 0 n True]
      else 0#single_bit (n-LENGTH('a)))"
    by pat_completeness auto
  termination
    apply (relation "measure id")
    apply simp
    apply (simp add: not_less less_diff_conv2)
    done

  declare single_bit.simps[simp del]

  lemma lookup_single_bit[simp]: "lookup i ((single_bit n)::'a::len word list) ⟷ i = n"
    apply (induction n arbitrary: i rule: single_bit.induct)
    apply (subst single_bit.simps)
    apply (auto simp add: bit_simps)
    done

  primrec set_bit :: "nat ⇒ 'a::len word list ⇒ 'a::len word list" where
    "set_bit i [] = single_bit i"
  | "set_bit i (w#ws) = (
      if i<LENGTH('a) then
        Bit_Operations.set_bit i w # ws
      else
        w # set_bit (i - LENGTH('a)) ws)"

  lemma set_bit_lookup[simp]: "lookup i (set_bit j ws) ⟷ (lookup i ws ∨ i=j)"
    apply (induction ws arbitrary: i j)
     apply (auto simp add: word_size Bit_Operations.bit_set_bit_iff)
    done

  primrec reset_bit :: "nat ⇒ 'a::len word list ⇒ 'a::len word list" where
    "reset_bit i [] = []"
  | "reset_bit i (w#ws) = (
      if i<LENGTH('a) then
        unset_bit i w # ws
      else
        w # reset_bit (i - LENGTH('a)) ws)"

  lemma reset_bit_lookup[simp]: "lookup i (reset_bit j ws) ⟷ (lookup i ws ∧ i≠j)"
    apply (induction ws arbitrary: i j)
    apply (auto simp: word_size bit_unset_bit_iff)
    done

  subsubsection ‹Binary Operations›

  context
    includes bit_operations_syntax
  begin

  definition
    is_bin_op_impl
    :: "(bool⇒bool⇒bool) ⇒ ('a::len word ⇒ 'a::len word ⇒ 'a::len word) ⇒ bool"
    where "is_bin_op_impl f g ≡
    (∀w v.  ∀i<LENGTH('a). bit (g w v) i ⟷ f (bit w i) (bit v i))"

  definition "is_strict_bin_op_impl f g ≡ is_bin_op_impl f g ∧ f False False = False"

  fun binary :: "('a::len word ⇒ 'a::len word ⇒ 'a::len word)
    ⇒ 'a::len word list ⇒ 'a::len word list ⇒ 'a::len word list"
    where
    "binary f [] [] = []"
  | "binary f [] (w#ws) = f 0 w # binary f [] ws"
  | "binary f (v#vs) [] = f v 0 # binary f vs []"
  | "binary f (v#vs) (w#ws) = f v w # binary f vs ws"

  lemma binary_lookup:
    assumes "is_strict_bin_op_impl f g"
    shows "lookup i (binary g ws vs) ⟷ f (lookup i ws) (lookup i vs)"
    using assms
    apply (induction g ws vs arbitrary: i rule: binary.induct)
    apply (auto simp: is_strict_bin_op_impl_def is_bin_op_impl_def)
    done

  subsection ‹Abstraction to Sets of Naturals›

  definition "α uv ≡ {n. lookup n uv}"

  lemma memb_correct: "lookup i ws ⟷ i∈α ws"
    by (auto simp: α_def)

  lemma empty_correct: "α empty = {}"
    by (simp add: α_def empty_def)

  lemma single_bit_correct: "α (single_bit n) = {n}"
    by (simp add: α_def)

  lemma insert_correct: "α (set_bit i ws) = Set.insert i (α ws)"
    by (auto simp add: α_def)

  lemma delete_correct: "α (reset_bit i ws) = (α ws) - {i}"
    by (auto simp add: α_def)

  lemma binary_correct:
    assumes "is_strict_bin_op_impl f g"
    shows "α (binary g ws vs) = { i . f (i∈α ws) (i∈α vs) }"
    unfolding α_def
    by (auto simp add: binary_lookup[OF assms])

  fun union :: "'a::len word list ⇒ 'a::len word list ⇒ 'a::len word list"
    where
    "union [] ws = ws"
  | "union vs [] = vs"
  | "union (v#vs) (w#ws) = (v OR w) # union vs ws"

  lemma union_lookup[simp]:
    fixes vs :: "'a::len word list"
    shows "lookup i (union vs ws) ⟷ lookup i vs ∨ lookup i ws"
    apply (induction vs ws arbitrary: i rule: union.induct)
    apply (auto simp: word_ao_nth)
    done

  lemma union_correct: "α (union ws vs) = α ws ∪ α vs"
    by (auto simp add: α_def)

  fun inter :: "'a::len word list ⇒ 'a::len word list ⇒ 'a::len word list"
    where
    "inter [] ws = []"
  | "inter vs [] = []"
  | "inter (v#vs) (w#ws) = (v AND w) # inter vs ws"

  lemma inter_lookup[simp]:
    fixes vs :: "'a::len word list"
    shows "lookup i (inter vs ws) ⟷ lookup i vs ∧ lookup i ws"
    apply (induction vs ws arbitrary: i rule: inter.induct)
    apply (auto simp: word_ao_nth)
    done

  lemma inter_correct: "α (inter ws vs) = α ws ∩ α vs"
    by (auto simp add: α_def)


  fun diff :: "'a::len word list ⇒ 'a::len word list ⇒ 'a::len word list"
    where
    "diff [] ws = []"
  | "diff vs [] = vs"
  | "diff (v#vs) (w#ws) = (v AND NOT w) # diff vs ws"

  lemma diff_lookup[simp]:
    fixes vs :: "'a::len word list"
    shows "lookup i (diff vs ws) ⟷ lookup i vs - lookup i ws"
    apply (induction vs ws arbitrary: i rule: diff.induct)
    apply (auto simp: word_ops_nth_size word_size)
    done

  lemma diff_correct: "α (diff ws vs) = α ws - α vs"
    by (auto simp add: α_def)

  fun zeroes :: "'a::len word list ⇒ bool" where
    "zeroes [] ⟷ True"
  | "zeroes (w#ws) ⟷ w=0 ∧ zeroes ws"

  lemma zeroes_lookup: "zeroes ws ⟷ (∀i. ¬lookup i ws)"
    apply (induction ws)
    apply (auto simp: word_eq_iff)
    by (metis diff_add_inverse2 not_add_less2)

  lemma isEmpty_correct: "zeroes ws ⟷ α ws = {}"
    by (auto simp: zeroes_lookup α_def)

  fun equal :: "'a::len word list ⇒ 'a::len word list ⇒ bool" where
    "equal [] [] ⟷ True"
  | "equal [] ws ⟷ zeroes ws"
  | "equal vs [] ⟷ zeroes vs"
  | "equal (v#vs) (w#ws) ⟷ v=w ∧ equal vs ws"

  lemma equal_lookup:
    fixes vs ws :: "'a::len word list"
    shows "equal vs ws ⟷ (∀i. lookup i vs = lookup i ws)"
  proof (induction vs ws rule: equal.induct)
    fix v w and vs ws :: "'a::len word list"
    assume IH: "equal vs ws = (∀i. lookup i vs = lookup i ws)"
    show "equal (v # vs) (w # ws) = (∀i. lookup i (v # vs) = lookup i (w # ws))"
    proof (rule iffI, rule allI)
      fix i
      assume "equal (v#vs) (w#ws)"
      thus "lookup i (v # vs) = lookup i (w # ws)"
        by (auto simp: IH)
    next
      assume "∀i. lookup i (v # vs) = lookup i (w # ws)"
      thus "equal (v # vs) (w # ws)"
        apply (auto simp: word_eq_iff IH)
        apply metis
        apply metis
        apply (drule_tac x="i + LENGTH('a)" in spec)
        apply auto []
        apply (drule_tac x="i + LENGTH('a)" in spec)
        apply auto []
        done
    qed
  qed (auto simp: zeroes_lookup)

  lemma equal_correct: "equal vs ws ⟷ α vs = α ws"
    by (auto simp: α_def equal_lookup)

  fun subseteq :: "'a::len word list ⇒ 'a::len word list ⇒ bool" where
    "subseteq [] ws ⟷ True"
  | "subseteq vs [] ⟷ zeroes vs"
  | "subseteq (v#vs) (w#ws) ⟷ (v AND NOT w = 0) ∧ subseteq vs ws"


  lemma subseteq_lookup:
    fixes vs ws :: "'a::len word list"
    shows "subseteq vs ws ⟷ (∀i. lookup i vs ⟶ lookup i ws)"
    apply (induction vs ws rule: subseteq.induct)
    apply simp
    apply (auto simp: zeroes_lookup) []
    apply (auto simp: word_ops_nth_size word_size word_eq_iff)
    by (metis diff_add_inverse2 not_add_less2)

  lemma subseteq_correct: "subseteq vs ws ⟷ α vs ⊆ α ws"
    by (auto simp: α_def subseteq_lookup)


  fun subset :: "'a::len word list ⇒ 'a::len word list ⇒ bool" where
    "subset [] ws ⟷ ¬zeroes ws"
  | "subset vs [] ⟷ False"
  | "subset (v#vs) (w#ws) ⟷ (if v=w then subset vs ws else subseteq (v#vs) (w#ws))"

  lemma subset_lookup:
    fixes vs ws :: "'a::len word list"
    shows "subset vs ws ⟷ ((∀i. lookup i vs ⟶ lookup i ws)
      ∧ (∃i. ¬lookup i vs ∧ lookup i ws))"
    apply (induction vs ws rule: subset.induct)
    apply (simp add: zeroes_lookup)
    apply (simp add: zeroes_lookup) []
    apply (simp add: subseteq_lookup)
    apply safe
    apply simp_all
    apply (auto simp: word_ops_nth_size word_size word_eq_iff)
    done

  lemma subset_correct: "subset vs ws ⟷ α vs ⊂ α ws"
    by (auto simp: α_def subset_lookup)


  fun disjoint :: "'a::len word list ⇒ 'a::len word list ⇒ bool" where
    "disjoint [] ws ⟷ True"
  | "disjoint vs [] ⟷ True"
  | "disjoint (v#vs) (w#ws) ⟷ (v AND w = 0) ∧ disjoint vs ws"

  lemma disjoint_lookup:
    fixes vs ws :: "'a::len word list"
    shows "disjoint vs ws ⟷ (∀i. ¬(lookup i vs ∧ lookup i ws))"
    apply (induction vs ws rule: disjoint.induct)
    apply simp
    apply simp
    apply (auto simp: word_ops_nth_size word_size word_eq_iff)
    by (metis diff_add_inverse2 not_add_less2)

  lemma disjoint_correct: "disjoint vs ws ⟷ α vs ∩ α ws = {}"
    by (auto simp: α_def disjoint_lookup)


subsection ‹Lifting to Uint›
  type_synonym uint_vector = "uint list"

  lift_definition uv_α :: "uint_vector ⇒ nat set" is α .
  lift_definition uv_lookup :: "nat ⇒ uint_vector ⇒ bool" is lookup .
  lift_definition uv_empty :: "uint_vector" is empty .
  lift_definition uv_single_bit :: "nat ⇒ uint_vector" is single_bit .
  lift_definition uv_set_bit :: "nat ⇒ uint_vector ⇒ uint_vector" is set_bit .
  lift_definition uv_reset_bit :: "nat ⇒ uint_vector ⇒ uint_vector" is reset_bit .
  lift_definition uv_union :: "uint_vector ⇒ uint_vector ⇒ uint_vector" is union .
  lift_definition uv_inter :: "uint_vector ⇒ uint_vector ⇒ uint_vector" is inter .
  lift_definition uv_diff :: "uint_vector ⇒ uint_vector ⇒ uint_vector" is diff .
  lift_definition uv_zeroes :: "uint_vector ⇒ bool" is zeroes .
  lift_definition uv_equal :: "uint_vector ⇒ uint_vector ⇒ bool" is equal .
  lift_definition uv_subseteq :: "uint_vector ⇒ uint_vector ⇒ bool" is subseteq .
  lift_definition uv_subset :: "uint_vector ⇒ uint_vector ⇒ bool" is subset .
  lift_definition uv_disjoint :: "uint_vector ⇒ uint_vector ⇒ bool" is disjoint .

  lemmas uv_memb_correct = memb_correct[where 'a=dflt_size, Transfer.transferred]
  lemmas uv_empty_correct = empty_correct[where 'a=dflt_size, Transfer.transferred]
  lemmas uv_single_bit_correct = single_bit_correct[where 'a=dflt_size, Transfer.transferred]
  lemmas uv_insert_correct = insert_correct[where 'a=dflt_size, Transfer.transferred]
  lemmas uv_delete_correct = delete_correct[where 'a=dflt_size, Transfer.transferred]
  lemmas uv_union_correct = union_correct[where 'a=dflt_size, Transfer.transferred]
  lemmas uv_inter_correct = inter_correct[where 'a=dflt_size, Transfer.transferred]
  lemmas uv_diff_correct = diff_correct[where 'a=dflt_size, Transfer.transferred]
  lemmas uv_isEmpty_correct = isEmpty_correct[where 'a=dflt_size, Transfer.transferred]
  lemmas uv_equal_correct = equal_correct[where 'a=dflt_size, Transfer.transferred]
  lemmas uv_subseteq_correct = subseteq_correct[where 'a=dflt_size, Transfer.transferred]
  lemmas uv_subset_correct = subset_correct[where 'a=dflt_size, Transfer.transferred]
  lemmas uv_disjoint_correct = disjoint_correct[where 'a=dflt_size, Transfer.transferred]



  lemmas [where 'a=dflt_size, Transfer.transferred, code] =
    lookup.simps
    empty_def
    single_bit.simps
    set_bit.simps
    reset_bit.simps
    union.simps
    inter.simps
    diff.simps
    zeroes.simps
    equal.simps
    subseteq.simps
    subset.simps
    disjoint.simps

  end

  hide_const (open) α lookup empty single_bit set_bit reset_bit union inter diff zeroes
    equal subseteq subset disjoint


  subsection ‹Autoref Setup›

  definition uv_set_rel_def_internal:
    "uv_set_rel Rk ≡
      if Rk=nat_rel then br uv_α (λ_. True) else {}"
  lemma uv_set_rel_def:
    "⟨nat_rel⟩uv_set_rel ≡ br uv_α (λ_. True)"
    unfolding uv_set_rel_def_internal relAPP_def by simp

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

  lemma uv_set_rel_sv[relator_props]: "single_valued (⟨nat_rel⟩uv_set_rel)"
    unfolding uv_set_rel_def by auto

  lemma uv_autoref[autoref_rules,param]:
    "(uv_lookup,(∈)) ∈ nat_rel → ⟨nat_rel⟩uv_set_rel → bool_rel"
    "(uv_empty,{}) ∈ ⟨nat_rel⟩uv_set_rel"
    "(uv_set_bit,insert) ∈ nat_rel → ⟨nat_rel⟩uv_set_rel → ⟨nat_rel⟩uv_set_rel"
    "(uv_reset_bit,op_set_delete) ∈ nat_rel → ⟨nat_rel⟩uv_set_rel → ⟨nat_rel⟩uv_set_rel"
    "(uv_union,(∪)) ∈ ⟨nat_rel⟩uv_set_rel → ⟨nat_rel⟩uv_set_rel → ⟨nat_rel⟩uv_set_rel"
    "(uv_inter,(∩)) ∈ ⟨nat_rel⟩uv_set_rel → ⟨nat_rel⟩uv_set_rel → ⟨nat_rel⟩uv_set_rel"
    "(uv_diff,(-)) ∈ ⟨nat_rel⟩uv_set_rel → ⟨nat_rel⟩uv_set_rel → ⟨nat_rel⟩uv_set_rel"
    "(uv_zeroes,op_set_isEmpty) ∈ ⟨nat_rel⟩uv_set_rel → bool_rel"
    "(uv_equal,(=)) ∈ ⟨nat_rel⟩uv_set_rel → ⟨nat_rel⟩uv_set_rel → bool_rel"
    "(uv_subseteq,(⊆)) ∈ ⟨nat_rel⟩uv_set_rel → ⟨nat_rel⟩uv_set_rel → bool_rel"
    "(uv_subset,(⊂)) ∈ ⟨nat_rel⟩uv_set_rel → ⟨nat_rel⟩uv_set_rel → bool_rel"
    "(uv_disjoint,op_set_disjoint) ∈ ⟨nat_rel⟩uv_set_rel → ⟨nat_rel⟩uv_set_rel → bool_rel"
    by (auto
      simp: uv_set_rel_def br_def
      simp: uv_memb_correct uv_empty_correct uv_insert_correct uv_delete_correct
      simp: uv_union_correct uv_inter_correct uv_diff_correct uv_isEmpty_correct
      simp: uv_equal_correct uv_subseteq_correct uv_subset_correct uv_disjoint_correct)

  export_code
    uv_lookup
    uv_empty
    uv_single_bit
    uv_set_bit
    uv_reset_bit
    uv_union
    uv_inter
    uv_diff
    uv_zeroes
    uv_equal
    uv_subseteq
    uv_subset
    uv_disjoint
  checking SML Scala Haskell? OCaml?

end