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