Map.ML integrated into Map.thy
authorwebertj
Fri Apr 11 23:11:13 2003 +0200 (2003-04-11)
changeset 139084bdfa9f77254
parent 13907 2bc462b99e70
child 13909 a5247a49c85e
Map.ML integrated into Map.thy
src/HOL/IsaMakefile
src/HOL/Map.ML
src/HOL/Map.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Apr 09 12:52:45 2003 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 11 23:11:13 2003 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4    Integ/NatSimprocs.thy Integ/int_arith1.ML Integ/int_arith2.ML \
     1.5    Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
     1.6    Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
     1.7 -  Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
     1.8 +  Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
     1.9    Nat.thy NatArith.ML NatArith.thy Numeral.thy \
    1.10    Power.ML Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML \
    1.11    Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
     2.1 --- a/src/HOL/Map.ML	Wed Apr 09 12:52:45 2003 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,267 +0,0 @@
     2.4 -(*  Title:      HOL/Map.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Tobias Nipkow
     2.7 -    Copyright   1997 TU Muenchen
     2.8 -
     2.9 -Map lemmas.
    2.10 -*)
    2.11 -
    2.12 -section "empty";
    2.13 -
    2.14 -Goal "empty(x := None) = empty";
    2.15 -by (rtac ext 1);
    2.16 -by (Simp_tac 1);
    2.17 -qed "empty_upd_none";
    2.18 -Addsimps [empty_upd_none];
    2.19 -
    2.20 -(* FIXME: what is this sum_case nonsense?? *)
    2.21 -Goal "sum_case empty empty = empty";
    2.22 -by (rtac ext 1);
    2.23 -by (simp_tac (simpset() addsplits [sum.split]) 1);
    2.24 -qed "sum_case_empty_empty";
    2.25 -Addsimps [sum_case_empty_empty];
    2.26 -
    2.27 -
    2.28 -section "map_upd";
    2.29 -
    2.30 -Goal "t k = Some x ==> t(k|->x) = t";
    2.31 -by (rtac ext 1);
    2.32 -by (Asm_simp_tac 1);
    2.33 -qed "map_upd_triv";
    2.34 -
    2.35 -Goal "t(k|->x) ~= empty";
    2.36 -by Safe_tac;
    2.37 -by (dres_inst_tac [("x","k")] fun_cong 1);
    2.38 -by (Full_simp_tac 1);
    2.39 -qed "map_upd_nonempty";
    2.40 -Addsimps[map_upd_nonempty];
    2.41 -
    2.42 -Goalw [image_def] "finite (range f) ==> finite (range (f(a|->b)))";
    2.43 -by (full_simp_tac (simpset() addsimps [full_SetCompr_eq]) 1);
    2.44 -by (rtac finite_subset 1);
    2.45 -by (assume_tac 2);
    2.46 -by Auto_tac;
    2.47 -qed "finite_range_updI";
    2.48 -
    2.49 -
    2.50 -(* FIXME: what is this sum_case nonsense?? *)
    2.51 -section "sum_case and empty/map_upd";
    2.52 -
    2.53 -Goal "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)";
    2.54 -by (rtac ext 1);
    2.55 -by (simp_tac (simpset() addsplits [sum.split]) 1);
    2.56 -qed "sum_case_map_upd_empty";
    2.57 -Addsimps[sum_case_map_upd_empty];
    2.58 -
    2.59 -Goal "sum_case empty (m(k|->y)) =  (sum_case empty m)(Inr k|->y)";
    2.60 -by (rtac ext 1);
    2.61 -by (simp_tac (simpset() addsplits [sum.split]) 1);
    2.62 -qed "sum_case_empty_map_upd";
    2.63 -Addsimps[sum_case_empty_map_upd];
    2.64 -
    2.65 -Goal "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)";
    2.66 -by (rtac ext 1);
    2.67 -by (simp_tac (simpset() addsplits [sum.split]) 1);
    2.68 -qed "sum_case_map_upd_map_upd";
    2.69 -Addsimps[sum_case_map_upd_map_upd];
    2.70 -
    2.71 -
    2.72 -section "map_upds";
    2.73 -
    2.74 -Goal "a ~: set as --> (!m bs. (m(a|->b)(as[|->]bs)) = (m(as[|->]bs)(a|->b)))";
    2.75 -by (induct_tac "as" 1);
    2.76 -by  (auto_tac (claset(), simpset() delsimps[fun_upd_apply]));
    2.77 -by (REPEAT(dtac spec 1));
    2.78 -by (rotate_tac ~1 1);
    2.79 -by (etac subst 1);
    2.80 -by (etac (fun_upd_twist RS subst) 1);
    2.81 -by (rtac refl 1);
    2.82 -qed_spec_mp "map_upds_twist";
    2.83 -Addsimps [map_upds_twist];
    2.84 -
    2.85 -
    2.86 -section "chg_map";
    2.87 -
    2.88 -Goalw [chg_map_def] "m a = None   ==> chg_map f a m = m";
    2.89 -by Auto_tac;
    2.90 -qed "chg_map_new";
    2.91 -
    2.92 -Goalw [chg_map_def] "m a = Some b ==> chg_map f a m = m(a|->f b)";
    2.93 -by Auto_tac;
    2.94 -qed "chg_map_upd";
    2.95 -
    2.96 -Addsimps[chg_map_new, chg_map_upd];
    2.97 -
    2.98 -
    2.99 -section "map_of";
   2.100 -
   2.101 -Goal "map_of xs k = Some y --> (k,y):set xs";
   2.102 -by (induct_tac "xs" 1);
   2.103 -by  Auto_tac;
   2.104 -qed_spec_mp "map_of_SomeD";
   2.105 -
   2.106 -Goal "inj f ==> map_of t k = Some x --> \
   2.107 -\  map_of (map (split (%k. Pair (f k))) t) (f k) = Some x";
   2.108 -by (induct_tac "t" 1);
   2.109 -by  (auto_tac (claset(),simpset()addsimps[inj_eq]));
   2.110 -qed_spec_mp "map_of_mapk_SomeI";
   2.111 -
   2.112 -Goal "(k, x) : set l --> (? x. map_of l k = Some x)";
   2.113 -by (induct_tac "l" 1);
   2.114 -by  Auto_tac;
   2.115 -qed_spec_mp "weak_map_of_SomeI";
   2.116 -
   2.117 -Goal 
   2.118 -"[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z";
   2.119 -by (rtac mp 1);
   2.120 -by (atac 2);
   2.121 -by (etac thin_rl 1);
   2.122 -by (induct_tac "xs" 1);
   2.123 -by  Auto_tac;
   2.124 -qed "map_of_filter_in";
   2.125 -
   2.126 -Goal "finite (range (map_of l))";
   2.127 -by (induct_tac "l" 1);
   2.128 -by  (ALLGOALS (simp_tac (simpset() addsimps [image_constant])));
   2.129 -by (rtac finite_subset 1);
   2.130 -by (assume_tac 2);
   2.131 -by Auto_tac;
   2.132 -qed "finite_range_map_of";
   2.133 -
   2.134 -Goal "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
   2.135 -by (induct_tac "xs" 1);
   2.136 -by Auto_tac;
   2.137 -qed "map_of_map";
   2.138 -
   2.139 -
   2.140 -section "option_map related";
   2.141 -
   2.142 -Goal "option_map f o empty = empty";
   2.143 -by (rtac ext 1);
   2.144 -by (Simp_tac 1);
   2.145 -qed "option_map_o_empty";
   2.146 -
   2.147 -Goal "option_map f o m(a|->b) = (option_map f o m)(a|->f b)";
   2.148 -by (rtac ext 1);
   2.149 -by (Simp_tac 1);
   2.150 -qed "option_map_o_map_upd";
   2.151 -
   2.152 -Addsimps[option_map_o_empty, option_map_o_map_upd];
   2.153 -
   2.154 -
   2.155 -section "++";
   2.156 -
   2.157 -Goalw [override_def] "m ++ empty = m";
   2.158 -by (Simp_tac 1);
   2.159 -qed "override_empty";
   2.160 -Addsimps [override_empty];
   2.161 -
   2.162 -Goalw [override_def] "empty ++ m = m";
   2.163 -by (Simp_tac 1);
   2.164 -by (rtac ext 1);
   2.165 -by (split_tac [option.split] 1);
   2.166 -by (Simp_tac 1);
   2.167 -qed "empty_override";
   2.168 -Addsimps [empty_override];
   2.169 -
   2.170 -Goalw [override_def]
   2.171 - "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
   2.172 -by (simp_tac (simpset() addsplits [option.split]) 1);
   2.173 -qed_spec_mp "override_Some_iff";
   2.174 -
   2.175 -bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
   2.176 -AddSDs[override_SomeD];
   2.177 -
   2.178 -Goal "!!xx. n k = Some xx ==> (m ++ n) k = Some xx";
   2.179 -by (stac override_Some_iff 1);
   2.180 -by (Fast_tac 1);
   2.181 -qed "override_find_right";
   2.182 -Addsimps[override_find_right];
   2.183 -
   2.184 -Goalw [override_def] "((m ++ n) k = None) = (n k = None & m k = None)";
   2.185 -by (simp_tac (simpset() addsplits [option.split]) 1);
   2.186 -qed "override_None";
   2.187 -AddIffs [override_None];
   2.188 -
   2.189 -Goalw [override_def] "f ++ g(x|->y) = (f ++ g)(x|->y)";
   2.190 -by (rtac ext 1);
   2.191 -by Auto_tac;
   2.192 -qed "override_upd";
   2.193 -Addsimps[override_upd];
   2.194 -
   2.195 -Goalw [override_def] "map_of ys ++ map_of xs = map_of (xs@ys)";
   2.196 -by (rtac sym 1);
   2.197 -by (induct_tac "xs" 1);
   2.198 -by (Simp_tac 1);
   2.199 -by (rtac ext 1);
   2.200 -by (asm_simp_tac (simpset() addsplits [option.split]) 1);
   2.201 -qed "map_of_override";
   2.202 -Addsimps [map_of_override];
   2.203 -
   2.204 -Delsimps[fun_upd_apply];
   2.205 -Goal "finite (range f) ==> finite (range (f ++ map_of l))";
   2.206 -by (induct_tac "l" 1);
   2.207 -by  Auto_tac;
   2.208 -by  (fold_goals_tac [empty_def]);
   2.209 -by  (Asm_simp_tac 1);
   2.210 -by (etac finite_range_updI 1);
   2.211 -qed "finite_range_map_of_override";
   2.212 -Addsimps [fun_upd_apply];
   2.213 -
   2.214 -
   2.215 -section "dom";
   2.216 -
   2.217 -Goalw [dom_def] "m a = Some b ==> a : dom m";
   2.218 -by Auto_tac;
   2.219 -qed "domI";
   2.220 -
   2.221 -Goalw [dom_def] "a : dom m ==> ? b. m a = Some b";
   2.222 -by Auto_tac;
   2.223 -qed "domD";
   2.224 -
   2.225 -Goalw [dom_def] "(a : dom m) = (m a ~= None)";
   2.226 -by Auto_tac;
   2.227 -qed "domIff";
   2.228 -AddIffs [domIff];
   2.229 -Delsimps [domIff];
   2.230 -
   2.231 -Goalw [dom_def] "dom empty = {}";
   2.232 -by (Simp_tac 1);
   2.233 -qed "dom_empty";
   2.234 -Addsimps [dom_empty];
   2.235 -
   2.236 -Goalw [dom_def] "dom(m(a|->b)) = insert a (dom m)";
   2.237 -by (Simp_tac 1);
   2.238 -by (Blast_tac 1);
   2.239 -qed "dom_map_upd";
   2.240 -Addsimps [dom_map_upd];
   2.241 -
   2.242 -Goalw [dom_def] "finite (dom (map_of l))";
   2.243 -by (induct_tac "l" 1);
   2.244 -by (auto_tac (claset(),
   2.245 -              simpset() addsimps [insert_Collect RS sym]));
   2.246 -qed "finite_dom_map_of";
   2.247 -
   2.248 -Goalw [dom_def] "dom(m++n) = dom n Un dom m";
   2.249 -by Auto_tac;
   2.250 -qed "dom_override";
   2.251 -Addsimps [dom_override];
   2.252 -
   2.253 -section "ran";
   2.254 -
   2.255 -Goalw [ran_def] "ran empty = {}";
   2.256 -by (Simp_tac 1);
   2.257 -qed "ran_empty";
   2.258 -Addsimps [ran_empty];
   2.259 -
   2.260 -Goalw [ran_def] "ran (%u. None) = {}";
   2.261 -by Auto_tac;
   2.262 -qed "ran_empty'";
   2.263 -Addsimps[ran_empty'];
   2.264 -
   2.265 -Goalw [ran_def] "m a = None ==> ran(m(a|->b)) = insert b (ran m)";
   2.266 -by Auto_tac;
   2.267 -by (subgoal_tac "~(aa = a)" 1);
   2.268 -by Auto_tac;
   2.269 -qed "ran_map_upd";
   2.270 -Addsimps [ran_map_upd];
     3.1 --- a/src/HOL/Map.thy	Wed Apr 09 12:52:45 2003 +0200
     3.2 +++ b/src/HOL/Map.thy	Fri Apr 11 23:11:13 2003 +0200
     3.3 @@ -1,14 +1,14 @@
     3.4  (*  Title:      HOL/Map.thy
     3.5      ID:         $Id$
     3.6      Author:     Tobias Nipkow, based on a theory by David von Oheimb
     3.7 -    Copyright   1997 TU Muenchen
     3.8 +    Copyright   1997-2003 TU Muenchen
     3.9  
    3.10  The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
    3.11  *)
    3.12  
    3.13 -Map = List +
    3.14 +theory Map = List:
    3.15  
    3.16 -types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
    3.17 +types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
    3.18  
    3.19  consts
    3.20  chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
    3.21 @@ -24,11 +24,11 @@
    3.22  					         ("_/'(_/|->_')"   [900,0,0]900)
    3.23  
    3.24  syntax (xsymbols)
    3.25 -  "~=>"     :: [type, type] => type      (infixr "\\<leadsto>" 0)
    3.26 +  "~=>"     :: "[type, type] => type"    (infixr "\<leadsto>" 0)
    3.27    map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
    3.28 -					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)
    3.29 +					  ("_/'(_/\<mapsto>/_')"  [900,0,0]900)
    3.30    map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    3.31 -				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
    3.32 +				         ("_/'(_/[\<mapsto>]/_')" [900,0,0]900)
    3.33  
    3.34  translations
    3.35    "empty"    => "_K None"
    3.36 @@ -38,12 +38,12 @@
    3.37  
    3.38  defs
    3.39  
    3.40 -chg_map_def  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    3.41 +chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    3.42  
    3.43 -override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    3.44 +override_def: "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    3.45  
    3.46 -dom_def "dom(m) == {a. m a ~= None}"
    3.47 -ran_def "ran(m) == {b. ? a. m a = Some b}"
    3.48 +dom_def: "dom(m) == {a. m a ~= None}"
    3.49 +ran_def: "ran(m) == {b. ? a. m a = Some b}"
    3.50  
    3.51  primrec
    3.52    "map_of [] = empty"
    3.53 @@ -52,4 +52,279 @@
    3.54  primrec "t([]  [|->]bs) = t"
    3.55          "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
    3.56  
    3.57 +
    3.58 +section "empty"
    3.59 +
    3.60 +lemma empty_upd_none: "empty(x := None) = empty"
    3.61 +apply (rule ext)
    3.62 +apply (simp (no_asm))
    3.63 +done
    3.64 +declare empty_upd_none [simp]
    3.65 +
    3.66 +(* FIXME: what is this sum_case nonsense?? *)
    3.67 +lemma sum_case_empty_empty: "sum_case empty empty = empty"
    3.68 +apply (rule ext)
    3.69 +apply (simp (no_asm) split add: sum.split)
    3.70 +done
    3.71 +declare sum_case_empty_empty [simp]
    3.72 +
    3.73 +
    3.74 +section "map_upd"
    3.75 +
    3.76 +lemma map_upd_triv: "t k = Some x ==> t(k|->x) = t"
    3.77 +apply (rule ext)
    3.78 +apply (simp (no_asm_simp))
    3.79 +done
    3.80 +
    3.81 +lemma map_upd_nonempty: "t(k|->x) ~= empty"
    3.82 +apply safe
    3.83 +apply (drule_tac x = "k" in fun_cong)
    3.84 +apply (simp (no_asm_use))
    3.85 +done
    3.86 +declare map_upd_nonempty [simp]
    3.87 +
    3.88 +lemma finite_range_updI: "finite (range f) ==> finite (range (f(a|->b)))"
    3.89 +apply (unfold image_def)
    3.90 +apply (simp (no_asm_use) add: full_SetCompr_eq)
    3.91 +apply (rule finite_subset)
    3.92 +prefer 2 apply (assumption)
    3.93 +apply auto
    3.94 +done
    3.95 +
    3.96 +
    3.97 +(* FIXME: what is this sum_case nonsense?? *)
    3.98 +section "sum_case and empty/map_upd"
    3.99 +
   3.100 +lemma sum_case_map_upd_empty: "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)"
   3.101 +apply (rule ext)
   3.102 +apply (simp (no_asm) split add: sum.split)
   3.103 +done
   3.104 +declare sum_case_map_upd_empty [simp]
   3.105 +
   3.106 +lemma sum_case_empty_map_upd: "sum_case empty (m(k|->y)) =  (sum_case empty m)(Inr k|->y)"
   3.107 +apply (rule ext)
   3.108 +apply (simp (no_asm) split add: sum.split)
   3.109 +done
   3.110 +declare sum_case_empty_map_upd [simp]
   3.111 +
   3.112 +lemma sum_case_map_upd_map_upd: "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)"
   3.113 +apply (rule ext)
   3.114 +apply (simp (no_asm) split add: sum.split)
   3.115 +done
   3.116 +declare sum_case_map_upd_map_upd [simp]
   3.117 +
   3.118 +
   3.119 +section "map_upds"
   3.120 +
   3.121 +lemma map_upds_twist [rule_format (no_asm)]: "a ~: set as --> (!m bs. (m(a|->b)(as[|->]bs)) = (m(as[|->]bs)(a|->b)))"
   3.122 +apply (induct_tac "as")
   3.123 +apply  (auto simp del: fun_upd_apply)
   3.124 +apply (drule spec)+
   3.125 +apply (rotate_tac -1)
   3.126 +apply (erule subst)
   3.127 +apply (erule fun_upd_twist [THEN subst])
   3.128 +apply (rule refl)
   3.129 +done
   3.130 +declare map_upds_twist [simp]
   3.131 +
   3.132 +
   3.133 +section "chg_map"
   3.134 +
   3.135 +lemma chg_map_new: "m a = None   ==> chg_map f a m = m"
   3.136 +apply (unfold chg_map_def)
   3.137 +apply auto
   3.138 +done
   3.139 +
   3.140 +lemma chg_map_upd: "m a = Some b ==> chg_map f a m = m(a|->f b)"
   3.141 +apply (unfold chg_map_def)
   3.142 +apply auto
   3.143 +done
   3.144 +
   3.145 +declare chg_map_new [simp] chg_map_upd [simp]
   3.146 +
   3.147 +
   3.148 +section "map_of"
   3.149 +
   3.150 +lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
   3.151 +apply (induct_tac "xs")
   3.152 +apply  auto
   3.153 +done
   3.154 +
   3.155 +lemma map_of_mapk_SomeI [rule_format (no_asm)]: "inj f ==> map_of t k = Some x -->  
   3.156 +   map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
   3.157 +apply (induct_tac "t")
   3.158 +apply  (auto simp add: inj_eq)
   3.159 +done
   3.160 +
   3.161 +lemma weak_map_of_SomeI [rule_format (no_asm)]: "(k, x) : set l --> (? x. map_of l k = Some x)"
   3.162 +apply (induct_tac "l")
   3.163 +apply  auto
   3.164 +done
   3.165 +
   3.166 +lemma map_of_filter_in: 
   3.167 +"[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z"
   3.168 +apply (rule mp)
   3.169 +prefer 2 apply (assumption)
   3.170 +apply (erule thin_rl)
   3.171 +apply (induct_tac "xs")
   3.172 +apply  auto
   3.173 +done
   3.174 +
   3.175 +lemma finite_range_map_of: "finite (range (map_of l))"
   3.176 +apply (induct_tac "l")
   3.177 +apply  (simp_all (no_asm) add: image_constant)
   3.178 +apply (rule finite_subset)
   3.179 +prefer 2 apply (assumption)
   3.180 +apply auto
   3.181 +done
   3.182 +
   3.183 +lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
   3.184 +apply (induct_tac "xs")
   3.185 +apply auto
   3.186 +done
   3.187 +
   3.188 +
   3.189 +section "option_map related"
   3.190 +
   3.191 +lemma option_map_o_empty: "option_map f o empty = empty"
   3.192 +apply (rule ext)
   3.193 +apply (simp (no_asm))
   3.194 +done
   3.195 +
   3.196 +lemma option_map_o_map_upd: "option_map f o m(a|->b) = (option_map f o m)(a|->f b)"
   3.197 +apply (rule ext)
   3.198 +apply (simp (no_asm))
   3.199 +done
   3.200 +
   3.201 +declare option_map_o_empty [simp] option_map_o_map_upd [simp]
   3.202 +
   3.203 +
   3.204 +section "++"
   3.205 +
   3.206 +lemma override_empty: "m ++ empty = m"
   3.207 +apply (unfold override_def)
   3.208 +apply (simp (no_asm))
   3.209 +done
   3.210 +declare override_empty [simp]
   3.211 +
   3.212 +lemma empty_override: "empty ++ m = m"
   3.213 +apply (unfold override_def)
   3.214 +apply (rule ext)
   3.215 +apply (simp split add: option.split)
   3.216 +done
   3.217 +declare empty_override [simp]
   3.218 +
   3.219 +lemma override_Some_iff [rule_format (no_asm)]: 
   3.220 + "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)"
   3.221 +apply (unfold override_def)
   3.222 +apply (simp (no_asm) split add: option.split)
   3.223 +done
   3.224 +
   3.225 +lemmas override_SomeD = override_Some_iff [THEN iffD1, standard]
   3.226 +declare override_SomeD [dest!]
   3.227 +
   3.228 +lemma override_find_right: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
   3.229 +apply (subst override_Some_iff)
   3.230 +apply fast
   3.231 +done
   3.232 +declare override_find_right [simp]
   3.233 +
   3.234 +lemma override_None: "((m ++ n) k = None) = (n k = None & m k = None)"
   3.235 +apply (unfold override_def)
   3.236 +apply (simp (no_asm) split add: option.split)
   3.237 +done
   3.238 +declare override_None [iff]
   3.239 +
   3.240 +lemma override_upd: "f ++ g(x|->y) = (f ++ g)(x|->y)"
   3.241 +apply (unfold override_def)
   3.242 +apply (rule ext)
   3.243 +apply auto
   3.244 +done
   3.245 +declare override_upd [simp]
   3.246 +
   3.247 +lemma map_of_override: "map_of ys ++ map_of xs = map_of (xs@ys)"
   3.248 +apply (unfold override_def)
   3.249 +apply (rule sym)
   3.250 +apply (induct_tac "xs")
   3.251 +apply (simp (no_asm))
   3.252 +apply (rule ext)
   3.253 +apply (simp (no_asm_simp) split add: option.split)
   3.254 +done
   3.255 +declare map_of_override [simp]
   3.256 +
   3.257 +declare fun_upd_apply [simp del]
   3.258 +lemma finite_range_map_of_override: "finite (range f) ==> finite (range (f ++ map_of l))"
   3.259 +apply (induct_tac "l")
   3.260 +apply  auto
   3.261 +apply (erule finite_range_updI)
   3.262 +done
   3.263 +declare fun_upd_apply [simp]
   3.264 +
   3.265 +
   3.266 +section "dom"
   3.267 +
   3.268 +lemma domI: "m a = Some b ==> a : dom m"
   3.269 +apply (unfold dom_def)
   3.270 +apply auto
   3.271 +done
   3.272 +
   3.273 +lemma domD: "a : dom m ==> ? b. m a = Some b"
   3.274 +apply (unfold dom_def)
   3.275 +apply auto
   3.276 +done
   3.277 +
   3.278 +lemma domIff: "(a : dom m) = (m a ~= None)"
   3.279 +apply (unfold dom_def)
   3.280 +apply auto
   3.281 +done
   3.282 +declare domIff [iff]
   3.283 +declare domIff [simp del]
   3.284 +
   3.285 +lemma dom_empty: "dom empty = {}"
   3.286 +apply (unfold dom_def)
   3.287 +apply (simp (no_asm))
   3.288 +done
   3.289 +declare dom_empty [simp]
   3.290 +
   3.291 +lemma dom_map_upd: "dom(m(a|->b)) = insert a (dom m)"
   3.292 +apply (unfold dom_def)
   3.293 +apply (simp (no_asm))
   3.294 +apply blast
   3.295 +done
   3.296 +declare dom_map_upd [simp]
   3.297 +
   3.298 +lemma finite_dom_map_of: "finite (dom (map_of l))"
   3.299 +apply (unfold dom_def)
   3.300 +apply (induct_tac "l")
   3.301 +apply (auto simp add: insert_Collect [symmetric])
   3.302 +done
   3.303 +
   3.304 +lemma dom_override: "dom(m++n) = dom n Un dom m"
   3.305 +apply (unfold dom_def)
   3.306 +apply auto
   3.307 +done
   3.308 +declare dom_override [simp]
   3.309 +
   3.310 +section "ran"
   3.311 +
   3.312 +lemma ran_empty: "ran empty = {}"
   3.313 +apply (unfold ran_def)
   3.314 +apply (simp (no_asm))
   3.315 +done
   3.316 +declare ran_empty [simp]
   3.317 +
   3.318 +lemma ran_empty': "ran (%u. None) = {}"
   3.319 +apply (unfold ran_def)
   3.320 +apply auto
   3.321 +done
   3.322 +declare ran_empty' [simp]
   3.323 +
   3.324 +lemma ran_map_upd: "m a = None ==> ran(m(a|->b)) = insert b (ran m)"
   3.325 +apply (unfold ran_def)
   3.326 +apply auto
   3.327 +apply (subgoal_tac "~ (aa = a) ")
   3.328 +apply auto
   3.329 +done
   3.330 +declare ran_map_upd [simp]
   3.331 +
   3.332  end