author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46714  a7ca72710dfe 
child 48001  c79adcae9869 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/WellType.thy 
12854  2 
Author: David von Oheimb 
3 
*) 

4 
header {* Welltypedness of Java programs *} 

5 

33965  6 
theory WellType 
7 
imports DeclConcepts 

8 
begin 

12854  9 

10 
text {* 

11 
improvements over Java Specification 1.0: 

12 
\begin{itemize} 

13 
\item methods of Object can be called upon references of interface or array type 

14 
\end{itemize} 

15 
simplifications: 

16 
\begin{itemize} 

17 
\item the type rules include all static checks on statements and expressions, 

18 
e.g. definedness of names (of parameters, locals, fields, methods) 

19 
\end{itemize} 

20 
design issues: 

21 
\begin{itemize} 

22 
\item unified type judgment for statements, variables, expressions, 

23 
expression lists 

24 
\item statements are typed like expressions with dummy type Void 

25 
\item the typing rules take an extra argument that is capable of determining 

26 
the dynamic type of objects. Therefore, they can be used for both 

27 
checking static types and determining runtime types in transition semantics. 

28 
\end{itemize} 

29 
*} 

30 

41778  31 
type_synonym lenv 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

32 
= "(lname, ty) table" {* local variables, including This and Result*} 
12854  33 

34 
record env = 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

35 
prg:: "prog" {* program *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

36 
cls:: "qtname" {* current package and class name *} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

37 
lcl:: "lenv" {* local environment *} 
12854  38 

39 
translations 

35431  40 
(type) "lenv" <= (type) "(lname, ty) table" 
41 
(type) "lenv" <= (type) "lname \<Rightarrow> ty option" 

42 
(type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>" 

43 
(type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>" 

12854  44 

45 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

46 
abbreviation 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

47 
pkg :: "env \<Rightarrow> pname" {* select the current package from an environment *} 
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

48 
where "pkg e == pid (cls e)" 
12854  49 

50 
section "Static overloading: maximally specific methods " 

51 

41778  52 
type_synonym 
12854  53 
emhead = "ref_ty \<times> mhead" 
54 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

55 
{* Some mnemotic selectors for emhead *} 
37956  56 
definition 
57 
"declrefT" :: "emhead \<Rightarrow> ref_ty" 

58 
where "declrefT = fst" 

12854  59 

37956  60 
definition 
61 
"mhd" :: "emhead \<Rightarrow> mhead" 

62 
where "mhd \<equiv> snd" 

12854  63 

64 
lemma declrefT_simp[simp]:"declrefT (r,m) = r" 

65 
by (simp add: declrefT_def) 

66 

67 
lemma mhd_simp[simp]:"mhd (r,m) = m" 

68 
by (simp add: mhd_def) 

69 

70 
lemma static_mhd_simp[simp]: "static (mhd m) = is_static m" 

71 
by (cases m) (simp add: member_is_static_simp mhd_def) 

72 

73 
lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m" 

74 
by (cases m) simp 

75 

76 
lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m" 

77 
by (cases m) simp 

78 

79 
lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m" 

80 
by (cases m) simp 

81 

37956  82 
definition 
83 
cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" 

84 
where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig))" 

85 

86 
definition 

87 
Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" where 

88 
"Objectmheads G S = 

89 
(\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 

90 
` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))" 

91 

92 
definition 

93 
accObjectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set" 

94 
where 

95 
"accObjectmheads G S T = 

96 
(if G\<turnstile>RefT T accessible_in (pid S) 

97 
then Objectmheads G S 

98 
else (\<lambda>sig. {}))" 

99 

100 
primrec mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set" 

101 
where 

102 
"mheads G S NullT = (\<lambda>sig. {})" 

103 
 "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 

104 
` accimethds G (pid S) I sig \<union> 

105 
accObjectmheads G S (IfaceT I) sig)" 

106 
 "mheads G S (ClassT C) = cmheads G S C" 

107 
 "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)" 

12854  108 

37406  109 
definition 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

110 
{* applicable methods, cf. 15.11.2.1 *} 
46212  111 
appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where 
37956  112 
"appl_methds G S rt = (\<lambda> sig. 
12854  113 
{(mh,pTs') mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
37406  114 
G\<turnstile>(parTs sig)[\<preceq>]pTs'})" 
12854  115 

37406  116 
definition 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

117 
{* more specific methods, cf. 15.11.2.2 *} 
37956  118 
more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where 
119 
"more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')" 

12854  120 
(*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*) 
121 

37406  122 
definition 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

123 
{* maximally specific methods, cf. 15.11.2.2 *} 
46212  124 
max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where 
37956  125 
"max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and> 
126 
(\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}" 

12854  127 

128 

129 
lemma max_spec2appl_meths: 

130 
"x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" 

131 
by (auto simp: max_spec_def) 

132 

133 
lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow> 

134 
mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'" 

135 
by (auto simp: appl_methds_def) 

136 

137 
lemma max_spec2mheads: 

138 
"max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A 

139 
\<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'" 

140 
apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD) 

141 
done 

142 

143 

37956  144 
definition 
145 
empty_dt :: "dyn_ty" 

146 
where "empty_dt = (\<lambda>a. None)" 

12854  147 

37956  148 
definition 
149 
invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where 

150 
"invmode m e = (if is_static m 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

151 
then Static 
37956  152 
else if e=Super then SuperM else IntVir)" 
12854  153 

154 
lemma invmode_nonstatic [simp]: 

155 
"invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir" 

156 
apply (unfold invmode_def) 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

157 
apply (simp (no_asm) add: member_is_static_simp) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

158 
done 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

159 

99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

160 

99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

161 
lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

162 
apply (unfold invmode_def) 
12854  163 
apply (simp (no_asm)) 
164 
done 

165 

166 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

167 
lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)" 
12854  168 
apply (unfold invmode_def) 
169 
apply (simp (no_asm)) 

170 
done 

171 

172 
lemma Null_staticD: 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

173 
"a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null" 
12854  174 
apply (clarsimp simp add: invmode_IntVir_eq) 
175 
done 

176 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

177 
section "Typing for unary operations" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

178 

37956  179 
primrec unop_type :: "unop \<Rightarrow> prim_ty" 
180 
where 

181 
"unop_type UPlus = Integer" 

182 
 "unop_type UMinus = Integer" 

183 
 "unop_type UBitNot = Integer" 

184 
 "unop_type UNot = Boolean" 

12854  185 

37956  186 
primrec wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool" 
187 
where 

188 
"wt_unop UPlus t = (t = PrimT Integer)" 

189 
 "wt_unop UMinus t = (t = PrimT Integer)" 

190 
 "wt_unop UBitNot t = (t = PrimT Integer)" 

191 
 "wt_unop UNot t = (t = PrimT Boolean)" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

192 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

193 
section "Typing for binary operations" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

194 

37956  195 
primrec binop_type :: "binop \<Rightarrow> prim_ty" 
196 
where 

197 
"binop_type Mul = Integer" 

198 
 "binop_type Div = Integer" 

199 
 "binop_type Mod = Integer" 

200 
 "binop_type Plus = Integer" 

201 
 "binop_type Minus = Integer" 

202 
 "binop_type LShift = Integer" 

203 
 "binop_type RShift = Integer" 

204 
 "binop_type RShiftU = Integer" 

205 
 "binop_type Less = Boolean" 

206 
 "binop_type Le = Boolean" 

207 
 "binop_type Greater = Boolean" 

208 
 "binop_type Ge = Boolean" 

209 
 "binop_type Eq = Boolean" 

210 
 "binop_type Neq = Boolean" 

211 
 "binop_type BitAnd = Integer" 

212 
 "binop_type And = Boolean" 

213 
 "binop_type BitXor = Integer" 

214 
 "binop_type Xor = Boolean" 

215 
 "binop_type BitOr = Integer" 

216 
 "binop_type Or = Boolean" 

217 
 "binop_type CondAnd = Boolean" 

218 
 "binop_type CondOr = Boolean" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

219 

37956  220 
primrec wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" 
221 
where 

222 
"wt_binop G Mul t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

223 
 "wt_binop G Div t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

224 
 "wt_binop G Mod t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

225 
 "wt_binop G Plus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

226 
 "wt_binop G Minus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

227 
 "wt_binop G LShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

228 
 "wt_binop G RShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

229 
 "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

230 
 "wt_binop G Less t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

231 
 "wt_binop G Le t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

232 
 "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

233 
 "wt_binop G Ge t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

234 
 "wt_binop G Eq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 

235 
 "wt_binop G Neq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 

236 
 "wt_binop G BitAnd t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

237 
 "wt_binop G And t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 

238 
 "wt_binop G BitXor t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

239 
 "wt_binop G Xor t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 

240 
 "wt_binop G BitOr t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 

241 
 "wt_binop G Or t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 

242 
 "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 

243 
 "wt_binop G CondOr t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

244 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

245 
section "Typing for terms" 
13384  246 

41778  247 
type_synonym tys = "ty + ty list" 
12854  248 
translations 
35431  249 
(type) "tys" <= (type) "ty + ty list" 
12854  250 

21765  251 

37956  252 
inductive wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50) 
253 
and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51] 50) 

21765  254 
and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50) 
255 
and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50) 

256 
and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" 

257 
("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50) 

258 
where 

259 

260 
"E,dt\<Turnstile>s\<Colon>\<surd> \<equiv> E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)" 

261 
 "E,dt\<Turnstile>e\<Colon>T \<equiv> E,dt\<Turnstile>In1l e\<Colon>Inl T" 

262 
 "E,dt\<Turnstile>e\<Colon>=T \<equiv> E,dt\<Turnstile>In2 e\<Colon>Inl T" 

263 
 "E,dt\<Turnstile>e\<Colon>\<doteq>T \<equiv> E,dt\<Turnstile>In3 e\<Colon>Inr T" 

264 

265 
{* welltyped statements *} 

266 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

267 
 Skip: "E,dt\<Turnstile>Skip\<Colon>\<surd>" 
21765  268 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

269 
 Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>T\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

270 
E,dt\<Turnstile>Expr e\<Colon>\<surd>" 
21765  271 
{* cf. 14.6 *} 
272 
 Lab: "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow> 

273 
E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 

274 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

275 
 Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

276 
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

277 
E,dt\<Turnstile>c1;; c2\<Colon>\<surd>" 
21765  278 

279 
{* cf. 14.8 *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

280 
 If: "\<lbrakk>E,dt\<Turnstile>e\<Colon>PrimT Boolean; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

281 
E,dt\<Turnstile>c1\<Colon>\<surd>; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

282 
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

283 
E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>" 
21765  284 

285 
{* cf. 14.10 *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

286 
 Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>PrimT Boolean; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

287 
E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

288 
E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>" 
21765  289 
{* cf. 14.13, 14.15, 14.16 *} 
290 
 Jmp: "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>" 

12854  291 

21765  292 
{* cf. 14.16 *} 
293 
 Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>Class tn; 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

294 
prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

295 
E,dt\<Turnstile>Throw e\<Colon>\<surd>" 
21765  296 
{* cf. 14.18 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

297 
 Try: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

298 
lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> 
21765  299 
\<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

300 
E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>" 
21765  301 

302 
{* cf. 14.18 *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

303 
 Fin: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

304 
E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>" 
21765  305 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

306 
 Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

307 
E,dt\<Turnstile>Init C\<Colon>\<surd>" 
21765  308 
{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
309 
The class isn't necessarily accessible from the points @{term Init} 

310 
is called. Therefor we only demand @{term is_class} and not 

311 
@{term is_acc_class} here. 

312 
*} 

313 

314 
{* welltyped expressions *} 

315 

316 
{* cf. 15.8 *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

317 
 NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

318 
E,dt\<Turnstile>NewC C\<Colon>Class C" 
21765  319 
{* cf. 15.9 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

320 
 NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

321 
E,dt\<Turnstile>i\<Colon>PrimT Integer\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

322 
E,dt\<Turnstile>New T[i]\<Colon>T.[]" 
21765  323 

324 
{* cf. 15.15 *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

325 
 Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>T; is_acc_type (prg E) (pkg E) T'; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

326 
prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

327 
E,dt\<Turnstile>Cast T' e\<Colon>T'" 
21765  328 

329 
{* cf. 15.19.2 *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

330 
 Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>RefT T; is_acc_type (prg E) (pkg E) (RefT T'); 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

331 
prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

332 
E,dt\<Turnstile>e InstOf T'\<Colon>PrimT Boolean" 
21765  333 

334 
{* cf. 15.7.1 *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

335 
 Lit: "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

336 
E,dt\<Turnstile>Lit x\<Colon>T" 
12854  337 

21765  338 
 UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
339 
\<Longrightarrow> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

340 
E,dt\<Turnstile>UnOp unop e\<Colon>T" 
21765  341 

342 
 BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>T1; E,dt\<Turnstile>e2\<Colon>T2; wt_binop (prg E) binop T1 T2; 

343 
T=PrimT (binop_type binop)\<rbrakk> 

344 
\<Longrightarrow> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

345 
E,dt\<Turnstile>BinOp binop e1 e2\<Colon>T" 
21765  346 

347 
{* cf. 15.10.2, 15.11.1 *} 

348 
 Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

349 
class (prg E) C = Some c\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

350 
E,dt\<Turnstile>Super\<Colon>Class (super c)" 
21765  351 

352 
{* cf. 15.13.1, 15.10.1, 15.12 *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

353 
 Acc: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

354 
E,dt\<Turnstile>Acc va\<Colon>T" 
21765  355 

356 
{* cf. 15.25, 15.25.1 *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

357 
 Ass: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

358 
E,dt\<Turnstile>v \<Colon>T'; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

359 
prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

360 
E,dt\<Turnstile>va:=v\<Colon>T'" 
21765  361 

362 
{* cf. 15.24 *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

363 
 Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>PrimT Boolean; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

364 
E,dt\<Turnstile>e1\<Colon>T1; E,dt\<Turnstile>e2\<Colon>T2; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

365 
prg E\<turnstile>T1\<preceq>T2 \<and> T = T2 \<or> prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

366 
E,dt\<Turnstile>e0 ? e1 : e2\<Colon>T" 
21765  367 

368 
{* cf. 15.11.1, 15.11.2, 15.11.3 *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

369 
 Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>RefT statT; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

370 
E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

371 
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
21765  372 
= {((statDeclT,m),pTs')} 
373 
\<rbrakk> \<Longrightarrow> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

374 
E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>(resTy m)" 
12854  375 

21765  376 
 Methd: "\<lbrakk>is_class (prg E) C; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

377 
methd (prg E) C sig = Some m; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

378 
E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>T\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

379 
E,dt\<Turnstile>Methd C sig\<Colon>T" 
21765  380 
{* The class @{term C} is the dynamic class of the method call 
381 
(cf. Eval.thy). 

382 
It hasn't got to be directly accessible from the current package 

383 
@{term "(pkg E)"}. 

384 
Only the static class must be accessible (enshured indirectly by 

385 
@{term Call}). 

386 
Note that l is just a dummy value. It is only used in the smallstep 

387 
semantics. To proof typesafety directly for the smallstep semantics 

388 
we would have to assume conformance of l here! 

389 
*} 

390 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

391 
 Body: "\<lbrakk>is_class (prg E) D; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

392 
E,dt\<Turnstile>blk\<Colon>\<surd>; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

393 
(lcl E) Result = Some T; 
21765  394 
is_type (prg E) T\<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

395 
E,dt\<Turnstile>Body D blk\<Colon>T" 
21765  396 
{* The class @{term D} implementing the method must not directly be 
397 
accessible from the current package @{term "(pkg E)"}, but can also 

398 
be indirectly accessible due to inheritance (enshured in @{term Call}) 

399 
The result type hasn't got to be accessible in Java! (If it is not 

400 
accessible you can only assign it to Object). 

401 
For dummy value l see rule @{term Methd}. 

402 
*} 

403 

404 
{* welltyped variables *} 

405 

406 
{* cf. 15.13.1 *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

407 
 LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

408 
E,dt\<Turnstile>LVar vn\<Colon>=T" 
21765  409 
{* cf. 15.10.1 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

410 
 FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>Class C; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

411 
accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

412 
E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)" 
21765  413 
{* cf. 15.12 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

414 
 AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>T.[]; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

415 
E,dt\<Turnstile>i\<Colon>PrimT Integer\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

416 
E,dt\<Turnstile>e.[i]\<Colon>=T" 
21765  417 

418 

419 
{* welltyped expression lists *} 

420 

421 
{* cf. 15.11.??? *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

422 
 Nil: "E,dt\<Turnstile>[]\<Colon>\<doteq>[]" 
21765  423 

424 
{* cf. 15.11.??? *} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

425 
 Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>T; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

426 
E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

427 
E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts" 
21765  428 

12854  429 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

430 
(* for purely static typing *) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

431 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

432 
wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("__::_" [51,51,51] 50) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

433 
where "Et::T == E,empty_dt\<Turnstile>t\<Colon> T" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

434 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

435 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

436 
wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("__:<>" [51,51 ] 50) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

437 
where "Es:<> == EIn1r s :: Inl (PrimT Void)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

438 

af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

439 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

440 
ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("__:_" [51,51,51] 50) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

441 
where "Ee:T == EIn1l e :: Inl T" 
12854  442 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

443 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

444 
ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("__:=_" [51,51,51] 50) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

445 
where "Ee:=T == EIn2 e :: Inl T" 
12854  446 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

447 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

448 
ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("__:#_" [51,51,51] 50) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

449 
where "Ee:#T == EIn3 e :: Inr T" 
12854  450 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

451 
notation (xsymbols) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

452 
wt_syntax ("_\<turnstile>_\<Colon>_" [51,51,51] 50) and 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

453 
wt_stmt_syntax ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50) and 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

454 
ty_expr_syntax ("_\<turnstile>_\<Colon>_" [51,51,51] 50) and 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

455 
ty_var_syntax ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) and 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset

456 
ty_exprs_syntax ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50) 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

457 

12854  458 
declare not_None_eq [simp del] 
459 
declare split_if [split del] split_if_asm [split del] 

460 
declare split_paired_All [simp del] split_paired_Ex [simp del] 

24019  461 
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *} 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

462 

23747  463 
inductive_cases wt_elim_cases [cases set]: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

464 
"E,dt\<Turnstile>In2 (LVar vn) \<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

465 
"E,dt\<Turnstile>In2 ({accC,statDeclC,s}e..fn)\<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

466 
"E,dt\<Turnstile>In2 (e.[i]) \<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

467 
"E,dt\<Turnstile>In1l (NewC C) \<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

468 
"E,dt\<Turnstile>In1l (New T'[i]) \<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

469 
"E,dt\<Turnstile>In1l (Cast T' e) \<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

470 
"E,dt\<Turnstile>In1l (e InstOf T') \<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

471 
"E,dt\<Turnstile>In1l (Lit x) \<Colon>T" 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

472 
"E,dt\<Turnstile>In1l (UnOp unop e) \<Colon>T" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

473 
"E,dt\<Turnstile>In1l (BinOp binop e1 e2) \<Colon>T" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

474 
"E,dt\<Turnstile>In1l (Super) \<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

475 
"E,dt\<Turnstile>In1l (Acc va) \<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

476 
"E,dt\<Turnstile>In1l (Ass va v) \<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

477 
"E,dt\<Turnstile>In1l (e0 ? e1 : e2) \<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

478 
"E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

479 
"E,dt\<Turnstile>In1l (Methd C sig) \<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

480 
"E,dt\<Turnstile>In1l (Body D blk) \<Colon>T" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

481 
"E,dt\<Turnstile>In3 ([]) \<Colon>Ts" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

482 
"E,dt\<Turnstile>In3 (e#es) \<Colon>Ts" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

483 
"E,dt\<Turnstile>In1r Skip \<Colon>x" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

484 
"E,dt\<Turnstile>In1r (Expr e) \<Colon>x" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

485 
"E,dt\<Turnstile>In1r (c1;; c2) \<Colon>x" 
12854  486 
"E,dt\<Turnstile>In1r (l\<bullet> c) \<Colon>x" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

487 
"E,dt\<Turnstile>In1r (If(e) c1 Else c2) \<Colon>x" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

488 
"E,dt\<Turnstile>In1r (l\<bullet> While(e) c) \<Colon>x" 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

489 
"E,dt\<Turnstile>In1r (Jmp jump) \<Colon>x" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

490 
"E,dt\<Turnstile>In1r (Throw e) \<Colon>x" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

491 
"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

492 
"E,dt\<Turnstile>In1r (c1 Finally c2) \<Colon>x" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

493 
"E,dt\<Turnstile>In1r (Init C) \<Colon>x" 
12854  494 
declare not_None_eq [simp] 
495 
declare split_if [split] split_if_asm [split] 

496 
declare split_paired_All [simp] split_paired_Ex [simp] 

24019  497 
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} 
12854  498 

499 
lemma is_acc_class_is_accessible: 

500 
"is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P" 

501 
by (auto simp add: is_acc_class_def) 

502 

503 
lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I" 

504 
by (auto simp add: is_acc_iface_def) 

505 

13524  506 
lemma is_acc_iface_Iface_is_accessible: 
12854  507 
"is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P" 
508 
by (auto simp add: is_acc_iface_def) 

509 

510 
lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T" 

511 
by (auto simp add: is_acc_type_def) 

512 

13524  513 
lemma is_acc_iface_is_accessible: 
514 
"is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P" 

12854  515 
by (auto simp add: is_acc_type_def) 
516 

517 
lemma wt_Methd_is_methd: 

518 
"E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig" 

519 
apply (erule_tac wt_elim_cases) 

520 
apply clarsimp 

521 
apply (erule is_methdI, assumption) 

522 
done 

523 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

524 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

525 
text {* Special versions of some typing rules, better suited to pattern 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

526 
match the conclusion (no selectors in the conclusion) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

527 
*} 
12854  528 

529 
lemma wt_Call: 

530 
"\<lbrakk>E,dt\<Turnstile>e\<Colon>RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; 

531 
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

532 
= {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

533 
mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>rT" 
12854  534 
by (auto elim: wt.Call) 
535 

536 

537 
lemma invocationTypeExpr_noClassD: 

538 
"\<lbrakk> E\<turnstile>e\<Colon>RefT statT\<rbrakk> 

539 
\<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM" 

540 
proof  

541 
assume wt: "E\<turnstile>e\<Colon>RefT statT" 

542 
show ?thesis 

543 
proof (cases "e=Super") 

544 
case True 

545 
with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases) 

546 
then show ?thesis by blast 

547 
next 

548 
case False then show ?thesis 

46714  549 
by (auto simp add: invmode_def) 
12854  550 
qed 
551 
qed 

552 

553 
lemma wt_Super: 

554 
"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> 

555 
\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>Class D" 

556 
by (auto elim: wt.Super) 

557 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

558 
lemma wt_FVar: 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

559 
"\<lbrakk>E,dt\<Turnstile>e\<Colon>Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f); 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

560 
sf=is_static f; fT=(type f); accC=cls E\<rbrakk> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

561 
\<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

562 
by (auto dest: wt.FVar) 
12854  563 

564 

565 
lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C" 

566 
by (auto elim: wt_elim_cases intro: "wt.Init") 

567 

568 
declare wt.Skip [iff] 

569 

570 
lemma wt_StatRef: 

571 
"is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>RefT rt" 

572 
apply (rule wt.Cast) 

573 
apply (rule wt.Lit) 

574 
apply (simp (no_asm)) 

575 
apply (simp (no_asm_simp)) 

576 
apply (rule cast.widen) 

577 
apply (simp (no_asm)) 

578 
done 

579 

580 
lemma wt_Inj_elim: 

581 
"\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of 

582 
In1 ec \<Rightarrow> (case ec of 

583 
Inl e \<Rightarrow> \<exists>T. U=Inl T 

584 
 Inr s \<Rightarrow> U=Inl (PrimT Void)) 

585 
 In2 e \<Rightarrow> (\<exists>T. U=Inl T) 

586 
 In3 e \<Rightarrow> (\<exists>T. U=Inr T)" 

587 
apply (erule wt.induct) 

588 
apply auto 

589 
done 

590 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

591 
{* In the special syntax to distinguish the typing judgements for expressions, 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

592 
statements, variables and expression lists the kind of term corresponds 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

593 
to the kind of type in the end e.g. An statement (injection @{term In3} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

594 
into terms, always has type void (injection @{term Inl} into the generalised 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

595 
types. The following simplification procedures establish these kinds of 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

596 
correlation. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

597 
*} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

598 

21765  599 
lemma wt_expr_eq: "E,dt\<Turnstile>In1l t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>T)" 
600 
by (auto, frule wt_Inj_elim, auto) 

601 

602 
lemma wt_var_eq: "E,dt\<Turnstile>In2 t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T)" 

603 
by (auto, frule wt_Inj_elim, auto) 

604 

605 
lemma wt_exprs_eq: "E,dt\<Turnstile>In3 t\<Colon>U = (\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts)" 

606 
by (auto, frule wt_Inj_elim, auto) 

607 

608 
lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)" 

609 
by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto) 

610 

24019  611 
simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = {* 
612 
fn _ => fn _ => fn ct => 

613 
(case Thm.term_of ct of 

614 
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE 

615 
 _ => SOME (mk_meta_eq @{thm wt_expr_eq})) *} 

616 

617 
simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = {* 

618 
fn _ => fn _ => fn ct => 

619 
(case Thm.term_of ct of 

620 
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE 

621 
 _ => SOME (mk_meta_eq @{thm wt_var_eq})) *} 

12854  622 

24019  623 
simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = {* 
624 
fn _ => fn _ => fn ct => 

625 
(case Thm.term_of ct of 

626 
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE 

627 
 _ => SOME (mk_meta_eq @{thm wt_exprs_eq})) *} 

12854  628 

24019  629 
simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = {* 
630 
fn _ => fn _ => fn ct => 

631 
(case Thm.term_of ct of 

632 
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE 

633 
 _ => SOME (mk_meta_eq @{thm wt_stmt_eq})) *} 

12854  634 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

635 
lemma wt_elim_BinOp: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

636 
"\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T; 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

637 
\<And>T1 T2 T3. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

638 
\<lbrakk>E,dt\<Turnstile>e1\<Colon>T1; E,dt\<Turnstile>e2\<Colon>T2; wt_binop (prg E) binop T1 T2; 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

639 
E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3; 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

640 
T = Inl (PrimT (binop_type binop))\<rbrakk> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

641 
\<Longrightarrow> P\<rbrakk> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

642 
\<Longrightarrow> P" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

643 
apply (erule wt_elim_cases) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

644 
apply (cases b) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

645 
apply auto 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

646 
done 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset

647 

12854  648 
lemma Inj_eq_lemma [simp]: 
649 
"(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))" 

650 
by auto 

651 

652 
(* unused *) 

653 
lemma single_valued_tys_lemma [rule_format (no_asm)]: 

654 
"\<forall>S T. G\<turnstile>S\<preceq>T \<longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T \<Longrightarrow> E,dt\<Turnstile>t\<Colon>T \<Longrightarrow> 

655 
G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T = T')" 

656 
apply (cases "E", erule wt.induct) 

657 
apply (safe del: disjE) 

658 
apply (simp_all (no_asm_use) split del: split_if_asm) 

659 
apply (safe del: disjE) 

660 
(* 17 subgoals *) 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24783
diff
changeset

661 
apply (tactic {* ALLGOALS (fn i => 
27239  662 
if i = 11 then EVERY' 
663 
[thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>PrimT Boolean", 

664 
thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>?T1", 

665 
thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>?T2"] i 

666 
else thin_tac @{context} "All ?P" i) *}) 

12854  667 
(*apply (safe del: disjE elim!: wt_elim_cases)*) 
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24783
diff
changeset

668 
apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*}) 
12854  669 
apply (simp_all (no_asm_use) split del: split_if_asm) 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

670 
apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *) 
12854  671 
apply ((blast del: equalityCE dest: sym [THEN trans])+) 
672 
done 

673 

674 
(* unused *) 

675 
lemma single_valued_tys: 

676 
"ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}" 

677 
apply (unfold single_valued_def) 

678 
apply clarsimp 

679 
apply (rule single_valued_tys_lemma) 

680 
apply (auto intro!: widen_antisym) 

681 
done 

682 

683 
lemma typeof_empty_is_type [rule_format (no_asm)]: 

684 
"typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T" 

685 
apply (rule val.induct) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

686 
apply auto 
12854  687 
done 
688 

689 
(* unused *) 

690 
lemma typeof_is_type [rule_format (no_asm)]: 

691 
"(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)" 

692 
apply (rule val.induct) 

693 
prefer 5 

694 
apply fast 

695 
apply (simp_all (no_asm)) 

696 
done 

697 

698 
end 