author  haftmann 
Tue, 23 Feb 2010 10:11:12 +0100  
changeset 35315  fbdc860d87a3 
parent 35069  09154b995ed8 
child 35416  d8d7d1b785af 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Term.thy 
12854  2 
Author: David von Oheimb 
3 
*) 

4 

5 
header {* Java expressions and statements *} 

6 

16417  7 
theory Term imports Value Table begin 
12854  8 

9 
text {* 

10 
design issues: 

11 
\begin{itemize} 

12 
\item invocation frames for local variables could be reduced to special static 

13 
objects (one per method). This would reduce redundancy, but yield a rather 

14 
nonstandard execution model more difficult to understand. 

15 
\item method bodies separated from calls to handle assumptions in axiomat. 

16 
semantics 

17 
NB: Body is intended to be in the environment of the called method. 

18 
\item class initialization is regarded as (auxiliary) statement 

19 
(required for AxSem) 

20 
\item result expression of method return is handled by a special result variable 

21 
result variable is treated uniformly with local variables 

22 
\begin{itemize} 

23 
\item[+] welltypedness and existence of the result/return expression is 

24 
ensured without extra efford 

25 
\end{itemize} 

26 
\end{itemize} 

27 

28 
simplifications: 

29 
\begin{itemize} 

30 
\item expression statement allowed for any expression 

31 
\item This is modeled as a special nonassignable local variable 

32 
\item Super is modeled as a general expression with the same value as This 

33 
\item access to field x in current class via This.x 

34 
\item NewA creates only onedimensional arrays; 

35 
initialization of further subarrays may be simulated with nested NewAs 

36 
\item The 'Lit' constructor is allowed to contain a reference value. 

37 
But this is assumed to be prohibited in the input language, which is enforced 

38 
by the typechecking rules. 

39 
\item a call of a static method via a type name may be simulated by a dummy 

40 
variable 

41 
\item no nested blocks with inner local variables 

42 
\item no synchronized statements 

43 
\item no secondary forms of if, while (e.g. no for) (may be easily simulated) 

44 
\item no switch (may be simulated with if) 

45 
\item the @{text try_catch_finally} statement is divided into the 

46 
@{text try_catch} statement 

47 
and a finally statement, which may be considered as try..finally with 

48 
empty catch 

49 
\item the @{text try_catch} statement has exactly one catch clause; 

50 
multiple ones can be 

51 
simulated with instanceof 

52 
\item the compiler is supposed to add the annotations {@{text _}} during 

53 
typechecking. This 

54 
transformation is left out as its result is checked by the type rules anyway 

55 
\end{itemize} 

56 
*} 

57 

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

58 

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

59 

13384  60 
types locals = "(lname, val) table" {* local variables *} 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

61 

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

62 

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

63 
datatype jump 
13384  64 
= Break label {* break *} 
65 
 Cont label {* continue *} 

66 
 Ret {* return from method *} 

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

67 

13384  68 
datatype xcpt {* exception *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

69 
= Loc loc {* location of allocated execption object *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

70 
 Std xname {* intermediate standard exception, see Eval.thy *} 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

71 

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

72 
datatype error 
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:
13384
diff
changeset

73 
= AccessViolation {* Access to a member that isn't permitted *} 
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:
13384
diff
changeset

74 
 CrossMethodJump {* Method exits with a break or continue *} 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

75 

13384  76 
datatype abrupt {* abrupt completion *} 
77 
= Xcpt xcpt {* exception *} 

78 
 Jump jump {* break, continue, return *} 

79 
 Error error  {* runtime errors, we wan't to detect and proof absent 

80 
in welltyped programms *} 

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

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

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

83 

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

84 
text {* Local variable store and exception. 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

85 
Anticipation of State.thy used by smallstep semantics. For a method call, 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

86 
we save the local variables of the caller in the term Callee to restore them 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

87 
after method return. Also an exception must be restored after the finally 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

89 

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

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

91 
"locals" <= (type) "(lname, val) table" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

92 

13384  93 
datatype inv_mode {* invocation mode for method calls *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

94 
= Static {* static *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

95 
 SuperM {* super *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

96 
 IntVir {* interface or virtual *} 
12854  97 

13384  98 
record sig = {* signature of a method, cf. 8.4.2 *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

99 
name ::"mname" {* acutally belongs to Decl.thy *} 
12854  100 
parTs::"ty list" 
101 

102 
translations 

103 
"sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>" 

104 
"sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>" 

105 

13384  106 
{* function codes for unary operations *} 
107 
datatype unop = UPlus  {*{\tt +} unary plus*} 

108 
 UMinus  {*{\tt } unary minus*} 

109 
 UBitNot  {*{\tt ~} bitwise NOT*} 

110 
 UNot  {*{\tt !} logical complement*} 

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

111 

13384  112 
{* function codes for binary operations *} 
113 
datatype binop = Mul  {*{\tt * } multiplication*} 

114 
 Div  {*{\tt /} division*} 

115 
 Mod  {*{\tt \%} remainder*} 

116 
 Plus  {*{\tt +} addition*} 

117 
 Minus  {*{\tt } subtraction*} 

118 
 LShift  {*{\tt <<} left shift*} 

119 
 RShift  {*{\tt >>} signed right shift*} 

120 
 RShiftU  {*{\tt >>>} unsigned right shift*} 

121 
 Less  {*{\tt <} less than*} 

122 
 Le  {*{\tt <=} less than or equal*} 

123 
 Greater  {*{\tt >} greater than*} 

124 
 Ge  {*{\tt >=} greater than or equal*} 

125 
 Eq  {*{\tt ==} equal*} 

126 
 Neq  {*{\tt !=} not equal*} 

127 
 BitAnd  {*{\tt \&} bitwise AND*} 

128 
 And  {*{\tt \&} boolean AND*} 

129 
 BitXor  {*{\texttt \^} bitwise Xor*} 

130 
 Xor  {*{\texttt \^} boolean Xor*} 

131 
 BitOr  {*{\tt } bitwise Or*} 

132 
 Or  {*{\tt } boolean Or*} 

133 
 CondAnd  {*{\tt \&\&} conditional And*} 

134 
 CondOr  {*{\tt } conditional Or *} 

135 
text{* The boolean operators {\tt \&} and {\tt } strictly evaluate both 

136 
of their arguments. The conditional operators {\tt \&\&} and {\tt } only 

137 
evaluate the second argument if the value of the whole expression isn't 

138 
allready determined by the first argument. 

139 
e.g.: {\tt false \&\& e} e is not evaluated; 

140 
{\tt true  e} e is not evaluated; 

141 
*} 

13358  142 

12854  143 
datatype var 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

144 
= LVar lname {* local variable (incl. parameters) *} 
13384  145 
 FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90) 
146 
{* class field *} 

147 
{* @{term "{accC,statDeclC,stat}e..fn"} *} 

148 
{* @{text accC}: accessing class (static class were *} 

149 
{* the code is declared. Annotation only needed for *} 

150 
{* evaluation to check accessibility) *} 

151 
{* @{text statDeclC}: static declaration class of field*} 

152 
{* @{text stat}: static or instance field?*} 

153 
{* @{text e}: reference to object*} 

154 
{* @{text fn}: field name*} 

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

155 
 AVar expr expr ("_.[_]"[90,10 ]90) 
13384  156 
{* array component *} 
157 
{* @{term "e1.[e2]"}: e1 array reference; e2 index *} 

158 
 InsInitV stmt var 

159 
{* insertion of initialization before evaluation *} 

160 
{* of var (technical term for smallstep semantics.)*} 

12854  161 

162 
and expr 

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

163 
= NewC qtname {* class instance creation *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

164 
 NewA ty expr ("New _[_]"[99,10 ]85) 
13384  165 
{* array creation *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

166 
 Cast ty expr {* type cast *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

167 
 Inst expr ref_ty ("_ InstOf _"[85,99] 85) 
13384  168 
{* instanceof *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

169 
 Lit val {* literal value, references not allowed *} 
13384  170 
 UnOp unop expr {* unary operation *} 
171 
 BinOp binop expr expr {* binary operation *} 

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

172 

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

173 
 Super {* special Super keyword *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

174 
 Acc var {* variable access *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

175 
 Ass var expr ("_:=_" [90,85 ]85) 
13384  176 
{* variable assign *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

177 
 Cond expr expr expr ("_ ? _ : _" [85,85,80]80) {* conditional *} 
13384  178 
 Call qtname ref_ty inv_mode expr mname "(ty list)" "(expr list)" 
179 
("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) 

180 
{* method call *} 

181 
{* @{term "{accC,statT,mode}e\<cdot>mn({pTs}args)"} " *} 

182 
{* @{text accC}: accessing class (static class were *} 

183 
{* the call code is declared. Annotation only needed for*} 

184 
{* evaluation to check accessibility) *} 

185 
{* @{text statT}: static declaration class/interface of *} 

186 
{* method *} 

187 
{* @{text mode}: invocation mode *} 

188 
{* @{text e}: reference to object*} 

189 
{* @{text mn}: field name*} 

190 
{* @{text pTs}: types of parameters *} 

191 
{* @{text args}: the actual parameters/arguments *} 

192 
 Methd qtname sig {* (folded) method (see below) *} 

193 
 Body qtname stmt {* (unfolded) method body *} 

194 
 InsInitE stmt expr 

195 
{* insertion of initialization before *} 

196 
{* evaluation of expr (technical term for smallstep sem.) *} 

197 
 Callee locals expr {* save callers locals in calleeFrame *} 

198 
{* (technical term for smallstep semantics) *} 

12854  199 
and stmt 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

200 
= Skip {* empty statement *} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

201 
 Expr expr {* expression statement *} 
13384  202 
 Lab jump stmt ("_\<bullet> _" [ 99,66]66) 
203 
{* labeled statement; handles break *} 

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

204 
 Comp stmt stmt ("_;; _" [ 66,65]65) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

205 
 If' expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

206 
 Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70) 
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:
13384
diff
changeset

207 
 Jmp jump {* break, continue, return *} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27226
diff
changeset

208 
 Throw expr 
13384  209 
 TryC stmt qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70) 
210 
{* @{term "Try c1 Catch(C vn) c2"} *} 

211 
{* @{text c1}: block were exception may be thrown *} 

212 
{* @{text C}: execption class to catch *} 

213 
{* @{text vn}: local name for exception used in @{text c2}*} 

214 
{* @{text c2}: block to execute when exception is cateched*} 

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

215 
 Fin stmt stmt ("_ Finally _" [ 79,79]70) 
13384  216 
 FinA abopt stmt {* Save abruption of first statement *} 
217 
{* technical term for smallstep sem.) *} 

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

218 
 Init qtname {* class initialization *} 
12854  219 

220 

221 
text {* 

222 
The expressions Methd and Body are artificial program constructs, in the 

223 
sense that they are not used to define a concrete Bali program. In the 

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

224 
operational semantic's they are "generated on the fly" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

225 
to decompose the task to define the behaviour of the Call expression. 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

226 
They are crucial for the axiomatic semantics to give a syntactic hook to insert 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

227 
some assertions (cf. AxSem.thy, Eval.thy). 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

228 
The Init statement (to initialize a class on its first use) is 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

229 
inserted in various places by the semantics. 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

230 
Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

231 
smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

232 
local variables of the caller for method return. So ve avoid modelling a 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

234 
The InsInitV/E terms are only used by the smallstep semantics to model the 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

235 
intermediate steps of classinitialisation. 
12854  236 
*} 
237 

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

238 
types "term" = "(expr+stmt,var,expr list) sum3" 
12854  239 
translations 
240 
"sig" <= (type) "mname \<times> ty list" 

241 
"var" <= (type) "Term.var" 

242 
"expr" <= (type) "Term.expr" 

243 
"stmt" <= (type) "Term.stmt" 

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

244 
"term" <= (type) "(expr+stmt,var,expr list) sum3" 
12854  245 

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

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

247 
where "this == Acc (LVar This)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

248 

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

249 
abbreviation LAcc :: "vname \<Rightarrow> expr" ("!!") 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

250 
where "!!v == Acc (LVar (EName (VNam v)))" 
12854  251 

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

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

253 
LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

254 
where "v:==e == Expr (Ass (LVar (EName (VNam v))) e)" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

255 

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

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

257 
Return :: "expr \<Rightarrow> stmt" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

258 
where "Return e == Expr (Ass (LVar (EName Res)) e);; Jmp Ret" {* \tt Res := e;; Jmp Ret *} 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

259 

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

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

261 
StatRef :: "ref_ty \<Rightarrow> expr" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

262 
where "StatRef rt == Cast (RefT rt) (Lit Null)" 
12854  263 

264 
constdefs 

265 

266 
is_stmt :: "term \<Rightarrow> bool" 

267 
"is_stmt t \<equiv> \<exists>c. t=In1r c" 

268 

27226  269 
ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *} 
12854  270 

271 
declare is_stmt_rews [simp] 

13345  272 

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

273 
text {* 
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:
13384
diff
changeset

274 
Here is some syntactic stuff to handle the injections of statements, 
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:
13384
diff
changeset

275 
expressions, variables and expression lists into general terms. 
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:
13384
diff
changeset

276 
*} 
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:
13384
diff
changeset

277 

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

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

279 
expr_inj_term :: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

280 
where "\<langle>e\<rangle>\<^sub>e == In1l e" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

281 

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

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

283 
stmt_inj_term :: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

284 
where "\<langle>c\<rangle>\<^sub>s == In1r c" 
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:
13384
diff
changeset

285 

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

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

287 
var_inj_term :: "var \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>v" 1000) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

288 
where "\<langle>v\<rangle>\<^sub>v == In2 v" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

289 

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

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

291 
lst_inj_term :: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000) 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

292 
where "\<langle>es\<rangle>\<^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:
13384
diff
changeset

293 

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

294 
text {* It seems to be more elegant to have an overloaded injection like 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:
13384
diff
changeset

295 
following. 
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:
13384
diff
changeset

296 
*} 
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:
13384
diff
changeset

297 

35315  298 
class inj_term = 
299 
fixes inj_term:: "'a \<Rightarrow> term" ("\<langle>_\<rangle>" 1000) 

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

300 

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

301 
text {* How this overloaded injections work can be seen in the theory 
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:
13384
diff
changeset

302 
@{text DefiniteAssignment}. Other big inductive relations 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:
13384
diff
changeset

303 
terms defined in theories @{text WellType}, @{text Eval}, @{text Evaln} and 
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:
13384
diff
changeset

304 
@{text AxSem} don't follow this convention right now, but introduce subtle 
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:
13384
diff
changeset

305 
syntactic sugar in the relations themselves to make a distinction 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:
13384
diff
changeset

306 
expressions, statements and so on. So unfortunately you will encounter a 
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

307 
mixture of dealing with these injections. The abbreviations above are used 
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:
13384
diff
changeset

308 
as bridge between the different conventions. 
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:
13384
diff
changeset

309 
*} 
13345  310 

35315  311 
instantiation stmt :: inj_term 
312 
begin 

13345  313 

35315  314 
definition 
315 
stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c" 

316 

317 
instance .. 

318 

319 
end 

13345  320 

321 
lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c" 

322 
by (simp add: stmt_inj_term_def) 

323 

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

324 
lemma stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y" 
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:
13384
diff
changeset

325 
by (simp add: stmt_inj_term_simp) 
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:
13384
diff
changeset

326 

35315  327 
instantiation expr :: inj_term 
328 
begin 

13345  329 

35315  330 
definition 
331 
expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e" 

332 

333 
instance .. 

334 

335 
end 

13345  336 

337 
lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e" 

338 
by (simp add: expr_inj_term_def) 

339 

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

340 
lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y" 
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:
13384
diff
changeset

341 
by (simp add: expr_inj_term_simp) 
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:
13384
diff
changeset

342 

35315  343 
instantiation var :: inj_term 
344 
begin 

13345  345 

35315  346 
definition 
347 
var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v" 

348 

349 
instance .. 

350 

351 
end 

13345  352 

353 
lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v" 

354 
by (simp add: var_inj_term_def) 

355 

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

356 
lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y" 
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:
13384
diff
changeset

357 
by (simp add: var_inj_term_simp) 
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:
13384
diff
changeset

358 

35315  359 
class expr_of = 
360 
fixes expr_of :: "'a \<Rightarrow> expr" 

361 

362 
instantiation expr :: expr_of 

363 
begin 

364 

365 
definition 

366 
"expr_of = (\<lambda>(e::expr). e)" 

367 

368 
instance .. 

369 

370 
end 

13345  371 

35315  372 
instantiation list :: (expr_of) inj_term 
373 
begin 

374 

375 
definition 

376 
"\<langle>es::'a list\<rangle> \<equiv> In3 (map expr_of es)" 

377 

378 
instance .. 

379 

380 
end 

381 

382 
lemma expr_list_inj_term_def: 

383 
"\<langle>es::expr list\<rangle> \<equiv> In3 es" 

384 
by (simp add: inj_term_list_def expr_of_expr_def) 

13345  385 

386 
lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es" 

387 
by (simp add: expr_list_inj_term_def) 

388 

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

389 
lemma expr_list_inj_term [iff]: "\<langle>x::expr list\<rangle> = \<langle>y\<rangle> \<equiv> x = y" 
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:
13384
diff
changeset

390 
by (simp add: expr_list_inj_term_simp) 
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:
13384
diff
changeset

391 

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

392 
lemmas inj_term_simps = stmt_inj_term_simp expr_inj_term_simp var_inj_term_simp 
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:
13384
diff
changeset

393 
expr_list_inj_term_simp 
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:
13384
diff
changeset

394 
lemmas inj_term_sym_simps = stmt_inj_term_simp [THEN sym] 
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:
13384
diff
changeset

395 
expr_inj_term_simp [THEN sym] 
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:
13384
diff
changeset

396 
var_inj_term_simp [THEN sym] 
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:
13384
diff
changeset

397 
expr_list_inj_term_simp [THEN sym] 
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:
13384
diff
changeset

398 

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

399 
lemma stmt_expr_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr\<rangle>" 
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:
13384
diff
changeset

400 
by (simp add: inj_term_simps) 
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:
13384
diff
changeset

401 
lemma expr_stmt_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::stmt\<rangle>" 
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:
13384
diff
changeset

402 
by (simp add: inj_term_simps) 
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:
13384
diff
changeset

403 
lemma stmt_var_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::var\<rangle>" 
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:
13384
diff
changeset

404 
by (simp add: inj_term_simps) 
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:
13384
diff
changeset

405 
lemma var_stmt_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::stmt\<rangle>" 
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:
13384
diff
changeset

406 
by (simp add: inj_term_simps) 
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:
13384
diff
changeset

407 
lemma stmt_elist_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr list\<rangle>" 
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:
13384
diff
changeset

408 
by (simp add: inj_term_simps) 
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:
13384
diff
changeset

409 
lemma elist_stmt_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::stmt\<rangle>" 
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:
13384
diff
changeset

410 
by (simp add: inj_term_simps) 
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:
13384
diff
changeset

411 
lemma expr_var_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::var\<rangle>" 
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:
13384
diff
changeset

412 
by (simp add: inj_term_simps) 
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:
13384
diff
changeset

413 
lemma var_expr_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr\<rangle>" 
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:
13384
diff
changeset

414 
by (simp add: inj_term_simps) 
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:
13384
diff
changeset

415 
lemma expr_elist_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::expr list\<rangle>" 
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:
13384
diff
changeset

416 
by (simp add: inj_term_simps) 
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:
13384
diff
changeset

417 
lemma elist_expr_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::expr\<rangle>" 
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:
13384
diff
changeset

418 
by (simp add: inj_term_simps) 
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:
13384
diff
changeset

419 
lemma var_elist_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr list\<rangle>" 
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:
13384
diff
changeset

420 
by (simp add: inj_term_simps) 
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:
13384
diff
changeset

421 
lemma elist_var_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::var\<rangle>" 
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:
13384
diff
changeset

422 
by (simp add: inj_term_simps) 
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:
13384
diff
changeset

423 

13690
ac335b2f4a39
Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents:
13688
diff
changeset

424 
lemma term_cases: " 
ac335b2f4a39
Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents:
13688
diff
changeset

425 
\<lbrakk>\<And> v. P \<langle>v\<rangle>\<^sub>v; \<And> e. P \<langle>e\<rangle>\<^sub>e;\<And> c. P \<langle>c\<rangle>\<^sub>s;\<And> l. P \<langle>l\<rangle>\<^sub>l\<rbrakk> 
ac335b2f4a39
Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents:
13688
diff
changeset

426 
\<Longrightarrow> P t" 
ac335b2f4a39
Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents:
13688
diff
changeset

427 
apply (cases t) 
ac335b2f4a39
Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents:
13688
diff
changeset

428 
apply (case_tac a) 
ac335b2f4a39
Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents:
13688
diff
changeset

429 
apply auto 
ac335b2f4a39
Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents:
13688
diff
changeset

430 
done 
ac335b2f4a39
Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents:
13688
diff
changeset

431 

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

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

433 
consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val" 
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:
13384
diff
changeset

434 
primrec 
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:
13384
diff
changeset

435 
"eval_unop UPlus v = Intg (the_Intg 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:
13384
diff
changeset

436 
"eval_unop UMinus v = Intg ( (the_Intg 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:
13384
diff
changeset

437 
"eval_unop UBitNot v = Intg 42"  "FIXME: Not yet implemented" 
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:
13384
diff
changeset

438 
"eval_unop UNot v = Bool (\<not> the_Bool 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:
13384
diff
changeset

439 

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

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

441 
consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val" 
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:
13384
diff
changeset

442 
primrec 
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:
13384
diff
changeset

443 
"eval_binop Mul v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
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:
13384
diff
changeset

444 
"eval_binop Div v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))" 
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:
13384
diff
changeset

445 
"eval_binop Mod v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))" 
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:
13384
diff
changeset

446 
"eval_binop Plus v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))" 
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:
13384
diff
changeset

447 
"eval_binop Minus v1 v2 = Intg ((the_Intg v1)  (the_Intg v2))" 
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:
13384
diff
changeset

448 

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

449 
 "Be aware of the explicit coercion of the shift distance to nat" 
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:
13384
diff
changeset

450 
"eval_binop LShift v1 v2 = Intg ((the_Intg v1) * (2^(nat (the_Intg v2))))" 
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:
13384
diff
changeset

451 
"eval_binop RShift v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))" 
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:
13384
diff
changeset

452 
"eval_binop RShiftU v1 v2 = Intg 42" "FIXME: Not yet implemented" 
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:
13384
diff
changeset

453 

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

454 
"eval_binop Less v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
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:
13384
diff
changeset

455 
"eval_binop Le v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))" 
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:
13384
diff
changeset

456 
"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))" 
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:
13384
diff
changeset

457 
"eval_binop Ge v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))" 
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:
13384
diff
changeset

458 

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

459 
"eval_binop Eq v1 v2 = Bool (v1=v2)" 
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:
13384
diff
changeset

460 
"eval_binop Neq v1 v2 = Bool (v1\<noteq>v2)" 
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:
13384
diff
changeset

461 
"eval_binop BitAnd v1 v2 = Intg 42"  "FIXME: Not yet implemented" 
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:
13384
diff
changeset

462 
"eval_binop And v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))" 
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:
13384
diff
changeset

463 
"eval_binop BitXor v1 v2 = Intg 42"  "FIXME: Not yet implemented" 
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:
13384
diff
changeset

464 
"eval_binop Xor v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))" 
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:
13384
diff
changeset

465 
"eval_binop BitOr v1 v2 = Intg 42"  "FIXME: Not yet implemented" 
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:
13384
diff
changeset

466 
"eval_binop Or v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))" 
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:
13384
diff
changeset

467 
"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))" 
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:
13384
diff
changeset

468 
"eval_binop CondOr v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))" 
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:
13384
diff
changeset

469 

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

470 
constdefs need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" 
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:
13384
diff
changeset

471 
"need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and> \<not> the_Bool v1) \<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:
13384
diff
changeset

472 
(binop=CondOr \<and> the_Bool v1))" 
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:
13384
diff
changeset

473 
text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument 
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:
13384
diff
changeset

474 
if the value isn't already determined by the first argument*} 
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:
13384
diff
changeset

475 

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

476 
lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13384
diff
changeset

477 
by (simp add: need_second_arg_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:
13384
diff
changeset

478 

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

479 
lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\<not> b)" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13384
diff
changeset

480 
by (simp add: need_second_arg_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:
13384
diff
changeset

481 

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

482 
lemma need_second_arg_strict[simp]: 
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:
13384
diff
changeset

483 
"\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13384
diff
changeset

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

485 
(simp_all add: need_second_arg_def) 
12854  486 
end 