Added thms
authornipkow
Mon Apr 14 18:52:13 2003 +0200 (2003-04-14)
changeset 13910f9a9ef16466f
parent 13909 a5247a49c85e
child 13911 f5c3750292f5
Added thms
src/HOL/Fun.thy
src/HOL/Map.thy
     1.1 --- a/src/HOL/Fun.thy	Mon Apr 14 13:51:31 2003 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Apr 14 18:52:13 2003 +0200
     1.3 @@ -37,11 +37,15 @@
     1.4  *)
     1.5  
     1.6  constdefs
     1.7 -  id :: "'a => 'a"
     1.8 -    "id == %x. x"
     1.9 + overwrite :: "('a => 'b) => ('a => 'b) => 'a set => ('a => 'b)"
    1.10 +              ("_/'(_|/_')"  [900,0,0]900)
    1.11 +"f(g|A) == %a. if a : A then g a else f a"
    1.12  
    1.13 -  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
    1.14 -    "f o g == %x. f(g(x))"
    1.15 + id :: "'a => 'a"
    1.16 +"id == %x. x"
    1.17 +
    1.18 + comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
    1.19 +"f o g == %x. f(g(x))"
    1.20  
    1.21  text{*compatibility*}
    1.22  lemmas o_def = comp_def
    1.23 @@ -335,6 +339,17 @@
    1.24  lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"
    1.25  by (rule ext, auto)
    1.26  
    1.27 +subsection{* overwrite *}
    1.28 +
    1.29 +lemma overwrite_emptyset[simp]: "f(g|{}) = f"
    1.30 +by(simp add:overwrite_def)
    1.31 +
    1.32 +lemma overwrite_apply_notin[simp]: "a ~: A ==> (f(g|A)) a = f a"
    1.33 +by(simp add:overwrite_def)
    1.34 +
    1.35 +lemma overwrite_apply_in[simp]: "a : A ==> (f(g|A)) a = g a"
    1.36 +by(simp add:overwrite_def)
    1.37 +
    1.38  text{*The ML section includes some compatibility bindings and a simproc
    1.39  for function updates, in addition to the usual ML-bindings of theorems.*}
    1.40  ML
     2.1 --- a/src/HOL/Map.thy	Mon Apr 14 13:51:31 2003 +0200
     2.2 +++ b/src/HOL/Map.thy	Mon Apr 14 18:52:13 2003 +0200
     2.3 @@ -17,11 +17,13 @@
     2.4  ran	:: "('a ~=> 'b) => 'b set"
     2.5  map_of	:: "('a * 'b)list => 'a ~=> 'b"
     2.6  map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
     2.7 -	    ('a ~=> 'b)"			 ("_/'(_[|->]_/')" [900,0,0]900)
     2.8 +	    ('a ~=> 'b)"		 ("_/'(_[|->]_/')" [900,0,0]900)
     2.9 +map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
    2.10 +
    2.11  syntax
    2.12  empty	::  "'a ~=> 'b"
    2.13  map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    2.14 -					         ("_/'(_/|->_')"   [900,0,0]900)
    2.15 +					 ("_/'(_/|->_')"   [900,0,0]900)
    2.16  
    2.17  syntax (xsymbols)
    2.18    "~=>"     :: "[type, type] => type"    (infixr "\<leadsto>" 0)
    2.19 @@ -37,7 +39,6 @@
    2.20    "m(a|->b)" == "m(a:=Some b)"
    2.21  
    2.22  defs
    2.23 -
    2.24  chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    2.25  
    2.26  override_def: "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    2.27 @@ -45,6 +46,8 @@
    2.28  dom_def: "dom(m) == {a. m a ~= None}"
    2.29  ran_def: "ran(m) == {b. ? a. m a = Some b}"
    2.30  
    2.31 +map_le_def: "m1 \<subseteq>\<^sub>m m2  ==  ALL a : dom m1. m1 a = m2 a"
    2.32 +
    2.33  primrec
    2.34    "map_of [] = empty"
    2.35    "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    2.36 @@ -55,19 +58,17 @@
    2.37  
    2.38  section {* empty *}
    2.39  
    2.40 -lemma empty_upd_none: "empty(x := None) = empty"
    2.41 +lemma empty_upd_none[simp]: "empty(x := None) = empty"
    2.42  apply (rule ext)
    2.43  apply (simp (no_asm))
    2.44  done
    2.45 -declare empty_upd_none [simp]
    2.46 +
    2.47  
    2.48  (* FIXME: what is this sum_case nonsense?? *)
    2.49 -lemma sum_case_empty_empty: "sum_case empty empty = empty"
    2.50 +lemma sum_case_empty_empty[simp]: "sum_case empty empty = empty"
    2.51  apply (rule ext)
    2.52  apply (simp (no_asm) split add: sum.split)
    2.53  done
    2.54 -declare sum_case_empty_empty [simp]
    2.55 -
    2.56  
    2.57  section {* map\_upd *}
    2.58  
    2.59 @@ -76,12 +77,11 @@
    2.60  apply (simp (no_asm_simp))
    2.61  done
    2.62  
    2.63 -lemma map_upd_nonempty: "t(k|->x) ~= empty"
    2.64 +lemma map_upd_nonempty[simp]: "t(k|->x) ~= empty"
    2.65  apply safe
    2.66  apply (drule_tac x = "k" in fun_cong)
    2.67  apply (simp (no_asm_use))
    2.68  done
    2.69 -declare map_upd_nonempty [simp]
    2.70  
    2.71  lemma finite_range_updI: "finite (range f) ==> finite (range (f(a|->b)))"
    2.72  apply (unfold image_def)
    2.73 @@ -95,53 +95,58 @@
    2.74  (* FIXME: what is this sum_case nonsense?? *)
    2.75  section {* sum\_case and empty/map\_upd *}
    2.76  
    2.77 -lemma sum_case_map_upd_empty: "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)"
    2.78 +lemma sum_case_map_upd_empty[simp]:
    2.79 + "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)"
    2.80  apply (rule ext)
    2.81  apply (simp (no_asm) split add: sum.split)
    2.82  done
    2.83 -declare sum_case_map_upd_empty [simp]
    2.84  
    2.85 -lemma sum_case_empty_map_upd: "sum_case empty (m(k|->y)) =  (sum_case empty m)(Inr k|->y)"
    2.86 +lemma sum_case_empty_map_upd[simp]:
    2.87 + "sum_case empty (m(k|->y)) =  (sum_case empty m)(Inr k|->y)"
    2.88  apply (rule ext)
    2.89  apply (simp (no_asm) split add: sum.split)
    2.90  done
    2.91 -declare sum_case_empty_map_upd [simp]
    2.92  
    2.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)"
    2.94 +lemma sum_case_map_upd_map_upd[simp]:
    2.95 + "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)"
    2.96  apply (rule ext)
    2.97  apply (simp (no_asm) split add: sum.split)
    2.98  done
    2.99 -declare sum_case_map_upd_map_upd [simp]
   2.100  
   2.101  
   2.102  section {* map\_upds *}
   2.103  
   2.104 -lemma map_upds_twist [rule_format (no_asm)]: "a ~: set as --> (!m bs. (m(a|->b)(as[|->]bs)) = (m(as[|->]bs)(a|->b)))"
   2.105 -apply (induct_tac "as")
   2.106 -apply  (auto simp del: fun_upd_apply)
   2.107 -apply (drule spec)+
   2.108 -apply (rotate_tac -1)
   2.109 -apply (erule subst)
   2.110 -apply (erule fun_upd_twist [THEN subst])
   2.111 -apply (rule refl)
   2.112 +lemma map_upd_upds_conv_if:
   2.113 + "!!x y ys f. (f(x|->y))(xs [|->] ys) =
   2.114 +              (if x : set xs then f(xs [|->] ys) else (f(xs [|->] ys))(x|->y))"
   2.115 +apply(induct xs)
   2.116 + apply simp
   2.117 +apply(simp split:split_if add:fun_upd_twist eq_sym_conv)
   2.118  done
   2.119 -declare map_upds_twist [simp]
   2.120 +
   2.121 +lemma map_upds_twist [simp]:
   2.122 + "a ~: set as ==> m(a|->b)(as[|->]bs) = m(as[|->]bs)(a|->b)"
   2.123 +by (simp add: map_upd_upds_conv_if)
   2.124  
   2.125 +lemma map_upds_apply_nontin[simp]:
   2.126 + "!!ys. x ~: set xs ==> (f(xs[|->]ys)) x = f x"
   2.127 +apply(induct xs)
   2.128 + apply simp
   2.129 +apply(simp add: fun_upd_apply map_upd_upds_conv_if split:split_if)
   2.130 +done
   2.131  
   2.132  section {* chg\_map *}
   2.133  
   2.134 -lemma chg_map_new: "m a = None   ==> chg_map f a m = m"
   2.135 +lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
   2.136  apply (unfold chg_map_def)
   2.137  apply auto
   2.138  done
   2.139  
   2.140 -lemma chg_map_upd: "m a = Some b ==> chg_map f a m = m(a|->f b)"
   2.141 +lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"
   2.142  apply (unfold chg_map_def)
   2.143  apply auto
   2.144  done
   2.145  
   2.146 -declare chg_map_new [simp] chg_map_upd [simp]
   2.147 -
   2.148  
   2.149  section {* map\_of *}
   2.150  
   2.151 @@ -186,33 +191,30 @@
   2.152  
   2.153  section {* option\_map related *}
   2.154  
   2.155 -lemma option_map_o_empty: "option_map f o empty = empty"
   2.156 +lemma option_map_o_empty[simp]: "option_map f o empty = empty"
   2.157  apply (rule ext)
   2.158  apply (simp (no_asm))
   2.159  done
   2.160  
   2.161 -lemma option_map_o_map_upd: "option_map f o m(a|->b) = (option_map f o m)(a|->f b)"
   2.162 +lemma option_map_o_map_upd[simp]:
   2.163 + "option_map f o m(a|->b) = (option_map f o m)(a|->f b)"
   2.164  apply (rule ext)
   2.165  apply (simp (no_asm))
   2.166  done
   2.167  
   2.168 -declare option_map_o_empty [simp] option_map_o_map_upd [simp]
   2.169 -
   2.170  
   2.171  section {* ++ *}
   2.172  
   2.173 -lemma override_empty: "m ++ empty = m"
   2.174 +lemma override_empty[simp]: "m ++ empty = m"
   2.175  apply (unfold override_def)
   2.176  apply (simp (no_asm))
   2.177  done
   2.178 -declare override_empty [simp]
   2.179  
   2.180 -lemma empty_override: "empty ++ m = m"
   2.181 +lemma empty_override[simp]: "empty ++ m = m"
   2.182  apply (unfold override_def)
   2.183  apply (rule ext)
   2.184  apply (simp split add: option.split)
   2.185  done
   2.186 -declare empty_override [simp]
   2.187  
   2.188  lemma override_Some_iff [rule_format (no_asm)]: 
   2.189   "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)"
   2.190 @@ -223,26 +225,23 @@
   2.191  lemmas override_SomeD = override_Some_iff [THEN iffD1, standard]
   2.192  declare override_SomeD [dest!]
   2.193  
   2.194 -lemma override_find_right: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
   2.195 +lemma override_find_right[simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
   2.196  apply (subst override_Some_iff)
   2.197  apply fast
   2.198  done
   2.199 -declare override_find_right [simp]
   2.200  
   2.201 -lemma override_None: "((m ++ n) k = None) = (n k = None & m k = None)"
   2.202 +lemma override_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
   2.203  apply (unfold override_def)
   2.204  apply (simp (no_asm) split add: option.split)
   2.205  done
   2.206 -declare override_None [iff]
   2.207  
   2.208 -lemma override_upd: "f ++ g(x|->y) = (f ++ g)(x|->y)"
   2.209 +lemma override_upd[simp]: "f ++ g(x|->y) = (f ++ g)(x|->y)"
   2.210  apply (unfold override_def)
   2.211  apply (rule ext)
   2.212  apply auto
   2.213  done
   2.214 -declare override_upd [simp]
   2.215  
   2.216 -lemma map_of_override: "map_of ys ++ map_of xs = map_of (xs@ys)"
   2.217 +lemma map_of_override[simp]: "map_of ys ++ map_of xs = map_of (xs@ys)"
   2.218  apply (unfold override_def)
   2.219  apply (rule sym)
   2.220  apply (induct_tac "xs")
   2.221 @@ -250,7 +249,6 @@
   2.222  apply (rule ext)
   2.223  apply (simp (no_asm_simp) split add: option.split)
   2.224  done
   2.225 -declare map_of_override [simp]
   2.226  
   2.227  declare fun_upd_apply [simp del]
   2.228  lemma finite_range_map_of_override: "finite (range f) ==> finite (range (f ++ map_of l))"
   2.229 @@ -273,25 +271,27 @@
   2.230  apply auto
   2.231  done
   2.232  
   2.233 -lemma domIff: "(a : dom m) = (m a ~= None)"
   2.234 +lemma domIff[iff]: "(a : dom m) = (m a ~= None)"
   2.235  apply (unfold dom_def)
   2.236  apply auto
   2.237  done
   2.238 -declare domIff [iff]
   2.239  declare domIff [simp del]
   2.240  
   2.241 -lemma dom_empty: "dom empty = {}"
   2.242 +lemma dom_empty[simp]: "dom empty = {}"
   2.243  apply (unfold dom_def)
   2.244  apply (simp (no_asm))
   2.245  done
   2.246 -declare dom_empty [simp]
   2.247  
   2.248 -lemma dom_map_upd: "dom(m(a|->b)) = insert a (dom m)"
   2.249 +lemma dom_fun_upd[simp]:
   2.250 + "dom(f(x := y)) = (if y=None then dom f - {x} else insert x (dom f))"
   2.251 +by (simp add:dom_def) blast
   2.252 +(*
   2.253 +lemma dom_map_upd[simp]: "dom(m(a|->b)) = insert a (dom m)"
   2.254  apply (unfold dom_def)
   2.255  apply (simp (no_asm))
   2.256  apply blast
   2.257  done
   2.258 -declare dom_map_upd [simp]
   2.259 +*)
   2.260  
   2.261  lemma finite_dom_map_of: "finite (dom (map_of l))"
   2.262  apply (unfold dom_def)
   2.263 @@ -299,32 +299,42 @@
   2.264  apply (auto simp add: insert_Collect [symmetric])
   2.265  done
   2.266  
   2.267 -lemma dom_override: "dom(m++n) = dom n Un dom m"
   2.268 +lemma dom_map_upds[simp]: "!!m vs. dom(m(xs[|->]vs)) = set xs Un dom m"
   2.269 +by(induct xs, simp_all)
   2.270 +
   2.271 +lemma dom_override[simp]: "dom(m++n) = dom n Un dom m"
   2.272  apply (unfold dom_def)
   2.273  apply auto
   2.274  done
   2.275 -declare dom_override [simp]
   2.276 +
   2.277 +lemma dom_overwrite[simp]:
   2.278 + "dom(f(g|A)) = (dom f  - {a. a : A - dom g}) Un {a. a : A Int dom g}"
   2.279 +by(auto simp add: dom_def overwrite_def)
   2.280  
   2.281  section {* ran *}
   2.282  
   2.283 -lemma ran_empty: "ran empty = {}"
   2.284 +lemma ran_empty[simp]: "ran empty = {}"
   2.285  apply (unfold ran_def)
   2.286  apply (simp (no_asm))
   2.287  done
   2.288 -declare ran_empty [simp]
   2.289  
   2.290 -lemma ran_empty': "ran (%u. None) = {}"
   2.291 -apply (unfold ran_def)
   2.292 -apply auto
   2.293 -done
   2.294 -declare ran_empty' [simp]
   2.295 -
   2.296 -lemma ran_map_upd: "m a = None ==> ran(m(a|->b)) = insert b (ran m)"
   2.297 +lemma ran_map_upd[simp]: "m a = None ==> ran(m(a|->b)) = insert b (ran m)"
   2.298  apply (unfold ran_def)
   2.299  apply auto
   2.300  apply (subgoal_tac "~ (aa = a) ")
   2.301  apply auto
   2.302  done
   2.303 -declare ran_map_upd [simp]
   2.304 +
   2.305 +section{* @{text"\<subseteq>\<^sub>m"} *}
   2.306 +
   2.307 +lemma [simp]: "empty \<subseteq>\<^sub>m g"
   2.308 +by(simp add:map_le_def)
   2.309 +
   2.310 +lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
   2.311 +by(fastsimp simp add:map_le_def)
   2.312 +
   2.313 +lemma map_le_upds[simp]:
   2.314 + "!!f g bs. f \<subseteq>\<^sub>m g ==> f(as [|->] bs) \<subseteq>\<^sub>m g(as [|->] bs)"
   2.315 +by(induct as, auto)
   2.316  
   2.317  end