*** empty log message ***
authornipkow
Wed May 14 10:22:09 2003 +0200 (2003-05-14)
changeset 14025d9b155757dc8
parent 14024 213dcc39358f
child 14026 c031a330a03f
*** empty log message ***
src/HOL/Bali/Conform.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/Table.thy
src/HOL/Bali/WellForm.thy
src/HOL/HoareParallel/RG_Hoare.thy
src/HOL/IsaMakefile
src/HOL/List.ML
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/BV/EffectMono.thy
src/HOL/MicroJava/BV/JVMType.thy
src/HOL/MicroJava/Comp/AuxLemmas.thy
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/MicroJava/Comp/LemmasComp.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/MicroJava/J/WellForm.thy
     1.1 --- a/src/HOL/Bali/Conform.thy	Tue May 13 08:59:21 2003 +0200
     1.2 +++ b/src/HOL/Bali/Conform.thy	Wed May 14 10:22:09 2003 +0200
     1.3 @@ -225,9 +225,9 @@
     1.4  apply (unfold lconf_def)
     1.5  apply (induct_tac "vns")
     1.6  apply  clarsimp
     1.7 -apply clarsimp
     1.8 +apply clarify
     1.9  apply (frule list_all2_lengthD)
    1.10 -apply clarsimp
    1.11 +apply (clarsimp)
    1.12  done
    1.13  
    1.14  
    1.15 @@ -308,7 +308,7 @@
    1.16  apply (unfold wlconf_def)
    1.17  apply (induct_tac "vns")
    1.18  apply  clarsimp
    1.19 -apply clarsimp
    1.20 +apply clarify
    1.21  apply (frule list_all2_lengthD)
    1.22  apply clarsimp
    1.23  done
     2.1 --- a/src/HOL/Bali/DeclConcepts.thy	Tue May 13 08:59:21 2003 +0200
     2.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed May 14 10:22:09 2003 +0200
     2.3 @@ -1650,7 +1650,7 @@
     2.4   "\<lbrakk>class G declC = Some c; ws_prog G;table_of (methods c) sig = Some m\<rbrakk> 
     2.5    \<Longrightarrow> methd G declC sig = Some (declC, m)"
     2.6  apply (simp only: methd_rec)
     2.7 -apply (rule disjI1 [THEN override_Some_iff [THEN iffD2]])
     2.8 +apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]])
     2.9  apply (auto elim: table_of_map_SomeI)
    2.10  done
    2.11  
    2.12 @@ -1764,7 +1764,7 @@
    2.13  apply (erule_tac ws_subcls1_induct, assumption)
    2.14  apply (subst methd_rec)
    2.15  apply (assumption)
    2.16 -apply (auto intro!: finite_range_map_of finite_range_filter_tab finite_range_map_of_override)
    2.17 +apply (auto intro!: finite_range_map_of finite_range_filter_tab finite_range_map_of_map_add)
    2.18  done
    2.19  
    2.20  lemma finite_dom_methd:
    2.21 @@ -1880,7 +1880,7 @@
    2.22  	 case True
    2.23  	 with subclseq_dynC_statC statM dynmethd_dynC_def
    2.24  	 have "?Dynmethd_def dynC sig = Some statM"
    2.25 -	   by (auto intro: override_find_right filter_tab_SomeI)
    2.26 +	   by (auto intro: map_add_find_right filter_tab_SomeI)
    2.27  	 with subclseq_dynC_statC True Some 
    2.28  	 show ?thesis
    2.29  	   by auto
    2.30 @@ -2201,8 +2201,8 @@
    2.31   \<Longrightarrow> table_of (fields G fd) (fn,fd) = Some f"
    2.32  apply (subst fields_rec)
    2.33  apply assumption+
    2.34 -apply (subst map_of_override [symmetric])
    2.35 -apply (rule disjI1 [THEN override_Some_iff [THEN iffD2]])
    2.36 +apply (subst map_of_append)
    2.37 +apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]])
    2.38  apply (auto elim: table_of_map2_SomeI)
    2.39  done
    2.40  
    2.41 @@ -2222,9 +2222,9 @@
    2.42  apply (rule ws_subcls1_induct, assumption, assumption)
    2.43  apply (subst fields_rec, assumption)
    2.44  apply clarify
    2.45 -apply (simp only: map_of_override [symmetric] del: map_of_override)
    2.46 +apply (simp only: map_of_append)
    2.47  apply (case_tac "table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn") 
    2.48 -apply   (force intro:rtrancl_into_rtrancl2 simp add: override_def)
    2.49 +apply   (force intro:rtrancl_into_rtrancl2 simp add: map_add_def)
    2.50  
    2.51  apply   (frule_tac fd="Ca" in fields_norec)
    2.52  apply     assumption
    2.53 @@ -2232,7 +2232,7 @@
    2.54  apply   (frule table_of_fieldsD)  
    2.55  apply   (frule_tac n="table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c))"
    2.56                and  m="table_of (if Ca = Object then [] else fields G (super c))"
    2.57 -         in override_find_right)
    2.58 +         in map_add_find_right)
    2.59  apply   (case_tac "efn")
    2.60  apply   (simp)
    2.61  done
     3.1 --- a/src/HOL/Bali/Table.thy	Tue May 13 08:59:21 2003 +0200
     3.2 +++ b/src/HOL/Bali/Table.thy	Wed May 14 10:22:09 2003 +0200
     3.3 @@ -49,9 +49,9 @@
     3.4    (type)"('a, 'b) table" <= (type)"'a \<leadsto> 'b"
     3.5  
     3.6  (* ### To map *)
     3.7 -lemma override_find_left[simp]:
     3.8 +lemma map_add_find_left[simp]:
     3.9  "n k = None \<Longrightarrow> (m ++ n) k = m k"
    3.10 -by (simp add: override_def)
    3.11 +by (simp add: map_add_def)
    3.12  
    3.13  section {* Conditional Override *}
    3.14  constdefs
    3.15 @@ -278,8 +278,8 @@
    3.16  
    3.17  lemma table_append_Some_iff: "table_of (xs@ys) k = Some z = 
    3.18   (table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))"
    3.19 -apply (simp only: map_of_override [THEN sym])
    3.20 -apply (rule override_Some_iff)
    3.21 +apply (simp)
    3.22 +apply (rule map_add_Some_iff)
    3.23  done
    3.24  
    3.25  lemma table_of_filter_unique_SomeD [rule_format (no_asm)]:
     4.1 --- a/src/HOL/Bali/WellForm.thy	Tue May 13 08:59:21 2003 +0200
     4.2 +++ b/src/HOL/Bali/WellForm.thy	Wed May 14 10:22:09 2003 +0200
     4.3 @@ -1514,7 +1514,7 @@
     4.4          methd G (super c) sig = Some old\<rbrakk> 
     4.5      \<Longrightarrow> methd G C sig = Some (C,new)"
     4.6  by (auto simp add: methd_rec
     4.7 -            intro: filter_tab_SomeI override_find_right table_of_map_SomeI)
     4.8 +            intro: filter_tab_SomeI map_add_find_right table_of_map_SomeI)
     4.9  
    4.10  lemma wf_prog_staticD:
    4.11    assumes     wf: "wf_prog G" and
    4.12 @@ -1667,8 +1667,7 @@
    4.13  	    by (auto simp add: inherits_def)
    4.14  	  with clsC ws no_new super neq_C_Obj
    4.15  	  have "methd G C sig = Some super_method"
    4.16 -	    by (auto simp add: methd_rec override_def
    4.17 -	                intro: filter_tab_SomeI)
    4.18 +	    by (auto simp add: methd_rec map_add_def intro: filter_tab_SomeI)
    4.19            with None show ?thesis
    4.20  	    by simp
    4.21  	qed
     5.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue May 13 08:59:21 2003 +0200
     5.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Wed May 14 10:22:09 2003 +0200
     5.3 @@ -658,6 +658,7 @@
     5.4  apply simp
     5.5  done
     5.6  
     5.7 +declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
     5.8  lemma Seq_sound1 [rule_format]: 
     5.9    "x\<in> cptn_mod \<Longrightarrow> \<forall>s P. x !0=(Some (Seq P Q), s) \<longrightarrow> 
    5.10    (\<forall>i<length x. fst(x!i)\<noteq>Some Q) \<longrightarrow> 
    5.11 @@ -670,8 +671,7 @@
    5.12      apply(rule_tac x="[(Some Pa, sa)]" in exI,simp add:CptnOne)
    5.13     apply(subgoal_tac "(\<forall>i < Suc (length xs). fst (((Some (Seq Pa Q), t) # xs) ! i) \<noteq> Some Q)")
    5.14      apply clarify
    5.15 -    apply(case_tac xsa,simp,simp)
    5.16 -    apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
    5.17 +    apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # zs" in exI,simp)
    5.18      apply(rule conjI,erule CptnEnv)
    5.19      apply(simp (no_asm_use) add:lift_def)
    5.20     apply clarify
    5.21 @@ -686,6 +686,7 @@
    5.22   apply(simp add:lift_def)
    5.23  apply simp
    5.24  done
    5.25 +declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
    5.26  
    5.27  lemma Seq_sound2 [rule_format]: 
    5.28    "x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x 
     6.1 --- a/src/HOL/IsaMakefile	Tue May 13 08:59:21 2003 +0200
     6.2 +++ b/src/HOL/IsaMakefile	Wed May 14 10:22:09 2003 +0200
     6.3 @@ -10,11 +10,11 @@
     6.4  images: HOL HOL-Algebra HOL-Complex TLA
     6.5  
     6.6  #Note: keep targets sorted (except for HOL-Library)
     6.7 +#  HOL-Bali
     6.8  test: \
     6.9    HOL-Library \
    6.10    HOL-Auth \
    6.11    HOL-AxClasses \
    6.12 -  HOL-Bali \
    6.13    HOL-Complex-ex \
    6.14    HOL-CTL \
    6.15    HOL-Extraction \
     7.1 --- a/src/HOL/List.ML	Tue May 13 08:59:21 2003 +0200
     7.2 +++ b/src/HOL/List.ML	Wed May 14 10:22:09 2003 +0200
     7.3 @@ -156,7 +156,7 @@
     7.4  val map_compose = thm "map_compose";
     7.5  val map_concat = thm "map_concat";
     7.6  val map_cong = thm "map_cong";
     7.7 -val map_eq_Cons = thm "map_eq_Cons";
     7.8 +val map_eq_Cons_conv = thm "map_eq_Cons_conv";
     7.9  val map_ext = thm "map_ext";
    7.10  val map_ident = thm "map_ident";
    7.11  val map_injective = thm "map_injective";
     8.1 --- a/src/HOL/List.thy	Tue May 13 08:59:21 2003 +0200
     8.2 +++ b/src/HOL/List.thy	Wed May 14 10:22:09 2003 +0200
     8.3 @@ -269,6 +269,14 @@
     8.4  "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
     8.5  by (induct xs) auto
     8.6  
     8.7 +lemma Suc_length_conv:
     8.8 +"(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
     8.9 +apply (induct xs)
    8.10 + apply simp
    8.11 +apply simp
    8.12 +apply blast
    8.13 +done
    8.14 +
    8.15  
    8.16  subsection {* @{text "@"} -- append *}
    8.17  
    8.18 @@ -441,13 +449,17 @@
    8.19  lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"
    8.20  by (cases xs) auto
    8.21  
    8.22 -lemma map_eq_Cons:
    8.23 -"(map f xs = y # ys) = (\<exists>x xs'. xs = x # xs' \<and> f x = y \<and> map f xs' = ys)"
    8.24 +lemma map_eq_Cons_conv[iff]:
    8.25 + "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"
    8.26  by (cases xs) auto
    8.27  
    8.28 +lemma Cons_eq_map_conv[iff]:
    8.29 + "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
    8.30 +by (cases ys) auto
    8.31 +
    8.32  lemma map_injective:
    8.33 -"!!xs. map f xs = map f ys ==> (\<forall>x y. f x = f y --> x = y) ==> xs = ys"
    8.34 -by (induct ys) (auto simp add: map_eq_Cons)
    8.35 + "!!xs. map f xs = map f ys ==> (\<forall>x y. f x = f y --> x = y) ==> xs = ys"
    8.36 +by (induct ys) auto
    8.37  
    8.38  lemma inj_mapI: "inj f ==> inj (map f)"
    8.39  by (rules dest: map_injective injD intro: inj_onI)
    8.40 @@ -858,6 +870,12 @@
    8.41   apply auto
    8.42  done
    8.43  
    8.44 +lemma set_take_subset: "\<And>n. set(take n xs) \<subseteq> set xs"
    8.45 +by(induct xs)(auto simp:take_Cons split:nat.split)
    8.46 +
    8.47 +lemma set_drop_subset: "\<And>n. set(drop n xs) \<subseteq> set xs"
    8.48 +by(induct xs)(auto simp:drop_Cons split:nat.split)
    8.49 +
    8.50  lemma append_eq_conv_conj:
    8.51  "!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
    8.52  apply(induct xs)
     9.1 --- a/src/HOL/Map.thy	Tue May 13 08:59:21 2003 +0200
     9.2 +++ b/src/HOL/Map.thy	Wed May 14 10:22:09 2003 +0200
     9.3 @@ -14,7 +14,7 @@
     9.4  
     9.5  consts
     9.6  chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
     9.7 -override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
     9.8 +map_add:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
     9.9  dom	:: "('a ~=> 'b) => 'a set"
    9.10  ran	:: "('a ~=> 'b) => 'b set"
    9.11  map_of	:: "('a * 'b)list => 'a ~=> 'b"
    9.12 @@ -43,10 +43,12 @@
    9.13  defs
    9.14  chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    9.15  
    9.16 -override_def: "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    9.17 +map_add_def: "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    9.18 +
    9.19 +map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    9.20  
    9.21  dom_def: "dom(m) == {a. m a ~= None}"
    9.22 -ran_def: "ran(m) == {b. ? a. m a = Some b}"
    9.23 +ran_def: "ran(m) == {b. EX a. m a = Some b}"
    9.24  
    9.25  map_le_def: "m1 \<subseteq>\<^sub>m m2  ==  ALL a : dom m1. m1 a = m2 a"
    9.26  
    9.27 @@ -54,9 +56,6 @@
    9.28    "map_of [] = empty"
    9.29    "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    9.30  
    9.31 -primrec "t([]  [|->]bs) = t"
    9.32 -        "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
    9.33 -
    9.34  
    9.35  subsection {* empty *}
    9.36  
    9.37 @@ -116,27 +115,6 @@
    9.38  done
    9.39  
    9.40  
    9.41 -subsection {* map\_upds *}
    9.42 -
    9.43 -lemma map_upd_upds_conv_if:
    9.44 - "!!x y ys f. (f(x|->y))(xs [|->] ys) =
    9.45 -              (if x : set xs then f(xs [|->] ys) else (f(xs [|->] ys))(x|->y))"
    9.46 -apply(induct xs)
    9.47 - apply simp
    9.48 -apply(simp split:split_if add:fun_upd_twist eq_sym_conv)
    9.49 -done
    9.50 -
    9.51 -lemma map_upds_twist [simp]:
    9.52 - "a ~: set as ==> m(a|->b)(as[|->]bs) = m(as[|->]bs)(a|->b)"
    9.53 -by (simp add: map_upd_upds_conv_if)
    9.54 -
    9.55 -lemma map_upds_apply_nontin[simp]:
    9.56 - "!!ys. x ~: set xs ==> (f(xs[|->]ys)) x = f x"
    9.57 -apply(induct xs)
    9.58 - apply simp
    9.59 -apply(simp add: fun_upd_apply map_upd_upds_conv_if split:split_if)
    9.60 -done
    9.61 -
    9.62  subsection {* chg\_map *}
    9.63  
    9.64  lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
    9.65 @@ -207,45 +185,49 @@
    9.66  
    9.67  subsection {* ++ *}
    9.68  
    9.69 -lemma override_empty[simp]: "m ++ empty = m"
    9.70 -apply (unfold override_def)
    9.71 +lemma map_add_empty[simp]: "m ++ empty = m"
    9.72 +apply (unfold map_add_def)
    9.73  apply (simp (no_asm))
    9.74  done
    9.75  
    9.76 -lemma empty_override[simp]: "empty ++ m = m"
    9.77 -apply (unfold override_def)
    9.78 +lemma empty_map_add[simp]: "empty ++ m = m"
    9.79 +apply (unfold map_add_def)
    9.80  apply (rule ext)
    9.81  apply (simp split add: option.split)
    9.82  done
    9.83  
    9.84 -lemma override_Some_iff [rule_format (no_asm)]: 
    9.85 +lemma map_add_assoc[simp]: "m1 ++ (m2 ++ m3) = (m1 ++ m2) ++ m3"
    9.86 +apply(rule ext)
    9.87 +apply(simp add: map_add_def split:option.split)
    9.88 +done
    9.89 +
    9.90 +lemma map_add_Some_iff: 
    9.91   "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)"
    9.92 -apply (unfold override_def)
    9.93 +apply (unfold map_add_def)
    9.94  apply (simp (no_asm) split add: option.split)
    9.95  done
    9.96  
    9.97 -lemmas override_SomeD = override_Some_iff [THEN iffD1, standard]
    9.98 -declare override_SomeD [dest!]
    9.99 +lemmas map_add_SomeD = map_add_Some_iff [THEN iffD1, standard]
   9.100 +declare map_add_SomeD [dest!]
   9.101  
   9.102 -lemma override_find_right[simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
   9.103 -apply (subst override_Some_iff)
   9.104 +lemma map_add_find_right[simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
   9.105 +apply (subst map_add_Some_iff)
   9.106  apply fast
   9.107  done
   9.108  
   9.109 -lemma override_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
   9.110 -apply (unfold override_def)
   9.111 +lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
   9.112 +apply (unfold map_add_def)
   9.113  apply (simp (no_asm) split add: option.split)
   9.114  done
   9.115  
   9.116 -lemma override_upd[simp]: "f ++ g(x|->y) = (f ++ g)(x|->y)"
   9.117 -apply (unfold override_def)
   9.118 +lemma map_add_upd[simp]: "f ++ g(x|->y) = (f ++ g)(x|->y)"
   9.119 +apply (unfold map_add_def)
   9.120  apply (rule ext)
   9.121  apply auto
   9.122  done
   9.123  
   9.124 -lemma map_of_override[simp]: "map_of ys ++ map_of xs = map_of (xs@ys)"
   9.125 -apply (unfold override_def)
   9.126 -apply (rule sym)
   9.127 +lemma map_of_append[simp]: "map_of (xs@ys) = map_of ys ++ map_of xs"
   9.128 +apply (unfold map_add_def)
   9.129  apply (induct_tac "xs")
   9.130  apply (simp (no_asm))
   9.131  apply (rule ext)
   9.132 @@ -253,7 +235,8 @@
   9.133  done
   9.134  
   9.135  declare fun_upd_apply [simp del]
   9.136 -lemma finite_range_map_of_override: "finite (range f) ==> finite (range (f ++ map_of l))"
   9.137 +lemma finite_range_map_of_map_add:
   9.138 + "finite (range f) ==> finite (range (f ++ map_of l))"
   9.139  apply (induct_tac "l")
   9.140  apply  auto
   9.141  apply (erule finite_range_updI)
   9.142 @@ -261,6 +244,42 @@
   9.143  declare fun_upd_apply [simp]
   9.144  
   9.145  
   9.146 +subsection {* map\_upds *}
   9.147 +
   9.148 +lemma map_upds_Nil1[simp]: "m([] [|->] bs) = m"
   9.149 +by(simp add:map_upds_def)
   9.150 +
   9.151 +lemma map_upds_Nil2[simp]: "m(as [|->] []) = m"
   9.152 +by(simp add:map_upds_def)
   9.153 +
   9.154 +lemma map_upds_Cons[simp]: "m(a#as [|->] b#bs) = (m(a|->b))(as[|->]bs)"
   9.155 +by(simp add:map_upds_def)
   9.156 +
   9.157 +
   9.158 +lemma map_upd_upds_conv_if: "!!x y ys f.
   9.159 + (f(x|->y))(xs [|->] ys) =
   9.160 + (if x : set(take (length ys) xs) then f(xs [|->] ys)
   9.161 +                                  else (f(xs [|->] ys))(x|->y))"
   9.162 +apply(induct xs)
   9.163 + apply simp
   9.164 +apply(case_tac ys)
   9.165 + apply(auto split:split_if simp:fun_upd_twist)
   9.166 +done
   9.167 +
   9.168 +lemma map_upds_twist [simp]:
   9.169 + "a ~: set as ==> m(a|->b)(as[|->]bs) = m(as[|->]bs)(a|->b)"
   9.170 +apply(insert set_take_subset)
   9.171 +apply (fastsimp simp add: map_upd_upds_conv_if)
   9.172 +done
   9.173 +
   9.174 +lemma map_upds_apply_nontin[simp]:
   9.175 + "!!ys. x ~: set xs ==> (f(xs[|->]ys)) x = f x"
   9.176 +apply(induct xs)
   9.177 + apply simp
   9.178 +apply(case_tac ys)
   9.179 + apply(auto simp: map_upd_upds_conv_if)
   9.180 +done
   9.181 +
   9.182  subsection {* dom *}
   9.183  
   9.184  lemma domI: "m a = Some b ==> a : dom m"
   9.185 @@ -287,13 +306,6 @@
   9.186  lemma dom_fun_upd[simp]:
   9.187   "dom(f(x := y)) = (if y=None then dom f - {x} else insert x (dom f))"
   9.188  by (simp add:dom_def) blast
   9.189 -(*
   9.190 -lemma dom_map_upd[simp]: "dom(m(a|->b)) = insert a (dom m)"
   9.191 -apply (unfold dom_def)
   9.192 -apply (simp (no_asm))
   9.193 -apply blast
   9.194 -done
   9.195 -*)
   9.196  
   9.197  lemma dom_map_of: "dom(map_of xys) = {x. \<exists>y. (x,y) : set xys}"
   9.198  apply(induct xys)
   9.199 @@ -306,10 +318,15 @@
   9.200  apply (auto simp add: insert_Collect [symmetric])
   9.201  done
   9.202  
   9.203 -lemma dom_map_upds[simp]: "!!m vs. dom(m(xs[|->]vs)) = set xs Un dom m"
   9.204 -by(induct xs, simp_all)
   9.205 +lemma dom_map_upds[simp]:
   9.206 + "!!m ys. dom(m(xs[|->]ys)) = set(take (length ys) xs) Un dom m"
   9.207 +apply(induct xs)
   9.208 + apply simp
   9.209 +apply(case_tac ys)
   9.210 + apply auto
   9.211 +done
   9.212  
   9.213 -lemma dom_override[simp]: "dom(m++n) = dom n Un dom m"
   9.214 +lemma dom_map_add[simp]: "dom(m++n) = dom n Un dom m"
   9.215  apply (unfold dom_def)
   9.216  apply auto
   9.217  done
   9.218 @@ -342,6 +359,10 @@
   9.219  
   9.220  lemma map_le_upds[simp]:
   9.221   "!!f g bs. f \<subseteq>\<^sub>m g ==> f(as [|->] bs) \<subseteq>\<^sub>m g(as [|->] bs)"
   9.222 -by(induct as, auto)
   9.223 +apply(induct as)
   9.224 + apply simp
   9.225 +apply(case_tac bs)
   9.226 + apply auto
   9.227 +done
   9.228  
   9.229  end
    10.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue May 13 08:59:21 2003 +0200
    10.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed May 14 10:22:09 2003 +0200
    10.3 @@ -600,7 +600,7 @@
    10.4      Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
    10.5      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
    10.6  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    10.7 -apply (clarsimp simp add: defs1 map_eq_Cons)
    10.8 +apply (clarsimp simp add: defs1)
    10.9  apply (blast intro: approx_loc_imp_approx_val_sup)
   10.10  done
   10.11  
   10.12 @@ -612,7 +612,7 @@
   10.13    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
   10.14    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
   10.15  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   10.16 -apply (clarsimp simp add: defs1 map_eq_Cons)
   10.17 +apply (clarsimp simp add: defs1)
   10.18  apply (blast intro: approx_loc_subst)
   10.19  done
   10.20  
   10.21 @@ -625,7 +625,7 @@
   10.22      Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
   10.23      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
   10.24  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
   10.25 -apply (clarsimp simp add: defs1 sup_PTS_eq map_eq_Cons)
   10.26 +apply (clarsimp simp add: defs1 sup_PTS_eq)
   10.27  apply (blast dest: conf_litval intro: conf_widen)
   10.28  done
   10.29  
   10.30 @@ -654,7 +654,7 @@
   10.31      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   10.32      fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   10.33  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   10.34 -apply (clarsimp simp add: defs2 wt_jvm_prog_def map_eq_Cons split: split_if_asm)
   10.35 +apply (clarsimp simp add: defs2 wt_jvm_prog_def split: split_if_asm)
   10.36  apply (blast intro: Cast_conf2)
   10.37  done
   10.38  
   10.39 @@ -668,7 +668,7 @@
   10.40    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   10.41    fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
   10.42  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   10.43 -apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def split_beta
   10.44 +apply (clarsimp simp add: defs2 wt_jvm_prog_def split_beta
   10.45                  split: option.split split_if_asm)
   10.46  apply (frule conf_widen)
   10.47  apply assumption+
   10.48 @@ -779,7 +779,7 @@
   10.49    from hp frame less suc_pc wf
   10.50    have "correct_frame G ?hp' (ST', LT') maxl ins ?f"
   10.51      apply (unfold correct_frame_def sup_state_conv)
   10.52 -    apply (clarsimp simp add: map_eq_Cons conf_def fun_upd_apply approx_val_def)
   10.53 +    apply (clarsimp simp add: conf_def fun_upd_apply approx_val_def)
   10.54      apply (blast intro: approx_stk_sup_heap approx_loc_sup_heap sup)
   10.55      done      
   10.56    moreover
   10.57 @@ -1082,7 +1082,7 @@
   10.58      proof -
   10.59        from wf hd_stk' len stk' less ST0
   10.60        have "approx_stk G hp (hd stk # drop (1+length pt) stk') ST''" 
   10.61 -        by (auto simp add: map_eq_Cons sup_state_conv
   10.62 +        by (auto simp add: sup_state_conv
   10.63                   dest!: approx_stk_append elim: conf_widen)
   10.64        moreover
   10.65        from wf loc' less
   10.66 @@ -1147,7 +1147,7 @@
   10.67    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   10.68    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   10.69  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   10.70 -apply (clarsimp simp add: defs2 map_eq_Cons)
   10.71 +apply (clarsimp simp add: defs2)
   10.72  apply (blast intro: conf_widen)
   10.73  done
   10.74  
   10.75 @@ -1159,7 +1159,7 @@
   10.76    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   10.77    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   10.78  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   10.79 -apply (clarsimp simp add: defs2 map_eq_Cons)
   10.80 +apply (clarsimp simp add: defs2)
   10.81  apply (blast intro: conf_widen)
   10.82  done
   10.83  
   10.84 @@ -1171,7 +1171,7 @@
   10.85    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   10.86    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   10.87  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   10.88 -apply (clarsimp simp add: defs2 map_eq_Cons)
   10.89 +apply (clarsimp simp add: defs2)
   10.90  apply (blast intro: conf_widen)
   10.91  done
   10.92  
   10.93 @@ -1183,7 +1183,7 @@
   10.94    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   10.95    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   10.96  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   10.97 -apply (clarsimp simp add: defs2 map_eq_Cons)
   10.98 +apply (clarsimp simp add: defs2)
   10.99  apply (blast intro: conf_widen)
  10.100  done
  10.101  
  10.102 @@ -1195,7 +1195,7 @@
  10.103    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
  10.104    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
  10.105  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
  10.106 -apply (clarsimp simp add: defs2 map_eq_Cons approx_val_def conf_def)
  10.107 +apply (clarsimp simp add: defs2 approx_val_def conf_def)
  10.108  apply blast
  10.109  done
  10.110  
    11.1 --- a/src/HOL/MicroJava/BV/EffectMono.thy	Tue May 13 08:59:21 2003 +0200
    11.2 +++ b/src/HOL/MicroJava/BV/EffectMono.thy	Wed May 14 10:22:09 2003 +0200
    11.3 @@ -130,7 +130,7 @@
    11.4      next
    11.5        case Store
    11.6        with G app show ?thesis
    11.7 -        by (cases s2, auto simp add: map_eq_Cons sup_loc_Cons2 sup_state_conv)
    11.8 +        by (cases s2, auto simp add: sup_loc_Cons2 sup_state_conv)
    11.9      next
   11.10        case LitPush
   11.11        with G app show ?thesis by (cases s2, auto simp add: sup_state_conv)
    12.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Tue May 13 08:59:21 2003 +0200
    12.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Wed May 14 10:22:09 2003 +0200
    12.3 @@ -387,12 +387,12 @@
    12.4  theorem sup_state_Cons1:
    12.5    "(G \<turnstile> (x#xt, a) <=s (yt, b)) = 
    12.6     (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
    12.7 -  by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def map_eq_Cons)
    12.8 +  by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def)
    12.9  
   12.10  theorem sup_state_Cons2:
   12.11    "(G \<turnstile> (xt, a) <=s (y#yt, b)) = 
   12.12     (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
   12.13 -  by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def map_eq_Cons sup_loc_Cons2)
   12.14 +  by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_Cons2)
   12.15  
   12.16  theorem sup_state_ignore_fst:  
   12.17    "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
    13.1 --- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Tue May 13 08:59:21 2003 +0200
    13.2 +++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Wed May 14 10:22:09 2003 +0200
    13.3 @@ -101,17 +101,9 @@
    13.4  
    13.5  lemma map_map_upds [rule_format (no_asm), simp]: 
    13.6  "\<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"
    13.7 -apply (induct ys)
    13.8 -apply simp
    13.9 -apply (intro strip)
   13.10 -apply (simp only: map_upds.simps)
   13.11 -apply (subgoal_tac "\<forall>y\<in>set list. y \<notin> set xs")
   13.12 -apply (subgoal_tac "a\<notin> set xs")
   13.13 -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")
   13.14 -apply (simp only:)
   13.15 -apply (erule map_map_upd)
   13.16 -apply blast
   13.17 -apply simp+
   13.18 +apply (induct xs)
   13.19 + apply simp
   13.20 +apply fastsimp
   13.21  done
   13.22  
   13.23  lemma map_upds_distinct [rule_format (no_asm), simp]: 
   13.24 @@ -121,11 +113,10 @@
   13.25  apply (intro strip)
   13.26  apply (case_tac vs)
   13.27  apply simp
   13.28 -apply (simp only: map_upds.simps distinct.simps hd.simps tl.simps)
   13.29 +apply (simp only: map_upds_Cons distinct.simps hd.simps tl.simps map.simps)
   13.30  apply clarify
   13.31 -apply (simp only: map.simps map_map_upd)
   13.32 +apply (simp del: o_apply)
   13.33  apply simp
   13.34 -apply (simp add: o_def)
   13.35  done
   13.36  
   13.37  
   13.38 @@ -138,7 +129,8 @@
   13.39    "\<forall> m ys. (m(xs[\<mapsto>]ys)) k = Some y \<longrightarrow> k \<in> (set xs) \<or> (m k = Some y)"
   13.40  apply (induct xs)
   13.41  apply simp
   13.42 -apply (case_tac "k = a")
   13.43 +apply auto
   13.44 +apply(case_tac ys)
   13.45  apply auto
   13.46  done
   13.47  
    14.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Tue May 13 08:59:21 2003 +0200
    14.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Wed May 14 10:22:09 2003 +0200
    14.3 @@ -300,7 +300,7 @@
    14.4  apply (subst method_rec) apply simp
    14.5  apply force
    14.6  apply assumption
    14.7 -apply (simp only: override_def)
    14.8 +apply (simp only: map_add_def)
    14.9  apply (split option.split)
   14.10  apply (rule conjI)
   14.11  apply force
    15.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue May 13 08:59:21 2003 +0200
    15.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed May 14 10:22:09 2003 +0200
    15.3 @@ -81,7 +81,7 @@
    15.4  apply (rule allI)
    15.5  apply (drule_tac x="a # ys" in spec)
    15.6  apply (simp only: rev.simps append_assoc append_Cons append_Nil
    15.7 -  map.simps map_of.simps map_upds.simps hd.simps tl.simps)
    15.8 +  map.simps map_of.simps map_upds_Cons hd.simps tl.simps)
    15.9  done
   15.10  
   15.11  lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\<mapsto>] (map snd xs))"
   15.12 @@ -90,7 +90,8 @@
   15.13  lemma map_of_rev: "unique xs \<Longrightarrow> map_of (rev xs) = map_of xs"
   15.14  apply (induct xs)
   15.15  apply simp
   15.16 -apply (simp add: unique_def map_of_append map_of_as_map_upds [THEN sym])
   15.17 +apply (simp add: unique_def map_of_append map_of_as_map_upds [THEN sym]
   15.18 +                 Map.map_of_append[symmetric] del:Map.map_of_append)
   15.19  done
   15.20  
   15.21  lemma map_upds_rev [rule_format]: "\<forall> xs. (distinct ks \<longrightarrow> length ks = length xs 
    16.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Tue May 13 08:59:21 2003 +0200
    16.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed May 14 10:22:09 2003 +0200
    16.3 @@ -254,7 +254,7 @@
    16.4  apply (rule inv_f_eq) apply (simp add: inj_on_def) apply simp
    16.5  
    16.6  apply (intro strip)
    16.7 -apply (simp add: override_Some_iff map_of_map del: split_paired_Ex)
    16.8 +apply (simp add: map_add_Some_iff map_of_map del: split_paired_Ex)
    16.9  apply (subgoal_tac "\<forall>x\<in>set ms. fst ((Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x")
   16.10  (*
   16.11  apply (subgoal_tac "\<forall>x\<in>set ms. fst (((\<lambda>(s, m). (s, Ca, m)) \<circ> compMethod G Ca) x) = fst x")
   16.12 @@ -329,14 +329,14 @@
   16.13  apply (case_tac "(method (G, D) ++  map_of (map (\<lambda>(s, m). (s, C, m)) ms)) S")
   16.14  
   16.15    (* case None *)
   16.16 -apply (simp (no_asm_simp) add: override_None)
   16.17 +apply (simp (no_asm_simp) add: map_add_None)
   16.18  apply (simp add: map_of_map_compMethod comp_method_result_def) 
   16.19  
   16.20    (* case Some *)
   16.21 -apply (simp add: override_Some_iff)
   16.22 +apply (simp add: map_add_Some_iff)
   16.23  apply (erule disjE)
   16.24    apply (simp add: split_beta map_of_map_compMethod)
   16.25 -  apply (simp add: override_def comp_method_result_def map_of_map_compMethod)
   16.26 +  apply (simp add: map_add_def comp_method_result_def map_of_map_compMethod)
   16.27  
   16.28    (* show subgoals *)
   16.29  apply (simp add: comp_subcls1) 
    17.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue May 13 08:59:21 2003 +0200
    17.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed May 14 10:22:09 2003 +0200
    17.3 @@ -398,4 +398,3 @@
    17.4  
    17.5  end
    17.6  
    17.7 -
    18.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Tue May 13 08:59:21 2003 +0200
    18.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Wed May 14 10:22:09 2003 +0200
    18.3 @@ -324,7 +324,7 @@
    18.4  apply(  assumption)
    18.5  apply( rotate_tac -1)
    18.6  apply( simp)
    18.7 -apply( drule override_SomeD)
    18.8 +apply( drule map_add_SomeD)
    18.9  apply( erule disjE)
   18.10  apply(  erule_tac V = "?P --> ?Q" in thin_rl)
   18.11  apply (frule map_of_SomeD)
   18.12 @@ -368,7 +368,7 @@
   18.13  apply( clarify)
   18.14  apply( subst method_rec)
   18.15  apply(  assumption)
   18.16 -apply( unfold override_def)
   18.17 +apply( unfold map_add_def)
   18.18  apply( simp (no_asm_simp) del: split_paired_Ex)
   18.19  apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z")
   18.20  apply(  erule exE)
   18.21 @@ -412,7 +412,7 @@
   18.22   apply (subst method_rec)
   18.23     apply (assumption)
   18.24    apply (assumption)
   18.25 - apply (simp add: override_def map_of_map split add: option.split)
   18.26 + apply (simp add: map_add_def map_of_map split add: option.split)
   18.27  done
   18.28  
   18.29  
   18.30 @@ -453,7 +453,7 @@
   18.31  
   18.32  apply clarify
   18.33  apply (subgoal_tac "((field (G, D)) ++ map_of (map (\<lambda>(s, f). (s, C, f)) fs)) vn = Some (Da, T)")
   18.34 -apply (simp (no_asm_use) only:  override_Some_iff)
   18.35 +apply (simp (no_asm_use) only: map_add_Some_iff)
   18.36  apply (erule disjE)
   18.37  apply (simp (no_asm_use) add: map_of_map) apply blast
   18.38  apply blast