Commit 5937172c authored by nipkow's avatar nipkow
Browse files

adapted to devel

parent c5634d89c985
......@@ -271,8 +271,8 @@ proof
qed auto
lemma map_add_eq_empty_conv[simp]:
"(empty = f++g) \<longleftrightarrow> f=empty \<and> g=empty"
"(f++g = empty) \<longleftrightarrow> f=empty \<and> g=empty"
"(Map.empty = f++g) \<longleftrightarrow> f=Map.empty \<and> g=Map.empty"
"(f++g = Map.empty) \<longleftrightarrow> f=Map.empty \<and> g=Map.empty"
apply (metis map_add_empty map_add_subsumed1 map_le_map_add)
by (metis map_add_None)
......@@ -2429,7 +2429,7 @@ lemma map_of_None_filterD:
"map_of xs x = None \<Longrightarrow> map_of (filter P xs) x = None"
by(induct xs) auto
lemma map_of_concat: "map_of (concat xss) = foldr (\<lambda>xs f. f ++ map_of xs) xss empty"
lemma map_of_concat: "map_of (concat xss) = foldr (\<lambda>xs f. f ++ map_of xs) xss Map.empty"
by(induct xss) simp_all
lemma map_of_Some_split:
......@@ -4060,7 +4060,7 @@ subsection "Maps"
lemma ran_add[simp]: "dom f \<inter> dom g = {} \<Longrightarrow> ran (f++g) = ran f \<union> ran g" by (fastforce simp add: ran_def map_add_def split: option.split_asm option.split)
lemma nempty_dom: "\<lbrakk>e\<noteq>empty; !!m. m\<in>dom e \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
lemma nempty_dom: "\<lbrakk>e\<noteq>Map.empty; !!m. m\<in>dom e \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
by (subgoal_tac "dom e \<noteq> {}") (blast, auto)
......@@ -4306,10 +4306,10 @@ proof (rule set_eqI)
by auto
qed
lemma map_to_set_empty[simp]: "map_to_set empty = {}"
lemma map_to_set_empty[simp]: "map_to_set Map.empty = {}"
unfolding map_to_set_def by simp
lemma set_to_map_empty[simp]: "set_to_map {} = empty"
lemma set_to_map_empty[simp]: "set_to_map {} = Map.empty"
unfolding set_to_map_def[abs_def] by simp
lemma map_to_set_empty_iff: "map_to_set m = {} \<longleftrightarrow> m = Map.empty"
......
......@@ -39,7 +39,7 @@ declare [[code drop: Mapping.is_empty]]
lemma is_empty_transfer [transfer_rule]:
includes lifting_syntax
shows "(pcr_mapping (=) (=) ===> (=)) (\<lambda>m. m = empty) Mapping.is_empty"
shows "(pcr_mapping (=) (=) ===> (=)) (\<lambda>m. m = Map.empty) Mapping.is_empty"
unfolding mapping.pcr_cr_eq
apply(rule rel_funI)
apply(case_tac y)
......
......@@ -190,7 +190,7 @@ apply auto
done
lemma lconf_empty[iff]: "P,h \<turnstile> empty (:\<le>)\<^sub>w E"
lemma lconf_empty[iff]: "P,h \<turnstile> Map.empty (:\<le>)\<^sub>w E"
by(simp add:lconf_def)
lemma lconf_upd2: "\<lbrakk>P,h \<turnstile> l (:\<le>)\<^sub>w E; P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> P,h \<turnstile> l(V\<mapsto>v) (:\<le>)\<^sub>w E(V\<mapsto>T)"
......
......@@ -28,7 +28,7 @@ definition addr_of_sys_xcpt :: "cname \<Rightarrow> addr" where
if s = OutOfMemory then 2 else undefined"
definition start_heap :: "prog \<Rightarrow> heap" where
"start_heap P \<equiv> empty (addr_of_sys_xcpt NullPointer \<mapsto> blank P NullPointer)
"start_heap P \<equiv> Map.empty (addr_of_sys_xcpt NullPointer \<mapsto> blank P NullPointer)
(addr_of_sys_xcpt ClassCast \<mapsto> blank P ClassCast)
(addr_of_sys_xcpt OutOfMemory \<mapsto> blank P OutOfMemory)"
......
......@@ -519,7 +519,7 @@ lift_definition new_Addr' :: "heap' \<Rightarrow> addr option" is "new_Addr" .
lift_definition start_heap' :: "prog \<Rightarrow> heap'" is "start_heap" .
lemma start_heap'_code [code]:
"start_heap' P = empty (addr_of_sys_xcpt NullPointer \<mapsto> blank' P NullPointer)
"start_heap' P = Map.empty (addr_of_sys_xcpt NullPointer \<mapsto> blank' P NullPointer)
(addr_of_sys_xcpt ClassCast \<mapsto> blank' P ClassCast)
(addr_of_sys_xcpt OutOfMemory \<mapsto> blank' P OutOfMemory)"
by transfer(simp add: start_heap_def)
......@@ -1096,20 +1096,20 @@ declare [[values_timeout = 180]]
values [expected "{Val (Intg 5)}"]
"{fst (e', s') | e' s'.
[],empty \<turnstile> \<langle>{''V'':Integer; ''V'' := Val(Intg 5);; Var ''V''},(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
[],Map.empty \<turnstile> \<langle>{''V'':Integer; ''V'' := Val(Intg 5);; Var ''V''},(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Val (Intg 11)}"]
"{fst (e', s') | e' s'.
[],empty \<turnstile> \<langle>(Val(Intg 5)) \<guillemotleft>Add\<guillemotright> (Val(Intg 6)),(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
[],Map.empty \<turnstile> \<langle>(Val(Intg 5)) \<guillemotleft>Add\<guillemotright> (Val(Intg 6)),(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Val (Intg 83)}"]
"{fst (e', s') | e' s'.
[],[''V''\<mapsto>Integer] \<turnstile> \<langle>(Var ''V'') \<guillemotleft>Add\<guillemotright> (Val(Intg 6)),
(empty,[''V''\<mapsto>Intg 77])\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
(Map.empty,[''V''\<mapsto>Intg 77])\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Some (Intg 6)}"]
"{lcl' (snd (e', s')) ''V'' | e' s'.
[],[''V''\<mapsto>Integer] \<turnstile> \<langle>''V'' := Val(Intg 6),(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
[],[''V''\<mapsto>Integer] \<turnstile> \<langle>''V'' := Val(Intg 6),(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Some (Intg 12)}"]
"{lcl' (snd (e', s')) ''mult'' | e' s'.
......@@ -1119,7 +1119,7 @@ values [expected "{Some (Intg 12)}"]
while (Var ''V'' \<guillemotleft>Eq\<guillemotright> Val(Intg 1))((''mult'' := Var ''mult'' \<guillemotleft>Add\<guillemotright> Var ''b'');;
(''a'' := Var ''a'' \<guillemotleft>Add\<guillemotright> Val(Intg (- 1)));;
(''V'' := (if(Var ''a'' \<guillemotleft>Eq\<guillemotright> Val(Intg 0)) Val(Intg 0) else Val(Intg 1)))),
(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Val (Intg 30)}"]
"{fst (e', s') | e' s'.
......@@ -1127,7 +1127,7 @@ values [expected "{Val (Intg 30)}"]
\<turnstile> \<langle>''a'' := Val(Intg 17);; ''b'' := Val(Intg 13);;
''c'' := Val(Intg 42);; ''cond'' := true;;
if (Var ''cond'') (Var ''a'' \<guillemotleft>Add\<guillemotright> Var ''b'') else (Var ''a'' \<guillemotleft>Add\<guillemotright> Var ''c''),
(empty,empty)\<rangle> \<Rightarrow>' \<langle>e',s'\<rangle>}"
(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e',s'\<rangle>}"
text {* progOverrider examples *}
......@@ -1162,81 +1162,81 @@ definition
values [expected "{Val(Ref(0,[''Bottom'',''Left'']))}"] \<comment> \<open>dynCastSide\<close>
"{fst (e', s') | e' s'.
progOverrider,[''V''\<mapsto>Class ''Right''] \<turnstile>
\<langle>''V'' := new ''Bottom'' ;; Cast ''Left'' (Var ''V''),(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
\<langle>''V'' := new ''Bottom'' ;; Cast ''Left'' (Var ''V''),(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Val(Ref(0,[''Right'']))}"] \<comment> \<open>dynCastViaSh\<close>
"{fst (e', s') | e' s'.
progOverrider,[''V''\<mapsto>Class ''Right2''] \<turnstile>
\<langle>''V'' := new ''Right'' ;; Cast ''Right'' (Var ''V''),(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
\<langle>''V'' := new ''Right'' ;; Cast ''Right'' (Var ''V''),(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Val (Intg 42)}"] \<comment> \<open>block\<close>
"{fst (e', s') | e' s'.
progOverrider,[''V''\<mapsto>Integer]
\<turnstile> \<langle>''V'' := Val(Intg 42) ;; {''V'':Class ''Left''; ''V'' := new ''Bottom''} ;; Var ''V'',
(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Val (Intg 8)}"] \<comment> \<open>staticCall\<close>
"{fst (e', s') | e' s'.
progOverrider,[''V''\<mapsto>Class ''Right'',''W''\<mapsto>Class ''Bottom'']
\<turnstile> \<langle>''V'' := new ''Bottom'' ;; ''W'' := new ''Bottom'' ;;
((Cast ''Left'' (Var ''W''))\<bullet>''x''{[''Left'',''Top'']} := Val(Intg 3));;
(Var ''W''\<bullet>(''Left''::)''f''([Var ''V'',Val(Intg 2)])),(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
(Var ''W''\<bullet>(''Left''::)''f''([Var ''V'',Val(Intg 2)])),(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Val (Intg 12)}"] \<comment> \<open>call\<close>
"{fst (e', s') | e' s'.
progOverrider,[''V''\<mapsto>Class ''Right2'',''W''\<mapsto>Class ''Left'']
\<turnstile> \<langle>''V'' := new ''Right'' ;; ''W'' := new ''Left'' ;;
(Var ''V''\<bullet>''f''([Var ''W'',Val(Intg 42)])) \<guillemotleft>Add\<guillemotright> (Var ''W''\<bullet>''f''([Var ''V'',Val(Intg 13)])),
(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Val(Intg 13)}"] \<comment> \<open>callOverrider\<close>
"{fst (e', s') | e' s'.
progOverrider,[''V''\<mapsto>Class ''Right2'',''W''\<mapsto>Class ''Left'']
\<turnstile> \<langle>''V'' := new ''Bottom'';; (Var ''V'' \<bullet> ''x'' {[''Right2'',''Top'']} := Val(Intg 6));;
''W'' := new ''Left'' ;; Var ''V''\<bullet>''f''([Var ''W'',Val(Intg 42)]),
(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Val(Ref(1,[''Left'',''Top'']))}"] \<comment> \<open>callClass\<close>
"{fst (e', s') | e' s'.
progOverrider,[''V''\<mapsto>Class ''Right2'']
\<turnstile> \<langle>''V'' := new ''Right'' ;; Var ''V''\<bullet>''g''([]),(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
\<turnstile> \<langle>''V'' := new ''Right'' ;; Var ''V''\<bullet>''g''([]),(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Val(Intg 42)}"] \<comment> \<open>fieldAss\<close>
"{fst (e', s') | e' s'.
progOverrider,[''V''\<mapsto>Class ''Right2'']
\<turnstile> \<langle>''V'' := new ''Right'' ;;
(Var ''V''\<bullet>''x''{[''Right2'',''Top'']} := (Val(Intg 42))) ;;
(Var ''V''\<bullet>''x''{[''Right2'',''Top'']}),(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
(Var ''V''\<bullet>''x''{[''Right2'',''Top'']}),(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
text {* typing rules *}
values [expected "{Class ''Bottom''}"] \<comment> \<open>typeNew\<close>
"{T. progOverrider,empty \<turnstile> new ''Bottom'' :: T}"
"{T. progOverrider,Map.empty \<turnstile> new ''Bottom'' :: T}"
values [expected "{Class ''Left''}"] \<comment> \<open>typeDynCast\<close>
"{T. progOverrider,empty \<turnstile> Cast ''Left'' (new ''Bottom'') :: T}"
"{T. progOverrider,Map.empty \<turnstile> Cast ''Left'' (new ''Bottom'') :: T}"
values [expected "{Class ''Left''}"] \<comment> \<open>typeStaticCast\<close>
"{T. progOverrider,empty \<turnstile> \<lparr>''Left''\<rparr> (new ''Bottom'') :: T}"
"{T. progOverrider,Map.empty \<turnstile> \<lparr>''Left''\<rparr> (new ''Bottom'') :: T}"
values [expected "{Integer}"] \<comment> \<open>typeVal\<close>
"{T. [],empty \<turnstile> Val(Intg 17) :: T}"
"{T. [],Map.empty \<turnstile> Val(Intg 17) :: T}"
values [expected "{Integer}"] \<comment> \<open>typeVar\<close>
"{T. [],[''V'' \<mapsto> Integer] \<turnstile> Var ''V'' :: T}"
values [expected "{Boolean}"] \<comment> \<open>typeBinOp\<close>
"{T. [],empty \<turnstile> (Val(Intg 5)) \<guillemotleft>Eq\<guillemotright> (Val(Intg 6)) :: T}"
"{T. [],Map.empty \<turnstile> (Val(Intg 5)) \<guillemotleft>Eq\<guillemotright> (Val(Intg 6)) :: T}"
values [expected "{Class ''Top''}"] \<comment> \<open>typeLAss\<close>
"{T. progOverrider,[''V'' \<mapsto> Class ''Top''] \<turnstile> ''V'' := (new ''Left'') :: T}"
values [expected "{Integer}"] \<comment> \<open>typeFAcc\<close>
"{T. progOverrider,empty \<turnstile> (new ''Right'')\<bullet>''x''{[''Right2'',''Top'']} :: T}"
"{T. progOverrider,Map.empty \<turnstile> (new ''Right'')\<bullet>''x''{[''Right2'',''Top'']} :: T}"
values [expected "{Integer}"] \<comment> \<open>typeFAss\<close>
"{T. progOverrider,empty \<turnstile> (new ''Right'')\<bullet>''x''{[''Right2'',''Top'']} :: T}"
"{T. progOverrider,Map.empty \<turnstile> (new ''Right'')\<bullet>''x''{[''Right2'',''Top'']} :: T}"
values [expected "{Integer}"] \<comment> \<open>typeStaticCall\<close>
"{T. progOverrider,[''V''\<mapsto>Class ''Left'']
......@@ -1247,16 +1247,16 @@ values [expected "{Class ''Top''}"] \<comment> \<open>typeCall\<close>
\<turnstile> ''V'' := new ''Right'' ;; Var ''V''\<bullet>''g''([]) :: T}"
values [expected "{Class ''Top''}"] \<comment> \<open>typeBlock\<close>
"{T. progOverrider,empty \<turnstile> {''V'':Class ''Top''; ''V'' := new ''Left''} :: T}"
"{T. progOverrider,Map.empty \<turnstile> {''V'':Class ''Top''; ''V'' := new ''Left''} :: T}"
values [expected "{Integer}"] \<comment> \<open>typeCond\<close>
"{T. [],empty \<turnstile> if (true) Val(Intg 6) else Val(Intg 9) :: T}"
"{T. [],Map.empty \<turnstile> if (true) Val(Intg 6) else Val(Intg 9) :: T}"
values [expected "{Void}"] \<comment> \<open>typeWhile\<close>
"{T. [],empty \<turnstile> while (false) Val(Intg 17) :: T}"
"{T. [],Map.empty \<turnstile> while (false) Val(Intg 17) :: T}"
values [expected "{Void}"] \<comment> \<open>typeThrow\<close>
"{T. progOverrider,empty \<turnstile> throw (new ''Bottom'') :: T}"
"{T. progOverrider,Map.empty \<turnstile> throw (new ''Bottom'') :: T}"
values [expected "{Integer}"] \<comment> \<open>typeBig\<close>
"{T. progOverrider,[''V''\<mapsto>Class ''Right2'',''W''\<mapsto>Class ''Left'']
......@@ -1298,12 +1298,12 @@ definition
values [expected "{Val(Ref(0,[''Bottom'',''Left'']))}"] \<comment> \<open>cast1\<close>
"{fst (e', s') | e' s'.
progDiamond,[''V''\<mapsto>Class ''Left''] \<turnstile> \<langle>''V'' := new ''Bottom'',
(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Val(Ref(0,[''TopSh'']))}"] \<comment> \<open>cast2\<close>
"{fst (e', s') | e' s'.
progDiamond,[''V''\<mapsto>Class ''TopSh''] \<turnstile> \<langle>''V'' := new ''Bottom'',
(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{}"] \<comment> \<open>typeCast3 not typeable\<close>
"{T. progDiamond,[''V''\<mapsto>Class ''TopRep''] \<turnstile> ''V'' := new ''Bottom'' :: T}"
......@@ -1314,33 +1314,33 @@ values [expected "{
}"] \<comment> \<open>cast3\<close>
"{fst (e', s') | e' s'.
progDiamond,[''V''\<mapsto>Class ''TopRep''] \<turnstile> \<langle>''V'' := new ''Bottom'',
(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
values [expected "{Val(Intg 17)}"] \<comment> \<open>fieldAss\<close>
"{fst (e', s') | e' s'.
progDiamond,[''V''\<mapsto>Class ''Bottom'']
\<turnstile> \<langle>''V'' := new ''Bottom'' ;;
((Var ''V'')\<bullet>''x''{[''Bottom'']} := (Val(Intg 17))) ;;
((Var ''V'')\<bullet>''x''{[''Bottom'']}),(empty,empty)\<rangle> \<Rightarrow>' \<langle>e',s'\<rangle>}"
((Var ''V'')\<bullet>''x''{[''Bottom'']}),(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e',s'\<rangle>}"
values [expected "{Val Null}"] \<comment> \<open>dynCastNull\<close>
"{fst (e', s') | e' s'.
progDiamond,empty \<turnstile> \<langle>Cast ''Right'' null,(empty,empty)\<rangle> \<Rightarrow>' \<langle>e',s'\<rangle>}"
progDiamond,Map.empty \<turnstile> \<langle>Cast ''Right'' null,(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e',s'\<rangle>}"
values [expected "{Val (Ref(0, [''Right'']))}"] \<comment> \<open>dynCastViaSh\<close>
"{fst (e', s') | e' s'.
progDiamond,[''V''\<mapsto>Class ''TopSh'']
\<turnstile> \<langle>''V'' := new ''Right'' ;; Cast ''Right'' (Var ''V''),(empty,empty)\<rangle> \<Rightarrow>' \<langle>e',s'\<rangle>}"
\<turnstile> \<langle>''V'' := new ''Right'' ;; Cast ''Right'' (Var ''V''),(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e',s'\<rangle>}"
values [expected "{Val Null}"] \<comment> \<open>dynCastFail\<close>
"{fst (e', s') | e' s'.
progDiamond,[''V''\<mapsto>Class ''TopRep'']
\<turnstile> \<langle>''V'' := new ''Right'' ;; Cast ''Bottom'' (Var ''V''),(empty,empty)\<rangle> \<Rightarrow>' \<langle>e',s'\<rangle>}"
\<turnstile> \<langle>''V'' := new ''Right'' ;; Cast ''Bottom'' (Var ''V''),(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e',s'\<rangle>}"
values [expected "{Val (Ref(0, [''Bottom'', ''Left'']))}"] \<comment> \<open>dynCastSide\<close>
"{fst (e', s') | e' s'.
progDiamond,[''V''\<mapsto>Class ''Right'']
\<turnstile> \<langle>''V'' := new ''Bottom'' ;; Cast ''Left'' (Var ''V''),(empty,empty)\<rangle> \<Rightarrow>' \<langle>e',s'\<rangle>}"
\<turnstile> \<langle>''V'' := new ''Bottom'' ;; Cast ''Left'' (Var ''V''),(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e',s'\<rangle>}"
text {* failing g++ example *}
......@@ -1369,9 +1369,9 @@ definition
values [expected "{Val (Intg 42)}"] \<comment> \<open>callFailGplusplus\<close>
"{fst (e', s') | e' s'.
ProgFailing,empty
ProgFailing,Map.empty
\<turnstile> \<langle>{''V'':Class ''D''; ''V'' := new ''D'';; Var ''V''\<bullet>''f''([])},
(empty,empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
(Map.empty,Map.empty)\<rangle> \<Rightarrow>' \<langle>e', s'\<rangle>}"
end
......@@ -1025,7 +1025,7 @@ next
with select "method" wf have "Ts' = Ts \<and> P \<turnstile> T \<le> T'"
by -(rule select_least_methods_subtypes,simp_all)
hence eqs:"Ts' = Ts" and sub:"P \<turnstile> T \<le> T'" by auto
from wf wtabody have "P,empty(this\<mapsto>Class(last Cs'),pns[\<mapsto>]Ts),h \<turnstile> body : T"
from wf wtabody have "P,Map.empty(this\<mapsto>Class(last Cs'),pns[\<mapsto>]Ts),h \<turnstile> body : T"
by -(rule WT_implies_WTrt,simp_all)
hence wtbody:"P,E(this#pns [\<mapsto>] Class (last Cs')#Ts),h \<turnstile> body : T"
by(rule WTrt_env_mono) simp
......@@ -1096,7 +1096,7 @@ next
with subo' wf lastC have "Subobjs P D ((Cs @\<^sub>p Cs'') @\<^sub>p Cs')"
by (fastforce intro:Subobjs_appendPath)
with Ds have suboDs:"Subobjs P D Ds" by simp
from wtabody have "P,empty(this#pns [\<mapsto>] Class (last Ds)#Ts),h \<turnstile> body : T"
from wtabody have "P,Map.empty(this#pns [\<mapsto>] Class (last Ds)#Ts),h \<turnstile> body : T"
by(rule WT_implies_WTrt)
hence "P,E(this#pns [\<mapsto>] Class (last Ds)#Ts),h \<turnstile> body : T"
by(rule WTrt_env_mono) simp
......
......@@ -432,7 +432,7 @@ proof -
from fin eval noread show "change_respecting \<langle>c, mds, mem\<rangle> \<langle>c', mds', mem'\<rangle> X"
proof (induct "X" arbitrary: mem mem' rule: finite_induct)
case empty
have "mem [\<mapsto> empty] = mem" "mem' [\<mapsto> empty] = mem'"
have "mem [\<mapsto> Map.empty] = mem" "mem' [\<mapsto> Map.empty] = mem'"
unfolding subst_def
by auto
hence "change_respecting \<langle>c, mds, mem\<rangle> \<langle>c', mds', mem'\<rangle> {}"
......
......@@ -291,11 +291,11 @@ qed
lemma state_update_vs_allInstances_generic_empty:
assumes [simp]: "\<And>a. pre_post (mk a) = a"
shows "(mk \<lparr>heap=empty, assocs=A\<rparr>) \<Turnstile> OclAllInstances_generic pre_post Type \<doteq> Set{}"
shows "(mk \<lparr>heap=Map.empty, assocs=A\<rparr>) \<Turnstile> OclAllInstances_generic pre_post Type \<doteq> Set{}"
proof -
have state_update_vs_allInstances_empty:
"(OclAllInstances_generic pre_post Type) (mk \<lparr>heap=empty, assocs=A\<rparr>) =
Set{} (mk \<lparr>heap=empty, assocs=A\<rparr>)"
"(OclAllInstances_generic pre_post Type) (mk \<lparr>heap=Map.empty, assocs=A\<rparr>) =
Set{} (mk \<lparr>heap=Map.empty, assocs=A\<rparr>)"
by(simp add: OclAllInstances_generic_def mtSet_def)
show ?thesis
apply(simp only: OclValid_def, subst StrictRefEq\<^sub>S\<^sub>e\<^sub>t.cp0,
......@@ -511,7 +511,7 @@ shows "is_represented_in_state snd x H \<tau>"
by(rule represented_generic_objects_in_state[OF A[simplified OclAllInstances_at_post_def]])
lemma state_update_vs_allInstances_at_post_empty:
shows "(\<sigma>, \<lparr>heap=empty, assocs=A\<rparr>) \<Turnstile> Type .allInstances() \<doteq> Set{}"
shows "(\<sigma>, \<lparr>heap=Map.empty, assocs=A\<rparr>) \<Turnstile> Type .allInstances() \<doteq> Set{}"
unfolding OclAllInstances_at_post_def
by(rule state_update_vs_allInstances_generic_empty[OF snd_conv])
......@@ -617,7 +617,7 @@ by(rule represented_generic_objects_in_state[OF A[simplified OclAllInstances_at_
lemma state_update_vs_allInstances_at_pre_empty:
shows "(\<lparr>heap=empty, assocs=A\<rparr>, \<sigma>) \<Turnstile> Type .allInstances@pre() \<doteq> Set{}"
shows "(\<lparr>heap=Map.empty, assocs=A\<rparr>, \<sigma>) \<Turnstile> Type .allInstances@pre() \<doteq> Set{}"
unfolding OclAllInstances_at_pre_def
by(rule state_update_vs_allInstances_generic_empty[OF fst_conv])
......
......@@ -681,8 +681,8 @@ by(rule OclAny_allInstances_generic_oclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\
lemma OclAny_allInstances_generic_oclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y2:
assumes [simp]: "\<And>x. pre_post (x, x) = x"
shows "\<exists>\<tau>. (\<tau> \<Turnstile> not ((OclAllInstances_generic pre_post OclAny)->forAll\<^sub>S\<^sub>e\<^sub>t(X|X .oclIsTypeOf(OclAny))))"
proof - fix oid a let ?t0 = "\<lparr>heap = empty(oid \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y (mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>a\<rfloor>)),
assocs = empty\<rparr>" show ?thesis
proof - fix oid a let ?t0 = "\<lparr>heap = Map.empty(oid \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y (mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>a\<rfloor>)),
assocs = Map.empty\<rparr>" show ?thesis
apply(rule_tac x = "(?t0, ?t0)" in exI, simp add: OclValid_def del: OclAllInstances_generic_def)
apply(simp only: UML_Set.OclForall_def refl if_True
OclAllInstances_generic_defined[simplified OclValid_def])
......@@ -1054,7 +1054,7 @@ definition "person9 \<equiv> mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n
text_raw{* \endisatagafp*}
definition
"\<sigma>\<^sub>1 \<equiv> \<lparr> heap = empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid0 \<lfloor>1000\<rfloor>))
"\<sigma>\<^sub>1 \<equiv> \<lparr> heap = Map.empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid0 \<lfloor>1000\<rfloor>))
(oid1 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid1 \<lfloor>1200\<rfloor>))
\<^cancel>\<open>oid2\<close>
(oid3 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid3 \<lfloor>2600\<rfloor>))
......@@ -1063,10 +1063,10 @@ definition
\<^cancel>\<open>oid6\<close>
\<^cancel>\<open>oid7\<close>
(oid8 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person9),
assocs = empty(oid\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<B>\<O>\<S>\<S> \<mapsto> [[[oid0],[oid1]],[[oid3],[oid4]],[[oid5],[oid3]]]) \<rparr>"
assocs = Map.empty(oid\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<B>\<O>\<S>\<S> \<mapsto> [[[oid0],[oid1]],[[oid3],[oid4]],[[oid5],[oid3]]]) \<rparr>"
definition
"\<sigma>\<^sub>1' \<equiv> \<lparr> heap = empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person1)
"\<sigma>\<^sub>1' \<equiv> \<lparr> heap = Map.empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person1)
(oid1 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person2)
(oid2 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person3)
(oid3 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person4)
......@@ -1075,9 +1075,9 @@ definition
(oid6 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person7)
(oid7 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person8)
(oid8 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person9),
assocs = empty(oid\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<B>\<O>\<S>\<S> \<mapsto> [[[oid0],[oid1]],[[oid1],[oid1]],[[oid5],[oid6]],[[oid6],[oid6]]]) \<rparr>"
assocs = Map.empty(oid\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<B>\<O>\<S>\<S> \<mapsto> [[[oid0],[oid1]],[[oid1],[oid1]],[[oid5],[oid6]],[[oid6],[oid6]]]) \<rparr>"
definition "\<sigma>\<^sub>0 \<equiv> \<lparr> heap = empty, assocs = empty \<rparr>"
definition "\<sigma>\<^sub>0 \<equiv> \<lparr> heap = Map.empty, assocs = Map.empty \<rparr>"
lemma basic_\<tau>_wff: "WFF(\<sigma>\<^sub>1,\<sigma>\<^sub>1')"
......@@ -1320,7 +1320,7 @@ proof -
done
qed
lemma perm_\<sigma>\<^sub>1' : "\<sigma>\<^sub>1' = \<lparr> heap = empty
lemma perm_\<sigma>\<^sub>1' : "\<sigma>\<^sub>1' = \<lparr> heap = Map.empty
(oid8 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person9)
(oid7 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person8)
(oid6 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person7)
......
......@@ -670,8 +670,8 @@ by(rule OclAny_allInstances_generic_oclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\
lemma OclAny_allInstances_generic_oclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y2:
assumes [simp]: "\<And>x. pre_post (x, x) = x"
shows "\<exists>\<tau>. (\<tau> \<Turnstile> not ((OclAllInstances_generic pre_post OclAny)->forAll\<^sub>S\<^sub>e\<^sub>t(X|X .oclIsTypeOf(OclAny))))"
proof - fix oid a let ?t0 = "\<lparr>heap = empty(oid \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y (mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>a\<rfloor>)),
assocs = empty\<rparr>" show ?thesis
proof - fix oid a let ?t0 = "\<lparr>heap = Map.empty(oid \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y (mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>a\<rfloor>)),
assocs = Map.empty\<rparr>" show ?thesis
apply(rule_tac x = "(?t0, ?t0)" in exI, simp add: OclValid_def del: OclAllInstances_generic_def)
apply(simp only: UML_Set.OclForall_def refl if_True
OclAllInstances_generic_defined[simplified OclValid_def])
......@@ -1012,7 +1012,7 @@ definition "person8 \<equiv> mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y
definition "person9 \<equiv> mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid8 \<lfloor>0\<rfloor> None"
definition
"\<sigma>\<^sub>1 \<equiv> \<lparr> heap = empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid0 \<lfloor>1000\<rfloor> \<lfloor>oid1\<rfloor>))
"\<sigma>\<^sub>1 \<equiv> \<lparr> heap = Map.empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid0 \<lfloor>1000\<rfloor> \<lfloor>oid1\<rfloor>))
(oid1 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid1 \<lfloor>1200\<rfloor> None))
\<^cancel>\<open>oid2\<close>
(oid3 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid3 \<lfloor>2600\<rfloor> \<lfloor>oid4\<rfloor>))
......@@ -1021,10 +1021,10 @@ definition
\<^cancel>\<open>oid6\<close>
\<^cancel>\<open>oid7\<close>
(oid8 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person9),
assocs = empty \<rparr>"
assocs = Map.empty \<rparr>"
definition
"\<sigma>\<^sub>1' \<equiv> \<lparr> heap = empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person1)
"\<sigma>\<^sub>1' \<equiv> \<lparr> heap = Map.empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person1)
(oid1 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person2)
(oid2 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person3)
(oid3 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person4)
......@@ -1033,9 +1033,9 @@ definition
(oid6 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person7)
(oid7 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person8)
(oid8 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person9),
assocs = empty \<rparr>"
assocs = Map.empty \<rparr>"
definition "\<sigma>\<^sub>0 \<equiv> \<lparr> heap = empty, assocs = empty \<rparr>"
definition "\<sigma>\<^sub>0 \<equiv> \<lparr> heap = Map.empty, assocs = Map.empty \<rparr>"
lemma basic_\<tau>_wff: "WFF(\<sigma>\<^sub>1,\<sigma>\<^sub>1')"
......@@ -1273,7 +1273,7 @@ proof -
done
qed
lemma perm_\<sigma>\<^sub>1' : "\<sigma>\<^sub>1' = \<lparr> heap = empty
lemma perm_\<sigma>\<^sub>1' : "\<sigma>\<^sub>1' = \<lparr> heap = Map.empty
(oid8 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person9)
(oid7 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person8)
(oid6 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person7)
......
......@@ -30,7 +30,7 @@ lemma map_default_insert:
"map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')"
by(simp add: map_default_def fun_eq_iff)
lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)"
lemma map_default_empty [simp]: "map_default b Map.empty = (\<lambda>a. b)"
by(simp add: fun_eq_iff map_default_def)
lemma map_default_inject:
......@@ -476,7 +476,7 @@ proof -
from fin anf fg show ?thesis
proof(induct "dom f" arbitrary: f)
case empty
from \<open>{} = dom f\<close> have "f = empty" by(auto simp add: dom_def)
from \<open>{} = dom f\<close> have "f = Map.empty" by(auto simp add: dom_def)
thus ?case by(simp add: finfun_const_def upd_const_same)
next
case (insert a' A)
......@@ -514,7 +514,7 @@ proof -
from fin anf fg show ?thesis
proof(induct "dom f" arbitrary: f)
case empty
from \<open>{} = dom f\<close> have "f = empty" by(auto simp add: dom_def)
from \<open>{} = dom f\<close> have "f = Map.empty" by(auto simp add: dom_def)
thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
next
case (insert a' A)
......@@ -742,9 +742,9 @@ lemma finfun_rec_const [simp]: "finfun_rec cnst upd (K$ c) = cnst c"
proof(cases "finite (UNIV :: 'a set)")
case False
hence "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = c" by(simp add: finfun_default_const)
moreover have "(THE g :: 'a \<rightharpoonup> 'b. (K$ c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g) = empty"
moreover have "(THE g :: 'a \<rightharpoonup> 'b. (K$ c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g) = Map.empty"
proof (rule the_equality)
show "(K$ c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
show "(K$ c) = Abs_finfun (map_default c Map.empty) \<and> finite (dom Map.empty) \<and> c \<notin> ran Map.empty"
by(auto simp add: finfun_const_def)
next
fix g :: "'a \<rightharpoonup> 'b"
......@@ -752,8 +752,8 @@ proof(cases "finite (UNIV :: 'a set)")
hence g: "(K$ c) = Abs_finfun (map_default c g)" and fin: "finite (dom g)" and ran: "c \<notin> ran g" by blast+
from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
by(simp add: finfun_const_def)
moreover have "map_default c empty = (\<lambda>a. c)" by simp
ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto)
moreover have "map_default c Map.empty = (\<lambda>a. c)" by simp
ultimately show "g = Map.empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto)
qed
ultimately show ?thesis by(simp add: finfun_rec_def)
next
......@@ -763,9 +763,9 @@ next
show ?thesis
proof(cases "c = undefined")
case True
have the: "The ?the = empty"
have the: "The ?the = Map.empty"
proof (rule the_equality)
from True show "?the empty" by(auto simp add: finfun_const_def)
from True show "?the Map.empty" by(auto simp add: finfun_const_def)
next
fix g'
assume "?the g'"
......@@ -774,7 +774,7 @@ next
from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
with fg have "map_default undefined g' = (\<lambda>a. c)"
by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1, symmetric])
with True show "g' = empty"
with True show "g' = Map.empty"
by -(rule map_default_inject(2)[OF _ fin g], auto)
qed
show ?thesis unfolding finfun_rec_def using \<open>finite UNIV\<close> True
......
......@@ -211,7 +211,7 @@ apply auto
done
(*>*)
lemma lconf_empty[iff]: "P,h \<turnstile> empty (:\<le>) E"
lemma lconf_empty[iff]: "P,h \<turnstile> Map.empty (:\<le>) E"
(*<*)by(simp add:lconf_def)(*>*)
lemma lconf_upd2: "\<lbrakk>P,h \<turnstile> l (:\<le>) E; P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> P,h \<turnstile> l(V\<mapsto>v) (:\<le>) E(V\<mapsto>T)"
......
......@@ -32,7 +32,7 @@ where
definition start_heap :: "'c prog \<Rightarrow> heap"
where
"start_heap G \<equiv> empty (addr_of_sys_xcpt NullPointer \<mapsto> blank G NullPointer)
"start_heap G \<equiv> Map.empty (addr_of_sys_xcpt NullPointer \<mapsto> blank G NullPointer)
(addr_of_sys_xcpt ClassCast \<mapsto> blank G ClassCast)
(addr_of_sys_xcpt OutOfMemory \<mapsto> blank G OutOfMemory)"
......
......@@ -79,11 +79,11 @@ lemma [simp]: "h a = Some(C,fs) \<Longrightarrow> typeof\<^bsub>(h(a\<mapsto>(C,
(*<*)by(induct v) (auto simp:fun_upd_apply)(*>*)
text{* For literal values the first parameter of @{term typeof} can be
set to @{term empty} because they do not contain addresses: *}
set to @{term Map.empty} because they do not contain addresses: *}
abbreviation
typeof :: "val \<Rightarrow> ty option" where
"typeof v == typeof_h empty v"
"typeof v == typeof_h Map.empty v"
lemma typeof_lit_typeof:
"typeof v = Some T \<Longrightarrow> typeof\<^bsub>h\<^esub> v = Some T"
......
......@@ -241,7 +241,7 @@ shows "P \<turnstile> C sees_methods Mm \<Longrightarrow>
using sub
proof (induct rule:converse_rtrancl_induct)
assume "P \<turnstile> C sees_methods Mm"
hence "?Q C C Mm empty" by simp
hence "?Q C C Mm Map.empty" by simp
thus "\<exists>Mm' Mm2. ?Q C C Mm' Mm2" by blast
next
fix C'' C'
......
......@@ -223,7 +223,7 @@ proof (induct rule:red_reds_inducts)
where wtabody: "P,[this#pns [\<mapsto>] Class D#Ts] \<turnstile> body :: T''"
and T''subT: "P \<turnstile> T'' \<le> T" and length_pns: "length pns = length Ts"
by(fastforce simp:wf_mdecl_def simp del:map_upds_twist)
from wtabody have "P,empty(this#pns [\<mapsto>] Class D#Ts),h \<turnstile> body : T''"
from wtabody have "P,Map.empty(this#pns [\<mapsto>] Class D#Ts),h \<turnstile> body : T''"
by(rule WT_implies_WTrt)
hence "P,E(this#pns [\<mapsto>] Class D#Ts),h \<turnstile> body : T''"
by(rule WTrt_env_mono) simp
......
......@@ -161,12 +161,12 @@ qed
notation execute ("_ \<turnstile> ((1\<langle>_,/_\<rangle>) \<Rightarrow>/ \<langle>'_, '_\<rangle>)" [51,0,0] 81)
definition "test1 = [] \<turnstile> \<langle>testExpr1,(empty,empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "test2 = [] \<turnstile> \<langle>testExpr2,(empty,empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "test3 = [] \<turnstile> \<langle>testExpr3,(empty,empty(''V''\<mapsto>Intg 77))\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "test4 = [] \<turnstile> \<langle>testExpr4,(empty,empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "test5 = [(''Object'',('''',[],[])),(''C'',(''Object'',[(''F'',Integer)],[]))] \<turnstile> \<langle>testExpr5,(empty,empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "test6 = [(''Object'',('''',[],[])), classI] \<turnstile> \<langle>testExpr6,(empty,empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "test1 = [] \<turnstile> \<langle>testExpr1,(Map.empty,Map.empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "test2 = [] \<turnstile> \<langle>testExpr2,(Map.empty,Map.empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "test3 = [] \<turnstile> \<langle>testExpr3,(Map.empty,Map.empty(''V''\<mapsto>Intg 77))\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "test4 = [] \<turnstile> \<langle>testExpr4,(Map.empty,Map.empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "test5 = [(''Object'',('''',[],[])),(''C'',(''Object'',[(''F'',Integer)],[]))] \<turnstile> \<langle>testExpr5,(Map.empty,Map.empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "test6 = [(''Object'',('''',[],[])), classI] \<turnstile> \<langle>testExpr6,(Map.empty,Map.empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "V = ''V''"
definition "C = ''C''"
......@@ -189,7 +189,7 @@ ML_val {*
val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 160)), _), _) = Predicate.yield @{code test6};
*}
definition "test7 = [classObject, classL] \<turnstile> \<langle>testExpr_BuildList, (empty,empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "test7 = [classObject, classL] \<turnstile> \<langle>testExpr_BuildList, (Map.empty,Map.empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"
definition "L = ''L''"
definition "N = ''N''"
......@@ -215,7 +215,7 @@ ML_val {*
fs4 (N, L) = SOME @{code Null});
*}
definition "test8 = [classObject, classA] \<turnstile> \<langle>testExpr_ClassA, (empty,empty)\<rangle> \<Rightarrow> \<langle>_,_\<rangle>"