Theory PartialMap

section ‹State Model›

subsection ‹Partial Heaps›

theory PartialMap
  imports Main
begin

type_synonym ('a, 'b) map = "'a ⇀ 'b"

fun compatible_options :: "('a ⇒ 'a ⇒ bool) ⇒ 'a option ⇒ 'a option ⇒ bool" where
  "compatible_options f (Some a) (Some b) ⟷ f a b"
| "compatible_options _ _ _ ⟷ True"

fun merge_option :: "('b ⇒ 'b ⇒ 'b) ⇒ 'b option ⇒ 'b option ⇒ 'b option" where
  "merge_option _ None None = None"
| "merge_option _ (Some a) None = Some a"
| "merge_option _ None (Some b) = Some b"
| "merge_option f (Some a) (Some b) = Some (f a b)"

definition merge_options :: "('c ⇒ 'c ⇒ 'c) ⇒ ('b, 'c) map ⇒ ('b, 'c) map ⇒ ('b, 'c) map" where
  "merge_options f a b p = merge_option f (a p) (b p)"

definition compatible_maps :: "('b ⇒ 'b ⇒ bool) ⇒ ('a, 'b) map ⇒ ('a, 'b) map ⇒ bool" where
  "compatible_maps f h1 h2 ⟷ (∀hl. compatible_options f (h1 hl) (h2 hl))"

lemma compatible_mapsI:
  assumes "⋀x a b. h1 x = Some a ∧ h2 x = Some b ⟹ f a b"
  shows "compatible_maps f h1 h2"
  by (metis assms compatible_maps_def compatible_options.elims(3))

definition map_included :: "('a, 'b) map ⇒ ('a, 'b) map ⇒ bool" where
  "map_included h1 h2 ⟷ (∀x. h1 x ≠ None ⟶ h1 x = h2 x)"

lemma map_includedI:
  assumes "⋀x r. h1 x = Some r ⟹ h2 x = Some r"
  shows "map_included h1 h2"
  by (metis assms map_included_def option.exhaust)

lemma compatible_maps_empty:
  "compatible_maps f h (Map.empty)"
  by (simp add: compatible_maps_def)

lemma compatible_maps_comm:
  "compatible_maps (=) h1 h2 ⟷ compatible_maps (=) h2 h1"
proof -
  have "⋀a b. compatible_maps (=) a b ⟹ compatible_maps (=) b a"
    by (metis (mono_tags, lifting) compatible_mapsI compatible_maps_def compatible_options.simps(1))
  then show ?thesis
    by auto
qed

lemma add_heaps_asso:
  "(h1 ++ h2) ++ h3 = h1 ++ (h2 ++ h3)"
  by auto

lemma compatible_maps_same:
  assumes "compatible_maps (=) ha hb"
      and "ha x = Some y"
    shows "(ha ++ hb) x = Some y"
proof (cases "hb x")
  case None
  then show ?thesis 
    by (simp add: assms(2) map_add_Some_iff)
next
  case (Some a)
  then show ?thesis
    by (metis (mono_tags) assms(1) assms(2) compatible_maps_def compatible_options.simps(1) map_add_def option.simps(5))
qed

lemma compatible_maps_refl:
  "compatible_maps (=) h h"
  using compatible_maps_def compatible_options.elims(3) by fastforce

lemma map_invo:
  "h ++ h = h"
  by (simp add: map_add_subsumed2)

lemma included_then_compatible_maps:
  assumes "map_included h1 h"
      and "map_included h2 h"
    shows "compatible_maps (=) h1 h2"
proof (rule compatible_mapsI)
  fix x a b assume "h1 x = Some a ∧ h2 x = Some b"
  show "a = b"
    by (metis ‹h1 x = Some a ∧ h2 x = Some b› assms(1) assms(2) map_included_def option.inject option.simps(3))
qed

lemma commut_charact:
  assumes "compatible_maps (=) h1 h2"
  shows "h1 ++ h2 = h2 ++ h1"
proof (rule ext)
  fix x
  show "(h1 ++ h2) x = (h2 ++ h1) x"
  proof (cases "h1 x")
    case None
    then show ?thesis
      by (simp add: domIff map_add_dom_app_simps(2) map_add_dom_app_simps(3))
  next
    case (Some a)
    then show ?thesis
      by (simp add: assms compatible_maps_same)
  qed
qed

end