author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44890  22f665a2e91c 
child 51717  9e7d1c139569 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Eval.thy 
12854  2 
Author: David von Oheimb 
3 
*) 

4 
header {* Operational evaluation (bigstep) semantics of Java expressions and 

5 
statements 

6 
*} 

7 

16417  8 
theory Eval imports State DeclConcepts begin 
12854  9 

10 
text {* 

11 

12 
improvements over Java Specification 1.0: 

13 
\begin{itemize} 

14 
\item dynamic method lookup does not need to consider the return type 

15 
(cf.15.11.4.4) 

16 
\item throw raises a NullPointer exception if a null reference is given, and 

17 
each throw of a standard exception yield a fresh exception object 

18 
(was not specified) 

19 
\item if there is not enough memory even to allocate an OutOfMemory exception, 

20 
evaluation/execution fails, i.e. simply stops (was not specified) 

21 
\item array assignment checks lhs (and may throw exceptions) before evaluating 

22 
rhs 

23 
\item fixed exact positions of class initializations 

24 
(immediate at first active use) 

25 
\end{itemize} 

26 

27 
design issues: 

28 
\begin{itemize} 

29 
\item evaluation vs. (singlestep) transition semantics 

30 
evaluation semantics chosen, because: 

31 
\begin{itemize} 

32 
\item[++] less verbose and therefore easier to read (and to handle in proofs) 

33 
\item[+] more abstract 

34 
\item[+] intermediate values (appearing in recursive rules) need not be 

35 
stored explicitly, e.g. no call body construct or stack of invocation 

36 
frames containing local variables and return addresses for method calls 

37 
needed 

38 
\item[+] convenient rule induction for subject reduction theorem 

39 
\item[] no interleaving (for parallelism) can be described 

40 
\item[] stating a property of infinite executions requires the metalevel 

41 
argument that this property holds for any finite prefixes of it 

42 
(e.g. stopped using a counter that is decremented to zero and then 

43 
throwing an exception) 

44 
\end{itemize} 

45 
\item unified evaluation for variables, expressions, expression lists, 

46 
statements 

47 
\item the value entry in statement rules is redundant 

48 
\item the value entry in rules is irrelevant in case of exceptions, but its full 

49 
inclusion helps to make the rule structure independent of exception occurence. 

50 
\item as irrelevant value entries are ignored, it does not matter if they are 

51 
unique. 

52 
For simplicity, (fixed) arbitrary values are preferred over "free" values. 

53 
\item the rule format is such that the start state may contain an exception. 

54 
\begin{itemize} 

55 
\item[++] faciliates exception handling 

56 
\item[+] symmetry 

57 
\end{itemize} 

58 
\item the rules are defined carefully in order to be applicable even in not 

59 
typecorrect situations (yielding undefined values), 

28524  60 
e.g. @{text "the_Addr (Val (Bool b)) = undefined"}. 
12854  61 
\begin{itemize} 
62 
\item[++] fewer rules 

63 
\item[] less readable because of auxiliary functions like @{text the_Addr} 

64 
\end{itemize} 

65 
Alternative: "defensive" evaluation throwing some InternalError exception 

66 
in case of (impossible, for correct programs) type mismatches 

67 
\item there is exactly one rule per syntactic construct 

68 
\begin{itemize} 

69 
\item[+] no redundancy in case distinctions 

70 
\end{itemize} 

71 
\item halloc fails iff there is no free heap address. When there is 

72 
only one free heap address left, it returns an OutOfMemory exception. 

73 
In this way it is guaranteed that when an OutOfMemory exception is thrown for 

74 
the first time, there is a free location on the heap to allocate it. 

75 
\item the allocation of objects that represent standard exceptions is deferred 

76 
until execution of any enclosing catch clause, which is transparent to 

77 
the program. 

78 
\begin{itemize} 

79 
\item[] requires an auxiliary execution relation 

80 
\item[++] avoids copies of allocation code and awkward case distinctions 

81 
(whether there is enough memory to allocate the exception) in 

82 
evaluation rules 

83 
\end{itemize} 

84 
\item unfortunately @{text new_Addr} is not directly executable because of 

85 
Hilbert operator. 

86 
\end{itemize} 

87 
simplifications: 

88 
\begin{itemize} 

89 
\item local variables are initialized with default values 

90 
(no definite assignment) 

91 
\item garbage collection not considered, therefore also no finalizers 

92 
\item stack overflow and memory overflow during class initialization not 

93 
modelled 

94 
\item exceptions in initializations not replaced by ExceptionInInitializerError 

95 
\end{itemize} 

96 
*} 

97 

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:
13601
diff
changeset

98 

41778  99 
type_synonym vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)" 
100 
type_synonym vals = "(val, vvar, val list) sum3" 

12854  101 
translations 
35431  102 
(type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)" 
103 
(type) "vals" <= (type) "(val, vvar, val list) sum3" 

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:
13601
diff
changeset

104 

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:
13601
diff
changeset

105 
text {* To avoid redundancy and to reduce the number of rules, there is only 
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:
13601
diff
changeset

106 
one evaluation rule for each syntactic term. This is also true for variables 
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:
13601
diff
changeset

107 
(e.g. see the rules below for @{text LVar}, @{text FVar} and @{text AVar}). 
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:
13601
diff
changeset

108 
So evaluation of a variable must capture both possible further uses: 
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:
13601
diff
changeset

109 
read (rule @{text Acc}) or write (rule @{text Ass}) to the variable. 
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:
13601
diff
changeset

110 
Therefor a variable evaluates to a special value @{term vvar}, which is 
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:
13601
diff
changeset

111 
a pair, consisting of the current value (for later read access) and an update 
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:
13601
diff
changeset

112 
function (for later write access). Because 
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:
13601
diff
changeset

113 
during assignment to an array variable an exception may occur if the types 
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:
13601
diff
changeset

114 
don't match, the update function is very generic: it transforms the 
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:
13601
diff
changeset

115 
full state. This generic update function causes some technical trouble during 
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:
13601
diff
changeset

116 
some proofs (e.g. type safety, correctness of definite assignment). There we 
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:
13601
diff
changeset

117 
need to prove some additional invariant on this update function to prove the 
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:
13601
diff
changeset

118 
assignment correct, since the update function could potentially alter the whole 
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:
13601
diff
changeset

119 
state in an arbitrary manner. This invariant must be carried around through 
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:
13601
diff
changeset

120 
the whole induction. 
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:
13601
diff
changeset

121 
So for future approaches it may be better not to take 
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:
13601
diff
changeset

122 
such a generic update function, but only to store the address and the kind 
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:
13601
diff
changeset

123 
of variable (array (+ element type), local variable or field) for later 
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:
13601
diff
changeset

124 
assignment. 
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:
13601
diff
changeset

125 
*} 
12854  126 

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

127 
abbreviation (xsymbols) 
12854  128 
dummy_res :: "vals" ("\<diamondsuit>") 
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

129 
where "\<diamondsuit> == In1 Unit" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

130 

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

131 
abbreviation (input) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

132 
val_inj_vals ("\<lfloor>_\<rfloor>\<^sub>e" 1000) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

133 
where "\<lfloor>e\<rfloor>\<^sub>e == In1 e" 
12854  134 

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

135 
abbreviation (input) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

136 
var_inj_vals ("\<lfloor>_\<rfloor>\<^sub>v" 1000) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

137 
where "\<lfloor>v\<rfloor>\<^sub>v == In2 v" 
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:
13601
diff
changeset

138 

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

139 
abbreviation (input) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

140 
lst_inj_vals ("\<lfloor>_\<rfloor>\<^sub>l" 1000) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

141 
where "\<lfloor>es\<rfloor>\<^sub>l == In3 es" 
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:
13601
diff
changeset

142 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35069
diff
changeset

143 
definition undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals" where 
37956  144 
"undefined3 = sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit)) 
28524  145 
(\<lambda>x. In2 undefined) (\<lambda>x. In3 undefined)" 
12854  146 

28524  147 
lemma [simp]: "undefined3 (In1l x) = In1 undefined" 
148 
by (simp add: undefined3_def) 

12854  149 

28524  150 
lemma [simp]: "undefined3 (In1r x) = \<diamondsuit>" 
151 
by (simp add: undefined3_def) 

12854  152 

28524  153 
lemma [simp]: "undefined3 (In2 x) = In2 undefined" 
154 
by (simp add: undefined3_def) 

12854  155 

28524  156 
lemma [simp]: "undefined3 (In3 x) = In3 undefined" 
157 
by (simp add: undefined3_def) 

12854  158 

159 

160 
section "exception throwing and catching" 

161 

37956  162 
definition 
163 
throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" where 

164 
"throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)" 

12854  165 

166 
lemma throw_def2: 

167 
"throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)" 

168 
apply (unfold throw_def) 

169 
apply (simp (no_asm)) 

170 
done 

171 

37956  172 
definition 
173 
fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60) 

174 
where "G,s\<turnstile>a' fits T = ((\<exists>rt. T=RefT rt) \<longrightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T)" 

12854  175 

176 
lemma fits_Null [simp]: "G,s\<turnstile>Null fits T" 

177 
by (simp add: fits_def) 

178 

179 

180 
lemma fits_Addr_RefT [simp]: 

181 
"G,s\<turnstile>Addr a fits RefT t = G\<turnstile>obj_ty (the (heap s a))\<preceq>RefT t" 

182 
by (simp add: fits_def) 

183 

184 
lemma fitsD: "\<And>X. G,s\<turnstile>a' fits T \<Longrightarrow> (\<exists>pt. T = PrimT pt) \<or> 

185 
(\<exists>t. T = RefT t) \<and> a' = Null \<or> 

186 
(\<exists>t. T = RefT t) \<and> a' \<noteq> Null \<and> G\<turnstile>obj_ty (lookup_obj s a')\<preceq>T" 

187 
apply (unfold fits_def) 

188 
apply (case_tac "\<exists>pt. T = PrimT pt") 

189 
apply simp_all 

190 
apply (case_tac "T") 

191 
defer 

192 
apply (case_tac "a' = Null") 

193 
apply simp_all 

17589  194 
apply iprover 
12854  195 
done 
196 

37956  197 
definition 
198 
catch :: "prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) where 

199 
"G,s\<turnstile>catch C = (\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 

200 
G,store s\<turnstile>Addr (the_Loc xc) fits Class C)" 

12854  201 

202 
lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn" 

203 
apply (unfold catch_def) 

204 
apply (simp (no_asm)) 

205 
done 

206 

207 
lemma catch_XcptLoc [simp]: 

208 
"G,(Some (Xcpt (Loc a)),s)\<turnstile>catch C = G,s\<turnstile>Addr a fits Class C" 

209 
apply (unfold catch_def) 

210 
apply (simp (no_asm)) 

211 
done 

212 

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:
13601
diff
changeset

213 
lemma catch_Jump [simp]: "\<not>G,(Some (Jump j),s)\<turnstile>catch tn" 
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:
13601
diff
changeset

214 
apply (unfold catch_def) 
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:
13601
diff
changeset

215 
apply (simp (no_asm)) 
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:
13601
diff
changeset

216 
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:
13601
diff
changeset

217 

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:
13601
diff
changeset

218 
lemma catch_Error [simp]: "\<not>G,(Some (Error e),s)\<turnstile>catch tn" 
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:
13601
diff
changeset

219 
apply (unfold catch_def) 
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:
13601
diff
changeset

220 
apply (simp (no_asm)) 
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:
13601
diff
changeset

221 
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:
13601
diff
changeset

222 

37956  223 
definition 
224 
new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" where 

225 
"new_xcpt_var vn = (\<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s))" 

12854  226 

227 
lemma new_xcpt_var_def2 [simp]: 

228 
"new_xcpt_var vn (x,s) = 

229 
Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)" 

230 
apply (unfold new_xcpt_var_def) 

231 
apply (simp (no_asm)) 

232 
done 

233 

234 

235 

236 
section "misc" 

237 

37956  238 
definition 
239 
assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where 

240 
"assign f v = (\<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s) 

241 
in (x',if x' = None then s' else s))" 

12854  242 

243 
(* 

244 
lemma assign_Norm_Norm [simp]: 

245 
"f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr> 

246 
\<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr>" 

247 
by (simp add: assign_def Let_def) 

248 
*) 

249 

250 
lemma assign_Norm_Norm [simp]: 

251 
"f v (Norm s) = Norm s' \<Longrightarrow> assign f v (Norm s) = Norm s'" 

252 
by (simp add: assign_def Let_def) 

253 

254 
(* 

255 
lemma assign_Norm_Some [simp]: 

256 
"\<lbrakk>abrupt (f v \<lparr>abrupt=None,store=s\<rparr>) = Some y\<rbrakk> 

257 
\<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=Some y,store =s\<rparr>" 

258 
by (simp add: assign_def Let_def split_beta) 

259 
*) 

260 

261 
lemma assign_Norm_Some [simp]: 

262 
"\<lbrakk>abrupt (f v (Norm s)) = Some y\<rbrakk> 

263 
\<Longrightarrow> assign f v (Norm s) = (Some y,s)" 

264 
by (simp add: assign_def Let_def split_beta) 

265 

266 

267 
lemma assign_Some [simp]: 

268 
"assign f v (Some x,s) = (Some x,s)" 

269 
by (simp add: assign_def Let_def split_beta) 

270 

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:
13601
diff
changeset

271 
lemma assign_Some1 [simp]: "\<not> normal s \<Longrightarrow> assign f v s = s" 
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:
13601
diff
changeset

272 
by (auto simp add: assign_def Let_def split_beta) 
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:
13601
diff
changeset

273 

12854  274 
lemma assign_supd [simp]: 
275 
"assign (\<lambda>v. supd (f v)) v (x,s) 

276 
= (x, if x = None then f v s else s)" 

277 
apply auto 

278 
done 

279 

280 
lemma assign_raise_if [simp]: 

281 
"assign (\<lambda>v (x,s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) = 

282 
(raise_if (b s v) xcpt x, if x=None \<and> \<not>b s v then f v s else s)" 

283 
apply (case_tac "x = None") 

284 
apply auto 

285 
done 

286 

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:
13601
diff
changeset

287 

12854  288 
(* 
289 
lemma assign_raise_if [simp]: 

290 
"assign (\<lambda>v s. \<lparr>abrupt=(raise_if (b (store s) v) xcpt) (abrupt s), 

291 
store = f v (store s)\<rparr>) v s = 

292 
\<lparr>abrupt=raise_if (b (store s) v) xcpt (abrupt s), 

293 
store= if (abrupt s)=None \<and> \<not>b (store s) v 

294 
then f v (store s) else (store s)\<rparr>" 

295 
apply (case_tac "abrupt s = None") 

296 
apply auto 

297 
done 

298 
*) 

299 

37956  300 
definition 
301 
init_comp_ty :: "ty \<Rightarrow> stmt" 

302 
where "init_comp_ty T = (if (\<exists>C. T = Class C) then Init (the_Class T) else Skip)" 

12854  303 

304 
lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip" 

305 
apply (unfold init_comp_ty_def) 

306 
apply (simp (no_asm)) 

307 
done 

308 

37956  309 
definition 
310 
invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" where 

311 
"invocation_class m s a' statT = 

312 
(case m of 

313 
Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 

314 
then the_Class (RefT statT) 

315 
else Object 

316 
 SuperM \<Rightarrow> the_Class (RefT statT) 

317 
 IntVir \<Rightarrow> obj_class (lookup_obj s a'))" 

12854  318 

37956  319 
definition 
320 
invocation_declclass :: "prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" where 

321 
"invocation_declclass G m s a' statT sig = 

322 
declclass (the (dynlookup G statT 

12854  323 
(invocation_class m s a' statT) 
324 
sig))" 

325 

326 
lemma invocation_class_IntVir [simp]: 

327 
"invocation_class IntVir s a' statT = obj_class (lookup_obj s a')" 

328 
by (simp add: invocation_class_def) 

329 

330 
lemma dynclass_SuperM [simp]: 

331 
"invocation_class SuperM s a' statT = the_Class (RefT statT)" 

332 
by (simp add: invocation_class_def) 

333 

334 
lemma invocation_class_Static [simp]: 

335 
"invocation_class Static s a' statT = (if (\<exists> statC. statT = ClassT statC) 

336 
then the_Class (RefT statT) 

337 
else Object)" 

338 
by (simp add: invocation_class_def) 

339 

37956  340 
definition 
341 
init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow> state \<Rightarrow> state" 

342 
where 

343 
"init_lvars G C sig mode a' pvs = 

344 
(\<lambda>(x,s). 

12854  345 
let m = mthd (the (methd G C sig)); 
346 
l = \<lambda> k. 

347 
(case k of 

348 
EName e 

349 
\<Rightarrow> (case e of 

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:
13601
diff
changeset

350 
VNam v \<Rightarrow> (empty ((pars m)[\<mapsto>]pvs)) v 
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:
13601
diff
changeset

351 
 Res \<Rightarrow> None) 
12854  352 
 This 
353 
\<Rightarrow> (if mode=Static then None else Some a')) 

37956  354 
in set_lvars l (if mode = Static then x else np a' x,s))" 
12854  355 

356 

357 

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:
13601
diff
changeset

358 
lemma init_lvars_def2: {* better suited for simplification *} 
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:
13601
diff
changeset

359 
"init_lvars G C sig mode a' pvs (x,s) = 
12854  360 
set_lvars 
361 
(\<lambda> k. 

362 
(case k of 

363 
EName e 

364 
\<Rightarrow> (case e of 

365 
VNam v 

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:
13601
diff
changeset

366 
\<Rightarrow> (empty ((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v 
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:
13601
diff
changeset

367 
 Res \<Rightarrow> None) 
12854  368 
 This 
369 
\<Rightarrow> (if mode=Static then None else Some a'))) 

370 
(if mode = Static then x else np a' x,s)" 

371 
apply (unfold init_lvars_def) 

372 
apply (simp (no_asm) add: Let_def) 

373 
done 

374 

37956  375 
definition 
376 
body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" where 

377 
"body G C sig = 

378 
(let m = the (methd G C sig) 

379 
in Body (declclass m) (stmt (mbody (mthd m))))" 

12854  380 

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:
13601
diff
changeset

381 
lemma body_def2: {* better suited for simplification *} 
12854  382 
"body G C sig = Body (declclass (the (methd G C sig))) 
383 
(stmt (mbody (mthd (the (methd G C sig)))))" 

384 
apply (unfold body_def Let_def) 

385 
apply auto 

386 
done 

387 

388 
section "variables" 

389 

37956  390 
definition 
391 
lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar" 

392 
where "lvar vn s = (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))" 

12854  393 

37956  394 
definition 
395 
fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where 

396 
"fvar C stat fn a' s = 

397 
(let (oref,xf) = if stat then (Stat C,id) 

398 
else (Heap (the_Addr a'),np a'); 

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

399 
n = Inl (fn,C); 
12854  400 
f = (\<lambda>v. supd (upd_gobj oref n v)) 
37956  401 
in ((the (values (the (globs (store s) oref)) n),f),abupd xf s))" 
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:
13601
diff
changeset

402 

37956  403 
definition 
404 
avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where 

405 
"avar G i' a' s = 

406 
(let oref = Heap (the_Addr a'); 

407 
i = the_Intg i'; 

408 
n = Inr i; 

409 
(T,k,cs) = the_Arr (globs (store s) oref); 

410 
f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 

12854  411 
ArrStore x 
412 
,upd_gobj oref n v s)) 

37956  413 
in ((the (cs n),f),abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s))" 
12854  414 

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:
13601
diff
changeset

415 
lemma fvar_def2: {* better suited for simplification *} 
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:
13601
diff
changeset

416 
"fvar C stat fn a' s = 
12854  417 
((the 
418 
(values 

419 
(the (globs (store s) (if stat then Stat C else Heap (the_Addr a')))) 

420 
(Inl (fn,C))) 

421 
,(\<lambda>v. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a')) 

422 
(Inl (fn,C)) 

423 
v))) 

424 
,abupd (if stat then id else np a') s) 

425 
" 

426 
apply (unfold fvar_def) 

427 
apply (simp (no_asm) add: Let_def split_beta) 

428 
done 

429 

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:
13601
diff
changeset

430 
lemma avar_def2: {* better suited for simplification *} 
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:
13601
diff
changeset

431 
"avar G i' a' s = 
12854  432 
((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a')))))) 
433 
(Inr (the_Intg i'))) 

434 
,(\<lambda>v (x,s'). (raise_if (\<not>G,s'\<turnstile>v fits (fst(the_Arr (globs (store s) 

435 
(Heap (the_Addr a')))))) 

436 
ArrStore x 

437 
,upd_gobj (Heap (the_Addr a')) 

438 
(Inr (the_Intg i')) v s'))) 

439 
,abupd (raise_if (\<not>(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s) 

440 
(Heap (the_Addr a'))))))) IndOutBound \<circ> np a') 

441 
s)" 

442 
apply (unfold avar_def) 

443 
apply (simp (no_asm) add: Let_def split_beta) 

444 
done 

445 

37956  446 
definition 
447 
check_field_access :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where 

448 
"check_field_access G accC statDeclC fn stat a' s = 

449 
(let oref = if stat then Stat statDeclC 

450 
else Heap (the_Addr a'); 

451 
dynC = case oref of 

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

452 
Heap a \<Rightarrow> obj_class (the (globs (store s) oref)) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

453 
 Stat C \<Rightarrow> C; 
37956  454 
f = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC))) 
455 
in abupd 

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

456 
(error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

457 
AccessViolation) 
37956  458 
s)" 
12854  459 

37956  460 
definition 
461 
check_method_access :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow> sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where 

462 
"check_method_access G accC statT mode sig a' s = 

463 
(let invC = invocation_class mode (store s) a' statT; 

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

464 
dynM = the (dynlookup G statT invC sig) 
37956  465 
in abupd 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

466 
(error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

467 
AccessViolation) 
37956  468 
s)" 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

469 

12854  470 
section "evaluation judgments" 
471 

23747  472 
inductive 
21765  473 
halloc :: "[prog,state,obj_tag,loc,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60) for G::prog 
474 
where {* allocating objects on the heap, cf. 12.5 *} 

12854  475 

476 
Abrupt: 

28524  477 
"G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>undefined\<rightarrow> (Some x,s)" 
12854  478 

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

479 
 New: "\<lbrakk>new_Addr (heap s) = Some a; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

480 
(x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

481 
else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk> 
12854  482 
\<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

483 
G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)" 
12854  484 

23747  485 
inductive sxalloc :: "[prog,state,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,61]60) for G::prog 
21765  486 
where {* allocating exception objects for 
487 
standard exceptions (other than OutOfMemory) *} 

12854  488 

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

489 
Norm: "G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> Norm s" 
12854  490 

21765  491 
 Jmp: "G\<turnstile>(Some (Jump j), s) \<midarrow>sxalloc\<rightarrow> (Some (Jump j), s)" 
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:
13601
diff
changeset

492 

21765  493 
 Error: "G\<turnstile>(Some (Error e), s) \<midarrow>sxalloc\<rightarrow> (Some (Error e), s)" 
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:
13601
diff
changeset

494 

21765  495 
 XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)" 
12854  496 

21765  497 
 SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

498 
G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)" 
12854  499 

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:
13601
diff
changeset

500 

23747  501 
inductive 
21765  502 
eval :: "[prog,state,term,vals,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> '(_, _')" [61,61,80,0,0]60) 
503 
and exec ::"[prog,state,stmt ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _" [61,61,65, 61]60) 

504 
and evar ::"[prog,state,var ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60) 

505 
and eval'::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<succ>_\<rightarrow> _"[61,61,80,61,61]60) 

506 
and evals::"[prog,state,expr list , 

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

507 
val list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60) 
21765  508 
for G::prog 
509 
where 

510 

511 
"G\<turnstile>s \<midarrow>c \<rightarrow> s' \<equiv> G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>, s')" 

512 
 "G\<turnstile>s \<midarrow>e\<succ>v \<rightarrow> s' \<equiv> G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v, s')" 

513 
 "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow> s' \<equiv> G\<turnstile>s \<midarrow>In2 e\<succ>\<rightarrow> (In2 vf, s')" 

514 
 "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow> s' \<equiv> G\<turnstile>s \<midarrow>In3 e\<succ>\<rightarrow> (In3 v, s')" 

12854  515 

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:
13601
diff
changeset

516 
{* propagation of abrupt completion *} 
12854  517 

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:
13601
diff
changeset

518 
{* cf. 14.1, 15.5 *} 
21765  519 
 Abrupt: 
28524  520 
"G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (undefined3 t, (Some xc, s))" 
12854  521 

522 

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:
13601
diff
changeset

523 
{* execution of statements *} 
12854  524 

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:
13601
diff
changeset

525 
{* cf. 14.5 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

526 
 Skip: "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s" 
12854  527 

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:
13601
diff
changeset

528 
{* cf. 14.7 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

529 
 Expr: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

530 
G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1" 
12854  531 

21765  532 
 Lab: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow> 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

533 
G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1" 
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:
13601
diff
changeset

534 
{* cf. 14.2 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

535 
 Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

536 
G\<turnstile> s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

537 
G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2" 
12854  538 

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:
13601
diff
changeset

539 
{* cf. 14.8.2 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

540 
 If: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>b\<rightarrow> s1; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

541 
G\<turnstile> s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

542 
G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2" 
12854  543 

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:
13601
diff
changeset

544 
{* cf. 14.10, 14.10.1 *} 
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:
13601
diff
changeset

545 

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:
13601
diff
changeset

546 
{* A continue jump from the while body @{term c} is handled by 
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:
13601
diff
changeset

547 
this rule. If a continue jump with the proper label was invoked inside 
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:
13601
diff
changeset

548 
@{term c} this label (Cont l) is deleted out of the abrupt component 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:
13601
diff
changeset

549 
the state before the iterative evaluation of the while statement. 
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:
13601
diff
changeset

550 
A break jump is handled by the Lab Statement @{text "Lab l (while\<dots>)"}. 
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:
13601
diff
changeset

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

552 
 Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>b\<rightarrow> s1; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

553 
if the_Bool b 
12854  554 
then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
555 
G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3) 

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

556 
else s3 = s1\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

557 
G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3" 
12854  558 

21765  559 
 Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<rightarrow> (Some (Jump j), s)" 
12854  560 

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:
13601
diff
changeset

561 
{* cf. 14.16 *} 
21765  562 
 Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

563 
G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1" 
12854  564 

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:
13601
diff
changeset

565 
{* cf. 14.18.1 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

566 
 Try: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

567 
if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

568 
G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3" 
12854  569 

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:
13601
diff
changeset

570 
{* cf. 14.18.2 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

571 
 Fin: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1); 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

572 
G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2; 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

573 
s3=(if (\<exists> err. x1=Some (Error err)) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

575 
else abupd (abrupt_if (x1\<noteq>None) x1) s2) \<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

577 
G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3" 
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:
13601
diff
changeset

578 
{* cf. 12.4.2, 8.5 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

579 
 Init: "\<lbrakk>the (class G C) = c; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

580 
if inited C (globs s0) then s3 = Norm s0 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

581 
else (G\<turnstile>Norm (init_class_obj G C s0) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

582 
\<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

583 
G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> 
12854  584 
\<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

585 
G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3" 
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:
13601
diff
changeset

586 
{* This class initialisation rule is a little bit inaccurate. Look at the 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

587 
exact sequence: 
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:
13601
diff
changeset

588 
(1) The current class object (the static fields) are initialised 
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:
13601
diff
changeset

589 
(@{text init_class_obj}), 
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:
13601
diff
changeset

590 
(2) the superclasses are initialised, 
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:
13601
diff
changeset

591 
(3) the static initialiser of the current class is invoked. 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

592 
More precisely we should expect another ordering, namely 2 1 3. 
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:
13601
diff
changeset

593 
But we can't just naively toggle 1 and 2. By calling 
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:
13601
diff
changeset

594 
@{text init_class_obj} 
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:
13601
diff
changeset

595 
before initialising the superclasses, we also implicitly record that 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

596 
we have started to initialise the current class (by setting an 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

597 
value for the class object). This becomes 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

598 
crucial for the completeness proof of the axiomatic semantics 
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:
13601
diff
changeset

599 
@{text "AxCompl.thy"}. Static initialisation requires an induction on 
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:
13601
diff
changeset

600 
the number of classes not yet initialised (or to be more precise, 
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:
13601
diff
changeset

601 
classes were the initialisation has not yet begun). 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

602 
So we could first assign a dummy value to the class before 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

603 
superclass initialisation and afterwards set the correct values. 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

604 
But as long as we don't take memory overflow into account 
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:
13601
diff
changeset

605 
when allocating class objects, we can leave things as they are for 
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:
13601
diff
changeset

606 
convenience. 
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:
13601
diff
changeset

607 
*} 
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:
13601
diff
changeset

608 
{* evaluation of expressions *} 
12854  609 

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:
13601
diff
changeset

610 
{* cf. 15.8.1, 12.4.1 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

611 
 NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

612 
G\<turnstile> s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

613 
G\<turnstile>Norm s0 \<midarrow>NewC C\<succ>Addr a\<rightarrow> s2" 
12854  614 

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:
13601
diff
changeset

615 
{* cf. 15.9.1, 12.4.1 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

616 
 NewA: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e\<succ>i'\<rightarrow> s2; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

617 
G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

618 
G\<turnstile>Norm s0 \<midarrow>New T[e]\<succ>Addr a\<rightarrow> s3" 
12854  619 

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:
13601
diff
changeset

620 
{* cf. 15.15 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

621 
 Cast: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<rightarrow> s1; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

622 
s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

623 
G\<turnstile>Norm s0 \<midarrow>Cast T e\<succ>v\<rightarrow> s2" 
12854  624 

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:
13601
diff
changeset

625 
{* cf. 15.19.2 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

626 
 Inst: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<rightarrow> s1; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

627 
b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

628 
G\<turnstile>Norm s0 \<midarrow>e InstOf T\<succ>Bool b\<rightarrow> s1" 
12854  629 

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:
13601
diff
changeset

630 
{* cf. 15.7.1 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

631 
 Lit: "G\<turnstile>Norm s \<midarrow>Lit v\<succ>v\<rightarrow> Norm s" 
12854  632 

21765  633 
 UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<rightarrow> s1\<rbrakk> 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

634 
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e\<succ>(eval_unop unop v)\<rightarrow> s1" 
13384  635 

21765  636 
 BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1\<succ>v1\<rightarrow> s1; 
13384  637 
G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip)) 
21765  638 
\<succ>\<rightarrow> (In1 v2, s2) 
13384  639 
\<rbrakk> 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

640 
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2\<succ>(eval_binop binop v1 v2)\<rightarrow> s2" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

641 

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:
13601
diff
changeset

642 
{* cf. 15.10.2 *} 
21765  643 
 Super: "G\<turnstile>Norm s \<midarrow>Super\<succ>val_this s\<rightarrow> Norm s" 
12854  644 

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:
13601
diff
changeset

645 
{* cf. 15.2 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

646 
 Acc: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

647 
G\<turnstile>Norm s0 \<midarrow>Acc va\<succ>v\<rightarrow> s1" 
12854  648 

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:
13601
diff
changeset

649 
{* cf. 15.25.1 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

650 
 Ass: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1; 
12854  651 
G\<turnstile> s1 \<midarrow>e\<succ>v \<rightarrow> s2\<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

652 
G\<turnstile>Norm s0 \<midarrow>va:=e\<succ>v\<rightarrow> assign f v s2" 
12854  653 

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:
13601
diff
changeset

654 
{* cf. 15.24 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

655 
 Cond: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0\<succ>b\<rightarrow> s1; 
12854  656 
G\<turnstile> s1 \<midarrow>(if the_Bool b then e1 else e2)\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

657 
G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2\<succ>v\<rightarrow> s2" 
12854  658 

659 

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:
13601
diff
changeset

660 
 {* The interplay of @{term Call}, @{term Methd} and @{term Body}: 
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:
13601
diff
changeset

661 
Method invocation is split up into these three rules: 
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:
13601
diff
changeset

662 
\begin{itemize} 
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:
13601
diff
changeset

663 
\item [@{term Call}] Calculates the target address and evaluates the 
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:
13601
diff
changeset

664 
arguments of the method, and then performs dynamic 
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:
13601
diff
changeset

665 
or static lookup of the method, corresponding to the 
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:
13601
diff
changeset

666 
call mode. Then the @{term Methd} rule is evaluated 
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:
13601
diff
changeset

667 
on the calculated declaration class of the method 
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:
13601
diff
changeset

668 
invocation. 
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:
13601
diff
changeset

669 
\item [@{term Methd}] A syntactic bridge for the folded method body. 
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:
13601
diff
changeset

670 
It is used by the axiomatic semantics to add the 
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:
13601
diff
changeset

671 
proper hypothesis for recursive calls of the method. 
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:
13601
diff
changeset

672 
\item [@{term Body}] An extra syntactic entity for the unfolded method 
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:
13601
diff
changeset

673 
body was introduced to properly trigger class 
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:
13601
diff
changeset

674 
initialisation. Without class initialisation we 
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:
13601
diff
changeset

675 
could just evaluate the body statement. 
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:
13601
diff
changeset

676 
\end{itemize} 
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:
13601
diff
changeset

677 
*} 
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:
13601
diff
changeset

678 
{* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

679 
 Call: 
12854  680 
"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2; 
681 
D = invocation_declclass G mode (store s2) a' 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:
12919
diff
changeset

682 
s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

683 
s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

684 
G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>\<succ>v\<rightarrow> s4\<rbrakk> 
12854  685 
\<Longrightarrow> 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

686 
G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)\<succ>v\<rightarrow> (restore_lvars s2 s4)" 
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:
13601
diff
changeset

687 
{* The accessibility check is after @{term init_lvars}, to keep it simple. 
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:
13601
diff
changeset

688 
@{term init_lvars} already tests for the absence of a nullpointer 
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:
13601
diff
changeset

689 
reference in case of an instance method invocation. 
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:
13601
diff
changeset

690 
*} 
12854  691 

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

692 
 Methd: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

693 
G\<turnstile>Norm s0 \<midarrow>Methd D sig\<succ>v\<rightarrow> s1" 
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:
13601
diff
changeset

694 

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

695 
 Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2; 
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:
13601
diff
changeset

696 
s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or> 
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:
13601
diff
changeset

697 
abrupt s2 = Some (Jump (Cont l))) 
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:
13601
diff
changeset

698 
then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
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:
13601
diff
changeset

699 
else s2)\<rbrakk> \<Longrightarrow> 
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:
13601
diff
changeset

700 
G\<turnstile>Norm s0 \<midarrow>Body D c\<succ>the (locals (store s2) Result) 
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:
13601
diff
changeset

701 
\<rightarrow>abupd (absorb Ret) s3" 
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:
13601
diff
changeset

702 
{* cf. 14.15, 12.4.1 *} 
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:
13601
diff
changeset

703 
{* We filter out a break/continue in @{term s2}, so that we can proof 
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:
13601
diff
changeset

704 
definite assignment 
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:
13601
diff
changeset

705 
correct, without the need of conformance of the state. By this the 
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:
13601
diff
changeset

706 
different parts of the typesafety proof can be disentangled a little. *} 
12854  707 

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:
13601
diff
changeset

708 
{* evaluation of variables *} 
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:
13601
diff
changeset

709 

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:
13601
diff
changeset

710 
{* cf. 15.13.1, 15.7.2 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

711 
 LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s" 
12854  712 

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:
13601
diff
changeset

713 
{* cf. 15.10.1, 12.4.1 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

714 
 FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e\<succ>a\<rightarrow> s2; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

715 
(v,s2') = fvar statDeclC stat fn a s2; 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

716 
s3 = check_field_access G accC statDeclC fn stat a s2' \<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

717 
G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<rightarrow> s3" 
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:
13601
diff
changeset

718 
{* The accessibility check is after @{term fvar}, to keep it simple. 
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:
13601
diff
changeset

719 
@{term fvar} already tests for the absence of a nullpointer reference 
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:
13601
diff
changeset

720 
in case of an instance field 
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:
13601
diff
changeset

721 
*} 
12854  722 

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:
13601
diff
changeset

723 
{* cf. 15.12.1, 15.25.1 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

724 
 AVar: "\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2\<succ>i\<rightarrow> s2; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

725 
(v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

726 
G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'" 
12854  727 

728 

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:
13601
diff
changeset

729 
{* evaluation of expression lists *} 
12854  730 

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:
13601
diff
changeset

731 
{* cf. 15.11.4.2 *} 
21765  732 
 Nil: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

733 
"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0" 
12854  734 

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:
13601
diff
changeset

735 
{* cf. 15.6.4 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

736 
 Cons: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e \<succ> v \<rightarrow> s1; 
12854  737 
G\<turnstile> s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

738 
G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2" 
12854  739 

740 
(* Rearrangement of premisses: 

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:
13601
diff
changeset

741 
[0,1(Abrupt),2(Skip),8(Jmp),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst), 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

742 
17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If), 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

743 
7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar), 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

744 
29(AVar),24(Call)] 
12854  745 
*) 
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:
13601
diff
changeset

746 

26480  747 
ML {* 
40340  748 
bind_thm ("eval_induct", rearrange_prems 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

749 
[0,1,2,8,4,30,31,27,15,16, 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

750 
17,18,19,20,21,3,5,25,26,23,6, 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

751 
7,11,9,13,14,12,22,10,28, 
24019  752 
29,24] @{thm eval.induct}) 
12854  753 
*} 
754 

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

755 

12854  756 
declare split_if [split del] split_if_asm [split del] 
757 
option.split [split del] option.split_asm [split del] 

23747  758 
inductive_cases halloc_elim_cases: 
12854  759 
"G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'" 
760 
"G\<turnstile>(Norm s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'" 

761 

23747  762 
inductive_cases sxalloc_elim_cases: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

763 
"G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> s'" 
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:
13601
diff
changeset

764 
"G\<turnstile>(Some (Jump j),s) \<midarrow>sxalloc\<rightarrow> s'" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

765 
"G\<turnstile>(Some (Error e),s) \<midarrow>sxalloc\<rightarrow> s'" 
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:
13601
diff
changeset

766 
"G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

767 
"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'" 
23747  768 
inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'" 
12854  769 

770 
lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'; 

771 
\<And>s. \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P; 

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:
13601
diff
changeset

772 
\<And>j s. \<lbrakk>s' = (Some (Jump j),s)\<rbrakk> \<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:
13601
diff
changeset

773 
\<And>e s. \<lbrakk>s' = (Some (Error e),s)\<rbrakk> \<Longrightarrow> P; 
12854  774 
\<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P 
775 
\<rbrakk> \<Longrightarrow> P" 

776 
apply cut_tac 

777 
apply (erule sxalloc_cases) 

778 
apply blast+ 

779 
done 

780 

781 
declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *) 

782 
declare split_paired_All [simp del] split_paired_Ex [simp del] 

24019  783 
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *} 
784 

23747  785 
inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')" 
12854  786 

23747  787 
inductive_cases eval_elim_cases [cases set]: 
21765  788 
"G\<turnstile>(Some xc,s) \<midarrow>t \<succ>\<rightarrow> (v, s')" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

789 
"G\<turnstile>Norm s \<midarrow>In1r Skip \<succ>\<rightarrow> (x, s')" 
21765  790 
"G\<turnstile>Norm s \<midarrow>In1r (Jmp j) \<succ>\<rightarrow> (x, s')" 
791 
"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c) \<succ>\<rightarrow> (x, s')" 

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

792 
"G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

793 
"G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

794 
"G\<turnstile>Norm s \<midarrow>In1l (Lit w) \<succ>\<rightarrow> (v, s')" 
21765  795 
"G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e) \<succ>\<rightarrow> (v, s')" 
796 
"G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2) \<succ>\<rightarrow> (v, s')" 

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

797 
"G\<turnstile>Norm s \<midarrow>In2 (LVar vn) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

798 
"G\<turnstile>Norm s \<midarrow>In1l (Cast T e) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

799 
"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

800 
"G\<turnstile>Norm s \<midarrow>In1l (Super) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

801 
"G\<turnstile>Norm s \<midarrow>In1l (Acc va) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

802 
"G\<turnstile>Norm s \<midarrow>In1r (Expr e) \<succ>\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

803 
"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2) \<succ>\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

804 
"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig) \<succ>\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

805 
"G\<turnstile>Norm s \<midarrow>In1l (Body D c) \<succ>\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

806 
"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

807 
"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2) \<succ>\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

808 
"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c) \<succ>\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

809 
"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2) \<succ>\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

810 
"G\<turnstile>Norm s \<midarrow>In1r (Throw e) \<succ>\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

811 
"G\<turnstile>Norm s \<midarrow>In1l (NewC C) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

812 
"G\<turnstile>Norm s \<midarrow>In1l (New T[e]) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

813 
"G\<turnstile>Norm s \<midarrow>In1l (Ass va e) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

814 
"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2) \<succ>\<rightarrow> (x, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

815 
"G\<turnstile>Norm s \<midarrow>In2 ({accC,statDeclC,stat}e..fn) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

816 
"G\<turnstile>Norm s \<midarrow>In2 (e1.[e2]) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

817 
"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> (v, s')" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
28524
diff
changeset

818 
"G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<rightarrow> (x, s')" 
12854  819 
declare not_None_eq [simp] (* IntDef.Zero_def [simp] *) 
820 
declare split_paired_All [simp] split_paired_Ex [simp] 

24019  821 
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} 
12854  822 
declare split_if [split] split_if_asm [split] 
823 
option.split [split] option.split_asm [split] 

824 

825 
lemma eval_Inj_elim: 

826 
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') 

827 
\<Longrightarrow> case t of 

828 
In1 ec \<Rightarrow> (case ec of 

829 
Inl e \<Rightarrow> (\<exists>v. w = In1 v) 

830 
 Inr c \<Rightarrow> w = \<diamondsuit>) 

831 
 In2 e \<Rightarrow> (\<exists>v. w = In2 v) 

832 
 In3 e \<Rightarrow> (\<exists>v. w = In3 v)" 

833 
apply (erule eval_cases) 

834 
apply auto 

835 
apply (induct_tac "t") 

836 
apply (induct_tac "a") 

837 
apply auto 

838 
done 

839 

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:
13601
diff
changeset

840 
text {* The following simplification procedures set up the proper injections 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:
13601
diff
changeset

841 
terms and their corresponding values in the evaluation relation: 
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:
13601
diff
changeset

842 
E.g. an expression 
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:
13601
diff
changeset

843 
(injection @{term In1l} into terms) always evaluates to ordinary values 
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:
13601
diff
changeset

844 
(injection @{term In1} into generalised values @{term vals}). 
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:
13601
diff
changeset

845 
*} 
21765  846 

847 
lemma eval_expr_eq: "G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s') = (\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t\<succ>v \<rightarrow> s')" 

848 
by (auto, frule eval_Inj_elim, auto) 

849 

850 
lemma eval_var_eq: "G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s') = (\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s')" 

851 
by (auto, frule eval_Inj_elim, auto) 

852 

853 
lemma eval_exprs_eq: "G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s') = (\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s')" 

854 
by (auto, frule eval_Inj_elim, auto) 

855 

856 
lemma eval_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<rightarrow> s')" 

857 
by (auto, frule eval_Inj_elim, auto, frule eval_Inj_elim, auto) 

858 

24019  859 
simproc_setup eval_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s')") = {* 
860 
fn _ => fn _ => fn ct => 

861 
(case Thm.term_of ct of 

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

863 
 _ => SOME (mk_meta_eq @{thm eval_expr_eq})) *} 

864 

865 
simproc_setup eval_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s')") = {* 

866 
fn _ => fn _ => fn ct => 

867 
(case Thm.term_of ct of 

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

869 
 _ => SOME (mk_meta_eq @{thm eval_var_eq})) *} 

870 

871 
simproc_setup eval_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s')") = {* 

872 
fn _ => fn _ => fn ct => 

873 
(case Thm.term_of ct of 

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

875 
 _ => SOME (mk_meta_eq @{thm eval_exprs_eq})) *} 

876 

877 
simproc_setup eval_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s')") = {* 

878 
fn _ => fn _ => fn ct => 

879 
(case Thm.term_of ct of 

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

881 
 _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *} 

882 

26480  883 
ML {* 
27226  884 
bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt}) 
12854  885 
*} 
886 

24019  887 
declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!] 
12854  888 

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

889 
text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

890 
used in smallstep semantics, not in the bigstep semantics. So their is no 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

891 
valid evaluation of these terms 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

893 

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

894 

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

895 
lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e\<succ>v\<rightarrow> s' = False" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

897 
{ fix s t v s' 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

898 
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

900 
callee: "t=In1l (Callee l e)" 
21765  901 
then have "False" by induct auto 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

903 
then show ?thesis 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
41778
diff
changeset

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

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

906 

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

907 

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

908 
lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e\<succ>v\<rightarrow> s' = False" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

910 
{ fix s t v s' 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

911 
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

913 
callee: "t=In1l (InsInitE c e)" 
21765  914 
then have "False" by induct auto 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

916 
then show ?thesis 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
41778
diff
changeset

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

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

919 

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

920 
lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

922 
{ fix s t v s' 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

923 
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

925 
callee: "t=In2 (InsInitV c w)" 
21765  926 
then have "False" by induct auto 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

928 
then show ?thesis 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
41778
diff
changeset

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

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

931 

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

932 
lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

934 
{ fix s t v s' 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

935 
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

937 
callee: "t=In1r (FinA a c)" 
21765  938 
then have "False" by induct auto 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

940 
then show ?thesis 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
41778
diff
changeset

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

942 
qed 
12854  943 

944 
lemma eval_no_abrupt_lemma: 

945 
"\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s" 

946 
by (erule eval_cases, auto) 

947 

948 
lemma eval_no_abrupt: 

949 
"G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = 

950 
(x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))" 

951 
apply auto 

952 
apply (frule eval_no_abrupt_lemma, auto)+ 

953 
done 

954 

24019  955 
simproc_setup eval_no_abrupt ("G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')") = {* 
956 
fn _ => fn _ => fn ct => 

957 
(case Thm.term_of ct of 

24165  958 
(_ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name None}, _)) $ _) $ _ $ _ $ _) => NONE 
24019  959 
 _ => SOME (mk_meta_eq @{thm eval_no_abrupt})) 
12854  960 
*} 
961 

962 

963 
lemma eval_abrupt_lemma: 

28524  964 
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = undefined3 t" 
12854  965 
by (erule eval_cases, auto) 
966 

967 
lemma eval_abrupt: 

968 
" G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') = 

28524  969 
(s'=(Some xc,s) \<and> w=undefined3 t \<and> 
970 
G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (undefined3 t,(Some xc,s)))" 

12854  971 
apply auto 
972 
apply (frule eval_abrupt_lemma, auto)+ 

973 
done 

974 

24019  975 
simproc_setup eval_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')") = {* 
976 
fn _ => fn _ => fn ct => 

977 
(case Thm.term_of ct of 

24165  978 
(_ $ _ $ _ $ _ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name Some}, _) $ _)$ _)) => NONE 
24019  979 
 _ => SOME (mk_meta_eq @{thm eval_abrupt})) 
12854  980 
*} 
981 

28524  982 
lemma LitI: "G\<turnstile>s \<midarrow>Lit v\<succ>(if normal s then v else undefined)\<rightarrow> s" 
12854  983 
apply (case_tac "s", case_tac "a = None") 
984 
by (auto intro!: eval.Lit) 

985 

986 
lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s" 

987 
apply (case_tac "s", case_tac "a = None") 

988 
by (auto intro!: eval.Skip) 

989 

990 
lemma ExprI: "G\<turnstile>s \<midarrow>e\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'" 

991 
apply (case_tac "s", case_tac "a = None") 

992 
by (auto intro!: eval.Expr) 

993 

994 
lemma CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<rightarrow> s2" 

995 
apply (case_tac "s", case_tac "a = None") 

996 
by (auto intro!: eval.Comp) 

997 

998 
lemma CondI: 

999 
"\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e\<succ>b\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow> 

28524  1000 
G\<turnstile>s \<midarrow>e ? e1 : e2\<succ>(if normal s1 then v else undefined)\<rightarrow> s2" 
12854  1001 
apply (case_tac "s", case_tac "a = None") 
1002 
by (auto intro!: eval.Cond) 

1003 

1004 
lemma IfI: "\<lbrakk>G\<turnstile>s \<midarrow>e\<succ>v\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<rightarrow> s2\<rbrakk> 

1005 
\<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2" 

1006 
apply (case_tac "s", case_tac "a = None") 

1007 
by (auto intro!: eval.If) 

1008 

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

1009 
lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig\<succ>v\<rightarrow> s' 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

1010 
\<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig\<succ>v\<rightarrow> s'" 
12854  1011 
apply (case_tac "s", case_tac "a = None") 
1012 
by (auto intro!: eval.Methd) 

1013 

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

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

1015 
"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

1016 
D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

1017 
s3 = init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

1018 
s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

1019 
G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>\<succ> v\<rightarrow> s4; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

1020 
s4' = restore_lvars s2 s4\<rbrakk> \<Longrightarrow> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

1021 
G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}ps)\<succ>v\<rightarrow> s4'" 
12854  1022 
apply (drule eval.Call, assumption) 
1023 
apply (rule HOL.refl) 

1024 
apply simp+ 

1025 
done 

1026 

1027 
lemma eval_Init: 

1028 
"\<lbrakk>if inited C (globs s0) then s3 = Norm s0 

1029 
else G\<turnstile>Norm (init_class_obj G C s0) 

1030 
\<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and> 

1031 
G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and> 

1032 
s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow> 

1033 
G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3" 

1034 
apply (rule eval.Init) 

1035 
apply auto 

1036 
done 

1037 

1038 
lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s" 

1039 
apply (case_tac "s", simp) 

1040 
apply (case_tac "a") 

1041 
apply safe 

1042 
apply (rule eval_Init) 

1043 
apply auto 

1044 
done 

1045 

1046 
lemma eval_StatRef: 

28524  1047 
"G\<turnstile>s \<midarrow>StatRef rt\<succ>(if abrupt s=None then Null else undefined)\<rightarrow> s" 
12854  1048 
apply (case_tac "s", simp) 
1049 
apply (case_tac "a = None") 

1050 
apply (auto del: eval.Abrupt intro!: eval.intros) 

1051 
done 

1052 

1053 

1054 
lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" 

1055 
apply (erule eval_cases) 

1056 
by auto 

1057 

1058 
lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')" 

1059 
by auto 

1060 

1061 
(*unused*) 

1062 
lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> 

1063 
(\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))" 

1064 
apply (erule eval.induct) 

1065 
apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+ 

1066 
apply auto 

1067 
done 

1068 

1069 
lemma halloc_xcpt [dest!]: 

1070 
"\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)" 

1071 
apply (erule_tac halloc_elim_cases) 

1072 
by auto 

1073 

1074 
(* 

1075 
G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This" 

1076 
G\<turnstile>(x,(h,l)) \<midarrow>s \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This" 

1077 
*) 

1078 

1079 
lemma eval_Methd: 

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

1080 
"G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

1081 
\<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')" 
12854  1082 
apply (case_tac "s") 
1083 
apply (case_tac "a") 

1084 
apply clarsimp+ 

1085 
apply (erule eval.Methd) 

1086 
apply (drule eval_abrupt_lemma) 

1087 
apply force 

1088 
done 

1089 

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:
13601
diff
changeset

1090 
lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2; 
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:
13601
diff
changeset

1091 
res=the (locals (store s2) Result); 
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:
13601
diff
changeset

1092 
s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or> 
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:
13601
diff
changeset

1093 
abrupt s2 = Some (Jump (Cont l))) 
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:
13601
diff
changeset

1094 
then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
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:
13601
diff
changeset

1095 
else s2); 
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:
13601
diff
changeset

1096 
s4=abupd (absorb Ret) s3\<rbrakk> \<Longrightarrow> 
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:
13601
diff
changeset

1097 
G\<turnstile>Norm s0 \<midarrow>Body D c\<succ>res\<rightarrow>s4" 
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:
13601
diff
changeset

1098 
by (auto elim: eval.Body) 
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:
13601
diff
changeset

1099 

13384  1100 
lemma eval_binop_arg2_indep: 
1101 
"\<not> need_second_arg binop v1 \<Longrightarrow> eval_binop binop v1 x = eval_binop binop v1 y" 

1102 
by (cases binop) 

1103 
(simp_all add: need_second_arg_def) 

1104 

1105 

1106 
lemma eval_BinOp_arg2_indepI: 

1107 
assumes eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1\<succ>v1\<rightarrow> s1" and 

1108 
no_need: "\<not> need_second_arg binop v1" 

1109 
shows "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2\<succ>(eval_binop binop v1 v2)\<rightarrow> s1" 

1110 
(is "?EvalBinOp v2") 

1111 
proof  

1112 
from eval_e1 

1113 
have "?EvalBinOp Unit" 

1114 
by (rule eval.BinOp) 

1115 
(simp add: no_need) 

1116 
moreover 

1117 
from no_need 

1118 
have "eval_binop binop v1 Unit = eval_binop binop v1 v2" 

1119 
by (simp add: eval_binop_arg2_indep) 

1120 
ultimately 

1121 
show ?thesis 

1122 
by simp 

1123 
qed 

1124 

12854  1125 

1126 
section "single valued" 

1127 

1128 
lemma unique_halloc [rule_format (no_asm)]: 

21765  1129 
"G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>halloc oi\<succ>a' \<rightarrow> s'' \<longrightarrow> a' = a \<and> s'' = s'" 
12854  1130 
apply (erule halloc.induct) 
1131 
apply (auto elim!: halloc_elim_cases split del: split_if split_if_asm) 

1132 
apply (drule trans [THEN sym], erule sym) 

1133 
defer 

1134 
apply (drule trans [THEN sym], erule sym) 

1135 
apply auto 

1136 
done 

1137 

1138 

1139 
lemma single_valued_halloc: 

1140 
"single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}" 

1141 
apply (unfold single_valued_def) 

1142 
by (clarsimp, drule (1) unique_halloc, auto) 

1143 

1144 

1145 
lemma unique_sxalloc [rule_format (no_asm)]: 

21765  1146 
"G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'" 
12854  1147 
apply (erule sxalloc.induct) 
1148 
apply (auto dest: unique_halloc elim!: sxalloc_elim_cases 

1149 
split del: split_if split_if_asm) 

1150 
done 

1151 

1152 
lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}" 

1153 
apply (unfold single_valued_def) 

1154 
apply (blast dest: unique_sxalloc) 

1155 
done 

1156 

1157 
lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p" 

1158 
by auto 

1159 

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:
13601
diff
changeset

1160 

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

1161 

12854  1162 
lemma unique_eval [rule_format (no_asm)]: 
21765  1163 
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w, s') \<Longrightarrow> (\<forall>w' s''. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w', s'') \<longrightarrow> w' = w \<and> s'' = s')" 
12854  1164 
apply (erule eval_induct) 
1165 
apply (tactic {* ALLGOALS (EVERY' 

39159  1166 
[strip_tac, rotate_tac ~1, eresolve_tac @{thms eval_elim_cases}]) *}) 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

1168 
prefer 28 (* Try *) 
12854  1169 
apply (simp (no_asm_use) only: split add: split_if_asm) 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

1171 
prefer 30 (* Init *) 
21765  1172 
apply (case_tac "inited C (globs s0)", (simp only: if_True if_False simp_thms)+) 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

1173 
prefer 26 (* While *) 
12854  1174 
apply (simp (no_asm_use) only: split add: split_if_asm, blast) 
21765  1175 
(* 36 subgoals *) 
12854  1176 
apply (blast dest: unique_sxalloc unique_halloc split_pairD)+ 
1177 
done 

1178 

1179 
(* unused *) 

1180 
lemma single_valued_eval: 

21765  1181 
"single_valued {((s, t), (v, s')). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')}" 
12854  1182 
apply (unfold single_valued_def) 
1183 
by (clarify, drule (1) unique_eval, auto) 

1184 

1185 
end 