src/HOL/Map.thy
changeset 14025 d9b155757dc8
parent 13937 e9d57517c9b1
child 14026 c031a330a03f
     1.1 --- a/src/HOL/Map.thy	Tue May 13 08:59:21 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed May 14 10:22:09 2003 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  consts
     1.6  chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
     1.7 -override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
     1.8 +map_add:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
     1.9  dom	:: "('a ~=> 'b) => 'a set"
    1.10  ran	:: "('a ~=> 'b) => 'b set"
    1.11  map_of	:: "('a * 'b)list => 'a ~=> 'b"
    1.12 @@ -43,10 +43,12 @@
    1.13  defs
    1.14  chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    1.15  
    1.16 -override_def: "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    1.17 +map_add_def: "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    1.18 +
    1.19 +map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    1.20  
    1.21  dom_def: "dom(m) == {a. m a ~= None}"
    1.22 -ran_def: "ran(m) == {b. ? a. m a = Some b}"
    1.23 +ran_def: "ran(m) == {b. EX a. m a = Some b}"
    1.24  
    1.25  map_le_def: "m1 \<subseteq>\<^sub>m m2  ==  ALL a : dom m1. m1 a = m2 a"
    1.26  
    1.27 @@ -54,9 +56,6 @@
    1.28    "map_of [] = empty"
    1.29    "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    1.30  
    1.31 -primrec "t([]  [|->]bs) = t"
    1.32 -        "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
    1.33 -
    1.34  
    1.35  subsection {* empty *}
    1.36  
    1.37 @@ -116,27 +115,6 @@
    1.38  done
    1.39  
    1.40  
    1.41 -subsection {* map\_upds *}
    1.42 -
    1.43 -lemma map_upd_upds_conv_if:
    1.44 - "!!x y ys f. (f(x|->y))(xs [|->] ys) =
    1.45 -              (if x : set xs then f(xs [|->] ys) else (f(xs [|->] ys))(x|->y))"
    1.46 -apply(induct xs)
    1.47 - apply simp
    1.48 -apply(simp split:split_if add:fun_upd_twist eq_sym_conv)
    1.49 -done
    1.50 -
    1.51 -lemma map_upds_twist [simp]:
    1.52 - "a ~: set as ==> m(a|->b)(as[|->]bs) = m(as[|->]bs)(a|->b)"
    1.53 -by (simp add: map_upd_upds_conv_if)
    1.54 -
    1.55 -lemma map_upds_apply_nontin[simp]:
    1.56 - "!!ys. x ~: set xs ==> (f(xs[|->]ys)) x = f x"
    1.57 -apply(induct xs)
    1.58 - apply simp
    1.59 -apply(simp add: fun_upd_apply map_upd_upds_conv_if split:split_if)
    1.60 -done
    1.61 -
    1.62  subsection {* chg\_map *}
    1.63  
    1.64  lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
    1.65 @@ -207,45 +185,49 @@
    1.66  
    1.67  subsection {* ++ *}
    1.68  
    1.69 -lemma override_empty[simp]: "m ++ empty = m"
    1.70 -apply (unfold override_def)
    1.71 +lemma map_add_empty[simp]: "m ++ empty = m"
    1.72 +apply (unfold map_add_def)
    1.73  apply (simp (no_asm))
    1.74  done
    1.75  
    1.76 -lemma empty_override[simp]: "empty ++ m = m"
    1.77 -apply (unfold override_def)
    1.78 +lemma empty_map_add[simp]: "empty ++ m = m"
    1.79 +apply (unfold map_add_def)
    1.80  apply (rule ext)
    1.81  apply (simp split add: option.split)
    1.82  done
    1.83  
    1.84 -lemma override_Some_iff [rule_format (no_asm)]: 
    1.85 +lemma map_add_assoc[simp]: "m1 ++ (m2 ++ m3) = (m1 ++ m2) ++ m3"
    1.86 +apply(rule ext)
    1.87 +apply(simp add: map_add_def split:option.split)
    1.88 +done
    1.89 +
    1.90 +lemma map_add_Some_iff: 
    1.91   "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)"
    1.92 -apply (unfold override_def)
    1.93 +apply (unfold map_add_def)
    1.94  apply (simp (no_asm) split add: option.split)
    1.95  done
    1.96  
    1.97 -lemmas override_SomeD = override_Some_iff [THEN iffD1, standard]
    1.98 -declare override_SomeD [dest!]
    1.99 +lemmas map_add_SomeD = map_add_Some_iff [THEN iffD1, standard]
   1.100 +declare map_add_SomeD [dest!]
   1.101  
   1.102 -lemma override_find_right[simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
   1.103 -apply (subst override_Some_iff)
   1.104 +lemma map_add_find_right[simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
   1.105 +apply (subst map_add_Some_iff)
   1.106  apply fast
   1.107  done
   1.108  
   1.109 -lemma override_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
   1.110 -apply (unfold override_def)
   1.111 +lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
   1.112 +apply (unfold map_add_def)
   1.113  apply (simp (no_asm) split add: option.split)
   1.114  done
   1.115  
   1.116 -lemma override_upd[simp]: "f ++ g(x|->y) = (f ++ g)(x|->y)"
   1.117 -apply (unfold override_def)
   1.118 +lemma map_add_upd[simp]: "f ++ g(x|->y) = (f ++ g)(x|->y)"
   1.119 +apply (unfold map_add_def)
   1.120  apply (rule ext)
   1.121  apply auto
   1.122  done
   1.123  
   1.124 -lemma map_of_override[simp]: "map_of ys ++ map_of xs = map_of (xs@ys)"
   1.125 -apply (unfold override_def)
   1.126 -apply (rule sym)
   1.127 +lemma map_of_append[simp]: "map_of (xs@ys) = map_of ys ++ map_of xs"
   1.128 +apply (unfold map_add_def)
   1.129  apply (induct_tac "xs")
   1.130  apply (simp (no_asm))
   1.131  apply (rule ext)
   1.132 @@ -253,7 +235,8 @@
   1.133  done
   1.134  
   1.135  declare fun_upd_apply [simp del]
   1.136 -lemma finite_range_map_of_override: "finite (range f) ==> finite (range (f ++ map_of l))"
   1.137 +lemma finite_range_map_of_map_add:
   1.138 + "finite (range f) ==> finite (range (f ++ map_of l))"
   1.139  apply (induct_tac "l")
   1.140  apply  auto
   1.141  apply (erule finite_range_updI)
   1.142 @@ -261,6 +244,42 @@
   1.143  declare fun_upd_apply [simp]
   1.144  
   1.145  
   1.146 +subsection {* map\_upds *}
   1.147 +
   1.148 +lemma map_upds_Nil1[simp]: "m([] [|->] bs) = m"
   1.149 +by(simp add:map_upds_def)
   1.150 +
   1.151 +lemma map_upds_Nil2[simp]: "m(as [|->] []) = m"
   1.152 +by(simp add:map_upds_def)
   1.153 +
   1.154 +lemma map_upds_Cons[simp]: "m(a#as [|->] b#bs) = (m(a|->b))(as[|->]bs)"
   1.155 +by(simp add:map_upds_def)
   1.156 +
   1.157 +
   1.158 +lemma map_upd_upds_conv_if: "!!x y ys f.
   1.159 + (f(x|->y))(xs [|->] ys) =
   1.160 + (if x : set(take (length ys) xs) then f(xs [|->] ys)
   1.161 +                                  else (f(xs [|->] ys))(x|->y))"
   1.162 +apply(induct xs)
   1.163 + apply simp
   1.164 +apply(case_tac ys)
   1.165 + apply(auto split:split_if simp:fun_upd_twist)
   1.166 +done
   1.167 +
   1.168 +lemma map_upds_twist [simp]:
   1.169 + "a ~: set as ==> m(a|->b)(as[|->]bs) = m(as[|->]bs)(a|->b)"
   1.170 +apply(insert set_take_subset)
   1.171 +apply (fastsimp simp add: map_upd_upds_conv_if)
   1.172 +done
   1.173 +
   1.174 +lemma map_upds_apply_nontin[simp]:
   1.175 + "!!ys. x ~: set xs ==> (f(xs[|->]ys)) x = f x"
   1.176 +apply(induct xs)
   1.177 + apply simp
   1.178 +apply(case_tac ys)
   1.179 + apply(auto simp: map_upd_upds_conv_if)
   1.180 +done
   1.181 +
   1.182  subsection {* dom *}
   1.183  
   1.184  lemma domI: "m a = Some b ==> a : dom m"
   1.185 @@ -287,13 +306,6 @@
   1.186  lemma dom_fun_upd[simp]:
   1.187   "dom(f(x := y)) = (if y=None then dom f - {x} else insert x (dom f))"
   1.188  by (simp add:dom_def) blast
   1.189 -(*
   1.190 -lemma dom_map_upd[simp]: "dom(m(a|->b)) = insert a (dom m)"
   1.191 -apply (unfold dom_def)
   1.192 -apply (simp (no_asm))
   1.193 -apply blast
   1.194 -done
   1.195 -*)
   1.196  
   1.197  lemma dom_map_of: "dom(map_of xys) = {x. \<exists>y. (x,y) : set xys}"
   1.198  apply(induct xys)
   1.199 @@ -306,10 +318,15 @@
   1.200  apply (auto simp add: insert_Collect [symmetric])
   1.201  done
   1.202  
   1.203 -lemma dom_map_upds[simp]: "!!m vs. dom(m(xs[|->]vs)) = set xs Un dom m"
   1.204 -by(induct xs, simp_all)
   1.205 +lemma dom_map_upds[simp]:
   1.206 + "!!m ys. dom(m(xs[|->]ys)) = set(take (length ys) xs) Un dom m"
   1.207 +apply(induct xs)
   1.208 + apply simp
   1.209 +apply(case_tac ys)
   1.210 + apply auto
   1.211 +done
   1.212  
   1.213 -lemma dom_override[simp]: "dom(m++n) = dom n Un dom m"
   1.214 +lemma dom_map_add[simp]: "dom(m++n) = dom n Un dom m"
   1.215  apply (unfold dom_def)
   1.216  apply auto
   1.217  done
   1.218 @@ -342,6 +359,10 @@
   1.219  
   1.220  lemma map_le_upds[simp]:
   1.221   "!!f g bs. f \<subseteq>\<^sub>m g ==> f(as [|->] bs) \<subseteq>\<^sub>m g(as [|->] bs)"
   1.222 -by(induct as, auto)
   1.223 +apply(induct as)
   1.224 + apply simp
   1.225 +apply(case_tac bs)
   1.226 + apply auto
   1.227 +done
   1.228  
   1.229  end