author  ballarin 
Fri, 29 Aug 2003 15:19:02 +0200  
changeset 14174  f3cafd2929d5 
parent 12934  6003b4f916c0 
child 14565  c6dc17aab88a 
permissions  rwrr 
11376  1 
(* Title: HOL/NanoJava/Equivalence.thy 
2 
ID: $Id$ 

3 
Author: David von Oheimb 

4 
Copyright 2001 Technische Universitaet Muenchen 

5 
*) 

6 

7 
header "Equivalence of Operational and Axiomatic Semantics" 

8 

9 
theory Equivalence = OpSem + AxSem: 

10 

11 
subsection "Validity" 

12 

13 
constdefs 

11476  14 
valid :: "[assn,stmt, assn] => bool" ("= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) 
15 
"= {P} c {Q} \<equiv> \<forall>s t. P s > (\<exists>n. s c n> t) > Q t" 

16 

17 
evalid :: "[assn,expr,vassn] => bool" ("=e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) 

18 
"=e {P} e {Q} \<equiv> \<forall>s v t. P s > (\<exists>n. s e>vn> t) > Q v t" 

19 

11376  20 

11476  21 
nvalid :: "[nat, triple ] => bool" ("=_: _" [61,61] 60) 
22 
"=n: t \<equiv> let (P,c,Q) = t in \<forall>s t. s c n> t > P s > Q t" 

11376  23 

11476  24 
envalid :: "[nat,etriple ] => bool" ("=_:e _" [61,61] 60) 
25 
"=n:e t \<equiv> let (P,e,Q) = t in \<forall>s v t. s e>vn> t > P s > Q v t" 

26 

27 
nvalids :: "[nat, triple set] => bool" ("=_: _" [61,61] 60) 

11376  28 
"=n: T \<equiv> \<forall>t\<in>T. =n: t" 
29 

11476  30 
cnvalids :: "[triple set,triple set] => bool" ("_ =/ _" [61,61] 60) 
31 
"A = C \<equiv> \<forall>n. =n: A > =n: C" 

32 

33 
cenvalid :: "[triple set,etriple ] => bool" ("_ =e/ _" [61,61] 60) 

34 
"A =e t \<equiv> \<forall>n. =n: A > =n:e t" 

11376  35 

36 
syntax (xsymbols) 

11476  37 
valid :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) 
11486  38 
evalid :: "[assn,expr,vassn] => bool" ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) 
11476  39 
nvalid :: "[nat, triple ] => bool" ("\<Turnstile>_: _" [61,61] 60) 
11486  40 
envalid :: "[nat,etriple ] => bool" ("\<Turnstile>_:\<^sub>e _" [61,61] 60) 
11476  41 
nvalids :: "[nat, triple set] => bool" ("\<Turnstile>_: _" [61,61] 60) 
11376  42 
cnvalids :: "[triple set,triple set] => bool" ("_ \<Turnstile>/ _" [61,61] 60) 
11486  43 
cenvalid :: "[triple set,etriple ] => bool" ("_ \<Turnstile>\<^sub>e/ _"[61,61] 60) 
11376  44 

45 

11476  46 
lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s cn\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t" 
11376  47 
by (simp add: nvalid_def Let_def) 
48 

11476  49 
lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n: (P,c,Q))" 
50 
apply (simp add: valid_def nvalid_def2) 

11376  51 
apply blast 
52 
done 

53 

11486  54 
lemma envalid_def2: "\<Turnstile>n:\<^sub>e (P,e,Q) \<equiv> \<forall>s v t. s e\<succ>vn\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t" 
11476  55 
by (simp add: envalid_def Let_def) 
56 

11486  57 
lemma evalid_def2: "\<Turnstile>\<^sub>e {P} e {Q} = (\<forall>n. \<Turnstile>n:\<^sub>e (P,e,Q))" 
11476  58 
apply (simp add: evalid_def envalid_def2) 
59 
apply blast 

60 
done 

61 

62 
lemma cenvalid_def2: 

11486  63 
"A\<Turnstile>\<^sub>e (P,e,Q) = (\<forall>n. \<Turnstile>n: A \<longrightarrow> (\<forall>s v t. s e\<succ>vn\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t))" 
11476  64 
by(simp add: cenvalid_def envalid_def2) 
65 

11376  66 

67 
subsection "Soundness" 

68 

11476  69 
declare exec_elim_cases [elim!] eval_elim_cases [elim!] 
11376  70 

11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

71 
lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl M,Q)" 
11476  72 
by (clarsimp simp add: nvalid_def2) 
11376  73 

11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

74 
lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body M,Q) \<Longrightarrow> \<Turnstile>Suc n: (P,Impl M,Q)" 
11476  75 
by (clarsimp simp add: nvalid_def2) 
11376  76 

77 
lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t" 

11476  78 
by (force simp add: split_paired_all nvalid_def2 intro: exec_mono) 
11376  79 

80 
lemma nvalids_SucD: "Ball A (nvalid (Suc n)) \<Longrightarrow> Ball A (nvalid n)" 

81 
by (fast intro: nvalid_SucD) 

82 

83 
lemma Loop_sound_lemma [rule_format (no_asm)]: 

11476  84 
"\<forall>s t. s cn\<rightarrow> t \<longrightarrow> P s \<and> s<x> \<noteq> Null \<longrightarrow> P t \<Longrightarrow> 
85 
(s c0n0\<rightarrow> t \<longrightarrow> P s \<longrightarrow> c0 = While (x) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<x> = Null)" 

14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
12934
diff
changeset

86 
apply (rule_tac ?P2.1="%s e v n t. True" in exec_eval.induct [THEN conjunct1]) 
11376  87 
apply clarsimp+ 
88 
done 

89 

90 
lemma Impl_sound_lemma: 

11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

91 
"\<lbrakk>\<forall>z n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (f z ` Ms) (nvalid n); 
12742  92 
Cm\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z Cm)" 
11376  93 
by blast 
94 

11476  95 
lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l" 
96 
by fast 

97 

98 
lemma all3_conjunct2: 

99 
"\<forall>a p l. (P' a p l \<and> P a p l) \<Longrightarrow> \<forall>a p l. P a p l" 

100 
by fast 

101 

102 
lemma cnvalid1_eq: 

103 
"A \<Turnstile> {(P,c,Q)} \<equiv> \<forall>n. \<Turnstile>n: A \<longrightarrow> (\<forall>s t. s cn\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)" 

104 
by(simp add: cnvalids_def nvalids_def nvalid_def2) 

105 

11486  106 
lemma hoare_sound_main:"\<And>t. (A \<turnstile> C \<longrightarrow> A \<Turnstile> C) \<and> (A \<turnstile>\<^sub>e t \<longrightarrow> A \<Turnstile>\<^sub>e t)" 
11476  107 
apply (tactic "split_all_tac 1", rename_tac P e Q) 
108 
apply (rule hoare_ehoare.induct) 

12524
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

109 
(*18*) 
11476  110 
apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *}) 
111 
apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : hoare") *}) 

112 
apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : ehoare") *}) 

113 
apply (simp_all only: cnvalid1_eq cenvalid_def2) 

12524
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

114 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

115 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

116 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

117 
apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

118 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

119 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

120 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

121 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

122 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

123 
apply fast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

124 
apply (clarsimp del: Meth_elim_cases) (* Call *) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

125 
apply (force del: Impl_elim_cases) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

126 
defer 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

127 
prefer 4 apply blast (* Conseq *) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

128 
prefer 4 apply blast (* eConseq *) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

129 
apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def) 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

130 
apply blast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

131 
apply blast 
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

132 
apply blast 
11376  133 
apply (rule allI) 
11565  134 
apply (rule_tac x=Z in spec) 
11376  135 
apply (induct_tac "n") 
12524
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

136 
apply (clarify intro!: Impl_nvalid_0) 
11376  137 
apply (clarify intro!: Impl_nvalid_Suc) 
138 
apply (drule nvalids_SucD) 

11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

139 
apply (simp only: all_simps) 
11376  140 
apply (erule (1) impE) 
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

141 
apply (drule (2) Impl_sound_lemma) 
12524
66eb843b1d35
mods due to mor powerful simprocs for 1point rules (quantifier1).
nipkow
parents:
11565
diff
changeset

142 
apply blast 
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

143 
apply assumption 
11376  144 
done 
145 

146 
theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}" 

147 
apply (simp only: valid_def2) 

11476  148 
apply (drule hoare_sound_main [THEN conjunct1, rule_format]) 
11376  149 
apply (unfold cnvalids_def nvalids_def) 
150 
apply fast 

151 
done 

152 

11486  153 
theorem ehoare_sound: "{} \<turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q}" 
11476  154 
apply (simp only: evalid_def2) 
155 
apply (drule hoare_sound_main [THEN conjunct2, rule_format]) 

156 
apply (unfold cenvalid_def nvalids_def) 

157 
apply fast 

158 
done 

159 

11376  160 

161 
subsection "(Relative) Completeness" 

162 

11476  163 
constdefs MGT :: "stmt => state => triple" 
11565  164 
"MGT c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda> t. \<exists>n. Z c n> t)" 
11486  165 
MGTe :: "expr => state => etriple" 
11565  166 
"MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z e>vn> t)" 
11486  167 
syntax (xsymbols) 
168 
MGTe :: "expr => state => etriple" ("MGT\<^sub>e") 

11376  169 

170 
lemma MGF_implies_complete: 

11565  171 
"\<forall>Z. {} \<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}" 
11376  172 
apply (simp only: valid_def2) 
173 
apply (unfold MGT_def) 

11476  174 
apply (erule hoare_ehoare.Conseq) 
175 
apply (clarsimp simp add: nvalid_def2) 

11376  176 
done 
177 

11476  178 
lemma eMGF_implies_complete: 
11565  179 
"\<forall>Z. {} \<turnstile>\<^sub>e MGT\<^sub>e e Z \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}" 
11476  180 
apply (simp only: evalid_def2) 
11486  181 
apply (unfold MGTe_def) 
11476  182 
apply (erule hoare_ehoare.eConseq) 
183 
apply (clarsimp simp add: envalid_def2) 

184 
done 

11376  185 

11476  186 
declare exec_eval.intros[intro!] 
11376  187 

11565  188 
lemma MGF_Loop: "\<forall>Z. A \<turnstile> {op = Z} c {\<lambda>t. \<exists>n. Z cn\<rightarrow> t} \<Longrightarrow> 
189 
A \<turnstile> {op = Z} While (x) c {\<lambda>t. \<exists>n. Z While (x) cn\<rightarrow> t}" 

190 
apply (rule_tac P' = "\<lambda>Z s. (Z,s) \<in> ({(s,t). \<exists>n. s<x> \<noteq> Null \<and> s cn\<rightarrow> t})^*" 

11476  191 
in hoare_ehoare.Conseq) 
11376  192 
apply (rule allI) 
11476  193 
apply (rule hoare_ehoare.Loop) 
194 
apply (erule hoare_ehoare.Conseq) 

11376  195 
apply clarsimp 
196 
apply (blast intro:rtrancl_into_rtrancl) 

197 
apply (erule thin_rl) 

198 
apply clarsimp 

11565  199 
apply (erule_tac x = Z in allE) 
11376  200 
apply clarsimp 
201 
apply (erule converse_rtrancl_induct) 

202 
apply blast 

203 
apply clarsimp 

11476  204 
apply (drule (1) exec_exec_max) 
11376  205 
apply (blast del: exec_elim_cases) 
206 
done 

207 

11565  208 
lemma MGF_lemma: "\<forall>M Z. A \<turnstile> {MGT (Impl M) Z} \<Longrightarrow> 
209 
(\<forall>Z. A \<turnstile> {MGT c Z}) \<and> (\<forall>Z. A \<turnstile>\<^sub>e MGT\<^sub>e e Z)" 

11486  210 
apply (simp add: MGT_def MGTe_def) 
11476  211 
apply (rule stmt_expr.induct) 
212 
apply (rule_tac [!] allI) 

11376  213 

11476  214 
apply (rule Conseq1 [OF hoare_ehoare.Skip]) 
11376  215 
apply blast 
216 

11476  217 
apply (rule hoare_ehoare.Comp) 
11376  218 
apply (erule spec) 
11476  219 
apply (erule hoare_ehoare.Conseq) 
11376  220 
apply clarsimp 
11476  221 
apply (drule (1) exec_exec_max) 
11376  222 
apply blast 
223 

11476  224 
apply (erule thin_rl) 
225 
apply (rule hoare_ehoare.Cond) 

226 
apply (erule spec) 

227 
apply (rule allI) 

228 
apply (simp) 

229 
apply (rule conjI) 

230 
apply (rule impI, erule hoare_ehoare.Conseq, clarsimp, drule (1) eval_exec_max, 

231 
erule thin_rl, erule thin_rl, force)+ 

11376  232 

233 
apply (erule MGF_Loop) 

234 

11476  235 
apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.LAss]) 
236 
apply fast 

11376  237 

11476  238 
apply (erule thin_rl) 
11565  239 
apply (rule_tac Q = "\<lambda>a s. \<exists>n. Z expr1\<succ>Addr an\<rightarrow> s" in hoare_ehoare.FAss) 
11476  240 
apply (drule spec) 
241 
apply (erule eConseq2) 

242 
apply fast 

243 
apply (rule allI) 

244 
apply (erule hoare_ehoare.eConseq) 

245 
apply clarsimp 

246 
apply (drule (1) eval_eval_max) 

11376  247 
apply blast 
248 

11507  249 
apply (simp only: split_paired_all) 
11476  250 
apply (rule hoare_ehoare.Meth) 
11376  251 
apply (rule allI) 
11476  252 
apply (drule spec, drule spec, erule hoare_ehoare.Conseq) 
11376  253 
apply blast 
254 

11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

255 
apply (simp add: split_paired_all) 
11476  256 

257 
apply (rule eConseq1 [OF hoare_ehoare.NewC]) 

258 
apply blast 

259 

260 
apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.Cast]) 

261 
apply fast 

262 

263 
apply (rule eConseq1 [OF hoare_ehoare.LAcc]) 

264 
apply blast 

265 

266 
apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.FAcc]) 

267 
apply fast 

268 

11565  269 
apply (rule_tac R = "\<lambda>a v s. \<exists>n1 n2 t. Z expr1\<succ>an1\<rightarrow> t \<and> t expr2\<succ>vn2\<rightarrow> s" in 
11476  270 
hoare_ehoare.Call) 
271 
apply (erule spec) 

272 
apply (rule allI) 

273 
apply (erule hoare_ehoare.eConseq) 

274 
apply clarsimp 

275 
apply blast 

276 
apply (rule allI)+ 

277 
apply (rule hoare_ehoare.Meth) 

278 
apply (rule allI) 

279 
apply (drule spec, drule spec, erule hoare_ehoare.Conseq) 

280 
apply (erule thin_rl, erule thin_rl) 

281 
apply (clarsimp del: Impl_elim_cases) 

282 
apply (drule (2) eval_eval_exec_max) 

11565  283 
apply (force del: Impl_elim_cases) 
11376  284 
done 
285 

11565  286 
lemma MGF_Impl: "{} \<turnstile> {MGT (Impl M) Z}" 
11376  287 
apply (unfold MGT_def) 
12934
6003b4f916c0
Clarification wrt. use of polymorphic variants of Hoare logic rules
oheimb
parents:
12742
diff
changeset

288 
apply (rule Impl1') 
11376  289 
apply (rule_tac [2] UNIV_I) 
290 
apply clarsimp 

11476  291 
apply (rule hoare_ehoare.ConjI) 
11376  292 
apply clarsimp 
293 
apply (rule ssubst [OF Impl_body_eq]) 

294 
apply (fold MGT_def) 

11476  295 
apply (rule MGF_lemma [THEN conjunct1, rule_format]) 
296 
apply (rule hoare_ehoare.Asm) 

11376  297 
apply force 
298 
done 

299 

300 
theorem hoare_relative_complete: "\<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}" 

301 
apply (rule MGF_implies_complete) 

302 
apply (erule_tac [2] asm_rl) 

303 
apply (rule allI) 

11476  304 
apply (rule MGF_lemma [THEN conjunct1, rule_format]) 
305 
apply (rule MGF_Impl) 

306 
done 

307 

11486  308 
theorem ehoare_relative_complete: "\<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}" 
11476  309 
apply (rule eMGF_implies_complete) 
310 
apply (erule_tac [2] asm_rl) 

311 
apply (rule allI) 

312 
apply (rule MGF_lemma [THEN conjunct2, rule_format]) 

11376  313 
apply (rule MGF_Impl) 
314 
done 

315 

11565  316 
lemma cFalse: "A \<turnstile> {\<lambda>s. False} c {Q}" 
317 
apply (rule cThin) 

318 
apply (rule hoare_relative_complete) 

319 
apply (auto simp add: valid_def) 

320 
done 

321 

322 
lemma eFalse: "A \<turnstile>\<^sub>e {\<lambda>s. False} e {Q}" 

323 
apply (rule eThin) 

324 
apply (rule ehoare_relative_complete) 

325 
apply (auto simp add: evalid_def) 

326 
done 

327 

11376  328 
end 