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