Theory PartialMap

section ‹State Model›

subsection ‹Partial Heaps›

text ‹In this file, we prove useful lemmas about partial maps. Partial maps are used to define
  permission heaps (see FractionalHeap.thy) and the family of unique action guard states (see StateModel.thy).›

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)"

text ‹Two maps are compatible iff they are compatible pointwise (i.e., if both define values,
then those values are compatible›
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