# 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 "\<dots> \<noteq> \<top>" by (rule wtl_take)
   finally show ?thesis .
 qed
-    
+
+
+lemma (in lbvs) phi0:
+  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
+  assumes 0:   "0 < length ins"
+  shows "s0 <=_r \<phi>!0"
+proof (cases "c!0 = \<bottom>")
+  case True
+  with 0 have "\<phi>!0 = wtl (take 0 ins) c 0 s0" ..
+  moreover have "wtl (take 0 ins) c 0 s0 = s0" by simp
+  ultimately have "\<phi>!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 \<noteq> \<top>"  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 \<noteq> \<top>" 
   assumes "s0 \<in> A" 
   shows "\<exists>ts. wt_step r \<top> step ts"
+proof -
+  have "wt_step r \<top> step \<phi>"
+  proof (unfold wt_step_def, intro strip conjI)
+    fix pc assume "pc < length \<phi>"
+    then obtain "pc < length ins" by simp
+    show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
+    show "stable r step \<phi> pc" by (rule wtl_stable)
+  qed
+  thus ?thesis ..
+qed
+
+
+theorem (in lbvs) wtl_sound_strong:
+  assumes "wtl ins c 0 s0 \<noteq> \<top>" 
+  assumes "s0 \<in> A" 
+  assumes "0 < length ins"
+  shows "\<exists>ts. wt_step r \<top> step ts \<and> s0 <=_r ts!0"
 proof -  
   have "wt_step r \<top> step \<phi>"
   proof (unfold wt_step_def, intro strip conjI)
@@ -146,8 +185,11 @@
     then obtain "pc < length ins" by simp
     show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
     show "stable r step \<phi> pc" by (rule wtl_stable)
-  qed    
-  thus ?thesis .. 
+  qed
+  moreover
+  have "s0 <=_r \<phi>!0" by (rule phi0)
+  ultimately
+  show ?thesis by fast
 qed
 
 end
\ No newline at end of file