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
--- 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;
--- 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