src/HOL/Bali/WellType.thy
author schirmer
Fri Feb 22 11:26:44 2002 +0100 (2002-02-22)
changeset 12925 99131847fb93
parent 12858 6214f03d6d27
child 13337 f75dfc606ac7
permissions -rw-r--r--
Added check for field/method access to operational semantics and proved the acesses valid.
     1 (*  Title:      HOL/Bali/WellType.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 header {* Well-typedness of Java programs *}
     7 
     8 theory WellType = DeclConcepts:
     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))) ` o2s (accmethd G S C sig)"
    92   Objectmheads_def:
    93 "Objectmheads G S  
    94   \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
    95     ` o2s (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 
   110 (* more detailed than necessary for type-safety, see below. *)
   111 constdefs
   112   (* applicable methods, cf. 15.11.2.1 *)
   113   appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
   114  "appl_methds G S rt \<equiv> \<lambda> sig. 
   115       {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
   116                            G\<turnstile>(parTs sig)[\<preceq>]pTs'}"
   117 
   118   (* more specific methods, cf. 15.11.2.2 *)
   119   more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool"
   120  "more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
   121 (*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'*)
   122 
   123   (* maximally specific methods, cf. 15.11.2.2 *)
   124    max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
   125 
   126  "max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and>
   127 		      (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
   128 (*
   129 rules (* all properties of more_spec, appl_methods and max_spec we actually need
   130          these can easily be proven from the above definitions *)
   131 
   132 max_spec2mheads "max_spec G S rt (mn, pTs) = insert (mh, pTs') A \<Longrightarrow>
   133       mh\<in>mheads G S rt (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   134 *)
   135 
   136 lemma max_spec2appl_meths: 
   137   "x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" 
   138 by (auto simp: max_spec_def)
   139 
   140 lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow>  
   141    mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   142 by (auto simp: appl_methds_def)
   143 
   144 lemma max_spec2mheads: 
   145 "max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A 
   146  \<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   147 apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD)
   148 done
   149 
   150 
   151 constdefs
   152   empty_dt :: "dyn_ty"
   153  "empty_dt \<equiv> \<lambda>a. None"
   154 
   155   invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode"
   156 "invmode m e \<equiv> if is_static m 
   157                   then Static 
   158                   else if e=Super then SuperM else IntVir"
   159 
   160 lemma invmode_nonstatic [simp]: 
   161   "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
   162 apply (unfold invmode_def)
   163 apply (simp (no_asm) add: member_is_static_simp)
   164 done
   165 
   166 
   167 lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m"
   168 apply (unfold invmode_def)
   169 apply (simp (no_asm))
   170 done
   171 
   172 
   173 lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)"
   174 apply (unfold invmode_def)
   175 apply (simp (no_asm))
   176 done
   177 
   178 lemma Null_staticD: 
   179   "a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
   180 apply (clarsimp simp add: invmode_IntVir_eq)
   181 done
   182 
   183 
   184 types tys  =        "ty + ty list"
   185 translations
   186   "tys"   <= (type) "ty + ty list"
   187 
   188 consts
   189   wt    :: "(env\<spacespace> \<times> dyn_ty\<spacespace> \<times>  term \<times> tys) set"
   190 (*wt    :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term \<times> tys) set" not feasible because of 
   191 					      \<spacespace>  changing env in Try stmt *)
   192 
   193 syntax
   194 wt      :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys]  \<Rightarrow> bool" ("_,_|=_::_" [51,51,51,51] 50)
   195 wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_|=_:<>" [51,51,51   ] 50)
   196 ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_|=_:-_" [51,51,51,51] 50)
   197 ty_var  :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_|=_:=_" [51,51,51,51] 50)
   198 ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
   199 	         \<spacespace>        \<spacespace>  ty   list] \<Rightarrow> bool" ("_,_|=_:#_" [51,51,51,51] 50)
   200 
   201 syntax (xsymbols)
   202 wt      :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
   203 wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
   204 ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
   205 ty_var  :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
   206 ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
   207 		  \<spacespace>        \<spacespace>  ty   list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
   208 
   209 translations
   210 	"E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt"
   211 	"E,dt\<Turnstile>s\<Colon>\<surd>"  == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
   212 	"E,dt\<Turnstile>e\<Colon>-T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T"
   213 	"E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2  e\<Colon>Inl T"
   214 	"E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3  e\<Colon>Inr T"
   215 
   216 syntax (* for purely static typing *)
   217   wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
   218   wt_stmt_ :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
   219   ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
   220   ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
   221   ty_exprs_:: "env \<Rightarrow> [expr list,
   222 		     \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
   223 
   224 syntax (xsymbols)
   225   wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
   226   wt_stmt_ ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
   227   ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
   228   ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
   229   ty_exprs_ :: "env \<Rightarrow> [expr list,
   230 		    \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
   231 
   232 translations
   233 	"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
   234 	"E\<turnstile>s\<Colon>\<surd>" == "E,empty_dt\<Turnstile>s\<Colon>\<surd>"
   235 	"E\<turnstile>e\<Colon>-T" == "E,empty_dt\<Turnstile>e\<Colon>-T"
   236 	"E\<turnstile>e\<Colon>=T" == "E,empty_dt\<Turnstile>e\<Colon>=T"
   237 	"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T"
   238 
   239 
   240 inductive wt intros 
   241 
   242 
   243 (* well-typed statements *)
   244 
   245   Skip:					"E,dt\<Turnstile>Skip\<Colon>\<surd>"
   246 
   247   Expr:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
   248 					 E,dt\<Turnstile>Expr e\<Colon>\<surd>"
   249   (* cf. 14.6 *)
   250   Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
   251                                          E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
   252 
   253   Comp:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
   254 	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   255 					 E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
   256 
   257   (* cf. 14.8 *)
   258   If:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   259 	  E,dt\<Turnstile>c1\<Colon>\<surd>;
   260 	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   261 					 E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
   262 
   263   (* cf. 14.10 *)
   264   Loop:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   265 	  E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   266 					 E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
   267   (* cf. 14.13, 14.15, 14.16 *)
   268   Do:                                   "E,dt\<Turnstile>Do jump\<Colon>\<surd>"
   269 
   270   (* cf. 14.16 *)
   271   Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
   272 	  prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
   273 					 E,dt\<Turnstile>Throw e\<Colon>\<surd>"
   274   (* cf. 14.18 *)
   275   Try:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
   276 	  lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
   277           \<Longrightarrow>
   278 					 E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
   279 
   280   (* cf. 14.18 *)
   281   Fin:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   282 					 E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
   283 
   284   Init:	"\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
   285 					 E,dt\<Turnstile>Init C\<Colon>\<surd>"
   286   (* Init is created on the fly during evaluation (see Eval.thy). The class
   287    * isn't necessarily accessible from the points Init is called. Therefor
   288    * we only demand is_class and not is_acc_class here 
   289    *)
   290 
   291 (* well-typed expressions *)
   292 
   293   (* cf. 15.8 *)
   294   NewC:	"\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
   295 					 E,dt\<Turnstile>NewC C\<Colon>-Class C"
   296   (* cf. 15.9 *)
   297   NewA:	"\<lbrakk>is_acc_type (prg E) (pkg E) T;
   298 	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   299 					 E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
   300 
   301   (* cf. 15.15 *)
   302   Cast:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
   303 	  prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
   304 					 E,dt\<Turnstile>Cast T' e\<Colon>-T'"
   305 
   306   (* cf. 15.19.2 *)
   307   Inst:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
   308 	  prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
   309 					 E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
   310 
   311   (* cf. 15.7.1 *)
   312   Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
   313 					 E,dt\<Turnstile>Lit x\<Colon>-T"
   314 
   315   (* cf. 15.10.2, 15.11.1 *)
   316   Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   317 	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
   318 					 E,dt\<Turnstile>Super\<Colon>-Class (super c)"
   319 
   320   (* cf. 15.13.1, 15.10.1, 15.12 *)
   321   Acc:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
   322 					 E,dt\<Turnstile>Acc va\<Colon>-T"
   323 
   324   (* cf. 15.25, 15.25.1 *)
   325   Ass:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
   326 	  E,dt\<Turnstile>v \<Colon>-T';
   327 	  prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
   328 					 E,dt\<Turnstile>va:=v\<Colon>-T'"
   329 
   330   (* cf. 15.24 *)
   331   Cond:	"\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
   332 	  E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
   333 	  prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
   334 					 E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
   335 
   336   (* cf. 15.11.1, 15.11.2, 15.11.3 *)
   337   Call:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
   338 	  E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
   339 	  max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   340             = {((statDeclT,m),pTs')}
   341          \<rbrakk> \<Longrightarrow>
   342 		   E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
   343 
   344   Methd: "\<lbrakk>is_class (prg E) C;
   345 	  methd (prg E) C sig = Some m;
   346 	  E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
   347 					 E,dt\<Turnstile>Methd C sig\<Colon>-T"
   348  (* The class C is the dynamic class of the method call (cf. Eval.thy). 
   349   * It hasn't got to be directly accessible from the current package (pkg E). 
   350   * Only the static class must be accessible (enshured indirectly by Call). 
   351   *)
   352 
   353   Body:	"\<lbrakk>is_class (prg E) D;
   354 	  E,dt\<Turnstile>blk\<Colon>\<surd>;
   355 	  (lcl E) Result = Some T;
   356           is_type (prg E) T\<rbrakk> \<Longrightarrow>
   357    					 E,dt\<Turnstile>Body D blk\<Colon>-T"
   358   (* the class D implementing the method must not directly be accessible 
   359    * from the current package (pkg E), but can also be indirectly accessible 
   360    * due to inheritance (enshured in Call)
   361    * The result type hasn't got to be accessible in Java! (If it is not 
   362    * accessible you can only assign it to Object) 
   363    *)
   364 
   365 (* well-typed variables *)
   366 
   367   (* cf. 15.13.1 *)
   368   LVar:	"\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
   369 					 E,dt\<Turnstile>LVar vn\<Colon>=T"
   370   (* cf. 15.10.1 *)
   371   FVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
   372 	  accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
   373 			 E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
   374   (* cf. 15.12 *)
   375   AVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
   376 	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   377 					 E,dt\<Turnstile>e.[i]\<Colon>=T"
   378 
   379 
   380 (* well-typed expression lists *)
   381 
   382   (* cf. 15.11.??? *)
   383   Nil:					"E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
   384 
   385   (* cf. 15.11.??? *)
   386   Cons:	"\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
   387 	  E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
   388 					 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
   389 
   390 
   391 declare not_None_eq [simp del] 
   392 declare split_if [split del] split_if_asm [split del]
   393 declare split_paired_All [simp del] split_paired_Ex [simp del]
   394 ML_setup {*
   395 simpset_ref() := simpset() delloop "split_all_tac"
   396 *}
   397 inductive_cases wt_stmt_cases: "E,dt\<Turnstile>c\<Colon>\<surd>"
   398 inductive_cases wt_elim_cases:
   399 	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
   400 	"E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
   401 	"E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
   402 	"E,dt\<Turnstile>In1l (NewC C)                \<Colon>T"
   403 	"E,dt\<Turnstile>In1l (New T'[i])             \<Colon>T"
   404 	"E,dt\<Turnstile>In1l (Cast T' e)             \<Colon>T"
   405 	"E,dt\<Turnstile>In1l (e InstOf T')           \<Colon>T"
   406 	"E,dt\<Turnstile>In1l (Lit x)                 \<Colon>T"
   407 	"E,dt\<Turnstile>In1l (Super)                 \<Colon>T"
   408 	"E,dt\<Turnstile>In1l (Acc va)                \<Colon>T"
   409 	"E,dt\<Turnstile>In1l (Ass va v)              \<Colon>T"
   410 	"E,dt\<Turnstile>In1l (e0 ? e1 : e2)          \<Colon>T"
   411 	"E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
   412 	"E,dt\<Turnstile>In1l (Methd C sig)           \<Colon>T"
   413 	"E,dt\<Turnstile>In1l (Body D blk)            \<Colon>T"
   414 	"E,dt\<Turnstile>In3  ([])                    \<Colon>Ts"
   415 	"E,dt\<Turnstile>In3  (e#es)                  \<Colon>Ts"
   416 	"E,dt\<Turnstile>In1r  Skip                   \<Colon>x"
   417 	"E,dt\<Turnstile>In1r (Expr e)                \<Colon>x"
   418 	"E,dt\<Turnstile>In1r (c1;; c2)               \<Colon>x"
   419         "E,dt\<Turnstile>In1r (l\<bullet> c)                  \<Colon>x" 
   420 	"E,dt\<Turnstile>In1r (If(e) c1 Else c2)      \<Colon>x"
   421 	"E,dt\<Turnstile>In1r (l\<bullet> While(e) c)         \<Colon>x"
   422         "E,dt\<Turnstile>In1r (Do jump)               \<Colon>x"
   423 	"E,dt\<Turnstile>In1r (Throw e)               \<Colon>x"
   424 	"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x"
   425 	"E,dt\<Turnstile>In1r (c1 Finally c2)         \<Colon>x"
   426 	"E,dt\<Turnstile>In1r (Init C)                \<Colon>x"
   427 declare not_None_eq [simp] 
   428 declare split_if [split] split_if_asm [split]
   429 declare split_paired_All [simp] split_paired_Ex [simp]
   430 ML_setup {*
   431 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   432 *}
   433 
   434 lemma is_acc_class_is_accessible: 
   435   "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
   436 by (auto simp add: is_acc_class_def)
   437 
   438 lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
   439 by (auto simp add: is_acc_iface_def)
   440 
   441 lemma is_acc_iface_is_accessible: 
   442   "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
   443 by (auto simp add: is_acc_iface_def)
   444 
   445 lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
   446 by (auto simp add: is_acc_type_def)
   447 
   448 lemma is_acc_iface_is_accessible: "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
   449 by (auto simp add: is_acc_type_def)
   450 
   451 lemma wt_Methd_is_methd: 
   452   "E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig"
   453 apply (erule_tac wt_elim_cases)
   454 apply clarsimp
   455 apply (erule is_methdI, assumption)
   456 done
   457 
   458 (* Special versions of some typing rules, better suited to pattern match the
   459  * conclusion (no selectors in the conclusion\<dots>)
   460  *)
   461 
   462 lemma wt_Super:
   463 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   464   class (prg E) C = Some c;D=super c\<rbrakk> 
   465  \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
   466 by (auto elim: wt.Super)
   467  
   468 
   469 lemma wt_Call: 
   470 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
   471   max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   472     = {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E;
   473  mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
   474 by (auto elim: wt.Call)
   475 
   476 
   477 lemma invocationTypeExpr_noClassD: 
   478 "\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
   479  \<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
   480 proof -
   481   assume wt: "E\<turnstile>e\<Colon>-RefT statT"
   482   show ?thesis
   483   proof (cases "e=Super")
   484     case True
   485     with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
   486     then show ?thesis by blast
   487   next 
   488     case False then show ?thesis 
   489       by (auto simp add: invmode_def split: split_if_asm)
   490   qed
   491 qed
   492 
   493 lemma wt_Super: 
   494 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> 
   495 \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
   496 by (auto elim: wt.Super)
   497 
   498 lemma wt_FVar:	
   499 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f);
   500   sf=is_static f; fT=(type f); accC=cls E\<rbrakk> 
   501 \<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT"
   502 by (auto dest: wt.FVar)
   503 
   504 
   505 lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C"
   506 by (auto elim: wt_elim_cases intro: "wt.Init")
   507 
   508 declare wt.Skip [iff]
   509 
   510 lemma wt_StatRef: 
   511   "is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt"
   512 apply (rule wt.Cast)
   513 apply  (rule wt.Lit)
   514 apply   (simp (no_asm))
   515 apply  (simp (no_asm_simp))
   516 apply (rule cast.widen)
   517 apply (simp (no_asm))
   518 done
   519 
   520 lemma wt_Inj_elim: 
   521   "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of 
   522                        In1 ec \<Rightarrow> (case ec of 
   523                                     Inl e \<Rightarrow> \<exists>T. U=Inl T  
   524                                   | Inr s \<Rightarrow> U=Inl (PrimT Void))  
   525                      | In2 e \<Rightarrow> (\<exists>T. U=Inl T) 
   526                      | In3 e \<Rightarrow> (\<exists>T. U=Inr T)"
   527 apply (erule wt.induct)
   528 apply auto
   529 done
   530 
   531 ML {*
   532 fun wt_fun name inj rhs =
   533 let
   534   val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U"
   535   val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   536 	(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac])
   537   fun is_Inj (Const (inj,_) $ _) = true
   538     | is_Inj _                   = false
   539   fun pred (t as (_ $ (Const ("Pair",_) $
   540      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   541        x))) $ _ )) = is_Inj x
   542 in
   543   make_simproc name lhs pred (thm name)
   544 end
   545 
   546 val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>-T"
   547 val wt_var_proc   = wt_fun "wt_var_eq"   "In2"  "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>=T"
   548 val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3"  "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"
   549 val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>"
   550 *}
   551 
   552 ML {*
   553 Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
   554 *}
   555 
   556 lemma Inj_eq_lemma [simp]: 
   557   "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
   558 by auto
   559 
   560 (* unused *)
   561 lemma single_valued_tys_lemma [rule_format (no_asm)]: 
   562   "\<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>  
   563      G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T  = T')"
   564 apply (cases "E", erule wt.induct)
   565 apply (safe del: disjE)
   566 apply (simp_all (no_asm_use) split del: split_if_asm)
   567 apply (safe del: disjE)
   568 (* 17 subgoals *)
   569 apply (tactic {* ALLGOALS (fn i => if i = 9 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) *})
   570 (*apply (safe del: disjE elim!: wt_elim_cases)*)
   571 apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
   572 apply (simp_all (no_asm_use) split del: split_if_asm)
   573 apply (erule_tac [10] V = "All ?P" in thin_rl) (* Call *)
   574 apply ((blast del: equalityCE dest: sym [THEN trans])+)
   575 done
   576 
   577 (* unused *)
   578 lemma single_valued_tys: 
   579 "ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
   580 apply (unfold single_valued_def)
   581 apply clarsimp
   582 apply (rule single_valued_tys_lemma)
   583 apply (auto intro!: widen_antisym)
   584 done
   585 
   586 lemma typeof_empty_is_type [rule_format (no_asm)]: 
   587   "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
   588 apply (rule val.induct)
   589 apply    	auto
   590 done
   591 
   592 (* unused *)
   593 lemma typeof_is_type [rule_format (no_asm)]: 
   594  "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
   595 apply (rule val.induct)
   596 prefer 5 
   597 apply     fast
   598 apply  (simp_all (no_asm))
   599 done
   600 
   601 end