summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/MicroJava/BV/LBVCorrect.thy

author | kleing |

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

changeset 13207 | 0d07e49dc9a5 |

parent 13080 | d9feada9c486 |

child 13209 | e62a6bd3f085 |

permissions | -rw-r--r-- |

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

1 (*

2 ID: $Id$

3 Author: Gerwin Klein

4 Copyright 1999 Technische Universitaet Muenchen

5 *)

7 header {* \isaheader{Correctness of the LBV} *}

9 theory LBVCorrect = LBVSpec + Typing_Framework:

11 locale lbvs = lbv +

12 fixes s0 :: 'a

13 fixes c :: "'a list"

14 fixes ins :: "'b list"

15 fixes phi :: "'a list" ("\<phi>")

16 defines phi_def:

17 "\<phi> \<equiv> map (\<lambda>pc. if c!pc = \<bottom> then wtl (take pc ins) c 0 s0 else c!pc)

18 [0..length ins(]"

20 assumes bounded: "bounded step (length ins)"

21 assumes cert: "cert_ok c (length ins) \<top> \<bottom> A"

22 assumes pres: "pres_type step (length ins) A"

25 lemma (in lbvs) phi_None [intro?]:

26 "\<lbrakk> pc < length ins; c!pc = \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = wtl (take pc ins) c 0 s0"

27 by (simp add: phi_def)

29 lemma (in lbvs) phi_Some [intro?]:

30 "\<lbrakk> pc < length ins; c!pc \<noteq> \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = c ! pc"

31 by (simp add: phi_def)

33 lemma (in lbvs) phi_len [simp]:

34 "length \<phi> = length ins"

35 by (simp add: phi_def)

38 lemma (in lbvs) wtl_suc_pc:

39 assumes all: "wtl ins c 0 s0 \<noteq> \<top>"

40 assumes pc: "pc+1 < length ins"

41 shows "wtl (take (pc+1) ins) c 0 s0 <=_r \<phi>!(pc+1)"

42 proof -

43 from all pc

44 have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) \<noteq> T" by (rule wtl_all)

45 with pc show ?thesis by (simp add: phi_def wtc split: split_if_asm)

46 qed

49 lemma (in lbvs) wtl_stable:

50 assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"

51 assumes s0: "s0 \<in> A"

52 assumes pc: "pc < length ins"

53 shows "stable r step \<phi> pc"

54 proof (unfold stable_def, clarify)

55 fix pc' s' assume step: "(pc',s') \<in> set (step pc (\<phi> ! pc))"

56 (is "(pc',s') \<in> set (?step pc)")

58 from bounded pc step have pc': "pc' < length ins" by (rule boundedD)

60 have tkpc: "wtl (take pc ins) c 0 s0 \<noteq> \<top>" (is "?s1 \<noteq> _") by (rule wtl_take)

61 have s2: "wtl (take (pc+1) ins) c 0 s0 \<noteq> \<top>" (is "?s2 \<noteq> _") by (rule wtl_take)

63 from wtl pc have wt_s1: "wtc c pc ?s1 \<noteq> \<top>" by (rule wtl_all)

65 have c_Some: "\<forall>pc t. pc < length ins \<longrightarrow> c!pc \<noteq> \<bottom> \<longrightarrow> \<phi>!pc = c!pc"

66 by (simp add: phi_def)

67 have c_None: "c!pc = \<bottom> \<Longrightarrow> \<phi>!pc = ?s1" ..

69 from wt_s1 pc c_None c_Some

70 have inst: "wtc c pc ?s1 = wti c pc (\<phi>!pc)"

71 by (simp add: wtc split: split_if_asm)

73 have "?s1 \<in> A" by (rule wtl_pres)

74 with pc c_Some cert c_None

75 have "\<phi>!pc \<in> A" by (cases "c!pc = \<bottom>") (auto dest: cert_okD1)

76 with pc pres

77 have step_in_A: "snd`set (?step pc) \<subseteq> A" by (auto dest: pres_typeD2)

79 show "s' <=_r \<phi>!pc'"

80 proof (cases "pc' = pc+1")

81 case True

82 with pc' cert

83 have cert_in_A: "c!(pc+1) \<in> A" by (auto dest: cert_okD1)

84 from True pc' have pc1: "pc+1 < length ins" by simp

85 with tkpc have "?s2 = wtc c pc ?s1" by - (rule wtl_Suc)

86 with inst

87 have merge: "?s2 = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti)

88 also

89 from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp

90 with cert_in_A step_in_A

91 have "?merge = (map snd [(p',t')\<in>?step pc. p'=pc+1] ++_f (c!(pc+1)))"

92 by (rule merge_not_top_s)

93 finally

94 have "s' <=_r ?s2" using step_in_A cert_in_A True step

95 by (auto intro: pp_ub1')

96 also

97 from wtl pc1 have "?s2 <=_r \<phi>!(pc+1)" by (rule wtl_suc_pc)

98 also note True [symmetric]

99 finally show ?thesis by simp

100 next

101 case False

102 from wt_s1 inst

103 have "merge c pc (?step pc) (c!(pc+1)) \<noteq> \<top>" by (simp add: wti)

104 with step_in_A

105 have "\<forall>(pc', s')\<in>set (?step pc). pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'"

106 by - (rule merge_not_top)

107 with step False

108 have ok: "s' <=_r c!pc'" by blast

109 moreover

110 from ok

111 have "c!pc' = \<bottom> \<Longrightarrow> s' = \<bottom>" by simp

112 moreover

113 from c_Some pc'

114 have "c!pc' \<noteq> \<bottom> \<Longrightarrow> \<phi>!pc' = c!pc'" by auto

115 ultimately

116 show ?thesis by (cases "c!pc' = \<bottom>") auto

117 qed

118 qed

121 lemma (in lbvs) phi_not_top:

122 assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"

123 assumes pc: "pc < length ins"

124 shows "\<phi>!pc \<noteq> \<top>"

125 proof (cases "c!pc = \<bottom>")

126 case False with pc

127 have "\<phi>!pc = c!pc" ..

128 also from cert pc have "\<dots> \<noteq> \<top>" by (rule cert_okD4)

129 finally show ?thesis .

130 next

131 case True with pc

132 have "\<phi>!pc = wtl (take pc ins) c 0 s0" ..

133 also from wtl have "\<dots> \<noteq> \<top>" by (rule wtl_take)

134 finally show ?thesis .

135 qed

138 lemma (in lbvs) phi0:

139 assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"

140 assumes 0: "0 < length ins"

141 shows "s0 <=_r \<phi>!0"

142 proof (cases "c!0 = \<bottom>")

143 case True

144 with 0 have "\<phi>!0 = wtl (take 0 ins) c 0 s0" ..

145 moreover have "wtl (take 0 ins) c 0 s0 = s0" by simp

146 ultimately have "\<phi>!0 = s0" by simp

147 thus ?thesis by simp

148 next

149 case False

150 with 0 have "phi!0 = c!0" ..

151 moreover

152 have "wtl (take 1 ins) c 0 s0 \<noteq> \<top>" by (rule wtl_take)

153 with 0 False

154 have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: split_if_asm)

155 ultimately

156 show ?thesis by simp

157 qed

160 theorem (in lbvs) wtl_sound:

161 assumes "wtl ins c 0 s0 \<noteq> \<top>"

162 assumes "s0 \<in> A"

163 shows "\<exists>ts. wt_step r \<top> step ts"

164 proof -

165 have "wt_step r \<top> step \<phi>"

166 proof (unfold wt_step_def, intro strip conjI)

167 fix pc assume "pc < length \<phi>"

168 then obtain "pc < length ins" by simp

169 show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)

170 show "stable r step \<phi> pc" by (rule wtl_stable)

171 qed

172 thus ?thesis ..

173 qed

176 theorem (in lbvs) wtl_sound_strong:

177 assumes "wtl ins c 0 s0 \<noteq> \<top>"

178 assumes "s0 \<in> A"

179 assumes "0 < length ins"

180 shows "\<exists>ts. wt_step r \<top> step ts \<and> s0 <=_r ts!0"

181 proof -

182 have "wt_step r \<top> step \<phi>"

183 proof (unfold wt_step_def, intro strip conjI)

184 fix pc assume "pc < length \<phi>"

185 then obtain "pc < length ins" by simp

186 show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)

187 show "stable r step \<phi> pc" by (rule wtl_stable)

188 qed

189 moreover

190 have "s0 <=_r \<phi>!0" by (rule phi0)

191 ultimately

192 show ?thesis by fast

193 qed

195 end