src/HOL/MicroJava/BV/Correct.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10042 7164dc0d24d8
     1.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -92,11 +92,11 @@
     1.4    "approx_val G hp Null (Ok (RefT x))"
     1.5  by (auto intro: null simp add: approx_val_def)
     1.6  
     1.7 -lemma approx_val_imp_approx_val_assConvertible [rulified]: 
     1.8 +lemma approx_val_imp_approx_val_assConvertible [rule_format]: 
     1.9    "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.10  by (cases T) (auto intro: conf_widen simp add: approx_val_def)
    1.11  
    1.12 -lemma approx_val_imp_approx_val_sup_heap [rulified]:
    1.13 +lemma approx_val_imp_approx_val_sup_heap [rule_format]:
    1.14    "approx_val G hp v at \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_val G hp' v at"
    1.15  apply (simp add: approx_val_def split: err.split)
    1.16  apply (blast intro: conf_hext)
    1.17 @@ -107,7 +107,7 @@
    1.18    \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v\<Colon>\<preceq>T"
    1.19  by (cases v, auto simp add: obj_ty_def conf_def)
    1.20  
    1.21 -lemma approx_val_imp_approx_val_sup [rulified]:
    1.22 +lemma approx_val_imp_approx_val_sup [rule_format]:
    1.23    "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.24  apply (simp add: sup_PTS_eq approx_val_def split: err.split)
    1.25  apply (blast intro: conf_widen)
    1.26 @@ -128,7 +128,7 @@
    1.27    "approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)"
    1.28  by (simp add: approx_loc_def)
    1.29  
    1.30 -lemma assConv_approx_stk_imp_approx_loc [rulified]:
    1.31 +lemma assConv_approx_stk_imp_approx_loc [rule_format]:
    1.32    "wf_prog wt G \<Longrightarrow> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) 
    1.33    \<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp s tys_n \<longrightarrow> 
    1.34    approx_loc G hp s (map Ok ts)"
    1.35 @@ -139,7 +139,7 @@
    1.36  .
    1.37  
    1.38  
    1.39 -lemma approx_loc_imp_approx_loc_sup_heap [rulified]:
    1.40 +lemma approx_loc_imp_approx_loc_sup_heap [rule_format]:
    1.41    "\<forall>lvars. approx_loc G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_loc G hp' lvars lt"
    1.42  apply (unfold approx_loc_def list_all2_def)
    1.43  apply (cases lt)
    1.44 @@ -149,7 +149,7 @@
    1.45  apply auto
    1.46  .
    1.47  
    1.48 -lemma approx_loc_imp_approx_loc_sup [rulified]:
    1.49 +lemma approx_loc_imp_approx_loc_sup [rule_format]:
    1.50    "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.51  apply (unfold sup_loc_def approx_loc_def list_all2_def)
    1.52  apply (auto simp add: all_set_conv_all_nth)
    1.53 @@ -157,7 +157,7 @@
    1.54  .
    1.55  
    1.56  
    1.57 -lemma approx_loc_imp_approx_loc_subst [rulified]:
    1.58 +lemma approx_loc_imp_approx_loc_subst [rule_format]:
    1.59    "\<forall>loc idx x X. (approx_loc G hp loc LT) \<longrightarrow> (approx_val G hp x X) 
    1.60    \<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
    1.61  apply (unfold approx_loc_def list_all2_def)
    1.62 @@ -167,7 +167,7 @@
    1.63  
    1.64  lemmas [cong] = conj_cong 
    1.65  
    1.66 -lemma approx_loc_append [rulified]:
    1.67 +lemma approx_loc_append [rule_format]:
    1.68    "\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow> 
    1.69    approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
    1.70  apply (unfold approx_loc_def list_all2_def)
    1.71 @@ -191,11 +191,11 @@
    1.72  by (auto intro: subst [OF approx_stk_rev_lem])
    1.73  
    1.74  
    1.75 -lemma approx_stk_imp_approx_stk_sup_heap [rulified]:
    1.76 +lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
    1.77    "\<forall>lvars. approx_stk G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_stk G hp' lvars lt"
    1.78  by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
    1.79  
    1.80 -lemma approx_stk_imp_approx_stk_sup [rulified]:
    1.81 +lemma approx_stk_imp_approx_stk_sup [rule_format]:
    1.82    "wf_prog wt G \<Longrightarrow> approx_stk G hp lvars st \<longrightarrow> (G \<turnstile> map Ok st <=l (map Ok st')) 
    1.83    \<longrightarrow> approx_stk G hp lvars st'" 
    1.84  by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
    1.85 @@ -232,13 +232,13 @@
    1.86  .
    1.87  
    1.88  
    1.89 -lemma oconf_imp_oconf_field_update [rulified]:
    1.90 +lemma oconf_imp_oconf_field_update [rule_format]:
    1.91    "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v\<Colon>\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
    1.92    \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
    1.93  by (simp add: oconf_def lconf_def)
    1.94  
    1.95  
    1.96 -lemma oconf_imp_oconf_heap_newref [rulified]:
    1.97 +lemma oconf_imp_oconf_heap_newref [rule_format]:
    1.98  "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.99  apply (unfold oconf_def lconf_def)
   1.100  apply simp
   1.101 @@ -246,7 +246,7 @@
   1.102  .
   1.103  
   1.104  
   1.105 -lemma oconf_imp_oconf_heap_update [rulified]:
   1.106 +lemma oconf_imp_oconf_heap_update [rule_format]:
   1.107    "hp a = Some obj' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd> 
   1.108    \<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
   1.109  apply (unfold oconf_def lconf_def)
   1.110 @@ -258,13 +258,13 @@
   1.111  (** hconf **)
   1.112  
   1.113  
   1.114 -lemma hconf_imp_hconf_newref [rulified]:
   1.115 +lemma hconf_imp_hconf_newref [rule_format]:
   1.116    "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.117  apply (simp add: hconf_def)
   1.118  apply (fast intro: oconf_imp_oconf_heap_newref)
   1.119  .
   1.120  
   1.121 -lemma hconf_imp_hconf_field_update [rulified]:
   1.122 +lemma hconf_imp_hconf_field_update [rule_format]:
   1.123    "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> 
   1.124    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.125  apply (simp add: hconf_def)
   1.126 @@ -276,7 +276,7 @@
   1.127  
   1.128  lemmas [simp del] = fun_upd_apply
   1.129  
   1.130 -lemma correct_frames_imp_correct_frames_field_update [rulified]:
   1.131 +lemma correct_frames_imp_correct_frames_field_update [rule_format]:
   1.132    "\<forall>rT C sig. correct_frames G hp phi rT sig frs \<longrightarrow> 
   1.133    hp a = Some (C,od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
   1.134    G,hp\<turnstile>v\<Colon>\<preceq>fd 
   1.135 @@ -299,7 +299,7 @@
   1.136  apply simp
   1.137  .
   1.138  
   1.139 -lemma correct_frames_imp_correct_frames_newref [rulified]:
   1.140 +lemma correct_frames_imp_correct_frames_newref [rule_format]:
   1.141    "\<forall>rT C sig. hp x = None \<longrightarrow> correct_frames G hp phi rT sig frs \<and> oconf G hp obj 
   1.142    \<longrightarrow> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
   1.143  apply (induct frs)