# HG changeset patch
# User webertj
# Date 1050095473 -7200
# Node ID 4bdfa9f7725461f1bb996e19bcc07a10354be038
# Parent  2bc462b99e709ad440a08a29f0d476aa4b82e255
Map.ML integrated into Map.thy

diff -r 2bc462b99e70 -r 4bdfa9f77254 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Apr 09 12:52:45 2003 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 11 23:11:13 2003 +0200
@@ -95,7 +95,7 @@
   Integ/NatSimprocs.thy Integ/int_arith1.ML Integ/int_arith2.ML \
   Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
   Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
-  Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
+  Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
   Nat.thy NatArith.ML NatArith.thy Numeral.thy \
   Power.ML Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML \
   Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
diff -r 2bc462b99e70 -r 4bdfa9f77254 src/HOL/Map.ML
--- a/src/HOL/Map.ML	Wed Apr 09 12:52:45 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,267 +0,0 @@
-(*  Title:      HOL/Map.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1997 TU Muenchen
-
-Map lemmas.
-*)
-
-section "empty";
-
-Goal "empty(x := None) = empty";
-by (rtac ext 1);
-by (Simp_tac 1);
-qed "empty_upd_none";
-Addsimps [empty_upd_none];
-
-(* FIXME: what is this sum_case nonsense?? *)
-Goal "sum_case empty empty = empty";
-by (rtac ext 1);
-by (simp_tac (simpset() addsplits [sum.split]) 1);
-qed "sum_case_empty_empty";
-Addsimps [sum_case_empty_empty];
-
-
-section "map_upd";
-
-Goal "t k = Some x ==> t(k|->x) = t";
-by (rtac ext 1);
-by (Asm_simp_tac 1);
-qed "map_upd_triv";
-
-Goal "t(k|->x) ~= empty";
-by Safe_tac;
-by (dres_inst_tac [("x","k")] fun_cong 1);
-by (Full_simp_tac 1);
-qed "map_upd_nonempty";
-Addsimps[map_upd_nonempty];
-
-Goalw [image_def] "finite (range f) ==> finite (range (f(a|->b)))";
-by (full_simp_tac (simpset() addsimps [full_SetCompr_eq]) 1);
-by (rtac finite_subset 1);
-by (assume_tac 2);
-by Auto_tac;
-qed "finite_range_updI";
-
-
-(* FIXME: what is this sum_case nonsense?? *)
-section "sum_case and empty/map_upd";
-
-Goal "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)";
-by (rtac ext 1);
-by (simp_tac (simpset() addsplits [sum.split]) 1);
-qed "sum_case_map_upd_empty";
-Addsimps[sum_case_map_upd_empty];
-
-Goal "sum_case empty (m(k|->y)) =  (sum_case empty m)(Inr k|->y)";
-by (rtac ext 1);
-by (simp_tac (simpset() addsplits [sum.split]) 1);
-qed "sum_case_empty_map_upd";
-Addsimps[sum_case_empty_map_upd];
-
-Goal "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)";
-by (rtac ext 1);
-by (simp_tac (simpset() addsplits [sum.split]) 1);
-qed "sum_case_map_upd_map_upd";
-Addsimps[sum_case_map_upd_map_upd];
-
-
-section "map_upds";
-
-Goal "a ~: set as --> (!m bs. (m(a|->b)(as[|->]bs)) = (m(as[|->]bs)(a|->b)))";
-by (induct_tac "as" 1);
-by  (auto_tac (claset(), simpset() delsimps[fun_upd_apply]));
-by (REPEAT(dtac spec 1));
-by (rotate_tac ~1 1);
-by (etac subst 1);
-by (etac (fun_upd_twist RS subst) 1);
-by (rtac refl 1);
-qed_spec_mp "map_upds_twist";
-Addsimps [map_upds_twist];
-
-
-section "chg_map";
-
-Goalw [chg_map_def] "m a = None   ==> chg_map f a m = m";
-by Auto_tac;
-qed "chg_map_new";
-
-Goalw [chg_map_def] "m a = Some b ==> chg_map f a m = m(a|->f b)";
-by Auto_tac;
-qed "chg_map_upd";
-
-Addsimps[chg_map_new, chg_map_upd];
-
-
-section "map_of";
-
-Goal "map_of xs k = Some y --> (k,y):set xs";
-by (induct_tac "xs" 1);
-by  Auto_tac;
-qed_spec_mp "map_of_SomeD";
-
-Goal "inj f ==> map_of t k = Some x --> \
-\  map_of (map (split (%k. Pair (f k))) t) (f k) = Some x";
-by (induct_tac "t" 1);
-by  (auto_tac (claset(),simpset()addsimps[inj_eq]));
-qed_spec_mp "map_of_mapk_SomeI";
-
-Goal "(k, x) : set l --> (? x. map_of l k = Some x)";
-by (induct_tac "l" 1);
-by  Auto_tac;
-qed_spec_mp "weak_map_of_SomeI";
-
-Goal 
-"[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z";
-by (rtac mp 1);
-by (atac 2);
-by (etac thin_rl 1);
-by (induct_tac "xs" 1);
-by  Auto_tac;
-qed "map_of_filter_in";
-
-Goal "finite (range (map_of l))";
-by (induct_tac "l" 1);
-by  (ALLGOALS (simp_tac (simpset() addsimps [image_constant])));
-by (rtac finite_subset 1);
-by (assume_tac 2);
-by Auto_tac;
-qed "finite_range_map_of";
-
-Goal "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "map_of_map";
-
-
-section "option_map related";
-
-Goal "option_map f o empty = empty";
-by (rtac ext 1);
-by (Simp_tac 1);
-qed "option_map_o_empty";
-
-Goal "option_map f o m(a|->b) = (option_map f o m)(a|->f b)";
-by (rtac ext 1);
-by (Simp_tac 1);
-qed "option_map_o_map_upd";
-
-Addsimps[option_map_o_empty, option_map_o_map_upd];
-
-
-section "++";
-
-Goalw [override_def] "m ++ empty = m";
-by (Simp_tac 1);
-qed "override_empty";
-Addsimps [override_empty];
-
-Goalw [override_def] "empty ++ m = m";
-by (Simp_tac 1);
-by (rtac ext 1);
-by (split_tac [option.split] 1);
-by (Simp_tac 1);
-qed "empty_override";
-Addsimps [empty_override];
-
-Goalw [override_def]
- "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
-by (simp_tac (simpset() addsplits [option.split]) 1);
-qed_spec_mp "override_Some_iff";
-
-bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
-AddSDs[override_SomeD];
-
-Goal "!!xx. n k = Some xx ==> (m ++ n) k = Some xx";
-by (stac override_Some_iff 1);
-by (Fast_tac 1);
-qed "override_find_right";
-Addsimps[override_find_right];
-
-Goalw [override_def] "((m ++ n) k = None) = (n k = None & m k = None)";
-by (simp_tac (simpset() addsplits [option.split]) 1);
-qed "override_None";
-AddIffs [override_None];
-
-Goalw [override_def] "f ++ g(x|->y) = (f ++ g)(x|->y)";
-by (rtac ext 1);
-by Auto_tac;
-qed "override_upd";
-Addsimps[override_upd];
-
-Goalw [override_def] "map_of ys ++ map_of xs = map_of (xs@ys)";
-by (rtac sym 1);
-by (induct_tac "xs" 1);
-by (Simp_tac 1);
-by (rtac ext 1);
-by (asm_simp_tac (simpset() addsplits [option.split]) 1);
-qed "map_of_override";
-Addsimps [map_of_override];
-
-Delsimps[fun_upd_apply];
-Goal "finite (range f) ==> finite (range (f ++ map_of l))";
-by (induct_tac "l" 1);
-by  Auto_tac;
-by  (fold_goals_tac [empty_def]);
-by  (Asm_simp_tac 1);
-by (etac finite_range_updI 1);
-qed "finite_range_map_of_override";
-Addsimps [fun_upd_apply];
-
-
-section "dom";
-
-Goalw [dom_def] "m a = Some b ==> a : dom m";
-by Auto_tac;
-qed "domI";
-
-Goalw [dom_def] "a : dom m ==> ? b. m a = Some b";
-by Auto_tac;
-qed "domD";
-
-Goalw [dom_def] "(a : dom m) = (m a ~= None)";
-by Auto_tac;
-qed "domIff";
-AddIffs [domIff];
-Delsimps [domIff];
-
-Goalw [dom_def] "dom empty = {}";
-by (Simp_tac 1);
-qed "dom_empty";
-Addsimps [dom_empty];
-
-Goalw [dom_def] "dom(m(a|->b)) = insert a (dom m)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "dom_map_upd";
-Addsimps [dom_map_upd];
-
-Goalw [dom_def] "finite (dom (map_of l))";
-by (induct_tac "l" 1);
-by (auto_tac (claset(),
-              simpset() addsimps [insert_Collect RS sym]));
-qed "finite_dom_map_of";
-
-Goalw [dom_def] "dom(m++n) = dom n Un dom m";
-by Auto_tac;
-qed "dom_override";
-Addsimps [dom_override];
-
-section "ran";
-
-Goalw [ran_def] "ran empty = {}";
-by (Simp_tac 1);
-qed "ran_empty";
-Addsimps [ran_empty];
-
-Goalw [ran_def] "ran (%u. None) = {}";
-by Auto_tac;
-qed "ran_empty'";
-Addsimps[ran_empty'];
-
-Goalw [ran_def] "m a = None ==> ran(m(a|->b)) = insert b (ran m)";
-by Auto_tac;
-by (subgoal_tac "~(aa = a)" 1);
-by Auto_tac;
-qed "ran_map_upd";
-Addsimps [ran_map_upd];
diff -r 2bc462b99e70 -r 4bdfa9f77254 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Wed Apr 09 12:52:45 2003 +0200
+++ b/src/HOL/Map.thy	Fri Apr 11 23:11:13 2003 +0200
@@ -1,14 +1,14 @@
 (*  Title:      HOL/Map.thy
     ID:         $Id$
     Author:     Tobias Nipkow, based on a theory by David von Oheimb
-    Copyright   1997 TU Muenchen
+    Copyright   1997-2003 TU Muenchen
 
 The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
 *)
 
-Map = List +
+theory Map = List:
 
-types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
+types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
 
 consts
 chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
@@ -24,11 +24,11 @@
 					         ("_/'(_/|->_')"   [900,0,0]900)
 
 syntax (xsymbols)
-  "~=>"     :: [type, type] => type      (infixr "\\<leadsto>" 0)
+  "~=>"     :: "[type, type] => type"    (infixr "\<leadsto>" 0)
   map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
-					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)
+					  ("_/'(_/\<mapsto>/_')"  [900,0,0]900)
   map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
-				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
+				         ("_/'(_/[\<mapsto>]/_')" [900,0,0]900)
 
 translations
   "empty"    => "_K None"
@@ -38,12 +38,12 @@
 
 defs
 
-chg_map_def  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
+chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
 
-override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
+override_def: "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
 
-dom_def "dom(m) == {a. m a ~= None}"
-ran_def "ran(m) == {b. ? a. m a = Some b}"
+dom_def: "dom(m) == {a. m a ~= None}"
+ran_def: "ran(m) == {b. ? a. m a = Some b}"
 
 primrec
   "map_of [] = empty"
@@ -52,4 +52,279 @@
 primrec "t([]  [|->]bs) = t"
         "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
 
+
+section "empty"
+
+lemma empty_upd_none: "empty(x := None) = empty"
+apply (rule ext)
+apply (simp (no_asm))
+done
+declare empty_upd_none [simp]
+
+(* FIXME: what is this sum_case nonsense?? *)
+lemma sum_case_empty_empty: "sum_case empty empty = empty"
+apply (rule ext)
+apply (simp (no_asm) split add: sum.split)
+done
+declare sum_case_empty_empty [simp]
+
+
+section "map_upd"
+
+lemma map_upd_triv: "t k = Some x ==> t(k|->x) = t"
+apply (rule ext)
+apply (simp (no_asm_simp))
+done
+
+lemma map_upd_nonempty: "t(k|->x) ~= empty"
+apply safe
+apply (drule_tac x = "k" in fun_cong)
+apply (simp (no_asm_use))
+done
+declare map_upd_nonempty [simp]
+
+lemma finite_range_updI: "finite (range f) ==> finite (range (f(a|->b)))"
+apply (unfold image_def)
+apply (simp (no_asm_use) add: full_SetCompr_eq)
+apply (rule finite_subset)
+prefer 2 apply (assumption)
+apply auto
+done
+
+
+(* FIXME: what is this sum_case nonsense?? *)
+section "sum_case and empty/map_upd"
+
+lemma sum_case_map_upd_empty: "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)"
+apply (rule ext)
+apply (simp (no_asm) split add: sum.split)
+done
+declare sum_case_map_upd_empty [simp]
+
+lemma sum_case_empty_map_upd: "sum_case empty (m(k|->y)) =  (sum_case empty m)(Inr k|->y)"
+apply (rule ext)
+apply (simp (no_asm) split add: sum.split)
+done
+declare sum_case_empty_map_upd [simp]
+
+lemma sum_case_map_upd_map_upd: "sum_case (m1(k1|->y1)) (m2(k2|->y2)) = (sum_case (m1(k1|->y1)) m2)(Inr k2|->y2)"
+apply (rule ext)
+apply (simp (no_asm) split add: sum.split)
+done
+declare sum_case_map_upd_map_upd [simp]
+
+
+section "map_upds"
+
+lemma map_upds_twist [rule_format (no_asm)]: "a ~: set as --> (!m bs. (m(a|->b)(as[|->]bs)) = (m(as[|->]bs)(a|->b)))"
+apply (induct_tac "as")
+apply  (auto simp del: fun_upd_apply)
+apply (drule spec)+
+apply (rotate_tac -1)
+apply (erule subst)
+apply (erule fun_upd_twist [THEN subst])
+apply (rule refl)
+done
+declare map_upds_twist [simp]
+
+
+section "chg_map"
+
+lemma chg_map_new: "m a = None   ==> chg_map f a m = m"
+apply (unfold chg_map_def)
+apply auto
+done
+
+lemma chg_map_upd: "m a = Some b ==> chg_map f a m = m(a|->f b)"
+apply (unfold chg_map_def)
+apply auto
+done
+
+declare chg_map_new [simp] chg_map_upd [simp]
+
+
+section "map_of"
+
+lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
+apply (induct_tac "xs")
+apply  auto
+done
+
+lemma map_of_mapk_SomeI [rule_format (no_asm)]: "inj f ==> map_of t k = Some x -->  
+   map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
+apply (induct_tac "t")
+apply  (auto simp add: inj_eq)
+done
+
+lemma weak_map_of_SomeI [rule_format (no_asm)]: "(k, x) : set l --> (? x. map_of l k = Some x)"
+apply (induct_tac "l")
+apply  auto
+done
+
+lemma map_of_filter_in: 
+"[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z"
+apply (rule mp)
+prefer 2 apply (assumption)
+apply (erule thin_rl)
+apply (induct_tac "xs")
+apply  auto
+done
+
+lemma finite_range_map_of: "finite (range (map_of l))"
+apply (induct_tac "l")
+apply  (simp_all (no_asm) add: image_constant)
+apply (rule finite_subset)
+prefer 2 apply (assumption)
+apply auto
+done
+
+lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
+apply (induct_tac "xs")
+apply auto
+done
+
+
+section "option_map related"
+
+lemma option_map_o_empty: "option_map f o empty = empty"
+apply (rule ext)
+apply (simp (no_asm))
+done
+
+lemma option_map_o_map_upd: "option_map f o m(a|->b) = (option_map f o m)(a|->f b)"
+apply (rule ext)
+apply (simp (no_asm))
+done
+
+declare option_map_o_empty [simp] option_map_o_map_upd [simp]
+
+
+section "++"
+
+lemma override_empty: "m ++ empty = m"
+apply (unfold override_def)
+apply (simp (no_asm))
+done
+declare override_empty [simp]
+
+lemma empty_override: "empty ++ m = m"
+apply (unfold override_def)
+apply (rule ext)
+apply (simp split add: option.split)
+done
+declare empty_override [simp]
+
+lemma override_Some_iff [rule_format (no_asm)]: 
+ "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)"
+apply (unfold override_def)
+apply (simp (no_asm) split add: option.split)
+done
+
+lemmas override_SomeD = override_Some_iff [THEN iffD1, standard]
+declare override_SomeD [dest!]
+
+lemma override_find_right: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
+apply (subst override_Some_iff)
+apply fast
+done
+declare override_find_right [simp]
+
+lemma override_None: "((m ++ n) k = None) = (n k = None & m k = None)"
+apply (unfold override_def)
+apply (simp (no_asm) split add: option.split)
+done
+declare override_None [iff]
+
+lemma override_upd: "f ++ g(x|->y) = (f ++ g)(x|->y)"
+apply (unfold override_def)
+apply (rule ext)
+apply auto
+done
+declare override_upd [simp]
+
+lemma map_of_override: "map_of ys ++ map_of xs = map_of (xs@ys)"
+apply (unfold override_def)
+apply (rule sym)
+apply (induct_tac "xs")
+apply (simp (no_asm))
+apply (rule ext)
+apply (simp (no_asm_simp) split add: option.split)
+done
+declare map_of_override [simp]
+
+declare fun_upd_apply [simp del]
+lemma finite_range_map_of_override: "finite (range f) ==> finite (range (f ++ map_of l))"
+apply (induct_tac "l")
+apply  auto
+apply (erule finite_range_updI)
+done
+declare fun_upd_apply [simp]
+
+
+section "dom"
+
+lemma domI: "m a = Some b ==> a : dom m"
+apply (unfold dom_def)
+apply auto
+done
+
+lemma domD: "a : dom m ==> ? b. m a = Some b"
+apply (unfold dom_def)
+apply auto
+done
+
+lemma domIff: "(a : dom m) = (m a ~= None)"
+apply (unfold dom_def)
+apply auto
+done
+declare domIff [iff]
+declare domIff [simp del]
+
+lemma dom_empty: "dom empty = {}"
+apply (unfold dom_def)
+apply (simp (no_asm))
+done
+declare dom_empty [simp]
+
+lemma dom_map_upd: "dom(m(a|->b)) = insert a (dom m)"
+apply (unfold dom_def)
+apply (simp (no_asm))
+apply blast
+done
+declare dom_map_upd [simp]
+
+lemma finite_dom_map_of: "finite (dom (map_of l))"
+apply (unfold dom_def)
+apply (induct_tac "l")
+apply (auto simp add: insert_Collect [symmetric])
+done
+
+lemma dom_override: "dom(m++n) = dom n Un dom m"
+apply (unfold dom_def)
+apply auto
+done
+declare dom_override [simp]
+
+section "ran"
+
+lemma ran_empty: "ran empty = {}"
+apply (unfold ran_def)
+apply (simp (no_asm))
+done
+declare ran_empty [simp]
+
+lemma ran_empty': "ran (%u. None) = {}"
+apply (unfold ran_def)
+apply auto
+done
+declare ran_empty' [simp]
+
+lemma ran_map_upd: "m a = None ==> ran(m(a|->b)) = insert b (ran m)"
+apply (unfold ran_def)
+apply auto
+apply (subgoal_tac "~ (aa = a) ")
+apply auto
+done
+declare ran_map_upd [simp]
+
 end