src/HOL/Bali/WellType.thy
author schirmer
Tue Jul 16 20:25:21 2002 +0200 (2002-07-16)
changeset 13384 a34e38154413
parent 13337 f75dfc606ac7
child 13462 56610e2ba220
permissions -rw-r--r--
Added conditional and (&&) and or (||).
     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_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: "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 (* Special versions of some typing rules, better suited to pattern match the
   539  * conclusion (no selectors in the conclusion\<dots>)
   540  *)
   541 
   542 lemma wt_Super:
   543 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   544   class (prg E) C = Some c;D=super c\<rbrakk> 
   545  \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
   546 by (auto elim: wt.Super)
   547  
   548 
   549 lemma wt_Call: 
   550 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
   551   max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   552     = {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E;
   553  mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
   554 by (auto elim: wt.Call)
   555 
   556 
   557 lemma invocationTypeExpr_noClassD: 
   558 "\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
   559  \<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
   560 proof -
   561   assume wt: "E\<turnstile>e\<Colon>-RefT statT"
   562   show ?thesis
   563   proof (cases "e=Super")
   564     case True
   565     with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
   566     then show ?thesis by blast
   567   next 
   568     case False then show ?thesis 
   569       by (auto simp add: invmode_def split: split_if_asm)
   570   qed
   571 qed
   572 
   573 lemma wt_Super: 
   574 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> 
   575 \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
   576 by (auto elim: wt.Super)
   577 
   578 lemma wt_FVar:	
   579 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f);
   580   sf=is_static f; fT=(type f); accC=cls E\<rbrakk> 
   581 \<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT"
   582 by (auto dest: wt.FVar)
   583 
   584 
   585 lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C"
   586 by (auto elim: wt_elim_cases intro: "wt.Init")
   587 
   588 declare wt.Skip [iff]
   589 
   590 lemma wt_StatRef: 
   591   "is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt"
   592 apply (rule wt.Cast)
   593 apply  (rule wt.Lit)
   594 apply   (simp (no_asm))
   595 apply  (simp (no_asm_simp))
   596 apply (rule cast.widen)
   597 apply (simp (no_asm))
   598 done
   599 
   600 lemma wt_Inj_elim: 
   601   "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of 
   602                        In1 ec \<Rightarrow> (case ec of 
   603                                     Inl e \<Rightarrow> \<exists>T. U=Inl T  
   604                                   | Inr s \<Rightarrow> U=Inl (PrimT Void))  
   605                      | In2 e \<Rightarrow> (\<exists>T. U=Inl T) 
   606                      | In3 e \<Rightarrow> (\<exists>T. U=Inr T)"
   607 apply (erule wt.induct)
   608 apply auto
   609 done
   610 
   611 ML {*
   612 fun wt_fun name inj rhs =
   613 let
   614   val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U"
   615   val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   616 	(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac])
   617   fun is_Inj (Const (inj,_) $ _) = true
   618     | is_Inj _                   = false
   619   fun pred (t as (_ $ (Const ("Pair",_) $
   620      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   621        x))) $ _ )) = is_Inj x
   622 in
   623   make_simproc name lhs pred (thm name)
   624 end
   625 
   626 val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>-T"
   627 val wt_var_proc   = wt_fun "wt_var_eq"   "In2"  "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>=T"
   628 val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3"  "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"
   629 val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>"
   630 *}
   631 
   632 ML {*
   633 Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
   634 *}
   635 
   636 lemma Inj_eq_lemma [simp]: 
   637   "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
   638 by auto
   639 
   640 (* unused *)
   641 lemma single_valued_tys_lemma [rule_format (no_asm)]: 
   642   "\<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>  
   643      G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T  = T')"
   644 apply (cases "E", erule wt.induct)
   645 apply (safe del: disjE)
   646 apply (simp_all (no_asm_use) split del: split_if_asm)
   647 apply (safe del: disjE)
   648 (* 17 subgoals *)
   649 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) *})
   650 (*apply (safe del: disjE elim!: wt_elim_cases)*)
   651 apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
   652 apply (simp_all (no_asm_use) split del: split_if_asm)
   653 apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
   654 apply ((blast del: equalityCE dest: sym [THEN trans])+)
   655 done
   656 
   657 (* unused *)
   658 lemma single_valued_tys: 
   659 "ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
   660 apply (unfold single_valued_def)
   661 apply clarsimp
   662 apply (rule single_valued_tys_lemma)
   663 apply (auto intro!: widen_antisym)
   664 done
   665 
   666 lemma typeof_empty_is_type [rule_format (no_asm)]: 
   667   "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
   668 apply (rule val.induct)
   669 apply    	auto
   670 done
   671 
   672 (* unused *)
   673 lemma typeof_is_type [rule_format (no_asm)]: 
   674  "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
   675 apply (rule val.induct)
   676 prefer 5 
   677 apply     fast
   678 apply  (simp_all (no_asm))
   679 done
   680 
   681 end