author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 41778  5f79a9e42507 
child 56199  8e8d28ed7529 
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 

41778  60 
type_synonym 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 *} 

41778  81 
type_synonym 
13337
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 
35431  91 
(type) "locals" <= (type) "(lname, val) table" 
13337
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 

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

12854  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 

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

12854  242 

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

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

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

245 

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

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

247 
where "!!v == Acc (LVar (EName (VNam v)))" 
12854  248 

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

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

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

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

252 

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

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

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

255 
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

256 

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

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

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

259 
where "StatRef rt == Cast (RefT rt) (Lit Null)" 
12854  260 

37956  261 
definition 
262 
is_stmt :: "term \<Rightarrow> bool" 

263 
where "is_stmt t = (\<exists>c. t=In1r c)" 

12854  264 

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

267 
declare is_stmt_rews [simp] 

13345  268 

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

269 
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

270 
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

271 
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

272 
*} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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 

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

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

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

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

277 

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

280 
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

281 

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

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

285 

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 
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

288 
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

289 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

290 
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

291 
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

292 
*} 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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 

35315  294 
class inj_term = 
295 
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

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 
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

298 
@{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

299 
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

300 
@{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

301 
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

302 
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

303 
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

304 
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

305 
*} 
13345  306 

35315  307 
instantiation stmt :: inj_term 
308 
begin 

13345  309 

35315  310 
definition 
37956  311 
stmt_inj_term_def: "\<langle>c::stmt\<rangle> = In1r c" 
35315  312 

313 
instance .. 

314 

315 
end 

13345  316 

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

318 
by (simp add: stmt_inj_term_def) 

319 

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

320 
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

321 
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

322 

35315  323 
instantiation expr :: inj_term 
324 
begin 

13345  325 

35315  326 
definition 
37956  327 
expr_inj_term_def: "\<langle>e::expr\<rangle> = In1l e" 
35315  328 

329 
instance .. 

330 

331 
end 

13345  332 

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

334 
by (simp add: expr_inj_term_def) 

335 

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

336 
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

337 
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

338 

35315  339 
instantiation var :: inj_term 
340 
begin 

13345  341 

35315  342 
definition 
37956  343 
var_inj_term_def: "\<langle>v::var\<rangle> = In2 v" 
35315  344 

345 
instance .. 

346 

347 
end 

13345  348 

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

350 
by (simp add: var_inj_term_def) 

351 

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

352 
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

353 
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

354 

35315  355 
class expr_of = 
356 
fixes expr_of :: "'a \<Rightarrow> expr" 

357 

358 
instantiation expr :: expr_of 

359 
begin 

360 

361 
definition 

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

363 

364 
instance .. 

365 

366 
end 

13345  367 

35315  368 
instantiation list :: (expr_of) inj_term 
369 
begin 

370 

371 
definition 

37956  372 
"\<langle>es::'a list\<rangle> = In3 (map expr_of es)" 
35315  373 

374 
instance .. 

375 

376 
end 

377 

378 
lemma expr_list_inj_term_def: 

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

380 
by (simp add: inj_term_list_def expr_of_expr_def) 

13345  381 

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

383 
by (simp add: expr_list_inj_term_def) 

384 

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

385 
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

386 
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

387 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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

388 
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

389 
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

390 
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

391 
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

392 
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

393 
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

394 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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 
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

396 
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

397 
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

398 
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

399 
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

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 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

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_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

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 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

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 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

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 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

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_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

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 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

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 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

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_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

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 

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

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

421 
\<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

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

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

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

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

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

427 

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

428 
section {* Evaluation of unary operations *} 
37956  429 
primrec eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val" 
430 
where 

431 
"eval_unop UPlus v = Intg (the_Intg v)" 

432 
 "eval_unop UMinus v = Intg ( (the_Intg v))" 

433 
 "eval_unop UBitNot v = Intg 42"  "FIXME: Not yet implemented" 

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

435 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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 
section {* Evaluation of binary operations *} 
37956  437 
primrec eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val" 
438 
where 

439 
"eval_binop Mul v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 

440 
 "eval_binop Div v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))" 

441 
 "eval_binop Mod v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))" 

442 
 "eval_binop Plus v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))" 

443 
 "eval_binop Minus v1 v2 = Intg ((the_Intg v1)  (the_Intg v2))" 

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

444 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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 
 "Be aware of the explicit coercion of the shift distance to nat" 
37956  446 
 "eval_binop LShift v1 v2 = Intg ((the_Intg v1) * (2^(nat (the_Intg v2))))" 
447 
 "eval_binop RShift v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))" 

448 
 "eval_binop RShiftU v1 v2 = Intg 42" "FIXME: Not yet implemented" 

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

449 

37956  450 
 "eval_binop Less v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
451 
 "eval_binop Le v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))" 

452 
 "eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))" 

453 
 "eval_binop Ge v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))" 

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

454 

37956  455 
 "eval_binop Eq v1 v2 = Bool (v1=v2)" 
456 
 "eval_binop Neq v1 v2 = Bool (v1\<noteq>v2)" 

457 
 "eval_binop BitAnd v1 v2 = Intg 42"  "FIXME: Not yet implemented" 

458 
 "eval_binop And v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))" 

459 
 "eval_binop BitXor v1 v2 = Intg 42"  "FIXME: Not yet implemented" 

460 
 "eval_binop Xor v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))" 

461 
 "eval_binop BitOr v1 v2 = Intg 42"  "FIXME: Not yet implemented" 

462 
 "eval_binop Or v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))" 

463 
 "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))" 

464 
 "eval_binop CondOr v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))" 

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

465 

37956  466 
definition 
467 
need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where 

468 
"need_second_arg binop v1 = (\<not> ((binop=CondAnd \<and> \<not> the_Bool v1) \<or> 

469 
(binop=CondOr \<and> the_Bool v1)))" 

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

470 
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

471 
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

472 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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 
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

474 
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

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_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

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_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

480 
"\<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

481 
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

482 
(simp_all add: need_second_arg_def) 
12854  483 
end 