# HG changeset patch
# User kleing
# Date 1023791733 7200
# Node ID 0d07e49dc9a5d2a4385664d29921c143a33b1ffb
# Parent 90e5852e55e6ab9a0556aef849c52bdb9e999ab9
included strong soundness (sound + s0 <= phi!0)
diff r 90e5852e55e6 r 0d07e49dc9a5 src/HOL/MicroJava/BV/LBVCorrect.thy
 a/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Jun 06 15:34:52 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Tue Jun 11 12:35:33 2002 +0200
@@ 133,12 +133,51 @@
also from wtl have "\ \ \" by (rule wtl_take)
finally show ?thesis .
qed

+
+
+lemma (in lbvs) phi0:
+ assumes wtl: "wtl ins c 0 s0 \ \"
+ assumes 0: "0 < length ins"
+ shows "s0 <=_r \!0"
+proof (cases "c!0 = \")
+ case True
+ with 0 have "\!0 = wtl (take 0 ins) c 0 s0" ..
+ moreover have "wtl (take 0 ins) c 0 s0 = s0" by simp
+ ultimately have "\!0 = s0" by simp
+ thus ?thesis by simp
+next
+ case False
+ with 0 have "phi!0 = c!0" ..
+ moreover
+ have "wtl (take 1 ins) c 0 s0 \ \" by (rule wtl_take)
+ with 0 False
+ have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: split_if_asm)
+ ultimately
+ show ?thesis by simp
+qed
+
theorem (in lbvs) wtl_sound:
assumes "wtl ins c 0 s0 \ \"
assumes "s0 \ A"
shows "\ts. wt_step r \ step ts"
+proof 
+ have "wt_step r \ step \"
+ proof (unfold wt_step_def, intro strip conjI)
+ fix pc assume "pc < length \"
+ then obtain "pc < length ins" by simp
+ show "\!pc \ \" by (rule phi_not_top)
+ show "stable r step \ pc" by (rule wtl_stable)
+ qed
+ thus ?thesis ..
+qed
+
+
+theorem (in lbvs) wtl_sound_strong:
+ assumes "wtl ins c 0 s0 \ \"
+ assumes "s0 \ A"
+ assumes "0 < length ins"
+ shows "\ts. wt_step r \ step ts \ s0 <=_r ts!0"
proof 
have "wt_step r \ step \"
proof (unfold wt_step_def, intro strip conjI)
@@ 146,8 +185,11 @@
then obtain "pc < length ins" by simp
show "\!pc \ \" by (rule phi_not_top)
show "stable r step \ pc" by (rule wtl_stable)
 qed
 thus ?thesis ..
+ qed
+ moreover
+ have "s0 <=_r \!0" by (rule phi0)
+ ultimately
+ show ?thesis by fast
qed
end
\ No newline at end of file