src/HOL/Bali/WellType.thy
author haftmann
Fri Jun 11 17:14:01 2010 +0200 (2010-06-11)
changeset 37406 982f3e02f3c4
parent 36367 49c7dee21a7f
child 37956 ee939247b2fb
permissions -rw-r--r--
modernized specifications
     1 (*  Title:      HOL/Bali/WellType.thy
     2     Author:     David von Oheimb
     3 *)
     4 header {* Well-typedness of Java programs *}
     5 
     6 theory WellType
     7 imports DeclConcepts
     8 begin
     9 
    10 text {*
    11 improvements over Java Specification 1.0:
    12 \begin{itemize}
    13 \item methods of Object can be called upon references of interface or array type
    14 \end{itemize}
    15 simplifications:
    16 \begin{itemize}
    17 \item the type rules include all static checks on statements and expressions, 
    18       e.g. definedness of names (of parameters, locals, fields, methods)
    19 \end{itemize}
    20 design issues:
    21 \begin{itemize}
    22 \item unified type judgment for statements, variables, expressions, 
    23       expression lists
    24 \item statements are typed like expressions with dummy type Void
    25 \item the typing rules take an extra argument that is capable of determining 
    26   the dynamic type of objects. Therefore, they can be used for both 
    27   checking static types and determining runtime types in transition semantics.
    28 \end{itemize}
    29 *}
    30 
    31 types lenv
    32         = "(lname, ty) table"  --{* local variables, including This and Result*}
    33 
    34 record env = 
    35          prg:: "prog"    --{* program *}
    36          cls:: "qtname"  --{* current package and class name *}
    37          lcl:: "lenv"    --{* local environment *}     
    38   
    39 translations
    40   (type) "lenv" <= (type) "(lname, ty) table"
    41   (type) "lenv" <= (type) "lname \<Rightarrow> ty option"
    42   (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
    43   (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
    44 
    45 
    46 abbreviation
    47   pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
    48   where "pkg e == pid (cls e)"
    49 
    50 section "Static overloading: maximally specific methods "
    51 
    52 types
    53   emhead = "ref_ty \<times> mhead"
    54 
    55 --{* Some mnemotic selectors for emhead *}
    56 definition "declrefT" :: "emhead \<Rightarrow> ref_ty" where
    57   "declrefT \<equiv> fst"
    58 
    59 definition "mhd"     :: "emhead \<Rightarrow> mhead" where
    60   "mhd \<equiv> snd"
    61 
    62 lemma declrefT_simp[simp]:"declrefT (r,m) = r"
    63 by (simp add: declrefT_def)
    64 
    65 lemma mhd_simp[simp]:"mhd (r,m) = m"
    66 by (simp add: mhd_def)
    67 
    68 lemma static_mhd_simp[simp]: "static (mhd m) = is_static m"
    69 by (cases m) (simp add: member_is_static_simp mhd_def)
    70 
    71 lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m"
    72 by (cases m) simp
    73 
    74 lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m"
    75 by (cases m) simp
    76 
    77 lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
    78 by (cases m) simp
    79 
    80 consts
    81   cmheads        :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
    82   Objectmheads   :: "prog \<Rightarrow> qtname           \<Rightarrow> sig \<Rightarrow> emhead set"
    83   accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
    84   mheads         :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
    85 defs
    86  cmheads_def:
    87 "cmheads G S C 
    88   \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig)"
    89   Objectmheads_def:
    90 "Objectmheads G S  
    91   \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
    92     ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
    93   accObjectmheads_def:
    94 "accObjectmheads G S T
    95    \<equiv> if G\<turnstile>RefT T accessible_in (pid S)
    96         then Objectmheads G S
    97         else (\<lambda>sig. {})"
    98 primrec
    99 "mheads G S  NullT     = (\<lambda>sig. {})"
   100 "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
   101                          ` accimethds G (pid S) I sig \<union> 
   102                            accObjectmheads G S (IfaceT I) sig)"
   103 "mheads G S (ClassT C) = cmheads G S C"
   104 "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
   105 
   106 definition
   107   --{* applicable methods, cf. 15.11.2.1 *}
   108   appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
   109  "appl_methds G S rt = (\<lambda> sig. 
   110       {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
   111                            G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
   112 
   113 definition
   114   --{* more specific methods, cf. 15.11.2.2 *}
   115   more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
   116  "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
   117 (*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
   118 
   119 definition
   120   --{* maximally specific methods, cf. 15.11.2.2 *}
   121    max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
   122  "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
   123                       (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
   124 
   125 
   126 lemma max_spec2appl_meths: 
   127   "x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" 
   128 by (auto simp: max_spec_def)
   129 
   130 lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow>  
   131    mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   132 by (auto simp: appl_methds_def)
   133 
   134 lemma max_spec2mheads: 
   135 "max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A 
   136  \<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   137 apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD)
   138 done
   139 
   140 
   141 definition empty_dt :: "dyn_ty" where
   142  "empty_dt \<equiv> \<lambda>a. None"
   143 
   144 definition invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
   145 "invmode m e \<equiv> if is_static m 
   146                   then Static 
   147                   else if e=Super then SuperM else IntVir"
   148 
   149 lemma invmode_nonstatic [simp]: 
   150   "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
   151 apply (unfold invmode_def)
   152 apply (simp (no_asm) add: member_is_static_simp)
   153 done
   154 
   155 
   156 lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m"
   157 apply (unfold invmode_def)
   158 apply (simp (no_asm))
   159 done
   160 
   161 
   162 lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)"
   163 apply (unfold invmode_def)
   164 apply (simp (no_asm))
   165 done
   166 
   167 lemma Null_staticD: 
   168   "a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
   169 apply (clarsimp simp add: invmode_IntVir_eq)
   170 done
   171 
   172 section "Typing for unary operations"
   173 
   174 consts unop_type :: "unop \<Rightarrow> prim_ty"
   175 primrec 
   176 "unop_type UPlus   = Integer"
   177 "unop_type UMinus  = Integer"
   178 "unop_type UBitNot = Integer"
   179 "unop_type UNot    = Boolean"    
   180 
   181 consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
   182 primrec
   183 "wt_unop UPlus   t = (t = PrimT Integer)"
   184 "wt_unop UMinus  t = (t = PrimT Integer)"
   185 "wt_unop UBitNot t = (t = PrimT Integer)"
   186 "wt_unop UNot    t = (t = PrimT Boolean)"
   187 
   188 section "Typing for binary operations"
   189 
   190 consts binop_type :: "binop \<Rightarrow> prim_ty"
   191 primrec
   192 "binop_type Mul      = Integer"     
   193 "binop_type Div      = Integer"
   194 "binop_type Mod      = Integer"
   195 "binop_type Plus     = Integer"
   196 "binop_type Minus    = Integer"
   197 "binop_type LShift   = Integer"
   198 "binop_type RShift   = Integer"
   199 "binop_type RShiftU  = Integer"
   200 "binop_type Less     = Boolean"
   201 "binop_type Le       = Boolean"
   202 "binop_type Greater  = Boolean"
   203 "binop_type Ge       = Boolean"
   204 "binop_type Eq       = Boolean"
   205 "binop_type Neq      = Boolean"
   206 "binop_type BitAnd   = Integer"
   207 "binop_type And      = Boolean"
   208 "binop_type BitXor   = Integer"
   209 "binop_type Xor      = Boolean"
   210 "binop_type BitOr    = Integer"
   211 "binop_type Or       = Boolean"
   212 "binop_type CondAnd  = Boolean"
   213 "binop_type CondOr   = Boolean"
   214 
   215 consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
   216 primrec
   217 "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   218 "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   219 "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   220 "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   221 "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   222 "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   223 "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   224 "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   225 "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   226 "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   227 "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   228 "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   229 "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
   230 "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
   231 "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   232 "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   233 "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   234 "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   235 "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   236 "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   237 "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   238 "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   239 
   240 section "Typing for terms"
   241 
   242 types tys  = "ty + ty list"
   243 translations
   244   (type) "tys" <= (type) "ty + ty list"
   245 
   246 
   247 inductive
   248   wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
   249   and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
   250   and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
   251   and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
   252   and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty   list] \<Rightarrow> bool"
   253     ("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
   254 where
   255 
   256   "E,dt\<Turnstile>s\<Colon>\<surd> \<equiv> E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
   257 | "E,dt\<Turnstile>e\<Colon>-T \<equiv> E,dt\<Turnstile>In1l e\<Colon>Inl T"
   258 | "E,dt\<Turnstile>e\<Colon>=T \<equiv> E,dt\<Turnstile>In2  e\<Colon>Inl T"
   259 | "E,dt\<Turnstile>e\<Colon>\<doteq>T \<equiv> E,dt\<Turnstile>In3  e\<Colon>Inr T"
   260 
   261 --{* well-typed statements *}
   262 
   263 | Skip:                                 "E,dt\<Turnstile>Skip\<Colon>\<surd>"
   264 
   265 | Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
   266                                          E,dt\<Turnstile>Expr e\<Colon>\<surd>"
   267   --{* cf. 14.6 *}
   268 | Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
   269                                          E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
   270 
   271 | Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
   272           E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   273                                          E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
   274 
   275   --{* cf. 14.8 *}
   276 | If:   "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   277           E,dt\<Turnstile>c1\<Colon>\<surd>;
   278           E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   279                                          E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
   280 
   281   --{* cf. 14.10 *}
   282 | Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   283           E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   284                                          E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
   285   --{* cf. 14.13, 14.15, 14.16 *}
   286 | Jmp:                                   "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>"
   287 
   288   --{* cf. 14.16 *}
   289 | Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
   290           prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
   291                                          E,dt\<Turnstile>Throw e\<Colon>\<surd>"
   292   --{* cf. 14.18 *}
   293 | Try:  "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
   294           lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
   295           \<Longrightarrow>
   296                                          E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
   297 
   298   --{* cf. 14.18 *}
   299 | Fin:  "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   300                                          E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
   301 
   302 | Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
   303                                          E,dt\<Turnstile>Init C\<Colon>\<surd>"
   304   --{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
   305      The class isn't necessarily accessible from the points @{term Init} 
   306      is called. Therefor we only demand @{term is_class} and not 
   307      @{term is_acc_class} here. 
   308    *}
   309 
   310 --{* well-typed expressions *}
   311 
   312   --{* cf. 15.8 *}
   313 | NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
   314                                          E,dt\<Turnstile>NewC C\<Colon>-Class C"
   315   --{* cf. 15.9 *}
   316 | NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T;
   317           E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   318                                          E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
   319 
   320   --{* cf. 15.15 *}
   321 | Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
   322           prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
   323                                          E,dt\<Turnstile>Cast T' e\<Colon>-T'"
   324 
   325   --{* cf. 15.19.2 *}
   326 | Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
   327           prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
   328                                          E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
   329 
   330   --{* cf. 15.7.1 *}
   331 | Lit:  "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
   332                                          E,dt\<Turnstile>Lit x\<Colon>-T"
   333 
   334 | UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
   335           \<Longrightarrow>
   336           E,dt\<Turnstile>UnOp unop e\<Colon>-T"
   337   
   338 | BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
   339            T=PrimT (binop_type binop)\<rbrakk> 
   340            \<Longrightarrow>
   341            E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
   342   
   343   --{* cf. 15.10.2, 15.11.1 *}
   344 | Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   345           class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
   346                                          E,dt\<Turnstile>Super\<Colon>-Class (super c)"
   347 
   348   --{* cf. 15.13.1, 15.10.1, 15.12 *}
   349 | Acc:  "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
   350                                          E,dt\<Turnstile>Acc va\<Colon>-T"
   351 
   352   --{* cf. 15.25, 15.25.1 *}
   353 | Ass:  "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
   354           E,dt\<Turnstile>v \<Colon>-T';
   355           prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
   356                                          E,dt\<Turnstile>va:=v\<Colon>-T'"
   357 
   358   --{* cf. 15.24 *}
   359 | Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
   360           E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
   361           prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
   362                                          E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
   363 
   364   --{* cf. 15.11.1, 15.11.2, 15.11.3 *}
   365 | Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
   366           E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
   367           max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   368             = {((statDeclT,m),pTs')}
   369          \<rbrakk> \<Longrightarrow>
   370                    E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
   371 
   372 | Methd: "\<lbrakk>is_class (prg E) C;
   373           methd (prg E) C sig = Some m;
   374           E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
   375                                          E,dt\<Turnstile>Methd C sig\<Colon>-T"
   376  --{* The class @{term C} is the dynamic class of the method call 
   377     (cf. Eval.thy). 
   378     It hasn't got to be directly accessible from the current package 
   379     @{term "(pkg E)"}. 
   380     Only the static class must be accessible (enshured indirectly by 
   381     @{term Call}). 
   382     Note that l is just a dummy value. It is only used in the smallstep 
   383     semantics. To proof typesafety directly for the smallstep semantics 
   384     we would have to assume conformance of l here!
   385   *}
   386 
   387 | Body: "\<lbrakk>is_class (prg E) D;
   388           E,dt\<Turnstile>blk\<Colon>\<surd>;
   389           (lcl E) Result = Some T;
   390           is_type (prg E) T\<rbrakk> \<Longrightarrow>
   391                                          E,dt\<Turnstile>Body D blk\<Colon>-T"
   392 --{* The class @{term D} implementing the method must not directly be 
   393      accessible  from the current package @{term "(pkg E)"}, but can also 
   394      be indirectly accessible due to inheritance (enshured in @{term Call})
   395     The result type hasn't got to be accessible in Java! (If it is not 
   396     accessible you can only assign it to Object).
   397     For dummy value l see rule @{term Methd}. 
   398    *}
   399 
   400 --{* well-typed variables *}
   401 
   402   --{* cf. 15.13.1 *}
   403 | LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
   404                                          E,dt\<Turnstile>LVar vn\<Colon>=T"
   405   --{* cf. 15.10.1 *}
   406 | FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
   407           accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
   408                          E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
   409   --{* cf. 15.12 *}
   410 | AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
   411           E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   412                                          E,dt\<Turnstile>e.[i]\<Colon>=T"
   413 
   414 
   415 --{* well-typed expression lists *}
   416 
   417   --{* cf. 15.11.??? *}
   418 | Nil:                                  "E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
   419 
   420   --{* cf. 15.11.??? *}
   421 | Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
   422           E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
   423                                          E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
   424 
   425 
   426 (* for purely static typing *)
   427 abbreviation
   428   wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
   429   where "E|-t::T == E,empty_dt\<Turnstile>t\<Colon> T"
   430 
   431 abbreviation
   432   wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
   433   where "E|-s:<> == E|-In1r s :: Inl (PrimT Void)"
   434 
   435 abbreviation
   436   ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
   437   where "E|-e:-T == E|-In1l e :: Inl T"
   438 
   439 abbreviation
   440   ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
   441   where "E|-e:=T == E|-In2 e :: Inl T"
   442 
   443 abbreviation
   444   ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
   445   where "E|-e:#T == E|-In3 e :: Inr T"
   446 
   447 notation (xsymbols)
   448   wt_syntax  ("_\<turnstile>_\<Colon>_"  [51,51,51] 50) and
   449   wt_stmt_syntax  ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50) and
   450   ty_expr_syntax  ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) and
   451   ty_var_syntax  ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) and
   452   ty_exprs_syntax  ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
   453 
   454 declare not_None_eq [simp del] 
   455 declare split_if [split del] split_if_asm [split del]
   456 declare split_paired_All [simp del] split_paired_Ex [simp del]
   457 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
   458 
   459 inductive_cases wt_elim_cases [cases set]:
   460         "E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
   461         "E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
   462         "E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
   463         "E,dt\<Turnstile>In1l (NewC C)                \<Colon>T"
   464         "E,dt\<Turnstile>In1l (New T'[i])             \<Colon>T"
   465         "E,dt\<Turnstile>In1l (Cast T' e)             \<Colon>T"
   466         "E,dt\<Turnstile>In1l (e InstOf T')           \<Colon>T"
   467         "E,dt\<Turnstile>In1l (Lit x)                 \<Colon>T"
   468         "E,dt\<Turnstile>In1l (UnOp unop e)           \<Colon>T"
   469         "E,dt\<Turnstile>In1l (BinOp binop e1 e2)     \<Colon>T"
   470         "E,dt\<Turnstile>In1l (Super)                 \<Colon>T"
   471         "E,dt\<Turnstile>In1l (Acc va)                \<Colon>T"
   472         "E,dt\<Turnstile>In1l (Ass va v)              \<Colon>T"
   473         "E,dt\<Turnstile>In1l (e0 ? e1 : e2)          \<Colon>T"
   474         "E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
   475         "E,dt\<Turnstile>In1l (Methd C sig)           \<Colon>T"
   476         "E,dt\<Turnstile>In1l (Body D blk)            \<Colon>T"
   477         "E,dt\<Turnstile>In3  ([])                    \<Colon>Ts"
   478         "E,dt\<Turnstile>In3  (e#es)                  \<Colon>Ts"
   479         "E,dt\<Turnstile>In1r  Skip                   \<Colon>x"
   480         "E,dt\<Turnstile>In1r (Expr e)                \<Colon>x"
   481         "E,dt\<Turnstile>In1r (c1;; c2)               \<Colon>x"
   482         "E,dt\<Turnstile>In1r (l\<bullet> c)                  \<Colon>x" 
   483         "E,dt\<Turnstile>In1r (If(e) c1 Else c2)      \<Colon>x"
   484         "E,dt\<Turnstile>In1r (l\<bullet> While(e) c)         \<Colon>x"
   485         "E,dt\<Turnstile>In1r (Jmp jump)              \<Colon>x"
   486         "E,dt\<Turnstile>In1r (Throw e)               \<Colon>x"
   487         "E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x"
   488         "E,dt\<Turnstile>In1r (c1 Finally c2)         \<Colon>x"
   489         "E,dt\<Turnstile>In1r (Init C)                \<Colon>x"
   490 declare not_None_eq [simp] 
   491 declare split_if [split] split_if_asm [split]
   492 declare split_paired_All [simp] split_paired_Ex [simp]
   493 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
   494 
   495 lemma is_acc_class_is_accessible: 
   496   "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
   497 by (auto simp add: is_acc_class_def)
   498 
   499 lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
   500 by (auto simp add: is_acc_iface_def)
   501 
   502 lemma is_acc_iface_Iface_is_accessible: 
   503   "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
   504 by (auto simp add: is_acc_iface_def)
   505 
   506 lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
   507 by (auto simp add: is_acc_type_def)
   508 
   509 lemma is_acc_iface_is_accessible:
   510   "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
   511 by (auto simp add: is_acc_type_def)
   512 
   513 lemma wt_Methd_is_methd: 
   514   "E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig"
   515 apply (erule_tac wt_elim_cases)
   516 apply clarsimp
   517 apply (erule is_methdI, assumption)
   518 done
   519 
   520 
   521 text {* Special versions of some typing rules, better suited to pattern 
   522         match the conclusion (no selectors in the conclusion)
   523 *}
   524 
   525 lemma wt_Call: 
   526 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
   527   max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   528     = {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E;
   529  mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
   530 by (auto elim: wt.Call)
   531 
   532 
   533 lemma invocationTypeExpr_noClassD: 
   534 "\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
   535  \<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
   536 proof -
   537   assume wt: "E\<turnstile>e\<Colon>-RefT statT"
   538   show ?thesis
   539   proof (cases "e=Super")
   540     case True
   541     with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
   542     then show ?thesis by blast
   543   next 
   544     case False then show ?thesis 
   545       by (auto simp add: invmode_def split: split_if_asm)
   546   qed
   547 qed
   548 
   549 lemma wt_Super: 
   550 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> 
   551 \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
   552 by (auto elim: wt.Super)
   553 
   554 lemma wt_FVar:  
   555 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f);
   556   sf=is_static f; fT=(type f); accC=cls E\<rbrakk> 
   557 \<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT"
   558 by (auto dest: wt.FVar)
   559 
   560 
   561 lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C"
   562 by (auto elim: wt_elim_cases intro: "wt.Init")
   563 
   564 declare wt.Skip [iff]
   565 
   566 lemma wt_StatRef: 
   567   "is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt"
   568 apply (rule wt.Cast)
   569 apply  (rule wt.Lit)
   570 apply   (simp (no_asm))
   571 apply  (simp (no_asm_simp))
   572 apply (rule cast.widen)
   573 apply (simp (no_asm))
   574 done
   575 
   576 lemma wt_Inj_elim: 
   577   "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of 
   578                        In1 ec \<Rightarrow> (case ec of 
   579                                     Inl e \<Rightarrow> \<exists>T. U=Inl T  
   580                                   | Inr s \<Rightarrow> U=Inl (PrimT Void))  
   581                      | In2 e \<Rightarrow> (\<exists>T. U=Inl T) 
   582                      | In3 e \<Rightarrow> (\<exists>T. U=Inr T)"
   583 apply (erule wt.induct)
   584 apply auto
   585 done
   586 
   587 --{* In the special syntax to distinguish the typing judgements for expressions, 
   588      statements, variables and expression lists the kind of term corresponds
   589      to the kind of type in the end e.g. An statement (injection @{term In3} 
   590     into terms, always has type void (injection @{term Inl} into the generalised
   591     types. The following simplification procedures establish these kinds of
   592     correlation. 
   593  *}
   594 
   595 lemma wt_expr_eq: "E,dt\<Turnstile>In1l t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T)"
   596   by (auto, frule wt_Inj_elim, auto)
   597 
   598 lemma wt_var_eq: "E,dt\<Turnstile>In2 t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T)"
   599   by (auto, frule wt_Inj_elim, auto)
   600 
   601 lemma wt_exprs_eq: "E,dt\<Turnstile>In3 t\<Colon>U = (\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts)"
   602   by (auto, frule wt_Inj_elim, auto)
   603 
   604 lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)"
   605   by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
   606 
   607 simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = {*
   608   fn _ => fn _ => fn ct =>
   609     (case Thm.term_of ct of
   610       (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   611     | _ => SOME (mk_meta_eq @{thm wt_expr_eq})) *}
   612 
   613 simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = {*
   614   fn _ => fn _ => fn ct =>
   615     (case Thm.term_of ct of
   616       (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   617     | _ => SOME (mk_meta_eq @{thm wt_var_eq})) *}
   618 
   619 simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = {*
   620   fn _ => fn _ => fn ct =>
   621     (case Thm.term_of ct of
   622       (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   623     | _ => SOME (mk_meta_eq @{thm wt_exprs_eq})) *}
   624 
   625 simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = {*
   626   fn _ => fn _ => fn ct =>
   627     (case Thm.term_of ct of
   628       (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   629     | _ => SOME (mk_meta_eq @{thm wt_stmt_eq})) *}
   630 
   631 lemma wt_elim_BinOp:
   632   "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
   633     \<And>T1 T2 T3.
   634        \<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2;
   635           E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3;
   636           T = Inl (PrimT (binop_type binop))\<rbrakk>
   637        \<Longrightarrow> P\<rbrakk>
   638 \<Longrightarrow> P"
   639 apply (erule wt_elim_cases)
   640 apply (cases b)
   641 apply auto
   642 done
   643 
   644 lemma Inj_eq_lemma [simp]: 
   645   "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
   646 by auto
   647 
   648 (* unused *)
   649 lemma single_valued_tys_lemma [rule_format (no_asm)]: 
   650   "\<forall>S T. G\<turnstile>S\<preceq>T \<longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T \<Longrightarrow> E,dt\<Turnstile>t\<Colon>T \<Longrightarrow>  
   651      G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T  = T')"
   652 apply (cases "E", erule wt.induct)
   653 apply (safe del: disjE)
   654 apply (simp_all (no_asm_use) split del: split_if_asm)
   655 apply (safe del: disjE)
   656 (* 17 subgoals *)
   657 apply (tactic {* ALLGOALS (fn i =>
   658   if i = 11 then EVERY'
   659    [thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
   660     thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
   661     thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
   662   else thin_tac @{context} "All ?P" i) *})
   663 (*apply (safe del: disjE elim!: wt_elim_cases)*)
   664 apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
   665 apply (simp_all (no_asm_use) split del: split_if_asm)
   666 apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
   667 apply ((blast del: equalityCE dest: sym [THEN trans])+)
   668 done
   669 
   670 (* unused *)
   671 lemma single_valued_tys: 
   672 "ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
   673 apply (unfold single_valued_def)
   674 apply clarsimp
   675 apply (rule single_valued_tys_lemma)
   676 apply (auto intro!: widen_antisym)
   677 done
   678 
   679 lemma typeof_empty_is_type [rule_format (no_asm)]: 
   680   "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
   681 apply (rule val.induct)
   682 apply           auto
   683 done
   684 
   685 (* unused *)
   686 lemma typeof_is_type [rule_format (no_asm)]: 
   687  "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
   688 apply (rule val.induct)
   689 prefer 5 
   690 apply     fast
   691 apply  (simp_all (no_asm))
   692 done
   693 
   694 end