src/HOL/Bali/WellType.thy
author berghofe
Mon Sep 30 16:14:02 2002 +0200 (2002-09-30)
changeset 13601 fd3e3d6b37b2
parent 13524 604d0f3622d6
child 13688 a0b16d42d489
permissions -rw-r--r--
Adapted to new simplifier.
     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 "binop_type CondAnd  = Boolean"
   220 "binop_type CondOr   = Boolean"
   221 
   222 consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
   223 primrec
   224 "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   225 "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   226 "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   227 "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   228 "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   229 "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   230 "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   231 "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   232 "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   233 "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   234 "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   235 "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   236 "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
   237 "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
   238 "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   239 "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   240 "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   241 "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   242 "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   243 "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   244 "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   245 "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   246 
   247 
   248 types tys  =        "ty + ty list"
   249 translations
   250   "tys"   <= (type) "ty + ty list"
   251 
   252 consts
   253   wt    :: "(env\<spacespace> \<times> dyn_ty\<spacespace> \<times>  term \<times> tys) set"
   254 (*wt    :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term \<times> tys) set" not feasible because of 
   255 					      \<spacespace>  changing env in Try stmt *)
   256 
   257 syntax
   258 wt      :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys]  \<Rightarrow> bool" ("_,_|=_::_" [51,51,51,51] 50)
   259 wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_|=_:<>" [51,51,51   ] 50)
   260 ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_|=_:-_" [51,51,51,51] 50)
   261 ty_var  :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_|=_:=_" [51,51,51,51] 50)
   262 ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
   263 	         \<spacespace>        \<spacespace>  ty   list] \<Rightarrow> bool" ("_,_|=_:#_" [51,51,51,51] 50)
   264 
   265 syntax (xsymbols)
   266 wt      :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
   267 wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51   ] 50)
   268 ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
   269 ty_var  :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
   270 ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
   271 		  \<spacespace>        \<spacespace>  ty   list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
   272 
   273 translations
   274 	"E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt"
   275 	"E,dt\<Turnstile>s\<Colon>\<surd>"  == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
   276 	"E,dt\<Turnstile>e\<Colon>-T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T"
   277 	"E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2  e\<Colon>Inl T"
   278 	"E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3  e\<Colon>Inr T"
   279 
   280 syntax (* for purely static typing *)
   281   wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
   282   wt_stmt_ :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
   283   ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
   284   ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
   285   ty_exprs_:: "env \<Rightarrow> [expr list,
   286 		     \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
   287 
   288 syntax (xsymbols)
   289   wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
   290   wt_stmt_ ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
   291   ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
   292   ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
   293   ty_exprs_ :: "env \<Rightarrow> [expr list,
   294 		    \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
   295 
   296 translations
   297 	"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
   298 	"E\<turnstile>s\<Colon>\<surd>" == "E,empty_dt\<Turnstile>s\<Colon>\<surd>"
   299 	"E\<turnstile>e\<Colon>-T" == "E,empty_dt\<Turnstile>e\<Colon>-T"
   300 	"E\<turnstile>e\<Colon>=T" == "E,empty_dt\<Turnstile>e\<Colon>=T"
   301 	"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T"
   302 
   303 
   304 
   305 inductive wt intros 
   306 
   307 
   308 (* well-typed statements *)
   309 
   310   Skip:					"E,dt\<Turnstile>Skip\<Colon>\<surd>"
   311 
   312   Expr:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
   313 					 E,dt\<Turnstile>Expr e\<Colon>\<surd>"
   314   (* cf. 14.6 *)
   315   Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
   316                                          E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
   317 
   318   Comp:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
   319 	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   320 					 E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
   321 
   322   (* cf. 14.8 *)
   323   If:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   324 	  E,dt\<Turnstile>c1\<Colon>\<surd>;
   325 	  E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   326 					 E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
   327 
   328   (* cf. 14.10 *)
   329   Loop:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   330 	  E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   331 					 E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
   332   (* cf. 14.13, 14.15, 14.16 *)
   333   Do:                                   "E,dt\<Turnstile>Do jump\<Colon>\<surd>"
   334 
   335   (* cf. 14.16 *)
   336   Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
   337 	  prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
   338 					 E,dt\<Turnstile>Throw e\<Colon>\<surd>"
   339   (* cf. 14.18 *)
   340   Try:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
   341 	  lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
   342           \<Longrightarrow>
   343 					 E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
   344 
   345   (* cf. 14.18 *)
   346   Fin:	"\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   347 					 E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
   348 
   349   Init:	"\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
   350 					 E,dt\<Turnstile>Init C\<Colon>\<surd>"
   351   (* Init is created on the fly during evaluation (see Eval.thy). The class
   352    * isn't necessarily accessible from the points Init is called. Therefor
   353    * we only demand is_class and not is_acc_class here 
   354    *)
   355 
   356 (* well-typed expressions *)
   357 
   358   (* cf. 15.8 *)
   359   NewC:	"\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
   360 					 E,dt\<Turnstile>NewC C\<Colon>-Class C"
   361   (* cf. 15.9 *)
   362   NewA:	"\<lbrakk>is_acc_type (prg E) (pkg E) T;
   363 	  E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   364 					 E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
   365 
   366   (* cf. 15.15 *)
   367   Cast:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
   368 	  prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
   369 					 E,dt\<Turnstile>Cast T' e\<Colon>-T'"
   370 
   371   (* cf. 15.19.2 *)
   372   Inst:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
   373 	  prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
   374 					 E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
   375 
   376   (* cf. 15.7.1 *)
   377   Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
   378 					 E,dt\<Turnstile>Lit x\<Colon>-T"
   379 
   380   UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
   381           \<Longrightarrow>
   382 	  E,dt\<Turnstile>UnOp unop e\<Colon>-T"
   383   
   384   BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
   385            T=PrimT (binop_type binop)\<rbrakk> 
   386            \<Longrightarrow>
   387 	   E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
   388   
   389   (* cf. 15.10.2, 15.11.1 *)
   390   Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   391 	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
   392 					 E,dt\<Turnstile>Super\<Colon>-Class (super c)"
   393 
   394   (* cf. 15.13.1, 15.10.1, 15.12 *)
   395   Acc:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
   396 					 E,dt\<Turnstile>Acc va\<Colon>-T"
   397 
   398   (* cf. 15.25, 15.25.1 *)
   399   Ass:	"\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
   400 	  E,dt\<Turnstile>v \<Colon>-T';
   401 	  prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
   402 					 E,dt\<Turnstile>va:=v\<Colon>-T'"
   403 
   404   (* cf. 15.24 *)
   405   Cond:	"\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
   406 	  E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
   407 	  prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
   408 					 E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
   409 
   410   (* cf. 15.11.1, 15.11.2, 15.11.3 *)
   411   Call:	"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
   412 	  E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
   413 	  max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   414             = {((statDeclT,m),pTs')}
   415          \<rbrakk> \<Longrightarrow>
   416 		   E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
   417 
   418   Methd: "\<lbrakk>is_class (prg E) C;
   419 	  methd (prg E) C sig = Some m;
   420 	  E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
   421 					 E,dt\<Turnstile>Methd C sig\<Colon>-T"
   422  (* The class C is the dynamic class of the method call (cf. Eval.thy). 
   423   * It hasn't got to be directly accessible from the current package (pkg E). 
   424   * Only the static class must be accessible (enshured indirectly by 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 D implementing the method must not directly be accessible 
   436    * from the current package (pkg E), but can also be indirectly accessible 
   437    * due to inheritance (enshured in 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 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 inductive_cases wt_stmt_cases: "E,dt\<Turnstile>c\<Colon>\<surd>"
   476 inductive_cases wt_elim_cases:
   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 (Do 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 (* Special versions of some typing rules, better suited to pattern match the
   540  * conclusion (no selectors in the conclusion\<dots>)
   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 ML {*
   606 fun wt_fun name inj rhs =
   607 let
   608   val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U"
   609   val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   610 	(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac])
   611   fun is_Inj (Const (inj,_) $ _) = true
   612     | is_Inj _                   = false
   613   fun pred (t as (_ $ (Const ("Pair",_) $
   614      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   615        x))) $ _ )) = is_Inj x
   616 in
   617   cond_simproc name lhs pred (thm name)
   618 end
   619 
   620 val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>-T"
   621 val wt_var_proc   = wt_fun "wt_var_eq"   "In2"  "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>=T"
   622 val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3"  "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"
   623 val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>"
   624 *}
   625 
   626 ML {*
   627 Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
   628 *}
   629 
   630 lemma Inj_eq_lemma [simp]: 
   631   "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
   632 by auto
   633 
   634 (* unused *)
   635 lemma single_valued_tys_lemma [rule_format (no_asm)]: 
   636   "\<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>  
   637      G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T  = T')"
   638 apply (cases "E", erule wt.induct)
   639 apply (safe del: disjE)
   640 apply (simp_all (no_asm_use) split del: split_if_asm)
   641 apply (safe del: disjE)
   642 (* 17 subgoals *)
   643 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) *})
   644 (*apply (safe del: disjE elim!: wt_elim_cases)*)
   645 apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
   646 apply (simp_all (no_asm_use) split del: split_if_asm)
   647 apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
   648 apply ((blast del: equalityCE dest: sym [THEN trans])+)
   649 done
   650 
   651 (* unused *)
   652 lemma single_valued_tys: 
   653 "ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
   654 apply (unfold single_valued_def)
   655 apply clarsimp
   656 apply (rule single_valued_tys_lemma)
   657 apply (auto intro!: widen_antisym)
   658 done
   659 
   660 lemma typeof_empty_is_type [rule_format (no_asm)]: 
   661   "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
   662 apply (rule val.induct)
   663 apply    	auto
   664 done
   665 
   666 (* unused *)
   667 lemma typeof_is_type [rule_format (no_asm)]: 
   668  "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
   669 apply (rule val.induct)
   670 prefer 5 
   671 apply     fast
   672 apply  (simp_all (no_asm))
   673 done
   674 
   675 end