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