1(*  Title:      HOL/Bali/Term.thy
2    Author:     David von Oheimb
3*)
4
5subsection \<open>Java expressions and statements\<close>
6
7theory Term imports Value Table begin
8
9text \<open>
10design 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  non-standard 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
28simplifications:
29\begin{itemize}
30\item expression statement allowed for any expression
31\item This  is modeled as a special non-assignable 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 one-dimensional 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 type-checking 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 \<open>try_catch_finally\<close> statement is divided into the 
46      \<open>try_catch\<close> statement 
47      and a finally statement, which may be considered as try..finally with 
48      empty catch
49\item the \<open>try_catch\<close> 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 {\<open>_\<close>} during 
53      type-checking. This
54  transformation is left out as its result is checked by the type rules anyway
55\end{itemize}
56\<close>
57
58
59
60type_synonym locals = "(lname, val) table"  \<comment> \<open>local variables\<close>
61
62
63datatype jump
64        = Break label \<comment> \<open>break\<close>
65        | Cont label  \<comment> \<open>continue\<close>
66        | Ret         \<comment> \<open>return from method\<close>
67
68datatype xcpt        \<comment> \<open>exception\<close>
69        = Loc loc    \<comment> \<open>location of allocated execption object\<close>
70        | Std xname  \<comment> \<open>intermediate standard exception, see Eval.thy\<close>
71
72datatype error
73       =  AccessViolation  \<comment> \<open>Access to a member that isn't permitted\<close>
74        | CrossMethodJump  \<comment> \<open>Method exits with a break or continue\<close>
75
76datatype abrupt       \<comment> \<open>abrupt completion\<close> 
77        = Xcpt xcpt   \<comment> \<open>exception\<close>
78        | Jump jump   \<comment> \<open>break, continue, return\<close>
79        | Error error \<comment> \<open>runtime errors, we wan't to detect and proof absent
80                            in welltyped programms\<close>
81type_synonym
82  abopt  = "abrupt option"
83
84text \<open>Local variable store and exception. 
85Anticipation of State.thy used by smallstep semantics. For a method call, 
86we save the local variables of the caller in the term Callee to restore them 
87after method return. Also an exception must be restored after the finally
88statement\<close>
89
90translations
91 (type) "locals" <= (type) "(lname, val) table"
92
93datatype inv_mode                  \<comment> \<open>invocation mode for method calls\<close>
94        = Static                   \<comment> \<open>static\<close>
95        | SuperM                   \<comment> \<open>super\<close>
96        | IntVir                   \<comment> \<open>interface or virtual\<close>
97
98record  sig =              \<comment> \<open>signature of a method, cf. 8.4.2\<close>
99          name ::"mname"   \<comment> \<open>acutally belongs to Decl.thy\<close>
100          parTs::"ty list"        
101
102translations
103  (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
104  (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
105
106\<comment> \<open>function codes for unary operations\<close>
107datatype unop =  UPlus    \<comment> \<open>{\tt +} unary plus\<close> 
108               | UMinus   \<comment> \<open>{\tt -} unary minus\<close>
109               | UBitNot  \<comment> \<open>{\tt ~} bitwise NOT\<close>
110               | UNot     \<comment> \<open>{\tt !} logical complement\<close>
111
112\<comment> \<open>function codes for binary operations\<close>
113datatype binop = Mul     \<comment> \<open>{\tt * }   multiplication\<close>
114               | Div     \<comment> \<open>{\tt /}   division\<close>
115               | Mod     \<comment> \<open>{\tt \%}   remainder\<close>
116               | Plus    \<comment> \<open>{\tt +}   addition\<close>
117               | Minus   \<comment> \<open>{\tt -}   subtraction\<close>
118               | LShift  \<comment> \<open>{\tt <<}  left shift\<close>
119               | RShift  \<comment> \<open>{\tt >>}  signed right shift\<close>
120               | RShiftU \<comment> \<open>{\tt >>>} unsigned right shift\<close>
121               | Less    \<comment> \<open>{\tt <}   less than\<close>
122               | Le      \<comment> \<open>{\tt <=}  less than or equal\<close>
123               | Greater \<comment> \<open>{\tt >}   greater than\<close>
124               | Ge      \<comment> \<open>{\tt >=}  greater than or equal\<close>
125               | Eq      \<comment> \<open>{\tt ==}  equal\<close>
126               | Neq     \<comment> \<open>{\tt !=}  not equal\<close>
127               | BitAnd  \<comment> \<open>{\tt \&}   bitwise AND\<close>
128               | And     \<comment> \<open>{\tt \&}   boolean AND\<close>
129               | BitXor  \<comment> \<open>{\texttt \^}   bitwise Xor\<close>
130               | Xor     \<comment> \<open>{\texttt \^}   boolean Xor\<close>
131               | BitOr   \<comment> \<open>{\tt |}   bitwise Or\<close>
132               | Or      \<comment> \<open>{\tt |}   boolean Or\<close>
133               | CondAnd \<comment> \<open>{\tt \&\&}  conditional And\<close>
134               | CondOr  \<comment> \<open>{\tt ||}  conditional Or\<close>
135text\<open>The boolean operators {\tt \&} and {\tt |} strictly evaluate both
136of their arguments. The conditional operators {\tt \&\&} and {\tt ||} only 
137evaluate the second argument if the value of the whole expression isn't 
138allready determined by the first argument.
139e.g.: {\tt false \&\& e} e is not evaluated;  
140      {\tt true || e} e is not evaluated; 
141\<close>
142
143datatype var
144        = LVar lname \<comment> \<open>local variable (incl. parameters)\<close>
145        | FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90)
146                     \<comment> \<open>class field\<close>
147                     \<comment> \<open>\<^term>\<open>{accC,statDeclC,stat}e..fn\<close>\<close>
148                     \<comment> \<open>\<open>accC\<close>: accessing class (static class were\<close>
149                     \<comment> \<open>the code is declared. Annotation only needed for\<close>
150                     \<comment> \<open>evaluation to check accessibility)\<close>
151                     \<comment> \<open>\<open>statDeclC\<close>: static declaration class of field\<close>
152                     \<comment> \<open>\<open>stat\<close>: static or instance field?\<close>
153                     \<comment> \<open>\<open>e\<close>: reference to object\<close>
154                     \<comment> \<open>\<open>fn\<close>: field name\<close>
155        | AVar expr expr ("_.[_]"[90,10   ]90)
156                     \<comment> \<open>array component\<close>
157                     \<comment> \<open>\<^term>\<open>e1.[e2]\<close>: e1 array reference; e2 index\<close>
158        | InsInitV stmt var 
159                     \<comment> \<open>insertion of initialization before evaluation\<close>
160                     \<comment> \<open>of var (technical term for smallstep semantics.)\<close>
161
162and expr
163        = NewC qtname         \<comment> \<open>class instance creation\<close>
164        | NewA ty expr ("New _[_]"[99,10   ]85) 
165                              \<comment> \<open>array creation\<close> 
166        | Cast ty expr        \<comment> \<open>type cast\<close>
167        | Inst expr ref_ty ("_ InstOf _"[85,99] 85)   
168                              \<comment> \<open>instanceof\<close>     
169        | Lit  val              \<comment> \<open>literal value, references not allowed\<close>
170        | UnOp unop expr        \<comment> \<open>unary operation\<close>
171        | BinOp binop expr expr \<comment> \<open>binary operation\<close>
172        
173        | Super               \<comment> \<open>special Super keyword\<close>
174        | Acc  var            \<comment> \<open>variable access\<close>
175        | Ass  var expr       ("_:=_"   [90,85   ]85)
176                              \<comment> \<open>variable assign\<close> 
177        | Cond expr expr expr ("_ ? _ : _" [85,85,80]80) \<comment> \<open>conditional\<close>  
178        | Call qtname ref_ty inv_mode expr mname "(ty list)" "(expr list)"  
179            ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) 
180                    \<comment> \<open>method call\<close> 
181                    \<comment> \<open>\<^term>\<open>{accC,statT,mode}e\<cdot>mn({pTs}args)\<close> "\<close>
182                    \<comment> \<open>\<open>accC\<close>: accessing class (static class were\<close>
183                    \<comment> \<open>the call code is declared. Annotation only needed for\<close>
184                    \<comment> \<open>evaluation to check accessibility)\<close>
185                    \<comment> \<open>\<open>statT\<close>: static declaration class/interface of\<close>
186                    \<comment> \<open>method\<close>
187                    \<comment> \<open>\<open>mode\<close>: invocation mode\<close>
188                    \<comment> \<open>\<open>e\<close>: reference to object\<close>
189                    \<comment> \<open>\<open>mn\<close>: field name\<close>   
190                    \<comment> \<open>\<open>pTs\<close>: types of parameters\<close>
191                    \<comment> \<open>\<open>args\<close>: the actual parameters/arguments\<close> 
192        | Methd qtname sig    \<comment> \<open>(folded) method (see below)\<close>
193        | Body qtname stmt    \<comment> \<open>(unfolded) method body\<close>
194        | InsInitE stmt expr  
195                 \<comment> \<open>insertion of initialization before\<close>
196                 \<comment> \<open>evaluation of expr (technical term for smallstep sem.)\<close>
197        | Callee locals expr  \<comment> \<open>save callers locals in callee-Frame\<close>
198                              \<comment> \<open>(technical term for smallstep semantics)\<close>
199and  stmt
200        = Skip                  \<comment> \<open>empty      statement\<close>
201        | Expr  expr            \<comment> \<open>expression statement\<close>
202        | Lab   jump stmt       ("_\<bullet> _" [      99,66]66)
203                                \<comment> \<open>labeled statement; handles break\<close>
204        | Comp  stmt stmt       ("_;; _"                  [      66,65]65)
205        | If'   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
206        | Loop  label expr stmt ("_\<bullet> While'(_') _"        [   99,80,79]70)
207        | Jmp jump              \<comment> \<open>break, continue, return\<close>
208        | Throw expr
209        | TryC  stmt qtname vname stmt ("Try _ Catch'(_ _') _"  [79,99,80,79]70)
210             \<comment> \<open>\<^term>\<open>Try c1 Catch(C vn) c2\<close>\<close> 
211             \<comment> \<open>\<open>c1\<close>: block were exception may be thrown\<close>
212             \<comment> \<open>\<open>C\<close>:  execption class to catch\<close>
213             \<comment> \<open>\<open>vn\<close>: local name for exception used in \<open>c2\<close>\<close>
214             \<comment> \<open>\<open>c2\<close>: block to execute when exception is cateched\<close>
215        | Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
216        | FinA abopt stmt       \<comment> \<open>Save abruption of first statement\<close> 
217                                \<comment> \<open>technical term  for smallstep sem.)\<close>
218        | Init  qtname          \<comment> \<open>class initialization\<close>
219
220datatype_compat var expr stmt
221
222
223text \<open>
224The expressions Methd and Body are artificial program constructs, in the
225sense that they are not used to define a concrete Bali program. In the 
226operational semantic's they are "generated on the fly" 
227to decompose the task to define the behaviour of the Call expression. 
228They are crucial for the axiomatic semantics to give a syntactic hook to insert 
229some assertions (cf. AxSem.thy, Eval.thy). 
230The Init statement (to initialize a class on its first use) is 
231inserted in various places by the semantics. 
232Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the
233smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the 
234local variables of the caller for method return. So ve avoid modelling a 
235frame stack.
236The InsInitV/E terms are only used by the smallstep semantics to model the
237intermediate steps of class-initialisation.
238\<close>
239 
240type_synonym "term" = "(expr+stmt,var,expr list) sum3"
241translations
242  (type) "sig"   <= (type) "mname \<times> ty list"
243  (type) "term"  <= (type) "(expr+stmt,var,expr list) sum3"
244
245abbreviation this :: expr
246  where "this == Acc (LVar This)"
247
248abbreviation LAcc :: "vname \<Rightarrow> expr" ("!!")
249  where "!!v == Acc (LVar (EName (VNam v)))"
250
251abbreviation
252  LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
253  where "v:==e == Expr (Ass (LVar (EName (VNam  v))) e)"
254
255abbreviation
256  Return :: "expr \<Rightarrow> stmt"
257  where "Return e == Expr (Ass (LVar (EName Res)) e);; Jmp Ret" \<comment> \<open>\tt Res := e;; Jmp Ret\<close>
258
259abbreviation
260  StatRef :: "ref_ty \<Rightarrow> expr"
261  where "StatRef rt == Cast (RefT rt) (Lit Null)"
262  
263definition
264  is_stmt :: "term \<Rightarrow> bool"
265  where "is_stmt t = (\<exists>c. t=In1r c)"
266
267ML \<open>ML_Thms.bind_thms ("is_stmt_rews", sum3_instantiate \<^context> @{thm is_stmt_def})\<close>
268
269declare is_stmt_rews [simp]
270
271text \<open>
272  Here is some syntactic stuff to handle the injections of statements,
273  expressions, variables and expression lists into general terms.
274\<close>
275
276abbreviation (input)
277  expr_inj_term :: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
278  where "\<langle>e\<rangle>\<^sub>e == In1l e"
279
280abbreviation (input)
281  stmt_inj_term :: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
282  where "\<langle>c\<rangle>\<^sub>s == In1r c"
283
284abbreviation (input)
285  var_inj_term :: "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 1000)
286  where "\<langle>v\<rangle>\<^sub>v == In2 v"
287
288abbreviation (input)
289  lst_inj_term :: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
290  where "\<langle>es\<rangle>\<^sub>l == In3 es"
291
292text \<open>It seems to be more elegant to have an overloaded injection like the
293following.
294\<close>
295
296class inj_term =
297  fixes inj_term:: "'a \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
298
299text \<open>How this overloaded injections work can be seen in the theory 
300\<open>DefiniteAssignment\<close>. Other big inductive relations on
301terms defined in theories \<open>WellType\<close>, \<open>Eval\<close>, \<open>Evaln\<close> and
302\<open>AxSem\<close> don't follow this convention right now, but introduce subtle 
303syntactic sugar in the relations themselves to make a distinction on 
304expressions, statements and so on. So unfortunately you will encounter a 
305mixture of dealing with these injections. The abbreviations above are used
306as bridge between the different conventions.  
307\<close>
308
309instantiation stmt :: inj_term
310begin
311
312definition
313  stmt_inj_term_def: "\<langle>c::stmt\<rangle> = In1r c"
314
315instance ..
316
317end
318
319lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
320by (simp add: stmt_inj_term_def)
321
322lemma  stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
323  by (simp add: stmt_inj_term_simp)
324
325instantiation expr :: inj_term
326begin
327
328definition
329  expr_inj_term_def: "\<langle>e::expr\<rangle> = In1l e"
330
331instance ..
332
333end
334
335lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
336by (simp add: expr_inj_term_def)
337
338lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
339  by (simp add: expr_inj_term_simp)
340
341instantiation var :: inj_term
342begin
343
344definition
345  var_inj_term_def: "\<langle>v::var\<rangle> = In2 v"
346
347instance ..
348
349end
350
351lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
352by (simp add: var_inj_term_def)
353
354lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
355  by (simp add: var_inj_term_simp)
356
357class expr_of =
358  fixes expr_of :: "'a \<Rightarrow> expr"
359
360instantiation expr :: expr_of
361begin
362
363definition
364  "expr_of = (\<lambda>(e::expr). e)"
365
366instance ..
367
368end 
369
370instantiation list :: (expr_of) inj_term
371begin
372
373definition
374  "\<langle>es::'a list\<rangle> = In3 (map expr_of es)"
375
376instance ..
377
378end
379
380lemma expr_list_inj_term_def:
381  "\<langle>es::expr list\<rangle> \<equiv> In3 es"
382  by (simp add: inj_term_list_def expr_of_expr_def)
383
384lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
385by (simp add: expr_list_inj_term_def)
386
387lemma expr_list_inj_term [iff]: "\<langle>x::expr list\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
388  by (simp add: expr_list_inj_term_simp)
389
390lemmas inj_term_simps = stmt_inj_term_simp expr_inj_term_simp var_inj_term_simp
391                        expr_list_inj_term_simp
392lemmas inj_term_sym_simps = stmt_inj_term_simp [THEN sym] 
393                            expr_inj_term_simp [THEN sym]
394                            var_inj_term_simp [THEN sym]
395                            expr_list_inj_term_simp [THEN sym]
396
397lemma stmt_expr_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr\<rangle>"
398  by (simp add: inj_term_simps)
399lemma expr_stmt_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
400  by (simp add: inj_term_simps)
401lemma stmt_var_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::var\<rangle>"
402  by (simp add: inj_term_simps)
403lemma var_stmt_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
404  by (simp add: inj_term_simps)
405lemma stmt_elist_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
406  by (simp add: inj_term_simps)
407lemma elist_stmt_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
408  by (simp add: inj_term_simps)
409lemma expr_var_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::var\<rangle>"
410  by (simp add: inj_term_simps)
411lemma var_expr_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr\<rangle>"
412  by (simp add: inj_term_simps)
413lemma expr_elist_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
414  by (simp add: inj_term_simps)
415lemma elist_expr_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::expr\<rangle>"
416  by (simp add: inj_term_simps)
417lemma var_elist_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
418  by (simp add: inj_term_simps)
419lemma elist_var_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::var\<rangle>"
420  by (simp add: inj_term_simps)
421
422lemma term_cases: "
423  \<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>
424  \<Longrightarrow> P t"
425  apply (cases t)
426  apply (rename_tac a, case_tac a)
427  apply auto
428  done
429
430subsubsection \<open>Evaluation of unary operations\<close>
431primrec eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
432where
433  "eval_unop UPlus v = Intg (the_Intg v)"
434| "eval_unop UMinus v = Intg (- (the_Intg v))"
435| "eval_unop UBitNot v = Intg 42"                \<comment> \<open>FIXME: Not yet implemented\<close>
436| "eval_unop UNot v = Bool (\<not> the_Bool v)"
437
438subsubsection \<open>Evaluation of binary operations\<close>
439primrec eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
440where
441  "eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
442| "eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
443| "eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
444| "eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
445| "eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
446
447\<comment> \<open>Be aware of the explicit coercion of the shift distance to nat\<close>
448| "eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
449| "eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
450| "eval_binop RShiftU v1 v2 = Intg 42" \<comment> \<open>FIXME: Not yet implemented\<close>
451
452| "eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
453| "eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
454| "eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
455| "eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
456
457| "eval_binop Eq      v1 v2 = Bool (v1=v2)"
458| "eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
459| "eval_binop BitAnd  v1 v2 = Intg 42" \<comment> \<open>FIXME: Not yet implemented\<close>
460| "eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
461| "eval_binop BitXor  v1 v2 = Intg 42" \<comment> \<open>FIXME: Not yet implemented\<close>
462| "eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
463| "eval_binop BitOr   v1 v2 = Intg 42" \<comment> \<open>FIXME: Not yet implemented\<close>
464| "eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
465| "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
466| "eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
467
468definition
469  need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
470  "need_second_arg binop v1 = (\<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
471                                 (binop=CondOr  \<and> the_Bool v1)))"
472text \<open>\<^term>\<open>CondAnd\<close> and \<^term>\<open>CondOr\<close> only evalulate the second argument
473 if the value isn't already determined by the first argument\<close>
474
475lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b" 
476by (simp add: need_second_arg_def)
477
478lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\<not> b)" 
479by (simp add: need_second_arg_def)
480
481lemma need_second_arg_strict[simp]: 
482 "\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
483by (cases binop) 
484   (simp_all add: need_second_arg_def)
485end
486