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