src/HOL/Map.thy
changeset 13937 e9d57517c9b1
parent 13914 026866537fae
child 14025 d9b155757dc8
     1.1 --- a/src/HOL/Map.thy	Wed Apr 30 10:01:35 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed Apr 30 17:53:47 2003 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4          "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
     1.5  
     1.6  
     1.7 -section {* empty *}
     1.8 +subsection {* empty *}
     1.9  
    1.10  lemma empty_upd_none[simp]: "empty(x := None) = empty"
    1.11  apply (rule ext)
    1.12 @@ -72,7 +72,7 @@
    1.13  apply (simp (no_asm) split add: sum.split)
    1.14  done
    1.15  
    1.16 -section {* map\_upd *}
    1.17 +subsection {* map\_upd *}
    1.18  
    1.19  lemma map_upd_triv: "t k = Some x ==> t(k|->x) = t"
    1.20  apply (rule ext)
    1.21 @@ -95,7 +95,7 @@
    1.22  
    1.23  
    1.24  (* FIXME: what is this sum_case nonsense?? *)
    1.25 -section {* sum\_case and empty/map\_upd *}
    1.26 +subsection {* sum\_case and empty/map\_upd *}
    1.27  
    1.28  lemma sum_case_map_upd_empty[simp]:
    1.29   "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)"
    1.30 @@ -116,7 +116,7 @@
    1.31  done
    1.32  
    1.33  
    1.34 -section {* map\_upds *}
    1.35 +subsection {* map\_upds *}
    1.36  
    1.37  lemma map_upd_upds_conv_if:
    1.38   "!!x y ys f. (f(x|->y))(xs [|->] ys) =
    1.39 @@ -137,7 +137,7 @@
    1.40  apply(simp add: fun_upd_apply map_upd_upds_conv_if split:split_if)
    1.41  done
    1.42  
    1.43 -section {* chg\_map *}
    1.44 +subsection {* chg\_map *}
    1.45  
    1.46  lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
    1.47  apply (unfold chg_map_def)
    1.48 @@ -150,7 +150,7 @@
    1.49  done
    1.50  
    1.51  
    1.52 -section {* map\_of *}
    1.53 +subsection {* map\_of *}
    1.54  
    1.55  lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
    1.56  apply (induct_tac "xs")
    1.57 @@ -191,7 +191,7 @@
    1.58  done
    1.59  
    1.60  
    1.61 -section {* option\_map related *}
    1.62 +subsection {* option\_map related *}
    1.63  
    1.64  lemma option_map_o_empty[simp]: "option_map f o empty = empty"
    1.65  apply (rule ext)
    1.66 @@ -205,7 +205,7 @@
    1.67  done
    1.68  
    1.69  
    1.70 -section {* ++ *}
    1.71 +subsection {* ++ *}
    1.72  
    1.73  lemma override_empty[simp]: "m ++ empty = m"
    1.74  apply (unfold override_def)
    1.75 @@ -261,7 +261,7 @@
    1.76  declare fun_upd_apply [simp]
    1.77  
    1.78  
    1.79 -section {* dom *}
    1.80 +subsection {* dom *}
    1.81  
    1.82  lemma domI: "m a = Some b ==> a : dom m"
    1.83  apply (unfold dom_def)
    1.84 @@ -295,6 +295,11 @@
    1.85  done
    1.86  *)
    1.87  
    1.88 +lemma dom_map_of: "dom(map_of xys) = {x. \<exists>y. (x,y) : set xys}"
    1.89 +apply(induct xys)
    1.90 +apply(auto simp del:fun_upd_apply)
    1.91 +done
    1.92 +
    1.93  lemma finite_dom_map_of: "finite (dom (map_of l))"
    1.94  apply (unfold dom_def)
    1.95  apply (induct_tac "l")
    1.96 @@ -313,7 +318,7 @@
    1.97   "dom(f(g|A)) = (dom f  - {a. a : A - dom g}) Un {a. a : A Int dom g}"
    1.98  by(auto simp add: dom_def overwrite_def)
    1.99  
   1.100 -section {* ran *}
   1.101 +subsection {* ran *}
   1.102  
   1.103  lemma ran_empty[simp]: "ran empty = {}"
   1.104  apply (unfold ran_def)
   1.105 @@ -327,7 +332,7 @@
   1.106  apply auto
   1.107  done
   1.108  
   1.109 -section {* map\_le *}
   1.110 +subsection {* map\_le *}
   1.111  
   1.112  lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
   1.113  by(simp add:map_le_def)