src/HOL/Bali/WellType.thy
author schirmer
Thu Oct 31 18:27:10 2002 +0100 (2002-10-31)
changeset 13688 a0b16d42d489
parent 13524 604d0f3622d6
child 14981 e73f8140af78
permissions -rw-r--r--
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
     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 constdefs
   110   --{* applicable methods, cf. 15.11.2.1 *}
   111   appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
   112  "appl_methds G S rt \<equiv> \<lambda> sig. 
   113       {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
   114                            G\<turnstile>(parTs sig)[\<preceq>]pTs'}"
   115 
   116   --{* more specific methods, cf. 15.11.2.2 *}
   117   more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool"
   118  "more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
   119 (*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
   120 
   121   --{* maximally specific methods, cf. 15.11.2.2 *}
   122    max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
   123 
   124  "max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and>
   125 		      (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
   126 
   127 
   128 lemma max_spec2appl_meths: 
   129   "x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" 
   130 by (auto simp: max_spec_def)
   131 
   132 lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow>  
   133    mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   134 by (auto simp: appl_methds_def)
   135 
   136 lemma max_spec2mheads: 
   137 "max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A 
   138  \<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   139 apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD)
   140 done
   141 
   142 
   143 constdefs
   144   empty_dt :: "dyn_ty"
   145  "empty_dt \<equiv> \<lambda>a. None"
   146 
   147   invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode"
   148 "invmode m e \<equiv> if is_static m 
   149                   then Static 
   150                   else if e=Super then SuperM else IntVir"
   151 
   152 lemma invmode_nonstatic [simp]: 
   153   "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
   154 apply (unfold invmode_def)
   155 apply (simp (no_asm) add: member_is_static_simp)
   156 done
   157 
   158 
   159 lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m"
   160 apply (unfold invmode_def)
   161 apply (simp (no_asm))
   162 done
   163 
   164 
   165 lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)"
   166 apply (unfold invmode_def)
   167 apply (simp (no_asm))
   168 done
   169 
   170 lemma Null_staticD: 
   171   "a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
   172 apply (clarsimp simp add: invmode_IntVir_eq)
   173 done
   174 
   175 section "Typing for unary operations"
   176 
   177 consts unop_type :: "unop \<Rightarrow> prim_ty"
   178 primrec 
   179 "unop_type UPlus   = Integer"
   180 "unop_type UMinus  = Integer"
   181 "unop_type UBitNot = Integer"
   182 "unop_type UNot    = Boolean"    
   183 
   184 consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
   185 primrec
   186 "wt_unop UPlus   t = (t = PrimT Integer)"
   187 "wt_unop UMinus  t = (t = PrimT Integer)"
   188 "wt_unop UBitNot t = (t = PrimT Integer)"
   189 "wt_unop UNot    t = (t = PrimT Boolean)"
   190 
   191 section "Typing for binary operations"
   192 
   193 consts binop_type :: "binop \<Rightarrow> prim_ty"
   194 primrec
   195 "binop_type Mul      = Integer"     
   196 "binop_type Div      = Integer"
   197 "binop_type Mod      = Integer"
   198 "binop_type Plus     = Integer"
   199 "binop_type Minus    = Integer"
   200 "binop_type LShift   = Integer"
   201 "binop_type RShift   = Integer"
   202 "binop_type RShiftU  = Integer"
   203 "binop_type Less     = Boolean"
   204 "binop_type Le       = Boolean"
   205 "binop_type Greater  = Boolean"
   206 "binop_type Ge       = Boolean"
   207 "binop_type Eq       = Boolean"
   208 "binop_type Neq      = Boolean"
   209 "binop_type BitAnd   = Integer"
   210 "binop_type And      = Boolean"
   211 "binop_type BitXor   = Integer"
   212 "binop_type Xor      = Boolean"
   213 "binop_type BitOr    = Integer"
   214 "binop_type Or       = Boolean"
   215 "binop_type CondAnd  = Boolean"
   216 "binop_type CondOr   = Boolean"
   217 
   218 consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
   219 primrec
   220 "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   221 "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   222 "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   223 "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   224 "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   225 "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   226 "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   227 "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   228 "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   229 "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   230 "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   231 "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   232 "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
   233 "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
   234 "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   235 "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   236 "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   237 "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   238 "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   239 "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   240 "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   241 "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   242 
   243 section "Typing for terms"
   244 
   245 types tys  =        "ty + ty list"
   246 translations
   247   "tys"   <= (type) "ty + ty list"
   248 
   249 consts
   250   wt    :: "(env\<spacespace> \<times> dyn_ty\<spacespace> \<times>  term \<times> tys) set"
   251 (*wt    :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term \<times> tys) set" not feasible because of 
   252 					      \<spacespace>  changing env in Try stmt *)
   253 
   254 syntax
   255 wt      :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys]  \<Rightarrow> bool" ("_,_|=_::_" [51,51,51,51] 50)
   256 wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_|=_:<>" [51,51,51   ] 50)
   257 ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_|=_:-_" [51,51,51,51] 50)
   258 ty_var  :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_|=_:=_" [51,51,51,51] 50)
   259 ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
   260 	         \<spacespace>        \<spacespace>  ty   list] \<Rightarrow> bool" ("_,_|=_:#_" [51,51,51,51] 50)
   261 
   262 syntax (xsymbols)
   263 wt      :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
   264 wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
   265 ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
   266 ty_var  :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
   267 ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
   268 		  \<spacespace>        \<spacespace>  ty   list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
   269 
   270 translations
   271 	"E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt"
   272 	"E,dt\<Turnstile>s\<Colon>\<surd>"  == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
   273 	"E,dt\<Turnstile>e\<Colon>-T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T"
   274 	"E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2  e\<Colon>Inl T"
   275 	"E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3  e\<Colon>Inr T"
   276 
   277 syntax (* for purely static typing *)
   278   wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
   279   wt_stmt_ :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
   280   ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
   281   ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
   282   ty_exprs_:: "env \<Rightarrow> [expr list,
   283 		     \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
   284 
   285 syntax (xsymbols)
   286   wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
   287   wt_stmt_ ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
   288   ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
   289   ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
   290   ty_exprs_ :: "env \<Rightarrow> [expr list,
   291 		    \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
   292 
   293 translations
   294 	"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
   295         "E\<turnstile>s\<Colon>\<surd>"  == "E\<turnstile>In1r s\<Colon>Inl (PrimT Void)"
   296 	"E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>Inl T"
   297 	"E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>Inl T"
   298 	"E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>Inr T"
   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   Jmp:                                   "E,dt\<Turnstile>Jmp 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   --{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
   348      The class isn't necessarily accessible from the points @{term Init} 
   349      is called. Therefor we only demand @{term is_class} and not 
   350      @{term is_acc_class} here. 
   351    *}
   352 
   353 --{* well-typed expressions *}
   354 
   355   --{* cf. 15.8 *}
   356   NewC:	"\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
   357 					 E,dt\<Turnstile>NewC C\<Colon>-Class C"
   358   --{* cf. 15.9 *}
   359   NewA:	"\<lbrakk>is_acc_type (prg E) (pkg E) T;
   360 	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   361 					 E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
   362 
   363   --{* cf. 15.15 *}
   364   Cast:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
   365 	  prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
   366 					 E,dt\<Turnstile>Cast T' e\<Colon>-T'"
   367 
   368   --{* cf. 15.19.2 *}
   369   Inst:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
   370 	  prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
   371 					 E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
   372 
   373   --{* cf. 15.7.1 *}
   374   Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
   375 					 E,dt\<Turnstile>Lit x\<Colon>-T"
   376 
   377   UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
   378           \<Longrightarrow>
   379 	  E,dt\<Turnstile>UnOp unop e\<Colon>-T"
   380   
   381   BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
   382            T=PrimT (binop_type binop)\<rbrakk> 
   383            \<Longrightarrow>
   384 	   E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
   385   
   386   --{* cf. 15.10.2, 15.11.1 *}
   387   Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   388 	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
   389 					 E,dt\<Turnstile>Super\<Colon>-Class (super c)"
   390 
   391   --{* cf. 15.13.1, 15.10.1, 15.12 *}
   392   Acc:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
   393 					 E,dt\<Turnstile>Acc va\<Colon>-T"
   394 
   395   --{* cf. 15.25, 15.25.1 *}
   396   Ass:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
   397 	  E,dt\<Turnstile>v \<Colon>-T';
   398 	  prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
   399 					 E,dt\<Turnstile>va:=v\<Colon>-T'"
   400 
   401   --{* cf. 15.24 *}
   402   Cond:	"\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
   403 	  E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
   404 	  prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
   405 					 E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
   406 
   407   --{* cf. 15.11.1, 15.11.2, 15.11.3 *}
   408   Call:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
   409 	  E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
   410 	  max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   411             = {((statDeclT,m),pTs')}
   412          \<rbrakk> \<Longrightarrow>
   413 		   E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
   414 
   415   Methd: "\<lbrakk>is_class (prg E) C;
   416 	  methd (prg E) C sig = Some m;
   417 	  E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
   418 					 E,dt\<Turnstile>Methd C sig\<Colon>-T"
   419  --{* The class @{term C} is the dynamic class of the method call 
   420     (cf. Eval.thy). 
   421     It hasn't got to be directly accessible from the current package 
   422     @{term "(pkg E)"}. 
   423     Only the static class must be accessible (enshured indirectly by 
   424     @{term Call}). 
   425     Note that l is just a dummy value. It is only used in the smallstep 
   426     semantics. To proof typesafety directly for the smallstep semantics 
   427     we would have to assume conformance of l here!
   428   *}
   429 
   430   Body:	"\<lbrakk>is_class (prg E) D;
   431 	  E,dt\<Turnstile>blk\<Colon>\<surd>;
   432 	  (lcl E) Result = Some T;
   433           is_type (prg E) T\<rbrakk> \<Longrightarrow>
   434    					 E,dt\<Turnstile>Body D blk\<Colon>-T"
   435 --{* The class @{term D} implementing the method must not directly be 
   436      accessible  from the current package @{term "(pkg E)"}, but can also 
   437      be indirectly accessible due to inheritance (enshured in @{term Call})
   438     The result type hasn't got to be accessible in Java! (If it is not 
   439     accessible you can only assign it to Object).
   440     For dummy value l see rule @{term Methd}. 
   441    *}
   442 
   443 --{* well-typed variables *}
   444 
   445   --{* cf. 15.13.1 *}
   446   LVar:	"\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
   447 					 E,dt\<Turnstile>LVar vn\<Colon>=T"
   448   --{* cf. 15.10.1 *}
   449   FVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
   450 	  accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
   451 			 E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
   452   --{* cf. 15.12 *}
   453   AVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
   454 	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   455 					 E,dt\<Turnstile>e.[i]\<Colon>=T"
   456 
   457 
   458 --{* well-typed expression lists *}
   459 
   460   --{* cf. 15.11.??? *}
   461   Nil:					"E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
   462 
   463   --{* cf. 15.11.??? *}
   464   Cons:	"\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
   465 	  E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
   466 					 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
   467 
   468 
   469 declare not_None_eq [simp del] 
   470 declare split_if [split del] split_if_asm [split del]
   471 declare split_paired_All [simp del] split_paired_Ex [simp del]
   472 ML_setup {*
   473 simpset_ref() := simpset() delloop "split_all_tac"
   474 *}
   475 
   476 inductive_cases wt_elim_cases [cases set]:
   477 	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
   478 	"E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
   479 	"E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
   480 	"E,dt\<Turnstile>In1l (NewC C)                \<Colon>T"
   481 	"E,dt\<Turnstile>In1l (New T'[i])             \<Colon>T"
   482 	"E,dt\<Turnstile>In1l (Cast T' e)             \<Colon>T"
   483 	"E,dt\<Turnstile>In1l (e InstOf T')           \<Colon>T"
   484 	"E,dt\<Turnstile>In1l (Lit x)                 \<Colon>T"
   485         "E,dt\<Turnstile>In1l (UnOp unop e)           \<Colon>T"
   486         "E,dt\<Turnstile>In1l (BinOp binop e1 e2)     \<Colon>T"
   487 	"E,dt\<Turnstile>In1l (Super)                 \<Colon>T"
   488 	"E,dt\<Turnstile>In1l (Acc va)                \<Colon>T"
   489 	"E,dt\<Turnstile>In1l (Ass va v)              \<Colon>T"
   490 	"E,dt\<Turnstile>In1l (e0 ? e1 : e2)          \<Colon>T"
   491 	"E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
   492 	"E,dt\<Turnstile>In1l (Methd C sig)           \<Colon>T"
   493 	"E,dt\<Turnstile>In1l (Body D blk)            \<Colon>T"
   494 	"E,dt\<Turnstile>In3  ([])                    \<Colon>Ts"
   495 	"E,dt\<Turnstile>In3  (e#es)                  \<Colon>Ts"
   496 	"E,dt\<Turnstile>In1r  Skip                   \<Colon>x"
   497 	"E,dt\<Turnstile>In1r (Expr e)                \<Colon>x"
   498 	"E,dt\<Turnstile>In1r (c1;; c2)               \<Colon>x"
   499         "E,dt\<Turnstile>In1r (l\<bullet> c)                  \<Colon>x" 
   500 	"E,dt\<Turnstile>In1r (If(e) c1 Else c2)      \<Colon>x"
   501 	"E,dt\<Turnstile>In1r (l\<bullet> While(e) c)         \<Colon>x"
   502         "E,dt\<Turnstile>In1r (Jmp jump)              \<Colon>x"
   503 	"E,dt\<Turnstile>In1r (Throw e)               \<Colon>x"
   504 	"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x"
   505 	"E,dt\<Turnstile>In1r (c1 Finally c2)         \<Colon>x"
   506 	"E,dt\<Turnstile>In1r (Init C)                \<Colon>x"
   507 declare not_None_eq [simp] 
   508 declare split_if [split] split_if_asm [split]
   509 declare split_paired_All [simp] split_paired_Ex [simp]
   510 ML_setup {*
   511 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   512 *}
   513 
   514 lemma is_acc_class_is_accessible: 
   515   "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
   516 by (auto simp add: is_acc_class_def)
   517 
   518 lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
   519 by (auto simp add: is_acc_iface_def)
   520 
   521 lemma is_acc_iface_Iface_is_accessible: 
   522   "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
   523 by (auto simp add: is_acc_iface_def)
   524 
   525 lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
   526 by (auto simp add: is_acc_type_def)
   527 
   528 lemma is_acc_iface_is_accessible:
   529   "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
   530 by (auto simp add: is_acc_type_def)
   531 
   532 lemma wt_Methd_is_methd: 
   533   "E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig"
   534 apply (erule_tac wt_elim_cases)
   535 apply clarsimp
   536 apply (erule is_methdI, assumption)
   537 done
   538 
   539 
   540 text {* Special versions of some typing rules, better suited to pattern 
   541         match the conclusion (no selectors in the conclusion)
   542 *}
   543 
   544 lemma wt_Call: 
   545 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
   546   max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   547     = {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E;
   548  mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
   549 by (auto elim: wt.Call)
   550 
   551 
   552 lemma invocationTypeExpr_noClassD: 
   553 "\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
   554  \<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
   555 proof -
   556   assume wt: "E\<turnstile>e\<Colon>-RefT statT"
   557   show ?thesis
   558   proof (cases "e=Super")
   559     case True
   560     with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
   561     then show ?thesis by blast
   562   next 
   563     case False then show ?thesis 
   564       by (auto simp add: invmode_def split: split_if_asm)
   565   qed
   566 qed
   567 
   568 lemma wt_Super: 
   569 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> 
   570 \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
   571 by (auto elim: wt.Super)
   572 
   573 lemma wt_FVar:	
   574 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f);
   575   sf=is_static f; fT=(type f); accC=cls E\<rbrakk> 
   576 \<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT"
   577 by (auto dest: wt.FVar)
   578 
   579 
   580 lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C"
   581 by (auto elim: wt_elim_cases intro: "wt.Init")
   582 
   583 declare wt.Skip [iff]
   584 
   585 lemma wt_StatRef: 
   586   "is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt"
   587 apply (rule wt.Cast)
   588 apply  (rule wt.Lit)
   589 apply   (simp (no_asm))
   590 apply  (simp (no_asm_simp))
   591 apply (rule cast.widen)
   592 apply (simp (no_asm))
   593 done
   594 
   595 lemma wt_Inj_elim: 
   596   "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of 
   597                        In1 ec \<Rightarrow> (case ec of 
   598                                     Inl e \<Rightarrow> \<exists>T. U=Inl T  
   599                                   | Inr s \<Rightarrow> U=Inl (PrimT Void))  
   600                      | In2 e \<Rightarrow> (\<exists>T. U=Inl T) 
   601                      | In3 e \<Rightarrow> (\<exists>T. U=Inr T)"
   602 apply (erule wt.induct)
   603 apply auto
   604 done
   605 
   606 --{* In the special syntax to distinguish the typing judgements for expressions, 
   607      statements, variables and expression lists the kind of term corresponds
   608      to the kind of type in the end e.g. An statement (injection @{term In3} 
   609     into terms, always has type void (injection @{term Inl} into the generalised
   610     types. The following simplification procedures establish these kinds of
   611     correlation. 
   612  *}
   613 
   614 ML {*
   615 fun wt_fun name inj rhs =
   616 let
   617   val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U"
   618   val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   619 	(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac])
   620   fun is_Inj (Const (inj,_) $ _) = true
   621     | is_Inj _                   = false
   622   fun pred (t as (_ $ (Const ("Pair",_) $
   623      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   624        x))) $ _ )) = is_Inj x
   625 in
   626   cond_simproc name lhs pred (thm name)
   627 end
   628 
   629 val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>-T"
   630 val wt_var_proc   = wt_fun "wt_var_eq"   "In2"  "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>=T"
   631 val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3"  "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"
   632 val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>"
   633 *}
   634 
   635 ML {*
   636 Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
   637 *}
   638 
   639 lemma wt_elim_BinOp:
   640   "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
   641     \<And>T1 T2 T3.
   642        \<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2;
   643           E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3;
   644           T = Inl (PrimT (binop_type binop))\<rbrakk>
   645        \<Longrightarrow> P\<rbrakk>
   646 \<Longrightarrow> P"
   647 apply (erule wt_elim_cases)
   648 apply (cases b)
   649 apply auto
   650 done
   651 
   652 lemma Inj_eq_lemma [simp]: 
   653   "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
   654 by auto
   655 
   656 (* unused *)
   657 lemma single_valued_tys_lemma [rule_format (no_asm)]: 
   658   "\<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>  
   659      G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T  = T')"
   660 apply (cases "E", erule wt.induct)
   661 apply (safe del: disjE)
   662 apply (simp_all (no_asm_use) split del: split_if_asm)
   663 apply (safe del: disjE)
   664 (* 17 subgoals *)
   665 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) *})
   666 (*apply (safe del: disjE elim!: wt_elim_cases)*)
   667 apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
   668 apply (simp_all (no_asm_use) split del: split_if_asm)
   669 apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
   670 apply ((blast del: equalityCE dest: sym [THEN trans])+)
   671 done
   672 
   673 (* unused *)
   674 lemma single_valued_tys: 
   675 "ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
   676 apply (unfold single_valued_def)
   677 apply clarsimp
   678 apply (rule single_valued_tys_lemma)
   679 apply (auto intro!: widen_antisym)
   680 done
   681 
   682 lemma typeof_empty_is_type [rule_format (no_asm)]: 
   683   "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
   684 apply (rule val.induct)
   685 apply    	auto
   686 done
   687 
   688 (* unused *)
   689 lemma typeof_is_type [rule_format (no_asm)]: 
   690  "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
   691 apply (rule val.induct)
   692 prefer 5 
   693 apply     fast
   694 apply  (simp_all (no_asm))
   695 done
   696 
   697 end