src/HOL/Bali/WellType.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62390 842917225d56
child 67443 3abf6a722518
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 (*  Title:      HOL/Bali/WellType.thy
     2     Author:     David von Oheimb
     3 *)
     4 subsection \<open>Well-typedness of Java programs\<close>
     5 
     6 theory WellType
     7 imports DeclConcepts
     8 begin
     9 
    10 text \<open>
    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 \<close>
    30 
    31 type_synonym lenv
    32         = "(lname, ty) table"  \<comment>\<open>local variables, including This and Result\<close>
    33 
    34 record env = 
    35          prg:: "prog"    \<comment>\<open>program\<close>
    36          cls:: "qtname"  \<comment>\<open>current package and class name\<close>
    37          lcl:: "lenv"    \<comment>\<open>local environment\<close>     
    38   
    39 translations
    40   (type) "lenv" <= (type) "(lname, ty) table"
    41   (type) "lenv" <= (type) "lname \<Rightarrow> ty option"
    42   (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
    43   (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
    44 
    45 
    46 abbreviation
    47   pkg :: "env \<Rightarrow> pname" \<comment>\<open>select the current package from an environment\<close>
    48   where "pkg e == pid (cls e)"
    49 
    50 subsubsection "Static overloading: maximally specific methods "
    51 
    52 type_synonym
    53   emhead = "ref_ty \<times> mhead"
    54 
    55 \<comment>\<open>Some mnemotic selectors for emhead\<close>
    56 definition
    57   "declrefT" :: "emhead \<Rightarrow> ref_ty"
    58   where "declrefT = fst"
    59 
    60 definition
    61   "mhd" :: "emhead \<Rightarrow> mhead"
    62   where "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 definition
    83   cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
    84   where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` set_option (accmethd G S C sig))"
    85 
    86 definition
    87   Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" where
    88   "Objectmheads G S =
    89     (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
    90       ` set_option (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))"
    91 
    92 definition
    93   accObjectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
    94 where
    95   "accObjectmheads G S T =
    96     (if G\<turnstile>RefT T accessible_in (pid S)
    97      then Objectmheads G S
    98      else (\<lambda>sig. {}))"
    99 
   100 primrec mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
   101 where
   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 definition
   110   \<comment>\<open>applicable methods, cf. 15.11.2.1\<close>
   111   appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where
   112   "appl_methds G S rt = (\<lambda> sig. 
   113       {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
   114                            G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
   115 
   116 definition
   117   \<comment>\<open>more specific methods, cf. 15.11.2.2\<close>
   118   more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
   119   "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
   120 (*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'*)
   121 
   122 definition
   123   \<comment>\<open>maximally specific methods, cf. 15.11.2.2\<close>
   124   max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where
   125   "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
   126                           (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
   127 
   128 
   129 lemma max_spec2appl_meths: 
   130   "x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" 
   131 by (auto simp: max_spec_def)
   132 
   133 lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow>  
   134    mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   135 by (auto simp: appl_methds_def)
   136 
   137 lemma max_spec2mheads: 
   138 "max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A 
   139  \<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
   140 apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD)
   141 done
   142 
   143 
   144 definition
   145   empty_dt :: "dyn_ty"
   146   where "empty_dt = (\<lambda>a. None)"
   147 
   148 definition
   149   invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
   150   "invmode m e = (if is_static m 
   151                   then Static 
   152                   else if e=Super then SuperM else IntVir)"
   153 
   154 lemma invmode_nonstatic [simp]: 
   155   "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
   156 apply (unfold invmode_def)
   157 apply (simp (no_asm) add: member_is_static_simp)
   158 done
   159 
   160 
   161 lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m"
   162 apply (unfold invmode_def)
   163 apply (simp (no_asm))
   164 done
   165 
   166 
   167 lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)"
   168 apply (unfold invmode_def)
   169 apply (simp (no_asm))
   170 done
   171 
   172 lemma Null_staticD: 
   173   "a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
   174 apply (clarsimp simp add: invmode_IntVir_eq)
   175 done
   176 
   177 subsubsection "Typing for unary operations"
   178 
   179 primrec unop_type :: "unop \<Rightarrow> prim_ty"
   180 where
   181   "unop_type UPlus   = Integer"
   182 | "unop_type UMinus  = Integer"
   183 | "unop_type UBitNot = Integer"
   184 | "unop_type UNot    = Boolean"    
   185 
   186 primrec wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
   187 where
   188   "wt_unop UPlus   t = (t = PrimT Integer)"
   189 | "wt_unop UMinus  t = (t = PrimT Integer)"
   190 | "wt_unop UBitNot t = (t = PrimT Integer)"
   191 | "wt_unop UNot    t = (t = PrimT Boolean)"
   192 
   193 subsubsection "Typing for binary operations"
   194 
   195 primrec binop_type :: "binop \<Rightarrow> prim_ty"
   196 where
   197   "binop_type Mul      = Integer"     
   198 | "binop_type Div      = Integer"
   199 | "binop_type Mod      = Integer"
   200 | "binop_type Plus     = Integer"
   201 | "binop_type Minus    = Integer"
   202 | "binop_type LShift   = Integer"
   203 | "binop_type RShift   = Integer"
   204 | "binop_type RShiftU  = Integer"
   205 | "binop_type Less     = Boolean"
   206 | "binop_type Le       = Boolean"
   207 | "binop_type Greater  = Boolean"
   208 | "binop_type Ge       = Boolean"
   209 | "binop_type Eq       = Boolean"
   210 | "binop_type Neq      = Boolean"
   211 | "binop_type BitAnd   = Integer"
   212 | "binop_type And      = Boolean"
   213 | "binop_type BitXor   = Integer"
   214 | "binop_type Xor      = Boolean"
   215 | "binop_type BitOr    = Integer"
   216 | "binop_type Or       = Boolean"
   217 | "binop_type CondAnd  = Boolean"
   218 | "binop_type CondOr   = Boolean"
   219 
   220 primrec wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
   221 where
   222   "wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   223 | "wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   224 | "wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   225 | "wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   226 | "wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   227 | "wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   228 | "wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   229 | "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   230 | "wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   231 | "wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   232 | "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   233 | "wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   234 | "wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
   235 | "wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
   236 | "wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   237 | "wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   238 | "wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   239 | "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   240 | "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   241 | "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   242 | "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   243 | "wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   244 
   245 subsubsection "Typing for terms"
   246 
   247 type_synonym tys  = "ty + ty list"
   248 translations
   249   (type) "tys" <= (type) "ty + ty list"
   250 
   251 
   252 inductive wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_"  [51,51,51,51] 50)
   253   and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow>  stmt       \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>"  [51,51,51] 50)
   254   and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
   255   and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
   256   and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty   list] \<Rightarrow> bool"
   257     ("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
   258 where
   259 
   260   "E,dt\<Turnstile>s\<Colon>\<surd> \<equiv> E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
   261 | "E,dt\<Turnstile>e\<Colon>-T \<equiv> E,dt\<Turnstile>In1l e\<Colon>Inl T"
   262 | "E,dt\<Turnstile>e\<Colon>=T \<equiv> E,dt\<Turnstile>In2  e\<Colon>Inl T"
   263 | "E,dt\<Turnstile>e\<Colon>\<doteq>T \<equiv> E,dt\<Turnstile>In3  e\<Colon>Inr T"
   264 
   265 \<comment>\<open>well-typed statements\<close>
   266 
   267 | Skip:                                 "E,dt\<Turnstile>Skip\<Colon>\<surd>"
   268 
   269 | Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
   270                                          E,dt\<Turnstile>Expr e\<Colon>\<surd>"
   271   \<comment>\<open>cf. 14.6\<close>
   272 | Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
   273                                          E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
   274 
   275 | Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
   276           E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   277                                          E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
   278 
   279   \<comment>\<open>cf. 14.8\<close>
   280 | If:   "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   281           E,dt\<Turnstile>c1\<Colon>\<surd>;
   282           E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   283                                          E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
   284 
   285   \<comment>\<open>cf. 14.10\<close>
   286 | Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   287           E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   288                                          E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
   289   \<comment>\<open>cf. 14.13, 14.15, 14.16\<close>
   290 | Jmp:                                   "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>"
   291 
   292   \<comment>\<open>cf. 14.16\<close>
   293 | Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
   294           prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
   295                                          E,dt\<Turnstile>Throw e\<Colon>\<surd>"
   296   \<comment>\<open>cf. 14.18\<close>
   297 | Try:  "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
   298           lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
   299           \<Longrightarrow>
   300                                          E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
   301 
   302   \<comment>\<open>cf. 14.18\<close>
   303 | Fin:  "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   304                                          E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
   305 
   306 | Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
   307                                          E,dt\<Turnstile>Init C\<Colon>\<surd>"
   308   \<comment>\<open>@{term Init} is created on the fly during evaluation (see Eval.thy). 
   309      The class isn't necessarily accessible from the points @{term Init} 
   310      is called. Therefor we only demand @{term is_class} and not 
   311      @{term is_acc_class} here. 
   312 \<close>
   313 
   314 \<comment>\<open>well-typed expressions\<close>
   315 
   316   \<comment>\<open>cf. 15.8\<close>
   317 | NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
   318                                          E,dt\<Turnstile>NewC C\<Colon>-Class C"
   319   \<comment>\<open>cf. 15.9\<close>
   320 | NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T;
   321           E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   322                                          E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
   323 
   324   \<comment>\<open>cf. 15.15\<close>
   325 | Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
   326           prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
   327                                          E,dt\<Turnstile>Cast T' e\<Colon>-T'"
   328 
   329   \<comment>\<open>cf. 15.19.2\<close>
   330 | Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
   331           prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
   332                                          E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
   333 
   334   \<comment>\<open>cf. 15.7.1\<close>
   335 | Lit:  "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
   336                                          E,dt\<Turnstile>Lit x\<Colon>-T"
   337 
   338 | UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
   339           \<Longrightarrow>
   340           E,dt\<Turnstile>UnOp unop e\<Colon>-T"
   341   
   342 | BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
   343            T=PrimT (binop_type binop)\<rbrakk> 
   344            \<Longrightarrow>
   345            E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
   346   
   347   \<comment>\<open>cf. 15.10.2, 15.11.1\<close>
   348 | Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   349           class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
   350                                          E,dt\<Turnstile>Super\<Colon>-Class (super c)"
   351 
   352   \<comment>\<open>cf. 15.13.1, 15.10.1, 15.12\<close>
   353 | Acc:  "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
   354                                          E,dt\<Turnstile>Acc va\<Colon>-T"
   355 
   356   \<comment>\<open>cf. 15.25, 15.25.1\<close>
   357 | Ass:  "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
   358           E,dt\<Turnstile>v \<Colon>-T';
   359           prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
   360                                          E,dt\<Turnstile>va:=v\<Colon>-T'"
   361 
   362   \<comment>\<open>cf. 15.24\<close>
   363 | Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
   364           E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
   365           prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
   366                                          E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
   367 
   368   \<comment>\<open>cf. 15.11.1, 15.11.2, 15.11.3\<close>
   369 | Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
   370           E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
   371           max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   372             = {((statDeclT,m),pTs')}
   373          \<rbrakk> \<Longrightarrow>
   374                    E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
   375 
   376 | Methd: "\<lbrakk>is_class (prg E) C;
   377           methd (prg E) C sig = Some m;
   378           E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
   379                                          E,dt\<Turnstile>Methd C sig\<Colon>-T"
   380  \<comment>\<open>The class @{term C} is the dynamic class of the method call 
   381     (cf. Eval.thy). 
   382     It hasn't got to be directly accessible from the current package 
   383     @{term "(pkg E)"}. 
   384     Only the static class must be accessible (enshured indirectly by 
   385     @{term Call}). 
   386     Note that l is just a dummy value. It is only used in the smallstep 
   387     semantics. To proof typesafety directly for the smallstep semantics 
   388     we would have to assume conformance of l here!
   389 \<close>
   390 
   391 | Body: "\<lbrakk>is_class (prg E) D;
   392           E,dt\<Turnstile>blk\<Colon>\<surd>;
   393           (lcl E) Result = Some T;
   394           is_type (prg E) T\<rbrakk> \<Longrightarrow>
   395                                          E,dt\<Turnstile>Body D blk\<Colon>-T"
   396 \<comment>\<open>The class @{term D} implementing the method must not directly be 
   397      accessible  from the current package @{term "(pkg E)"}, but can also 
   398      be indirectly accessible due to inheritance (enshured in @{term Call})
   399     The result type hasn't got to be accessible in Java! (If it is not 
   400     accessible you can only assign it to Object).
   401     For dummy value l see rule @{term Methd}. 
   402 \<close>
   403 
   404 \<comment>\<open>well-typed variables\<close>
   405 
   406   \<comment>\<open>cf. 15.13.1\<close>
   407 | LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
   408                                          E,dt\<Turnstile>LVar vn\<Colon>=T"
   409   \<comment>\<open>cf. 15.10.1\<close>
   410 | FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
   411           accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
   412                          E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
   413   \<comment>\<open>cf. 15.12\<close>
   414 | AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
   415           E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   416                                          E,dt\<Turnstile>e.[i]\<Colon>=T"
   417 
   418 
   419 \<comment>\<open>well-typed expression lists\<close>
   420 
   421   \<comment>\<open>cf. 15.11.???\<close>
   422 | Nil:                                  "E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
   423 
   424   \<comment>\<open>cf. 15.11.???\<close>
   425 | Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
   426           E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
   427                                          E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
   428 
   429 
   430 (* for purely static typing *)
   431 abbreviation
   432   wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
   433   where "E\<turnstile>t\<Colon>T == E,empty_dt\<Turnstile>t\<Colon> T"
   434 
   435 abbreviation
   436   wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
   437   where "E\<turnstile>s\<Colon>\<surd> == E\<turnstile>In1r s \<Colon> Inl (PrimT Void)"
   438 
   439 abbreviation
   440   ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) 
   441   where "E\<turnstile>e\<Colon>-T == E\<turnstile>In1l e \<Colon> Inl T"
   442 
   443 abbreviation
   444   ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
   445   where "E\<turnstile>e\<Colon>=T == E\<turnstile>In2 e \<Colon> Inl T"
   446 
   447 abbreviation
   448   ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
   449   where "E\<turnstile>e\<Colon>\<doteq>T == E\<turnstile>In3 e \<Colon> Inr T"
   450 
   451 notation (ASCII)
   452   wt_syntax  ("_|-_::_" [51,51,51] 50) and
   453   wt_stmt_syntax  ("_|-_:<>" [51,51   ] 50) and
   454   ty_expr_syntax  ("_|-_:-_" [51,51,51] 50) and
   455   ty_var_syntax  ("_|-_:=_" [51,51,51] 50) and
   456   ty_exprs_syntax  ("_|-_:#_" [51,51,51] 50)
   457 
   458 declare not_None_eq [simp del] 
   459 declare if_split [split del] if_split_asm [split del]
   460 declare split_paired_All [simp del] split_paired_Ex [simp del]
   461 setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
   462 
   463 inductive_cases wt_elim_cases [cases set]:
   464         "E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
   465         "E,dt\<Turnstile>In2  ({accC,statDeclC,s}e..fn)\<Colon>T"
   466         "E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T"
   467         "E,dt\<Turnstile>In1l (NewC C)                \<Colon>T"
   468         "E,dt\<Turnstile>In1l (New T'[i])             \<Colon>T"
   469         "E,dt\<Turnstile>In1l (Cast T' e)             \<Colon>T"
   470         "E,dt\<Turnstile>In1l (e InstOf T')           \<Colon>T"
   471         "E,dt\<Turnstile>In1l (Lit x)                 \<Colon>T"
   472         "E,dt\<Turnstile>In1l (UnOp unop e)           \<Colon>T"
   473         "E,dt\<Turnstile>In1l (BinOp binop e1 e2)     \<Colon>T"
   474         "E,dt\<Turnstile>In1l (Super)                 \<Colon>T"
   475         "E,dt\<Turnstile>In1l (Acc va)                \<Colon>T"
   476         "E,dt\<Turnstile>In1l (Ass va v)              \<Colon>T"
   477         "E,dt\<Turnstile>In1l (e0 ? e1 : e2)          \<Colon>T"
   478         "E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
   479         "E,dt\<Turnstile>In1l (Methd C sig)           \<Colon>T"
   480         "E,dt\<Turnstile>In1l (Body D blk)            \<Colon>T"
   481         "E,dt\<Turnstile>In3  ([])                    \<Colon>Ts"
   482         "E,dt\<Turnstile>In3  (e#es)                  \<Colon>Ts"
   483         "E,dt\<Turnstile>In1r  Skip                   \<Colon>x"
   484         "E,dt\<Turnstile>In1r (Expr e)                \<Colon>x"
   485         "E,dt\<Turnstile>In1r (c1;; c2)               \<Colon>x"
   486         "E,dt\<Turnstile>In1r (l\<bullet> c)                  \<Colon>x" 
   487         "E,dt\<Turnstile>In1r (If(e) c1 Else c2)      \<Colon>x"
   488         "E,dt\<Turnstile>In1r (l\<bullet> While(e) c)         \<Colon>x"
   489         "E,dt\<Turnstile>In1r (Jmp jump)              \<Colon>x"
   490         "E,dt\<Turnstile>In1r (Throw e)               \<Colon>x"
   491         "E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x"
   492         "E,dt\<Turnstile>In1r (c1 Finally c2)         \<Colon>x"
   493         "E,dt\<Turnstile>In1r (Init C)                \<Colon>x"
   494 declare not_None_eq [simp] 
   495 declare if_split [split] if_split_asm [split]
   496 declare split_paired_All [simp] split_paired_Ex [simp]
   497 setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
   498 
   499 lemma is_acc_class_is_accessible: 
   500   "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
   501 by (auto simp add: is_acc_class_def)
   502 
   503 lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
   504 by (auto simp add: is_acc_iface_def)
   505 
   506 lemma is_acc_iface_Iface_is_accessible: 
   507   "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
   508 by (auto simp add: is_acc_iface_def)
   509 
   510 lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
   511 by (auto simp add: is_acc_type_def)
   512 
   513 lemma is_acc_iface_is_accessible:
   514   "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
   515 by (auto simp add: is_acc_type_def)
   516 
   517 lemma wt_Methd_is_methd: 
   518   "E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig"
   519 apply (erule_tac wt_elim_cases)
   520 apply clarsimp
   521 apply (erule is_methdI, assumption)
   522 done
   523 
   524 
   525 text \<open>Special versions of some typing rules, better suited to pattern 
   526         match the conclusion (no selectors in the conclusion)
   527 \<close>
   528 
   529 lemma wt_Call: 
   530 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
   531   max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   532     = {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E;
   533  mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
   534 by (auto elim: wt.Call)
   535 
   536 
   537 lemma invocationTypeExpr_noClassD: 
   538 "\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
   539  \<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
   540 proof -
   541   assume wt: "E\<turnstile>e\<Colon>-RefT statT"
   542   show ?thesis
   543   proof (cases "e=Super")
   544     case True
   545     with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
   546     then show ?thesis by blast
   547   next 
   548     case False then show ?thesis 
   549       by (auto simp add: invmode_def)
   550   qed
   551 qed
   552 
   553 lemma wt_Super: 
   554 "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> 
   555 \<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
   556 by (auto elim: wt.Super)
   557 
   558 lemma wt_FVar:  
   559 "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f);
   560   sf=is_static f; fT=(type f); accC=cls E\<rbrakk> 
   561 \<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT"
   562 by (auto dest: wt.FVar)
   563 
   564 
   565 lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C"
   566 by (auto elim: wt_elim_cases intro: "wt.Init")
   567 
   568 declare wt.Skip [iff]
   569 
   570 lemma wt_StatRef: 
   571   "is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt"
   572 apply (rule wt.Cast)
   573 apply  (rule wt.Lit)
   574 apply   (simp (no_asm))
   575 apply  (simp (no_asm_simp))
   576 apply (rule cast.widen)
   577 apply (simp (no_asm))
   578 done
   579 
   580 lemma wt_Inj_elim: 
   581   "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of 
   582                        In1 ec \<Rightarrow> (case ec of 
   583                                     Inl e \<Rightarrow> \<exists>T. U=Inl T  
   584                                   | Inr s \<Rightarrow> U=Inl (PrimT Void))  
   585                      | In2 e \<Rightarrow> (\<exists>T. U=Inl T) 
   586                      | In3 e \<Rightarrow> (\<exists>T. U=Inr T)"
   587 apply (erule wt.induct)
   588 apply auto
   589 done
   590 
   591 \<comment>\<open>In the special syntax to distinguish the typing judgements for expressions, 
   592      statements, variables and expression lists the kind of term corresponds
   593      to the kind of type in the end e.g. An statement (injection @{term In3} 
   594     into terms, always has type void (injection @{term Inl} into the generalised
   595     types. The following simplification procedures establish these kinds of
   596     correlation. 
   597 \<close>
   598 
   599 lemma wt_expr_eq: "E,dt\<Turnstile>In1l t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T)"
   600   by (auto, frule wt_Inj_elim, auto)
   601 
   602 lemma wt_var_eq: "E,dt\<Turnstile>In2 t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T)"
   603   by (auto, frule wt_Inj_elim, auto)
   604 
   605 lemma wt_exprs_eq: "E,dt\<Turnstile>In3 t\<Colon>U = (\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts)"
   606   by (auto, frule wt_Inj_elim, auto)
   607 
   608 lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)"
   609   by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
   610 
   611 simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = \<open>
   612   fn _ => fn _ => fn ct =>
   613     (case Thm.term_of ct of
   614       (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   615     | _ => SOME (mk_meta_eq @{thm wt_expr_eq}))\<close>
   616 
   617 simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = \<open>
   618   fn _ => fn _ => fn ct =>
   619     (case Thm.term_of ct of
   620       (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   621     | _ => SOME (mk_meta_eq @{thm wt_var_eq}))\<close>
   622 
   623 simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = \<open>
   624   fn _ => fn _ => fn ct =>
   625     (case Thm.term_of ct of
   626       (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   627     | _ => SOME (mk_meta_eq @{thm wt_exprs_eq}))\<close>
   628 
   629 simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = \<open>
   630   fn _ => fn _ => fn ct =>
   631     (case Thm.term_of ct of
   632       (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   633     | _ => SOME (mk_meta_eq @{thm wt_stmt_eq}))\<close>
   634 
   635 lemma wt_elim_BinOp:
   636   "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
   637     \<And>T1 T2 T3.
   638        \<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2;
   639           E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3;
   640           T = Inl (PrimT (binop_type binop))\<rbrakk>
   641        \<Longrightarrow> P\<rbrakk>
   642 \<Longrightarrow> P"
   643 apply (erule wt_elim_cases)
   644 apply (cases b)
   645 apply auto
   646 done
   647 
   648 lemma Inj_eq_lemma [simp]: 
   649   "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
   650 by auto
   651 
   652 (* unused *)
   653 lemma single_valued_tys_lemma [rule_format (no_asm)]: 
   654   "\<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>  
   655      G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T  = T')"
   656 apply (cases "E", erule wt.induct)
   657 apply (safe del: disjE)
   658 apply (simp_all (no_asm_use) split del: if_split_asm)
   659 apply (safe del: disjE)
   660 (* 17 subgoals *)
   661 apply (tactic \<open>ALLGOALS (fn i =>
   662   if i = 11 then EVERY'
   663    [Rule_Insts.thin_tac @{context} "E,dt\<Turnstile>e0\<Colon>-PrimT Boolean" [(@{binding E}, NONE, NoSyn)],
   664     Rule_Insts.thin_tac @{context} "E,dt\<Turnstile>e1\<Colon>-T1" [(@{binding E}, NONE, NoSyn), (@{binding T1}, NONE, NoSyn)],
   665     Rule_Insts.thin_tac @{context} "E,dt\<Turnstile>e2\<Colon>-T2" [(@{binding E}, NONE, NoSyn), (@{binding T2}, NONE, NoSyn)]] i
   666   else Rule_Insts.thin_tac @{context} "All P" [(@{binding P}, NONE, NoSyn)] i)\<close>)
   667 (*apply (safe del: disjE elim!: wt_elim_cases)*)
   668 apply (tactic \<open>ALLGOALS (eresolve_tac @{context} @{thms wt_elim_cases})\<close>)
   669 apply (simp_all (no_asm_use) split del: if_split_asm)
   670 apply (erule_tac [12] V = "All P" for P in thin_rl) (* Call *)
   671 apply (blast del: equalityCE dest: sym [THEN trans])+
   672 done
   673 
   674 (* unused *)
   675 lemma single_valued_tys: 
   676 "ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
   677 apply (unfold single_valued_def)
   678 apply clarsimp
   679 apply (rule single_valued_tys_lemma)
   680 apply (auto intro!: widen_antisym)
   681 done
   682 
   683 lemma typeof_empty_is_type: "typeof (\<lambda>a. None) v = Some T \<Longrightarrow> is_type G T"
   684   by (induct v) auto
   685 
   686 (* unused *)
   687 lemma typeof_is_type: "(\<forall>a. v \<noteq> Addr a) \<Longrightarrow> \<exists>T. typeof dt v = Some T \<and> is_type G T"
   688   by (induct v) auto
   689 
   690 end