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