--- a/src/HOL/Bali/AxSound.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/AxSound.thy Tue Mar 14 18:19:10 2023 +0100
@@ -1468,7 +1468,7 @@
EName e
\<Rightarrow> (case e of
VNam v
- \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
+ \<Rightarrow>((table_of (lcls (mbody (mthd dynM))))
(pars (mthd dynM)[\<mapsto>]pTs')) v
| Res \<Rightarrow> Some (resTy dynM))
| This \<Rightarrow> if is_static statM
--- a/src/HOL/Bali/DefiniteAssignment.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy Tue Mar 14 18:19:10 2023 +0100
@@ -608,7 +608,7 @@
\<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A"
| Try: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1;
- Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> (B \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
+ Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>\<turnstile> (B \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2;
nrm A = nrm C1 \<inter> nrm C2;
brk A = brk C1 \<Rightarrow>\<inter> brk C2\<rbrakk>
\<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A"
@@ -1170,7 +1170,7 @@
from \<open>Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'\<close>
obtain C1' C2'
where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
- da_c2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn}
+ da_c2': "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn}
\<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
A': "nrm A' = nrm C1' \<inter> nrm C2'"
"brk A' = brk C1' \<Rightarrow>\<inter> brk C2'"
@@ -1180,7 +1180,7 @@
moreover note da_c1'
ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
by blast
- note \<open>PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)
+ note \<open>PROP ?Hyp (Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>)
(B \<union> {VName vn}) \<langle>c2\<rangle> C2\<close>
with B' da_c2'
obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
@@ -1448,11 +1448,11 @@
qed
moreover
obtain C2' where
- "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
+ "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
proof -
from B' have "B \<union> {VName vn} \<subseteq> B' \<union> {VName vn}" by blast
moreover
- have "PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)
+ have "PROP ?Hyp (Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>)
(B \<union> {VName vn}) \<langle>c2\<rangle>"
by (rule Try.hyps)
ultimately
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Tue Mar 14 18:19:10 2023 +0100
@@ -494,7 +494,7 @@
note G = \<open>prg Env = G\<close>
from Try.prems obtain
wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
- wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
+ wt_c2: "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases)
{
fix j
@@ -531,7 +531,7 @@
moreover have "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
moreover note wt_c2
moreover from G
- have "prg (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>) = G"
+ have "prg (Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>) = G"
by simp
moreover note jmp
ultimately show ?thesis
@@ -3170,13 +3170,13 @@
from Try.prems obtain C1 C2 where
da_c1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
da_c2:
- "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>
+ "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>
\<turnstile> (dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"
by (elim da_elim_cases) simp
from Try.prems obtain
wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
- wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
+ wt_c2: "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases)
have sxalloc: "prg Env\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" using Try.hyps G
by (simp (no_asm_simp))
@@ -3257,7 +3257,7 @@
qed
with da_c2
obtain C2' where
- da_C2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>
+ da_C2': "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>
\<turnstile> dom (locals (store (new_xcpt_var vn s2))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
and nrm_C2': "nrm C2 \<subseteq> nrm C2'"
and brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"
--- a/src/HOL/Bali/Example.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/Example.thy Tue Mar 14 18:19:10 2023 +0100
@@ -1208,12 +1208,11 @@
abbreviation
"obj_a == \<lparr>tag=Arr (PrimT Boolean) 2
- ,values= Map.empty(Inr 0\<mapsto>Bool False)(Inr 1\<mapsto>Bool False)\<rparr>"
+ ,values= Map.empty(Inr 0\<mapsto>Bool False, Inr 1\<mapsto>Bool False)\<rparr>"
abbreviation
"obj_b == \<lparr>tag=CInst Ext
- ,values=(Map.empty(Inl (vee, Base)\<mapsto>Null )
- (Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
+ ,values=(Map.empty(Inl (vee, Base)\<mapsto>Null, Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
abbreviation
"obj_c == \<lparr>tag=CInst (SXcpt NullPointer),values=CONST Map.empty\<rparr>"
@@ -1222,15 +1221,15 @@
abbreviation "arr_a == Map.empty(Inl (arr, Base)\<mapsto>Addr a)"
abbreviation
- "globs1 == Map.empty(Inr Ext \<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>)
- (Inr Base \<mapsto>\<lparr>tag=undefined, values=arr_N\<rparr>)
- (Inr Object\<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>)"
+ "globs1 == Map.empty(Inr Ext \<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>,
+ Inr Base \<mapsto>\<lparr>tag=undefined, values=arr_N\<rparr>,
+ Inr Object\<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>)"
abbreviation
- "globs2 == Map.empty(Inr Ext \<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>)
- (Inr Object\<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>)
- (Inl a\<mapsto>obj_a)
- (Inr Base \<mapsto>\<lparr>tag=undefined, values=arr_a\<rparr>)"
+ "globs2 == Map.empty(Inr Ext \<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>,
+ Inr Object\<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>,
+ Inl a\<mapsto>obj_a,
+ Inr Base \<mapsto>\<lparr>tag=undefined, values=arr_a\<rparr>)"
abbreviation "globs3 == globs2(Inl b\<mapsto>obj_b)"
abbreviation "globs8 == globs3(Inl c\<mapsto>obj_c)"
--- a/src/HOL/Bali/State.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/State.thy Tue Mar 14 18:19:10 2023 +0100
@@ -293,7 +293,7 @@
lemma init_arr_comps_step [simp]:
"0 < j \<Longrightarrow> init_vals (arr_comps T j ) =
- init_vals (arr_comps T (j - 1))(j - 1\<mapsto>default_val T)"
+ (init_vals (arr_comps T (j - 1)))(j - 1\<mapsto>default_val T)"
apply (unfold arr_comps_def in_bounds_def)
apply (rule ext)
apply auto
@@ -335,7 +335,7 @@
apply (simp (no_asm))
done
-lemma globs_gupd [simp]: "globs (gupd(r\<mapsto>obj) s) = globs s(r\<mapsto>obj)"
+lemma globs_gupd [simp]: "globs (gupd(r\<mapsto>obj) s) = (globs s)(r\<mapsto>obj)"
apply (induct "s")
by (simp add: gupd_def)
@@ -347,7 +347,7 @@
apply (induct "s")
by (simp add: gupd_def)
-lemma locals_lupd [simp]: "locals (lupd(vn\<mapsto>v ) s) = locals s(vn\<mapsto>v )"
+lemma locals_lupd [simp]: "locals (lupd(vn\<mapsto>v ) s) = (locals s)(vn\<mapsto>v )"
apply (induct "s")
by (simp add: lupd_def)
@@ -359,7 +359,7 @@
done
lemma globs_upd_gobj_upd [rule_format (no_asm), simp]:
-"globs s r=Some obj\<longrightarrow> globs (upd_gobj r n v s) = globs s(r\<mapsto>upd_obj n v obj)"
+"globs s r=Some obj\<longrightarrow> globs (upd_gobj r n v s) = (globs s)(r\<mapsto>upd_obj n v obj)"
apply (unfold upd_gobj_def)
apply (induct "s")
apply auto
@@ -390,7 +390,7 @@
done
lemma heap_heap_upd [simp]:
- "heap (st (g(Inl a\<mapsto>obj)) l) = heap (st g l)(a\<mapsto>obj)"
+ "heap (st (g(Inl a\<mapsto>obj)) l) = (heap (st g l))(a\<mapsto>obj)"
apply (rule ext)
apply (simp (no_asm))
done
@@ -403,7 +403,7 @@
apply (simp (no_asm))
done
-lemma heap_gupd_Heap [simp]: "heap (gupd(Heap a\<mapsto>obj) s) = heap s(a\<mapsto>obj)"
+lemma heap_gupd_Heap [simp]: "heap (gupd(Heap a\<mapsto>obj) s) = (heap s)(a\<mapsto>obj)"
apply (rule ext)
apply (simp (no_asm))
done
--- a/src/HOL/Bali/TypeSafe.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/TypeSafe.thy Tue Mar 14 18:19:10 2023 +0100
@@ -815,7 +815,7 @@
wf_mhead G P sig mh;
list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig)\<rbrakk> \<Longrightarrow>
G,s\<turnstile>Map.empty (pars mh[\<mapsto>]pvs)
- [\<sim>\<Colon>\<preceq>]table_of lvars(pars mh[\<mapsto>]parTs sig)"
+ [\<sim>\<Colon>\<preceq>](table_of lvars)(pars mh[\<mapsto>]parTs sig)"
apply (unfold wf_mhead_def)
apply clarify
apply (erule (1) wlconf_empty_vals [THEN wlconf_ext_list])
@@ -895,7 +895,7 @@
(case k of
EName e \<Rightarrow> (case e of
VNam v
- \<Rightarrow> (table_of (lcls (mbody (mthd dm)))
+ \<Rightarrow> ((table_of (lcls (mbody (mthd dm))))
(pars (mthd dm)[\<mapsto>]parTs sig)) v
| Res \<Rightarrow> Some (resTy (mthd dm)))
| This \<Rightarrow> if (is_static (mthd sm))
@@ -1180,7 +1180,7 @@
lemma map_upds_upd_eq_length_simp:
"\<And> tab qs x y. length ps = length qs
- \<Longrightarrow> tab(ps[\<mapsto>]qs)(x\<mapsto>y) = tab(ps@[x][\<mapsto>]qs@[y])"
+ \<Longrightarrow> tab(ps[\<mapsto>]qs, x\<mapsto>y) = tab(ps@[x][\<mapsto>]qs@[y])"
proof (induct "ps")
case Nil thus ?case by simp
next
@@ -1189,7 +1189,7 @@
obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
by (cases qs) auto
from eq_length
- have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs')(x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
+ have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs', x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
by (rule Cons.hyps)
with qs show ?case
by simp
@@ -1219,7 +1219,7 @@
show ?thesis by simp
next
case (Cons y ys')
- have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
+ have "(tab(x\<mapsto>y, xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y, xs[\<mapsto>]ys')) z"
by (iprover intro: Hyps map_upd_cong_ext)
with Cons show ?thesis
by simp
@@ -1230,7 +1230,7 @@
by simp
lemma map_upds_eq_length_suffix: "\<And> tab qs.
- length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs)(xs[\<mapsto>][])"
+ length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs, xs[\<mapsto>][])"
proof (induct ps)
case Nil thus ?case by simp
next
@@ -1238,7 +1238,7 @@
then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
by (cases qs) auto
from eq_length
- have "tab(p\<mapsto>q)(ps @ xs[\<mapsto>]qs') = tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>][])"
+ have "tab(p\<mapsto>q, ps @ xs[\<mapsto>]qs') = tab(p\<mapsto>q, ps[\<mapsto>]qs', xs[\<mapsto>][])"
by (rule Cons.hyps)
with qs show ?case
by simp
@@ -1247,7 +1247,7 @@
lemma map_upds_upds_eq_length_prefix_simp:
"\<And> tab qs. length ps = length qs
- \<Longrightarrow> tab(ps[\<mapsto>]qs)(xs[\<mapsto>]ys) = tab(ps@xs[\<mapsto>]qs@ys)"
+ \<Longrightarrow> tab(ps[\<mapsto>]qs, xs[\<mapsto>]ys) = tab(ps@xs[\<mapsto>]qs@ys)"
proof (induct ps)
case Nil thus ?case by simp
next
@@ -1255,7 +1255,7 @@
then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
by (cases qs) auto
from eq_length
- have "tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>]ys) = tab(p\<mapsto>q)(ps @ xs[\<mapsto>](qs' @ ys))"
+ have "tab(p\<mapsto>q, ps[\<mapsto>]qs', xs[\<mapsto>]ys) = tab(p\<mapsto>q, ps @ xs[\<mapsto>](qs' @ ys))"
by (rule Cons.hyps)
with qs
show ?case by simp
@@ -1297,11 +1297,11 @@
lemma map_upd_Some_swap:
- "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z \<Longrightarrow> \<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z"
+ "(tab(r\<mapsto>w, u\<mapsto>v)) vn = Some z \<Longrightarrow> \<exists> z. (tab(u\<mapsto>v, r\<mapsto>w)) vn = Some z"
by (simp add: fun_upd_def)
lemma map_upd_None_swap:
- "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = None \<Longrightarrow> (tab(u\<mapsto>v)(r\<mapsto>w)) vn = None"
+ "(tab(r\<mapsto>w, u\<mapsto>v)) vn = None \<Longrightarrow> (tab(u\<mapsto>v, r\<mapsto>w)) vn = None"
by (simp add: fun_upd_def)
@@ -1331,7 +1331,7 @@
show ?thesis
proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
case True
- with some ys have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = Some z"
+ with some ys have "(tab'(x\<mapsto>y, xs[\<mapsto>]tl)) vn = Some z"
by (fastforce intro: Cons.hyps)
with ys show ?thesis
by simp
@@ -1345,7 +1345,7 @@
ultimately
have "(tab(x\<mapsto>y)) vn =(tab'(x\<mapsto>y)) vn"
by simp
- hence "(tab(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = (tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn"
+ hence "(tab(x\<mapsto>y, xs[\<mapsto>]tl)) vn = (tab'(x\<mapsto>y, xs[\<mapsto>]tl)) vn"
by (rule map_upds_cong_ext)
with some ys
show ?thesis
@@ -1355,18 +1355,18 @@
qed
lemma map_upds_Some_swap:
- assumes r_u: "(tab(r\<mapsto>w)(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
- shows "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
-proof (cases "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z")
+ assumes r_u: "(tab(r\<mapsto>w, u\<mapsto>v, xs[\<mapsto>]ys)) vn = Some z"
+ shows "\<exists> z. (tab(u\<mapsto>v, r\<mapsto>w, xs[\<mapsto>]ys)) vn = Some z"
+proof (cases "(tab(r\<mapsto>w, u\<mapsto>v)) vn = Some z")
case True
- then obtain z' where "(tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z'"
+ then obtain z' where "(tab(u\<mapsto>v, r\<mapsto>w)) vn = Some z'"
by (rule map_upd_Some_swap [elim_format]) blast
- thus "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
+ thus "\<exists> z. (tab(u\<mapsto>v, r\<mapsto>w, xs[\<mapsto>]ys)) vn = Some z"
by (rule map_upds_Some_expand)
next
case False
with r_u
- have "(tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
+ have "(tab(u\<mapsto>v, r\<mapsto>w, xs[\<mapsto>]ys)) vn = Some z"
by (rule map_upds_in_expansion_map_swap)
thus ?thesis
by simp
@@ -1374,7 +1374,7 @@
lemma map_upds_Some_insert:
assumes z: "(tab(xs[\<mapsto>]ys)) vn = Some z"
- shows "\<exists> z. (tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
+ shows "\<exists> z. (tab(u\<mapsto>v, xs[\<mapsto>]ys)) vn = Some z"
proof (cases "\<exists> z. tab vn = Some z")
case True
then obtain z' where "tab vn = Some z'" by blast
@@ -1386,7 +1386,7 @@
case False
hence "tab vn \<noteq> Some z" by simp
with z
- have "(tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
+ have "(tab(u\<mapsto>v, xs[\<mapsto>]ys)) vn = Some z"
by (rule map_upds_in_expansion_map_swap)
thus ?thesis ..
qed
@@ -1425,7 +1425,7 @@
have "(tab(x\<mapsto>y)) vn = Some el"
by - (rule Cons.hyps,auto)
moreover from tab'_vn ys
- have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = None"
+ have "(tab'(x\<mapsto>y, xs[\<mapsto>]tl)) vn = None"
by simp
hence "(tab'(x\<mapsto>y)) vn = None"
by (rule map_upds_None_cut)
@@ -1436,7 +1436,7 @@
lemma dom_vname_split:
- "dom (case_lname (case_ename (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
+ "dom (case_lname (case_ename (tab(x\<mapsto>y, xs[\<mapsto>]ys)) a) b)
= dom (case_lname (case_ename (tab(x\<mapsto>y)) a) b) \<union>
dom (case_lname (case_ename (tab(xs[\<mapsto>]ys)) a) b)"
(is "?List x xs y ys = ?Hd x y \<union> ?Tl xs ys")
@@ -1503,7 +1503,7 @@
case Nil with len show ?thesis by simp
next
case (Cons y tl)
- with len have "dom (tab(x\<mapsto>y)(xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
+ with len have "dom (tab(x\<mapsto>y, xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
by - (rule Hyp,simp)
moreover
have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
@@ -3162,7 +3162,7 @@
EName e
\<Rightarrow> (case e of
VNam v
- \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
+ \<Rightarrow>((table_of (lcls (mbody (mthd dynM))))
(pars (mthd dynM)[\<mapsto>]pTs')) v
| Res \<Rightarrow> Some (resTy dynM))
| This \<Rightarrow> if is_static statM
--- a/src/HOL/Bali/WellForm.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/WellForm.thy Tue Mar 14 18:19:10 2023 +0100
@@ -85,7 +85,7 @@
EName e
\<Rightarrow> (case e of
VNam v
- \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
+ \<Rightarrow>((table_of (lcls (mbody m)))(pars m [\<mapsto>] parTs sig)) v
| Res \<Rightarrow> Some (resTy m))
| This \<Rightarrow> if is_static m then None else Some (Class C)))"
@@ -110,7 +110,7 @@
lemma callee_lcl_VNam_simp [simp]:
"callee_lcl C sig m (EName (VNam v))
- = (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v"
+ = ((table_of (lcls (mbody m)))(pars m [\<mapsto>] parTs sig)) v"
by (simp add: callee_lcl_def)
lemma callee_lcl_Res_simp [simp]:
--- a/src/HOL/Bali/WellType.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/Bali/WellType.thy Tue Mar 14 18:19:10 2023 +0100
@@ -295,7 +295,7 @@
E,dt\<Turnstile>Throw e\<Colon>\<surd>"
\<comment> \<open>cf. 14.18\<close>
| Try: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
- lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
+ lcl E (VName vn)=None; E \<lparr>lcl := (lcl E)(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
\<Longrightarrow>
E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Tue Mar 14 18:19:10 2023 +0100
@@ -102,7 +102,7 @@
apply fastforce+
done
-lemma map_of_upds_SomeD: "(map_of m (xs[\<mapsto>]ys)) k = Some y
+lemma map_of_upds_SomeD: "((map_of m) (xs[\<mapsto>]ys)) k = Some y
\<Longrightarrow> k \<in> (set (xs @ map fst m))"
by (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma)
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Tue Mar 14 18:19:10 2023 +0100
@@ -266,7 +266,7 @@
"env_of_jmb G C S ==
(let (mn,pTs) = S;
(D,rT,(pns,lvars,blk,res)) = the(method (G, C) S) in
- (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)))"
+ (G,(map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class C)))"
lemma env_of_jmb_fst [simp]: "fst (env_of_jmb G C S) = G"
by (simp add: env_of_jmb_def split_beta)
@@ -406,7 +406,7 @@
wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
\<Longrightarrow> wtpd_stmt (env_of_jmb G D (md, pTs)) blk"
apply (simp add: wtpd_stmt_def env_of_jmb_def)
- apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> blk \<surd> " in method_preserves)
+ apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). (G, (map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class D)) \<turnstile> blk \<surd> " in method_preserves)
apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
done
@@ -415,7 +415,7 @@
wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
\<Longrightarrow> wtpd_expr (env_of_jmb G D (md, pTs)) res"
apply (simp add: wtpd_expr_def env_of_jmb_def)
- apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). \<exists>T. (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> res :: T " in method_preserves)
+ apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). \<exists>T. (G, (map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class D)) \<turnstile> res :: T " in method_preserves)
apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
done
@@ -539,7 +539,7 @@
{cG, D, S} \<turnstile>
{h, os, (a' # pvs @ lvals)}
>- (compInitLvars (pns, lvars, blk, res) lvars) \<rightarrow>
- {h, os, (locvars_xstate G C S (Norm (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))))})"
+ {h, os, (locvars_xstate G C S (Norm (h, (init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))))})"
apply (simp only: compInitLvars_def)
apply (frule method_yields_wf_java_mdecl, assumption, assumption)
@@ -587,7 +587,7 @@
method (G, dynT) (mn, pTs) = Some (md, rT, pns, lvars, blk, res);
list_all2 (conf G h) pvs pTs; G,h \<turnstile> a' ::\<preceq> Class md\<rbrakk>
\<Longrightarrow>
- (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs))"
+ (np a' x, h, (init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs))"
apply (frule wf_prog_ws_prog)
apply (frule method_in_md [THEN conjunct2], assumption+)
apply (frule method_yields_wf_java_mdecl, assumption, assumption)
@@ -1173,7 +1173,7 @@
apply (simp (no_asm_simp))
(* show s3::\<preceq>\<dots> *)
- apply (rule_tac xs = "(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))" and st=blk in state_ok_exec)
+ apply (rule_tac xs = "(np a' x, h, (init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))" and st=blk in state_ok_exec)
apply assumption
apply (simp (no_asm_simp) only: env_of_jmb_fst)
apply assumption
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Mar 14 18:19:10 2023 +0100
@@ -20,7 +20,7 @@
definition local_env :: "[java_mb prog, cname, sig, vname list,(vname \<times> ty) list] \<Rightarrow> java_mb env" where
"local_env G C S pns lvars ==
- let (mn, pTs) = S in (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C))"
+ let (mn, pTs) = S in (G,(map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class C))"
lemma local_env_fst [simp]: "fst (local_env G C S pns lvars) = G"
by (simp add: local_env_def split_beta)
@@ -42,7 +42,7 @@
subsection "index"
lemma local_env_snd:
- "snd (local_env G C (mn, pTs) pns lvars) = map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)"
+ "snd (local_env G C (mn, pTs) pns lvars) = (map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class C)"
by (simp add: local_env_def)
@@ -62,7 +62,7 @@
lemma map_upds_append:
- "length k1s = length x1s \<Longrightarrow> m(k1s[\<mapsto>]x1s)(k2s[\<mapsto>]x2s) = m ((k1s@k2s)[\<mapsto>](x1s@x2s))"
+ "length k1s = length x1s \<Longrightarrow> m(k1s[\<mapsto>]x1s, k2s[\<mapsto>]x2s) = m ((k1s@k2s)[\<mapsto>](x1s@x2s))"
apply (induct k1s arbitrary: x1s m)
apply simp
apply (subgoal_tac "\<exists>x xr. x1s = x # xr")
@@ -114,7 +114,7 @@
apply (clarify)
apply (drule_tac x=kr in spec)
apply (simp only: rev.simps)
- apply (subgoal_tac "(Map.empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = Map.empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
+ apply (subgoal_tac "(Map.empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = Map.empty (rev kr[\<mapsto>]rev xs, [k'][\<mapsto>][a])")
apply (simp split:if_split_asm)
apply (simp add: map_upds_append [symmetric])
apply (case_tac ks)
--- a/src/HOL/MicroJava/Comp/DefsComp.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/Comp/DefsComp.thy Tue Mar 14 18:19:10 2023 +0100
@@ -65,7 +65,7 @@
definition locals_locvars :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> locvars \<Rightarrow> State.locals" where
"locals_locvars G C S lvs ==
- Map.empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs)) (This\<mapsto>(hd lvs))"
+ Map.empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs), This\<mapsto>(hd lvs))"
definition locvars_xstate :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> xstate \<Rightarrow> locvars" where
"locvars_xstate G C S xs == locvars_locals G C S (gl xs)"
--- a/src/HOL/MicroJava/J/Eval.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy Tue Mar 14 18:19:10 2023 +0100
@@ -83,7 +83,7 @@
| Call: "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
(md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
- G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs)(This\<mapsto>a'))) -blk-> s3;
+ G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))) -blk-> s3;
G\<turnstile> s3 -res\<succ>v -> (x4,s4) |] ==>
G\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\<succ>v-> (x4,(heap s4,l))"
@@ -135,7 +135,7 @@
lemmas eval_evals_exec_induct = eval_evals_exec.induct [split_format (complete)]
lemma NewCI: "[|new_Addr (heap s) = (a,x);
- s' = c_hupd (heap s(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==>
+ s' = c_hupd ((heap s)(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==>
G\<turnstile>Norm s -NewC C\<succ>Addr a-> s'"
apply simp
apply (rule eval_evals_exec.NewC)
@@ -197,7 +197,7 @@
"[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
(md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
- G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs)(This\<mapsto>a'))) -blk-> s3;
+ G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))) -blk-> s3;
G\<turnstile> s3 -res\<succ>v -> (x4,(h4, l4)) |] ==>
G\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\<succ>v-> (x4,(h4,l))"
using Call[of G s0 e a' s1 a ps pvs x h l dynT md rT pns lvars blk res mn pTs s3 v x4 "(h4, l4)" C]
--- a/src/HOL/MicroJava/J/Example.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Tue Mar 14 18:19:10 2023 +0100
@@ -120,11 +120,11 @@
abbreviation
obj1 :: obj where
- "obj1 == (Ext, Map.empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))"
+ "obj1 == (Ext, Map.empty((vee, Base)\<mapsto>Bool False, (vee, Ext )\<mapsto>Intg 0))"
abbreviation "s0 == Norm (Map.empty, Map.empty)"
abbreviation "s1 == Norm (Map.empty(a\<mapsto>obj1),Map.empty(e\<mapsto>Addr a))"
-abbreviation "s2 == Norm (Map.empty(a\<mapsto>obj1),Map.empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
+abbreviation "s2 == Norm (Map.empty(a\<mapsto>obj1),Map.empty(x\<mapsto>Null, This\<mapsto>Addr a))"
abbreviation "s3 == (Some NP, Map.empty(a\<mapsto>obj1),Map.empty(e\<mapsto>Addr a))"
lemmas map_of_Cons = map_of.simps(2)
--- a/src/HOL/MicroJava/J/Exceptions.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/J/Exceptions.thy Tue Mar 14 18:19:10 2023 +0100
@@ -10,9 +10,9 @@
"blank G C \<equiv> (C,init_vars (fields(G,C)))"
definition start_heap :: "'c prog \<Rightarrow> aheap" where
- "start_heap G \<equiv> Map.empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
- (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
- (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
+ "start_heap G \<equiv> Map.empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer),
+ XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast),
+ XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
abbreviation
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Tue Mar 14 18:19:10 2023 +0100
@@ -105,7 +105,7 @@
list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;
length pTs' = length pns; distinct pns;
Ball (set lvars) (case_prod (\<lambda>vn. is_type G))
- |] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')"
+ |] ==> G,h\<turnstile>(init_vars lvars)(pns[\<mapsto>]pvs)[::\<preceq>](map_of lvars)(pns[\<mapsto>]pTs')"
apply (unfold wf_mhead_def)
apply( clarsimp)
apply( rule lconf_ext_list)
@@ -122,7 +122,7 @@
list_all2 (conf G h) pvs pTsa;
(md, rT, pns, lvars, blk, res) =
the (method (G,fst (the (h (the_Addr a')))) (mn, pTs'));
- \<forall>lT. (np a' None, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) -->
+ \<forall>lT. (np a' None, h, (init_vars lvars)(pns[\<mapsto>]pvs, This\<mapsto>a'))::\<preceq>(G, lT) -->
(G, lT)\<turnstile>blk\<surd> --> h\<le>|xi \<and> (xcptb, xi, xl)::\<preceq>(G, lT);
\<forall>lT. (xcptb,xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T -->
xi\<le>|h' \<and> (x',h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T));
--- a/src/HOL/MicroJava/J/WellType.thy Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Tue Mar 14 18:19:10 2023 +0100
@@ -194,7 +194,7 @@
This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and>
(\<forall>pn\<in>set pns. map_of lvars pn = None) \<and>
(\<forall>(vn,T)\<in>set lvars. is_type G T) &
- (let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in
+ (let E = (G,(map_of lvars)(pns[\<mapsto>]pTs, This\<mapsto>Class C)) in
E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
abbreviation "wf_java_prog == wf_prog wf_java_mdecl"