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