Theory Conform

Up to index of Isabelle/Bali5

theory Conform = State:

(*  Title:      isabelle/Bali/Conform.thy
    ID:         $Id: Conform.thy,v 1.6 2001/05/11 14:41:56 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

Conformance notions for the type soundness proof for Java

design issues:
* lconf allows for (arbitrary) inaccessible values
* "conforms" does not directly imply that the dynamic types of all objects on
  the heap are indeed existing classes. Yet this can be inferred for all
  referenced objs.
*)

theory Conform = State:

types   env_ = "prog × (lname, ty) table" (* same as env of WellType.thy *)


section "extension of global store"

constdefs

  gext    :: "st \<Rightarrow> st \<Rightarrow> bool"                ("_\<le>|_"       [71,71]   70)
   "s\<le>|s' \<equiv> \<forall>r. \<forall>(oi, fs)\<in>globs s r: \<exists>(oi',fs')\<in>globs s' r: oi' = oi"

lemma gext_objD: "\<lbrakk>s\<le>|s'; globs s r = Some (oi, fs)\<rbrakk> \<Longrightarrow> \<exists>fs'. globs s' r = Some (oi, fs')"
apply (simp only: gext_def)
by force

lemma rev_gext_objD: "\<lbrakk>globs s r = Some (oi, fs); s\<le>|s'\<rbrakk> \<Longrightarrow> \<exists>fs'. globs s' r = Some (oi, fs')"
by (auto elim: gext_objD)

lemma init_class_obj_inited: 
   "init_class_obj G C s1\<le>|s2 \<Longrightarrow> inited C (globs s2)"
apply (unfold inited_def init_obj_def)
apply (auto dest!: gext_objD)
done

lemma gext_refl [intro!, simp]: "s\<le>|s"
apply (unfold gext_def)
apply (fast del: fst_splitE)
done

lemma gext_gupd [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>|gupd(r\<mapsto>x)s"
by (auto simp: gext_def)

lemma gext_new [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>|init_obj G oi r s"
apply (simp only: init_obj_def)
apply (erule_tac gext_gupd)
done

lemma gext_trans [elim]: "\<And>X. \<lbrakk>s\<le>|s'; s'\<le>|s''\<rbrakk> \<Longrightarrow> s\<le>|s''" 
by (force simp: gext_def)

lemma gext_upd_gobj [intro!]: "s\<le>|upd_gobj r n v s"
apply (simp only: gext_def)
apply auto
apply (case_tac "ra = r")
apply auto
apply (case_tac "globs s r = None")
apply auto
done

lemma gext_cong1 [simp]: "set_locals l s1\<le>|s2 = s1\<le>|s2"
by (auto simp: gext_def)

lemma gext_cong2 [simp]: "s1\<le>|set_locals l s2 = s1\<le>|s2"
by (auto simp: gext_def)


lemma gext_lupd1 [simp]: "lupd(vn\<mapsto>v)s1\<le>|s2 = s1\<le>|s2"
by (auto simp: gext_def)

lemma gext_lupd2 [simp]: "s1\<le>|lupd(vn\<mapsto>v)s2 = s1\<le>|s2"
by (auto simp: gext_def)


lemma inited_gext: "\<lbrakk>inited C (globs s); s\<le>|s'\<rbrakk> \<Longrightarrow> inited C (globs s')"
apply (unfold inited_def)
apply (auto dest: gext_objD)
done


section "value conformance"

constdefs

  conf  :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool"    ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
           "G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. option_map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T"

lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
by (auto simp: conf_def)

lemma conf_lupd [simp]: "G,lupd(vn\<mapsto>va)s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
by (auto simp: conf_def)

lemma conf_PrimT [simp]: "\<forall>dt. typeof dt v = Some (PrimT t) \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>PrimT t"
apply (simp add: conf_def)
done

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)
apply (rule val.induct)
apply auto
done

lemma conf_Null [simp]: "G,s\<turnstile>Null\<Colon>\<preceq>T = G\<turnstile>NT\<preceq>T"
by (simp add: conf_def)

lemma conf_Addr: "G,s\<turnstile>Addr a\<Colon>\<preceq>T = (\<exists>obj. heap s a = Some obj \<and> G\<turnstile>obj_ty obj\<preceq>T)"
by (auto simp: conf_def)

lemma conf_AddrI:"\<lbrakk>heap s a = Some obj; G\<turnstile>obj_ty obj\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T"
apply (rule conf_Addr [THEN iffD2])
by fast

lemma defval_conf [rule_format (no_asm), elim]: 
  "is_type G T \<longrightarrow> G,s\<turnstile>default_val T\<Colon>\<preceq>T"
apply (unfold conf_def)
apply (induct "T")
apply (auto intro: prim_ty.induct)
done

lemma conf_widen [rule_format (no_asm), elim]: 
  "G\<turnstile>T\<preceq>T' \<Longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T \<longrightarrow> ws_prog G \<longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T'"
apply (unfold conf_def)
apply (rule val.induct)
apply (auto elim: ws_widen_trans)
done

lemma conf_gext [rule_format (no_asm), elim]: "G,s\<turnstile>v\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T"
apply (unfold gext_def conf_def)
apply (rule val.induct)
apply force+
done


lemma conf_list_widen [rule_format (no_asm)]: "ws_prog G \<Longrightarrow>  \<forall>Ts Ts'. list_all2 (conf G s) vs Ts \<longrightarrow>   G\<turnstile>Ts[\<preceq>] Ts' \<longrightarrow> list_all2 (conf G s) vs Ts'"
apply (unfold widens_def)
apply (rule list_all2_trans)
apply auto
done

lemma conf_RefTD [rule_format (no_asm)]: "G,s\<turnstile>a'\<Colon>\<preceq>RefT T \<longrightarrow> a' = Null \<or>  
 (\<exists>a oi vs T'. a' = Addr a \<and> heap s a = Some (oi,vs) \<and>  
               obj_ty (oi,vs) = T' \<and> G\<turnstile>T'\<preceq>RefT T)"
apply (unfold conf_def)
apply (induct_tac "a'")
apply (auto dest: widen_PrimT)
done


section "value list conformance"

constdefs

  lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool"
                                                ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
           "G,s\<turnstile>vs[\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"

lemma lconfD: "\<lbrakk>G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T\<rbrakk> \<Longrightarrow> G,s\<turnstile>(the (vs n))\<Colon>\<preceq>T"
by (force simp: lconf_def)


lemma lconf_cong [simp]: "\<And>s. G,set_locals x s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L"
by (auto simp: lconf_def)

lemma lconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L"
by (auto simp: lconf_def)

(* unused *)
lemma lconf_new: "\<lbrakk>L vn = None; G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L"
by (auto simp: lconf_def)

lemma lconf_upd: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow>  
  G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L"
by (auto simp: lconf_def)

lemma lconf_ext: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L(vn\<mapsto>T)"
by (auto simp: lconf_def)

lemma lconf_map_sum [simp]: 
 "G,s\<turnstile>l1 (+) l2[\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<Colon>\<preceq>]L2)"
apply (unfold lconf_def)
apply safe
apply (case_tac [3] "n")
apply (force split add: sum.split)+
done

lemma lconf_ext_list [rule_format (no_asm)]: "\<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> \<forall>vs Ts. nodups vns \<longrightarrow> length Ts = length vns \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
apply (unfold lconf_def)
apply (induct_tac "vns")
apply  clarsimp
apply clarsimp
apply (frule list_all2_lengthD)
apply clarsimp
done


lemma lconf_deallocL: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L(vn\<mapsto>T); L vn = None\<rbrakk> \<Longrightarrow> G,s\<turnstile>l[\<Colon>\<preceq>]L"
apply (simp only: lconf_def)
apply safe
apply (drule spec)
apply (drule ospec)
apply auto
done 


lemma lconf_gext [elim]: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; s\<le>|s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<Colon>\<preceq>]L"
apply (simp only: lconf_def)
apply fast
done

lemma lconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<Colon>\<preceq>]empty"
apply (unfold lconf_def)
apply force
done

lemma lconf_init_vals [intro!]: 
        "\<And>X. \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs"
apply (unfold lconf_def)
apply force
done


section "object conformance"

constdefs

  oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool"  ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70)
           "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>snd obj[\<Colon>\<preceq>]var_tys G (fst obj) r \<and> (case r of 
                              Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> True)"

lemma oconf_def2:  "G,s\<turnstile>(oi,fs)\<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 (oi,fs)) | 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)

lemma oconf_lconf: "G2,s2\<turnstile>(oi2, fs2)\<Colon>\<preceq>\<surd>r2 \<Longrightarrow> G2,s2\<turnstile>fs2[\<Colon>\<preceq>]var_tys G2 oi2 r2"
apply (rule oconf_def2 [THEN iffD1 [THEN conjunct1]])
by assumption

lemma oconf_cong [simp]: "G,set_locals l s\<turnstile>obj\<Colon>\<preceq>\<surd>r = G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
by (auto simp: oconf_def Let_def)


ML_setup {*
claset_ref()  := claset() delSWrapper "split_all_tac";
simpset_ref() := simpset() delloop "split_all_tac"
*}
lemma oconf_init_obj_lemma: "\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (fields G C);  
  \<And>C c f m T. \<lbrakk>class G C = Some c; table_of (fields G C) f = Some (m, T) \<rbrakk> 
            \<Longrightarrow> is_type G T;  
 (case r of Heap a \<Rightarrow> is_type G (obj_ty (oi,fs)) | Stat C \<Rightarrow> is_class G C)\<rbrakk> \<Longrightarrow> 
  G,s\<turnstile>(oi, init_vals (var_tys G oi r))\<Colon>\<preceq>\<surd>r"
apply (auto simp add: oconf_def2)
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
ML_setup {*
claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
*}


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>
                                          G,s\<turnstile>l    [\<Colon>\<preceq>]L   \<and>
          (\<forall>a. fst xs=Some(XcptLoc a) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable))"

section "conforms"

lemma conforms_globsD: 
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some (oi,fs)\<rbrakk> \<Longrightarrow> G,s\<turnstile>(oi,fs)\<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"
by (auto simp: conforms_def Let_def)

lemma conforms_XcptLocD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (XcptLoc a)\<rbrakk> \<Longrightarrow>  
          G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable)"
by (auto simp: conforms_def Let_def)

lemma conforms_RefTD: "\<lbrakk>G,s2\<turnstile>a'\<Colon>\<preceq>RefT t; a' \<noteq> Null; (x2,s2) \<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow>  
  \<exists>a oi vs. a' = Addr a \<and> globs s2 (Inl a) = Some (oi, vs) \<and>  
  G\<turnstile>obj_ty (oi, vs)\<preceq>RefT t \<and> is_type G (obj_ty (oi, vs))"
apply (drule_tac conf_RefTD)
apply clarsimp
apply (rule conforms_globsD [THEN oconf_is_type])
apply auto
done

lemma conforms_StdXcpt [iff]: 
  "((Some (StdXcpt xn), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
by (auto simp: conforms_def)

lemma conforms_raise_if [iff]: 
  "((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
by (auto simp: xcpt_if_def)


lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)"
by (auto simp: conforms_def Let_def)

lemma conformsI: "\<lbrakk>\<forall>r. \<forall>(oi,fs)\<in>globs s r: G,s\<turnstile>(oi,fs)\<Colon>\<preceq>\<surd>r;  
      G,s\<turnstile>locals s[\<Colon>\<preceq>]L;  
      \<forall>a. x = Some (XcptLoc a) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable)\<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 (XcptLoc a) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable)\<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_def2)

lemmas conforms_allocL_aux = conforms_localD [THEN lconf_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_def2)

lemmas conforms_deallocL_aux = conforms_localD [THEN lconf_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 
         elim: conforms_XcptLocD conforms_deallocL_aux)

lemma conforms_gext: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>|s';  
  \<forall>r. \<forall>(oi,fs)\<in>globs s' r: G,s'\<turnstile>(oi,fs)\<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)


lemma conforms_xgext: 
  "\<And>s s'. \<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s\<rbrakk> \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)"
apply (erule_tac conforms_xconf)
apply (fast dest: conforms_XcptLocD)
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> \<Longrightarrow>  
  (x, gupd(r\<mapsto>obj)s)\<Colon>\<preceq>(G, L)"
apply (rule conforms_gext)
apply    auto
apply (force dest: conforms_globsD simp add: oconf_def2)+
done

lemma conforms_upd_gobj: "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); globs s r = Some (oi, vs);  
  var_tys G oi r n = Some T; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x,upd_gobj r n v s)\<Colon>\<preceq>(G,L)"
apply (rule conforms_gext)
apply auto
apply (force dest: conforms_globsD intro!: lconf_upd 
       simp add: oconf_def2 cong del: sum.weak_case_cong)+
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_def2)
done

lemma conforms_return: "\<And>s'. \<lbrakk>(x,s)\<Colon>\<preceq>(G, L); (x',s')\<Colon>\<preceq>(G, L'); s\<le>|s'\<rbrakk> \<Longrightarrow>  
  (x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)"
apply (rule conforms_xconf)
prefer 2 apply (force dest: conforms_XcptLocD)
apply (erule conforms_gext)
apply (force dest: conforms_globsD)+
done

end

extension of global store

lemma gext_objD:

  [| s\<le>|s'; globs s r = Some (oi, fs) |]
  ==> EX fs'. globs s' r = Some (oi, fs')

lemma rev_gext_objD:

  [| globs s r = Some (oi, fs); s\<le>|s' |]
  ==> EX fs'. globs s' r = Some (oi, fs')

lemma init_class_obj_inited:

  (init_class_obj G C) s1\<le>|s2 ==> inited C (globs s2)

lemma gext_refl:

  s\<le>|s

lemma gext_gupd:

  globs s r = None ==> s\<le>|gupd(r\<mapsto>x) s

lemma gext_new:

  globs s r = None ==> s\<le>|init_obj G oi r s

lemma gext_trans:

  [| s\<le>|s'; s'\<le>|s'' |] ==> s\<le>|s''

lemma gext_upd_gobj:

  s\<le>|upd_gobj r n v s

lemma gext_cong1:

  set_locals l s1\<le>|s2 = s1\<le>|s2

lemma gext_cong2:

  s1\<le>|set_locals l s2 = s1\<le>|s2

lemma gext_lupd1:

  lupd(vn\<mapsto>v) s1\<le>|s2 = s1\<le>|s2

lemma gext_lupd2:

  s1\<le>|lupd(vn\<mapsto>v) s2 = s1\<le>|s2

lemma inited_gext:

  [| inited C (globs s); s\<le>|s' |] ==> inited C (globs s')

value conformance

lemma conf_cong:

  G,set_locals l s\<turnstile>v\<Colon>\<preceq>T =
  G,s\<turnstile>v\<Colon>\<preceq>T

lemma conf_lupd:

  G,lupd(vn\<mapsto>va) s\<turnstile>v\<Colon>\<preceq>T =
  G,s\<turnstile>v\<Colon>\<preceq>T

lemma conf_PrimT:

  ALL dt. typeof dt v = Some (PrimT t)
  ==> G,s\<turnstile>v\<Colon>\<preceq>PrimT t
    [!]

lemma conf_litval:

  typeof (%a. None) v = Some T ==> G,s\<turnstile>v\<Colon>\<preceq>T  [!]

lemma conf_Null:

  G,s\<turnstile>Null\<Colon>\<preceq>T = G|-NT<=:T

lemma conf_Addr:

  G,s\<turnstile>Addr a\<Colon>\<preceq>T =
  (EX obj. heap s a = Some obj & G|-obj_ty obj<=:T)

lemma conf_AddrI:

  [| heap s a = Some obj; G|-obj_ty obj<=:T |]
  ==> G,s\<turnstile>Addr a\<Colon>\<preceq>T

lemma defval_conf:

  is_type G T ==> G,s\<turnstile>default_val T\<Colon>\<preceq>T  [!]

lemma conf_widen:

  [| G|-T<=:T'; G,s\<turnstile>x\<Colon>\<preceq>T; ws_prog G |]
  ==> G,s\<turnstile>x\<Colon>\<preceq>T'
    [!]

lemma conf_gext:

  [| G,s\<turnstile>v\<Colon>\<preceq>T; s\<le>|s' |]
  ==> G,s'\<turnstile>v\<Colon>\<preceq>T

lemma conf_list_widen:

  [| ws_prog G; list_all2 (conf G s) vs Ts; G\<turnstile>Ts[\<preceq>]Ts' |]
  ==> list_all2 (conf G s) vs Ts'
    [!]

lemma conf_RefTD:

  G,s\<turnstile>a'\<Colon>\<preceq>RefT T
  ==> a' = Null |
      (EX a oi vs T'.
          a' = Addr a &
          heap s a = Some (oi, vs) & obj_ty (oi, vs) = T' & G|-T'<=:RefT T)
    [!]

value list conformance

lemma lconfD:

  [| G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T |]
  ==> G,s\<turnstile>the (vs n)\<Colon>\<preceq>T

lemma lconf_cong:

  G,set_locals x s\<turnstile>l[\<Colon>\<preceq>]L =
  G,s\<turnstile>l[\<Colon>\<preceq>]L

lemma lconf_lupd:

  G,lupd(vn\<mapsto>v) s\<turnstile>l[\<Colon>\<preceq>]L =
  G,s\<turnstile>l[\<Colon>\<preceq>]L

lemma lconf_new:

  [| L vn = None; G,s\<turnstile>l[\<Colon>\<preceq>]L |]
  ==> G,s\<turnstile>l(vn|->v)[\<Colon>\<preceq>]L

lemma lconf_upd:

  [| G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T;
     L vn = Some T |]
  ==> G,s\<turnstile>l(vn|->v)[\<Colon>\<preceq>]L

lemma lconf_ext:

  [| G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T |]
  ==> G,s\<turnstile>l(vn|->v)[\<Colon>\<preceq>]L(vn|->T)

lemma lconf_map_sum:

  G,s\<turnstile>l1 (+) l2[\<Colon>\<preceq>]L1 (+) L2 =
  (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 &
   G,s\<turnstile>l2[\<Colon>\<preceq>]L2)

lemma lconf_ext_list:

  [| G,s\<turnstile>l[\<Colon>\<preceq>]L; nodups vns; length Ts = length vns;
     list_all2 (conf G s) vs Ts |]
  ==> G,s\<turnstile>l(vns[|->]vs)[\<Colon>\<preceq>]L(vns[|->]Ts)

lemma lconf_deallocL:

  [| G,s\<turnstile>l[\<Colon>\<preceq>]L(vn|->T); L vn = None |]
  ==> G,s\<turnstile>l[\<Colon>\<preceq>]L

lemma lconf_gext:

  [| G,s\<turnstile>l[\<Colon>\<preceq>]L; s\<le>|s' |]
  ==> G,s'\<turnstile>l[\<Colon>\<preceq>]L

lemma lconf_empty:

  G,s\<turnstile>vs[\<Colon>\<preceq>]empty

lemma lconf_init_vals:

  ALL n. Ball (o2s (fs n)) (is_type G)
  ==> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs
    [!]

object conformance

lemma oconf_def2:

  G,s\<turnstile>(oi, fs)\<Colon>\<preceq>\<surd>r =
  (G,s\<turnstile>fs[\<Colon>\<preceq>]var_tys G oi r &
   (case r of Inl a => is_type G (obj_ty (oi, fs)) | Inr C => True))

lemma oconf_is_type:

  G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Inl a ==> is_type G (obj_ty obj)

lemma oconf_lconf:

  G2,s2\<turnstile>(oi2, fs2)\<Colon>\<preceq>\<surd>r2
  ==> G2,s2\<turnstile>fs2[\<Colon>\<preceq>]var_tys G2 oi2 r2

lemma oconf_cong:

  G,set_locals l s\<turnstile>obj\<Colon>\<preceq>\<surd>r =
  G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r

lemma oconf_init_obj_lemma:

  [| !!C c. class G C = Some c ==> unique (fields G C);
     !!C c f m T.
        [| class G C = Some c; table_of (fields G C) f = Some (m, T) |]
        ==> is_type G T;
     case r of Inl a => is_type G (obj_ty (oi, fs)) | Inr C => is_class G C |]
  ==> G,s\<turnstile>(oi, init_vals (var_tys G oi r))\<Colon>\<preceq>\<surd>r
    [!]

state conformance

conforms

lemma conforms_globsD:

  [| (x, s)\<Colon>\<preceq>(G, L); globs s r = Some (oi, fs) |]
  ==> G,s\<turnstile>(oi, fs)\<Colon>\<preceq>\<surd>r

lemma conforms_localD:

  (x, s)\<Colon>\<preceq>(G, L) ==> G,s\<turnstile>locals s[\<Colon>\<preceq>]L

lemma conforms_XcptLocD:

  [| (x, s)\<Colon>\<preceq>(G, L); x = Some (XcptLoc a) |]
  ==> G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable)

lemma conforms_RefTD:

  [| G,s2\<turnstile>a'\<Colon>\<preceq>RefT t; a' ~= Null;
     (x2, s2)\<Colon>\<preceq>(G, L) |]
  ==> EX a oi vs.
         a' = Addr a &
         globs s2 (Inl a) = Some (oi, vs) &
         G|-obj_ty (oi, vs)<=:RefT t & is_type G (obj_ty (oi, vs))
    [!]

lemma conforms_StdXcpt:

  (Some (StdXcpt xn), s)\<Colon>\<preceq>(G, L) = Norm s\<Colon>\<preceq>(G, L)

lemma conforms_raise_if:

  ((raise_if c xn) x, s)\<Colon>\<preceq>(G, L) = (x, s)\<Colon>\<preceq>(G, L)

lemma conforms_NormI:

  (x, s)\<Colon>\<preceq>(G, L) ==> Norm s\<Colon>\<preceq>(G, L)

lemma conformsI:

  [| ALL r. ! (oi, fs):globs s r:
               G,s\<turnstile>(oi, fs)\<Colon>\<preceq>\<surd>r;
     G,s\<turnstile>locals s[\<Colon>\<preceq>]L;
     ALL a. x = Some (XcptLoc a) -->
            G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable) |]
  ==> (x, s)\<Colon>\<preceq>(G, L)

lemma conforms_xconf:

  [| (x, s)\<Colon>\<preceq>(G, L);
     ALL a. x' = Some (XcptLoc a) -->
            G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable) |]
  ==> (x', s)\<Colon>\<preceq>(G, L)

lemma conforms_lupd:

  [| (x, s)\<Colon>\<preceq>(G, L); L vn = Some T;
     G,s\<turnstile>v\<Colon>\<preceq>T |]
  ==> (x, lupd(vn\<mapsto>v) s)\<Colon>\<preceq>(G, L)

lemmas conforms_allocL_aux:

  [| (x_1, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>v\<Colon>\<preceq>T |]
  ==> G,s\<turnstile>locals s(vn|->v)[\<Colon>\<preceq>]L(vn|->T)
    [term]

lemma conforms_allocL:

  [| (x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>v\<Colon>\<preceq>T |]
  ==> (x, lupd(vn\<mapsto>v) s)\<Colon>\<preceq>(G, L(vn|->T))

lemmas conforms_deallocL_aux:

  [| (x_1, s)\<Colon>\<preceq>(G, L(vn|->T)); L vn = None |]
  ==> G,s\<turnstile>locals s[\<Colon>\<preceq>]L
    [term]

lemma conforms_deallocL:

  [| s\<Colon>\<preceq>(G, L(vn|->T)); L vn = None |] ==> s\<Colon>\<preceq>(G, L)

lemma conforms_gext:

  [| (x, s)\<Colon>\<preceq>(G, L); s\<le>|s';
     ALL r. ! (oi, fs):globs s' r:
               G,s'\<turnstile>(oi, fs)\<Colon>\<preceq>\<surd>r;
     locals s' = locals s |]
  ==> (x, s')\<Colon>\<preceq>(G, L)

lemma conforms_xgext:

  [| (x, s)\<Colon>\<preceq>(G, L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s |]
  ==> (x', s)\<Colon>\<preceq>(G, L)

lemma conforms_gupd:

  [| (x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r;
     s\<le>|gupd(r\<mapsto>obj) s |]
  ==> (x, gupd(r\<mapsto>obj) s)\<Colon>\<preceq>(G, L)

lemma conforms_upd_gobj:

  [| (x, s)\<Colon>\<preceq>(G, L); globs s r = Some (oi, vs);
     var_tys G oi r n = Some T; G,s\<turnstile>v\<Colon>\<preceq>T |]
  ==> (x, upd_gobj r n v s)\<Colon>\<preceq>(G, L)

lemma conforms_set_locals:

  [| (x, s)\<Colon>\<preceq>(G, L'); G,s\<turnstile>l[\<Colon>\<preceq>]L |]
  ==> (x, set_locals l s)\<Colon>\<preceq>(G, L)

lemma conforms_return:

  [| (x, s)\<Colon>\<preceq>(G, L); (x', s')\<Colon>\<preceq>(G, L'); s\<le>|s' |]
  ==> (x', set_locals (locals s) s')\<Colon>\<preceq>(G, L)