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