stronger strong soundness
authorkleing
Tue Jun 11 22:53:19 2002 +0200 (2002-06-11)
changeset 13209e62a6bd3f085
parent 13208 965f95a3abd9
child 13210 254b3967ac12
stronger strong soundness
src/HOL/MicroJava/BV/LBVCorrect.thy
     1.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Jun 11 16:43:17 2002 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Jun 11 22:53:19 2002 +0200
     1.3 @@ -177,7 +177,7 @@
     1.4    assumes "wtl ins c 0 s0 \<noteq> \<top>" 
     1.5    assumes "s0 \<in> A" 
     1.6    assumes "0 < length ins"
     1.7 -  shows "\<exists>ts. wt_step r \<top> step ts \<and> s0 <=_r ts!0"
     1.8 +  shows "\<exists>ts. wt_step r \<top> step ts \<and> s0 <=_r ts!0 \<and> size ts = size ins"
     1.9  proof -  
    1.10    have "wt_step r \<top> step \<phi>"
    1.11    proof (unfold wt_step_def, intro strip conjI)
    1.12 @@ -188,6 +188,8 @@
    1.13    qed
    1.14    moreover
    1.15    have "s0 <=_r \<phi>!0" by (rule phi0)
    1.16 +  moreover
    1.17 +  have "size \<phi> = size ins" by simp
    1.18    ultimately
    1.19    show ?thesis by fast
    1.20  qed