# Theory Conform

Up to index of Isabelle/HOL/Bali

theory Conform
imports State
begin

    (*  Title:      HOL/Bali/Conform.thy
        ID:         $Id: Conform.thy,v 1.10 2005/06/17 14:13:06 haftmann Exp $
        Author:     David von Oheimb
    *)

    header {* Conformance notions for the type soundness proof for Java *}

    theory Conform imports State begin

    text {*
    design issues:
    \begin{itemize}
    \item lconf allows for (arbitrary) inaccessible values
    \item ''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.
    \end{itemize}
    *}

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

    section "extension of global store"

    constdefs

      gext    :: "st => st => bool"                ("_≤|_"       [71,71]   70)
       "s≤|s' ≡ ∀r. ∀obj∈globs s r: ∃obj'∈globs s' r: tag obj'= tag obj"

    text {* For the the proof of type soundness we will need the
    property that during execution, objects are not lost and moreover retain the
    values of their tags. So the object store grows conservatively. Note that if
    we considered garbage collection, we would have to restrict this property to
    accessible objects.
    *}

    lemma gext_objD:
    "[|s≤|s'; globs s r = Some obj|]
    ==> ∃obj'. globs s' r = Some obj' ∧ tag obj' = tag obj"
    apply (simp only: gext_def)
    by force

    lemma rev_gext_objD:
    "[|globs s r = Some obj; s≤|s'|]
     ==> ∃obj'. globs s' r = Some obj' ∧ tag obj' = tag obj"
    by (auto elim: gext_objD)

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

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

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

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

    lemma gext_trans [elim]: "!!X. [|s≤|s'; s'≤|s''|] ==> s≤|s''"
    by (force simp: gext_def)

    lemma gext_upd_gobj [intro!]: "s≤|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≤|s2 = s1≤|s2"
    by (auto simp: gext_def)

    lemma gext_cong2 [simp]: "s1≤|set_locals l s2 = s1≤|s2"
    by (auto simp: gext_def)

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

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

    lemma inited_gext: "[|inited C (globs s); s≤|s'|] ==> inited C (globs s')"
    apply (unfold inited_def)
    apply (auto dest: gext_objD)
    done

    section "value conformance"

    constdefs

      conf  :: "prog => st => val => ty => bool"    ("_,_\<turnstile>_::\<preceq>_"   [71,71,71,71] 70)
               "G,s\<turnstile>v::\<preceq>T ≡ ∃T'∈typeof (λ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::\<preceq>T = G,s\<turnstile>v::\<preceq>T"
    by (auto simp: conf_def)

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

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

    lemma conf_Boolean: "G,s\<turnstile>v::\<preceq>PrimT Boolean ==> ∃ 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 (λa. None) v = Some T --> G,s\<turnstile>v::\<preceq>T"
    apply (unfold conf_def)
    apply (rule val.induct)
    apply auto
    done

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

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

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

    lemma defval_conf [rule_format (no_asm), elim]:
      "is_type G T --> G,s\<turnstile>default_val T::\<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' ==> G,s\<turnstile>x::\<preceq>T --> ws_prog G --> G,s\<turnstile>x::\<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::\<preceq>T --> s≤|s' --> G,s'\<turnstile>v::\<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 ==>
      ∀Ts Ts'. list_all2 (conf G s) vs Ts
               -->   G\<turnstile>Ts[\<preceq>] Ts' --> 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'::\<preceq>RefT T
      --> a' = Null ∨ (∃a obj T'. a' = Addr a ∧ heap s a = Some obj ∧
                        obj_ty obj = T' ∧ 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 => st => ('a, val) table => ('a, ty) table => bool"
                                                    ("_,_\<turnstile>_[::\<preceq>]_" [71,71,71,71] 70)
               "G,s\<turnstile>vs[::\<preceq>]Ts ≡ ∀n. ∀T∈Ts n: ∃v∈vs n: G,s\<turnstile>v::\<preceq>T"

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

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

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

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

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

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

    lemma lconf_map_sum [simp]:
     "G,s\<turnstile>l1 (+) l2[::\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[::\<preceq>]L1 ∧ G,s\<turnstile>l2[::\<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)]: "
     !!X. [|G,s\<turnstile>l[::\<preceq>]L|] ==>
          ∀vs Ts. distinct vns --> length Ts = length vns
          --> list_all2 (conf G s) vs Ts --> G,s\<turnstile>l(vns[\<mapsto>]vs)[::\<preceq>]L(vns[\<mapsto>]Ts)"
    apply (unfold lconf_def)
    apply (induct_tac "vns")
    apply  clarsimp
    apply clarify
    apply (frule list_all2_lengthD)
    apply (clarsimp)
    done

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

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

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

    lemma lconf_init_vals [intro!]:
            " ∀n. ∀T∈fs n:is_type G T ==> G,s\<turnstile>init_vals fs[::\<preceq>]fs"
    apply (unfold lconf_def)
    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 => st => ('a, val) table => ('a, ty) table => bool"
                                              ("_,_\<turnstile>_[∼::\<preceq>]_" [71,71,71,71] 70)
               "G,s\<turnstile>vs[∼::\<preceq>]Ts ≡ ∀n. ∀T∈Ts n: ∀ v∈vs n: G,s\<turnstile>v::\<preceq>T"

    lemma wlconfD: "[|G,s\<turnstile>vs[∼::\<preceq>]Ts; Ts n = Some T; vs n = Some v|] ==> G,s\<turnstile>v::\<preceq>T"
    by (auto simp: wlconf_def)

    lemma wlconf_cong [simp]: "!!s. G,set_locals x s\<turnstile>l[∼::\<preceq>]L = G,s\<turnstile>l[∼::\<preceq>]L"
    by (auto simp: wlconf_def)

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

    lemma wlconf_upd: "[|G,s\<turnstile>l[∼::\<preceq>]L; G,s\<turnstile>v::\<preceq>T; L vn = Some T|] ==>
      G,s\<turnstile>l(vn\<mapsto>v)[∼::\<preceq>]L"
    by (auto simp: wlconf_def)

    lemma wlconf_ext: "[|G,s\<turnstile>l[∼::\<preceq>]L; G,s\<turnstile>v::\<preceq>T|] ==> G,s\<turnstile>l(vn\<mapsto>v)[∼::\<preceq>]L(vn\<mapsto>T)"
    by (auto simp: wlconf_def)

    lemma wlconf_map_sum [simp]:
     "G,s\<turnstile>l1 (+) l2[∼::\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[∼::\<preceq>]L1 ∧ G,s\<turnstile>l2[∼::\<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)]: "
     !!X. [|G,s\<turnstile>l[∼::\<preceq>]L|] ==>
          ∀vs Ts. distinct vns --> length Ts = length vns
          --> list_all2 (conf G s) vs Ts --> G,s\<turnstile>l(vns[\<mapsto>]vs)[∼::\<preceq>]L(vns[\<mapsto>]Ts)"
    apply (unfold wlconf_def)
    apply (induct_tac "vns")
    apply  clarsimp
    apply clarify
    apply (frule list_all2_lengthD)
    apply clarsimp
    done

    lemma wlconf_deallocL: "[|G,s\<turnstile>l[∼::\<preceq>]L(vn\<mapsto>T); L vn = None|] ==> G,s\<turnstile>l[∼::\<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]: "[|G,s\<turnstile>l[∼::\<preceq>]L; s≤|s'|] ==> G,s'\<turnstile>l[∼::\<preceq>]L"
    apply (simp only: wlconf_def)
    apply fast
    done

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

    lemma wlconf_empty_vals: "G,s\<turnstile>empty[∼::\<preceq>]ts"
      by (simp add: wlconf_def)

    lemma wlconf_init_vals [intro!]:
            " ∀n. ∀T∈fs n:is_type G T ==> G,s\<turnstile>init_vals fs[∼::\<preceq>]fs"
    apply (unfold wlconf_def)
    apply force
    done

    lemma lconf_wlconf:
     "G,s\<turnstile>l[::\<preceq>]L ==> G,s\<turnstile>l[∼::\<preceq>]L"
    by (force simp add: lconf_def wlconf_def)

    section "object conformance"

    constdefs

      oconf :: "prog => st => obj => oref => bool"  ("_,_\<turnstile>_::\<preceq>\<surd>_"  [71,71,71,71] 70)
               "G,s\<turnstile>obj::\<preceq>\<surd>r ≡ G,s\<turnstile>values obj[::\<preceq>]var_tys G (tag obj) r ∧
                               (case r of
                                  Heap a => is_type G (obj_ty obj)
                                | Stat C => True)"

    lemma oconf_is_type: "G,s\<turnstile>obj::\<preceq>\<surd>Heap a ==> is_type G (obj_ty obj)"
    by (auto simp: oconf_def Let_def)

    lemma oconf_lconf: "G,s\<turnstile>obj::\<preceq>\<surd>r ==> G,s\<turnstile>values obj[::\<preceq>]var_tys G (tag obj) r"
    by (simp add: oconf_def)

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

    lemma oconf_init_obj_lemma:
    "[|!!C c. class G C = Some c ==> unique (DeclConcepts.fields G C);
      !!C c f fld. [|class G C = Some c;
                    table_of (DeclConcepts.fields G C) f = Some fld |]
                ==> is_type G (type fld);
      (case r of
         Heap a => is_type G (obj_ty obj)
      | Stat C => is_class G C)
    |] ==>  G,s\<turnstile>obj (|values:=init_vals (var_tys G (tag obj) r)|)),::\<preceq>\<surd>r"
    apply (auto simp add: oconf_def)
    apply (drule_tac var_tys_Some_eq [THEN iffD1])
    defer
    apply (subst obj_ty_cong)
    apply(auto dest!: fields_table_SomeD obj_ty_CInst1 obj_ty_Arr1
               split add: sum.split_asm obj_tag.split_asm)
    done

    section "state conformance"

    constdefs

      conforms :: "state => env_ => bool"          (     "_::\<preceq>_"   [71,71]      70)
       "xs::\<preceq>E ≡ let (G, L) = E; s = snd xs; l = locals s in
        (∀r. ∀obj∈globs s r:           G,s\<turnstile>obj   ::\<preceq>\<surd>r) ∧
                                         G,s\<turnstile>l    [∼::\<preceq>]L   ∧
        (∀a. fst xs=Some(Xcpt (Loc a)) --> G,s\<turnstile>Addr a::\<preceq> Class (SXcpt Throwable)) ∧
             (fst xs=Some(Jump Ret) --> l Result ≠ None)"

    section "conforms"

    lemma conforms_globsD:
    "[|(x, s)::\<preceq>(G, L); globs s r = Some obj|] ==> G,s\<turnstile>obj::\<preceq>\<surd>r"
    by (auto simp: conforms_def Let_def)

    lemma conforms_localD: "(x, s)::\<preceq>(G, L) ==> G,s\<turnstile>locals s[∼::\<preceq>]L"
    by (auto simp: conforms_def Let_def)

    lemma conforms_XcptLocD: "[|(x, s)::\<preceq>(G, L); x = Some (Xcpt (Loc a))|] ==>
              G,s\<turnstile>Addr a::\<preceq> Class (SXcpt Throwable)"
    by (auto simp: conforms_def Let_def)

    lemma conforms_RetD: "[|(x, s)::\<preceq>(G, L); x = Some (Jump Ret)|] ==>
              (locals s) Result ≠ None"
    by (auto simp: conforms_def Let_def)

    lemma conforms_RefTD:
     "[|G,s\<turnstile>a'::\<preceq>RefT t; a' ≠ Null; (x,s) ::\<preceq>(G, L)|] ==>
       ∃a obj. a' = Addr a ∧ globs s (Inl a) = Some obj ∧
       G\<turnstile>obj_ty obj\<preceq>RefT t ∧ is_type G (obj_ty obj)"
    apply (drule_tac conf_RefTD)
    apply clarsimp
    apply (rule conforms_globsD [THEN oconf_is_type])
    apply auto
    done

    lemma conforms_Jump [iff]:
      "j=Ret --> locals s Result ≠ None
       ==> ((Some (Jump j), s)::\<preceq>(G, L)) = (Norm s::\<preceq>(G, L))"
    by (auto simp: conforms_def Let_def)

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

    lemma conforms_Err [iff]:
       "((Some (Error e), s)::\<preceq>(G, L)) = (Norm s::\<preceq>(G, L))"
      by (auto simp: conforms_def)

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

    lemma conforms_error_if [iff]:
      "((error_if c err x, s)::\<preceq>(G, L)) = ((x, s)::\<preceq>(G, L))"
    by (auto simp: abrupt_if_def split: split_if)

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

    lemma conforms_absorb [rule_format]:
      "(a, b)::\<preceq>(G, L) --> (absorb j a, b)::\<preceq>(G, L)"
    apply (rule impI)
    apply ( case_tac a)
    apply (case_tac "absorb j a")
    apply auto
    apply (case_tac "absorb j (Some a)",auto)
    apply (erule conforms_NormI)
    done

    lemma conformsI: "[|∀r. ∀obj∈globs s r: G,s\<turnstile>obj::\<preceq>\<surd>r;
         G,s\<turnstile>locals s[∼::\<preceq>]L;
         ∀a. x = Some (Xcpt (Loc a)) --> G,s\<turnstile>Addr a::\<preceq> Class (SXcpt Throwable);
         x = Some (Jump Ret)--> locals s Result ≠ None|] ==>
      (x, s)::\<preceq>(G, L)"
    by (auto simp: conforms_def Let_def)

    lemma conforms_xconf: "[|(x, s)::\<preceq>(G,L);
     ∀a. x' = Some (Xcpt (Loc a)) --> G,s\<turnstile>Addr a::\<preceq> Class (SXcpt Throwable);
         x' = Some (Jump Ret) --> locals s Result ≠ None|] ==>
     (x',s)::\<preceq>(G,L)"
    by (fast intro: conformsI elim: conforms_globsD conforms_localD)

    lemma conforms_lupd:
     "[|(x, s)::\<preceq>(G, L); L vn = Some T; G,s\<turnstile>v::\<preceq>T|] ==> (x, lupd(vn\<mapsto>v)s)::\<preceq>(G, L)"
    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 wlconf_ext]

    lemma conforms_allocL:
      "[|(x, s)::\<preceq>(G, L); G,s\<turnstile>v::\<preceq>T|] ==> (x, lupd(vn\<mapsto>v)s)::\<preceq>(G, L(vn\<mapsto>T))"
    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 wlconf_deallocL]

    lemma conforms_deallocL: "!!s.[|s::\<preceq>(G, L(vn\<mapsto>T)); L vn = None|] ==> s::\<preceq>(G,L)"
    by (fast intro: conformsI dest: conforms_globsD conforms_RetD
             elim: conforms_XcptLocD conforms_deallocL_aux)

    lemma conforms_gext: "[|(x, s)::\<preceq>(G,L); s≤|s';
      ∀r. ∀obj∈globs s' r: G,s'\<turnstile>obj::\<preceq>\<surd>r;
       locals s'=locals s|] ==> (x,s')::\<preceq>(G,L)"
    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:
      "[|(x ,s)::\<preceq>(G,L); (x', s')::\<preceq>(G, L); s'≤|s;dom (locals s') ⊆ dom (locals s)|]
       ==> (x',s)::\<preceq>(G,L)"
    apply (erule_tac conforms_xconf)
    apply  (fast dest: conforms_XcptLocD)
    apply (intro strip)
    apply (drule (1) conforms_RetD)
    apply (auto dest: domI)
    done

    lemma conforms_gupd: "!!obj. [|(x, s)::\<preceq>(G, L); G,s\<turnstile>obj::\<preceq>\<surd>r; s≤|gupd(r\<mapsto>obj)s|]
    ==>  (x, gupd(r\<mapsto>obj)s)::\<preceq>(G, L)"
    apply (rule conforms_gext)
    apply    auto
    apply (force dest: conforms_globsD simp add: oconf_def)+
    done

    lemma conforms_upd_gobj: "[|(x,s)::\<preceq>(G, L); globs s r = Some obj;
      var_tys G (tag obj) r n = Some T; G,s\<turnstile>v::\<preceq>T|] ==> (x,upd_gobj r n v s)::\<preceq>(G,L)"
    apply (rule conforms_gext)
    apply auto
    apply (drule (1) conforms_globsD)
    apply (simp add: oconf_def)
    apply safe
    apply (rule lconf_upd)
    apply auto
    apply (simp only: obj_ty_cong)
    apply (force dest: conforms_globsD intro!: lconf_upd
           simp add: oconf_def cong del: sum.weak_case_cong)
    done

    lemma conforms_set_locals:
      "[|(x,s)::\<preceq>(G, L'); G,s\<turnstile>l[∼::\<preceq>]L; x=Some (Jump Ret) --> l Result ≠ None|]
       ==> (x,set_locals l s)::\<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:
      "[|(a,b)::\<preceq>(G, L); L x = Some T;locals b x ≠None|]
       ==> G,b\<turnstile>the (locals b x)::\<preceq>T"
    apply (force simp: conforms_def Let_def wlconf_def)
    done

    lemma conforms_return:
    "!!s'. [|(x,s)::\<preceq>(G, L); (x',s')::\<preceq>(G, L'); s≤|s';x'≠Some (Jump Ret)|] ==>
      (x',set_locals (locals s) s')::\<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≤|s'; globs s r = Some obj |]
      ==> ∃obj'. globs s' r = Some obj' ∧ obj.tag obj' = obj.tag obj

lemma rev_gext_objD:

      [| globs s r = Some obj; s≤|s' |]
      ==> ∃obj'. globs s' r = Some obj' ∧ obj.tag obj' = obj.tag obj

lemma init_class_obj_inited:

      (init_class_obj G C) s1.0≤|s2.0 ==> inited C (globs s2.0)

lemma gext_refl:

      s≤|s

lemma gext_gupd:

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

lemma gext_new:

      globs s r = None ==> s≤|init_obj G oi r s

lemma gext_trans:

      [| s≤|s'; s'≤|s'' |] ==> s≤|s''

lemma gext_upd_gobj:

      s≤|upd_gobj r n v s

lemma gext_cong1:

      set_locals l s1.0≤|s2.0 = s1.0≤|s2.0

lemma gext_cong2:

      s1.0≤|set_locals l s2.0 = s1.0≤|s2.0

lemma gext_lupd1:

      lupd(vn\<mapsto>v) s1.0≤|s2.0 = s1.0≤|s2.0

lemma gext_lupd2:

      s1.0≤|lupd(vn\<mapsto>v) s2.0 = s1.0≤|s2.0

lemma inited_gext:

      [| inited C (globs s); s≤|s' |] ==> inited C (globs s')

## value conformance

lemma conf_cong:

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

lemma conf_lupd:

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

lemma conf_PrimT:

      ∀dt. typeof dt v = Some (PrimT t) ==> G,s\<turnstile>v::\<preceq>PrimT t

lemma conf_Boolean:

      G,s\<turnstile>v::\<preceq>PrimT Boolean ==> ∃b. v = Bool b

lemma conf_litval:

      typeof empty v = Some T ==> G,s\<turnstile>v::\<preceq>T

lemma conf_Null:

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

lemma conf_Addr:

      G,s\<turnstile>Addr a::\<preceq>T =
      (∃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::\<preceq>T

lemma defval_conf:

      is_type G T ==> G,s\<turnstile>default_val T::\<preceq>T

lemma conf_widen:

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

lemma conf_gext:

      [| G,s\<turnstile>v::\<preceq>T; s≤|s' |] ==> G,s'\<turnstile>v::\<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'::\<preceq>RefT T
      ==> a' = Null ∨
          (∃a obj T'.
              a' = Addr a ∧ heap s a = Some obj ∧ obj_ty obj = T' ∧ G|-T'<=:RefT T)

## value list conformance

lemma lconfD:

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

lemma lconf_cong:

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

lemma lconf_lupd:

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

lemma lconf_new:

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

lemma lconf_upd:

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

lemma lconf_ext:

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

lemma lconf_map_sum:

      G,s\<turnstile>l1.0 (+) l2.0[::\<preceq>]L1.0 (+) L2.0 =
      (G,s\<turnstile>l1.0[::\<preceq>]L1.0 ∧ G,s\<turnstile>l2.0[::\<preceq>]L2.0)

lemma lconf_ext_list:

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

lemma lconf_deallocL:

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

lemma lconf_gext:

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

lemma lconf_empty:

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

lemma lconf_init_vals:

      ∀n. ! T:fs n: is_type G T ==> G,s\<turnstile>init_vals fs[::\<preceq>]fs

## weak value list conformance

lemma wlconfD:

      [| G,s\<turnstile>vs[∼::\<preceq>]Ts; Ts n = Some T; vs n = Some v |]
      ==> G,s\<turnstile>v::\<preceq>T

lemma wlconf_cong:

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

lemma wlconf_lupd:

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

lemma wlconf_upd:

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

lemma wlconf_ext:

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

lemma wlconf_map_sum:

      G,s\<turnstile>l1.0 (+) l2.0[∼::\<preceq>]L1.0 (+) L2.0 =
      (G,s\<turnstile>l1.0[∼::\<preceq>]L1.0 ∧ G,s\<turnstile>l2.0[∼::\<preceq>]L2.0)

lemma wlconf_ext_list:

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

lemma wlconf_deallocL:

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

lemma wlconf_gext:

      [| G,s\<turnstile>l[∼::\<preceq>]L; s≤|s' |]
      ==> G,s'\<turnstile>l[∼::\<preceq>]L

lemma wlconf_empty:

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

lemma wlconf_empty_vals:

      G,s\<turnstile>empty[∼::\<preceq>]ts

lemma wlconf_init_vals:

      ∀n. ! T:fs n: is_type G T ==> G,s\<turnstile>init_vals fs[∼::\<preceq>]fs

lemma lconf_wlconf:

      G,s\<turnstile>l[::\<preceq>]L ==> G,s\<turnstile>l[∼::\<preceq>]L

## object conformance

lemma oconf_is_type:

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

lemma oconf_lconf:

      G,s\<turnstile>obj::\<preceq>\<surd>r
      ==> G,s\<turnstile>values obj[::\<preceq>]var_tys G (obj.tag obj) r

lemma oconf_cong:

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

lemma oconf_init_obj_lemma:

      [| !!C c. class G C = Some c ==> unique (DeclConcepts.fields G C);
         !!C c f fld.
            [| class G C = Some c; table_of (DeclConcepts.fields G C) f = Some fld |]
            ==> is_type G (type fld);
         case r of Inl a => is_type G (obj_ty obj) | Inr C => is_class G C |]
      ==> G,s\<turnstile>obj
          (| values := init_vals (var_tys G (obj.tag obj) r) |)::\<preceq>\<surd>r

## state conformance

## conforms

lemma conforms_globsD:

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

lemma conforms_localD:

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

lemma conforms_XcptLocD:

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

lemma conforms_RetD:

      [| (x, s)::\<preceq>(G, L); x = Some (Jump Ret) |] ==> locals s Result ≠ None

lemma conforms_RefTD:

      [| G,s\<turnstile>a'::\<preceq>RefT t; a' ≠ Null; (x, s)::\<preceq>(G, L) |]
      ==> ∃a obj.
             a' = Addr a ∧
             globs s (Inl a) = Some obj ∧
             G|-obj_ty obj<=:RefT t ∧ is_type G (obj_ty obj)

lemma conforms_Jump:

      j = Ret --> locals s Result ≠ None
      ==> (Some (Jump j), s)::\<preceq>(G, L) = Norm s::\<preceq>(G, L)

lemma conforms_StdXcpt:

      (Some (Xcpt (Std xn)), s)::\<preceq>(G, L) = Norm s::\<preceq>(G, L)

lemma conforms_Err:

      (Some (Error e), s)::\<preceq>(G, L) = Norm s::\<preceq>(G, L)

lemma conforms_raise_if:

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

lemma conforms_error_if:

      ((error_if c err) x, s)::\<preceq>(G, L) = (x, s)::\<preceq>(G, L)

lemma conforms_NormI:

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

lemma conforms_absorb:

      (a, b)::\<preceq>(G, L) ==> (absorb j a, b)::\<preceq>(G, L)

lemma conformsI:

      [| ∀r. ! obj:globs s r: G,s\<turnstile>obj::\<preceq>\<surd>r;
         G,s\<turnstile>locals s[∼::\<preceq>]L;
         ∀a. x = Some (Xcpt (Loc a)) -->
             G,s\<turnstile>Addr a::\<preceq>Class (SXcpt Throwable);
         x = Some (Jump Ret) --> locals s Result ≠ None |]
      ==> (x, s)::\<preceq>(G, L)

lemma conforms_xconf:

      [| (x, s)::\<preceq>(G, L);
         ∀a. x' = Some (Xcpt (Loc a)) -->
             G,s\<turnstile>Addr a::\<preceq>Class (SXcpt Throwable);
         x' = Some (Jump Ret) --> locals s Result ≠ None |]
      ==> (x', s)::\<preceq>(G, L)

lemma conforms_lupd:

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

lemmas conforms_allocL_aux:

      [| (x1, s)::\<preceq>(G, L); G,s\<turnstile>v::\<preceq>T |]
      ==> G,s\<turnstile>locals s(vn |-> v)[∼::\<preceq>]L(vn |-> T)

lemmas conforms_allocL_aux:

      [| (x1, s)::\<preceq>(G, L); G,s\<turnstile>v::\<preceq>T |]
      ==> G,s\<turnstile>locals s(vn |-> v)[∼::\<preceq>]L(vn |-> T)

lemma conforms_allocL:

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

lemmas conforms_deallocL_aux:

      [| (x1, s)::\<preceq>(G, L(vn |-> T)); L vn = None |]
      ==> G,s\<turnstile>locals s[∼::\<preceq>]L

lemmas conforms_deallocL_aux:

      [| (x1, s)::\<preceq>(G, L(vn |-> T)); L vn = None |]
      ==> G,s\<turnstile>locals s[∼::\<preceq>]L

lemma conforms_deallocL:

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

lemma conforms_gext:

      [| (x, s)::\<preceq>(G, L); s≤|s';
         ∀r. ! obj:globs s' r: G,s'\<turnstile>obj::\<preceq>\<surd>r;
         locals s' = locals s |]
      ==> (x, s')::\<preceq>(G, L)

lemma conforms_xgext:

      [| (x, s)::\<preceq>(G, L); (x', s')::\<preceq>(G, L); s'≤|s;
         dom (locals s') ⊆ dom (locals s) |]
      ==> (x', s)::\<preceq>(G, L)

lemma conforms_gupd:

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

lemma conforms_upd_gobj:

      [| (x, s)::\<preceq>(G, L); globs s r = Some obj;
         var_tys G (obj.tag obj) r n = Some T; G,s\<turnstile>v::\<preceq>T |]
      ==> (x, upd_gobj r n v s)::\<preceq>(G, L)

lemma conforms_set_locals:

      [| (x, s)::\<preceq>(G, L'); G,s\<turnstile>l[∼::\<preceq>]L;
         x = Some (Jump Ret) --> l Result ≠ None |]
      ==> (x, set_locals l s)::\<preceq>(G, L)

lemma conforms_locals:

      [| (a, b)::\<preceq>(G, L); L x = Some T; locals b x ≠ None |]
      ==> G,b\<turnstile>the (locals b x)::\<preceq>T

lemma conforms_return:

      [| (x, s)::\<preceq>(G, L); (x', s')::\<preceq>(G, L'); s≤|s';
         x' ≠ Some (Jump Ret) |]
      ==> (x', set_locals (locals s) s')::\<preceq>(G, L)