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

src/HOL/MicroJava/BV/LBVCorrect.thy

author | webertj |

Mon Mar 07 19:30:53 2005 +0100 (2005-03-07) | |

changeset 15584 | 3478bb4f93ff |

parent 15425 | 6356d2523f73 |

child 16417 | 9bc16273c2d4 |

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

refute_params: default value itself=1 added (for type classes)

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 (open) lbvs = lbv +

12 fixes s0 :: 'a ("s\<^sub>0")

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 s\<^sub>0 \<noteq> \<top>"

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

41 shows "wtl (take (pc+1) ins) c 0 s0 \<le>\<^sub>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

137 lemma (in lbvs) phi_in_A:

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

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

140 shows "\<phi> \<in> list (length ins) A"

141 proof -

142 { fix x assume "x \<in> set \<phi>"

143 then obtain xs ys where "\<phi> = xs @ x # ys"

144 by (auto simp add: in_set_conv_decomp)

145 then obtain pc where pc: "pc < length \<phi>" and x: "\<phi>!pc = x"

146 by (simp add: that [of "length xs"] nth_append)

148 from wtl s0 pc

149 have "wtl (take pc ins) c 0 s0 \<in> A" by (auto intro!: wtl_pres)

150 moreover

151 from pc have "pc < length ins" by simp

152 with cert have "c!pc \<in> A" ..

153 ultimately

154 have "\<phi>!pc \<in> A" using pc by (simp add: phi_def)

155 hence "x \<in> A" using x by simp

156 }

157 hence "set \<phi> \<subseteq> A" ..

158 thus ?thesis by (unfold list_def) simp

159 qed

162 lemma (in lbvs) phi0:

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

164 assumes 0: "0 < length ins"

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

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

167 case True

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

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

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

171 thus ?thesis by simp

172 next

173 case False

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

175 moreover

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

177 with 0 False

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

179 ultimately

180 show ?thesis by simp

181 qed

184 theorem (in lbvs) wtl_sound:

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

186 assumes "s0 \<in> A"

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

188 proof -

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

190 proof (unfold wt_step_def, intro strip conjI)

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

192 then obtain "pc < length ins" by simp

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

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

195 qed

196 thus ?thesis ..

197 qed

200 theorem (in lbvs) wtl_sound_strong:

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

202 assumes "s0 \<in> A"

203 assumes "0 < length ins"

204 shows "\<exists>ts \<in> list (length ins) A. wt_step r \<top> step ts \<and> s0 <=_r ts!0"

205 proof -

206 have "\<phi> \<in> list (length ins) A" by (rule phi_in_A)

207 moreover

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

209 proof (unfold wt_step_def, intro strip conjI)

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

211 then obtain "pc < length ins" by simp

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

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

214 qed

215 moreover

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

217 ultimately

218 show ?thesis by fast

219 qed

221 end