src/HOL/Bali/WellType.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 17876 b9c92f384109
child 21765 89275a3ed7be
permissions -rw-r--r--
simplified code generator setup
     1 (*  Title:      HOL/Bali/WellType.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4 *)
     5 header {* Well-typedness of Java programs *}
     6 
     7 theory WellType imports DeclConcepts begin
     8 
     9 text {*
    10 improvements over Java Specification 1.0:
    11 \begin{itemize}
    12 \item methods of Object can be called upon references of interface or array type
    13 \end{itemize}
    14 simplifications:
    15 \begin{itemize}
    16 \item the type rules include all static checks on statements and expressions, 
    17       e.g. definedness of names (of parameters, locals, fields, methods)
    18 \end{itemize}
    19 design issues:
    20 \begin{itemize}
    21 \item unified type judgment for statements, variables, expressions, 
    22       expression lists
    23 \item statements are typed like expressions with dummy type Void
    24 \item the typing rules take an extra argument that is capable of determining 
    25   the dynamic type of objects. Therefore, they can be used for both 
    26   checking static types and determining runtime types in transition semantics.
    27 \end{itemize}
    28 *}
    29 
    30 types	lenv
    31 	= "(lname, ty) table"  --{* local variables, including This and Result*}
    32 
    33 record env = 
    34          prg:: "prog"    --{* program *}
    35          cls:: "qtname"  --{* current package and class name *}
    36          lcl:: "lenv"    --{* local environment *}     
    37   
    38 translations
    39   "lenv" <= (type) "(lname, ty) table"
    40   "lenv" <= (type) "lname \<Rightarrow> ty option"
    41   "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
    42   "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
    43 
    44 
    45 
    46 syntax
    47   pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
    48 translations 
    49   "pkg e" == "pid (cls e)"
    50 
    51 section "Static overloading: maximally specific methods "
    52 
    53 types
    54   emhead = "ref_ty \<times> mhead"
    55 
    56 --{* Some mnemotic selectors for emhead *}
    57 constdefs 
    58   "declrefT" :: "emhead \<Rightarrow> ref_ty"
    59   "declrefT \<equiv> fst"
    60 
    61   "mhd"     :: "emhead \<Rightarrow> mhead"
    62   "mhd \<equiv> snd"
    63 
    64 lemma declrefT_simp[simp]:"declrefT (r,m) = r"
    65 by (simp add: declrefT_def)
    66 
    67 lemma mhd_simp[simp]:"mhd (r,m) = m"
    68 by (simp add: mhd_def)
    69 
    70 lemma static_mhd_simp[simp]: "static (mhd m) = is_static m"
    71 by (cases m) (simp add: member_is_static_simp mhd_def)
    72 
    73 lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m"
    74 by (cases m) simp
    75 
    76 lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m"
    77 by (cases m) simp
    78 
    79 lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
    80 by (cases m) simp
    81 
    82 consts
    83   cmheads        :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
    84   Objectmheads   :: "prog \<Rightarrow> qtname           \<Rightarrow> sig \<Rightarrow> emhead set"
    85   accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
    86   mheads         :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
    87 defs
    88  cmheads_def:
    89 "cmheads G S C 
    90   \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` o2s (accmethd G S C sig)"
    91   Objectmheads_def:
    92 "Objectmheads G S  
    93   \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
    94     ` o2s (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
    95   accObjectmheads_def:
    96 "accObjectmheads G S T
    97    \<equiv> if G\<turnstile>RefT T accessible_in (pid S)
    98         then Objectmheads G S
    99         else \<lambda>sig. {}"
   100 primrec
   101 "mheads G S  NullT     = (\<lambda>sig. {})"
   102 "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 
   103                          ` accimethds G (pid S) I sig \<union> 
   104                            accObjectmheads G S (IfaceT I) sig)"
   105 "mheads G S (ClassT C) = cmheads G S C"
   106 "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
   107 
   108 constdefs
   109   --{* applicable methods, cf. 15.11.2.1 *}
   110   appl_methds   :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
   111  "appl_methds G S rt \<equiv> \<lambda> sig. 
   112       {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
   113                            G\<turnstile>(parTs sig)[\<preceq>]pTs'}"
   114 
   115   --{* more specific methods, cf. 15.11.2.2 *}
   116   more_spec     :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool"
   117  "more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
   118 (*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'*)
   119 
   120   --{* maximally specific methods, cf. 15.11.2.2 *}
   121    max_spec     :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
   122 
   123  "max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and>
   124 		      (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
   125 
   126 
   127 lemma max_spec2appl_meths: 
   128   "x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" 
   129 by (auto simp: max_spec_def)
   130 
   131 lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow>  
   132    mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   133 by (auto simp: appl_methds_def)
   134 
   135 lemma max_spec2mheads: 
   136 "max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A 
   137  \<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   138 apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD)
   139 done
   140 
   141 
   142 constdefs
   143   empty_dt :: "dyn_ty"
   144  "empty_dt \<equiv> \<lambda>a. None"
   145 
   146   invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode"
   147 "invmode m e \<equiv> if is_static m 
   148                   then Static 
   149                   else if e=Super then SuperM else IntVir"
   150 
   151 lemma invmode_nonstatic [simp]: 
   152   "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
   153 apply (unfold invmode_def)
   154 apply (simp (no_asm) add: member_is_static_simp)
   155 done
   156 
   157 
   158 lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m"
   159 apply (unfold invmode_def)
   160 apply (simp (no_asm))
   161 done
   162 
   163 
   164 lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)"
   165 apply (unfold invmode_def)
   166 apply (simp (no_asm))
   167 done
   168 
   169 lemma Null_staticD: 
   170   "a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
   171 apply (clarsimp simp add: invmode_IntVir_eq)
   172 done
   173 
   174 section "Typing for unary operations"
   175 
   176 consts unop_type :: "unop \<Rightarrow> prim_ty"
   177 primrec 
   178 "unop_type UPlus   = Integer"
   179 "unop_type UMinus  = Integer"
   180 "unop_type UBitNot = Integer"
   181 "unop_type UNot    = Boolean"    
   182 
   183 consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
   184 primrec
   185 "wt_unop UPlus   t = (t = PrimT Integer)"
   186 "wt_unop UMinus  t = (t = PrimT Integer)"
   187 "wt_unop UBitNot t = (t = PrimT Integer)"
   188 "wt_unop UNot    t = (t = PrimT Boolean)"
   189 
   190 section "Typing for binary operations"
   191 
   192 consts binop_type :: "binop \<Rightarrow> prim_ty"
   193 primrec
   194 "binop_type Mul      = Integer"     
   195 "binop_type Div      = Integer"
   196 "binop_type Mod      = Integer"
   197 "binop_type Plus     = Integer"
   198 "binop_type Minus    = Integer"
   199 "binop_type LShift   = Integer"
   200 "binop_type RShift   = Integer"
   201 "binop_type RShiftU  = Integer"
   202 "binop_type Less     = Boolean"
   203 "binop_type Le       = Boolean"
   204 "binop_type Greater  = Boolean"
   205 "binop_type Ge       = Boolean"
   206 "binop_type Eq       = Boolean"
   207 "binop_type Neq      = Boolean"
   208 "binop_type BitAnd   = Integer"
   209 "binop_type And      = Boolean"
   210 "binop_type BitXor   = Integer"
   211 "binop_type Xor      = Boolean"
   212 "binop_type BitOr    = Integer"
   213 "binop_type Or       = Boolean"
   214 "binop_type CondAnd  = Boolean"
   215 "binop_type CondOr   = Boolean"
   216 
   217 consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
   218 primrec
   219 "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   220 "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   221 "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   222 "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   223 "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   224 "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   225 "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   226 "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   227 "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   228 "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   229 "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   230 "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   231 "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
   232 "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
   233 "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   234 "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   235 "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   236 "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   237 "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   238 "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   239 "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   240 "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   241 
   242 section "Typing for terms"
   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\<turnstile>In1r s\<Colon>Inl (PrimT Void)"
   295 	"E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>Inl T"
   296 	"E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>Inl T"
   297 	"E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>Inr T"
   298 
   299 
   300 inductive wt intros 
   301 
   302 
   303 --{* well-typed statements *}
   304 
   305   Skip:					"E,dt\<Turnstile>Skip\<Colon>\<surd>"
   306 
   307   Expr:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
   308 					 E,dt\<Turnstile>Expr e\<Colon>\<surd>"
   309   --{* cf. 14.6 *}
   310   Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
   311                                          E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
   312 
   313   Comp:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
   314 	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   315 					 E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
   316 
   317   --{* cf. 14.8 *}
   318   If:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   319 	  E,dt\<Turnstile>c1\<Colon>\<surd>;
   320 	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   321 					 E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
   322 
   323   --{* cf. 14.10 *}
   324   Loop:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   325 	  E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   326 					 E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
   327   --{* cf. 14.13, 14.15, 14.16 *}
   328   Jmp:                                   "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>"
   329 
   330   --{* cf. 14.16 *}
   331   Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
   332 	  prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
   333 					 E,dt\<Turnstile>Throw e\<Colon>\<surd>"
   334   --{* cf. 14.18 *}
   335   Try:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
   336 	  lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
   337           \<Longrightarrow>
   338 					 E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
   339 
   340   --{* cf. 14.18 *}
   341   Fin:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   342 					 E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
   343 
   344   Init:	"\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
   345 					 E,dt\<Turnstile>Init C\<Colon>\<surd>"
   346   --{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
   347      The class isn't necessarily accessible from the points @{term Init} 
   348      is called. Therefor we only demand @{term is_class} and not 
   349      @{term 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 @{term C} is the dynamic class of the method call 
   419     (cf. Eval.thy). 
   420     It hasn't got to be directly accessible from the current package 
   421     @{term "(pkg E)"}. 
   422     Only the static class must be accessible (enshured indirectly by 
   423     @{term Call}). 
   424     Note that l is just a dummy value. It is only used in the smallstep 
   425     semantics. To proof typesafety directly for the smallstep semantics 
   426     we would have to assume conformance of l here!
   427   *}
   428 
   429   Body:	"\<lbrakk>is_class (prg E) D;
   430 	  E,dt\<Turnstile>blk\<Colon>\<surd>;
   431 	  (lcl E) Result = Some T;
   432           is_type (prg E) T\<rbrakk> \<Longrightarrow>
   433    					 E,dt\<Turnstile>Body D blk\<Colon>-T"
   434 --{* The class @{term D} implementing the method must not directly be 
   435      accessible  from the current package @{term "(pkg E)"}, but can also 
   436      be indirectly accessible due to inheritance (enshured in @{term Call})
   437     The result type hasn't got to be accessible in Java! (If it is not 
   438     accessible you can only assign it to Object).
   439     For dummy value l see rule @{term Methd}. 
   440    *}
   441 
   442 --{* well-typed variables *}
   443 
   444   --{* cf. 15.13.1 *}
   445   LVar:	"\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
   446 					 E,dt\<Turnstile>LVar vn\<Colon>=T"
   447   --{* cf. 15.10.1 *}
   448   FVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
   449 	  accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
   450 			 E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
   451   --{* cf. 15.12 *}
   452   AVar:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
   453 	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   454 					 E,dt\<Turnstile>e.[i]\<Colon>=T"
   455 
   456 
   457 --{* well-typed expression lists *}
   458 
   459   --{* cf. 15.11.??? *}
   460   Nil:					"E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
   461 
   462   --{* cf. 15.11.??? *}
   463   Cons:	"\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
   464 	  E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
   465 					 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
   466 
   467 
   468 declare not_None_eq [simp del] 
   469 declare split_if [split del] split_if_asm [split del]
   470 declare split_paired_All [simp del] split_paired_Ex [simp del]
   471 ML_setup {*
   472 change_simpset (fn ss => ss delloop "split_all_tac")
   473 *}
   474 
   475 inductive_cases wt_elim_cases [cases set]:
   476 	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
   477 	"E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
   478 	"E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
   479 	"E,dt\<Turnstile>In1l (NewC C)                \<Colon>T"
   480 	"E,dt\<Turnstile>In1l (New T'[i])             \<Colon>T"
   481 	"E,dt\<Turnstile>In1l (Cast T' e)             \<Colon>T"
   482 	"E,dt\<Turnstile>In1l (e InstOf T')           \<Colon>T"
   483 	"E,dt\<Turnstile>In1l (Lit x)                 \<Colon>T"
   484         "E,dt\<Turnstile>In1l (UnOp unop e)           \<Colon>T"
   485         "E,dt\<Turnstile>In1l (BinOp binop e1 e2)     \<Colon>T"
   486 	"E,dt\<Turnstile>In1l (Super)                 \<Colon>T"
   487 	"E,dt\<Turnstile>In1l (Acc va)                \<Colon>T"
   488 	"E,dt\<Turnstile>In1l (Ass va v)              \<Colon>T"
   489 	"E,dt\<Turnstile>In1l (e0 ? e1 : e2)          \<Colon>T"
   490 	"E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
   491 	"E,dt\<Turnstile>In1l (Methd C sig)           \<Colon>T"
   492 	"E,dt\<Turnstile>In1l (Body D blk)            \<Colon>T"
   493 	"E,dt\<Turnstile>In3  ([])                    \<Colon>Ts"
   494 	"E,dt\<Turnstile>In3  (e#es)                  \<Colon>Ts"
   495 	"E,dt\<Turnstile>In1r  Skip                   \<Colon>x"
   496 	"E,dt\<Turnstile>In1r (Expr e)                \<Colon>x"
   497 	"E,dt\<Turnstile>In1r (c1;; c2)               \<Colon>x"
   498         "E,dt\<Turnstile>In1r (l\<bullet> c)                  \<Colon>x" 
   499 	"E,dt\<Turnstile>In1r (If(e) c1 Else c2)      \<Colon>x"
   500 	"E,dt\<Turnstile>In1r (l\<bullet> While(e) c)         \<Colon>x"
   501         "E,dt\<Turnstile>In1r (Jmp jump)              \<Colon>x"
   502 	"E,dt\<Turnstile>In1r (Throw e)               \<Colon>x"
   503 	"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x"
   504 	"E,dt\<Turnstile>In1r (c1 Finally c2)         \<Colon>x"
   505 	"E,dt\<Turnstile>In1r (Init C)                \<Colon>x"
   506 declare not_None_eq [simp] 
   507 declare split_if [split] split_if_asm [split]
   508 declare split_paired_All [simp] split_paired_Ex [simp]
   509 ML_setup {*
   510 change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
   511 *}
   512 
   513 lemma is_acc_class_is_accessible: 
   514   "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
   515 by (auto simp add: is_acc_class_def)
   516 
   517 lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
   518 by (auto simp add: is_acc_iface_def)
   519 
   520 lemma is_acc_iface_Iface_is_accessible: 
   521   "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
   522 by (auto simp add: is_acc_iface_def)
   523 
   524 lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
   525 by (auto simp add: is_acc_type_def)
   526 
   527 lemma is_acc_iface_is_accessible:
   528   "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
   529 by (auto simp add: is_acc_type_def)
   530 
   531 lemma wt_Methd_is_methd: 
   532   "E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig"
   533 apply (erule_tac wt_elim_cases)
   534 apply clarsimp
   535 apply (erule is_methdI, assumption)
   536 done
   537 
   538 
   539 text {* Special versions of some typing rules, better suited to pattern 
   540         match the conclusion (no selectors in the conclusion)
   541 *}
   542 
   543 lemma wt_Call: 
   544 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
   545   max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   546     = {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E;
   547  mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
   548 by (auto elim: wt.Call)
   549 
   550 
   551 lemma invocationTypeExpr_noClassD: 
   552 "\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
   553  \<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
   554 proof -
   555   assume wt: "E\<turnstile>e\<Colon>-RefT statT"
   556   show ?thesis
   557   proof (cases "e=Super")
   558     case True
   559     with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
   560     then show ?thesis by blast
   561   next 
   562     case False then show ?thesis 
   563       by (auto simp add: invmode_def split: split_if_asm)
   564   qed
   565 qed
   566 
   567 lemma wt_Super: 
   568 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> 
   569 \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
   570 by (auto elim: wt.Super)
   571 
   572 lemma wt_FVar:	
   573 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f);
   574   sf=is_static f; fT=(type f); accC=cls E\<rbrakk> 
   575 \<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT"
   576 by (auto dest: wt.FVar)
   577 
   578 
   579 lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C"
   580 by (auto elim: wt_elim_cases intro: "wt.Init")
   581 
   582 declare wt.Skip [iff]
   583 
   584 lemma wt_StatRef: 
   585   "is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt"
   586 apply (rule wt.Cast)
   587 apply  (rule wt.Lit)
   588 apply   (simp (no_asm))
   589 apply  (simp (no_asm_simp))
   590 apply (rule cast.widen)
   591 apply (simp (no_asm))
   592 done
   593 
   594 lemma wt_Inj_elim: 
   595   "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of 
   596                        In1 ec \<Rightarrow> (case ec of 
   597                                     Inl e \<Rightarrow> \<exists>T. U=Inl T  
   598                                   | Inr s \<Rightarrow> U=Inl (PrimT Void))  
   599                      | In2 e \<Rightarrow> (\<exists>T. U=Inl T) 
   600                      | In3 e \<Rightarrow> (\<exists>T. U=Inr T)"
   601 apply (erule wt.induct)
   602 apply auto
   603 done
   604 
   605 --{* In the special syntax to distinguish the typing judgements for expressions, 
   606      statements, variables and expression lists the kind of term corresponds
   607      to the kind of type in the end e.g. An statement (injection @{term In3} 
   608     into terms, always has type void (injection @{term Inl} into the generalised
   609     types. The following simplification procedures establish these kinds of
   610     correlation. 
   611  *}
   612 
   613 ML {*
   614 fun wt_fun name inj rhs =
   615 let
   616   val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U"
   617   val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   618 	(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac])
   619   fun is_Inj (Const (inj,_) $ _) = true
   620     | is_Inj _                   = false
   621   fun pred (t as (_ $ (Const ("Pair",_) $
   622      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   623        x))) $ _ )) = is_Inj x
   624 in
   625   cond_simproc name lhs pred (thm name)
   626 end
   627 
   628 val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>-T"
   629 val wt_var_proc   = wt_fun "wt_var_eq"   "In2"  "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>=T"
   630 val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3"  "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"
   631 val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>"
   632 *}
   633 
   634 ML {*
   635 Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
   636 *}
   637 
   638 lemma wt_elim_BinOp:
   639   "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
   640     \<And>T1 T2 T3.
   641        \<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2;
   642           E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3;
   643           T = Inl (PrimT (binop_type binop))\<rbrakk>
   644        \<Longrightarrow> P\<rbrakk>
   645 \<Longrightarrow> P"
   646 apply (erule wt_elim_cases)
   647 apply (cases b)
   648 apply auto
   649 done
   650 
   651 lemma Inj_eq_lemma [simp]: 
   652   "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
   653 by auto
   654 
   655 (* unused *)
   656 lemma single_valued_tys_lemma [rule_format (no_asm)]: 
   657   "\<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>  
   658      G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T  = T')"
   659 apply (cases "E", erule wt.induct)
   660 apply (safe del: disjE)
   661 apply (simp_all (no_asm_use) split del: split_if_asm)
   662 apply (safe del: disjE)
   663 (* 17 subgoals *)
   664 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) *})
   665 (*apply (safe del: disjE elim!: wt_elim_cases)*)
   666 apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
   667 apply (simp_all (no_asm_use) split del: split_if_asm)
   668 apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
   669 apply ((blast del: equalityCE dest: sym [THEN trans])+)
   670 done
   671 
   672 (* unused *)
   673 lemma single_valued_tys: 
   674 "ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
   675 apply (unfold single_valued_def)
   676 apply clarsimp
   677 apply (rule single_valued_tys_lemma)
   678 apply (auto intro!: widen_antisym)
   679 done
   680 
   681 lemma typeof_empty_is_type [rule_format (no_asm)]: 
   682   "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
   683 apply (rule val.induct)
   684 apply    	auto
   685 done
   686 
   687 (* unused *)
   688 lemma typeof_is_type [rule_format (no_asm)]: 
   689  "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
   690 apply (rule val.induct)
   691 prefer 5 
   692 apply     fast
   693 apply  (simp_all (no_asm))
   694 done
   695 
   696 end