src/HOL/MicroJava/BV/Correct.thy
changeset 10042 7164dc0d24d8
parent 9941 fe05af7ec816
child 10056 9f84ffa4a8d0
     1.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -11,26 +11,26 @@
     1.4  theory Correct = BVSpec:
     1.5  
     1.6  constdefs
     1.7 - approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
     1.8 -"approx_val G h v any \<equiv> case any of Err \<Rightarrow> True | Ok T \<Rightarrow> G,h\<turnstile>v\<Colon>\<preceq>T"
     1.9 + approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
    1.10 +"approx_val G h v any == case any of Err => True | Ok T => G,h\<turnstile>v::\<preceq>T"
    1.11  
    1.12 - approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool"
    1.13 -"approx_loc G hp loc LT \<equiv> list_all2 (approx_val G hp) loc LT"
    1.14 + approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
    1.15 +"approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
    1.16  
    1.17 - approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool"
    1.18 -"approx_stk G hp stk ST \<equiv> approx_loc G hp stk (map Ok ST)"
    1.19 + approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
    1.20 +"approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)"
    1.21  
    1.22 - correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
    1.23 -"correct_frame G hp \<equiv> \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
    1.24 + correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool"
    1.25 +"correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
    1.26     approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
    1.27     pc < length ins \<and> length loc=length(snd sig)+maxl+1"
    1.28  
    1.29 - correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
    1.30 -"correct_frame_opt G hp s \<equiv> case s of None \<Rightarrow> \<lambda>maxl ins f. False | Some t \<Rightarrow> correct_frame G hp t"
    1.31 + correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] => frame => bool"
    1.32 +"correct_frame_opt G hp s == case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t"
    1.33  
    1.34  
    1.35  consts
    1.36 - correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool"
    1.37 + correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool"
    1.38  primrec
    1.39  "correct_frames G hp phi rT0 sig0 [] = True"
    1.40  
    1.41 @@ -52,13 +52,13 @@
    1.42  
    1.43  
    1.44  constdefs
    1.45 - correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
    1.46 + correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
    1.47                    ("_,_\<turnstile>JVM _\<surd>"  [51,51] 50)
    1.48 -"correct_state G phi \<equiv> \<lambda>(xp,hp,frs).
    1.49 +"correct_state G phi == \<lambda>(xp,hp,frs).
    1.50     case xp of
    1.51 -     None \<Rightarrow> (case frs of
    1.52 -	           [] \<Rightarrow> True
    1.53 -             | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and>
    1.54 +     None => (case frs of
    1.55 +	           [] => True
    1.56 +             | (f#fs) => G\<turnstile>h hp\<surd> \<and>
    1.57  			(let (stk,loc,C,sig,pc) = f
    1.58  		         in
    1.59                           \<exists>rT maxl ins s.
    1.60 @@ -66,11 +66,11 @@
    1.61                           phi C sig ! pc = Some s \<and>
    1.62  			 correct_frame G hp s maxl ins f \<and> 
    1.63  		         correct_frames G hp phi rT sig fs))
    1.64 -   | Some x \<Rightarrow> True" 
    1.65 +   | Some x => True" 
    1.66  
    1.67  
    1.68  lemma sup_heap_newref:
    1.69 -  "hp x = None \<Longrightarrow> hp \<le>| hp(newref hp \<mapsto> obj)"
    1.70 +  "hp x = None ==> hp \<le>| hp(newref hp \<mapsto> obj)"
    1.71  apply (unfold hext_def)
    1.72  apply clarsimp
    1.73  apply (drule newref_None 1) back
    1.74 @@ -78,7 +78,7 @@
    1.75  .
    1.76  
    1.77  lemma sup_heap_update_value:
    1.78 -  "hp a = Some (C,od') \<Longrightarrow> hp \<le>| hp (a \<mapsto> (C,od))"
    1.79 +  "hp a = Some (C,od') ==> hp \<le>| hp (a \<mapsto> (C,od))"
    1.80  by (simp add: hext_def)
    1.81  
    1.82  
    1.83 @@ -93,29 +93,29 @@
    1.84  by (auto intro: null simp add: approx_val_def)
    1.85  
    1.86  lemma approx_val_imp_approx_val_assConvertible [rule_format]: 
    1.87 -  "wf_prog wt G \<Longrightarrow> approx_val G hp v (Ok T) \<longrightarrow> G\<turnstile> T\<preceq>T' \<longrightarrow> approx_val G hp v (Ok T')"
    1.88 +  "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T' --> approx_val G hp v (Ok T')"
    1.89  by (cases T) (auto intro: conf_widen simp add: approx_val_def)
    1.90  
    1.91  lemma approx_val_imp_approx_val_sup_heap [rule_format]:
    1.92 -  "approx_val G hp v at \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_val G hp' v at"
    1.93 +  "approx_val G hp v at --> hp \<le>| hp' --> approx_val G hp' v at"
    1.94  apply (simp add: approx_val_def split: err.split)
    1.95  apply (blast intro: conf_hext)
    1.96  .
    1.97  
    1.98  lemma approx_val_imp_approx_val_heap_update:
    1.99 -  "\<lbrakk>hp a = Some obj'; G,hp\<turnstile> v\<Colon>\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> 
   1.100 -  \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v\<Colon>\<preceq>T"
   1.101 +  "[|hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|] 
   1.102 +  ==> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
   1.103  by (cases v, auto simp add: obj_ty_def conf_def)
   1.104  
   1.105  lemma approx_val_imp_approx_val_sup [rule_format]:
   1.106 -  "wf_prog wt G \<Longrightarrow> (approx_val G h v us) \<longrightarrow> (G \<turnstile> us <=o us') \<longrightarrow> (approx_val G h v us')"
   1.107 +  "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') --> (approx_val G h v us')"
   1.108  apply (simp add: sup_PTS_eq approx_val_def split: err.split)
   1.109  apply (blast intro: conf_widen)
   1.110  .
   1.111  
   1.112  lemma approx_loc_imp_approx_val_sup:
   1.113 -  "\<lbrakk>wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at\<rbrakk>
   1.114 -  \<Longrightarrow> approx_val G hp v at"
   1.115 +  "[|wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at|]
   1.116 +  ==> approx_val G hp v at"
   1.117  apply (unfold approx_loc_def)
   1.118  apply (unfold list_all2_def)
   1.119  apply (auto intro: approx_val_imp_approx_val_sup simp add: split_def all_set_conv_all_nth)
   1.120 @@ -129,8 +129,8 @@
   1.121  by (simp add: approx_loc_def)
   1.122  
   1.123  lemma assConv_approx_stk_imp_approx_loc [rule_format]:
   1.124 -  "wf_prog wt G \<Longrightarrow> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) 
   1.125 -  \<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp s tys_n \<longrightarrow> 
   1.126 +  "wf_prog wt G ==> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) 
   1.127 +  --> length tys_n = length ts --> approx_stk G hp s tys_n --> 
   1.128    approx_loc G hp s (map Ok ts)"
   1.129  apply (unfold approx_stk_def approx_loc_def list_all2_def)
   1.130  apply (clarsimp simp add: all_set_conv_all_nth)
   1.131 @@ -140,7 +140,7 @@
   1.132  
   1.133  
   1.134  lemma approx_loc_imp_approx_loc_sup_heap [rule_format]:
   1.135 -  "\<forall>lvars. approx_loc G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_loc G hp' lvars lt"
   1.136 +  "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' --> approx_loc G hp' lvars lt"
   1.137  apply (unfold approx_loc_def list_all2_def)
   1.138  apply (cases lt)
   1.139   apply simp
   1.140 @@ -150,7 +150,7 @@
   1.141  .
   1.142  
   1.143  lemma approx_loc_imp_approx_loc_sup [rule_format]:
   1.144 -  "wf_prog wt G \<Longrightarrow> approx_loc G hp lvars lt \<longrightarrow> G \<turnstile> lt <=l lt' \<longrightarrow> approx_loc G hp lvars lt'"
   1.145 +  "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' --> approx_loc G hp lvars lt'"
   1.146  apply (unfold sup_loc_def approx_loc_def list_all2_def)
   1.147  apply (auto simp add: all_set_conv_all_nth)
   1.148  apply (auto elim: approx_val_imp_approx_val_sup)
   1.149 @@ -158,8 +158,8 @@
   1.150  
   1.151  
   1.152  lemma approx_loc_imp_approx_loc_subst [rule_format]:
   1.153 -  "\<forall>loc idx x X. (approx_loc G hp loc LT) \<longrightarrow> (approx_val G hp x X) 
   1.154 -  \<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
   1.155 +  "\<forall>loc idx x X. (approx_loc G hp loc LT) --> (approx_val G hp x X) 
   1.156 +  --> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
   1.157  apply (unfold approx_loc_def list_all2_def)
   1.158  apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
   1.159  .
   1.160 @@ -168,7 +168,7 @@
   1.161  lemmas [cong] = conj_cong 
   1.162  
   1.163  lemma approx_loc_append [rule_format]:
   1.164 -  "\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow> 
   1.165 +  "\<forall>L1 l2 L2. length l1=length L1 --> 
   1.166    approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
   1.167  apply (unfold approx_loc_def list_all2_def)
   1.168  apply simp
   1.169 @@ -192,12 +192,12 @@
   1.170  
   1.171  
   1.172  lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
   1.173 -  "\<forall>lvars. approx_stk G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_stk G hp' lvars lt"
   1.174 +  "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' --> approx_stk G hp' lvars lt"
   1.175  by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
   1.176  
   1.177  lemma approx_stk_imp_approx_stk_sup [rule_format]:
   1.178 -  "wf_prog wt G \<Longrightarrow> approx_stk G hp lvars st \<longrightarrow> (G \<turnstile> map Ok st <=l (map Ok st')) 
   1.179 -  \<longrightarrow> approx_stk G hp lvars st'" 
   1.180 +  "wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map Ok st <=l (map Ok st')) 
   1.181 +  --> approx_stk G hp lvars st'" 
   1.182  by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
   1.183  
   1.184  lemma approx_stk_Nil [iff]:
   1.185 @@ -215,7 +215,7 @@
   1.186  by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
   1.187  
   1.188  lemma approx_stk_append_lemma:
   1.189 -  "approx_stk G hp stk (S@ST') \<Longrightarrow>
   1.190 +  "approx_stk G hp stk (S@ST') ==>
   1.191     (\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length ST' \<and> 
   1.192               approx_stk G hp s S \<and> approx_stk G hp stk' ST')"
   1.193  by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
   1.194 @@ -224,7 +224,7 @@
   1.195  (** oconf **)
   1.196  
   1.197  lemma correct_init_obj:
   1.198 -  "\<lbrakk>is_class G C; wf_prog wt G\<rbrakk> \<Longrightarrow> 
   1.199 +  "[|is_class G C; wf_prog wt G|] ==> 
   1.200    G,h \<turnstile> (C, map_of (map (\<lambda>(f,fT).(f,default_val fT)) (fields(G,C)))) \<surd>"
   1.201  apply (unfold oconf_def lconf_def)
   1.202  apply (simp add: map_of_map)
   1.203 @@ -233,13 +233,13 @@
   1.204  
   1.205  
   1.206  lemma oconf_imp_oconf_field_update [rule_format]:
   1.207 -  "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v\<Colon>\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
   1.208 -  \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
   1.209 +  "[|map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> |]
   1.210 +  ==> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
   1.211  by (simp add: oconf_def lconf_def)
   1.212  
   1.213  
   1.214  lemma oconf_imp_oconf_heap_newref [rule_format]:
   1.215 -"hp x = None \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G,hp\<turnstile>obj'\<surd> \<longrightarrow> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>"
   1.216 +"hp x = None --> G,hp\<turnstile>obj\<surd> --> G,hp\<turnstile>obj'\<surd> --> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>"
   1.217  apply (unfold oconf_def lconf_def)
   1.218  apply simp
   1.219  apply (fast intro: conf_hext sup_heap_newref)
   1.220 @@ -247,8 +247,8 @@
   1.221  
   1.222  
   1.223  lemma oconf_imp_oconf_heap_update [rule_format]:
   1.224 -  "hp a = Some obj' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd> 
   1.225 -  \<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
   1.226 +  "hp a = Some obj' --> obj_ty obj' = obj_ty obj'' --> G,hp\<turnstile>obj\<surd> 
   1.227 +  --> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
   1.228  apply (unfold oconf_def lconf_def)
   1.229  apply simp
   1.230  apply (force intro: approx_val_imp_approx_val_heap_update)
   1.231 @@ -259,14 +259,14 @@
   1.232  
   1.233  
   1.234  lemma hconf_imp_hconf_newref [rule_format]:
   1.235 -  "hp x = None \<longrightarrow> G\<turnstile>h hp\<surd> \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
   1.236 +  "hp x = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
   1.237  apply (simp add: hconf_def)
   1.238  apply (fast intro: oconf_imp_oconf_heap_newref)
   1.239  .
   1.240  
   1.241  lemma hconf_imp_hconf_field_update [rule_format]:
   1.242    "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> 
   1.243 -  G,hp\<turnstile>v\<Colon>\<preceq>T \<and> G\<turnstile>h hp\<surd> \<longrightarrow> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>"
   1.244 +  G,hp\<turnstile>v::\<preceq>T \<and> G\<turnstile>h hp\<surd> --> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>"
   1.245  apply (simp add: hconf_def)
   1.246  apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update 
   1.247               simp add: obj_ty_def)
   1.248 @@ -277,10 +277,10 @@
   1.249  lemmas [simp del] = fun_upd_apply
   1.250  
   1.251  lemma correct_frames_imp_correct_frames_field_update [rule_format]:
   1.252 -  "\<forall>rT C sig. correct_frames G hp phi rT sig frs \<longrightarrow> 
   1.253 -  hp a = Some (C,od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
   1.254 -  G,hp\<turnstile>v\<Colon>\<preceq>fd 
   1.255 -  \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs";
   1.256 +  "\<forall>rT C sig. correct_frames G hp phi rT sig frs --> 
   1.257 +  hp a = Some (C,od) --> map_of (fields (G, C)) fl = Some fd --> 
   1.258 +  G,hp\<turnstile>v::\<preceq>fd 
   1.259 +  --> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs";
   1.260  apply (induct frs)
   1.261   apply simp
   1.262  apply (clarsimp simp add: correct_frame_def) (*takes long*)
   1.263 @@ -300,8 +300,8 @@
   1.264  .
   1.265  
   1.266  lemma correct_frames_imp_correct_frames_newref [rule_format]:
   1.267 -  "\<forall>rT C sig. hp x = None \<longrightarrow> correct_frames G hp phi rT sig frs \<and> oconf G hp obj 
   1.268 -  \<longrightarrow> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
   1.269 +  "\<forall>rT C sig. hp x = None --> correct_frames G hp phi rT sig frs \<and> oconf G hp obj 
   1.270 +  --> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
   1.271  apply (induct frs)
   1.272   apply simp
   1.273  apply (clarsimp simp add: correct_frame_def)