# HG changeset patch
# User oheimb
# Date 902930667 -7200
# Node ID 2b1ca524ace80f291beb3e82b7646b11f0941be9
# Parent  d15a4155b96bda73c6e8c8c8daa73fc7980a8bf2
defined map_upd by translation via fun_upd
changed syntax of map_upd to be consistent with that of fun_upd
added chg_map, map_upds

diff -r d15a4155b96b -r 2b1ca524ace8 src/HOL/Map.ML
--- a/src/HOL/Map.ML	Wed Aug 12 15:40:47 1998 +0200
+++ b/src/HOL/Map.ML	Wed Aug 12 16:04:27 1998 +0200
@@ -6,23 +6,43 @@
 Map lemmas
 *)
 
+section "empty";
+
 Goalw [empty_def] "empty k = None";
 by (Simp_tac 1);
 qed "empty_def2";
 Addsimps [empty_def2];
 
-Goalw [map_upd_def] "(m[a|->b])x = (if x=a then Some b else m x)";
-by (Simp_tac 1);
-qed "map_upd_def2";
-Addsimps [map_upd_def2];
+
+section "map_upd";
+
+qed_goal "map_upd_triv" thy "!!X. t k = Some x ==> t(k|->x) = t"
+	(K [rtac ext 1, Asm_simp_tac 1]);
+(*Addsimps [map_upd_triv];*)
+
+
+section "map_upds";
 
-qed_goal "map_upd_same" thy "(t[k|->x]) k = Some x" 
-	(K [Simp_tac 1]);
-qed_goal "map_upd_other" thy "!!X. l~=k ==> (t[k|->x]) l = t l"
-	(K [Asm_simp_tac 1]);
-qed_goal "map_upd_triv" thy "!!X. t k = Some x ==> t[k|->x] = t"
-	(K [rtac ext 1, Asm_simp_tac 1]);
-(*Addsimps [map_upd_same, map_upd_other, map_upd_triv];*)
+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";
+
+qed_goalw "chg_map_new" thy [chg_map_def]
+	"!!s. m a = None   ==> chg_map f a m = m"          (K [Auto_tac]);
+qed_goalw "chg_map_upd" thy [chg_map_def]
+	"!!s. m a = Some b ==> chg_map f a m = m(a|->f b)" (K [Auto_tac]);
+Addsimps[chg_map_new, chg_map_upd];
+
 
 section "option_map";
 
@@ -30,10 +50,11 @@
          "option_map f o empty = empty" (K [rtac ext 1, Simp_tac 1]);
 
 qed_goal "option_map_o_map_upd" thy 
-	 "option_map f o m[a|->b] = (option_map f o m)[a|->f b]" 
+	 "option_map f o m(a|->b) = (option_map f o m)(a|->f b)" 
 	(K [rtac ext 1, Simp_tac 1]);
 Addsimps[option_map_o_empty, option_map_o_map_upd];
 
+
 section "++";
 
 Goalw [override_def] "m ++ empty = m";
@@ -77,6 +98,7 @@
 by (Asm_simp_tac 1);
 qed_spec_mp "map_of_SomeD";
 
+
 section "dom";
 
 Goalw [dom_def] "dom empty = {}";
@@ -84,7 +106,7 @@
 qed "dom_empty";
 Addsimps [dom_empty];
 
-Goalw [dom_def] "dom(m[a|->b]) = insert a (dom m)";
+Goalw [dom_def] "dom(m(a|->b)) = insert a (dom m)";
 by (Simp_tac 1);
 by (Blast_tac 1);
 qed "dom_map_upd";
@@ -108,7 +130,7 @@
 qed "ran_empty";
 Addsimps [ran_empty];
 
-Goalw [ran_def] "m a = None ==> ran(m[a|->b]) = insert b (ran m)";
+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;
diff -r d15a4155b96b -r 2b1ca524ace8 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Wed Aug 12 15:40:47 1998 +0200
+++ b/src/HOL/Map.thy	Wed Aug 12 16:04:27 1998 +0200
@@ -11,26 +11,38 @@
 types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
 
 consts
-empty   :: "'a ~=> 'b"
-map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
-           ("_/[_/|->/_]" [900,0,0] 900)
+empty	::  "'a ~=> 'b"
+chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
 override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
-dom     :: "('a ~=> 'b) => 'a set"
-ran     :: "('a ~=> 'b) => 'b set"
-map_of  :: "('a * 'b)list => 'a ~=> 'b"
+dom	:: "('a ~=> 'b) => 'a set"
+ran	:: "('a ~=> 'b) => 'b set"
+map_of	:: "('a * 'b)list => 'a ~=> 'b"
+map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
+	    ('a ~=> 'b)"			 ("_/'(_[|->]_/')" [900,0,0]900)
+
+
+syntax
+map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
+					         ("_/'(_/|->_')"   [900,0,0]900)
 
 syntax (symbols)
-  "~=>"     :: [type, type] => type
-               (infixr "\\<leadsto>" 0)
-  map_upd    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
-               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
+  "~=>"     :: [type, type] => type      (infixr "\\<leadsto>" 0)
+  map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
+					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)
+  map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
+				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
   override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
-               (infixl "\\<oplus>" 100)
+				         (infixl "\\<oplus>" 100)
+
+translations
+
+  "m(a|->b)" == "m(a:=Some b)"
 
 defs
-empty_def "empty == %x. None"
 
-map_upd_def "m[a|->b] == %x. if x=a then Some b else m x"
+empty_def    "empty == %x. None"
+
+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"
 
@@ -39,6 +51,9 @@
 
 primrec
   "map_of [] = empty"
-  "map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
+  "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
+
+primrec "t([]  [|->]bs) = t"
+        "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
 
 end