author | schirmer |
Tue, 16 Jul 2002 20:25:21 +0200 | |
changeset 13384 | a34e38154413 |
parent 13358 | c837ba4cfb62 |
child 13688 | a0b16d42d489 |
permissions | -rw-r--r-- |
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 |
non-standard 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 non-assignable 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 one-dimensional 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 type-checking 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 |
type-checking. 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 |
|
13384 | 63 |
types locals = "(lname, val) table" --{* local variables *} |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
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 |
13384 | 67 |
= Break label --{* break *} |
68 |
| Cont label --{* continue *} |
|
69 |
| 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
|
70 |
|
13384 | 71 |
datatype xcpt --{* exception *} |
72 |
= Loc loc --{* location of allocated execption object *} |
|
73 |
| 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
|
74 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
75 |
datatype error |
13384 | 76 |
= AccessViolation --{* Access to a member that isn't permitted *} |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
77 |
|
13384 | 78 |
datatype abrupt --{* abrupt completion *} |
79 |
= Xcpt xcpt --{* exception *} |
|
80 |
| Jump jump --{* break, continue, return *} |
|
81 |
| Error error -- {* runtime errors, we wan't to detect and proof absent |
|
82 |
in welltyped programms *} |
|
13337
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 |
|
13384 | 95 |
datatype inv_mode --{* invocation mode for method calls *} |
96 |
= Static --{* static *} |
|
97 |
| SuperM --{* super *} |
|
98 |
| IntVir --{* interface or virtual *} |
|
12854 | 99 |
|
13384 | 100 |
record sig = --{* signature of a method, cf. 8.4.2 *} |
101 |
name ::"mname" --{* acutally belongs to Decl.thy *} |
|
12854 | 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 |
||
13384 | 108 |
--{* function codes for unary operations *} |
109 |
datatype unop = UPlus -- {*{\tt +} unary plus*} |
|
110 |
| UMinus -- {*{\tt -} unary minus*} |
|
111 |
| UBitNot -- {*{\tt ~} bitwise NOT*} |
|
112 |
| 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
|
113 |
|
13384 | 114 |
--{* function codes for binary operations *} |
115 |
datatype binop = Mul -- {*{\tt * } multiplication*} |
|
116 |
| Div -- {*{\tt /} division*} |
|
117 |
| Mod -- {*{\tt \%} remainder*} |
|
118 |
| Plus -- {*{\tt +} addition*} |
|
119 |
| Minus -- {*{\tt -} subtraction*} |
|
120 |
| LShift -- {*{\tt <<} left shift*} |
|
121 |
| RShift -- {*{\tt >>} signed right shift*} |
|
122 |
| RShiftU -- {*{\tt >>>} unsigned right shift*} |
|
123 |
| Less -- {*{\tt <} less than*} |
|
124 |
| Le -- {*{\tt <=} less than or equal*} |
|
125 |
| Greater -- {*{\tt >} greater than*} |
|
126 |
| Ge -- {*{\tt >=} greater than or equal*} |
|
127 |
| Eq -- {*{\tt ==} equal*} |
|
128 |
| Neq -- {*{\tt !=} not equal*} |
|
129 |
| BitAnd -- {*{\tt \&} bitwise AND*} |
|
130 |
| And -- {*{\tt \&} boolean AND*} |
|
131 |
| BitXor -- {*{\texttt \^} bitwise Xor*} |
|
132 |
| Xor -- {*{\texttt \^} boolean Xor*} |
|
133 |
| BitOr -- {*{\tt |} bitwise Or*} |
|
134 |
| Or -- {*{\tt |} boolean Or*} |
|
135 |
| CondAnd -- {*{\tt \&\&} conditional And*} |
|
136 |
| CondOr -- {*{\tt ||} conditional Or *} |
|
137 |
text{* The boolean operators {\tt \&} and {\tt |} strictly evaluate both |
|
138 |
of their arguments. The conditional operators {\tt \&\&} and {\tt ||} only |
|
139 |
evaluate the second argument if the value of the whole expression isn't |
|
140 |
allready determined by the first argument. |
|
141 |
e.g.: {\tt false \&\& e} e is not evaluated; |
|
142 |
{\tt true || e} e is not evaluated; |
|
143 |
*} |
|
13358 | 144 |
|
12854 | 145 |
datatype var |
13384 | 146 |
= LVar lname --{* local variable (incl. parameters) *} |
147 |
| FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90) |
|
148 |
--{* class field *} |
|
149 |
--{* @{term "{accC,statDeclC,stat}e..fn"} *} |
|
150 |
--{* @{text accC}: accessing class (static class were *} |
|
151 |
--{* the code is declared. Annotation only needed for *} |
|
152 |
--{* evaluation to check accessibility) *} |
|
153 |
--{* @{text statDeclC}: static declaration class of field*} |
|
154 |
--{* @{text stat}: static or instance field?*} |
|
155 |
--{* @{text e}: reference to object*} |
|
156 |
--{* @{text fn}: field name*} |
|
157 |
| AVar expr expr ("_.[_]"[90,10 ]90) |
|
158 |
--{* array component *} |
|
159 |
--{* @{term "e1.[e2]"}: e1 array reference; e2 index *} |
|
160 |
| InsInitV stmt var |
|
161 |
--{* insertion of initialization before evaluation *} |
|
162 |
--{* of var (technical term for smallstep semantics.)*} |
|
12854 | 163 |
|
164 |
and expr |
|
13384 | 165 |
= NewC qtname --{* class instance creation *} |
166 |
| NewA ty expr ("New _[_]"[99,10 ]85) |
|
167 |
--{* array creation *} |
|
168 |
| Cast ty expr --{* type cast *} |
|
169 |
| Inst expr ref_ty ("_ InstOf _"[85,99] 85) |
|
170 |
--{* instanceof *} |
|
171 |
| Lit val --{* literal value, references not allowed *} |
|
172 |
| UnOp unop expr --{* unary operation *} |
|
173 |
| 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
|
174 |
|
13384 | 175 |
| Super --{* special Super keyword *} |
176 |
| Acc var --{* variable access *} |
|
177 |
| Ass var expr ("_:=_" [90,85 ]85) |
|
178 |
--{* variable assign *} |
|
179 |
| Cond expr expr expr ("_ ? _ : _" [85,85,80]80) --{* conditional *} |
|
180 |
| Call qtname ref_ty inv_mode expr mname "(ty list)" "(expr list)" |
|
181 |
("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) |
|
182 |
--{* method call *} |
|
183 |
--{* @{term "{accC,statT,mode}e\<cdot>mn({pTs}args)"} " *} |
|
184 |
--{* @{text accC}: accessing class (static class were *} |
|
185 |
--{* the call code is declared. Annotation only needed for*} |
|
186 |
--{* evaluation to check accessibility) *} |
|
187 |
--{* @{text statT}: static declaration class/interface of *} |
|
188 |
--{* method *} |
|
189 |
--{* @{text mode}: invocation mode *} |
|
190 |
--{* @{text e}: reference to object*} |
|
191 |
--{* @{text mn}: field name*} |
|
192 |
--{* @{text pTs}: types of parameters *} |
|
193 |
--{* @{text args}: the actual parameters/arguments *} |
|
194 |
| Methd qtname sig --{* (folded) method (see below) *} |
|
195 |
| Body qtname stmt --{* (unfolded) method body *} |
|
196 |
| InsInitE stmt expr |
|
197 |
--{* insertion of initialization before *} |
|
198 |
--{* evaluation of expr (technical term for smallstep sem.) *} |
|
199 |
| Callee locals expr --{* save callers locals in callee-Frame *} |
|
200 |
--{* (technical term for smallstep semantics) *} |
|
12854 | 201 |
and stmt |
13384 | 202 |
= Skip --{* empty statement *} |
203 |
| Expr expr --{* expression statement *} |
|
204 |
| Lab jump stmt ("_\<bullet> _" [ 99,66]66) |
|
205 |
--{* labeled statement; handles break *} |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
206 |
| Comp stmt stmt ("_;; _" [ 66,65]65) |
13384 | 207 |
| If_ expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70) |
208 |
| Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70) |
|
209 |
| Do jump --{* break, continue, return *} |
|
12854 | 210 |
| Throw expr |
13384 | 211 |
| TryC stmt qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70) |
212 |
--{* @{term "Try c1 Catch(C vn) c2"} *} |
|
213 |
--{* @{text c1}: block were exception may be thrown *} |
|
214 |
--{* @{text C}: execption class to catch *} |
|
215 |
--{* @{text vn}: local name for exception used in @{text c2}*} |
|
216 |
--{* @{text c2}: block to execute when exception is cateched*} |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
217 |
| Fin stmt stmt ("_ Finally _" [ 79,79]70) |
13384 | 218 |
| FinA abopt stmt --{* Save abruption of first statement *} |
219 |
--{* technical term for smallstep sem.) *} |
|
220 |
| Init qtname --{* class initialization *} |
|
12854 | 221 |
|
222 |
||
223 |
text {* |
|
224 |
The expressions Methd and Body are artificial program constructs, in the |
|
225 |
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
|
226 |
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
|
227 |
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
|
228 |
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
|
229 |
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
|
230 |
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
|
231 |
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
|
232 |
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
|
233 |
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
|
234 |
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
|
235 |
frame stack. |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
236 |
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
|
237 |
intermediate steps of class-initialisation. |
12854 | 238 |
*} |
239 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
240 |
types "term" = "(expr+stmt,var,expr list) sum3" |
12854 | 241 |
translations |
242 |
"sig" <= (type) "mname \<times> ty list" |
|
243 |
"var" <= (type) "Term.var" |
|
244 |
"expr" <= (type) "Term.expr" |
|
245 |
"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
|
246 |
"term" <= (type) "(expr+stmt,var,expr list) sum3" |
12854 | 247 |
|
248 |
syntax |
|
249 |
||
250 |
this :: expr |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
251 |
LAcc :: "vname \<Rightarrow> expr" ("!!") |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
252 |
LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85) |
12854 | 253 |
Return :: "expr \<Rightarrow> stmt" |
254 |
StatRef :: "ref_ty \<Rightarrow> expr" |
|
255 |
||
256 |
translations |
|
257 |
||
258 |
"this" == "Acc (LVar This)" |
|
259 |
"!!v" == "Acc (LVar (EName (VNam v)))" |
|
260 |
"v:==e" == "Expr (Ass (LVar (EName (VNam v))) e)" |
|
261 |
"Return e" == "Expr (Ass (LVar (EName Res)) e);; Do Ret" |
|
13384 | 262 |
--{* \tt Res := e;; Do Ret *} |
12854 | 263 |
"StatRef rt" == "Cast (RefT rt) (Lit Null)" |
264 |
||
265 |
constdefs |
|
266 |
||
267 |
is_stmt :: "term \<Rightarrow> bool" |
|
268 |
"is_stmt t \<equiv> \<exists>c. t=In1r c" |
|
269 |
||
270 |
ML {* |
|
271 |
bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def")); |
|
272 |
*} |
|
273 |
||
274 |
declare is_stmt_rews [simp] |
|
13345 | 275 |
|
276 |
axclass inj_term < "type" |
|
277 |
consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83) |
|
278 |
||
279 |
instance stmt::inj_term .. |
|
280 |
||
281 |
defs (overloaded) |
|
282 |
stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c" |
|
283 |
||
284 |
lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c" |
|
285 |
by (simp add: stmt_inj_term_def) |
|
286 |
||
287 |
instance expr::inj_term .. |
|
288 |
||
289 |
defs (overloaded) |
|
290 |
expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e" |
|
291 |
||
292 |
lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e" |
|
293 |
by (simp add: expr_inj_term_def) |
|
294 |
||
295 |
instance var::inj_term .. |
|
296 |
||
297 |
defs (overloaded) |
|
298 |
var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v" |
|
299 |
||
300 |
lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v" |
|
301 |
by (simp add: var_inj_term_def) |
|
302 |
||
303 |
instance "list":: (type) inj_term .. |
|
304 |
||
305 |
defs (overloaded) |
|
306 |
expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es" |
|
307 |
||
308 |
lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es" |
|
309 |
by (simp add: expr_list_inj_term_def) |
|
310 |
||
12854 | 311 |
end |