Methods rule_tac etc support static (Isar) contexts.
1 (* Title: HOL/NanoJava/Equivalence.thy
3 Author: David von Oheimb
4 Copyright 2001 Technische Universitaet Muenchen
7 header "Equivalence of Operational and Axiomatic Semantics"
9 theory Equivalence = OpSem + AxSem:
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"
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"
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"
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"
27 nvalids :: "[nat, triple set] => bool" ("||=_: _" [61,61] 60)
28 "||=n: T \<equiv> \<forall>t\<in>T. |=n: t"
30 cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _" [61,61] 60)
31 "A ||= C \<equiv> \<forall>n. ||=n: A --> ||=n: C"
33 cenvalid :: "[triple set,etriple ] => bool" ("_ ||=e/ _" [61,61] 60)
34 "A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t"
37 valid :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
38 evalid :: "[assn,expr,vassn] => bool" ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
39 nvalid :: "[nat, triple ] => bool" ("\<Turnstile>_: _" [61,61] 60)
40 envalid :: "[nat,etriple ] => bool" ("\<Turnstile>_:\<^sub>e _" [61,61] 60)
41 nvalids :: "[nat, triple set] => bool" ("|\<Turnstile>_: _" [61,61] 60)
42 cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
43 cenvalid :: "[triple set,etriple ] => bool" ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
46 lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
47 by (simp add: nvalid_def Let_def)
49 lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n: (P,c,Q))"
50 apply (simp add: valid_def nvalid_def2)
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"
55 by (simp add: envalid_def Let_def)
57 lemma evalid_def2: "\<Turnstile>\<^sub>e {P} e {Q} = (\<forall>n. \<Turnstile>n:\<^sub>e (P,e,Q))"
58 apply (simp add: evalid_def envalid_def2)
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))"
64 by(simp add: cenvalid_def envalid_def2)
67 subsection "Soundness"
69 declare exec_elim_cases [elim!] eval_elim_cases [elim!]
71 lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl M,Q)"
72 by (clarsimp simp add: nvalid_def2)
74 lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body M,Q) \<Longrightarrow> \<Turnstile>Suc n: (P,Impl M,Q)"
75 by (clarsimp simp add: nvalid_def2)
77 lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t"
78 by (force simp add: split_paired_all nvalid_def2 intro: exec_mono)
80 lemma nvalids_SucD: "Ball A (nvalid (Suc n)) \<Longrightarrow> Ball A (nvalid n)"
81 by (fast intro: nvalid_SucD)
83 lemma Loop_sound_lemma [rule_format (no_asm)]:
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])
90 lemma Impl_sound_lemma:
91 "\<lbrakk>\<forall>z n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (f z ` Ms) (nvalid n);
92 Cm\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z Cm)"
95 lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l"
99 "\<forall>a p l. (P' a p l \<and> P a p l) \<Longrightarrow> \<forall>a p l. P a p l"
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)
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)"
107 apply (tactic "split_all_tac 1", rename_tac P e Q)
108 apply (rule hoare_ehoare.induct)
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)
117 apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
124 apply (clarsimp del: Meth_elim_cases) (* Call *)
125 apply (force del: Impl_elim_cases)
127 prefer 4 apply blast (* Conseq *)
128 prefer 4 apply blast (* eConseq *)
129 apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def)
134 apply (rule_tac x=Z in spec)
135 apply (induct_tac "n")
136 apply (clarify intro!: Impl_nvalid_0)
137 apply (clarify intro!: Impl_nvalid_Suc)
138 apply (drule nvalids_SucD)
139 apply (simp only: all_simps)
140 apply (erule (1) impE)
141 apply (drule (2) Impl_sound_lemma)
146 theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}"
147 apply (simp only: valid_def2)
148 apply (drule hoare_sound_main [THEN conjunct1, rule_format])
149 apply (unfold cnvalids_def nvalids_def)
153 theorem ehoare_sound: "{} \<turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q}"
154 apply (simp only: evalid_def2)
155 apply (drule hoare_sound_main [THEN conjunct2, rule_format])
156 apply (unfold cenvalid_def nvalids_def)
161 subsection "(Relative) Completeness"
163 constdefs MGT :: "stmt => state => triple"
164 "MGT c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda> t. \<exists>n. Z -c- n-> t)"
165 MGTe :: "expr => state => etriple"
166 "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e>v-n-> t)"
168 MGTe :: "expr => state => etriple" ("MGT\<^sub>e")
170 lemma MGF_implies_complete:
171 "\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
172 apply (simp only: valid_def2)
173 apply (unfold MGT_def)
174 apply (erule hoare_ehoare.Conseq)
175 apply (clarsimp simp add: nvalid_def2)
178 lemma eMGF_implies_complete:
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}"
180 apply (simp only: evalid_def2)
181 apply (unfold MGTe_def)
182 apply (erule hoare_ehoare.eConseq)
183 apply (clarsimp simp add: envalid_def2)
186 declare exec_eval.intros[intro!]
188 lemma MGF_Loop: "\<forall>Z. A \<turnstile> {op = Z} c {\<lambda>t. \<exists>n. Z -c-n\<rightarrow> t} \<Longrightarrow>
189 A \<turnstile> {op = Z} While (x) c {\<lambda>t. \<exists>n. Z -While (x) c-n\<rightarrow> t}"
190 apply (rule_tac P' = "\<lambda>Z s. (Z,s) \<in> ({(s,t). \<exists>n. s<x> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
191 in hoare_ehoare.Conseq)
193 apply (rule hoare_ehoare.Loop)
194 apply (erule hoare_ehoare.Conseq)
196 apply (blast intro:rtrancl_into_rtrancl)
197 apply (erule thin_rl)
199 apply (erule_tac x = Z in allE)
201 apply (erule converse_rtrancl_induct)
204 apply (drule (1) exec_exec_max)
205 apply (blast del: exec_elim_cases)
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)"
210 apply (simp add: MGT_def MGTe_def)
211 apply (rule stmt_expr.induct)
212 apply (rule_tac [!] allI)
214 apply (rule Conseq1 [OF hoare_ehoare.Skip])
217 apply (rule hoare_ehoare.Comp)
219 apply (erule hoare_ehoare.Conseq)
221 apply (drule (1) exec_exec_max)
224 apply (erule thin_rl)
225 apply (rule hoare_ehoare.Cond)
230 apply (rule impI, erule hoare_ehoare.Conseq, clarsimp, drule (1) eval_exec_max,
231 erule thin_rl, erule thin_rl, force)+
233 apply (erule MGF_Loop)
235 apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.LAss])
238 apply (erule thin_rl)
239 apply (rule_tac Q = "\<lambda>a s. \<exists>n. Z -expr1\<succ>Addr a-n\<rightarrow> s" in hoare_ehoare.FAss)
241 apply (erule eConseq2)
244 apply (erule hoare_ehoare.eConseq)
246 apply (drule (1) eval_eval_max)
249 apply (simp only: split_paired_all)
250 apply (rule hoare_ehoare.Meth)
252 apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
255 apply (simp add: split_paired_all)
257 apply (rule eConseq1 [OF hoare_ehoare.NewC])
260 apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.Cast])
263 apply (rule eConseq1 [OF hoare_ehoare.LAcc])
266 apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.FAcc])
269 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
273 apply (erule hoare_ehoare.eConseq)
277 apply (rule hoare_ehoare.Meth)
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)
283 apply (force del: Impl_elim_cases)
286 lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl M) Z}"
287 apply (unfold MGT_def)
289 apply (rule_tac [2] UNIV_I)
291 apply (rule hoare_ehoare.ConjI)
293 apply (rule ssubst [OF Impl_body_eq])
295 apply (rule MGF_lemma [THEN conjunct1, rule_format])
296 apply (rule hoare_ehoare.Asm)
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)
304 apply (rule MGF_lemma [THEN conjunct1, rule_format])
305 apply (rule MGF_Impl)
308 theorem ehoare_relative_complete: "\<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}"
309 apply (rule eMGF_implies_complete)
310 apply (erule_tac [2] asm_rl)
312 apply (rule MGF_lemma [THEN conjunct2, rule_format])
313 apply (rule MGF_Impl)
316 lemma cFalse: "A \<turnstile> {\<lambda>s. False} c {Q}"
318 apply (rule hoare_relative_complete)
319 apply (auto simp add: valid_def)
322 lemma eFalse: "A \<turnstile>\<^sub>e {\<lambda>s. False} e {Q}"
324 apply (rule ehoare_relative_complete)
325 apply (auto simp add: evalid_def)