src/HOL/Bali/Term.thy
author wenzelm
Sat, 29 Mar 2008 19:14:00 +0100
changeset 26480 544cef16045b
parent 24783 5a3e336a2e37
child 27226 5a3e5e46d977
permissions -rw-r--r--
replaced 'ML_setup' by 'ML';
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 *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    70
	= Loc loc    --{* location of allocated execption object *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
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 *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    95
	= Static                   --{* static *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
    96
	| SuperM                   --{* super  *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
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  *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
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
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   145
	= LVar lname --{* local variable (incl. parameters) *}
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*}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   156
	| AVar expr expr ("_.[_]"[90,10   ]90)
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
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   164
	= NewC qtname         --{* class instance creation *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   165
	| NewA ty expr ("New _[_]"[99,10   ]85) 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   166
                              --{* array creation *} 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   167
	| Cast ty expr        --{* type cast  *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   168
	| Inst expr ref_ty ("_ InstOf _"[85,99] 85)   
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   169
                              --{* instanceof *}     
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   170
	| Lit  val              --{* literal value, references not allowed *}
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
        
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   174
	| Super               --{* special Super keyword *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   175
	| Acc  var            --{* variable access *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   176
	| Ass  var expr       ("_:=_"   [90,85   ]85)
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   177
                              --{* variable assign *} 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   178
	| Cond expr expr expr ("_ ? _ : _" [85,85,80]80) --{* conditional *}  
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
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   201
	= Skip                  --{* empty      statement *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
diff changeset
   202
	| Expr  expr            --{* expression statement *}
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 *}
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   205
	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
24783
5a3e336a2e37 avoid internal names;
wenzelm
parents: 24019
diff changeset
   206
	| If'   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
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 *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
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*}
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
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.) *}
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13358
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
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
  this    :: expr
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   250
  LAcc    :: "vname \<Rightarrow> expr" ("!!")
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   251
  LAss    :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
  Return  :: "expr \<Rightarrow> stmt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
  StatRef :: "ref_ty \<Rightarrow> expr"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
 "this"       == "Acc (LVar This)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
 "!!v"        == "Acc (LVar (EName (VNam v)))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
 "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
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
   260
 "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Jmp Ret" 
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
   261
                  --{* \tt Res := e;; Jmp Ret *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
 "StatRef rt" == "Cast (RefT rt) (Lit Null)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
  is_stmt :: "term \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
 "is_stmt t \<equiv> \<exists>c. t=In1r c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
26480
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 24783
diff changeset
   269
ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
declare is_stmt_rews [simp]
13345
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   272
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
   273
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
   274
  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
   275
  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
   276
*}
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
syntax 
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
   279
  expr_inj_term:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 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
   280
  stmt_inj_term:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 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
   281
  var_inj_term::  "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 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
   282
  lst_inj_term:: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 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
   283
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
   284
translations 
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
   285
  "\<langle>e\<rangle>\<^sub>e" \<rightharpoonup> "In1l e"
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
  "\<langle>c\<rangle>\<^sub>s" \<rightharpoonup> "In1r c"
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
   287
  "\<langle>v\<rangle>\<^sub>v" \<rightharpoonup> "In2 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
   288
  "\<langle>es\<rangle>\<^sub>l" \<rightharpoonup> "In3 es"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   289
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   290
text {* It seems to be more elegant to have an overloaded injection like the
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   291
following.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   292
*}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   293
13345
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   294
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
   295
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
   296
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   297
text {* How this overloaded injections work can be seen in the theory 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   298
@{text DefiniteAssignment}. Other big inductive relations on
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   299
terms defined in theories @{text WellType}, @{text Eval}, @{text Evaln} and
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   300
@{text AxSem} don't follow this convention right now, but introduce subtle 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   301
syntactic sugar in the relations themselves to make a distinction on 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   302
expressions, statements and so on. So unfortunately you will encounter a 
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
mixture of dealing with these injections. The translations above are used
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   304
as bridge between the different conventions.  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13384
diff changeset
   305
*}
13345
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   306
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   307
instance stmt::inj_term ..
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   308
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   309
defs (overloaded)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   310
stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   311
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   312
lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   313
by (simp add: stmt_inj_term_def)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   314
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
   315
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
   316
  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
   317
13345
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   318
instance expr::inj_term ..
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   319
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   320
defs (overloaded)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   321
expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   322
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   323
lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   324
by (simp add: expr_inj_term_def)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   325
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
   326
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
   327
  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
   328
13345
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   329
instance var::inj_term ..
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   330
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   331
defs (overloaded)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   332
var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   333
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   334
lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   335
by (simp add: var_inj_term_def)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   336
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
   337
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
   338
  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
   339
13345
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   340
instance "list":: (type) inj_term ..
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   341
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   342
defs (overloaded)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   343
expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   344
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   345
lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   346
by (simp add: expr_list_inj_term_def)
bd611943cbc2 Fixed markup error in comment.
schirmer
parents: 13337
diff changeset
   347
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
   348
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
   349
  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
   350
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
   351
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
   352
                        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
   353
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
   354
                            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
   355
                            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
   356
                            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
   357
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
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
   359
  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
   360
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
   361
  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
   362
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
   363
  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
   364
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
   365
  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
   366
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
   367
  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
   368
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
   369
  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
   370
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
   371
  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
   372
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
   373
  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
   374
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
   375
  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
   376
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
   377
  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
   378
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
   379
  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
   380
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
   381
  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
   382
13690
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   383
lemma term_cases: "
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   384
  \<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
   385
  \<Longrightarrow> P t"
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   386
  apply (cases t)
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   387
  apply (case_tac a)
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   388
  apply auto
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   389
  done
ac335b2f4a39 Inserted some extra paragraphs in large proofs to make tex run...
schirmer
parents: 13688
diff changeset
   390
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
   391
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
   392
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
   393
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
   394
"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
   395
"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
   396
"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
   397
"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
   398
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
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
   400
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
   401
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
   402
"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
   403
"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
   404
"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
   405
"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
   406
"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
   407
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
-- "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
   409
"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
   410
"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
   411
"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
   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
"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
   414
"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
   415
"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
   416
"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
   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 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
   419
"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
   420
"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
   421
"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
   422
"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
   423
"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
   424
"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
   425
"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
   426
"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
   427
"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
   428
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
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
   430
"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
   431
                               (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
   432
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
   433
 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
   434
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
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
   436
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
   437
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
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
   439
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
   440
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
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
   442
 "\<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
   443
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
   444
   (simp_all add: need_second_arg_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
end