src/HOL/Map.thy
changeset 14100 804be4c4b642
parent 14033 bc723de8ec95
child 14134 0fdf5708c7a8
     1.1 --- a/src/HOL/Map.thy	Fri Jul 11 14:12:02 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Fri Jul 11 14:12:06 2003 +0200
     1.3 @@ -11,15 +11,22 @@
     1.4  theory Map = List:
     1.5  
     1.6  types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
     1.7 +translations (type) "a ~=> b " <= (type) "a => b option"
     1.8  
     1.9  consts
    1.10  chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
    1.11 -map_add:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    1.12 +map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    1.13 +map_image::"('b => 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixr "`>" 90)
    1.14 +restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_|'__" [90, 91] 90)
    1.15  dom	:: "('a ~=> 'b) => 'a set"
    1.16  ran	:: "('a ~=> 'b) => 'b set"
    1.17  map_of	:: "('a * 'b)list => 'a ~=> 'b"
    1.18  map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
    1.19  	    ('a ~=> 'b)"		 ("_/'(_[|->]_/')" [900,0,0]900)
    1.20 +map_upd_s::"('a ~=> 'b) => 'a set => 'b => 
    1.21 +	    ('a ~=> 'b)"			 ("_/'(_{|->}_/')" [900,0,0]900)
    1.22 +map_subst::"('a ~=> 'b) => 'b => 'b => 
    1.23 +	    ('a ~=> 'b)"			 ("_/'(_~>_/')"    [900,0,0]900)
    1.24  map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
    1.25  
    1.26  syntax
    1.27 @@ -29,23 +36,35 @@
    1.28  
    1.29  syntax (xsymbols)
    1.30    "~=>"     :: "[type, type] => type"    (infixr "\<leadsto>" 0)
    1.31 +  restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<lfloor>_" [90, 91] 90)
    1.32    map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
    1.33  					  ("_/'(_/\<mapsto>/_')"  [900,0,0]900)
    1.34    map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    1.35  				         ("_/'(_/[\<mapsto>]/_')" [900,0,0]900)
    1.36 +  map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
    1.37 +				    		 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
    1.38 +  map_subst :: "('a ~=> 'b) => 'b => 'b => 
    1.39 +	        ('a ~=> 'b)"			 ("_/'(_\<leadsto>_/')"    [900,0,0]900)
    1.40 + "@chg_map" :: "('a ~=> 'b) => 'a => ('b => 'b) => ('a ~=> 'b)"
    1.41 +					  ("_/'(_/\<mapsto>\<lambda>_. _')"  [900,0,0,0] 900)
    1.42  
    1.43  translations
    1.44    "empty"    => "_K None"
    1.45    "empty"    <= "%x. None"
    1.46  
    1.47    "m(a|->b)" == "m(a:=Some b)"
    1.48 +  "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
    1.49  
    1.50  defs
    1.51  chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    1.52  
    1.53 -map_add_def: "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    1.54 +map_add_def:   "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    1.55 +map_image_def: "f`>m == option_map f o m"
    1.56 +restrict_map_def: "m|_A == %x. if x : A then m x else None"
    1.57  
    1.58  map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    1.59 +map_upd_s_def: "m(as{|->}b) == %x. if x : as then Some b else m x"
    1.60 +map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
    1.61  
    1.62  dom_def: "dom(m) == {a. m a ~= None}"
    1.63  ran_def: "ran(m) == {b. EX a. m a = Some b}"
    1.64 @@ -57,7 +76,7 @@
    1.65    "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    1.66  
    1.67  
    1.68 -subsection {* empty *}
    1.69 +subsection {* @{term empty} *}
    1.70  
    1.71  lemma empty_upd_none[simp]: "empty(x := None) = empty"
    1.72  apply (rule ext)
    1.73 @@ -71,7 +90,7 @@
    1.74  apply (simp (no_asm) split add: sum.split)
    1.75  done
    1.76  
    1.77 -subsection {* map\_upd *}
    1.78 +subsection {* @{term map_upd} *}
    1.79  
    1.80  lemma map_upd_triv: "t k = Some x ==> t(k|->x) = t"
    1.81  apply (rule ext)
    1.82 @@ -84,6 +103,13 @@
    1.83  apply (simp (no_asm_use))
    1.84  done
    1.85  
    1.86 +lemma map_upd_eqD1: "m(a\<mapsto>x) = n(a\<mapsto>y) \<Longrightarrow> x = y"
    1.87 +by (drule fun_cong [of _ _ a], auto)
    1.88 +
    1.89 +lemma map_upd_Some_unfold: 
    1.90 +  "((m(a|->b)) x = Some y) = (x = a \<and> b = y \<or> x \<noteq> a \<and> m x = Some y)"
    1.91 +by auto
    1.92 +
    1.93  lemma finite_range_updI: "finite (range f) ==> finite (range (f(a|->b)))"
    1.94  apply (unfold image_def)
    1.95  apply (simp (no_asm_use) add: full_SetCompr_eq)
    1.96 @@ -94,7 +120,7 @@
    1.97  
    1.98  
    1.99  (* FIXME: what is this sum_case nonsense?? *)
   1.100 -subsection {* sum\_case and empty/map\_upd *}
   1.101 +subsection {* @{term sum_case} and @{term empty}/@{term map_upd} *}
   1.102  
   1.103  lemma sum_case_map_upd_empty[simp]:
   1.104   "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)"
   1.105 @@ -115,7 +141,7 @@
   1.106  done
   1.107  
   1.108  
   1.109 -subsection {* chg\_map *}
   1.110 +subsection {* @{term chg_map} *}
   1.111  
   1.112  lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
   1.113  apply (unfold chg_map_def)
   1.114 @@ -128,7 +154,7 @@
   1.115  done
   1.116  
   1.117  
   1.118 -subsection {* map\_of *}
   1.119 +subsection {* @{term map_of} *}
   1.120  
   1.121  lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
   1.122  apply (induct_tac "xs")
   1.123 @@ -169,7 +195,7 @@
   1.124  done
   1.125  
   1.126  
   1.127 -subsection {* option\_map related *}
   1.128 +subsection {* @{term option_map} related *}
   1.129  
   1.130  lemma option_map_o_empty[simp]: "option_map f o empty = empty"
   1.131  apply (rule ext)
   1.132 @@ -183,7 +209,7 @@
   1.133  done
   1.134  
   1.135  
   1.136 -subsection {* ++ *}
   1.137 +subsection {* @{text "++"} *}
   1.138  
   1.139  lemma map_add_empty[simp]: "m ++ empty = m"
   1.140  apply (unfold map_add_def)
   1.141 @@ -243,8 +269,37 @@
   1.142  done
   1.143  declare fun_upd_apply [simp]
   1.144  
   1.145 +subsection {* @{term map_image} *}
   1.146  
   1.147 -subsection {* map\_upds *}
   1.148 +lemma map_image_empty [simp]: "f`>empty = empty" 
   1.149 +by (auto simp: map_image_def empty_def)
   1.150 +
   1.151 +lemma map_image_upd [simp]: "f`>m(a|->b) = (f`>m)(a|->f b)" 
   1.152 +apply (auto simp: map_image_def fun_upd_def)
   1.153 +by (rule ext, auto)
   1.154 +
   1.155 +subsection {* @{term restrict_map} *}
   1.156 +
   1.157 +lemma restrict_in [simp]: "x \<in> A \<Longrightarrow> (m\<lfloor>A) x = m x"
   1.158 +by (auto simp: restrict_map_def)
   1.159 +
   1.160 +lemma restrict_out [simp]: "x \<notin> A \<Longrightarrow> (m\<lfloor>A) x = None"
   1.161 +by (auto simp: restrict_map_def)
   1.162 +
   1.163 +lemma ran_restrictD: "y \<in> ran (m\<lfloor>A) \<Longrightarrow> \<exists>x\<in>A. m x = Some y"
   1.164 +by (auto simp: restrict_map_def ran_def split: split_if_asm)
   1.165 +
   1.166 +lemma dom_valF_restrict [simp]: "dom (m\<lfloor>A) = dom m \<inter> A"
   1.167 +by (auto simp: restrict_map_def dom_def split: split_if_asm)
   1.168 +
   1.169 +lemma restrict_upd_same [simp]: "m(x\<mapsto>y)\<lfloor>(-{x}) = m\<lfloor>(-{x})"
   1.170 +by (rule ext, auto simp: restrict_map_def)
   1.171 +
   1.172 +lemma restrict_restrict [simp]: "m\<lfloor>A\<lfloor>B = m\<lfloor>(A\<inter>B)"
   1.173 +by (rule ext, auto simp: restrict_map_def)
   1.174 +
   1.175 +
   1.176 +subsection {* @{term map_upds} *}
   1.177  
   1.178  lemma map_upds_Nil1[simp]: "m([] [|->] bs) = m"
   1.179  by(simp add:map_upds_def)
   1.180 @@ -280,12 +335,23 @@
   1.181   apply(auto simp: map_upd_upds_conv_if)
   1.182  done
   1.183  
   1.184 -subsection {* dom *}
   1.185 +subsection {* @{term map_upd_s} *}
   1.186 +
   1.187 +lemma map_upd_s_apply [simp]: 
   1.188 +  "(m(as{|->}b)) x = (if x : as then Some b else m x)"
   1.189 +by (simp add: map_upd_s_def)
   1.190 +
   1.191 +lemma map_subst_apply [simp]: 
   1.192 +  "(m(a~>b)) x = (if m x = Some a then Some b else m x)" 
   1.193 +by (simp add: map_subst_def)
   1.194 +
   1.195 +subsection {* @{term dom} *}
   1.196  
   1.197  lemma domI: "m a = Some b ==> a : dom m"
   1.198  apply (unfold dom_def)
   1.199  apply auto
   1.200  done
   1.201 +(* declare domI [intro]? *)
   1.202  
   1.203  lemma domD: "a : dom m ==> ? b. m a = Some b"
   1.204  apply (unfold dom_def)
   1.205 @@ -340,7 +406,11 @@
   1.206  apply(fastsimp simp:map_add_def split:option.split)
   1.207  done
   1.208  
   1.209 -subsection {* ran *}
   1.210 +subsection {* @{term ran} *}
   1.211 +
   1.212 +lemma ranI: "m a = Some b ==> b : ran m" 
   1.213 +by (auto simp add: ran_def)
   1.214 +(* declare ranI [intro]? *)
   1.215  
   1.216  lemma ran_empty[simp]: "ran empty = {}"
   1.217  apply (unfold ran_def)
   1.218 @@ -354,7 +424,7 @@
   1.219  apply auto
   1.220  done
   1.221  
   1.222 -subsection {* map\_le *}
   1.223 +subsection {* @{text "map_le"} *}
   1.224  
   1.225  lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
   1.226  by(simp add:map_le_def)