wenzelm@12857: (* Title: HOL/Bali/Term.thy schirmer@12854: Author: David von Oheimb schirmer@12854: *) schirmer@12854: schirmer@12854: header {* Java expressions and statements *} schirmer@12854: haftmann@16417: theory Term imports Value Table begin schirmer@12854: schirmer@12854: text {* schirmer@12854: design issues: schirmer@12854: \begin{itemize} schirmer@12854: \item invocation frames for local variables could be reduced to special static schirmer@12854: objects (one per method). This would reduce redundancy, but yield a rather schirmer@12854: non-standard execution model more difficult to understand. schirmer@12854: \item method bodies separated from calls to handle assumptions in axiomat. schirmer@12854: semantics schirmer@12854: NB: Body is intended to be in the environment of the called method. schirmer@12854: \item class initialization is regarded as (auxiliary) statement schirmer@12854: (required for AxSem) schirmer@12854: \item result expression of method return is handled by a special result variable schirmer@12854: result variable is treated uniformly with local variables schirmer@12854: \begin{itemize} schirmer@12854: \item[+] welltypedness and existence of the result/return expression is schirmer@12854: ensured without extra efford schirmer@12854: \end{itemize} schirmer@12854: \end{itemize} schirmer@12854: schirmer@12854: simplifications: schirmer@12854: \begin{itemize} schirmer@12854: \item expression statement allowed for any expression schirmer@12854: \item This is modeled as a special non-assignable local variable schirmer@12854: \item Super is modeled as a general expression with the same value as This schirmer@12854: \item access to field x in current class via This.x schirmer@12854: \item NewA creates only one-dimensional arrays; schirmer@12854: initialization of further subarrays may be simulated with nested NewAs schirmer@12854: \item The 'Lit' constructor is allowed to contain a reference value. schirmer@12854: But this is assumed to be prohibited in the input language, which is enforced schirmer@12854: by the type-checking rules. schirmer@12854: \item a call of a static method via a type name may be simulated by a dummy schirmer@12854: variable schirmer@12854: \item no nested blocks with inner local variables schirmer@12854: \item no synchronized statements schirmer@12854: \item no secondary forms of if, while (e.g. no for) (may be easily simulated) schirmer@12854: \item no switch (may be simulated with if) schirmer@12854: \item the @{text try_catch_finally} statement is divided into the schirmer@12854: @{text try_catch} statement schirmer@12854: and a finally statement, which may be considered as try..finally with schirmer@12854: empty catch schirmer@12854: \item the @{text try_catch} statement has exactly one catch clause; schirmer@12854: multiple ones can be schirmer@12854: simulated with instanceof schirmer@12854: \item the compiler is supposed to add the annotations {@{text _}} during schirmer@12854: type-checking. This schirmer@12854: transformation is left out as its result is checked by the type rules anyway schirmer@12854: \end{itemize} schirmer@12854: *} schirmer@12854: schirmer@13337: schirmer@13337: schirmer@13384: types locals = "(lname, val) table" --{* local variables *} schirmer@13337: schirmer@13337: schirmer@13337: datatype jump schirmer@13384: = Break label --{* break *} schirmer@13384: | Cont label --{* continue *} schirmer@13384: | Ret --{* return from method *} schirmer@13337: schirmer@13384: datatype xcpt --{* exception *} wenzelm@32960: = Loc loc --{* location of allocated execption object *} wenzelm@32960: | Std xname --{* intermediate standard exception, see Eval.thy *} schirmer@13337: schirmer@13337: datatype error schirmer@13688: = AccessViolation --{* Access to a member that isn't permitted *} schirmer@13688: | CrossMethodJump --{* Method exits with a break or continue *} schirmer@13337: schirmer@13384: datatype abrupt --{* abrupt completion *} schirmer@13384: = Xcpt xcpt --{* exception *} schirmer@13384: | Jump jump --{* break, continue, return *} schirmer@13384: | Error error -- {* runtime errors, we wan't to detect and proof absent schirmer@13384: in welltyped programms *} schirmer@13337: types schirmer@13337: abopt = "abrupt option" schirmer@13337: schirmer@13337: text {* Local variable store and exception. schirmer@13337: Anticipation of State.thy used by smallstep semantics. For a method call, schirmer@13337: we save the local variables of the caller in the term Callee to restore them schirmer@13337: after method return. Also an exception must be restored after the finally schirmer@13337: statement *} schirmer@13337: schirmer@13337: translations wenzelm@35431: (type) "locals" <= (type) "(lname, val) table" schirmer@13337: schirmer@13384: datatype inv_mode --{* invocation mode for method calls *} wenzelm@32960: = Static --{* static *} wenzelm@32960: | SuperM --{* super *} wenzelm@32960: | IntVir --{* interface or virtual *} schirmer@12854: schirmer@13384: record sig = --{* signature of a method, cf. 8.4.2 *} wenzelm@32960: name ::"mname" --{* acutally belongs to Decl.thy *} schirmer@12854: parTs::"ty list" schirmer@12854: schirmer@12854: translations wenzelm@35431: (type) "sig" <= (type) "\name::mname,parTs::ty list\" wenzelm@35431: (type) "sig" <= (type) "\name::mname,parTs::ty list,\::'a\" schirmer@12854: schirmer@13384: --{* function codes for unary operations *} schirmer@13384: datatype unop = UPlus -- {*{\tt +} unary plus*} schirmer@13384: | UMinus -- {*{\tt -} unary minus*} schirmer@13384: | UBitNot -- {*{\tt ~} bitwise NOT*} schirmer@13384: | UNot -- {*{\tt !} logical complement*} schirmer@13337: schirmer@13384: --{* function codes for binary operations *} schirmer@13384: datatype binop = Mul -- {*{\tt * } multiplication*} schirmer@13384: | Div -- {*{\tt /} division*} schirmer@13384: | Mod -- {*{\tt \%} remainder*} schirmer@13384: | Plus -- {*{\tt +} addition*} schirmer@13384: | Minus -- {*{\tt -} subtraction*} schirmer@13384: | LShift -- {*{\tt <<} left shift*} schirmer@13384: | RShift -- {*{\tt >>} signed right shift*} schirmer@13384: | RShiftU -- {*{\tt >>>} unsigned right shift*} schirmer@13384: | Less -- {*{\tt <} less than*} schirmer@13384: | Le -- {*{\tt <=} less than or equal*} schirmer@13384: | Greater -- {*{\tt >} greater than*} schirmer@13384: | Ge -- {*{\tt >=} greater than or equal*} schirmer@13384: | Eq -- {*{\tt ==} equal*} schirmer@13384: | Neq -- {*{\tt !=} not equal*} schirmer@13384: | BitAnd -- {*{\tt \&} bitwise AND*} schirmer@13384: | And -- {*{\tt \&} boolean AND*} schirmer@13384: | BitXor -- {*{\texttt \^} bitwise Xor*} schirmer@13384: | Xor -- {*{\texttt \^} boolean Xor*} schirmer@13384: | BitOr -- {*{\tt |} bitwise Or*} schirmer@13384: | Or -- {*{\tt |} boolean Or*} schirmer@13384: | CondAnd -- {*{\tt \&\&} conditional And*} schirmer@13384: | CondOr -- {*{\tt ||} conditional Or *} schirmer@13384: text{* The boolean operators {\tt \&} and {\tt |} strictly evaluate both schirmer@13384: of their arguments. The conditional operators {\tt \&\&} and {\tt ||} only schirmer@13384: evaluate the second argument if the value of the whole expression isn't schirmer@13384: allready determined by the first argument. schirmer@13384: e.g.: {\tt false \&\& e} e is not evaluated; schirmer@13384: {\tt true || e} e is not evaluated; schirmer@13384: *} schirmer@13358: schirmer@12854: datatype var wenzelm@32960: = LVar lname --{* local variable (incl. parameters) *} schirmer@13384: | FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90) schirmer@13384: --{* class field *} schirmer@13384: --{* @{term "{accC,statDeclC,stat}e..fn"} *} schirmer@13384: --{* @{text accC}: accessing class (static class were *} schirmer@13384: --{* the code is declared. Annotation only needed for *} schirmer@13384: --{* evaluation to check accessibility) *} schirmer@13384: --{* @{text statDeclC}: static declaration class of field*} schirmer@13384: --{* @{text stat}: static or instance field?*} schirmer@13384: --{* @{text e}: reference to object*} schirmer@13384: --{* @{text fn}: field name*} wenzelm@32960: | AVar expr expr ("_.[_]"[90,10 ]90) schirmer@13384: --{* array component *} schirmer@13384: --{* @{term "e1.[e2]"}: e1 array reference; e2 index *} schirmer@13384: | InsInitV stmt var schirmer@13384: --{* insertion of initialization before evaluation *} schirmer@13384: --{* of var (technical term for smallstep semantics.)*} schirmer@12854: schirmer@12854: and expr wenzelm@32960: = NewC qtname --{* class instance creation *} wenzelm@32960: | NewA ty expr ("New _[_]"[99,10 ]85) schirmer@13384: --{* array creation *} wenzelm@32960: | Cast ty expr --{* type cast *} wenzelm@32960: | Inst expr ref_ty ("_ InstOf _"[85,99] 85) schirmer@13384: --{* instanceof *} wenzelm@32960: | Lit val --{* literal value, references not allowed *} schirmer@13384: | UnOp unop expr --{* unary operation *} schirmer@13384: | BinOp binop expr expr --{* binary operation *} schirmer@13337: wenzelm@32960: | Super --{* special Super keyword *} wenzelm@32960: | Acc var --{* variable access *} wenzelm@32960: | Ass var expr ("_:=_" [90,85 ]85) schirmer@13384: --{* variable assign *} wenzelm@32960: | Cond expr expr expr ("_ ? _ : _" [85,85,80]80) --{* conditional *} schirmer@13384: | Call qtname ref_ty inv_mode expr mname "(ty list)" "(expr list)" schirmer@13384: ("{_,_,_}_\_'( {_}_')"[10,10,10,85,99,10,10]85) schirmer@13384: --{* method call *} schirmer@13384: --{* @{term "{accC,statT,mode}e\mn({pTs}args)"} " *} schirmer@13384: --{* @{text accC}: accessing class (static class were *} schirmer@13384: --{* the call code is declared. Annotation only needed for*} schirmer@13384: --{* evaluation to check accessibility) *} schirmer@13384: --{* @{text statT}: static declaration class/interface of *} schirmer@13384: --{* method *} schirmer@13384: --{* @{text mode}: invocation mode *} schirmer@13384: --{* @{text e}: reference to object*} schirmer@13384: --{* @{text mn}: field name*} schirmer@13384: --{* @{text pTs}: types of parameters *} schirmer@13384: --{* @{text args}: the actual parameters/arguments *} schirmer@13384: | Methd qtname sig --{* (folded) method (see below) *} schirmer@13384: | Body qtname stmt --{* (unfolded) method body *} schirmer@13384: | InsInitE stmt expr schirmer@13384: --{* insertion of initialization before *} schirmer@13384: --{* evaluation of expr (technical term for smallstep sem.) *} schirmer@13384: | Callee locals expr --{* save callers locals in callee-Frame *} schirmer@13384: --{* (technical term for smallstep semantics) *} schirmer@12854: and stmt wenzelm@32960: = Skip --{* empty statement *} wenzelm@32960: | Expr expr --{* expression statement *} schirmer@13384: | Lab jump stmt ("_\ _" [ 99,66]66) schirmer@13384: --{* labeled statement; handles break *} wenzelm@32960: | Comp stmt stmt ("_;; _" [ 66,65]65) wenzelm@32960: | If' expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70) wenzelm@32960: | Loop label expr stmt ("_\ While'(_') _" [ 99,80,79]70) schirmer@13688: | Jmp jump --{* break, continue, return *} wenzelm@32960: | Throw expr schirmer@13384: | TryC stmt qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70) schirmer@13384: --{* @{term "Try c1 Catch(C vn) c2"} *} schirmer@13384: --{* @{text c1}: block were exception may be thrown *} schirmer@13384: --{* @{text C}: execption class to catch *} schirmer@13384: --{* @{text vn}: local name for exception used in @{text c2}*} schirmer@13384: --{* @{text c2}: block to execute when exception is cateched*} wenzelm@32960: | Fin stmt stmt ("_ Finally _" [ 79,79]70) schirmer@13384: | FinA abopt stmt --{* Save abruption of first statement *} schirmer@13384: --{* technical term for smallstep sem.) *} wenzelm@32960: | Init qtname --{* class initialization *} schirmer@12854: schirmer@12854: schirmer@12854: text {* schirmer@12854: The expressions Methd and Body are artificial program constructs, in the schirmer@12854: sense that they are not used to define a concrete Bali program. In the schirmer@13337: operational semantic's they are "generated on the fly" schirmer@13337: to decompose the task to define the behaviour of the Call expression. schirmer@13337: They are crucial for the axiomatic semantics to give a syntactic hook to insert schirmer@13337: some assertions (cf. AxSem.thy, Eval.thy). schirmer@13337: The Init statement (to initialize a class on its first use) is schirmer@13337: inserted in various places by the semantics. schirmer@13337: Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the schirmer@13337: smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the schirmer@13337: local variables of the caller for method return. So ve avoid modelling a schirmer@13337: frame stack. schirmer@13337: The InsInitV/E terms are only used by the smallstep semantics to model the schirmer@13337: intermediate steps of class-initialisation. schirmer@12854: *} schirmer@12854: schirmer@13337: types "term" = "(expr+stmt,var,expr list) sum3" schirmer@12854: translations wenzelm@35431: (type) "sig" <= (type) "mname \ ty list" wenzelm@35431: (type) "term" <= (type) "(expr+stmt,var,expr list) sum3" schirmer@12854: wenzelm@35067: abbreviation this :: expr wenzelm@35067: where "this == Acc (LVar This)" wenzelm@35067: wenzelm@35067: abbreviation LAcc :: "vname \ expr" ("!!") wenzelm@35067: where "!!v == Acc (LVar (EName (VNam v)))" schirmer@12854: wenzelm@35067: abbreviation wenzelm@35067: LAss :: "vname \ expr \stmt" ("_:==_" [90,85] 85) wenzelm@35067: where "v:==e == Expr (Ass (LVar (EName (VNam v))) e)" wenzelm@35067: wenzelm@35067: abbreviation wenzelm@35067: Return :: "expr \ stmt" wenzelm@35067: where "Return e == Expr (Ass (LVar (EName Res)) e);; Jmp Ret" --{* \tt Res := e;; Jmp Ret *} wenzelm@35067: wenzelm@35067: abbreviation wenzelm@35067: StatRef :: "ref_ty \ expr" wenzelm@35067: where "StatRef rt == Cast (RefT rt) (Lit Null)" schirmer@12854: haftmann@35416: definition is_stmt :: "term \ bool" where schirmer@12854: "is_stmt t \ \c. t=In1r c" schirmer@12854: wenzelm@27226: ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *} schirmer@12854: schirmer@12854: declare is_stmt_rews [simp] schirmer@13345: schirmer@13688: text {* schirmer@13688: Here is some syntactic stuff to handle the injections of statements, schirmer@13688: expressions, variables and expression lists into general terms. schirmer@13688: *} schirmer@13688: wenzelm@35067: abbreviation (input) wenzelm@35067: expr_inj_term :: "expr \ term" ("\_\\<^sub>e" 1000) wenzelm@35067: where "\e\\<^sub>e == In1l e" wenzelm@35067: wenzelm@35067: abbreviation (input) wenzelm@35067: stmt_inj_term :: "stmt \ term" ("\_\\<^sub>s" 1000) wenzelm@35067: where "\c\\<^sub>s == In1r c" schirmer@13688: wenzelm@35067: abbreviation (input) wenzelm@35067: var_inj_term :: "var \ term" ("\_\\<^sub>v" 1000) wenzelm@35067: where "\v\\<^sub>v == In2 v" wenzelm@35067: wenzelm@35067: abbreviation (input) wenzelm@35067: lst_inj_term :: "expr list \ term" ("\_\\<^sub>l" 1000) wenzelm@35067: where "\es\\<^sub>l == In3 es" schirmer@13688: schirmer@13688: text {* It seems to be more elegant to have an overloaded injection like the schirmer@13688: following. schirmer@13688: *} schirmer@13688: haftmann@35315: class inj_term = haftmann@35315: fixes inj_term:: "'a \ term" ("\_\" 1000) schirmer@13688: schirmer@13688: text {* How this overloaded injections work can be seen in the theory schirmer@13688: @{text DefiniteAssignment}. Other big inductive relations on schirmer@13688: terms defined in theories @{text WellType}, @{text Eval}, @{text Evaln} and schirmer@13688: @{text AxSem} don't follow this convention right now, but introduce subtle schirmer@13688: syntactic sugar in the relations themselves to make a distinction on schirmer@13688: expressions, statements and so on. So unfortunately you will encounter a wenzelm@35067: mixture of dealing with these injections. The abbreviations above are used schirmer@13688: as bridge between the different conventions. schirmer@13688: *} schirmer@13345: haftmann@35315: instantiation stmt :: inj_term haftmann@35315: begin schirmer@13345: haftmann@35315: definition haftmann@35315: stmt_inj_term_def: "\c::stmt\ \ In1r c" haftmann@35315: haftmann@35315: instance .. haftmann@35315: haftmann@35315: end schirmer@13345: schirmer@13345: lemma stmt_inj_term_simp: "\c::stmt\ = In1r c" schirmer@13345: by (simp add: stmt_inj_term_def) schirmer@13345: schirmer@13688: lemma stmt_inj_term [iff]: "\x::stmt\ = \y\ \ x = y" schirmer@13688: by (simp add: stmt_inj_term_simp) schirmer@13688: haftmann@35315: instantiation expr :: inj_term haftmann@35315: begin schirmer@13345: haftmann@35315: definition haftmann@35315: expr_inj_term_def: "\e::expr\ \ In1l e" haftmann@35315: haftmann@35315: instance .. haftmann@35315: haftmann@35315: end schirmer@13345: schirmer@13345: lemma expr_inj_term_simp: "\e::expr\ = In1l e" schirmer@13345: by (simp add: expr_inj_term_def) schirmer@13345: schirmer@13688: lemma expr_inj_term [iff]: "\x::expr\ = \y\ \ x = y" schirmer@13688: by (simp add: expr_inj_term_simp) schirmer@13688: haftmann@35315: instantiation var :: inj_term haftmann@35315: begin schirmer@13345: haftmann@35315: definition haftmann@35315: var_inj_term_def: "\v::var\ \ In2 v" haftmann@35315: haftmann@35315: instance .. haftmann@35315: haftmann@35315: end schirmer@13345: schirmer@13345: lemma var_inj_term_simp: "\v::var\ = In2 v" schirmer@13345: by (simp add: var_inj_term_def) schirmer@13345: schirmer@13688: lemma var_inj_term [iff]: "\x::var\ = \y\ \ x = y" schirmer@13688: by (simp add: var_inj_term_simp) schirmer@13688: haftmann@35315: class expr_of = haftmann@35315: fixes expr_of :: "'a \ expr" haftmann@35315: haftmann@35315: instantiation expr :: expr_of haftmann@35315: begin haftmann@35315: haftmann@35315: definition haftmann@35315: "expr_of = (\(e::expr). e)" haftmann@35315: haftmann@35315: instance .. haftmann@35315: haftmann@35315: end schirmer@13345: haftmann@35315: instantiation list :: (expr_of) inj_term haftmann@35315: begin haftmann@35315: haftmann@35315: definition haftmann@35315: "\es::'a list\ \ In3 (map expr_of es)" haftmann@35315: haftmann@35315: instance .. haftmann@35315: haftmann@35315: end haftmann@35315: haftmann@35315: lemma expr_list_inj_term_def: haftmann@35315: "\es::expr list\ \ In3 es" haftmann@35315: by (simp add: inj_term_list_def expr_of_expr_def) schirmer@13345: schirmer@13345: lemma expr_list_inj_term_simp: "\es::expr list\ = In3 es" schirmer@13345: by (simp add: expr_list_inj_term_def) schirmer@13345: schirmer@13688: lemma expr_list_inj_term [iff]: "\x::expr list\ = \y\ \ x = y" schirmer@13688: by (simp add: expr_list_inj_term_simp) schirmer@13688: schirmer@13688: lemmas inj_term_simps = stmt_inj_term_simp expr_inj_term_simp var_inj_term_simp schirmer@13688: expr_list_inj_term_simp schirmer@13688: lemmas inj_term_sym_simps = stmt_inj_term_simp [THEN sym] schirmer@13688: expr_inj_term_simp [THEN sym] schirmer@13688: var_inj_term_simp [THEN sym] schirmer@13688: expr_list_inj_term_simp [THEN sym] schirmer@13688: schirmer@13688: lemma stmt_expr_inj_term [iff]: "\t::stmt\ \ \w::expr\" schirmer@13688: by (simp add: inj_term_simps) schirmer@13688: lemma expr_stmt_inj_term [iff]: "\t::expr\ \ \w::stmt\" schirmer@13688: by (simp add: inj_term_simps) schirmer@13688: lemma stmt_var_inj_term [iff]: "\t::stmt\ \ \w::var\" schirmer@13688: by (simp add: inj_term_simps) schirmer@13688: lemma var_stmt_inj_term [iff]: "\t::var\ \ \w::stmt\" schirmer@13688: by (simp add: inj_term_simps) schirmer@13688: lemma stmt_elist_inj_term [iff]: "\t::stmt\ \ \w::expr list\" schirmer@13688: by (simp add: inj_term_simps) schirmer@13688: lemma elist_stmt_inj_term [iff]: "\t::expr list\ \ \w::stmt\" schirmer@13688: by (simp add: inj_term_simps) schirmer@13688: lemma expr_var_inj_term [iff]: "\t::expr\ \ \w::var\" schirmer@13688: by (simp add: inj_term_simps) schirmer@13688: lemma var_expr_inj_term [iff]: "\t::var\ \ \w::expr\" schirmer@13688: by (simp add: inj_term_simps) schirmer@13688: lemma expr_elist_inj_term [iff]: "\t::expr\ \ \w::expr list\" schirmer@13688: by (simp add: inj_term_simps) schirmer@13688: lemma elist_expr_inj_term [iff]: "\t::expr list\ \ \w::expr\" schirmer@13688: by (simp add: inj_term_simps) schirmer@13688: lemma var_elist_inj_term [iff]: "\t::var\ \ \w::expr list\" schirmer@13688: by (simp add: inj_term_simps) schirmer@13688: lemma elist_var_inj_term [iff]: "\t::expr list\ \ \w::var\" schirmer@13688: by (simp add: inj_term_simps) schirmer@13688: schirmer@13690: lemma term_cases: " schirmer@13690: \\ v. P \v\\<^sub>v; \ e. P \e\\<^sub>e;\ c. P \c\\<^sub>s;\ l. P \l\\<^sub>l\ schirmer@13690: \ P t" schirmer@13690: apply (cases t) schirmer@13690: apply (case_tac a) schirmer@13690: apply auto schirmer@13690: done schirmer@13690: schirmer@13688: section {* Evaluation of unary operations *} schirmer@13688: consts eval_unop :: "unop \ val \ val" schirmer@13688: primrec schirmer@13688: "eval_unop UPlus v = Intg (the_Intg v)" schirmer@13688: "eval_unop UMinus v = Intg (- (the_Intg v))" schirmer@13688: "eval_unop UBitNot v = Intg 42" -- "FIXME: Not yet implemented" schirmer@13688: "eval_unop UNot v = Bool (\ the_Bool v)" schirmer@13688: schirmer@13688: section {* Evaluation of binary operations *} schirmer@13688: consts eval_binop :: "binop \ val \ val \ val" schirmer@13688: primrec schirmer@13688: "eval_binop Mul v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" schirmer@13688: "eval_binop Div v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))" schirmer@13688: "eval_binop Mod v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))" schirmer@13688: "eval_binop Plus v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))" schirmer@13688: "eval_binop Minus v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))" schirmer@13688: schirmer@13688: -- "Be aware of the explicit coercion of the shift distance to nat" schirmer@13688: "eval_binop LShift v1 v2 = Intg ((the_Intg v1) * (2^(nat (the_Intg v2))))" schirmer@13688: "eval_binop RShift v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))" schirmer@13688: "eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented" schirmer@13688: schirmer@13688: "eval_binop Less v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" schirmer@13688: "eval_binop Le v1 v2 = Bool ((the_Intg v1) \ (the_Intg v2))" schirmer@13688: "eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))" schirmer@13688: "eval_binop Ge v1 v2 = Bool ((the_Intg v2) \ (the_Intg v1))" schirmer@13688: schirmer@13688: "eval_binop Eq v1 v2 = Bool (v1=v2)" schirmer@13688: "eval_binop Neq v1 v2 = Bool (v1\v2)" schirmer@13688: "eval_binop BitAnd v1 v2 = Intg 42" -- "FIXME: Not yet implemented" schirmer@13688: "eval_binop And v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))" schirmer@13688: "eval_binop BitXor v1 v2 = Intg 42" -- "FIXME: Not yet implemented" schirmer@13688: "eval_binop Xor v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))" schirmer@13688: "eval_binop BitOr v1 v2 = Intg 42" -- "FIXME: Not yet implemented" schirmer@13688: "eval_binop Or v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))" schirmer@13688: "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))" schirmer@13688: "eval_binop CondOr v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))" schirmer@13688: haftmann@35416: definition need_second_arg :: "binop \ val \ bool" where schirmer@13688: "need_second_arg binop v1 \ \ ((binop=CondAnd \ \ the_Bool v1) \ schirmer@13688: (binop=CondOr \ the_Bool v1))" schirmer@13688: text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument schirmer@13688: if the value isn't already determined by the first argument*} schirmer@13688: schirmer@13688: lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b" schirmer@13688: by (simp add: need_second_arg_def) schirmer@13688: schirmer@13688: lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\ b)" schirmer@13688: by (simp add: need_second_arg_def) schirmer@13688: schirmer@13688: lemma need_second_arg_strict[simp]: schirmer@13688: "\binop\CondAnd; binop\CondOr\ \ need_second_arg binop b" schirmer@13688: by (cases binop) schirmer@13688: (simp_all add: need_second_arg_def) schirmer@12854: end