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