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