--- a/src/HOL/MicroJava/BV/Correct.ML Thu Nov 18 12:12:39 1999 +0100
+++ b/src/HOL/MicroJava/BV/Correct.ML Fri Nov 19 16:30:52 1999 +0100
@@ -62,14 +62,14 @@
Goal
-"wf_prog wt G \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us' >= us \\<longrightarrow> approx_val G h val us'";
+"wf_prog wt G \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us <=o us' \\<longrightarrow> approx_val G h val us'";
by (asm_simp_tac (simpset() addsimps [sup_PTS_eq,approx_val_def] addsplits [option.split,val_.split,ty.split]) 1);
by(blast_tac (claset() addIs [conf_widen]) 1);
qed_spec_mp "approx_val_imp_approx_val_sup";
Goal
-"\\<lbrakk> wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\<turnstile> at >= LT ! idx \\<rbrakk> \
+"\\<lbrakk> wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\<turnstile> LT ! idx <=o at\\<rbrakk> \
\\\<Longrightarrow> approx_val G hp val at";
by (fast_tac (claset() addIs [approx_val_imp_approx_val_sup] addss (simpset() addsimps
[split_def,approx_loc_def,all_set_conv_all_nth])) 1);
@@ -104,7 +104,7 @@
Goalw [sup_loc_def,approx_loc_def]
-"wf_prog wt G \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt' >>= lt \\<longrightarrow> approx_loc G hp lvars lt'";
+"wf_prog wt G \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt <=l lt' \\<longrightarrow> approx_loc G hp lvars lt'";
by (auto_tac (claset() , simpset() addsimps [all_set_conv_all_nth,split_def]));
by (auto_tac (claset() addEs [approx_val_imp_approx_val_sup] , simpset()));
qed_spec_mp "approx_loc_imp_approx_loc_sup";
@@ -154,7 +154,7 @@
Goalw [approx_stk_def]
-"wf_prog wt G \\<Longrightarrow> approx_stk G hp lvars st \\<longrightarrow> G \\<turnstile> (map Some st') >>= (map Some st) \\<longrightarrow> approx_stk G hp lvars st'";
+"wf_prog wt G \\<Longrightarrow> approx_stk G hp lvars st \\<longrightarrow> G \\<turnstile> (map Some st) <=l (map Some st') \\<longrightarrow> approx_stk G hp lvars st'";
by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup]) 1);
qed_spec_mp "approx_stk_imp_approx_stk_sup";