author | kleing |

Tue Jun 11 12:35:33 2002 +0200 (2002-06-11) | |

changeset 13207 | 0d07e49dc9a5 |

parent 13206 | 90e5852e55e6 |

child 13208 | 965f95a3abd9 |

included strong soundness (sound + s0 <= phi!0)

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