# Theory WellType

Up to index of Isabelle/HOL/Bali

theory WellType
imports DeclConcepts
begin

    (*  Title:      HOL/Bali/WellType.thy
        ID:         $Id: WellType.thy,v 1.11 2005/06/17 14:13:06 haftmann Exp $
        Author:     David von Oheimb
    *)
    header {* Well-typedness of Java programs *}

    theory WellType imports DeclConcepts begin

    text {*
    improvements over Java Specification 1.0:
    \begin{itemize}
    \item methods of Object can be called upon references of interface or array type
    \end{itemize}
    simplifications:
    \begin{itemize}
    \item the type rules include all static checks on statements and expressions,
          e.g. definedness of names (of parameters, locals, fields, methods)
    \end{itemize}
    design issues:
    \begin{itemize}
    \item unified type judgment for statements, variables, expressions,
          expression lists
    \item statements are typed like expressions with dummy type Void
    \item the typing rules take an extra argument that is capable of determining
      the dynamic type of objects. Therefore, they can be used for both
      checking static types and determining runtime types in transition semantics.
    \end{itemize}
    *}

    types   lenv
            = "(lname, ty) table"  --{* local variables, including This and Result*}

    record env =
             prg:: "prog"    --{* program *}
             cls:: "qtname"  --{* current package and class name *}
             lcl:: "lenv"    --{* local environment *}

    translations
      "lenv" <= (type) "(lname, ty) table"
      "lenv" <= (type) "lname => ty option"
      "env" <= (type) "(|prg::prog,cls::qtname,lcl::lenv|)),"
      "env" <= (type) "(|prg::prog,cls::qtname,lcl::lenv,…::'a|)),"

    syntax
      pkg :: "env => pname" --{* select the current package from an environment *}
    translations
      "pkg e" == "pid (cls e)"

    section "Static overloading: maximally specific methods "

    types
      emhead = "ref_ty × mhead"

    --{* Some mnemotic selectors for emhead *}
    constdefs
      "declrefT" :: "emhead => ref_ty"
      "declrefT ≡ fst"

      "mhd"     :: "emhead => mhead"
      "mhd ≡ snd"

    lemma declrefT_simp[simp]:"declrefT (r,m) = r"
    by (simp add: declrefT_def)

    lemma mhd_simp[simp]:"mhd (r,m) = m"
    by (simp add: mhd_def)

    lemma static_mhd_simp[simp]: "static (mhd m) = is_static m"
    by (cases m) (simp add: member_is_static_simp mhd_def)

    lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m"
    by (cases m) simp

    lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m"
    by (cases m) simp

    lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
    by (cases m) simp

    consts
      cmheads        :: "prog => qtname => qtname => sig => emhead set"
      Objectmheads   :: "prog => qtname           => sig => emhead set"
      accObjectmheads:: "prog => qtname => ref_ty => sig => emhead set"
      mheads         :: "prog => qtname => ref_ty => sig => emhead set"
    defs
     cmheads_def:
    "cmheads G S C
      ≡ λsig. (λ(Cls,mthd). (ClassT Cls,(mhead mthd))) ` o2s (accmethd G S C sig)"
      Objectmheads_def:
    "Objectmheads G S
      ≡ λsig. (λ(Cls,mthd). (ClassT Cls,(mhead mthd)))
        ` o2s (filter_tab (λsig m. accmodi m ≠ Private) (accmethd G S Object) sig)"
      accObjectmheads_def:
    "accObjectmheads G S T
       ≡ if G\<turnstile>RefT T accessible_in (pid S)
            then Objectmheads G S
            else λsig. {}"
    primrec
    "mheads G S  NullT     = (λsig. {})"
    "mheads G S (IfaceT I) = (λsig. (λ(I,h).(IfaceT I,h))
                             ` accimethds G (pid S) I sig ∪
                               accObjectmheads G S (IfaceT I) sig)"
    "mheads G S (ClassT C) = cmheads G S C"
    "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"

    constdefs
      --{* applicable methods, cf. 15.11.2.1 *}
      appl_methds   :: "prog => qtname =>  ref_ty => sig => (emhead × ty list)   set"
     "appl_methds G S rt ≡ λ sig.
          {(mh,pTs') |mh pTs'. mh ∈ mheads G S rt (|name=name sig,parTs=pTs'|)), ∧
                               G\<turnstile>(parTs sig)[\<preceq>]pTs'}"

      --{* more specific methods, cf. 15.11.2.2 *}
      more_spec     :: "prog => emhead × ty list => emhead × ty list => bool"
     "more_spec G ≡ λ(mh,pTs). λ(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
    (*more_spec G ≡λ((d,h),pTs). λ((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'∧G\<turnstile>pTs[\<preceq>]pTs'*)

      --{* maximally specific methods, cf. 15.11.2.2 *}
       max_spec     :: "prog => qtname => ref_ty => sig => (emhead × ty list)   set"

     "max_spec G S rt sig ≡{m. m ∈appl_methds G S rt sig ∧
                          (∀m'∈appl_methds G S rt sig. more_spec G m' m --> m'=m)}"

    lemma max_spec2appl_meths:
      "x ∈ max_spec G S T sig ==> x ∈ appl_methds G S T sig"
    by (auto simp: max_spec_def)

    lemma appl_methsD: "(mh,pTs')∈appl_methds G S T (|name=mn,parTs=pTs|)), ==>
       mh ∈ mheads G S T (|name=mn,parTs=pTs'|)), ∧ G\<turnstile>pTs[\<preceq>]pTs'"
    by (auto simp: appl_methds_def)

    lemma max_spec2mheads:
    "max_spec G S rt (|name=mn,parTs=pTs|)), = insert (mh, pTs') A
     ==> mh ∈ mheads G S rt (|name=mn,parTs=pTs'|)), ∧ G\<turnstile>pTs[\<preceq>]pTs'"
    apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD)
    done

    constdefs
      empty_dt :: "dyn_ty"
     "empty_dt ≡ λa. None"

      invmode :: "('a::type)member_scheme => expr => inv_mode"
    "invmode m e ≡ if is_static m
                      then Static
                      else if e=Super then SuperM else IntVir"

    lemma invmode_nonstatic [simp]:
      "invmode (|access=a,static=False,…=x|)), (Acc (LVar e)) = IntVir"
    apply (unfold invmode_def)
    apply (simp (no_asm) add: member_is_static_simp)
    done

    lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m"
    apply (unfold invmode_def)
    apply (simp (no_asm))
    done

    lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (¬(is_static m) ∧ e≠Super)"
    apply (unfold invmode_def)
    apply (simp (no_asm))
    done

    lemma Null_staticD:
      "a'=Null --> (is_static m) ==> invmode m e = IntVir --> a' ≠ Null"
    apply (clarsimp simp add: invmode_IntVir_eq)
    done

    section "Typing for unary operations"

    consts unop_type :: "unop => prim_ty"
    primrec
    "unop_type UPlus   = Integer"
    "unop_type UMinus  = Integer"
    "unop_type UBitNot = Integer"
    "unop_type UNot    = Boolean"

    consts wt_unop :: "unop => ty => bool"
    primrec
    "wt_unop UPlus   t = (t = PrimT Integer)"
    "wt_unop UMinus  t = (t = PrimT Integer)"
    "wt_unop UBitNot t = (t = PrimT Integer)"
    "wt_unop UNot    t = (t = PrimT Boolean)"

    section "Typing for binary operations"

    consts binop_type :: "binop => prim_ty"
    primrec
    "binop_type Mul      = Integer"
    "binop_type Div      = Integer"
    "binop_type Mod      = Integer"
    "binop_type Plus     = Integer"
    "binop_type Minus    = Integer"
    "binop_type LShift   = Integer"
    "binop_type RShift   = Integer"
    "binop_type RShiftU  = Integer"
    "binop_type Less     = Boolean"
    "binop_type Le       = Boolean"
    "binop_type Greater  = Boolean"
    "binop_type Ge       = Boolean"
    "binop_type Eq       = Boolean"
    "binop_type Neq      = Boolean"
    "binop_type BitAnd   = Integer"
    "binop_type And      = Boolean"
    "binop_type BitXor   = Integer"
    "binop_type Xor      = Boolean"
    "binop_type BitOr    = Integer"
    "binop_type Or       = Boolean"
    "binop_type CondAnd  = Boolean"
    "binop_type CondOr   = Boolean"

    consts wt_binop :: "prog => binop => ty => ty => bool"
    primrec
    "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 ∨ G\<turnstile>t2\<preceq>t1)"
    "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 ∨ G\<turnstile>t2\<preceq>t1)"
    "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) ∧ (t2 = PrimT Boolean))"
    "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) ∧ (t2 = PrimT Boolean))"
    "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) ∧ (t2 = PrimT Integer))"
    "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) ∧ (t2 = PrimT Boolean))"
    "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) ∧ (t2 = PrimT Boolean))"
    "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) ∧ (t2 = PrimT Boolean))"

    section "Typing for terms"

    types tys  =        "ty + ty list"
    translations
      "tys"   <= (type) "ty + ty list"

    consts
      wt    :: "(env   × dyn_ty   ×  term × tys) set"
    (*wt    :: " env => dyn_ty => (term × tys) set" not feasible because of
                                                      changing env in Try stmt *)

    syntax
    wt      :: "env => dyn_ty => [term,tys]  => bool" ("_,_|=_::_" [51,51,51,51] 50)
    wt_stmt :: "env => dyn_ty =>  stmt       => bool" ("_,_|=_:<>" [51,51,51   ] 50)
    ty_expr :: "env => dyn_ty => [expr ,ty ] => bool" ("_,_|=_:-_" [51,51,51,51] 50)
    ty_var  :: "env => dyn_ty => [var  ,ty ] => bool" ("_,_|=_:=_" [51,51,51,51] 50)
    ty_exprs:: "env => dyn_ty => [expr list,
                                   ty   list] => bool" ("_,_|=_:#_" [51,51,51,51] 50)

    syntax (xsymbols)
    wt      :: "env => dyn_ty => [term,tys] => bool" ("_,_\<Turnstile>_::_"  [51,51,51,51] 50)
    wt_stmt :: "env => dyn_ty =>  stmt       => bool" ("_,_\<Turnstile>_::\<surd>"  [51,51,51   ] 50)
    ty_expr :: "env => dyn_ty => [expr ,ty ] => bool" ("_,_\<Turnstile>_::-_" [51,51,51,51] 50)
    ty_var  :: "env => dyn_ty => [var  ,ty ] => bool" ("_,_\<Turnstile>_::=_" [51,51,51,51] 50)
    ty_exprs:: "env => dyn_ty => [expr list,
                                    ty   list] => bool"("_,_\<Turnstile>_::\<doteq>_" [51,51,51,51] 50)

    translations
            "E,dt\<Turnstile>t::T" == "(E,dt,t,T) ∈ wt"
            "E,dt\<Turnstile>s::\<surd>"  == "E,dt\<Turnstile>In1r s::Inl (PrimT Void)"
            "E,dt\<Turnstile>e::-T" == "E,dt\<Turnstile>In1l e::Inl T"
            "E,dt\<Turnstile>e::=T" == "E,dt\<Turnstile>In2  e::Inl T"
            "E,dt\<Turnstile>e::\<doteq>T" == "E,dt\<Turnstile>In3  e::Inr T"

    syntax (* for purely static typing *)
      wt_      :: "env => [term,tys] => bool" ("_|-_::_" [51,51,51] 50)
      wt_stmt_ :: "env =>  stmt       => bool" ("_|-_:<>" [51,51   ] 50)
      ty_expr_ :: "env => [expr ,ty ] => bool" ("_|-_:-_" [51,51,51] 50)
      ty_var_  :: "env => [var  ,ty ] => bool" ("_|-_:=_" [51,51,51] 50)
      ty_exprs_:: "env => [expr list,
                            ty   list] => bool" ("_|-_:#_" [51,51,51] 50)

    syntax (xsymbols)
      wt_      :: "env => [term,tys] => bool" ("_\<turnstile>_::_"  [51,51,51] 50)
      wt_stmt_ ::  "env =>  stmt       => bool" ("_\<turnstile>_::\<surd>"  [51,51   ] 50)
      ty_expr_ :: "env => [expr ,ty ] => bool" ("_\<turnstile>_::-_" [51,51,51] 50)
      ty_var_  :: "env => [var  ,ty ] => bool" ("_\<turnstile>_::=_" [51,51,51] 50)
      ty_exprs_ :: "env => [expr list,
                            ty   list] => bool" ("_\<turnstile>_::\<doteq>_" [51,51,51] 50)

    translations
            "E\<turnstile>t:: T" == "E,empty_dt\<Turnstile>t:: T"
            "E\<turnstile>s::\<surd>"  == "E\<turnstile>In1r s::Inl (PrimT Void)"
            "E\<turnstile>e::-T" == "E\<turnstile>In1l e::Inl T"
            "E\<turnstile>e::=T" == "E\<turnstile>In2  e::Inl T"
            "E\<turnstile>e::\<doteq>T" == "E\<turnstile>In3  e::Inr T"

    inductive wt intros

    --{* well-typed statements *}

      Skip:                                 "E,dt\<Turnstile>Skip::\<surd>"

      Expr: "[|E,dt\<Turnstile>e::-T|] ==>
                                             E,dt\<Turnstile>Expr e::\<surd>"
      --{* cf. 14.6 *}
      Lab:  "E,dt\<Turnstile>c::\<surd> ==>
                                             E,dt\<Turnstile>l• c::\<surd>"

      Comp: "[|E,dt\<Turnstile>c1::\<surd>;
              E,dt\<Turnstile>c2::\<surd>|] ==>
                                             E,dt\<Turnstile>c1;; c2::\<surd>"

      --{* cf. 14.8 *}
      If:   "[|E,dt\<Turnstile>e::-PrimT Boolean;
              E,dt\<Turnstile>c1::\<surd>;
              E,dt\<Turnstile>c2::\<surd>|] ==>
                                             E,dt\<Turnstile>If(e) c1 Else c2::\<surd>"

      --{* cf. 14.10 *}
      Loop: "[|E,dt\<Turnstile>e::-PrimT Boolean;
              E,dt\<Turnstile>c::\<surd>|] ==>
                                             E,dt\<Turnstile>l• While(e) c::\<surd>"
      --{* cf. 14.13, 14.15, 14.16 *}
      Jmp:                                   "E,dt\<Turnstile>Jmp jump::\<surd>"

      --{* cf. 14.16 *}
      Throw: "[|E,dt\<Turnstile>e::-Class tn;
              prg E\<turnstile>tn\<preceq>C SXcpt Throwable|] ==>
                                             E,dt\<Turnstile>Throw e::\<surd>"
      --{* cf. 14.18 *}
      Try:  "[|E,dt\<Turnstile>c1::\<surd>; prg E\<turnstile>tn\<preceq>C SXcpt Throwable;
              lcl E (VName vn)=None; E (|lcl := lcl E(VName vn\<mapsto>Class tn)|)),,dt\<Turnstile>c2::\<surd>|]
              ==>
                                             E,dt\<Turnstile>Try c1 Catch(tn vn) c2::\<surd>"

      --{* cf. 14.18 *}
      Fin:  "[|E,dt\<Turnstile>c1::\<surd>; E,dt\<Turnstile>c2::\<surd>|] ==>
                                             E,dt\<Turnstile>c1 Finally c2::\<surd>"

      Init: "[|is_class (prg E) C|] ==>
                                             E,dt\<Turnstile>Init C::\<surd>"
      --{* @{term Init} is created on the fly during evaluation (see Eval.thy).
         The class isn't necessarily accessible from the points @{term Init}
         is called. Therefor we only demand @{term is_class} and not
         @{term is_acc_class} here.
       *}

    --{* well-typed expressions *}

      --{* cf. 15.8 *}
      NewC: "[|is_acc_class (prg E) (pkg E) C|] ==>
                                             E,dt\<Turnstile>NewC C::-Class C"
      --{* cf. 15.9 *}
      NewA: "[|is_acc_type (prg E) (pkg E) T;
              E,dt\<Turnstile>i::-PrimT Integer|] ==>
                                             E,dt\<Turnstile>New T[i]::-T.[]"

      --{* cf. 15.15 *}
      Cast: "[|E,dt\<Turnstile>e::-T; is_acc_type (prg E) (pkg E) T';
              prg E\<turnstile>T\<preceq>? T'|] ==>
                                             E,dt\<Turnstile>Cast T' e::-T'"

      --{* cf. 15.19.2 *}
      Inst: "[|E,dt\<Turnstile>e::-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
              prg E\<turnstile>RefT T\<preceq>? RefT T'|] ==>
                                             E,dt\<Turnstile>e InstOf T'::-PrimT Boolean"

      --{* cf. 15.7.1 *}
      Lit:  "[|typeof dt x = Some T|] ==>
                                             E,dt\<Turnstile>Lit x::-T"

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

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

      --{* cf. 15.10.2, 15.11.1 *}
      Super: "[|lcl E This = Some (Class C); C ≠ Object;
              class (prg E) C = Some c|] ==>
                                             E,dt\<Turnstile>Super::-Class (super c)"

      --{* cf. 15.13.1, 15.10.1, 15.12 *}
      Acc:  "[|E,dt\<Turnstile>va::=T|] ==>
                                             E,dt\<Turnstile>Acc va::-T"

      --{* cf. 15.25, 15.25.1 *}
      Ass:  "[|E,dt\<Turnstile>va::=T; va ≠ LVar This;
              E,dt\<Turnstile>v ::-T';
              prg E\<turnstile>T'\<preceq>T|] ==>
                                             E,dt\<Turnstile>va:=v::-T'"

      --{* cf. 15.24 *}
      Cond: "[|E,dt\<Turnstile>e0::-PrimT Boolean;
              E,dt\<Turnstile>e1::-T1; E,dt\<Turnstile>e2::-T2;
              prg E\<turnstile>T1\<preceq>T2 ∧ T = T2  ∨  prg E\<turnstile>T2\<preceq>T1 ∧ T = T1|] ==>
                                             E,dt\<Turnstile>e0 ? e1 : e2::-T"

      --{* cf. 15.11.1, 15.11.2, 15.11.3 *}
      Call: "[|E,dt\<Turnstile>e::-RefT statT;
              E,dt\<Turnstile>ps::\<doteq>pTs;
              max_spec (prg E) (cls E) statT (|name=mn,parTs=pTs|)),
                = {((statDeclT,m),pTs')}
             |] ==>
                       E,dt\<Turnstile>{cls E,statT,invmode m e}e·mn({pTs'}ps)::-(resTy m)"

      Methd: "[|is_class (prg E) C;
              methd (prg E) C sig = Some m;
              E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))::-T|] ==>
                                             E,dt\<Turnstile>Methd C sig::-T"
     --{* The class @{term C} is the dynamic class of the method call
        (cf. Eval.thy).
        It hasn't got to be directly accessible from the current package
        @{term "(pkg E)"}.
        Only the static class must be accessible (enshured indirectly by
        @{term Call}).
        Note that l is just a dummy value. It is only used in the smallstep
        semantics. To proof typesafety directly for the smallstep semantics
        we would have to assume conformance of l here!
      *}

      Body: "[|is_class (prg E) D;
              E,dt\<Turnstile>blk::\<surd>;
              (lcl E) Result = Some T;
              is_type (prg E) T|] ==>
                                             E,dt\<Turnstile>Body D blk::-T"
    --{* The class @{term D} implementing the method must not directly be
         accessible  from the current package @{term "(pkg E)"}, but can also
         be indirectly accessible due to inheritance (enshured in @{term Call})
        The result type hasn't got to be accessible in Java! (If it is not
        accessible you can only assign it to Object).
        For dummy value l see rule @{term Methd}.
       *}

    --{* well-typed variables *}

      --{* cf. 15.13.1 *}
      LVar: "[|lcl E vn = Some T; is_acc_type (prg E) (pkg E) T|] ==>
                                             E,dt\<Turnstile>LVar vn::=T"
      --{* cf. 15.10.1 *}
      FVar: "[|E,dt\<Turnstile>e::-Class C;
              accfield (prg E) (cls E) C fn = Some (statDeclC,f)|] ==>
                             E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn::=(type f)"
      --{* cf. 15.12 *}
      AVar: "[|E,dt\<Turnstile>e::-T.[];
              E,dt\<Turnstile>i::-PrimT Integer|] ==>
                                             E,dt\<Turnstile>e.[i]::=T"

    --{* well-typed expression lists *}

      --{* cf. 15.11.??? *}
      Nil:                                  "E,dt\<Turnstile>[]::\<doteq>[]"

      --{* cf. 15.11.??? *}
      Cons: "[|E,dt\<Turnstile>e ::-T;
              E,dt\<Turnstile>es::\<doteq>Ts|] ==>
                                             E,dt\<Turnstile>e#es::\<doteq>T#Ts"

    declare not_None_eq [simp del]
    declare split_if [split del] split_if_asm [split del]
    declare split_paired_All [simp del] split_paired_Ex [simp del]
    ML_setup {*
    simpset_ref() := simpset() delloop "split_all_tac"
    *}

    inductive_cases wt_elim_cases [cases set]:
            "E,dt\<Turnstile>In2  (LVar vn)               ::T"
            "E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)::T"
            "E,dt\<Turnstile>In2  (e.[i])                 ::T"
            "E,dt\<Turnstile>In1l (NewC C)                ::T"
            "E,dt\<Turnstile>In1l (New T'[i])             ::T"
            "E,dt\<Turnstile>In1l (Cast T' e)             ::T"
            "E,dt\<Turnstile>In1l (e InstOf T')           ::T"
            "E,dt\<Turnstile>In1l (Lit x)                 ::T"
            "E,dt\<Turnstile>In1l (UnOp unop e)           ::T"
            "E,dt\<Turnstile>In1l (BinOp binop e1 e2)     ::T"
            "E,dt\<Turnstile>In1l (Super)                 ::T"
            "E,dt\<Turnstile>In1l (Acc va)                ::T"
            "E,dt\<Turnstile>In1l (Ass va v)              ::T"
            "E,dt\<Turnstile>In1l (e0 ? e1 : e2)          ::T"
            "E,dt\<Turnstile>In1l ({accC,statT,mode}e·mn({pT'}p))::T"
            "E,dt\<Turnstile>In1l (Methd C sig)           ::T"
            "E,dt\<Turnstile>In1l (Body D blk)            ::T"
            "E,dt\<Turnstile>In3  ([])                    ::Ts"
            "E,dt\<Turnstile>In3  (e#es)                  ::Ts"
            "E,dt\<Turnstile>In1r  Skip                   ::x"
            "E,dt\<Turnstile>In1r (Expr e)                ::x"
            "E,dt\<Turnstile>In1r (c1;; c2)               ::x"
            "E,dt\<Turnstile>In1r (l• c)                  ::x"
            "E,dt\<Turnstile>In1r (If(e) c1 Else c2)      ::x"
            "E,dt\<Turnstile>In1r (l• While(e) c)         ::x"
            "E,dt\<Turnstile>In1r (Jmp jump)              ::x"
            "E,dt\<Turnstile>In1r (Throw e)               ::x"
            "E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)::x"
            "E,dt\<Turnstile>In1r (c1 Finally c2)         ::x"
            "E,dt\<Turnstile>In1r (Init C)                ::x"
    declare not_None_eq [simp]
    declare split_if [split] split_if_asm [split]
    declare split_paired_All [simp] split_paired_Ex [simp]
    ML_setup {*
    simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    *}

    lemma is_acc_class_is_accessible:
      "is_acc_class G P C ==> G\<turnstile>(Class C) accessible_in P"
    by (auto simp add: is_acc_class_def)

    lemma is_acc_iface_is_iface: "is_acc_iface G P I ==> is_iface G I"
    by (auto simp add: is_acc_iface_def)

    lemma is_acc_iface_Iface_is_accessible:
      "is_acc_iface G P I ==> G\<turnstile>(Iface I) accessible_in P"
    by (auto simp add: is_acc_iface_def)

    lemma is_acc_type_is_type: "is_acc_type G P T ==> is_type G T"
    by (auto simp add: is_acc_type_def)

    lemma is_acc_iface_is_accessible:
      "is_acc_type G P T ==> G\<turnstile>T accessible_in P"
    by (auto simp add: is_acc_type_def)

    lemma wt_Methd_is_methd:
      "E\<turnstile>In1l (Methd C sig)::T ==> is_methd (prg E) C sig"
    apply (erule_tac wt_elim_cases)
    apply clarsimp
    apply (erule is_methdI, assumption)
    done

    text {* Special versions of some typing rules, better suited to pattern
            match the conclusion (no selectors in the conclusion)
    *}

    lemma wt_Call:
    "[|E,dt\<Turnstile>e::-RefT statT; E,dt\<Turnstile>ps::\<doteq>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\<Turnstile>{accC,statT,mode}e·mn({pTs'}ps)::-rT"
    by (auto elim: wt.Call)

    lemma invocationTypeExpr_noClassD:
    "[| E\<turnstile>e::-RefT statT|]
     ==> (∀ statC. statT ≠ ClassT statC) --> invmode m e ≠ SuperM"
    proof -
      assume wt: "E\<turnstile>e::-RefT statT"
      show ?thesis
      proof (cases "e=Super")
        case True
        with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
        then show ?thesis by blast
      next
        case False then show ?thesis
          by (auto simp add: invmode_def split: split_if_asm)
      qed
    qed

    lemma wt_Super:
    "[|lcl E This = Some (Class C); C ≠ Object; class (prg E) C = Some c; D=super c|]
    ==> E,dt\<Turnstile>Super::-Class D"
    by (auto elim: wt.Super)

    lemma wt_FVar:
    "[|E,dt\<Turnstile>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\<Turnstile>{accC,statDeclC,sf}e..fn::=fT"
    by (auto dest: wt.FVar)

    lemma wt_init [iff]: "E,dt\<Turnstile>Init C::\<surd> = is_class (prg E) C"
    by (auto elim: wt_elim_cases intro: "wt.Init")

    declare wt.Skip [iff]

    lemma wt_StatRef:
      "is_acc_type (prg E) (pkg E) (RefT rt) ==> E\<turnstile>StatRef rt::-RefT rt"
    apply (rule wt.Cast)
    apply  (rule wt.Lit)
    apply   (simp (no_asm))
    apply  (simp (no_asm_simp))
    apply (rule cast.widen)
    apply (simp (no_asm))
    done

    lemma wt_Inj_elim:
      "!!E. E,dt\<Turnstile>t::U ==> case t of
                           In1 ec => (case ec of
                                        Inl e => ∃T. U=Inl T
                                      | Inr s => U=Inl (PrimT Void))
                         | In2 e => (∃T. U=Inl T)
                         | In3 e => (∃T. U=Inr T)"
    apply (erule wt.induct)
    apply auto
    done

    --{* In the special syntax to distinguish the typing judgements for expressions,
         statements, variables and expression lists the kind of term corresponds
         to the kind of type in the end e.g. An statement (injection @{term In3}
        into terms, always has type void (injection @{term Inl} into the generalised
        types. The following simplification procedures establish these kinds of
        correlation.
     *}

    ML {*
    fun wt_fun name inj rhs =
    let
      val lhs = "E,dt\<Turnstile>" ^ inj ^ " t::U"
      val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")")
            (K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac])
      fun is_Inj (Const (inj,_) $ _) = true
        | is_Inj _                   = false
      fun pred (t as (_ $ (Const ("Pair",_) $
         _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
           x))) $ _ )) = is_Inj x
    in
      cond_simproc name lhs pred (thm name)
    end

    val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "∃T.  U=Inl T  ∧ E,dt\<Turnstile>t::-T"
    val wt_var_proc   = wt_fun "wt_var_eq"   "In2"  "∃T.  U=Inl T  ∧ E,dt\<Turnstile>t::=T"
    val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3"  "∃Ts. U=Inr Ts ∧ E,dt\<Turnstile>t::\<doteq>Ts"
    val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "In1r" "U=Inl(PrimT Void)∧E,dt\<Turnstile>t::\<surd>"
    *}

    ML {*
    Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
    *}

    lemma wt_elim_BinOp:
      "[|E,dt\<Turnstile>In1l (BinOp binop e1 e2)::T;
        !!T1 T2 T3.
           [|E,dt\<Turnstile>e1::-T1; E,dt\<Turnstile>e2::-T2; wt_binop (prg E) binop T1 T2;
              E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)::T3;
              T = Inl (PrimT (binop_type binop))|]
           ==> P|]
    ==> P"
    apply (erule wt_elim_cases)
    apply (cases b)
    apply auto
    done

    lemma Inj_eq_lemma [simp]:
      "(∀T. (∃T'. T = Inj T' ∧ P T') --> Q T) = (∀T'. P T' --> Q (Inj T'))"
    by auto

    (* unused *)
    lemma single_valued_tys_lemma [rule_format (no_asm)]:
      "∀S T. G\<turnstile>S\<preceq>T --> G\<turnstile>T\<preceq>S --> S = T ==> E,dt\<Turnstile>t::T ==>
         G = prg E --> (∀T'. E,dt\<Turnstile>t::T' --> T  = T')"
    apply (cases "E", erule wt.induct)
    apply (safe del: disjE)
    apply (simp_all (no_asm_use) split del: split_if_asm)
    apply (safe del: disjE)
    (* 17 subgoals *)
    apply (tactic {* ALLGOALS (fn i => if i = 11 then EVERY'[thin_tac "?E,dt\<Turnstile>e0::-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1::-?T1", thin_tac "?E,dt\<Turnstile>e2::-?T2"] i else thin_tac "All ?P" i) *})
    (*apply (safe del: disjE elim!: wt_elim_cases)*)
    apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
    apply (simp_all (no_asm_use) split del: split_if_asm)
    apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
    apply ((blast del: equalityCE dest: sym [THEN trans])+)
    done

    (* unused *)
    lemma single_valued_tys:
    "ws_prog (prg E) ==> single_valued {(t,T). E,dt\<Turnstile>t::T}"
    apply (unfold single_valued_def)
    apply clarsimp
    apply (rule single_valued_tys_lemma)
    apply (auto intro!: widen_antisym)
    done

    lemma typeof_empty_is_type [rule_format (no_asm)]:
      "typeof (λa. None) v = Some T --> is_type G T"
    apply (rule val.induct)
    apply           auto
    done

    (* unused *)
    lemma typeof_is_type [rule_format (no_asm)]:
     "(∀a. v ≠ Addr a) --> (∃T. typeof dt v = Some T ∧ is_type G T)"
    apply (rule val.induct)
    prefer 5
    apply     fast
    apply  (simp_all (no_asm))
    done

    end

## Static overloading: maximally specific methods

lemma declrefT_simp:

      declrefT (r, m) = r

lemma mhd_simp:

      mhd (r, m) = m

lemma static_mhd_simp:

      static (mhd m) = is_static m

lemma mhd_resTy_simp:

      resTy (mhd m) = resTy m

lemma mhd_is_static_simp:

      is_static (mhd m) = is_static m

lemma mhd_accmodi_simp:

      accmodi (mhd m) = accmodi m

lemma max_spec2appl_meths:

      x ∈ max_spec G S T sig ==> x ∈ appl_methds G S T sig

lemma appl_methsD:

      (mh, pTs') ∈ appl_methds G S T (| name = mn, parTs = pTs |)
      ==> mh ∈ mheads G S T (| name = mn, parTs = pTs' |) ∧
          G\<turnstile>pTs[\<preceq>]pTs'

lemma max_spec2mheads:

      max_spec G S rt (| name = mn, parTs = pTs |) = insert (mh, pTs') A
      ==> mh ∈ mheads G S rt (| name = mn, parTs = pTs' |) ∧
          G\<turnstile>pTs[\<preceq>]pTs'

lemma invmode_nonstatic:

      invmode (| access = a, static = False, ... = x |) (Acc (LVar e)) = IntVir

lemma invmode_Static_eq:

      (invmode m e = Static) = is_static m

lemma invmode_IntVir_eq:

      (invmode m e = IntVir) = (¬ is_static m ∧ e ≠ Super)

lemma Null_staticD:

      a' = Null --> is_static m ==> invmode m e = IntVir --> a' ≠ Null

## Typing for unary operations

## Typing for binary operations

## Typing for terms

lemmas wt_elim_cases:

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

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

      [| E,dt|=In2 (e.[i])::T;
         !!T. [| E,dt|=e:-T.[]; E,dt|=i:-PrimT Integer; T = Inl T |] ==> P |]
      ==> P

      [| E,dt|=In1l (NewC C)::T;
         [| is_acc_class (prg E) (pkg E) C; T = Inl (Class C) |] ==> P |]
      ==> P

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

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

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

      [| E,dt|=In1l (Lit x)::T; !!T. [| typeof dt x = Some T; T = Inl T |] ==> P |]
      ==> P

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

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

      [| E,dt|=In1l Super::T;
         !!C c. [| lcl E This = Some (Class C); C ≠ Object; class (prg E) C = Some c;
                   T = Inl (Class (super c)) |]
                ==> P |]
      ==> P

      [| E,dt|=In1l (Acc va)::T; !!T. [| E,dt|=va:=T; T = Inl T |] ==> P |] ==> P

      [| E,dt|=In1l (va:=v)::T;
         !!T T'.
            [| E,dt|=va:=T; va ≠ LVar This; E,dt|=v:-T'; prg E|-T'<=:T; T = Inl T' |]
            ==> P |]
      ==> P

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

      [| E,dt|=In1l ({accC,statT,mode}e·mn( {pT'}p))::T;
         !!m pTs statDeclT.
            [| E,dt|=e:-RefT statT; E,dt|=p:#pTs;
               max_spec (prg E) (cls E) statT (| name = mn, parTs = pTs |) =
               {((statDeclT, m), pT')};
               T = Inl (resTy m); accC = cls E; mode = invmode m e |]
            ==> P |]
      ==> P

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

      [| E,dt|=In1l (Body D blk)::T;
         !!T. [| is_class (prg E) D; E,dt|=blk:<>; lcl E Result = Some T;
                 is_type (prg E) T; T = Inl T |]
              ==> P |]
      ==> P

      [| E,dt|=In3 []::Ts; Ts = Inr [] ==> P |] ==> P

      [| E,dt|=In3 (e # es)::Ts;
         !!T Ts. [| E,dt|=e:-T; E,dt|=es:#Ts; Ts = Inr (T # Ts) |] ==> P |]
      ==> P

      [| E,dt|=In1r Skip::x; x = Inl (PrimT Void) ==> P |] ==> P

      [| E,dt|=In1r (Expr e)::x; !!T. [| E,dt|=e:-T; x = Inl (PrimT Void) |] ==> P |]
      ==> P

      [| E,dt|=In1r (c1.0;; c2.0)::x;
         [| E,dt|=c1.0:<>; E,dt|=c2.0:<>; x = Inl (PrimT Void) |] ==> P |]
      ==> P

      [| E,dt|=In1r (l• c)::x; [| E,dt|=c:<>; x = Inl (PrimT Void) |] ==> P |] ==> P

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

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

      [| E,dt|=In1r (Jmp jump)::x; x = Inl (PrimT Void) ==> P |] ==> P

      [| E,dt|=In1r (Throw e)::x;
         !!tn. [| E,dt|=e:-Class tn; prg E|-tn<=:C SXcpt Throwable;
                  x = Inl (PrimT Void) |]
               ==> P |]
      ==> P

      [| E,dt|=In1r (Try c1.0 Catch(tn vn) c2.0)::x;
         [| 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:<>;
            x = Inl (PrimT Void) |]
         ==> P |]
      ==> P

      [| E,dt|=In1r (c1.0 Finally c2.0)::x;
         [| E,dt|=c1.0:<>; E,dt|=c2.0:<>; x = Inl (PrimT Void) |] ==> P |]
      ==> P

      [| E,dt|=In1r (Init C)::x;
         [| is_class (prg E) C; x = Inl (PrimT Void) |] ==> P |]
      ==> P

lemma is_acc_class_is_accessible:

      is_acc_class G P C ==> G \<turnstile> Class C accessible_in P

lemma is_acc_iface_is_iface:

      is_acc_iface G P I ==> is_iface G I

lemma is_acc_iface_Iface_is_accessible:

      is_acc_iface G P I ==> G \<turnstile> Iface I accessible_in P

lemma is_acc_type_is_type:

      is_acc_type G P T ==> is_type G T

lemma is_acc_iface_is_accessible:

      is_acc_type G P T ==> G \<turnstile> T accessible_in P

lemma wt_Methd_is_methd:

      E|-In1l (Methd C sig)::T ==> is_methd (prg E) C sig

lemma wt_Call:

      [| 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

lemma invocationTypeExpr_noClassD:

      E|-e:-RefT statT ==> (∀statC. statT ≠ ClassT statC) --> invmode m e ≠ SuperM

lemma wt_Super:

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

lemma wt_FVar:

      [| 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

lemma wt_init:

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

lemma wt_StatRef:

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

lemma wt_Inj_elim:

      E,dt|=t::U
      ==> case t of
          In1 ec => case ec of Inl e => ∃T. U = Inl T | Inr s => U = Inl (PrimT Void)
          | In2 e => ∃T. U = Inl T | In3 e => ∃T. U = Inr T

theorem wt_expr_eq:

      (E,dt|=In1l t::U) = (∃T. U = Inl T ∧ E,dt|=t:-T)

theorem wt_var_eq:

      (E,dt|=In2 t::U) = (∃T. U = Inl T ∧ E,dt|=t:=T)

theorem wt_exprs_eq:

      (E,dt|=In3 t::U) = (∃Ts. U = Inr Ts ∧ E,dt|=t:#Ts)

theorem wt_stmt_eq:

      (E,dt|=In1r t::U) = (U = Inl (PrimT Void) ∧ E,dt|=t:<>)

lemma wt_elim_BinOp:

      [| E,dt|=In1l (BinOp binop e1.0 e2.0)::T;
         !!T1 T2 T3.
            [| E,dt|=e1.0:-T1; E,dt|=e2.0:-T2; wt_binop (prg E) binop T1 T2;
               E,dt|=(if b then In1l e2.0 else In1r Skip)::T3;
               T = Inl (PrimT (binop_type binop)) |]
            ==> P |]
      ==> P

lemma Inj_eq_lemma:

      (∀T. (∃T'. T = Inj T' ∧ P T') --> Q T) = (∀T'. P T' --> Q (Inj T'))

lemma single_valued_tys_lemma:

      [| ∀S T. G|-S<=:T --> G|-T<=:S --> S = T; E,dt|=t::T; G = prg E; E,dt|=t::T' |]
      ==> T = T'

lemma single_valued_tys:

      ws_prog (prg E) ==> single_valued {(t, T). E,dt|=t::T}

lemma typeof_empty_is_type:

      typeof empty v = Some T ==> is_type G T

lemma typeof_is_type:

      ∀a. v ≠ Addr a ==> ∃T. typeof dt v = Some T ∧ is_type G T