src/HOL/Map.thy
changeset 14186 6d2a494e33be
parent 14180 d2e550609c40
child 14187 26dfcd0ac436
     1.1 --- a/src/HOL/Map.thy	Thu Sep 04 19:39:52 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Thu Sep 11 22:33:12 2003 +0200
     1.3 @@ -264,6 +264,9 @@
     1.4  apply auto
     1.5  done
     1.6  
     1.7 +lemma map_add_upds[simp]: "m1 ++ (m2(xs[\<mapsto>]ys)) = (m1++m2)(xs[\<mapsto>]ys)"
     1.8 +by(simp add:map_upds_def)
     1.9 +
    1.10  lemma map_of_append[simp]: "map_of (xs@ys) = map_of ys ++ map_of xs"
    1.11  apply (unfold map_add_def)
    1.12  apply (induct_tac "xs")
    1.13 @@ -292,6 +295,12 @@
    1.14  
    1.15  subsection {* @{term restrict_map} *}
    1.16  
    1.17 +lemma restrict_map_to_empty[simp]: "m\<lfloor>{} = empty"
    1.18 +by(simp add: restrict_map_def)
    1.19 +
    1.20 +lemma restrict_map_empty[simp]: "empty\<lfloor>D = empty"
    1.21 +by(simp add: restrict_map_def)
    1.22 +
    1.23  lemma restrict_in [simp]: "x \<in> A \<Longrightarrow> (m\<lfloor>A) x = m x"
    1.24  by (auto simp: restrict_map_def)
    1.25  
    1.26 @@ -301,7 +310,7 @@
    1.27  lemma ran_restrictD: "y \<in> ran (m\<lfloor>A) \<Longrightarrow> \<exists>x\<in>A. m x = Some y"
    1.28  by (auto simp: restrict_map_def ran_def split: split_if_asm)
    1.29  
    1.30 -lemma dom_valF_restrict [simp]: "dom (m\<lfloor>A) = dom m \<inter> A"
    1.31 +lemma dom_restrict [simp]: "dom (m\<lfloor>A) = dom m \<inter> A"
    1.32  by (auto simp: restrict_map_def dom_def split: split_if_asm)
    1.33  
    1.34  lemma restrict_upd_same [simp]: "m(x\<mapsto>y)\<lfloor>(-{x}) = m\<lfloor>(-{x})"
    1.35 @@ -310,6 +319,22 @@
    1.36  lemma restrict_restrict [simp]: "m\<lfloor>A\<lfloor>B = m\<lfloor>(A\<inter>B)"
    1.37  by (rule ext, auto simp: restrict_map_def)
    1.38  
    1.39 +lemma restrict_fun_upd[simp]:
    1.40 + "m(x := y)\<lfloor>D = (if x \<in> D then (m\<lfloor>(D-{x}))(x := y) else m\<lfloor>D)"
    1.41 +by(simp add: restrict_map_def expand_fun_eq)
    1.42 +
    1.43 +lemma fun_upd_None_restrict[simp]:
    1.44 +  "(m\<lfloor>D)(x := None) = (if x:D then m\<lfloor>(D - {x}) else m\<lfloor>D)"
    1.45 +by(simp add: restrict_map_def expand_fun_eq)
    1.46 +
    1.47 +lemma fun_upd_restrict:
    1.48 + "(m\<lfloor>D)(x := y) = (m\<lfloor>(D-{x}))(x := y)"
    1.49 +by(simp add: restrict_map_def expand_fun_eq)
    1.50 +
    1.51 +lemma fun_upd_restrict_conv[simp]:
    1.52 + "x \<in> D \<Longrightarrow> (m\<lfloor>D)(x := y) = (m\<lfloor>(D-{x}))(x := y)"
    1.53 +by(simp add: restrict_map_def expand_fun_eq)
    1.54 +
    1.55  
    1.56  subsection {* @{term map_upds} *}
    1.57  
    1.58 @@ -347,6 +372,18 @@
    1.59   apply(auto simp: map_upd_upds_conv_if)
    1.60  done
    1.61  
    1.62 +lemma restrict_map_upds[simp]: "!!m ys.
    1.63 + \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
    1.64 + \<Longrightarrow> m(xs [\<mapsto>] ys)\<lfloor>D = (m\<lfloor>(D - set xs))(xs [\<mapsto>] ys)"
    1.65 +apply(induct xs)
    1.66 + apply simp
    1.67 +apply(case_tac ys)
    1.68 + apply simp
    1.69 +apply(simp add:Diff_insert[symmetric] insert_absorb)
    1.70 +apply(simp add: map_upd_upds_conv_if)
    1.71 +done
    1.72 +
    1.73 +
    1.74  subsection {* @{term map_upd_s} *}
    1.75  
    1.76  lemma map_upd_s_apply [simp]: