included strong soundness (sound + s0 <= phi!0)
authorkleing
Tue Jun 11 12:35:33 2002 +0200 (2002-06-11)
changeset 132070d07e49dc9a5
parent 13206 90e5852e55e6
child 13208 965f95a3abd9
included strong soundness (sound + s0 <= phi!0)
src/HOL/MicroJava/BV/LBVCorrect.thy
     1.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Jun 06 15:34:52 2002 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Jun 11 12:35:33 2002 +0200
     1.3 @@ -133,12 +133,51 @@
     1.4    also from wtl have "\<dots> \<noteq> \<top>" by (rule wtl_take)
     1.5    finally show ?thesis .
     1.6  qed
     1.7 -    
     1.8 +
     1.9 +
    1.10 +lemma (in lbvs) phi0:
    1.11 +  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
    1.12 +  assumes 0:   "0 < length ins"
    1.13 +  shows "s0 <=_r \<phi>!0"
    1.14 +proof (cases "c!0 = \<bottom>")
    1.15 +  case True
    1.16 +  with 0 have "\<phi>!0 = wtl (take 0 ins) c 0 s0" ..
    1.17 +  moreover have "wtl (take 0 ins) c 0 s0 = s0" by simp
    1.18 +  ultimately have "\<phi>!0 = s0" by simp
    1.19 +  thus ?thesis by simp
    1.20 +next
    1.21 +  case False
    1.22 +  with 0 have "phi!0 = c!0" ..
    1.23 +  moreover 
    1.24 +  have "wtl (take 1 ins) c 0 s0 \<noteq> \<top>"  by (rule wtl_take)
    1.25 +  with 0 False 
    1.26 +  have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: split_if_asm)
    1.27 +  ultimately
    1.28 +  show ?thesis by simp
    1.29 +qed
    1.30 +
    1.31  
    1.32  theorem (in lbvs) wtl_sound:
    1.33    assumes "wtl ins c 0 s0 \<noteq> \<top>" 
    1.34    assumes "s0 \<in> A" 
    1.35    shows "\<exists>ts. wt_step r \<top> step ts"
    1.36 +proof -
    1.37 +  have "wt_step r \<top> step \<phi>"
    1.38 +  proof (unfold wt_step_def, intro strip conjI)
    1.39 +    fix pc assume "pc < length \<phi>"
    1.40 +    then obtain "pc < length ins" by simp
    1.41 +    show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
    1.42 +    show "stable r step \<phi> pc" by (rule wtl_stable)
    1.43 +  qed
    1.44 +  thus ?thesis ..
    1.45 +qed
    1.46 +
    1.47 +
    1.48 +theorem (in lbvs) wtl_sound_strong:
    1.49 +  assumes "wtl ins c 0 s0 \<noteq> \<top>" 
    1.50 +  assumes "s0 \<in> A" 
    1.51 +  assumes "0 < length ins"
    1.52 +  shows "\<exists>ts. wt_step r \<top> step ts \<and> s0 <=_r ts!0"
    1.53  proof -  
    1.54    have "wt_step r \<top> step \<phi>"
    1.55    proof (unfold wt_step_def, intro strip conjI)
    1.56 @@ -146,8 +185,11 @@
    1.57      then obtain "pc < length ins" by simp
    1.58      show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
    1.59      show "stable r step \<phi> pc" by (rule wtl_stable)
    1.60 -  qed    
    1.61 -  thus ?thesis .. 
    1.62 +  qed
    1.63 +  moreover
    1.64 +  have "s0 <=_r \<phi>!0" by (rule phi0)
    1.65 +  ultimately
    1.66 +  show ?thesis by fast
    1.67  qed
    1.68  
    1.69  end
    1.70 \ No newline at end of file