src/HOL/Bali/WellType.thy
author haftmann
Fri Nov 27 08:42:50 2009 +0100 (2009-11-27)
changeset 33965 f57c11db4ad4
parent 32960 69916a850301
child 35067 af4c18c30593
permissions -rw-r--r--
Inl and Inr now with authentic syntax
     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   "lenv" <= (type) "(lname, ty) table"
    41   "lenv" <= (type) "lname \<Rightarrow> ty option"
    42   "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
    43   "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
    44 
    45 
    46 
    47 syntax
    48   pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
    49 translations 
    50   "pkg e" == "pid (cls e)"
    51 
    52 section "Static overloading: maximally specific methods "
    53 
    54 types
    55   emhead = "ref_ty \<times> mhead"
    56 
    57 --{* Some mnemotic selectors for emhead *}
    58 constdefs 
    59   "declrefT" :: "emhead \<Rightarrow> ref_ty"
    60   "declrefT \<equiv> fst"
    61 
    62   "mhd"     :: "emhead \<Rightarrow> mhead"
    63   "mhd \<equiv> snd"
    64 
    65 lemma declrefT_simp[simp]:"declrefT (r,m) = r"
    66 by (simp add: declrefT_def)
    67 
    68 lemma mhd_simp[simp]:"mhd (r,m) = m"
    69 by (simp add: mhd_def)
    70 
    71 lemma static_mhd_simp[simp]: "static (mhd m) = is_static m"
    72 by (cases m) (simp add: member_is_static_simp mhd_def)
    73 
    74 lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m"
    75 by (cases m) simp
    76 
    77 lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m"
    78 by (cases m) simp
    79 
    80 lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
    81 by (cases m) simp
    82 
    83 consts
    84   cmheads        :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
    85   Objectmheads   :: "prog \<Rightarrow> qtname           \<Rightarrow> sig \<Rightarrow> emhead set"
    86   accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
    87   mheads         :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
    88 defs
    89  cmheads_def:
    90 "cmheads G S C 
    91   \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig)"
    92   Objectmheads_def:
    93 "Objectmheads G S  
    94   \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
    95     ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
    96   accObjectmheads_def:
    97 "accObjectmheads G S T
    98    \<equiv> if G\<turnstile>RefT T accessible_in (pid S)
    99         then Objectmheads G S
   100         else \<lambda>sig. {}"
   101 primrec
   102 "mheads G S  NullT     = (\<lambda>sig. {})"
   103 "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
   104                          ` accimethds G (pid S) I sig \<union> 
   105                            accObjectmheads G S (IfaceT I) sig)"
   106 "mheads G S (ClassT C) = cmheads G S C"
   107 "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
   108 
   109 constdefs
   110   --{* applicable methods, cf. 15.11.2.1 *}
   111   appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
   112  "appl_methds G S rt \<equiv> \<lambda> sig. 
   113       {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
   114                            G\<turnstile>(parTs sig)[\<preceq>]pTs'}"
   115 
   116   --{* more specific methods, cf. 15.11.2.2 *}
   117   more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool"
   118  "more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
   119 (*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'*)
   120 
   121   --{* maximally specific methods, cf. 15.11.2.2 *}
   122    max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
   123 
   124  "max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and>
   125                       (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
   126 
   127 
   128 lemma max_spec2appl_meths: 
   129   "x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" 
   130 by (auto simp: max_spec_def)
   131 
   132 lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow>  
   133    mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   134 by (auto simp: appl_methds_def)
   135 
   136 lemma max_spec2mheads: 
   137 "max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A 
   138  \<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   139 apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD)
   140 done
   141 
   142 
   143 constdefs
   144   empty_dt :: "dyn_ty"
   145  "empty_dt \<equiv> \<lambda>a. None"
   146 
   147   invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode"
   148 "invmode m e \<equiv> if is_static m 
   149                   then Static 
   150                   else if e=Super then SuperM else IntVir"
   151 
   152 lemma invmode_nonstatic [simp]: 
   153   "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
   154 apply (unfold invmode_def)
   155 apply (simp (no_asm) add: member_is_static_simp)
   156 done
   157 
   158 
   159 lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m"
   160 apply (unfold invmode_def)
   161 apply (simp (no_asm))
   162 done
   163 
   164 
   165 lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)"
   166 apply (unfold invmode_def)
   167 apply (simp (no_asm))
   168 done
   169 
   170 lemma Null_staticD: 
   171   "a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
   172 apply (clarsimp simp add: invmode_IntVir_eq)
   173 done
   174 
   175 section "Typing for unary operations"
   176 
   177 consts unop_type :: "unop \<Rightarrow> prim_ty"
   178 primrec 
   179 "unop_type UPlus   = Integer"
   180 "unop_type UMinus  = Integer"
   181 "unop_type UBitNot = Integer"
   182 "unop_type UNot    = Boolean"    
   183 
   184 consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
   185 primrec
   186 "wt_unop UPlus   t = (t = PrimT Integer)"
   187 "wt_unop UMinus  t = (t = PrimT Integer)"
   188 "wt_unop UBitNot t = (t = PrimT Integer)"
   189 "wt_unop UNot    t = (t = PrimT Boolean)"
   190 
   191 section "Typing for binary operations"
   192 
   193 consts binop_type :: "binop \<Rightarrow> prim_ty"
   194 primrec
   195 "binop_type Mul      = Integer"     
   196 "binop_type Div      = Integer"
   197 "binop_type Mod      = Integer"
   198 "binop_type Plus     = Integer"
   199 "binop_type Minus    = Integer"
   200 "binop_type LShift   = Integer"
   201 "binop_type RShift   = Integer"
   202 "binop_type RShiftU  = Integer"
   203 "binop_type Less     = Boolean"
   204 "binop_type Le       = Boolean"
   205 "binop_type Greater  = Boolean"
   206 "binop_type Ge       = Boolean"
   207 "binop_type Eq       = Boolean"
   208 "binop_type Neq      = Boolean"
   209 "binop_type BitAnd   = Integer"
   210 "binop_type And      = Boolean"
   211 "binop_type BitXor   = Integer"
   212 "binop_type Xor      = Boolean"
   213 "binop_type BitOr    = Integer"
   214 "binop_type Or       = Boolean"
   215 "binop_type CondAnd  = Boolean"
   216 "binop_type CondOr   = Boolean"
   217 
   218 consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
   219 primrec
   220 "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   221 "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   222 "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   223 "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   224 "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   225 "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   226 "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   227 "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   228 "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   229 "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   230 "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   231 "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   232 "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
   233 "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
   234 "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   235 "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   236 "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   237 "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   238 "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   239 "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   240 "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   241 "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   242 
   243 section "Typing for terms"
   244 
   245 types tys  =        "ty + ty list"
   246 translations
   247   "tys"   <= (type) "ty + ty list"
   248 
   249 
   250 inductive
   251   wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
   252   and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
   253   and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
   254   and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
   255   and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty   list] \<Rightarrow> bool"
   256     ("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
   257 where
   258 
   259   "E,dt\<Turnstile>s\<Colon>\<surd> \<equiv> E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
   260 | "E,dt\<Turnstile>e\<Colon>-T \<equiv> E,dt\<Turnstile>In1l e\<Colon>Inl T"
   261 | "E,dt\<Turnstile>e\<Colon>=T \<equiv> E,dt\<Turnstile>In2  e\<Colon>Inl T"
   262 | "E,dt\<Turnstile>e\<Colon>\<doteq>T \<equiv> E,dt\<Turnstile>In3  e\<Colon>Inr T"
   263 
   264 --{* well-typed statements *}
   265 
   266 | Skip:                                 "E,dt\<Turnstile>Skip\<Colon>\<surd>"
   267 
   268 | Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
   269                                          E,dt\<Turnstile>Expr e\<Colon>\<surd>"
   270   --{* cf. 14.6 *}
   271 | Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
   272                                          E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
   273 
   274 | Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
   275           E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   276                                          E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
   277 
   278   --{* cf. 14.8 *}
   279 | If:   "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   280           E,dt\<Turnstile>c1\<Colon>\<surd>;
   281           E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   282                                          E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
   283 
   284   --{* cf. 14.10 *}
   285 | Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   286           E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   287                                          E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
   288   --{* cf. 14.13, 14.15, 14.16 *}
   289 | Jmp:                                   "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>"
   290 
   291   --{* cf. 14.16 *}
   292 | Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
   293           prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
   294                                          E,dt\<Turnstile>Throw e\<Colon>\<surd>"
   295   --{* cf. 14.18 *}
   296 | Try:  "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
   297           lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
   298           \<Longrightarrow>
   299                                          E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
   300 
   301   --{* cf. 14.18 *}
   302 | Fin:  "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   303                                          E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
   304 
   305 | Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
   306                                          E,dt\<Turnstile>Init C\<Colon>\<surd>"
   307   --{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
   308      The class isn't necessarily accessible from the points @{term Init} 
   309      is called. Therefor we only demand @{term is_class} and not 
   310      @{term is_acc_class} here. 
   311    *}
   312 
   313 --{* well-typed expressions *}
   314 
   315   --{* cf. 15.8 *}
   316 | NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
   317                                          E,dt\<Turnstile>NewC C\<Colon>-Class C"
   318   --{* cf. 15.9 *}
   319 | NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T;
   320           E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   321                                          E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
   322 
   323   --{* cf. 15.15 *}
   324 | Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
   325           prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
   326                                          E,dt\<Turnstile>Cast T' e\<Colon>-T'"
   327 
   328   --{* cf. 15.19.2 *}
   329 | Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
   330           prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
   331                                          E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
   332 
   333   --{* cf. 15.7.1 *}
   334 | Lit:  "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
   335                                          E,dt\<Turnstile>Lit x\<Colon>-T"
   336 
   337 | UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
   338           \<Longrightarrow>
   339           E,dt\<Turnstile>UnOp unop e\<Colon>-T"
   340   
   341 | BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
   342            T=PrimT (binop_type binop)\<rbrakk> 
   343            \<Longrightarrow>
   344            E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
   345   
   346   --{* cf. 15.10.2, 15.11.1 *}
   347 | Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   348           class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
   349                                          E,dt\<Turnstile>Super\<Colon>-Class (super c)"
   350 
   351   --{* cf. 15.13.1, 15.10.1, 15.12 *}
   352 | Acc:  "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
   353                                          E,dt\<Turnstile>Acc va\<Colon>-T"
   354 
   355   --{* cf. 15.25, 15.25.1 *}
   356 | Ass:  "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
   357           E,dt\<Turnstile>v \<Colon>-T';
   358           prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
   359                                          E,dt\<Turnstile>va:=v\<Colon>-T'"
   360 
   361   --{* cf. 15.24 *}
   362 | Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
   363           E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
   364           prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
   365                                          E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
   366 
   367   --{* cf. 15.11.1, 15.11.2, 15.11.3 *}
   368 | Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
   369           E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
   370           max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   371             = {((statDeclT,m),pTs')}
   372          \<rbrakk> \<Longrightarrow>
   373                    E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
   374 
   375 | Methd: "\<lbrakk>is_class (prg E) C;
   376           methd (prg E) C sig = Some m;
   377           E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
   378                                          E,dt\<Turnstile>Methd C sig\<Colon>-T"
   379  --{* The class @{term C} is the dynamic class of the method call 
   380     (cf. Eval.thy). 
   381     It hasn't got to be directly accessible from the current package 
   382     @{term "(pkg E)"}. 
   383     Only the static class must be accessible (enshured indirectly by 
   384     @{term Call}). 
   385     Note that l is just a dummy value. It is only used in the smallstep 
   386     semantics. To proof typesafety directly for the smallstep semantics 
   387     we would have to assume conformance of l here!
   388   *}
   389 
   390 | Body: "\<lbrakk>is_class (prg E) D;
   391           E,dt\<Turnstile>blk\<Colon>\<surd>;
   392           (lcl E) Result = Some T;
   393           is_type (prg E) T\<rbrakk> \<Longrightarrow>
   394                                          E,dt\<Turnstile>Body D blk\<Colon>-T"
   395 --{* The class @{term D} implementing the method must not directly be 
   396      accessible  from the current package @{term "(pkg E)"}, but can also 
   397      be indirectly accessible due to inheritance (enshured in @{term Call})
   398     The result type hasn't got to be accessible in Java! (If it is not 
   399     accessible you can only assign it to Object).
   400     For dummy value l see rule @{term Methd}. 
   401    *}
   402 
   403 --{* well-typed variables *}
   404 
   405   --{* cf. 15.13.1 *}
   406 | LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
   407                                          E,dt\<Turnstile>LVar vn\<Colon>=T"
   408   --{* cf. 15.10.1 *}
   409 | FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
   410           accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
   411                          E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
   412   --{* cf. 15.12 *}
   413 | AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
   414           E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   415                                          E,dt\<Turnstile>e.[i]\<Colon>=T"
   416 
   417 
   418 --{* well-typed expression lists *}
   419 
   420   --{* cf. 15.11.??? *}
   421 | Nil:                                  "E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
   422 
   423   --{* cf. 15.11.??? *}
   424 | Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
   425           E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
   426                                          E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
   427 
   428 
   429 syntax (* for purely static typing *)
   430   "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
   431   "_wt_stmt" :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
   432   "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
   433   "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
   434   "_ty_exprs":: "env \<Rightarrow> [expr list,
   435                      \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
   436 
   437 syntax (xsymbols)
   438   "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
   439   "_wt_stmt" ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
   440   "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
   441   "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
   442   "_ty_exprs" :: "env \<Rightarrow> [expr list,
   443                     \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
   444 
   445 translations
   446         "E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
   447         "E\<turnstile>s\<Colon>\<surd>"  == "E\<turnstile>In1r s\<Colon>CONST Inl (PrimT Void)"
   448         "E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>CONST Inl T"
   449         "E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>CONST Inl T"
   450         "E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>CONST Inr T"
   451 
   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