src/HOL/Bali/Term.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (22 months ago)
changeset 66983 df83b66f1d94
parent 62390 842917225d56
child 67443 3abf6a722518
permissions -rw-r--r--
proper merge (amending fb46c031c841);
     1 (*  Title:      HOL/Bali/Term.thy
     2     Author:     David von Oheimb
     3 *)
     4 
     5 subsection \<open>Java expressions and statements\<close>
     6 
     7 theory Term imports Value Table begin
     8 
     9 text \<open>
    10 design 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 
    28 simplifications:
    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 
    60 type_synonym locals = "(lname, val) table"  \<comment>\<open>local variables\<close>
    61 
    62 
    63 datatype jump
    64         = Break label \<comment>\<open>break\<close>
    65         | Cont label  \<comment>\<open>continue\<close>
    66         | Ret         \<comment>\<open>return from method\<close>
    67 
    68 datatype 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 
    72 datatype 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 
    76 datatype 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>
    81 type_synonym
    82   abopt  = "abrupt option"
    83 
    84 text \<open>Local variable store and exception. 
    85 Anticipation of State.thy used by smallstep semantics. For a method call, 
    86 we save the local variables of the caller in the term Callee to restore them 
    87 after method return. Also an exception must be restored after the finally
    88 statement\<close>
    89 
    90 translations
    91  (type) "locals" <= (type) "(lname, val) table"
    92 
    93 datatype 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 
    98 record  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 
   102 translations
   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>
   107 datatype 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>
   113 datatype 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>
   135 text\<open>The boolean operators {\tt \&} and {\tt |} strictly evaluate both
   136 of their arguments. The conditional operators {\tt \&\&} and {\tt ||} only 
   137 evaluate the second argument if the value of the whole expression isn't 
   138 allready determined by the first argument.
   139 e.g.: {\tt false \&\& e} e is not evaluated;  
   140       {\tt true || e} e is not evaluated; 
   141 \<close>
   142 
   143 datatype 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 "{accC,statDeclC,stat}e..fn"}\<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 "e1.[e2]"}: 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 
   162 and 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 "{accC,statT,mode}e\<cdot>mn({pTs}args)"} "\<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>
   199 and  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 "Try c1 Catch(C vn) c2"}\<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 
   220 datatype_compat var expr stmt
   221 
   222 
   223 text \<open>
   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 \<close>
   239  
   240 type_synonym "term" = "(expr+stmt,var,expr list) sum3"
   241 translations
   242   (type) "sig"   <= (type) "mname \<times> ty list"
   243   (type) "term"  <= (type) "(expr+stmt,var,expr list) sum3"
   244 
   245 abbreviation this :: expr
   246   where "this == Acc (LVar This)"
   247 
   248 abbreviation LAcc :: "vname \<Rightarrow> expr" ("!!")
   249   where "!!v == Acc (LVar (EName (VNam v)))"
   250 
   251 abbreviation
   252   LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
   253   where "v:==e == Expr (Ass (LVar (EName (VNam  v))) e)"
   254 
   255 abbreviation
   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 
   259 abbreviation
   260   StatRef :: "ref_ty \<Rightarrow> expr"
   261   where "StatRef rt == Cast (RefT rt) (Lit Null)"
   262   
   263 definition
   264   is_stmt :: "term \<Rightarrow> bool"
   265   where "is_stmt t = (\<exists>c. t=In1r c)"
   266 
   267 ML \<open>ML_Thms.bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def})\<close>
   268 
   269 declare is_stmt_rews [simp]
   270 
   271 text \<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 
   276 abbreviation (input)
   277   expr_inj_term :: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
   278   where "\<langle>e\<rangle>\<^sub>e == In1l e"
   279 
   280 abbreviation (input)
   281   stmt_inj_term :: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
   282   where "\<langle>c\<rangle>\<^sub>s == In1r c"
   283 
   284 abbreviation (input)
   285   var_inj_term :: "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 1000)
   286   where "\<langle>v\<rangle>\<^sub>v == In2 v"
   287 
   288 abbreviation (input)
   289   lst_inj_term :: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
   290   where "\<langle>es\<rangle>\<^sub>l == In3 es"
   291 
   292 text \<open>It seems to be more elegant to have an overloaded injection like the
   293 following.
   294 \<close>
   295 
   296 class inj_term =
   297   fixes inj_term:: "'a \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
   298 
   299 text \<open>How this overloaded injections work can be seen in the theory 
   300 \<open>DefiniteAssignment\<close>. Other big inductive relations on
   301 terms 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 
   303 syntactic sugar in the relations themselves to make a distinction on 
   304 expressions, statements and so on. So unfortunately you will encounter a 
   305 mixture of dealing with these injections. The abbreviations above are used
   306 as bridge between the different conventions.  
   307 \<close>
   308 
   309 instantiation stmt :: inj_term
   310 begin
   311 
   312 definition
   313   stmt_inj_term_def: "\<langle>c::stmt\<rangle> = In1r c"
   314 
   315 instance ..
   316 
   317 end
   318 
   319 lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
   320 by (simp add: stmt_inj_term_def)
   321 
   322 lemma  stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   323   by (simp add: stmt_inj_term_simp)
   324 
   325 instantiation expr :: inj_term
   326 begin
   327 
   328 definition
   329   expr_inj_term_def: "\<langle>e::expr\<rangle> = In1l e"
   330 
   331 instance ..
   332 
   333 end
   334 
   335 lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
   336 by (simp add: expr_inj_term_def)
   337 
   338 lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   339   by (simp add: expr_inj_term_simp)
   340 
   341 instantiation var :: inj_term
   342 begin
   343 
   344 definition
   345   var_inj_term_def: "\<langle>v::var\<rangle> = In2 v"
   346 
   347 instance ..
   348 
   349 end
   350 
   351 lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
   352 by (simp add: var_inj_term_def)
   353 
   354 lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   355   by (simp add: var_inj_term_simp)
   356 
   357 class expr_of =
   358   fixes expr_of :: "'a \<Rightarrow> expr"
   359 
   360 instantiation expr :: expr_of
   361 begin
   362 
   363 definition
   364   "expr_of = (\<lambda>(e::expr). e)"
   365 
   366 instance ..
   367 
   368 end 
   369 
   370 instantiation list :: (expr_of) inj_term
   371 begin
   372 
   373 definition
   374   "\<langle>es::'a list\<rangle> = In3 (map expr_of es)"
   375 
   376 instance ..
   377 
   378 end
   379 
   380 lemma 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 
   384 lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
   385 by (simp add: expr_list_inj_term_def)
   386 
   387 lemma 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 
   390 lemmas inj_term_simps = stmt_inj_term_simp expr_inj_term_simp var_inj_term_simp
   391                         expr_list_inj_term_simp
   392 lemmas 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 
   397 lemma stmt_expr_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr\<rangle>"
   398   by (simp add: inj_term_simps)
   399 lemma expr_stmt_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
   400   by (simp add: inj_term_simps)
   401 lemma stmt_var_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::var\<rangle>"
   402   by (simp add: inj_term_simps)
   403 lemma var_stmt_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
   404   by (simp add: inj_term_simps)
   405 lemma stmt_elist_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
   406   by (simp add: inj_term_simps)
   407 lemma elist_stmt_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
   408   by (simp add: inj_term_simps)
   409 lemma expr_var_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::var\<rangle>"
   410   by (simp add: inj_term_simps)
   411 lemma var_expr_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr\<rangle>"
   412   by (simp add: inj_term_simps)
   413 lemma expr_elist_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
   414   by (simp add: inj_term_simps)
   415 lemma elist_expr_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::expr\<rangle>"
   416   by (simp add: inj_term_simps)
   417 lemma var_elist_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
   418   by (simp add: inj_term_simps)
   419 lemma elist_var_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::var\<rangle>"
   420   by (simp add: inj_term_simps)
   421 
   422 lemma 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 
   430 subsubsection \<open>Evaluation of unary operations\<close>
   431 primrec eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
   432 where
   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> "FIXME: Not yet implemented"
   436 | "eval_unop UNot v = Bool (\<not> the_Bool v)"
   437 
   438 subsubsection \<open>Evaluation of binary operations\<close>
   439 primrec eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
   440 where
   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> "Be aware of the explicit coercion of the shift distance to nat"
   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>"FIXME: Not yet implemented"
   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> "FIXME: Not yet implemented"
   460 | "eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
   461 | "eval_binop BitXor  v1 v2 = Intg 42" \<comment> "FIXME: Not yet implemented"
   462 | "eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
   463 | "eval_binop BitOr   v1 v2 = Intg 42" \<comment> "FIXME: Not yet implemented"
   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 
   468 definition
   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)))"
   472 text \<open>@{term CondAnd} and @{term CondOr} only evalulate the second argument
   473  if the value isn't already determined by the first argument\<close>
   474 
   475 lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b" 
   476 by (simp add: need_second_arg_def)
   477 
   478 lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\<not> b)" 
   479 by (simp add: need_second_arg_def)
   480 
   481 lemma need_second_arg_strict[simp]: 
   482  "\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
   483 by (cases binop) 
   484    (simp_all add: need_second_arg_def)
   485 end