src/HOL/Map.thy
author nipkow
Sun Apr 09 14:47:24 2006 +0200 (2006-04-09)
changeset 19378 6cc9ac729eb5
parent 19323 ec5cd5b1804c
child 19656 09be06943252
permissions -rw-r--r--
Made "empty" an abbreviation.
     1 (*  Title:      HOL/Map.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, based on a theory by David von Oheimb
     4     Copyright   1997-2003 TU Muenchen
     5 
     6 The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
     7 *)
     8 
     9 header {* Maps *}
    10 
    11 theory Map
    12 imports List
    13 begin
    14 
    15 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
    16 translations (type) "a ~=> b " <= (type) "a => b option"
    17 
    18 abbreviation
    19   empty     ::  "'a ~=> 'b"
    20   "empty == %x. None"
    21 
    22 constdefs
    23   map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
    24   "f o_m g  == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    25 
    26 consts
    27 map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    28 restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" (infixl "|`"  110)
    29 dom	:: "('a ~=> 'b) => 'a set"
    30 ran	:: "('a ~=> 'b) => 'b set"
    31 map_of	:: "('a * 'b)list => 'a ~=> 'b"
    32 map_upds:: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    33 map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
    34 
    35 nonterminals
    36   maplets maplet
    37 
    38 syntax
    39   "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
    40   "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
    41   ""         :: "maplet => maplets"             ("_")
    42   "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
    43   "_MapUpd"  :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
    44   "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
    45 
    46 syntax (xsymbols)
    47   "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
    48 
    49   map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "\<circ>\<^sub>m" 55)
    50 
    51   "_maplet"  :: "['a, 'a] => maplet"             ("_ /\<mapsto>/ _")
    52   "_maplets" :: "['a, 'a] => maplet"             ("_ /[\<mapsto>]/ _")
    53 
    54 syntax (latex output)
    55   restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
    56   --"requires amssymb!"
    57 
    58 translations
    59   "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
    60   "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
    61   "_MapUpd m (_maplets x y)"    == "map_upds m x y"
    62   "_Map ms"                     == "_MapUpd empty ms"
    63   "_Map (_Maplets ms1 ms2)"     <= "_MapUpd (_Map ms1) ms2"
    64   "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
    65 
    66 defs
    67 map_add_def:   "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    68 restrict_map_def: "m|`A == %x. if x : A then m x else None"
    69 
    70 map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    71 
    72 dom_def: "dom(m) == {a. m a ~= None}"
    73 ran_def: "ran(m) == {b. EX a. m a = Some b}"
    74 
    75 map_le_def: "m\<^isub>1 \<subseteq>\<^sub>m m\<^isub>2  ==  ALL a : dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a"
    76 
    77 primrec
    78   "map_of [] = empty"
    79   "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    80 
    81 (* special purpose constants that should be defined somewhere else and
    82 whose syntax is a bit odd as well:
    83 
    84  "@chg_map" :: "('a ~=> 'b) => 'a => ('b => 'b) => ('a ~=> 'b)"
    85 					  ("_/'(_/\<mapsto>\<lambda>_. _')"  [900,0,0,0] 900)
    86   "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
    87 
    88 map_upd_s::"('a ~=> 'b) => 'a set => 'b => 
    89 	    ('a ~=> 'b)"			 ("_/'(_{|->}_/')" [900,0,0]900)
    90 map_subst::"('a ~=> 'b) => 'b => 'b => 
    91 	    ('a ~=> 'b)"			 ("_/'(_~>_/')"    [900,0,0]900)
    92 
    93 map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"
    94 map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
    95 
    96   map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
    97 				    		 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
    98   map_subst :: "('a ~=> 'b) => 'b => 'b => 
    99 	        ('a ~=> 'b)"			 ("_/'(_\<leadsto>_/')"    [900,0,0]900)
   100 
   101 
   102 subsection {* @{term [source] map_upd_s} *}
   103 
   104 lemma map_upd_s_apply [simp]: 
   105   "(m(as{|->}b)) x = (if x : as then Some b else m x)"
   106 by (simp add: map_upd_s_def)
   107 
   108 lemma map_subst_apply [simp]: 
   109   "(m(a~>b)) x = (if m x = Some a then Some b else m x)" 
   110 by (simp add: map_subst_def)
   111 
   112 *)
   113 
   114 subsection {* @{term [source] empty} *}
   115 
   116 lemma empty_upd_none[simp]: "empty(x := None) = empty"
   117 apply (rule ext)
   118 apply (simp (no_asm))
   119 done
   120 
   121 
   122 (* FIXME: what is this sum_case nonsense?? *)
   123 lemma sum_case_empty_empty[simp]: "sum_case empty empty = empty"
   124 apply (rule ext)
   125 apply (simp (no_asm) split add: sum.split)
   126 done
   127 
   128 subsection {* @{term [source] map_upd} *}
   129 
   130 lemma map_upd_triv: "t k = Some x ==> t(k|->x) = t"
   131 apply (rule ext)
   132 apply (simp (no_asm_simp))
   133 done
   134 
   135 lemma map_upd_nonempty[simp]: "t(k|->x) ~= empty"
   136 apply safe
   137 apply (drule_tac x = k in fun_cong)
   138 apply (simp (no_asm_use))
   139 done
   140 
   141 lemma map_upd_eqD1: "m(a\<mapsto>x) = n(a\<mapsto>y) \<Longrightarrow> x = y"
   142 by (drule fun_cong [of _ _ a], auto)
   143 
   144 lemma map_upd_Some_unfold: 
   145   "((m(a|->b)) x = Some y) = (x = a \<and> b = y \<or> x \<noteq> a \<and> m x = Some y)"
   146 by auto
   147 
   148 lemma image_map_upd[simp]: "x \<notin> A \<Longrightarrow> m(x \<mapsto> y) ` A = m ` A"
   149 by fastsimp
   150 
   151 lemma finite_range_updI: "finite (range f) ==> finite (range (f(a|->b)))"
   152 apply (unfold image_def)
   153 apply (simp (no_asm_use) add: full_SetCompr_eq)
   154 apply (rule finite_subset)
   155 prefer 2 apply assumption
   156 apply auto
   157 done
   158 
   159 
   160 (* FIXME: what is this sum_case nonsense?? *)
   161 subsection {* @{term [source] sum_case} and @{term [source] empty}/@{term [source] map_upd} *}
   162 
   163 lemma sum_case_map_upd_empty[simp]:
   164  "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)"
   165 apply (rule ext)
   166 apply (simp (no_asm) split add: sum.split)
   167 done
   168 
   169 lemma sum_case_empty_map_upd[simp]:
   170  "sum_case empty (m(k|->y)) =  (sum_case empty m)(Inr k|->y)"
   171 apply (rule ext)
   172 apply (simp (no_asm) split add: sum.split)
   173 done
   174 
   175 lemma sum_case_map_upd_map_upd[simp]:
   176  "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)"
   177 apply (rule ext)
   178 apply (simp (no_asm) split add: sum.split)
   179 done
   180 
   181 
   182 subsection {* @{term [source] map_of} *}
   183 
   184 lemma map_of_eq_None_iff:
   185  "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
   186 by (induct xys) simp_all
   187 
   188 lemma map_of_is_SomeD:
   189  "map_of xys x = Some y \<Longrightarrow> (x,y) \<in> set xys"
   190 apply(induct xys)
   191  apply simp
   192 apply(clarsimp split:if_splits)
   193 done
   194 
   195 lemma map_of_eq_Some_iff[simp]:
   196  "distinct(map fst xys) \<Longrightarrow> (map_of xys x = Some y) = ((x,y) \<in> set xys)"
   197 apply(induct xys)
   198  apply(simp)
   199 apply(auto simp:map_of_eq_None_iff[symmetric])
   200 done
   201 
   202 lemma Some_eq_map_of_iff[simp]:
   203  "distinct(map fst xys) \<Longrightarrow> (Some y = map_of xys x) = ((x,y) \<in> set xys)"
   204 by(auto simp del:map_of_eq_Some_iff simp add:map_of_eq_Some_iff[symmetric])
   205 
   206 lemma map_of_is_SomeI [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
   207   \<Longrightarrow> map_of xys x = Some y"
   208 apply (induct xys)
   209  apply simp
   210 apply force
   211 done
   212 
   213 lemma map_of_zip_is_None[simp]:
   214   "length xs = length ys \<Longrightarrow> (map_of (zip xs ys) x = None) = (x \<notin> set xs)"
   215 by (induct rule:list_induct2, simp_all)
   216 
   217 lemma finite_range_map_of: "finite (range (map_of xys))"
   218 apply (induct xys)
   219 apply  (simp_all (no_asm) add: image_constant)
   220 apply (rule finite_subset)
   221 prefer 2 apply assumption
   222 apply auto
   223 done
   224 
   225 lemma map_of_SomeD [rule_format]: "map_of xs k = Some y --> (k,y):set xs"
   226 by (induct "xs", auto)
   227 
   228 lemma map_of_mapk_SomeI [rule_format]:
   229      "inj f ==> map_of t k = Some x -->  
   230         map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
   231 apply (induct "t")
   232 apply  (auto simp add: inj_eq)
   233 done
   234 
   235 lemma weak_map_of_SomeI [rule_format]:
   236      "(k, x) : set l --> (\<exists>x. map_of l k = Some x)"
   237 by (induct "l", auto)
   238 
   239 lemma map_of_filter_in: 
   240 "[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z"
   241 apply (rule mp)
   242 prefer 2 apply assumption
   243 apply (erule thin_rl)
   244 apply (induct "xs", auto)
   245 done
   246 
   247 lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
   248 by (induct "xs", auto)
   249 
   250 
   251 subsection {* @{term [source] option_map} related *}
   252 
   253 lemma option_map_o_empty[simp]: "option_map f o empty = empty"
   254 apply (rule ext)
   255 apply (simp (no_asm))
   256 done
   257 
   258 lemma option_map_o_map_upd[simp]:
   259  "option_map f o m(a|->b) = (option_map f o m)(a|->f b)"
   260 apply (rule ext)
   261 apply (simp (no_asm))
   262 done
   263 
   264 subsection {* @{term [source] map_comp} related *}
   265 
   266 lemma map_comp_empty [simp]: 
   267   "m \<circ>\<^sub>m empty = empty"
   268   "empty \<circ>\<^sub>m m = empty"
   269   by (auto simp add: map_comp_def intro: ext split: option.splits)
   270 
   271 lemma map_comp_simps [simp]: 
   272   "m2 k = None \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = None"
   273   "m2 k = Some k' \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = m1 k'" 
   274   by (auto simp add: map_comp_def)
   275 
   276 lemma map_comp_Some_iff:
   277   "((m1 \<circ>\<^sub>m m2) k = Some v) = (\<exists>k'. m2 k = Some k' \<and> m1 k' = Some v)" 
   278   by (auto simp add: map_comp_def split: option.splits)
   279 
   280 lemma map_comp_None_iff:
   281   "((m1 \<circ>\<^sub>m m2) k = None) = (m2 k = None \<or> (\<exists>k'. m2 k = Some k' \<and> m1 k' = None)) " 
   282   by (auto simp add: map_comp_def split: option.splits)
   283 
   284 subsection {* @{text "++"} *}
   285 
   286 lemma map_add_empty[simp]: "m ++ empty = m"
   287 apply (unfold map_add_def)
   288 apply (simp (no_asm))
   289 done
   290 
   291 lemma empty_map_add[simp]: "empty ++ m = m"
   292 apply (unfold map_add_def)
   293 apply (rule ext)
   294 apply (simp split add: option.split)
   295 done
   296 
   297 lemma map_add_assoc[simp]: "m1 ++ (m2 ++ m3) = (m1 ++ m2) ++ m3"
   298 apply(rule ext)
   299 apply(simp add: map_add_def split:option.split)
   300 done
   301 
   302 lemma map_add_Some_iff: 
   303  "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)"
   304 apply (unfold map_add_def)
   305 apply (simp (no_asm) split add: option.split)
   306 done
   307 
   308 lemmas map_add_SomeD = map_add_Some_iff [THEN iffD1, standard]
   309 declare map_add_SomeD [dest!]
   310 
   311 lemma map_add_find_right[simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
   312 by (subst map_add_Some_iff, fast)
   313 
   314 lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
   315 apply (unfold map_add_def)
   316 apply (simp (no_asm) split add: option.split)
   317 done
   318 
   319 lemma map_add_upd[simp]: "f ++ g(x|->y) = (f ++ g)(x|->y)"
   320 apply (unfold map_add_def)
   321 apply (rule ext, auto)
   322 done
   323 
   324 lemma map_add_upds[simp]: "m1 ++ (m2(xs[\<mapsto>]ys)) = (m1++m2)(xs[\<mapsto>]ys)"
   325 by(simp add:map_upds_def)
   326 
   327 lemma map_of_append[simp]: "map_of (xs@ys) = map_of ys ++ map_of xs"
   328 apply (unfold map_add_def)
   329 apply (induct "xs")
   330 apply (simp (no_asm))
   331 apply (rule ext)
   332 apply (simp (no_asm_simp) split add: option.split)
   333 done
   334 
   335 declare fun_upd_apply [simp del]
   336 lemma finite_range_map_of_map_add:
   337  "finite (range f) ==> finite (range (f ++ map_of l))"
   338 apply (induct "l", auto)
   339 apply (erule finite_range_updI)
   340 done
   341 declare fun_upd_apply [simp]
   342 
   343 lemma inj_on_map_add_dom[iff]:
   344  "inj_on (m ++ m') (dom m') = inj_on m' (dom m')"
   345 by(fastsimp simp add:map_add_def dom_def inj_on_def split:option.splits)
   346 
   347 subsection {* @{term [source] restrict_map} *}
   348 
   349 lemma restrict_map_to_empty[simp]: "m|`{} = empty"
   350 by(simp add: restrict_map_def)
   351 
   352 lemma restrict_map_empty[simp]: "empty|`D = empty"
   353 by(simp add: restrict_map_def)
   354 
   355 lemma restrict_in [simp]: "x \<in> A \<Longrightarrow> (m|`A) x = m x"
   356 by (auto simp: restrict_map_def)
   357 
   358 lemma restrict_out [simp]: "x \<notin> A \<Longrightarrow> (m|`A) x = None"
   359 by (auto simp: restrict_map_def)
   360 
   361 lemma ran_restrictD: "y \<in> ran (m|`A) \<Longrightarrow> \<exists>x\<in>A. m x = Some y"
   362 by (auto simp: restrict_map_def ran_def split: split_if_asm)
   363 
   364 lemma dom_restrict [simp]: "dom (m|`A) = dom m \<inter> A"
   365 by (auto simp: restrict_map_def dom_def split: split_if_asm)
   366 
   367 lemma restrict_upd_same [simp]: "m(x\<mapsto>y)|`(-{x}) = m|`(-{x})"
   368 by (rule ext, auto simp: restrict_map_def)
   369 
   370 lemma restrict_restrict [simp]: "m|`A|`B = m|`(A\<inter>B)"
   371 by (rule ext, auto simp: restrict_map_def)
   372 
   373 lemma restrict_fun_upd[simp]:
   374  "m(x := y)|`D = (if x \<in> D then (m|`(D-{x}))(x := y) else m|`D)"
   375 by(simp add: restrict_map_def expand_fun_eq)
   376 
   377 lemma fun_upd_None_restrict[simp]:
   378   "(m|`D)(x := None) = (if x:D then m|`(D - {x}) else m|`D)"
   379 by(simp add: restrict_map_def expand_fun_eq)
   380 
   381 lemma fun_upd_restrict:
   382  "(m|`D)(x := y) = (m|`(D-{x}))(x := y)"
   383 by(simp add: restrict_map_def expand_fun_eq)
   384 
   385 lemma fun_upd_restrict_conv[simp]:
   386  "x \<in> D \<Longrightarrow> (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
   387 by(simp add: restrict_map_def expand_fun_eq)
   388 
   389 
   390 subsection {* @{term [source] map_upds} *}
   391 
   392 lemma map_upds_Nil1[simp]: "m([] [|->] bs) = m"
   393 by(simp add:map_upds_def)
   394 
   395 lemma map_upds_Nil2[simp]: "m(as [|->] []) = m"
   396 by(simp add:map_upds_def)
   397 
   398 lemma map_upds_Cons[simp]: "m(a#as [|->] b#bs) = (m(a|->b))(as[|->]bs)"
   399 by(simp add:map_upds_def)
   400 
   401 lemma map_upds_append1[simp]: "\<And>ys m. size xs < size ys \<Longrightarrow>
   402   m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
   403 apply(induct xs)
   404  apply(clarsimp simp add:neq_Nil_conv)
   405 apply (case_tac ys, simp, simp)
   406 done
   407 
   408 lemma map_upds_list_update2_drop[simp]:
   409  "\<And>m ys i. \<lbrakk>size xs \<le> i; i < size ys\<rbrakk>
   410      \<Longrightarrow> m(xs[\<mapsto>]ys[i:=y]) = m(xs[\<mapsto>]ys)"
   411 apply (induct xs, simp)
   412 apply (case_tac ys, simp)
   413 apply(simp split:nat.split)
   414 done
   415 
   416 lemma map_upd_upds_conv_if: "!!x y ys f.
   417  (f(x|->y))(xs [|->] ys) =
   418  (if x : set(take (length ys) xs) then f(xs [|->] ys)
   419                                   else (f(xs [|->] ys))(x|->y))"
   420 apply (induct xs, simp)
   421 apply(case_tac ys)
   422  apply(auto split:split_if simp:fun_upd_twist)
   423 done
   424 
   425 lemma map_upds_twist [simp]:
   426  "a ~: set as ==> m(a|->b)(as[|->]bs) = m(as[|->]bs)(a|->b)"
   427 apply(insert set_take_subset)
   428 apply (fastsimp simp add: map_upd_upds_conv_if)
   429 done
   430 
   431 lemma map_upds_apply_nontin[simp]:
   432  "!!ys. x ~: set xs ==> (f(xs[|->]ys)) x = f x"
   433 apply (induct xs, simp)
   434 apply(case_tac ys)
   435  apply(auto simp: map_upd_upds_conv_if)
   436 done
   437 
   438 lemma fun_upds_append_drop[simp]:
   439   "!!m ys. size xs = size ys \<Longrightarrow> m(xs@zs[\<mapsto>]ys) = m(xs[\<mapsto>]ys)"
   440 apply(induct xs)
   441  apply (simp)
   442 apply(case_tac ys)
   443 apply simp_all
   444 done
   445 
   446 lemma fun_upds_append2_drop[simp]:
   447   "!!m ys. size xs = size ys \<Longrightarrow> m(xs[\<mapsto>]ys@zs) = m(xs[\<mapsto>]ys)"
   448 apply(induct xs)
   449  apply (simp)
   450 apply(case_tac ys)
   451 apply simp_all
   452 done
   453 
   454 
   455 lemma restrict_map_upds[simp]: "!!m ys.
   456  \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
   457  \<Longrightarrow> m(xs [\<mapsto>] ys)|`D = (m|`(D - set xs))(xs [\<mapsto>] ys)"
   458 apply (induct xs, simp)
   459 apply (case_tac ys, simp)
   460 apply(simp add:Diff_insert[symmetric] insert_absorb)
   461 apply(simp add: map_upd_upds_conv_if)
   462 done
   463 
   464 
   465 subsection {* @{term [source] dom} *}
   466 
   467 lemma domI: "m a = Some b ==> a : dom m"
   468 by (unfold dom_def, auto)
   469 (* declare domI [intro]? *)
   470 
   471 lemma domD: "a : dom m ==> \<exists>b. m a = Some b"
   472 apply (case_tac "m a") 
   473 apply (auto simp add: dom_def) 
   474 done
   475 
   476 lemma domIff[iff]: "(a : dom m) = (m a ~= None)"
   477 by (unfold dom_def, auto)
   478 declare domIff [simp del]
   479 
   480 lemma dom_empty[simp]: "dom empty = {}"
   481 apply (unfold dom_def)
   482 apply (simp (no_asm))
   483 done
   484 
   485 lemma dom_fun_upd[simp]:
   486  "dom(f(x := y)) = (if y=None then dom f - {x} else insert x (dom f))"
   487 by (simp add:dom_def) blast
   488 
   489 lemma dom_map_of: "dom(map_of xys) = {x. \<exists>y. (x,y) : set xys}"
   490 apply(induct xys)
   491 apply(auto simp del:fun_upd_apply)
   492 done
   493 
   494 lemma dom_map_of_conv_image_fst:
   495   "dom(map_of xys) = fst ` (set xys)"
   496 by(force simp: dom_map_of)
   497 
   498 lemma dom_map_of_zip[simp]: "[| length xs = length ys; distinct xs |] ==>
   499   dom(map_of(zip xs ys)) = set xs"
   500 by(induct rule: list_induct2, simp_all)
   501 
   502 lemma finite_dom_map_of: "finite (dom (map_of l))"
   503 apply (unfold dom_def)
   504 apply (induct "l")
   505 apply (auto simp add: insert_Collect [symmetric])
   506 done
   507 
   508 lemma dom_map_upds[simp]:
   509  "!!m ys. dom(m(xs[|->]ys)) = set(take (length ys) xs) Un dom m"
   510 apply (induct xs, simp)
   511 apply (case_tac ys, auto)
   512 done
   513 
   514 lemma dom_map_add[simp]: "dom(m++n) = dom n Un dom m"
   515 by (unfold dom_def, auto)
   516 
   517 lemma dom_override_on[simp]:
   518  "dom(override_on f g A) =
   519  (dom f  - {a. a : A - dom g}) Un {a. a : A Int dom g}"
   520 by(auto simp add: dom_def override_on_def)
   521 
   522 lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
   523 apply(rule ext)
   524 apply(force simp: map_add_def dom_def split:option.split) 
   525 done
   526 
   527 subsection {* @{term [source] ran} *}
   528 
   529 lemma ranI: "m a = Some b ==> b : ran m" 
   530 by (auto simp add: ran_def)
   531 (* declare ranI [intro]? *)
   532 
   533 lemma ran_empty[simp]: "ran empty = {}"
   534 apply (unfold ran_def)
   535 apply (simp (no_asm))
   536 done
   537 
   538 lemma ran_map_upd[simp]: "m a = None ==> ran(m(a|->b)) = insert b (ran m)"
   539 apply (unfold ran_def, auto)
   540 apply (subgoal_tac "~ (aa = a) ")
   541 apply auto
   542 done
   543 
   544 subsection {* @{text "map_le"} *}
   545 
   546 lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
   547 by(simp add:map_le_def)
   548 
   549 lemma upd_None_map_le [simp]: "f(x := None) \<subseteq>\<^sub>m f"
   550 by(force simp add:map_le_def)
   551 
   552 lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
   553 by(fastsimp simp add:map_le_def)
   554 
   555 lemma map_le_imp_upd_le [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
   556 by(force simp add:map_le_def)
   557 
   558 lemma map_le_upds[simp]:
   559  "!!f g bs. f \<subseteq>\<^sub>m g ==> f(as [|->] bs) \<subseteq>\<^sub>m g(as [|->] bs)"
   560 apply (induct as, simp)
   561 apply (case_tac bs, auto)
   562 done
   563 
   564 lemma map_le_implies_dom_le: "(f \<subseteq>\<^sub>m g) \<Longrightarrow> (dom f \<subseteq> dom g)"
   565   by (fastsimp simp add: map_le_def dom_def)
   566 
   567 lemma map_le_refl [simp]: "f \<subseteq>\<^sub>m f"
   568   by (simp add: map_le_def)
   569 
   570 lemma map_le_trans[trans]: "\<lbrakk> m1 \<subseteq>\<^sub>m m2; m2 \<subseteq>\<^sub>m m3\<rbrakk> \<Longrightarrow> m1 \<subseteq>\<^sub>m m3"
   571   by (auto simp add: map_le_def dom_def)
   572 
   573 lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
   574   apply (unfold map_le_def)
   575   apply (rule ext)
   576   apply (case_tac "x \<in> dom f", simp)
   577   apply (case_tac "x \<in> dom g", simp, fastsimp)
   578 done
   579 
   580 lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
   581   by (fastsimp simp add: map_le_def)
   582 
   583 lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
   584 by(fastsimp simp add:map_add_def map_le_def expand_fun_eq split:option.splits)
   585 
   586 lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
   587 by (fastsimp simp add: map_le_def map_add_def dom_def)
   588 
   589 lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h; f \<subseteq>\<^sub>m f++g \<rbrakk> \<Longrightarrow> f++g \<subseteq>\<^sub>m h"
   590 by (clarsimp simp add: map_le_def map_add_def dom_def split:option.splits)
   591 
   592 end