Theory Separation_Logic_Imperative_HOL.Hash_Map

section "Hash-Maps"
theory Hash_Map
  imports Hash_Table
begin

subsection ‹Auxiliary Lemmas›
lemma map_of_ls_update: 
  "map_of (fst (ls_update k v l)) = (map_of l)(k ↦ v)"
  apply (induct l rule: ls_update.induct)
  by (auto simp add: ext Let_def)

lemma map_of_concat:
  "k ∈ dom (map_of(concat l)) 
  ⟹ ∃i. k ∈ dom (map_of(l!i)) ∧ i < length l"
  apply (induct l)
  apply simp
  apply auto
  apply (rule_tac x = 0 in exI)
  apply auto
  by (metis Suc_mono domI nth_Cons_Suc)

lemma map_of_concat':
  "k ∈ dom (map_of(l!i)) ∧ i < length l ⟹ k ∈ dom (map_of(concat l))"
  apply (induct l arbitrary: i)
  apply simp
  apply auto
  apply (case_tac i)
  apply auto
  done

lemma map_of_concat''':
  assumes "∃i. k ∈ dom (map_of(l!i)) ∧ i < length l"
  shows "k ∈ dom (map_of(concat l))"
proof -
  from assms obtain i where "k ∈ dom (map_of (l ! i)) ∧ i < length l" by blast
  from map_of_concat'[OF this] show ?thesis .
qed
 
lemma map_of_concat'':
  "(k ∈ dom (map_of(concat l))) 
  ⟷ (∃i. k ∈ dom (map_of(l!i)) ∧ i < length l)"
  apply rule
  using map_of_concat[of k l]
  apply simp
  using map_of_concat'[of k l]
  by blast

lemma abs_update_length: "length (abs_update k v l) = length l"
  by (simp add: abs_update_def)

lemma ls_update_map_of_eq:
  "map_of (fst (ls_update k v ls)) k = Some v"
  apply (induct ls rule: ls_update.induct)
  by (simp_all add: Let_def)

lemma ls_update_map_of_neq:
  "x ≠ k ⟹ map_of (fst (ls_update k v ls)) x = map_of ls x"
  apply (induct ls rule: ls_update.induct)
  by (auto simp add: Let_def)

subsection ‹Main Definitions and Lemmas›

definition is_hashmap' 
  :: "('k, 'v) map 
    ⇒ ('k × 'v) list list 
    ⇒ ('k::{heap,hashable}, 'v::heap) hashtable
    ⇒ assn" 
  where
  "is_hashmap' m l ht = is_hashtable l ht * ↑ (map_of (concat l) = m)"


definition is_hashmap 
  :: "('k, 'v) map ⇒ ('k::{heap,hashable}, 'v::heap) hashtable ⇒ assn" 
  where
  "is_hashmap m ht = (∃⇩Al. is_hashmap' m l ht)"

lemma is_hashmap'_prec:
  "∀s s'. h⊨(is_hashmap' m l ht * F1) ∧⇩A (is_hashmap' m' l' ht * F2)
  ⟶ l=l' ∧ m=m'"
  unfolding is_hashmap'_def
  apply (auto simp add: preciseD[OF is_hashtable_prec])
  apply (subgoal_tac "l = l'")
  by (auto simp add: preciseD[OF is_hashtable_prec])

lemma is_hashmap_prec: "precise is_hashmap"
  unfolding is_hashmap_def[abs_def]
  apply rule
  by (auto simp add: is_hashmap'_prec)

abbreviation "hm_new ≡ ht_new"
lemma hm_new_rule': 
  "<emp> 
  hm_new::('k::{heap,hashable}, 'v::heap) hashtable Heap 
  <is_hashmap' Map.empty (replicate (def_hashmap_size TYPE('k)) [])>"
  apply (rule cons_post_rule)
  using complete_ht_new
  apply simp
  apply (simp add: is_hashmap'_def)
  done 

lemma hm_new_rule: 
  "<emp> hm_new <is_hashmap Map.empty>"
  apply (rule cons_post_rule)
  using complete_ht_new
  apply simp
  apply (simp add: is_hashmap_def is_hashmap'_def)
  apply sep_auto
  done

lemma ht_hash_distinct:
  "ht_hash l 
  ⟹ ∀i j . i≠j ∧ i < length l ∧ j < length l 
    ⟶ set (l!i) ∩ set (l!j) = {}"
  apply (auto simp add: ht_hash_def)
  apply metis
  done

lemma ht_hash_in_dom_in_dom_bounded_hashcode_nat:
  assumes "ht_hash l"
  assumes "k ∈ dom (map_of(concat l))"
  shows "k ∈ dom (map_of(l!bounded_hashcode_nat (length l) k))"
proof -
  from map_of_concat[OF assms(2)] obtain i 
    where i: "k ∈ dom (map_of (l ! i)) ∧ i < length l" 
    by blast
  thm ht_hash_def
  hence "∃v. (k,v)∈set(l!i)" by (auto dest: map_of_SomeD)
  from this obtain v where v: "(k,v)∈set(l!i)" by blast
  from assms(1)[unfolded ht_hash_def] i v bounded_hashcode_nat_bounds 
  have "bounded_hashcode_nat (length l) k = i"
    by (metis fst_conv)
  with i show ?thesis by simp
qed

lemma ht_hash_in_dom_bounded_hashcode_nat_in_dom:
  assumes "ht_hash l"
  assumes "1 < length l"
  assumes "k ∈ dom (map_of(l!bounded_hashcode_nat (length l) k))"
  shows "k ∈ dom (map_of(concat l))"
  using map_of_concat'[of k l "bounded_hashcode_nat (length l) k"] 
    assms(2,3) bounded_hashcode_nat_bounds[of "length l" k]
  by simp


lemma ht_hash_in_dom_in_dom_bounded_hashcode_nat_eq:
  assumes "ht_hash l"
  assumes "1 < length l"
  shows "(k ∈ dom (map_of(concat l))) 
  = (k ∈ dom (map_of(l!bounded_hashcode_nat (length l) k)))"
  apply rule
  using ht_hash_in_dom_in_dom_bounded_hashcode_nat[OF assms(1)] 
    ht_hash_in_dom_bounded_hashcode_nat_in_dom[OF assms]
  by simp_all


lemma ht_hash_in_dom_i_bounded_hashcode_nat_i:
  assumes "ht_hash l"
  assumes "1 < length l"
  assumes "i < length l"
  assumes "k ∈ dom (map_of (l!i))" 
  shows "i = bounded_hashcode_nat (length l) k"
  using assms
  using bounded_hashcode_nat_bounds
  by (auto simp add: ht_hash_def ht_distinct_def dom_map_of_conv_image_fst)

lemma ht_hash_in_bounded_hashcode_nat_not_i_not_in_dom_i:
  assumes "ht_hash l"
  assumes "1 < length l"
  assumes "i < length l"
  assumes "i ≠ bounded_hashcode_nat (length l) k"
  shows "k ∉ dom (map_of (l!i))" 
  using assms
  using bounded_hashcode_nat_bounds
  by (auto simp add: ht_hash_def ht_distinct_def dom_map_of_conv_image_fst)

lemma ht_hash_ht_distinct_in_dom_unique_value:
  assumes "ht_hash l"
  assumes "ht_distinct l"
  assumes "1 < length l"
  assumes "k ∈ dom (map_of (concat l))"
  shows "∃!v. (k,v) ∈ set (concat l)"
proof -
  from assms(4) have ex: "∃v. (k,v) ∈ set (concat l)"  
    by (auto dest!: map_of_SomeD)
  have "v = w" if kv: "(k,v) ∈ set (concat l)" and kw: "(k,w) ∈ set (concat l)" for v w
  proof -
    from ht_hash_in_dom_in_dom_bounded_hashcode_nat[OF assms(1,4)] 
    have a: "k ∈ dom (map_of (l ! bounded_hashcode_nat (length l) k))" .
    have "k ∉ dom(map_of(l!i))"
      if "i < length l" and "i ≠ bounded_hashcode_nat (length l) k" for i
    proof -
      from ht_hash_in_bounded_hashcode_nat_not_i_not_in_dom_i[OF assms(1,3) that]
      show ?thesis .
    qed
    have v: "(k,v) ∈ set (l ! bounded_hashcode_nat (length l) k)"
    proof -
      from kv have "∃i. i < length l ∧ (k, v) ∈ set (l!i)" 
        by auto (metis in_set_conv_nth)
      from this obtain i where i: "i < length l ∧ (k, v) ∈ set (l!i)"
        by blast
      hence "k ∈ dom (map_of (l!i))"
        by (metis (no_types) prod.exhaust a assms(1) fst_conv ht_hash_def) 
      from i ht_hash_in_dom_i_bounded_hashcode_nat_i[OF assms(1,3) _ this] 
      have "i = bounded_hashcode_nat (length l) k" by simp
      with i show ?thesis by simp
    qed
    have w: "(k,w) ∈ set (l ! bounded_hashcode_nat (length l) k)"
    proof -
      from kw have "∃i. i < length l ∧ (k, w) ∈ set (l!i)" 
        by auto (metis in_set_conv_nth)
      from this obtain i where i: "i < length l ∧ (k, w) ∈ set (l!i)"
        by blast
      hence "k ∈ dom (map_of (l!i))"
        by (metis (no_types) prod.exhaust a assms(1) fst_conv ht_hash_def) 
      from i ht_hash_in_dom_i_bounded_hashcode_nat_i[OF assms(1,3) _ this] 
      have "i = bounded_hashcode_nat (length l) k" by simp
      with i show ?thesis by simp
    qed
    from assms(2,3) have 
      "distinct (map fst (l ! bounded_hashcode_nat (length l) k))"
      by (simp add: ht_distinct_def bounded_hashcode_nat_bounds)
    from Map.map_of_is_SomeI[OF this v] Map.map_of_is_SomeI[OF this w]
    show "v = w" by simp
  qed    
  with ex show ?thesis by blast
qed


lemma ht_hash_ht_distinct_map_of:
  assumes "ht_hash l"
  assumes "ht_distinct l"
  assumes "1 < length l"
  shows "map_of (concat l) k 
  = map_of(l!bounded_hashcode_nat (length l) k) k"
proof (cases "k ∈ dom (map_of(concat l))")
  case False
  hence a: "map_of (concat l) k = None" by auto
  from ht_hash_in_dom_in_dom_bounded_hashcode_nat_eq[OF assms(1,3)] False 
  have "k ∉ dom (map_of (l ! bounded_hashcode_nat (length l) k))" by simp
  hence "map_of(l!bounded_hashcode_nat (length l) k) k = None" by auto
  with a show ?thesis by simp
next
  case True
  from True obtain y where y: "map_of (concat l) k = Some y" by auto
  hence a: "(k,y) ∈ set (concat l)" by (metis map_of_SomeD)
  from ht_hash_in_dom_in_dom_bounded_hashcode_nat_eq[OF assms(1,3)] True 
  have "k ∈ dom (map_of (l ! bounded_hashcode_nat (length l) k))" by simp
  from this obtain z where 
    z: "map_of(l!bounded_hashcode_nat (length l) k) k = Some z" by auto
  hence "(k,z) ∈ set (l ! bounded_hashcode_nat (length l) k)"
    by (metis map_of_SomeD) 
  with bounded_hashcode_nat_bounds[OF assms(3), of k] 
  have b: "(k,z) ∈ set (concat l)" by auto
  from ht_hash_ht_distinct_in_dom_unique_value[OF assms True] a b 
  have "y = z" by auto
  with y z show ?thesis by simp
qed

lemma ls_lookup_map_of_pre:
  "distinct (map fst l) ⟹ ls_lookup k l = map_of l k"
  apply (induct l)
  apply simp
  apply (case_tac a)
  by simp

lemma ls_lookup_map_of:
  assumes "ht_hash l"
  assumes "ht_distinct l" 
  assumes "1 < length l" 
  shows "ls_lookup k (l ! bounded_hashcode_nat (length l) k) 
  = map_of (concat l) k"  
proof -
  from assms(2,3) 
  have "distinct (map fst (l ! bounded_hashcode_nat (length l) k))" 
    by (simp add: ht_distinct_def bounded_hashcode_nat_bounds)
  from ls_lookup_map_of_pre[OF this] 
  have "ls_lookup k (l ! bounded_hashcode_nat (length l) k) 
    = map_of (l ! bounded_hashcode_nat (length l) k) k" .
  also from ht_hash_ht_distinct_map_of[OF assms] 
  have "map_of (l ! bounded_hashcode_nat (length l) k) k 
    = map_of (concat l) k"
    by simp
  finally show ?thesis .
qed

abbreviation "hm_lookup ≡ ht_lookup"
lemma hm_lookup_rule':
  "<is_hashmap' m l ht> hm_lookup k ht 
    <λr. is_hashmap' m l ht * 
      ↑(r = m k)>"
  unfolding is_hashmap'_def
  apply sep_auto
  apply (rule cons_post_rule)
  using complete_ht_lookup[of l ht k]
  apply simp
  apply sep_auto
  by (simp add: ls_lookup_map_of is_hashtable_def)

lemma hm_lookup_rule:
  "<is_hashmap m ht> hm_lookup k ht 
    <λr. is_hashmap m ht * 
      ↑(r = m k)>"
  unfolding is_hashmap_def
  apply sep_auto
  apply (rule cons_post_rule[OF hm_lookup_rule'])
  by sep_auto

lemma abs_update_map_of'':
  assumes "ht_hash l"
  assumes "ht_distinct l"
  assumes "1 < length l"
  shows "map_of (concat (abs_update k v l)) k = Some v"
proof -
  from ht_hash_ht_distinct_map_of[
    OF ht_hash_update[OF assms(1)] 
       ht_distinct_update[OF assms(2)] 
       length_update[OF assms(3)], 
    of k v k]
  have "map_of (concat (abs_update k v l)) k 
    = map_of ((abs_update k v l) ! bounded_hashcode_nat (length l) k) k"
    by (simp add: abs_update_length)
  also have 
    "… = map_of (fst (ls_update k v 
                        (l ! bounded_hashcode_nat (length l) k))) k"
    by (simp add: abs_update_def bounded_hashcode_nat_bounds[OF assms(3)])
  also have "... = Some v" by (simp add: ls_update_map_of_eq)
  finally show ?thesis .
qed

lemma abs_update_map_of_hceq:
  assumes "ht_hash l"
  assumes "ht_distinct l"
  assumes "1 < length l"
  assumes "x ≠ k"
  assumes "bounded_hashcode_nat (length l) x 
    = bounded_hashcode_nat (length l) k"
  shows "map_of (concat (abs_update k v l)) x = map_of (concat l) x"
proof -
  from ht_hash_ht_distinct_map_of[
    OF ht_hash_update[OF assms(1)] 
       ht_distinct_update[OF assms(2)] 
       length_update[OF assms(3)], 
    of k v x]
  have "map_of (concat (abs_update k v l)) x 
    = map_of ((abs_update k v l) ! bounded_hashcode_nat (length l) x) x"
    by (simp add: abs_update_length)
  also from assms(5) have 
    "… = map_of (fst (ls_update k v 
                        (l ! bounded_hashcode_nat (length l) k))) x"
    by (simp add: abs_update_def bounded_hashcode_nat_bounds[OF assms(3)])
  also have 
    "… = map_of (l ! bounded_hashcode_nat (length l) x) x" 
    by (simp add: ls_update_map_of_neq[OF assms(4)] assms(5))
  also from ht_hash_ht_distinct_map_of[OF assms(1-3)] have 
    "… = map_of (concat l) x"
    by simp
  finally show ?thesis .
qed

lemma abs_update_map_of_hcneq:
  assumes "ht_hash l"
  assumes "ht_distinct l"
  assumes "1 < length l"
  assumes "x ≠ k"
  assumes "bounded_hashcode_nat (length l) x 
    ≠ bounded_hashcode_nat (length l) k"
  shows "map_of (concat (abs_update k v l)) x = map_of (concat l) x"
proof -
  from ht_hash_ht_distinct_map_of[
    OF ht_hash_update[OF assms(1)] 
        ht_distinct_update[OF assms(2)] 
        length_update[OF assms(3)], 
    of k v x]
  have "map_of (concat (abs_update k v l)) x 
    = map_of ((abs_update k v l) ! bounded_hashcode_nat (length l) x) x"
    by (simp add: abs_update_length)
  also from assms(5) 
  have "… = map_of (l ! bounded_hashcode_nat (length l) x) x"
    by (simp add: abs_update_def bounded_hashcode_nat_bounds[OF assms(3)])
  also from ht_hash_ht_distinct_map_of[OF assms(1-3)] 
  have "… = map_of (concat l) x"
    by simp
  finally show ?thesis .
qed  
 

lemma abs_update_map_of''':
  assumes "ht_hash l"
  assumes "ht_distinct l"
  assumes "1 < length l"
  assumes "x ≠ k"
  shows "map_of (concat (abs_update k v l)) x = map_of (concat l) x"
  apply (cases 
    "bounded_hashcode_nat (length l) x = bounded_hashcode_nat (length l) k")
  by (auto simp add: abs_update_map_of_hceq[OF assms] 
    abs_update_map_of_hcneq[OF assms])

lemma abs_update_map_of':  
  assumes "ht_hash l"
  assumes "ht_distinct l"
  assumes "1 < length l"
  shows "map_of (concat (abs_update k v l)) x 
    = ((map_of (concat l))(k ↦ v)) x"
  apply (cases "x = k")
  apply (simp add: abs_update_map_of''[OF assms])
  by (simp add: abs_update_map_of'''[OF assms])

lemma abs_update_map_of:  
  assumes "ht_hash l"
  assumes "ht_distinct l"
  assumes "1 < length l"
  shows "map_of (concat (abs_update k v l)) 
    = (map_of (concat l))(k ↦ v) "
  apply (rule ext)
  by (simp add: abs_update_map_of'[OF assms])


lemma ls_insls_map_of:
  assumes "ht_hash ld"
  assumes "ht_distinct ld"
  assumes "1 < length ld"
  assumes "distinct (map fst xs)"
  shows "map_of (concat (ls_insls xs ld)) = map_of (concat ld) ++ map_of xs"
  using assms
  apply (induct xs arbitrary: ld)
  apply simp
  apply (case_tac a)
  apply (simp only: ls_insls.simps)
  subgoal premises prems
  proof -
    from prems(5) prems(1)[OF ht_hash_update[OF prems(2)] 
      ht_distinct_update[OF prems(3)] 
      length_update[OF prems(4)]] 
      abs_update_map_of[OF prems(2-4)] 
    show ?thesis
      apply simp
      apply (rule map_add_upd_left)
      apply (metis dom_map_of_conv_image_fst)
      done
  qed
  done

lemma ls_insls_map_of':
  assumes "ht_hash ls"
  assumes "ht_distinct ls"
  assumes "ht_hash ld"
  assumes "ht_distinct ld"
  assumes "1 < length ld"
  assumes "n < length ls"
  shows "map_of (concat (ls_insls (ls ! n) ld)) 
      ++ map_of (concat (take n ls))
    = map_of (concat ld) ++ map_of (concat (take (Suc n) ls))"
proof -
  from assms(2,6) have "distinct (map fst (ls ! n))" 
    by (simp add: ht_distinct_def)
  from ls_insls_map_of[OF assms(3-5) this] assms(6) show ?thesis
    by (simp add: List.take_Suc_conv_app_nth)
qed

lemma ls_copy_map_of:
  assumes "ht_hash ls"
  assumes "ht_distinct ls"
  assumes "ht_hash ld"
  assumes "ht_distinct ld"
  assumes "1 < length ld"
  assumes "n ≤ length ls"
  shows "map_of (concat (ls_copy n ls ld)) = map_of (concat ld) ++ map_of (concat (take n ls))"
  using assms
  apply (induct n arbitrary: ld)
  apply simp
  subgoal premises prems for n ld
  proof -
    note a = ht_hash_ls_insls[OF prems(4), of "ls ! n"]
    note b = ht_distinct_ls_insls[OF prems(5), of "ls ! n"]
    note c = length_ls_insls[OF prems(6), of "ls ! n"]
    from prems have "n < length ls" by simp
    with 
      ls_insls_map_of'[OF prems(2-6) this] 
      prems(1)[OF assms(1,2) a b c]
    show ?thesis by simp
  qed
  done


lemma ls_rehash_map_of:
  assumes "ht_hash l"
  assumes "ht_distinct l"
  assumes "1 < length l"
  shows "map_of (concat (ls_rehash l)) = map_of (concat l)"
  using assms(3) ls_copy_map_of[OF assms(1,2) 
    ht_hash_replicate ht_distinct_replicate]
  by (simp add: ls_rehash_def)


lemma abs_update_rehash_map_of:
  assumes "ht_hash l"
  assumes "ht_distinct l"
  assumes "1 < length l"
  shows "map_of (concat (abs_update k v (ls_rehash l))) 
  = (map_of (concat l))(k ↦ v)"
proof -
  note a = ht_hash_ls_rehash[of l]
  note b = ht_distinct_ls_rehash[of l]
  note c = length_ls_rehash[OF assms(3)]
  from abs_update_map_of[OF a b c] ls_rehash_map_of[OF assms] 
  show ?thesis by simp
qed

abbreviation "hm_update ≡ ht_update"
lemma hm_update_rule':
  "<is_hashmap' m l ht> 
    hm_update k v ht 
  <λr. is_hashmap (m(k ↦ v)) r * true>"
proof (cases "length l * load_factor ≤ the_size ht * 100")
  case True
  show ?thesis
    unfolding is_hashmap'_def
    apply sep_auto    
    apply (rule cons_post_rule[OF complete_ht_update_rehash[OF True]])
    unfolding is_hashmap_def is_hashmap'_def
    apply sep_auto
    apply (simp add: abs_update_rehash_map_of is_hashtable_def)
    done
next
  case False
  show ?thesis    
    unfolding is_hashmap'_def is_hashtable_def
    apply sep_auto
    apply (rule cons_post_rule)
    using complete_ht_update_normal[OF False, simplified is_hashtable_def, 
      simplified, of k v]
    apply auto
    unfolding is_hashmap_def is_hashmap'_def
    apply sep_auto
    by (simp add: abs_update_map_of is_hashtable_def)
qed

lemma hm_update_rule:
  "<is_hashmap m ht> 
    hm_update k v ht 
  <λr. is_hashmap (m(k ↦ v)) r * true>"
  unfolding is_hashmap_def[of m]
  by (sep_auto heap add: hm_update_rule')

lemma ls_delete_map_of:
  assumes "distinct (map fst l)"
  shows "map_of (fst (ls_delete k l)) x = ((map_of l) |` (- {k})) x"
  using assms
  apply (induct l rule: ls_delete.induct)
  apply simp
  apply (auto simp add: map_of_eq_None_iff Let_def)
  by (metis ComplD ComplI Compl_insert option.set(2) 
    insertE insertI2 map_upd_eq_restrict restrict_map_def)

lemma update_ls_delete_map_of: 
  assumes "ht_hash l"
  assumes "ht_distinct l"
  assumes "ht_hash (l[bounded_hashcode_nat (length l) k 
  := fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])"
  assumes "ht_distinct (l[bounded_hashcode_nat (length l) k 
  := fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])"
  assumes "1 < length l"
  shows "map_of (concat (l[bounded_hashcode_nat (length l) k 
    := fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])) x
  = ((map_of (concat l)) |` (- {k})) x"
proof -
  from assms(2) bounded_hashcode_nat_bounds[OF assms(5)] have 
    distinct: "distinct (map fst (l ! bounded_hashcode_nat (length l) k))"
    by (auto simp add: ht_distinct_def)
  note id1 = ht_hash_ht_distinct_map_of[OF assms(3,4), simplified, 
    OF assms(5)[simplified], of x]
  note id2 = ht_hash_ht_distinct_map_of[OF assms(1,2,5), of x]
  show ?thesis
  proof (cases 
      "bounded_hashcode_nat (length l) x = bounded_hashcode_nat (length l) k")
    case True
    with id1
    have "map_of (concat (l[bounded_hashcode_nat (length l) k 
      := fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])) x 
      =
      map_of (l[bounded_hashcode_nat (length l) k 
        := fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))] 
      ! bounded_hashcode_nat (length l) k) x"
      by simp
    also have 
      "… = map_of (fst (ls_delete k 
                          (l ! bounded_hashcode_nat (length l) k))) x"
      by (simp add: bounded_hashcode_nat_bounds[OF assms(5)])
    also from ls_delete_map_of[OF distinct] have 
      "… = (map_of (l ! bounded_hashcode_nat (length l) k) |` (- {k})) x"
      by simp
    finally show ?thesis
      by (cases "x = k") (simp_all add: id2 True)
  next
    case False
    with bounded_hashcode_nat_bounds[OF assms(5)] id1 id2[symmetric] 
    show ?thesis
      by (cases "x = k") simp_all
  qed
qed

abbreviation "hm_delete ≡ ht_delete"
lemma hm_delete_rule': 
  "<is_hashmap' m l ht> hm_delete k ht <is_hashmap (m |` (-{k}))>"
  apply (simp only: is_hashmap'_def[of m] is_hashtable_def)
  apply sep_auto
  apply (rule cons_post_rule)
  using complete_ht_delete[simplified is_hashtable_def]
  apply sep_auto
  apply (simp add: is_hashmap_def is_hashmap'_def)
  apply (sep_auto)
  apply (simp add: is_hashtable_def)
  apply (sep_auto)
  by (auto simp add: update_ls_delete_map_of)

lemma hm_delete_rule: 
  "<is_hashmap m ht> hm_delete k ht <is_hashmap (m |` (-{k}))>"
  unfolding is_hashmap_def[of m]
  by (sep_auto heap add: hm_delete_rule')

definition hm_isEmpty :: "('k, 'v) hashtable ⇒ bool Heap" where
  "hm_isEmpty ht ≡ return (the_size ht = 0)"

lemma hm_isEmpty_rule': 
  "<is_hashmap' m l ht> 
  hm_isEmpty ht 
  <λr. is_hashmap' m l ht * ↑(r ⟷ m=Map.empty)>"
  unfolding hm_isEmpty_def
  unfolding is_hashmap_def is_hashmap'_def is_hashtable_def ht_size_def
  apply (cases ht, simp)
  apply sep_auto
  done

lemma hm_isEmpty_rule: 
  "<is_hashmap m ht> hm_isEmpty ht <λr. is_hashmap m ht * ↑(r ⟷ m=Map.empty)>"
  unfolding is_hashmap_def
  apply (sep_auto heap: hm_isEmpty_rule')
  done

definition hm_size :: "('k, 'v) hashtable ⇒ nat Heap" where
  "hm_size ht ≡ return (the_size ht)"

lemma length_card_dom_map_of:
  assumes "distinct (map fst l)"
  shows "length l = card (dom (map_of l))"
  using assms
  apply (induct l)
  apply simp
  apply simp
  apply (case_tac a)
  apply (auto intro!: fst_conv map_of_SomeD)
  apply (subgoal_tac "aa ∉ dom (map_of l)")
  apply simp
  by (metis dom_map_of_conv_image_fst)

lemma ht_hash_dom_map_of_disj:
  assumes "ht_hash l"
  assumes "i < length l"
  assumes "j < length l"
  assumes "i ≠ j"
  shows "dom (map_of (l!i)) ∩ dom (map_of(l!j)) = {}"
  using assms
  unfolding ht_hash_def
  apply auto
  by (metis fst_conv map_of_SomeD)


lemma ht_hash_dom_map_of_disj_drop:
  assumes "ht_hash l"
  assumes "i < length l"
  shows "dom (map_of (l!i)) ∩ dom (map_of (concat (drop (Suc i) l))) = {}"
  apply auto
  subgoal premises prems for x y z
  proof -
    from prems(2) have "x ∈ dom (map_of (concat (drop (Suc i) l)))"
      by auto
    hence "∃j. j < length (drop (Suc i) l) 
      ∧ x ∈ dom (map_of ((drop (Suc i) l)!j))"
      by (metis Hash_Map.map_of_concat 
        ‹x ∈ dom (map_of (concat (drop (Suc i) l)))› length_drop)
    from this obtain j where 
      j: "j < length (drop (Suc i) l) 
        ∧ x ∈ dom (map_of ((drop (Suc i) l)!j))" 
      by blast
    hence length: "(Suc i + j) < length l" by auto
    from j have neq: "i ≠ (Suc i + j)" by simp
    from j have in_dom: "x ∈ dom (map_of (l!(Suc i + j)))" by auto
    from prems(1) have in_dom2: "x ∈ dom (map_of (l ! i))" by auto
    from ht_hash_dom_map_of_disj[OF assms length neq] in_dom in_dom2
    show ?thesis by auto
  qed
  done

lemma sum_list_length_card_dom_map_of_concat:
  assumes "ht_hash l"
  assumes "ht_distinct l"
  shows "sum_list (map length l) = card (dom (map_of (concat l)))"
  using assms
proof -
  from ht_hash_dom_map_of_disj_drop[OF assms(1)]
  have "∀i. i < length l 
    ⟶ dom (map_of (l ! i)) ∩ dom (map_of (concat (drop (Suc i) l)))
        = {}" 
    by auto
  with assms(2) show ?thesis
  proof (induct l)
    case Nil
    thus ?case by simp
  next
    case (Cons l ls)
    from Cons(2) have a: "ht_distinct ls" by (auto simp add: ht_distinct_def)
    from Cons(3) have b: "∀i < length ls. dom (map_of (ls ! i)) 
      ∩ dom (map_of (concat (drop (Suc i) ls))) = {}" 
      apply simp
      apply (rule allI)
      apply (rule_tac x="Suc i" and P="(λi. i<Suc (length ls) ⟶
             dom (map_of ((l # ls) ! i)) ∩ dom (map_of (concat (drop i ls))) =
             {})" in allE)
      by simp_all
    from Cons(2) have "distinct (map fst l)" by (auto simp add: ht_distinct_def)
    note l = length_card_dom_map_of[OF this]
    from Cons(3) have c: "dom (map_of l) ∩ dom (map_of (concat ls)) = {}"
      apply (rule_tac x="0" and P="(λi. i<Suc (length ls) ⟶
             dom (map_of ((l # ls) ! i)) 
               ∩ dom (map_of (concat (drop i ls))) 
             = {})" in allE)
      by simp_all
    from Cons(1)[OF a b] l c show ?case by (simp add: card_Un_disjoint)
  qed
qed


lemma hm_size_rule': 
  "<is_hashmap' m l ht> 
  hm_size ht 
  <λr. is_hashmap' m l ht * ↑(r = card (dom m))>"
  unfolding hm_size_def is_hashmap_def is_hashmap'_def is_hashtable_def
  apply sep_auto
  apply (cases ht)
  apply (simp add: ht_size_def)
  apply sep_auto
  by (simp add: sum_list_length_card_dom_map_of_concat)

lemma hm_size_rule: 
  "<is_hashmap m ht> 
    hm_size ht 
  <λr. is_hashmap m ht * ↑(r = card (dom m))>"
  unfolding is_hashmap_def
  by (sep_auto heap: hm_size_rule')

subsection ‹Iterators›

subsubsection ‹Definitions›
type_synonym ('k,'v) hm_it = "(nat × ('k×'v) list × ('k,'v) hashtable)"

fun hm_it_adjust 
  :: "nat ⇒ ('k::{heap,hashable},'v::heap) hashtable ⇒ nat Heap"
  where
  "hm_it_adjust 0 ht = return 0"
| "hm_it_adjust n ht = do {
    l ← Array.nth (the_array ht) n;
    case l of 
      [] ⇒ hm_it_adjust (n - 1) ht
    | _ ⇒  return n
  }"

definition hm_it_init 
  :: "('k::{heap,hashable},'v::heap) hashtable ⇒ ('k,'v) hm_it Heap"
  where 
  "hm_it_init ht ≡ do {
  n←Array.len (the_array ht);
  if n = 0 then return (0,[],ht)
  else do {
    i←hm_it_adjust (n - 1) ht;
    l←Array.nth (the_array ht) i;
    return (i,l,ht)
  }
}"

definition hm_it_has_next 
  :: "('k::{heap,hashable},'v::heap) hm_it ⇒ bool Heap"
  where "hm_it_has_next it 
  ≡ return (case it of (0,[],_) ⇒ False | _ ⇒ True)"

definition hm_it_next :: 
  "('k::{heap,hashable},'v::heap) hm_it 
    ⇒ (('k×'v)×('k,'v) hm_it) Heap"
  where "hm_it_next it ≡ case it of 
    (i,a#b#l,ht) ⇒ return (a,(i,b#l,ht))
  | (0,[a],ht) ⇒ return (a,(0,[],ht))
  | (Suc i,[a],ht) ⇒ do {
    i ← hm_it_adjust i ht;
    l ← Array.nth (the_array ht) i;
    return (a,(i,rev l,ht))
  }
  "

definition "hm_is_it' l ht l' it ≡  
  is_hashtable l ht * 
  ↑(let (i,r,ht')=it in 
       ht = ht' 
     ∧ l' = (concat (take i l) @ rev r)
     ∧ distinct (map fst (l'))
     ∧ i ≤ length l ∧ (r=[] ⟶ i=0)
   )"

definition "hm_is_it m ht m' it ≡ ∃⇩Al l'. 
  hm_is_it' l ht l' it 
  * ↑(map_of (concat l) = m ∧ map_of l' = m') 
  "

subsubsection ‹Auxiliary Lemmas›
lemma concat_take_Suc_empty: "⟦ n < length l; l!n=[] ⟧ 
  ⟹ concat (take (Suc n) l) = concat (take n l)"
  apply (induct n arbitrary: l)
  apply (case_tac l)
  apply auto [2]
  apply (case_tac l)
  apply auto [2]
  done

lemma nth_concat_splitE:
  assumes "i<length (concat ls)"
  obtains j k where
  "j < length ls" 
  and "k < length (ls!j)" 
  and "concat ls ! i = ls!j!k"
  and "i = length (concat (take j ls)) + k"
  using assms
proof (induct ls arbitrary: i thesis)
  case Nil thus ?case by auto
next
  case (Cons l ls)
  show ?case proof (cases)
    assume L: "i < length l"
    hence "concat (l#ls) ! i = (l#ls)!0!i" by (auto simp: nth_append)
    thus ?thesis 
      apply (rule_tac Cons.prems(1)[of 0 i])
      apply (simp_all add: L)
      done
  next
    assume L: "¬(i < length l)"
    hence 1: "concat (l#ls)!i = concat ls ! (i - length l)"
      by (auto simp: nth_append)
    obtain j k where
      "j < length ls" and "k < length (ls!j)" 
      and "concat ls ! (i - length l) = ls!j!k"
      and "i - length l = length (concat (take j ls)) + k"
      apply (rule Cons.hyps[of "i - length l"])
      using Cons.prems L
      by auto
    thus ?case using L 
      apply (rule_tac Cons.prems(1)[of "Suc j" k])
      apply (auto simp: nth_append)
      done
  qed
qed

lemma is_hashmap'_distinct: 
  "is_hashtable l ht 
    ⟹⇩A is_hashtable l ht * ↑(distinct (map fst (concat l)))"
  apply (simp add: distinct_conv_nth)
proof (intro allI impI, elim exE)
  fix i j a b
  assume 1: "i < length (concat l)"
  assume 2: "j < length (concat l)"
  assume 3: "i≠j"
  
  assume HM: "(a,b) ⊨ is_hashtable l ht"

  from 1 obtain ji ki where
    IFMT: "i = length (concat (take ji l)) + ki" 
    and JI_LEN: "ji < length l"
    and KI_LEN: "ki < length (l!ji)"
    and [simp]: "concat l ! i = l!ji!ki"
    by (blast elim: nth_concat_splitE)

  from 2 obtain jj kj where
    JFMT: "j = length (concat (take jj l)) + kj" 
    and JJ_LEN: "jj < length l"
    and KJ_LEN: "kj < length (l!jj)"
    and [simp]: "concat l ! j = l!jj!kj"
    by (blast elim: nth_concat_splitE)

  show "fst (concat l ! i) ≠ fst (concat l ! j)"
  proof cases
    assume [simp]: "ji=jj"
    with IFMT JFMT ‹i≠j› have "ki≠kj" by auto
    moreover from HM JJ_LEN have "distinct (map fst (l!jj))"
      unfolding is_hashmap'_def is_hashtable_def ht_distinct_def
      by auto
    ultimately show ?thesis using KI_LEN KJ_LEN
      by (simp add: distinct_conv_nth)
  next
    assume NE: "ji≠jj"
    from HM have 
      "∀x∈set (l!ji). bounded_hashcode_nat (length l) (fst x) = ji"
      "∀x∈set (l!jj). bounded_hashcode_nat (length l) (fst x) = jj"
      unfolding is_hashmap'_def is_hashtable_def ht_hash_def
      using JI_LEN JJ_LEN
      by auto
    with KI_LEN KJ_LEN NE show ?thesis 
      apply (auto) by (metis nth_mem)
  qed
qed

lemma take_set: "set (take n l) = { l!i | i. i<n ∧ i<length l }"
  apply (auto simp add: set_conv_nth)
  apply (rule_tac x=i in exI)
  apply auto
  done

lemma skip_empty_aux:
  assumes A: "concat (take (Suc n) l) = concat (take (Suc x) l)"
  assumes L[simp]: "Suc n ≤ length l" "x ≤ n"
  shows "∀i. x<i ∧ i≤n ⟶ l!i=[]"
proof -
  have "take (Suc n) l = take (Suc x + (n - x)) l"
    by simp
  also have "… = take (Suc x) l @ take (n - x) (drop (Suc x) l)"
    by (simp only: take_add)
  finally   have 
    "concat (take (Suc x) l) = 
      concat (take (Suc x) l) @ concat (take (n - x) (drop (Suc x) l))"
    using A by simp
  hence 1: "∀l∈set (take (n - x) (drop (Suc x) l)). l=[]" by simp
  show ?thesis
  proof safe
    fix i
    assume "x<i" and "i≤n"
    hence "l!i ∈ set (take (n - x) (drop (Suc x) l))"
      using L[simp del]
      apply (auto simp: take_set)
      apply (rule_tac x="i - Suc x" in exI)
      apply auto
      done
    with 1 show "l!i=[]" by blast
  qed
qed

lemma take_Suc0: 
  "l≠[] ⟹ take (Suc 0) l = [l!0]" 
  "0 < length l ⟹ take (Suc 0) l = [l!0]" 
  "Suc n ≤ length l ⟹ take (Suc 0) l = [l!0]" 
  by (cases l, auto)+


lemma concat_take_Suc_app_nth:
  assumes "x < length l"
  shows "concat (take (Suc x) l) = concat (take x l) @ l ! x"
  using assms
  by (auto simp: take_Suc_conv_app_nth)

lemma hm_hashcode_eq:
  assumes "j < length (l!i)"
  assumes "i < length l"
  assumes "h ⊨ is_hashtable l ht"
  shows "bounded_hashcode_nat (length l) (fst (l!i!j)) = i"
  using assms
  unfolding is_hashtable_def ht_hash_def
  apply (cases "l!i!j")
  apply (force simp: set_conv_nth)
  done

lemma distinct_imp_distinct_take: 
  "distinct (map fst (concat l))
  ⟹ distinct (map fst (concat (take x l)))"
  apply (subst (asm) append_take_drop_id[of x l,symmetric])
  apply (simp del: append_take_drop_id)
  done

lemma hm_it_adjust_rule:
  "i<length l ⟹ <is_hashtable l ht> 
    hm_it_adjust i ht 
   <λj. is_hashtable l ht * ↑(
      j≤i ∧ 
      (concat (take (Suc i) l) = concat (take (Suc j) l)) ∧
      (j=0 ∨ l!j ≠ [])
    )    
   >"
proof (induct i)
  case 0 thus ?case by sep_auto
next
  case (Suc n)
  show ?case using Suc.prems
    by (sep_auto 
      heap add: Suc.hyps
      simp: concat_take_Suc_empty
      split: list.split)
qed  

lemma hm_it_next_rule': "l'≠[] ⟹ 
    <hm_is_it' l ht l' it> 
      hm_it_next it 
    <λ((k,v),it'). 
      hm_is_it' l ht (butlast l') it' 
    * ↑(last l' = (k,v) ∧ distinct (map fst l') )>"
  unfolding hm_it_next_def hm_is_it'_def is_hashmap'_def
  using [[hypsubst_thin = true]]
  apply (sep_auto (plain)
    split: nat.split list.split 
    heap: hm_it_adjust_rule
    simp: take_Suc0)
  apply (simp split: prod.split nat.split list.split)
  apply (intro allI impI conjI)
  apply auto []
  apply auto []
  apply sep_auto []

  apply (sep_auto (plain)
    heap: hm_it_adjust_rule)
  apply auto []
  apply sep_auto

  apply (cases l, auto) []
  apply (metis SUP_upper fst_image_mp image_mono set_concat)

  apply (drule skip_empty_aux, simp_all) []
  defer
  apply (auto simp: concat_take_Suc_app_nth) []

  apply auto []
  apply sep_auto

  apply (auto simp: butlast_append) []
  apply (auto simp: butlast_append) []

  apply sep_auto
  apply (auto simp: butlast_append) []
  apply (auto simp: butlast_append) []
  by (metis Ex_list_of_length Suc_leD concat_take_Suc_app_nth le_neq_implies_less le_trans nat.inject not_less_eq_eq)

subsubsection ‹Main Lemmas›

lemma hm_it_next_rule: "m'≠Map.empty ⟹ 
    <hm_is_it m ht m' it> 
      hm_it_next it 
    <λ((k,v),it'). hm_is_it m ht (m' |` (-{k})) it' * ↑(m' k = Some v)>"
proof -
  { fix ys a
    have aux3: " 
      ⟦distinct (map fst ys); a ∉ fst ` set ys⟧ ⟹ map_of ys a = None"
      by (induct ys) auto
  } note aux3 = this

  assume "m'≠Map.empty"
  thus ?thesis
    unfolding hm_is_it_def 
    apply (sep_auto heap: hm_it_next_rule')
    apply (case_tac l' rule: rev_cases, 
      auto simp: restrict_map_def aux3 intro!: ext) []
    apply (case_tac l' rule: rev_cases, auto)
    done
qed

lemma hm_it_init_rule:
  fixes ht :: "('k::{heap,hashable},'v::heap) hashtable"
  shows "<is_hashmap m ht> hm_it_init ht <hm_is_it m ht m>⇩t"
  unfolding hm_it_init_def is_hashmap_def is_hashmap'_def 
    hm_is_it_def hm_is_it'_def
  apply (sep_auto simp del: map_of_append heap add: hm_it_adjust_rule)
  apply (case_tac l, auto) []
  apply (sep_auto simp del: concat_eq_Nil_conv map_of_append)
  apply (auto simp: distinct_imp_distinct_take 
    dest: ent_fwd[OF _ is_hashmap'_distinct]) []

  apply (drule sym)
  apply (auto 
    simp: is_hashtable_def ht_distinct_def rev_map[symmetric]) []

  apply (auto simp: set_conv_nth) []
  apply (hypsubst_thin)
  apply (drule_tac j=ia in hm_hashcode_eq, simp_all) []
  apply (drule_tac j=ib in hm_hashcode_eq, simp_all) []

  apply (auto 
    simp: is_hashmap'_def is_hashtable_def ht_distinct_def) []

  apply (clarsimp)
  apply (drule ent_fwd[OF _ is_hashmap'_distinct])
  apply clarsimp
  apply (subst concat_take_Suc_app_nth)
  apply (case_tac l,auto) []
  apply (simp)
  apply (hypsubst_thin)
  apply (subst (asm) (2) concat_take_Suc_app_nth)
  apply (case_tac l,auto) []
  apply (subst map_of_rev_distinct)
  apply auto
  done

lemma hm_it_has_next_rule:
  "<hm_is_it m ht m' it> hm_it_has_next it 
    <λr. hm_is_it m ht m' it * ↑(r⟷m'≠Map.empty)>"
  unfolding is_hashmap'_def hm_is_it_def hm_is_it'_def hm_it_has_next_def
  by (sep_auto split: nat.split list.split)

lemma hm_it_finish: "hm_is_it m p m' it ⟹⇩A is_hashmap m p"
  unfolding hm_is_it_def hm_is_it'_def is_hashmap_def is_hashmap'_def
  by sep_auto

end