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