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>v-n-> 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>v-n-> 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 -c-n\<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>v-n\<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>v-n\<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 |
|
11476
|
71 |
lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl C m,Q)"
|
|
72 |
by (clarsimp simp add: nvalid_def2)
|
11376
|
73 |
|
11476
|
74 |
lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body C m,Q) \<Longrightarrow> \<Turnstile>Suc n: (P,Impl C m,Q)"
|
|
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 -c-n\<rightarrow> t \<longrightarrow> P s \<and> s<x> \<noteq> Null \<longrightarrow> P t \<Longrightarrow>
|
|
85 |
(s -c0-n0\<rightarrow> t \<longrightarrow> P s \<longrightarrow> c0 = While (x) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<x> = Null)"
|
|
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:
|
|
91 |
"\<lbrakk>\<forall>n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (\<Union>z. split (f z) ` ms) (nvalid n);
|
|
92 |
(C, m) \<in> ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z C m)"
|
|
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 -c-n\<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)
|
|
109 |
apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
|
|
110 |
apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : hoare") *})
|
|
111 |
apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : ehoare") *})
|
|
112 |
apply (simp_all only: cnvalid1_eq cenvalid_def2)
|
|
113 |
apply fast
|
|
114 |
apply fast
|
|
115 |
apply fast
|
|
116 |
apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
|
|
117 |
apply fast
|
|
118 |
apply fast
|
|
119 |
apply fast
|
|
120 |
apply fast
|
|
121 |
apply fast
|
|
122 |
apply fast
|
11376
|
123 |
apply (clarsimp del: Meth_elim_cases) (* Call *)
|
11476
|
124 |
apply (tactic "smp_tac 1 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
|
|
125 |
apply (tactic "smp_tac 2 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
|
|
126 |
apply (tactic "smp_tac 4 1", tactic "smp_tac 2 1", fast)
|
11376
|
127 |
apply (clarsimp del: Impl_elim_cases) (* Meth *)
|
|
128 |
defer
|
11476
|
129 |
prefer 4 apply blast (* Conseq *)
|
|
130 |
prefer 4 apply blast (* eConseq *)
|
11376
|
131 |
apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def)
|
|
132 |
apply blast
|
|
133 |
apply blast
|
|
134 |
apply blast
|
|
135 |
(* Impl *)
|
|
136 |
apply (rule allI)
|
|
137 |
apply (induct_tac "n")
|
|
138 |
apply (clarify intro!: Impl_nvalid_0)
|
|
139 |
apply (clarify intro!: Impl_nvalid_Suc)
|
|
140 |
apply (drule nvalids_SucD)
|
|
141 |
apply (erule (1) impE)
|
|
142 |
apply (drule (4) Impl_sound_lemma)
|
|
143 |
done
|
|
144 |
|
|
145 |
theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}"
|
|
146 |
apply (simp only: valid_def2)
|
11476
|
147 |
apply (drule hoare_sound_main [THEN conjunct1, rule_format])
|
11376
|
148 |
apply (unfold cnvalids_def nvalids_def)
|
|
149 |
apply fast
|
|
150 |
done
|
|
151 |
|
11486
|
152 |
theorem ehoare_sound: "{} \<turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q}"
|
11476
|
153 |
apply (simp only: evalid_def2)
|
|
154 |
apply (drule hoare_sound_main [THEN conjunct2, rule_format])
|
|
155 |
apply (unfold cenvalid_def nvalids_def)
|
|
156 |
apply fast
|
|
157 |
done
|
|
158 |
|
11376
|
159 |
|
|
160 |
subsection "(Relative) Completeness"
|
|
161 |
|
11476
|
162 |
constdefs MGT :: "stmt => state => triple"
|
11486
|
163 |
"MGT c z \<equiv> (\<lambda>s. z = s, c, \<lambda> t. \<exists>n. z -c- n-> t)"
|
|
164 |
MGTe :: "expr => state => etriple"
|
|
165 |
"MGTe e z \<equiv> (\<lambda>s. z = s, e, \<lambda>v t. \<exists>n. z -e>v-n-> t)"
|
|
166 |
syntax (xsymbols)
|
|
167 |
MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
|
11376
|
168 |
|
|
169 |
lemma MGF_implies_complete:
|
11476
|
170 |
"\<forall>z. {} |\<turnstile> { MGT c z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
|
11376
|
171 |
apply (simp only: valid_def2)
|
|
172 |
apply (unfold MGT_def)
|
11476
|
173 |
apply (erule hoare_ehoare.Conseq)
|
|
174 |
apply (clarsimp simp add: nvalid_def2)
|
11376
|
175 |
done
|
|
176 |
|
11476
|
177 |
lemma eMGF_implies_complete:
|
11486
|
178 |
"\<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
|
179 |
apply (simp only: evalid_def2)
|
11486
|
180 |
apply (unfold MGTe_def)
|
11476
|
181 |
apply (erule hoare_ehoare.eConseq)
|
|
182 |
apply (clarsimp simp add: envalid_def2)
|
|
183 |
done
|
11376
|
184 |
|
11476
|
185 |
declare exec_eval.intros[intro!]
|
11376
|
186 |
|
|
187 |
lemma MGF_Loop: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow>
|
11486
|
188 |
A \<turnstile> {op = z} While (x) c {\<lambda>t. \<exists>n. z -While (x) c-n\<rightarrow> t}"
|
|
189 |
apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<x> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
|
11476
|
190 |
in hoare_ehoare.Conseq)
|
11376
|
191 |
apply (rule allI)
|
11476
|
192 |
apply (rule hoare_ehoare.Loop)
|
|
193 |
apply (erule hoare_ehoare.Conseq)
|
11376
|
194 |
apply clarsimp
|
|
195 |
apply (blast intro:rtrancl_into_rtrancl)
|
|
196 |
apply (erule thin_rl)
|
|
197 |
apply clarsimp
|
|
198 |
apply (erule_tac x = z in allE)
|
|
199 |
apply clarsimp
|
|
200 |
apply (erule converse_rtrancl_induct)
|
|
201 |
apply blast
|
|
202 |
apply clarsimp
|
11476
|
203 |
apply (drule (1) exec_exec_max)
|
11376
|
204 |
apply (blast del: exec_elim_cases)
|
|
205 |
done
|
|
206 |
|
11476
|
207 |
lemma MGF_lemma: "\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z} \<Longrightarrow>
|
11486
|
208 |
(\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>\<^sub>e MGT\<^sub>e e z)"
|
|
209 |
apply (simp add: MGT_def MGTe_def)
|
11476
|
210 |
apply (rule stmt_expr.induct)
|
|
211 |
apply (rule_tac [!] allI)
|
11376
|
212 |
|
11476
|
213 |
apply (rule Conseq1 [OF hoare_ehoare.Skip])
|
11376
|
214 |
apply blast
|
|
215 |
|
11476
|
216 |
apply (rule hoare_ehoare.Comp)
|
11376
|
217 |
apply (erule spec)
|
11476
|
218 |
apply (erule hoare_ehoare.Conseq)
|
11376
|
219 |
apply clarsimp
|
11476
|
220 |
apply (drule (1) exec_exec_max)
|
11376
|
221 |
apply blast
|
|
222 |
|
11476
|
223 |
apply (erule thin_rl)
|
|
224 |
apply (rule hoare_ehoare.Cond)
|
|
225 |
apply (erule spec)
|
|
226 |
apply (rule allI)
|
|
227 |
apply (simp)
|
|
228 |
apply (rule conjI)
|
|
229 |
apply (rule impI, erule hoare_ehoare.Conseq, clarsimp, drule (1) eval_exec_max,
|
|
230 |
erule thin_rl, erule thin_rl, force)+
|
11376
|
231 |
|
|
232 |
apply (erule MGF_Loop)
|
|
233 |
|
11476
|
234 |
apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.LAss])
|
|
235 |
apply fast
|
11376
|
236 |
|
11476
|
237 |
apply (erule thin_rl)
|
|
238 |
apply (rule_tac Q = "\<lambda>a s. \<exists>n. z -expr1\<succ>Addr a-n\<rightarrow> s" in hoare_ehoare.FAss)
|
|
239 |
apply (drule spec)
|
|
240 |
apply (erule eConseq2)
|
|
241 |
apply fast
|
|
242 |
apply (rule allI)
|
|
243 |
apply (erule hoare_ehoare.eConseq)
|
|
244 |
apply clarsimp
|
|
245 |
apply (drule (1) eval_eval_max)
|
11376
|
246 |
apply blast
|
|
247 |
|
11476
|
248 |
apply (rule hoare_ehoare.Meth)
|
11376
|
249 |
apply (rule allI)
|
11476
|
250 |
apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
|
11376
|
251 |
apply blast
|
|
252 |
|
|
253 |
apply blast
|
11476
|
254 |
|
|
255 |
apply (rule eConseq1 [OF hoare_ehoare.NewC])
|
|
256 |
apply blast
|
|
257 |
|
|
258 |
apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.Cast])
|
|
259 |
apply fast
|
|
260 |
|
|
261 |
apply (rule eConseq1 [OF hoare_ehoare.LAcc])
|
|
262 |
apply blast
|
|
263 |
|
|
264 |
apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.FAcc])
|
|
265 |
apply fast
|
|
266 |
|
|
267 |
apply (rule_tac R = "\<lambda>a v s. \<exists>n1 n2 t. z -expr1\<succ>a-n1\<rightarrow> t \<and> t -expr2\<succ>v-n2\<rightarrow> s" in
|
|
268 |
hoare_ehoare.Call)
|
|
269 |
apply (erule spec)
|
|
270 |
apply (rule allI)
|
|
271 |
apply (erule hoare_ehoare.eConseq)
|
|
272 |
apply clarsimp
|
|
273 |
apply blast
|
|
274 |
apply (rule allI)+
|
|
275 |
apply (rule hoare_ehoare.Meth)
|
|
276 |
apply (rule allI)
|
|
277 |
apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
|
|
278 |
apply (erule thin_rl, erule thin_rl)
|
|
279 |
apply (clarsimp del: Impl_elim_cases)
|
|
280 |
apply (drule (2) eval_eval_exec_max)
|
|
281 |
apply (fast del: Impl_elim_cases)
|
11376
|
282 |
done
|
|
283 |
|
|
284 |
lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl C m) z}"
|
|
285 |
apply (unfold MGT_def)
|
|
286 |
apply (rule Impl1)
|
|
287 |
apply (rule_tac [2] UNIV_I)
|
|
288 |
apply clarsimp
|
11476
|
289 |
apply (rule hoare_ehoare.ConjI)
|
11376
|
290 |
apply clarsimp
|
|
291 |
apply (rule ssubst [OF Impl_body_eq])
|
|
292 |
apply (fold MGT_def)
|
11476
|
293 |
apply (rule MGF_lemma [THEN conjunct1, rule_format])
|
|
294 |
apply (rule hoare_ehoare.Asm)
|
11376
|
295 |
apply force
|
|
296 |
done
|
|
297 |
|
|
298 |
theorem hoare_relative_complete: "\<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
|
|
299 |
apply (rule MGF_implies_complete)
|
|
300 |
apply (erule_tac [2] asm_rl)
|
|
301 |
apply (rule allI)
|
11476
|
302 |
apply (rule MGF_lemma [THEN conjunct1, rule_format])
|
|
303 |
apply (rule MGF_Impl)
|
|
304 |
done
|
|
305 |
|
11486
|
306 |
theorem ehoare_relative_complete: "\<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}"
|
11476
|
307 |
apply (rule eMGF_implies_complete)
|
|
308 |
apply (erule_tac [2] asm_rl)
|
|
309 |
apply (rule allI)
|
|
310 |
apply (rule MGF_lemma [THEN conjunct2, rule_format])
|
11376
|
311 |
apply (rule MGF_Impl)
|
|
312 |
done
|
|
313 |
|
|
314 |
end
|