66 |
66 |
67 subsection "Soundness" |
67 subsection "Soundness" |
68 |
68 |
69 declare exec_elim_cases [elim!] eval_elim_cases [elim!] |
69 declare exec_elim_cases [elim!] eval_elim_cases [elim!] |
70 |
70 |
71 lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl C m,Q)" |
71 lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl M,Q)" |
72 by (clarsimp simp add: nvalid_def2) |
72 by (clarsimp simp add: nvalid_def2) |
73 |
73 |
74 lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body C m,Q) \<Longrightarrow> \<Turnstile>Suc n: (P,Impl C m,Q)" |
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) |
75 by (clarsimp simp add: nvalid_def2) |
76 |
76 |
77 lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t" |
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) |
78 by (force simp add: split_paired_all nvalid_def2 intro: exec_mono) |
79 |
79 |
86 apply (rule_tac "P2.1"="%s e v n t. True" in exec_eval.induct [THEN conjunct1]) |
86 apply (rule_tac "P2.1"="%s e v n t. True" in exec_eval.induct [THEN conjunct1]) |
87 apply clarsimp+ |
87 apply clarsimp+ |
88 done |
88 done |
89 |
89 |
90 lemma Impl_sound_lemma: |
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); |
91 "\<lbrakk>\<forall>z n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (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)" |
92 M\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z M)" |
93 by blast |
93 by blast |
94 |
94 |
95 lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l" |
95 lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l" |
96 by fast |
96 by fast |
97 |
97 |
122 apply fast |
122 apply fast |
123 apply (clarsimp del: Meth_elim_cases) (* Call *) |
123 apply (clarsimp del: Meth_elim_cases) (* Call *) |
124 apply (tactic "smp_tac 1 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1") |
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") |
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) |
126 apply (tactic "smp_tac 4 1", tactic "smp_tac 2 1", fast) |
127 apply (clarsimp del: Impl_elim_cases) (* Meth *) |
127 apply (force del: Impl_elim_cases) (* Meth *) |
128 defer |
128 defer |
129 prefer 4 apply blast (* Conseq *) |
129 prefer 4 apply blast (* Conseq *) |
130 prefer 4 apply blast (* eConseq *) |
130 prefer 4 apply blast (* eConseq *) |
131 apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def) |
131 apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def) |
132 apply blast |
132 apply blast |
133 apply blast |
133 apply blast |
134 apply blast |
134 apply blast |
135 (* Impl *) |
135 (* Impl *) |
136 apply (rule allI) |
136 apply (rule allI) |
|
137 apply (rule_tac x=z in spec) |
137 apply (induct_tac "n") |
138 apply (induct_tac "n") |
138 apply (clarify intro!: Impl_nvalid_0) |
139 apply (clarify intro!: Impl_nvalid_0) |
139 apply (clarify intro!: Impl_nvalid_Suc) |
140 apply (clarify intro!: Impl_nvalid_Suc) |
140 apply (drule nvalids_SucD) |
141 apply (drule nvalids_SucD) |
|
142 apply (simp only: all_simps) |
141 apply (erule (1) impE) |
143 apply (erule (1) impE) |
142 apply (drule (4) Impl_sound_lemma) |
144 apply (drule (2) Impl_sound_lemma) |
|
145 apply blast |
|
146 apply assumption |
143 done |
147 done |
144 |
148 |
145 theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}" |
149 theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}" |
146 apply (simp only: valid_def2) |
150 apply (simp only: valid_def2) |
147 apply (drule hoare_sound_main [THEN conjunct1, rule_format]) |
151 apply (drule hoare_sound_main [THEN conjunct1, rule_format]) |
202 apply clarsimp |
206 apply clarsimp |
203 apply (drule (1) exec_exec_max) |
207 apply (drule (1) exec_exec_max) |
204 apply (blast del: exec_elim_cases) |
208 apply (blast del: exec_elim_cases) |
205 done |
209 done |
206 |
210 |
207 lemma MGF_lemma: "\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z} \<Longrightarrow> |
211 lemma MGF_lemma: "\<forall>M z. A |\<turnstile> {MGT (Impl M) z} \<Longrightarrow> |
208 (\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>\<^sub>e MGT\<^sub>e e z)" |
212 (\<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) |
213 apply (simp add: MGT_def MGTe_def) |
210 apply (rule stmt_expr.induct) |
214 apply (rule stmt_expr.induct) |
211 apply (rule_tac [!] allI) |
215 apply (rule_tac [!] allI) |
212 |
216 |
248 apply (rule hoare_ehoare.Meth) |
252 apply (rule hoare_ehoare.Meth) |
249 apply (rule allI) |
253 apply (rule allI) |
250 apply (drule spec, drule spec, erule hoare_ehoare.Conseq) |
254 apply (drule spec, drule spec, erule hoare_ehoare.Conseq) |
251 apply blast |
255 apply blast |
252 |
256 |
253 apply blast |
257 apply (simp add: split_paired_all) |
254 |
258 |
255 apply (rule eConseq1 [OF hoare_ehoare.NewC]) |
259 apply (rule eConseq1 [OF hoare_ehoare.NewC]) |
256 apply blast |
260 apply blast |
257 |
261 |
258 apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.Cast]) |
262 apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.Cast]) |
279 apply (clarsimp del: Impl_elim_cases) |
283 apply (clarsimp del: Impl_elim_cases) |
280 apply (drule (2) eval_eval_exec_max) |
284 apply (drule (2) eval_eval_exec_max) |
281 apply (fast del: Impl_elim_cases) |
285 apply (fast del: Impl_elim_cases) |
282 done |
286 done |
283 |
287 |
284 lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl C m) z}" |
288 lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl M) z}" |
285 apply (unfold MGT_def) |
289 apply (unfold MGT_def) |
286 apply (rule Impl1) |
290 apply (rule Impl1) |
287 apply (rule_tac [2] UNIV_I) |
291 apply (rule_tac [2] UNIV_I) |
288 apply clarsimp |
292 apply clarsimp |
289 apply (rule hoare_ehoare.ConjI) |
293 apply (rule hoare_ehoare.ConjI) |