src/HOL/Bali/Evaln.thy
author schirmer
Fri Nov 01 13:16:28 2002 +0100 (2002-11-01)
changeset 13690 ac335b2f4a39
parent 13688 a0b16d42d489
child 14674 3506a9af46fc
permissions -rw-r--r--
Inserted some extra paragraphs in large proofs to make tex run...
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@13690
   746
-- {* 
schirmer@13690
   747
\par
schirmer@13690
   748
*} (* dummy text command to break paragraph for latex;
schirmer@13690
   749
              large paragraphs exhaust memory of debian pdflatex *)
schirmer@13688
   750
  case (Acc f s0 s1 v va)
schirmer@13688
   751
  then obtain n where
schirmer@13688
   752
    "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
schirmer@13688
   753
    by (rules)
schirmer@13688
   754
  then
schirmer@13688
   755
  have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13688
   756
    by (rule evaln.Acc)
schirmer@13688
   757
  then show ?case ..
schirmer@13688
   758
next
schirmer@13688
   759
  case (Ass e f s0 s1 s2 v var w)
schirmer@13688
   760
  then obtain n1 n2 where 
schirmer@13688
   761
    "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   762
    "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
schirmer@13688
   763
    by (rules)
schirmer@13688
   764
  then
schirmer@13688
   765
  have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
schirmer@13688
   766
    by (blast intro: evaln.Ass dest: evaln_max2)
schirmer@13688
   767
  then show ?case ..
schirmer@13688
   768
next
schirmer@13688
   769
  case (Cond b e0 e1 e2 s0 s1 s2 v)
schirmer@13688
   770
  then obtain n1 n2 where 
schirmer@13688
   771
    "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   772
    "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
schirmer@13688
   773
    by (rules)
schirmer@13688
   774
  then
schirmer@13688
   775
  have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
schirmer@13688
   776
    by (blast intro: evaln.Cond dest: evaln_max2)
schirmer@13688
   777
  then show ?case ..
schirmer@13688
   778
next
schirmer@13688
   779
  case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
schirmer@13688
   780
        v vs)
schirmer@13688
   781
  then obtain n1 n2 where
schirmer@13688
   782
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   783
    "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
schirmer@13688
   784
    by rules
schirmer@13688
   785
  moreover
schirmer@13688
   786
  have "invDeclC = invocation_declclass G mode (store s2) a' statT 
schirmer@13688
   787
                       \<lparr>name=mn,parTs=pTs'\<rparr>" .
schirmer@13688
   788
  moreover
schirmer@13688
   789
  have "s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2" .
schirmer@13688
   790
  moreover
schirmer@13688
   791
  have "s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3".
schirmer@13688
   792
  moreover 
schirmer@13688
   793
  from Call.hyps
schirmer@13688
   794
  obtain m where 
schirmer@13688
   795
    "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
schirmer@13688
   796
    by rules
schirmer@13688
   797
  ultimately
schirmer@13688
   798
  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
   799
            (set_lvars (locals (store s2))) s4"
schirmer@13688
   800
    by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
schirmer@13688
   801
  thus ?case ..
schirmer@13688
   802
next
schirmer@13688
   803
  case (Methd D s0 s1 sig v )
schirmer@13688
   804
  then obtain n where
schirmer@13688
   805
    "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13688
   806
    by rules
schirmer@13688
   807
  then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
schirmer@13688
   808
    by (rule evaln.Methd)
schirmer@13688
   809
  then show ?case ..
schirmer@13688
   810
next
schirmer@13688
   811
  case (Body D c s0 s1 s2 s3 )
schirmer@13688
   812
  from Body.hyps obtain n1 n2 where 
schirmer@13688
   813
    evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
schirmer@13688
   814
    evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
schirmer@13688
   815
    by (rules)
schirmer@13688
   816
  moreover
schirmer@13688
   817
  have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
schirmer@13688
   818
                     fst s2 = Some (Jump (Cont l))
schirmer@13688
   819
                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
schirmer@13688
   820
                 else s2)".
schirmer@13688
   821
  ultimately
schirmer@13688
   822
  have
schirmer@12925
   823
     "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
schirmer@13688
   824
       \<rightarrow> abupd (absorb Ret) s3"
schirmer@13688
   825
    by (rules intro: evaln.Body dest: evaln_max2)
schirmer@13688
   826
  then show ?case ..
schirmer@13688
   827
next
schirmer@13688
   828
  case (LVar s vn )
schirmer@13688
   829
  obtain n where
schirmer@13688
   830
    "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
schirmer@13688
   831
    by (rules intro: evaln.LVar)
schirmer@13688
   832
  then show ?case ..
schirmer@13688
   833
next
schirmer@13688
   834
  case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v)
schirmer@13688
   835
  then obtain n1 n2 where
schirmer@13688
   836
    "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   837
    "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
schirmer@13688
   838
    by rules
schirmer@13688
   839
  moreover
schirmer@13688
   840
  have "s3 = check_field_access G accC statDeclC fn stat a s2'" 
schirmer@13688
   841
       "(v, s2') = fvar statDeclC stat fn a s2" .
schirmer@13688
   842
  ultimately
schirmer@13688
   843
  have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
schirmer@13688
   844
    by (rules intro: evaln.FVar dest: evaln_max2)
schirmer@13688
   845
  then show ?case ..
schirmer@13688
   846
next
schirmer@13688
   847
  case (AVar a e1 e2 i s0 s1 s2 s2' v )
schirmer@13688
   848
  then obtain n1 n2 where 
schirmer@13688
   849
    "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   850
    "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
schirmer@13688
   851
    by rules
schirmer@13688
   852
  moreover 
schirmer@13688
   853
  have "(v, s2') = avar G i a s2" .
schirmer@13688
   854
  ultimately 
schirmer@13688
   855
  have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
schirmer@13688
   856
    by (blast intro!: evaln.AVar dest: evaln_max2)
schirmer@13688
   857
  then show ?case ..
schirmer@13688
   858
next
schirmer@13688
   859
  case (Nil s0)
schirmer@13688
   860
  show ?case by (rules intro: evaln.Nil)
schirmer@13688
   861
next
schirmer@13688
   862
  case (Cons e es s0 s1 s2 v vs)
schirmer@13688
   863
  then obtain n1 n2 where 
schirmer@13688
   864
    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
schirmer@13688
   865
    "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
schirmer@13688
   866
    by rules
schirmer@13688
   867
  then
schirmer@13688
   868
  have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
schirmer@13688
   869
    by (blast intro!: evaln.Cons dest: evaln_max2)
schirmer@13688
   870
  then show ?case ..
schirmer@12925
   871
qed
schirmer@13688
   872
       
schirmer@12854
   873
end