1 (* Author: Rafal Kolanski, 2008

     2    Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>

     3                 Rafal Kolanski <rafal.kolanski at nicta.com.au>

     4 *)

     5 

     6 header {* More properties of maps plus map disjuction. *}

     7 

     8 theory Map_Extra

     9   imports Main

    10 begin

    11 

    12 text {*

    13   A note on naming:

    14   Anything not involving heap disjuction can potentially be incorporated

    15   directly into Map.thy, thus uses @{text "m"} for map variable names.

    16   Anything involving heap disjunction is not really mergeable with Map, is

    17   destined for use in separation logic, and hence uses @{text "h"}

    18 *}

    19 

    20 section {* Things that could go into Option Type *}

    21 

    22 text {* Misc option lemmas *}

    23 

    24 lemma None_not_eq: "(None \<noteq> x) = (\<exists>y. x = Some y)" by (cases x) auto

    25 

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

    27 

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

    29 

    30 

    31 section {* Things that go into Map.thy *}

    32 

    33 text {* Map intersection: set of all keys for which the maps agree. *}

    34 

    35 definition

    36   map_inter :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a set" (infixl "\<inter>\<^isub>m" 70) where

    37   "m\<^isub>1 \<inter>\<^isub>m m\<^isub>2 \<equiv> {x \<in> dom m\<^isub>1. m\<^isub>1 x = m\<^isub>2 x}"

    38 

    39 text {* Map restriction via domain subtraction *}

    40 

    41 definition

    42   sub_restrict_map :: "('a \<rightharpoonup> 'b) => 'a set => ('a \<rightharpoonup> 'b)" (infixl "`-"  110)

    43   where

    44   "m `- S \<equiv> (\<lambda>x. if x \<in> S then None else m x)"

    45 

    46 

    47 subsection {* Properties of maps not related to restriction *}

    48 

    49 lemma empty_forall_equiv: "(m = empty) = (\<forall>x. m x = None)"

    50   by (fastforce intro!: ext)

    51 

    52 lemma map_le_empty2 [simp]:

    53   "(m \<subseteq>\<^sub>m empty) = (m = empty)"

    54   by (auto simp: map_le_def intro: ext)

    55 

    56 lemma dom_iff:

    57   "(\<exists>y. m x = Some y) = (x \<in> dom m)"

    58   by auto

    59 

    60 lemma non_dom_eval:

    61   "x \<notin> dom m \<Longrightarrow> m x = None"

    62   by auto

    63 

    64 lemma non_dom_eval_eq:

    65   "x \<notin> dom m = (m x = None)"

    66   by auto

    67 

    68 lemma map_add_same_left_eq:

    69   "m\<^isub>1 = m\<^isub>1' \<Longrightarrow> (m\<^isub>0 ++ m\<^isub>1 = m\<^isub>0 ++ m\<^isub>1')"

    70   by simp

    71 

    72 lemma map_add_left_cancelI [intro!]:

    73   "m\<^isub>1 = m\<^isub>1' \<Longrightarrow> m\<^isub>0 ++ m\<^isub>1 = m\<^isub>0 ++ m\<^isub>1'"

    74   by simp

    75 

    76 lemma dom_empty_is_empty:

    77   "(dom m = {}) = (m = empty)"

    78 proof (rule iffI)

    79   assume a: "dom m = {}"

    80   { assume "m \<noteq> empty"

    81     hence "dom m \<noteq> {}"

    82       by - (subst (asm) empty_forall_equiv, simp add: dom_def)

    83     hence False using a by blast

    84   }

    85   thus "m = empty" by blast

    86 next

    87   assume a: "m = empty"

    88   thus "dom m = {}" by simp

    89 qed

    90 

    91 lemma map_add_dom_eq:

    92   "dom m = dom m' \<Longrightarrow> m ++ m' = m'"

    93   by (rule ext) (auto simp: map_add_def split: option.splits)

    94 

    95 lemma map_add_right_dom_eq:

    96   "\<lbrakk> m\<^isub>0 ++ m\<^isub>1 = m\<^isub>0' ++ m\<^isub>1'; dom m\<^isub>1 = dom m\<^isub>1' \<rbrakk> \<Longrightarrow> m\<^isub>1 = m\<^isub>1'"

    97   unfolding map_add_def

    98   by (rule ext, rule ccontr,

    99       drule_tac x=x in fun_cong, clarsimp split: option.splits,

   100       drule sym, drule sym, force+)

   101 

   102 lemma map_le_same_dom_eq:

   103   "\<lbrakk> m\<^isub>0 \<subseteq>\<^sub>m m\<^isub>1 ; dom m\<^isub>0 = dom m\<^isub>1 \<rbrakk> \<Longrightarrow> m\<^isub>0 = m\<^isub>1"

   104   by (auto intro!: ext simp: map_le_def elim!: ballE)

   105 

   106 

   107 subsection {* Properties of map restriction *}

   108 

   109 lemma restrict_map_cancel:

   110   "(m |` S = m |` T) = (dom m \<inter> S = dom m \<inter> T)"

   111   by (fastforce intro: ext dest: fun_cong

   112                simp: restrict_map_def None_not_eq

   113                split: split_if_asm)

   114 

   115 lemma map_add_restricted_self [simp]:

   116   "m ++ m |` S = m"

   117   by (auto intro: ext simp: restrict_map_def map_add_def split: option.splits)

   118 

   119 lemma map_add_restrict_dom_right [simp]:

   120   "(m ++ m') |` dom m' = m'"

   121   by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)

   122 

   123 lemma restrict_map_UNIV [simp]:

   124   "m |` UNIV = m"

   125   by (simp add: restrict_map_def)

   126 

   127 lemma restrict_map_dom:

   128   "S = dom m \<Longrightarrow> m |` S = m"

   129   by (auto intro!: ext simp: restrict_map_def None_not_eq)

   130 

   131 lemma restrict_map_subdom:

   132   "dom m \<subseteq> S \<Longrightarrow> m |` S = m"

   133   by (fastforce simp: restrict_map_def None_com intro: ext)

   134 

   135 lemma map_add_restrict:

   136   "(m\<^isub>0 ++ m\<^isub>1) |` S = ((m\<^isub>0 |` S) ++ (m\<^isub>1 |` S))"

   137   by (force simp: map_add_def restrict_map_def intro: ext)

   138 

   139 lemma map_le_restrict:

   140   "m \<subseteq>\<^sub>m m' \<Longrightarrow> m = m' |` dom m"

   141   by (force simp: map_le_def restrict_map_def None_com intro: ext)

   142 

   143 lemma restrict_map_le:

   144   "m |` S \<subseteq>\<^sub>m m"

   145   by (auto simp: map_le_def)

   146 

   147 lemma restrict_map_remerge:

   148   "\<lbrakk> S \<inter> T = {} \<rbrakk> \<Longrightarrow> m |` S ++ m |` T = m |` (S \<union> T)"

   149   by (rule ext, clarsimp simp: restrict_map_def map_add_def

   150                          split: option.splits)

   151 

   152 lemma restrict_map_empty:

   153   "dom m \<inter> S = {} \<Longrightarrow> m |` S = empty"

   154   by (fastforce simp: restrict_map_def intro: ext)

   155 

   156 lemma map_add_restrict_comp_right [simp]:

   157   "(m |` S ++ m |` (UNIV - S)) = m"

   158   by (force simp: map_add_def restrict_map_def split: option.splits intro: ext)

   159 

   160 lemma map_add_restrict_comp_right_dom [simp]:

   161   "(m |` S ++ m |` (dom m - S)) = m"

   162   by (auto simp: map_add_def restrict_map_def split: option.splits intro!: ext)

   163 

   164 lemma map_add_restrict_comp_left [simp]:

   165   "(m |` (UNIV - S) ++ m |` S) = m"

   166   by (subst map_add_comm, auto)

   167 

   168 lemma restrict_self_UNIV:

   169   "m |` (dom m - S) = m |` (UNIV - S)"

   170   by (auto intro!: ext simp: restrict_map_def)

   171 

   172 lemma map_add_restrict_nonmember_right:

   173   "x \<notin> dom m' \<Longrightarrow> (m ++ m') |` {x} = m |` {x}"

   174   by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)

   175 

   176 lemma map_add_restrict_nonmember_left:

   177   "x \<notin> dom m \<Longrightarrow> (m ++ m') |` {x} = m' |` {x}"

   178   by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)

   179 

   180 lemma map_add_restrict_right:

   181   "x \<subseteq> dom m' \<Longrightarrow> (m ++ m') |` x = m' |` x"

   182   by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)

   183 

   184 lemma restrict_map_compose:

   185   "\<lbrakk> S \<union> T = dom m ; S \<inter> T = {} \<rbrakk> \<Longrightarrow> m |` S ++ m |` T = m"

   186   by (fastforce intro: ext simp: map_add_def restrict_map_def)

   187 

   188 lemma map_le_dom_subset_restrict:

   189   "\<lbrakk> m' \<subseteq>\<^sub>m m; dom m' \<subseteq> S \<rbrakk> \<Longrightarrow> m' \<subseteq>\<^sub>m (m |` S)"

   190   by (force simp: restrict_map_def map_le_def)

   191 

   192 lemma map_le_dom_restrict_sub_add:

   193   "m' \<subseteq>\<^sub>m m \<Longrightarrow> m |` (dom m - dom m') ++ m' = m"

   194   by (auto simp: None_com map_add_def restrict_map_def map_le_def

   195            split: option.splits

   196            intro!: ext)

   197      (force simp: Some_com)+

   198 

   199 lemma subset_map_restrict_sub_add:

   200   "T \<subseteq> S \<Longrightarrow> m |` (S - T) ++ m |` T = m |` S"

   201   by (auto simp: restrict_map_def map_add_def intro!: ext split: option.splits)

   202 

   203 lemma restrict_map_sub_union:

   204   "m |` (dom m - (S \<union> T)) = (m |` (dom m - T)) |` (dom m - S)"

   205   by (auto intro!: ext simp: restrict_map_def)

   206 

   207 lemma prod_restrict_map_add:

   208   "\<lbrakk> S \<union> T = U; S \<inter> T = {} \<rbrakk> \<Longrightarrow> m |` (X \<times> S) ++ m |` (X \<times> T) = m |` (X \<times> U)"

   209   by (auto simp: map_add_def restrict_map_def intro!: ext split: option.splits)

   210 

   211 

   212 section {* Things that should not go into Map.thy (separation logic) *}

   213 

   214 subsection {* Definitions *}

   215 

   216 text {* Map disjuction *}

   217 

   218 definition

   219   map_disj :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix "\<bottom>" 51) where

   220   "h\<^isub>0 \<bottom> h\<^isub>1 \<equiv> dom h\<^isub>0 \<inter> dom h\<^isub>1 = {}"

   221 

   222 declare None_not_eq [simp]

   223 

   224 

   225 subsection {* Properties of @{term "sub_restrict_map"} *}

   226 

   227 lemma restrict_map_sub_disj: "h |` S \<bottom> h `- S"

   228   by (fastforce simp: sub_restrict_map_def restrict_map_def map_disj_def

   229                split: option.splits split_if_asm)

   230 

   231 lemma restrict_map_sub_add: "h |` S ++ h `- S = h"

   232   by (fastforce simp: sub_restrict_map_def restrict_map_def map_add_def

   233                split: option.splits split_if

   234                intro: ext)

   235 

   236 

   237 subsection {* Properties of map disjunction *}

   238 

   239 lemma map_disj_empty_right [simp]:

   240   "h \<bottom> empty"

   241   by (simp add: map_disj_def)

   242 

   243 lemma map_disj_empty_left [simp]:

   244   "empty \<bottom> h"

   245   by (simp add: map_disj_def)

   246 

   247 lemma map_disj_com:

   248   "h\<^isub>0 \<bottom> h\<^isub>1 = h\<^isub>1 \<bottom> h\<^isub>0"

   249   by (simp add: map_disj_def, fast)

   250 

   251 lemma map_disjD:

   252   "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> dom h\<^isub>0 \<inter> dom h\<^isub>1 = {}"

   253   by (simp add: map_disj_def)

   254 

   255 lemma map_disjI:

   256   "dom h\<^isub>0 \<inter> dom h\<^isub>1 = {} \<Longrightarrow> h\<^isub>0 \<bottom> h\<^isub>1"

   257   by (simp add: map_disj_def)

   258 

   259 

   260 subsection {* Map associativity-commutativity based on map disjuction *}

   261 

   262 lemma map_add_com:

   263   "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> h\<^isub>0 ++ h\<^isub>1 = h\<^isub>1 ++ h\<^isub>0"

   264   by (drule map_disjD, rule map_add_comm, force)

   265 

   266 lemma map_add_left_commute:

   267   "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> h\<^isub>0 ++ (h\<^isub>1 ++ h\<^isub>2) = h\<^isub>1 ++ (h\<^isub>0 ++ h\<^isub>2)"

   268   by (simp add: map_add_com map_disj_com map_add_assoc)

   269 

   270 lemma map_add_disj:

   271   "h\<^isub>0 \<bottom> (h\<^isub>1 ++ h\<^isub>2) = (h\<^isub>0 \<bottom> h\<^isub>1 \<and> h\<^isub>0 \<bottom> h\<^isub>2)"

   272   by (simp add: map_disj_def, fast)

   273 

   274 lemma map_add_disj':

   275   "(h\<^isub>1 ++ h\<^isub>2) \<bottom> h\<^isub>0 = (h\<^isub>1 \<bottom> h\<^isub>0 \<and> h\<^isub>2 \<bottom> h\<^isub>0)"

   276   by (simp add: map_disj_def, fast)

   277 

   278 text {*

   279   We redefine @{term "map_add"} associativity to bind to the right, which

   280   seems to be the more common case.

   281   Note that when a theory includes Map again, @{text "map_add_assoc"} will

   282   return to the simpset and will cause infinite loops if its symmetric

   283   counterpart is added (e.g. via @{text "map_add_ac"})

   284   *}

   285 

   286 declare map_add_assoc [simp del]

   287 

   288 text {*

   289   Since the associativity-commutativity of @{term "map_add"} relies on

   290   map disjunction, we include some basic rules into the ac set.

   291   *}

   292 

   293 lemmas map_add_ac =

   294   map_add_assoc[symmetric] map_add_com map_disj_com

   295   map_add_left_commute map_add_disj map_add_disj'

   296 

   297 

   298 subsection {* Basic properties *}

   299 

   300 lemma map_disj_None_right:

   301   "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; x \<in> dom h\<^isub>0 \<rbrakk> \<Longrightarrow> h\<^isub>1 x = None"

   302   by (auto simp: map_disj_def dom_def)

   303 

   304 lemma map_disj_None_left:

   305   "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; x \<in> dom h\<^isub>1 \<rbrakk> \<Longrightarrow> h\<^isub>0 x = None"

   306   by (auto simp: map_disj_def dom_def)

   307 

   308 lemma map_disj_None_left':

   309   "\<lbrakk> h\<^isub>0 x = Some y ; h\<^isub>1 \<bottom> h\<^isub>0 \<rbrakk> \<Longrightarrow> h\<^isub>1 x = None "

   310   by (auto simp: map_disj_def)

   311 

   312 lemma map_disj_None_right':

   313   "\<lbrakk> h\<^isub>1 x = Some y ; h\<^isub>1 \<bottom> h\<^isub>0 \<rbrakk> \<Longrightarrow> h\<^isub>0 x = None "

   314   by (auto simp: map_disj_def)

   315 

   316 lemma map_disj_common:

   317   "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; h\<^isub>0 p = Some v ; h\<^isub>1 p = Some v' \<rbrakk> \<Longrightarrow> False"

   318   by (frule (1) map_disj_None_left', simp)

   319 

   320 lemma map_disj_eq_dom_left:

   321   "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; dom h\<^isub>0' = dom h\<^isub>0 \<rbrakk> \<Longrightarrow> h\<^isub>0' \<bottom> h\<^isub>1"

   322   by (auto simp: map_disj_def)

   323 

   324 

   325 subsection {* Map disjunction and addition *}

   326 

   327 lemma map_add_eval_left:

   328   "\<lbrakk> x \<in> dom h ; h \<bottom> h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h x"

   329   by (auto dest!: map_disj_None_right simp: map_add_def cong: option.case_cong)

   330 

   331 lemma map_add_eval_right:

   332   "\<lbrakk> x \<in> dom h' ; h \<bottom> h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h' x"

   333   by (auto elim!: map_disjD simp: map_add_comm map_add_eval_left map_disj_com)

   334 

   335 lemma map_add_eval_left':

   336   "\<lbrakk> x \<notin> dom h' ; h \<bottom> h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h x"

   337   by (clarsimp simp: map_disj_def map_add_def split: option.splits)

   338 

   339 lemma map_add_eval_right':

   340   "\<lbrakk> x \<notin> dom h ; h \<bottom> h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h' x"

   341   by (clarsimp simp: map_disj_def map_add_def split: option.splits)

   342 

   343 lemma map_add_left_dom_eq:

   344   assumes eq: "h\<^isub>0 ++ h\<^isub>1 = h\<^isub>0' ++ h\<^isub>1'"

   345   assumes etc: "h\<^isub>0 \<bottom> h\<^isub>1" "h\<^isub>0' \<bottom> h\<^isub>1'" "dom h\<^isub>0 = dom h\<^isub>0'"

   346   shows "h\<^isub>0 = h\<^isub>0'"

   347 proof -

   348   from eq have "h\<^isub>1 ++ h\<^isub>0 = h\<^isub>1' ++ h\<^isub>0'" using etc by (simp add: map_add_ac)

   349   thus ?thesis using etc

   350     by (fastforce elim!: map_add_right_dom_eq simp: map_add_ac)

   351 qed

   352 

   353 lemma map_add_left_eq:

   354   assumes eq: "h\<^isub>0 ++ h = h\<^isub>1 ++ h"

   355   assumes disj: "h\<^isub>0 \<bottom> h" "h\<^isub>1 \<bottom> h"

   356   shows "h\<^isub>0 = h\<^isub>1"

   357 proof (rule ext)

   358   fix x

   359   from eq have eq': "(h\<^isub>0 ++ h) x = (h\<^isub>1 ++ h) x" by (auto intro!: ext)

   360   { assume "x \<in> dom h"

   361     hence "h\<^isub>0 x = h\<^isub>1 x" using disj by (simp add: map_disj_None_left)

   362   } moreover {

   363     assume "x \<notin> dom h"

   364     hence "h\<^isub>0 x = h\<^isub>1 x" using disj eq' by (simp add: map_add_eval_left')

   365   }

   366   ultimately show "h\<^isub>0 x = h\<^isub>1 x" by cases

   367 qed

   368 

   369 lemma map_add_right_eq:

   370   "\<lbrakk>h ++ h\<^isub>0 = h ++ h\<^isub>1; h\<^isub>0 \<bottom> h; h\<^isub>1 \<bottom> h\<rbrakk> \<Longrightarrow> h\<^isub>0 = h\<^isub>1"

   371   by (rule_tac h=h in map_add_left_eq, auto simp: map_add_ac)

   372 

   373 lemma map_disj_add_eq_dom_right_eq:

   374   assumes merge: "h\<^isub>0 ++ h\<^isub>1 = h\<^isub>0' ++ h\<^isub>1'" and d: "dom h\<^isub>0 = dom h\<^isub>0'" and

   375       ab_disj: "h\<^isub>0 \<bottom> h\<^isub>1" and cd_disj: "h\<^isub>0' \<bottom> h\<^isub>1'"

   376   shows "h\<^isub>1 = h\<^isub>1'"

   377 proof (rule ext)

   378   fix x

   379   from merge have merge_x: "(h\<^isub>0 ++ h\<^isub>1) x = (h\<^isub>0' ++ h\<^isub>1') x" by simp

   380   with d ab_disj cd_disj show  "h\<^isub>1 x = h\<^isub>1' x"

   381     by - (case_tac "h\<^isub>1 x", case_tac "h\<^isub>1' x", simp, fastforce simp: map_disj_def,

   382           case_tac "h\<^isub>1' x", clarsimp, simp add: Some_com,

   383           force simp: map_disj_def, simp)

   384 qed

   385 

   386 lemma map_disj_add_eq_dom_left_eq:

   387   assumes add: "h\<^isub>0 ++ h\<^isub>1 = h\<^isub>0' ++ h\<^isub>1'" and

   388           dom: "dom h\<^isub>1 = dom h\<^isub>1'" and

   389           disj: "h\<^isub>0 \<bottom> h\<^isub>1" "h\<^isub>0' \<bottom> h\<^isub>1'"

   390   shows "h\<^isub>0 = h\<^isub>0'"

   391 proof -

   392   have "h\<^isub>1 ++ h\<^isub>0 = h\<^isub>1' ++ h\<^isub>0'" using add disj by (simp add: map_add_ac)

   393   thus ?thesis using dom disj

   394     by - (rule map_disj_add_eq_dom_right_eq, auto simp: map_disj_com)

   395 qed

   396 

   397 lemma map_add_left_cancel:

   398   assumes disj: "h\<^isub>0 \<bottom> h\<^isub>1" "h\<^isub>0 \<bottom> h\<^isub>1'"

   399   shows "(h\<^isub>0 ++ h\<^isub>1 = h\<^isub>0 ++ h\<^isub>1') = (h\<^isub>1 = h\<^isub>1')"

   400 proof (rule iffI, rule ext)

   401   fix x

   402   assume "(h\<^isub>0 ++ h\<^isub>1) = (h\<^isub>0 ++ h\<^isub>1')"

   403   hence "(h\<^isub>0 ++ h\<^isub>1) x = (h\<^isub>0 ++ h\<^isub>1') x" by (auto intro!: ext)

   404   hence "h\<^isub>1 x = h\<^isub>1' x" using disj

   405     by - (cases "x \<in> dom h\<^isub>0",

   406           simp_all add: map_disj_None_right map_add_eval_right')

   407   thus "h\<^isub>1 x = h\<^isub>1' x" by (auto intro!: ext)

   408 qed auto

   409 

   410 lemma map_add_lr_disj:

   411   "\<lbrakk> h\<^isub>0 ++ h\<^isub>1 = h\<^isub>0' ++ h\<^isub>1'; h\<^isub>1 \<bottom> h\<^isub>1'  \<rbrakk> \<Longrightarrow> dom h\<^isub>1 \<subseteq> dom h\<^isub>0'"

   412   by (clarsimp simp: map_disj_def map_add_def, drule_tac x=x in fun_cong)

   413      (auto split: option.splits)

   414 

   415 

   416 subsection {* Map disjunction and map updates *}

   417 

   418 lemma map_disj_update_left [simp]:

   419   "p \<in> dom h\<^isub>1 \<Longrightarrow> h\<^isub>0 \<bottom> h\<^isub>1(p \<mapsto> v) = h\<^isub>0 \<bottom> h\<^isub>1"

   420   by (clarsimp simp add: map_disj_def, blast)

   421 

   422 lemma map_disj_update_right [simp]:

   423   "p \<in> dom h\<^isub>1 \<Longrightarrow> h\<^isub>1(p \<mapsto> v) \<bottom> h\<^isub>0 = h\<^isub>1 \<bottom> h\<^isub>0"

   424   by (simp add: map_disj_com)

   425 

   426 lemma map_add_update_left:

   427   "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; p \<in> dom h\<^isub>0 \<rbrakk> \<Longrightarrow> (h\<^isub>0 ++ h\<^isub>1)(p \<mapsto> v) = (h\<^isub>0(p \<mapsto> v) ++ h\<^isub>1)"

   428   by (drule (1) map_disj_None_right)

   429      (auto intro: ext simp: map_add_def cong: option.case_cong)

   430 

   431 lemma map_add_update_right:

   432   "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; p \<in> dom h\<^isub>1  \<rbrakk> \<Longrightarrow> (h\<^isub>0 ++ h\<^isub>1)(p \<mapsto> v) = (h\<^isub>0 ++ h\<^isub>1 (p \<mapsto> v))"

   433   by (drule (1) map_disj_None_left)

   434      (auto intro: ext simp: map_add_def cong: option.case_cong)

   435 

   436 lemma map_add3_update:

   437   "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; h\<^isub>1  \<bottom> h\<^isub>2 ; h\<^isub>0 \<bottom> h\<^isub>2 ; p \<in> dom h\<^isub>0 \<rbrakk>

   438   \<Longrightarrow> (h\<^isub>0 ++ h\<^isub>1 ++ h\<^isub>2)(p \<mapsto> v) = h\<^isub>0(p \<mapsto> v) ++ h\<^isub>1 ++ h\<^isub>2"

   439   by (auto simp: map_add_update_left[symmetric] map_add_ac)

   440 

   441 

   442 subsection {* Map disjunction and @{term "map_le"} *}

   443 

   444 lemma map_le_override [simp]:

   445   "\<lbrakk> h \<bottom> h' \<rbrakk> \<Longrightarrow> h \<subseteq>\<^sub>m h ++ h'"

   446   by (auto simp: map_le_def map_add_def map_disj_def split: option.splits)

   447 

   448 lemma map_leI_left:

   449   "\<lbrakk> h = h\<^isub>0 ++ h\<^isub>1 ; h\<^isub>0 \<bottom> h\<^isub>1 \<rbrakk> \<Longrightarrow> h\<^isub>0 \<subseteq>\<^sub>m h" by auto

   450 

   451 lemma map_leI_right:

   452   "\<lbrakk> h = h\<^isub>0 ++ h\<^isub>1 ; h\<^isub>0 \<bottom> h\<^isub>1 \<rbrakk> \<Longrightarrow> h\<^isub>1 \<subseteq>\<^sub>m h" by auto

   453 

   454 lemma map_disj_map_le:

   455   "\<lbrakk> h\<^isub>0' \<subseteq>\<^sub>m h\<^isub>0; h\<^isub>0 \<bottom> h\<^isub>1 \<rbrakk> \<Longrightarrow> h\<^isub>0' \<bottom> h\<^isub>1"

   456   by (force simp: map_disj_def map_le_def)

   457 

   458 lemma map_le_on_disj_left:

   459   "\<lbrakk> h' \<subseteq>\<^sub>m h ; h\<^isub>0 \<bottom> h\<^isub>1 ; h' = h\<^isub>0 ++ h\<^isub>1 \<rbrakk> \<Longrightarrow> h\<^isub>0 \<subseteq>\<^sub>m h"

   460   unfolding map_le_def

   461   by (rule ballI, erule_tac x=a in ballE, auto simp: map_add_eval_left)+

   462 

   463 lemma map_le_on_disj_right:

   464   "\<lbrakk> h' \<subseteq>\<^sub>m h ; h\<^isub>0 \<bottom> h\<^isub>1 ; h' = h\<^isub>1 ++ h\<^isub>0 \<rbrakk> \<Longrightarrow> h\<^isub>0 \<subseteq>\<^sub>m h"

   465   by (auto simp: map_le_on_disj_left map_add_ac)

   466 

   467 lemma map_le_add_cancel:

   468   "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1 ; h\<^isub>0' \<subseteq>\<^sub>m h\<^isub>0 \<rbrakk> \<Longrightarrow> h\<^isub>0' ++ h\<^isub>1 \<subseteq>\<^sub>m h\<^isub>0 ++ h\<^isub>1"

   469   by (auto simp: map_le_def map_add_def map_disj_def split: option.splits)

   470 

   471 lemma map_le_override_bothD:

   472   assumes subm: "h\<^isub>0' ++ h\<^isub>1 \<subseteq>\<^sub>m h\<^isub>0 ++ h\<^isub>1"

   473   assumes disj': "h\<^isub>0' \<bottom> h\<^isub>1"

   474   assumes disj: "h\<^isub>0 \<bottom> h\<^isub>1"

   475   shows "h\<^isub>0' \<subseteq>\<^sub>m h\<^isub>0"

   476 unfolding map_le_def

   477 proof (rule ballI)

   478   fix a

   479   assume a: "a \<in> dom h\<^isub>0'"

   480   hence sumeq: "(h\<^isub>0' ++ h\<^isub>1) a = (h\<^isub>0 ++ h\<^isub>1) a"

   481     using subm unfolding map_le_def by auto

   482   from a have "a \<notin> dom h\<^isub>1" using disj' by (auto dest!: map_disj_None_right)

   483   thus "h\<^isub>0' a = h\<^isub>0 a" using a sumeq disj disj'

   484     by (simp add: map_add_eval_left map_add_eval_left')

   485 qed

   486 

   487 lemma map_le_conv:

   488   "(h\<^isub>0' \<subseteq>\<^sub>m h\<^isub>0 \<and> h\<^isub>0' \<noteq> h\<^isub>0) = (\<exists>h\<^isub>1. h\<^isub>0 = h\<^isub>0' ++ h\<^isub>1 \<and> h\<^isub>0' \<bottom> h\<^isub>1 \<and> h\<^isub>0' \<noteq> h\<^isub>0)"

   489   unfolding map_le_def map_disj_def map_add_def

   490   by (rule iffI,

   491       clarsimp intro!: exI[where x="\<lambda>x. if x \<notin> dom h\<^isub>0' then h\<^isub>0 x else None"])

   492      (fastforce intro: ext intro: split: option.splits split_if_asm)+

   493 

   494 lemma map_le_conv2:

   495   "h\<^isub>0' \<subseteq>\<^sub>m h\<^isub>0 = (\<exists>h\<^isub>1. h\<^isub>0 = h\<^isub>0' ++ h\<^isub>1 \<and> h\<^isub>0' \<bottom> h\<^isub>1)"

   496   by (case_tac "h\<^isub>0'=h\<^isub>0", insert map_le_conv, auto intro: exI[where x=empty])

   497 

   498 

   499 subsection {* Map disjunction and restriction *}

   500 

   501 lemma map_disj_comp [simp]:

   502   "h\<^isub>0 \<bottom> h\<^isub>1 |` (UNIV - dom h\<^isub>0)"

   503   by (force simp: map_disj_def)

   504 

   505 lemma restrict_map_disj:

   506   "S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h |` T"

   507   by (auto simp: map_disj_def restrict_map_def dom_def)

   508 

   509 lemma map_disj_restrict_dom [simp]:

   510   "h\<^isub>0 \<bottom> h\<^isub>1 |` (dom h\<^isub>1 - dom h\<^isub>0)"

   511   by (force simp: map_disj_def)

   512 

   513 lemma restrict_map_disj_dom_empty:

   514   "h \<bottom> h' \<Longrightarrow> h |` dom h' = empty"

   515   by (fastforce simp: map_disj_def restrict_map_def intro: ext)

   516 

   517 lemma restrict_map_univ_disj_eq:

   518   "h \<bottom> h' \<Longrightarrow> h |` (UNIV - dom h') = h"

   519   by (rule ext, auto simp: map_disj_def restrict_map_def)

   520 

   521 lemma restrict_map_disj_dom:

   522   "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> h |` dom h\<^isub>0 \<bottom> h |` dom h\<^isub>1"

   523   by (auto simp: map_disj_def restrict_map_def dom_def)

   524 

   525 lemma map_add_restrict_dom_left:

   526   "h \<bottom> h' \<Longrightarrow> (h ++ h') |` dom h = h"

   527   by (rule ext, auto simp: restrict_map_def map_add_def dom_def map_disj_def

   528                      split: option.splits)

   529 

   530 lemma map_add_restrict_dom_left':

   531   "h \<bottom> h' \<Longrightarrow> S = dom h \<Longrightarrow> (h ++ h') |` S = h"

   532   by (rule ext, auto simp: restrict_map_def map_add_def dom_def map_disj_def

   533                      split: option.splits)

   534 

   535 lemma restrict_map_disj_left:

   536   "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> h\<^isub>0 |` S \<bottom> h\<^isub>1"

   537   by (auto simp: map_disj_def)

   538 

   539 lemma restrict_map_disj_right:

   540   "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> h\<^isub>0 \<bottom> h\<^isub>1 |` S"

   541   by (auto simp: map_disj_def)

   542 

   543 lemmas restrict_map_disj_both = restrict_map_disj_right restrict_map_disj_left

   544 

   545 lemma map_dom_disj_restrict_right:

   546   "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> (h\<^isub>0 ++ h\<^isub>0') |` dom h\<^isub>1 = h\<^isub>0' |` dom h\<^isub>1"

   547   by (simp add: map_add_restrict restrict_map_empty map_disj_def)

   548 

   549 lemma restrict_map_on_disj:

   550   "h\<^isub>0' \<bottom> h\<^isub>1 \<Longrightarrow> h\<^isub>0 |` dom h\<^isub>0' \<bottom> h\<^isub>1"

   551   unfolding map_disj_def by auto

   552 

   553 lemma restrict_map_on_disj':

   554   "h\<^isub>0 \<bottom> h\<^isub>1 \<Longrightarrow> h\<^isub>0 \<bottom> h\<^isub>1 |` S"

   555   by (auto simp: map_disj_def map_add_def)

   556 

   557 lemma map_le_sub_dom:

   558   "\<lbrakk> h\<^isub>0 ++ h\<^isub>1 \<subseteq>\<^sub>m h ; h\<^isub>0 \<bottom> h\<^isub>1 \<rbrakk> \<Longrightarrow> h\<^isub>0 \<subseteq>\<^sub>m h |` (dom h - dom h\<^isub>1)"

   559   by (rule map_le_override_bothD, subst map_le_dom_restrict_sub_add)

   560      (auto elim: map_add_le_mapE simp: map_add_ac)

   561 

   562 lemma map_submap_break:

   563   "\<lbrakk> h \<subseteq>\<^sub>m h' \<rbrakk> \<Longrightarrow> h' = (h' |` (UNIV - dom h)) ++ h"

   564   by (fastforce intro!: ext split: option.splits

   565                simp: map_le_restrict restrict_map_def map_le_def map_add_def

   566                      dom_def)

   567 

   568 lemma map_add_disj_restrict_both:

   569   "\<lbrakk> h\<^isub>0 \<bottom> h\<^isub>1; S \<inter> S' = {}; T \<inter> T' = {} \<rbrakk>

   570    \<Longrightarrow> (h\<^isub>0 |` S) ++ (h\<^isub>1 |` T) \<bottom> (h\<^isub>0 |` S') ++ (h\<^isub>1 |` T')"

   571   by (auto simp: map_add_ac intro!: restrict_map_disj_both restrict_map_disj)

   572 

   573 end