src/HOL/Bali/Term.thy
author schirmer
Fri Nov 01 13:16:28 2002 +0100 (2002-11-01)
changeset 13690 ac335b2f4a39
parent 13688 a0b16d42d489
child 14981 e73f8140af78
permissions -rw-r--r--
Inserted some extra paragraphs in large proofs to make tex run...
     1 (*  Title:      HOL/Bali/Term.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 header {* Java expressions and statements *}
     8 
     9 theory Term = Value + Table:
    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 This  is modeled as a special non-assignable local variable
    34 \item Super is modeled as a general expression with the same value as This
    35 \item access to field x in current class via This.x
    36 \item NewA creates only one-dimensional arrays;
    37   initialization of further subarrays may be simulated with nested NewAs
    38 \item The 'Lit' constructor is allowed to contain a reference value.
    39   But this is assumed to be prohibited in the input language, which is enforced
    40   by the type-checking rules.
    41 \item a call of a static method via a type name may be simulated by a dummy 
    42       variable
    43 \item no nested blocks with inner local variables
    44 \item no synchronized statements
    45 \item no secondary forms of if, while (e.g. no for) (may be easily simulated)
    46 \item no switch (may be simulated with if)
    47 \item the @{text try_catch_finally} statement is divided into the 
    48       @{text try_catch} statement 
    49       and a finally statement, which may be considered as try..finally with 
    50       empty catch
    51 \item the @{text try_catch} statement has exactly one catch clause; 
    52       multiple ones can be
    53   simulated with instanceof
    54 \item the compiler is supposed to add the annotations {@{text _}} during 
    55       type-checking. This
    56   transformation is left out as its result is checked by the type rules anyway
    57 \end{itemize}
    58 *}
    59 
    60 
    61 
    62 types locals = "(lname, val) table"  --{* local variables *}
    63 
    64 
    65 datatype jump
    66         = Break label --{* break *}
    67         | Cont label  --{* continue *}
    68         | Ret         --{* return from method *}
    69 
    70 datatype xcpt        --{* exception *}
    71 	= Loc loc    --{* location of allocated execption object *}
    72 	| Std xname  --{* intermediate standard exception, see Eval.thy *}
    73 
    74 datatype error
    75        =  AccessViolation  --{* Access to a member that isn't permitted *}
    76         | CrossMethodJump  --{* Method exits with a break or continue *}
    77 
    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 *}
    83 types
    84   abopt  = "abrupt option"
    85 
    86 text {* Local variable store and exception. 
    87 Anticipation of State.thy used by smallstep semantics. For a method call, 
    88 we save the local variables of the caller in the term Callee to restore them 
    89 after method return. Also an exception must be restored after the finally
    90 statement *}
    91 
    92 translations
    93  "locals" <= (type) "(lname, val) table"
    94 
    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 
   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*}
   113 
   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 *}
   144 
   145 datatype var
   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.)*}
   163 
   164 and expr
   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 *}
   174         
   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) *}
   201 and  stmt
   202 	= Skip                  --{* empty      statement *}
   203 	| Expr  expr            --{* expression statement *}
   204         | Lab   jump stmt       ("_\<bullet> _" [      99,66]66)
   205                                 --{* labeled statement; handles break *}
   206 	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
   207 	| If_   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
   208 	| Loop  label expr stmt ("_\<bullet> While'(_') _"        [   99,80,79]70)
   209         | Jmp jump              --{* break, continue, return *}
   210 	| Throw expr
   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*}
   217 	| Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
   218         | FinA abopt stmt       --{* Save abruption of first statement *} 
   219                                 --{* technical term  for smallstep sem.) *}
   220 	| Init  qtname          --{* class initialization *}
   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 
   226 operational semantic's they are "generated on the fly" 
   227 to decompose the task to define the behaviour of the Call expression. 
   228 They are crucial for the axiomatic semantics to give a syntactic hook to insert 
   229 some assertions (cf. AxSem.thy, Eval.thy). 
   230 The Init statement (to initialize a class on its first use) is 
   231 inserted in various places by the semantics. 
   232 Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the
   233 smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the 
   234 local variables of the caller for method return. So ve avoid modelling a 
   235 frame stack.
   236 The InsInitV/E terms are only used by the smallstep semantics to model the
   237 intermediate steps of class-initialisation.
   238 *}
   239  
   240 types "term" = "(expr+stmt,var,expr list) sum3"
   241 translations
   242   "sig"   <= (type) "mname \<times> ty list"
   243   "var"   <= (type) "Term.var"
   244   "expr"  <= (type) "Term.expr"
   245   "stmt"  <= (type) "Term.stmt"
   246   "term"  <= (type) "(expr+stmt,var,expr list) sum3"
   247 
   248 syntax
   249   
   250   this    :: expr
   251   LAcc    :: "vname \<Rightarrow> expr" ("!!")
   252   LAss    :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
   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);; Jmp Ret" 
   262                   --{* \tt Res := e;; Jmp Ret *}
   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]
   275 
   276 text {*
   277   Here is some syntactic stuff to handle the injections of statements,
   278   expressions, variables and expression lists into general terms.
   279 *}
   280 
   281 syntax 
   282   expr_inj_term:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
   283   stmt_inj_term:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
   284   var_inj_term::  "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 1000)
   285   lst_inj_term:: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
   286 
   287 translations 
   288   "\<langle>e\<rangle>\<^sub>e" \<rightharpoonup> "In1l e"
   289   "\<langle>c\<rangle>\<^sub>s" \<rightharpoonup> "In1r c"
   290   "\<langle>v\<rangle>\<^sub>v" \<rightharpoonup> "In2 v"
   291   "\<langle>es\<rangle>\<^sub>l" \<rightharpoonup> "In3 es"
   292 
   293 text {* It seems to be more elegant to have an overloaded injection like the
   294 following.
   295 *}
   296 
   297 axclass inj_term < "type"
   298 consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
   299 
   300 text {* How this overloaded injections work can be seen in the theory 
   301 @{text DefiniteAssignment}. Other big inductive relations on
   302 terms defined in theories @{text WellType}, @{text Eval}, @{text Evaln} and
   303 @{text AxSem} don't follow this convention right now, but introduce subtle 
   304 syntactic sugar in the relations themselves to make a distinction on 
   305 expressions, statements and so on. So unfortunately you will encounter a 
   306 mixture of dealing with these injections. The translations above are used
   307 as bridge between the different conventions.  
   308 *}
   309 
   310 instance stmt::inj_term ..
   311 
   312 defs (overloaded)
   313 stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
   314 
   315 lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
   316 by (simp add: stmt_inj_term_def)
   317 
   318 lemma  stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   319   by (simp add: stmt_inj_term_simp)
   320 
   321 instance expr::inj_term ..
   322 
   323 defs (overloaded)
   324 expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
   325 
   326 lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
   327 by (simp add: expr_inj_term_def)
   328 
   329 lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   330   by (simp add: expr_inj_term_simp)
   331 
   332 instance var::inj_term ..
   333 
   334 defs (overloaded)
   335 var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
   336 
   337 lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
   338 by (simp add: var_inj_term_def)
   339 
   340 lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   341   by (simp add: var_inj_term_simp)
   342 
   343 instance "list":: (type) inj_term ..
   344 
   345 defs (overloaded)
   346 expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
   347 
   348 lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
   349 by (simp add: expr_list_inj_term_def)
   350 
   351 lemma expr_list_inj_term [iff]: "\<langle>x::expr list\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   352   by (simp add: expr_list_inj_term_simp)
   353 
   354 lemmas inj_term_simps = stmt_inj_term_simp expr_inj_term_simp var_inj_term_simp
   355                         expr_list_inj_term_simp
   356 lemmas inj_term_sym_simps = stmt_inj_term_simp [THEN sym] 
   357                             expr_inj_term_simp [THEN sym]
   358                             var_inj_term_simp [THEN sym]
   359                             expr_list_inj_term_simp [THEN sym]
   360 
   361 lemma stmt_expr_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr\<rangle>"
   362   by (simp add: inj_term_simps)
   363 lemma expr_stmt_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
   364   by (simp add: inj_term_simps)
   365 lemma stmt_var_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::var\<rangle>"
   366   by (simp add: inj_term_simps)
   367 lemma var_stmt_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
   368   by (simp add: inj_term_simps)
   369 lemma stmt_elist_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
   370   by (simp add: inj_term_simps)
   371 lemma elist_stmt_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
   372   by (simp add: inj_term_simps)
   373 lemma expr_var_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::var\<rangle>"
   374   by (simp add: inj_term_simps)
   375 lemma var_expr_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr\<rangle>"
   376   by (simp add: inj_term_simps)
   377 lemma expr_elist_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
   378   by (simp add: inj_term_simps)
   379 lemma elist_expr_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::expr\<rangle>"
   380   by (simp add: inj_term_simps)
   381 lemma var_elist_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
   382   by (simp add: inj_term_simps)
   383 lemma elist_var_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::var\<rangle>"
   384   by (simp add: inj_term_simps)
   385 
   386 lemma term_cases: "
   387   \<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>
   388   \<Longrightarrow> P t"
   389   apply (cases t)
   390   apply (case_tac a)
   391   apply auto
   392   done
   393 
   394 section {* Evaluation of unary operations *}
   395 consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
   396 primrec
   397 "eval_unop UPlus   v = Intg (the_Intg v)"
   398 "eval_unop UMinus  v = Intg (- (the_Intg v))"
   399 "eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
   400 "eval_unop UNot    v = Bool (\<not> the_Bool v)"
   401 
   402 section {* Evaluation of binary operations *}
   403 consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
   404 primrec
   405 "eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
   406 "eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
   407 "eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
   408 "eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
   409 "eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
   410 
   411 -- "Be aware of the explicit coercion of the shift distance to nat"
   412 "eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
   413 "eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
   414 "eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
   415 
   416 "eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
   417 "eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
   418 "eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
   419 "eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
   420 
   421 "eval_binop Eq      v1 v2 = Bool (v1=v2)"
   422 "eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
   423 "eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   424 "eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
   425 "eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   426 "eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
   427 "eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   428 "eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
   429 "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
   430 "eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
   431 
   432 constdefs need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool"
   433 "need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
   434                                (binop=CondOr  \<and> the_Bool v1))"
   435 text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
   436  if the value isn't already determined by the first argument*}
   437 
   438 lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b" 
   439 by (simp add: need_second_arg_def)
   440 
   441 lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\<not> b)" 
   442 by (simp add: need_second_arg_def)
   443 
   444 lemma need_second_arg_strict[simp]: 
   445  "\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
   446 by (cases binop) 
   447    (simp_all add: need_second_arg_def)
   448 end