Theory MapExtra
section ‹More properties of maps plus map disjuction.›
theory MapExtra
imports Main
begin
text ‹
BEWARE: we are not interested in using the @{term "dom x ∩ dom y = {}"}
rules from Map for our separation logic proofs. As such, we overwrite the
Map rules where that form of disjointness is in the assumption conflicts
with a name we want to use with @{text "⊥"}.›
text ‹
A note on naming:
Anything not involving heap disjuction can potentially be incorporated
directly into Map.thy, thus uses @{text "m"}.
Anything involving heap disjunction is not really mergeable with Map, is
destined for use in separation logic, and hence uses @{text "h"}
›
text ‹---------------------------------------›
text ‹Things that should go into Option Type›
text ‹---------------------------------------›
text ‹Misc option lemmas›
lemma : "(None ≠ x) = (∃y. x = Some y)" by (cases x) auto
lemma : "(None = x) = (x = None)" by fast
lemma : "(Some y = x) = (x = Some y)" by fast
text ‹---------------------------------------›
text ‹Things that should go into Map.thy›
text ‹---------------------------------------›
text ‹Map intersection: set of all keys for which the maps agree.›
:: "('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›
:: "('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 : "(m = Map.empty) = (∀x. m x = None)"
by (rule fun_eq_iff)
lemma [simp]:
"(m ⊆⇩m Map.empty) = (m = Map.empty)"
by (auto simp: map_le_def)
lemma :
"(∃y. m x = Some y) = (x ∈ dom m)"
by auto
lemma :
"x ∉ dom m ⟹ m x = None"
by auto
lemma :
"x ∉ dom m = (m x = None)"
by auto
lemma :
"m⇩1 = m⇩1' ⟹ (m⇩0 ++ m⇩1 = m⇩0 ++ m⇩1')"
by simp
lemma [intro!]:
"m⇩1 = m⇩1' ⟹ m⇩0 ++ m⇩1 = m⇩0 ++ m⇩1'"
by simp
lemma :
"(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 :
"dom m = dom m' ⟹ m ++ m' = m'"
by (rule ext) (auto simp: map_add_def split: option.splits)
lemma :
"⟦ m⇩0 ++ m⇩1 = m⇩0' ++ m⇩1'; dom m⇩1 = dom m⇩1' ⟧ ⟹ m⇩1 = m⇩1'"
unfolding map_add_def
apply (rule ext)
apply (rule ccontr)
subgoal for x
apply (drule fun_cong [where x=x], clarsimp split: option.splits)
apply (drule sym, drule sym, force+)
done
done
lemma :
"⟦ m⇩0 ⊆⇩m m⇩1 ; dom m⇩0 = dom m⇩1 ⟧ ⟹ m⇩0 = m⇩1"
by (simp add: map_le_antisym map_le_def)
subsection ‹Properties of map restriction›
lemma :
"(m |` S = m |` T) = (dom m ∩ S = dom m ∩ T)"
by (fastforce intro: set_eqI dest: fun_cong
simp: restrict_map_def None_not_eq
split: if_split_asm)
lemma [simp]:
"m ++ m |` S = m"
by (auto simp: restrict_map_def map_add_def split: option.splits)
lemma [simp]:
"(m ++ m') |` dom m' = m'"
by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)
lemma [simp]:
"m |` UNIV = m"
by (simp add: restrict_map_def)
lemma :
"S = dom m ⟹ m |` S = m"
by (fastforce simp: restrict_map_def None_not_eq)
lemma :
"dom m ⊆ S ⟹ m |` S = m"
by (fastforce simp: restrict_map_def None_com)
lemma :
"(m⇩0 ++ m⇩1) |` S = ((m⇩0 |` S) ++ (m⇩1 |` S))"
by (force simp: map_add_def restrict_map_def)
lemma :
"m ⊆⇩m m' ⟹ m = m' |` dom m"
by (force simp: map_le_def restrict_map_def None_com)
lemma :
"m |` S ⊆⇩m m"
by (auto simp: map_le_def)
lemma :
"⟦ S ∩ T = {} ⟧ ⟹ m |` S ++ m |` T = m |` (S ∪ T)"
by (rule ext, clarsimp simp: restrict_map_def map_add_def
split: option.splits)
lemma :
"dom m ∩ S = {} ⟹ m |` S = Map.empty"
by (fastforce simp: restrict_map_def)
lemma [simp]:
"(m |` S ++ m |` (UNIV - S)) = m"
by (force simp: map_add_def restrict_map_def split: option.splits)
lemma [simp]:
"(m |` S ++ m |` (dom m - S)) = m"
by (fastforce simp: map_add_def restrict_map_def split: option.splits)
lemma [simp]:
"(m |` (UNIV - S) ++ m |` S) = m"
by (subst map_add_comm, auto)
lemma :
"m |` (dom m - S) = m |` (UNIV - S)"
by (fastforce simp: restrict_map_def)
lemma :
"x ∉ dom m' ⟹ (m ++ m') |` {x} = m |` {x}"
by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)
lemma :
"x ∉ dom m ⟹ (m ++ m') |` {x} = m' |` {x}"
by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)
lemma :
"x ⊆ dom m' ⟹ (m ++ m') |` x = m' |` x"
by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)
lemma :
"⟦ S ∪ T = dom m ; S ∩ T = {} ⟧ ⟹ m |` S ++ m |` T = m"
by (fastforce simp: map_add_def restrict_map_def)
lemma :
"⟦ m' ⊆⇩m m; dom m' ⊆ S ⟧ ⟹ m' ⊆⇩m (m |` S)"
by (force simp: restrict_map_def map_le_def)
lemma :
"m' ⊆⇩m m ⟹ m |` (dom m - dom m') ++ m' = m"
by (metis map_add_restrict_comp_right_dom map_le_iff_map_add_commute map_le_restrict)
lemma :
"T ⊆ S ⟹ m |` (S - T) ++ m |` T = m |` S"
by (fastforce simp: restrict_map_def map_add_def split: option.splits)
lemma :
"m |` (dom m - (S ∪ T)) = (m |` (dom m - T)) |` (dom m - S)"
by (auto simp: restrict_map_def)
lemma :
"⟦ S ∪ T = U; S ∩ T = {} ⟧ ⟹ m |` (X × S) ++ m |` (X × T) = m |` (X × U)"
by (auto simp: map_add_def restrict_map_def split: option.splits)
text ‹---------------------------------------›
text ‹Things that should NOT go into Map.thy›
text ‹---------------------------------------›
section ‹Definitions›
text ‹Map disjuction›
:: "('a ⇀ 'b) ⇒ ('a ⇀ 'b) ⇒ bool" (infix "⊥" 51) where
"h⇩0 ⊥ h⇩1 ≡ dom h⇩0 ∩ dom h⇩1 = {}"
declare None_not_eq [simp]
text ‹Heap monotonicity and the frame property›
:: "(('a ⇀ 'b) ⇒ 'c option) ⇒ bool" where
"heap_mono f ≡ ∀h h' v. h ⊥ h' ∧ f h = Some v ⟶ f (h ++ h') = Some v"
lemma :
"⟦ heap_mono f ; f h = Some v ; h ⊥ h' ⟧ ⟹ f (h ++ h') = Some v"
unfolding heap_mono_def by blast
lemma :
"⟦ heap_mono f ; f h = Some v ; h ⊥ h' ⟧ ⟹ f (h ++ h') = f h"
by (frule (2) heap_monoE, simp)
:: "(('a ⇀ 'b) ⇒ 'c option) ⇒ bool" where
"heap_frame f ≡ ∀h h' v. h ⊥ h' ∧ f (h ++ h') = Some v
⟶ (f h = Some v ∨ f h = None)"
lemma :
"⟦ heap_frame f ; f (h ++ h') = Some v ; h ⊥ h' ⟧
⟹ f h = Some v ∨ f h = None"
unfolding heap_frame_def by fastforce
section ‹Properties of @{term "sub_restrict_map"}›
lemma : "h |` S ⊥ h `- S"
by (fastforce simp: sub_restrict_map_def restrict_map_def map_disj_def
split: option.splits if_split_asm)
lemma : "h |` S ++ h `- S = h"
by (fastforce simp: sub_restrict_map_def restrict_map_def map_add_def
split: option.splits if_split)
section ‹Properties of map disjunction›
lemma [simp]:
"h ⊥ Map.empty"
by (simp add: map_disj_def)
lemma [simp]:
"Map.empty ⊥ h"
by (simp add: map_disj_def)
lemma :
"h⇩0 ⊥ h⇩1 = h⇩1 ⊥ h⇩0"
by (simp add: map_disj_def, fast)
lemma :
"h⇩0 ⊥ h⇩1 ⟹ dom h⇩0 ∩ dom h⇩1 = {}"
by (simp add: map_disj_def)
lemma :
"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 :
"h⇩0 ⊥ h⇩1 ⟹ h⇩0 ++ h⇩1 = h⇩1 ++ h⇩0"
by (drule map_disjD, rule map_add_comm, force)
lemma :
"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)
lemma :
"h⇩0 ⊥ (h⇩1 ++ h⇩2) = (h⇩0 ⊥ h⇩1 ∧ h⇩0 ⊥ h⇩2)"
by (simp add: map_disj_def, fast)
lemma :
"(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, @{text "map_add_assoc"} will
return to the simpset and will cause infinite loops if its symmetric
counterpart is added (e.g. via @{text "map_ac_simps"})
›
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_assoc[symmetric] map_add_com map_disj_com
map_add_left_commute map_add_disj map_add_disj'
subsection ‹Basic properties›
lemma :
"⟦ h⇩0 ⊥ h⇩1 ; x ∈ dom h⇩0 ⟧ ⟹ h⇩1 x = None"
by (auto simp: map_disj_def dom_def)
lemma :
"⟦ h⇩0 ⊥ h⇩1 ; x ∈ dom h⇩1 ⟧ ⟹ h⇩0 x = None"
by (auto simp: map_disj_def dom_def)
lemma :
"⟦ h⇩0 x = Some y ; h⇩1 ⊥ h⇩0 ⟧ ⟹ h⇩1 x = None "
by (auto simp: map_disj_def)
lemma :
"⟦ h⇩1 x = Some y ; h⇩1 ⊥ h⇩0 ⟧ ⟹ h⇩0 x = None "
by (auto simp: map_disj_def)
lemma :
"⟦ h⇩0 ⊥ h⇩1 ; h⇩0 p = Some v ; h⇩1 p = Some v' ⟧ ⟹ False"
by (frule (1) map_disj_None_left', simp)
subsection ‹Map disjunction and addition›
lemma :
"⟦ 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 :
"⟦ 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 :
"⟦ x ∉ dom h' ; h ⊥ h' ⟧ ⟹ (h ++ h') x = h x"
by (clarsimp simp: map_disj_def map_add_def split: option.splits)
lemma :
"⟦ x ∉ dom h ; h ⊥ h' ⟧ ⟹ (h ++ h') x = h' x"
by (clarsimp simp: map_disj_def map_add_def split: option.splits)
lemma :
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_ac_simps)
thus ?thesis using etc
by (fastforce elim!: map_add_right_dom_eq simp: map_ac_simps)
qed
lemma :
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
{ 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 :
"⟦h ++ h⇩0 = h ++ h⇩1; h⇩0 ⊥ h; h⇩1 ⊥ h⟧ ⟹ h⇩0 = h⇩1"
by (rule map_add_left_eq [where h=h], auto simp: map_ac_simps)
lemma :
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"
apply (cases "h⇩1 x")
apply (cases "h⇩1' x")
apply force
apply (fastforce simp: map_disj_def)
apply (cases "h⇩1' x")
apply clarsimp
apply (simp add: Some_com)
by (force simp: map_disj_def)+
qed
lemma :
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_ac_simps)
thus ?thesis using dom disj
by - (rule map_disj_add_eq_dom_right_eq, auto simp: map_disj_com)
qed
lemma :
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
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
qed auto
lemma :
"⟦ h⇩0 ++ h⇩1 = h⇩0' ++ h⇩1'; h⇩1 ⊥ h⇩1' ⟧ ⟹ dom h⇩1 ⊆ dom h⇩0'"
apply (clarsimp simp: map_disj_def map_add_def)
subgoal for x y
apply (drule fun_cong [where x=x])
apply (auto split: option.splits)
done
done
subsection ‹Map disjunction and updates›
lemma [simp]:
"p ∈ dom h⇩1 ⟹ h⇩0 ⊥ h⇩1(p ↦ v) = h⇩0 ⊥ h⇩1"
by (clarsimp simp add: map_disj_def, blast)
lemma [simp]:
"p ∈ dom h⇩1 ⟹ h⇩1(p ↦ v) ⊥ h⇩0 = h⇩1 ⊥ h⇩0"
by (simp add: map_disj_com)
lemma :
"⟦ 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 simp: map_add_def cong: option.case_cong)
lemma :
"⟦ 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 simp: map_add_def cong: option.case_cong)
lemma :
"⟦ 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_ac_simps)
subsection ‹Map disjunction and @{term "map_le"}›
lemma [simp]:
"⟦ h ⊥ h' ⟧ ⟹ h ⊆⇩m h ++ h'"
by (auto simp: map_le_def map_add_def map_disj_def split: option.splits)
lemma :
"⟦ h = h⇩0 ++ h⇩1 ; h⇩0 ⊥ h⇩1 ⟧ ⟹ h⇩0 ⊆⇩m h" by auto
lemma :
"⟦ h = h⇩0 ++ h⇩1 ; h⇩0 ⊥ h⇩1 ⟧ ⟹ h⇩1 ⊆⇩m h" by auto
lemma :
"⟦ h⇩0' ⊆⇩m h⇩0; h⇩0 ⊥ h⇩1 ⟧ ⟹ h⇩0' ⊥ h⇩1"
by (force simp: map_disj_def map_le_def)
lemma :
"⟦ h' ⊆⇩m h ; h⇩0 ⊥ h⇩1 ; h' = h⇩0 ++ h⇩1 ⟧ ⟹ h⇩0 ⊆⇩m h"
unfolding map_le_def
apply (rule ballI)
subgoal for a
apply (erule ballE [where x=a], auto simp: map_add_eval_left)+
done
done
lemma :
"⟦ 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_ac_simps)
lemma :
"⟦ 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 :
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 :
"(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
using exI[where x="λx. if x ∉ dom h⇩0' then h⇩0 x else None"]
by (rule iffI, clarsimp)
(fastforce intro: set_eqI split: option.splits if_split_asm)+
lemma :
"h⇩0' ⊆⇩m h⇩0 = (∃h⇩1. h⇩0 = h⇩0' ++ h⇩1 ∧ h⇩0' ⊥ h⇩1)"
by (cases "h⇩0'=h⇩0", insert map_le_conv, auto intro: exI[where x=Map.empty])
subsection ‹Map disjunction and restriction›
lemma [simp]:
"h⇩0 ⊥ h⇩1 |` (UNIV - dom h⇩0)"
by (force simp: map_disj_def)
lemma :
"S ∩ T = {} ⟹ h |` S ⊥ h |` T"
by (auto simp: map_disj_def restrict_map_def dom_def)
lemma [simp]:
"h⇩0 ⊥ h⇩1 |` (dom h⇩1 - dom h⇩0)"
by (force simp: map_disj_def)
lemma :
"h ⊥ h' ⟹ h |` dom h' = Map.empty"
by (fastforce simp: map_disj_def restrict_map_def)
lemma :
"h ⊥ h' ⟹ h |` (UNIV - dom h') = h"
by (rule ext, auto simp: map_disj_def restrict_map_def)
lemma :
"h⇩0 ⊥ h⇩1 ⟹ h |` dom h⇩0 ⊥ h |` dom h⇩1"
by (auto simp: map_disj_def restrict_map_def dom_def)
lemma :
"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 :
"h⇩0 ⊥ h⇩1 ⟹ h⇩0 |` S ⊥ h⇩1"
by (auto simp: map_disj_def)
lemma :
"h⇩0 ⊥ h⇩1 ⟹ h⇩0 ⊥ h⇩1 |` S"
by (auto simp: map_disj_def)
lemmas = restrict_map_disj_right restrict_map_disj_left
lemma :
"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 :
"h⇩0' ⊥ h⇩1 ⟹ h⇩0 |` dom h⇩0' ⊥ h⇩1"
unfolding map_disj_def by auto
lemma :
"h⇩0 ⊥ h⇩1 ⟹ h⇩0 ⊥ h⇩1 |` S"
by (auto simp: map_disj_def map_add_def)
lemma :
"⟦ 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_ac_simps)
lemma :
"⟦ h ⊆⇩m h' ⟧ ⟹ h' = (h' |` (UNIV - dom h)) ++ h"
by (fastforce split: option.splits
simp: map_le_restrict restrict_map_def map_le_def map_add_def dom_def)
lemma :
"⟦ h⇩0 ⊥ h⇩1; S ∩ S' = {}; T ∩ T' = {} ⟧
⟹ (h⇩0 |` S) ++ (h⇩1 |` T) ⊥ (h⇩0 |` S') ++ (h⇩1 |` T')"
by (auto simp: map_ac_simps intro!: restrict_map_disj_both restrict_map_disj)
end