# HG changeset patch
# User nipkow
# Date 1052900529 -7200
# Node ID d9b155757dc892f45907bc1f5f09d08402faaf05
# Parent  213dcc39358faefae737f8e7d2eea67658e9eedf
*** empty log message ***

diff -r 213dcc39358f -r d9b155757dc8 src/HOL/Bali/Conform.thy
--- a/src/HOL/Bali/Conform.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/Bali/Conform.thy	Wed May 14 10:22:09 2003 +0200
@@ -225,9 +225,9 @@
 apply (unfold lconf_def)
 apply (induct_tac "vns")
 apply  clarsimp
-apply clarsimp
+apply clarify
 apply (frule list_all2_lengthD)
-apply clarsimp
+apply (clarsimp)
 done
 
 
@@ -308,7 +308,7 @@
 apply (unfold wlconf_def)
 apply (induct_tac "vns")
 apply  clarsimp
-apply clarsimp
+apply clarify
 apply (frule list_all2_lengthD)
 apply clarsimp
 done
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy	Wed May 14 10:22:09 2003 +0200
@@ -1650,7 +1650,7 @@
  "\<lbrakk>class G declC = Some c; ws_prog G;table_of (methods c) sig = Some m\<rbrakk> 
   \<Longrightarrow> methd G declC sig = Some (declC, m)"
 apply (simp only: methd_rec)
-apply (rule disjI1 [THEN override_Some_iff [THEN iffD2]])
+apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]])
 apply (auto elim: table_of_map_SomeI)
 done
 
@@ -1764,7 +1764,7 @@
 apply (erule_tac ws_subcls1_induct, assumption)
 apply (subst methd_rec)
 apply (assumption)
-apply (auto intro!: finite_range_map_of finite_range_filter_tab finite_range_map_of_override)
+apply (auto intro!: finite_range_map_of finite_range_filter_tab finite_range_map_of_map_add)
 done
 
 lemma finite_dom_methd:
@@ -1880,7 +1880,7 @@
 	 case True
 	 with subclseq_dynC_statC statM dynmethd_dynC_def
 	 have "?Dynmethd_def dynC sig = Some statM"
-	   by (auto intro: override_find_right filter_tab_SomeI)
+	   by (auto intro: map_add_find_right filter_tab_SomeI)
 	 with subclseq_dynC_statC True Some 
 	 show ?thesis
 	   by auto
@@ -2201,8 +2201,8 @@
  \<Longrightarrow> table_of (fields G fd) (fn,fd) = Some f"
 apply (subst fields_rec)
 apply assumption+
-apply (subst map_of_override [symmetric])
-apply (rule disjI1 [THEN override_Some_iff [THEN iffD2]])
+apply (subst map_of_append)
+apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]])
 apply (auto elim: table_of_map2_SomeI)
 done
 
@@ -2222,9 +2222,9 @@
 apply (rule ws_subcls1_induct, assumption, assumption)
 apply (subst fields_rec, assumption)
 apply clarify
-apply (simp only: map_of_override [symmetric] del: map_of_override)
+apply (simp only: map_of_append)
 apply (case_tac "table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn") 
-apply   (force intro:rtrancl_into_rtrancl2 simp add: override_def)
+apply   (force intro:rtrancl_into_rtrancl2 simp add: map_add_def)
 
 apply   (frule_tac fd="Ca" in fields_norec)
 apply     assumption
@@ -2232,7 +2232,7 @@
 apply   (frule table_of_fieldsD)  
 apply   (frule_tac n="table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c))"
               and  m="table_of (if Ca = Object then [] else fields G (super c))"
-         in override_find_right)
+         in map_add_find_right)
 apply   (case_tac "efn")
 apply   (simp)
 done
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/Bali/Table.thy	Wed May 14 10:22:09 2003 +0200
@@ -49,9 +49,9 @@
   (type)"('a, 'b) table" <= (type)"'a \<leadsto> 'b"
 
 (* ### To map *)
-lemma override_find_left[simp]:
+lemma map_add_find_left[simp]:
 "n k = None \<Longrightarrow> (m ++ n) k = m k"
-by (simp add: override_def)
+by (simp add: map_add_def)
 
 section {* Conditional Override *}
 constdefs
@@ -278,8 +278,8 @@
 
 lemma table_append_Some_iff: "table_of (xs@ys) k = Some z = 
  (table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))"
-apply (simp only: map_of_override [THEN sym])
-apply (rule override_Some_iff)
+apply (simp)
+apply (rule map_add_Some_iff)
 done
 
 lemma table_of_filter_unique_SomeD [rule_format (no_asm)]:
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/Bali/WellForm.thy	Wed May 14 10:22:09 2003 +0200
@@ -1514,7 +1514,7 @@
         methd G (super c) sig = Some old\<rbrakk> 
     \<Longrightarrow> methd G C sig = Some (C,new)"
 by (auto simp add: methd_rec
-            intro: filter_tab_SomeI override_find_right table_of_map_SomeI)
+            intro: filter_tab_SomeI map_add_find_right table_of_map_SomeI)
 
 lemma wf_prog_staticD:
   assumes     wf: "wf_prog G" and
@@ -1667,8 +1667,7 @@
 	    by (auto simp add: inherits_def)
 	  with clsC ws no_new super neq_C_Obj
 	  have "methd G C sig = Some super_method"
-	    by (auto simp add: methd_rec override_def
-	                intro: filter_tab_SomeI)
+	    by (auto simp add: methd_rec map_add_def intro: filter_tab_SomeI)
           with None show ?thesis
 	    by simp
 	qed
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Wed May 14 10:22:09 2003 +0200
@@ -658,6 +658,7 @@
 apply simp
 done
 
+declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
 lemma Seq_sound1 [rule_format]: 
   "x\<in> cptn_mod \<Longrightarrow> \<forall>s P. x !0=(Some (Seq P Q), s) \<longrightarrow> 
   (\<forall>i<length x. fst(x!i)\<noteq>Some Q) \<longrightarrow> 
@@ -670,8 +671,7 @@
     apply(rule_tac x="[(Some Pa, sa)]" in exI,simp add:CptnOne)
    apply(subgoal_tac "(\<forall>i < Suc (length xs). fst (((Some (Seq Pa Q), t) # xs) ! i) \<noteq> Some Q)")
     apply clarify
-    apply(case_tac xsa,simp,simp)
-    apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
+    apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # zs" in exI,simp)
     apply(rule conjI,erule CptnEnv)
     apply(simp (no_asm_use) add:lift_def)
    apply clarify
@@ -686,6 +686,7 @@
  apply(simp add:lift_def)
 apply simp
 done
+declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
 
 lemma Seq_sound2 [rule_format]: 
   "x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x 
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/IsaMakefile	Wed May 14 10:22:09 2003 +0200
@@ -10,11 +10,11 @@
 images: HOL HOL-Algebra HOL-Complex TLA
 
 #Note: keep targets sorted (except for HOL-Library)
+#  HOL-Bali
 test: \
   HOL-Library \
   HOL-Auth \
   HOL-AxClasses \
-  HOL-Bali \
   HOL-Complex-ex \
   HOL-CTL \
   HOL-Extraction \
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/List.ML
--- a/src/HOL/List.ML	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/List.ML	Wed May 14 10:22:09 2003 +0200
@@ -156,7 +156,7 @@
 val map_compose = thm "map_compose";
 val map_concat = thm "map_concat";
 val map_cong = thm "map_cong";
-val map_eq_Cons = thm "map_eq_Cons";
+val map_eq_Cons_conv = thm "map_eq_Cons_conv";
 val map_ext = thm "map_ext";
 val map_ident = thm "map_ident";
 val map_injective = thm "map_injective";
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/List.thy	Wed May 14 10:22:09 2003 +0200
@@ -269,6 +269,14 @@
 "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
 by (induct xs) auto
 
+lemma Suc_length_conv:
+"(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
+apply (induct xs)
+ apply simp
+apply simp
+apply blast
+done
+
 
 subsection {* @{text "@"} -- append *}
 
@@ -441,13 +449,17 @@
 lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"
 by (cases xs) auto
 
-lemma map_eq_Cons:
-"(map f xs = y # ys) = (\<exists>x xs'. xs = x # xs' \<and> f x = y \<and> map f xs' = ys)"
+lemma map_eq_Cons_conv[iff]:
+ "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"
 by (cases xs) auto
 
+lemma Cons_eq_map_conv[iff]:
+ "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
+by (cases ys) auto
+
 lemma map_injective:
-"!!xs. map f xs = map f ys ==> (\<forall>x y. f x = f y --> x = y) ==> xs = ys"
-by (induct ys) (auto simp add: map_eq_Cons)
+ "!!xs. map f xs = map f ys ==> (\<forall>x y. f x = f y --> x = y) ==> xs = ys"
+by (induct ys) auto
 
 lemma inj_mapI: "inj f ==> inj (map f)"
 by (rules dest: map_injective injD intro: inj_onI)
@@ -858,6 +870,12 @@
  apply auto
 done
 
+lemma set_take_subset: "\<And>n. set(take n xs) \<subseteq> set xs"
+by(induct xs)(auto simp:take_Cons split:nat.split)
+
+lemma set_drop_subset: "\<And>n. set(drop n xs) \<subseteq> set xs"
+by(induct xs)(auto simp:drop_Cons split:nat.split)
+
 lemma append_eq_conv_conj:
 "!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
 apply(induct xs)
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/Map.thy	Wed May 14 10:22:09 2003 +0200
@@ -14,7 +14,7 @@
 
 consts
 chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
-override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
+map_add:: "('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"
@@ -43,10 +43,12 @@
 defs
 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"
+map_add_def: "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
+
+map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
 
 dom_def: "dom(m) == {a. m a ~= None}"
-ran_def: "ran(m) == {b. ? a. m a = Some b}"
+ran_def: "ran(m) == {b. EX a. m a = Some b}"
 
 map_le_def: "m1 \<subseteq>\<^sub>m m2  ==  ALL a : dom m1. m1 a = m2 a"
 
@@ -54,9 +56,6 @@
   "map_of [] = empty"
   "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)"
-
 
 subsection {* empty *}
 
@@ -116,27 +115,6 @@
 done
 
 
-subsection {* map\_upds *}
-
-lemma map_upd_upds_conv_if:
- "!!x y ys f. (f(x|->y))(xs [|->] ys) =
-              (if x : set xs then f(xs [|->] ys) else (f(xs [|->] ys))(x|->y))"
-apply(induct xs)
- apply simp
-apply(simp split:split_if add:fun_upd_twist eq_sym_conv)
-done
-
-lemma map_upds_twist [simp]:
- "a ~: set as ==> m(a|->b)(as[|->]bs) = m(as[|->]bs)(a|->b)"
-by (simp add: map_upd_upds_conv_if)
-
-lemma map_upds_apply_nontin[simp]:
- "!!ys. x ~: set xs ==> (f(xs[|->]ys)) x = f x"
-apply(induct xs)
- apply simp
-apply(simp add: fun_upd_apply map_upd_upds_conv_if split:split_if)
-done
-
 subsection {* chg\_map *}
 
 lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
@@ -207,45 +185,49 @@
 
 subsection {* ++ *}
 
-lemma override_empty[simp]: "m ++ empty = m"
-apply (unfold override_def)
+lemma map_add_empty[simp]: "m ++ empty = m"
+apply (unfold map_add_def)
 apply (simp (no_asm))
 done
 
-lemma empty_override[simp]: "empty ++ m = m"
-apply (unfold override_def)
+lemma empty_map_add[simp]: "empty ++ m = m"
+apply (unfold map_add_def)
 apply (rule ext)
 apply (simp split add: option.split)
 done
 
-lemma override_Some_iff [rule_format (no_asm)]: 
+lemma map_add_assoc[simp]: "m1 ++ (m2 ++ m3) = (m1 ++ m2) ++ m3"
+apply(rule ext)
+apply(simp add: map_add_def split:option.split)
+done
+
+lemma map_add_Some_iff: 
  "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)"
-apply (unfold override_def)
+apply (unfold map_add_def)
 apply (simp (no_asm) split add: option.split)
 done
 
-lemmas override_SomeD = override_Some_iff [THEN iffD1, standard]
-declare override_SomeD [dest!]
+lemmas map_add_SomeD = map_add_Some_iff [THEN iffD1, standard]
+declare map_add_SomeD [dest!]
 
-lemma override_find_right[simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
-apply (subst override_Some_iff)
+lemma map_add_find_right[simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
+apply (subst map_add_Some_iff)
 apply fast
 done
 
-lemma override_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
-apply (unfold override_def)
+lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
+apply (unfold map_add_def)
 apply (simp (no_asm) split add: option.split)
 done
 
-lemma override_upd[simp]: "f ++ g(x|->y) = (f ++ g)(x|->y)"
-apply (unfold override_def)
+lemma map_add_upd[simp]: "f ++ g(x|->y) = (f ++ g)(x|->y)"
+apply (unfold map_add_def)
 apply (rule ext)
 apply auto
 done
 
-lemma map_of_override[simp]: "map_of ys ++ map_of xs = map_of (xs@ys)"
-apply (unfold override_def)
-apply (rule sym)
+lemma map_of_append[simp]: "map_of (xs@ys) = map_of ys ++ map_of xs"
+apply (unfold map_add_def)
 apply (induct_tac "xs")
 apply (simp (no_asm))
 apply (rule ext)
@@ -253,7 +235,8 @@
 done
 
 declare fun_upd_apply [simp del]
-lemma finite_range_map_of_override: "finite (range f) ==> finite (range (f ++ map_of l))"
+lemma finite_range_map_of_map_add:
+ "finite (range f) ==> finite (range (f ++ map_of l))"
 apply (induct_tac "l")
 apply  auto
 apply (erule finite_range_updI)
@@ -261,6 +244,42 @@
 declare fun_upd_apply [simp]
 
 
+subsection {* map\_upds *}
+
+lemma map_upds_Nil1[simp]: "m([] [|->] bs) = m"
+by(simp add:map_upds_def)
+
+lemma map_upds_Nil2[simp]: "m(as [|->] []) = m"
+by(simp add:map_upds_def)
+
+lemma map_upds_Cons[simp]: "m(a#as [|->] b#bs) = (m(a|->b))(as[|->]bs)"
+by(simp add:map_upds_def)
+
+
+lemma map_upd_upds_conv_if: "!!x y ys f.
+ (f(x|->y))(xs [|->] ys) =
+ (if x : set(take (length ys) xs) then f(xs [|->] ys)
+                                  else (f(xs [|->] ys))(x|->y))"
+apply(induct xs)
+ apply simp
+apply(case_tac ys)
+ apply(auto split:split_if simp:fun_upd_twist)
+done
+
+lemma map_upds_twist [simp]:
+ "a ~: set as ==> m(a|->b)(as[|->]bs) = m(as[|->]bs)(a|->b)"
+apply(insert set_take_subset)
+apply (fastsimp simp add: map_upd_upds_conv_if)
+done
+
+lemma map_upds_apply_nontin[simp]:
+ "!!ys. x ~: set xs ==> (f(xs[|->]ys)) x = f x"
+apply(induct xs)
+ apply simp
+apply(case_tac ys)
+ apply(auto simp: map_upd_upds_conv_if)
+done
+
 subsection {* dom *}
 
 lemma domI: "m a = Some b ==> a : dom m"
@@ -287,13 +306,6 @@
 lemma dom_fun_upd[simp]:
  "dom(f(x := y)) = (if y=None then dom f - {x} else insert x (dom f))"
 by (simp add:dom_def) blast
-(*
-lemma dom_map_upd[simp]: "dom(m(a|->b)) = insert a (dom m)"
-apply (unfold dom_def)
-apply (simp (no_asm))
-apply blast
-done
-*)
 
 lemma dom_map_of: "dom(map_of xys) = {x. \<exists>y. (x,y) : set xys}"
 apply(induct xys)
@@ -306,10 +318,15 @@
 apply (auto simp add: insert_Collect [symmetric])
 done
 
-lemma dom_map_upds[simp]: "!!m vs. dom(m(xs[|->]vs)) = set xs Un dom m"
-by(induct xs, simp_all)
+lemma dom_map_upds[simp]:
+ "!!m ys. dom(m(xs[|->]ys)) = set(take (length ys) xs) Un dom m"
+apply(induct xs)
+ apply simp
+apply(case_tac ys)
+ apply auto
+done
 
-lemma dom_override[simp]: "dom(m++n) = dom n Un dom m"
+lemma dom_map_add[simp]: "dom(m++n) = dom n Un dom m"
 apply (unfold dom_def)
 apply auto
 done
@@ -342,6 +359,10 @@
 
 lemma map_le_upds[simp]:
  "!!f g bs. f \<subseteq>\<^sub>m g ==> f(as [|->] bs) \<subseteq>\<^sub>m g(as [|->] bs)"
-by(induct as, auto)
+apply(induct as)
+ apply simp
+apply(case_tac bs)
+ apply auto
+done
 
 end
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed May 14 10:22:09 2003 +0200
@@ -600,7 +600,7 @@
     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
     G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (clarsimp simp add: defs1)
 apply (blast intro: approx_loc_imp_approx_val_sup)
 done
 
@@ -612,7 +612,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (clarsimp simp add: defs1)
 apply (blast intro: approx_loc_subst)
 done
 
@@ -625,7 +625,7 @@
     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
     G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
-apply (clarsimp simp add: defs1 sup_PTS_eq map_eq_Cons)
+apply (clarsimp simp add: defs1 sup_PTS_eq)
 apply (blast dest: conf_litval intro: conf_widen)
 done
 
@@ -654,7 +654,7 @@
     G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
     fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 wt_jvm_prog_def map_eq_Cons split: split_if_asm)
+apply (clarsimp simp add: defs2 wt_jvm_prog_def split: split_if_asm)
 apply (blast intro: Cast_conf2)
 done
 
@@ -668,7 +668,7 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def split_beta
+apply (clarsimp simp add: defs2 wt_jvm_prog_def split_beta
                 split: option.split split_if_asm)
 apply (frule conf_widen)
 apply assumption+
@@ -779,7 +779,7 @@
   from hp frame less suc_pc wf
   have "correct_frame G ?hp' (ST', LT') maxl ins ?f"
     apply (unfold correct_frame_def sup_state_conv)
-    apply (clarsimp simp add: map_eq_Cons conf_def fun_upd_apply approx_val_def)
+    apply (clarsimp simp add: conf_def fun_upd_apply approx_val_def)
     apply (blast intro: approx_stk_sup_heap approx_loc_sup_heap sup)
     done      
   moreover
@@ -1082,7 +1082,7 @@
     proof -
       from wf hd_stk' len stk' less ST0
       have "approx_stk G hp (hd stk # drop (1+length pt) stk') ST''" 
-        by (auto simp add: map_eq_Cons sup_state_conv
+        by (auto simp add: sup_state_conv
                  dest!: approx_stk_append elim: conf_widen)
       moreover
       from wf loc' less
@@ -1147,7 +1147,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 map_eq_Cons)
+apply (clarsimp simp add: defs2)
 apply (blast intro: conf_widen)
 done
 
@@ -1159,7 +1159,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 map_eq_Cons)
+apply (clarsimp simp add: defs2)
 apply (blast intro: conf_widen)
 done
 
@@ -1171,7 +1171,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 map_eq_Cons)
+apply (clarsimp simp add: defs2)
 apply (blast intro: conf_widen)
 done
 
@@ -1183,7 +1183,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 map_eq_Cons)
+apply (clarsimp simp add: defs2)
 apply (blast intro: conf_widen)
 done
 
@@ -1195,7 +1195,7 @@
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 map_eq_Cons approx_val_def conf_def)
+apply (clarsimp simp add: defs2 approx_val_def conf_def)
 apply blast
 done
 
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Wed May 14 10:22:09 2003 +0200
@@ -130,7 +130,7 @@
     next
       case Store
       with G app show ?thesis
-        by (cases s2, auto simp add: map_eq_Cons sup_loc_Cons2 sup_state_conv)
+        by (cases s2, auto simp add: sup_loc_Cons2 sup_state_conv)
     next
       case LitPush
       with G app show ?thesis by (cases s2, auto simp add: sup_state_conv)
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Wed May 14 10:22:09 2003 +0200
@@ -387,12 +387,12 @@
 theorem sup_state_Cons1:
   "(G \<turnstile> (x#xt, a) <=s (yt, b)) = 
    (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
-  by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def map_eq_Cons)
+  by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def)
 
 theorem sup_state_Cons2:
   "(G \<turnstile> (xt, a) <=s (y#yt, b)) = 
    (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
-  by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def map_eq_Cons sup_loc_Cons2)
+  by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_Cons2)
 
 theorem sup_state_ignore_fst:  
   "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/MicroJava/Comp/AuxLemmas.thy
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Wed May 14 10:22:09 2003 +0200
@@ -101,17 +101,9 @@
 
 lemma map_map_upds [rule_format (no_asm), simp]: 
 "\<forall> f vs. (\<forall>y\<in>set ys. y \<notin> set xs) \<longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs"
-apply (induct ys)
-apply simp
-apply (intro strip)
-apply (simp only: map_upds.simps)
-apply (subgoal_tac "\<forall>y\<in>set list. y \<notin> set xs")
-apply (subgoal_tac "a\<notin> set xs")
-apply (subgoal_tac "map (the \<circ> f(a\<mapsto>hd vs)(list[\<mapsto>]tl vs)) xs = map (the \<circ> f(a\<mapsto>hd vs)) xs")
-apply (simp only:)
-apply (erule map_map_upd)
-apply blast
-apply simp+
+apply (induct xs)
+ apply simp
+apply fastsimp
 done
 
 lemma map_upds_distinct [rule_format (no_asm), simp]: 
@@ -121,11 +113,10 @@
 apply (intro strip)
 apply (case_tac vs)
 apply simp
-apply (simp only: map_upds.simps distinct.simps hd.simps tl.simps)
+apply (simp only: map_upds_Cons distinct.simps hd.simps tl.simps map.simps)
 apply clarify
-apply (simp only: map.simps map_map_upd)
+apply (simp del: o_apply)
 apply simp
-apply (simp add: o_def)
 done
 
 
@@ -138,7 +129,8 @@
   "\<forall> m ys. (m(xs[\<mapsto>]ys)) k = Some y \<longrightarrow> k \<in> (set xs) \<or> (m k = Some y)"
 apply (induct xs)
 apply simp
-apply (case_tac "k = a")
+apply auto
+apply(case_tac ys)
 apply auto
 done
 
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Wed May 14 10:22:09 2003 +0200
@@ -300,7 +300,7 @@
 apply (subst method_rec) apply simp
 apply force
 apply assumption
-apply (simp only: override_def)
+apply (simp only: map_add_def)
 apply (split option.split)
 apply (rule conjI)
 apply force
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed May 14 10:22:09 2003 +0200
@@ -81,7 +81,7 @@
 apply (rule allI)
 apply (drule_tac x="a # ys" in spec)
 apply (simp only: rev.simps append_assoc append_Cons append_Nil
-  map.simps map_of.simps map_upds.simps hd.simps tl.simps)
+  map.simps map_of.simps map_upds_Cons hd.simps tl.simps)
 done
 
 lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\<mapsto>] (map snd xs))"
@@ -90,7 +90,8 @@
 lemma map_of_rev: "unique xs \<Longrightarrow> map_of (rev xs) = map_of xs"
 apply (induct xs)
 apply simp
-apply (simp add: unique_def map_of_append map_of_as_map_upds [THEN sym])
+apply (simp add: unique_def map_of_append map_of_as_map_upds [THEN sym]
+                 Map.map_of_append[symmetric] del:Map.map_of_append)
 done
 
 lemma map_upds_rev [rule_format]: "\<forall> xs. (distinct ks \<longrightarrow> length ks = length xs 
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed May 14 10:22:09 2003 +0200
@@ -254,7 +254,7 @@
 apply (rule inv_f_eq) apply (simp add: inj_on_def) apply simp
 
 apply (intro strip)
-apply (simp add: override_Some_iff map_of_map del: split_paired_Ex)
+apply (simp add: map_add_Some_iff map_of_map del: split_paired_Ex)
 apply (subgoal_tac "\<forall>x\<in>set ms. fst ((Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x")
 (*
 apply (subgoal_tac "\<forall>x\<in>set ms. fst (((\<lambda>(s, m). (s, Ca, m)) \<circ> compMethod G Ca) x) = fst x")
@@ -329,14 +329,14 @@
 apply (case_tac "(method (G, D) ++  map_of (map (\<lambda>(s, m). (s, C, m)) ms)) S")
 
   (* case None *)
-apply (simp (no_asm_simp) add: override_None)
+apply (simp (no_asm_simp) add: map_add_None)
 apply (simp add: map_of_map_compMethod comp_method_result_def) 
 
   (* case Some *)
-apply (simp add: override_Some_iff)
+apply (simp add: map_add_Some_iff)
 apply (erule disjE)
   apply (simp add: split_beta map_of_map_compMethod)
-  apply (simp add: override_def comp_method_result_def map_of_map_compMethod)
+  apply (simp add: map_add_def comp_method_result_def map_of_map_compMethod)
 
   (* show subgoals *)
 apply (simp add: comp_subcls1) 
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed May 14 10:22:09 2003 +0200
@@ -398,4 +398,3 @@
 
 end
 
-
diff -r 213dcc39358f -r d9b155757dc8 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed May 14 10:22:09 2003 +0200
@@ -324,7 +324,7 @@
 apply(  assumption)
 apply( rotate_tac -1)
 apply( simp)
-apply( drule override_SomeD)
+apply( drule map_add_SomeD)
 apply( erule disjE)
 apply(  erule_tac V = "?P --> ?Q" in thin_rl)
 apply (frule map_of_SomeD)
@@ -368,7 +368,7 @@
 apply( clarify)
 apply( subst method_rec)
 apply(  assumption)
-apply( unfold override_def)
+apply( unfold map_add_def)
 apply( simp (no_asm_simp) del: split_paired_Ex)
 apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z")
 apply(  erule exE)
@@ -412,7 +412,7 @@
  apply (subst method_rec)
    apply (assumption)
   apply (assumption)
- apply (simp add: override_def map_of_map split add: option.split)
+ apply (simp add: map_add_def map_of_map split add: option.split)
 done
 
 
@@ -453,7 +453,7 @@
 
 apply clarify
 apply (subgoal_tac "((field (G, D)) ++ map_of (map (\<lambda>(s, f). (s, C, f)) fs)) vn = Some (Da, T)")
-apply (simp (no_asm_use) only:  override_Some_iff)
+apply (simp (no_asm_use) only: map_add_Some_iff)
 apply (erule disjE)
 apply (simp (no_asm_use) add: map_of_map) apply blast
 apply blast