author  schirmer 
Mon, 15 Jul 2002 10:41:34 +0200  
changeset 13358  c837ba4cfb62 
parent 13345  bd611943cbc2 
child 13384  a34e38154413 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Term.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

12858  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
12854  5 
*) 
6 

7 
header {* Java expressions and statements *} 

8 

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

9 
theory Term = Value + Table: 
12854  10 

11 
text {* 

12 
design issues: 

13 
\begin{itemize} 

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

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

16 
nonstandard execution model more difficult to understand. 

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

18 
semantics 

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

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

21 
(required for AxSem) 

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

23 
result variable is treated uniformly with local variables 

24 
\begin{itemize} 

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

26 
ensured without extra efford 

27 
\end{itemize} 

28 
\end{itemize} 

29 

30 
simplifications: 

31 
\begin{itemize} 

32 
\item expression statement allowed for any expression 

33 
\item no unary, binary, etc, operators 

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

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

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

37 
\item NewA creates only onedimensional arrays; 

38 
initialization of further subarrays may be simulated with nested NewAs 

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

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

41 
by the typechecking rules. 

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

43 
variable 

44 
\item no nested blocks with inner local variables 

45 
\item no synchronized statements 

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

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

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

49 
@{text try_catch} statement 

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

51 
empty catch 

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

53 
multiple ones can be 

54 
simulated with instanceof 

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

56 
typechecking. This 

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

58 
\end{itemize} 

59 
*} 

60 

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 
types locals = "(lname, val) table" (* local variables *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

64 

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

65 

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

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

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

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

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

70 

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

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

72 
= Loc loc (* location of allocated execption object *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

74 

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

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

76 
= AccessViolation (* Access to a member that isn't permitted *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

77 

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

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

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

80 
 Jump jump (* break, continue, return *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

81 
 Error error (* runtime errors, we wan't to detect and proof absent 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

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

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

85 

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

86 
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

87 
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

88 
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

89 
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

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

91 

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

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

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

94 

12854  95 
datatype inv_mode (* invocation mode for method calls *) 
96 
= Static (* static *) 

97 
 SuperM (* super *) 

98 
 IntVir (* interface or virtual *) 

99 

100 
record sig = (* signature of a method, cf. 8.4.2 *) 

101 
name ::"mname" (* acutally belongs to Decl.thy *) 

102 
parTs::"ty list" 

103 

104 
translations 

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

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

107 

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

108 
 "function codes for unary operations" 
13358  109 
datatype unop = UPlus 
110 
 UMinus 

111 
 UBitNot 

112 
 UNot 

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

113 

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

114 
 "function codes for binary operations" 
13358  115 
datatype binop = Mul 
116 
 Div 

117 
 Mod 

118 
 Plus 

119 
 Minus 

120 
 LShift 

121 
 RShift 

122 
 RShiftU 

123 
 Less 

124 
 Le 

125 
 Greater 

126 
 Ge 

127 
 Eq 

128 
 Neq 

129 
 BitAnd 

130 
 And 

131 
 BitXor 

132 
 Xor 

133 
 BitOr 

134 
 Or 

135 

12854  136 
datatype var 
137 
= LVar lname(* local variable (incl. parameters) *) 

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

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

139 
(*class field*)("{_,_,_}_.._"[10,10,10,85,99]90) 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

140 
 AVar expr expr (* array component *) ("_.[_]"[90,10 ]90) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

141 
 InsInitV stmt var (* insertion of initialization before 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

142 
evaluation of var (for smallstep sem.) *) 
12854  143 

144 
and expr 

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

145 
= NewC qtname (* class instance creation *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

146 
 NewA ty expr (* array creation *) ("New _[_]"[99,10 ]85) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

147 
 Cast ty expr (* type cast *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

148 
 Inst expr ref_ty (* instanceof *) ("_ InstOf _"[85,99] 85) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

149 
 Lit val (* literal value, references not allowed *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

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

152 

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

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

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

155 
 Ass var expr (* variable assign *) ("_:=_" [90,85 ]85) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

156 
 Cond expr expr expr (* conditional *) ("_ ? _ : _" [85,85,80]80) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

157 
 Call qtname ref_ty inv_mode expr mname "(ty list)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

158 
"(expr list)" (* method call *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

159 
("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

160 
 Methd qtname sig (* (folded) method (see below) *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

161 
 Body qtname stmt (* (unfolded) method body *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

162 
 InsInitE stmt expr (* insertion of initialization before 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

163 
evaluation of expr (for smallstep sem.) *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

164 
 Callee locals expr (* save Callers locals in CalleeFrame 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

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

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

169 
 Lab jump stmt ("_\<bullet> _"(* labeled statement*)[ 99,66]66) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

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

171 
 Comp stmt stmt ("_;; _" [ 66,65]65) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

172 
 If_ expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

173 
 Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

174 
 Do jump (* break, continue, return *) 
12854  175 
 Throw expr 
176 
 TryC stmt 

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

177 
qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

178 
 Fin stmt stmt ("_ Finally _" [ 79,79]70) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

179 
 FinA abopt stmt (* Save abruption of first statement 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

180 
(for smallstep sem.) *) 
12854  181 
 Init qtname (* class initialization *) 
182 

183 

184 
text {* 

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

186 
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

187 
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

188 
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

189 
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

190 
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

191 
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

192 
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

193 
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

194 
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

195 
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

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

197 
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

198 
intermediate steps of classinitialisation. 
12854  199 
*} 
200 

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

201 
types "term" = "(expr+stmt,var,expr list) sum3" 
12854  202 
translations 
203 
"sig" <= (type) "mname \<times> ty list" 

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

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

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

207 
"term" <= (type) "(expr+stmt,var,expr list) sum3" 
12854  208 

209 
syntax 

210 

211 
this :: expr 

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

212 
LAcc :: "vname \<Rightarrow> expr" ("!!") 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

213 
LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85) 
12854  214 
Return :: "expr \<Rightarrow> stmt" 
215 
StatRef :: "ref_ty \<Rightarrow> expr" 

216 

217 
translations 

218 

219 
"this" == "Acc (LVar This)" 

220 
"!!v" == "Acc (LVar (EName (VNam v)))" 

221 
"v:==e" == "Expr (Ass (LVar (EName (VNam v))) e)" 

222 
"Return e" == "Expr (Ass (LVar (EName Res)) e);; Do Ret" 

223 
(* Res := e;; Do Ret *) 

224 
"StatRef rt" == "Cast (RefT rt) (Lit Null)" 

225 

226 
constdefs 

227 

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

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

230 

231 
ML {* 

232 
bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def")); 

233 
*} 

234 

235 
declare is_stmt_rews [simp] 

13345  236 

237 
axclass inj_term < "type" 

238 
consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83) 

239 

240 
instance stmt::inj_term .. 

241 

242 
defs (overloaded) 

243 
stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c" 

244 

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

246 
by (simp add: stmt_inj_term_def) 

247 

248 
instance expr::inj_term .. 

249 

250 
defs (overloaded) 

251 
expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e" 

252 

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

254 
by (simp add: expr_inj_term_def) 

255 

256 
instance var::inj_term .. 

257 

258 
defs (overloaded) 

259 
var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v" 

260 

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

262 
by (simp add: var_inj_term_def) 

263 

264 
instance "list":: (type) inj_term .. 

265 

266 
defs (overloaded) 

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

268 

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

270 
by (simp add: expr_list_inj_term_def) 

271 

12854  272 
end 