# Theory Example

Up to index of Isabelle/HOL/Bali

theory Example
imports Eval WellForm
begin

    (*  Title:      HOL/Bali/Example.thy
        ID:         $Id: Example.thy,v 1.9 2005/06/17 14:13:06 haftmann Exp $
        Author:     David von Oheimb
    *)
    header {* Example Bali program *}

    theory Example imports Eval WellForm begin

    text {*
    The following example Bali program includes:
    \begin{itemize}
    \item class and interface declarations with inheritance, hiding of fields,
        overriding of methods (with refined result type), array type,
    \item method call (with dynamic binding), parameter access, return expressions,
    \item expression statements, sequential composition, literal values,
        local assignment, local access, field assignment, type cast,
    \item exception generation and propagation, try and catch statement, throw
          statement
    \item instance creation and (default) static initialization
    \end{itemize}
    \begin{verbatim}
    package java_lang

    public interface HasFoo {
      public Base foo(Base z);
    }

    public class Base implements HasFoo {
      static boolean arr[] = new boolean[2];
      public HasFoo vee;
      public Base foo(Base z) {
        return z;
      }
    }

    public class Ext extends Base {
      public int vee;
      public Ext foo(Base z) {
        ((Ext)z).vee = 1;
        return null;
      }
    }

    public class Main {
      public static void main(String args[]) throws Throwable {
        Base e = new Ext();
        try {e.foo(null); }
        catch(NullPointerException z) {
          while(Ext.arr[2]) ;
        }
      }
    }
    \end{verbatim}
    *}
    declare widen.null [intro]

    lemma wf_fdecl_def2: "!!fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
    apply (unfold wf_fdecl_def)
    apply (simp (no_asm))
    done

    declare wf_fdecl_def2 [iff]

    section "type and expression names"

    (** unfortunately cannot simply instantiate tnam **)
    datatype tnam_  = HasFoo_ | Base_ | Ext_ | Main_
    datatype vnam_  = arr_ | vee_ | z_ | e_
    datatype label_ = lab1_

    consts

      tnam_ :: "tnam_  => tnam"
      vnam_ :: "vnam_  => vname"
      label_:: "label_ => label"
    axioms  (** tnam_, vnam_ and label are intended to be isomorphic
                to tnam, vname and label **)

      inj_tnam_  [simp]: "(tnam_  x = tnam_  y) = (x = y)"
      inj_vnam_  [simp]: "(vnam_  x = vnam_  y) = (x = y)"
      inj_label_ [simp]: "(label_ x = label_ y) = (x = y)"

      surj_tnam_:  "∃m. n = tnam_  m"
      surj_vnam_:  "∃m. n = vnam_  m"
      surj_label_:" ∃m. n = label_ m"

    syntax

      HasFoo :: qtname
      Base   :: qtname
      Ext    :: qtname
      Main   :: qtname
      arr :: ename
      vee :: ename
      z   :: ename
      e   :: ename
      lab1:: label
    translations

      "HasFoo" == "(|pid=java_lang,tid=TName (tnam_ HasFoo_)|)),"
      "Base"   == "(|pid=java_lang,tid=TName (tnam_ Base_)|)),"
      "Ext"    == "(|pid=java_lang,tid=TName (tnam_ Ext_)|)),"
      "Main"   == "(|pid=java_lang,tid=TName (tnam_ Main_)|)),"
      "arr"    ==        "(vnam_ arr_)"
      "vee"    ==        "(vnam_ vee_)"
      "z"      ==        "(vnam_ z_)"
      "e"      ==        "(vnam_ e_)"
      "lab1"   ==        "label_ lab1_"

    lemma neq_Base_Object [simp]: "Base≠Object"
    by (simp add: Object_def)

    lemma neq_Ext_Object [simp]: "Ext≠Object"
    by (simp add: Object_def)

    lemma neq_Main_Object [simp]: "Main≠Object"
    by (simp add: Object_def)

    lemma neq_Base_SXcpt [simp]: "Base≠SXcpt xn"
    by (simp add: SXcpt_def)

    lemma neq_Ext_SXcpt [simp]: "Ext≠SXcpt xn"
    by (simp add: SXcpt_def)

    lemma neq_Main_SXcpt [simp]: "Main≠SXcpt xn"
    by (simp add: SXcpt_def)

    section "classes and interfaces"

    defs

      Object_mdecls_def: "Object_mdecls ≡ []"
      SXcpt_mdecls_def:  "SXcpt_mdecls  ≡ []"

    consts

      foo    :: mname

    constdefs

      foo_sig   :: sig
     "foo_sig   ≡ (|name=foo,parTs=[Class Base]|)),"

      foo_mhead :: mhead
     "foo_mhead ≡ (|access=Public,static=False,pars=[z],resT=Class Base|)),"

    constdefs

      Base_foo :: mdecl
     "Base_foo ≡ (foo_sig, (|access=Public,static=False,pars=[z],resT=Class Base,
                            mbody=(|lcls=[],stmt=Return (!!z)|)),|)),)"

    constdefs
      Ext_foo  :: mdecl
     "Ext_foo  ≡ (foo_sig,
                  (|access=Public,static=False,pars=[z],resT=Class Ext,
                   mbody=(|lcls=[]
                         ,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee :=
                                                                 Lit (Intg 1)) ;;
                                    Return (Lit Null)|)),
                  |)),)"

    constdefs

    arr_viewed_from :: "qtname => qtname => var"
    "arr_viewed_from accC C ≡ {accC,Base,True}StatRef (ClassT C)..arr"

    BaseCl :: class
    "BaseCl ≡ (|access=Public,
               cfields=[(arr, (|access=Public,static=True ,type=PrimT Boolean.[]|)),),
                        (vee, (|access=Public,static=False,type=Iface HasFoo    |)),)],
               methods=[Base_foo],
               init=Expr(arr_viewed_from Base Base
                         :=New (PrimT Boolean)[Lit (Intg 2)]),
               super=Object,
               superIfs=[HasFoo]|)),"

    ExtCl  :: class
    "ExtCl  ≡ (|access=Public,
               cfields=[(vee, (|access=Public,static=False,type= PrimT Integer|)),)],
               methods=[Ext_foo],
               init=Skip,
               super=Base,
               superIfs=[]|)),"

    MainCl :: class
    "MainCl ≡ (|access=Public,
               cfields=[],
               methods=[],
               init=Skip,
               super=Object,
               superIfs=[]|)),"
    (* The "main" method is modeled seperately (see tprg) *)

    constdefs

      HasFooInt :: iface
     "HasFooInt ≡ (|access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]|)),"

      Ifaces ::"idecl list"
     "Ifaces ≡ [(HasFoo,HasFooInt)]"

     "Classes" ::"cdecl list"
     "Classes ≡ [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"

    lemmas table_classes_defs =
         Classes_def standard_classes_def ObjectC_def SXcptC_def

    lemma table_ifaces [simp]: "table_of Ifaces = empty(HasFoo\<mapsto>HasFooInt)"
    apply (unfold Ifaces_def)
    apply (simp (no_asm))
    done

    lemma table_classes_Object [simp]:
     "table_of Classes Object = Some (|access=Public,cfields=[]
                                     ,methods=Object_mdecls
                                     ,init=Skip,super=arbitrary,superIfs=[]|)),"
    apply (unfold table_classes_defs)
    apply (simp (no_asm) add:Object_def)
    done

    lemma table_classes_SXcpt [simp]:
      "table_of Classes (SXcpt xn)
        = Some (|access=Public,cfields=[],methods=SXcpt_mdecls,
                init=Skip,
                super=if xn = Throwable then Object else SXcpt Throwable,
                superIfs=[]|)),"
    apply (unfold table_classes_defs)
    apply (induct_tac xn)
    apply (simp add: Object_def SXcpt_def)+
    done

    lemma table_classes_HasFoo [simp]: "table_of Classes HasFoo = None"
    apply (unfold table_classes_defs)
    apply (simp (no_asm) add: Object_def SXcpt_def)
    done

    lemma table_classes_Base [simp]: "table_of Classes Base = Some BaseCl"
    apply (unfold table_classes_defs )
    apply (simp (no_asm) add: Object_def SXcpt_def)
    done

    lemma table_classes_Ext [simp]: "table_of Classes Ext = Some ExtCl"
    apply (unfold table_classes_defs )
    apply (simp (no_asm) add: Object_def SXcpt_def)
    done

    lemma table_classes_Main [simp]: "table_of Classes Main = Some MainCl"
    apply (unfold table_classes_defs )
    apply (simp (no_asm) add: Object_def SXcpt_def)
    done

    section "program"

    syntax
      tprg :: prog

    translations
      "tprg" == "(|ifaces=Ifaces,classes=Classes|)),"

    constdefs
      test    :: "(ty)list => stmt"
     "test pTs ≡ e:==NewC Ext;;
                  Try Expr({Main,ClassT Base,IntVir}!!e·foo({pTs}[Lit Null]))
                  Catch((SXcpt NullPointer) z)
               (lab1• While(Acc
                            (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip)"

    section "well-structuredness"

    lemma not_Object_subcls_any [elim!]: "(Object, C) ∈ (subcls1 tprg)^+ ==> R"
    apply (auto dest!: tranclD subcls1D)
    done

    lemma not_Throwable_subcls_SXcpt [elim!]:
      "(SXcpt Throwable, SXcpt xn) ∈ (subcls1 tprg)^+ ==> R"
    apply (auto dest!: tranclD subcls1D)
    apply (simp add: Object_def SXcpt_def)
    done

    lemma not_SXcpt_n_subcls_SXcpt_n [elim!]:
      "(SXcpt xn, SXcpt xn)  ∈ (subcls1 tprg)^+ ==> R"
    apply (auto dest!: tranclD subcls1D)
    apply (drule rtranclD)
    apply auto
    done

    lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) ∈ (subcls1 tprg)^+  ==> R"
    apply (auto dest!: tranclD subcls1D simp add: BaseCl_def)
    done

    lemma not_TName_n_subcls_TName_n [rule_format (no_asm), elim!]:
      "((|pid=java_lang,tid=TName tn|)),, (|pid=java_lang,tid=TName tn|)),)
       ∈ (subcls1 tprg)^+ --> R"
    apply (rule_tac n1 = "tn" in surj_tnam_ [THEN exE])
    apply (erule ssubst)
    apply (rule tnam_.induct)
    apply  safe
    apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def MainCl_def)
    apply (drule rtranclD)
    apply auto
    done

    lemma ws_idecl_HasFoo: "ws_idecl tprg HasFoo []"
    apply (unfold ws_idecl_def)
    apply (simp (no_asm))
    done

    lemma ws_cdecl_Object: "ws_cdecl tprg Object any"
    apply (unfold ws_cdecl_def)
    apply auto
    done

    lemma ws_cdecl_Throwable: "ws_cdecl tprg (SXcpt Throwable) Object"
    apply (unfold ws_cdecl_def)
    apply auto
    done

    lemma ws_cdecl_SXcpt: "ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)"
    apply (unfold ws_cdecl_def)
    apply auto
    done

    lemma ws_cdecl_Base: "ws_cdecl tprg Base Object"
    apply (unfold ws_cdecl_def)
    apply auto
    done

    lemma ws_cdecl_Ext: "ws_cdecl tprg Ext Base"
    apply (unfold ws_cdecl_def)
    apply auto
    done

    lemma ws_cdecl_Main: "ws_cdecl tprg Main Object"
    apply (unfold ws_cdecl_def)
    apply auto
    done

    lemmas ws_cdecls = ws_cdecl_SXcpt ws_cdecl_Object ws_cdecl_Throwable
                       ws_cdecl_Base ws_cdecl_Ext ws_cdecl_Main

    declare not_Object_subcls_any [rule del]
              not_Throwable_subcls_SXcpt [rule del]
              not_SXcpt_n_subcls_SXcpt_n [rule del]
              not_Base_subcls_Ext [rule del] not_TName_n_subcls_TName_n [rule del]

    lemma ws_idecl_all:
     "G=tprg ==> (∀(I,i)∈set Ifaces. ws_idecl G I (isuperIfs i))"
    apply (simp (no_asm) add: Ifaces_def HasFooInt_def)
    apply (auto intro!: ws_idecl_HasFoo)
    done

    lemma ws_cdecl_all: "G=tprg ==> (∀(C,c)∈set Classes. ws_cdecl G C (super c))"
    apply (simp (no_asm) add: Classes_def BaseCl_def ExtCl_def MainCl_def)
    apply (auto intro!: ws_cdecls simp add: standard_classes_def ObjectC_def
            SXcptC_def)
    done

    lemma ws_tprg: "ws_prog tprg"
    apply (unfold ws_prog_def)
    apply (auto intro!: ws_idecl_all ws_cdecl_all)
    done

    section "misc program properties (independent of well-structuredness)"

    lemma single_iface [simp]: "is_iface tprg I = (I = HasFoo)"
    apply (unfold Ifaces_def)
    apply (simp (no_asm))
    done

    lemma empty_subint1 [simp]: "subint1 tprg = {}"
    apply (unfold subint1_def Ifaces_def HasFooInt_def)
    apply auto
    done

    lemma unique_ifaces: "unique Ifaces"
    apply (unfold Ifaces_def)
    apply (simp (no_asm))
    done

    lemma unique_classes: "unique Classes"
    apply (unfold table_classes_defs )
    apply (simp )
    done

    lemma SXcpt_subcls_Throwable [simp]: "tprg\<turnstile>SXcpt xn\<preceq>C SXcpt Throwable"
    apply (rule SXcpt_subcls_Throwable_lemma)
    apply auto
    done

    lemma Ext_subclseq_Base [simp]: "tprg\<turnstile>Ext \<preceq>C Base"
    apply (rule subcls_direct1)
    apply  (simp (no_asm) add: ExtCl_def)
    apply  (simp add: Object_def)
    apply (simp (no_asm))
    done

    lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext \<prec>C Base"
    apply (rule subcls_direct2)
    apply  (simp (no_asm) add: ExtCl_def)
    apply  (simp add: Object_def)
    apply (simp (no_asm))
    done

    section "fields and method lookup"

    lemma fields_tprg_Object [simp]: "DeclConcepts.fields tprg Object = []"
    by (rule ws_tprg [THEN fields_emptyI], force+)

    lemma fields_tprg_Throwable [simp]:
      "DeclConcepts.fields tprg (SXcpt Throwable) = []"
    by (rule ws_tprg [THEN fields_emptyI], force+)

    lemma fields_tprg_SXcpt [simp]: "DeclConcepts.fields tprg (SXcpt xn) = []"
    apply (case_tac "xn = Throwable")
    apply  (simp (no_asm_simp))
    by (rule ws_tprg [THEN fields_emptyI], force+)

    lemmas fields_rec_ = fields_rec [OF _ ws_tprg]

    lemma fields_Base [simp]:
    "DeclConcepts.fields tprg Base
      = [((arr,Base), (|access=Public,static=True ,type=PrimT Boolean.[]|)),),
         ((vee,Base), (|access=Public,static=False,type=Iface HasFoo    |)),)]"
    apply (subst fields_rec_)
    apply   (auto simp add: BaseCl_def)
    done

    lemma fields_Ext [simp]:
     "DeclConcepts.fields tprg Ext
      = [((vee,Ext), (|access=Public,static=False,type= PrimT Integer|)),)]
        @ DeclConcepts.fields tprg Base"
    apply (rule trans)
    apply (rule fields_rec_)
    apply   (auto simp add: ExtCl_def Object_def)
    done

    lemmas imethds_rec_ = imethds_rec [OF _ ws_tprg]
    lemmas methd_rec_  = methd_rec  [OF _ ws_tprg]

    lemma imethds_HasFoo [simp]:
      "imethds tprg HasFoo = o2s o empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
    apply (rule trans)
    apply (rule imethds_rec_)
    apply  (auto simp add: HasFooInt_def)
    done

    lemma methd_tprg_Object [simp]: "methd tprg Object = empty"
    apply (subst methd_rec_)
    apply (auto simp add: Object_mdecls_def)
    done

    lemma methd_Base [simp]:
      "methd tprg Base = table_of [(λ(s,m). (s, Base, m)) Base_foo]"
    apply (rule trans)
    apply (rule methd_rec_)
    apply   (auto simp add: BaseCl_def)
    done

    lemma memberid_Base_foo_simp [simp]:
     "memberid (mdecl Base_foo) = mid foo_sig"
    by (simp add: Base_foo_def)

    lemma memberid_Ext_foo_simp [simp]:
     "memberid (mdecl Ext_foo) = mid foo_sig"
    by (simp add: Ext_foo_def)

    lemma Base_declares_foo:
      "tprg\<turnstile>mdecl Base_foo declared_in Base"
    by (auto simp add: declared_in_def cdeclaredmethd_def BaseCl_def Base_foo_def)

    lemma foo_sig_not_undeclared_in_Base:
      "¬ tprg\<turnstile>mid foo_sig undeclared_in Base"
    proof -
      from Base_declares_foo
      show ?thesis
        by (auto dest!: declared_not_undeclared )
    qed

    lemma Ext_declares_foo:
      "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
    by (auto simp add: declared_in_def cdeclaredmethd_def ExtCl_def Ext_foo_def)

    lemma foo_sig_not_undeclared_in_Ext:
      "¬ tprg\<turnstile>mid foo_sig undeclared_in Ext"
    proof -
      from Ext_declares_foo
      show ?thesis
        by (auto dest!: declared_not_undeclared )
    qed

    lemma Base_foo_not_inherited_in_Ext:
     "¬ tprg \<turnstile> Ext inherits (Base,mdecl Base_foo)"
    by (auto simp add: inherits_def foo_sig_not_undeclared_in_Ext)

    lemma Ext_method_inheritance:
     "filter_tab (λsig m. tprg \<turnstile> Ext inherits method sig m)
         (empty(fst ((λ(s, m). (s, Base, m)) Base_foo)\<mapsto>
          snd ((λ(s, m). (s, Base, m)) Base_foo)))
      = empty"
    proof -
      from Base_foo_not_inherited_in_Ext
      show ?thesis
        by (auto intro: filter_tab_all_False simp add: Base_foo_def)
    qed

    lemma methd_Ext [simp]: "methd tprg Ext =
      table_of [(λ(s,m). (s, Ext, m)) Ext_foo]"
    apply (rule trans)
    apply (rule methd_rec_)
    apply   (auto simp add: ExtCl_def Object_def Ext_method_inheritance)
    done

    section "accessibility"

    lemma classesDefined:
     "[|class tprg C = Some c; C≠Object|] ==> ∃ sc. class tprg (super c) = Some sc"
    apply (auto simp add: Classes_def standard_classes_def
                          BaseCl_def ExtCl_def MainCl_def
                          SXcptC_def ObjectC_def)
    done

    lemma superclassesBase [simp]: "superclasses tprg Base={Object}"
    proof -
      have ws: "ws_prog tprg" by (rule ws_tprg)
      then show ?thesis
        by (auto simp add: superclasses_rec  BaseCl_def)
    qed

    lemma superclassesExt [simp]: "superclasses tprg Ext={Base,Object}"
    proof -
      have ws: "ws_prog tprg" by (rule ws_tprg)
      then show ?thesis
        by (auto simp add: superclasses_rec  ExtCl_def BaseCl_def)
    qed

    lemma superclassesMain [simp]: "superclasses tprg Main={Object}"
    proof -
      have ws: "ws_prog tprg" by (rule ws_tprg)
      then show ?thesis
        by (auto simp add: superclasses_rec  MainCl_def)
    qed

    lemma HasFoo_accessible[simp]:"tprg\<turnstile>(Iface HasFoo) accessible_in P"
    by (simp add: accessible_in_RefT_simp is_public_def HasFooInt_def)

    lemma HasFoo_is_acc_iface[simp]: "is_acc_iface tprg P HasFoo"
    by (simp add: is_acc_iface_def)

    lemma HasFoo_is_acc_type[simp]: "is_acc_type tprg P (Iface HasFoo)"
    by (simp add: is_acc_type_def)

    lemma Base_accessible[simp]:"tprg\<turnstile>(Class Base) accessible_in P"
    by (simp add: accessible_in_RefT_simp is_public_def BaseCl_def)

    lemma Base_is_acc_class[simp]: "is_acc_class tprg P Base"
    by (simp add: is_acc_class_def)

    lemma Base_is_acc_type[simp]: "is_acc_type tprg P (Class Base)"
    by (simp add: is_acc_type_def)

    lemma Ext_accessible[simp]:"tprg\<turnstile>(Class Ext) accessible_in P"
    by (simp add: accessible_in_RefT_simp is_public_def ExtCl_def)

    lemma Ext_is_acc_class[simp]: "is_acc_class tprg P Ext"
    by (simp add: is_acc_class_def)

    lemma Ext_is_acc_type[simp]: "is_acc_type tprg P (Class Ext)"
    by (simp add: is_acc_type_def)

    lemma accmethd_tprg_Object [simp]: "accmethd tprg S Object = empty"
    apply (unfold accmethd_def)
    apply (simp)
    done

    lemma  snd_special_simp: "snd ((λ(s, m). (s, a, m)) x) = (a,snd x)"
    by (cases x) (auto)

    lemma  fst_special_simp: "fst ((λ(s, m). (s, a, m)) x) = fst x"
    by (cases x) (auto)

    lemma foo_sig_undeclared_in_Object:
      "tprg\<turnstile>mid foo_sig undeclared_in Object"
    by (auto simp add: undeclared_in_def cdeclaredmethd_def Object_mdecls_def)

    lemma unique_sig_Base_foo:
     "tprg\<turnstile> mdecl (sig, snd Base_foo) declared_in Base ==> sig=foo_sig"
    by (auto simp add: declared_in_def cdeclaredmethd_def
                       Base_foo_def BaseCl_def)

    lemma Base_foo_no_override:
     "tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides old ==> P"
    apply (drule overrides_commonD)
    apply (clarsimp)
    apply (frule subclsEval)
    apply    (rule ws_tprg)
    apply    (simp)
    apply    (rule classesDefined)
    apply    assumption+
    apply (frule unique_sig_Base_foo)
    apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
                dest: unique_sig_Base_foo)
    done

    lemma Base_foo_no_stat_override:
     "tprg,sig\<turnstile>(Base,(snd Base_foo)) overridesS old ==> P"
    apply (drule stat_overrides_commonD)
    apply (clarsimp)
    apply (frule subclsEval)
    apply    (rule ws_tprg)
    apply    (simp)
    apply    (rule classesDefined)
    apply    assumption+
    apply (frule unique_sig_Base_foo)
    apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
                dest: unique_sig_Base_foo)
    done

    lemma Base_foo_no_hide:
     "tprg,sig\<turnstile>(Base,(snd Base_foo)) hides old ==> P"
    by (auto dest: hidesD simp add: Base_foo_def member_is_static_simp)

    lemma Ext_foo_no_hide:
     "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) hides old ==> P"
    by (auto dest: hidesD simp add: Ext_foo_def member_is_static_simp)

    lemma unique_sig_Ext_foo:
     "tprg\<turnstile> mdecl (sig, snd Ext_foo) declared_in Ext ==> sig=foo_sig"
    by (auto simp add: declared_in_def cdeclaredmethd_def
                       Ext_foo_def ExtCl_def)

    lemma Ext_foo_override:
     "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides old
      ==> old = (Base,(snd Base_foo))"
    apply (drule overrides_commonD)
    apply (clarsimp)
    apply (frule subclsEval)
    apply    (rule ws_tprg)
    apply    (simp)
    apply    (rule classesDefined)
    apply    assumption+
    apply (frule unique_sig_Ext_foo)
    apply (case_tac "old")
    apply (insert Base_declares_foo foo_sig_undeclared_in_Object)
    apply (auto simp add: ExtCl_def Ext_foo_def
                          BaseCl_def Base_foo_def Object_mdecls_def
                          split_paired_all
                          member_is_static_simp
               dest: declared_not_undeclared unique_declaration)
    done

    lemma Ext_foo_stat_override:
     "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overridesS old
      ==> old = (Base,(snd Base_foo))"
    apply (drule stat_overrides_commonD)
    apply (clarsimp)
    apply (frule subclsEval)
    apply    (rule ws_tprg)
    apply    (simp)
    apply    (rule classesDefined)
    apply    assumption+
    apply (frule unique_sig_Ext_foo)
    apply (case_tac "old")
    apply (insert Base_declares_foo foo_sig_undeclared_in_Object)
    apply (auto simp add: ExtCl_def Ext_foo_def
                          BaseCl_def Base_foo_def Object_mdecls_def
                          split_paired_all
                          member_is_static_simp
               dest: declared_not_undeclared unique_declaration)
    done

    lemma Base_foo_member_of_Base:
      "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
    by (auto intro!: members.Immediate Base_declares_foo)

    lemma Base_foo_member_in_Base:
      "tprg\<turnstile>(Base,mdecl Base_foo) member_in Base"
    by (rule member_of_to_member_in [OF Base_foo_member_of_Base])

    lemma Ext_foo_member_of_Ext:
      "tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
    by (auto intro!: members.Immediate Ext_declares_foo)

    lemma Ext_foo_member_in_Ext:
      "tprg\<turnstile>(Ext,mdecl Ext_foo) member_in Ext"
    by (rule member_of_to_member_in [OF Ext_foo_member_of_Ext])

    lemma Base_foo_permits_acc:
     "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_from S"
    by ( simp add: permits_acc_def Base_foo_def)

    lemma Base_foo_accessible [simp]:
     "tprg\<turnstile>(Base,mdecl Base_foo) of Base accessible_from S"
    by (auto intro: accessible_fromR.Immediate
                    Base_foo_member_of_Base Base_foo_permits_acc)

    lemma Base_foo_dyn_accessible [simp]:
     "tprg\<turnstile>(Base,mdecl Base_foo) in Base dyn_accessible_from S"
    apply (rule dyn_accessible_fromR.Immediate)
    apply   (rule Base_foo_member_in_Base)
    apply   (rule Base_foo_permits_acc)
    done

    lemma accmethd_Base [simp]:
      "accmethd tprg S Base = methd tprg Base"
    apply (simp add: accmethd_def)
    apply (rule filter_tab_all_True)
    apply (simp add: snd_special_simp fst_special_simp)
    done

    lemma Ext_foo_permits_acc:
     "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_from S"
    by ( simp add: permits_acc_def Ext_foo_def)

    lemma Ext_foo_accessible [simp]:
     "tprg\<turnstile>(Ext,mdecl Ext_foo) of Ext accessible_from S"
    by (auto intro: accessible_fromR.Immediate
                    Ext_foo_member_of_Ext Ext_foo_permits_acc)

    lemma Ext_foo_dyn_accessible [simp]:
     "tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from S"
    apply (rule dyn_accessible_fromR.Immediate)
    apply   (rule Ext_foo_member_in_Ext)
    apply   (rule Ext_foo_permits_acc)
    done

    lemma Ext_foo_overrides_Base_foo:
     "tprg\<turnstile>(Ext,Ext_foo) overrides (Base,Base_foo)"
    proof (rule overridesR.Direct, simp_all)
      show "¬ is_static Ext_foo"
        by (simp add: member_is_static_simp Ext_foo_def)
      show "¬ is_static Base_foo"
        by (simp add: member_is_static_simp Base_foo_def)
      show "accmodi Ext_foo ≠ Private"
        by (simp add: Ext_foo_def)
      show "msig (Ext, Ext_foo) = msig (Base, Base_foo)"
        by (simp add: Ext_foo_def Base_foo_def)
      show "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
        by (auto intro: Ext_declares_foo)
      show "tprg\<turnstile>mdecl Base_foo declared_in Base"
        by (auto intro: Base_declares_foo)
      show "tprg \<turnstile>(Base, mdecl Base_foo) inheritable_in java_lang"
        by (simp add: inheritable_in_def Base_foo_def)
      show "tprg\<turnstile>resTy Ext_foo\<preceq>resTy Base_foo"
        by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp)
    qed

    lemma accmethd_Ext [simp]:
      "accmethd tprg S Ext = methd tprg Ext"
    apply (simp add: accmethd_def)
    apply (rule filter_tab_all_True)
    apply (auto simp add: snd_special_simp fst_special_simp)
    done

    lemma cls_Ext: "class tprg Ext = Some ExtCl"
    by simp
    lemma dynmethd_Ext_foo:
     "dynmethd tprg Base Ext (|name = foo, parTs = [Class Base]|)),
      = Some (Ext,snd Ext_foo)"
    proof -
      have "methd tprg Base (|name = foo, parTs = [Class Base]|)),
              = Some (Base,snd Base_foo)" and
           "methd tprg Ext (|name = foo, parTs = [Class Base]|)),
              = Some (Ext,snd Ext_foo)"
        by (auto simp add: Ext_foo_def Base_foo_def foo_sig_def)
      with cls_Ext ws_tprg Ext_foo_overrides_Base_foo
      show ?thesis
        by (auto simp add: dynmethd_rec simp add: Ext_foo_def Base_foo_def)
    qed

    lemma Base_fields_accessible[simp]:
     "accfield tprg S Base
      = table_of((map (λ((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))"
    apply (auto simp add: accfield_def expand_fun_eq Let_def
                          accessible_in_RefT_simp
                          is_public_def
                          BaseCl_def
                          permits_acc_def
                          declared_in_def
                          cdeclaredfield_def
                   intro!: filter_tab_all_True_Some filter_tab_None
                           accessible_fromR.Immediate
                   intro: members.Immediate)
    done

    lemma arr_member_of_Base:
      "tprg\<turnstile>(Base, fdecl (arr,
                     (|access = Public, static = True, type = PrimT Boolean.[]|)),))
              member_of Base"
    by (auto intro: members.Immediate
           simp add: declared_in_def cdeclaredfield_def BaseCl_def)

    lemma arr_member_in_Base:
      "tprg\<turnstile>(Base, fdecl (arr,
                     (|access = Public, static = True, type = PrimT Boolean.[]|)),))
              member_in Base"
    by (rule member_of_to_member_in [OF arr_member_of_Base])

    lemma arr_member_of_Ext:
      "tprg\<turnstile>(Base, fdecl (arr,
                        (|access = Public, static = True, type = PrimT Boolean.[]|)),))
                 member_of Ext"
    apply (rule members.Inherited)
    apply   (simp add: inheritable_in_def)
    apply   (simp add: undeclared_in_def cdeclaredfield_def ExtCl_def)
    apply   (auto intro: arr_member_of_Base simp add: subcls1_def ExtCl_def)
    done

    lemma arr_member_in_Ext:
      "tprg\<turnstile>(Base, fdecl (arr,
                     (|access = Public, static = True, type = PrimT Boolean.[]|)),))
              member_in Ext"
    by (rule member_of_to_member_in [OF arr_member_of_Ext])

    lemma Ext_fields_accessible[simp]:
    "accfield tprg S Ext
      = table_of((map (λ((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))"
    apply (auto simp add: accfield_def expand_fun_eq Let_def
                          accessible_in_RefT_simp
                          is_public_def
                          BaseCl_def
                          ExtCl_def
                          permits_acc_def
                   intro!: filter_tab_all_True_Some filter_tab_None
                           accessible_fromR.Immediate)
    apply (auto intro: members.Immediate arr_member_of_Ext
                simp add: declared_in_def cdeclaredfield_def ExtCl_def)
    done

    lemma arr_Base_dyn_accessible [simp]:
    "tprg\<turnstile>(Base, fdecl (arr, (|access=Public,static=True ,type=PrimT Boolean.[]|)),))
           in Base dyn_accessible_from S"
    apply (rule dyn_accessible_fromR.Immediate)
    apply   (rule arr_member_in_Base)
    apply   (simp add: permits_acc_def)
    done

    lemma arr_Ext_dyn_accessible[simp]:
    "tprg\<turnstile>(Base, fdecl (arr, (|access=Public,static=True ,type=PrimT Boolean.[]|)),))
           in Ext dyn_accessible_from S"
    apply (rule dyn_accessible_fromR.Immediate)
    apply   (rule arr_member_in_Ext)
    apply   (simp add: permits_acc_def)
    done

    lemma array_of_PrimT_acc [simp]:
     "is_acc_type tprg java_lang (PrimT t.[])"
    apply (simp add: is_acc_type_def accessible_in_RefT_simp)
    done

    lemma PrimT_acc [simp]:
     "is_acc_type tprg java_lang (PrimT t)"
    apply (simp add: is_acc_type_def accessible_in_RefT_simp)
    done

    lemma Object_acc [simp]:
     "is_acc_class tprg java_lang Object"
    apply (auto simp add: is_acc_class_def accessible_in_RefT_simp is_public_def)
    done

    section "well-formedness"

    lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)"
    apply (unfold wf_idecl_def HasFooInt_def)
    apply (auto intro!: wf_mheadI ws_idecl_HasFoo
                simp add: foo_sig_def foo_mhead_def mhead_resTy_simp
                          member_is_static_simp )
    done

    declare member_is_static_simp [simp]
    declare wt.Skip [rule del] wt.Init [rule del]
    ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
    lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
    lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros

    lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
    lemmas Ext_foo_defs  = Ext_foo_def  foo_sig_def

    lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo"
    apply (unfold Base_foo_defs )
    apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs
                simp add: mhead_resTy_simp)
    (* for definite assignment *)
    apply (rule exI)
    apply (simp add: parameters_def)
    apply (rule conjI)
    apply  (rule da.Comp)
    apply     (rule da.Expr)
    apply     (rule da.AssLVar)
    apply       (rule da.AccLVar)
    apply         (simp)
    apply        (rule assigned.select_convs)
    apply       (simp)
    apply      (rule assigned.select_convs)
    apply     (simp)
    apply    (simp)
    apply    (rule da.Jmp)
    apply      (simp)
    apply     (rule assigned.select_convs)
    apply    (simp)
    apply   (rule assigned.select_convs)
    apply  (simp)
    apply (simp)
    done

    lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo"
    apply (unfold Ext_foo_defs )
    apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs
                simp add: mhead_resTy_simp )
    apply  (rule wt.Cast)
    prefer 2
    apply    simp
    apply   (rule_tac [2] narrow.subcls [THEN cast.narrow])
    apply   (auto intro!: wtIs)
    (* for definite assignment *)
    apply (rule exI)
    apply (simp add: parameters_def)
    apply (rule conjI)
    apply  (rule da.Comp)
    apply     (rule da.Expr)
    apply     (rule da.Ass)
    apply       simp
    apply      (rule da.FVar)
    apply      (rule da.Cast)
    apply      (rule da.AccLVar)
    apply        simp
    apply       (rule assigned.select_convs)
    apply      simp
    apply     (rule da_Lit)
    apply     (simp)
    apply    (rule da.Comp)
    apply       (rule da.Expr)
    apply       (rule da.AssLVar)
    apply         (rule da.Lit)
    apply        (rule assigned.select_convs)
    apply       simp
    apply      (rule da.Jmp)
    apply        simp
    apply       (rule assigned.select_convs)
    apply      simp
    apply     (rule assigned.select_convs)
    apply    (simp)
    apply   (rule assigned.select_convs)
    apply  simp
    apply simp
    done

    declare mhead_resTy_simp [simp add]
    declare member_is_static_simp [simp add]

    lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
    apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
    apply (auto intro!: wf_Base_foo)
    apply        (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def)
    apply   (auto intro!: wtIs)
    (* for definite assignment *)
    apply   (rule exI)
    apply   (rule da.Expr)
    apply  (rule da.Ass)
    apply    (simp)
    apply   (rule da.FVar)
    apply   (rule da.Cast)
    apply   (rule da_Lit)
    apply   simp
    apply  (rule da.NewA)
    apply  (rule da.Lit)
    apply (auto simp add: Base_foo_defs entails_def Let_def)
    apply   (insert Base_foo_no_stat_override, simp add: Base_foo_def,blast)+
    apply (insert Base_foo_no_hide         , simp add: Base_foo_def,blast)
    done

    lemma wf_ExtC: "wf_cdecl tprg (Ext,ExtCl)"
    apply (unfold wf_cdecl_def ExtCl_def)
    apply (auto intro!: wf_Ext_foo ws_cdecl_Ext)
    apply  (auto simp add: entails_def snd_special_simp)
    apply      (insert Ext_foo_stat_override)
    apply      (rule exI,rule da.Skip)
    apply     (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
    apply    (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
    apply   (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
    apply  (insert Ext_foo_no_hide)
    apply  (simp_all add: qmdecl_def)
    apply  blast+
    done

    lemma wf_MainC: "wf_cdecl tprg (Main,MainCl)"
    apply (unfold wf_cdecl_def MainCl_def)
    apply (auto intro: ws_cdecl_Main)
    apply (rule exI,rule da.Skip)
    done

    lemma wf_idecl_all: "p=tprg ==> Ball (set Ifaces) (wf_idecl p)"
    apply (simp (no_asm) add: Ifaces_def)
    apply (simp (no_asm_simp))
    apply (rule wf_HasFoo)
    done

    lemma wf_cdecl_all_standard_classes:
      "Ball (set standard_classes) (wf_cdecl tprg)"
    apply (unfold standard_classes_def Let_def
           ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
    apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
    apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def
                intro: da.Skip)
    apply (auto simp add: Object_def Classes_def standard_classes_def
                          SXcptC_def SXcpt_def)
    done

    lemma wf_cdecl_all: "p=tprg ==> Ball (set Classes) (wf_cdecl p)"
    apply (simp (no_asm) add: Classes_def)
    apply (simp (no_asm_simp))
    apply    (rule wf_BaseC [THEN conjI])
    apply   (rule wf_ExtC [THEN conjI])
    apply  (rule wf_MainC [THEN conjI])
    apply (rule wf_cdecl_all_standard_classes)
    done

    theorem wf_tprg: "wf_prog tprg"
    apply (unfold wf_prog_def Let_def)
    apply (simp (no_asm) add: unique_ifaces unique_classes)
    apply (rule conjI)
    apply  ((simp (no_asm) add: Classes_def standard_classes_def))
    apply (rule conjI)
    apply (simp add: Object_mdecls_def)
    apply safe
    apply  (cut_tac xn_cases)
    apply  (simp (no_asm_simp) add: Classes_def standard_classes_def)
    apply  (insert wf_idecl_all)
    apply  (insert wf_cdecl_all)
    apply  auto
    done

    section "max spec"

    lemma appl_methds_Base_foo:
    "appl_methds tprg S (ClassT Base) (|name=foo, parTs=[NT]|)), =
      {((ClassT Base, (|access=Public,static=False,pars=[z],resT=Class Base|)),)
        ,[Class Base])}"
    apply (unfold appl_methds_def)
    apply (simp (no_asm))
    apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
    apply  (auto simp add: cmheads_def Base_foo_defs)
    done

    lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) (|name=foo,parTs=[NT]|)), =
      {((ClassT Base, (|access=Public,static=False,pars=[z],resT=Class Base|)),)
       , [Class Base])}"
    apply (unfold max_spec_def)
    apply (simp (no_asm) add: appl_methds_Base_foo)
    apply auto
    done

    section "well-typedness"

    lemma wt_test: "(|prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)|)),\<turnstile>test ?pTs::\<surd>"
    apply (unfold test_def arr_viewed_from_def)
    (* ?pTs = [Class Base] *)
    apply (rule wtIs (* ;; *))
    apply  (rule wtIs (* Ass *))
    apply  (rule wtIs (* NewC *))
    apply     (rule wtIs (* LVar *))
    apply      (simp)
    apply     (simp)
    apply    (simp)
    apply   (rule wtIs (* NewC *))
    apply   (simp)
    apply  (simp)
    apply (rule wtIs (* Try *))
    prefer 4
    apply    (simp)
    defer
    apply    (rule wtIs (* Expr *))
    apply    (rule wtIs (* Call *))
    apply       (rule wtIs (* Acc *))
    apply       (rule wtIs (* LVar *))
    apply        (simp)
    apply       (simp)
    apply      (rule wtIs (* Cons *))
    apply       (rule wtIs (* Lit *))
    apply       (simp)
    apply      (rule wtIs (* Nil *))
    apply     (simp)
    apply     (rule max_spec_Base_foo)
    apply    (simp)
    apply   (simp)
    apply  (simp)
    apply  (simp)
    apply  (simp)
    apply (rule wtIs (* While *))
    apply  (rule wtIs (* Acc *))
    apply   (rule wtIs (* AVar *))
    apply   (rule wtIs (* Acc *))
    apply   (rule wtIs (* FVar *))
    apply    (rule wtIs (* StatRef *))
    apply    (simp)
    apply   (simp)
    apply   (simp )
    apply   (simp)
    apply   (simp)
    apply  (rule wtIs (* LVar *))
    apply  (simp)
    apply (rule wtIs (* Skip *))
    done

    section "definite assignment"

    lemma da_test: "(|prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)|)),
                      \<turnstile>{} »⟨test ?pTs⟩» (|nrm={VName e},brk=λ l. UNIV|)),"
    apply (unfold test_def arr_viewed_from_def)
    apply (rule da.Comp)
    apply    (rule da.Expr)
    apply    (rule da.AssLVar)
    apply      (rule da.NewC)
    apply     (rule assigned.select_convs)
    apply    (simp)
    apply   (rule da.Try)
    apply      (rule da.Expr)
    apply      (rule da.Call)
    apply       (rule da.AccLVar)
    apply         (simp)
    apply        (rule assigned.select_convs)
    apply       (simp)
    apply      (rule da.Cons)
    apply       (rule da.Lit)
    apply      (rule da.Nil)
    apply     (rule da.Loop)
    apply        (rule da.Acc)
    apply         (simp)
    apply        (rule da.AVar)
    apply         (rule da.Acc)
    apply          simp
    apply         (rule da.FVar)
    apply         (rule da.Cast)
    apply         (rule da.Lit)
    apply        (rule da.Lit)
    apply       (rule da_Skip)
    apply       (simp)
    apply      (simp,rule assigned.select_convs)
    apply     (simp)
    apply    (simp,rule assigned.select_convs)
    apply   (simp)
    apply  simp
    apply  blast
    apply simp
    apply (simp add: intersect_ts_def)
    done

    section "execution"

    lemma alloc_one: "!!a obj. [|the (new_Addr h) = a; atleast_free h (Suc n)|] ==>
      new_Addr h = Some a ∧ atleast_free (h(a\<mapsto>obj)) n"
    apply (frule atleast_free_SucD)
    apply (drule atleast_free_Suc [THEN iffD1])
    apply clarsimp
    apply (frule new_Addr_SomeI)
    apply force
    done

    declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp]
    declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp]
    declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
            Base_foo_defs  [simp]

    ML {* bind_thms ("eval_intros", map
            (simplify (simpset() delsimps [thm "Skip_eq"]
                                 addsimps [thm "lvar_def"]) o
             rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *}
    lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros

    consts
      a :: loc
      b :: loc
      c :: loc

    syntax

      tprg :: prog

      obj_a :: obj
      obj_b :: obj
      obj_c :: obj
      arr_N :: "(vn, val) table"
      arr_a :: "(vn, val) table"
      globs1 :: globs
      globs2 :: globs
      globs3 :: globs
      globs8 :: globs
      locs3 :: locals
      locs4 :: locals
      locs8 :: locals
      s0  :: state
      s0' :: state
      s9' :: state
      s1  :: state
      s1' :: state
      s2  :: state
      s2' :: state
      s3  :: state
      s3' :: state
      s4  :: state
      s4' :: state
      s6' :: state
      s7' :: state
      s8  :: state
      s8' :: state

    translations

      "tprg"    == "(|ifaces=Ifaces,classes=Classes|)),"

      "obj_a"   <= "(|tag=Arr (PrimT Boolean) two
                    ,values=empty(Inr 0\<mapsto>Bool False)(Inr one\<mapsto>Bool False)|)),"
      "obj_b"   <= "(|tag=CInst Ext
                    ,values=(empty(Inl (vee, Base)\<mapsto>Null   )
                                  (Inl (vee, Ext )\<mapsto>Intg 0))|)),"
      "obj_c"   == "(|tag=CInst (SXcpt NullPointer),values=empty|)),"
      "arr_N"   == "empty(Inl (arr, Base)\<mapsto>Null)"
      "arr_a"   == "empty(Inl (arr, Base)\<mapsto>Addr a)"
      "globs1"  == "empty(Inr Ext   \<mapsto>(|tag=arbitrary, values=empty|)),)
                         (Inr Base  \<mapsto>(|tag=arbitrary, values=arr_N|)),)
                         (Inr Object\<mapsto>(|tag=arbitrary, values=empty|)),)"
      "globs2"  == "empty(Inr Ext   \<mapsto>(|tag=arbitrary, values=empty|)),)
                         (Inr Object\<mapsto>(|tag=arbitrary, values=empty|)),)
                         (Inl a\<mapsto>obj_a)
                         (Inr Base  \<mapsto>(|tag=arbitrary, values=arr_a|)),)"
      "globs3"  == "globs2(Inl b\<mapsto>obj_b)"
      "globs8"  == "globs3(Inl c\<mapsto>obj_c)"
      "locs3"   == "empty(VName e\<mapsto>Addr b)"
      "locs4"   == "empty(VName z\<mapsto>Null)(Inr()\<mapsto>Addr b)"
      "locs8"   == "locs3(VName z\<mapsto>Addr c)"
      "s0"  == "       st empty  empty"
      "s0'" == " Norm  s0"
      "s1"  == "       st globs1 empty"
      "s1'" == " Norm  s1"
      "s2"  == "       st globs2 empty"
      "s2'" == " Norm  s2"
      "s3"  == "       st globs3 locs3 "
      "s3'" == " Norm  s3"
      "s4"  == "       st globs3 locs4"
      "s4'" == " Norm  s4"
      "s6'" == "(Some (Xcpt (Std NullPointer)), s4)"
      "s7'" == "(Some (Xcpt (Std NullPointer)), s3)"
      "s8"  == "       st globs8 locs8"
      "s8'" == " Norm  s8"
      "s9'" == "(Some (Xcpt (Std IndOutBound)), s8)"

    syntax "four"::nat
           "tree"::nat
           "two" ::nat
           "one" ::nat
    translations
      "one"  == "Suc 0"
      "two"  == "Suc one"
      "tree" == "Suc two"
      "four" == "Suc tree"

    declare Pair_eq [simp del]
    lemma exec_test:
    "[|the (new_Addr (heap  s1)) = a;
      the (new_Addr (heap ?s2)) = b;
      the (new_Addr (heap ?s3)) = c|] ==>
      atleast_free  (heap s0) four ==>
      tprg\<turnstile>s0' \<midarrow>test [Class Base]-> ?s9'"
    apply (unfold test_def arr_viewed_from_def)
    (* ?s9' = s9' *)
    apply (simp (no_asm_use))
    apply (drule (1) alloc_one,clarsimp)
    apply (rule eval_Is (* ;; *))
    apply  (erule_tac V = "the (new_Addr ?h) = c" in thin_rl)
    apply  (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
    apply  (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
    apply  (rule eval_Is (* Expr *))
    apply  (rule eval_Is (* Ass *))
    apply   (rule eval_Is (* LVar *))
    apply  (rule eval_Is (* NewC *))
          (* begin init Ext *)
    apply   (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
    apply   (erule_tac V = "atleast_free ?h tree" in thin_rl)
    apply   (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
    apply   (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
    apply   (rule eval_Is (* Init Ext *))
    apply   (simp)
    apply   (rule conjI)
    prefer 2 apply (rule conjI HOL.refl)+
    apply   (rule eval_Is (* Init Base *))
    apply   (simp add: arr_viewed_from_def)
    apply   (rule conjI)
    apply    (rule eval_Is (* Init Object *))
    apply    (simp)
    apply    (rule conjI, rule HOL.refl)+
    apply    (rule HOL.refl)
    apply   (simp)
    apply   (rule conjI, rule_tac [2] HOL.refl)
    apply   (rule eval_Is (* Expr *))
    apply   (rule eval_Is (* Ass *))
    apply    (rule eval_Is (* FVar *))
    apply         (rule init_done, simp)
    apply        (rule eval_Is (* StatRef *))
    apply       (simp)
    apply     (simp add: check_field_access_def Let_def)
    apply   (rule eval_Is (* NewA *))
    apply     (simp)
    apply    (rule eval_Is (* Lit *))
    apply   (simp)
    apply   (rule halloc.New)
    apply    (simp (no_asm_simp))
    apply   (drule atleast_free_weaken,drule atleast_free_weaken)
    apply   (simp (no_asm_simp))
    apply  (simp add: upd_gobj_def)
          (* end init Ext *)
    apply  (rule halloc.New)
    apply   (drule alloc_one)
    prefer 2 apply fast
    apply   (simp (no_asm_simp))
    apply  (drule atleast_free_weaken)
    apply  force
    apply (simp)
    apply (drule alloc_one)
    apply  (simp (no_asm_simp))
    apply clarsimp
    apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
    apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
    apply (simp (no_asm_use))
    apply (rule eval_Is (* Try *))
    apply   (rule eval_Is (* Expr *))
          (* begin method call *)
    apply   (rule eval_Is (* Call *))
    apply      (rule eval_Is (* Acc *))
    apply      (rule eval_Is (* LVar *))
    apply     (rule eval_Is (* Cons *))
    apply      (rule eval_Is (* Lit *))
    apply     (rule eval_Is (* Nil *))
    apply    (simp)
    apply    (simp)
    apply    (subgoal_tac
                 "tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from Main")
    apply      (simp add: check_method_access_def Let_def
                          invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
    apply      (rule Ext_foo_dyn_accessible)
    apply   (rule eval_Is (* Methd *))
    apply   (simp add: body_def Let_def)
    apply   (rule eval_Is (* Body *))
    apply     (rule init_done, simp)
    apply       (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
    apply    (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
    apply    (rule eval_Is (* Comp *))
    apply     (rule eval_Is (* Expr *))
    apply     (rule eval_Is (* Ass *))
    apply      (rule eval_Is (* FVar *))
    apply         (rule init_done, simp)
    apply        (rule eval_Is (* Cast *))
    apply         (rule eval_Is (* Acc *))
    apply         (rule eval_Is (* LVar *))
    apply        (simp)
    apply       (simp split del: split_if)
    apply      (simp add: check_field_access_def Let_def)
    apply     (rule eval_Is (* XcptE *))
    apply    (simp)
    apply    (rule conjI)
    apply     (simp)
    apply    (rule eval_Is (* Comp *))
    apply   (simp)
          (* end method call *)
    apply  simp
    apply  (rule sxalloc.intros)
    apply  (rule halloc.New)
    apply   (erule alloc_one [THEN conjunct1])
    apply   (simp (no_asm_simp))
    apply  (simp (no_asm_simp))
    apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
    apply (drule alloc_one [THEN conjunct1])
    apply  (simp (no_asm_simp))
    apply (erule_tac V = "atleast_free ?h two" in thin_rl)
    apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
    apply simp
    apply (rule eval_Is (* While *))
    apply  (rule eval_Is (* Acc *))
    apply  (rule eval_Is (* AVar *))
    apply    (rule eval_Is (* Acc *))
    apply    (rule eval_Is (* FVar *))
    apply      (rule init_done, simp)
    apply     (rule eval_Is (* StatRef *))
    apply    (simp)
    apply    (simp add: check_field_access_def Let_def)
    apply   (rule eval_Is (* Lit *))
    apply  (simp (no_asm_simp))
    apply (auto simp add: in_bounds_def)
    done
    declare Pair_eq [simp]

    end

lemma wf_fdecl_def2:

      wf_fdecl G P fd = is_acc_type G P (type (snd fd))

## type and expression names

lemma neq_Base_Object:

      Base ≠ Object

lemma neq_Ext_Object:

      Ext ≠ Object

lemma neq_Main_Object:

      Main ≠ Object

lemma neq_Base_SXcpt:

      Base ≠ SXcpt xn

lemma neq_Ext_SXcpt:

      Ext ≠ SXcpt xn

lemma neq_Main_SXcpt:

      Main ≠ SXcpt xn

## classes and interfaces

lemmas table_classes_defs:

      Classes == [(Base, BaseCl), (Ext, ExtCl), (Main, MainCl)] @ standard_classes

      standard_classes ==
      [ObjectC, SXcptC Throwable, SXcptC NullPointer, SXcptC OutOfMemory,
       SXcptC ClassCast, SXcptC NegArrSize, SXcptC IndOutBound, SXcptC ArrStore]

      ObjectC ==
      (Object,
       (| access = Public, cfields = [], methods = Object_mdecls, init = Skip,
          super = arbitrary, superIfs = [] |))

      SXcptC xn ==
      (SXcpt xn,
       (| access = Public, cfields = [], methods = SXcpt_mdecls, init = Skip,
          super = if xn = Throwable then Object else SXcpt Throwable,
          superIfs = [] |))

lemmas table_classes_defs:

      Classes == [(Base, BaseCl), (Ext, ExtCl), (Main, MainCl)] @ standard_classes

      standard_classes ==
      [ObjectC, SXcptC Throwable, SXcptC NullPointer, SXcptC OutOfMemory,
       SXcptC ClassCast, SXcptC NegArrSize, SXcptC IndOutBound, SXcptC ArrStore]

      ObjectC ==
      (Object,
       (| access = Public, cfields = [], methods = Object_mdecls, init = Skip,
          super = arbitrary, superIfs = [] |))

      SXcptC xn ==
      (SXcpt xn,
       (| access = Public, cfields = [], methods = SXcpt_mdecls, init = Skip,
          super = if xn = Throwable then Object else SXcpt Throwable,
          superIfs = [] |))

lemma table_ifaces:

      table_of Ifaces = [HasFoo |-> HasFooInt]

lemma table_classes_Object:

      table_of Classes Object =
      Some (| access = Public, cfields = [], methods = Object_mdecls, init = Skip,
              super = arbitrary, superIfs = [] |)

lemma table_classes_SXcpt:

      table_of Classes (SXcpt xn) =
      Some (| access = Public, cfields = [], methods = SXcpt_mdecls, init = Skip,
              super = if xn = Throwable then Object else SXcpt Throwable,
              superIfs = [] |)

lemma table_classes_HasFoo:

      table_of Classes HasFoo = None

lemma table_classes_Base:

      table_of Classes Base = Some BaseCl

lemma table_classes_Ext:

      table_of Classes Ext = Some ExtCl

lemma table_classes_Main:

      table_of Classes Main = Some MainCl

## program

## well-structuredness

lemma not_Object_subcls_any:

      tprg|-Object<:C C ==> R

lemma not_Throwable_subcls_SXcpt:

      tprg|-SXcpt Throwable<:C SXcpt xn ==> R

lemma not_SXcpt_n_subcls_SXcpt_n:

      tprg|-SXcpt xn<:C SXcpt xn ==> R

lemma not_Base_subcls_Ext:

      tprg|-Base<:C Ext ==> R

lemma not_TName_n_subcls_TName_n:

      tprg|-(| pid = java_lang,
               tid = TName tn |)<:C (| pid = java_lang, tid = TName tn |)
      ==> R

lemma ws_idecl_HasFoo:

      ws_idecl tprg HasFoo []

lemma ws_cdecl_Object:

      ws_cdecl tprg Object any

lemma ws_cdecl_Throwable:

      ws_cdecl tprg (SXcpt Throwable) Object

lemma ws_cdecl_SXcpt:

      ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)

lemma ws_cdecl_Base:

      ws_cdecl tprg Base Object

lemma ws_cdecl_Ext:

      ws_cdecl tprg Ext Base

lemma ws_cdecl_Main:

      ws_cdecl tprg Main Object

lemmas ws_cdecls:

      ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)

      ws_cdecl tprg Object any

      ws_cdecl tprg (SXcpt Throwable) Object

      ws_cdecl tprg Base Object

      ws_cdecl tprg Ext Base

      ws_cdecl tprg Main Object

lemmas ws_cdecls:

      ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)

      ws_cdecl tprg Object any

      ws_cdecl tprg (SXcpt Throwable) Object

      ws_cdecl tprg Base Object

      ws_cdecl tprg Ext Base

      ws_cdecl tprg Main Object

lemma ws_idecl_all:

      G = tprg ==> ∀(I, i)∈set Ifaces. ws_idecl G I (isuperIfs i)

lemma ws_cdecl_all:

      G = tprg ==> ∀(C, c)∈set Classes. ws_cdecl G C (super c)

lemma ws_tprg:

      ws_prog tprg

## misc program properties (independent of well-structuredness)

lemma single_iface:

      is_iface tprg I = (I = HasFoo)

lemma empty_subint1:

      subint1 tprg = {}

lemma unique_ifaces:

      unique Ifaces

lemma unique_classes:

      unique Classes

lemma SXcpt_subcls_Throwable:

      tprg|-SXcpt xn<=:C SXcpt Throwable

lemma Ext_subclseq_Base:

      tprg|-Ext<=:C Base

lemma Ext_subcls_Base:

      tprg|-Ext<:C Base

## fields and method lookup

lemma fields_tprg_Object:

      DeclConcepts.fields tprg Object = []

lemma fields_tprg_Throwable:

      DeclConcepts.fields tprg (SXcpt Throwable) = []

lemma fields_tprg_SXcpt:

      DeclConcepts.fields tprg (SXcpt xn) = []

lemmas fields_rec_:

      class tprg C = Some c
      ==> DeclConcepts.fields tprg C =
          map (%(fn, ft). ((fn, C), ft)) (cfields c) @
          (if C = Object then [] else DeclConcepts.fields tprg (super c))

lemmas fields_rec_:

      class tprg C = Some c
      ==> DeclConcepts.fields tprg C =
          map (%(fn, ft). ((fn, C), ft)) (cfields c) @
          (if C = Object then [] else DeclConcepts.fields tprg (super c))

lemma fields_Base:

      DeclConcepts.fields tprg Base =
      [((arr, Base), (| access = Public, static = True, type = PrimT Boolean.[] |)),
       ((vee, Base), (| access = Public, static = False, type = Iface HasFoo |))]

lemma fields_Ext:

      DeclConcepts.fields tprg Ext =
      [((vee, Ext), (| access = Public, static = False, type = PrimT Integer |))] @
      DeclConcepts.fields tprg Base

lemmas imethds_rec_:

      iface tprg I = Some i
      ==> DeclConcepts.imethds tprg I =
          Un_tables (DeclConcepts.imethds tprg ` set (isuperIfs i)) ⊕⊕
          (o2s o table_of (map (%(s, mh). (s, I, mh)) (imethods i)))

lemmas imethds_rec_:

      iface tprg I = Some i
      ==> DeclConcepts.imethds tprg I =
          Un_tables (DeclConcepts.imethds tprg ` set (isuperIfs i)) ⊕⊕
          (o2s o table_of (map (%(s, mh). (s, I, mh)) (imethods i)))

lemmas methd_rec_:

      class tprg C = Some c
      ==> methd tprg C =
          (if C = Object then empty
           else filter_tab (%sig m. tprg \<turnstile> C inherits method sig m)
                 (methd tprg (super c))) ++
          table_of (map (%(s, m). (s, C, m)) (methods c))

lemmas methd_rec_:

      class tprg C = Some c
      ==> methd tprg C =
          (if C = Object then empty
           else filter_tab (%sig m. tprg \<turnstile> C inherits method sig m)
                 (methd tprg (super c))) ++
          table_of (map (%(s, m). (s, C, m)) (methods c))

lemma imethds_HasFoo:

      DeclConcepts.imethds tprg HasFoo = o2s o [foo_sig |-> (HasFoo, foo_mhead)]

lemma methd_tprg_Object:

      methd tprg Object = empty

lemma methd_Base:

      methd tprg Base = table_of [(%(s, m). (s, Base, m)) Base_foo]

lemma memberid_Base_foo_simp:

      memberid (mdecl Base_foo) = mid foo_sig

lemma memberid_Ext_foo_simp:

      memberid (mdecl Ext_foo) = mid foo_sig

lemma Base_declares_foo:

      tprg\<turnstile> mdecl Base_foo declared_in Base

lemma foo_sig_not_undeclared_in_Base:

      ¬ tprg\<turnstile> mid foo_sig undeclared_in Base

lemma Ext_declares_foo:

      tprg\<turnstile> mdecl Ext_foo declared_in Ext

lemma foo_sig_not_undeclared_in_Ext:

      ¬ tprg\<turnstile> mid foo_sig undeclared_in Ext

lemma Base_foo_not_inherited_in_Ext:

      ¬ tprg \<turnstile> Ext inherits (Base, mdecl Base_foo)

lemma Ext_method_inheritance:

      filter_tab (%sig m. tprg \<turnstile> Ext inherits method sig m)
       [fst ((%(s, m). (s, Base, m)) Base_foo) |->
        snd ((%(s, m). (s, Base, m)) Base_foo)] =
      empty

lemma methd_Ext:

      methd tprg Ext = table_of [(%(s, m). (s, Ext, m)) Ext_foo]

## accessibility

lemma classesDefined:

      [| class tprg C = Some c; C ≠ Object |] ==> ∃sc. class tprg (super c) = Some sc

lemma superclassesBase:

      superclasses tprg Base = {Object}

lemma superclassesExt:

      superclasses tprg Ext = {Base, Object}

lemma superclassesMain:

      superclasses tprg Main = {Object}

lemma HasFoo_accessible:

      tprg \<turnstile> Iface HasFoo accessible_in P

lemma HasFoo_is_acc_iface:

      is_acc_iface tprg P HasFoo

lemma HasFoo_is_acc_type:

      is_acc_type tprg P (Iface HasFoo)

lemma Base_accessible:

      tprg \<turnstile> Class Base accessible_in P

lemma Base_is_acc_class:

      is_acc_class tprg P Base

lemma Base_is_acc_type:

      is_acc_type tprg P (Class Base)

lemma Ext_accessible:

      tprg \<turnstile> Class Ext accessible_in P

lemma Ext_is_acc_class:

      is_acc_class tprg P Ext

lemma Ext_is_acc_type:

      is_acc_type tprg P (Class Ext)

lemma accmethd_tprg_Object:

      accmethd tprg S Object = empty

lemma snd_special_simp:

      snd ((%(s, m). (s, a, m)) x) = (a, snd x)

lemma fst_special_simp:

      fst ((%(s, m). (s, a, m)) x) = fst x

lemma foo_sig_undeclared_in_Object:

      tprg\<turnstile> mid foo_sig undeclared_in Object

lemma unique_sig_Base_foo:

      tprg\<turnstile> mdecl (sig, snd Base_foo) declared_in Base ==> sig = foo_sig

lemma Base_foo_no_override:

      tprg \<turnstile> qmdecl sig (Base, snd Base_foo) overrides qmdecl sig old ==> P

lemma Base_foo_no_stat_override:

      tprg \<turnstile> qmdecl sig (Base, snd Base_foo) overridesS qmdecl sig old
      ==> P

lemma Base_foo_no_hide:

      tprg\<turnstile> qmdecl sig (Base, snd Base_foo) hides qmdecl sig old ==> P

lemma Ext_foo_no_hide:

      tprg\<turnstile> qmdecl sig (Ext, snd Ext_foo) hides qmdecl sig old ==> P

lemma unique_sig_Ext_foo:

      tprg\<turnstile> mdecl (sig, snd Ext_foo) declared_in Ext ==> sig = foo_sig

lemma Ext_foo_override:

      tprg \<turnstile> qmdecl sig (Ext, snd Ext_foo) overrides qmdecl sig old
      ==> old = (Base, snd Base_foo)

lemma Ext_foo_stat_override:

      tprg \<turnstile> qmdecl sig (Ext, snd Ext_foo) overridesS qmdecl sig old
      ==> old = (Base, snd Base_foo)

lemma Base_foo_member_of_Base:

      (Base, Base, mdecl Base_foo) ∈ members tprg

lemma Base_foo_member_in_Base:

      tprg \<turnstile> (Base, mdecl Base_foo) member_in Base

lemma Ext_foo_member_of_Ext:

      (Ext, Ext, mdecl Ext_foo) ∈ members tprg

lemma Ext_foo_member_in_Ext:

      tprg \<turnstile> (Ext, mdecl Ext_foo) member_in Ext

lemma Base_foo_permits_acc:

      tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_from S

lemma Base_foo_accessible:

      tprg \<turnstile> (Base, mdecl Base_foo) of Base accessible_from S

lemma Base_foo_dyn_accessible:

      tprg \<turnstile> (Base, mdecl Base_foo) in Base dyn_accessible_from S

lemma accmethd_Base:

      accmethd tprg S Base = methd tprg Base

lemma Ext_foo_permits_acc:

      tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_from S

lemma Ext_foo_accessible:

      tprg \<turnstile> (Ext, mdecl Ext_foo) of Ext accessible_from S

lemma Ext_foo_dyn_accessible:

      tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext dyn_accessible_from S

lemma Ext_foo_overrides_Base_foo:

      ((Ext, Ext_foo), Base, Base_foo) ∈ overridesR tprg

lemma accmethd_Ext:

      accmethd tprg S Ext = methd tprg Ext

lemma cls_Ext:

      class tprg Ext = Some ExtCl

lemma dynmethd_Ext_foo:

      dynmethd tprg Base Ext (| name = foo, parTs = [Class Base] |) =
      Some (Ext, snd Ext_foo)

lemma Base_fields_accessible:

      accfield tprg S Base =
      table_of (map (%((n, d), f). (n, d, f)) (DeclConcepts.fields tprg Base))

lemma arr_member_of_Base:

      (Base, Base,
       fdecl (arr, (| access = Public, static = True, type = PrimT Boolean.[] |)))
      ∈ members tprg

lemma arr_member_in_Base:

      tprg \<turnstile> (Base,
                         fdecl
                          (arr,
                           (| access = Public, static = True,
                              type = PrimT Boolean.[] |))) member_in Base

lemma arr_member_of_Ext:

      (Ext, Base,
       fdecl (arr, (| access = Public, static = True, type = PrimT Boolean.[] |)))
      ∈ members tprg

lemma arr_member_in_Ext:

      tprg \<turnstile> (Base,
                         fdecl
                          (arr,
                           (| access = Public, static = True,
                              type = PrimT Boolean.[] |))) member_in Ext

lemma Ext_fields_accessible:

      accfield tprg S Ext =
      table_of (map (%((n, d), f). (n, d, f)) (DeclConcepts.fields tprg Ext))

lemma arr_Base_dyn_accessible:

      tprg \<turnstile> (Base,
                         fdecl
                          (arr,
                           (| access = Public, static = True,
                              type =
                                PrimT Boolean.[] |))) in Base dyn_accessible_from S

lemma arr_Ext_dyn_accessible:

      tprg \<turnstile> (Base,
                         fdecl
                          (arr,
                           (| access = Public, static = True,
                              type =
                                PrimT Boolean.[] |))) in Ext dyn_accessible_from S

lemma array_of_PrimT_acc:

      is_acc_type tprg java_lang (PrimT t.[])

lemma PrimT_acc:

      is_acc_type tprg java_lang (PrimT t)

lemma Object_acc:

      is_acc_class tprg java_lang Object

## well-formedness

lemma wf_HasFoo:

      wf_idecl tprg (HasFoo, HasFooInt)

theorems wt_intros:

      E,dt|=Skip:<>

      E,dt|=e:-T ==> E,dt|=Expr e:<>

      E,dt|=c:<> ==> E,dt|=l• c:<>

      [| E,dt|=c1.0:<>; E,dt|=c2.0:<> |] ==> E,dt|=c1.0;; c2.0:<>

      [| E,dt|=e:-PrimT Boolean; E,dt|=c1.0:<>; E,dt|=c2.0:<> |]
      ==> E,dt|=If(e) c1.0 Else c2.0:<>

      [| E,dt|=e:-PrimT Boolean; E,dt|=c:<> |] ==> E,dt|=l• While(e) c:<>

      E,dt|=Jmp jump:<>

      [| E,dt|=e:-Class tn; prg E|-tn<=:C SXcpt Throwable |] ==> E,dt|=Throw e:<>

      [| E,dt|=c1.0:<>; prg E|-tn<=:C SXcpt Throwable; lcl E (VName vn) = None;
         E(| lcl := lcl E(VName vn |-> Class tn) |),dt|=c2.0:<> |]
      ==> E,dt|=Try c1.0 Catch(tn vn) c2.0:<>

      [| E,dt|=c1.0:<>; E,dt|=c2.0:<> |] ==> E,dt|=c1.0 Finally c2.0:<>

      is_class (prg E) C ==> E,dt|=Init C:<>

      is_acc_class (prg E) (pkg E) C ==> E,dt|=NewC C:-Class C

      [| is_acc_type (prg E) (pkg E) T; E,dt|=i:-PrimT Integer |]
      ==> E,dt|=New T[i]:-T.[]

      [| E,dt|=e:-T; is_acc_type (prg E) (pkg E) T'; prg E|-T<=:? T' |]
      ==> E,dt|=Cast T' e:-T'

      [| E,dt|=e:-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
         prg E|-RefT T<=:? RefT T' |]
      ==> E,dt|=e InstOf T':-PrimT Boolean

      typeof dt x = Some T ==> E,dt|=Lit x:-T

      [| E,dt|=e:-Te; wt_unop unop Te; T = PrimT (unop_type unop) |]
      ==> E,dt|=UnOp unop e:-T

      [| E,dt|=e1.0:-T1.0; E,dt|=e2.0:-T2.0; wt_binop (prg E) binop T1.0 T2.0;
         T = PrimT (binop_type binop) |]
      ==> E,dt|=BinOp binop e1.0 e2.0:-T

      [| lcl E This = Some (Class C); C ≠ Object; class (prg E) C = Some c |]
      ==> E,dt|=Super:-Class (super c)

      E,dt|=va:=T ==> E,dt|=Acc va:-T

      [| E,dt|=va:=T; va ≠ LVar This; E,dt|=v:-T'; prg E|-T'<=:T |]
      ==> E,dt|=va:=v:-T'

      [| E,dt|=e0.0:-PrimT Boolean; E,dt|=e1.0:-T1.0; E,dt|=e2.0:-T2.0;
         prg E|-T1.0<=:T2.0 ∧ T = T2.0 ∨ prg E|-T2.0<=:T1.0 ∧ T = T1.0 |]
      ==> E,dt|=e0.0 ? e1.0 : e2.0:-T

      [| E,dt|=e:-RefT statT; E,dt|=ps:#pTs;
         max_spec (prg E) (cls E) statT (| name = mn, parTs = pTs |) =
         {((statDeclT, m), pTs')} |]
      ==> E,dt|={cls E,statT,invmode m e}e·mn( {pTs'}ps):-resTy m

      [| is_class (prg E) C; methd (prg E) C sig = Some m;
         E,dt|=Body (declclass m) (stmt (mbody (mthd m))):-T |]
      ==> E,dt|=Methd C sig:-T

      [| is_class (prg E) D; E,dt|=blk:<>; lcl E Result = Some T; is_type (prg E) T |]
      ==> E,dt|=Body D blk:-T

      [| lcl E vn = Some T; is_acc_type (prg E) (pkg E) T |] ==> E,dt|=LVar vn:=T

      [| E,dt|=e:-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC, f) |]
      ==> E,dt|={cls E,statDeclC,is_static f}e..fn:=type f

      [| E,dt|=e:-T.[]; E,dt|=i:-PrimT Integer |] ==> E,dt|=e.[i]:=T

      E,dt|=[]:#[]

      [| E,dt|=e:-T; E,dt|=es:#Ts |] ==> E,dt|=e # es:#T # Ts

lemmas wtIs:

      [| E,dt|=e:-RefT statT; E,dt|=ps:#pTs;
         max_spec (prg E) (cls E) statT (| name = mn, parTs = pTs |) =
         {((statDeclC, m), pTs')};
         rT = resTy m; accC = cls E; mode = invmode m e |]
      ==> E,dt|={accC,statT,mode}e·mn( {pTs'}ps):-rT

      [| lcl E This = Some (Class C); C ≠ Object; class (prg E) C = Some c;
         D = super c |]
      ==> E,dt|=Super:-Class D

      [| E,dt|=e:-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC, f);
         sf = is_static f; fT = type f; accC = cls E |]
      ==> E,dt|={accC,statDeclC,sf}e..fn:=fT

      is_acc_type (prg E) (pkg E) (RefT rt) ==> E|-StatRef rt:-RefT rt

      E,dt|=Skip:<>

      E,dt|=e:-T ==> E,dt|=Expr e:<>

      E,dt|=c:<> ==> E,dt|=l• c:<>

      [| E,dt|=c1.0:<>; E,dt|=c2.0:<> |] ==> E,dt|=c1.0;; c2.0:<>

      [| E,dt|=e:-PrimT Boolean; E,dt|=c1.0:<>; E,dt|=c2.0:<> |]
      ==> E,dt|=If(e) c1.0 Else c2.0:<>

      [| E,dt|=e:-PrimT Boolean; E,dt|=c:<> |] ==> E,dt|=l• While(e) c:<>

      E,dt|=Jmp jump:<>

      [| E,dt|=e:-Class tn; prg E|-tn<=:C SXcpt Throwable |] ==> E,dt|=Throw e:<>

      [| E,dt|=c1.0:<>; prg E|-tn<=:C SXcpt Throwable; lcl E (VName vn) = None;
         E(| lcl := lcl E(VName vn |-> Class tn) |),dt|=c2.0:<> |]
      ==> E,dt|=Try c1.0 Catch(tn vn) c2.0:<>

      [| E,dt|=c1.0:<>; E,dt|=c2.0:<> |] ==> E,dt|=c1.0 Finally c2.0:<>

      is_class (prg E) C ==> E,dt|=Init C:<>

      is_acc_class (prg E) (pkg E) C ==> E,dt|=NewC C:-Class C

      [| is_acc_type (prg E) (pkg E) T; E,dt|=i:-PrimT Integer |]
      ==> E,dt|=New T[i]:-T.[]

      [| E,dt|=e:-T; is_acc_type (prg E) (pkg E) T'; prg E|-T<=:? T' |]
      ==> E,dt|=Cast T' e:-T'

      [| E,dt|=e:-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
         prg E|-RefT T<=:? RefT T' |]
      ==> E,dt|=e InstOf T':-PrimT Boolean

      typeof dt x = Some T ==> E,dt|=Lit x:-T

      [| E,dt|=e:-Te; wt_unop unop Te; T = PrimT (unop_type unop) |]
      ==> E,dt|=UnOp unop e:-T

      [| E,dt|=e1.0:-T1.0; E,dt|=e2.0:-T2.0; wt_binop (prg E) binop T1.0 T2.0;
         T = PrimT (binop_type binop) |]
      ==> E,dt|=BinOp binop e1.0 e2.0:-T

      [| lcl E This = Some (Class C); C ≠ Object; class (prg E) C = Some c |]
      ==> E,dt|=Super:-Class (super c)

      E,dt|=va:=T ==> E,dt|=Acc va:-T

      [| E,dt|=va:=T; va ≠ LVar This; E,dt|=v:-T'; prg E|-T'<=:T |]
      ==> E,dt|=va:=v:-T'

      [| E,dt|=e0.0:-PrimT Boolean; E,dt|=e1.0:-T1.0; E,dt|=e2.0:-T2.0;
         prg E|-T1.0<=:T2.0 ∧ T = T2.0 ∨ prg E|-T2.0<=:T1.0 ∧ T = T1.0 |]
      ==> E,dt|=e0.0 ? e1.0 : e2.0:-T

      [| E,dt|=e:-RefT statT; E,dt|=ps:#pTs;
         max_spec (prg E) (cls E) statT (| name = mn, parTs = pTs |) =
         {((statDeclT, m), pTs')} |]
      ==> E,dt|={cls E,statT,invmode m e}e·mn( {pTs'}ps):-resTy m

      [| is_class (prg E) C; methd (prg E) C sig = Some m;
         E,dt|=Body (declclass m) (stmt (mbody (mthd m))):-T |]
      ==> E,dt|=Methd C sig:-T

      [| is_class (prg E) D; E,dt|=blk:<>; lcl E Result = Some T; is_type (prg E) T |]
      ==> E,dt|=Body D blk:-T

      [| lcl E vn = Some T; is_acc_type (prg E) (pkg E) T |] ==> E,dt|=LVar vn:=T

      [| E,dt|=e:-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC, f) |]
      ==> E,dt|={cls E,statDeclC,is_static f}e..fn:=type f

      [| E,dt|=e:-T.[]; E,dt|=i:-PrimT Integer |] ==> E,dt|=e.[i]:=T

      E,dt|=[]:#[]

      [| E,dt|=e:-T; E,dt|=es:#Ts |] ==> E,dt|=e # es:#T # Ts

lemmas wtIs:

      [| E,dt|=e:-RefT statT; E,dt|=ps:#pTs;
         max_spec (prg E) (cls E) statT (| name = mn, parTs = pTs |) =
         {((statDeclC, m), pTs')};
         rT = resTy m; accC = cls E; mode = invmode m e |]
      ==> E,dt|={accC,statT,mode}e·mn( {pTs'}ps):-rT

      [| lcl E This = Some (Class C); C ≠ Object; class (prg E) C = Some c;
         D = super c |]
      ==> E,dt|=Super:-Class D

      [| E,dt|=e:-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC, f);
         sf = is_static f; fT = type f; accC = cls E |]
      ==> E,dt|={accC,statDeclC,sf}e..fn:=fT

      is_acc_type (prg E) (pkg E) (RefT rt) ==> E|-StatRef rt:-RefT rt

      E,dt|=Skip:<>

      E,dt|=e:-T ==> E,dt|=Expr e:<>

      E,dt|=c:<> ==> E,dt|=l• c:<>

      [| E,dt|=c1.0:<>; E,dt|=c2.0:<> |] ==> E,dt|=c1.0;; c2.0:<>

      [| E,dt|=e:-PrimT Boolean; E,dt|=c1.0:<>; E,dt|=c2.0:<> |]
      ==> E,dt|=If(e) c1.0 Else c2.0:<>

      [| E,dt|=e:-PrimT Boolean; E,dt|=c:<> |] ==> E,dt|=l• While(e) c:<>

      E,dt|=Jmp jump:<>

      [| E,dt|=e:-Class tn; prg E|-tn<=:C SXcpt Throwable |] ==> E,dt|=Throw e:<>

      [| E,dt|=c1.0:<>; prg E|-tn<=:C SXcpt Throwable; lcl E (VName vn) = None;
         E(| lcl := lcl E(VName vn |-> Class tn) |),dt|=c2.0:<> |]
      ==> E,dt|=Try c1.0 Catch(tn vn) c2.0:<>

      [| E,dt|=c1.0:<>; E,dt|=c2.0:<> |] ==> E,dt|=c1.0 Finally c2.0:<>

      is_class (prg E) C ==> E,dt|=Init C:<>

      is_acc_class (prg E) (pkg E) C ==> E,dt|=NewC C:-Class C

      [| is_acc_type (prg E) (pkg E) T; E,dt|=i:-PrimT Integer |]
      ==> E,dt|=New T[i]:-T.[]

      [| E,dt|=e:-T; is_acc_type (prg E) (pkg E) T'; prg E|-T<=:? T' |]
      ==> E,dt|=Cast T' e:-T'

      [| E,dt|=e:-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
         prg E|-RefT T<=:? RefT T' |]
      ==> E,dt|=e InstOf T':-PrimT Boolean

      typeof dt x = Some T ==> E,dt|=Lit x:-T

      [| E,dt|=e:-Te; wt_unop unop Te; T = PrimT (unop_type unop) |]
      ==> E,dt|=UnOp unop e:-T

      [| E,dt|=e1.0:-T1.0; E,dt|=e2.0:-T2.0; wt_binop (prg E) binop T1.0 T2.0;
         T = PrimT (binop_type binop) |]
      ==> E,dt|=BinOp binop e1.0 e2.0:-T

      [| lcl E This = Some (Class C); C ≠ Object; class (prg E) C = Some c |]
      ==> E,dt|=Super:-Class (super c)

      E,dt|=va:=T ==> E,dt|=Acc va:-T

      [| E,dt|=va:=T; va ≠ LVar This; E,dt|=v:-T'; prg E|-T'<=:T |]
      ==> E,dt|=va:=v:-T'

      [| E,dt|=e0.0:-PrimT Boolean; E,dt|=e1.0:-T1.0; E,dt|=e2.0:-T2.0;
         prg E|-T1.0<=:T2.0 ∧ T = T2.0 ∨ prg E|-T2.0<=:T1.0 ∧ T = T1.0 |]
      ==> E,dt|=e0.0 ? e1.0 : e2.0:-T

      [| E,dt|=e:-RefT statT; E,dt|=ps:#pTs;
         max_spec (prg E) (cls E) statT (| name = mn, parTs = pTs |) =
         {((statDeclT, m), pTs')} |]
      ==> E,dt|={cls E,statT,invmode m e}e·mn( {pTs'}ps):-resTy m

      [| is_class (prg E) C; methd (prg E) C sig = Some m;
         E,dt|=Body (declclass m) (stmt (mbody (mthd m))):-T |]
      ==> E,dt|=Methd C sig:-T

      [| is_class (prg E) D; E,dt|=blk:<>; lcl E Result = Some T; is_type (prg E) T |]
      ==> E,dt|=Body D blk:-T

      [| lcl E vn = Some T; is_acc_type (prg E) (pkg E) T |] ==> E,dt|=LVar vn:=T

      [| E,dt|=e:-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC, f) |]
      ==> E,dt|={cls E,statDeclC,is_static f}e..fn:=type f

      [| E,dt|=e:-T.[]; E,dt|=i:-PrimT Integer |] ==> E,dt|=e.[i]:=T

      E,dt|=[]:#[]

      [| E,dt|=e:-T; E,dt|=es:#Ts |] ==> E,dt|=e # es:#T # Ts

lemmas daIs:

      nrm (| nrm = nrm, brk = brk, ... = more |) = nrm

      brk (| nrm = nrm, brk = brk, ... = more |) = brk

      assigned.more (| nrm = nrm, brk = brk, ... = more |) = more

      A = (| nrm = B, brk = %l. UNIV |) ==> Env\<turnstile> B »⟨Skip⟩» A

      A = (| nrm = B, brk = %l. UNIV |) ==> Env\<turnstile> B »⟨NewC C⟩» A

      A = (| nrm = B, brk = %l. UNIV |) ==> Env\<turnstile> B »⟨Lit v⟩» A

      [| This ∈ B; A = (| nrm = B, brk = %l. UNIV |) |]
      ==> Env\<turnstile> B »⟨Super⟩» A

      Env\<turnstile> B »⟨Skip⟩» (| nrm = B, brk = %l. UNIV |)

      Env\<turnstile> B »⟨e⟩» A ==> Env\<turnstile> B »⟨Expr e⟩» A

      [| Env\<turnstile> B »⟨c⟩» C; nrm A = nrm C ∩ brk C l;
         brk A = rmlab l (brk C) |]
      ==> Env\<turnstile> B »⟨Break l• c⟩» A

      [| Env\<turnstile> B »⟨c1.0⟩» C1.0; Env\<turnstile> nrm C1.0 »⟨c2.0⟩» C2.0;
         nrm A = nrm C2.0; brk A = brk C1.0 =>∩  brk C2.0 |]
      ==> Env\<turnstile> B »⟨c1.0;; c2.0⟩» A

      [| Env\<turnstile> B »⟨e⟩» E;
         Env\<turnstile> B ∪ assigns_if True e »⟨c1.0⟩» C1.0;
         Env\<turnstile> B ∪ assigns_if False e »⟨c2.0⟩» C2.0;
         nrm A = nrm C1.0 ∩ nrm C2.0; brk A = brk C1.0 =>∩  brk C2.0 |]
      ==> Env\<turnstile> B »⟨If(e) c1.0 Else c2.0⟩» A

      [| Env\<turnstile> B »⟨e⟩» E; Env\<turnstile> B ∪ assigns_if True e »⟨c⟩» C;
         nrm A = nrm C ∩ (B ∪ assigns_if False e); brk A = brk C |]
      ==> Env\<turnstile> B »⟨l• While(e) c⟩» A

      [| jump = Ret --> Result ∈ B; nrm A = UNIV;
         brk A =
         (case jump of Break l => %k. if k = l then B else UNIV | _ => %k. UNIV) |]
      ==> Env\<turnstile> B »⟨Jmp jump⟩» A

      [| Env\<turnstile> B »⟨e⟩» E; nrm A = UNIV; brk A = (%l. UNIV) |]
      ==> Env\<turnstile> B »⟨Throw e⟩» A

      [| Env\<turnstile> B »⟨c1.0⟩» C1.0;
         Env(| lcl := lcl Env(VName vn |->
                 Class C) |)\<turnstile> B ∪ {VName vn} »⟨c2.0⟩» C2.0;
         nrm A = nrm C1.0 ∩ nrm C2.0; brk A = brk C1.0 =>∩  brk C2.0 |]
      ==> Env\<turnstile> B »⟨Try c1.0 Catch(C vn) c2.0⟩» A

      [| Env\<turnstile> B »⟨c1.0⟩» C1.0; Env\<turnstile> B »⟨c2.0⟩» C2.0;
         nrm A = nrm C1.0 ∪ nrm C2.0;
         brk A = (brk C1.0 =>∪∀ nrm C2.0) =>∩  brk C2.0 |]
      ==> Env\<turnstile> B »⟨c1.0 Finally c2.0⟩» A

      Env\<turnstile> B »⟨Init C⟩» (| nrm = B, brk = %l. UNIV |)

      Env\<turnstile> B »⟨NewC C⟩» (| nrm = B, brk = %l. UNIV |)

      Env\<turnstile> B »⟨e⟩» A ==> Env\<turnstile> B »⟨New T[e]⟩» A

      Env\<turnstile> B »⟨e⟩» A ==> Env\<turnstile> B »⟨Cast T e⟩» A

      Env\<turnstile> B »⟨e⟩» A ==> Env\<turnstile> B »⟨e InstOf T⟩» A

      Env\<turnstile> B »⟨Lit v⟩» (| nrm = B, brk = %l. UNIV |)

      Env\<turnstile> B »⟨e⟩» A ==> Env\<turnstile> B »⟨UnOp unop e⟩» A

      [| Env\<turnstile> B »⟨e1.0⟩» E1.0;
         Env\<turnstile> B ∪ assigns_if True e1.0 »⟨e2.0⟩» E2.0;
         nrm A =
         B ∪ assigns_if True (BinOp CondAnd e1.0 e2.0) ∩
             assigns_if False (BinOp CondAnd e1.0 e2.0);
         brk A = (%l. UNIV) |]
      ==> Env\<turnstile> B »⟨BinOp CondAnd e1.0 e2.0⟩» A

      [| Env\<turnstile> B »⟨e1.0⟩» E1.0;
         Env\<turnstile> B ∪ assigns_if False e1.0 »⟨e2.0⟩» E2.0;
         nrm A =
         B ∪ assigns_if True (BinOp CondOr e1.0 e2.0) ∩
             assigns_if False (BinOp CondOr e1.0 e2.0);
         brk A = (%l. UNIV) |]
      ==> Env\<turnstile> B »⟨BinOp CondOr e1.0 e2.0⟩» A

      [| Env\<turnstile> B »⟨e1.0⟩» E1.0; Env\<turnstile> nrm E1.0 »⟨e2.0⟩» A;
         binop ≠ CondAnd; binop ≠ CondOr |]
      ==> Env\<turnstile> B »⟨BinOp binop e1.0 e2.0⟩» A

      This ∈ B ==> Env\<turnstile> B »⟨Super⟩» (| nrm = B, brk = %l. UNIV |)

      [| vn ∈ B; nrm A = B; brk A = (%k. UNIV) |]
      ==> Env\<turnstile> B »⟨Acc (LVar vn)⟩» A

      [| ∀vn. v ≠ LVar vn; Env\<turnstile> B »⟨v⟩» A |]
      ==> Env\<turnstile> B »⟨Acc v⟩» A

      [| Env\<turnstile> B »⟨e⟩» E; nrm A = nrm E ∪ {vn}; brk A = brk E |]
      ==> Env\<turnstile> B »⟨LVar vn:=e⟩» A

      [| ∀vn. v ≠ LVar vn; Env\<turnstile> B »⟨v⟩» V; Env\<turnstile> nrm V »⟨e⟩» A |]
      ==> Env\<turnstile> B »⟨v:=e⟩» A

      [| Env|-c ? e1.0 : e2.0:-PrimT Boolean; Env\<turnstile> B »⟨c⟩» C;
         Env\<turnstile> B ∪ assigns_if True c »⟨e1.0⟩» E1.0;
         Env\<turnstile> B ∪ assigns_if False c »⟨e2.0⟩» E2.0;
         nrm A =
         B ∪ assigns_if True (c ? e1.0 : e2.0) ∩ assigns_if False (c ? e1.0 : e2.0);
         brk A = (%l. UNIV) |]
      ==> Env\<turnstile> B »⟨c ? e1.0 : e2.0⟩» A

      [| (Env, empty_dt, In1l (c ? e1.0 : e2.0), Inl (PrimT Boolean)) ∉ wt;
         Env\<turnstile> B »⟨c⟩» C;
         Env\<turnstile> B ∪ assigns_if True c »⟨e1.0⟩» E1.0;
         Env\<turnstile> B ∪ assigns_if False c »⟨e2.0⟩» E2.0;
         nrm A = nrm E1.0 ∩ nrm E2.0; brk A = (%l. UNIV) |]
      ==> Env\<turnstile> B »⟨c ? e1.0 : e2.0⟩» A

      [| Env\<turnstile> B »⟨e⟩» E; Env\<turnstile> nrm E »⟨args⟩» A |]
      ==> Env\<turnstile> B »⟨{accC,statT,mode}e·mn( {pTs}args)⟩» A

      [| methd (prg Env) D sig = Some m;
         Env\<turnstile> B »⟨Body (declclass m) (stmt (mbody (mthd m)))⟩» A |]
      ==> Env\<turnstile> B »⟨Methd D sig⟩» A

      [| Env\<turnstile> B »⟨c⟩» C; jumpNestingOkS {Ret} c; Result ∈ nrm C; nrm A = B;
         brk A = (%l. UNIV) |]
      ==> Env\<turnstile> B »⟨Body D c⟩» A

      Env\<turnstile> B »⟨LVar vn⟩» (| nrm = B, brk = %l. UNIV |)

      Env\<turnstile> B »⟨e⟩» A ==> Env\<turnstile> B »⟨{accC,statDeclC,stat}e..fn⟩» A

      [| Env\<turnstile> B »⟨e1.0⟩» E1.0; Env\<turnstile> nrm E1.0 »⟨e2.0⟩» A |]
      ==> Env\<turnstile> B »⟨e1.0.[e2.0]⟩» A

      Env\<turnstile> B »⟨[]⟩» (| nrm = B, brk = %l. UNIV |)

      [| Env\<turnstile> B »⟨e⟩» E; Env\<turnstile> nrm E »⟨es⟩» A |]
      ==> Env\<turnstile> B »⟨e # es⟩» A

lemmas daIs:

      nrm (| nrm = nrm, brk = brk, ... = more |) = nrm

      brk (| nrm = nrm, brk = brk, ... = more |) = brk

      assigned.more (| nrm = nrm, brk = brk, ... = more |) = more

      A = (| nrm = B, brk = %l. UNIV |) ==> Env\<turnstile> B »⟨Skip⟩» A

      A = (| nrm = B, brk = %l. UNIV |) ==> Env\<turnstile> B »⟨NewC C⟩» A

      A = (| nrm = B, brk = %l. UNIV |) ==> Env\<turnstile> B »⟨Lit v⟩» A

      [| This ∈ B; A = (| nrm = B, brk = %l. UNIV |) |]
      ==> Env\<turnstile> B »⟨Super⟩» A

      Env\<turnstile> B »⟨Skip⟩» (| nrm = B, brk = %l. UNIV |)

      Env\<turnstile> B »⟨e⟩» A ==> Env\<turnstile> B »⟨Expr e⟩» A

      [| Env\<turnstile> B »⟨c⟩» C; nrm A = nrm C ∩ brk C l;
         brk A = rmlab l (brk C) |]
      ==> Env\<turnstile> B »⟨Break l• c⟩» A

      [| Env\<turnstile> B »⟨c1.0⟩» C1.0; Env\<turnstile> nrm C1.0 »⟨c2.0⟩» C2.0;
         nrm A = nrm C2.0; brk A = brk C1.0 =>∩  brk C2.0 |]
      ==> Env\<turnstile> B »⟨c1.0;; c2.0⟩» A

      [| Env\<turnstile> B »⟨e⟩» E;
         Env\<turnstile> B ∪ assigns_if True e »⟨c1.0⟩» C1.0;
         Env\<turnstile> B ∪ assigns_if False e »⟨c2.0⟩» C2.0;
         nrm A = nrm C1.0 ∩ nrm C2.0; brk A = brk C1.0 =>∩  brk C2.0 |]
      ==> Env\<turnstile> B »⟨If(e) c1.0 Else c2.0⟩» A

      [| Env\<turnstile> B »⟨e⟩» E; Env\<turnstile> B ∪ assigns_if True e »⟨c⟩» C;
         nrm A = nrm C ∩ (B ∪ assigns_if False e); brk A = brk C |]
      ==> Env\<turnstile> B »⟨l• While(e) c⟩» A

      [| jump = Ret --> Result ∈ B; nrm A = UNIV;
         brk A =
         (case jump of Break l => %k. if k = l then B else UNIV | _ => %k. UNIV) |]
      ==> Env\<turnstile> B »⟨Jmp jump⟩» A

      [| Env\<turnstile> B »⟨e⟩» E; nrm A = UNIV; brk A = (%l. UNIV) |]
      ==> Env\<turnstile> B »⟨Throw e⟩» A

      [| Env\<turnstile> B »⟨c1.0⟩» C1.0;
         Env(| lcl := lcl Env(VName vn |->
                 Class C) |)\<turnstile> B ∪ {VName vn} »⟨c2.0⟩» C2.0;
         nrm A = nrm C1.0 ∩ nrm C2.0; brk A = brk C1.0 =>∩  brk C2.0 |]
      ==> Env\<turnstile> B »⟨Try c1.0 Catch(C vn) c2.0⟩» A

      [| Env\<turnstile> B »⟨c1.0⟩» C1.0; Env\<turnstile> B »⟨c2.0⟩» C2.0;
         nrm A = nrm C1.0 ∪ nrm C2.0;
         brk A = (brk C1.0 =>∪∀ nrm C2.0) =>∩  brk C2.0 |]
      ==> Env\<turnstile> B »⟨c1.0 Finally c2.0⟩» A

      Env\<turnstile> B »⟨Init C⟩» (| nrm = B, brk = %l. UNIV |)

      Env\<turnstile> B »⟨NewC C⟩» (| nrm = B, brk = %l. UNIV |)

      Env\<turnstile> B »⟨e⟩» A ==> Env\<turnstile> B »⟨New T[e]⟩» A

      Env\<turnstile> B »⟨e⟩» A ==> Env\<turnstile> B »⟨Cast T e⟩» A

      Env\<turnstile> B »⟨e⟩» A ==> Env\<turnstile> B »⟨e InstOf T⟩» A

      Env\<turnstile> B »⟨Lit v⟩» (| nrm = B, brk = %l. UNIV |)

      Env\<turnstile> B »⟨e⟩» A ==> Env\<turnstile> B »⟨UnOp unop e⟩» A

      [| Env\<turnstile> B »⟨e1.0⟩» E1.0;
         Env\<turnstile> B ∪ assigns_if True e1.0 »⟨e2.0⟩» E2.0;
         nrm A =
         B ∪ assigns_if True (BinOp CondAnd e1.0 e2.0) ∩
             assigns_if False (BinOp CondAnd e1.0 e2.0);
         brk A = (%l. UNIV) |]
      ==> Env\<turnstile> B »⟨BinOp CondAnd e1.0 e2.0⟩» A

      [| Env\<turnstile> B »⟨e1.0⟩» E1.0;
         Env\<turnstile> B ∪ assigns_if False e1.0 »⟨e2.0⟩» E2.0;
         nrm A =
         B ∪ assigns_if True (BinOp CondOr e1.0 e2.0) ∩
             assigns_if False (BinOp CondOr e1.0 e2.0);
         brk A = (%l. UNIV) |]
      ==> Env\<turnstile> B »⟨BinOp CondOr e1.0 e2.0⟩» A

      [| Env\<turnstile> B »⟨e1.0⟩» E1.0; Env\<turnstile> nrm E1.0 »⟨e2.0⟩» A;
         binop ≠ CondAnd; binop ≠ CondOr |]
      ==> Env\<turnstile> B »⟨BinOp binop e1.0 e2.0⟩» A

      This ∈ B ==> Env\<turnstile> B »⟨Super⟩» (| nrm = B, brk = %l. UNIV |)

      [| vn ∈ B; nrm A = B; brk A = (%k. UNIV) |]
      ==> Env\<turnstile> B »⟨Acc (LVar vn)⟩» A

      [| ∀vn. v ≠ LVar vn; Env\<turnstile> B »⟨v⟩» A |]
      ==> Env\<turnstile> B »⟨Acc v⟩» A

      [| Env\<turnstile> B »⟨e⟩» E; nrm A = nrm E ∪ {vn}; brk A = brk E |]
      ==> Env\<turnstile> B »⟨LVar vn:=e⟩» A

      [| ∀vn. v ≠ LVar vn; Env\<turnstile> B »⟨v⟩» V; Env\<turnstile> nrm V »⟨e⟩» A |]
      ==> Env\<turnstile> B »⟨v:=e⟩» A

      [| Env|-c ? e1.0 : e2.0:-PrimT Boolean; Env\<turnstile> B »⟨c⟩» C;
         Env\<turnstile> B ∪ assigns_if True c »⟨e1.0⟩» E1.0;
         Env\<turnstile> B ∪ assigns_if False c »⟨e2.0⟩» E2.0;
         nrm A =
         B ∪ assigns_if True (c ? e1.0 : e2.0) ∩ assigns_if False (c ? e1.0 : e2.0);
         brk A = (%l. UNIV) |]
      ==> Env\<turnstile> B »⟨c ? e1.0 : e2.0⟩» A

      [| (Env, empty_dt, In1l (c ? e1.0 : e2.0), Inl (PrimT Boolean)) ∉ wt;
         Env\<turnstile> B »⟨c⟩» C;
         Env\<turnstile> B ∪ assigns_if True c »⟨e1.0⟩» E1.0;
         Env\<turnstile> B ∪ assigns_if False c »⟨e2.0⟩» E2.0;
         nrm A = nrm E1.0 ∩ nrm E2.0; brk A = (%l. UNIV) |]
      ==> Env\<turnstile> B »⟨c ? e1.0 : e2.0⟩» A

      [| Env\<turnstile> B »⟨e⟩» E; Env\<turnstile> nrm E »⟨args⟩» A |]
      ==> Env\<turnstile> B »⟨{accC,statT,mode}e·mn( {pTs}args)⟩» A

      [| methd (prg Env) D sig = Some m;
         Env\<turnstile> B »⟨Body (declclass m) (stmt (mbody (mthd m)))⟩» A |]
      ==> Env\<turnstile> B »⟨Methd D sig⟩» A

      [| Env\<turnstile> B »⟨c⟩» C; jumpNestingOkS {Ret} c; Result ∈ nrm C; nrm A = B;
         brk A = (%l. UNIV) |]
      ==> Env\<turnstile> B »⟨Body D c⟩» A

      Env\<turnstile> B »⟨LVar vn⟩» (| nrm = B, brk = %l. UNIV |)

      Env\<turnstile> B »⟨e⟩» A ==> Env\<turnstile> B »⟨{accC,statDeclC,stat}e..fn⟩» A

      [| Env\<turnstile> B »⟨e1.0⟩» E1.0; Env\<turnstile> nrm E1.0 »⟨e2.0⟩» A |]
      ==> Env\<turnstile> B »⟨e1.0.[e2.0]⟩» A

      Env\<turnstile> B »⟨[]⟩» (| nrm = B, brk = %l. UNIV |)

      [| Env\<turnstile> B »⟨e⟩» E; Env\<turnstile> nrm E »⟨es⟩» A |]
      ==> Env\<turnstile> B »⟨e # es⟩» A

lemmas Base_foo_defs:

      Base_foo ==
      (foo_sig,
       (| access = Public, static = False, pars = [z], resT = Class Base,
          mbody = (| lcls = [], stmt = Return (!! z) |) |))

      foo_sig == (| name = foo, parTs = [Class Base] |)

      foo_mhead ==
      (| access = Public, static = False, pars = [z], resT = Class Base |)

lemmas Base_foo_defs:

      Base_foo ==
      (foo_sig,
       (| access = Public, static = False, pars = [z], resT = Class Base,
          mbody = (| lcls = [], stmt = Return (!! z) |) |))

      foo_sig == (| name = foo, parTs = [Class Base] |)

      foo_mhead ==
      (| access = Public, static = False, pars = [z], resT = Class Base |)

lemmas Ext_foo_defs:

      Ext_foo ==
      (foo_sig,
       (| access = Public, static = False, pars = [z], resT = Class Ext,
          mbody =
            (| lcls = [],
               stmt =
                 Expr ({Ext,Ext,False}Cast (Class Ext)
                                       (!! z)..vee:=Lit
             (Intg 1));; Return (Lit Null) |) |))

      foo_sig == (| name = foo, parTs = [Class Base] |)

lemmas Ext_foo_defs:

      Ext_foo ==
      (foo_sig,
       (| access = Public, static = False, pars = [z], resT = Class Ext,
          mbody =
            (| lcls = [],
               stmt =
                 Expr ({Ext,Ext,False}Cast (Class Ext)
                                       (!! z)..vee:=Lit
             (Intg 1));; Return (Lit Null) |) |))

      foo_sig == (| name = foo, parTs = [Class Base] |)

lemma wf_Base_foo:

      wf_mdecl tprg Base Base_foo

lemma wf_Ext_foo:

      wf_mdecl tprg Ext Ext_foo

lemma wf_BaseC:

      wf_cdecl tprg (Base, BaseCl)

lemma wf_ExtC:

      wf_cdecl tprg (Ext, ExtCl)

lemma wf_MainC:

      wf_cdecl tprg (Main, MainCl)

lemma wf_idecl_all:

      p = tprg ==> Ball (set Ifaces) (wf_idecl p)

lemma wf_cdecl_all_standard_classes:

      Ball (set standard_classes) (wf_cdecl tprg)

lemma wf_cdecl_all:

      p = tprg ==> Ball (set Classes) (wf_cdecl p)

theorem wf_tprg:

      wf_prog tprg

## max spec

lemma appl_methds_Base_foo:

      appl_methds tprg S (ClassT Base) (| name = foo, parTs = [NT] |) =
      {((ClassT Base,
         (| access = Public, static = False, pars = [z], resT = Class Base |)),
        [Class Base])}

lemma max_spec_Base_foo:

      max_spec tprg S (ClassT Base) (| name = foo, parTs = [NT] |) =
      {((ClassT Base,
         (| access = Public, static = False, pars = [z], resT = Class Base |)),
        [Class Base])}

## well-typedness

lemma wt_test:

      (| prg = tprg, cls = Main,
         lcl = [VName e |-> Class Base] |)|-test [Class Base]:<>

## definite assignment

lemma da_test:

      (| prg = tprg, cls = Main,
         lcl = [VName e |->
                Class
                 Base] |)\<turnstile> {} »⟨test pTs⟩» (| nrm = {VName e},
                 brk = %l. UNIV |)

## execution

lemma alloc_one:

      [| the (new_Addr h) = a; atleast_free h (Suc n) |]
      ==> new_Addr h = Some a ∧ atleast_free (h(a |-> obj)) n

theorems eval_intros:

      G|-(Some xc, s) -t>-> (arbitrary3 t, Some xc, s)

      G|-Norm s -Skip-> Norm s

      G|-Norm s0.0 -e->v-> s1.0 ==> G|-Norm s0.0 -Expr e-> s1.0

      G|-Norm s0.0 -c-> s1.0 ==> G|-Norm s0.0 -l• c-> abupd (absorb l) s1.0

      [| G|-Norm s0.0 -c1.0-> s1.0; G|-s1.0 -c2.0-> s2.0 |]
      ==> G|-Norm s0.0 -c1.0;; c2.0-> s2.0

      [| G|-Norm s0.0 -e->b-> s1.0;
         G|-s1.0 -(if the_Bool b then c1.0 else c2.0)-> s2.0 |]
      ==> G|-Norm s0.0 -If(e) c1.0 Else c2.0-> s2.0

      [| G|-Norm s0.0 -e->b-> s1.0;
         if the_Bool b
         then G|-s1.0 -c-> s2.0 ∧
              G|-abupd (absorb (Cont l)) s2.0 -l• While(e) c-> s3.0
         else s3.0 = s1.0 |]
      ==> G|-Norm s0.0 -l• While(e) c-> s3.0

      G|-Norm s -Jmp j-> (Some (Jump j), s)

      G|-Norm s0.0 -e->a'-> s1.0 ==> G|-Norm s0.0 -Throw e-> abupd (throw a') s1.0

      [| G|-Norm s0.0 -c1.0-> s1.0; G|-s1.0 -sxalloc-> s2.0;
         if G,s2.0\<turnstile>catch C then G|-new_xcpt_var vn s2.0 -c2.0-> s3.0
         else s3.0 = s2.0 |]
      ==> G|-Norm s0.0 -Try c1.0 Catch(C vn) c2.0-> s3.0

      [| G|-Norm s0.0 -c1.0-> (x1.0, s1.0); G|-Norm s1.0 -c2.0-> s2.0;
         s3.0 =
         (if ∃err. x1.0 = Some (Error err) then (x1.0, s1.0)
          else abupd (abrupt_if (x1.0 ≠ None) x1.0) s2.0) |]
      ==> G|-Norm s0.0 -c1.0 Finally c2.0-> s3.0

      [| the (class G C) = c;
         if inited C (globs s0.0) then s3.0 = Norm s0.0
         else G|-Norm ((init_class_obj G C)
                        s0.0) -(if C = Object then Skip else Init (super c))-> s1.0 ∧
              G|-(set_lvars empty) s1.0 -init c-> s2.0 ∧
              s3.0 = (set_lvars (locals (snd s1.0))) s2.0 |]
      ==> G|-Norm s0.0 -Init C-> s3.0

      [| G|-Norm s0.0 -Init C-> s1.0; G|-s1.0 -halloc CInst C>a-> s2.0 |]
      ==> G|-Norm s0.0 -NewC C->Addr a-> s2.0

      [| G|-Norm s0.0 -init_comp_ty T-> s1.0; G|-s1.0 -e->i'-> s2.0;
         G|-abupd (check_neg i') s2.0 -halloc Arr T (the_Intg i')>a-> s3.0 |]
      ==> G|-Norm s0.0 -New T[e]->Addr a-> s3.0

      [| G|-Norm s0.0 -e->v-> s1.0;
         s2.0 = abupd (raise_if (¬ G,snd s1.0\<turnstile>v fits T) ClassCast) s1.0 |]
      ==> G|-Norm s0.0 -Cast T e->v-> s2.0

      [| G|-Norm s0.0 -e->v-> s1.0;
         b = (v ≠ Null ∧ G,snd s1.0\<turnstile>v fits RefT T) |]
      ==> G|-Norm s0.0 -e InstOf T->Bool b-> s1.0

      G|-Norm s -Lit v->v-> Norm s

      G|-Norm s0.0 -e->v-> s1.0 ==> G|-Norm s0.0 -UnOp unop e->eval_unop unop v-> s1.0

      [| G|-Norm s0.0 -e1.0->v1.0-> s1.0;
         G|-s1.0 -(if need_second_arg binop v1.0 then In1l e2.0
                   else In1r Skip)>-> (In1 v2.0, s2.0) |]
      ==> G|-Norm s0.0 -BinOp binop e1.0 e2.0->eval_binop binop v1.0 v2.0-> s2.0

      G|-Norm s -Super->val_this s-> Norm s

      G|-Norm s0.0 -va=>(v, f)-> s1.0 ==> G|-Norm s0.0 -Acc va->v-> s1.0

      [| G|-Norm s0.0 -va=>(w, f)-> s1.0; G|-s1.0 -e->v-> s2.0 |]
      ==> G|-Norm s0.0 -va:=e->v-> (%(x, s).
                                       (%(x', s'). (x', if x' = None then s' else s))
                                        ((if x = None then f v else id) (x, s)))
                                    s2.0

      [| G|-Norm s0.0 -e0.0->b-> s1.0;
         G|-s1.0 -(if the_Bool b then e1.0 else e2.0)->v-> s2.0 |]
      ==> G|-Norm s0.0 -e0.0 ? e1.0 : e2.0->v-> s2.0

      [| G|-Norm s0.0 -e->a'-> s1.0; G|-s1.0 -args#>vs-> s2.0;
         D = invocation_declclass G mode (snd s2.0) a' statT
              (| name = mn, parTs = pTs |);
         s3.0 = init_lvars G D (| name = mn, parTs = pTs |) mode a' vs s2.0;
         s3' =
         check_method_access G accC statT mode (| name = mn, parTs = pTs |) a' s3.0;
         G|-s3' -Methd D (| name = mn, parTs = pTs |)->v-> s4.0 |]
      ==> G|-Norm s0.0 -{accC,statT,mode}e·mn( {pTs}args)->v-> (set_lvars
                         (locals (snd s2.0)))
                        s4.0

      G|-Norm s0.0 -body G D sig->v-> s1.0 ==> G|-Norm s0.0 -Methd D sig->v-> s1.0

      [| G|-Norm s0.0 -Init D-> s1.0; G|-s1.0 -c-> s2.0;
         s3.0 =
         (if ∃l. fst s2.0 = Some (Jump (Break l)) ∨ fst s2.0 = Some (Jump (Cont l))
          then abupd (%x. Some (Error CrossMethodJump)) s2.0 else s2.0) |]
      ==> G|-Norm s0.0 -Body D
                         c->the (locals (snd s2.0) Result)-> abupd (absorb Ret) s3.0

      G|-Norm s -LVar vn=>(the (locals s vn), %v. supd lupd(vn\<mapsto>v))-> Norm s

      [| G|-Norm s0.0 -Init statDeclC-> s1.0; G|-s1.0 -e->a-> s2.0;
         (v, s2') = fvar statDeclC stat fn a s2.0;
         s3.0 = check_field_access G accC statDeclC fn stat a s2' |]
      ==> G|-Norm s0.0 -{accC,statDeclC,stat}e..fn=>v-> s3.0

      [| G|-Norm s0.0 -e1.0->a-> s1.0; G|-s1.0 -e2.0->i-> s2.0;
         (v, s2') = avar G i a s2.0 |]
      ==> G|-Norm s0.0 -e1.0.[e2.0]=>v-> s2'

      G|-Norm s0.0 -[]#>[]-> Norm s0.0

      [| G|-Norm s0.0 -e->v-> s1.0; G|-s1.0 -es#>vs-> s2.0 |]
      ==> G|-Norm s0.0 -e # es#>v # vs-> s2.0

lemmas eval_Is:

      if inited C (globs s0.0) then s3.0 = Norm s0.0
      else G|-Norm ((init_class_obj G C)
                     s0.0) -(if C = Object then Skip
                             else Init (super (the (class G C))))-> s1.0 ∧
           G|-(set_lvars empty) s1.0 -init (the (class G C))-> s2.0 ∧
           s3.0 = (set_lvars (locals (snd s1.0))) s2.0
      ==> G|-Norm s0.0 -Init C-> s3.0

      G|-s -StatRef rt->(if fst s = None then Null else arbitrary)-> s

      G|-(Some xc, s) -x->arbitrary-> (Some xc, s)

      G|-(Some xc, s) -x=>arbitrary-> (Some xc, s)

      G|-(Some xc, s) -x#>arbitrary-> (Some xc, s)

      G|-(Some xc, s) -x-> (Some xc, s)

      G|-(Some xc, s) -t>-> (arbitrary3 t, Some xc, s)

      G|-Norm s -Skip-> Norm s

      G|-Norm s0.0 -e->v-> s1.0 ==> G|-Norm s0.0 -Expr e-> s1.0

      G|-Norm s0.0 -c-> s1.0 ==> G|-Norm s0.0 -l• c-> abupd (absorb l) s1.0

      [| G|-Norm s0.0 -c1.0-> s1.0; G|-s1.0 -c2.0-> s2.0 |]
      ==> G|-Norm s0.0 -c1.0;; c2.0-> s2.0

      [| G|-Norm s0.0 -e->b-> s1.0;
         G|-s1.0 -(if the_Bool b then c1.0 else c2.0)-> s2.0 |]
      ==> G|-Norm s0.0 -If(e) c1.0 Else c2.0-> s2.0

      [| G|-Norm s0.0 -e->b-> s1.0;
         if the_Bool b
         then G|-s1.0 -c-> s2.0 ∧
              G|-abupd (absorb (Cont l)) s2.0 -l• While(e) c-> s3.0
         else s3.0 = s1.0 |]
      ==> G|-Norm s0.0 -l• While(e) c-> s3.0

      G|-Norm s -Jmp j-> (Some (Jump j), s)

      G|-Norm s0.0 -e->a'-> s1.0 ==> G|-Norm s0.0 -Throw e-> abupd (throw a') s1.0

      [| G|-Norm s0.0 -c1.0-> s1.0; G|-s1.0 -sxalloc-> s2.0;
         if G,s2.0\<turnstile>catch C then G|-new_xcpt_var vn s2.0 -c2.0-> s3.0
         else s3.0 = s2.0 |]
      ==> G|-Norm s0.0 -Try c1.0 Catch(C vn) c2.0-> s3.0

      [| G|-Norm s0.0 -c1.0-> (x1.0, s1.0); G|-Norm s1.0 -c2.0-> s2.0;
         s3.0 =
         (if ∃err. x1.0 = Some (Error err) then (x1.0, s1.0)
          else abupd (abrupt_if (x1.0 ≠ None) x1.0) s2.0) |]
      ==> G|-Norm s0.0 -c1.0 Finally c2.0-> s3.0

      [| the (class G C) = c;
         if inited C (globs s0.0) then s3.0 = Norm s0.0
         else G|-Norm ((init_class_obj G C)
                        s0.0) -(if C = Object then Skip else Init (super c))-> s1.0 ∧
              G|-(set_lvars empty) s1.0 -init c-> s2.0 ∧
              s3.0 = (set_lvars (locals (snd s1.0))) s2.0 |]
      ==> G|-Norm s0.0 -Init C-> s3.0

      [| G|-Norm s0.0 -Init C-> s1.0; G|-s1.0 -halloc CInst C>a-> s2.0 |]
      ==> G|-Norm s0.0 -NewC C->Addr a-> s2.0

      [| G|-Norm s0.0 -init_comp_ty T-> s1.0; G|-s1.0 -e->i'-> s2.0;
         G|-abupd (check_neg i') s2.0 -halloc Arr T (the_Intg i')>a-> s3.0 |]
      ==> G|-Norm s0.0 -New T[e]->Addr a-> s3.0

      [| G|-Norm s0.0 -e->v-> s1.0;
         s2.0 = abupd (raise_if (¬ G,snd s1.0\<turnstile>v fits T) ClassCast) s1.0 |]
      ==> G|-Norm s0.0 -Cast T e->v-> s2.0

      [| G|-Norm s0.0 -e->v-> s1.0;
         b = (v ≠ Null ∧ G,snd s1.0\<turnstile>v fits RefT T) |]
      ==> G|-Norm s0.0 -e InstOf T->Bool b-> s1.0

      G|-Norm s -Lit v->v-> Norm s

      G|-Norm s0.0 -e->v-> s1.0 ==> G|-Norm s0.0 -UnOp unop e->eval_unop unop v-> s1.0

      [| G|-Norm s0.0 -e1.0->v1.0-> s1.0;
         G|-s1.0 -(if need_second_arg binop v1.0 then In1l e2.0
                   else In1r Skip)>-> (In1 v2.0, s2.0) |]
      ==> G|-Norm s0.0 -BinOp binop e1.0 e2.0->eval_binop binop v1.0 v2.0-> s2.0

      G|-Norm s -Super->val_this s-> Norm s

      G|-Norm s0.0 -va=>(v, f)-> s1.0 ==> G|-Norm s0.0 -Acc va->v-> s1.0

      [| G|-Norm s0.0 -va=>(w, f)-> s1.0; G|-s1.0 -e->v-> s2.0 |]
      ==> G|-Norm s0.0 -va:=e->v-> (%(x, s).
                                       (%(x', s'). (x', if x' = None then s' else s))
                                        ((if x = None then f v else id) (x, s)))
                                    s2.0

      [| G|-Norm s0.0 -e0.0->b-> s1.0;
         G|-s1.0 -(if the_Bool b then e1.0 else e2.0)->v-> s2.0 |]
      ==> G|-Norm s0.0 -e0.0 ? e1.0 : e2.0->v-> s2.0

      [| G|-Norm s0.0 -e->a'-> s1.0; G|-s1.0 -args#>vs-> s2.0;
         D = invocation_declclass G mode (snd s2.0) a' statT
              (| name = mn, parTs = pTs |);
         s3.0 = init_lvars G D (| name = mn, parTs = pTs |) mode a' vs s2.0;
         s3' =
         check_method_access G accC statT mode (| name = mn, parTs = pTs |) a' s3.0;
         G|-s3' -Methd D (| name = mn, parTs = pTs |)->v-> s4.0 |]
      ==> G|-Norm s0.0 -{accC,statT,mode}e·mn( {pTs}args)->v-> (set_lvars
                         (locals (snd s2.0)))
                        s4.0

      G|-Norm s0.0 -body G D sig->v-> s1.0 ==> G|-Norm s0.0 -Methd D sig->v-> s1.0

      [| G|-Norm s0.0 -Init D-> s1.0; G|-s1.0 -c-> s2.0;
         s3.0 =
         (if ∃l. fst s2.0 = Some (Jump (Break l)) ∨ fst s2.0 = Some (Jump (Cont l))
          then abupd (%x. Some (Error CrossMethodJump)) s2.0 else s2.0) |]
      ==> G|-Norm s0.0 -Body D
                         c->the (locals (snd s2.0) Result)-> abupd (absorb Ret) s3.0

      G|-Norm s -LVar vn=>(the (locals s vn), %v. supd lupd(vn\<mapsto>v))-> Norm s

      [| G|-Norm s0.0 -Init statDeclC-> s1.0; G|-s1.0 -e->a-> s2.0;
         (v, s2') = fvar statDeclC stat fn a s2.0;
         s3.0 = check_field_access G accC statDeclC fn stat a s2' |]
      ==> G|-Norm s0.0 -{accC,statDeclC,stat}e..fn=>v-> s3.0

      [| G|-Norm s0.0 -e1.0->a-> s1.0; G|-s1.0 -e2.0->i-> s2.0;
         (v, s2') = avar G i a s2.0 |]
      ==> G|-Norm s0.0 -e1.0.[e2.0]=>v-> s2'

      G|-Norm s0.0 -[]#>[]-> Norm s0.0

      [| G|-Norm s0.0 -e->v-> s1.0; G|-s1.0 -es#>vs-> s2.0 |]
      ==> G|-Norm s0.0 -e # es#>v # vs-> s2.0

lemmas eval_Is:

      if inited C (globs s0.0) then s3.0 = Norm s0.0
      else G|-Norm ((init_class_obj G C)
                     s0.0) -(if C = Object then Skip
                             else Init (super (the (class G C))))-> s1.0 ∧
           G|-(set_lvars empty) s1.0 -init (the (class G C))-> s2.0 ∧
           s3.0 = (set_lvars (locals (snd s1.0))) s2.0
      ==> G|-Norm s0.0 -Init C-> s3.0

      G|-s -StatRef rt->(if fst s = None then Null else arbitrary)-> s

      G|-(Some xc, s) -x->arbitrary-> (Some xc, s)

      G|-(Some xc, s) -x=>arbitrary-> (Some xc, s)

      G|-(Some xc, s) -x#>arbitrary-> (Some xc, s)

      G|-(Some xc, s) -x-> (Some xc, s)

      G|-(Some xc, s) -t>-> (arbitrary3 t, Some xc, s)

      G|-Norm s -Skip-> Norm s

      G|-Norm s0.0 -e->v-> s1.0 ==> G|-Norm s0.0 -Expr e-> s1.0

      G|-Norm s0.0 -c-> s1.0 ==> G|-Norm s0.0 -l• c-> abupd (absorb l) s1.0

      [| G|-Norm s0.0 -c1.0-> s1.0; G|-s1.0 -c2.0-> s2.0 |]
      ==> G|-Norm s0.0 -c1.0;; c2.0-> s2.0

      [| G|-Norm s0.0 -e->b-> s1.0;
         G|-s1.0 -(if the_Bool b then c1.0 else c2.0)-> s2.0 |]
      ==> G|-Norm s0.0 -If(e) c1.0 Else c2.0-> s2.0

      [| G|-Norm s0.0 -e->b-> s1.0;
         if the_Bool b
         then G|-s1.0 -c-> s2.0 ∧
              G|-abupd (absorb (Cont l)) s2.0 -l• While(e) c-> s3.0
         else s3.0 = s1.0 |]
      ==> G|-Norm s0.0 -l• While(e) c-> s3.0

      G|-Norm s -Jmp j-> (Some (Jump j), s)

      G|-Norm s0.0 -e->a'-> s1.0 ==> G|-Norm s0.0 -Throw e-> abupd (throw a') s1.0

      [| G|-Norm s0.0 -c1.0-> s1.0; G|-s1.0 -sxalloc-> s2.0;
         if G,s2.0\<turnstile>catch C then G|-new_xcpt_var vn s2.0 -c2.0-> s3.0
         else s3.0 = s2.0 |]
      ==> G|-Norm s0.0 -Try c1.0 Catch(C vn) c2.0-> s3.0

      [| G|-Norm s0.0 -c1.0-> (x1.0, s1.0); G|-Norm s1.0 -c2.0-> s2.0;
         s3.0 =
         (if ∃err. x1.0 = Some (Error err) then (x1.0, s1.0)
          else abupd (abrupt_if (x1.0 ≠ None) x1.0) s2.0) |]
      ==> G|-Norm s0.0 -c1.0 Finally c2.0-> s3.0

      [| the (class G C) = c;
         if inited C (globs s0.0) then s3.0 = Norm s0.0
         else G|-Norm ((init_class_obj G C)
                        s0.0) -(if C = Object then Skip else Init (super c))-> s1.0 ∧
              G|-(set_lvars empty) s1.0 -init c-> s2.0 ∧
              s3.0 = (set_lvars (locals (snd s1.0))) s2.0 |]
      ==> G|-Norm s0.0 -Init C-> s3.0

      [| G|-Norm s0.0 -Init C-> s1.0; G|-s1.0 -halloc CInst C>a-> s2.0 |]
      ==> G|-Norm s0.0 -NewC C->Addr a-> s2.0

      [| G|-Norm s0.0 -init_comp_ty T-> s1.0; G|-s1.0 -e->i'-> s2.0;
         G|-abupd (check_neg i') s2.0 -halloc Arr T (the_Intg i')>a-> s3.0 |]
      ==> G|-Norm s0.0 -New T[e]->Addr a-> s3.0

      [| G|-Norm s0.0 -e->v-> s1.0;
         s2.0 = abupd (raise_if (¬ G,snd s1.0\<turnstile>v fits T) ClassCast) s1.0 |]
      ==> G|-Norm s0.0 -Cast T e->v-> s2.0

      [| G|-Norm s0.0 -e->v-> s1.0;
         b = (v ≠ Null ∧ G,snd s1.0\<turnstile>v fits RefT T) |]
      ==> G|-Norm s0.0 -e InstOf T->Bool b-> s1.0

      G|-Norm s -Lit v->v-> Norm s

      G|-Norm s0.0 -e->v-> s1.0 ==> G|-Norm s0.0 -UnOp unop e->eval_unop unop v-> s1.0

      [| G|-Norm s0.0 -e1.0->v1.0-> s1.0;
         G|-s1.0 -(if need_second_arg binop v1.0 then In1l e2.0
                   else In1r Skip)>-> (In1 v2.0, s2.0) |]
      ==> G|-Norm s0.0 -BinOp binop e1.0 e2.0->eval_binop binop v1.0 v2.0-> s2.0

      G|-Norm s -Super->val_this s-> Norm s

      G|-Norm s0.0 -va=>(v, f)-> s1.0 ==> G|-Norm s0.0 -Acc va->v-> s1.0

      [| G|-Norm s0.0 -va=>(w, f)-> s1.0; G|-s1.0 -e->v-> s2.0 |]
      ==> G|-Norm s0.0 -va:=e->v-> (%(x, s).
                                       (%(x', s'). (x', if x' = None then s' else s))
                                        ((if x = None then f v else id) (x, s)))
                                    s2.0

      [| G|-Norm s0.0 -e0.0->b-> s1.0;
         G|-s1.0 -(if the_Bool b then e1.0 else e2.0)->v-> s2.0 |]
      ==> G|-Norm s0.0 -e0.0 ? e1.0 : e2.0->v-> s2.0

      [| G|-Norm s0.0 -e->a'-> s1.0; G|-s1.0 -args#>vs-> s2.0;
         D = invocation_declclass G mode (snd s2.0) a' statT
              (| name = mn, parTs = pTs |);
         s3.0 = init_lvars G D (| name = mn, parTs = pTs |) mode a' vs s2.0;
         s3' =
         check_method_access G accC statT mode (| name = mn, parTs = pTs |) a' s3.0;
         G|-s3' -Methd D (| name = mn, parTs = pTs |)->v-> s4.0 |]
      ==> G|-Norm s0.0 -{accC,statT,mode}e·mn( {pTs}args)->v-> (set_lvars
                         (locals (snd s2.0)))
                        s4.0

      G|-Norm s0.0 -body G D sig->v-> s1.0 ==> G|-Norm s0.0 -Methd D sig->v-> s1.0

      [| G|-Norm s0.0 -Init D-> s1.0; G|-s1.0 -c-> s2.0;
         s3.0 =
         (if ∃l. fst s2.0 = Some (Jump (Break l)) ∨ fst s2.0 = Some (Jump (Cont l))
          then abupd (%x. Some (Error CrossMethodJump)) s2.0 else s2.0) |]
      ==> G|-Norm s0.0 -Body D
                         c->the (locals (snd s2.0) Result)-> abupd (absorb Ret) s3.0

      G|-Norm s -LVar vn=>(the (locals s vn), %v. supd lupd(vn\<mapsto>v))-> Norm s

      [| G|-Norm s0.0 -Init statDeclC-> s1.0; G|-s1.0 -e->a-> s2.0;
         (v, s2') = fvar statDeclC stat fn a s2.0;
         s3.0 = check_field_access G accC statDeclC fn stat a s2' |]
      ==> G|-Norm s0.0 -{accC,statDeclC,stat}e..fn=>v-> s3.0

      [| G|-Norm s0.0 -e1.0->a-> s1.0; G|-s1.0 -e2.0->i-> s2.0;
         (v, s2') = avar G i a s2.0 |]
      ==> G|-Norm s0.0 -e1.0.[e2.0]=>v-> s2'

      G|-Norm s0.0 -[]#>[]-> Norm s0.0

      [| G|-Norm s0.0 -e->v-> s1.0; G|-s1.0 -es#>vs-> s2.0 |]
      ==> G|-Norm s0.0 -e # es#>v # vs-> s2.0

lemma exec_test:

      [| the (new_Addr
               (heap (st [Inr Ext |-> (| obj.tag = arbitrary, values = empty |),
                          Inr Base |-> (| obj.tag = arbitrary, values = arr_N |),
                          Inr Object |-> (| obj.tag = arbitrary, values = empty |)]
                       empty))) =
         a;
         the (new_Addr
               (heap (st [Inr Ext |-> (| obj.tag = arbitrary, values = empty |),
                          Inr Object |-> (| obj.tag = arbitrary, values = empty |),
                          Inl a |->
                          (| obj.tag = Arr (PrimT Boolean) 2,
                             values = [Inr 0 |-> Bool False, Inr 1 |-> Bool False] |),
                          Inr Base |-> (| obj.tag = arbitrary, values = arr_a |)]
                       empty))) =
         b;
         the (new_Addr
               (heap (st [Inr Ext |-> (| obj.tag = arbitrary, values = empty |),
                          Inr Object |-> (| obj.tag = arbitrary, values = empty |),
                          Inl a |->
                          (| obj.tag = Arr (PrimT Boolean) 2,
                             values = [Inr 0 |-> Bool False, Inr 1 |-> Bool False] |),
                          Inr Base |-> (| obj.tag = arbitrary, values = arr_a |),
                          Inl b |->
                          (| obj.tag = CInst Ext,
                             values =
                               [Inl (vee, Base) |-> Null, Inl (vee, Ext) |->
                                Intg 0] |)]
                       locs3))) =
         c;
         atleast_free (heap s0) four |]
      ==> tprg|-s0' -test [Class
                            Base]-> (Some (Xcpt (Std IndOutBound)),
                                     st [Inr Ext |->
                                         (| obj.tag = arbitrary, values = empty |),
                                         Inr Object |->
                                         (| obj.tag = arbitrary, values = empty |),
                                         Inl a |->
                                         (| obj.tag = Arr (PrimT Boolean) 2,
                                            values =
      [Inr 0 |-> Bool False, Inr 1 |-> Bool False] |),
                                         Inr Base |->
                                         (| obj.tag = arbitrary, values = arr_a |),
                                         Inl b |->
                                         (| obj.tag = CInst Ext,
                                            values =
      [Inl (vee, Base) |-> Null, Inl (vee, Ext) |-> Intg 0] |),
                                         Inl c |->
                                         (| obj.tag = CInst (SXcpt NullPointer),
                                            values = empty |)]
                                      locs8)