# HG changeset patch
# User kleing
# Date 1023828799 -7200
# Node ID e62a6bd3f08526c9da01263dc8fc1049e84340d3
# Parent  965f95a3abd9f0ca3bb821bea21e3e720b1bee18
stronger strong soundness

diff -r 965f95a3abd9 -r e62a6bd3f085 src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Jun 11 16:43:17 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Jun 11 22:53:19 2002 +0200
@@ -177,7 +177,7 @@
   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"
+  shows "\<exists>ts. wt_step r \<top> step ts \<and> s0 <=_r ts!0 \<and> size ts = size ins"
 proof -  
   have "wt_step r \<top> step \<phi>"
   proof (unfold wt_step_def, intro strip conjI)
@@ -188,6 +188,8 @@
   qed
   moreover
   have "s0 <=_r \<phi>!0" by (rule phi0)
+  moreover
+  have "size \<phi> = size ins" by simp
   ultimately
   show ?thesis by fast
 qed