
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) "\<lparr>name::mname,parTs::ty list\<rparr>"
wenzelm@35431:   (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
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:             ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) 
schirmer@13384:                     --{* method call *} 
schirmer@13384:                     --{* @{term "{accC,statT,mode}e\<cdot>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       ("_\<bullet> _" [      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 ("_\<bullet> 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 \<times> 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 \<Rightarrow> expr" ("!!")
wenzelm@35067:   where "!!v == Acc (LVar (EName (VNam v)))"
schirmer@12854: 
wenzelm@35067: abbreviation
wenzelm@35067:   LAss :: "vname \<Rightarrow> expr \<Rightarrow>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 \<Rightarrow> 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 \<Rightarrow> expr"
wenzelm@35067:   where "StatRef rt == Cast (RefT rt) (Lit Null)"
schirmer@12854:   
haftmann@35416: definition is_stmt :: "term \<Rightarrow> bool" where
schirmer@12854:  "is_stmt t \<equiv> \<exists>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 \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
wenzelm@35067:   where "\<langle>e\<rangle>\<^sub>e == In1l e"
wenzelm@35067: 
wenzelm@35067: abbreviation (input)
wenzelm@35067:   stmt_inj_term :: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
wenzelm@35067:   where "\<langle>c\<rangle>\<^sub>s == In1r c"
schirmer@13688: 
wenzelm@35067: abbreviation (input)
wenzelm@35067:   var_inj_term :: "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 1000)
wenzelm@35067:   where "\<langle>v\<rangle>\<^sub>v == In2 v"
wenzelm@35067: 
wenzelm@35067: abbreviation (input)
wenzelm@35067:   lst_inj_term :: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
wenzelm@35067:   where "\<langle>es\<rangle>\<^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 \<Rightarrow> term" ("\<langle>_\<rangle>" 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: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
haftmann@35315: 
haftmann@35315: instance ..
haftmann@35315: 
haftmann@35315: end
schirmer@13345: 
schirmer@13345: lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
schirmer@13345: by (simp add: stmt_inj_term_def)
schirmer@13345: 
schirmer@13688: lemma  stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> 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: "\<langle>e::expr\<rangle> \<equiv> In1l e"
haftmann@35315: 
haftmann@35315: instance ..
haftmann@35315: 
haftmann@35315: end
schirmer@13345: 
schirmer@13345: lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
schirmer@13345: by (simp add: expr_inj_term_def)
schirmer@13345: 
schirmer@13688: lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> 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: "\<langle>v::var\<rangle> \<equiv> In2 v"
haftmann@35315: 
haftmann@35315: instance ..
haftmann@35315: 
haftmann@35315: end
schirmer@13345: 
schirmer@13345: lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
schirmer@13345: by (simp add: var_inj_term_def)
schirmer@13345: 
schirmer@13688: lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
schirmer@13688:   by (simp add: var_inj_term_simp)
schirmer@13688: 
haftmann@35315: class expr_of =
haftmann@35315:   fixes expr_of :: "'a \<Rightarrow> expr"
haftmann@35315: 
haftmann@35315: instantiation expr :: expr_of
haftmann@35315: begin
haftmann@35315: 
haftmann@35315: definition
haftmann@35315:   "expr_of = (\<lambda>(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:   "\<langle>es::'a list\<rangle> \<equiv> 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:   "\<langle>es::expr list\<rangle> \<equiv> 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: "\<langle>es::expr list\<rangle> = In3 es"
schirmer@13345: by (simp add: expr_list_inj_term_def)
schirmer@13345: 
schirmer@13688: lemma expr_list_inj_term [iff]: "\<langle>x::expr list\<rangle> = \<langle>y\<rangle> \<equiv> 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]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr\<rangle>"
schirmer@13688:   by (simp add: inj_term_simps)
schirmer@13688: lemma expr_stmt_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
schirmer@13688:   by (simp add: inj_term_simps)
schirmer@13688: lemma stmt_var_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::var\<rangle>"
schirmer@13688:   by (simp add: inj_term_simps)
schirmer@13688: lemma var_stmt_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
schirmer@13688:   by (simp add: inj_term_simps)
schirmer@13688: lemma stmt_elist_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
schirmer@13688:   by (simp add: inj_term_simps)
schirmer@13688: lemma elist_stmt_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
schirmer@13688:   by (simp add: inj_term_simps)
schirmer@13688: lemma expr_var_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::var\<rangle>"
schirmer@13688:   by (simp add: inj_term_simps)
schirmer@13688: lemma var_expr_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr\<rangle>"
schirmer@13688:   by (simp add: inj_term_simps)
schirmer@13688: lemma expr_elist_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
schirmer@13688:   by (simp add: inj_term_simps)
schirmer@13688: lemma elist_expr_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::expr\<rangle>"
schirmer@13688:   by (simp add: inj_term_simps)
schirmer@13688: lemma var_elist_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
schirmer@13688:   by (simp add: inj_term_simps)
schirmer@13688: lemma elist_var_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::var\<rangle>"
schirmer@13688:   by (simp add: inj_term_simps)
schirmer@13688: 
schirmer@13690: lemma term_cases: "
schirmer@13690:   \<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>
schirmer@13690:   \<Longrightarrow> 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 \<Rightarrow> val \<Rightarrow> 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 (\<not> the_Bool v)"
schirmer@13688: 
schirmer@13688: section {* Evaluation of binary operations *}
schirmer@13688: consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> 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) \<le> (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) \<le> (the_Intg v1))"
schirmer@13688: 
schirmer@13688: "eval_binop Eq      v1 v2 = Bool (v1=v2)"
schirmer@13688: "eval_binop Neq     v1 v2 = Bool (v1\<noteq>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) \<and> (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) \<noteq> (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) \<or> (the_Bool v2))"
schirmer@13688: "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
schirmer@13688: "eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
schirmer@13688: 
haftmann@35416: definition need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
schirmer@13688: "need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
schirmer@13688:                                (binop=CondOr  \<and> 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) = (\<not> b)" 
schirmer@13688: by (simp add: need_second_arg_def)
schirmer@13688: 
schirmer@13688: lemma need_second_arg_strict[simp]: 
schirmer@13688:  "\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
schirmer@13688: by (cases binop) 
schirmer@13688:    (simp_all add: need_second_arg_def)
schirmer@12854: end



