src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
changeset 10042 7164dc0d24d8
parent 9941 fe05af7ec816
child 10056 9f84ffa4a8d0
     1.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -24,13 +24,13 @@
     1.4  done
     1.5  
     1.6  lemma Load_correct:
     1.7 -"\<lbrakk> wf_prog wt G;
     1.8 +"[| wf_prog wt G;
     1.9     method (G,C) sig = Some (C,rT,maxl,ins); 
    1.10     ins!pc = Load idx; 
    1.11     wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    1.12     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
    1.13 -   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
    1.14 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    1.15 +   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
    1.16 +==> G,phi \<turnstile>JVM state'\<surd>"
    1.17  apply (clarsimp simp add: defs1 map_eq_Cons)
    1.18  apply (rule conjI)
    1.19   apply (rule approx_loc_imp_approx_val_sup)
    1.20 @@ -39,13 +39,13 @@
    1.21  done
    1.22  
    1.23  lemma Store_correct:
    1.24 -"\<lbrakk> wf_prog wt G;
    1.25 +"[| wf_prog wt G;
    1.26    method (G,C) sig = Some (C,rT,maxl,ins);
    1.27    ins!pc = Store idx;
    1.28    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
    1.29    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
    1.30 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
    1.31 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    1.32 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
    1.33 +==> G,phi \<turnstile>JVM state'\<surd>"
    1.34  apply (clarsimp simp add: defs1 map_eq_Cons)
    1.35  apply (rule conjI)
    1.36   apply (blast intro: approx_stk_imp_approx_stk_sup)
    1.37 @@ -54,18 +54,18 @@
    1.38  
    1.39  
    1.40  lemma conf_Intg_Integer [iff]:
    1.41 -  "G,h \<turnstile> Intg i \<Colon>\<preceq> PrimT Integer"
    1.42 +  "G,h \<turnstile> Intg i ::\<preceq> PrimT Integer"
    1.43  by (simp add: conf_def)
    1.44  
    1.45  
    1.46  lemma Bipush_correct:
    1.47 -"\<lbrakk> wf_prog wt G;
    1.48 +"[| wf_prog wt G;
    1.49    method (G,C) sig = Some (C,rT,maxl,ins); 
    1.50    ins!pc = Bipush i; 
    1.51    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    1.52    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
    1.53 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
    1.54 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    1.55 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
    1.56 +==> G,phi \<turnstile>JVM state'\<surd>"
    1.57  apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
    1.58  apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
    1.59  done
    1.60 @@ -73,7 +73,7 @@
    1.61  lemma NT_subtype_conv:
    1.62    "G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))"
    1.63  proof -
    1.64 -  have "\<And>T T'. G \<turnstile> T' \<preceq> T \<Longrightarrow> T' = NT \<longrightarrow> (T=NT | (\<exists>C. T = Class C))"
    1.65 +  have "!!T T'. G \<turnstile> T' \<preceq> T ==> T' = NT --> (T=NT | (\<exists>C. T = Class C))"
    1.66      apply (erule widen.induct)
    1.67      apply auto
    1.68      apply (case_tac R)
    1.69 @@ -86,13 +86,13 @@
    1.70  qed
    1.71  
    1.72  lemma Aconst_null_correct:
    1.73 -"\<lbrakk> wf_prog wt G;
    1.74 +"[| wf_prog wt G;
    1.75    method (G,C) sig = Some (C,rT,maxl,ins); 
    1.76    ins!pc =  Aconst_null; 
    1.77    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    1.78    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
    1.79 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
    1.80 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
    1.81 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
    1.82 +==> G,phi \<turnstile>JVM state'\<surd>"
    1.83  apply (clarsimp simp add: defs1 map_eq_Cons)
    1.84  apply (rule conjI)
    1.85   apply (force simp add: approx_val_Null NT_subtype_conv)
    1.86 @@ -101,8 +101,8 @@
    1.87  
    1.88  
    1.89  lemma Cast_conf2:
    1.90 -  "\<lbrakk>wf_prog ok G; G,h\<turnstile>v\<Colon>\<preceq>RefT rt; cast_ok G C h v; G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk> 
    1.91 -  \<Longrightarrow> G,h\<turnstile>v\<Colon>\<preceq>T"
    1.92 +  "[|wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; G\<turnstile>Class C\<preceq>T; is_class G C|] 
    1.93 +  ==> G,h\<turnstile>v::\<preceq>T"
    1.94  apply (unfold cast_ok_def)
    1.95  apply (frule widen_Class)
    1.96  apply (elim exE disjE)
    1.97 @@ -114,26 +114,26 @@
    1.98  
    1.99  
   1.100  lemma Checkcast_correct:
   1.101 -"\<lbrakk> wf_prog wt G;
   1.102 +"[| wf_prog wt G;
   1.103    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.104    ins!pc = Checkcast D; 
   1.105    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.106    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.107 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.108 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.109 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.110 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.111  apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
   1.112  apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2)
   1.113  done
   1.114  
   1.115  
   1.116  lemma Getfield_correct:
   1.117 -"\<lbrakk> wf_prog wt G;
   1.118 +"[| wf_prog wt G;
   1.119    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.120    ins!pc = Getfield F D; 
   1.121    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.122    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.123 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.124 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.125 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.126 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.127  apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split)
   1.128  apply (frule conf_widen)
   1.129  apply assumption+
   1.130 @@ -147,13 +147,13 @@
   1.131  done
   1.132  
   1.133  lemma Putfield_correct:
   1.134 -"\<lbrakk> wf_prog wt G;
   1.135 +"[| wf_prog wt G;
   1.136    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.137    ins!pc = Putfield F D; 
   1.138    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.139    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.140 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.141 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.142 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.143 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.144  apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split)
   1.145  apply (clarsimp simp add: approx_val_def)
   1.146  apply (frule conf_widen)
   1.147 @@ -174,13 +174,13 @@
   1.148    by fast
   1.149  
   1.150  lemma New_correct:
   1.151 -"\<lbrakk> wf_prog wt G;
   1.152 +"[| wf_prog wt G;
   1.153    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.154    ins!pc = New cl_idx; 
   1.155    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.156    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.157 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.158 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.159 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.160 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.161  apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def
   1.162  		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
   1.163         split: option.split)
   1.164 @@ -199,13 +199,13 @@
   1.165  lemmas [simp del] = split_paired_Ex
   1.166  
   1.167  lemma Invoke_correct:
   1.168 -"\<lbrakk> wt_jvm_prog G phi; 
   1.169 +"[| wt_jvm_prog G phi; 
   1.170    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.171    ins ! pc = Invoke C' mn pTs; 
   1.172    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.173    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.174 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.175 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
   1.176 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.177 +==> G,phi \<turnstile>JVM state'\<surd>" 
   1.178  proof -
   1.179    assume wtprog: "wt_jvm_prog G phi"
   1.180    assume method: "method (G,C) sig = Some (C,rT,maxl,ins)"
   1.181 @@ -282,7 +282,7 @@
   1.182      by simp
   1.183  
   1.184    with state' method ins 
   1.185 -  have Null_ok: "oX = Null \<Longrightarrow> ?thesis"
   1.186 +  have Null_ok: "oX = Null ==> ?thesis"
   1.187      by (simp add: correct_state_def raise_xcpt_def)
   1.188    
   1.189    { fix ref
   1.190 @@ -434,13 +434,13 @@
   1.191  lemmas [simp del] = map_append
   1.192  
   1.193  lemma Return_correct:
   1.194 -"\<lbrakk> wt_jvm_prog G phi;  
   1.195 +"[| wt_jvm_prog G phi;  
   1.196    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.197    ins ! pc = Return; 
   1.198    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.199    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.200 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.201 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.202 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.203 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.204  apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm)
   1.205  apply (frule wt_jvm_prog_impl_wt_instr)
   1.206  apply (assumption, erule Suc_lessD)
   1.207 @@ -455,102 +455,102 @@
   1.208  lemmas [simp] = map_append
   1.209  
   1.210  lemma Goto_correct:
   1.211 -"\<lbrakk> wf_prog wt G; 
   1.212 +"[| wf_prog wt G; 
   1.213    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.214    ins ! pc = Goto branch; 
   1.215    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.216    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.217 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.218 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.219 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.220 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.221  apply (clarsimp simp add: defs1)
   1.222  apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
   1.223  done
   1.224  
   1.225  
   1.226  lemma Ifcmpeq_correct:
   1.227 -"\<lbrakk> wf_prog wt G; 
   1.228 +"[| wf_prog wt G; 
   1.229    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.230    ins ! pc = Ifcmpeq branch; 
   1.231    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.232    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.233 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.234 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.235 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.236 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.237  apply (clarsimp simp add: defs1)
   1.238  apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
   1.239  done
   1.240  
   1.241  lemma Pop_correct:
   1.242 -"\<lbrakk> wf_prog wt G; 
   1.243 +"[| wf_prog wt G; 
   1.244    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.245    ins ! pc = Pop;
   1.246    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.247    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.248 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.249 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.250 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.251 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.252  apply (clarsimp simp add: defs1)
   1.253  apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
   1.254  done
   1.255  
   1.256  lemma Dup_correct:
   1.257 -"\<lbrakk> wf_prog wt G; 
   1.258 +"[| wf_prog wt G; 
   1.259    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.260    ins ! pc = Dup;
   1.261    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.262    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.263 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.264 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.265 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.266 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.267  apply (clarsimp simp add: defs1 map_eq_Cons)
   1.268  apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   1.269               simp add: defs1 map_eq_Cons)
   1.270  done
   1.271  
   1.272  lemma Dup_x1_correct:
   1.273 -"\<lbrakk> wf_prog wt G; 
   1.274 +"[| wf_prog wt G; 
   1.275    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.276    ins ! pc = Dup_x1;
   1.277    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.278    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.279 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.280 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.281 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.282 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.283  apply (clarsimp simp add: defs1 map_eq_Cons)
   1.284  apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   1.285               simp add: defs1 map_eq_Cons)
   1.286  done
   1.287  
   1.288  lemma Dup_x2_correct:
   1.289 -"\<lbrakk> wf_prog wt G; 
   1.290 +"[| wf_prog wt G; 
   1.291    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.292    ins ! pc = Dup_x2;
   1.293    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.294    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.295 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.296 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.297 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.298 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.299  apply (clarsimp simp add: defs1 map_eq_Cons)
   1.300  apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   1.301               simp add: defs1 map_eq_Cons)
   1.302  done
   1.303  
   1.304  lemma Swap_correct:
   1.305 -"\<lbrakk> wf_prog wt G; 
   1.306 +"[| wf_prog wt G; 
   1.307    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.308    ins ! pc = Swap;
   1.309    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.310    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.311 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.312 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.313 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.314 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.315  apply (clarsimp simp add: defs1 map_eq_Cons)
   1.316  apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   1.317               simp add: defs1 map_eq_Cons)
   1.318  done
   1.319  
   1.320  lemma IAdd_correct:
   1.321 -"\<lbrakk> wf_prog wt G; 
   1.322 +"[| wf_prog wt G; 
   1.323    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.324    ins ! pc = IAdd; 
   1.325    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.326    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.327 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.328 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.329 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.330 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.331  apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
   1.332  apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup)
   1.333  done
   1.334 @@ -559,11 +559,11 @@
   1.335  (** instr correct **)
   1.336  
   1.337  lemma instr_correct:
   1.338 -"\<lbrakk> wt_jvm_prog G phi; 
   1.339 +"[| wt_jvm_prog G phi; 
   1.340    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.341    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
   1.342 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
   1.343 -\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.344 +  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.345 +==> G,phi \<turnstile>JVM state'\<surd>"
   1.346  apply (frule wt_jvm_prog_impl_wt_instr_cor)
   1.347  apply assumption+
   1.348  apply (cases "ins!pc")
   1.349 @@ -583,13 +583,13 @@
   1.350  
   1.351  lemma correct_state_impl_Some_method:
   1.352    "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
   1.353 -  \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
   1.354 +  ==> \<exists>meth. method (G,C) sig = Some(C,meth)"
   1.355  by (auto simp add: correct_state_def Let_def)
   1.356  
   1.357  
   1.358  lemma BV_correct_1 [rule_format]:
   1.359 -"\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> 
   1.360 - \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   1.361 +"!!state. [| wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>|] 
   1.362 + ==> exec (G,state) = Some state' --> G,phi \<turnstile>JVM state'\<surd>"
   1.363  apply (simp only: split_tupled_all)
   1.364  apply (rename_tac xp hp frs)
   1.365  apply (case_tac xp)
   1.366 @@ -605,12 +605,12 @@
   1.367  
   1.368  
   1.369  lemma L0:
   1.370 -  "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
   1.371 +  "[| xp=None; frs\<noteq>[] |] ==> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
   1.372  by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex)
   1.373  
   1.374  lemma L1:
   1.375 -  "\<lbrakk>wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]\<rbrakk> 
   1.376 -  \<Longrightarrow> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
   1.377 +  "[|wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]|] 
   1.378 +  ==> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
   1.379  apply (drule L0)
   1.380  apply assumption
   1.381  apply (fast intro: BV_correct_1)
   1.382 @@ -618,7 +618,7 @@
   1.383  
   1.384  
   1.385  theorem BV_correct [rule_format]:
   1.386 -"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>"
   1.387 +"[| wt_jvm_prog G phi; G \<turnstile> s -jvm-> t |] ==> G,phi \<turnstile>JVM s\<surd> --> G,phi \<turnstile>JVM t\<surd>"
   1.388  apply (unfold exec_all_def)
   1.389  apply (erule rtrancl_induct)
   1.390   apply simp
   1.391 @@ -627,8 +627,8 @@
   1.392  
   1.393  
   1.394  theorem BV_correct_initial:
   1.395 -"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> 
   1.396 - \<Longrightarrow>  approx_stk G hp stk (fst (the (((phi  C)  sig) ! pc))) \<and> approx_loc G hp loc (snd (the (((phi  C)  sig) ! pc)))"
   1.397 +"[| wt_jvm_prog G phi; G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|] 
   1.398 + ==>  approx_stk G hp stk (fst (the (((phi  C)  sig) ! pc))) \<and> approx_loc G hp loc (snd (the (((phi  C)  sig) ! pc)))"
   1.399  apply (drule BV_correct)
   1.400  apply assumption+
   1.401  apply (simp add: correct_state_def correct_frame_def split_def split: option.splits)