Theory Map_Extra

(* Author: Rafal Kolanski, 2008
   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
                Rafal Kolanski <rafal.kolanski at nicta.com.au>
*)

section ‹More properties of maps plus map disjuction.›

theory Map_Extra
  imports Main
begin

text ‹
  A note on naming:
  Anything not involving heap disjuction can potentially be incorporated
  directly into Map.thy, thus uses ‹m› for map variable names.
  Anything involving heap disjunction is not really mergeable with Map, is
  destined for use in separation logic, and hence uses ‹h›
›

section ‹Things that could go into Option Type›

text ‹Misc option lemmas›

lemma None_not_eq: "(None ≠ x) = (∃y. x = Some y)" by (cases x) auto

lemma None_com: "(None = x) = (x = None)" by fast

lemma Some_com: "(Some y = x) = (x = Some y)" by fast


section ‹Things that go into Map.thy›

text ‹Map intersection: set of all keys for which the maps agree.›

definition
  map_inter :: "('a ⇀ 'b) ⇒ ('a ⇀ 'b) ⇒ 'a set" (infixl ‹∩⇩m› 70) where
  "m⇩1 ∩⇩m m⇩2 ≡ {x ∈ dom m⇩1. m⇩1 x = m⇩2 x}"

text ‹Map restriction via domain subtraction›

definition
  sub_restrict_map :: "('a ⇀ 'b) => 'a set => ('a ⇀ 'b)" (infixl ‹`-›  110)
  where
  "m `- S ≡ (λx. if x ∈ S then None else m x)"


subsection ‹Properties of maps not related to restriction›

lemma empty_forall_equiv: "(m = Map.empty) = (∀x. m x = None)"
  by (fastforce intro!: ext)

lemma map_le_empty2 [simp]:
  "(m ⊆⇩m Map.empty) = (m = Map.empty)"
  by (auto simp: map_le_def intro: ext)

lemma dom_iff:
  "(∃y. m x = Some y) = (x ∈ dom m)"
  by auto

lemma non_dom_eval:
  "x ∉ dom m ⟹ m x = None"
  by auto

lemma non_dom_eval_eq:
  "x ∉ dom m = (m x = None)"
  by auto

lemma map_add_same_left_eq:
  "m⇩1 = m⇩1' ⟹ (m⇩0 ++ m⇩1 = m⇩0 ++ m⇩1')"
  by simp

lemma map_add_left_cancelI [intro!]:
  "m⇩1 = m⇩1' ⟹ m⇩0 ++ m⇩1 = m⇩0 ++ m⇩1'"
  by simp

lemma dom_empty_is_empty:
  "(dom m = {}) = (m = Map.empty)"
proof (rule iffI)
  assume a: "dom m = {}"
  { assume "m ≠ Map.empty"
    hence "dom m ≠ {}"
      by - (subst (asm) empty_forall_equiv, simp add: dom_def)
    hence False using a by blast
  }
  thus "m = Map.empty" by blast
next
  assume a: "m = Map.empty"
  thus "dom m = {}" by simp
qed

lemma map_add_dom_eq:
  "dom m = dom m' ⟹ m ++ m' = m'"
  by (rule ext) (auto simp: map_add_def split: option.splits)

lemma map_add_right_dom_eq:
  "⟦ m⇩0 ++ m⇩1 = m⇩0' ++ m⇩1'; dom m⇩1 = dom m⇩1' ⟧ ⟹ m⇩1 = m⇩1'"
  unfolding map_add_def
  by (rule ext, rule ccontr,
      drule_tac x=x in fun_cong, clarsimp split: option.splits,
      drule sym, drule sym, force+)

lemma map_le_same_dom_eq:
  "⟦ m⇩0 ⊆⇩m m⇩1 ; dom m⇩0 = dom m⇩1 ⟧ ⟹ m⇩0 = m⇩1"
  by (auto intro!: ext simp: map_le_def elim!: ballE)


subsection ‹Properties of map restriction›

lemma restrict_map_cancel:
  "(m |` S = m |` T) = (dom m ∩ S = dom m ∩ T)"
  by (fastforce intro: ext dest: fun_cong
               simp: restrict_map_def None_not_eq
               split: if_split_asm)

lemma map_add_restricted_self [simp]:
  "m ++ m |` S = m"
  by (auto intro: ext simp: restrict_map_def map_add_def split: option.splits)

lemma map_add_restrict_dom_right [simp]:
  "(m ++ m') |` dom m' = m'"
  by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)

lemma restrict_map_UNIV [simp]:
  "m |` UNIV = m"
  by (simp add: restrict_map_def)

lemma restrict_map_dom:
  "S = dom m ⟹ m |` S = m"
  by (auto intro!: ext simp: restrict_map_def None_not_eq)

lemma restrict_map_subdom:
  "dom m ⊆ S ⟹ m |` S = m"
  by (fastforce simp: restrict_map_def None_com intro: ext)

lemma map_add_restrict:
  "(m⇩0 ++ m⇩1) |` S = ((m⇩0 |` S) ++ (m⇩1 |` S))"
  by (force simp: map_add_def restrict_map_def intro: ext)

lemma map_le_restrict:
  "m ⊆⇩m m' ⟹ m = m' |` dom m"
  by (force simp: map_le_def restrict_map_def None_com intro: ext)

lemma restrict_map_le:
  "m |` S ⊆⇩m m"
  by (auto simp: map_le_def)

lemma restrict_map_remerge:
  "⟦ S ∩ T = {} ⟧ ⟹ m |` S ++ m |` T = m |` (S ∪ T)"
  by (rule ext, clarsimp simp: restrict_map_def map_add_def
                         split: option.splits)

lemma restrict_map_empty:
  "dom m ∩ S = {} ⟹ m |` S = Map.empty"
  by (fastforce simp: restrict_map_def intro: ext)

lemma map_add_restrict_comp_right [simp]:
  "(m |` S ++ m |` (UNIV - S)) = m"
  by (force simp: map_add_def restrict_map_def split: option.splits intro: ext)

lemma map_add_restrict_comp_right_dom [simp]:
  "(m |` S ++ m |` (dom m - S)) = m"
  by (auto simp: map_add_def restrict_map_def split: option.splits intro!: ext)

lemma map_add_restrict_comp_left [simp]:
  "(m |` (UNIV - S) ++ m |` S) = m"
  by (subst map_add_comm, auto)

lemma restrict_self_UNIV:
  "m |` (dom m - S) = m |` (UNIV - S)"
  by (auto intro!: ext simp: restrict_map_def)

lemma map_add_restrict_nonmember_right:
  "x ∉ dom m' ⟹ (m ++ m') |` {x} = m |` {x}"
  by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)

lemma map_add_restrict_nonmember_left:
  "x ∉ dom m ⟹ (m ++ m') |` {x} = m' |` {x}"
  by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)

lemma map_add_restrict_right:
  "x ⊆ dom m' ⟹ (m ++ m') |` x = m' |` x"
  by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)

lemma restrict_map_compose:
  "⟦ S ∪ T = dom m ; S ∩ T = {} ⟧ ⟹ m |` S ++ m |` T = m"
  by (fastforce intro: ext simp: map_add_def restrict_map_def)

lemma map_le_dom_subset_restrict:
  "⟦ m' ⊆⇩m m; dom m' ⊆ S ⟧ ⟹ m' ⊆⇩m (m |` S)"
  by (force simp: restrict_map_def map_le_def)

lemma map_le_dom_restrict_sub_add:
  "m' ⊆⇩m m ⟹ m |` (dom m - dom m') ++ m' = m"
  by (auto simp: None_com map_add_def restrict_map_def map_le_def
           split: option.splits
           intro!: ext)
     (force simp: Some_com)+

lemma subset_map_restrict_sub_add:
  "T ⊆ S ⟹ m |` (S - T) ++ m |` T = m |` S"
  by (auto simp: restrict_map_def map_add_def intro!: ext split: option.splits)

lemma restrict_map_sub_union:
  "m |` (dom m - (S ∪ T)) = (m |` (dom m - T)) |` (dom m - S)"
  by (auto intro!: ext simp: restrict_map_def)

lemma prod_restrict_map_add:
  "⟦ S ∪ T = U; S ∩ T = {} ⟧ ⟹ m |` (X × S) ++ m |` (X × T) = m |` (X × U)"
  by (auto simp: map_add_def restrict_map_def intro!: ext split: option.splits)


section ‹Things that should not go into Map.thy (separation logic)›

subsection ‹Definitions›

text ‹Map disjuction›

definition
  map_disj :: "('a ⇀ 'b) ⇒ ('a ⇀ 'b) ⇒ bool" (infix ‹⊥› 51) where
  "h⇩0 ⊥ h⇩1 ≡ dom h⇩0 ∩ dom h⇩1 = {}"

declare None_not_eq [simp]


subsection ‹Properties of @{term "sub_restrict_map"}›

lemma restrict_map_sub_disj: "h |` S ⊥ h `- S"
  by (fastforce simp: sub_restrict_map_def restrict_map_def map_disj_def
               split: option.splits if_split_asm)

lemma restrict_map_sub_add: "h |` S ++ h `- S = h"
  by (fastforce simp: sub_restrict_map_def restrict_map_def map_add_def
               split: option.splits if_split
               intro: ext)


subsection ‹Properties of map disjunction›

lemma map_disj_empty_right [simp]:
  "h ⊥ Map.empty"
  by (simp add: map_disj_def)

lemma map_disj_empty_left [simp]:
  "Map.empty ⊥ h"
  by (simp add: map_disj_def)

lemma map_disj_com:
  "h⇩0 ⊥ h⇩1 = h⇩1 ⊥ h⇩0"
  by (simp add: map_disj_def, fast)

lemma map_disjD:
  "h⇩0 ⊥ h⇩1 ⟹ dom h⇩0 ∩ dom h⇩1 = {}"
  by (simp add: map_disj_def)

lemma map_disjI:
  "dom h⇩0 ∩ dom h⇩1 = {} ⟹ h⇩0 ⊥ h⇩1"
  by (simp add: map_disj_def)


subsection ‹Map associativity-commutativity based on map disjuction›

lemma map_add_com:
  "h⇩0 ⊥ h⇩1 ⟹ h⇩0 ++ h⇩1 = h⇩1 ++ h⇩0"
  by (drule map_disjD, rule map_add_comm, force)

lemma map_add_left_commute:
  "h⇩0 ⊥ h⇩1 ⟹ h⇩0 ++ (h⇩1 ++ h⇩2) = h⇩1 ++ (h⇩0 ++ h⇩2)"
  by (simp add: map_add_com map_disj_com map_add_assoc)

lemma map_add_disj:
  "h⇩0 ⊥ (h⇩1 ++ h⇩2) = (h⇩0 ⊥ h⇩1 ∧ h⇩0 ⊥ h⇩2)"
  by (simp add: map_disj_def, fast)

lemma map_add_disj':
  "(h⇩1 ++ h⇩2) ⊥ h⇩0 = (h⇩1 ⊥ h⇩0 ∧ h⇩2 ⊥ h⇩0)"
  by (simp add: map_disj_def, fast)

text ‹
  We redefine @{term "map_add"} associativity to bind to the right, which
  seems to be the more common case.
  Note that when a theory includes Map again, ‹map_add_assoc› will
  return to the simpset and will cause infinite loops if its symmetric
  counterpart is added (e.g. via ‹map_add_ac›)
›

declare map_add_assoc [simp del]

text ‹
  Since the associativity-commutativity of @{term "map_add"} relies on
  map disjunction, we include some basic rules into the ac set.
›

lemmas map_add_ac =
  map_add_assoc[symmetric] map_add_com map_disj_com
  map_add_left_commute map_add_disj map_add_disj'


subsection ‹Basic properties›

lemma map_disj_None_right:
  "⟦ h⇩0 ⊥ h⇩1 ; x ∈ dom h⇩0 ⟧ ⟹ h⇩1 x = None"
  by (auto simp: map_disj_def dom_def)

lemma map_disj_None_left:
  "⟦ h⇩0 ⊥ h⇩1 ; x ∈ dom h⇩1 ⟧ ⟹ h⇩0 x = None"
  by (auto simp: map_disj_def dom_def)

lemma map_disj_None_left':
  "⟦ h⇩0 x = Some y ; h⇩1 ⊥ h⇩0 ⟧ ⟹ h⇩1 x = None "
  by (auto simp: map_disj_def)

lemma map_disj_None_right':
  "⟦ h⇩1 x = Some y ; h⇩1 ⊥ h⇩0 ⟧ ⟹ h⇩0 x = None "
  by (auto simp: map_disj_def)

lemma map_disj_common:
  "⟦ h⇩0 ⊥ h⇩1 ; h⇩0 p = Some v ; h⇩1 p = Some v' ⟧ ⟹ False"
  by (frule (1) map_disj_None_left', simp)

lemma map_disj_eq_dom_left:
  "⟦ h⇩0 ⊥ h⇩1 ; dom h⇩0' = dom h⇩0 ⟧ ⟹ h⇩0' ⊥ h⇩1"
  by (auto simp: map_disj_def)


subsection ‹Map disjunction and addition›

lemma map_add_eval_left:
  "⟦ x ∈ dom h ; h ⊥ h' ⟧ ⟹ (h ++ h') x = h x"
  by (auto dest!: map_disj_None_right simp: map_add_def cong: option.case_cong)

lemma map_add_eval_right:
  "⟦ x ∈ dom h' ; h ⊥ h' ⟧ ⟹ (h ++ h') x = h' x"
  by (auto elim!: map_disjD simp: map_add_comm map_add_eval_left map_disj_com)

lemma map_add_eval_left':
  "⟦ x ∉ dom h' ; h ⊥ h' ⟧ ⟹ (h ++ h') x = h x"
  by (clarsimp simp: map_disj_def map_add_def split: option.splits)

lemma map_add_eval_right':
  "⟦ x ∉ dom h ; h ⊥ h' ⟧ ⟹ (h ++ h') x = h' x"
  by (clarsimp simp: map_disj_def map_add_def split: option.splits)

lemma map_add_left_dom_eq:
  assumes eq: "h⇩0 ++ h⇩1 = h⇩0' ++ h⇩1'"
  assumes etc: "h⇩0 ⊥ h⇩1" "h⇩0' ⊥ h⇩1'" "dom h⇩0 = dom h⇩0'"
  shows "h⇩0 = h⇩0'"
proof -
  from eq have "h⇩1 ++ h⇩0 = h⇩1' ++ h⇩0'" using etc by (simp add: map_add_ac)
  thus ?thesis using etc
    by (fastforce elim!: map_add_right_dom_eq simp: map_add_ac)
qed

lemma map_add_left_eq:
  assumes eq: "h⇩0 ++ h = h⇩1 ++ h"
  assumes disj: "h⇩0 ⊥ h" "h⇩1 ⊥ h"
  shows "h⇩0 = h⇩1"
proof (rule ext)
  fix x
  from eq have eq': "(h⇩0 ++ h) x = (h⇩1 ++ h) x" by (auto intro!: ext)
  { assume "x ∈ dom h"
    hence "h⇩0 x = h⇩1 x" using disj by (simp add: map_disj_None_left)
  } moreover {
    assume "x ∉ dom h"
    hence "h⇩0 x = h⇩1 x" using disj eq' by (simp add: map_add_eval_left')
  }
  ultimately show "h⇩0 x = h⇩1 x" by cases
qed

lemma map_add_right_eq:
  "⟦h ++ h⇩0 = h ++ h⇩1; h⇩0 ⊥ h; h⇩1 ⊥ h⟧ ⟹ h⇩0 = h⇩1"
  by (rule_tac h=h in map_add_left_eq, auto simp: map_add_ac)

lemma map_disj_add_eq_dom_right_eq:
  assumes merge: "h⇩0 ++ h⇩1 = h⇩0' ++ h⇩1'" and d: "dom h⇩0 = dom h⇩0'" and
      ab_disj: "h⇩0 ⊥ h⇩1" and cd_disj: "h⇩0' ⊥ h⇩1'"
  shows "h⇩1 = h⇩1'"
proof (rule ext)
  fix x
  from merge have merge_x: "(h⇩0 ++ h⇩1) x = (h⇩0' ++ h⇩1') x" by simp
  with d ab_disj cd_disj show  "h⇩1 x = h⇩1' x"
    by - (case_tac "h⇩1 x", case_tac "h⇩1' x", simp, fastforce simp: map_disj_def,
          case_tac "h⇩1' x", clarsimp, simp add: Some_com,
          force simp: map_disj_def, simp)
qed

lemma map_disj_add_eq_dom_left_eq:
  assumes add: "h⇩0 ++ h⇩1 = h⇩0' ++ h⇩1'" and
          dom: "dom h⇩1 = dom h⇩1'" and
          disj: "h⇩0 ⊥ h⇩1" "h⇩0' ⊥ h⇩1'"
  shows "h⇩0 = h⇩0'"
proof -
  have "h⇩1 ++ h⇩0 = h⇩1' ++ h⇩0'" using add disj by (simp add: map_add_ac)
  thus ?thesis using dom disj
    by - (rule map_disj_add_eq_dom_right_eq, auto simp: map_disj_com)
qed

lemma map_add_left_cancel:
  assumes disj: "h⇩0 ⊥ h⇩1" "h⇩0 ⊥ h⇩1'"
  shows "(h⇩0 ++ h⇩1 = h⇩0 ++ h⇩1') = (h⇩1 = h⇩1')"
proof (rule iffI, rule ext)
  fix x
  assume "(h⇩0 ++ h⇩1) = (h⇩0 ++ h⇩1')"
  hence "(h⇩0 ++ h⇩1) x = (h⇩0 ++ h⇩1') x" by (auto intro!: ext)
  hence "h⇩1 x = h⇩1' x" using disj
    by - (cases "x ∈ dom h⇩0",
          simp_all add: map_disj_None_right map_add_eval_right')
  thus "h⇩1 x = h⇩1' x" by (auto intro!: ext)
qed auto

lemma map_add_lr_disj:
  "⟦ h⇩0 ++ h⇩1 = h⇩0' ++ h⇩1'; h⇩1 ⊥ h⇩1'  ⟧ ⟹ dom h⇩1 ⊆ dom h⇩0'"
  by (clarsimp simp: map_disj_def map_add_def, drule_tac x=x in fun_cong)
     (auto split: option.splits)


subsection ‹Map disjunction and map updates›

lemma map_disj_update_left [simp]:
  "p ∈ dom h⇩1 ⟹ h⇩0 ⊥ h⇩1(p ↦ v) = h⇩0 ⊥ h⇩1"
  by (clarsimp simp add: map_disj_def, blast)

lemma map_disj_update_right [simp]:
  "p ∈ dom h⇩1 ⟹ h⇩1(p ↦ v) ⊥ h⇩0 = h⇩1 ⊥ h⇩0"
  by (simp add: map_disj_com)

lemma map_add_update_left:
  "⟦ h⇩0 ⊥ h⇩1 ; p ∈ dom h⇩0 ⟧ ⟹ (h⇩0 ++ h⇩1)(p ↦ v) = (h⇩0(p ↦ v) ++ h⇩1)"
  by (drule (1) map_disj_None_right)
     (auto intro: ext simp: map_add_def cong: option.case_cong)

lemma map_add_update_right:
  "⟦ h⇩0 ⊥ h⇩1 ; p ∈ dom h⇩1  ⟧ ⟹ (h⇩0 ++ h⇩1)(p ↦ v) = (h⇩0 ++ h⇩1 (p ↦ v))"
  by (drule (1) map_disj_None_left)
     (auto intro: ext simp: map_add_def cong: option.case_cong)

lemma map_add3_update:
  "⟦ h⇩0 ⊥ h⇩1 ; h⇩1  ⊥ h⇩2 ; h⇩0 ⊥ h⇩2 ; p ∈ dom h⇩0 ⟧
  ⟹ (h⇩0 ++ h⇩1 ++ h⇩2)(p ↦ v) = h⇩0(p ↦ v) ++ h⇩1 ++ h⇩2"
  by (auto simp: map_add_update_left[symmetric] map_add_ac)


subsection ‹Map disjunction and @{term "map_le"}›

lemma map_le_override [simp]:
  "⟦ h ⊥ h' ⟧ ⟹ h ⊆⇩m h ++ h'"
  by (auto simp: map_le_def map_add_def map_disj_def split: option.splits)

lemma map_leI_left:
  "⟦ h = h⇩0 ++ h⇩1 ; h⇩0 ⊥ h⇩1 ⟧ ⟹ h⇩0 ⊆⇩m h" by auto

lemma map_leI_right:
  "⟦ h = h⇩0 ++ h⇩1 ; h⇩0 ⊥ h⇩1 ⟧ ⟹ h⇩1 ⊆⇩m h" by auto

lemma map_disj_map_le:
  "⟦ h⇩0' ⊆⇩m h⇩0; h⇩0 ⊥ h⇩1 ⟧ ⟹ h⇩0' ⊥ h⇩1"
  by (force simp: map_disj_def map_le_def)

lemma map_le_on_disj_left:
  "⟦ h' ⊆⇩m h ; h⇩0 ⊥ h⇩1 ; h' = h⇩0 ++ h⇩1 ⟧ ⟹ h⇩0 ⊆⇩m h"
  unfolding map_le_def
  by (rule ballI, erule_tac x=a in ballE, auto simp: map_add_eval_left)+

lemma map_le_on_disj_right:
  "⟦ h' ⊆⇩m h ; h⇩0 ⊥ h⇩1 ; h' = h⇩1 ++ h⇩0 ⟧ ⟹ h⇩0 ⊆⇩m h"
  by (auto simp: map_le_on_disj_left map_add_ac)

lemma map_le_add_cancel:
  "⟦ h⇩0 ⊥ h⇩1 ; h⇩0' ⊆⇩m h⇩0 ⟧ ⟹ h⇩0' ++ h⇩1 ⊆⇩m h⇩0 ++ h⇩1"
  by (auto simp: map_le_def map_add_def map_disj_def split: option.splits)

lemma map_le_override_bothD:
  assumes subm: "h⇩0' ++ h⇩1 ⊆⇩m h⇩0 ++ h⇩1"
  assumes disj': "h⇩0' ⊥ h⇩1"
  assumes disj: "h⇩0 ⊥ h⇩1"
  shows "h⇩0' ⊆⇩m h⇩0"
unfolding map_le_def
proof (rule ballI)
  fix a
  assume a: "a ∈ dom h⇩0'"
  hence sumeq: "(h⇩0' ++ h⇩1) a = (h⇩0 ++ h⇩1) a"
    using subm unfolding map_le_def by auto
  from a have "a ∉ dom h⇩1" using disj' by (auto dest!: map_disj_None_right)
  thus "h⇩0' a = h⇩0 a" using a sumeq disj disj'
    by (simp add: map_add_eval_left map_add_eval_left')
qed

lemma map_le_conv:
  "(h⇩0' ⊆⇩m h⇩0 ∧ h⇩0' ≠ h⇩0) = (∃h⇩1. h⇩0 = h⇩0' ++ h⇩1 ∧ h⇩0' ⊥ h⇩1 ∧ h⇩0' ≠ h⇩0)"
  unfolding map_le_def map_disj_def map_add_def
  by (rule iffI,
      clarsimp intro!: exI[where x="λx. if x ∉ dom h⇩0' then h⇩0 x else None"])
     (fastforce intro: ext intro: split: option.splits if_split_asm)+

lemma map_le_conv2:
  "h⇩0' ⊆⇩m h⇩0 = (∃h⇩1. h⇩0 = h⇩0' ++ h⇩1 ∧ h⇩0' ⊥ h⇩1)"
  by (case_tac "h⇩0'=h⇩0", insert map_le_conv, auto intro: exI[where x=Map.empty])


subsection ‹Map disjunction and restriction›

lemma map_disj_comp [simp]:
  "h⇩0 ⊥ h⇩1 |` (UNIV - dom h⇩0)"
  by (force simp: map_disj_def)

lemma restrict_map_disj:
  "S ∩ T = {} ⟹ h |` S ⊥ h |` T"
  by (auto simp: map_disj_def restrict_map_def dom_def)

lemma map_disj_restrict_dom [simp]:
  "h⇩0 ⊥ h⇩1 |` (dom h⇩1 - dom h⇩0)"
  by (force simp: map_disj_def)

lemma restrict_map_disj_dom_empty:
  "h ⊥ h' ⟹ h |` dom h' = Map.empty"
  by (fastforce simp: map_disj_def restrict_map_def intro: ext)

lemma restrict_map_univ_disj_eq:
  "h ⊥ h' ⟹ h |` (UNIV - dom h') = h"
  by (rule ext, auto simp: map_disj_def restrict_map_def)

lemma restrict_map_disj_dom:
  "h⇩0 ⊥ h⇩1 ⟹ h |` dom h⇩0 ⊥ h |` dom h⇩1"
  by (auto simp: map_disj_def restrict_map_def dom_def)

lemma map_add_restrict_dom_left:
  "h ⊥ h' ⟹ (h ++ h') |` dom h = h"
  by (rule ext, auto simp: restrict_map_def map_add_def dom_def map_disj_def
                     split: option.splits)

lemma map_add_restrict_dom_left':
  "h ⊥ h' ⟹ S = dom h ⟹ (h ++ h') |` S = h"
  by (rule ext, auto simp: restrict_map_def map_add_def dom_def map_disj_def
                     split: option.splits)

lemma restrict_map_disj_left:
  "h⇩0 ⊥ h⇩1 ⟹ h⇩0 |` S ⊥ h⇩1"
  by (auto simp: map_disj_def)

lemma restrict_map_disj_right:
  "h⇩0 ⊥ h⇩1 ⟹ h⇩0 ⊥ h⇩1 |` S"
  by (auto simp: map_disj_def)

lemmas restrict_map_disj_both = restrict_map_disj_right restrict_map_disj_left

lemma map_dom_disj_restrict_right:
  "h⇩0 ⊥ h⇩1 ⟹ (h⇩0 ++ h⇩0') |` dom h⇩1 = h⇩0' |` dom h⇩1"
  by (simp add: map_add_restrict restrict_map_empty map_disj_def)

lemma restrict_map_on_disj:
  "h⇩0' ⊥ h⇩1 ⟹ h⇩0 |` dom h⇩0' ⊥ h⇩1"
  unfolding map_disj_def by auto

lemma restrict_map_on_disj':
  "h⇩0 ⊥ h⇩1 ⟹ h⇩0 ⊥ h⇩1 |` S"
  by (auto simp: map_disj_def map_add_def)

lemma map_le_sub_dom:
  "⟦ h⇩0 ++ h⇩1 ⊆⇩m h ; h⇩0 ⊥ h⇩1 ⟧ ⟹ h⇩0 ⊆⇩m h |` (dom h - dom h⇩1)"
  by (rule map_le_override_bothD, subst map_le_dom_restrict_sub_add)
     (auto elim: map_add_le_mapE simp: map_add_ac)

lemma map_submap_break:
  "⟦ h ⊆⇩m h' ⟧ ⟹ h' = (h' |` (UNIV - dom h)) ++ h"
  by (fastforce intro!: ext split: option.splits
               simp: map_le_restrict restrict_map_def map_le_def map_add_def
                     dom_def)

lemma map_add_disj_restrict_both:
  "⟦ h⇩0 ⊥ h⇩1; S ∩ S' = {}; T ∩ T' = {} ⟧
   ⟹ (h⇩0 |` S) ++ (h⇩1 |` T) ⊥ (h⇩0 |` S') ++ (h⇩1 |` T')"
  by (auto simp: map_add_ac intro!: restrict_map_disj_both restrict_map_disj)

end