src/HOL/Bali/WellType.thy
author schirmer
Wed Jul 10 15:07:02 2002 +0200 (2002-07-10)
changeset 13337 f75dfc606ac7
parent 12925 99131847fb93
child 13384 a34e38154413
permissions -rw-r--r--
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
     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 consts unop_type :: "unop \<Rightarrow> prim_ty"
   184 primrec 
   185 "unop_type UPlus   = Integer"
   186 "unop_type UMinus  = Integer"
   187 "unop_type UBitNot = Integer"
   188 "unop_type UNot    = Boolean"    
   189 
   190 consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
   191 primrec
   192 "wt_unop UPlus   t = (t = PrimT Integer)"
   193 "wt_unop UMinus  t = (t = PrimT Integer)"
   194 "wt_unop UBitNot t = (t = PrimT Integer)"
   195 "wt_unop UNot    t = (t = PrimT Boolean)"
   196 
   197 consts binop_type :: "binop \<Rightarrow> prim_ty"
   198 primrec
   199 "binop_type Mul      = Integer"     
   200 "binop_type Div      = Integer"
   201 "binop_type Mod      = Integer"
   202 "binop_type Plus     = Integer"
   203 "binop_type Minus    = Integer"
   204 "binop_type LShift   = Integer"
   205 "binop_type RShift   = Integer"
   206 "binop_type RShiftU  = Integer"
   207 "binop_type Less     = Boolean"
   208 "binop_type Le       = Boolean"
   209 "binop_type Greater  = Boolean"
   210 "binop_type Ge       = Boolean"
   211 "binop_type Eq       = Boolean"
   212 "binop_type Neq      = Boolean"
   213 "binop_type BitAnd   = Integer"
   214 "binop_type And      = Boolean"
   215 "binop_type BitXor   = Integer"
   216 "binop_type Xor      = Boolean"
   217 "binop_type BitOr    = Integer"
   218 "binop_type Or       = Boolean"
   219 
   220 consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
   221 primrec
   222 "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   223 "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   224 "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   225 "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   226 "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   227 "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   228 "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   229 "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   230 "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   231 "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   232 "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   233 "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   234 "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
   235 "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
   236 "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   237 "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   238 "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   239 "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   240 "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   241 "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   242 
   243       
   244 types tys  =        "ty + ty list"
   245 translations
   246   "tys"   <= (type) "ty + ty list"
   247 
   248 consts
   249   wt    :: "(env\<spacespace> \<times> dyn_ty\<spacespace> \<times>  term \<times> tys) set"
   250 (*wt    :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term \<times> tys) set" not feasible because of 
   251 					      \<spacespace>  changing env in Try stmt *)
   252 
   253 syntax
   254 wt      :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys]  \<Rightarrow> bool" ("_,_|=_::_" [51,51,51,51] 50)
   255 wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_|=_:<>" [51,51,51   ] 50)
   256 ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_|=_:-_" [51,51,51,51] 50)
   257 ty_var  :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_|=_:=_" [51,51,51,51] 50)
   258 ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
   259 	         \<spacespace>        \<spacespace>  ty   list] \<Rightarrow> bool" ("_,_|=_:#_" [51,51,51,51] 50)
   260 
   261 syntax (xsymbols)
   262 wt      :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
   263 wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
   264 ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
   265 ty_var  :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
   266 ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
   267 		  \<spacespace>        \<spacespace>  ty   list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
   268 
   269 translations
   270 	"E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt"
   271 	"E,dt\<Turnstile>s\<Colon>\<surd>"  == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
   272 	"E,dt\<Turnstile>e\<Colon>-T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T"
   273 	"E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2  e\<Colon>Inl T"
   274 	"E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3  e\<Colon>Inr T"
   275 
   276 syntax (* for purely static typing *)
   277   wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
   278   wt_stmt_ :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
   279   ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
   280   ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
   281   ty_exprs_:: "env \<Rightarrow> [expr list,
   282 		     \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
   283 
   284 syntax (xsymbols)
   285   wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
   286   wt_stmt_ ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
   287   ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
   288   ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
   289   ty_exprs_ :: "env \<Rightarrow> [expr list,
   290 		    \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
   291 
   292 translations
   293 	"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
   294 	"E\<turnstile>s\<Colon>\<surd>" == "E,empty_dt\<Turnstile>s\<Colon>\<surd>"
   295 	"E\<turnstile>e\<Colon>-T" == "E,empty_dt\<Turnstile>e\<Colon>-T"
   296 	"E\<turnstile>e\<Colon>=T" == "E,empty_dt\<Turnstile>e\<Colon>=T"
   297 	"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T"
   298 
   299 
   300 
   301 inductive wt intros 
   302 
   303 
   304 (* well-typed statements *)
   305 
   306   Skip:					"E,dt\<Turnstile>Skip\<Colon>\<surd>"
   307 
   308   Expr:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
   309 					 E,dt\<Turnstile>Expr e\<Colon>\<surd>"
   310   (* cf. 14.6 *)
   311   Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
   312                                          E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
   313 
   314   Comp:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
   315 	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   316 					 E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
   317 
   318   (* cf. 14.8 *)
   319   If:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   320 	  E,dt\<Turnstile>c1\<Colon>\<surd>;
   321 	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   322 					 E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
   323 
   324   (* cf. 14.10 *)
   325   Loop:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   326 	  E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   327 					 E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
   328   (* cf. 14.13, 14.15, 14.16 *)
   329   Do:                                   "E,dt\<Turnstile>Do jump\<Colon>\<surd>"
   330 
   331   (* cf. 14.16 *)
   332   Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
   333 	  prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
   334 					 E,dt\<Turnstile>Throw e\<Colon>\<surd>"
   335   (* cf. 14.18 *)
   336   Try:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
   337 	  lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
   338           \<Longrightarrow>
   339 					 E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
   340 
   341   (* cf. 14.18 *)
   342   Fin:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   343 					 E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
   344 
   345   Init:	"\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
   346 					 E,dt\<Turnstile>Init C\<Colon>\<surd>"
   347   (* Init is created on the fly during evaluation (see Eval.thy). The class
   348    * isn't necessarily accessible from the points Init is called. Therefor
   349    * we only demand is_class and not is_acc_class here 
   350    *)
   351 
   352 (* well-typed expressions *)
   353 
   354   (* cf. 15.8 *)
   355   NewC:	"\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
   356 					 E,dt\<Turnstile>NewC C\<Colon>-Class C"
   357   (* cf. 15.9 *)
   358   NewA:	"\<lbrakk>is_acc_type (prg E) (pkg E) T;
   359 	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   360 					 E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
   361 
   362   (* cf. 15.15 *)
   363   Cast:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
   364 	  prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
   365 					 E,dt\<Turnstile>Cast T' e\<Colon>-T'"
   366 
   367   (* cf. 15.19.2 *)
   368   Inst:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
   369 	  prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
   370 					 E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
   371 
   372   (* cf. 15.7.1 *)
   373   Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
   374 					 E,dt\<Turnstile>Lit x\<Colon>-T"
   375 
   376   UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
   377           \<Longrightarrow>
   378 	  E,dt\<Turnstile>UnOp unop e\<Colon>-T"
   379   
   380   BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
   381            T=PrimT (binop_type binop)\<rbrakk> 
   382            \<Longrightarrow>
   383 	   E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
   384   
   385   (* cf. 15.10.2, 15.11.1 *)
   386   Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   387 	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
   388 					 E,dt\<Turnstile>Super\<Colon>-Class (super c)"
   389 
   390   (* cf. 15.13.1, 15.10.1, 15.12 *)
   391   Acc:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
   392 					 E,dt\<Turnstile>Acc va\<Colon>-T"
   393 
   394   (* cf. 15.25, 15.25.1 *)
   395   Ass:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
   396 	  E,dt\<Turnstile>v \<Colon>-T';
   397 	  prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
   398 					 E,dt\<Turnstile>va:=v\<Colon>-T'"
   399 
   400   (* cf. 15.24 *)
   401   Cond:	"\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
   402 	  E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
   403 	  prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
   404 					 E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
   405 
   406   (* cf. 15.11.1, 15.11.2, 15.11.3 *)
   407   Call:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
   408 	  E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
   409 	  max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   410             = {((statDeclT,m),pTs')}
   411          \<rbrakk> \<Longrightarrow>
   412 		   E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
   413 
   414   Methd: "\<lbrakk>is_class (prg E) C;
   415 	  methd (prg E) C sig = Some m;
   416 	  E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
   417 					 E,dt\<Turnstile>Methd C sig\<Colon>-T"
   418  (* The class C is the dynamic class of the method call (cf. Eval.thy). 
   419   * It hasn't got to be directly accessible from the current package (pkg E). 
   420   * Only the static class must be accessible (enshured indirectly by Call). 
   421   * Note that l is just a dummy value. It is only used in the smallstep 
   422   * semantics. To proof typesafety directly for the smallstep semantics 
   423   * we would have to assume conformance of l here!
   424   *)
   425 
   426   Body:	"\<lbrakk>is_class (prg E) D;
   427 	  E,dt\<Turnstile>blk\<Colon>\<surd>;
   428 	  (lcl E) Result = Some T;
   429           is_type (prg E) T\<rbrakk> \<Longrightarrow>
   430    					 E,dt\<Turnstile>Body D blk\<Colon>-T"
   431   (* the class D implementing the method must not directly be accessible 
   432    * from the current package (pkg E), but can also be indirectly accessible 
   433    * due to inheritance (enshured in Call)
   434    * The result type hasn't got to be accessible in Java! (If it is not 
   435    * accessible you can only assign it to Object).
   436    * For dummy value l see rule Methd. 
   437    *)
   438 
   439 (* well-typed variables *)
   440 
   441   (* cf. 15.13.1 *)
   442   LVar:	"\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
   443 					 E,dt\<Turnstile>LVar vn\<Colon>=T"
   444   (* cf. 15.10.1 *)
   445   FVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
   446 	  accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
   447 			 E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
   448   (* cf. 15.12 *)
   449   AVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
   450 	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   451 					 E,dt\<Turnstile>e.[i]\<Colon>=T"
   452 
   453 
   454 (* well-typed expression lists *)
   455 
   456   (* cf. 15.11.??? *)
   457   Nil:					"E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
   458 
   459   (* cf. 15.11.??? *)
   460   Cons:	"\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
   461 	  E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
   462 					 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
   463 
   464 
   465 declare not_None_eq [simp del] 
   466 declare split_if [split del] split_if_asm [split del]
   467 declare split_paired_All [simp del] split_paired_Ex [simp del]
   468 ML_setup {*
   469 simpset_ref() := simpset() delloop "split_all_tac"
   470 *}
   471 inductive_cases wt_stmt_cases: "E,dt\<Turnstile>c\<Colon>\<surd>"
   472 inductive_cases wt_elim_cases:
   473 	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
   474 	"E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
   475 	"E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
   476 	"E,dt\<Turnstile>In1l (NewC C)                \<Colon>T"
   477 	"E,dt\<Turnstile>In1l (New T'[i])             \<Colon>T"
   478 	"E,dt\<Turnstile>In1l (Cast T' e)             \<Colon>T"
   479 	"E,dt\<Turnstile>In1l (e InstOf T')           \<Colon>T"
   480 	"E,dt\<Turnstile>In1l (Lit x)                 \<Colon>T"
   481         "E,dt\<Turnstile>In1l (UnOp unop e)           \<Colon>T"
   482         "E,dt\<Turnstile>In1l (BinOp binop e1 e2)     \<Colon>T"
   483 	"E,dt\<Turnstile>In1l (Super)                 \<Colon>T"
   484 	"E,dt\<Turnstile>In1l (Acc va)                \<Colon>T"
   485 	"E,dt\<Turnstile>In1l (Ass va v)              \<Colon>T"
   486 	"E,dt\<Turnstile>In1l (e0 ? e1 : e2)          \<Colon>T"
   487 	"E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
   488 	"E,dt\<Turnstile>In1l (Methd C sig)           \<Colon>T"
   489 	"E,dt\<Turnstile>In1l (Body D blk)            \<Colon>T"
   490 	"E,dt\<Turnstile>In3  ([])                    \<Colon>Ts"
   491 	"E,dt\<Turnstile>In3  (e#es)                  \<Colon>Ts"
   492 	"E,dt\<Turnstile>In1r  Skip                   \<Colon>x"
   493 	"E,dt\<Turnstile>In1r (Expr e)                \<Colon>x"
   494 	"E,dt\<Turnstile>In1r (c1;; c2)               \<Colon>x"
   495         "E,dt\<Turnstile>In1r (l\<bullet> c)                  \<Colon>x" 
   496 	"E,dt\<Turnstile>In1r (If(e) c1 Else c2)      \<Colon>x"
   497 	"E,dt\<Turnstile>In1r (l\<bullet> While(e) c)         \<Colon>x"
   498         "E,dt\<Turnstile>In1r (Do jump)               \<Colon>x"
   499 	"E,dt\<Turnstile>In1r (Throw e)               \<Colon>x"
   500 	"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x"
   501 	"E,dt\<Turnstile>In1r (c1 Finally c2)         \<Colon>x"
   502 	"E,dt\<Turnstile>In1r (Init C)                \<Colon>x"
   503 declare not_None_eq [simp] 
   504 declare split_if [split] split_if_asm [split]
   505 declare split_paired_All [simp] split_paired_Ex [simp]
   506 ML_setup {*
   507 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   508 *}
   509 
   510 lemma is_acc_class_is_accessible: 
   511   "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
   512 by (auto simp add: is_acc_class_def)
   513 
   514 lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
   515 by (auto simp add: is_acc_iface_def)
   516 
   517 lemma is_acc_iface_is_accessible: 
   518   "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
   519 by (auto simp add: is_acc_iface_def)
   520 
   521 lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
   522 by (auto simp add: is_acc_type_def)
   523 
   524 lemma is_acc_iface_is_accessible: "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
   525 by (auto simp add: is_acc_type_def)
   526 
   527 lemma wt_Methd_is_methd: 
   528   "E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig"
   529 apply (erule_tac wt_elim_cases)
   530 apply clarsimp
   531 apply (erule is_methdI, assumption)
   532 done
   533 
   534 (* Special versions of some typing rules, better suited to pattern match the
   535  * conclusion (no selectors in the conclusion\<dots>)
   536  *)
   537 
   538 lemma wt_Super:
   539 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   540   class (prg E) C = Some c;D=super c\<rbrakk> 
   541  \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
   542 by (auto elim: wt.Super)
   543  
   544 
   545 lemma wt_Call: 
   546 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
   547   max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   548     = {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E;
   549  mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
   550 by (auto elim: wt.Call)
   551 
   552 
   553 lemma invocationTypeExpr_noClassD: 
   554 "\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
   555  \<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
   556 proof -
   557   assume wt: "E\<turnstile>e\<Colon>-RefT statT"
   558   show ?thesis
   559   proof (cases "e=Super")
   560     case True
   561     with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
   562     then show ?thesis by blast
   563   next 
   564     case False then show ?thesis 
   565       by (auto simp add: invmode_def split: split_if_asm)
   566   qed
   567 qed
   568 
   569 lemma wt_Super: 
   570 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> 
   571 \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
   572 by (auto elim: wt.Super)
   573 
   574 lemma wt_FVar:	
   575 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f);
   576   sf=is_static f; fT=(type f); accC=cls E\<rbrakk> 
   577 \<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT"
   578 by (auto dest: wt.FVar)
   579 
   580 
   581 lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C"
   582 by (auto elim: wt_elim_cases intro: "wt.Init")
   583 
   584 declare wt.Skip [iff]
   585 
   586 lemma wt_StatRef: 
   587   "is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt"
   588 apply (rule wt.Cast)
   589 apply  (rule wt.Lit)
   590 apply   (simp (no_asm))
   591 apply  (simp (no_asm_simp))
   592 apply (rule cast.widen)
   593 apply (simp (no_asm))
   594 done
   595 
   596 lemma wt_Inj_elim: 
   597   "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of 
   598                        In1 ec \<Rightarrow> (case ec of 
   599                                     Inl e \<Rightarrow> \<exists>T. U=Inl T  
   600                                   | Inr s \<Rightarrow> U=Inl (PrimT Void))  
   601                      | In2 e \<Rightarrow> (\<exists>T. U=Inl T) 
   602                      | In3 e \<Rightarrow> (\<exists>T. U=Inr T)"
   603 apply (erule wt.induct)
   604 apply auto
   605 done
   606 
   607 ML {*
   608 fun wt_fun name inj rhs =
   609 let
   610   val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U"
   611   val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   612 	(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac])
   613   fun is_Inj (Const (inj,_) $ _) = true
   614     | is_Inj _                   = false
   615   fun pred (t as (_ $ (Const ("Pair",_) $
   616      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   617        x))) $ _ )) = is_Inj x
   618 in
   619   make_simproc name lhs pred (thm name)
   620 end
   621 
   622 val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>-T"
   623 val wt_var_proc   = wt_fun "wt_var_eq"   "In2"  "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>=T"
   624 val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3"  "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"
   625 val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>"
   626 *}
   627 
   628 ML {*
   629 Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
   630 *}
   631 
   632 lemma Inj_eq_lemma [simp]: 
   633   "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
   634 by auto
   635 
   636 (* unused *)
   637 lemma single_valued_tys_lemma [rule_format (no_asm)]: 
   638   "\<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>  
   639      G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T  = T')"
   640 apply (cases "E", erule wt.induct)
   641 apply (safe del: disjE)
   642 apply (simp_all (no_asm_use) split del: split_if_asm)
   643 apply (safe del: disjE)
   644 (* 17 subgoals *)
   645 apply (tactic {* ALLGOALS (fn i => if i = 11 then EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i else thin_tac "All ?P" i) *})
   646 (*apply (safe del: disjE elim!: wt_elim_cases)*)
   647 apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
   648 apply (simp_all (no_asm_use) split del: split_if_asm)
   649 apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
   650 apply ((blast del: equalityCE dest: sym [THEN trans])+)
   651 done
   652 
   653 (* unused *)
   654 lemma single_valued_tys: 
   655 "ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
   656 apply (unfold single_valued_def)
   657 apply clarsimp
   658 apply (rule single_valued_tys_lemma)
   659 apply (auto intro!: widen_antisym)
   660 done
   661 
   662 lemma typeof_empty_is_type [rule_format (no_asm)]: 
   663   "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
   664 apply (rule val.induct)
   665 apply    	auto
   666 done
   667 
   668 (* unused *)
   669 lemma typeof_is_type [rule_format (no_asm)]: 
   670  "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
   671 apply (rule val.induct)
   672 prefer 5 
   673 apply     fast
   674 apply  (simp_all (no_asm))
   675 done
   676 
   677 end