src/HOL/Bali/Evaln.thy
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Jan 28 17:00:19 2002 +0100
     1.3 @@ -0,0 +1,373 @@
     1.4 +(*  Title:      isabelle/Bali/Evaln.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1999 Technische Universitaet Muenchen
     1.8 +*)
     1.9 +header {* Operational evaluation (big-step) semantics of Java expressions and 
    1.10 +          statements
    1.11 +*}
    1.12 +
    1.13 +theory Evaln = Eval:
    1.14 +
    1.15 +text {*
    1.16 +Variant of eval relation with counter for bounded recursive depth
    1.17 +Evaln could completely replace Eval.
    1.18 +*}
    1.19 +
    1.20 +consts
    1.21 +
    1.22 +  evaln	:: "prog \<Rightarrow> (state \<times> term \<times> nat \<times> vals \<times> state) set"
    1.23 +
    1.24 +syntax
    1.25 +
    1.26 +  evaln	:: "[prog, state, term,        nat, vals * state] => bool"
    1.27 +				("_|-_ -_>-_-> _"   [61,61,80,   61,61] 60)
    1.28 +  evarn	:: "[prog, state, var  , vvar        , nat, state] => bool"
    1.29 +				("_|-_ -_=>_-_-> _" [61,61,90,61,61,61] 60)
    1.30 +  eval_n:: "[prog, state, expr , val         , nat, state] => bool"
    1.31 +				("_|-_ -_->_-_-> _" [61,61,80,61,61,61] 60)
    1.32 +  evalsn:: "[prog, state, expr list, val list, nat, state] => bool"
    1.33 +				("_|-_ -_#>_-_-> _" [61,61,61,61,61,61] 60)
    1.34 +  execn	:: "[prog, state, stmt ,               nat, state] => bool"
    1.35 +				("_|-_ -_-_-> _"    [61,61,65,   61,61] 60)
    1.36 +
    1.37 +syntax (xsymbols)
    1.38 +
    1.39 +  evaln	:: "[prog, state, term,         nat, vals \<times> state] \<Rightarrow> bool"
    1.40 +				("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> _"   [61,61,80,   61,61] 60)
    1.41 +  evarn	:: "[prog, state, var  , vvar         , nat, state] \<Rightarrow> bool"
    1.42 +				("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
    1.43 +  eval_n:: "[prog, state, expr , val ,          nat, state] \<Rightarrow> bool"
    1.44 +				("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
    1.45 +  evalsn:: "[prog, state, expr list, val  list, nat, state] \<Rightarrow> bool"
    1.46 +				("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
    1.47 +  execn	:: "[prog, state, stmt ,                nat, state] \<Rightarrow> bool"
    1.48 +				("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
    1.49 +
    1.50 +translations
    1.51 +
    1.52 +  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow>  w___s' " == "(s,t,n,w___s') \<in> evaln G"
    1.53 +  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow> (w,  s')" <= "(s,t,n,w,  s') \<in> evaln G"
    1.54 +  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow> (w,x,s')" <= "(s,t,n,w,x,s') \<in> evaln G"
    1.55 +  "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,x,s')"
    1.56 +  "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,  s')"
    1.57 +  "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')"
    1.58 +  "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,  s')"
    1.59 +  "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')"
    1.60 +  "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n\<rightarrow> (In2 vf,  s')"
    1.61 +  "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')"
    1.62 +  "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')"
    1.63 +
    1.64 +
    1.65 +inductive "evaln G" intros
    1.66 +
    1.67 +(* propagation of abrupt completion *)
    1.68 +
    1.69 +  Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
    1.70 +
    1.71 +
    1.72 +(* evaluation of variables *)
    1.73 +
    1.74 +  LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
    1.75 +
    1.76 +  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s2;
    1.77 +	  (v,s2') = fvar C stat fn a' s2\<rbrakk> \<Longrightarrow>
    1.78 +	  G\<turnstile>Norm s0 \<midarrow>{C,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s2'"
    1.79 +
    1.80 +  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; 
    1.81 +	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
    1.82 +	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'"
    1.83 +
    1.84 +
    1.85 +
    1.86 +
    1.87 +(* evaluation of expressions *)
    1.88 +
    1.89 +  NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
    1.90 +	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
    1.91 +	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
    1.92 +
    1.93 +  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; 
    1.94 +	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
    1.95 +	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n\<rightarrow> s3"
    1.96 +
    1.97 +  Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
    1.98 +	  s2 = abupd (raise_if (\<not>G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
    1.99 +			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
   1.100 +
   1.101 +  Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
   1.102 +	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
   1.103 +			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
   1.104 +
   1.105 +  Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
   1.106 +
   1.107 +  Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
   1.108 +
   1.109 +  Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.110 +	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.111 +
   1.112 +  Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
   1.113 +          G\<turnstile>     s1 \<midarrow>e-\<succ>v     \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.114 +				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n\<rightarrow> assign f v s2"
   1.115 +
   1.116 +  Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
   1.117 +          G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.118 +			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
   1.119 +
   1.120 +  Call:	
   1.121 +  "\<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;
   1.122 +    D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
   1.123 +    G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2
   1.124 +            \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s3\<rbrakk>
   1.125 +   \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>{statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s3)"
   1.126 +
   1.127 +  Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.128 +				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
   1.129 +
   1.130 +  Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2\<rbrakk>\<Longrightarrow>
   1.131 + G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
   1.132 +
   1.133 +(* evaluation of expression lists *)
   1.134 +
   1.135 +  Nil:
   1.136 +				"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
   1.137 +
   1.138 +  Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
   1.139 +          G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.140 +			     G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
   1.141 +
   1.142 +
   1.143 +(* execution of statements *)
   1.144 +
   1.145 +  Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
   1.146 +
   1.147 +  Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.148 +				  G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
   1.149 +
   1.150 +  Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.151 +                             G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb (Break l)) s1"
   1.152 +
   1.153 +  Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
   1.154 +	  G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.155 +				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
   1.156 +
   1.157 +  If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   1.158 +	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.159 +		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
   1.160 +
   1.161 +  Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   1.162 +	  if normal s1 \<and> the_Bool b 
   1.163 +             then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> 
   1.164 +                   G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3)
   1.165 +	     else s3 = s1\<rbrakk> \<Longrightarrow>
   1.166 +			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
   1.167 +  
   1.168 +  Do: "G\<turnstile>Norm s \<midarrow>Do j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
   1.169 +  
   1.170 +  Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.171 +				 G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
   1.172 +
   1.173 +  Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
   1.174 +	  if G,s2\<turnstile>catch tn then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 else s3 = s2\<rbrakk>
   1.175 +          \<Longrightarrow>
   1.176 +		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
   1.177 +
   1.178 +  Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
   1.179 +	  G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.180 +              G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
   1.181 +  
   1.182 +  Init:	"\<lbrakk>the (class G C) = c;
   1.183 +	  if inited C (globs s0) then s3 = Norm s0
   1.184 +	  else (G\<turnstile>Norm (init_class_obj G C s0)
   1.185 +	          \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
   1.186 +	        G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
   1.187 +                s3 = restore_lvars s1 s2)\<rbrakk>
   1.188 +          \<Longrightarrow>
   1.189 +		 G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
   1.190 +monos
   1.191 +  if_def2
   1.192 +
   1.193 +lemma evaln_eval: "\<And>ws. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> ws \<Longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws"
   1.194 +apply (simp (no_asm_simp) only: split_tupled_all)
   1.195 +apply (erule evaln.induct)
   1.196 +apply (rule eval.intros, (assumption+)?,(force split del: split_if)?)+
   1.197 +done
   1.198 +
   1.199 +
   1.200 +lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
   1.201 +apply (frule Suc_le_D)
   1.202 +apply fast
   1.203 +done
   1.204 +
   1.205 +lemma evaln_nonstrict [rule_format (no_asm), elim]: 
   1.206 +  "\<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"
   1.207 +apply (simp (no_asm_simp) only: split_tupled_all)
   1.208 +apply (erule evaln.induct)
   1.209 +apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
   1.210 +  REPEAT o smp_tac 1, 
   1.211 +  resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
   1.212 +(* 3 subgoals *)
   1.213 +apply (auto split del: split_if)
   1.214 +done
   1.215 +
   1.216 +lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
   1.217 +
   1.218 +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> 
   1.219 +             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"
   1.220 +apply (fast intro: le_maxI1 le_maxI2)
   1.221 +done
   1.222 +
   1.223 +lemma evaln_max3: 
   1.224 +"\<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>
   1.225 + G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1 \<and>
   1.226 + G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2 \<and> 
   1.227 + G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3"
   1.228 +apply (drule (1) evaln_max2, erule thin_rl)
   1.229 +apply (fast intro!: le_maxI1 le_maxI2)
   1.230 +done
   1.231 +
   1.232 +lemma eval_evaln: "\<And>ws. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<exists>n. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> ws)"
   1.233 +apply (simp (no_asm_simp) only: split_tupled_all)
   1.234 +apply (erule eval.induct)
   1.235 +apply (tactic {* ALLGOALS 
   1.236 +         (asm_full_simp_tac (HOL_basic_ss addsplits [split_if_asm])) *})
   1.237 +apply (tactic {* ALLGOALS (EVERY'[
   1.238 +   REPEAT o eresolve_tac [exE, conjE], rtac exI,
   1.239 +                     TRY o datac (thm "evaln_max3") 2, REPEAT o etac conjE,
   1.240 +  resolve_tac (thms "evaln.intros") THEN_ALL_NEW 
   1.241 +  force_tac (HOL_cs, HOL_ss)]) *})
   1.242 +done
   1.243 +
   1.244 +declare split_if     [split del] split_if_asm     [split del]
   1.245 +        option.split [split del] option.split_asm [split del]
   1.246 +inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'"
   1.247 +
   1.248 +inductive_cases evaln_elim_cases:
   1.249 +	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> vs'"
   1.250 +	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> xs'"
   1.251 +        "G\<turnstile>Norm s \<midarrow>In1r (Do j)                    \<succ>\<midarrow>n\<rightarrow> xs'"
   1.252 +        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> xs'"
   1.253 +	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> vs'"
   1.254 +	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> vs'"
   1.255 +	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> vs'"
   1.256 +	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> vs'"
   1.257 +	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> vs'"
   1.258 +	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> vs'"
   1.259 +	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> vs'"
   1.260 +	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> vs'"
   1.261 +	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> xs'"
   1.262 +	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> xs'"
   1.263 +	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> xs'"
   1.264 +	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n\<rightarrow> xs'"
   1.265 +	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> vs'"
   1.266 +	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> xs'"
   1.267 +	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<midarrow>n\<rightarrow> xs'"
   1.268 +	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> xs'"
   1.269 +	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> xs'"
   1.270 +	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> vs'"
   1.271 +	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> vs'"
   1.272 +	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> vs'"
   1.273 +	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> xs'"
   1.274 +	"G\<turnstile>Norm s \<midarrow>In2  ({C,stat}e..fn)           \<succ>\<midarrow>n\<rightarrow> vs'"
   1.275 +	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> vs'"
   1.276 +	"G\<turnstile>Norm s \<midarrow>In1l ({statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> vs'"
   1.277 +	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> xs'"
   1.278 +declare split_if     [split] split_if_asm     [split] 
   1.279 +        option.split [split] option.split_asm [split]
   1.280 +
   1.281 +lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
   1.282 +  (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
   1.283 +  | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
   1.284 +apply (erule evaln_cases , auto)
   1.285 +apply (induct_tac "t")
   1.286 +apply   (induct_tac "a")
   1.287 +apply auto
   1.288 +done
   1.289 +
   1.290 +ML_setup {*
   1.291 +fun enf nam inj rhs =
   1.292 +let
   1.293 +  val name = "evaln_" ^ nam ^ "_eq"
   1.294 +  val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<midarrow>n\<rightarrow> (w, s')"
   1.295 +  val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   1.296 +	(K [Auto_tac, ALLGOALS (ftac (thm "evaln_Inj_elim")) THEN Auto_tac])
   1.297 +  fun is_Inj (Const (inj,_) $ _) = true
   1.298 +    | is_Inj _                   = false
   1.299 +  fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $ 
   1.300 +    (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x
   1.301 +in
   1.302 +  make_simproc name lhs pred (thm name)
   1.303 +end;
   1.304 +
   1.305 +val evaln_expr_proc = enf "expr" "In1l" "\<exists>v.  w=In1 v  \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s'";
   1.306 +val evaln_var_proc  = enf "var"  "In2"  "\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s'";
   1.307 +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'";
   1.308 +val evaln_stmt_proc = enf "stmt" "In1r" "     w=\<diamondsuit>      \<and> G\<turnstile>s \<midarrow>t     \<midarrow>n\<rightarrow> s'";
   1.309 +Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
   1.310 +
   1.311 +bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
   1.312 +*}
   1.313 +declare evaln_AbruptIs [intro!]
   1.314 +
   1.315 +lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
   1.316 + fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
   1.317 +apply (erule evaln_cases , auto)
   1.318 +done
   1.319 +
   1.320 +lemma evaln_abrupt: 
   1.321 + "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>  
   1.322 +  w=arbitrary3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (arbitrary3 e,(Some xc,s)))"
   1.323 +apply auto
   1.324 +apply (frule evaln_abrupt_lemma, auto)+
   1.325 +done
   1.326 +
   1.327 +ML {*
   1.328 +local
   1.329 +  fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
   1.330 +    | is_Some _ = false
   1.331 +  fun pred (_ $ (Const ("Pair",_) $
   1.332 +     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   1.333 +       (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x
   1.334 +in
   1.335 +  val evaln_abrupt_proc = 
   1.336 + make_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
   1.337 +end;
   1.338 +Addsimprocs [evaln_abrupt_proc]
   1.339 +*}
   1.340 +
   1.341 +lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
   1.342 +apply (case_tac "s", case_tac "a = None")
   1.343 +by (auto intro!: evaln.Lit)
   1.344 +
   1.345 +lemma CondI: 
   1.346 + "\<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> 
   1.347 +  G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<midarrow>n\<rightarrow> s2"
   1.348 +apply (case_tac "s", case_tac "a = None")
   1.349 +by (auto intro!: evaln.Cond)
   1.350 +
   1.351 +lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s"
   1.352 +apply (case_tac "s", case_tac "a = None")
   1.353 +by (auto intro!: evaln.Skip)
   1.354 +
   1.355 +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'"
   1.356 +apply (case_tac "s", case_tac "a = None")
   1.357 +by (auto intro!: evaln.Expr)
   1.358 +
   1.359 +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"
   1.360 +apply (case_tac "s", case_tac "a = None")
   1.361 +by (auto intro!: evaln.Comp)
   1.362 +
   1.363 +lemma evaln_IfI: 
   1.364 + "\<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> 
   1.365 +  G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2"
   1.366 +apply (case_tac "s", case_tac "a = None")
   1.367 +by (auto intro!: evaln.If)
   1.368 +
   1.369 +lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s" 
   1.370 +by (erule evaln_cases, auto)
   1.371 +
   1.372 +lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')"
   1.373 +apply auto
   1.374 +done
   1.375 +
   1.376 +end