Theory AList-Utils

theory "AList-Utils"
imports Main "~~/src/HOL/Library/AList"
begin
declare implies_True_equals [simp] False_implies_equals[simp]
text {* We want to have @{text delete} and @{text update} back in the namespace. *}

abbreviation delete where "delete ≡ AList.delete"
abbreviation update where "update ≡ AList.update"
abbreviation restrictA where "restrictA ≡ AList.restrict"
abbreviation clearjunk where "clearjunk ≡ AList.clearjunk"

lemmas restrict_eq = AList.restrict_eq
  and delete_eq = AList.delete_eq

lemma restrictA_append: "restrictA S (a@b) = restrictA S a @ restrictA S b"
  unfolding restrict_eq by (rule filter_append)

lemma length_restrictA_le: "length (restrictA S a) ≤ length a"
  by (metis length_filter_le restrict_eq)

subsubsection {* The domain of an associative list *}

definition domA
  where "domA h = fst ` set h"

lemma domA_append[simp]:"domA (a @ b) = domA a ∪ domA b"
  and [simp]:"domA ((v,e) # h) = insert v (domA h)"
  and [simp]:"domA (p # h) = insert (fst p) (domA h)"
  and [simp]:"domA [] = {}"
  by (auto simp add: domA_def)

lemma domA_from_set:
  "(x, e) ∈ set h ⟹ x ∈ domA h"
by (induct h, auto)

lemma finite_domA[simp]:
  "finite (domA Γ)"
  by (auto simp add: domA_def)

lemma domA_delete[simp]:
  "domA (delete x Γ) = domA Γ - {x}"
  by (induct Γ) auto

lemma domA_restrictA[simp]:
  "domA (restrictA S Γ) = domA Γ ∩ S"
  by (induct Γ) auto

lemma delete_not_domA[simp]:
  "x ∉ domA Γ ⟹  delete x Γ = Γ"
  by (induct Γ) auto

lemma deleted_not_domA: "x ∉ domA (delete x Γ)"
  by (induct Γ) auto

lemma dom_map_of_conv_domA:
  "dom (map_of Γ) = domA Γ"
  by (induct Γ) (auto simp add: dom_if)

lemma domA_map_of_Some_the:
  "x ∈ domA Γ ⟹ map_of Γ x = Some (the (map_of Γ x))"
  by (induct Γ) (auto simp add: dom_if)

lemma domA_clearjunk[simp]: "domA (clearjunk Γ) = domA Γ"
  unfolding domA_def using dom_clearjunk.

lemma the_map_option_domA[simp]: "x ∈ domA Γ ⟹ the (map_option f (map_of Γ x)) = f (the (map_of Γ x))"
  by (induction Γ) auto

lemma map_of_domAD: "map_of Γ x = Some e ⟹ x ∈ domA Γ"
  using dom_map_of_conv_domA by fastforce

lemma restrictA_noop: "domA Γ ⊆ S ⟹ restrictA S Γ = Γ"
  unfolding restrict_eq by (induction Γ) auto

lemma restrictA_cong:
  "(⋀x. x ∈ domA m1 ⟹ x ∈ V ⟷ x ∈ V') ⟹ m1 = m2 ⟹ restrictA V m1 = restrictA V' m2"
  unfolding restrict_eq by (induction m1 arbitrary: m2) auto

subsubsection {* Other lemmas about associative lists *}

lemma delete_set_none: "(map_of l)(x := None) = map_of (delete x l)"
proof (induct l)
  case Nil thus ?case by simp
  case (Cons l ls)
  from this[symmetric]
  show ?case
  by (cases "fst l = x") auto
qed

lemma list_size_delete[simp]: "size_list size (delete x l) < Suc (size_list size l)"
  by (induct l) auto

lemma delete_append[simp]: "delete x (l1 @ l2) = delete x l1 @ delete x l2"
  unfolding AList.delete_eq by simp

lemma map_of_delete_insert:
  assumes "map_of Γ x = Some e"
  shows "map_of ((x,e) # delete x Γ) = map_of Γ"
  using assms by (induct Γ) (auto split:prod.split)

lemma map_of_delete_iff[simp]: "map_of (delete x Γ) xa = Some e ⟷ (map_of Γ xa = Some e) ∧ xa ≠ x"
  by (metis delete_conv fun_upd_same map_of_delete option.distinct(1))

lemma map_add_domA[simp]: 
  "x ∈ domA Γ ⟹ (map_of Δ ++ map_of Γ) x = map_of Γ x"
  "x ∉ domA Γ ⟹ (map_of Δ ++ map_of Γ) x = map_of Δ x"
    apply (metis dom_map_of_conv_domA map_add_dom_app_simps(1))
    apply (metis dom_map_of_conv_domA map_add_dom_app_simps(3))
    done


lemma map_of_empty_iff1[simp]: "map_of Γ = empty ⟷ Γ = []"
  by (cases "Γ") auto

lemma map_of_empty_iff2[simp]: "empty = map_of Γ ⟷ Γ = []"
  apply (subst eq_commute)
  by (rule map_of_empty_iff1)

lemma set_delete_subset: "set (delete k al) ⊆ set al"
  by (auto simp add: delete_eq)

lemma dom_delete_subset: "snd ` set (delete k al) ⊆ snd ` set al"
  by (auto simp add: delete_eq)

(*
lemma ran_map_cong[fundef_cong]:
  "⟦ list_all2 (λ x y. fst x = fst y ∧ f1 (fst x) (snd x) = f2 (fst y) (snd y)) m1 m2 ⟧
      ⟹ map_ran f1 m1 = map_ran f2 m2"    
  by (induction rule: list_all2_induct) auto
*)
lemma map_ran_cong[fundef_cong]:
  "⟦ ⋀ x . x ∈ set m1 ⟹ f1 (fst x) (snd x) = f2 (fst x) (snd x) ; m1 = m2 ⟧
      ⟹ map_ran f1 m1 = map_ran f2 m2"    
  by (induction m1 arbitrary: m2) auto

lemma domA_map_ran[simp]: "domA (map_ran f m) = domA m"
  unfolding domA_def by (rule dom_map_ran)

lemma map_ran_delete:
  "map_ran f (delete x Γ) = delete x (map_ran f Γ)"
  by (induction Γ)  auto

lemma map_ran_restrictA:
  "map_ran f (restrictA V Γ) = restrictA V (map_ran f Γ)"
  by (induction Γ)  auto

lemma map_ran_append:
  "map_ran f (Γ@Δ) = map_ran f Γ @ map_ran f Δ"
  by (induction Γ)  auto

subsubsection {* Syntax for map comprehensions *}

definition mapCollect :: "('a ⇒ 'b ⇒ 'c) ⇒ ('a ⇀ 'b) ⇒ 'c set"
  where "mapCollect f m = {f k v | k v . m k = Some v}"

syntax
 "_MapCollect" :: "'c ⇒ pttrn => pttrn ⇒ 'a ⇀ 'b => 'c set"    ("(1{_ |/_/↦/_/∈/_/})")
translations
  "{e | k↦v ∈ m}" == "CONST mapCollect (λk v. e) m"

lemma mapCollect_empty[simp]: "{f k v | k ↦ v ∈ empty} = {}"
  unfolding mapCollect_def by simp

lemma mapCollect_const[simp]:
  "m ≠ empty ⟹ {e | k↦v∈m} = {e}"
  unfolding mapCollect_def by auto

lemma mapCollect_cong[fundef_cong]:
  "(⋀ k v. m1 k = Some v ⟹ f1 k v = f2 k v) ⟹ m1 = m2 ⟹ mapCollect f1 m1 = mapCollect f2 m2"
  unfolding mapCollect_def by force

lemma mapCollectE[elim!]:
  assumes "x ∈ {f k v | k ↦ v ∈ m}"
  obtains k v where "m k = Some v" and "x = f k v"
  using assms by (auto simp add: mapCollect_def)

lemma mapCollectI[intro]:
  assumes  "m k = Some v"
  shows "f k v ∈ {f k v | k ↦ v ∈ m}"
  using assms by (auto simp add: mapCollect_def)


lemma ball_mapCollect[simp]:
  "(∀ x ∈ {f k v | k ↦ v ∈ m}. P x) ⟷ (∀ k v. m k = Some v ⟶ P (f k v))"
  by (auto simp add: mapCollect_def)

lemma image_mapCollect[simp]: 
  "g ` {f k v | k ↦ v ∈ m} = { g (f k v) | k ↦ v ∈ m}"
  by (auto simp add: mapCollect_def)

lemma mapCollect_map_upd[simp]:
  "mapCollect f (m(k↦v)) = insert (f k v) (mapCollect f (m(k := None)))"
unfolding mapCollect_def by auto


definition mapCollectFilter :: "('a ⇒ 'b ⇒ (bool × 'c)) ⇒ ('a ⇀ 'b) ⇒ 'c set"
  where "mapCollectFilter f m = {snd (f k v) | k v . m k = Some v ∧ fst (f k v)}"

syntax
 "_MapCollectFilter" :: "'c ⇒ pttrn ⇒ pttrn ⇒ ('a ⇀ 'b) ⇒ bool ⇒ 'c set"    ("(1{_ |/_/↦/_/∈/_/./ _})")
translations
  "{e | k↦v ∈ m . P }" == "CONST mapCollectFilter (λk v. (P,e)) m"

lemma mapCollectFilter_const_False[simp]:
  "{e | k↦v ∈ m . False } = {}"
  unfolding mapCollect_def mapCollectFilter_def by simp

lemma mapCollectFilter_const_True[simp]:
  "{e | k↦v ∈ m . True } = {e | k↦v ∈ m}"
  unfolding mapCollect_def mapCollectFilter_def by simp



end