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