1(*
2    Author:      Norbert Schirmer
3    Maintainer:  Norbert Schirmer, norbert.schirmer at web de
4    License:     LGPL
5*)
6
7(*  Title:      HoarePartialProps.thy
8    Author:     Norbert Schirmer, TU Muenchen
9
10Copyright (C) 2004-2008 Norbert Schirmer
11Some rights reserved, TU Muenchen
12
13This library is free software; you can redistribute it and/or modify
14it under the terms of the GNU Lesser General Public License as
15published by the Free Software Foundation; either version 2.1 of the
16License, or (at your option) any later version.
17
18This library is distributed in the hope that it will be useful, but
19WITHOUT ANY WARRANTY; without even the implied warranty of
20MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
21Lesser General Public License for more details.
22
23You should have received a copy of the GNU Lesser General Public
24License along with this library; if not, write to the Free Software
25Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
26USA
27*)
28
29section \<open>Properties of Partial Correctness Hoare Logic\<close>
30
31theory HoarePartialProps imports HoarePartialDef begin
32
33subsection \<open>Soundness\<close>
34
35lemma hoare_cnvalid:
36 assumes hoare: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
37 shows "\<And>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
38using hoare
39proof (induct)
40  case (Skip \<Theta> F P A)
41  show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P Skip P,A"
42  proof (rule cnvalidI)
43    fix s t
44    assume "\<Gamma>\<turnstile>\<langle>Skip,Normal s\<rangle> =n\<Rightarrow> t" "s \<in> P"
45    thus "t \<in> Normal ` P \<union> Abrupt ` A"
46      by cases auto
47  qed
48next
49  case (Basic \<Theta> F f P A)
50  show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> {s. f s \<in> P} (Basic f) P,A"
51  proof (rule cnvalidI)
52    fix s t
53    assume "\<Gamma>\<turnstile>\<langle>Basic f,Normal s\<rangle> =n\<Rightarrow> t" "s \<in> {s. f s \<in> P}"
54    thus "t \<in> Normal ` P \<union> Abrupt ` A"
55      by cases auto
56  qed
57next
58  case (Spec \<Theta> F r Q A)
59  show "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {s. (\<forall>t. (s, t) \<in> r \<longrightarrow> t \<in> Q) \<and> (\<exists>t. (s, t) \<in> r)} Spec r Q,A"
60  proof (rule cnvalidI)
61    fix s t
62    assume exec: "\<Gamma>\<turnstile>\<langle>Spec r,Normal s\<rangle> =n\<Rightarrow> t"
63    assume P: "s \<in> {s. (\<forall>t. (s, t) \<in> r \<longrightarrow> t \<in> Q) \<and> (\<exists>t. (s, t) \<in> r)}"
64    from exec P
65    show "t \<in> Normal ` Q \<union> Abrupt ` A"
66      by cases auto
67  qed
68next
69  case (Seq \<Theta> F P c1 R A c2 Q)
70  have valid_c1: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c1 R,A" by fact
71  have valid_c2: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> R c2 Q,A" by fact
72  show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P Seq c1 c2 Q,A"
73  proof (rule cnvalidI)
74    fix s t
75    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
76    assume exec: "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> =n\<Rightarrow> t"
77    assume t_notin_F: "t \<notin> Fault ` F"
78    assume P: "s \<in> P"
79    from exec P obtain r where
80      exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> =n\<Rightarrow> r" and exec_c2:  "\<Gamma>\<turnstile>\<langle>c2,r\<rangle> =n\<Rightarrow> t"
81      by cases auto
82    with t_notin_F have "r \<notin> Fault ` F"
83      by (auto dest: execn_Fault_end)
84    with valid_c1 ctxt exec_c1 P
85    have r: "r\<in>Normal ` R \<union> Abrupt ` A"
86      by (rule cnvalidD)
87    show "t\<in>Normal ` Q \<union> Abrupt ` A"
88    proof (cases r)
89      case (Normal r')
90      with exec_c2 r
91      show "t\<in>Normal ` Q \<union> Abrupt ` A"
92        apply -
93        apply (rule cnvalidD [OF valid_c2 ctxt _ _ t_notin_F])
94        apply auto
95        done
96    next
97      case (Abrupt r')
98      with exec_c2 have "t=Abrupt r'"
99        by (auto elim: execn_elim_cases)
100      with Abrupt r show ?thesis
101        by auto
102    next
103      case Fault with r show ?thesis by blast
104    next
105      case Stuck with r show ?thesis by blast
106    qed
107  qed
108next
109  case (Cond \<Theta> F P b c1 Q A c2)
110  have valid_c1: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> (P \<inter> b) c1 Q,A" by fact
111  have valid_c2: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> (P \<inter> - b) c2 Q,A" by fact
112  show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P Cond b c1 c2 Q,A"
113  proof (rule cnvalidI)
114    fix s t
115    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
116    assume exec: "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> =n\<Rightarrow> t"
117    assume P: "s \<in> P"
118    assume t_notin_F: "t \<notin> Fault ` F"
119    show "t \<in> Normal ` Q \<union> Abrupt ` A"
120    proof (cases "s\<in>b")
121      case True
122      with exec have "\<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> =n\<Rightarrow> t"
123        by cases auto
124      with P True
125      show ?thesis
126        by - (rule cnvalidD [OF valid_c1 ctxt _ _ t_notin_F],auto)
127    next
128      case False
129      with exec P have "\<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> =n\<Rightarrow> t"
130        by cases auto
131      with P False
132      show ?thesis
133        by - (rule cnvalidD [OF valid_c2 ctxt _ _ t_notin_F],auto)
134    qed
135  qed
136next
137  case (While \<Theta> F P b c A n)
138  have valid_c: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> (P \<inter> b) c P,A" by fact
139  show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P While b c (P \<inter> - b),A"
140  proof (rule cnvalidI)
141    fix s t
142    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
143    assume exec: "\<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> =n\<Rightarrow> t"
144    assume P: "s \<in> P"
145    assume t_notin_F: "t \<notin> Fault ` F"
146    show "t \<in> Normal ` (P \<inter> - b) \<union> Abrupt ` A"
147    proof (cases "s \<in> b")
148      case True
149      {
150        fix d::"('b,'a,'c) com" fix s t
151        assume exec: "\<Gamma>\<turnstile>\<langle>d,s\<rangle> =n\<Rightarrow> t"
152        assume d: "d=While b c"
153        assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
154        from exec d ctxt
155        have "\<lbrakk>s \<in> Normal ` P; t \<notin> Fault ` F\<rbrakk>
156               \<Longrightarrow> t \<in> Normal ` (P \<inter> - b) \<union> Abrupt`A"
157        proof (induct)
158          case (WhileTrue s b' c' n r t)
159          have t_notin_F: "t \<notin> Fault ` F" by fact
160          have eqs: "While b' c' = While b c" by fact
161          note valid_c
162          moreover have ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" by fact
163          moreover from WhileTrue
164          obtain "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> r" and
165            "\<Gamma>\<turnstile>\<langle>While b c,r\<rangle> =n\<Rightarrow> t" and
166            "Normal s \<in> Normal `(P \<inter> b)" by auto
167          moreover with t_notin_F have "r \<notin> Fault ` F"
168            by (auto dest: execn_Fault_end)
169          ultimately
170          have r: "r \<in> Normal ` P \<union> Abrupt ` A"
171            by - (rule cnvalidD,auto)
172          from this _ ctxt
173          show "t \<in> Normal ` (P \<inter> - b) \<union> Abrupt ` A "
174          proof (cases r)
175            case (Normal r')
176            with r ctxt eqs t_notin_F
177            show ?thesis
178              by - (rule WhileTrue.hyps,auto)
179          next
180            case (Abrupt r')
181            have "\<Gamma>\<turnstile>\<langle>While b' c',r\<rangle> =n\<Rightarrow> t" by fact
182            with Abrupt have "t=r"
183              by (auto dest: execn_Abrupt_end)
184            with r Abrupt show ?thesis
185              by blast
186          next
187            case Fault with r show ?thesis by blast
188          next
189            case Stuck with r show ?thesis by blast
190          qed
191        qed auto
192      }
193      with exec ctxt P t_notin_F
194      show ?thesis
195        by auto
196    next
197      case False
198      with exec P have "t=Normal s"
199        by cases auto
200      with P False
201      show ?thesis
202        by auto
203    qed
204  qed
205next
206  case (Guard \<Theta> F g P c Q A f)
207  have valid_c: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> (g \<inter> P) c Q,A" by fact
208  show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> (g \<inter> P) Guard f g c  Q,A"
209  proof (rule cnvalidI)
210    fix s t
211    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
212    assume exec: "\<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> =n\<Rightarrow> t"
213    assume t_notin_F: "t \<notin> Fault ` F"
214    assume P:"s \<in> (g \<inter> P)"
215    from exec P have "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
216      by cases auto
217    from valid_c ctxt this P t_notin_F
218    show "t \<in> Normal ` Q \<union> Abrupt ` A"
219      by (rule cnvalidD)
220  qed
221next
222  case (Guarantee f F \<Theta> g P c Q A)
223  have valid_c: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> (g \<inter> P) c Q,A" by fact
224  have f_F: "f \<in> F" by fact
225  show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P Guard f g c  Q,A"
226  proof (rule cnvalidI)
227    fix s t
228    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
229    assume exec: "\<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> =n\<Rightarrow> t"
230    assume t_notin_F: "t \<notin> Fault ` F"
231    assume P:"s \<in> P"
232    from exec f_F t_notin_F have g: "s \<in> g"
233      by cases auto
234    with P have P': "s \<in> g \<inter> P"
235      by blast
236    from exec P g have "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
237      by cases auto
238    from valid_c ctxt this P' t_notin_F
239    show "t \<in> Normal ` Q \<union> Abrupt ` A"
240      by (rule cnvalidD)
241  qed
242next
243  case (CallRec P p Q A Specs \<Theta> F)
244  have p: "(P,p,Q,A) \<in> Specs" by fact
245  have valid_body:
246    "\<forall>(P,p,Q,A) \<in> Specs. p \<in> dom \<Gamma> \<and> (\<forall>n. \<Gamma>,\<Theta> \<union> Specs \<Turnstile>n:\<^bsub>/F\<^esub> P (the (\<Gamma> p)) Q,A)"
247    using CallRec.hyps by blast
248  show "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P Call p Q,A"
249  proof -
250    {
251      fix n
252      have "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A
253        \<Longrightarrow> \<forall>(P,p,Q,A) \<in>Specs. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
254      proof (induct n)
255        case 0
256        show "\<forall>(P,p,Q,A) \<in>Specs. \<Gamma>\<Turnstile>0:\<^bsub>/F\<^esub> P (Call p) Q,A"
257          by (fastforce elim!: execn_elim_cases simp add: nvalid_def)
258      next
259        case (Suc m)
260        have hyp: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>m:\<^bsub>/F\<^esub> P (Call p) Q,A
261              \<Longrightarrow> \<forall>(P,p,Q,A) \<in>Specs. \<Gamma>\<Turnstile>m:\<^bsub>/F\<^esub> P (Call p) Q,A" by fact
262        have "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>Suc m:\<^bsub>/F\<^esub> P (Call p) Q,A" by fact
263        hence ctxt_m: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>m:\<^bsub>/F\<^esub> P (Call p) Q,A"
264          by (fastforce simp add: nvalid_def intro: execn_Suc)
265        hence valid_Proc:
266          "\<forall>(P,p,Q,A) \<in>Specs. \<Gamma>\<Turnstile>m:\<^bsub>/F\<^esub> P (Call p) Q,A"
267          by (rule hyp)
268        let ?\<Theta>'= "\<Theta> \<union> Specs"
269        from valid_Proc ctxt_m
270        have "\<forall>(P, p, Q, A)\<in>?\<Theta>'. \<Gamma> \<Turnstile>m:\<^bsub>/F\<^esub> P (Call p) Q,A"
271          by fastforce
272        with valid_body
273        have valid_body_m:
274          "\<forall>(P,p,Q,A) \<in>Specs. \<forall>n. \<Gamma> \<Turnstile>m:\<^bsub>/F\<^esub> P (the (\<Gamma> p)) Q,A"
275          by (fastforce simp add: cnvalid_def)
276        show "\<forall>(P,p,Q,A) \<in>Specs. \<Gamma> \<Turnstile>Suc m:\<^bsub>/F\<^esub> P (Call p) Q,A"
277        proof (clarify)
278          fix P p Q A assume p: "(P,p,Q,A) \<in> Specs"
279          show "\<Gamma> \<Turnstile>Suc m:\<^bsub>/F\<^esub> P (Call p) Q,A"
280          proof (rule nvalidI)
281            fix s t
282            assume exec_call:
283              "\<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> =Suc m\<Rightarrow> t"
284            assume Pre: "s \<in> P"
285            assume t_notin_F: "t \<notin> Fault ` F"
286            from exec_call
287            show "t \<in> Normal ` Q \<union> Abrupt ` A"
288            proof (cases)
289              fix bdy m'
290              assume m: "Suc m = Suc m'"
291              assume bdy: "\<Gamma> p = Some bdy"
292              assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal s\<rangle> =m'\<Rightarrow> t"
293              from Pre valid_body_m exec_body bdy m p t_notin_F
294              show ?thesis
295                by (fastforce simp add: nvalid_def)
296            next
297              assume "\<Gamma> p = None"
298              with valid_body p have False by auto
299              thus ?thesis ..
300            qed
301          qed
302        qed
303      qed
304    }
305    with p show ?thesis
306      by (fastforce simp add: cnvalid_def)
307  qed
308next
309  case (DynCom P \<Theta> F c Q A)
310  hence valid_c: "\<forall>s\<in>P. (\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P (c s) Q,A)" by auto
311  show "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P DynCom c Q,A"
312  proof (rule cnvalidI)
313    fix s t
314    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
315    assume exec: "\<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> =n\<Rightarrow> t"
316    assume P: "s \<in> P"
317    assume t_notin_Fault: "t \<notin> Fault ` F"
318    from exec show "t \<in> Normal ` Q \<union> Abrupt ` A"
319    proof (cases)
320      assume "\<Gamma>\<turnstile>\<langle>c s,Normal s\<rangle> =n\<Rightarrow> t"
321      from cnvalidD [OF valid_c [rule_format, OF P] ctxt this P t_notin_Fault]
322      show ?thesis .
323    qed
324  qed
325next
326  case (Throw \<Theta> F A Q)
327  show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> A Throw Q,A"
328  proof (rule cnvalidI)
329    fix s t
330    assume "\<Gamma>\<turnstile>\<langle>Throw,Normal s\<rangle> =n\<Rightarrow> t" "s \<in> A"
331    then show "t \<in> Normal ` Q \<union> Abrupt ` A"
332      by cases simp
333  qed
334next
335  case (Catch \<Theta> F P c\<^sub>1 Q R c\<^sub>2 A)
336  have valid_c1: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c\<^sub>1 Q,R" by fact
337  have valid_c2: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> R c\<^sub>2 Q,A" by fact
338  show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P Catch c\<^sub>1 c\<^sub>2 Q,A"
339  proof (rule cnvalidI)
340    fix s t
341    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
342    assume exec: "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal s\<rangle> =n\<Rightarrow> t"
343    assume P: "s \<in> P"
344    assume t_notin_Fault: "t \<notin> Fault ` F"
345    from exec show "t \<in> Normal ` Q \<union> Abrupt ` A"
346    proof (cases)
347      fix s'
348      assume exec_c1: "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> Abrupt s'"
349      assume exec_c2: "\<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s'\<rangle> =n\<Rightarrow> t"
350      from cnvalidD [OF valid_c1 ctxt exec_c1 P ]
351      have "Abrupt s' \<in> Abrupt ` R"
352        by auto
353      with cnvalidD [OF valid_c2 ctxt _ _ t_notin_Fault] exec_c2
354      show ?thesis
355        by fastforce
356    next
357      assume exec_c1: "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> t"
358      assume notAbr: "\<not> isAbr t"
359      from cnvalidD [OF valid_c1 ctxt exec_c1 P t_notin_Fault]
360      have "t \<in> Normal ` Q \<union> Abrupt ` R" .
361      with notAbr
362      show ?thesis
363        by auto
364    qed
365  qed
366next
367  case (Conseq P \<Theta> F c Q A)
368  hence adapt: "\<forall>s \<in> P. (\<exists>P' Q' A'. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P' c Q',A'  \<and>
369                          s \<in> P' \<and> Q' \<subseteq> Q \<and> A' \<subseteq> A)"
370    by blast
371  show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
372  proof (rule cnvalidI)
373    fix s t
374    assume ctxt:"\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
375    assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
376    assume P: "s \<in> P"
377    assume t_notin_F: "t \<notin> Fault ` F"
378    show "t \<in> Normal ` Q \<union> Abrupt ` A"
379    proof -
380      from P adapt obtain P' Q' A' Z  where
381        spec: "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P' c Q',A'" and
382        P': "s \<in> P'"  and  strengthen: "Q' \<subseteq> Q \<and> A' \<subseteq> A"
383        by auto
384      from spec [rule_format] ctxt exec P' t_notin_F
385      have "t \<in> Normal ` Q' \<union> Abrupt ` A'"
386        by (rule cnvalidD)
387      with strengthen show ?thesis
388        by blast
389    qed
390  qed
391next
392  case (Asm P p Q A \<Theta> F)
393  have asm: "(P, p, Q, A) \<in> \<Theta>" by fact
394  show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
395  proof (rule cnvalidI)
396    fix s t
397    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
398    assume exec: "\<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> =n\<Rightarrow> t"
399    from asm ctxt have "\<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P Call p Q,A" by auto
400    moreover
401    assume "s \<in> P" "t \<notin> Fault ` F"
402    ultimately
403    show "t \<in> Normal ` Q \<union> Abrupt ` A"
404      using exec
405      by (auto simp add: nvalid_def)
406  qed
407next
408  case ExFalso thus ?case by iprover
409qed
410
411theorem hoare_sound: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> \<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A"
412  by (iprover intro: cnvalid_to_cvalid hoare_cnvalid)
413
414subsection \<open>Completeness\<close>
415
416lemma MGT_valid:
417"\<Gamma>\<Turnstile>\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union>  Fault ` (-F))} c
418   {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
419proof (rule validI)
420  fix s t
421  assume "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
422         "s \<in> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union>  Fault ` (-F))}"
423         "t \<notin> Fault ` F"
424  thus "t \<in> Normal ` {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t} \<union>
425            Abrupt ` {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
426    by (cases t) (auto simp add: final_notin_def)
427qed
428
429text \<open>The consequence rule where the existential @{term Z} is instantiated
430to @{term s}. Usefull in proof of \<open>MGT_lemma\<close>.\<close>
431lemma ConseqMGT:
432  assumes modif: "\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)"
433  assumes impl: "\<And>s. s \<in> P \<Longrightarrow> s \<in> P' s \<and> (\<forall>t. t \<in> Q' s \<longrightarrow> t \<in> Q) \<and>
434                                            (\<forall>t. t \<in> A' s \<longrightarrow> t \<in> A)"
435  shows "\<Gamma>,\<Theta> \<turnstile>\<^bsub>/F\<^esub> P c Q,A"
436using impl
437by -  (rule conseq [OF modif],blast)
438
439
440lemma Seq_NoFaultStuckD1:
441  assumes noabort: "\<Gamma>\<turnstile>\<langle>Seq c1 c2,s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault `  F)"
442  shows "\<Gamma>\<turnstile>\<langle>c1,s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault `  F)"
443proof (rule final_notinI)
444  fix t
445  assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,s\<rangle> \<Rightarrow> t"
446  show "t \<notin> {Stuck} \<union> Fault `  F"
447  proof
448    assume "t \<in> {Stuck} \<union> Fault `  F"
449    moreover
450    {
451      assume "t = Stuck"
452      with exec_c1
453      have "\<Gamma>\<turnstile>\<langle>Seq c1 c2,s\<rangle> \<Rightarrow> Stuck"
454        by (auto intro: exec_Seq')
455      with noabort have False
456        by (auto simp add: final_notin_def)
457      hence False ..
458    }
459    moreover
460    {
461      assume "t \<in> Fault ` F"
462      then obtain f where
463      t: "t=Fault f" and f: "f \<in> F"
464        by auto
465      from t exec_c1
466      have "\<Gamma>\<turnstile>\<langle>Seq c1 c2,s\<rangle> \<Rightarrow> Fault f"
467        by (auto intro: exec_Seq')
468      with noabort f have False
469        by (auto simp add: final_notin_def)
470      hence False ..
471    }
472    ultimately show False by auto
473  qed
474qed
475
476lemma Seq_NoFaultStuckD2:
477  assumes noabort: "\<Gamma>\<turnstile>\<langle>Seq c1 c2,s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault `  F)"
478  shows "\<forall>t. \<Gamma>\<turnstile>\<langle>c1,s\<rangle> \<Rightarrow> t \<longrightarrow> t\<notin> ({Stuck} \<union> Fault `  F) \<longrightarrow>
479             \<Gamma>\<turnstile>\<langle>c2,t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault `  F)"
480using noabort
481by (auto simp add: final_notin_def intro: exec_Seq')
482
483
484lemma MGT_implies_complete:
485  assumes MGT: "\<forall>Z. \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union>  Fault ` (-F))} c
486                           {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},
487                           {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
488  assumes valid: "\<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P c Q,A"
489  shows "\<Gamma>,{} \<turnstile>\<^bsub>/F\<^esub> P c Q,A"
490  using MGT
491  apply (rule ConseqMGT)
492  apply (insert valid)
493  apply (auto simp add: valid_def intro!: final_notinI)
494  done
495
496text \<open>Equipped only with the classic consequence rule @{thm "conseqPrePost"}
497        we can only derive this syntactically more involved version
498        of completeness. But semantically it is equivalent to the "real" one
499        (see below)\<close>
500lemma MGT_implies_complete':
501  assumes MGT: "\<forall>Z. \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub>
502                       {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union>  Fault ` (-F))} c
503                           {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},
504                           {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
505  assumes valid: "\<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P c Q,A"
506  shows "\<Gamma>,{} \<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> s \<in> P} c {t. Z \<in> P \<longrightarrow> t \<in> Q},{t. Z \<in> P \<longrightarrow> t \<in> A}"
507  using MGT [rule_format, of Z]
508  apply (rule conseqPrePost)
509  apply (insert valid)
510  apply   (fastforce simp add: valid_def final_notin_def)
511  apply  (fastforce simp add: valid_def)
512  apply (fastforce simp add: valid_def)
513  done
514
515text \<open>Semantic equivalence of both kind of formulations\<close>
516lemma valid_involved_to_valid:
517  assumes valid:
518    "\<forall>Z. \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> s \<in> P} c {t. Z \<in> P \<longrightarrow> t \<in> Q},{t. Z \<in> P \<longrightarrow> t \<in> A}"
519  shows "\<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P c Q,A"
520  using valid
521  apply (simp add: valid_def)
522  apply clarsimp
523  apply (erule_tac x="x" in allE)
524  apply (erule_tac x="Normal x" in allE)
525  apply (erule_tac x=t in allE)
526  apply fastforce
527  done
528
529text \<open>The sophisticated consequence rule allow us to do this
530        semantical transformation on the hoare-level, too.
531        The magic is, that it allow us to
532        choose the instance of @{term Z} under the assumption of an state @{term "s \<in> P"}\<close>
533lemma
534  assumes deriv:
535    "\<forall>Z. \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> s \<in> P} c {t. Z \<in> P \<longrightarrow> t \<in> Q},{t. Z \<in> P \<longrightarrow> t \<in> A}"
536  shows "\<Gamma>,{} \<turnstile>\<^bsub>/F\<^esub> P c Q,A"
537  apply (rule ConseqMGT [OF deriv])
538  apply auto
539  done
540
541lemma valid_to_valid_involved:
542  "\<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow>
543   \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> s \<in> P} c {t. Z \<in> P \<longrightarrow> t \<in> Q},{t. Z \<in> P \<longrightarrow> t \<in> A}"
544by (simp add: valid_def Collect_conv_if)
545
546lemma
547  assumes deriv: "\<Gamma>,{} \<turnstile>\<^bsub>/F\<^esub> P c Q,A"
548  shows "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> s \<in> P} c {t. Z \<in> P \<longrightarrow> t \<in> Q},{t. Z \<in> P \<longrightarrow> t \<in> A}"
549  apply (rule conseqPrePost [OF deriv])
550  apply auto
551  done
552
553lemma conseq_extract_state_indep_prop:
554  assumes state_indep_prop:"\<forall>s \<in> P. R"
555  assumes to_show: "R \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
556  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
557  apply (rule Conseq)
558  apply (clarify)
559  apply (rule_tac x="P" in exI)
560  apply (rule_tac x="Q" in exI)
561  apply (rule_tac x="A" in exI)
562  using state_indep_prop to_show
563  by blast
564
565
566lemma MGT_lemma:
567  assumes MGT_Calls:
568    "\<forall>p\<in>dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^bsub>/F\<^esub>
569       {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
570        (Call p)
571       {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
572       {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
573  shows "\<And>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c
574             {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
575proof (induct c)
576  case Skip
577  show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Skip,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} Skip
578           {t. \<Gamma>\<turnstile>\<langle>Skip,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>Skip,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
579    by (rule hoarep.Skip [THEN conseqPre])
580       (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
581next
582  case (Basic f)
583  show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Basic f,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} Basic f
584           {t. \<Gamma>\<turnstile>\<langle>Basic f,Normal Z\<rangle> \<Rightarrow> Normal t},
585           {t. \<Gamma>\<turnstile>\<langle>Basic f,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
586    by (rule hoarep.Basic [THEN conseqPre])
587       (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
588next
589  case (Spec r)
590  show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Spec r,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} Spec r
591           {t. \<Gamma>\<turnstile>\<langle>Spec r,Normal Z\<rangle> \<Rightarrow> Normal t},
592           {t. \<Gamma>\<turnstile>\<langle>Spec r,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
593    apply (rule hoarep.Spec [THEN conseqPre])
594    apply (clarsimp simp add: final_notin_def)
595    apply (case_tac "\<exists>t. (Z,t) \<in> r")
596    apply (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
597    done
598next
599  case (Seq c1 c2)
600  have hyp_c1: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c1
601                           {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t},
602                           {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
603    using Seq.hyps by iprover
604  have hyp_c2: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c2
605                          {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t},
606                          {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
607    using Seq.hyps by iprover
608  from hyp_c1
609  have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c1
610              {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t \<and>
611                  \<Gamma>\<turnstile>\<langle>c2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))},
612              {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
613    by (rule ConseqMGT)
614       (auto dest: Seq_NoFaultStuckD1 [simplified] Seq_NoFaultStuckD2 [simplified]
615             intro: exec.Seq)
616  thus "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
617                   Seq c1 c2
618              {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
619              {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
620  proof (rule hoarep.Seq )
621    show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t \<and>
622                      \<Gamma>\<turnstile>\<langle>c2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
623                   c2
624                 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
625                 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
626    proof (rule ConseqMGT [OF hyp_c2],safe)
627      fix r t
628      assume "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal r" "\<Gamma>\<turnstile>\<langle>c2,Normal r\<rangle> \<Rightarrow> Normal t"
629      then show "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t"
630        by (iprover intro: exec.intros)
631    next
632      fix r t
633      assume "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal r" "\<Gamma>\<turnstile>\<langle>c2,Normal r\<rangle> \<Rightarrow> Abrupt t"
634      then show "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t"
635        by (iprover intro: exec.intros)
636    qed
637  qed
638next
639  case (Cond b c1 c2)
640  have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c1
641                 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t},
642                 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
643    using Cond.hyps by iprover
644  hence "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}\<inter>b)
645                   c1
646                {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
647                {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
648    by (rule ConseqMGT)
649       (fastforce intro: exec.CondTrue simp add: final_notin_def)
650  moreover
651  have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c2
652                    {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t},
653                    {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
654    using Cond.hyps by iprover
655  hence "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}\<inter>-b)
656                  c2
657                {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
658                {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
659    by (rule ConseqMGT)
660       (fastforce intro: exec.CondFalse simp add: final_notin_def)
661  ultimately
662  show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
663                 Cond b c1 c2
664              {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
665              {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
666    by (rule hoarep.Cond)
667next
668  case (While b c)
669  let ?unroll = "({(s,t). s\<in>b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t})\<^sup>*"
670  let ?P' = "\<lambda>Z. {t. (Z,t)\<in>?unroll \<and>
671                    (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b
672                         \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
673                             (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
674                                  \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u))}"
675  let ?A' = "\<lambda>Z. {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
676  show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
677                While b c
678              {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t},
679              {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
680  proof (rule ConseqMGT [where ?P'="?P'"
681                         and ?Q'="\<lambda>Z. ?P' Z \<inter> - b" and ?A'="?A'"])
682    show "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (?P' Z) (While b c) (?P' Z \<inter> - b),(?A' Z)"
683    proof (rule allI, rule hoarep.While)
684      fix Z
685      from While
686      have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c
687                        {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},
688                        {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by iprover
689      then show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (?P' Z  \<inter> b) c (?P' Z),(?A' Z)"
690      proof (rule ConseqMGT)
691        fix s
692        assume  "s\<in> {t. (Z, t) \<in> ?unroll \<and>
693                      (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b
694                           \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
695                               (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
696                                    \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u))}
697                   \<inter> b"
698        then obtain
699          Z_s_unroll: "(Z,s) \<in> ?unroll" and
700          noabort:"\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b
701                        \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
702                            (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
703                                  \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" and
704          s_in_b: "s\<in>b"
705          by blast
706        show "s \<in> {t. t = s \<and> \<Gamma>\<turnstile>\<langle>c,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} \<and>
707        (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t} \<longrightarrow>
708             t \<in> {t. (Z, t) \<in> ?unroll \<and>
709                  (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow>  e\<in>b
710                       \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
711                           (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
712                                  \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u))}) \<and>
713         (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t} \<longrightarrow>
714             t \<in> {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t})"
715          (is "?C1 \<and> ?C2 \<and> ?C3")
716        proof (intro conjI)
717          from Z_s_unroll noabort s_in_b show ?C1 by blast
718        next
719          {
720            fix t
721            assume s_t: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t"
722            moreover
723            from Z_s_unroll s_t s_in_b
724            have "(Z, t) \<in> ?unroll"
725              by (blast intro: rtrancl_into_rtrancl)
726            moreover note noabort
727            ultimately
728            have "(Z, t) \<in> ?unroll \<and>
729                  (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b
730                        \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
731                            (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
732                                  \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u))"
733              by iprover
734          }
735          then show ?C2 by blast
736        next
737          {
738            fix t
739            assume s_t:  "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t"
740            from Z_s_unroll noabort s_t s_in_b
741            have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t"
742              by blast
743          } thus ?C3 by simp
744        qed
745      qed
746    qed
747  next
748    fix s
749    assume P: "s \<in> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}"
750    hence WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
751      by auto
752    show "s \<in> ?P' s \<and>
753    (\<forall>t. t\<in>(?P' s \<inter> - b)\<longrightarrow>
754         t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t})\<and>
755    (\<forall>t. t\<in>?A' s \<longrightarrow> t\<in>?A' Z)"
756    proof (intro conjI)
757      {
758        fix e
759        assume "(Z,e) \<in> ?unroll" "e \<in> b"
760        from this WhileNoFault
761        have "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
762               (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
763                    \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" (is "?Prop Z e")
764        proof (induct rule: converse_rtrancl_induct [consumes 1])
765          assume e_in_b: "e \<in> b"
766          assume WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
767          with e_in_b WhileNoFault
768          have cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
769            by (auto simp add: final_notin_def intro: exec.intros)
770          moreover
771          {
772            fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u"
773            with e_in_b have "\<Gamma>\<turnstile>\<langle>While b c,Normal e\<rangle> \<Rightarrow> Abrupt u"
774              by (blast intro: exec.intros)
775          }
776          ultimately
777          show "?Prop e e"
778            by iprover
779        next
780          fix Z r
781          assume e_in_b: "e\<in>b"
782          assume WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
783          assume hyp: "\<lbrakk>e\<in>b;\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))\<rbrakk>
784                       \<Longrightarrow> ?Prop r e"
785          assume Z_r:
786            "(Z, r) \<in> {(Z, r). Z \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r}"
787          with WhileNoFault
788          have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
789            by (auto simp add: final_notin_def intro: exec.intros)
790          from hyp [OF e_in_b this] obtain
791            cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" and
792            Abrupt_r: "\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u \<longrightarrow>
793                            \<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u"
794            by simp
795
796           {
797            fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u"
798            with Abrupt_r have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u" by simp
799            moreover from  Z_r obtain
800              "Z \<in> b"  "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r"
801              by simp
802            ultimately have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u"
803              by (blast intro: exec.intros)
804          }
805          with cNoFault show "?Prop Z e"
806            by iprover
807        qed
808      }
809      with P show "s \<in> ?P' s"
810        by blast
811    next
812      {
813        fix t
814        assume "termination": "t \<notin> b"
815        assume "(Z, t) \<in> ?unroll"
816        hence "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t"
817        proof (induct rule: converse_rtrancl_induct [consumes 1])
818          from "termination"
819          show "\<Gamma>\<turnstile>\<langle>While b c,Normal t\<rangle> \<Rightarrow> Normal t"
820            by (blast intro: exec.WhileFalse)
821        next
822          fix Z r
823          assume first_body:
824                 "(Z, r) \<in> {(s, t). s \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t}"
825          assume "(r, t) \<in> ?unroll"
826          assume rest_loop: "\<Gamma>\<turnstile>\<langle>While b c, Normal r\<rangle> \<Rightarrow> Normal t"
827          show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t"
828          proof -
829            from first_body obtain
830              "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r"
831              by fast
832            moreover
833            from rest_loop have
834              "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Normal t"
835              by fast
836            ultimately show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t"
837              by (rule exec.WhileTrue)
838          qed
839        qed
840      }
841      with P
842      show "(\<forall>t. t\<in>(?P' s \<inter> - b)
843            \<longrightarrow>t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t})"
844        by blast
845    next
846      from P show "\<forall>t. t\<in>?A' s \<longrightarrow> t\<in>?A' Z" by simp
847    qed
848  qed
849next
850  case (Call p)
851  let ?P = "{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}"
852  from noStuck_Call have "\<forall>s \<in> ?P. p \<in> dom \<Gamma>"
853    by (fastforce simp add: final_notin_def )
854  then show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ?P (Call p)
855               {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
856               {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
857  proof (rule conseq_extract_state_indep_prop)
858    assume p_definied: "p \<in> dom \<Gamma>"
859    with MGT_Calls show
860      "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s=Z \<and>
861                 \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
862                  (Call p)
863                 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
864                 {t. \<Gamma>\<turnstile>\<langle>Call  p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
865      by (auto)
866  qed
867next
868  case (DynCom c)
869  have hyp:
870    "\<And>s'. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c s',Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c s'
871      {t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Abrupt t}"
872    using DynCom by simp
873  have hyp':
874  "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s = Z \<and> \<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c Z
875        {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
876    by (rule ConseqMGT [OF hyp])
877       (fastforce simp add: final_notin_def intro: exec.intros)
878  show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s = Z \<and> \<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
879               DynCom c
880             {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t},
881             {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
882    apply (rule hoarep.DynCom)
883    apply (clarsimp)
884    apply (rule hyp' [simplified])
885    done
886next
887  case (Guard f g c)
888  have hyp_c: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c
889                    {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},
890                    {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
891    using Guard by iprover
892  show ?case
893  proof (cases "f \<in> F")
894    case True
895    from hyp_c
896    have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>(g \<inter> {s. s = Z \<and>
897                    \<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (- F))})
898             c
899           {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Normal t},
900           {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
901      apply (rule ConseqMGT)
902      apply (insert True)
903      apply (auto simp add: final_notin_def intro: exec.intros)
904      done
905    from True this
906    show ?thesis
907      by (rule conseqPre [OF Guarantee]) auto
908  next
909    case False
910    from hyp_c
911    have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>
912           (g \<inter> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))})
913           c
914           {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Normal t},
915           {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
916      apply (rule ConseqMGT)
917      apply clarify
918      apply (frule Guard_noFaultStuckD [OF _ False])
919      apply (auto simp add: final_notin_def intro: exec.intros)
920      done
921    then show ?thesis
922      apply (rule conseqPre [OF hoarep.Guard])
923      apply clarify
924      apply (frule Guard_noFaultStuckD [OF _ False])
925      apply auto
926      done
927  qed
928next
929  case Throw
930  show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Throw,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} Throw
931              {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Normal t},
932              {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
933    by (rule conseqPre [OF hoarep.Throw]) (blast intro: exec.intros)
934next
935  case (Catch c\<^sub>1 c\<^sub>2)
936  have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c\<^sub>1
937                  {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Normal t},
938                  {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
939    using Catch.hyps by iprover
940  hence "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c\<^sub>1
941               {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},
942               {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t \<and>
943                   \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}"
944    by (rule ConseqMGT)
945       (fastforce intro: exec.intros simp add: final_notin_def)
946  moreover
947  have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c\<^sub>2
948                  {t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},
949                  {t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
950    using Catch.hyps by iprover
951  hence "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow>Abrupt s \<and>
952                   \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
953               c\<^sub>2
954               {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},
955               {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
956    by (rule ConseqMGT)
957       (fastforce intro: exec.intros  simp add: final_notin_def)
958  ultimately
959  show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
960                   Catch c\<^sub>1 c\<^sub>2
961              {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},
962              {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
963    by (rule hoarep.Catch)
964qed
965
966lemma MGT_Calls:
967 "\<forall>p\<in>dom \<Gamma>. \<forall>Z.
968     \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
969            (Call p)
970          {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
971          {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
972proof -
973  {
974    fix p Z
975    assume defined: "p \<in> dom \<Gamma>"
976    have
977      "\<Gamma>,(\<Union>p\<in>dom \<Gamma>. \<Union>Z.
978          {({s. s=Z \<and>
979             \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))},
980             p,
981             {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
982             {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t})})
983       \<turnstile>\<^bsub>/F\<^esub>{s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
984          (the (\<Gamma> p))
985          {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
986          {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
987      (is "\<Gamma>,?\<Theta> \<turnstile>\<^bsub>/F\<^esub> (?Pre p Z) (the (\<Gamma> p)) (?Post p Z),(?Abr p Z)")
988    proof -
989      have MGT_Calls:
990       "\<forall>p\<in>dom \<Gamma>. \<forall>Z. \<Gamma>,?\<Theta> \<turnstile>\<^bsub>/F\<^esub>
991        {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
992         (Call p)
993        {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
994        {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
995        by (intro ballI allI, rule HoarePartialDef.Asm,auto)
996      have "\<forall>Z. \<Gamma>,?\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>the (\<Gamma> p) ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault`(-F))}
997                        (the (\<Gamma> p))
998                        {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t},
999                        {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1000        by (iprover intro: MGT_lemma [OF MGT_Calls])
1001      thus "\<Gamma>,?\<Theta>\<turnstile>\<^bsub>/F\<^esub> (?Pre p Z) (the (\<Gamma> p)) (?Post p Z),(?Abr p Z)"
1002        apply (rule ConseqMGT)
1003        apply (clarify,safe)
1004      proof -
1005        assume "\<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1006        with defined show "\<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1007          by (fastforce simp add: final_notin_def
1008                intro: exec.intros)
1009      next
1010        fix t
1011        assume "\<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t"
1012        with defined
1013        show "\<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow>Normal t"
1014          by  (auto intro: exec.Call)
1015      next
1016        fix t
1017        assume "\<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t"
1018        with defined
1019        show "\<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow>Abrupt t"
1020          by  (auto intro: exec.Call)
1021      qed
1022    qed
1023  }
1024  then show ?thesis
1025    apply -
1026    apply (intro ballI allI)
1027    apply (rule CallRec' [where Procs="dom \<Gamma>"  and
1028      P="\<lambda>p Z. {s. s=Z \<and>
1029                  \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}"and
1030      Q="\<lambda>p Z.
1031        {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}" and
1032      A="\<lambda>p Z.
1033        {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"] )
1034    apply simp+
1035    done
1036qed
1037
1038theorem hoare_complete: "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
1039  by (iprover intro: MGT_implies_complete MGT_lemma [OF MGT_Calls])
1040
1041lemma hoare_complete':
1042  assumes cvalid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
1043  shows  "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
1044proof (cases "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A")
1045  case True
1046  hence "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
1047    by (rule hoare_complete)
1048  thus "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P c Q,A"
1049    by (rule hoare_augment_context) simp
1050next
1051  case False
1052  with cvalid
1053  show ?thesis
1054    by (rule ExFalso)
1055qed
1056
1057
1058lemma hoare_strip_\<Gamma>:
1059  assumes deriv: "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P p Q,A"
1060  assumes F': "F' \<subseteq> -F"
1061  shows "strip F' \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P p Q,A"
1062proof (rule hoare_complete)
1063  from hoare_sound [OF deriv] have "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P p Q,A"
1064    by (simp add: cvalid_def)
1065  from this F'
1066  show "strip F' \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P p Q,A"
1067    by (rule valid_to_valid_strip)
1068qed
1069
1070
1071subsection \<open>And Now: Some Useful Rules\<close>
1072
1073subsubsection \<open>Consequence\<close>
1074
1075
1076lemma LiberalConseq_sound:
1077fixes F::"'f set"
1078assumes cons: "\<forall>s \<in> P. \<forall>(t::('s,'f) xstate). \<exists>P' Q' A'. (\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P' c Q',A') \<and>
1079                ((s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A')
1080                              \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A)"
1081shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A "
1082proof (rule cnvalidI)
1083  fix s t
1084  assume ctxt:"\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
1085  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
1086  assume P: "s \<in> P"
1087  assume t_notin_F: "t \<notin> Fault ` F"
1088  show "t \<in> Normal ` Q \<union> Abrupt ` A"
1089  proof -
1090    from P cons obtain P' Q' A' where
1091      spec: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P' c Q',A'" and
1092      adapt: "(s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A')
1093                              \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A"
1094      apply -
1095      apply (drule (1) bspec)
1096      apply (erule_tac x=t in allE)
1097      apply (elim exE conjE)
1098      apply iprover
1099      done
1100    from exec spec ctxt t_notin_F
1101    have "s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A'"
1102      by (simp add: cnvalid_def nvalid_def)
1103    with adapt show ?thesis
1104      by simp
1105  qed
1106qed
1107
1108lemma LiberalConseq:
1109fixes F:: "'f set"
1110assumes cons: "\<forall>s \<in> P.  \<forall>(t::('s,'f) xstate). \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' c Q',A' \<and>
1111                ((s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A')
1112                              \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A)"
1113shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A "
1114apply (rule hoare_complete')
1115apply (rule allI)
1116apply (rule LiberalConseq_sound)
1117using cons
1118apply (clarify)
1119apply (drule (1) bspec)
1120apply (erule_tac x=t in allE)
1121apply clarify
1122apply (rule_tac x=P' in exI)
1123apply (rule_tac x=Q' in exI)
1124apply (rule_tac x=A' in exI)
1125apply (rule conjI)
1126apply (blast intro: hoare_cnvalid)
1127apply assumption
1128done
1129
1130lemma "\<forall>s \<in> P. \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' c Q',A' \<and> s \<in> P' \<and> Q' \<subseteq> Q \<and> A' \<subseteq> A
1131           \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
1132  apply (rule LiberalConseq)
1133  apply (rule ballI)
1134  apply (drule (1) bspec)
1135  apply clarify
1136  apply (rule_tac x=P' in exI)
1137  apply (rule_tac x=Q' in exI)
1138  apply (rule_tac x=A' in exI)
1139  apply auto
1140  done
1141
1142lemma
1143fixes F:: "'f set"
1144assumes cons: "\<forall>s \<in> P.  \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' c Q',A' \<and>
1145                (\<forall>(t::('s,'f) xstate). (s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A')
1146                              \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A)"
1147shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A "
1148  apply (rule Conseq)
1149  apply (rule ballI)
1150  apply (insert cons)
1151  apply (drule (1) bspec)
1152  apply clarify
1153  apply (rule_tac x=P' in exI)
1154  apply (rule_tac x=Q' in exI)
1155  apply (rule_tac x=A' in exI)
1156  apply (rule conjI)
1157  apply  assumption
1158  (* no way to get s \<in> P' *)
1159  oops
1160
1161lemma LiberalConseq':
1162fixes F:: "'f set"
1163assumes cons: "\<forall>s \<in> P.  \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' c Q',A' \<and>
1164                (\<forall>(t::('s,'f) xstate). (s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A')
1165                              \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A)"
1166shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A "
1167apply (rule LiberalConseq)
1168apply (rule ballI)
1169apply (rule allI)
1170apply (insert cons)
1171apply (drule (1) bspec)
1172apply clarify
1173apply (rule_tac x=P' in exI)
1174apply (rule_tac x=Q' in exI)
1175apply (rule_tac x=A' in exI)
1176apply iprover
1177done
1178
1179lemma LiberalConseq'':
1180fixes F:: "'f set"
1181assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)"
1182assumes cons: "\<forall>s (t::('s,'f) xstate).
1183                 (\<forall>Z. s \<in> P' Z \<longrightarrow> t \<in> Normal ` Q' Z \<union> Abrupt ` A' Z)
1184                  \<longrightarrow> (s \<in> P \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A)"
1185shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A "
1186apply (rule LiberalConseq)
1187apply (rule ballI)
1188apply (rule allI)
1189apply (insert cons)
1190apply (erule_tac x=s in allE)
1191apply (erule_tac x=t in allE)
1192apply (case_tac "t \<in> Normal ` Q \<union> Abrupt ` A")
1193apply (insert spec)
1194apply  iprover
1195apply auto
1196done
1197
1198primrec procs:: "('s,'p,'f) com \<Rightarrow> 'p set"
1199where
1200"procs Skip = {}" |
1201"procs (Basic f) = {}" |
1202"procs (Seq c\<^sub>1 c\<^sub>2)  = (procs c\<^sub>1 \<union> procs c\<^sub>2)" |
1203"procs (Cond b c\<^sub>1 c\<^sub>2) = (procs c\<^sub>1 \<union> procs c\<^sub>2)" |
1204"procs (While b c) = procs c" |
1205"procs (Call p) = {p}" |
1206"procs (DynCom c) = (\<Union>s. procs (c s))" |
1207"procs (Guard f g c) = procs c" |
1208"procs Throw = {}" |
1209"procs (Catch c\<^sub>1 c\<^sub>2) = (procs c\<^sub>1 \<union> procs c\<^sub>2)"
1210
1211primrec noSpec:: "('s,'p,'f) com \<Rightarrow> bool"
1212where
1213"noSpec Skip = True" |
1214"noSpec (Basic f) = True" |
1215"noSpec (Spec r) = False" |
1216"noSpec (Seq c\<^sub>1 c\<^sub>2)  = (noSpec c\<^sub>1 \<and> noSpec c\<^sub>2)" |
1217"noSpec (Cond b c\<^sub>1 c\<^sub>2) = (noSpec c\<^sub>1 \<and> noSpec c\<^sub>2)" |
1218"noSpec (While b c) = noSpec c" |
1219"noSpec (Call p) = True" |
1220"noSpec (DynCom c) = (\<forall>s. noSpec (c s))" |
1221"noSpec (Guard f g c) = noSpec c" |
1222"noSpec Throw = True" |
1223"noSpec (Catch c\<^sub>1 c\<^sub>2) = (noSpec c\<^sub>1 \<and> noSpec c\<^sub>2)"
1224
1225lemma exec_noSpec_no_Stuck:
1226 assumes exec: "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t"
1227 assumes noSpec_c: "noSpec c"
1228 assumes noSpec_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noSpec (the (\<Gamma> p))"
1229 assumes procs_subset: "procs c \<subseteq> dom \<Gamma>"
1230 assumes procs_subset_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. procs (the (\<Gamma> p)) \<subseteq> dom \<Gamma>"
1231 assumes s_no_Stuck: "s\<noteq>Stuck"
1232 shows "t\<noteq>Stuck"
1233using exec noSpec_c procs_subset s_no_Stuck proof induct
1234  case (Call p bdy s t) with noSpec_\<Gamma> procs_subset_\<Gamma> show ?case
1235    by (auto dest!: bspec [of _ _ p])
1236next
1237  case (DynCom c s t) then show ?case
1238   by auto blast
1239qed auto
1240
1241lemma execn_noSpec_no_Stuck:
1242 assumes exec: "\<Gamma>\<turnstile>\<langle>c,s\<rangle> =n\<Rightarrow> t"
1243 assumes noSpec_c: "noSpec c"
1244 assumes noSpec_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noSpec (the (\<Gamma> p))"
1245 assumes procs_subset: "procs c \<subseteq> dom \<Gamma>"
1246 assumes procs_subset_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. procs (the (\<Gamma> p)) \<subseteq> dom \<Gamma>"
1247 assumes s_no_Stuck: "s\<noteq>Stuck"
1248 shows "t\<noteq>Stuck"
1249using exec noSpec_c procs_subset s_no_Stuck proof induct
1250  case (Call p bdy n s t) with noSpec_\<Gamma> procs_subset_\<Gamma> show ?case
1251    by (auto dest!: bspec [of _ _ p])
1252next
1253  case (DynCom c s t) then show ?case
1254    by auto blast
1255qed auto
1256
1257lemma LiberalConseq_noguards_nothrows_sound:
1258assumes spec: "\<forall>Z. \<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)"
1259assumes cons: "\<forall>s t. (\<forall>Z. s \<in> P' Z \<longrightarrow> t \<in>  Q' Z )
1260                  \<longrightarrow> (s \<in> P \<longrightarrow> t \<in> Q )"
1261assumes noguards_c: "noguards c"
1262assumes noguards_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noguards (the (\<Gamma> p))"
1263assumes nothrows_c: "nothrows c"
1264assumes nothrows_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. nothrows (the (\<Gamma> p))"
1265assumes noSpec_c: "noSpec c"
1266assumes noSpec_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noSpec (the (\<Gamma> p))"
1267assumes procs_subset: "procs c \<subseteq> dom \<Gamma>"
1268assumes procs_subset_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. procs (the (\<Gamma> p)) \<subseteq> dom \<Gamma>"
1269shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A "
1270proof (rule cnvalidI)
1271  fix s t
1272  assume ctxt:"\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
1273  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
1274  assume P: "s \<in> P"
1275  assume t_notin_F: "t \<notin> Fault ` F"
1276  show "t \<in> Normal ` Q \<union> Abrupt ` A"
1277  proof -
1278    from execn_noguards_no_Fault [OF exec noguards_c noguards_\<Gamma>]
1279     execn_nothrows_no_Abrupt [OF exec nothrows_c nothrows_\<Gamma> ]
1280     execn_noSpec_no_Stuck [OF exec
1281              noSpec_c  noSpec_\<Gamma> procs_subset
1282      procs_subset_\<Gamma>]
1283    obtain t' where t: "t=Normal t'"
1284      by (cases t) auto
1285    with exec spec ctxt
1286    have "(\<forall>Z. s \<in> P' Z \<longrightarrow> t' \<in>  Q' Z)"
1287      by (unfold  cnvalid_def nvalid_def) blast
1288    with cons P t show ?thesis
1289      by simp
1290  qed
1291qed
1292
1293
1294lemma LiberalConseq_noguards_nothrows:
1295assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)"
1296assumes cons: "\<forall>s t. (\<forall>Z. s \<in> P' Z \<longrightarrow> t \<in>  Q' Z )
1297                  \<longrightarrow> (s \<in> P \<longrightarrow> t \<in> Q )"
1298assumes noguards_c: "noguards c"
1299assumes noguards_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noguards (the (\<Gamma> p))"
1300assumes nothrows_c: "nothrows c"
1301assumes nothrows_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. nothrows (the (\<Gamma> p))"
1302assumes noSpec_c: "noSpec c"
1303assumes noSpec_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noSpec (the (\<Gamma> p))"
1304assumes procs_subset: "procs c \<subseteq> dom \<Gamma>"
1305assumes procs_subset_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. procs (the (\<Gamma> p)) \<subseteq> dom \<Gamma>"
1306shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A "
1307apply (rule hoare_complete')
1308apply (rule allI)
1309apply (rule LiberalConseq_noguards_nothrows_sound
1310             [OF _ cons noguards_c noguards_\<Gamma> nothrows_c nothrows_\<Gamma>
1311                 noSpec_c noSpec_\<Gamma>
1312                 procs_subset procs_subset_\<Gamma>])
1313apply (insert spec)
1314apply (intro allI)
1315apply (erule_tac x=Z in allE)
1316by (rule hoare_cnvalid)
1317
1318lemma
1319assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s=fst Z \<and> P s (snd Z)} c {t. Q (fst Z) (snd Z) t},{}"
1320assumes noguards_c: "noguards c"
1321assumes noguards_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noguards (the (\<Gamma> p))"
1322assumes nothrows_c: "nothrows c"
1323assumes nothrows_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. nothrows (the (\<Gamma> p))"
1324assumes noSpec_c: "noSpec c"
1325assumes noSpec_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noSpec (the (\<Gamma> p))"
1326assumes procs_subset: "procs c \<subseteq> dom \<Gamma>"
1327assumes procs_subset_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. procs (the (\<Gamma> p)) \<subseteq> dom \<Gamma>"
1328shows "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s=\<sigma>} c {t. \<forall>l. P \<sigma> l \<longrightarrow> Q \<sigma> l t},{}"
1329apply (rule allI)
1330apply (rule LiberalConseq_noguards_nothrows
1331              [OF spec _ noguards_c noguards_\<Gamma> nothrows_c nothrows_\<Gamma>
1332                  noSpec_c noSpec_\<Gamma>
1333                  procs_subset procs_subset_\<Gamma>])
1334apply auto
1335done
1336
1337subsubsection \<open>Modify Return\<close>
1338
1339lemma ProcModifyReturn_sound:
1340  assumes valid_call: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P call init p return' c Q,A"
1341  assumes valid_modif:
1342    "\<forall>\<sigma>. \<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/UNIV\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
1343  assumes ret_modif:
1344    "\<forall>s t. t \<in> Modif (init s)
1345           \<longrightarrow> return' s t = return s t"
1346  assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
1347                             \<longrightarrow> return' s t = return s t"
1348  shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (call init p return c) Q,A"
1349proof (rule cnvalidI)
1350  fix s t
1351  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
1352  then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/UNIV\<^esub> P (Call p) Q,A"
1353    by (auto intro: nvalid_augment_Faults)
1354  assume exec: "\<Gamma>\<turnstile>\<langle>call init p return c,Normal s\<rangle> =n\<Rightarrow> t"
1355  assume P: "s \<in> P"
1356  assume t_notin_F: "t \<notin> Fault ` F"
1357  from exec
1358  show "t \<in> Normal ` Q \<union> Abrupt ` A"
1359  proof (cases rule: execn_call_Normal_elim)
1360    fix bdy m t'
1361    assume bdy: "\<Gamma> p = Some bdy"
1362    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'"
1363    assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc m\<Rightarrow> t"
1364    assume n: "n = Suc m"
1365    from exec_body n bdy
1366    have "\<Gamma>\<turnstile>\<langle>Call p,Normal (init s)\<rangle> =n\<Rightarrow> Normal t'"
1367      by (auto simp add: intro: execn.Call)
1368    from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt' this] P
1369    have "t' \<in> Modif (init s)"
1370      by auto
1371    with ret_modif have "Normal (return' s t') =
1372      Normal (return s t')"
1373      by simp
1374    with exec_body exec_c bdy n
1375    have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1376      by (auto intro: execn_call)
1377    from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
1378    show ?thesis
1379      by simp
1380  next
1381    fix bdy m t'
1382    assume bdy: "\<Gamma> p = Some bdy"
1383    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'"
1384    assume n: "n = Suc m"
1385    assume t: "t = Abrupt (return s t')"
1386    also from exec_body n bdy
1387    have "\<Gamma>\<turnstile>\<langle>Call p,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t'"
1388      by (auto simp add: intro: execn.intros)
1389    from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt' this] P
1390    have "t' \<in> ModifAbr (init s)"
1391      by auto
1392    with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
1393      by simp
1394    finally have "t = Abrupt (return' s t')"  .
1395    with exec_body bdy n
1396    have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1397      by (auto intro: execn_callAbrupt)
1398    from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
1399    show ?thesis
1400      by simp
1401  next
1402    fix bdy m f
1403    assume bdy: "\<Gamma> p = Some bdy"
1404    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f" "n = Suc m"
1405      "t = Fault f"
1406    with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t"
1407      by (auto intro: execn_callFault)
1408    from valid_call [rule_format] ctxt this P t_notin_F
1409    show ?thesis
1410      by (rule cnvalidD)
1411  next
1412    fix bdy m
1413    assume bdy: "\<Gamma> p = Some bdy"
1414    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m"
1415      "t = Stuck"
1416    with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t"
1417      by (auto intro: execn_callStuck)
1418    from valid_call [rule_format] ctxt this P t_notin_F
1419    show ?thesis
1420      by (rule cnvalidD)
1421  next
1422    fix m
1423    assume "\<Gamma> p = None"
1424    and  "n = Suc m" "t = Stuck"
1425    then have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t"
1426      by (auto intro: execn_callUndefined)
1427    from valid_call [rule_format] ctxt this P t_notin_F
1428    show ?thesis
1429      by (rule cnvalidD)
1430  qed
1431qed
1432
1433
1434lemma ProcModifyReturn:
1435  assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return' c) Q,A"
1436  assumes result_conform:
1437      "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)"
1438  assumes return_conform:
1439      "\<forall>s t. t \<in> ModifAbr (init s)
1440             \<longrightarrow> (return' s t) = (return s t)"
1441  assumes modifies_spec:
1442  "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
1443  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return c) Q,A"
1444apply (rule hoare_complete')
1445apply (rule allI)
1446apply (rule ProcModifyReturn_sound
1447          [where Modif=Modif and ModifAbr=ModifAbr,
1448            OF _ _ result_conform return_conform] )
1449using spec
1450apply (blast intro: hoare_cnvalid)
1451using modifies_spec
1452apply (blast intro: hoare_cnvalid)
1453done
1454
1455lemma ProcModifyReturnSameFaults_sound:
1456  assumes valid_call: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P call init p return' c Q,A"
1457  assumes valid_modif:
1458    "\<forall>\<sigma>. \<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
1459  assumes ret_modif:
1460    "\<forall>s t. t \<in> Modif (init s)
1461           \<longrightarrow> return' s t = return s t"
1462  assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
1463                             \<longrightarrow> return' s t = return s t"
1464  shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (call init p return c) Q,A"
1465proof (rule cnvalidI)
1466  fix s t
1467  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
1468  assume exec: "\<Gamma>\<turnstile>\<langle>call init p return c,Normal s\<rangle> =n\<Rightarrow> t"
1469  assume P: "s \<in> P"
1470  assume t_notin_F: "t \<notin> Fault ` F"
1471  from exec
1472  show "t \<in> Normal ` Q \<union> Abrupt ` A"
1473  proof (cases rule: execn_call_Normal_elim)
1474    fix bdy m t'
1475    assume bdy: "\<Gamma> p = Some bdy"
1476    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'"
1477    assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc m\<Rightarrow> t"
1478    assume n: "n = Suc m"
1479    from exec_body n bdy
1480    have "\<Gamma>\<turnstile>\<langle>Call p,Normal (init s)\<rangle> =n\<Rightarrow> Normal t'"
1481      by (auto simp add: intro: execn.intros)
1482    from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt this] P
1483    have "t' \<in> Modif (init s)"
1484      by auto
1485    with ret_modif have "Normal (return' s t') =
1486      Normal (return s t')"
1487      by simp
1488    with exec_body exec_c bdy n
1489    have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1490      by (auto intro: execn_call)
1491    from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
1492    show ?thesis
1493      by simp
1494  next
1495    fix bdy m t'
1496    assume bdy: "\<Gamma> p = Some bdy"
1497    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'"
1498    assume n: "n = Suc m"
1499    assume t: "t = Abrupt (return s t')"
1500    also
1501    from exec_body n bdy
1502    have "\<Gamma>\<turnstile>\<langle>Call p,Normal (init s)\<rangle> =n \<Rightarrow> Abrupt t'"
1503      by (auto simp add: intro: execn.intros)
1504    from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt this] P
1505    have "t' \<in> ModifAbr (init s)"
1506      by auto
1507    with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
1508      by simp
1509    finally have "t = Abrupt (return' s t')" .
1510    with exec_body bdy n
1511    have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1512      by (auto intro: execn_callAbrupt)
1513    from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
1514    show ?thesis
1515      by simp
1516  next
1517    fix bdy m f
1518    assume bdy: "\<Gamma> p = Some bdy"
1519    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f" "n = Suc m"  and
1520      t: "t = Fault f"
1521    with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t"
1522      by (auto intro: execn_callFault)
1523    from cnvalidD [OF valid_call [rule_format] ctxt this P] t t_notin_F
1524    show ?thesis
1525      by simp
1526  next
1527    fix bdy m
1528    assume bdy: "\<Gamma> p = Some bdy"
1529    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m"
1530      "t = Stuck"
1531    with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t"
1532      by (auto intro: execn_callStuck)
1533    from valid_call [rule_format] ctxt this P t_notin_F
1534    show ?thesis
1535      by (rule cnvalidD)
1536  next
1537    fix m
1538    assume "\<Gamma> p = None"
1539    and  "n = Suc m" "t = Stuck"
1540    then have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t"
1541      by (auto intro: execn_callUndefined)
1542    from valid_call [rule_format] ctxt this P t_notin_F
1543    show ?thesis
1544      by (rule cnvalidD)
1545  qed
1546qed
1547
1548
1549lemma ProcModifyReturnSameFaults:
1550  assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return' c) Q,A"
1551  assumes result_conform:
1552      "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)"
1553  assumes return_conform:
1554  "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> (return' s t) = (return s t)"
1555  assumes modifies_spec:
1556  "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
1557  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return c) Q,A"
1558apply (rule hoare_complete')
1559apply (rule allI)
1560apply (rule ProcModifyReturnSameFaults_sound
1561          [where Modif=Modif and ModifAbr=ModifAbr,
1562         OF _ _ result_conform return_conform])
1563using spec
1564apply (blast intro: hoare_cnvalid)
1565using modifies_spec
1566apply (blast intro: hoare_cnvalid)
1567done
1568
1569subsubsection \<open>DynCall\<close>
1570
1571lemma dynProcModifyReturn_sound:
1572assumes valid_call: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
1573assumes valid_modif:
1574    "\<forall>s \<in> P. \<forall>\<sigma>. \<forall>n.
1575       \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
1576assumes ret_modif:
1577    "\<forall>s t. t \<in> Modif (init s)
1578           \<longrightarrow> return' s t = return s t"
1579assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
1580                             \<longrightarrow> return' s t = return s t"
1581shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
1582proof (rule cnvalidI)
1583  fix s t
1584  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
1585  then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/UNIV\<^esub> P (Call p) Q,A"
1586    by (auto intro: nvalid_augment_Faults)
1587  assume exec: "\<Gamma>\<turnstile>\<langle>dynCall init p return c,Normal s\<rangle> =n\<Rightarrow> t"
1588  assume t_notin_F: "t \<notin> Fault ` F"
1589  assume P: "s \<in> P"
1590  with valid_modif
1591  have valid_modif': "\<forall>\<sigma>. \<forall>n.
1592       \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
1593    by blast
1594  from exec
1595  have "\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> =n\<Rightarrow> t"
1596    by (cases rule: execn_dynCall_Normal_elim)
1597  then show "t \<in> Normal ` Q \<union> Abrupt ` A"
1598  proof (cases rule: execn_call_Normal_elim)
1599    fix bdy m t'
1600    assume bdy: "\<Gamma> (p s) = Some bdy"
1601    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'"
1602    assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc m\<Rightarrow> t"
1603    assume n: "n = Suc m"
1604    from exec_body n bdy
1605    have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n\<Rightarrow> Normal t'"
1606      by (auto simp add: intro: execn.intros)
1607    from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt' this] P
1608    have "t' \<in> Modif (init s)"
1609      by auto
1610    with ret_modif have "Normal (return' s t') = Normal (return s t')"
1611      by simp
1612    with exec_body exec_c bdy n
1613    have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> =n\<Rightarrow> t"
1614      by (auto intro: execn_call)
1615    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1616      by (rule execn_dynCall)
1617    from cnvalidD [OF valid_call ctxt this] P t_notin_F
1618    show ?thesis
1619      by simp
1620  next
1621    fix bdy m t'
1622    assume bdy: "\<Gamma> (p s) = Some bdy"
1623    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'"
1624    assume n: "n = Suc m"
1625    assume t: "t = Abrupt (return s t')"
1626    also from exec_body n bdy
1627    have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t'"
1628      by (auto simp add: intro: execn.intros)
1629    from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt' this] P
1630    have "t' \<in> ModifAbr (init s)"
1631      by auto
1632    with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
1633      by simp
1634    finally have "t = Abrupt (return' s t')" .
1635    with exec_body bdy n
1636    have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> =n\<Rightarrow> t"
1637      by (auto intro: execn_callAbrupt)
1638    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1639      by (rule execn_dynCall)
1640    from cnvalidD [OF valid_call ctxt this] P t_notin_F
1641    show ?thesis
1642      by simp
1643  next
1644    fix bdy m f
1645    assume bdy: "\<Gamma> (p s) = Some bdy"
1646    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f" "n = Suc m"
1647      "t = Fault f"
1648    with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t"
1649      by (auto intro: execn_callFault)
1650    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1651      by (rule execn_dynCall)
1652    from valid_call ctxt this P t_notin_F
1653    show ?thesis
1654      by (rule cnvalidD)
1655  next
1656    fix bdy m
1657    assume bdy: "\<Gamma> (p s) = Some bdy"
1658    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m"
1659      "t = Stuck"
1660    with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t"
1661      by (auto intro: execn_callStuck)
1662    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1663      by (rule execn_dynCall)
1664    from valid_call ctxt this P t_notin_F
1665    show ?thesis
1666      by (rule cnvalidD)
1667  next
1668    fix m
1669    assume "\<Gamma> (p s) = None"
1670    and  "n = Suc m" "t = Stuck"
1671    hence "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t"
1672      by (auto intro: execn_callUndefined)
1673    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1674      by (rule execn_dynCall)
1675    from valid_call ctxt this P t_notin_F
1676    show ?thesis
1677      by (rule cnvalidD)
1678  qed
1679qed
1680
1681lemma dynProcModifyReturn:
1682assumes dyn_call: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
1683assumes ret_modif:
1684    "\<forall>s t. t \<in> Modif (init s)
1685           \<longrightarrow> return' s t = return s t"
1686assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
1687                             \<longrightarrow> return' s t = return s t"
1688assumes modif:
1689    "\<forall>s \<in> P. \<forall>\<sigma>.
1690       \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
1691shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
1692apply (rule hoare_complete')
1693apply (rule allI)
1694apply (rule dynProcModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr,
1695          OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr])
1696apply (intro ballI allI)
1697apply (rule hoare_cnvalid [OF modif [rule_format]])
1698apply assumption
1699done
1700
1701lemma dynProcModifyReturnSameFaults_sound:
1702assumes valid_call: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
1703assumes valid_modif:
1704    "\<forall>s \<in> P. \<forall>\<sigma>. \<forall>n.
1705       \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
1706assumes ret_modif:
1707    "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t"
1708assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t"
1709shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
1710proof (rule cnvalidI)
1711  fix s t
1712  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
1713  assume exec: "\<Gamma>\<turnstile>\<langle>dynCall init p return c,Normal s\<rangle> =n\<Rightarrow> t"
1714  assume t_notin_F: "t \<notin> Fault ` F"
1715  assume P: "s \<in> P"
1716  with valid_modif
1717  have valid_modif': "\<forall>\<sigma>. \<forall>n.
1718    \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
1719    by blast
1720  from exec
1721  have "\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> =n\<Rightarrow> t"
1722    by (cases rule: execn_dynCall_Normal_elim)
1723  then show "t \<in> Normal ` Q \<union> Abrupt ` A"
1724  proof (cases rule: execn_call_Normal_elim)
1725    fix bdy m t'
1726    assume bdy: "\<Gamma> (p s) = Some bdy"
1727    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'"
1728    assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc m\<Rightarrow> t"
1729    assume n: "n = Suc m"
1730    from exec_body n bdy
1731    have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n \<Rightarrow> Normal t'"
1732      by (auto simp add: intro: execn.Call)
1733    from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt this] P
1734    have "t' \<in> Modif (init s)"
1735      by auto
1736    with ret_modif have "Normal (return' s t') = Normal (return s t')"
1737      by simp
1738    with exec_body exec_c bdy n
1739    have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> =n\<Rightarrow> t"
1740      by (auto intro: execn_call)
1741    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1742      by (rule execn_dynCall)
1743    from cnvalidD [OF valid_call ctxt this] P t_notin_F
1744    show ?thesis
1745      by simp
1746  next
1747    fix bdy m t'
1748    assume bdy: "\<Gamma> (p s) = Some bdy"
1749    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'"
1750    assume n: "n = Suc m"
1751    assume t: "t = Abrupt (return s t')"
1752    also from exec_body n bdy
1753    have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n \<Rightarrow> Abrupt t'"
1754      by (auto simp add: intro: execn.intros)
1755    from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt this] P
1756    have "t' \<in> ModifAbr (init s)"
1757      by auto
1758    with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
1759      by simp
1760    finally have "t = Abrupt (return' s t')" .
1761    with exec_body bdy n
1762    have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> =n\<Rightarrow> t"
1763      by (auto intro: execn_callAbrupt)
1764    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1765      by (rule execn_dynCall)
1766    from cnvalidD [OF valid_call ctxt this] P t_notin_F
1767    show ?thesis
1768      by simp
1769  next
1770    fix bdy m f
1771    assume bdy: "\<Gamma> (p s) = Some bdy"
1772    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f" "n = Suc m"  and
1773      t: "t = Fault f"
1774    with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t"
1775      by (auto intro: execn_callFault)
1776    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1777      by (rule execn_dynCall)
1778    from cnvalidD [OF valid_call ctxt this P] t t_notin_F
1779    show ?thesis
1780      by simp
1781  next
1782    fix bdy m
1783    assume bdy: "\<Gamma> (p s) = Some bdy"
1784    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m"
1785      "t = Stuck"
1786    with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t"
1787      by (auto intro: execn_callStuck)
1788    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1789      by (rule execn_dynCall)
1790    from valid_call ctxt this P t_notin_F
1791    show ?thesis
1792      by (rule cnvalidD)
1793  next
1794    fix m
1795    assume "\<Gamma> (p s) = None"
1796    and  "n = Suc m" "t = Stuck"
1797    hence "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t"
1798      by (auto intro: execn_callUndefined)
1799    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
1800      by (rule execn_dynCall)
1801    from valid_call ctxt this P t_notin_F
1802    show ?thesis
1803      by (rule cnvalidD)
1804  qed
1805qed
1806
1807lemma dynProcModifyReturnSameFaults:
1808assumes dyn_call: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
1809assumes ret_modif:
1810    "\<forall>s t. t \<in> Modif (init s)
1811           \<longrightarrow> return' s t = return s t"
1812assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
1813                             \<longrightarrow> return' s t = return s t"
1814assumes modif:
1815    "\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
1816shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
1817apply (rule hoare_complete')
1818apply (rule allI)
1819apply (rule dynProcModifyReturnSameFaults_sound
1820        [where Modif=Modif and ModifAbr=ModifAbr,
1821           OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr])
1822apply (intro ballI allI)
1823apply (rule hoare_cnvalid [OF modif [rule_format]])
1824apply assumption
1825done
1826
1827
1828subsubsection \<open>Conjunction of Postcondition\<close>
1829
1830lemma PostConjI_sound:
1831assumes valid_Q: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
1832assumes valid_R: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c R,B"
1833shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> B)"
1834proof (rule cnvalidI)
1835  fix s t
1836  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
1837  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
1838  assume P: "s \<in> P"
1839  assume t_notin_F: "t \<notin> Fault ` F"
1840  from valid_Q [rule_format] ctxt exec P t_notin_F have "t \<in> Normal ` Q \<union> Abrupt ` A"
1841    by (rule cnvalidD)
1842  moreover
1843  from valid_R [rule_format] ctxt exec P t_notin_F have "t \<in> Normal ` R \<union> Abrupt ` B"
1844    by (rule cnvalidD)
1845  ultimately show "t \<in> Normal ` (Q \<inter> R) \<union> Abrupt ` (A \<inter> B)"
1846    by blast
1847qed
1848
1849lemma PostConjI:
1850  assumes deriv_Q: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
1851  assumes deriv_R: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c R,B"
1852  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> B)"
1853apply (rule hoare_complete')
1854apply (rule allI)
1855apply (rule PostConjI_sound)
1856using deriv_Q
1857apply (blast intro: hoare_cnvalid)
1858using deriv_R
1859apply (blast intro: hoare_cnvalid)
1860done
1861
1862lemma Merge_PostConj_sound:
1863  assumes validF: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
1864  assumes validG: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/G\<^esub> P' c R,X"
1865  assumes F_G: "F \<subseteq> G"
1866  assumes P_P': "P \<subseteq> P'"
1867  shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> X)"
1868proof (rule cnvalidI)
1869  fix s t
1870  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
1871  with F_G have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/G\<^esub> P (Call p) Q,A"
1872    by (auto intro: nvalid_augment_Faults)
1873  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
1874  assume P: "s \<in> P"
1875  with P_P' have P': "s \<in> P'"
1876    by auto
1877  assume t_noFault: "t \<notin> Fault ` F"
1878  show "t \<in> Normal ` (Q \<inter> R) \<union> Abrupt ` (A \<inter> X)"
1879  proof -
1880    from cnvalidD [OF validF [rule_format] ctxt exec P t_noFault]
1881    have *: "t \<in> Normal ` Q \<union> Abrupt ` A".
1882    then have "t \<notin> Fault ` G"
1883      by auto
1884    from cnvalidD [OF validG [rule_format] ctxt' exec P' this]
1885    have "t \<in> Normal ` R \<union> Abrupt ` X" .
1886    with * show ?thesis by auto
1887  qed
1888qed
1889
1890lemma Merge_PostConj:
1891  assumes validF: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
1892  assumes validG: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/G\<^esub> P' c R,X"
1893  assumes F_G: "F \<subseteq> G"
1894  assumes P_P': "P \<subseteq> P'"
1895  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> X)"
1896apply (rule hoare_complete')
1897apply (rule allI)
1898apply (rule Merge_PostConj_sound [OF _ _ F_G P_P'])
1899using validF apply (blast intro:hoare_cnvalid)
1900using validG apply (blast intro:hoare_cnvalid)
1901done
1902
1903subsubsection \<open>Weaken Context\<close>
1904
1905
1906lemma WeakenContext_sound:
1907  assumes valid_c: "\<forall>n. \<Gamma>,\<Theta>'\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
1908  assumes valid_ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>'. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
1909  shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
1910proof (rule cnvalidI)
1911  fix s t
1912  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
1913  with valid_ctxt
1914  have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>'. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
1915    by (simp add: cnvalid_def)
1916  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
1917  assume P: "s \<in> P"
1918  assume t_notin_F: "t \<notin> Fault ` F"
1919  from valid_c [rule_format] ctxt' exec P t_notin_F
1920  show "t \<in> Normal ` Q \<union> Abrupt ` A"
1921    by (rule cnvalidD)
1922qed
1923
1924lemma WeakenContext:
1925  assumes deriv_c: "\<Gamma>,\<Theta>'\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
1926  assumes deriv_ctxt: "\<forall>(P,p,Q,A)\<in>\<Theta>'. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A"
1927  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
1928apply (rule hoare_complete')
1929apply (rule allI)
1930apply (rule WeakenContext_sound)
1931using deriv_c
1932apply (blast intro: hoare_cnvalid)
1933using deriv_ctxt
1934apply (blast intro: hoare_cnvalid)
1935done
1936
1937subsubsection \<open>Guards and Guarantees\<close>
1938
1939lemma SplitGuards_sound:
1940assumes valid_c1: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c\<^sub>1 Q,A"
1941assumes valid_c2: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c\<^sub>2 UNIV,UNIV"
1942assumes c: "(c\<^sub>1 \<inter>\<^sub>g c\<^sub>2) = Some c"
1943shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
1944proof (rule cnvalidI)
1945  fix s t
1946  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
1947  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
1948  assume P: "s \<in> P"
1949  assume t_notin_F: "t \<notin> Fault ` F"
1950  show "t \<in> Normal ` Q \<union> Abrupt ` A"
1951  proof (cases t)
1952    case Normal
1953    with inter_guards_execn_noFault [OF c exec]
1954    have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> t" by simp
1955    from valid_c1 [rule_format] ctxt this P t_notin_F
1956    show ?thesis
1957      by (rule cnvalidD)
1958  next
1959    case Abrupt
1960    with inter_guards_execn_noFault [OF c exec]
1961    have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> t" by simp
1962    from valid_c1 [rule_format] ctxt this P t_notin_F
1963    show ?thesis
1964      by (rule cnvalidD)
1965  next
1966    case (Fault f)
1967    with exec inter_guards_execn_Fault [OF c]
1968    have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> Fault f \<or> \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> =n\<Rightarrow> Fault f"
1969      by auto
1970    then show ?thesis
1971    proof (cases rule: disjE [consumes 1])
1972      assume "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> Fault f"
1973      from Fault cnvalidD [OF valid_c1 [rule_format] ctxt this P] t_notin_F
1974      show ?thesis
1975        by blast
1976    next
1977      assume "\<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> =n\<Rightarrow> Fault f"
1978      from Fault cnvalidD [OF valid_c2 [rule_format] ctxt this P] t_notin_F
1979      show ?thesis
1980        by blast
1981    qed
1982  next
1983    case Stuck
1984    with inter_guards_execn_noFault [OF c exec]
1985    have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> t" by simp
1986    from valid_c1 [rule_format] ctxt this P t_notin_F
1987    show ?thesis
1988      by (rule cnvalidD)
1989  qed
1990qed
1991
1992lemma SplitGuards:
1993  assumes c: "(c\<^sub>1 \<inter>\<^sub>g c\<^sub>2) = Some c"
1994  assumes deriv_c1: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>1 Q,A"
1995  assumes deriv_c2: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>2 UNIV,UNIV"
1996  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
1997apply (rule hoare_complete')
1998apply (rule allI)
1999apply (rule SplitGuards_sound [OF _ _ c])
2000using deriv_c1
2001apply (blast intro: hoare_cnvalid)
2002using deriv_c2
2003apply (blast intro: hoare_cnvalid)
2004done
2005
2006lemma CombineStrip_sound:
2007  assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
2008  assumes valid_strip: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P (strip_guards (-F) c) UNIV,UNIV"
2009  shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P c Q,A"
2010proof (rule cnvalidI)
2011  fix s t
2012  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/{}\<^esub> P (Call p) Q,A"
2013  hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
2014    by (auto intro: nvalid_augment_Faults)
2015  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
2016  assume P: "s \<in> P"
2017  assume t_noFault: "t \<notin> Fault ` {}"
2018  show "t \<in> Normal ` Q \<union> Abrupt ` A"
2019  proof (cases t)
2020    case (Normal t')
2021    from cnvalidD [OF valid [rule_format] ctxt' exec P] Normal
2022    show ?thesis
2023      by auto
2024  next
2025    case (Abrupt t')
2026    from cnvalidD [OF valid [rule_format] ctxt' exec P] Abrupt
2027    show ?thesis
2028      by auto
2029  next
2030    case (Fault f)
2031    show ?thesis
2032    proof (cases "f \<in> F")
2033      case True
2034      hence "f \<notin> -F" by simp
2035      with exec Fault
2036      have "\<Gamma>\<turnstile>\<langle>strip_guards (-F) c,Normal s\<rangle> =n\<Rightarrow> Fault f"
2037        by (auto intro: execn_to_execn_strip_guards_Fault)
2038      from cnvalidD [OF valid_strip [rule_format] ctxt this P] Fault
2039      have False
2040        by auto
2041      thus ?thesis ..
2042    next
2043      case False
2044      with cnvalidD [OF valid [rule_format] ctxt' exec P] Fault
2045      show ?thesis
2046        by auto
2047    qed
2048  next
2049    case Stuck
2050    from cnvalidD [OF valid [rule_format] ctxt' exec P] Stuck
2051    show ?thesis
2052      by auto
2053  qed
2054qed
2055
2056lemma CombineStrip:
2057  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
2058  assumes deriv_strip: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P (strip_guards (-F) c) UNIV,UNIV"
2059  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A"
2060apply (rule hoare_complete')
2061apply (rule allI)
2062apply (rule CombineStrip_sound)
2063apply  (iprover intro: hoare_cnvalid [OF deriv])
2064apply (iprover intro: hoare_cnvalid [OF deriv_strip])
2065done
2066
2067lemma GuardsFlip_sound:
2068  assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
2069  assumes validFlip: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/-F\<^esub> P c UNIV,UNIV"
2070  shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P c Q,A"
2071proof (rule cnvalidI)
2072  fix s t
2073  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/{}\<^esub> P (Call p) Q,A"
2074  hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
2075    by (auto intro: nvalid_augment_Faults)
2076  from ctxt have ctxtFlip: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/-F\<^esub> P (Call p) Q,A"
2077    by (auto intro: nvalid_augment_Faults)
2078  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
2079  assume P: "s \<in> P"
2080  assume t_noFault: "t \<notin> Fault ` {}"
2081  show "t \<in> Normal ` Q \<union> Abrupt ` A"
2082  proof (cases t)
2083    case (Normal t')
2084    from cnvalidD [OF valid [rule_format] ctxt' exec P] Normal
2085    show ?thesis
2086      by auto
2087  next
2088    case (Abrupt t')
2089    from cnvalidD [OF valid [rule_format] ctxt' exec P] Abrupt
2090    show ?thesis
2091      by auto
2092  next
2093    case (Fault f)
2094    show ?thesis
2095    proof (cases "f \<in> F")
2096      case True
2097      hence "f \<notin> -F" by simp
2098      with cnvalidD [OF validFlip [rule_format] ctxtFlip exec P] Fault
2099      have False
2100        by auto
2101      thus ?thesis ..
2102    next
2103      case False
2104      with cnvalidD [OF valid [rule_format] ctxt' exec P] Fault
2105      show ?thesis
2106        by auto
2107    qed
2108  next
2109    case Stuck
2110    from cnvalidD [OF valid [rule_format] ctxt' exec P] Stuck
2111    show ?thesis
2112      by auto
2113  qed
2114qed
2115
2116lemma GuardsFlip:
2117  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
2118  assumes derivFlip: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/-F\<^esub> P c UNIV,UNIV"
2119  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A"
2120apply (rule hoare_complete')
2121apply (rule allI)
2122apply (rule GuardsFlip_sound)
2123apply  (iprover intro: hoare_cnvalid [OF deriv])
2124apply (iprover intro: hoare_cnvalid [OF derivFlip])
2125done
2126
2127lemma MarkGuardsI_sound:
2128  assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P c Q,A"
2129  shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P mark_guards f c Q,A"
2130proof (rule cnvalidI)
2131  fix s t
2132  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/{}\<^esub> P (Call p) Q,A"
2133  assume exec: "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s\<rangle> =n\<Rightarrow> t"
2134  from execn_mark_guards_to_execn [OF exec] obtain t' where
2135    exec_c: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t'" and
2136    t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t"
2137    by blast
2138  assume P: "s \<in> P"
2139  assume t_noFault: "t \<notin> Fault ` {}"
2140  show "t \<in> Normal ` Q \<union> Abrupt ` A"
2141  proof -
2142    from cnvalidD [OF valid [rule_format] ctxt exec_c P]
2143    have "t' \<in> Normal ` Q \<union> Abrupt ` A"
2144      by blast
2145    with t'_noFault
2146    show ?thesis
2147      by auto
2148  qed
2149qed
2150
2151lemma MarkGuardsI:
2152  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A"
2153  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P mark_guards f c Q,A"
2154apply (rule hoare_complete')
2155apply (rule allI)
2156apply (rule MarkGuardsI_sound)
2157apply (iprover intro: hoare_cnvalid [OF deriv])
2158done
2159
2160lemma MarkGuardsD_sound:
2161  assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P mark_guards f c Q,A"
2162  shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P c Q,A"
2163proof (rule cnvalidI)
2164  fix s t
2165  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/{}\<^esub> P (Call p) Q,A"
2166  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
2167  assume P: "s \<in> P"
2168  assume t_noFault: "t \<notin> Fault ` {}"
2169  show "t \<in> Normal ` Q \<union> Abrupt ` A"
2170  proof (cases "isFault t")
2171    case True
2172    with execn_to_execn_mark_guards_Fault [OF exec ]
2173    obtain f' where "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s\<rangle> =n\<Rightarrow> Fault f'"
2174      by (fastforce elim: isFaultE)
2175    from cnvalidD [OF valid [rule_format] ctxt this P]
2176    have False
2177      by auto
2178    thus ?thesis ..
2179  next
2180    case False
2181    from execn_to_execn_mark_guards [OF exec False]
2182    obtain f' where "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s\<rangle> =n\<Rightarrow> t"
2183      by auto
2184    from cnvalidD [OF valid [rule_format] ctxt this P]
2185    show ?thesis
2186      by auto
2187  qed
2188qed
2189
2190lemma MarkGuardsD:
2191  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P mark_guards f c Q,A"
2192  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A"
2193apply (rule hoare_complete')
2194apply (rule allI)
2195apply (rule MarkGuardsD_sound)
2196apply (iprover intro: hoare_cnvalid [OF deriv])
2197done
2198
2199lemma MergeGuardsI_sound:
2200  assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
2201  shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P merge_guards c Q,A"
2202proof (rule cnvalidI)
2203  fix s t
2204  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
2205  assume exec_merge: "\<Gamma>\<turnstile>\<langle>merge_guards c,Normal s\<rangle> =n\<Rightarrow> t"
2206  from execn_merge_guards_to_execn [OF exec_merge]
2207  have exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" .
2208  assume P: "s \<in> P"
2209  assume t_notin_F: "t \<notin> Fault ` F"
2210  from cnvalidD [OF valid [rule_format] ctxt exec P t_notin_F]
2211  show "t \<in> Normal ` Q \<union> Abrupt ` A".
2212qed
2213
2214lemma MergeGuardsI:
2215  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
2216  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P merge_guards c Q,A"
2217apply (rule hoare_complete')
2218apply (rule allI)
2219apply (rule MergeGuardsI_sound)
2220apply (iprover intro: hoare_cnvalid [OF deriv])
2221done
2222
2223lemma MergeGuardsD_sound:
2224  assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P merge_guards c Q,A"
2225  shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
2226proof (rule cnvalidI)
2227  fix s t
2228  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
2229  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
2230  from execn_to_execn_merge_guards [OF exec]
2231  have exec_merge: "\<Gamma>\<turnstile>\<langle>merge_guards c,Normal s\<rangle> =n\<Rightarrow> t".
2232  assume P: "s \<in> P"
2233  assume t_notin_F: "t \<notin> Fault ` F"
2234  from cnvalidD [OF valid [rule_format] ctxt exec_merge P t_notin_F]
2235  show "t \<in> Normal ` Q \<union> Abrupt ` A".
2236qed
2237
2238lemma MergeGuardsD:
2239  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P merge_guards c Q,A"
2240  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
2241apply (rule hoare_complete')
2242apply (rule allI)
2243apply (rule MergeGuardsD_sound)
2244apply (iprover intro: hoare_cnvalid [OF deriv])
2245done
2246
2247
2248lemma SubsetGuards_sound:
2249  assumes c_c': "c \<subseteq>\<^sub>g c'"
2250  assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P c' Q,A"
2251  shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P c Q,A"
2252proof (rule cnvalidI)
2253  fix s t
2254  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/{}\<^esub> P (Call p) Q,A"
2255  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
2256  from execn_to_execn_subseteq_guards [OF c_c' exec] obtain t' where
2257    exec_c': "\<Gamma>\<turnstile>\<langle>c',Normal s\<rangle> =n\<Rightarrow> t'" and
2258    t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t"
2259    by blast
2260  assume P: "s \<in> P"
2261  assume t_noFault: "t \<notin> Fault ` {}"
2262  from cnvalidD [OF valid [rule_format] ctxt exec_c' P] t'_noFault t_noFault
2263  show "t \<in> Normal ` Q \<union> Abrupt ` A"
2264    by auto
2265qed
2266
2267lemma SubsetGuards:
2268  assumes c_c': "c \<subseteq>\<^sub>g c'"
2269  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c' Q,A"
2270  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A"
2271apply (rule hoare_complete')
2272apply (rule allI)
2273apply (rule SubsetGuards_sound [OF c_c'])
2274apply (iprover intro: hoare_cnvalid [OF deriv])
2275done
2276
2277lemma NormalizeD_sound:
2278  assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P (normalize c) Q,A"
2279  shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
2280proof (rule cnvalidI)
2281  fix s t
2282  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
2283  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
2284  hence exec_norm: "\<Gamma>\<turnstile>\<langle>normalize c,Normal s\<rangle> =n\<Rightarrow> t"
2285    by (rule execn_to_execn_normalize)
2286  assume P: "s \<in> P"
2287  assume noFault: "t \<notin> Fault ` F"
2288  from cnvalidD [OF valid [rule_format] ctxt exec_norm P noFault]
2289  show "t \<in> Normal ` Q \<union> Abrupt ` A".
2290qed
2291
2292lemma NormalizeD:
2293  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (normalize c) Q,A"
2294  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
2295apply (rule hoare_complete')
2296apply (rule allI)
2297apply (rule NormalizeD_sound)
2298apply (iprover intro: hoare_cnvalid [OF deriv])
2299done
2300
2301lemma NormalizeI_sound:
2302  assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
2303  shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P (normalize c) Q,A"
2304proof (rule cnvalidI)
2305  fix s t
2306  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
2307  assume "\<Gamma>\<turnstile>\<langle>normalize c,Normal s\<rangle> =n\<Rightarrow> t"
2308  hence exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
2309    by (rule execn_normalize_to_execn)
2310  assume P: "s \<in> P"
2311  assume noFault: "t \<notin> Fault ` F"
2312  from cnvalidD [OF valid [rule_format] ctxt exec P noFault]
2313  show "t \<in> Normal ` Q \<union> Abrupt ` A".
2314qed
2315
2316lemma NormalizeI:
2317  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
2318  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (normalize c) Q,A"
2319apply (rule hoare_complete')
2320apply (rule allI)
2321apply (rule NormalizeI_sound)
2322apply (iprover intro: hoare_cnvalid [OF deriv])
2323done
2324
2325
2326subsubsection \<open>Restricting the Procedure Environment\<close>
2327
2328lemma nvalid_restrict_to_nvalid:
2329assumes valid_c: "\<Gamma>|\<^bsub>M\<^esub>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
2330shows "\<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A"
2331proof (rule nvalidI)
2332  fix s t
2333  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
2334  assume P: "s \<in> P"
2335  assume t_notin_F: "t \<notin> Fault ` F"
2336  show "t \<in> Normal ` Q \<union> Abrupt ` A"
2337  proof -
2338    from execn_to_execn_restrict [OF exec]
2339    obtain t' where
2340      exec_res: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t'" and
2341      t_Fault: "\<forall>f. t = Fault f \<longrightarrow> t' \<in> {Fault f, Stuck}" and
2342      t'_notStuck: "t'\<noteq>Stuck \<longrightarrow> t'=t"
2343      by blast
2344    from t_Fault t_notin_F t'_notStuck have "t' \<notin> Fault ` F"
2345      by (cases t') auto
2346    with valid_c exec_res P
2347    have "t' \<in> Normal ` Q \<union> Abrupt ` A"
2348      by (auto simp add: nvalid_def)
2349    with t'_notStuck
2350    show ?thesis
2351      by auto
2352  qed
2353qed
2354
2355lemma valid_restrict_to_valid:
2356assumes valid_c: "\<Gamma>|\<^bsub>M\<^esub>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A"
2357shows "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A"
2358proof (rule validI)
2359  fix s t
2360  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
2361  assume P: "s \<in> P"
2362  assume t_notin_F: "t \<notin> Fault ` F"
2363  show "t \<in> Normal ` Q \<union> Abrupt ` A"
2364  proof -
2365    from exec_to_exec_restrict [OF exec]
2366    obtain t' where
2367      exec_res: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t'" and
2368      t_Fault: "\<forall>f. t = Fault f \<longrightarrow> t' \<in> {Fault f, Stuck}" and
2369      t'_notStuck: "t'\<noteq>Stuck \<longrightarrow> t'=t"
2370      by blast
2371    from t_Fault t_notin_F t'_notStuck have "t' \<notin> Fault ` F"
2372      by (cases t') auto
2373    with valid_c exec_res P
2374    have "t' \<in> Normal ` Q \<union> Abrupt ` A"
2375      by (auto simp add: valid_def)
2376    with t'_notStuck
2377    show ?thesis
2378      by auto
2379  qed
2380qed
2381
2382lemma augment_procs:
2383assumes deriv_c: "\<Gamma>|\<^bsub>M\<^esub>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
2384shows "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
2385  apply (rule hoare_complete)
2386  apply (rule valid_restrict_to_valid)
2387  apply (insert hoare_sound [OF deriv_c])
2388  by (simp add: cvalid_def)
2389
2390lemma augment_Faults:
2391assumes deriv_c: "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
2392assumes F: "F \<subseteq> F'"
2393shows "\<Gamma>,{}\<turnstile>\<^bsub>/F'\<^esub> P c Q,A"
2394  apply (rule hoare_complete)
2395  apply (rule valid_augment_Faults [OF _ F])
2396  apply (insert hoare_sound [OF deriv_c])
2397  by (simp add: cvalid_def)
2398
2399end
2400