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<len_of TYPE('a) then test_bit w n else lookup (n-len_of TYPE('a)) ws)"

  lemma lookup_append[simp]: "lookup n (w1@w2 :: 'a::len word list) 
    <-> (
      if n < len_of TYPE('a) * length w1 then 
        lookup n w1 
      else lookup (n - len_of TYPE('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 < len_of TYPE('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<len_of TYPE('a)) then 
        [set_bit 0 n True] 
      else 0#single_bit (n-len_of TYPE('a)))"
    by pat_completeness auto
  termination
    apply (relation "measure id")
    apply simp
    apply simp
    by (metis diff_less le0 lens_not_0(2) sup.semilattice_strict_iff_order)

  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: bin_nth_sc_gen)
    done

find_consts name: set_bit

  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<len_of TYPE('a) then 
        bits_class.set_bit w i True # ws 
      else 
        w # set_bit (i - len_of TYPE('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: test_bit_set_gen word_size)
    done


  primrec reset_bit :: "nat => 'a::len word list => 'a::len word list" where
    "reset_bit i [] = []"
  | "reset_bit i (w#ws) = (
      if i<len_of TYPE('a) then 
        bits_class.set_bit w i False # ws 
      else 
        w # reset_bit (i - len_of TYPE('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: test_bit_set_gen word_size)
    done

  subsubsection {* Binary Operations *}

  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<len_of TYPE('a). test_bit (g w v) i <-> f (test_bit w i) (test_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 + len_of TYPE('a)" in spec)
        apply auto []
        apply (drule_tac x="i + len_of TYPE('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 del: subseteq_correct 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 
    

  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,op ∈) ∈ 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,op ∪) ∈ ⟨nat_rel⟩uv_set_rel -> ⟨nat_rel⟩uv_set_rel -> ⟨nat_rel⟩uv_set_rel"
    "(uv_inter,op ∩) ∈ ⟨nat_rel⟩uv_set_rel -> ⟨nat_rel⟩uv_set_rel -> ⟨nat_rel⟩uv_set_rel"
    "(uv_diff,op -) ∈ ⟨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,op =) ∈ ⟨nat_rel⟩uv_set_rel -> ⟨nat_rel⟩uv_set_rel -> bool_rel"
    "(uv_subseteq,op ⊆) ∈ ⟨nat_rel⟩uv_set_rel -> ⟨nat_rel⟩uv_set_rel -> bool_rel"
    "(uv_subset,op ⊂) ∈ ⟨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