tuned spacing for document generation
authorkleing
Thu Sep 21 19:25:57 2000 +0200 (2000-09-21)
changeset 100569f84ffa4a8d0
parent 10055 2264bdd8becc
child 10057 8c8d2d0d3ef8
tuned spacing for document generation
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/BV/Convert.thy
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/J/Eval.thy
src/HOL/MicroJava/JVM/JVMExecInstr.thy
     1.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Sep 21 18:58:25 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Sep 21 19:25:57 2000 +0200
     1.3 @@ -7,11 +7,13 @@
     1.4  programs.
     1.5  *)
     1.6  
     1.7 -header "Type Safety Proof"
     1.8 +header "BV Type Safety Proof"
     1.9  
    1.10  theory BVSpecTypeSafe = Correct:
    1.11  
    1.12 -lemmas defs1 = sup_state_def correct_state_def correct_frame_def wt_instr_def step_def
    1.13 +lemmas defs1 = sup_state_def correct_state_def correct_frame_def 
    1.14 +               wt_instr_def step_def
    1.15 +
    1.16  lemmas [simp del] = split_paired_All
    1.17  
    1.18  lemma wt_jvm_prog_impl_wt_instr_cor:
    1.19 @@ -25,17 +27,18 @@
    1.20  
    1.21  lemma Load_correct:
    1.22  "[| wf_prog wt G;
    1.23 -   method (G,C) sig = Some (C,rT,maxl,ins); 
    1.24 -   ins!pc = Load idx; 
    1.25 -   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    1.26 -   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
    1.27 -   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
    1.28 +    method (G,C) sig = Some (C,rT,maxl,ins); 
    1.29 +    ins!pc = Load idx; 
    1.30 +    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    1.31 +    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
    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 (rule approx_loc_imp_approx_val_sup)
    1.37   apply simp+
    1.38 -apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
    1.39 +apply (blast intro: approx_stk_imp_approx_stk_sup 
    1.40 +                    approx_loc_imp_approx_loc_sup)
    1.41  done
    1.42  
    1.43  lemma Store_correct:
    1.44 @@ -49,7 +52,8 @@
    1.45  apply (clarsimp simp add: defs1 map_eq_Cons)
    1.46  apply (rule conjI)
    1.47   apply (blast intro: approx_stk_imp_approx_stk_sup)
    1.48 -apply (blast intro: approx_loc_imp_approx_loc_subst approx_loc_imp_approx_loc_sup)
    1.49 +apply (blast intro: approx_loc_imp_approx_loc_subst 
    1.50 +                    approx_loc_imp_approx_loc_sup)
    1.51  done
    1.52  
    1.53  
    1.54 @@ -60,14 +64,15 @@
    1.55  
    1.56  lemma Bipush_correct:
    1.57  "[| wf_prog wt G;
    1.58 -  method (G,C) sig = Some (C,rT,maxl,ins); 
    1.59 -  ins!pc = Bipush i; 
    1.60 -  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    1.61 -  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
    1.62 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
    1.63 +    method (G,C) sig = Some (C,rT,maxl,ins); 
    1.64 +    ins!pc = Bipush i; 
    1.65 +    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    1.66 +    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
    1.67 +    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
    1.68  ==> G,phi \<turnstile>JVM state'\<surd>"
    1.69  apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
    1.70 -apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
    1.71 +apply (blast intro: approx_stk_imp_approx_stk_sup 
    1.72 +                    approx_loc_imp_approx_loc_sup)
    1.73  done
    1.74  
    1.75  lemma NT_subtype_conv:
    1.76 @@ -87,21 +92,23 @@
    1.77  
    1.78  lemma Aconst_null_correct:
    1.79  "[| wf_prog wt G;
    1.80 -  method (G,C) sig = Some (C,rT,maxl,ins); 
    1.81 -  ins!pc =  Aconst_null; 
    1.82 -  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    1.83 -  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
    1.84 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
    1.85 +    method (G,C) sig = Some (C,rT,maxl,ins); 
    1.86 +    ins!pc =  Aconst_null; 
    1.87 +    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
    1.88 +    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
    1.89 +    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
    1.90  ==> G,phi \<turnstile>JVM state'\<surd>"
    1.91  apply (clarsimp simp add: defs1 map_eq_Cons)
    1.92  apply (rule conjI)
    1.93   apply (force simp add: approx_val_Null NT_subtype_conv)
    1.94 -apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
    1.95 +apply (blast intro: approx_stk_imp_approx_stk_sup 
    1.96 +                    approx_loc_imp_approx_loc_sup)
    1.97  done
    1.98  
    1.99  
   1.100  lemma Cast_conf2:
   1.101 -  "[|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.102 +  "[| wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; 
   1.103 +      G\<turnstile>Class C\<preceq>T; is_class G C|] 
   1.104    ==> G,h\<turnstile>v::\<preceq>T"
   1.105  apply (unfold cast_ok_def)
   1.106  apply (frule widen_Class)
   1.107 @@ -115,14 +122,15 @@
   1.108  
   1.109  lemma Checkcast_correct:
   1.110  "[| wf_prog wt G;
   1.111 -  method (G,C) sig = Some (C,rT,maxl,ins); 
   1.112 -  ins!pc = Checkcast D; 
   1.113 -  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.114 -  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.115 -  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.116 +    method (G,C) sig = Some (C,rT,maxl,ins); 
   1.117 +    ins!pc = Checkcast D; 
   1.118 +    wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
   1.119 +    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.120 +    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.121  ==> G,phi \<turnstile>JVM state'\<surd>"
   1.122  apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
   1.123 -apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2)
   1.124 +apply (blast intro: approx_stk_imp_approx_stk_sup 
   1.125 +                    approx_loc_imp_approx_loc_sup Cast_conf2)
   1.126  done
   1.127  
   1.128  
   1.129 @@ -134,7 +142,8 @@
   1.130    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.131    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.132  ==> G,phi \<turnstile>JVM state'\<surd>"
   1.133 -apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split)
   1.134 +apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def
   1.135 +                split: option.split)
   1.136  apply (frule conf_widen)
   1.137  apply assumption+
   1.138  apply (drule conf_RefTD)
   1.139 @@ -143,7 +152,8 @@
   1.140   apply (drule widen_cfs_fields)
   1.141   apply assumption+
   1.142   apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def)
   1.143 -apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
   1.144 +apply (blast intro: approx_stk_imp_approx_stk_sup 
   1.145 +                    approx_loc_imp_approx_loc_sup)
   1.146  done
   1.147  
   1.148  lemma Putfield_correct:
   1.149 @@ -162,11 +172,14 @@
   1.150  apply assumption
   1.151  apply (drule conf_RefTD)
   1.152  apply clarsimp
   1.153 -apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap
   1.154 -  approx_stk_imp_approx_stk_sup
   1.155 -  approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
   1.156 -  hconf_imp_hconf_field_update
   1.157 -  correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields)
   1.158 +apply (blast 
   1.159 +       intro: 
   1.160 +         sup_heap_update_value approx_stk_imp_approx_stk_sup_heap
   1.161 +         approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup_heap 
   1.162 +         approx_loc_imp_approx_loc_sup hconf_imp_hconf_field_update
   1.163 +         correct_frames_imp_correct_frames_field_update conf_widen 
   1.164 +       dest: 
   1.165 +         widen_cfs_fields)
   1.166  done
   1.167  
   1.168  lemma collapse_paired_All:
   1.169 @@ -181,15 +194,18 @@
   1.170    Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   1.171    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.172  ==> G,phi \<turnstile>JVM state'\<surd>"
   1.173 -apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def
   1.174 -		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
   1.175 +apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def defs1
   1.176 +		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def 
   1.177         split: option.split)
   1.178  apply (force dest!: iffD1 [OF collapse_paired_All]
   1.179 -            intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup
   1.180 -                   approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
   1.181 -                   hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref
   1.182 -                   correct_init_obj simp add:  NT_subtype_conv approx_val_def conf_def
   1.183 -		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
   1.184 +       intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap 
   1.185 +              approx_stk_imp_approx_stk_sup 
   1.186 +              approx_loc_imp_approx_loc_sup_heap 
   1.187 +              approx_loc_imp_approx_loc_sup
   1.188 +              hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref
   1.189 +              correct_init_obj 
   1.190 +       simp add: NT_subtype_conv approx_val_def conf_def defs1
   1.191 +         fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def 
   1.192         split: option.split)
   1.193  done
   1.194  
   1.195 @@ -366,7 +382,8 @@
   1.196          by (simp add: wt_start_def sup_state_def)
   1.197  
   1.198        have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)"
   1.199 -        by (simp add: approx_loc_def approx_val_Err list_all2_def set_replicate_conv_if)
   1.200 +        by (simp add: approx_loc_def approx_val_Err 
   1.201 +                      list_all2_def set_replicate_conv_if)
   1.202  
   1.203        from wfprog mD
   1.204        have "G \<turnstile> Class D \<preceq> Class D''"
   1.205 @@ -463,7 +480,8 @@
   1.206    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.207  ==> G,phi \<turnstile>JVM state'\<surd>"
   1.208  apply (clarsimp simp add: defs1)
   1.209 -apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
   1.210 +apply (fast intro: approx_loc_imp_approx_loc_sup 
   1.211 +                   approx_stk_imp_approx_stk_sup)
   1.212  done
   1.213  
   1.214  
   1.215 @@ -476,7 +494,8 @@
   1.216    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.217  ==> G,phi \<turnstile>JVM state'\<surd>"
   1.218  apply (clarsimp simp add: defs1)
   1.219 -apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
   1.220 +apply (fast intro: approx_loc_imp_approx_loc_sup 
   1.221 +                   approx_stk_imp_approx_stk_sup)
   1.222  done
   1.223  
   1.224  lemma Pop_correct:
   1.225 @@ -488,7 +507,8 @@
   1.226    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.227  ==> G,phi \<turnstile>JVM state'\<surd>"
   1.228  apply (clarsimp simp add: defs1)
   1.229 -apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
   1.230 +apply (fast intro: approx_loc_imp_approx_loc_sup 
   1.231 +                   approx_stk_imp_approx_stk_sup)
   1.232  done
   1.233  
   1.234  lemma Dup_correct:
   1.235 @@ -500,7 +520,9 @@
   1.236    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.237  ==> G,phi \<turnstile>JVM state'\<surd>"
   1.238  apply (clarsimp simp add: defs1 map_eq_Cons)
   1.239 -apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   1.240 +apply (force intro: approx_stk_imp_approx_stk_sup 
   1.241 +                    approx_val_imp_approx_val_sup 
   1.242 +                    approx_loc_imp_approx_loc_sup
   1.243               simp add: defs1 map_eq_Cons)
   1.244  done
   1.245  
   1.246 @@ -513,7 +535,9 @@
   1.247    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.248  ==> G,phi \<turnstile>JVM state'\<surd>"
   1.249  apply (clarsimp simp add: defs1 map_eq_Cons)
   1.250 -apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   1.251 +apply (force intro: approx_stk_imp_approx_stk_sup 
   1.252 +                    approx_val_imp_approx_val_sup 
   1.253 +                    approx_loc_imp_approx_loc_sup
   1.254               simp add: defs1 map_eq_Cons)
   1.255  done
   1.256  
   1.257 @@ -526,7 +550,9 @@
   1.258    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.259  ==> G,phi \<turnstile>JVM state'\<surd>"
   1.260  apply (clarsimp simp add: defs1 map_eq_Cons)
   1.261 -apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   1.262 +apply (force intro: approx_stk_imp_approx_stk_sup 
   1.263 +                    approx_val_imp_approx_val_sup 
   1.264 +                    approx_loc_imp_approx_loc_sup
   1.265               simp add: defs1 map_eq_Cons)
   1.266  done
   1.267  
   1.268 @@ -539,7 +565,9 @@
   1.269    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.270  ==> G,phi \<turnstile>JVM state'\<surd>"
   1.271  apply (clarsimp simp add: defs1 map_eq_Cons)
   1.272 -apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
   1.273 +apply (force intro: approx_stk_imp_approx_stk_sup 
   1.274 +                    approx_val_imp_approx_val_sup 
   1.275 +                    approx_loc_imp_approx_loc_sup
   1.276               simp add: defs1 map_eq_Cons)
   1.277  done
   1.278  
   1.279 @@ -552,7 +580,9 @@
   1.280    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   1.281  ==> G,phi \<turnstile>JVM state'\<surd>"
   1.282  apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
   1.283 -apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup)
   1.284 +apply (blast intro: approx_stk_imp_approx_stk_sup 
   1.285 +                    approx_val_imp_approx_val_sup 
   1.286 +                    approx_loc_imp_approx_loc_sup)
   1.287  done
   1.288  
   1.289  
   1.290 @@ -572,10 +602,11 @@
   1.291  prefer 9
   1.292  apply (blast intro: Return_correct)
   1.293  apply (unfold wt_jvm_prog_def)
   1.294 -apply (fast intro: Load_correct Store_correct Bipush_correct Aconst_null_correct 
   1.295 -       Checkcast_correct Getfield_correct Putfield_correct New_correct 
   1.296 -       Goto_correct Ifcmpeq_correct Pop_correct Dup_correct 
   1.297 -       Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+
   1.298 +apply (fast intro: 
   1.299 +  Load_correct Store_correct Bipush_correct Aconst_null_correct 
   1.300 +  Checkcast_correct Getfield_correct Putfield_correct New_correct 
   1.301 +  Goto_correct Ifcmpeq_correct Pop_correct Dup_correct 
   1.302 +  Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+
   1.303  done
   1.304  
   1.305  
   1.306 @@ -627,11 +658,14 @@
   1.307  
   1.308  
   1.309  theorem BV_correct_initial:
   1.310 -"[| wt_jvm_prog G phi; G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|] 
   1.311 - ==>  approx_stk G hp stk (fst (the (((phi  C)  sig) ! pc))) \<and> approx_loc G hp loc (snd (the (((phi  C)  sig) ! pc)))"
   1.312 +"[| wt_jvm_prog G phi; 
   1.313 +    G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|] 
   1.314 +==> approx_stk G hp stk (fst (the (((phi  C)  sig) ! pc))) \<and> 
   1.315 +    approx_loc G hp loc (snd (the (((phi  C)  sig) ! pc)))"
   1.316  apply (drule BV_correct)
   1.317  apply assumption+
   1.318 -apply (simp add: correct_state_def correct_frame_def split_def split: option.splits)
   1.319 +apply (simp add: correct_state_def correct_frame_def split_def 
   1.320 +            split: option.splits)
   1.321  done
   1.322  
   1.323  end
     2.1 --- a/src/HOL/MicroJava/BV/Convert.thy	Thu Sep 21 18:58:25 2000 +0200
     2.2 +++ b/src/HOL/MicroJava/BV/Convert.thy	Thu Sep 21 19:25:57 2000 +0200
     2.3 @@ -40,11 +40,13 @@
     2.4  
     2.5    (* lifts a relation to option with None as bottom element *)
     2.6    lift_bottom :: "('a => 'b => bool) => ('a option => 'b option => bool)"
     2.7 -  "lift_bottom P a' a == case a' of 
     2.8 -                          None    => True 
     2.9 -                        | Some t' => (case a of None => False | Some t => P t' t)"
    2.10 +  "lift_bottom P a' a == 
    2.11 +   case a' of 
    2.12 +     None    => True 
    2.13 +   | Some t' => (case a of None => False | Some t => P t' t)"
    2.14  
    2.15 -  sup_ty_opt :: "['code prog,ty err,ty err] => bool" ("_ \<turnstile> _ <=o _" [71,71] 70)
    2.16 +  sup_ty_opt :: "['code prog,ty err,ty err] => bool" 
    2.17 +                 ("_ \<turnstile> _ <=o _" [71,71] 70)
    2.18    "sup_ty_opt G == lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
    2.19  
    2.20    sup_loc :: "['code prog,locvars_type,locvars_type] => bool" 
    2.21 @@ -53,17 +55,22 @@
    2.22  
    2.23    sup_state :: "['code prog,state_type,state_type] => bool"	  
    2.24                 ("_ \<turnstile> _ <=s _"  [71,71] 70)
    2.25 -  "G \<turnstile> s <=s s' == (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
    2.26 +  "G \<turnstile> s <=s s' == 
    2.27 +   (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
    2.28  
    2.29    sup_state_opt :: "['code prog,state_type option,state_type option] => bool" 
    2.30                     ("_ \<turnstile> _ <=' _"  [71,71] 70)
    2.31    "sup_state_opt G == lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
    2.32  
    2.33  syntax (HTML output) 
    2.34 -  sup_ty_opt :: "['code prog,ty err,ty err] => bool" ("_ |- _ <=o _")
    2.35 -  sup_loc :: "['code prog,locvars_type,locvars_type] => bool" ("_ |- _ <=l _"  [71,71] 70)
    2.36 -  sup_state :: "['code prog,state_type,state_type] => bool"	("_ |- _ <=s _"  [71,71] 70)
    2.37 -  sup_state_opt :: "['code prog,state_type option,state_type option] => bool" ("_ |- _ <=' _"  [71,71] 70)
    2.38 +  sup_ty_opt    :: "['code prog,ty err,ty err] => bool" 
    2.39 +                   ("_ |- _ <=o _")
    2.40 +  sup_loc       :: "['code prog,locvars_type,locvars_type] => bool" 
    2.41 +                   ("_ |- _ <=l _"  [71,71] 70)
    2.42 +  sup_state     :: "['code prog,state_type,state_type] => bool"	
    2.43 +                   ("_ |- _ <=s _"  [71,71] 70)
    2.44 +  sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
    2.45 +                   ("_ |- _ <=' _"  [71,71] 70)
    2.46                     
    2.47  
    2.48  lemma not_Err_eq [iff]:
    2.49 @@ -80,7 +87,7 @@
    2.50    by (simp add: lift_top_def split: err.splits)
    2.51  
    2.52  lemma lift_top_trans [trans]:
    2.53 -  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] 
    2.54 +  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |]
    2.55    ==> lift_top P x z"
    2.56  proof -
    2.57    assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
    2.58 @@ -141,7 +148,8 @@
    2.59    by (simp add: lift_bottom_def split: option.splits)
    2.60  
    2.61  lemma lift_bottom_trans [trans]:
    2.62 -  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_bottom P x y; lift_bottom P y z |]
    2.63 +  "[| !!x y z. [| P x y; P y z |] ==> P x z; 
    2.64 +      lift_bottom P x y; lift_bottom P y z |]
    2.65    ==> lift_bottom P x z"
    2.66  proof -
    2.67    assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
    2.68 @@ -286,8 +294,8 @@
    2.69  
    2.70  
    2.71  theorem all_nth_sup_loc:
    2.72 -  "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n))) --> 
    2.73 -       (G \<turnstile> a <=l b)" (is "?P a")
    2.74 +  "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n))) 
    2.75 +  --> (G \<turnstile> a <=l b)" (is "?P a")
    2.76  proof (induct a)
    2.77    show "?P []" by simp
    2.78  
     3.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Thu Sep 21 18:58:25 2000 +0200
     3.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Sep 21 19:25:57 2000 +0200
     3.3 @@ -6,27 +6,29 @@
     3.4  The invariant for the type safety proof.
     3.5  *)
     3.6  
     3.7 -header "Type Safety Invariant"
     3.8 +header "BV Type Safety Invariant"
     3.9  
    3.10  theory Correct = BVSpec:
    3.11  
    3.12  constdefs
    3.13 - approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
    3.14 -"approx_val G h v any == case any of Err => True | Ok T => G,h\<turnstile>v::\<preceq>T"
    3.15 +  approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
    3.16 +  "approx_val G h v any == case any of Err => True | Ok T => G,h\<turnstile>v::\<preceq>T"
    3.17  
    3.18 - approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
    3.19 -"approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
    3.20 +  approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
    3.21 +  "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
    3.22 +
    3.23 +  approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
    3.24 +  "approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)"
    3.25  
    3.26 - approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
    3.27 -"approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)"
    3.28 +  correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool"
    3.29 +  "correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
    3.30 +                         approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
    3.31 +                         pc < length ins \<and> length loc=length(snd sig)+maxl+1"
    3.32  
    3.33 - correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool"
    3.34 -"correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
    3.35 -   approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
    3.36 -   pc < length ins \<and> length loc=length(snd sig)+maxl+1"
    3.37 -
    3.38 - correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] => frame => bool"
    3.39 -"correct_frame_opt G hp s == case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t"
    3.40 +  correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] 
    3.41 +                        => frame => bool"
    3.42 +  "correct_frame_opt G hp s == 
    3.43 +    case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t"
    3.44  
    3.45  
    3.46  consts
    3.47 @@ -75,7 +77,7 @@
    3.48  apply clarsimp
    3.49  apply (drule newref_None 1) back
    3.50  apply simp
    3.51 -.
    3.52 +done
    3.53  
    3.54  lemma sup_heap_update_value:
    3.55    "hp a = Some (C,od') ==> hp \<le>| hp (a \<mapsto> (C,od))"
    3.56 @@ -93,14 +95,15 @@
    3.57  by (auto intro: null simp add: approx_val_def)
    3.58  
    3.59  lemma approx_val_imp_approx_val_assConvertible [rule_format]: 
    3.60 -  "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T' --> approx_val G hp v (Ok T')"
    3.61 +  "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T' 
    3.62 +  --> approx_val G hp v (Ok T')"
    3.63  by (cases T) (auto intro: conf_widen simp add: approx_val_def)
    3.64  
    3.65  lemma approx_val_imp_approx_val_sup_heap [rule_format]:
    3.66    "approx_val G hp v at --> hp \<le>| hp' --> approx_val G hp' v at"
    3.67  apply (simp add: approx_val_def split: err.split)
    3.68  apply (blast intro: conf_hext)
    3.69 -.
    3.70 +done
    3.71  
    3.72  lemma approx_val_imp_approx_val_heap_update:
    3.73    "[|hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|] 
    3.74 @@ -108,24 +111,28 @@
    3.75  by (cases v, auto simp add: obj_ty_def conf_def)
    3.76  
    3.77  lemma approx_val_imp_approx_val_sup [rule_format]:
    3.78 -  "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') --> (approx_val G h v us')"
    3.79 +  "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') 
    3.80 +  --> (approx_val G h v us')"
    3.81  apply (simp add: sup_PTS_eq approx_val_def split: err.split)
    3.82  apply (blast intro: conf_widen)
    3.83 -.
    3.84 +done
    3.85  
    3.86  lemma approx_loc_imp_approx_val_sup:
    3.87 -  "[|wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at|]
    3.88 +  "[| wf_prog wt G; approx_loc G hp loc LT; idx < length LT; 
    3.89 +      v = loc!idx; G \<turnstile> LT!idx <=o at |]
    3.90    ==> approx_val G hp v at"
    3.91  apply (unfold approx_loc_def)
    3.92  apply (unfold list_all2_def)
    3.93 -apply (auto intro: approx_val_imp_approx_val_sup simp add: split_def all_set_conv_all_nth)
    3.94 -.
    3.95 +apply (auto intro: approx_val_imp_approx_val_sup 
    3.96 +            simp add: split_def all_set_conv_all_nth)
    3.97 +done
    3.98  
    3.99  
   3.100  (** approx_loc **)
   3.101  
   3.102  lemma approx_loc_Cons [iff]:
   3.103 -  "approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)"
   3.104 +  "approx_loc G hp (s#xs) (l#ls) = 
   3.105 +  (approx_val G hp s l \<and> approx_loc G hp xs ls)"
   3.106  by (simp add: approx_loc_def)
   3.107  
   3.108  lemma assConv_approx_stk_imp_approx_loc [rule_format]:
   3.109 @@ -136,25 +143,27 @@
   3.110  apply (clarsimp simp add: all_set_conv_all_nth)
   3.111  apply (rule approx_val_imp_approx_val_assConvertible)
   3.112  apply auto
   3.113 -.
   3.114 +done
   3.115  
   3.116  
   3.117  lemma approx_loc_imp_approx_loc_sup_heap [rule_format]:
   3.118 -  "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' --> approx_loc G hp' lvars lt"
   3.119 +  "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' 
   3.120 +  --> approx_loc G hp' lvars lt"
   3.121  apply (unfold approx_loc_def list_all2_def)
   3.122  apply (cases lt)
   3.123   apply simp
   3.124  apply clarsimp
   3.125  apply (rule approx_val_imp_approx_val_sup_heap)
   3.126  apply auto
   3.127 -.
   3.128 +done
   3.129  
   3.130  lemma approx_loc_imp_approx_loc_sup [rule_format]:
   3.131 -  "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' --> approx_loc G hp lvars lt'"
   3.132 +  "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' 
   3.133 +  --> approx_loc G hp lvars lt'"
   3.134  apply (unfold sup_loc_def approx_loc_def list_all2_def)
   3.135  apply (auto simp add: all_set_conv_all_nth)
   3.136  apply (auto elim: approx_val_imp_approx_val_sup)
   3.137 -.
   3.138 +done
   3.139  
   3.140  
   3.141  lemma approx_loc_imp_approx_loc_subst [rule_format]:
   3.142 @@ -162,18 +171,19 @@
   3.143    --> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
   3.144  apply (unfold approx_loc_def list_all2_def)
   3.145  apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
   3.146 -.
   3.147 +done
   3.148  
   3.149  
   3.150  lemmas [cong] = conj_cong 
   3.151  
   3.152  lemma approx_loc_append [rule_format]:
   3.153    "\<forall>L1 l2 L2. length l1=length L1 --> 
   3.154 -  approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
   3.155 +  approx_loc G hp (l1@l2) (L1@L2) = 
   3.156 +  (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
   3.157  apply (unfold approx_loc_def list_all2_def)
   3.158  apply simp
   3.159  apply blast
   3.160 -.
   3.161 +done
   3.162  
   3.163  lemmas [cong del] = conj_cong
   3.164  
   3.165 @@ -184,7 +194,7 @@
   3.166    "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
   3.167  apply (unfold approx_stk_def approx_loc_def list_all2_def)
   3.168  apply (auto simp add: zip_rev sym [OF rev_map])
   3.169 -.
   3.170 +done
   3.171  
   3.172  lemma approx_stk_rev:
   3.173    "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)"
   3.174 @@ -192,7 +202,8 @@
   3.175  
   3.176  
   3.177  lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
   3.178 -  "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' --> approx_stk G hp' lvars lt"
   3.179 +  "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' 
   3.180 +  --> approx_stk G hp' lvars lt"
   3.181  by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
   3.182  
   3.183  lemma approx_stk_imp_approx_stk_sup [rule_format]:
   3.184 @@ -229,7 +240,7 @@
   3.185  apply (unfold oconf_def lconf_def)
   3.186  apply (simp add: map_of_map)
   3.187  apply (force intro: defval_conf dest: map_of_SomeD is_type_fields)
   3.188 -.
   3.189 +done
   3.190  
   3.191  
   3.192  lemma oconf_imp_oconf_field_update [rule_format]:
   3.193 @@ -243,7 +254,7 @@
   3.194  apply (unfold oconf_def lconf_def)
   3.195  apply simp
   3.196  apply (fast intro: conf_hext sup_heap_newref)
   3.197 -.
   3.198 +done
   3.199  
   3.200  
   3.201  lemma oconf_imp_oconf_heap_update [rule_format]:
   3.202 @@ -252,7 +263,7 @@
   3.203  apply (unfold oconf_def lconf_def)
   3.204  apply simp
   3.205  apply (force intro: approx_val_imp_approx_val_heap_update)
   3.206 -.
   3.207 +done
   3.208  
   3.209  
   3.210  (** hconf **)
   3.211 @@ -262,7 +273,7 @@
   3.212    "hp x = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
   3.213  apply (simp add: hconf_def)
   3.214  apply (fast intro: oconf_imp_oconf_heap_newref)
   3.215 -.
   3.216 +done
   3.217  
   3.218  lemma hconf_imp_hconf_field_update [rule_format]:
   3.219    "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> 
   3.220 @@ -270,7 +281,7 @@
   3.221  apply (simp add: hconf_def)
   3.222  apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update 
   3.223               simp add: obj_ty_def)
   3.224 -.
   3.225 +done
   3.226  
   3.227  (** correct_frames **)
   3.228  
   3.229 @@ -297,7 +308,7 @@
   3.230   apply simp
   3.231  apply (rule sup_heap_update_value)
   3.232  apply simp
   3.233 -.
   3.234 +done
   3.235  
   3.236  lemma correct_frames_imp_correct_frames_newref [rule_format]:
   3.237    "\<forall>rT C sig. hp x = None --> correct_frames G hp phi rT sig frs \<and> oconf G hp obj 
   3.238 @@ -318,7 +329,7 @@
   3.239   apply simp
   3.240  apply (rule sup_heap_newref)
   3.241  apply simp
   3.242 -.
   3.243 +done
   3.244  
   3.245  end
   3.246  
     4.1 --- a/src/HOL/MicroJava/J/Eval.thy	Thu Sep 21 18:58:25 2000 +0200
     4.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Thu Sep 21 19:25:57 2000 +0200
     4.3 @@ -15,113 +15,115 @@
     4.4    exec  :: "java_mb prog => (xstate \\<times> stmt                 \\<times> xstate) set"
     4.5  
     4.6  syntax
     4.7 -  eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "("_\\<turnstile>_ -_\\<succ>_-> _"[51,82,82,82,82]81)
     4.8 +  eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
     4.9 +          ("_\\<turnstile>_ -_\\<succ>_-> _"[51,82,82,82,82]81)
    4.10    evals:: "[java_mb prog,xstate,expr list,
    4.11 -	                      val list,xstate] => bool "("_\\<turnstile>_ -_[\\<succ>]_-> _"[51,82,51,51,82]81)
    4.12 -  exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "("_\\<turnstile>_ -_-> _"  [51,82,82,   82]81)
    4.13 +                        val list,xstate] => bool "
    4.14 +          ("_\\<turnstile>_ -_[\\<succ>]_-> _"[51,82,51,51,82]81)
    4.15 +  exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
    4.16 +          ("_\\<turnstile>_ -_-> _"  [51,82,82,   82]81)
    4.17  
    4.18  translations
    4.19    "G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval  G"
    4.20 -  "G\\<turnstile>s -e \\<succ> v->    s' " == "(s, e, v,    s' ) \\<in> eval  G"
    4.21 +  "G\\<turnstile>s -e \\<succ> v->    s' " == "(s, e, v,    s') \\<in> eval  G"
    4.22    "G\\<turnstile>s -e[\\<succ>]v-> (x,s')" <= "(s, e, v, x, s') \\<in> evals G"
    4.23 -  "G\\<turnstile>s -e[\\<succ>]v->    s' " == "(s, e, v,    s' ) \\<in> evals G"
    4.24 -  "G\\<turnstile>s -c    -> (x,s')" <= "(s, c, x, s') \\<in> exec  G"
    4.25 -  "G\\<turnstile>s -c    ->    s' " == "(s, c,    s') \\<in> exec  G"
    4.26 +  "G\\<turnstile>s -e[\\<succ>]v->    s' " == "(s, e, v,    s') \\<in> evals G"
    4.27 +  "G\\<turnstile>s -c    -> (x,s')" <= "(s, c, x, s') \\<in> exec G"
    4.28 +  "G\\<turnstile>s -c    ->    s' " == "(s, c,    s') \\<in> exec G"
    4.29  
    4.30  inductive "eval G" "evals G" "exec G" intrs
    4.31  
    4.32  (* evaluation of expressions *)
    4.33  
    4.34    (* cf. 15.5 *)
    4.35 -  XcptE				  "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary-> (Some xc,s)"
    4.36 +  XcptE "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary-> (Some xc,s)"
    4.37  
    4.38    (* cf. 15.8.1 *)
    4.39 -  NewC	"[|h = heap s; (a,x) = new_Addr h;
    4.40 -	  h'= h(a\\<mapsto>(C,init_vars (fields (G,C))))|] ==>
    4.41 -				   G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> c_hupd h' (x,s)"
    4.42 +  NewC  "[| h = heap s; (a,x) = new_Addr h;
    4.43 +            h'= h(a\\<mapsto>(C,init_vars (fields (G,C)))) |] ==>
    4.44 +         G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> c_hupd h' (x,s)"
    4.45  
    4.46    (* cf. 15.15 *)
    4.47 -  Cast	"[|G\\<turnstile>Norm s0 -e\\<succ>v-> (x1,s1);
    4.48 -	  x2=raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1|] ==>
    4.49 -			        G\\<turnstile>Norm s0 -Cast C e\\<succ>v-> (x2,s1)"
    4.50 +  Cast  "[| G\\<turnstile>Norm s0 -e\\<succ>v-> (x1,s1);
    4.51 +            x2 = raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1 |] ==>
    4.52 +         G\\<turnstile>Norm s0 -Cast C e\\<succ>v-> (x2,s1)"
    4.53  
    4.54    (* cf. 15.7.1 *)
    4.55 -  Lit				   "G\\<turnstile>Norm s -Lit v\\<succ>v-> Norm s"
    4.56 +  Lit   "G\\<turnstile>Norm s -Lit v\\<succ>v-> Norm s"
    4.57  
    4.58 -  BinOp "[|G\\<turnstile>Norm s -e1\\<succ>v1-> s1;
    4.59 -	  G\\<turnstile>s1     -e2\\<succ>v2-> s2;
    4.60 -	  v = (case bop of Eq  => Bool (v1 = v2)
    4.61 -	                 | Add => Intg (the_Intg v1 + the_Intg v2))|] ==>
    4.62 -				   G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v-> s2"
    4.63 +  BinOp "[| G\\<turnstile>Norm s -e1\\<succ>v1-> s1;
    4.64 +            G\\<turnstile>s1     -e2\\<succ>v2-> s2;
    4.65 +            v = (case bop of Eq  => Bool (v1 = v2)
    4.66 +                           | Add => Intg (the_Intg v1 + the_Intg v2)) |] ==>
    4.67 +         G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v-> s2"
    4.68  
    4.69    (* cf. 15.13.1, 15.2 *)
    4.70 -  LAcc				  "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)-> Norm s"
    4.71 +  LAcc  "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)-> Norm s"
    4.72  
    4.73    (* cf. 15.25.1 *)
    4.74 -  LAss  "[|G\\<turnstile>Norm s -e\\<succ>v->  (x,(h,l));
    4.75 -	  l' = (if x = None then l(va\\<mapsto>v) else l)|] ==>
    4.76 -				   G\\<turnstile>Norm s -va::=e\\<succ>v-> (x,(h,l'))"
    4.77 +  LAss  "[| G\\<turnstile>Norm s -e\\<succ>v-> (x,(h,l));
    4.78 +            l' = (if x = None then l(va\\<mapsto>v) else l) |] ==>
    4.79 +         G\\<turnstile>Norm s -va::=e\\<succ>v-> (x,(h,l'))"
    4.80  
    4.81  
    4.82    (* cf. 15.10.1, 15.2 *)
    4.83 -  FAcc	"[|G\\<turnstile>Norm s0 -e\\<succ>a'-> (x1,s1); 
    4.84 -	  v = the (snd (the (heap s1 (the_Addr a'))) (fn,T))|] ==>
    4.85 -				 G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v-> (np a' x1,s1)"
    4.86 +  FAcc  "[| G\\<turnstile>Norm s0 -e\\<succ>a'-> (x1,s1); 
    4.87 +            v = the (snd (the (heap s1 (the_Addr a'))) (fn,T)) |] ==>
    4.88 +         G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v-> (np a' x1,s1)"
    4.89  
    4.90    (* cf. 15.25.1 *)
    4.91 -  FAss  "[|G\\<turnstile>     Norm s0  -e1\\<succ>a'-> (x1,s1); a = the_Addr a';
    4.92 -	  G\\<turnstile>(np a' x1,s1) -e2\\<succ>v -> (x2,s2);
    4.93 -	  h = heap s2; (c,fs) = the (h a);
    4.94 -	  h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v))))|] ==>
    4.95 -			  G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v-> c_hupd h' (x2,s2)"
    4.96 +  FAss  "[| G\\<turnstile>     Norm s0  -e1\\<succ>a'-> (x1,s1); a = the_Addr a';
    4.97 +            G\\<turnstile>(np a' x1,s1) -e2\\<succ>v -> (x2,s2);
    4.98 +            h  = heap s2; (c,fs) = the (h a);
    4.99 +            h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v)))) |] ==>
   4.100 +         G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v-> c_hupd h' (x2,s2)"
   4.101  
   4.102    (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
   4.103 -  Call	"[|G\\<turnstile>Norm s0 -e\\<succ>a'-> s1; a = the_Addr a';
   4.104 -	   G\\<turnstile>s1 -ps[\\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
   4.105 -	   (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
   4.106 -	   G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk-> s3;
   4.107 -	   G\\<turnstile>     s3 -res\\<succ>v -> (x4,s4)|] ==>
   4.108 -			    G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
   4.109 +  Call  "[| G\\<turnstile>Norm s0 -e\\<succ>a'-> s1; a = the_Addr a';
   4.110 +            G\\<turnstile>s1 -ps[\\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
   4.111 +            (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
   4.112 +            G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk-> s3;
   4.113 +            G\\<turnstile> s3 -res\\<succ>v -> (x4,s4) |] ==>
   4.114 +         G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
   4.115  
   4.116  
   4.117  (* evaluation of expression lists *)
   4.118  
   4.119    (* cf. 15.5 *)
   4.120 -  XcptEs			  "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary-> (Some xc,s)"
   4.121 +  XcptEs "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary-> (Some xc,s)"
   4.122  
   4.123    (* cf. 15.11.??? *)
   4.124 -  Nil
   4.125 -				    "G\\<turnstile>Norm s0 -[][\\<succ>][]-> Norm s0"
   4.126 +  Nil   "G\\<turnstile>Norm s0 -[][\\<succ>][]-> Norm s0"
   4.127  
   4.128    (* cf. 15.6.4 *)
   4.129 -  Cons	"[|G\\<turnstile>Norm s0 -e  \\<succ> v -> s1;
   4.130 -           G\\<turnstile>     s1 -es[\\<succ>]vs-> s2|] ==>
   4.131 -				   G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs-> s2"
   4.132 +  Cons  "[| G\\<turnstile>Norm s0 -e  \\<succ> v -> s1;
   4.133 +            G\\<turnstile>     s1 -es[\\<succ>]vs-> s2 |] ==>
   4.134 +         G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs-> s2"
   4.135  
   4.136  (* execution of statements *)
   4.137  
   4.138    (* cf. 14.1 *)
   4.139 -  XcptS				 "G\\<turnstile>(Some xc,s) -s0-> (Some xc,s)"
   4.140 +  XcptS "G\\<turnstile>(Some xc,s) -s0-> (Some xc,s)"
   4.141  
   4.142    (* cf. 14.5 *)
   4.143 -  Skip	 			    "G\\<turnstile>Norm s -Skip-> Norm s"
   4.144 +  Skip  "G\\<turnstile>Norm s -Skip-> Norm s"
   4.145  
   4.146    (* cf. 14.7 *)
   4.147 -  Expr	"[|G\\<turnstile>Norm s0 -e\\<succ>v-> s1|] ==>
   4.148 -				  G\\<turnstile>Norm s0 -Expr e-> s1"
   4.149 +  Expr  "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1 |] ==>
   4.150 +         G\\<turnstile>Norm s0 -Expr e-> s1"
   4.151  
   4.152    (* cf. 14.2 *)
   4.153 -  Comp	"[|G\\<turnstile>Norm s0 -s -> s1;
   4.154 -	  G\\<turnstile>     s1 -t -> s2|] ==>
   4.155 -				 G\\<turnstile>Norm s0 -(s;; t)-> s2"
   4.156 +  Comp  "[| G\\<turnstile>Norm s0 -s -> s1;
   4.157 +            G\\<turnstile> s1 -t -> s2|] ==>
   4.158 +         G\\<turnstile>Norm s0 -(s;; t)-> s2"
   4.159  
   4.160    (* cf. 14.8.2 *)
   4.161 -  Cond	"[|G\\<turnstile>Norm s0  -e \\<succ>v-> s1;
   4.162 -	  G\\<turnstile>     s1 -(if  the_Bool v then s else t)-> s2|] ==>
   4.163 -		        G\\<turnstile>Norm s0 -(If(e) s Else t)-> s2"
   4.164 +  Cond  "[| G\\<turnstile>Norm s0  -e \\<succ>v-> s1;
   4.165 +            G\\<turnstile> s1 -(if  the_Bool v then s else t)-> s2|] ==>
   4.166 +         G\\<turnstile>Norm s0 -(If(e) s Else t)-> s2"
   4.167  
   4.168    (* cf. 14.10, 14.10.1 *)
   4.169 -  Loop	"[|G\\<turnstile>Norm s0 -(If(e) (s;; While(e) s) Else Skip)-> s1|] ==>
   4.170 -			    G\\<turnstile>Norm s0 -(While(e) s)-> s1"
   4.171 +  Loop  "[| G\\<turnstile>Norm s0 -(If(e) (s;; While(e) s) Else Skip)-> s1 |] ==>
   4.172 +         G\\<turnstile>Norm s0 -(While(e) s)-> s1"
   4.173  
   4.174  end
     5.1 --- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Thu Sep 21 18:58:25 2000 +0200
     5.2 +++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Thu Sep 21 19:25:57 2000 +0200
     5.3 @@ -9,7 +9,8 @@
     5.4  JVMExecInstr = JVMInstructions + JVMState +
     5.5  
     5.6  consts
     5.7 -exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state"
     5.8 +  exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, 
     5.9 +                  cname, sig, p_count, frame list] => jvm_state"
    5.10  primrec
    5.11   "exec_instr (Load idx) G hp stk vars Cl sig pc frs = 
    5.12        (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"
    5.13 @@ -63,9 +64,9 @@
    5.14  	     xp'	= raise_xcpt (oref=Null) NullPointer;
    5.15  	     dynT	= fst(the(hp(the_Addr oref)));
    5.16  	     (dc,mh,mxl,c)= the (method (G,dynT) (mn,ps));
    5.17 -	     frs'	= if xp'=None
    5.18 -	                  then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
    5.19 -	                  else []
    5.20 +	     frs'	= if xp'=None then 
    5.21 +                [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
    5.22 +	            else []
    5.23  	 in
    5.24        (xp', hp, frs'@(drop (n+1) stk, vars, Cl, sig, pc+1)#frs))"
    5.25  
    5.26 @@ -84,11 +85,13 @@
    5.27        (None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)"
    5.28  
    5.29   "exec_instr Dup_x1 G hp stk vars Cl sig pc frs = 
    5.30 -      (None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)), vars, Cl, sig, pc+1)#frs)"
    5.31 +      (None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)), 
    5.32 +                  vars, Cl, sig, pc+1)#frs)"
    5.33  
    5.34   "exec_instr Dup_x2 G hp stk vars Cl sig pc frs = 
    5.35 -      (None, hp, (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
    5.36 -                  vars, Cl, sig, pc+1)#frs)"
    5.37 +      (None, hp, 
    5.38 +       (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
    5.39 +       vars, Cl, sig, pc+1)#frs)"
    5.40  
    5.41   "exec_instr Swap G hp stk vars Cl sig pc frs =
    5.42  	(let (val1,val2) = (hd stk,hd (tl stk))
    5.43 @@ -98,7 +101,8 @@
    5.44   "exec_instr IAdd G hp stk vars Cl sig pc frs =
    5.45    (let (val1,val2) = (hd stk,hd (tl stk))
    5.46     in
    5.47 -      (None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))"
    5.48 +      (None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), 
    5.49 +       vars, Cl, sig, pc+1)#frs))"
    5.50  
    5.51   "exec_instr (Ifcmpeq i) G hp stk vars Cl sig pc frs =
    5.52  	(let (val1,val2) = (hd stk, hd (tl stk));