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