src/HOL/Bali/Evaln.thy
author schirmer
Thu Oct 31 18:27:10 2002 +0100 (2002-10-31)
changeset 13688 a0b16d42d489
parent 13601 fd3e3d6b37b2
child 13690 ac335b2f4a39
permissions -rw-r--r--
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
wenzelm@12857
     1
(*  Title:      HOL/Bali/Evaln.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12925
     3
    Author:     David von Oheimb and Norbert Schirmer
wenzelm@12859
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
schirmer@12854
     5
*)
schirmer@12854
     6
header {* Operational evaluation (big-step) semantics of Java expressions and 
schirmer@12854
     7
          statements
schirmer@12854
     8
*}
schirmer@12854
     9
schirmer@13688
    10
theory Evaln = TypeSafe:
schirmer@13688
    11
schirmer@12854
    12
schirmer@12854
    13
text {*
schirmer@13688
    14
Variant of @{term eval} relation with counter for bounded recursive depth. 
schirmer@13688
    15
In principal @{term evaln} could replace @{term eval}.
schirmer@13688
    16
schirmer@13688
    17
Validity of the axiomatic semantics builds on @{term evaln}. 
schirmer@13688
    18
For recursive method calls the axiomatic semantics rule assumes the method ok 
schirmer@13688
    19
to derive a proof for the body. To prove the method rule sound we need to 
schirmer@13688
    20
perform induction on the recursion depth. 
schirmer@13688
    21
For the completeness proof of the axiomatic semantics the notion of the most
schirmer@13688
    22
general formula is used. The most general formula right now builds on the 
schirmer@13688
    23
ordinary evaluation relation @{term eval}. 
schirmer@13688
    24
So sometimes we have to switch between @{term evaln} and @{term eval} and vice 
schirmer@13688
    25
versa. To make
schirmer@13688
    26
this switch easy @{term evaln} also does all the technical accessibility tests 
schirmer@13688
    27
@{term check_field_access} and @{term check_method_access} like @{term eval}. 
schirmer@13688
    28
If it would omit them @{term evaln} and @{term eval} would only be equivalent 
schirmer@13688
    29
for welltyped, and definitely assigned terms.
schirmer@12854
    30
*}
schirmer@12854
    31
schirmer@12854
    32
consts
schirmer@12854
    33
schirmer@12854
    34
  evaln	:: "prog \<Rightarrow> (state \<times> term \<times> nat \<times> vals \<times> state) set"
schirmer@12854
    35
schirmer@12854
    36
syntax
schirmer@12854
    37
schirmer@12854
    38
  evaln	:: "[prog, state, term,        nat, vals * state] => bool"
schirmer@12854
    39
				("_|-_ -_>-_-> _"   [61,61,80,   61,61] 60)
schirmer@12854
    40
  evarn	:: "[prog, state, var  , vvar        , nat, state] => bool"
schirmer@12854
    41
				("_|-_ -_=>_-_-> _" [61,61,90,61,61,61] 60)
schirmer@12854
    42
  eval_n:: "[prog, state, expr , val         , nat, state] => bool"
schirmer@12854
    43
				("_|-_ -_->_-_-> _" [61,61,80,61,61,61] 60)
schirmer@12854
    44
  evalsn:: "[prog, state, expr list, val list, nat, state] => bool"
schirmer@12854
    45
				("_|-_ -_#>_-_-> _" [61,61,61,61,61,61] 60)
schirmer@12854
    46
  execn	:: "[prog, state, stmt ,               nat, state] => bool"
schirmer@12854
    47
				("_|-_ -_-_-> _"    [61,61,65,   61,61] 60)
schirmer@12854
    48
schirmer@12854
    49
syntax (xsymbols)
schirmer@12854
    50
schirmer@12854
    51
  evaln	:: "[prog, state, term,         nat, vals \<times> state] \<Rightarrow> bool"
schirmer@12854
    52
				("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> _"   [61,61,80,   61,61] 60)
schirmer@12854
    53
  evarn	:: "[prog, state, var  , vvar         , nat, state] \<Rightarrow> bool"
schirmer@12854
    54
				("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
schirmer@12854
    55
  eval_n:: "[prog, state, expr , val ,          nat, state] \<Rightarrow> bool"
schirmer@12854
    56
				("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
schirmer@12854
    57
  evalsn:: "[prog, state, expr list, val  list, nat, state] \<Rightarrow> bool"
schirmer@12854
    58
				("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
schirmer@12854
    59
  execn	:: "[prog, state, stmt ,                nat, state] \<Rightarrow> bool"
schirmer@12854
    60
				("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
schirmer@12854
    61
schirmer@12854
    62
translations
schirmer@12854
    63
schirmer@12854
    64
  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow>  w___s' " == "(s,t,n,w___s') \<in> evaln G"
schirmer@12854
    65
  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow> (w,  s')" <= "(s,t,n,w,  s') \<in> evaln G"
schirmer@12854
    66
  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow> (w,x,s')" <= "(s,t,n,w,x,s') \<in> evaln G"
schirmer@12854
    67
  "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,x,s')"
schirmer@12854
    68
  "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,  s')"
schirmer@12854
    69
  "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,x,s')"
schirmer@12854
    70
  "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,  s')"
schirmer@12854
    71
  "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n\<rightarrow> (In2 vf,x,s')"
schirmer@12854
    72
  "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n\<rightarrow> (In2 vf,  s')"
schirmer@12854
    73
  "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v  \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In3  e\<succ>\<midarrow>n\<rightarrow> (In3 v ,x,s')"
schirmer@12854
    74
  "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v  \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In3  e\<succ>\<midarrow>n\<rightarrow> (In3 v ,  s')"
schirmer@12854
    75
schirmer@12854
    76
schirmer@12854
    77
inductive "evaln G" intros
schirmer@12854
    78
schirmer@13688
    79
--{* propagation of abrupt completion *}
schirmer@12854
    80
schirmer@12854
    81
  Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
schirmer@12854
    82
schirmer@12854
    83
schirmer@13688
    84
--{* evaluation of variables *}
schirmer@12854
    85
schirmer@12854
    86
  LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
schirmer@12854
    87
schirmer@13688
    88
  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2;
schirmer@13688
    89
	  (v,s2') = fvar statDeclC stat fn a s2;
schirmer@13688
    90
          s3 = check_field_access G accC statDeclC fn stat a s2'\<rbrakk> \<Longrightarrow>
schirmer@13688
    91
	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s3"
schirmer@12854
    92
schirmer@12854
    93
  AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n\<rightarrow> s1 ; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n\<rightarrow> s2; 
schirmer@12854
    94
	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
schirmer@12854
    95
	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'"
schirmer@12854
    96
schirmer@12854
    97
schirmer@12854
    98
schirmer@12854
    99
schirmer@13688
   100
--{* evaluation of expressions *}
schirmer@12854
   101
schirmer@12854
   102
  NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
schirmer@12854
   103
	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   104
	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
schirmer@12854
   105
schirmer@12854
   106
  NewA:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<midarrow>n\<rightarrow> s2; 
schirmer@12854
   107
	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
schirmer@12854
   108
	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n\<rightarrow> s3"
schirmer@12854
   109
schirmer@12854
   110
  Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
schirmer@12854
   111
	  s2 = abupd (raise_if (\<not>G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   112
			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
schirmer@12854
   113
schirmer@12854
   114
  Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
schirmer@12854
   115
	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
schirmer@12854
   116
			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
schirmer@12854
   117
schirmer@12854
   118
  Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
schirmer@12854
   119
schirmer@13337
   120
  UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> 
schirmer@13337
   121
         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
schirmer@13337
   122
schirmer@13384
   123
  BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; 
schirmer@13384
   124
           G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
schirmer@13384
   125
            \<succ>\<midarrow>n\<rightarrow> (In1 v2,s2)\<rbrakk> 
schirmer@13337
   126
         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
schirmer@13337
   127
schirmer@12854
   128
  Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
schirmer@12854
   129
schirmer@12854
   130
  Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   131
	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@12854
   132
schirmer@12854
   133
  Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
schirmer@12854
   134
          G\<turnstile>     s1 \<midarrow>e-\<succ>v     \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   135
				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n\<rightarrow> assign f v s2"
schirmer@12854
   136
schirmer@12854
   137
  Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
schirmer@12854
   138
          G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   139
			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
schirmer@12854
   140
schirmer@12854
   141
  Call:	
schirmer@12854
   142
  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2;
schirmer@12854
   143
    D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
schirmer@13688
   144
    s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
schirmer@13688
   145
    s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
schirmer@13688
   146
    G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4
schirmer@13688
   147
   \<rbrakk>
schirmer@12925
   148
   \<Longrightarrow> 
schirmer@13688
   149
    G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s4)"
schirmer@12854
   150
schirmer@12854
   151
  Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   152
				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
schirmer@12854
   153
schirmer@13688
   154
  Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2;
schirmer@13688
   155
          s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>  
schirmer@13688
   156
                         abrupt s2 = Some (Jump (Cont l)))
schirmer@13688
   157
                  then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
schirmer@13688
   158
                  else s2)\<rbrakk>\<Longrightarrow>
schirmer@13337
   159
         G\<turnstile>Norm s0 \<midarrow>Body D c
schirmer@13688
   160
          -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s3"
schirmer@12854
   161
schirmer@13688
   162
--{* evaluation of expression lists *}
schirmer@12854
   163
schirmer@12854
   164
  Nil:
schirmer@12854
   165
				"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
schirmer@12854
   166
schirmer@12854
   167
  Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
schirmer@12854
   168
          G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   169
			     G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
schirmer@12854
   170
schirmer@12854
   171
schirmer@13688
   172
--{* execution of statements *}
schirmer@12854
   173
schirmer@12854
   174
  Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
schirmer@12854
   175
schirmer@12854
   176
  Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   177
				  G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
schirmer@12854
   178
schirmer@12854
   179
  Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@13337
   180
                             G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
schirmer@12854
   181
schirmer@12854
   182
  Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
schirmer@12854
   183
	  G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   184
				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
schirmer@12854
   185
schirmer@12854
   186
  If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
schirmer@12854
   187
	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   188
		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
schirmer@12854
   189
schirmer@12854
   190
  Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
schirmer@13688
   191
	  if the_Bool b 
schirmer@12854
   192
             then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> 
schirmer@12854
   193
                   G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3)
schirmer@12854
   194
	     else s3 = s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   195
			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
schirmer@12854
   196
  
schirmer@13688
   197
  Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
schirmer@12854
   198
  
schirmer@12854
   199
  Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   200
				 G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
schirmer@12854
   201
schirmer@12854
   202
  Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
schirmer@12854
   203
	  if G,s2\<turnstile>catch tn then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 else s3 = s2\<rbrakk>
schirmer@12854
   204
          \<Longrightarrow>
schirmer@12854
   205
		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
schirmer@12854
   206
schirmer@12854
   207
  Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
schirmer@13688
   208
	  G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2;
schirmer@13688
   209
          s3=(if (\<exists> err. x1=Some (Error err)) 
schirmer@13688
   210
              then (x1,s1) 
schirmer@13688
   211
              else abupd (abrupt_if (x1\<noteq>None) x1) s2)\<rbrakk> \<Longrightarrow>
schirmer@13688
   212
              G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
schirmer@12854
   213
  
schirmer@12854
   214
  Init:	"\<lbrakk>the (class G C) = c;
schirmer@12854
   215
	  if inited C (globs s0) then s3 = Norm s0
schirmer@12854
   216
	  else (G\<turnstile>Norm (init_class_obj G C s0)
schirmer@12854
   217
	          \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
schirmer@12854
   218
	        G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
schirmer@12854
   219
                s3 = restore_lvars s1 s2)\<rbrakk>
schirmer@12854
   220
          \<Longrightarrow>
schirmer@12854
   221
		 G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
schirmer@12854
   222
monos
schirmer@12854
   223
  if_def2
schirmer@12854
   224
schirmer@12854
   225
schirmer@12854
   226
declare split_if     [split del] split_if_asm     [split del]
schirmer@12854
   227
        option.split [split del] option.split_asm [split del]
schirmer@13688
   228
        not_None_eq [simp del] 
schirmer@13688
   229
        split_paired_All [simp del] split_paired_Ex [simp del]
schirmer@13688
   230
ML_setup {*
schirmer@13688
   231
simpset_ref() := simpset() delloop "split_all_tac"
schirmer@13688
   232
*}
schirmer@12854
   233
inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   234
schirmer@12854
   235
inductive_cases evaln_elim_cases:
schirmer@12854
   236
	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   237
	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@13688
   238
        "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                   \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   239
        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   240
	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   241
	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   242
	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@13337
   243
        "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@13337
   244
        "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   245
	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   246
	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   247
	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   248
	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   249
	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   250
	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   251
	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   252
	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   253
	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   254
	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   255
	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   256
	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   257
	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   258
	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   259
	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   260
	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   261
	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   262
	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12925
   263
	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   264
	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12925
   265
	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   266
	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@13688
   267
        "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@13688
   268
schirmer@12854
   269
declare split_if     [split] split_if_asm     [split] 
schirmer@12854
   270
        option.split [split] option.split_asm [split]
schirmer@13688
   271
        not_None_eq [simp] 
schirmer@13688
   272
        split_paired_All [simp] split_paired_Ex [simp]
schirmer@13688
   273
ML_setup {*
schirmer@13688
   274
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
schirmer@13688
   275
*}
schirmer@12854
   276
lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
schirmer@12854
   277
  (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
schirmer@12854
   278
  | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
schirmer@12854
   279
apply (erule evaln_cases , auto)
schirmer@12854
   280
apply (induct_tac "t")
schirmer@12854
   281
apply   (induct_tac "a")
schirmer@12854
   282
apply auto
schirmer@12854
   283
done
schirmer@12854
   284
schirmer@13688
   285
text {* The following simplification procedures set up the proper injections of
schirmer@13688
   286
 terms and their corresponding values in the evaluation relation:
schirmer@13688
   287
 E.g. an expression 
schirmer@13688
   288
 (injection @{term In1l} into terms) always evaluates to ordinary values 
schirmer@13688
   289
 (injection @{term In1} into generalised values @{term vals}). 
schirmer@13688
   290
*}
schirmer@13688
   291
schirmer@12854
   292
ML_setup {*
schirmer@12854
   293
fun enf nam inj rhs =
schirmer@12854
   294
let
schirmer@12854
   295
  val name = "evaln_" ^ nam ^ "_eq"
schirmer@12854
   296
  val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<midarrow>n\<rightarrow> (w, s')"
schirmer@12854
   297
  val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
schirmer@12854
   298
	(K [Auto_tac, ALLGOALS (ftac (thm "evaln_Inj_elim")) THEN Auto_tac])
schirmer@12854
   299
  fun is_Inj (Const (inj,_) $ _) = true
schirmer@12854
   300
    | is_Inj _                   = false
schirmer@12854
   301
  fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $ 
schirmer@12854
   302
    (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x
schirmer@12854
   303
in
wenzelm@13462
   304
  cond_simproc name lhs pred (thm name)
schirmer@12854
   305
end;
schirmer@12854
   306
schirmer@12854
   307
val evaln_expr_proc = enf "expr" "In1l" "\<exists>v.  w=In1 v  \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s'";
schirmer@12854
   308
val evaln_var_proc  = enf "var"  "In2"  "\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s'";
schirmer@12854
   309
val evaln_exprs_proc= enf "exprs""In3"  "\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s'";
schirmer@12854
   310
val evaln_stmt_proc = enf "stmt" "In1r" "     w=\<diamondsuit>      \<and> G\<turnstile>s \<midarrow>t     \<midarrow>n\<rightarrow> s'";
schirmer@12854
   311
Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
schirmer@12854
   312
schirmer@12854
   313
bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
schirmer@12854
   314
*}
schirmer@12854
   315
declare evaln_AbruptIs [intro!]
schirmer@12854
   316
schirmer@13337
   317
lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
schirmer@13337
   318
proof -
schirmer@13337
   319
  { fix s t v s'
schirmer@13337
   320
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
schirmer@13337
   321
         normal: "normal s" and
schirmer@13337
   322
         callee: "t=In1l (Callee l e)"
schirmer@13337
   323
    then have "False"
schirmer@13337
   324
    proof (induct)
schirmer@13337
   325
    qed (auto)
schirmer@13337
   326
  }
schirmer@13337
   327
  then show ?thesis
schirmer@13337
   328
    by (cases s') fastsimp 
schirmer@13337
   329
qed
schirmer@13337
   330
schirmer@13337
   331
lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
schirmer@13337
   332
proof -
schirmer@13337
   333
  { fix s t v s'
schirmer@13337
   334
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
schirmer@13337
   335
         normal: "normal s" and
schirmer@13337
   336
         callee: "t=In1l (InsInitE c e)"
schirmer@13337
   337
    then have "False"
schirmer@13337
   338
    proof (induct)
schirmer@13337
   339
    qed (auto)
schirmer@13337
   340
  }
schirmer@13337
   341
  then show ?thesis
schirmer@13337
   342
    by (cases s') fastsimp
schirmer@13337
   343
qed
schirmer@13337
   344
schirmer@13337
   345
lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
schirmer@13337
   346
proof -
schirmer@13337
   347
  { fix s t v s'
schirmer@13337
   348
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
schirmer@13337
   349
         normal: "normal s" and
schirmer@13337
   350
         callee: "t=In2 (InsInitV c w)"
schirmer@13337
   351
    then have "False"
schirmer@13337
   352
    proof (induct)
schirmer@13337
   353
    qed (auto)
schirmer@13337
   354
  }  
schirmer@13337
   355
  then show ?thesis
schirmer@13337
   356
    by (cases s') fastsimp
schirmer@13337
   357
qed
schirmer@13337
   358
schirmer@13337
   359
lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
schirmer@13337
   360
proof -
schirmer@13337
   361
  { fix s t v s'
schirmer@13337
   362
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
schirmer@13337
   363
         normal: "normal s" and
schirmer@13337
   364
         callee: "t=In1r (FinA a c)"
schirmer@13337
   365
    then have "False"
schirmer@13337
   366
    proof (induct)
schirmer@13337
   367
    qed (auto)
schirmer@13337
   368
  } 
schirmer@13337
   369
  then show ?thesis
schirmer@13337
   370
    by (cases s') fastsimp
schirmer@13337
   371
qed
schirmer@13337
   372
schirmer@12854
   373
lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
schirmer@12854
   374
 fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
schirmer@12854
   375
apply (erule evaln_cases , auto)
schirmer@12854
   376
done
schirmer@12854
   377
schirmer@12854
   378
lemma evaln_abrupt: 
schirmer@12854
   379
 "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>  
schirmer@12854
   380
  w=arbitrary3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (arbitrary3 e,(Some xc,s)))"
schirmer@12854
   381
apply auto
schirmer@12854
   382
apply (frule evaln_abrupt_lemma, auto)+
schirmer@12854
   383
done
schirmer@12854
   384
schirmer@12854
   385
ML {*
schirmer@12854
   386
local
wenzelm@12919
   387
  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
schirmer@12854
   388
    | is_Some _ = false
schirmer@12854
   389
  fun pred (_ $ (Const ("Pair",_) $
schirmer@12854
   390
     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
schirmer@12854
   391
       (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x
schirmer@12854
   392
in
schirmer@12854
   393
  val evaln_abrupt_proc = 
wenzelm@13462
   394
 cond_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
schirmer@12854
   395
end;
schirmer@12854
   396
Addsimprocs [evaln_abrupt_proc]
schirmer@12854
   397
*}
schirmer@12854
   398
schirmer@12854
   399
lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
schirmer@12854
   400
apply (case_tac "s", case_tac "a = None")
schirmer@12854
   401
by (auto intro!: evaln.Lit)
schirmer@12854
   402
schirmer@12854
   403
lemma CondI: 
schirmer@12854
   404
 "\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
schirmer@12854
   405
  G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<midarrow>n\<rightarrow> s2"
schirmer@12854
   406
apply (case_tac "s", case_tac "a = None")
schirmer@12854
   407
by (auto intro!: evaln.Cond)
schirmer@12854
   408
schirmer@12854
   409
lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s"
schirmer@12854
   410
apply (case_tac "s", case_tac "a = None")
schirmer@12854
   411
by (auto intro!: evaln.Skip)
schirmer@12854
   412
schirmer@12854
   413
lemma evaln_ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<midarrow>n\<rightarrow> s'"
schirmer@12854
   414
apply (case_tac "s", case_tac "a = None")
schirmer@12854
   415
by (auto intro!: evaln.Expr)
schirmer@12854
   416
schirmer@12854
   417
lemma evaln_CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
schirmer@12854
   418
apply (case_tac "s", case_tac "a = None")
schirmer@12854
   419
by (auto intro!: evaln.Comp)
schirmer@12854
   420
schirmer@12854
   421
lemma evaln_IfI: 
schirmer@12854
   422
 "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
schirmer@12854
   423
  G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2"
schirmer@12854
   424
apply (case_tac "s", case_tac "a = None")
schirmer@12854
   425
by (auto intro!: evaln.If)
schirmer@12854
   426
schirmer@12854
   427
lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s" 
schirmer@12854
   428
by (erule evaln_cases, auto)
schirmer@12854
   429
schirmer@12854
   430
lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')"
schirmer@12854
   431
apply auto
schirmer@12854
   432
done
schirmer@12854
   433
schirmer@13688
   434
schirmer@13688
   435
schirmer@13384
   436
schirmer@13384
   437
section {* evaln implies eval *}
schirmer@13688
   438
schirmer@12925
   439
lemma evaln_eval:  
schirmer@13688
   440
  assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" 
wenzelm@12937
   441
  shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
schirmer@13688
   442
using evaln 
schirmer@13688
   443
proof (induct)
schirmer@13688
   444
  case (Loop b c e l n s0 s1 s2 s3)
schirmer@13688
   445
  have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1".
schirmer@13688
   446
  moreover
schirmer@13688
   447
  have "if the_Bool b
schirmer@13688
   448
        then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2) \<and> 
schirmer@13688
   449
             G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3
schirmer@13688
   450
        else s3 = s1"
schirmer@13688
   451
    using Loop.hyps by simp
schirmer@13688
   452
  ultimately show ?case by (rule eval.Loop)
schirmer@13688
   453
next
schirmer@13688
   454
  case (Try c1 c2 n s0 s1 s2 s3 C vn)
schirmer@13688
   455
  have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1".
schirmer@13688
   456
  moreover
schirmer@13688
   457
  have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2".
schirmer@13688
   458
  moreover
schirmer@13688
   459
  have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
schirmer@13688
   460
    using Try.hyps by simp
schirmer@13688
   461
  ultimately show ?case by (rule eval.Try)
schirmer@13688
   462
next
schirmer@13688
   463
  case (Init C c n s0 s1 s2 s3)
schirmer@13688
   464
  have "the (class G C) = c".
schirmer@13688
   465
  moreover
schirmer@13688
   466
  have "if inited C (globs s0) 
schirmer@13688
   467
           then s3 = Norm s0
schirmer@13688
   468
           else G\<turnstile>Norm ((init_class_obj G C) s0) 
schirmer@13688
   469
                  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
schirmer@13688
   470
                G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2 \<and>
schirmer@13688
   471
                s3 = (set_lvars (locals (store s1))) s2"
schirmer@13688
   472
    using Init.hyps by simp
schirmer@13688
   473
  ultimately show ?case by (rule eval.Init)
schirmer@13688
   474
qed (rule eval.intros,(assumption+ | assumption?))+
schirmer@12925
   475
schirmer@12925
   476
lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
schirmer@12925
   477
apply (frule Suc_le_D)
schirmer@12925
   478
apply fast
schirmer@12925
   479
done
schirmer@12925
   480
schirmer@12925
   481
lemma evaln_nonstrict [rule_format (no_asm), elim]: 
schirmer@12925
   482
  "\<And>ws. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> ws \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> ws"
schirmer@12925
   483
apply (simp (no_asm_simp) only: split_tupled_all)
schirmer@12925
   484
apply (erule evaln.induct)
schirmer@12925
   485
apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
schirmer@12925
   486
  REPEAT o smp_tac 1, 
schirmer@12925
   487
  resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
schirmer@12925
   488
(* 3 subgoals *)
schirmer@12925
   489
apply (auto split del: split_if)
schirmer@12925
   490
done
schirmer@12925
   491
schirmer@12925
   492
lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
schirmer@12925
   493
schirmer@12925
   494
lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2\<rbrakk> \<Longrightarrow> 
schirmer@12925
   495
             G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> ws1 \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> ws2"
schirmer@13688
   496
by (fast intro: le_maxI1 le_maxI2)
schirmer@13688
   497
schirmer@13688
   498
corollary evaln_max2E [consumes 2]:
schirmer@13688
   499
  "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2; 
schirmer@13688
   500
    \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> ws1;G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> ws2 \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
schirmer@13688
   501
by (drule (1) evaln_max2) simp
schirmer@13688
   502
schirmer@12925
   503
schirmer@12925
   504
lemma evaln_max3: 
schirmer@12925
   505
"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2; G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> ws3\<rbrakk> \<Longrightarrow>
schirmer@12925
   506
 G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1 \<and>
schirmer@12925
   507
 G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2 \<and> 
schirmer@12925
   508
 G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3"
schirmer@12925
   509
apply (drule (1) evaln_max2, erule thin_rl)
schirmer@12925
   510
apply (fast intro!: le_maxI1 le_maxI2)
schirmer@12925
   511
done
schirmer@12925
   512
schirmer@13688
   513
corollary evaln_max3E: 
schirmer@13688
   514
"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2; G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> ws3;
schirmer@13688
   515
   \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1;
schirmer@13688
   516
    G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2; 
schirmer@13688
   517
    G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3
schirmer@13688
   518
   \<rbrakk> \<Longrightarrow> P
schirmer@13688
   519
  \<rbrakk> \<Longrightarrow> P"
schirmer@13688
   520
by (drule (2) evaln_max3) simp
schirmer@13688
   521
schirmer@13688
   522
schirmer@12925
   523
lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
schirmer@12925
   524
proof -
schirmer@12925
   525
  have "n2 \<le> max n2 n3"
schirmer@12925
   526
    by (rule le_maxI1)
schirmer@12925
   527
  also
schirmer@12925
   528
  have "max n2 n3 \<le> max n1 (max n2 n3)"
schirmer@12925
   529
    by (rule le_maxI2)
schirmer@12925
   530
  finally
schirmer@12925
   531
  show ?thesis .
schirmer@12925
   532
qed
schirmer@12925
   533
schirmer@12925
   534
lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)"
schirmer@12925
   535
proof -
schirmer@12925
   536
  have "n3 \<le> max n2 n3"
schirmer@12925
   537
    by (rule le_maxI2)
schirmer@12925
   538
  also
schirmer@12925
   539
  have "max n2 n3 \<le> max n1 (max n2 n3)"
schirmer@12925
   540
    by (rule le_maxI2)
schirmer@12925
   541
  finally
schirmer@12925
   542
  show ?thesis .
schirmer@12925
   543
qed
schirmer@12925
   544
schirmer@13688
   545
ML {*
schirmer@13688
   546
Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
schirmer@13688
   547
*}
schirmer@13688
   548
schirmer@13384
   549
section {* eval implies evaln *}
schirmer@12925
   550
lemma eval_evaln: 
schirmer@13688
   551
  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
wenzelm@12937
   552
  shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
schirmer@13688
   553
using eval 
schirmer@13688
   554
proof (induct)
schirmer@13688
   555
  case (Abrupt s t xc)
schirmer@13688
   556
  obtain n where
schirmer@13688
   557
    "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
schirmer@13688
   558
    by (rules intro: evaln.Abrupt)
schirmer@13688
   559
  then show ?case ..
schirmer@13688
   560
next
schirmer@13688
   561
  case Skip
schirmer@13688
   562
  show ?case by (blast intro: evaln.Skip)
schirmer@13688
   563
next
schirmer@13688
   564
  case (Expr e s0 s1 v)
schirmer@13688
   565
  then obtain n where
schirmer@13688
   566
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13688
   567
    by (rules)
schirmer@13688
   568
  then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
schirmer@13688
   569
    by (rule evaln.Expr) 
schirmer@13688
   570
  then show ?case ..
schirmer@13688
   571
next
schirmer@13688
   572
  case (Lab c l s0 s1)
schirmer@13688
   573
  then obtain n where
schirmer@13688
   574
    "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
schirmer@13688
   575
    by (rules)
schirmer@13688
   576
  then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
schirmer@13688
   577
    by (rule evaln.Lab)
schirmer@13688
   578
  then show ?case ..
schirmer@13688
   579
next
schirmer@13688
   580
  case (Comp c1 c2 s0 s1 s2)
schirmer@13688
   581
  then obtain n1 n2 where
schirmer@13688
   582
    "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   583
    "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
schirmer@13688
   584
    by (rules)
schirmer@13688
   585
  then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
schirmer@13688
   586
    by (blast intro: evaln.Comp dest: evaln_max2 )
schirmer@13688
   587
  then show ?case ..
schirmer@13688
   588
next
schirmer@13688
   589
  case (If b c1 c2 e s0 s1 s2)
schirmer@13688
   590
  then obtain n1 n2 where
schirmer@13688
   591
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   592
    "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
schirmer@13688
   593
    by (rules)
schirmer@13688
   594
  then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
schirmer@13688
   595
    by (blast intro: evaln.If dest: evaln_max2)
schirmer@13688
   596
  then show ?case ..
schirmer@13688
   597
next
schirmer@13688
   598
  case (Loop b c e l s0 s1 s2 s3)
schirmer@13688
   599
  from Loop.hyps obtain n1 where
schirmer@13688
   600
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   601
    by (rules)
schirmer@13688
   602
  moreover from Loop.hyps obtain n2 where
schirmer@13688
   603
    "if the_Bool b 
schirmer@13688
   604
        then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
schirmer@13688
   605
              G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
schirmer@13688
   606
	else s3 = s1"
schirmer@13688
   607
    by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
schirmer@13688
   608
  ultimately
schirmer@13688
   609
  have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
schirmer@13688
   610
    apply -
schirmer@13688
   611
    apply (rule evaln.Loop)
schirmer@13688
   612
    apply   (rules intro: evaln_nonstrict intro: le_maxI1)
schirmer@12925
   613
schirmer@13688
   614
    apply   (auto intro: evaln_nonstrict intro: le_maxI2)
schirmer@13688
   615
    done
schirmer@13688
   616
  then show ?case ..
schirmer@13688
   617
next
schirmer@13688
   618
  case (Jmp j s)
schirmer@13688
   619
  have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
schirmer@13688
   620
    by (rule evaln.Jmp)
schirmer@13688
   621
  then show ?case ..
schirmer@13688
   622
next
schirmer@13688
   623
  case (Throw a e s0 s1)
schirmer@13688
   624
  then obtain n where
schirmer@13688
   625
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
schirmer@13688
   626
    by (rules)
schirmer@13688
   627
  then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
schirmer@13688
   628
    by (rule evaln.Throw)
schirmer@13688
   629
  then show ?case ..
schirmer@13688
   630
next 
schirmer@13688
   631
  case (Try catchC c1 c2 s0 s1 s2 s3 vn)
schirmer@13688
   632
  from Try.hyps obtain n1 where
schirmer@13688
   633
    "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   634
    by (rules)
schirmer@13688
   635
  moreover 
schirmer@13688
   636
  have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
schirmer@13688
   637
  moreover
schirmer@13688
   638
  from Try.hyps obtain n2 where
schirmer@13688
   639
    "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
schirmer@13688
   640
    by fastsimp 
schirmer@13688
   641
  ultimately
schirmer@13688
   642
  have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
schirmer@13688
   643
    by (auto intro!: evaln.Try le_maxI1 le_maxI2)
schirmer@13688
   644
  then show ?case ..
schirmer@13688
   645
next
schirmer@13688
   646
  case (Fin c1 c2 s0 s1 s2 s3 x1)
schirmer@13688
   647
  from Fin obtain n1 n2 where 
schirmer@13688
   648
    "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
schirmer@13688
   649
    "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
schirmer@13688
   650
    by rules
schirmer@13688
   651
  moreover
schirmer@13688
   652
  have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
schirmer@13688
   653
                     then (x1, s1)
schirmer@13688
   654
                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
schirmer@13688
   655
  ultimately 
schirmer@13688
   656
  have 
schirmer@13688
   657
    "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3"
schirmer@13688
   658
    by (blast intro: evaln.Fin dest: evaln_max2)
schirmer@13688
   659
  then show ?case ..
schirmer@13688
   660
next
schirmer@13688
   661
  case (Init C c s0 s1 s2 s3)
schirmer@13688
   662
  have     cls: "the (class G C) = c" .
schirmer@13688
   663
  moreover from Init.hyps obtain n where
schirmer@12925
   664
      "if inited C (globs s0) then s3 = Norm s0
schirmer@12925
   665
       else (G\<turnstile>Norm (init_class_obj G C s0)
schirmer@12925
   666
	      \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
schirmer@12925
   667
	           G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
schirmer@12925
   668
                   s3 = restore_lvars s1 s2)"
schirmer@13688
   669
    by (auto intro: evaln_nonstrict le_maxI1 le_maxI2)
schirmer@13688
   670
  ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
schirmer@13688
   671
    by (rule evaln.Init)
schirmer@13688
   672
  then show ?case ..
schirmer@13688
   673
next
schirmer@13688
   674
  case (NewC C a s0 s1 s2)
schirmer@13688
   675
  then obtain n where 
schirmer@13688
   676
    "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
schirmer@13688
   677
    by (rules)
schirmer@13688
   678
  with NewC 
schirmer@13688
   679
  have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
schirmer@13688
   680
    by (rules intro: evaln.NewC)
schirmer@13688
   681
  then show ?case ..
schirmer@13688
   682
next
schirmer@13688
   683
  case (NewA T a e i s0 s1 s2 s3)
schirmer@13688
   684
  then obtain n1 n2 where 
schirmer@13688
   685
    "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   686
    "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
schirmer@13688
   687
    by (rules)
schirmer@13688
   688
  moreover
schirmer@13688
   689
  have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
schirmer@13688
   690
  ultimately
schirmer@13688
   691
  have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
schirmer@13688
   692
    by (blast intro: evaln.NewA dest: evaln_max2)
schirmer@13688
   693
  then show ?case ..
schirmer@13688
   694
next
schirmer@13688
   695
  case (Cast castT e s0 s1 s2 v)
schirmer@13688
   696
  then obtain n where
schirmer@13688
   697
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13688
   698
    by (rules)
schirmer@13688
   699
  moreover 
schirmer@13688
   700
  have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
schirmer@13688
   701
  ultimately
schirmer@13688
   702
  have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
schirmer@13688
   703
    by (rule evaln.Cast)
schirmer@13688
   704
  then show ?case ..
schirmer@13688
   705
next
schirmer@13688
   706
  case (Inst T b e s0 s1 v)
schirmer@13688
   707
  then obtain n where
schirmer@13688
   708
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13688
   709
    by (rules)
schirmer@13688
   710
  moreover 
schirmer@13688
   711
  have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
schirmer@13688
   712
  ultimately
schirmer@13688
   713
  have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
schirmer@13688
   714
    by (rule evaln.Inst)
schirmer@13688
   715
  then show ?case ..
schirmer@13688
   716
next
schirmer@13688
   717
  case (Lit s v)
schirmer@13688
   718
  have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
schirmer@13688
   719
    by (rule evaln.Lit)
schirmer@13688
   720
  then show ?case ..
schirmer@13688
   721
next
schirmer@13688
   722
  case (UnOp e s0 s1 unop v )
schirmer@13688
   723
  then obtain n where
schirmer@13688
   724
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13688
   725
    by (rules)
schirmer@13688
   726
  hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
schirmer@13688
   727
    by (rule evaln.UnOp)
schirmer@13688
   728
  then show ?case ..
schirmer@13688
   729
next
schirmer@13688
   730
  case (BinOp binop e1 e2 s0 s1 s2 v1 v2)
schirmer@13688
   731
  then obtain n1 n2 where 
schirmer@13688
   732
    "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   733
    "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
schirmer@13384
   734
               else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"    
schirmer@13688
   735
    by (rules)
schirmer@13688
   736
  hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
schirmer@13688
   737
          \<rightarrow> s2"
schirmer@13688
   738
    by (blast intro!: evaln.BinOp dest: evaln_max2)
schirmer@13688
   739
  then show ?case ..
schirmer@13688
   740
next
schirmer@13688
   741
  case (Super s )
schirmer@13688
   742
  have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
schirmer@13688
   743
    by (rule evaln.Super)
schirmer@13688
   744
  then show ?case ..
schirmer@13688
   745
next
schirmer@13688
   746
  case (Acc f s0 s1 v va)
schirmer@13688
   747
  then obtain n where
schirmer@13688
   748
    "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
schirmer@13688
   749
    by (rules)
schirmer@13688
   750
  then
schirmer@13688
   751
  have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13688
   752
    by (rule evaln.Acc)
schirmer@13688
   753
  then show ?case ..
schirmer@13688
   754
next
schirmer@13688
   755
  case (Ass e f s0 s1 s2 v var w)
schirmer@13688
   756
  then obtain n1 n2 where 
schirmer@13688
   757
    "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   758
    "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
schirmer@13688
   759
    by (rules)
schirmer@13688
   760
  then
schirmer@13688
   761
  have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
schirmer@13688
   762
    by (blast intro: evaln.Ass dest: evaln_max2)
schirmer@13688
   763
  then show ?case ..
schirmer@13688
   764
next
schirmer@13688
   765
  case (Cond b e0 e1 e2 s0 s1 s2 v)
schirmer@13688
   766
  then obtain n1 n2 where 
schirmer@13688
   767
    "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   768
    "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
schirmer@13688
   769
    by (rules)
schirmer@13688
   770
  then
schirmer@13688
   771
  have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
schirmer@13688
   772
    by (blast intro: evaln.Cond dest: evaln_max2)
schirmer@13688
   773
  then show ?case ..
schirmer@13688
   774
next
schirmer@13688
   775
  case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
schirmer@13688
   776
        v vs)
schirmer@13688
   777
  then obtain n1 n2 where
schirmer@13688
   778
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   779
    "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
schirmer@13688
   780
    by rules
schirmer@13688
   781
  moreover
schirmer@13688
   782
  have "invDeclC = invocation_declclass G mode (store s2) a' statT 
schirmer@13688
   783
                       \<lparr>name=mn,parTs=pTs'\<rparr>" .
schirmer@13688
   784
  moreover
schirmer@13688
   785
  have "s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2" .
schirmer@13688
   786
  moreover
schirmer@13688
   787
  have "s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3".
schirmer@13688
   788
  moreover 
schirmer@13688
   789
  from Call.hyps
schirmer@13688
   790
  obtain m where 
schirmer@13688
   791
    "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
schirmer@13688
   792
    by rules
schirmer@13688
   793
  ultimately
schirmer@13688
   794
  have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
schirmer@12925
   795
            (set_lvars (locals (store s2))) s4"
schirmer@13688
   796
    by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
schirmer@13688
   797
  thus ?case ..
schirmer@13688
   798
next
schirmer@13688
   799
  case (Methd D s0 s1 sig v )
schirmer@13688
   800
  then obtain n where
schirmer@13688
   801
    "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13688
   802
    by rules
schirmer@13688
   803
  then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
schirmer@13688
   804
    by (rule evaln.Methd)
schirmer@13688
   805
  then show ?case ..
schirmer@13688
   806
next
schirmer@13688
   807
  case (Body D c s0 s1 s2 s3 )
schirmer@13688
   808
  from Body.hyps obtain n1 n2 where 
schirmer@13688
   809
    evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
schirmer@13688
   810
    evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
schirmer@13688
   811
    by (rules)
schirmer@13688
   812
  moreover
schirmer@13688
   813
  have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
schirmer@13688
   814
                     fst s2 = Some (Jump (Cont l))
schirmer@13688
   815
                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
schirmer@13688
   816
                 else s2)".
schirmer@13688
   817
  ultimately
schirmer@13688
   818
  have
schirmer@12925
   819
     "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
schirmer@13688
   820
       \<rightarrow> abupd (absorb Ret) s3"
schirmer@13688
   821
    by (rules intro: evaln.Body dest: evaln_max2)
schirmer@13688
   822
  then show ?case ..
schirmer@13688
   823
next
schirmer@13688
   824
  case (LVar s vn )
schirmer@13688
   825
  obtain n where
schirmer@13688
   826
    "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
schirmer@13688
   827
    by (rules intro: evaln.LVar)
schirmer@13688
   828
  then show ?case ..
schirmer@13688
   829
next
schirmer@13688
   830
  case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v)
schirmer@13688
   831
  then obtain n1 n2 where
schirmer@13688
   832
    "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   833
    "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
schirmer@13688
   834
    by rules
schirmer@13688
   835
  moreover
schirmer@13688
   836
  have "s3 = check_field_access G accC statDeclC fn stat a s2'" 
schirmer@13688
   837
       "(v, s2') = fvar statDeclC stat fn a s2" .
schirmer@13688
   838
  ultimately
schirmer@13688
   839
  have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
schirmer@13688
   840
    by (rules intro: evaln.FVar dest: evaln_max2)
schirmer@13688
   841
  then show ?case ..
schirmer@13688
   842
next
schirmer@13688
   843
  case (AVar a e1 e2 i s0 s1 s2 s2' v )
schirmer@13688
   844
  then obtain n1 n2 where 
schirmer@13688
   845
    "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   846
    "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
schirmer@13688
   847
    by rules
schirmer@13688
   848
  moreover 
schirmer@13688
   849
  have "(v, s2') = avar G i a s2" .
schirmer@13688
   850
  ultimately 
schirmer@13688
   851
  have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
schirmer@13688
   852
    by (blast intro!: evaln.AVar dest: evaln_max2)
schirmer@13688
   853
  then show ?case ..
schirmer@13688
   854
next
schirmer@13688
   855
  case (Nil s0)
schirmer@13688
   856
  show ?case by (rules intro: evaln.Nil)
schirmer@13688
   857
next
schirmer@13688
   858
  case (Cons e es s0 s1 s2 v vs)
schirmer@13688
   859
  then obtain n1 n2 where 
schirmer@13688
   860
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   861
    "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
schirmer@13688
   862
    by rules
schirmer@13688
   863
  then
schirmer@13688
   864
  have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
schirmer@13688
   865
    by (blast intro!: evaln.Cons dest: evaln_max2)
schirmer@13688
   866
  then show ?case ..
schirmer@12925
   867
qed
schirmer@13688
   868
       
schirmer@12854
   869
end