src/HOL/Map.thy
changeset 13910 f9a9ef16466f
parent 13909 a5247a49c85e
child 13912 3c0a340be514
     1.1 --- a/src/HOL/Map.thy	Mon Apr 14 13:51:31 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Mon Apr 14 18:52:13 2003 +0200
     1.3 @@ -17,11 +17,13 @@
     1.4  ran	:: "('a ~=> 'b) => 'b set"
     1.5  map_of	:: "('a * 'b)list => 'a ~=> 'b"
     1.6  map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
     1.7 -	    ('a ~=> 'b)"			 ("_/'(_[|->]_/')" [900,0,0]900)
     1.8 +	    ('a ~=> 'b)"		 ("_/'(_[|->]_/')" [900,0,0]900)
     1.9 +map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
    1.10 +
    1.11  syntax
    1.12  empty	::  "'a ~=> 'b"
    1.13  map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    1.14 -					         ("_/'(_/|->_')"   [900,0,0]900)
    1.15 +					 ("_/'(_/|->_')"   [900,0,0]900)
    1.16  
    1.17  syntax (xsymbols)
    1.18    "~=>"     :: "[type, type] => type"    (infixr "\<leadsto>" 0)
    1.19 @@ -37,7 +39,6 @@
    1.20    "m(a|->b)" == "m(a:=Some b)"
    1.21  
    1.22  defs
    1.23 -
    1.24  chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    1.25  
    1.26  override_def: "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    1.27 @@ -45,6 +46,8 @@
    1.28  dom_def: "dom(m) == {a. m a ~= None}"
    1.29  ran_def: "ran(m) == {b. ? a. m a = Some b}"
    1.30  
    1.31 +map_le_def: "m1 \<subseteq>\<^sub>m m2  ==  ALL a : dom m1. m1 a = m2 a"
    1.32 +
    1.33  primrec
    1.34    "map_of [] = empty"
    1.35    "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    1.36 @@ -55,19 +58,17 @@
    1.37  
    1.38  section {* empty *}
    1.39  
    1.40 -lemma empty_upd_none: "empty(x := None) = empty"
    1.41 +lemma empty_upd_none[simp]: "empty(x := None) = empty"
    1.42  apply (rule ext)
    1.43  apply (simp (no_asm))
    1.44  done
    1.45 -declare empty_upd_none [simp]
    1.46 +
    1.47  
    1.48  (* FIXME: what is this sum_case nonsense?? *)
    1.49 -lemma sum_case_empty_empty: "sum_case empty empty = empty"
    1.50 +lemma sum_case_empty_empty[simp]: "sum_case empty empty = empty"
    1.51  apply (rule ext)
    1.52  apply (simp (no_asm) split add: sum.split)
    1.53  done
    1.54 -declare sum_case_empty_empty [simp]
    1.55 -
    1.56  
    1.57  section {* map\_upd *}
    1.58  
    1.59 @@ -76,12 +77,11 @@
    1.60  apply (simp (no_asm_simp))
    1.61  done
    1.62  
    1.63 -lemma map_upd_nonempty: "t(k|->x) ~= empty"
    1.64 +lemma map_upd_nonempty[simp]: "t(k|->x) ~= empty"
    1.65  apply safe
    1.66  apply (drule_tac x = "k" in fun_cong)
    1.67  apply (simp (no_asm_use))
    1.68  done
    1.69 -declare map_upd_nonempty [simp]
    1.70  
    1.71  lemma finite_range_updI: "finite (range f) ==> finite (range (f(a|->b)))"
    1.72  apply (unfold image_def)
    1.73 @@ -95,53 +95,58 @@
    1.74  (* FIXME: what is this sum_case nonsense?? *)
    1.75  section {* sum\_case and empty/map\_upd *}
    1.76  
    1.77 -lemma sum_case_map_upd_empty: "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)"
    1.78 +lemma sum_case_map_upd_empty[simp]:
    1.79 + "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)"
    1.80  apply (rule ext)
    1.81  apply (simp (no_asm) split add: sum.split)
    1.82  done
    1.83 -declare sum_case_map_upd_empty [simp]
    1.84  
    1.85 -lemma sum_case_empty_map_upd: "sum_case empty (m(k|->y)) =  (sum_case empty m)(Inr k|->y)"
    1.86 +lemma sum_case_empty_map_upd[simp]:
    1.87 + "sum_case empty (m(k|->y)) =  (sum_case empty m)(Inr k|->y)"
    1.88  apply (rule ext)
    1.89  apply (simp (no_asm) split add: sum.split)
    1.90  done
    1.91 -declare sum_case_empty_map_upd [simp]
    1.92  
    1.93 -lemma sum_case_map_upd_map_upd: "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)"
    1.94 +lemma sum_case_map_upd_map_upd[simp]:
    1.95 + "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)"
    1.96  apply (rule ext)
    1.97  apply (simp (no_asm) split add: sum.split)
    1.98  done
    1.99 -declare sum_case_map_upd_map_upd [simp]
   1.100  
   1.101  
   1.102  section {* map\_upds *}
   1.103  
   1.104 -lemma map_upds_twist [rule_format (no_asm)]: "a ~: set as --> (!m bs. (m(a|->b)(as[|->]bs)) = (m(as[|->]bs)(a|->b)))"
   1.105 -apply (induct_tac "as")
   1.106 -apply  (auto simp del: fun_upd_apply)
   1.107 -apply (drule spec)+
   1.108 -apply (rotate_tac -1)
   1.109 -apply (erule subst)
   1.110 -apply (erule fun_upd_twist [THEN subst])
   1.111 -apply (rule refl)
   1.112 +lemma map_upd_upds_conv_if:
   1.113 + "!!x y ys f. (f(x|->y))(xs [|->] ys) =
   1.114 +              (if x : set xs then f(xs [|->] ys) else (f(xs [|->] ys))(x|->y))"
   1.115 +apply(induct xs)
   1.116 + apply simp
   1.117 +apply(simp split:split_if add:fun_upd_twist eq_sym_conv)
   1.118  done
   1.119 -declare map_upds_twist [simp]
   1.120 +
   1.121 +lemma map_upds_twist [simp]:
   1.122 + "a ~: set as ==> m(a|->b)(as[|->]bs) = m(as[|->]bs)(a|->b)"
   1.123 +by (simp add: map_upd_upds_conv_if)
   1.124  
   1.125 +lemma map_upds_apply_nontin[simp]:
   1.126 + "!!ys. x ~: set xs ==> (f(xs[|->]ys)) x = f x"
   1.127 +apply(induct xs)
   1.128 + apply simp
   1.129 +apply(simp add: fun_upd_apply map_upd_upds_conv_if split:split_if)
   1.130 +done
   1.131  
   1.132  section {* chg\_map *}
   1.133  
   1.134 -lemma chg_map_new: "m a = None   ==> chg_map f a m = m"
   1.135 +lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
   1.136  apply (unfold chg_map_def)
   1.137  apply auto
   1.138  done
   1.139  
   1.140 -lemma chg_map_upd: "m a = Some b ==> chg_map f a m = m(a|->f b)"
   1.141 +lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
   1.142  apply (unfold chg_map_def)
   1.143  apply auto
   1.144  done
   1.145  
   1.146 -declare chg_map_new [simp] chg_map_upd [simp]
   1.147 -
   1.148  
   1.149  section {* map\_of *}
   1.150  
   1.151 @@ -186,33 +191,30 @@
   1.152  
   1.153  section {* option\_map related *}
   1.154  
   1.155 -lemma option_map_o_empty: "option_map f o empty = empty"
   1.156 +lemma option_map_o_empty[simp]: "option_map f o empty = empty"
   1.157  apply (rule ext)
   1.158  apply (simp (no_asm))
   1.159  done
   1.160  
   1.161 -lemma option_map_o_map_upd: "option_map f o m(a|->b) = (option_map f o m)(a|->f b)"
   1.162 +lemma option_map_o_map_upd[simp]:
   1.163 + "option_map f o m(a|->b) = (option_map f o m)(a|->f b)"
   1.164  apply (rule ext)
   1.165  apply (simp (no_asm))
   1.166  done
   1.167  
   1.168 -declare option_map_o_empty [simp] option_map_o_map_upd [simp]
   1.169 -
   1.170  
   1.171  section {* ++ *}
   1.172  
   1.173 -lemma override_empty: "m ++ empty = m"
   1.174 +lemma override_empty[simp]: "m ++ empty = m"
   1.175  apply (unfold override_def)
   1.176  apply (simp (no_asm))
   1.177  done
   1.178 -declare override_empty [simp]
   1.179  
   1.180 -lemma empty_override: "empty ++ m = m"
   1.181 +lemma empty_override[simp]: "empty ++ m = m"
   1.182  apply (unfold override_def)
   1.183  apply (rule ext)
   1.184  apply (simp split add: option.split)
   1.185  done
   1.186 -declare empty_override [simp]
   1.187  
   1.188  lemma override_Some_iff [rule_format (no_asm)]: 
   1.189   "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)"
   1.190 @@ -223,26 +225,23 @@
   1.191  lemmas override_SomeD = override_Some_iff [THEN iffD1, standard]
   1.192  declare override_SomeD [dest!]
   1.193  
   1.194 -lemma override_find_right: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
   1.195 +lemma override_find_right[simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
   1.196  apply (subst override_Some_iff)
   1.197  apply fast
   1.198  done
   1.199 -declare override_find_right [simp]
   1.200  
   1.201 -lemma override_None: "((m ++ n) k = None) = (n k = None & m k = None)"
   1.202 +lemma override_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
   1.203  apply (unfold override_def)
   1.204  apply (simp (no_asm) split add: option.split)
   1.205  done
   1.206 -declare override_None [iff]
   1.207  
   1.208 -lemma override_upd: "f ++ g(x|->y) = (f ++ g)(x|->y)"
   1.209 +lemma override_upd[simp]: "f ++ g(x|->y) = (f ++ g)(x|->y)"
   1.210  apply (unfold override_def)
   1.211  apply (rule ext)
   1.212  apply auto
   1.213  done
   1.214 -declare override_upd [simp]
   1.215  
   1.216 -lemma map_of_override: "map_of ys ++ map_of xs = map_of (xs@ys)"
   1.217 +lemma map_of_override[simp]: "map_of ys ++ map_of xs = map_of (xs@ys)"
   1.218  apply (unfold override_def)
   1.219  apply (rule sym)
   1.220  apply (induct_tac "xs")
   1.221 @@ -250,7 +249,6 @@
   1.222  apply (rule ext)
   1.223  apply (simp (no_asm_simp) split add: option.split)
   1.224  done
   1.225 -declare map_of_override [simp]
   1.226  
   1.227  declare fun_upd_apply [simp del]
   1.228  lemma finite_range_map_of_override: "finite (range f) ==> finite (range (f ++ map_of l))"
   1.229 @@ -273,25 +271,27 @@
   1.230  apply auto
   1.231  done
   1.232  
   1.233 -lemma domIff: "(a : dom m) = (m a ~= None)"
   1.234 +lemma domIff[iff]: "(a : dom m) = (m a ~= None)"
   1.235  apply (unfold dom_def)
   1.236  apply auto
   1.237  done
   1.238 -declare domIff [iff]
   1.239  declare domIff [simp del]
   1.240  
   1.241 -lemma dom_empty: "dom empty = {}"
   1.242 +lemma dom_empty[simp]: "dom empty = {}"
   1.243  apply (unfold dom_def)
   1.244  apply (simp (no_asm))
   1.245  done
   1.246 -declare dom_empty [simp]
   1.247  
   1.248 -lemma dom_map_upd: "dom(m(a|->b)) = insert a (dom m)"
   1.249 +lemma dom_fun_upd[simp]:
   1.250 + "dom(f(x := y)) = (if y=None then dom f - {x} else insert x (dom f))"
   1.251 +by (simp add:dom_def) blast
   1.252 +(*
   1.253 +lemma dom_map_upd[simp]: "dom(m(a|->b)) = insert a (dom m)"
   1.254  apply (unfold dom_def)
   1.255  apply (simp (no_asm))
   1.256  apply blast
   1.257  done
   1.258 -declare dom_map_upd [simp]
   1.259 +*)
   1.260  
   1.261  lemma finite_dom_map_of: "finite (dom (map_of l))"
   1.262  apply (unfold dom_def)
   1.263 @@ -299,32 +299,42 @@
   1.264  apply (auto simp add: insert_Collect [symmetric])
   1.265  done
   1.266  
   1.267 -lemma dom_override: "dom(m++n) = dom n Un dom m"
   1.268 +lemma dom_map_upds[simp]: "!!m vs. dom(m(xs[|->]vs)) = set xs Un dom m"
   1.269 +by(induct xs, simp_all)
   1.270 +
   1.271 +lemma dom_override[simp]: "dom(m++n) = dom n Un dom m"
   1.272  apply (unfold dom_def)
   1.273  apply auto
   1.274  done
   1.275 -declare dom_override [simp]
   1.276 +
   1.277 +lemma dom_overwrite[simp]:
   1.278 + "dom(f(g|A)) = (dom f  - {a. a : A - dom g}) Un {a. a : A Int dom g}"
   1.279 +by(auto simp add: dom_def overwrite_def)
   1.280  
   1.281  section {* ran *}
   1.282  
   1.283 -lemma ran_empty: "ran empty = {}"
   1.284 +lemma ran_empty[simp]: "ran empty = {}"
   1.285  apply (unfold ran_def)
   1.286  apply (simp (no_asm))
   1.287  done
   1.288 -declare ran_empty [simp]
   1.289  
   1.290 -lemma ran_empty': "ran (%u. None) = {}"
   1.291 -apply (unfold ran_def)
   1.292 -apply auto
   1.293 -done
   1.294 -declare ran_empty' [simp]
   1.295 -
   1.296 -lemma ran_map_upd: "m a = None ==> ran(m(a|->b)) = insert b (ran m)"
   1.297 +lemma ran_map_upd[simp]: "m a = None ==> ran(m(a|->b)) = insert b (ran m)"
   1.298  apply (unfold ran_def)
   1.299  apply auto
   1.300  apply (subgoal_tac "~ (aa = a) ")
   1.301  apply auto
   1.302  done
   1.303 -declare ran_map_upd [simp]
   1.304 +
   1.305 +section{* @{text"\<subseteq>\<^sub>m"} *}
   1.306 +
   1.307 +lemma [simp]: "empty \<subseteq>\<^sub>m g"
   1.308 +by(simp add:map_le_def)
   1.309 +
   1.310 +lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
   1.311 +by(fastsimp simp add:map_le_def)
   1.312 +
   1.313 +lemma map_le_upds[simp]:
   1.314 + "!!f g bs. f \<subseteq>\<^sub>m g ==> f(as [|->] bs) \<subseteq>\<^sub>m g(as [|->] bs)"
   1.315 +by(induct as, auto)
   1.316  
   1.317  end