--- a/src/HOL/Bali/Conform.thy Wed Oct 30 12:44:18 2002 +0100
+++ b/src/HOL/Bali/Conform.thy Thu Oct 31 18:27:10 2002 +0100
@@ -115,6 +115,13 @@
apply (simp add: conf_def)
done
+lemma conf_Boolean: "G,s\<turnstile>v\<Colon>\<preceq>PrimT Boolean \<Longrightarrow> \<exists> b. v=Bool b"
+by (cases v)
+ (auto simp: conf_def obj_ty_def
+ dest: widen_Boolean2
+ split: obj_tag.splits)
+
+
lemma conf_litval [rule_format (no_asm)]:
"typeof (\<lambda>a. None) v = Some T \<longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
apply (unfold conf_def)
@@ -249,6 +256,97 @@
apply force
done
+section "weak value list conformance"
+
+text {* Only if the value is defined it has to conform to its type.
+ This is the contribution of the definite assignment analysis to
+ the notion of conformance. The definite assignment analysis ensures
+ that the program only attempts to access local variables that
+ actually have a defined value in the state.
+ So conformance must only ensure that the
+ defined values are of the right type, and not also that the value
+ is defined.
+*}
+
+
+constdefs
+
+ wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool"
+ ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
+ "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
+
+lemma wlconfD: "\<lbrakk>G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts; Ts n = Some T; vs n = Some v\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
+by (auto simp: wlconf_def)
+
+
+lemma wlconf_cong [simp]: "\<And>s. G,set_locals x s\<turnstile>l[\<sim>\<Colon>\<preceq>]L = G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
+by (auto simp: wlconf_def)
+
+lemma wlconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<sim>\<Colon>\<preceq>]L = G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
+by (auto simp: wlconf_def)
+
+
+lemma wlconf_upd: "\<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow>
+ G,s\<turnstile>l(vn\<mapsto>v)[\<sim>\<Colon>\<preceq>]L"
+by (auto simp: wlconf_def)
+
+lemma wlconf_ext: "\<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<sim>\<Colon>\<preceq>]L(vn\<mapsto>T)"
+by (auto simp: wlconf_def)
+
+lemma wlconf_map_sum [simp]:
+ "G,s\<turnstile>l1 (+) l2[\<sim>\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<sim>\<Colon>\<preceq>]L2)"
+apply (unfold wlconf_def)
+apply safe
+apply (case_tac [3] "n")
+apply (force split add: sum.split)+
+done
+
+lemma wlconf_ext_list [rule_format (no_asm)]: "
+ \<And>X. \<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow>
+ \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns
+ \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<sim>\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
+apply (unfold wlconf_def)
+apply (induct_tac "vns")
+apply clarsimp
+apply clarsimp
+apply (frule list_all2_lengthD)
+apply clarsimp
+done
+
+
+lemma wlconf_deallocL: "\<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L(vn\<mapsto>T); L vn = None\<rbrakk> \<Longrightarrow> G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
+apply (simp only: wlconf_def)
+apply safe
+apply (drule spec)
+apply (drule ospec)
+defer
+apply (drule ospec )
+apply auto
+done
+
+
+lemma wlconf_gext [elim]: "\<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L; s\<le>|s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
+apply (simp only: wlconf_def)
+apply fast
+done
+
+lemma wlconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]empty"
+apply (unfold wlconf_def)
+apply force
+done
+
+lemma wlconf_empty_vals: "G,s\<turnstile>empty[\<sim>\<Colon>\<preceq>]ts"
+ by (simp add: wlconf_def)
+
+lemma wlconf_init_vals [intro!]:
+ " \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<sim>\<Colon>\<preceq>]fs"
+apply (unfold wlconf_def)
+apply force
+done
+
+lemma lconf_wlconf:
+ "G,s\<turnstile>l[\<Colon>\<preceq>]L \<Longrightarrow> G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
+by (force simp add: lconf_def wlconf_def)
section "object conformance"
@@ -259,18 +357,8 @@
(case r of
Heap a \<Rightarrow> is_type G (obj_ty obj)
| Stat C \<Rightarrow> True)"
-(*
-lemma oconf_def2: "G,s\<turnstile>\<lparr>tag=oi,values=fs\<rparr>\<Colon>\<preceq>\<surd>r =
- (G,s\<turnstile>fs[\<Colon>\<preceq>]var_tys G oi r \<and>
- (case r of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>) | Stat C \<Rightarrow> True))"
-by (simp add: oconf_def Let_def)
-*)
-(*
-lemma oconf_def2: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r =
- (G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and>
- (case r of Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> True))"
-by (simp add: oconf_def Let_def)
-*)
+
+
lemma oconf_is_type: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)"
by (auto simp: oconf_def Let_def)
@@ -297,33 +385,16 @@
split add: sum.split_asm obj_tag.split_asm)
done
-(*
-lemma oconf_init_obj_lemma:
-"\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (fields G C);
- \<And>C c f fld. \<lbrakk>class G C = Some c; table_of (fields G C) f = Some fld \<rbrakk>
- \<Longrightarrow> is_type G (type fld);
- (case r of
- Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>)
- | Stat C \<Rightarrow> is_class G C)
-\<rbrakk> \<Longrightarrow> G,s\<turnstile>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>\<Colon>\<preceq>\<surd>r"
-apply (auto simp add: oconf_def)
-apply (drule_tac var_tys_Some_eq [THEN iffD1])
-defer
-apply (subst obj_ty_eq)
-apply(auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm)
-done
-*)
-
-
section "state conformance"
constdefs
conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool" ( "_\<Colon>\<preceq>_" [71,71] 70)
"xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
- (\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and>
- \<spacespace> G,s\<turnstile>l [\<Colon>\<preceq>]L\<spacespace> \<and>
- (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable))"
+ (\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and>
+ \<spacespace> G,s\<turnstile>l [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
+ (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
+ (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None)"
section "conforms"
@@ -331,13 +402,17 @@
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some obj\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
by (auto simp: conforms_def Let_def)
-lemma conforms_localD: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> G,s\<turnstile>locals s[\<Colon>\<preceq>]L"
+lemma conforms_localD: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L"
by (auto simp: conforms_def Let_def)
lemma conforms_XcptLocD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Xcpt (Loc a))\<rbrakk> \<Longrightarrow>
G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)"
by (auto simp: conforms_def Let_def)
+lemma conforms_RetD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Jump Ret)\<rbrakk> \<Longrightarrow>
+ (locals s) Result \<noteq> None"
+by (auto simp: conforms_def Let_def)
+
lemma conforms_RefTD:
"\<lbrakk>G,s\<turnstile>a'\<Colon>\<preceq>RefT t; a' \<noteq> Null; (x,s) \<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow>
\<exists>a obj. a' = Addr a \<and> globs s (Inl a) = Some obj \<and>
@@ -349,8 +424,9 @@
done
lemma conforms_Jump [iff]:
- "((Some (Jump j), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
-by (auto simp: conforms_def)
+ "j=Ret \<longrightarrow> locals s Result \<noteq> None
+ \<Longrightarrow> ((Some (Jump j), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
+by (auto simp: conforms_def Let_def)
lemma conforms_StdXcpt [iff]:
"((Some (Xcpt (Std xn)), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
@@ -382,45 +458,61 @@
done
lemma conformsI: "\<lbrakk>\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r;
- G,s\<turnstile>locals s[\<Colon>\<preceq>]L;
- \<forall>a. x = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)\<rbrakk> \<Longrightarrow>
+ G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L;
+ \<forall>a. x = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable);
+ x = Some (Jump Ret)\<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow>
(x, s)\<Colon>\<preceq>(G, L)"
by (auto simp: conforms_def Let_def)
lemma conforms_xconf: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L);
- \<forall>a. x' = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)\<rbrakk> \<Longrightarrow>
+ \<forall>a. x' = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable);
+ x' = Some (Jump Ret) \<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow>
(x',s)\<Colon>\<preceq>(G,L)"
by (fast intro: conformsI elim: conforms_globsD conforms_localD)
lemma conforms_lupd:
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); L vn = Some T; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x, lupd(vn\<mapsto>v)s)\<Colon>\<preceq>(G, L)"
-by (force intro: conformsI lconf_upd dest: conforms_globsD conforms_localD
- conforms_XcptLocD simp: oconf_def)
+by (force intro: conformsI wlconf_upd dest: conforms_globsD conforms_localD
+ conforms_XcptLocD conforms_RetD
+ simp: oconf_def)
-lemmas conforms_allocL_aux = conforms_localD [THEN lconf_ext]
+lemmas conforms_allocL_aux = conforms_localD [THEN wlconf_ext]
lemma conforms_allocL:
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x, lupd(vn\<mapsto>v)s)\<Colon>\<preceq>(G, L(vn\<mapsto>T))"
-by (force intro: conformsI dest: conforms_globsD
- elim: conforms_XcptLocD conforms_allocL_aux simp: oconf_def)
+by (force intro: conformsI dest: conforms_globsD conforms_RetD
+ elim: conforms_XcptLocD conforms_allocL_aux
+ simp: oconf_def)
-lemmas conforms_deallocL_aux = conforms_localD [THEN lconf_deallocL]
+lemmas conforms_deallocL_aux = conforms_localD [THEN wlconf_deallocL]
lemma conforms_deallocL: "\<And>s.\<lbrakk>s\<Colon>\<preceq>(G, L(vn\<mapsto>T)); L vn = None\<rbrakk> \<Longrightarrow> s\<Colon>\<preceq>(G,L)"
-by (fast intro: conformsI dest: conforms_globsD
+by (fast intro: conformsI dest: conforms_globsD conforms_RetD
elim: conforms_XcptLocD conforms_deallocL_aux)
lemma conforms_gext: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>|s';
\<forall>r. \<forall>obj\<in>globs s' r: G,s'\<turnstile>obj\<Colon>\<preceq>\<surd>r;
locals s'=locals s\<rbrakk> \<Longrightarrow> (x,s')\<Colon>\<preceq>(G,L)"
-by (force intro!: conformsI dest: conforms_localD conforms_XcptLocD)
+apply (rule conformsI)
+apply assumption
+apply (drule conforms_localD) apply force
+apply (intro strip)
+apply (drule (1) conforms_XcptLocD) apply force
+apply (intro strip)
+apply (drule (1) conforms_RetD) apply force
+done
+
lemma conforms_xgext:
- "\<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s\<rbrakk> \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)"
+ "\<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s;dom (locals s') \<subseteq> dom (locals s)\<rbrakk>
+ \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)"
apply (erule_tac conforms_xconf)
-apply (fast dest: conforms_XcptLocD)
+apply (fast dest: conforms_XcptLocD)
+apply (intro strip)
+apply (drule (1) conforms_RetD)
+apply (auto dest: domI)
done
lemma conforms_gupd: "\<And>obj. \<lbrakk>(x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r; s\<le>|gupd(r\<mapsto>obj)s\<rbrakk>
@@ -445,17 +537,29 @@
done
lemma conforms_set_locals:
- "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L'); G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> (x,set_locals l s)\<Colon>\<preceq>(G,L)"
-apply (auto intro!: conformsI dest: conforms_globsD
- elim!: conforms_XcptLocD simp add: oconf_def)
+ "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L'); G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L; x=Some (Jump Ret) \<longrightarrow> l Result \<noteq> None\<rbrakk>
+ \<Longrightarrow> (x,set_locals l s)\<Colon>\<preceq>(G,L)"
+apply (rule conformsI)
+apply (intro strip)
+apply simp
+apply (drule (2) conforms_globsD)
+apply simp
+apply (intro strip)
+apply (drule (1) conforms_XcptLocD)
+apply simp
+apply (intro strip)
+apply (drule (1) conforms_RetD)
+apply simp
done
-lemma conforms_locals [rule_format]:
- "(a,b)\<Colon>\<preceq>(G, L) \<longrightarrow> L x = Some T \<longrightarrow> G,b\<turnstile>the (locals b x)\<Colon>\<preceq>T"
-apply (force simp: conforms_def Let_def lconf_def)
+lemma conforms_locals:
+ "\<lbrakk>(a,b)\<Colon>\<preceq>(G, L); L x = Some T;locals b x \<noteq>None\<rbrakk>
+ \<Longrightarrow> G,b\<turnstile>the (locals b x)\<Colon>\<preceq>T"
+apply (force simp: conforms_def Let_def wlconf_def)
done
-lemma conforms_return: "\<And>s'. \<lbrakk>(x,s)\<Colon>\<preceq>(G, L); (x',s')\<Colon>\<preceq>(G, L'); s\<le>|s'\<rbrakk> \<Longrightarrow>
+lemma conforms_return:
+"\<And>s'. \<lbrakk>(x,s)\<Colon>\<preceq>(G, L); (x',s')\<Colon>\<preceq>(G, L'); s\<le>|s';x'\<noteq>Some (Jump Ret)\<rbrakk> \<Longrightarrow>
(x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)"
apply (rule conforms_xconf)
prefer 2 apply (force dest: conforms_XcptLocD)