33 cenvalid :: "[triple set,etriple ] => bool" ("_ ||=e/ _" [61,61] 60) |
33 cenvalid :: "[triple set,etriple ] => bool" ("_ ||=e/ _" [61,61] 60) |
34 "A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t" |
34 "A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t" |
35 |
35 |
36 syntax (xsymbols) |
36 syntax (xsymbols) |
37 valid :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) |
37 valid :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) |
38 evalid :: "[assn,expr,vassn] => bool" ("\<Turnstile>e {(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) |
39 nvalid :: "[nat, triple ] => bool" ("\<Turnstile>_: _" [61,61] 60) |
40 envalid :: "[nat,etriple ] => bool" ("\<Turnstile>_:e _" [61,61] 60) |
40 envalid :: "[nat,etriple ] => bool" ("\<Turnstile>_:\<^sub>e _" [61,61] 60) |
41 nvalids :: "[nat, triple set] => bool" ("|\<Turnstile>_: _" [61,61] 60) |
41 nvalids :: "[nat, triple set] => bool" ("|\<Turnstile>_: _" [61,61] 60) |
42 cnvalids :: "[triple set,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>e/ _"[61,61] 60) |
43 cenvalid :: "[triple set,etriple ] => bool" ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60) |
44 |
44 |
45 |
45 |
46 lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t" |
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) |
47 by (simp add: nvalid_def Let_def) |
48 |
48 |
49 lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n: (P,c,Q))" |
49 lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n: (P,c,Q))" |
50 apply (simp add: valid_def nvalid_def2) |
50 apply (simp add: valid_def nvalid_def2) |
51 apply blast |
51 apply blast |
52 done |
52 done |
53 |
53 |
54 lemma envalid_def2: "\<Turnstile>n:e (P,e,Q) \<equiv> \<forall>s v t. s -e\<succ>v-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t" |
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) |
55 by (simp add: envalid_def Let_def) |
56 |
56 |
57 lemma evalid_def2: "\<Turnstile>e {P} e {Q} = (\<forall>n. \<Turnstile>n:e (P,e,Q))" |
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) |
58 apply (simp add: evalid_def envalid_def2) |
59 apply blast |
59 apply blast |
60 done |
60 done |
61 |
61 |
62 lemma cenvalid_def2: |
62 lemma cenvalid_def2: |
63 "A|\<Turnstile>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))" |
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) |
64 by(simp add: cenvalid_def envalid_def2) |
65 |
65 |
66 |
66 |
67 subsection "Soundness" |
67 subsection "Soundness" |
68 |
68 |
101 |
101 |
102 lemma cnvalid1_eq: |
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)" |
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) |
104 by(simp add: cnvalids_def nvalids_def nvalid_def2) |
105 |
105 |
106 lemma hoare_sound_main:"\<And>t. (A |\<turnstile> C \<longrightarrow> A |\<Turnstile> C) \<and> (A |\<turnstile>e t \<longrightarrow> A |\<Turnstile>e t)" |
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) |
107 apply (tactic "split_all_tac 1", rename_tac P e Q) |
108 apply (rule hoare_ehoare.induct) |
108 apply (rule hoare_ehoare.induct) |
109 apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *}) |
109 apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *}) |
110 apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : hoare") *}) |
110 apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : hoare") *}) |
111 apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : ehoare") *}) |
111 apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : ehoare") *}) |
147 apply (drule hoare_sound_main [THEN conjunct1, rule_format]) |
147 apply (drule hoare_sound_main [THEN conjunct1, rule_format]) |
148 apply (unfold cnvalids_def nvalids_def) |
148 apply (unfold cnvalids_def nvalids_def) |
149 apply fast |
149 apply fast |
150 done |
150 done |
151 |
151 |
152 theorem ehoare_sound: "{} \<turnstile>e {P} e {Q} \<Longrightarrow> \<Turnstile>e {P} e {Q}" |
152 theorem ehoare_sound: "{} \<turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q}" |
153 apply (simp only: evalid_def2) |
153 apply (simp only: evalid_def2) |
154 apply (drule hoare_sound_main [THEN conjunct2, rule_format]) |
154 apply (drule hoare_sound_main [THEN conjunct2, rule_format]) |
155 apply (unfold cenvalid_def nvalids_def) |
155 apply (unfold cenvalid_def nvalids_def) |
156 apply fast |
156 apply fast |
157 done |
157 done |
158 |
158 |
159 |
159 |
160 subsection "(Relative) Completeness" |
160 subsection "(Relative) Completeness" |
161 |
161 |
162 constdefs MGT :: "stmt => state => triple" |
162 constdefs MGT :: "stmt => state => triple" |
163 "MGT c z \<equiv> (\<lambda>s. z = s, c, \<lambda> t. \<exists>n. z -c- n-> t)" |
163 "MGT c z \<equiv> (\<lambda>s. z = s, c, \<lambda> t. \<exists>n. z -c- n-> t)" |
164 eMGT :: "expr => state => etriple" |
164 MGTe :: "expr => state => etriple" |
165 "eMGT e z \<equiv> (\<lambda>s. z = s, e, \<lambda>v t. \<exists>n. z -e>v-n-> t)" |
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") |
166 |
168 |
167 lemma MGF_implies_complete: |
169 lemma MGF_implies_complete: |
168 "\<forall>z. {} |\<turnstile> { MGT c z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}" |
170 "\<forall>z. {} |\<turnstile> { MGT c z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}" |
169 apply (simp only: valid_def2) |
171 apply (simp only: valid_def2) |
170 apply (unfold MGT_def) |
172 apply (unfold MGT_def) |
171 apply (erule hoare_ehoare.Conseq) |
173 apply (erule hoare_ehoare.Conseq) |
172 apply (clarsimp simp add: nvalid_def2) |
174 apply (clarsimp simp add: nvalid_def2) |
173 done |
175 done |
174 |
176 |
175 lemma eMGF_implies_complete: |
177 lemma eMGF_implies_complete: |
176 "\<forall>z. {} |\<turnstile>e eMGT e z \<Longrightarrow> \<Turnstile>e {P} e {Q} \<Longrightarrow> {} \<turnstile>e {P} e {Q}" |
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}" |
177 apply (simp only: evalid_def2) |
179 apply (simp only: evalid_def2) |
178 apply (unfold eMGT_def) |
180 apply (unfold MGTe_def) |
179 apply (erule hoare_ehoare.eConseq) |
181 apply (erule hoare_ehoare.eConseq) |
180 apply (clarsimp simp add: envalid_def2) |
182 apply (clarsimp simp add: envalid_def2) |
181 done |
183 done |
182 |
184 |
183 declare exec_eval.intros[intro!] |
185 declare exec_eval.intros[intro!] |
184 |
186 |
185 lemma MGF_Loop: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow> |
187 lemma MGF_Loop: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow> |
186 A \<turnstile> {op = z} While (e) c {\<lambda>t. \<exists>n. z -While (e) c-n\<rightarrow> t}" |
188 A \<turnstile> {op = z} While (x) c {\<lambda>t. \<exists>n. z -While (x) c-n\<rightarrow> t}" |
187 apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<e> \<noteq> Null \<and> s -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})^*" |
188 in hoare_ehoare.Conseq) |
190 in hoare_ehoare.Conseq) |
189 apply (rule allI) |
191 apply (rule allI) |
190 apply (rule hoare_ehoare.Loop) |
192 apply (rule hoare_ehoare.Loop) |
191 apply (erule hoare_ehoare.Conseq) |
193 apply (erule hoare_ehoare.Conseq) |
192 apply clarsimp |
194 apply clarsimp |
201 apply (drule (1) exec_exec_max) |
203 apply (drule (1) exec_exec_max) |
202 apply (blast del: exec_elim_cases) |
204 apply (blast del: exec_elim_cases) |
203 done |
205 done |
204 |
206 |
205 lemma MGF_lemma: "\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z} \<Longrightarrow> |
207 lemma MGF_lemma: "\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z} \<Longrightarrow> |
206 (\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>e eMGT e z)" |
208 (\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>\<^sub>e MGT\<^sub>e e z)" |
207 apply (simp add: MGT_def eMGT_def) |
209 apply (simp add: MGT_def MGTe_def) |
208 apply (rule stmt_expr.induct) |
210 apply (rule stmt_expr.induct) |
209 apply (rule_tac [!] allI) |
211 apply (rule_tac [!] allI) |
210 |
212 |
211 apply (rule Conseq1 [OF hoare_ehoare.Skip]) |
213 apply (rule Conseq1 [OF hoare_ehoare.Skip]) |
212 apply blast |
214 apply blast |
299 apply (rule allI) |
301 apply (rule allI) |
300 apply (rule MGF_lemma [THEN conjunct1, rule_format]) |
302 apply (rule MGF_lemma [THEN conjunct1, rule_format]) |
301 apply (rule MGF_Impl) |
303 apply (rule MGF_Impl) |
302 done |
304 done |
303 |
305 |
304 theorem ehoare_relative_complete: "\<Turnstile>e {P} e {Q} \<Longrightarrow> {} \<turnstile>e {P} e {Q}" |
306 theorem ehoare_relative_complete: "\<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}" |
305 apply (rule eMGF_implies_complete) |
307 apply (rule eMGF_implies_complete) |
306 apply (erule_tac [2] asm_rl) |
308 apply (erule_tac [2] asm_rl) |
307 apply (rule allI) |
309 apply (rule allI) |
308 apply (rule MGF_lemma [THEN conjunct2, rule_format]) |
310 apply (rule MGF_lemma [THEN conjunct2, rule_format]) |
309 apply (rule MGF_Impl) |
311 apply (rule MGF_Impl) |