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