--- a/src/HOL/Bali/AxCompl.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/AxCompl.thy Fri Jun 15 13:02:12 2018 +0200
@@ -332,7 +332,7 @@
qed
next
from mgf_hyp'
- show "\<forall>l. G,A\<turnstile>{?Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty}
+ show "\<forall>l. G,A\<turnstile>{?Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars Map.empty}
.init c.
{set_lvars l .; ?R}"
apply (rule MGFnD' [THEN conseq12, THEN allI])
--- a/src/HOL/Bali/AxSem.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/AxSem.thy Fri Jun 15 13:02:12 2018 +0200
@@ -623,7 +623,7 @@
| Init: "\<lbrakk>the (class G C) = c;
G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}
.(if C = Object then Skip else Init (super c)). {Q};
- \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}
+ \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars Map.empty}
.init c. {set_lvars l .; R}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}"
@@ -1088,7 +1088,7 @@
subsubsection "rules derived from Init and Done"
lemma ax_InitS: "\<lbrakk>the (class G C) = c; C \<noteq> Object;
- \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}
+ \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars Map.empty}
.init c. {set_lvars l .; R};
G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}
.Init (super c). {Q}\<rbrakk> \<Longrightarrow>
--- a/src/HOL/Bali/AxSound.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/AxSound.thy Fri Jun 15 13:02:12 2018 +0200
@@ -1350,7 +1350,7 @@
with R s3 invDeclC invC l abrupt_s3
have R': "PROP ?R"
by auto
- have conf_s3': "s3'\<Colon>\<preceq>(G, empty)"
+ have conf_s3': "s3'\<Colon>\<preceq>(G, Map.empty)"
(* we need an arbirary environment (here empty) that s2' conforms to
to apply validE *)
proof -
@@ -2506,7 +2506,7 @@
.(if C = Object then Skip else Init (super c)).
{Q} }\<close>
have valid_init:
- "\<And> l. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty}
+ "\<And> l. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars Map.empty}
.init c.
{set_lvars l .; R} }"
using Init.hyps by simp
@@ -2528,7 +2528,7 @@
eval_super:
"G\<turnstile>Norm ((init_class_obj G C) (store s0))
\<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1" and
- eval_init: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2" and
+ eval_init: "G\<turnstile>(set_lvars Map.empty) s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2" and
s3: "s3 = (set_lvars (locals (store s1))) s2"
using normal_s0 by (auto elim!: evaln_elim_cases)
from wt c have
@@ -2566,18 +2566,18 @@
obtain Q: "Q \<diamondsuit> s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
by (rule validE)
- from cls_C wf have wt_init: "\<lparr>prg=G, cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>"
+ from cls_C wf have wt_init: "\<lparr>prg=G, cls=C,lcl=Map.empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>"
by (rule wf_prog_cdecl [THEN wf_cdecl_wt_init])
from cls_C wf obtain I where
- "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<^sub>s\<guillemotright> I"
+ "\<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<^sub>s\<guillemotright> I"
by (rule wf_prog_cdecl [THEN wf_cdeclE,simplified]) blast
(* simplified: to rewrite \<langle>init c\<rangle> to In1r (init c) *)
then obtain I' where
da_init:
- "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>dom (locals (store ((set_lvars empty) s1)))
+ "\<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile>dom (locals (store ((set_lvars Map.empty) s1)))
\<guillemotright>\<langle>init c\<rangle>\<^sub>s\<guillemotright> I'"
by (rule da_weakenE) simp
- have conf_s1_empty: "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
+ have conf_s1_empty: "(set_lvars Map.empty) s1\<Colon>\<preceq>(G, Map.empty)"
proof -
from eval_super have
"G\<turnstile>Norm ((init_class_obj G C) (store s0))
@@ -2595,8 +2595,8 @@
obtain l where l: "l = locals (store s1)"
by simp
with Q
- have Q': "(Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty)
- \<diamondsuit> ((set_lvars empty) s1) Z"
+ have Q': "(Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars Map.empty)
+ \<diamondsuit> ((set_lvars Map.empty) s1) Z"
by auto
from valid_init Q' valid_A conf_s1_empty eval_init wt_init da_init
have "(set_lvars l .; R) \<diamondsuit> s2 Z"
--- a/src/HOL/Bali/Conform.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/Conform.thy Fri Jun 15 13:02:12 2018 +0200
@@ -237,7 +237,7 @@
apply fast
done
-lemma lconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<Colon>\<preceq>]empty"
+lemma lconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<Colon>\<preceq>]Map.empty"
apply (unfold lconf_def)
apply force
done
@@ -320,12 +320,12 @@
apply fast
done
-lemma wlconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]empty"
+lemma wlconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Map.empty"
apply (unfold wlconf_def)
apply force
done
-lemma wlconf_empty_vals: "G,s\<turnstile>empty[\<sim>\<Colon>\<preceq>]ts"
+lemma wlconf_empty_vals: "G,s\<turnstile>Map.empty[\<sim>\<Colon>\<preceq>]ts"
by (simp add: wlconf_def)
lemma wlconf_init_vals [intro!]:
--- a/src/HOL/Bali/DeclConcepts.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy Fri Jun 15 13:02:12 2018 +0200
@@ -1416,7 +1416,7 @@
definition
methd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
"methd G C =
- class_rec G C empty
+ class_rec G C Map.empty
(\<lambda>C c subcls_mthds.
filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
subcls_mthds
@@ -1450,7 +1450,7 @@
then (case methd G statC sig of
None \<Rightarrow> None
| Some statM
- \<Rightarrow> (class_rec G dynC empty
+ \<Rightarrow> (class_rec G dynC Map.empty
(\<lambda>C c subcls_mthds.
subcls_mthds
++
@@ -1493,7 +1493,7 @@
dynlookup :: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
"dynlookup G statT dynC =
(case statT of
- NullT \<Rightarrow> empty
+ NullT \<Rightarrow> Map.empty
| IfaceT I \<Rightarrow> dynimethd G I dynC
| ClassT statC \<Rightarrow> dynmethd G statC dynC
| ArrayT ty \<Rightarrow> dynmethd G Object dynC)"
@@ -1602,7 +1602,7 @@
lemma methd_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>
methd G C
= (if C = Object
- then empty
+ then Map.empty
else filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
(methd G (super c)))
++ table_of (map (\<lambda>(s,m). (s,C,m)) (methods c))"
@@ -1827,7 +1827,7 @@
(\<lambda>_ dynM. G,sig \<turnstile> dynM overrides statM \<or> dynM = statM)
(methd G C)"
let ?class_rec =
- "\<lambda>C. class_rec G C empty
+ "\<lambda>C. class_rec G C Map.empty
(\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C))"
from statM Subcls ws subclseq_dynC_statC
have dynmethd_dynC_def:
@@ -2133,7 +2133,7 @@
lemma dynlookup_cases:
assumes "dynlookup G statT dynC sig = x"
- obtains (NullT) "statT = NullT" and "empty sig = x"
+ obtains (NullT) "statT = NullT" and "Map.empty sig = x"
| (IfaceT) I where "statT = IfaceT I" and "dynimethd G I dynC sig = x"
| (ClassT) statC where "statT = ClassT statC" and "dynmethd G statC dynC sig = x"
| (ArrayT) ty where "statT = ArrayT ty" and "dynmethd G Object dynC sig = x"
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Fri Jun 15 13:02:12 2018 +0200
@@ -605,16 +605,16 @@
from hyp_s1 [OF _ _ wt_super G]
have "?Jmp jmps s1"
by simp
- hence jmp_s1: "?Jmp jmps ((set_lvars empty) s1)" by (cases s1) simp
+ hence jmp_s1: "?Jmp jmps ((set_lvars Map.empty) s1)" by (cases s1) simp
from False Init.hyps
- have "?HypObj (In1r (init c)) ((set_lvars empty) s1) s2 (\<diamondsuit>::vals)"
+ have "?HypObj (In1r (init c)) ((set_lvars Map.empty) s1) s2 (\<diamondsuit>::vals)"
apply (simp (no_asm_use) only: False if_False simp_thms)
apply (erule conjE)+
apply assumption
done
note hyp_init_c = this [rule_format (no_asm)]
from wf_cdecl
- have wt_init_c: "\<lparr>prg = G, cls = C, lcl = empty\<rparr>\<turnstile>init c\<Colon>\<surd>"
+ have wt_init_c: "\<lparr>prg = G, cls = C, lcl = Map.empty\<rparr>\<turnstile>init c\<Colon>\<surd>"
by (rule wf_cdecl_wt_init)
from wf_cdecl have "jumpNestingOkS {} (init c)"
by (cases rule: wf_cdeclE)
@@ -3498,7 +3498,7 @@
obtain eval_initC:
"prg Env\<turnstile>Norm ((init_class_obj G C) s0)
\<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and
- eval_init: "prg Env\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and
+ eval_init: "prg Env\<turnstile>(set_lvars Map.empty) s1 \<midarrow>init c\<rightarrow> s2" and
s3: "s3=(set_lvars (locals (store s1))) s2"
by simp
have "?NormalAssigned s3 A"
--- a/src/HOL/Bali/Eval.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/Eval.thy Fri Jun 15 13:02:12 2018 +0200
@@ -346,7 +346,7 @@
(case k of
EName e
\<Rightarrow> (case e of
- VNam v \<Rightarrow> (empty ((pars m)[\<mapsto>]pvs)) v
+ VNam v \<Rightarrow> (Map.empty ((pars m)[\<mapsto>]pvs)) v
| Res \<Rightarrow> None)
| This
\<Rightarrow> (if mode=Static then None else Some a'))
@@ -362,7 +362,7 @@
EName e
\<Rightarrow> (case e of
VNam v
- \<Rightarrow> (empty ((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v
+ \<Rightarrow> (Map.empty ((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v
| Res \<Rightarrow> None)
| This
\<Rightarrow> (if mode=Static then None else Some a')))
@@ -578,7 +578,7 @@
if inited C (globs s0) then s3 = Norm s0
else (G\<turnstile>Norm (init_class_obj G C s0)
\<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
- G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk>
+ G\<turnstile>set_lvars Map.empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk>
\<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
\<comment> \<open>This class initialisation rule is a little bit inaccurate. Look at the
@@ -1022,7 +1022,7 @@
"\<lbrakk>if inited C (globs s0) then s3 = Norm s0
else G\<turnstile>Norm (init_class_obj G C s0)
\<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>
- G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and>
+ G\<turnstile>set_lvars Map.empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and>
s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
apply (rule eval.Init)
--- a/src/HOL/Bali/Evaln.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/Evaln.thy Fri Jun 15 13:02:12 2018 +0200
@@ -185,7 +185,7 @@
if inited C (globs s0) then s3 = Norm s0
else (G\<turnstile>Norm (init_class_obj G C s0)
\<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
- G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and>
+ G\<turnstile>set_lvars Map.empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and>
s3 = restore_lvars s1 s2)\<rbrakk>
\<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
@@ -434,7 +434,7 @@
then s3 = Norm s0
else G\<turnstile>Norm ((init_class_obj G C) s0)
\<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
- G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2 \<and>
+ G\<turnstile>(set_lvars Map.empty) s1 \<midarrow>init c\<rightarrow> s2 \<and>
s3 = (set_lvars (locals (store s1))) s2"
using Init.hyps by simp
ultimately show ?case by (rule eval.Init)
@@ -628,7 +628,7 @@
"if inited C (globs s0) then s3 = Norm s0
else (G\<turnstile>Norm (init_class_obj G C s0)
\<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
- G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and>
+ G\<turnstile>set_lvars Map.empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and>
s3 = restore_lvars s1 s2)"
by (auto intro: evaln_nonstrict max.cobounded1 max.cobounded2)
ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
--- a/src/HOL/Bali/Example.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/Example.thy Fri Jun 15 13:02:12 2018 +0200
@@ -226,7 +226,7 @@
lemmas table_classes_defs =
Classes_def standard_classes_def ObjectC_def SXcptC_def
-lemma table_ifaces [simp]: "table_of Ifaces = empty(HasFoo\<mapsto>HasFooInt)"
+lemma table_ifaces [simp]: "table_of Ifaces = Map.empty(HasFoo\<mapsto>HasFooInt)"
apply (unfold Ifaces_def)
apply (simp (no_asm))
done
@@ -462,13 +462,13 @@
lemmas methd_rec' = methd_rec [OF _ ws_tprg]
lemma imethds_HasFoo [simp]:
- "imethds tprg HasFoo = set_option \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
+ "imethds tprg HasFoo = set_option \<circ> Map.empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
apply (rule trans)
apply (rule imethds_rec')
apply (auto simp add: HasFooInt_def)
done
-lemma methd_tprg_Object [simp]: "methd tprg Object = empty"
+lemma methd_tprg_Object [simp]: "methd tprg Object = Map.empty"
apply (subst methd_rec')
apply (auto simp add: Object_mdecls_def)
done
@@ -518,9 +518,9 @@
lemma Ext_method_inheritance:
"filter_tab (\<lambda>sig m. tprg \<turnstile> Ext inherits method sig m)
- (empty(fst ((\<lambda>(s, m). (s, Base, m)) Base_foo)\<mapsto>
+ (Map.empty(fst ((\<lambda>(s, m). (s, Base, m)) Base_foo)\<mapsto>
snd ((\<lambda>(s, m). (s, Base, m)) Base_foo)))
- = empty"
+ = Map.empty"
proof -
from Base_foo_not_inherited_in_Ext
show ?thesis
@@ -592,7 +592,7 @@
lemma Ext_is_acc_type[simp]: "is_acc_type tprg P (Class Ext)"
by (simp add: is_acc_type_def)
-lemma accmethd_tprg_Object [simp]: "accmethd tprg S Object = empty"
+lemma accmethd_tprg_Object [simp]: "accmethd tprg S Object = Map.empty"
apply (unfold accmethd_def)
apply (simp)
done
@@ -1082,7 +1082,7 @@
subsubsection "well-typedness"
-schematic_goal wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
+schematic_goal wt_test: "\<lparr>prg=tprg,cls=Main,lcl=Map.empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
apply (unfold test_def arr_viewed_from_def)
(* ?pTs = [Class Base] *)
apply (rule wtIs (* ;; *))
@@ -1134,7 +1134,7 @@
subsubsection "definite assignment"
-schematic_goal da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
+schematic_goal da_test: "\<lparr>prg=tprg,cls=Main,lcl=Map.empty(VName e\<mapsto>Class Base)\<rparr>
\<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
apply (unfold test_def arr_viewed_from_def)
apply (rule da.Comp)
@@ -1208,40 +1208,40 @@
abbreviation
"obj_a == \<lparr>tag=Arr (PrimT Boolean) 2
- ,values= 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=(empty(Inl (vee, Base)\<mapsto>Null )
+ ,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 empty\<rparr>"
+ "obj_c == \<lparr>tag=CInst (SXcpt NullPointer),values=CONST Map.empty\<rparr>"
-abbreviation "arr_N == empty(Inl (arr, Base)\<mapsto>Null)"
-abbreviation "arr_a == empty(Inl (arr, Base)\<mapsto>Addr a)"
+abbreviation "arr_N == Map.empty(Inl (arr, Base)\<mapsto>Null)"
+abbreviation "arr_a == Map.empty(Inl (arr, Base)\<mapsto>Addr a)"
abbreviation
- "globs1 == empty(Inr Ext \<mapsto>\<lparr>tag=undefined, values=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=empty\<rparr>)"
+ (Inr Object\<mapsto>\<lparr>tag=undefined, values=Map.empty\<rparr>)"
abbreviation
- "globs2 == empty(Inr Ext \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
- (Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<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)"
-abbreviation "locs3 == empty(VName e\<mapsto>Addr b)"
+abbreviation "locs3 == Map.empty(VName e\<mapsto>Addr b)"
abbreviation "locs8 == locs3(VName z\<mapsto>Addr c)"
-abbreviation "s0 == st empty empty"
+abbreviation "s0 == st Map.empty Map.empty"
abbreviation "s0' == Norm s0"
-abbreviation "s1 == st globs1 empty"
+abbreviation "s1 == st globs1 Map.empty"
abbreviation "s1' == Norm s1"
-abbreviation "s2 == st globs2 empty"
+abbreviation "s2 == st globs2 Map.empty"
abbreviation "s2' == Norm s2"
abbreviation "s3 == st globs3 locs3"
abbreviation "s3' == Norm s3"
--- a/src/HOL/Bali/State.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/State.thy Fri Jun 15 13:02:12 2018 +0200
@@ -191,10 +191,10 @@
"var_tys G oi r =
(case r of
Heap a \<Rightarrow> (case oi of
- CInst C \<Rightarrow> fields_table G C (\<lambda>n f. \<not>static f) (+) empty
- | Arr T k \<Rightarrow> empty (+) arr_comps T k)
+ CInst C \<Rightarrow> fields_table G C (\<lambda>n f. \<not>static f) (+) Map.empty
+ | Arr T k \<Rightarrow> Map.empty (+) arr_comps T k)
| Stat C \<Rightarrow> fields_table G C (\<lambda>fn f. declclassf fn = C \<and> static f)
- (+) empty)"
+ (+) Map.empty)"
lemma var_tys_Some_eq:
"var_tys G oi r n = Some T
@@ -285,7 +285,7 @@
abbreviation init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table"
where "init_vals vs == map_option default_val \<circ> vs"
-lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty"
+lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = Map.empty"
apply (unfold arr_comps_def in_bounds_def)
apply (rule ext)
apply auto
@@ -697,7 +697,7 @@
initd :: "qtname \<Rightarrow> state \<Rightarrow> bool"
where "initd C = inited C \<circ> globs \<circ> store"
-lemma not_inited_empty [simp]: "\<not>inited C empty"
+lemma not_inited_empty [simp]: "\<not>inited C Map.empty"
apply (unfold inited_def)
apply (simp (no_asm))
done
--- a/src/HOL/Bali/Table.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/Table.thy Fri Jun 15 13:02:12 2018 +0200
@@ -65,10 +65,10 @@
then Some new_val
else Some old_val))))"
-lemma cond_override_empty1[simp]: "cond_override c empty t = t"
+lemma cond_override_empty1[simp]: "cond_override c Map.empty t = t"
by (simp add: cond_override_def fun_eq_iff)
-lemma cond_override_empty2[simp]: "cond_override c t empty = t"
+lemma cond_override_empty2[simp]: "cond_override c t Map.empty = t"
by (simp add: cond_override_def fun_eq_iff)
lemma cond_override_None[simp]:
@@ -103,13 +103,13 @@
None \<Rightarrow> None
| Some x \<Rightarrow> if c k x then Some x else None))"
-lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
+lemma filter_tab_empty[simp]: "filter_tab c Map.empty = Map.empty"
by (simp add: filter_tab_def empty_def)
lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t"
by (simp add: fun_eq_iff filter_tab_def)
-lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty"
+lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = Map.empty"
by (simp add: fun_eq_iff filter_tab_def empty_def)
lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t"
@@ -144,7 +144,7 @@
by (auto simp add: filter_tab_def fun_eq_iff)
lemma filter_tab_all_False:
- "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty"
+ "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = Map.empty"
by (auto simp add: filter_tab_def fun_eq_iff)
lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
@@ -328,10 +328,10 @@
"t hiding s entails R \<Longrightarrow> t k = Some x \<Longrightarrow> s k = Some y \<Longrightarrow> R x y"
by (simp add: hiding_entails_def)
-lemma empty_hiding_entails [simp]: "empty hiding s entails R"
+lemma empty_hiding_entails [simp]: "Map.empty hiding s entails R"
by (simp add: hiding_entails_def)
-lemma hiding_empty_entails [simp]: "t hiding empty entails R"
+lemma hiding_empty_entails [simp]: "t hiding Map.empty entails R"
by (simp add: hiding_entails_def)
@@ -341,10 +341,10 @@
"\<lbrakk>t hiding s under C entails R; t k = Some x; s k = Some y; C x y\<rbrakk> \<Longrightarrow> R x y"
by (simp add: cond_hiding_entails_def)
-lemma empty_cond_hiding_entails[simp]: "empty hiding s under C entails R"
+lemma empty_cond_hiding_entails[simp]: "Map.empty hiding s under C entails R"
by (simp add: cond_hiding_entails_def)
-lemma cond_hiding_empty_entails[simp]: "t hiding empty under C entails R"
+lemma cond_hiding_empty_entails[simp]: "t hiding Map.empty under C entails R"
by (simp add: cond_hiding_entails_def)
lemma hidings_entailsD: "\<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y"
--- a/src/HOL/Bali/TypeSafe.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Fri Jun 15 13:02:12 2018 +0200
@@ -814,7 +814,7 @@
lemma conforms_init_lvars_lemma: "\<lbrakk>wf_prog G;
wf_mhead G P sig mh;
list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig)\<rbrakk> \<Longrightarrow>
- G,s\<turnstile>empty (pars mh[\<mapsto>]pvs)
+ G,s\<turnstile>Map.empty (pars mh[\<mapsto>]pvs)
[\<sim>\<Colon>\<preceq>]table_of lvars(pars mh[\<mapsto>]parTs sig)"
apply (unfold wf_mhead_def)
apply clarify
@@ -1561,7 +1561,7 @@
have static_m': "is_static m = static m"
by simp
from len
- have dom_vnames: "dom (empty(pars m[\<mapsto>]pvs))=set (pars m)"
+ have dom_vnames: "dom (Map.empty(pars m[\<mapsto>]pvs))=set (pars m)"
by (simp add: dom_map_upds)
show ?thesis
proof (cases "static m")
@@ -2289,14 +2289,14 @@
eval_init_super:
"G\<turnstile>Norm ((init_class_obj G C) s0)
\<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and
- eval_init: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and
+ eval_init: "G\<turnstile>(set_lvars Map.empty) s1 \<midarrow>init c\<rightarrow> s2" and
s3: "s3 = (set_lvars (locals (store s1))) s2"
by simp
have "?TypeSafeObj (Norm ((init_class_obj G C) s0)) s1
(In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
using False Init.hyps by simp
note hyp_init_super = this [rule_format]
- have "?TypeSafeObj ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>"
+ have "?TypeSafeObj ((set_lvars Map.empty) s1) s2 (In1r (init c)) \<diamondsuit>"
using False Init.hyps by simp
note hyp_init_c = this [rule_format]
from conf_s0 wf cls_C False
@@ -2330,29 +2330,29 @@
by - (rule eval_statement_no_jump [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"],
auto)
with conf_s1
- have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
+ have "(set_lvars Map.empty) s1\<Colon>\<preceq>(G, Map.empty)"
by (cases s1) (auto intro: conforms_set_locals)
moreover
from error_free_s1
- have error_free_empty: "error_free ((set_lvars empty) s1)"
+ have error_free_empty: "error_free ((set_lvars Map.empty) s1)"
by simp
- from cls_C wf have wt_init_c: "\<lparr>prg=G, cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>"
+ from cls_C wf have wt_init_c: "\<lparr>prg=G, cls=C,lcl=Map.empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>"
by (rule wf_prog_cdecl [THEN wf_cdecl_wt_init])
moreover from cls_C wf obtain I
- where "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>In1r (init c)\<guillemotright> I"
+ where "\<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile> {} \<guillemotright>In1r (init c)\<guillemotright> I"
by (rule wf_prog_cdecl [THEN wf_cdeclE,simplified]) blast
(* simplified: to rewrite \<langle>init c\<rangle> to In1r (init c) *)
then obtain I' where
- "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>dom (locals (store ((set_lvars empty) s1)))
+ "\<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile>dom (locals (store ((set_lvars Map.empty) s1)))
\<guillemotright>In1r (init c)\<guillemotright> I'"
by (rule da_weakenE) simp
ultimately
- obtain conf_s2: "s2\<Colon>\<preceq>(G, empty)" and error_free_s2: "error_free s2"
+ obtain conf_s2: "s2\<Colon>\<preceq>(G, Map.empty)" and error_free_s2: "error_free s2"
by (rule hyp_init_c [elim_format]) (simp add: error_free_empty)
have "abrupt s2 \<noteq> Some (Jump Ret)"
proof -
from s1_no_ret
- have "\<And> j. abrupt ((set_lvars empty) s1) \<noteq> Some (Jump j)"
+ have "\<And> j. abrupt ((set_lvars Map.empty) s1) \<noteq> Some (Jump j)"
by simp
moreover
from cls_C wf have "jumpNestingOkS {} (init c)"
@@ -2361,7 +2361,7 @@
show ?thesis
using eval_init wt_init_c wf
by - (rule eval_statement_no_jump
- [where ?Env="\<lparr>prg=G,cls=C,lcl=empty\<rparr>"],simp+)
+ [where ?Env="\<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>"],simp+)
qed
with conf_s2 s3 conf_s1 eval_init
have "s3\<Colon>\<preceq>(G, L)"
--- a/src/HOL/Bali/WellForm.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Bali/WellForm.thy Fri Jun 15 13:02:12 2018 +0200
@@ -330,7 +330,7 @@
"\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x"
by (simp add: entails_def)
-lemma empty_entails[simp]: "empty entails P"
+lemma empty_entails[simp]: "Map.empty entails P"
by (simp add: entails_def)
definition
@@ -346,8 +346,8 @@
(\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and>
(\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and>
jumpNestingOkS {} (init c) \<and>
- (\<exists> A. \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<guillemotright> A) \<and>
- \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and>
+ (\<exists> A. \<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<guillemotright> A) \<and>
+ \<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and>
(C \<noteq> Object \<longrightarrow>
(is_acc_class G (pid C) (super c) \<and>
(table_of (map (\<lambda> (s,m). (s,C,m)) (methods c))
@@ -403,8 +403,8 @@
\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f; unique (cfields c);
\<forall>m\<in>set (methods c). wf_mdecl G C m; unique (methods c);
jumpNestingOkS {} (init c);
- \<exists> A. \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<guillemotright> A;
- \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>;
+ \<exists> A. \<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<guillemotright> A;
+ \<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>;
ws_cdecl G C (super c);
(C \<noteq> Object \<longrightarrow>
(is_acc_class G (pid C) (super c) \<and>
@@ -494,7 +494,7 @@
done
lemma wf_cdecl_wt_init:
- "wf_cdecl G (C, c) \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>init c\<Colon>\<surd>"
+ "wf_cdecl G (C, c) \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile>init c\<Colon>\<surd>"
apply (unfold wf_cdecl_def)
apply auto
done
@@ -621,7 +621,7 @@
by (force intro: fields_emptyI)
lemma accfield_Object [simp]:
- "wf_prog G \<Longrightarrow> accfield G S Object = empty"
+ "wf_prog G \<Longrightarrow> accfield G S Object = Map.empty"
apply (unfold accfield_def)
apply (simp (no_asm_simp) add: Let_def)
done
--- a/src/HOL/Hoare/Separation.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Hoare/Separation.thy Fri Jun 15 13:02:12 2018 +0200
@@ -20,7 +20,7 @@
where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}"
definition is_empty :: "heap \<Rightarrow> bool"
- where "is_empty h \<longleftrightarrow> h = empty"
+ where "is_empty h \<longleftrightarrow> h = Map.empty"
definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
where "singl h x y \<longleftrightarrow> dom h = {x} & h x = Some y"
--- a/src/HOL/IMP/Fold.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/IMP/Fold.thy Fri Jun 15 13:02:12 2018 +0200
@@ -192,13 +192,13 @@
lemma approx_empty [simp]:
- "approx empty = (\<lambda>_. True)"
+ "approx Map.empty = (\<lambda>_. True)"
by (auto simp: approx_def)
theorem constant_folding_equiv:
- "fold c empty \<sim> c"
- using approx_eq [of empty c]
+ "fold c Map.empty \<sim> c"
+ using approx_eq [of Map.empty c]
by (simp add: equiv_up_to_True sim_sym)
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Fri Jun 15 13:02:12 2018 +0200
@@ -90,7 +90,7 @@
done
lemma map_of_map_as_map_upd:
- "distinct (map f zs) \<Longrightarrow> map_of (map (\<lambda> p. (f p, g p)) zs) = empty (map f zs [\<mapsto>] map g zs)"
+ "distinct (map f zs) \<Longrightarrow> map_of (map (\<lambda> p. (f p, g p)) zs) = Map.empty (map f zs [\<mapsto>] map g zs)"
by (induct zs) auto
(* In analogy to Map.map_of_SomeD *)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Jun 15 13:02:12 2018 +0200
@@ -83,7 +83,7 @@
list.map map_of.simps map_upds_Cons list.sel)
done
-lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\<mapsto>] (map snd xs))"
+lemma map_of_as_map_upds: "map_of (rev xs) = Map.empty ((map fst xs) [\<mapsto>] (map snd xs))"
by (rule map_of_append [of _ "[]", simplified])
lemma map_of_rev: "unique xs \<Longrightarrow> map_of (rev xs) = map_of xs"
@@ -105,7 +105,7 @@
done
lemma map_upds_takeWhile [rule_format]:
- "\<forall>ks. (empty(rev ks[\<mapsto>]rev xs)) k = Some x \<longrightarrow> length ks = length xs \<longrightarrow>
+ "\<forall>ks. (Map.empty(rev ks[\<mapsto>]rev xs)) k = Some x \<longrightarrow> length ks = length xs \<longrightarrow>
xs ! length (takeWhile (\<lambda>z. z \<noteq> k) ks) = x"
apply (induct xs)
apply simp
@@ -114,7 +114,7 @@
apply (clarify)
apply (drule_tac x=kr in spec)
apply (simp only: rev.simps)
- apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = 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 Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/MicroJava/Comp/DefsComp.thy Fri Jun 15 13:02:12 2018 +0200
@@ -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 ==
- 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/Example.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Fri Jun 15 13:02:12 2018 +0200
@@ -120,12 +120,12 @@
abbreviation
obj1 :: obj where
- "obj1 == (Ext, 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 (empty, empty)"
-abbreviation "s1 == Norm (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
-abbreviation "s2 == Norm (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
-abbreviation "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
+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 "s3 == (Some NP, Map.empty(a\<mapsto>obj1),Map.empty(e\<mapsto>Addr a))"
lemmas map_of_Cons = map_of.simps(2)
@@ -375,7 +375,7 @@
done
lemmas t = ty_expr_ty_exprs_wt_stmt.intros
-schematic_goal wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>
+schematic_goal wt_test: "(tprg, Map.empty(e\<mapsto>Class Base))\<turnstile>
Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
apply (rule ty_expr_ty_exprs_wt_stmt.intros) \<comment> \<open>;;\<close>
apply (rule t) \<comment> \<open>Expr\<close>
--- a/src/HOL/MicroJava/J/Exceptions.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/MicroJava/J/Exceptions.thy Fri Jun 15 13:02:12 2018 +0200
@@ -10,7 +10,7 @@
"blank G C \<equiv> (C,init_vars (fields(G,C)))"
definition start_heap :: "'c prog \<Rightarrow> aheap" where
- "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
+ "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))"
--- a/src/HOL/MicroJava/J/JListExample.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Fri Jun 15 13:02:12 2018 +0200
@@ -162,10 +162,10 @@
append_name({[RefT (ClassT list_name)]}[LAcc l4_name]))"
definition test where
- "test = Predicate.Pred (\<lambda>s. example_prg\<turnstile>Norm (empty, empty) -E-> s)"
+ "test = Predicate.Pred (\<lambda>s. example_prg\<turnstile>Norm (Map.empty, Map.empty) -E-> s)"
lemma test_code [code]:
- "test = exec_i_i_i_o example_prg (Norm (empty, empty)) E"
+ "test = exec_i_i_i_o example_prg (Norm (Map.empty, Map.empty)) E"
by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def)
ML_val \<open>
--- a/src/HOL/MicroJava/J/TypeRel.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Jun 15 13:02:12 2018 +0200
@@ -178,7 +178,7 @@
definition "method" :: "'c prog \<times> cname => (sig \<rightharpoonup> cname \<times> ty \<times> 'c)"
\<comment> \<open>methods of a class, with inheritance, overriding and hiding, cf. 8.4.6\<close>
- where [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
+ where [code]: "method \<equiv> \<lambda>(G,C). class_rec G C Map.empty (\<lambda>C fs ms ts.
ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
definition fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list"
@@ -190,7 +190,7 @@
where [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)\<inverse>)|] ==>
- method (G,C) = (if C = Object then empty else method (G,D)) ++
+ method (G,C) = (if C = Object then Map.empty else method (G,D)) ++
map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
apply (unfold method_def)
apply (simp split del: if_split)
--- a/src/HOL/MicroJava/J/WellForm.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Fri Jun 15 13:02:12 2018 +0200
@@ -266,7 +266,7 @@
lemma field_rec: "\<lbrakk>class G C = Some (D, fs, ms); ws_prog G\<rbrakk>
\<Longrightarrow> field (G, C) =
- (if C = Object then empty else field (G, D)) ++
+ (if C = Object then Map.empty else field (G, D)) ++
map_of (map (\<lambda>(s, f). (s, C, f)) fs)"
apply (simp only: field_def)
apply (frule fields_rec, assumption)
--- a/src/HOL/NanoJava/Example.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/NanoJava/Example.thy Fri Jun 15 13:02:12 2018 +0200
@@ -77,7 +77,7 @@
\<lparr> par=NT, res=Class Nat, lcl=[],
bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This \<rparr>"
-axiomatization where field_Nat [simp]: "field Nat = empty(pred\<mapsto>Class Nat)"
+axiomatization where field_Nat [simp]: "field Nat = Map.empty(pred\<mapsto>Class Nat)"
lemma init_locs_Nat_add [simp]: "init_locs Nat add s = s"
by (simp add: init_locs_def init_vars_def)
@@ -86,7 +86,7 @@
by (simp add: init_locs_def init_vars_def)
lemma upd_obj_new_obj_Nat [simp]:
- "upd_obj a pred v (new_obj a Nat s) = hupd(a\<mapsto>(Nat, empty(pred\<mapsto>v))) s"
+ "upd_obj a pred v (new_obj a Nat s) = hupd(a\<mapsto>(Nat, Map.empty(pred\<mapsto>v))) s"
by (simp add: new_obj_def init_vars_def upd_obj_def Let_def)
--- a/src/HOL/NanoJava/State.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/NanoJava/State.thy Fri Jun 15 13:02:12 2018 +0200
@@ -45,7 +45,7 @@
(type) "state" \<leftharpoondown> (type) "(|heap :: heap, locals :: locals|)"
definition del_locs :: "state => state" where
- "del_locs s \<equiv> s (| locals := empty |)"
+ "del_locs s \<equiv> s (| locals := Map.empty |)"
definition init_locs :: "cname => mname => state => state" where
"init_locs C m s \<equiv> s (| locals := locals s ++
--- a/src/HOL/NanoJava/TypeRel.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy Fri Jun 15 13:02:12 2018 +0200
@@ -93,10 +93,10 @@
where
"class_rec \<equiv> wfrec (subcls1\<inverse>) (\<lambda>rec C f.
case class C of None \<Rightarrow> undefined
- | Some m \<Rightarrow> (if C = Object then empty else rec (super m) f) ++ map_of (f m))"
+ | Some m \<Rightarrow> (if C = Object then Map.empty else rec (super m) f) ++ map_of (f m))"
lemma class_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
- class_rec C f = (if C = Object then empty else class_rec (super m) f) ++
+ class_rec C f = (if C = Object then Map.empty else class_rec (super m) f) ++
map_of (f m)"
apply (drule wf_subcls1)
apply (subst def_wfrec[OF class_rec_def], auto)
@@ -108,7 +108,7 @@
"method C \<equiv> class_rec C methods"
lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
-method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)"
+method C = (if C=Object then Map.empty else method (super m)) ++ map_of (methods m)"
apply (unfold method_def)
apply (erule (1) class_rec [THEN trans])
apply simp
@@ -120,7 +120,7 @@
"field C \<equiv> class_rec C flds"
lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
-field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)"
+field C = (if C=Object then Map.empty else field (super m)) ++ map_of (flds m)"
apply (unfold field_def)
apply (erule (1) class_rec [THEN trans])
apply simp
--- a/src/HOL/Unix/Unix.thy Fri Jun 15 10:45:12 2018 +0200
+++ b/src/HOL/Unix/Unix.thy Fri Jun 15 13:02:12 2018 +0200
@@ -195,7 +195,7 @@
definition
"init users =
Env \<lparr>owner = 0, others = {Readable}\<rparr>
- (\<lambda>u. if u \<in> users then Some (Env \<lparr>owner = u, others = {Readable}\<rparr> empty)
+ (\<lambda>u. if u \<in> users then Some (Env \<lparr>owner = u, others = {Readable}\<rparr> Map.empty)
else None)"
@@ -364,7 +364,7 @@
and "access root path uid {} = Some (Val plain)"
| mkdir:
"root \<midarrow>(Mkdir uid perms path)\<rightarrow>
- update path (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root"
+ update path (Some (Env \<lparr>owner = uid, others = perms\<rparr> Map.empty)) root"
if "path = parent_path @ [name]"
and "access root parent_path uid {Writable} = Some (Env att parent)"
and "access root path uid {} = None"
@@ -372,7 +372,7 @@
"root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root"
if "path = parent_path @ [name]"
and "access root parent_path uid {Writable} = Some (Env att parent)"
- and "access root path uid {} = Some (Env att' empty)"
+ and "access root path uid {} = Some (Env att' Map.empty)"
| readdir:
"root \<midarrow>(Readdir uid names path)\<rightarrow> root"
if "access root path uid {Readable} = Some (Env att dir)"
@@ -822,7 +822,7 @@
definition
"invariant root path \<longleftrightarrow>
(\<exists>att dir.
- access root path user\<^sub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>
+ access root path user\<^sub>1 {} = Some (Env att dir) \<and> dir \<noteq> Map.empty \<and>
user\<^sub>1 \<noteq> owner att \<and>
access root path user\<^sub>1 {Writable} = None)"
@@ -860,9 +860,9 @@
from inv obtain "file" where "access root bogus_path user\<^sub>1 {} = Some file"
unfolding invariant_def by blast
moreover
- from rmdir obtain att where "access root [user\<^sub>1, name\<^sub>1] user\<^sub>1 {} = Some (Env att empty)"
+ from rmdir obtain att where "access root [user\<^sub>1, name\<^sub>1] user\<^sub>1 {} = Some (Env att Map.empty)"
by cases auto
- then have "access root ([user\<^sub>1, name\<^sub>1] @ [name\<^sub>2]) user\<^sub>1 {} = empty name\<^sub>2"
+ then have "access root ([user\<^sub>1, name\<^sub>1] @ [name\<^sub>2]) user\<^sub>1 {} = Map.empty name\<^sub>2"
by (simp only: access_empty_lookup lookup_append_some) simp
ultimately show False by (simp add: bogus_path_def)
qed
@@ -898,7 +898,7 @@
proof -
from inv obtain att dir where
inv1: "access root path user\<^sub>1 {} = Some (Env att dir)" and
- inv2: "dir \<noteq> empty" and
+ inv2: "dir \<noteq> Map.empty" and
inv3: "user\<^sub>1 \<noteq> owner att" and
inv4: "access root path user\<^sub>1 {Writable} = None"
by (auto simp add: invariant_def)
@@ -969,7 +969,7 @@
obtain dir' where
lookup': "lookup root' path = Some (Env att dir')" and
- inv2': "dir' \<noteq> empty"
+ inv2': "dir' \<noteq> Map.empty"
proof (cases ys)
assume "ys = []"
with path have parent: "path_of x = path @ [y]" by simp
@@ -978,7 +978,7 @@
by cases auto
with lookup parent have "lookup root' path = Some (Env att (dir(y\<mapsto>file)))"
by (simp only: update_append_some update_cons_nil_env)
- moreover have "dir(y\<mapsto>file) \<noteq> empty" by simp
+ moreover have "dir(y\<mapsto>file) \<noteq> Map.empty" by simp
ultimately show ?thesis ..
next
fix z zs assume ys: "ys = z # zs"
@@ -1009,7 +1009,7 @@
qed
with ys show ?thesis using that by auto
qed
- also have "dir(y\<mapsto>file') \<noteq> empty" by simp
+ also have "dir(y\<mapsto>file') \<noteq> Map.empty" by simp
ultimately show ?thesis ..
qed