Theory Map_Of

theory Map_Of
imports 
  "HOL-Library.Mapping"
  Shows_Literal
begin
  
definition map_of_default :: "'b ⇒ ('a × 'b)list ⇒ 'a ⇒ 'b" where
  "map_of_default d xs = Mapping.lookup_default d (Mapping.of_alist xs)" 

lemma map_of_default_Nil[simp]: "map_of_default d [] = (λx. d)"
  and map_of_default_Cons:
   "map_of_default d (a#alist) k = (if fst a = k then snd a else map_of_default d alist k)"
  by (auto simp: map_of_default_def lookup_default_def lookup_of_alist)

lemma map_of_defaultI: assumes "⋀ a b. (a,b) ∈ set xs ⟹ P b" "P d"
  shows "P (map_of_default d xs a)"
proof -
  note d = map_of_default_def lookup_default_def lookup_of_alist
  show ?thesis
  proof (cases "map_of xs a")
    case None
    then show ?thesis unfolding d using assms(2) by auto
  next
    case (Some b)
    then have ab: "(a,b) ∈ set xs" by (rule map_of_SomeD)
    from assms(1)[OF this]
    show ?thesis unfolding d Some by auto
  qed
qed

lemma map_of_defaultI2: assumes "⋀ b. (a,b) ∈ set xs ⟹ P b" "a ∉ fst ` set xs ⟹ P d"
  shows "P (map_of_default d xs a)"
proof -
  note d = map_of_default_def lookup_default_def lookup_of_alist
  show ?thesis
  proof (cases "map_of xs a")
    case None with this[unfolded map_of_eq_None_iff] assms(2) show ?thesis by (auto simp: d)
  next
    case (Some b)
    then have ab: "(a,b) ∈ set xs" by (rule map_of_SomeD)
    from assms(1)[OF this]
    show ?thesis unfolding d Some by auto
  qed
qed

definition map_of :: "('a × 'b)list ⇒ 'a ⇒ 'b option" where
  "map_of xs = Mapping.lookup (Mapping.of_alist xs)" 
  
hide_const(open) map_of
  
lemma map_of[simp]: "Map_Of.map_of = map_of" 
  by (intro ext, unfold Map_Of.map_of_def, rule lookup_of_alist) 

definition map_of_total :: "('a ⇒ showsl) ⇒ ('a × 'b)list ⇒ 'a ⇒ 'b" where
  "map_of_total err xys = (let m = Mapping.of_alist xys in (λ x. case Mapping.lookup m x of
     Some y ⇒ y | None ⇒ Code.abort (err x (STR '''')) (λ _. the None)))" 
  
lemma map_of_total[simp]: "map_of_total err xs = the o map_of xs"
  unfolding lookup_of_alist map_of_total_def Let_def
  by (intro ext, auto split: option.splits)
    
end