src/HOL/Bali/Term.thy
author wenzelm
Wed, 10 Feb 2010 00:45:16 +0100
changeset 35067 af4c18c30593
parent 32960 69916a850301
child 35069 09154b995ed8
permissions -rw-r--r--
modernized syntax translations, using mostly abbreviation/notation; minor tuning;
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
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {* Java expressions and statements *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     8
theory Term imports Value Table begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
design issues:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
\item invocation frames for local variables could be reduced to special static
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
  objects (one per method). This would reduce redundancy, but yield a rather
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
  non-standard execution model more difficult to understand.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
\item method bodies separated from calls to handle assumptions in axiomat. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
  semantics
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
  NB: Body is intended to be in the environment of the called method.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
\item class initialization is regarded as (auxiliary) statement 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
      (required for AxSem)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
\item result expression of method return is handled by a special result variable
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
  result variable is treated uniformly with local variables
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
  \begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
  \item[+] welltypedness and existence of the result/return expression is 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
           ensured without extra efford
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
  \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
simplifications:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
\item expression statement allowed for any expression
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
\item This  is modeled as a special non-assignable local variable
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
\item Super is modeled as a general expression with the same value as This
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
\item access to field x in current class via This.x
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
\item NewA creates only one-dimensional arrays;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
  initialization of further subarrays may be simulated with nested NewAs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
\item The 'Lit' constructor is allowed to contain a reference value.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
  But this is assumed to be prohibited in the input language, which is enforced
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
  by the type-checking rules.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
\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
    41
      variable
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
\item no nested blocks with inner local variables
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
\item no synchronized statements
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
\item no secondary forms of if, while (e.g. no for) (may be easily simulated)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
\item no switch (may be simulated with if)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
\item the @{text try_catch_finally} statement is divided into the 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
      @{text try_catch} statement 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
      and a finally statement, which may be considered as try..finally with 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
      empty catch
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
\item the @{text try_catch} statement has exactly one catch clause; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
      multiple ones can be
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
  simulated with instanceof
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
\item the compiler is supposed to add the annotations {@{text _}} during 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
      type-checking. This
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
  transformation is left out as its result is checked by the type rules anyway
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    59
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    60
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    61
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
    62
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    63
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    64
datatype jump
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    65
        = Break label --{* break *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    66
        | Cont label  --{* continue *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    67
        | 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
    68
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    69
datatype xcpt        --{* exception *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
    70
        = Loc loc    --{* location of allocated execption object *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
    71
        | 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
    72
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    73
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
    74
       =  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
    75
        | 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
    76
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    77
datatype abrupt       --{* abrupt completion *} 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    78
        = Xcpt xcpt   --{* exception *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    79
        | Jump jump   --{* break, continue, return *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    80
        | Error error -- {* runtime errors, we wan't to detect and proof absent
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    81
                            in welltyped programms *}
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    82
types
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    83
  abopt  = "abrupt option"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    84
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    85
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
    86
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
    87
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
    88
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
    89
statement *}
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    90
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    91
translations
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    92
 "locals" <= (type) "(lname, val) table"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    93
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    94
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
    95
        = Static                   --{* static *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
    96
        | SuperM                   --{* super  *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
    97
        | IntVir                   --{* interface or virtual *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    99
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
   100
          name ::"mname"   --{* acutally belongs to Decl.thy *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
          parTs::"ty list"        
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
  "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
  "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   107
--{* function codes for unary operations *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   108
datatype unop =  UPlus    -- {*{\tt +} unary plus*} 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   109
               | UMinus   -- {*{\tt -} unary minus*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   110
               | UBitNot  -- {*{\tt ~} bitwise NOT*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   111
               | 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
   112
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   113
--{* function codes for binary operations *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   114
datatype binop = Mul     -- {*{\tt * }   multiplication*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   115
               | Div     -- {*{\tt /}   division*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   116
               | Mod     -- {*{\tt \%}   remainder*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   117
               | Plus    -- {*{\tt +}   addition*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   118
               | Minus   -- {*{\tt -}   subtraction*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   119
               | LShift  -- {*{\tt <<}  left shift*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   120
               | RShift  -- {*{\tt >>}  signed right shift*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   121
               | RShiftU -- {*{\tt >>>} unsigned right shift*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   122
               | Less    -- {*{\tt <}   less than*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   123
               | Le      -- {*{\tt <=}  less than or equal*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   124
               | Greater -- {*{\tt >}   greater than*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   125
               | Ge      -- {*{\tt >=}  greater than or equal*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   126
               | Eq      -- {*{\tt ==}  equal*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   127
               | Neq     -- {*{\tt !=}  not equal*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   128
               | BitAnd  -- {*{\tt \&}   bitwise AND*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   129
               | And     -- {*{\tt \&}   boolean AND*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   130
               | BitXor  -- {*{\texttt \^}   bitwise Xor*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   131
               | Xor     -- {*{\texttt \^}   boolean Xor*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   132
               | BitOr   -- {*{\tt |}   bitwise Or*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   133
               | Or      -- {*{\tt |}   boolean Or*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   134
               | CondAnd -- {*{\tt \&\&}  conditional And*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   135
               | CondOr  -- {*{\tt ||}  conditional Or *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   136
text{* The boolean operators {\tt \&} and {\tt |} strictly evaluate both
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   137
of their arguments. The conditional operators {\tt \&\&} and {\tt ||} only 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   138
evaluate the second argument if the value of the whole expression isn't 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   139
allready determined by the first argument.
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   140
e.g.: {\tt false \&\& e} e is not evaluated;  
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   141
      {\tt true || e} e is not evaluated; 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   142
*}
13358
c837ba4cfb62 fix latex output
schirmer
parents: 13345
diff changeset
   143
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
datatype var
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   145
        = LVar lname --{* local variable (incl. parameters) *}
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   146
        | FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90)
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   147
                     --{* class field *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   148
                     --{* @{term "{accC,statDeclC,stat}e..fn"}   *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   149
                     --{* @{text accC}: accessing class (static class were *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   150
                     --{* the code is declared. Annotation only needed for *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   151
                     --{* evaluation to check accessibility) *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   152
                     --{* @{text statDeclC}: static declaration class of field*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   153
                     --{* @{text stat}: static or instance field?*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   154
                     --{* @{text e}: reference to object*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   155
                     --{* @{text fn}: field name*}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   156
        | AVar expr expr ("_.[_]"[90,10   ]90)
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   157
                     --{* array component *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   158
                     --{* @{term "e1.[e2]"}: e1 array reference; e2 index *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   159
        | InsInitV stmt var 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   160
                     --{* insertion of initialization before evaluation   *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   161
                     --{* of var (technical term for smallstep semantics.)*}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
and expr
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   164
        = NewC qtname         --{* class instance creation *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   165
        | NewA ty expr ("New _[_]"[99,10   ]85) 
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   166
                              --{* array creation *} 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   167
        | Cast ty expr        --{* type cast  *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   168
        | Inst expr ref_ty ("_ InstOf _"[85,99] 85)   
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   169
                              --{* instanceof *}     
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   170
        | Lit  val              --{* literal value, references not allowed *}
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   171
        | UnOp unop expr        --{* unary operation *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   172
        | 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
   173
        
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   174
        | Super               --{* special Super keyword *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   175
        | Acc  var            --{* variable access *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   176
        | Ass  var expr       ("_:=_"   [90,85   ]85)
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   177
                              --{* variable assign *} 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   178
        | Cond expr expr expr ("_ ? _ : _" [85,85,80]80) --{* conditional *}  
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   179
        | Call qtname ref_ty inv_mode expr mname "(ty list)" "(expr list)"  
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   180
            ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   181
                    --{* method call *} 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   182
                    --{* @{term "{accC,statT,mode}e\<cdot>mn({pTs}args)"} " *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   183
                    --{* @{text accC}: accessing class (static class were *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   184
                    --{* the call code is declared. Annotation only needed for*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   185
                    --{* evaluation to check accessibility) *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   186
                    --{* @{text statT}: static declaration class/interface of *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   187
                    --{* method *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   188
                    --{* @{text mode}: invocation mode *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   189
                    --{* @{text e}: reference to object*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   190
                    --{* @{text mn}: field name*}   
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   191
                    --{* @{text pTs}: types of parameters *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   192
                    --{* @{text args}: the actual parameters/arguments *} 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   193
        | Methd qtname sig    --{*   (folded) method (see below) *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   194
        | Body qtname stmt    --{* (unfolded) method body *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   195
        | InsInitE stmt expr  
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   196
                 --{* insertion of initialization before *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   197
                 --{* evaluation of expr (technical term for smallstep sem.) *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   198
        | Callee locals expr  --{* save callers locals in callee-Frame *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   199
                              --{* (technical term for smallstep semantics) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
and  stmt
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   201
        = Skip                  --{* empty      statement *}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   202
        | Expr  expr            --{* expression statement *}
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   203
        | Lab   jump stmt       ("_\<bullet> _" [      99,66]66)
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   204
                                --{* labeled statement; handles break *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   205
        | Comp  stmt stmt       ("_;; _"                  [      66,65]65)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   206
        | 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
   207
        | 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
   208
        | Jmp jump              --{* break, continue, return *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   209
        | Throw expr
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   210
        | TryC  stmt qtname vname stmt ("Try _ Catch'(_ _') _"  [79,99,80,79]70)
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   211
             --{* @{term "Try c1 Catch(C vn) c2"} *} 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   212
             --{* @{text c1}: block were exception may be thrown *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   213
             --{* @{text C}:  execption class to catch *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   214
             --{* @{text vn}: local name for exception used in @{text c2}*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   215
             --{* @{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
   216
        | Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   217
        | FinA abopt stmt       --{* Save abruption of first statement *} 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   218
                                --{* technical term  for smallstep sem.) *}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27226
diff changeset
   219
        | Init  qtname          --{* class initialization *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
The expressions Methd and Body are artificial program constructs, in the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
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
   225
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
   226
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
   227
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
   228
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
   229
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
   230
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
   231
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
   232
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
   233
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
   234
frame stack.
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   235
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
   236
intermediate steps of class-initialisation.
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
 
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   239
types "term" = "(expr+stmt,var,expr list) sum3"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
  "sig"   <= (type) "mname \<times> ty list"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
  "var"   <= (type) "Term.var"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
  "expr"  <= (type) "Term.expr"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
  "stmt"  <= (type) "Term.stmt"
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   245
  "term"  <= (type) "(expr+stmt,var,expr list) sum3"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   247
abbreviation this :: expr
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   248
  where "this == Acc (LVar This)"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   249
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   250
abbreviation LAcc :: "vname \<Rightarrow> expr" ("!!")
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   251
  where "!!v == Acc (LVar (EName (VNam v)))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
35067
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
  LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   255
  where "v:==e == Expr (Ass (LVar (EName (VNam  v))) e)"
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
  Return :: "expr \<Rightarrow> stmt"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   259
  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
   260
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   261
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   262
  StatRef :: "ref_ty \<Rightarrow> expr"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   263
  where "StatRef rt == Cast (RefT rt) (Lit Null)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
  is_stmt :: "term \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
 "is_stmt t \<equiv> \<exists>c. t=In1r c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
27226
5a3e5e46d977 sum3_instantiate: proper context;
wenzelm
parents: 26480
diff changeset
   270
ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
declare is_stmt_rews [simp]
13345
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   273
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
   274
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
   275
  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
   276
  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
   277
*}
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
   278
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   279
abbreviation (input)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   280
  expr_inj_term :: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   281
  where "\<langle>e\<rangle>\<^sub>e == In1l e"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   282
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   283
abbreviation (input)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   284
  stmt_inj_term :: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   285
  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
   286
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   287
abbreviation (input)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   288
  var_inj_term :: "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 1000)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   289
  where "\<langle>v\<rangle>\<^sub>v == In2 v"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   290
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   291
abbreviation (input)
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
   292
  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
   293
  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
   294
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
   295
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
   296
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
   297
*}
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
13345
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   299
axclass inj_term < "type"
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
   300
consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
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
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
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
   303
@{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
   304
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
   305
@{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
   306
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
   307
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
   308
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
   309
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
   310
*}
13345
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   311
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   312
instance stmt::inj_term ..
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   313
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   314
defs (overloaded)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   315
stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
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
13345
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   323
instance expr::inj_term ..
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   324
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   325
defs (overloaded)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   326
expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   327
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   328
lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   329
by (simp add: expr_inj_term_def)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   330
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
   331
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
   332
  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
   333
13345
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   334
instance var::inj_term ..
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   335
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   336
defs (overloaded)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   337
var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   338
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   339
lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   340
by (simp add: var_inj_term_def)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   341
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
   342
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
   343
  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
   344
13345
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   345
instance "list":: (type) inj_term ..
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   346
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   347
defs (overloaded)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   348
expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   349
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   350
lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   351
by (simp add: expr_list_inj_term_def)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   352
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
   353
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
   354
  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
   355
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
   356
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
   357
                        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
   358
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
   359
                            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
   360
                            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
   361
                            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
   362
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
   363
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
   364
  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
   365
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
   366
  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
   367
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
   368
  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
   369
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
   370
  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
   371
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
   372
  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
   373
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
   374
  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
   375
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
   376
  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
   377
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
   378
  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
   379
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
   380
  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
   381
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
   382
  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
   383
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
   384
  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
   385
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
   386
  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
   387
13690
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   388
lemma term_cases: "
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   389
  \<lbrakk>\<And> v. P \<langle>v\<rangle>\<^sub>v; \<And> e. P \<langle>e\<rangle>\<^sub>e;\<And> c. P \<langle>c\<rangle>\<^sub>s;\<And> l. P \<langle>l\<rangle>\<^sub>l\<rbrakk>
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   390
  \<Longrightarrow> P t"
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   391
  apply (cases t)
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   392
  apply (case_tac a)
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   393
  apply auto
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   394
  done
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   395
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
   396
section {* Evaluation of unary operations *}
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
consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
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
primrec
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
"eval_unop UPlus   v = Intg (the_Intg v)"
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
"eval_unop UMinus  v = Intg (- (the_Intg v))"
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
"eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
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
"eval_unop UNot    v = Bool (\<not> the_Bool v)"
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
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
section {* Evaluation of binary operations *}
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
consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
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
primrec
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
"eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
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
"eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
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
"eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
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
"eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
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
"eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
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
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
-- "Be aware of the explicit coercion of the shift distance to nat"
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
"eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
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
"eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
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
"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
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
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
"eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
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
"eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
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
   420
"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
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
   421
"eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
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
   422
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
   423
"eval_binop Eq      v1 v2 = Bool (v1=v2)"
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
   424
"eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
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
   425
"eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
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
   426
"eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
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
   427
"eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
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
"eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
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
   429
"eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
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
   430
"eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
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
   431
"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
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
   432
"eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
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
   433
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
   434
constdefs need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool"
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
"need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
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
                               (binop=CondOr  \<and> the_Bool v1))"
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
   437
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
   438
 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
   439
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
   440
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
   441
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
   442
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
   443
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
   444
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
   445
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
   446
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
   447
 "\<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
   448
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
   449
   (simp_all add: need_second_arg_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
end