--- a/src/HOL/MicroJava/BV/Correct.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Thu Sep 07 21:10:11 2000 +0200
@@ -92,11 +92,11 @@
"approx_val G hp Null (Ok (RefT x))"
by (auto intro: null simp add: approx_val_def)
-lemma approx_val_imp_approx_val_assConvertible [rulify]:
+lemma approx_val_imp_approx_val_assConvertible [rulified]:
"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')"
by (cases T) (auto intro: conf_widen simp add: approx_val_def)
-lemma approx_val_imp_approx_val_sup_heap [rulify]:
+lemma approx_val_imp_approx_val_sup_heap [rulified]:
"approx_val G hp v at \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_val G hp' v at"
apply (simp add: approx_val_def split: err.split)
apply (blast intro: conf_hext)
@@ -107,7 +107,7 @@
\<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v\<Colon>\<preceq>T"
by (cases v, auto simp add: obj_ty_def conf_def)
-lemma approx_val_imp_approx_val_sup [rulify]:
+lemma approx_val_imp_approx_val_sup [rulified]:
"wf_prog wt G \<Longrightarrow> (approx_val G h v us) \<longrightarrow> (G \<turnstile> us <=o us') \<longrightarrow> (approx_val G h v us')"
apply (simp add: sup_PTS_eq approx_val_def split: err.split)
apply (blast intro: conf_widen)
@@ -128,7 +128,7 @@
"approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)"
by (simp add: approx_loc_def)
-lemma assConv_approx_stk_imp_approx_loc [rulify]:
+lemma assConv_approx_stk_imp_approx_loc [rulified]:
"wf_prog wt G \<Longrightarrow> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G)
\<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp s tys_n \<longrightarrow>
approx_loc G hp s (map Ok ts)"
@@ -139,7 +139,7 @@
.
-lemma approx_loc_imp_approx_loc_sup_heap [rulify]:
+lemma approx_loc_imp_approx_loc_sup_heap [rulified]:
"\<forall>lvars. approx_loc G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_loc G hp' lvars lt"
apply (unfold approx_loc_def list_all2_def)
apply (cases lt)
@@ -149,7 +149,7 @@
apply auto
.
-lemma approx_loc_imp_approx_loc_sup [rulify]:
+lemma approx_loc_imp_approx_loc_sup [rulified]:
"wf_prog wt G \<Longrightarrow> approx_loc G hp lvars lt \<longrightarrow> G \<turnstile> lt <=l lt' \<longrightarrow> approx_loc G hp lvars lt'"
apply (unfold sup_loc_def approx_loc_def list_all2_def)
apply (auto simp add: all_set_conv_all_nth)
@@ -157,7 +157,7 @@
.
-lemma approx_loc_imp_approx_loc_subst [rulify]:
+lemma approx_loc_imp_approx_loc_subst [rulified]:
"\<forall>loc idx x X. (approx_loc G hp loc LT) \<longrightarrow> (approx_val G hp x X)
\<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
apply (unfold approx_loc_def list_all2_def)
@@ -167,7 +167,7 @@
lemmas [cong] = conj_cong
-lemma approx_loc_append [rulify]:
+lemma approx_loc_append [rulified]:
"\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow>
approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
apply (unfold approx_loc_def list_all2_def)
@@ -191,11 +191,11 @@
by (auto intro: subst [OF approx_stk_rev_lem])
-lemma approx_stk_imp_approx_stk_sup_heap [rulify]:
+lemma approx_stk_imp_approx_stk_sup_heap [rulified]:
"\<forall>lvars. approx_stk G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_stk G hp' lvars lt"
by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
-lemma approx_stk_imp_approx_stk_sup [rulify]:
+lemma approx_stk_imp_approx_stk_sup [rulified]:
"wf_prog wt G \<Longrightarrow> approx_stk G hp lvars st \<longrightarrow> (G \<turnstile> map Ok st <=l (map Ok st'))
\<longrightarrow> approx_stk G hp lvars st'"
by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
@@ -232,13 +232,13 @@
.
-lemma oconf_imp_oconf_field_update [rulify]:
+lemma oconf_imp_oconf_field_update [rulified]:
"\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v\<Colon>\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
\<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
by (simp add: oconf_def lconf_def)
-lemma oconf_imp_oconf_heap_newref [rulify]:
+lemma oconf_imp_oconf_heap_newref [rulified]:
"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>"
apply (unfold oconf_def lconf_def)
apply simp
@@ -246,7 +246,7 @@
.
-lemma oconf_imp_oconf_heap_update [rulify]:
+lemma oconf_imp_oconf_heap_update [rulified]:
"hp a = Some obj' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd>
\<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
apply (unfold oconf_def lconf_def)
@@ -258,13 +258,13 @@
(** hconf **)
-lemma hconf_imp_hconf_newref [rulify]:
+lemma hconf_imp_hconf_newref [rulified]:
"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>"
apply (simp add: hconf_def)
apply (fast intro: oconf_imp_oconf_heap_newref)
.
-lemma hconf_imp_hconf_field_update [rulify]:
+lemma hconf_imp_hconf_field_update [rulified]:
"map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and>
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>"
apply (simp add: hconf_def)
@@ -276,7 +276,7 @@
lemmas [simp del] = fun_upd_apply
-lemma correct_frames_imp_correct_frames_field_update [rulify]:
+lemma correct_frames_imp_correct_frames_field_update [rulified]:
"\<forall>rT C sig. correct_frames G hp phi rT sig frs \<longrightarrow>
hp a = Some (C,od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow>
G,hp\<turnstile>v\<Colon>\<preceq>fd
@@ -299,7 +299,7 @@
apply simp
.
-lemma correct_frames_imp_correct_frames_newref [rulify]:
+lemma correct_frames_imp_correct_frames_newref [rulified]:
"\<forall>rT C sig. hp x = None \<longrightarrow> correct_frames G hp phi rT sig frs \<and> oconf G hp obj
\<longrightarrow> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
apply (induct frs)