--- 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
--- 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
--- 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)]:
--- 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
--- 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
--- 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 \
--- 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";
--- 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)
--- 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
--- 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
--- 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)
--- 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)"
--- 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
--- 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
--- 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
--- 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)
--- 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
-
--- 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