1(*
2    Author:      Norbert Schirmer
3    Maintainer:  Norbert Schirmer, norbert.schirmer at web de
4    License:     LGPL
5*)
6
7(*  Title:      HoarePartial.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 Total Correctness Hoare Logic\<close>
30
31theory HoareTotalProps imports SmallStep HoareTotalDef HoarePartialProps begin
32
33subsection \<open>Soundness\<close>
34
35lemma hoaret_sound:
36 assumes hoare: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
37 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
38using hoare
39proof (induct)
40  case (Skip \<Theta> F P A)
41  show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Skip P,A"
42  proof (rule cvalidtI)
43    fix s t
44    assume "\<Gamma>\<turnstile>\<langle>Skip,Normal s\<rangle> \<Rightarrow> t" "s \<in> P"
45    thus "t \<in> Normal ` P \<union> Abrupt ` A"
46      by cases auto
47  next
48    fix s show "\<Gamma>\<turnstile>Skip \<down> Normal s"
49      by (rule terminates.intros)
50  qed
51next
52  case (Basic \<Theta> F f P A)
53  show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. f s \<in> P} (Basic f) P,A"
54  proof (rule cvalidtI)
55    fix s t
56    assume "\<Gamma>\<turnstile>\<langle>Basic f,Normal s\<rangle> \<Rightarrow> t" "s \<in> {s. f s \<in> P}"
57    thus "t \<in> Normal ` P \<union> Abrupt ` A"
58      by cases auto
59  next
60    fix s show "\<Gamma>\<turnstile>Basic f \<down> Normal s"
61      by (rule terminates.intros)
62  qed
63next
64  case (Spec \<Theta> F r Q A)
65  show "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^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"
66  proof (rule cvalidtI)
67    fix s t
68    assume "\<Gamma>\<turnstile>\<langle>Spec r ,Normal s\<rangle> \<Rightarrow> t"
69           "s \<in> {s. (\<forall>t. (s, t) \<in> r \<longrightarrow> t \<in> Q) \<and> (\<exists>t. (s, t) \<in> r)}"
70    thus "t \<in> Normal ` Q \<union> Abrupt ` A"
71      by cases auto
72  next
73    fix s show "\<Gamma>\<turnstile>Spec r \<down> Normal s"
74      by (rule terminates.intros)
75  qed
76next
77  case (Seq \<Theta> F P c1 R A c2 Q)
78  have valid_c1: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c1 R,A" by fact
79  have valid_c2: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> R c2 Q,A" by fact
80  show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Seq c1 c2 Q,A"
81  proof (rule cvalidtI)
82    fix s t
83    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
84    assume exec: "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow> t"
85    assume P: "s \<in> P"
86    assume t_notin_F: "t \<notin> Fault ` F"
87    from exec P obtain r where
88      exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow> r" and exec_c2:  "\<Gamma>\<turnstile>\<langle>c2,r\<rangle> \<Rightarrow> t"
89      by cases auto
90    with t_notin_F have "r \<notin> Fault ` F"
91      by (auto dest: Fault_end)
92    from valid_c1 ctxt exec_c1 P this
93    have r: "r \<in> Normal ` R \<union> Abrupt ` A"
94      by (rule cvalidt_postD)
95    show "t\<in>Normal ` Q \<union> Abrupt ` A"
96    proof (cases r)
97      case (Normal r')
98      with exec_c2 r
99      show "t\<in>Normal ` Q \<union> Abrupt ` A"
100        apply -
101        apply (rule cvalidt_postD [OF valid_c2 ctxt _ _ t_notin_F])
102        apply auto
103        done
104    next
105      case (Abrupt r')
106      with exec_c2 have "t=Abrupt r'"
107        by (auto elim: exec_elim_cases)
108      with Abrupt r show ?thesis
109        by auto
110    next
111      case Fault with r show ?thesis by blast
112    next
113      case Stuck with r show ?thesis by blast
114    qed
115  next
116    fix s
117    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
118    assume P: "s\<in>P"
119    show "\<Gamma>\<turnstile>Seq c1 c2 \<down> Normal s"
120    proof -
121      from valid_c1 ctxt P
122      have "\<Gamma>\<turnstile>c1\<down> Normal s"
123        by (rule cvalidt_termD)
124      moreover
125      {
126        fix r assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow> r"
127        have "\<Gamma>\<turnstile>c2 \<down> r"
128        proof (cases r)
129          case (Normal r')
130          with cvalidt_postD [OF valid_c1 ctxt exec_c1 P]
131          have r: "r\<in>Normal ` R"
132            by auto
133          with cvalidt_termD [OF valid_c2 ctxt] exec_c1
134          show "\<Gamma>\<turnstile>c2 \<down> r"
135            by auto
136        qed auto
137      }
138      ultimately show ?thesis
139        by (iprover intro: terminates.intros)
140    qed
141  qed
142next
143  case (Cond \<Theta> F P b c1 Q A c2)
144  have valid_c1: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> (P \<inter> b) c1 Q,A" by fact
145  have valid_c2: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> (P \<inter> - b) c2 Q,A" by fact
146  show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Cond b c1 c2 Q,A"
147  proof (rule cvalidtI)
148    fix s t
149    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
150    assume exec: "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow> t"
151    assume P: "s \<in> P"
152    assume t_notin_F: "t \<notin> Fault ` F"
153    show "t \<in> Normal ` Q \<union> Abrupt ` A"
154    proof (cases "s\<in>b")
155      case True
156      with exec have "\<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow> t"
157        by cases auto
158      with P True
159      show ?thesis
160        by - (rule cvalidt_postD [OF valid_c1 ctxt _ _ t_notin_F],auto)
161    next
162      case False
163      with exec P have "\<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow> t"
164        by cases auto
165      with P False
166      show ?thesis
167        by - (rule cvalidt_postD [OF valid_c2 ctxt _ _ t_notin_F],auto)
168    qed
169  next
170    fix s
171    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
172    assume P: "s \<in> P"
173    thus "\<Gamma>\<turnstile>Cond b c1 c2 \<down> Normal s"
174      using cvalidt_termD [OF valid_c1 ctxt] cvalidt_termD [OF valid_c2 ctxt]
175      by (cases "s \<in> b") (auto intro: terminates.intros)
176  qed
177next
178  case (While r \<Theta> F P b c A)
179  assume wf: "wf r"
180  have valid_c: "\<forall>\<sigma>. \<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> P \<inter> b) c ({t. (t, \<sigma>) \<in> r} \<inter> P),A"
181    using While.hyps by iprover
182  show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (While b c) (P \<inter> - b),A"
183  proof (rule cvalidtI)
184    fix s t
185    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
186    assume wprems: "\<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow> t" "s \<in> P" "t \<notin> Fault ` F"
187    from wf
188    have "\<And>t. \<lbrakk>\<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow> t; s \<in> P; t \<notin> Fault ` F\<rbrakk>
189                 \<Longrightarrow> t \<in> Normal ` (P \<inter> - b) \<union> Abrupt ` A"
190    proof (induct)
191      fix s t
192      assume hyp:
193        "\<And>s' t. \<lbrakk>(s',s)\<in>r; \<Gamma>\<turnstile>\<langle>While b c,Normal s'\<rangle> \<Rightarrow> t; s' \<in> P; t \<notin> Fault ` F\<rbrakk>
194                 \<Longrightarrow> t \<in> Normal ` (P \<inter> - b) \<union> Abrupt ` A"
195      assume exec: "\<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow> t"
196      assume P: "s \<in> P"
197      assume t_notin_F: "t \<notin> Fault ` F"
198      from exec
199      show "t \<in> Normal ` (P \<inter> - b) \<union> Abrupt ` A"
200      proof (cases)
201        fix s'
202        assume b: "s\<in>b"
203        assume exec_c: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> s'"
204        assume exec_w: "\<Gamma>\<turnstile>\<langle>While b c,s'\<rangle> \<Rightarrow> t"
205        from exec_w t_notin_F have "s' \<notin> Fault ` F"
206          by (auto dest: Fault_end)
207        from exec_c P b valid_c ctxt this
208        have s': "s' \<in> Normal ` ({s'. (s', s) \<in> r} \<inter> P) \<union> Abrupt ` A"
209          by (auto simp add: cvalidt_def validt_def valid_def)
210        show ?thesis
211        proof (cases s')
212          case Normal
213          with exec_w s' t_notin_F
214          show ?thesis
215            by - (rule hyp,auto)
216        next
217          case Abrupt
218          with exec_w have "t=s'"
219            by (auto dest: Abrupt_end)
220          with Abrupt s' show ?thesis
221            by blast
222        next
223          case Fault
224          with exec_w have "t=s'"
225            by (auto dest: Fault_end)
226          with Fault s' show ?thesis
227            by blast
228        next
229          case Stuck
230          with exec_w have "t=s'"
231            by (auto dest: Stuck_end)
232          with Stuck s' show ?thesis
233            by blast
234        qed
235      next
236        assume "s\<notin>b" "t=Normal s" with P show ?thesis by simp
237      qed
238    qed
239    with wprems show "t \<in> Normal ` (P \<inter> - b) \<union> Abrupt ` A" by blast
240  next
241    fix s
242    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
243    assume "s \<in> P"
244    with wf
245    show "\<Gamma>\<turnstile>While b c \<down> Normal s"
246    proof (induct)
247      fix s
248      assume hyp: "\<And>s'. \<lbrakk>(s',s)\<in>r; s' \<in> P\<rbrakk>
249                         \<Longrightarrow> \<Gamma>\<turnstile>While b c \<down> Normal s'"
250      assume P: "s \<in> P"
251      show "\<Gamma>\<turnstile>While b c \<down> Normal s"
252      proof (cases "s \<in> b")
253        case False with P show ?thesis
254          by (blast intro: terminates.intros)
255      next
256        case True
257        with valid_c P ctxt
258        have "\<Gamma>\<turnstile>c \<down> Normal s"
259          by (simp add: cvalidt_def validt_def)
260        moreover
261        {
262          fix s'
263          assume exec_c: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> s'"
264          have "\<Gamma>\<turnstile>While b c \<down> s'"
265          proof (cases s')
266            case (Normal s'')
267            with exec_c P True valid_c ctxt
268            have s': "s' \<in> Normal ` ({s'. (s', s) \<in> r} \<inter> P)"
269              by (fastforce simp add: cvalidt_def validt_def valid_def)
270            then show ?thesis
271              by (blast intro: hyp)
272          qed auto
273        }
274        ultimately
275        show ?thesis
276          by (blast intro: terminates.intros)
277      qed
278    qed
279  qed
280next
281  case (Guard \<Theta> F g P c Q A  f)
282  have valid_c: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> P) c Q,A" by fact
283  show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> P) Guard f g c Q,A"
284  proof (rule cvalidtI)
285    fix s t
286    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
287    assume exec: "\<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> t"
288    assume t_notin_F: "t \<notin> Fault ` F"
289    assume P:"s \<in> (g \<inter> P)"
290    from exec P have "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
291      by cases auto
292    from valid_c ctxt this P t_notin_F
293    show "t \<in> Normal ` Q \<union> Abrupt ` A"
294      by (rule cvalidt_postD)
295  next
296    fix s
297    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
298    assume P:"s \<in> (g \<inter> P)"
299    thus "\<Gamma>\<turnstile>Guard f g c  \<down> Normal s"
300      by (auto intro: terminates.intros cvalidt_termD [OF valid_c ctxt])
301  qed
302next
303  case (Guarantee f F \<Theta> g P c Q A)
304  have valid_c: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> P) c Q,A" by fact
305  have f_F: "f \<in> F" by fact
306  show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Guard f g c Q,A"
307  proof (rule cvalidtI)
308    fix s t
309    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
310    assume exec: "\<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> t"
311    assume t_notin_F: "t \<notin> Fault ` F"
312    assume P:"s \<in> P"
313    from exec f_F t_notin_F have g: "s \<in> g"
314      by cases auto
315    with P have P': "s \<in> g \<inter> P"
316      by blast
317    from exec g have "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
318      by cases auto
319    from valid_c ctxt this P' t_notin_F
320    show "t \<in> Normal ` Q \<union> Abrupt ` A"
321      by (rule cvalidt_postD)
322  next
323    fix s
324    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
325    assume P:"s \<in> P"
326    thus "\<Gamma>\<turnstile>Guard f g c  \<down> Normal s"
327      by (auto intro: terminates.intros cvalidt_termD [OF valid_c ctxt])
328  qed
329next
330  case (CallRec P p Q A Specs r Specs_wf \<Theta>  F)
331  have p: "(P,p,Q,A) \<in> Specs"  by fact
332  have wf: "wf r" by fact
333  have Specs_wf:
334    "Specs_wf = (\<lambda>p \<tau>. (\<lambda>(P,q,Q,A). (P \<inter> {s. ((s, q),\<tau>,p) \<in> r},q,Q,A)) ` Specs)" by fact
335  from CallRec.hyps
336  have valid_body:
337    "\<forall>(P, p, Q, A)\<in>Specs. p \<in> dom \<Gamma> \<and>
338        (\<forall>\<tau>. \<Gamma>,\<Theta> \<union> Specs_wf p \<tau>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> P) the (\<Gamma> p) Q,A)" by auto
339  show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
340  proof -
341    {
342      fix \<tau>p
343      assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
344      from wf
345      have "\<And>\<tau> p P Q A.  \<lbrakk>\<tau>p = (\<tau>,p); (P,p,Q,A) \<in> Specs\<rbrakk> \<Longrightarrow>
346                  \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> P) (the (\<Gamma> (p))) Q,A"
347      proof (induct \<tau>p rule: wf_induct [rule_format, consumes 1, case_names WF])
348        case (WF \<tau>p \<tau> p P Q A)
349        have \<tau>p: "\<tau>p = (\<tau>, p)" by fact
350        have p: "(P, p, Q, A) \<in> Specs" by fact
351        {
352          fix q P' Q' A'
353          assume q: "(P',q,Q',A') \<in> Specs"
354          have "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' \<inter> {s. ((s,q), \<tau>,p) \<in> r}) (Call q) Q',A'"
355          proof (rule validtI)
356            fix s t
357            assume exec_q:
358              "\<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow> t"
359            assume Pre: "s \<in> P' \<inter> {s. ((s,q), \<tau>,p) \<in> r}"
360            assume t_notin_F: "t \<notin> Fault ` F"
361            from Pre q \<tau>p
362            have valid_bdy:
363              "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s} \<inter> P') the (\<Gamma> q) Q',A'"
364              by - (rule WF.hyps, auto)
365            from Pre q
366            have Pre': "s \<in> {s} \<inter> P'"
367              by auto
368            from exec_q show "t \<in> Normal ` Q' \<union> Abrupt ` A'"
369            proof (cases)
370              fix bdy
371              assume bdy: "\<Gamma> q = Some bdy"
372              assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal s\<rangle> \<Rightarrow> t"
373              from valid_bdy [simplified bdy option.sel]  t_notin_F exec_bdy Pre'
374              have "t \<in> Normal ` Q' \<union> Abrupt ` A'"
375                by (auto simp add: validt_def valid_def)
376              with Pre q
377              show ?thesis
378                by auto
379            next
380              assume "\<Gamma> q = None"
381              with q valid_body have False by auto
382              thus ?thesis ..
383            qed
384          next
385            fix s
386            assume Pre: "s \<in> P' \<inter> {s. ((s,q), \<tau>,p) \<in> r}"
387            from Pre q \<tau>p
388            have valid_bdy:
389              "\<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s} \<inter> P') (the (\<Gamma> q)) Q',A'"
390              by - (rule WF.hyps, auto)
391            from Pre q
392            have Pre': "s \<in> {s} \<inter> P'"
393              by auto
394            from valid_bdy ctxt Pre'
395            have "\<Gamma>\<turnstile>the (\<Gamma> q) \<down> Normal s"
396              by (auto simp add: validt_def)
397            with valid_body q
398            show "\<Gamma>\<turnstile>Call q\<down> Normal s"
399              by (fastforce intro: terminates.Call)
400          qed
401        }
402        hence "\<forall>(P, p, Q, A)\<in>Specs_wf p \<tau>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Call p Q,A"
403          by (auto simp add: cvalidt_def Specs_wf)
404        with ctxt have "\<forall>(P, p, Q, A)\<in>\<Theta> \<union> Specs_wf p \<tau>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Call p Q,A"
405          by auto
406        with p valid_body
407        show "\<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> P) (the (\<Gamma> p)) Q,A"
408          by (simp add: cvalidt_def) blast
409      qed
410    }
411    note lem = this
412    have valid_body':
413      "\<And>\<tau>. \<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A \<Longrightarrow>
414      \<forall>(P,p,Q,A)\<in>Specs. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> P) (the (\<Gamma> p)) Q,A"
415      by (auto intro: lem)
416    show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
417    proof (rule cvalidtI)
418      fix s t
419      assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
420      assume exec_call: "\<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow> t"
421      assume P: "s \<in> P"
422      assume t_notin_F: "t \<notin> Fault ` F"
423      from exec_call show "t \<in> Normal ` Q \<union> Abrupt ` A"
424      proof (cases)
425        fix bdy
426        assume bdy: "\<Gamma> p = Some bdy"
427        assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal s\<rangle> \<Rightarrow> t"
428        from exec_body bdy p P t_notin_F
429          valid_body' [of "s", OF ctxt]
430          ctxt
431        have "t \<in> Normal ` Q \<union> Abrupt ` A"
432          apply (simp only: cvalidt_def validt_def valid_def)
433          apply (drule (1) bspec)
434          apply auto
435          done
436        with p P
437        show ?thesis
438          by simp
439      next
440        assume "\<Gamma> p = None"
441        with p valid_body have False by auto
442        thus ?thesis by simp
443      qed
444    next
445      fix s
446      assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
447      assume P: "s \<in> P"
448      show "\<Gamma>\<turnstile>Call p \<down> Normal s"
449      proof -
450        from ctxt P p valid_body' [of "s",OF ctxt]
451        have "\<Gamma>\<turnstile>(the (\<Gamma> p)) \<down> Normal s"
452          by (auto simp add: cvalidt_def validt_def)
453        with valid_body p show ?thesis
454          by (fastforce intro: terminates.Call)
455      qed
456    qed
457  qed
458next
459  case (DynCom P \<Theta> F c Q A)
460  hence valid_c: "\<forall>s\<in>P. \<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (c s) Q,A" by simp
461  show "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P DynCom c Q,A"
462  proof (rule cvalidtI)
463    fix s t
464    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
465    assume exec: "\<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> \<Rightarrow> t"
466    assume P: "s \<in> P"
467    assume t_notin_F: "t \<notin> Fault ` F"
468    from exec show "t \<in> Normal ` Q \<union> Abrupt ` A"
469    proof (cases)
470      assume "\<Gamma>\<turnstile>\<langle>c s,Normal s\<rangle> \<Rightarrow> t"
471      from cvalidt_postD [OF valid_c [rule_format, OF P] ctxt this P t_notin_F]
472      show ?thesis .
473    qed
474  next
475    fix s
476    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
477    assume P: "s \<in> P"
478    show "\<Gamma>\<turnstile>DynCom c \<down> Normal s"
479    proof -
480      from cvalidt_termD [OF valid_c [rule_format, OF P] ctxt P]
481      have "\<Gamma>\<turnstile>c s \<down> Normal s" .
482      thus ?thesis
483        by (rule terminates.intros)
484    qed
485  qed
486next
487  case (Throw \<Theta> F A Q)
488  show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> A Throw Q,A"
489  proof (rule cvalidtI)
490    fix s t
491    assume "\<Gamma>\<turnstile>\<langle>Throw,Normal s\<rangle> \<Rightarrow> t" "s \<in> A"
492    then show "t \<in> Normal ` Q \<union> Abrupt ` A"
493      by cases simp
494  next
495    fix s
496    show "\<Gamma>\<turnstile>Throw \<down> Normal s"
497      by (rule terminates.intros)
498  qed
499next
500  case (Catch \<Theta> F P c\<^sub>1 Q R c\<^sub>2 A)
501  have valid_c1: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c\<^sub>1 Q,R" by fact
502  have valid_c2: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> R c\<^sub>2 Q,A" by fact
503  show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Catch c\<^sub>1 c\<^sub>2 Q,A"
504  proof (rule cvalidtI)
505    fix s t
506    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
507    assume exec: "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t"
508    assume P: "s \<in> P"
509    assume t_notin_F: "t \<notin> Fault ` F"
510    from exec show "t \<in> Normal ` Q \<union> Abrupt ` A"
511    proof (cases)
512      fix s'
513      assume exec_c1: "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'"
514      assume exec_c2: "\<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t"
515      from cvalidt_postD [OF valid_c1 ctxt exec_c1 P]
516      have "Abrupt s' \<in> Abrupt ` R"
517        by auto
518      with cvalidt_postD [OF valid_c2 ctxt] exec_c2 t_notin_F
519      show ?thesis
520        by fastforce
521    next
522      assume exec_c1: "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t"
523      assume notAbr: "\<not> isAbr t"
524      from cvalidt_postD [OF valid_c1 ctxt exec_c1 P] t_notin_F
525      have "t \<in> Normal ` Q \<union> Abrupt ` R" .
526      with notAbr
527      show ?thesis
528        by auto
529    qed
530  next
531    fix s
532    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
533    assume P: "s \<in> P"
534    show "\<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 \<down> Normal s"
535    proof -
536      from valid_c1 ctxt P
537      have "\<Gamma>\<turnstile>c\<^sub>1\<down> Normal s"
538        by (rule cvalidt_termD)
539      moreover
540      {
541        fix r assume exec_c1: "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt r"
542        from cvalidt_postD [OF valid_c1 ctxt exec_c1 P]
543        have r: "Abrupt r\<in>Normal ` Q \<union> Abrupt ` R"
544          by auto
545        hence "Abrupt r\<in>Abrupt ` R" by fast
546        with cvalidt_termD [OF valid_c2 ctxt] exec_c1
547        have "\<Gamma>\<turnstile>c\<^sub>2 \<down> Normal r"
548          by fast
549      }
550      ultimately show ?thesis
551        by (iprover intro: terminates.intros)
552    qed
553  qed
554next
555  case (Conseq P \<Theta> F c Q A)
556  hence adapt:
557    "\<forall>s \<in> P. (\<exists>P' Q' A'. (\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q',A') \<and> s \<in> P'\<and> Q' \<subseteq> Q \<and> A' \<subseteq> A)" by blast
558  show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
559  proof (rule cvalidtI)
560    fix s t
561    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
562    assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
563    assume P: "s \<in> P"
564    assume t_notin_F: "t \<notin> Fault ` F"
565    show "t \<in> Normal ` Q \<union> Abrupt ` A"
566    proof -
567      from adapt [rule_format, OF P]
568      obtain P' and Q' and A' where
569        valid_P'_Q': "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q',A'"
570        and weaken: "s \<in> P'" "Q' \<subseteq>  Q" "A'\<subseteq> A"
571        by blast
572      from exec valid_P'_Q' ctxt t_notin_F
573      have P'_Q': "Normal s \<in> Normal ` P' \<longrightarrow>
574        t \<in> Normal ` Q' \<union> Abrupt ` A'"
575        by (unfold cvalidt_def validt_def valid_def) blast
576      hence "s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A'"
577        by blast
578      with weaken
579      show ?thesis
580        by blast
581    qed
582  next
583    fix s
584    assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
585    assume P: "s \<in> P"
586    show "\<Gamma>\<turnstile>c \<down> Normal s"
587    proof -
588      from P adapt
589      obtain P' and Q' and  A' where
590        "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q',A'"
591        "s \<in> P'"
592        by blast
593      with ctxt
594      show ?thesis
595        by (simp add: cvalidt_def validt_def)
596    qed
597  qed
598next
599  case (Asm P p Q A \<Theta> F)
600  assume "(P, p, Q, A) \<in> \<Theta>"
601  then show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
602    by (auto simp add: cvalidt_def )
603next
604  case ExFalso thus ?case by iprover
605qed
606
607lemma hoaret_sound':
608"\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
609  apply (drule hoaret_sound)
610  apply (simp add: cvalidt_def)
611  done
612
613theorem total_to_partial:
614 assumes total: "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" shows "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
615proof -
616  from total have "\<Gamma>,{}\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
617    by (rule hoaret_sound)
618  hence "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A"
619    by (simp add: cvalidt_def validt_def cvalid_def)
620  thus ?thesis
621    by (rule hoare_complete)
622qed
623
624subsection \<open>Completeness\<close>
625
626lemma MGT_valid:
627"\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F \<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> \<Gamma>\<turnstile>c\<down>Normal s} c
628    {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
629proof (rule validtI)
630  fix s t
631  assume "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
632         "s \<in> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> \<Gamma>\<turnstile>c\<down>Normal s}"
633         "t \<notin> Fault ` F"
634  thus "t \<in> Normal ` {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t} \<union>
635            Abrupt ` {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
636    apply (cases t)
637    apply (auto simp add: final_notin_def)
638    done
639next
640  fix s
641  assume "s \<in> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> \<Gamma>\<turnstile>c\<down>Normal s}"
642  thus "\<Gamma>\<turnstile>c\<down>Normal s"
643    by blast
644qed
645
646text \<open>The consequence rule where the existential @{term Z} is instantiated
647to @{term s}. Usefull in proof of \<open>MGT_lemma\<close>.\<close>
648lemma ConseqMGT:
649  assumes modif: "\<forall>Z::'a. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z::'a assn) c (Q' Z),(A' Z)"
650  assumes impl: "\<And>s. s \<in> P \<Longrightarrow> s \<in> P' s \<and> (\<forall>t. t \<in> Q' s \<longrightarrow> t \<in> Q) \<and>
651                                            (\<forall>t. t \<in> A' s \<longrightarrow> t \<in> A)"
652  shows "\<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
653using impl
654by - (rule conseq [OF modif],blast)
655
656lemma MGT_implies_complete:
657  assumes MGT: "\<forall>Z. \<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
658                                 \<Gamma>\<turnstile>c\<down>Normal s}
659                              c
660                            {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},
661                            {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
662  assumes valid: "\<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
663  shows "\<Gamma>,{} \<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
664  using MGT
665  apply (rule ConseqMGT)
666  apply (insert valid)
667  apply (auto simp add: validt_def valid_def intro!: final_notinI)
668  done
669
670lemma conseq_extract_state_indep_prop:
671  assumes state_indep_prop:"\<forall>s \<in> P. R"
672  assumes to_show: "R \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
673  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
674  apply (rule Conseq)
675  apply (clarify)
676  apply (rule_tac x="P" in exI)
677  apply (rule_tac x="Q" in exI)
678  apply (rule_tac x="A" in exI)
679  using state_indep_prop to_show
680  by blast
681
682lemma MGT_lemma:
683  assumes MGT_Calls:
684    "\<forall>p \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>
685       {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
686           \<Gamma>\<turnstile>(Call p)\<down>Normal s}
687             (Call p)
688       {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
689       {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
690  shows "\<And>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
691                          \<Gamma>\<turnstile>c\<down>Normal s}
692               c
693             {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
694proof (induct c)
695  case Skip
696  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Skip,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
697                   \<Gamma>\<turnstile>Skip \<down> Normal s}
698               Skip
699            {t. \<Gamma>\<turnstile>\<langle>Skip,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>Skip,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
700    by (rule hoaret.Skip [THEN conseqPre])
701       (auto elim: exec_elim_cases simp add: final_notin_def
702             intro: exec.intros terminates.intros)
703next
704  case (Basic f)
705  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Basic f,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
706                 \<Gamma>\<turnstile>Basic f \<down> Normal s}
707                Basic f
708              {t. \<Gamma>\<turnstile>\<langle>Basic f,Normal Z\<rangle> \<Rightarrow> Normal t},
709              {t. \<Gamma>\<turnstile>\<langle>Basic f,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
710    by (rule hoaret.Basic [THEN conseqPre])
711       (auto elim: exec_elim_cases simp add: final_notin_def
712             intro: exec.intros terminates.intros)
713next
714  case (Spec r)
715  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Spec r,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
716                    \<Gamma>\<turnstile>Spec r \<down> Normal s}
717                Spec r
718              {t. \<Gamma>\<turnstile>\<langle>Spec r,Normal Z\<rangle> \<Rightarrow> Normal t},
719              {t. \<Gamma>\<turnstile>\<langle>Spec r,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
720    apply (rule hoaret.Spec [THEN conseqPre])
721    apply (clarsimp simp add: final_notin_def)
722    apply (case_tac "\<exists>t. (Z,t) \<in> r")
723    apply (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
724    done
725next
726  case (Seq c1 c2)
727  have hyp_c1: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
728                                \<Gamma>\<turnstile>c1\<down>Normal s}
729                            c1
730                           {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t},
731                           {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
732    using Seq.hyps by iprover
733  have hyp_c2: "\<forall> Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
734                                 \<Gamma>\<turnstile>c2\<down>Normal s}
735                              c2
736                            {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t},
737                            {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
738    using Seq.hyps by iprover
739  from hyp_c1
740  have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
741                \<Gamma>\<turnstile>Seq c1 c2\<down>Normal s} c1
742    {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t \<and> \<Gamma>\<turnstile>\<langle>c2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
743        \<Gamma>\<turnstile>c2\<down>Normal t},
744    {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
745    by (rule ConseqMGT)
746       (auto dest: Seq_NoFaultStuckD1 [simplified] Seq_NoFaultStuckD2 [simplified]
747             elim: terminates_Normal_elim_cases
748             intro: exec.intros)
749  thus "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
750                 \<Gamma>\<turnstile>Seq c1 c2\<down>Normal s}
751                Seq c1 c2
752              {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
753              {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
754  proof (rule hoaret.Seq )
755    show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t \<and>
756                    \<Gamma>\<turnstile>\<langle>c2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> \<Gamma>\<turnstile>c2 \<down> Normal t}
757                 c2
758                {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
759                {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
760    proof (rule ConseqMGT [OF hyp_c2],safe)
761      fix r t
762      assume "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal r" "\<Gamma>\<turnstile>\<langle>c2,Normal r\<rangle> \<Rightarrow> Normal t"
763      then show "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t"
764        by (rule exec.intros)
765    next
766      fix r t
767      assume "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal r" "\<Gamma>\<turnstile>\<langle>c2,Normal r\<rangle> \<Rightarrow> Abrupt t"
768      then show "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t"
769        by (rule exec.intros)
770    qed
771  qed
772next
773  case (Cond b c1 c2)
774  have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
775                         \<Gamma>\<turnstile>c1\<down>Normal s}
776                     c1
777                   {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t},
778                   {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
779    using Cond.hyps by iprover
780  hence "\<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
781                     \<Gamma>\<turnstile>(Cond b c1 c2)\<down>Normal s}\<inter>b)
782                c1
783                {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
784                {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
785    by (rule ConseqMGT)
786       (fastforce simp add: final_notin_def intro: exec.CondTrue
787                 elim: terminates_Normal_elim_cases)
788  moreover
789  have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
790                               \<Gamma>\<turnstile>c2\<down>Normal s}
791                      c2
792                    {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t},
793                    {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
794    using Cond.hyps by iprover
795  hence "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
796                    \<Gamma>\<turnstile>(Cond b c1 c2)\<down>Normal s}\<inter>-b)
797                c2
798                {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
799                {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
800    by (rule ConseqMGT)
801       (fastforce simp add: final_notin_def intro: exec.CondFalse
802                 elim: terminates_Normal_elim_cases)
803  ultimately
804  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
805               \<Gamma>\<turnstile>(Cond b c1 c2)\<down>Normal s}
806               (Cond b c1 c2)
807              {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
808              {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
809    by (rule hoaret.Cond)
810next
811  case (While b c)
812  let ?unroll = "({(s,t). s\<in>b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t})\<^sup>*"
813  let ?P' = "\<lambda>Z. {t. (Z,t)\<in>?unroll \<and>
814                    (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b
815                         \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
816                             (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
817                                  \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and>
818                    \<Gamma>\<turnstile>(While b c)\<down>Normal t}"
819  let ?A = "\<lambda>Z. {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
820  let ?r = "{(t,s). \<Gamma>\<turnstile>(While b c)\<down>Normal s \<and> s\<in>b \<and>
821                    \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t}"
822  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
823                  \<Gamma>\<turnstile>(While b c)\<down>Normal s}
824              (While b c)
825              {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t},
826              {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
827  proof (rule ConseqMGT [where ?P'="\<lambda> Z. ?P' Z"
828                         and ?Q'="\<lambda> Z. ?P' Z \<inter> - b"])
829    have wf_r: "wf ?r" by (rule wf_terminates_while)
830    show "\<forall> Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (?P' Z) (While b c) (?P' Z \<inter> - b),(?A Z)"
831    proof (rule allI, rule hoaret.While [OF wf_r])
832      fix Z
833      from While
834      have hyp_c: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
835                                  \<Gamma>\<turnstile>c\<down>Normal s}
836                                c
837                              {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},
838                              {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by iprover
839      show "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> ?P' Z  \<inter> b) c
840                       ({t. (t, \<sigma>) \<in> ?r} \<inter> ?P' Z),(?A Z)"
841      proof (rule allI, rule ConseqMGT [OF hyp_c])
842        fix \<sigma> s
843        assume  "s\<in> {\<sigma>} \<inter>
844                   {t. (Z, t) \<in> ?unroll \<and>
845                      (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b
846                           \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
847                               (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
848                                    \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and>
849                      \<Gamma>\<turnstile>(While b c)\<down>Normal t}
850                   \<inter> b"
851        then obtain
852          s_eq_\<sigma>: "s=\<sigma>" and
853          Z_s_unroll: "(Z,s) \<in> ?unroll" and
854          noabort:"\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b
855                        \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
856                            (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
857                                  \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" and
858          while_term:  "\<Gamma>\<turnstile>(While b c)\<down>Normal s" and
859          s_in_b: "s\<in>b"
860          by blast
861        show "s \<in> {t. t = s \<and> \<Gamma>\<turnstile>\<langle>c,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
862                       \<Gamma>\<turnstile>c\<down>Normal t} \<and>
863        (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t} \<longrightarrow>
864             t \<in> {t. (t,\<sigma>) \<in> ?r} \<inter>
865                 {t. (Z, t) \<in> ?unroll \<and>
866                     (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow>  e\<in>b
867                           \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
868                              (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
869                                  \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and>
870                      \<Gamma>\<turnstile>(While b c)\<down>Normal t})  \<and>
871         (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t} \<longrightarrow>
872             t \<in> {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t})"
873          (is "?C1 \<and> ?C2 \<and> ?C3")
874        proof (intro conjI)
875          from Z_s_unroll noabort s_in_b while_term show ?C1
876            by (blast elim: terminates_Normal_elim_cases)
877        next
878          {
879            fix t
880            assume s_t: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t"
881            with s_eq_\<sigma> while_term s_in_b have "(t,\<sigma>) \<in> ?r"
882              by blast
883            moreover
884            from Z_s_unroll s_t s_in_b
885            have "(Z, t) \<in> ?unroll"
886              by (blast intro: rtrancl_into_rtrancl)
887            moreover from while_term s_t s_in_b
888            have "\<Gamma>\<turnstile>(While b c)\<down>Normal t"
889              by (blast elim: terminates_Normal_elim_cases)
890            moreover note noabort
891            ultimately
892            have "(t,\<sigma>) \<in> ?r \<and> (Z, t) \<in> ?unroll \<and>
893                  (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b
894                        \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
895                            (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
896                                  \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and>
897                  \<Gamma>\<turnstile>(While b c)\<down>Normal t"
898              by iprover
899          }
900          then show ?C2 by blast
901        next
902          {
903            fix t
904            assume s_t:  "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t"
905            from Z_s_unroll noabort s_t s_in_b
906            have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t"
907              by blast
908          } thus ?C3 by simp
909        qed
910      qed
911    qed
912  next
913    fix s
914    assume P: "s \<in> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
915                       \<Gamma>\<turnstile>While b c \<down> Normal s}"
916    hence WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
917      by auto
918    show "s \<in> ?P' s \<and>
919     (\<forall>t. t\<in>(?P' s \<inter> - b)\<longrightarrow>
920          t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t})\<and>
921     (\<forall>t. t\<in>?A s \<longrightarrow> t\<in>?A Z)"
922    proof (intro conjI)
923      {
924        fix e
925        assume "(Z,e) \<in> ?unroll" "e \<in> b"
926        from this WhileNoFault
927        have "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
928               (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
929                    \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" (is "?Prop Z e")
930        proof (induct rule: converse_rtrancl_induct [consumes 1])
931          assume e_in_b: "e \<in> b"
932          assume WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
933          with e_in_b WhileNoFault
934          have cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
935            by (auto simp add: final_notin_def intro: exec.intros)
936          moreover
937          {
938            fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u"
939            with e_in_b have "\<Gamma>\<turnstile>\<langle>While b c,Normal e\<rangle> \<Rightarrow> Abrupt u"
940              by (blast intro: exec.intros)
941          }
942          ultimately
943          show "?Prop e e"
944            by iprover
945        next
946          fix Z r
947          assume e_in_b: "e\<in>b"
948          assume WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
949          assume hyp: "\<lbrakk>e\<in>b;\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))\<rbrakk>
950                       \<Longrightarrow> ?Prop r e"
951          assume Z_r:
952            "(Z, r) \<in> {(Z, r). Z \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r}"
953          with WhileNoFault
954          have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
955            by (auto simp add: final_notin_def intro: exec.intros)
956          from hyp [OF e_in_b this] obtain
957            cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" and
958            Abrupt_r: "\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u \<longrightarrow>
959                            \<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u"
960            by simp
961
962           {
963            fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u"
964            with Abrupt_r have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u" by simp
965            moreover from  Z_r obtain
966              "Z \<in> b"  "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r"
967              by simp
968            ultimately have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u"
969              by (blast intro: exec.intros)
970          }
971          with cNoFault show "?Prop Z e"
972            by iprover
973        qed
974      }
975      with P show "s \<in> ?P' s"
976        by blast
977    next
978      {
979        fix t
980        assume "termination": "t \<notin> b"
981        assume "(Z, t) \<in> ?unroll"
982        hence "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t"
983        proof (induct rule: converse_rtrancl_induct [consumes 1])
984          from "termination"
985          show "\<Gamma>\<turnstile>\<langle>While b c,Normal t\<rangle> \<Rightarrow> Normal t"
986            by (blast intro: exec.WhileFalse)
987        next
988          fix Z r
989          assume first_body:
990                 "(Z, r) \<in> {(s, t). s \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t}"
991          assume "(r, t) \<in> ?unroll"
992          assume rest_loop: "\<Gamma>\<turnstile>\<langle>While b c, Normal r\<rangle> \<Rightarrow> Normal t"
993          show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t"
994          proof -
995            from first_body obtain
996              "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r"
997              by fast
998            moreover
999            from rest_loop have
1000              "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Normal t"
1001              by fast
1002            ultimately show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t"
1003              by (rule exec.WhileTrue)
1004          qed
1005        qed
1006      }
1007      with P
1008      show "(\<forall>t. t\<in>(?P' s \<inter> - b)
1009            \<longrightarrow>t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t})"
1010        by blast
1011    next
1012      from P show "\<forall>t. t\<in>?A s \<longrightarrow> t\<in>?A Z"
1013        by simp
1014    qed
1015  qed
1016next
1017  case (Call p)
1018  from noStuck_Call
1019  have "\<forall>s \<in> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1020                         \<Gamma>\<turnstile>Call p\<down> Normal s}.
1021          p \<in> dom \<Gamma>"
1022    by (fastforce simp add: final_notin_def)
1023  then show ?case
1024  proof (rule conseq_extract_state_indep_prop)
1025    assume p_defined: "p \<in> dom \<Gamma>"
1026    with MGT_Calls show
1027    "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>{s. s=Z \<and>
1028                 \<Gamma>\<turnstile>\<langle>Call p ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))\<and>
1029                 \<Gamma>\<turnstile>Call  p\<down>Normal s}
1030                (Call p)
1031               {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
1032               {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1033      by (auto)
1034  qed
1035next
1036  case (DynCom c)
1037  have hyp:
1038    "\<And>s'. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c s',Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1039                       \<Gamma>\<turnstile>c s'\<down>Normal s} c s'
1040      {t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1041    using DynCom by simp
1042  have hyp':
1043  "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>{s. s = Z \<and> \<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1044            \<Gamma>\<turnstile>DynCom c\<down>Normal s}
1045         (c Z)
1046        {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1047    by (rule ConseqMGT [OF hyp])
1048       (fastforce simp add: final_notin_def intro: exec.intros
1049          elim: terminates_Normal_elim_cases)
1050  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1051                 \<Gamma>\<turnstile>DynCom c\<down>Normal s}
1052                DynCom c
1053             {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t},
1054             {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1055    apply (rule hoaret.DynCom)
1056    apply (clarsimp)
1057    apply (rule hyp' [simplified])
1058    done
1059next
1060  case (Guard f g c)
1061  have hyp_c: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1062                              \<Gamma>\<turnstile>c\<down>Normal s}
1063                     c
1064                   {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},
1065                   {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1066    using Guard by iprover
1067  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1068                    \<Gamma>\<turnstile>Guard f g c\<down> Normal s}
1069                Guard f g c
1070              {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t},
1071              {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1072  proof (cases "f \<in> F")
1073    case True
1074    from hyp_c
1075    have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>(g \<inter> {s. s=Z \<and>
1076                     \<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck}\<union> Fault ` (-F))\<and>
1077                     \<Gamma>\<turnstile>Guard f g c\<down> Normal s})
1078                   c
1079                 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Normal t},
1080                 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1081      apply (rule ConseqMGT)
1082      apply (insert True)
1083      apply  (auto simp add: final_notin_def intro: exec.intros
1084                   elim: terminates_Normal_elim_cases)
1085      done
1086    from True this
1087    show ?thesis
1088      by (rule conseqPre [OF Guarantee]) auto
1089  next
1090    case False
1091    from hyp_c
1092    have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>(g \<inter> {s. s \<in> g \<and> s=Z \<and>
1093                     \<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck}\<union> Fault ` (-F))\<and>
1094                     \<Gamma>\<turnstile>Guard f g c\<down> Normal s} )
1095                   c
1096                 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Normal t},
1097                 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1098      apply (rule ConseqMGT)
1099      apply clarify
1100      apply (frule Guard_noFaultStuckD [OF _ False])
1101      apply  (auto simp add: final_notin_def intro: exec.intros
1102                   elim: terminates_Normal_elim_cases)
1103      done
1104    then show ?thesis
1105      apply (rule conseqPre [OF hoaret.Guard])
1106      apply clarify
1107      apply (frule Guard_noFaultStuckD [OF _ False])
1108      apply auto
1109      done
1110  qed
1111next
1112  case Throw
1113  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Throw,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1114                    \<Gamma>\<turnstile>Throw \<down> Normal s}
1115              Throw
1116              {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Normal t},
1117              {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1118    by (rule conseqPre [OF hoaret.Throw])
1119       (blast intro: exec.intros terminates.intros)
1120next
1121  case (Catch c\<^sub>1 c\<^sub>2)
1122  have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1123                        \<Gamma>\<turnstile>c\<^sub>1 \<down> Normal s}
1124                    c\<^sub>1
1125                  {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Normal t},
1126                  {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1127    using Catch.hyps by iprover
1128  hence "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^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)) \<and>
1129                   \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 \<down> Normal s}
1130                c\<^sub>1
1131               {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},
1132               {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t \<and> \<Gamma>\<turnstile>c\<^sub>2 \<down> Normal t \<and>
1133                   \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}"
1134    by (rule ConseqMGT)
1135       (fastforce intro: exec.intros terminates.intros
1136                 elim: terminates_Normal_elim_cases
1137                 simp add: final_notin_def)
1138  moreover
1139  have
1140    "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1141                     \<Gamma>\<turnstile>c\<^sub>2 \<down> Normal s} c\<^sub>2
1142                  {t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},
1143                  {t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1144    using Catch.hyps by iprover
1145  hence "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow>Abrupt s \<and> \<Gamma>\<turnstile>c\<^sub>2 \<down> Normal s \<and>
1146                   \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}
1147               c\<^sub>2
1148               {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},
1149               {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1150      by (rule ConseqMGT)
1151         (fastforce intro: exec.intros terminates.intros
1152                   simp add: noFault_def')
1153  ultimately
1154  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^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)) \<and>
1155                   \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 \<down> Normal s}
1156                Catch c\<^sub>1 c\<^sub>2
1157               {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},
1158               {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1159    by (rule hoaret.Catch )
1160qed
1161
1162
1163lemma Call_lemma':
1164 assumes Call_hyp:
1165 "\<forall>q\<in>dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1166                       \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma>}
1167                 (Call q)
1168                {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t},
1169                {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1170 shows "\<And>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>
1171      {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1172                (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c \<in> redexes c')}
1173              c
1174      {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},
1175      {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1176proof (induct c)
1177  case Skip
1178  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Skip,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1179                 \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and>
1180                (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Skip \<in> redexes c')}
1181               Skip
1182              {t. \<Gamma>\<turnstile>\<langle>Skip,Normal Z\<rangle> \<Rightarrow> Normal t},
1183              {t. \<Gamma>\<turnstile>\<langle>Skip,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1184    by (rule hoaret.Skip [THEN conseqPre]) (blast intro: exec.Skip)
1185next
1186  case (Basic f)
1187  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Basic f,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1188                   \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1189                (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and>
1190                      Basic f \<in> redexes c')}
1191               Basic f
1192              {t. \<Gamma>\<turnstile>\<langle>Basic f,Normal Z\<rangle> \<Rightarrow> Normal t},
1193              {t. \<Gamma>\<turnstile>\<langle>Basic f,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1194    by (rule hoaret.Basic [THEN conseqPre]) (blast intro: exec.Basic)
1195next
1196  case (Spec r)
1197  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Spec r,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1198                   \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1199                (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and>
1200                 Spec r \<in> redexes c')}
1201               Spec r
1202              {t. \<Gamma>\<turnstile>\<langle>Spec r,Normal Z\<rangle> \<Rightarrow> Normal t},
1203              {t. \<Gamma>\<turnstile>\<langle>Spec r,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1204    apply (rule hoaret.Spec [THEN conseqPre])
1205    apply (clarsimp)
1206    apply (case_tac "\<exists>t. (Z,t) \<in> r")
1207    apply (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros)
1208    done
1209next
1210  case (Seq c1 c2)
1211  have hyp_c1:
1212    "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1213                     \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1214                 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c1 \<in> redexes c')}
1215                c1
1216               {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t},
1217               {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1218    using Seq.hyps by iprover
1219  have hyp_c2:
1220    "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1221                    \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1222                 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c2 \<in> redexes c')}
1223                c2
1224               {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t},
1225               {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1226    using Seq.hyps (2) by iprover
1227  have c1: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1228                    \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1229              (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and>
1230                    Seq c1 c2 \<in> redexes c')}
1231               c1
1232               {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t \<and>
1233                   \<Gamma>\<turnstile>\<langle>c2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1234                   \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1235                  (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and>
1236                        c2 \<in> redexes c')},
1237               {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1238  proof (rule ConseqMGT [OF hyp_c1],clarify,safe)
1239    assume "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1240    thus "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1241      by (blast dest: Seq_NoFaultStuckD1)
1242  next
1243    fix c'
1244    assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)"
1245    assume red: "Seq c1 c2 \<in> redexes c'"
1246    from redexes_subset [OF red] steps_c'
1247    show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c1 \<in> redexes c'"
1248      by (auto iff: root_in_redexes)
1249  next
1250    fix t
1251    assume "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1252            "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t"
1253    thus "\<Gamma>\<turnstile>\<langle>c2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1254      by (blast dest: Seq_NoFaultStuckD2)
1255  next
1256    fix c' t
1257    assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)"
1258    assume red: "Seq c1 c2 \<in> redexes c'"
1259    assume exec_c1: "\<Gamma>\<turnstile> \<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t"
1260    show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal t) \<and> c2 \<in> redexes c'"
1261    proof -
1262      note steps_c'
1263      also
1264      from exec_impl_steps_Normal [OF exec_c1]
1265      have "\<Gamma>\<turnstile> (c1, Normal Z) \<rightarrow>\<^sup>* (Skip, Normal t)".
1266      from steps_redexes_Seq [OF this red]
1267      obtain c'' where
1268        steps_c'': "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow>\<^sup>* (c'', Normal t)" and
1269        Skip: "Seq Skip c2 \<in> redexes c''"
1270        by blast
1271      note steps_c''
1272      also
1273      have step_Skip: "\<Gamma>\<turnstile> (Seq Skip c2,Normal t) \<rightarrow> (c2,Normal t)"
1274        by (rule step.SeqSkip)
1275      from step_redexes [OF step_Skip Skip]
1276      obtain c''' where
1277        step_c''': "\<Gamma>\<turnstile> (c'', Normal t) \<rightarrow> (c''', Normal t)" and
1278        c2: "c2 \<in> redexes c'''"
1279        by blast
1280      note step_c'''
1281      finally show ?thesis
1282        using c2
1283        by blast
1284    qed
1285  next
1286    fix t
1287    assume "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1288    thus "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1289      by (blast intro: exec.intros)
1290  qed
1291  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1292                  \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1293              (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Seq c1 c2 \<in> redexes c')}
1294              Seq c1 c2
1295              {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
1296              {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1297    by (rule hoaret.Seq [OF c1 ConseqMGT [OF hyp_c2]])
1298       (blast intro: exec.intros)
1299next
1300  case (Cond b c1 c2)
1301  have hyp_c1:
1302       "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1303                        \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1304                    (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c1 \<in> redexes c')}
1305                   c1
1306                  {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t},
1307                  {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1308    using Cond.hyps by iprover
1309  have
1310  "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1311           \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1312           (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and>
1313                 Cond b c1 c2 \<in> redexes c')}
1314           \<inter> b)
1315           c1
1316          {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
1317          {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1318  proof (rule ConseqMGT [OF hyp_c1],safe)
1319    assume "Z \<in> b" "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1320    thus "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1321      by (auto simp add: final_notin_def intro: exec.CondTrue)
1322  next
1323    fix c'
1324    assume b: "Z \<in> b"
1325    assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)"
1326    assume redex_c': "Cond b c1 c2 \<in> redexes c'"
1327    show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c1 \<in> redexes c'"
1328    proof -
1329      note steps_c'
1330      also
1331      from b
1332      have "\<Gamma>\<turnstile>(Cond b c1 c2, Normal Z) \<rightarrow> (c1, Normal Z)"
1333        by (rule step.CondTrue)
1334      from step_redexes [OF this redex_c'] obtain c'' where
1335        step_c'': "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)" and
1336        c1: "c1 \<in> redexes c''"
1337        by blast
1338      note step_c''
1339      finally show ?thesis
1340        using c1
1341        by blast
1342    qed
1343  next
1344    fix t assume "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t"
1345    thus "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t"
1346      by (blast intro: exec.CondTrue)
1347  next
1348    fix t assume "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1349    thus "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1350      by (blast intro: exec.CondTrue)
1351  qed
1352  moreover
1353  have hyp_c2:
1354       "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1355                     \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1356                    (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c2 \<in> redexes c')}
1357                   c2
1358                  {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t},
1359                  {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1360    using Cond.hyps by iprover
1361  have
1362  "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1363              \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1364           (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal s) \<and>
1365                 Cond b c1 c2 \<in> redexes c')}
1366           \<inter> -b)
1367           c2
1368          {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
1369          {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1370  proof (rule ConseqMGT [OF hyp_c2],safe)
1371    assume "Z \<notin> b" "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1372    thus "\<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1373      by (auto simp add: final_notin_def intro: exec.CondFalse)
1374  next
1375    fix c'
1376    assume b: "Z \<notin> b"
1377    assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)"
1378    assume redex_c': "Cond b c1 c2 \<in> redexes c'"
1379    show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c2 \<in> redexes c'"
1380    proof -
1381      note steps_c'
1382      also
1383      from b
1384      have "\<Gamma>\<turnstile>(Cond b c1 c2, Normal Z) \<rightarrow> (c2, Normal Z)"
1385        by (rule step.CondFalse)
1386      from step_redexes [OF this redex_c'] obtain c'' where
1387        step_c'': "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)" and
1388        c1: "c2 \<in> redexes c''"
1389        by blast
1390      note step_c''
1391      finally show ?thesis
1392        using c1
1393        by blast
1394    qed
1395  next
1396    fix t assume "Z \<notin> b" "\<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t"
1397    thus "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t"
1398      by (blast intro: exec.CondFalse)
1399  next
1400    fix t assume "Z \<notin> b" "\<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1401    thus "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1402      by (blast intro: exec.CondFalse)
1403  qed
1404  ultimately
1405  show
1406   "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1407              \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1408           (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and>
1409                 Cond b c1 c2 \<in> redexes c')}
1410           (Cond b c1 c2)
1411          {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t},
1412          {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1413    by (rule hoaret.Cond)
1414next
1415  case (While b c)
1416  let ?unroll = "({(s,t). s\<in>b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t})\<^sup>*"
1417  let ?P' = "\<lambda>Z. {t. (Z,t)\<in>?unroll \<and>
1418                    (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b
1419                         \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1420                             (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
1421                                  \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and>
1422                    \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1423                  (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+
1424                               (c',Normal t) \<and> While b c \<in> redexes c')}"
1425  let ?A = "\<lambda>Z. {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1426  let ?r = "{(t,s). \<Gamma>\<turnstile>(While b c)\<down>Normal s \<and> s\<in>b \<and>
1427                    \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t}"
1428  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>
1429       {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1430                 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1431          (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>)\<rightarrow>\<^sup>+(c',Normal s) \<and> While b c \<in> redexes c')}
1432         (While b c)
1433       {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t},
1434       {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1435  proof (rule ConseqMGT [where ?P'="\<lambda> Z. ?P' Z"
1436                         and ?Q'="\<lambda> Z. ?P' Z \<inter> - b"])
1437    have wf_r: "wf ?r" by (rule wf_terminates_while)
1438    show "\<forall> Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (?P' Z) (While b c) (?P' Z \<inter> - b),(?A Z)"
1439    proof (rule allI, rule hoaret.While [OF wf_r])
1440      fix Z
1441      from While
1442      have hyp_c: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>
1443            {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1444                \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1445               (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c \<in> redexes c')}
1446              c
1447            {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},
1448            {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by iprover
1449      show "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> ?P' Z  \<inter> b) c
1450                       ({t. (t, \<sigma>) \<in> ?r} \<inter> ?P' Z),(?A Z)"
1451      proof (rule allI, rule ConseqMGT [OF hyp_c])
1452        fix \<tau> s
1453        assume  asm: "s\<in> {\<tau>} \<inter>
1454                   {t. (Z, t) \<in> ?unroll \<and>
1455                      (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b
1456                           \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1457                               (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
1458                                    \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and>
1459                     \<Gamma>\<turnstile>Call p\<down> Normal \<sigma> \<and>
1460                     (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+
1461                                  (c',Normal t) \<and> While b c \<in> redexes c')}
1462                   \<inter> b"
1463        then obtain c' where
1464          s_eq_\<tau>: "s=\<tau>" and
1465          Z_s_unroll: "(Z,s) \<in> ?unroll" and
1466          noabort:"\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b
1467                        \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1468                            (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
1469                                  \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" and
1470          termi:  "\<Gamma>\<turnstile>Call p \<down> Normal \<sigma>" and
1471          reach: "\<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s)" and
1472          red_c': "While b c \<in> redexes c'" and
1473          s_in_b: "s\<in>b"
1474          by blast
1475        obtain c'' where
1476          reach_c: "\<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c'',Normal s)"
1477                   "Seq c (While b c) \<in> redexes c''"
1478        proof -
1479          note reach
1480          also from s_in_b
1481          have "\<Gamma>\<turnstile>(While b c,Normal s) \<rightarrow> (Seq c (While b c),Normal s)"
1482            by (rule step.WhileTrue)
1483          from step_redexes [OF this red_c'] obtain c'' where
1484            step: "\<Gamma>\<turnstile> (c', Normal s) \<rightarrow> (c'', Normal s)" and
1485            red_c'': "Seq c (While b c) \<in> redexes c''"
1486            by blast
1487          note step
1488          finally
1489          show ?thesis
1490            using red_c''
1491            by (blast intro: that)
1492        qed
1493        from reach termi
1494        have "\<Gamma>\<turnstile>c' \<down> Normal s"
1495          by (rule steps_preserves_termination')
1496        from redexes_preserves_termination [OF this red_c']
1497        have termi_while: "\<Gamma>\<turnstile>While b c \<down> Normal s" .
1498        show "s \<in> {t. t = s \<and> \<Gamma>\<turnstile>\<langle>c,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1499                      \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and>
1500                   (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> c \<in> redexes c')} \<and>
1501        (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t} \<longrightarrow>
1502             t \<in> {t. (t,\<tau>) \<in> ?r} \<inter>
1503                 {t. (Z, t) \<in> ?unroll \<and>
1504                     (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow>  e\<in>b
1505                           \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1506                              (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
1507                                  \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and>
1508                      \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and>
1509                    (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and>
1510                          While b c \<in> redexes c')}) \<and>
1511         (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t} \<longrightarrow>
1512             t \<in> {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t})"
1513          (is "?C1 \<and> ?C2 \<and> ?C3")
1514        proof (intro conjI)
1515          from Z_s_unroll noabort s_in_b termi reach_c show ?C1
1516            apply clarsimp
1517            apply (drule redexes_subset)
1518            apply simp
1519            apply (blast intro: root_in_redexes)
1520            done
1521        next
1522          {
1523            fix t
1524            assume s_t: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t"
1525            with s_eq_\<tau> termi_while s_in_b have "(t,\<tau>) \<in> ?r"
1526              by blast
1527            moreover
1528            from Z_s_unroll s_t s_in_b
1529            have "(Z, t) \<in> ?unroll"
1530              by (blast intro: rtrancl_into_rtrancl)
1531            moreover
1532            obtain c'' where
1533              reach_c'': "\<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c'',Normal t)"
1534                        "(While b c) \<in> redexes c''"
1535            proof -
1536              note reach_c (1)
1537              also from s_in_b
1538              have "\<Gamma>\<turnstile>(While b c,Normal s)\<rightarrow> (Seq c (While b c),Normal s)"
1539                by (rule step.WhileTrue)
1540              have "\<Gamma>\<turnstile> (Seq c (While b c), Normal s) \<rightarrow>\<^sup>+
1541                        (While b c, Normal t)"
1542              proof -
1543                from exec_impl_steps_Normal [OF s_t]
1544                have "\<Gamma>\<turnstile> (c, Normal s) \<rightarrow>\<^sup>* (Skip, Normal t)".
1545                hence "\<Gamma>\<turnstile> (Seq c (While b c), Normal s) \<rightarrow>\<^sup>*
1546                          (Seq Skip (While b c), Normal t)"
1547                  by (rule SeqSteps) auto
1548                moreover
1549                have "\<Gamma>\<turnstile>(Seq Skip (While b c), Normal t)\<rightarrow>(While b c, Normal t)"
1550                  by (rule step.SeqSkip)
1551                ultimately show ?thesis by (rule rtranclp_into_tranclp1)
1552              qed
1553              from steps_redexes' [OF this reach_c (2)]
1554              obtain c''' where
1555                step: "\<Gamma>\<turnstile> (c'', Normal s) \<rightarrow>\<^sup>+ (c''', Normal t)" and
1556                red_c'': "While b c \<in> redexes c'''"
1557                by blast
1558              note step
1559              finally
1560              show ?thesis
1561                using red_c''
1562                by (blast intro: that)
1563            qed
1564            moreover note noabort termi
1565            ultimately
1566            have "(t,\<tau>) \<in> ?r \<and> (Z, t) \<in> ?unroll \<and>
1567                  (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b
1568                        \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1569                            (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
1570                                  \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and>
1571                  \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and>
1572                    (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal t) \<and>
1573                             While b c \<in> redexes c')"
1574              by iprover
1575          }
1576          then show ?C2 by blast
1577        next
1578          {
1579            fix t
1580            assume s_t:  "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t"
1581            from Z_s_unroll noabort s_t s_in_b
1582            have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1583              by blast
1584          } thus ?C3 by simp
1585        qed
1586      qed
1587    qed
1588  next
1589    fix s
1590    assume P: "s \<in> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1591                       \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1592                   (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and>
1593                         While b c \<in> redexes c')}"
1594    hence WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1595      by auto
1596    show "s \<in> ?P' s \<and>
1597     (\<forall>t. t\<in>(?P' s \<inter> - b)\<longrightarrow>
1598          t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t})\<and>
1599     (\<forall>t. t\<in>?A s \<longrightarrow> t\<in>?A Z)"
1600    proof (intro conjI)
1601      {
1602        fix e
1603        assume "(Z,e) \<in> ?unroll" "e \<in> b"
1604        from this WhileNoFault
1605        have "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1606               (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow>
1607                    \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" (is "?Prop Z e")
1608        proof (induct rule: converse_rtrancl_induct [consumes 1])
1609          assume e_in_b: "e \<in> b"
1610          assume WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1611          with e_in_b WhileNoFault
1612          have cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1613            by (auto simp add: final_notin_def intro: exec.intros)
1614          moreover
1615          {
1616            fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u"
1617            with e_in_b have "\<Gamma>\<turnstile>\<langle>While b c,Normal e\<rangle> \<Rightarrow> Abrupt u"
1618              by (blast intro: exec.intros)
1619          }
1620          ultimately
1621          show "?Prop e e"
1622            by iprover
1623        next
1624          fix Z r
1625          assume e_in_b: "e\<in>b"
1626          assume WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1627          assume hyp: "\<lbrakk>e\<in>b;\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))\<rbrakk>
1628                       \<Longrightarrow> ?Prop r e"
1629          assume Z_r:
1630            "(Z, r) \<in> {(Z, r). Z \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r}"
1631          with WhileNoFault
1632          have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1633            by (auto simp add: final_notin_def intro: exec.intros)
1634          from hyp [OF e_in_b this] obtain
1635            cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" and
1636            Abrupt_r: "\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u \<longrightarrow>
1637                            \<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u"
1638            by simp
1639
1640           {
1641            fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u"
1642            with Abrupt_r have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u" by simp
1643            moreover from  Z_r obtain
1644              "Z \<in> b"  "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r"
1645              by simp
1646            ultimately have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u"
1647              by (blast intro: exec.intros)
1648          }
1649          with cNoFault show "?Prop Z e"
1650            by iprover
1651        qed
1652      }
1653      with P show "s \<in> ?P' s"
1654        by blast
1655    next
1656      {
1657        fix t
1658        assume "termination": "t \<notin> b"
1659        assume "(Z, t) \<in> ?unroll"
1660        hence "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t"
1661        proof (induct rule: converse_rtrancl_induct [consumes 1])
1662          from "termination"
1663          show "\<Gamma>\<turnstile>\<langle>While b c,Normal t\<rangle> \<Rightarrow> Normal t"
1664            by (blast intro: exec.WhileFalse)
1665        next
1666          fix Z r
1667          assume first_body:
1668                 "(Z, r) \<in> {(s, t). s \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t}"
1669          assume "(r, t) \<in> ?unroll"
1670          assume rest_loop: "\<Gamma>\<turnstile>\<langle>While b c, Normal r\<rangle> \<Rightarrow> Normal t"
1671          show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t"
1672          proof -
1673            from first_body obtain
1674              "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r"
1675              by fast
1676            moreover
1677            from rest_loop have
1678              "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Normal t"
1679              by fast
1680            ultimately show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t"
1681              by (rule exec.WhileTrue)
1682          qed
1683        qed
1684      }
1685      with P
1686      show "\<forall>t. t\<in>(?P' s \<inter> - b)
1687            \<longrightarrow>t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t}"
1688        by blast
1689    next
1690      from P show "\<forall>t. t\<in>?A s \<longrightarrow> t\<in>?A Z"
1691        by simp
1692    qed
1693  qed
1694next
1695  case (Call q)
1696  let ?P = "{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1697               \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1698              (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Call q \<in> redexes c')}"
1699  from noStuck_Call
1700  have "\<forall>s \<in> ?P. q \<in> dom \<Gamma>"
1701    by (fastforce simp add: final_notin_def)
1702  then show ?case
1703  proof (rule conseq_extract_state_indep_prop)
1704    assume q_defined: "q \<in> dom \<Gamma>"
1705    from Call_hyp have
1706      "\<forall>q\<in>dom \<Gamma>. \<forall>Z.
1707        \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1708                        \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma>}
1709                 (Call q)
1710                {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t},
1711                {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1712      by (simp add: exec_Call_body' noFaultStuck_Call_body' [simplified]
1713         terminates_Normal_Call_body)
1714    from Call_hyp q_defined have Call_hyp':
1715    "\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1716                     \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma>}
1717                  (Call q)
1718                 {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t},
1719                 {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1720      by auto
1721    show
1722     "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ?P
1723           (Call q)
1724          {t. \<Gamma>\<turnstile>\<langle>Call q ,Normal Z\<rangle> \<Rightarrow> Normal t},
1725          {t. \<Gamma>\<turnstile>\<langle>Call q ,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1726    proof (rule ConseqMGT [OF Call_hyp'],safe)
1727      fix c'
1728      assume termi: "\<Gamma>\<turnstile>Call p \<down> Normal \<sigma>"
1729      assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)"
1730      assume red_c': "Call q \<in> redexes c'"
1731      show "\<Gamma>\<turnstile>Call q \<down> Normal Z"
1732      proof -
1733        from steps_preserves_termination' [OF steps_c' termi]
1734        have "\<Gamma>\<turnstile>c' \<down> Normal Z" .
1735        from redexes_preserves_termination [OF this red_c']
1736        show ?thesis .
1737      qed
1738    next
1739      fix c'
1740      assume termi: "\<Gamma>\<turnstile>Call p \<down> Normal \<sigma>"
1741      assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)"
1742      assume red_c': "Call q \<in> redexes c'"
1743      from redex_redexes [OF this]
1744      have "redex c' = Call q"
1745        by auto
1746      with termi steps_c'
1747      show "((Z, q), \<sigma>, p) \<in> termi_call_steps \<Gamma>"
1748        by (auto simp add: termi_call_steps_def)
1749    qed
1750  qed
1751next
1752  case (DynCom c)
1753  have hyp:
1754    "\<And>s'. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>
1755      {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c s',Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1756            \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and>
1757          (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c s' \<in> redexes c')}
1758        (c s')
1759       {t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1760    using DynCom by simp
1761  have hyp':
1762    "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1763                 \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and>
1764               (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> DynCom c \<in> redexes c')}
1765        (c Z)
1766       {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1767  proof (rule ConseqMGT [OF hyp],safe)
1768    assume "\<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1769    then show "\<Gamma>\<turnstile>\<langle>c Z,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1770      by (fastforce simp add: final_notin_def intro: exec.intros)
1771  next
1772    fix c'
1773    assume steps: "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)"
1774    assume c': "DynCom c \<in> redexes c'"
1775    have "\<Gamma>\<turnstile> (DynCom c, Normal Z) \<rightarrow> (c Z,Normal Z)"
1776      by (rule step.DynCom)
1777    from step_redexes [OF this c'] obtain c'' where
1778      step: "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)"  and c'': "c Z \<in> redexes c''"
1779      by blast
1780    note steps also note step
1781    finally show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c Z \<in> redexes c'"
1782      using c'' by blast
1783  next
1784    fix t
1785    assume "\<Gamma>\<turnstile>\<langle>c Z,Normal Z\<rangle> \<Rightarrow> Normal t"
1786    thus "\<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t"
1787      by (auto intro: exec.intros)
1788  next
1789    fix t
1790    assume "\<Gamma>\<turnstile>\<langle>c Z,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1791    thus "\<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1792      by (auto intro: exec.intros)
1793  qed
1794  show ?case
1795    apply (rule hoaret.DynCom)
1796    apply safe
1797    apply (rule hyp')
1798    done
1799next
1800  case (Guard f g c)
1801  have hyp_c: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>
1802         {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1803              \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1804            (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c \<in> redexes c')}
1805          c
1806         {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},
1807         {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1808    using Guard.hyps by iprover
1809  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1810                  \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1811            (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Guard f g c \<in> redexes c')}
1812              Guard f g c
1813              {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t},
1814              {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1815  proof (cases "f \<in> F")
1816    case True
1817    have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> {s. s=Z \<and>
1818                     \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1819                 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1820            (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and>
1821                  Guard f g c \<in> redexes c')})
1822              c
1823              {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t},
1824              {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1825    proof (rule ConseqMGT [OF hyp_c], safe)
1826      assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" "Z\<in>g"
1827      thus "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1828        by (auto simp add: final_notin_def intro: exec.intros)
1829    next
1830      fix c'
1831      assume steps: "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)"
1832      assume c': "Guard f g c \<in> redexes c'"
1833      assume "Z \<in> g"
1834      from this have "\<Gamma>\<turnstile>(Guard f g c,Normal Z) \<rightarrow> (c,Normal Z)"
1835        by (rule step.Guard)
1836      from step_redexes [OF this c'] obtain c'' where
1837        step: "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)"  and c'': "c \<in> redexes c''"
1838        by blast
1839      note steps also note step
1840      finally show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c \<in> redexes c'"
1841        using c'' by blast
1842    next
1843      fix t
1844      assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1845             "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t" "Z \<in> g"
1846      thus "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t"
1847        by (auto simp add: final_notin_def intro: exec.intros )
1848    next
1849      fix t
1850      assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1851              "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t" "Z \<in> g"
1852      thus "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1853        by (auto simp add: final_notin_def intro: exec.intros )
1854    qed
1855    from True this show ?thesis
1856      by (rule conseqPre [OF Guarantee]) auto
1857  next
1858    case False
1859    have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> {s. s=Z \<and>
1860                     \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1861                 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1862            (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and>
1863                  Guard f g c \<in> redexes c')})
1864              c
1865              {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t},
1866              {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1867    proof (rule ConseqMGT [OF hyp_c], safe)
1868      assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1869      thus "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1870        using False
1871        by (cases "Z\<in> g") (auto simp add: final_notin_def intro: exec.intros)
1872    next
1873      fix c'
1874      assume steps: "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)"
1875      assume c': "Guard f g c \<in> redexes c'"
1876
1877      assume "Z \<in> g"
1878      from this have "\<Gamma>\<turnstile>(Guard f g c,Normal Z) \<rightarrow> (c,Normal Z)"
1879        by (rule step.Guard)
1880      from step_redexes [OF this c'] obtain c'' where
1881        step: "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)"  and c'': "c \<in> redexes c''"
1882        by blast
1883      note steps also note step
1884      finally show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c \<in> redexes c'"
1885        using c'' by blast
1886    next
1887      fix t
1888      assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1889        "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t"
1890      thus "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t"
1891        using False
1892        by (cases "Z\<in> g") (auto simp add: final_notin_def intro: exec.intros )
1893    next
1894      fix t
1895      assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1896             "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1897      thus "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1898        using False
1899        by (cases "Z\<in> g") (auto simp add: final_notin_def intro: exec.intros )
1900    qed
1901    then show ?thesis
1902      apply (rule conseqPre [OF hoaret.Guard])
1903      apply clarify
1904      apply (frule Guard_noFaultStuckD [OF _ False])
1905      apply auto
1906      done
1907  qed
1908next
1909  case Throw
1910  show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Throw,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1911                  \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and>
1912                (\<exists>c'. \<Gamma>\<turnstile>(Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Throw \<in> redexes c')}
1913              Throw
1914              {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Normal t},
1915              {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1916    by (rule conseqPre [OF hoaret.Throw])
1917       (blast intro: exec.intros terminates.intros)
1918next
1919  case (Catch c\<^sub>1 c\<^sub>2)
1920  have hyp_c1:
1921   "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s= Z \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1922                    \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and>
1923                (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and>
1924                      c\<^sub>1 \<in> redexes c')}
1925               c\<^sub>1
1926              {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1927    using Catch.hyps by iprover
1928  have hyp_c2:
1929   "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s= Z \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
1930                     \<Gamma>\<turnstile>Call p\<down> Normal \<sigma> \<and>
1931                (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c\<^sub>2 \<in> redexes c')}
1932               c\<^sub>2
1933              {t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
1934    using Catch.hyps by iprover
1935  have
1936    "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^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)) \<and>
1937               \<Gamma>\<turnstile>Call p\<down> Normal \<sigma> \<and>
1938            (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>)\<rightarrow>\<^sup>+(c',Normal s) \<and>
1939                   Catch c\<^sub>1 c\<^sub>2 \<in> redexes c')}
1940            c\<^sub>1
1941           {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},
1942           {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t \<and>
1943               \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault`(-F)) \<and> \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and>
1944               (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> c\<^sub>2 \<in> redexes c')}"
1945  proof (rule ConseqMGT [OF hyp_c1],clarify,safe)
1946    assume "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1947    thus "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1948      by (fastforce simp add: final_notin_def intro: exec.intros)
1949  next
1950    fix c'
1951    assume steps: "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)"
1952    assume c': "Catch c\<^sub>1 c\<^sub>2 \<in> redexes c'"
1953    from steps redexes_subset [OF this]
1954    show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c\<^sub>1 \<in> redexes c'"
1955      by (auto iff:  root_in_redexes)
1956  next
1957    fix t
1958    assume "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Normal t"
1959    thus "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t"
1960      by (auto intro: exec.intros)
1961  next
1962    fix t
1963    assume "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1964      "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1965    thus "\<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))"
1966      by (auto simp add: final_notin_def intro: exec.intros)
1967  next
1968    fix c' t
1969    assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)"
1970    assume red: "Catch c\<^sub>1 c\<^sub>2 \<in> redexes c'"
1971    assume exec_c\<^sub>1: "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t"
1972    show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal t) \<and> c\<^sub>2 \<in> redexes c'"
1973    proof -
1974      note steps_c'
1975      also
1976      from exec_impl_steps_Normal_Abrupt [OF exec_c\<^sub>1]
1977      have "\<Gamma>\<turnstile> (c\<^sub>1, Normal Z) \<rightarrow>\<^sup>* (Throw, Normal t)".
1978      from steps_redexes_Catch [OF this red]
1979      obtain c'' where
1980        steps_c'': "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow>\<^sup>* (c'', Normal t)" and
1981        Catch: "Catch Throw c\<^sub>2 \<in> redexes c''"
1982        by blast
1983      note steps_c''
1984      also
1985      have step_Catch: "\<Gamma>\<turnstile> (Catch Throw c\<^sub>2,Normal t) \<rightarrow> (c\<^sub>2,Normal t)"
1986        by (rule step.CatchThrow)
1987      from step_redexes [OF step_Catch Catch]
1988      obtain c''' where
1989        step_c''': "\<Gamma>\<turnstile> (c'', Normal t) \<rightarrow> (c''', Normal t)" and
1990        c2: "c\<^sub>2 \<in> redexes c'''"
1991        by blast
1992      note step_c'''
1993      finally show ?thesis
1994        using c2
1995        by blast
1996    qed
1997  qed
1998  moreover
1999  have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t \<and>
2000                  \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
2001                  \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and>
2002                  (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> c\<^sub>2 \<in> redexes c')}
2003               c\<^sub>2
2004              {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},
2005              {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
2006    by (rule ConseqMGT [OF hyp_c2]) (fastforce intro: exec.intros)
2007  ultimately show ?case
2008    by (rule hoaret.Catch)
2009qed
2010
2011
2012text \<open>To prove a procedure implementation correct it suffices to assume
2013       only the procedure specifications of procedures that actually
2014       occur during evaluation of the body.
2015\<close>
2016
2017lemma Call_lemma:
2018 assumes A:
2019 "\<forall>q \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>
2020                 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
2021                    \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma>}
2022                 (Call q)
2023                {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t},
2024                {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
2025 assumes pdef: "p \<in> dom \<Gamma>"
2026 shows "\<And>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>
2027              ({\<sigma>} \<inter> {s. s=Z \<and>\<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
2028                                 \<Gamma>\<turnstile>the (\<Gamma> p)\<down>Normal s})
2029                 the (\<Gamma> p)
2030              {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t},
2031              {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}"
2032apply (rule conseqPre)
2033apply (rule Call_lemma' [OF A])
2034using pdef
2035apply (fastforce intro: terminates.intros tranclp.r_into_trancl [of "(step \<Gamma>)", OF step.Call] root_in_redexes)
2036done
2037
2038lemma Call_lemma_switch_Call_body:
2039 assumes
2040 call: "\<forall>q \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>
2041                 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
2042                    \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma>}
2043                 (Call q)
2044                {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t},
2045                {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
2046 assumes p_defined: "p \<in> dom \<Gamma>"
2047 shows "\<And>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>
2048              ({\<sigma>} \<inter> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
2049                                 \<Gamma>\<turnstile>Call p\<down>Normal s})
2050                 the (\<Gamma> p)
2051              {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
2052              {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
2053apply (simp only: exec_Call_body' [OF p_defined] noFaultStuck_Call_body' [OF p_defined] terminates_Normal_Call_body [OF p_defined])
2054apply (rule conseqPre)
2055apply (rule Call_lemma')
2056apply (rule call)
2057using p_defined
2058apply (fastforce intro: terminates.intros tranclp.r_into_trancl [of "(step \<Gamma>)", OF step.Call]
2059root_in_redexes)
2060done
2061
2062lemma MGT_Call:
2063"\<forall>p \<in> dom \<Gamma>. \<forall>Z.
2064  \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
2065             \<Gamma>\<turnstile>(Call p)\<down>Normal s}
2066           (Call p)
2067          {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
2068          {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
2069apply (intro ballI allI)
2070apply (rule CallRec' [where Procs="dom \<Gamma>" and
2071    P="\<lambda>p Z. {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
2072                    \<Gamma>\<turnstile>Call p\<down>Normal s}" and
2073    Q="\<lambda>p Z. {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}" and
2074    A="\<lambda>p Z. {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" and
2075    r="termi_call_steps \<Gamma>"
2076    ])
2077apply    simp
2078apply   simp
2079apply  (rule wf_termi_call_steps)
2080apply (intro ballI allI)
2081apply simp
2082apply (rule Call_lemma_switch_Call_body [rule_format, simplified])
2083apply  (rule hoaret.Asm)
2084apply  fastforce
2085apply assumption
2086done
2087
2088
2089lemma CollInt_iff: "{s. P s} \<inter> {s. Q s} = {s. P s \<and> Q s}"
2090  by auto
2091
2092lemma image_Un_conv: "f ` (\<Union>p\<in>dom \<Gamma>. \<Union>Z. {x p Z}) =  (\<Union>p\<in>dom \<Gamma>. \<Union>Z. {f (x p Z)})"
2093  by (auto iff: not_None_eq)
2094
2095
2096text \<open>Another proof of \<open>MGT_Call\<close>, maybe a little more readable\<close>
2097lemma
2098"\<forall>p \<in> dom \<Gamma>. \<forall>Z.
2099  \<Gamma>,{} \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
2100             \<Gamma>\<turnstile>(Call p)\<down>Normal s}
2101           (Call p)
2102          {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
2103          {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
2104proof -
2105  {
2106    fix p Z \<sigma>
2107    assume defined: "p \<in> dom \<Gamma>"
2108    define Specs where "Specs = (\<Union>p\<in>dom \<Gamma>. \<Union>Z.
2109            {({s. s=Z \<and>
2110              \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
2111              \<Gamma>\<turnstile>Call p\<down>Normal s},
2112             p,
2113             {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
2114             {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t})})"
2115    define Specs_wf where "Specs_wf p \<sigma> = (\<lambda>(P,q,Q,A).
2116                       (P \<inter> {s. ((s,q),\<sigma>,p) \<in> termi_call_steps \<Gamma>}, q, Q, A)) ` Specs" for p \<sigma>
2117    have "\<Gamma>,Specs_wf p \<sigma>
2118            \<turnstile>\<^sub>t\<^bsub>/F\<^esub>({\<sigma>} \<inter>
2119                 {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
2120                  \<Gamma>\<turnstile>the (\<Gamma> p)\<down>Normal s})
2121                (the (\<Gamma> p))
2122               {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t},
2123               {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}"
2124      apply (rule Call_lemma [rule_format, OF _ defined])
2125      apply (rule hoaret.Asm)
2126      apply (clarsimp simp add: Specs_wf_def Specs_def image_Un_conv)
2127      apply (rule_tac x=q in bexI)
2128      apply (rule_tac x=Z in exI)
2129      apply (clarsimp simp add: CollInt_iff)
2130      apply auto
2131      done
2132    hence "\<Gamma>,Specs_wf p \<sigma>
2133            \<turnstile>\<^sub>t\<^bsub>/F\<^esub>({\<sigma>} \<inter>
2134                 {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
2135                  \<Gamma>\<turnstile>Call p\<down>Normal s})
2136                (the (\<Gamma> p))
2137               {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
2138               {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
2139      by (simp only: exec_Call_body' [OF defined]
2140                   noFaultStuck_Call_body' [OF defined]
2141                  terminates_Normal_Call_body [OF defined])
2142  } note bdy=this
2143  show ?thesis
2144    apply (intro ballI allI)
2145    apply (rule hoaret.CallRec [where Specs="(\<Union>p\<in>dom \<Gamma>. \<Union>Z.
2146            {({s. s=Z \<and>
2147              \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
2148              \<Gamma>\<turnstile>Call p\<down>Normal s},
2149             p,
2150             {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
2151             {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t})})",
2152             OF _ wf_termi_call_steps [of \<Gamma>] refl])
2153    apply fastforce
2154    apply clarify
2155    apply (rule conjI)
2156    apply  fastforce
2157    apply (rule allI)
2158    apply (simp (no_asm_use) only : Un_empty_left)
2159    apply (rule bdy)
2160    apply auto
2161    done
2162qed
2163
2164
2165theorem hoaret_complete: "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> \<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
2166  by (iprover intro: MGT_implies_complete MGT_lemma [OF MGT_Call])
2167
2168lemma hoaret_complete':
2169  assumes cvalid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
2170  shows  "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
2171proof (cases "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A")
2172  case True
2173  hence "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
2174    by (rule hoaret_complete)
2175  thus "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
2176    by (rule hoaret_augment_context) simp
2177next
2178  case False
2179  with cvalid
2180  show ?thesis
2181    by (rule ExFalso)
2182qed
2183
2184subsection \<open>And Now: Some Useful Rules\<close>
2185
2186subsubsection \<open>Modify Return\<close>
2187
2188lemma ProcModifyReturn_sound:
2189  assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P call init p return' c Q,A"
2190  assumes valid_modif:
2191  "\<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call p) (Modif \<sigma>),(ModifAbr \<sigma>)"
2192  assumes res_modif:
2193  "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t"
2194  assumes ret_modifAbr:
2195  "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t"
2196  shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A"
2197proof (rule cvalidtI)
2198  fix s t
2199  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2200  hence "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A"
2201    by (auto simp add: validt_def)
2202  then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/UNIV\<^esub> P (Call p) Q,A"
2203    by (auto intro: valid_augment_Faults)
2204  assume exec: "\<Gamma>\<turnstile>\<langle>call init p return c,Normal s\<rangle> \<Rightarrow> t"
2205  assume P: "s \<in> P"
2206  assume t_notin_F: "t \<notin> Fault ` F"
2207  from exec
2208  show "t \<in> Normal ` Q \<union> Abrupt ` A"
2209  proof (cases rule: exec_call_Normal_elim)
2210    fix bdy t'
2211    assume bdy: "\<Gamma> p = Some bdy"
2212    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t'"
2213    assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t"
2214    from exec_body bdy
2215    have "\<Gamma>\<turnstile>\<langle>(Call p ),Normal (init s)\<rangle> \<Rightarrow> Normal t'"
2216      by (auto simp add: intro: exec.intros)
2217    from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
2218    have "t' \<in> Modif (init s)"
2219      by auto
2220    with res_modif have "Normal (return' s t') = Normal (return s t')"
2221      by simp
2222    with exec_body exec_c bdy
2223    have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> \<Rightarrow> t"
2224      by (auto intro: exec_call)
2225    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
2226    show ?thesis
2227      by simp
2228  next
2229    fix bdy t'
2230    assume bdy: "\<Gamma> p = Some bdy"
2231    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'"
2232    assume t: "t = Abrupt (return s t')"
2233    also from exec_body bdy
2234    have "\<Gamma>\<turnstile>\<langle>(Call p),Normal (init s)\<rangle> \<Rightarrow> Abrupt t'"
2235      by (auto simp add: intro: exec.intros)
2236    from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
2237    have "t' \<in> ModifAbr (init s)"
2238      by auto
2239    with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
2240      by simp
2241    finally have "t = Abrupt (return' s t')" .
2242    with exec_body bdy
2243    have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> \<Rightarrow> t"
2244      by (auto intro: exec_callAbrupt)
2245    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
2246    show ?thesis
2247      by simp
2248  next
2249    fix bdy f
2250    assume bdy: "\<Gamma> p = Some bdy"
2251    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f"  and
2252      t: "t = Fault f"
2253    with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> \<Rightarrow> t"
2254      by (auto intro: exec_callFault)
2255    from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F
2256    show ?thesis
2257      by simp
2258  next
2259    fix bdy
2260    assume bdy: "\<Gamma> p = Some bdy"
2261    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck"
2262      "t = Stuck"
2263    with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> \<Rightarrow> t"
2264      by (auto intro: exec_callStuck)
2265    from valid_call ctxt this P t_notin_F
2266    show ?thesis
2267      by (rule cvalidt_postD)
2268  next
2269    assume "\<Gamma> p = None" "t=Stuck"
2270    hence "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> \<Rightarrow> t"
2271      by (auto intro: exec_callUndefined)
2272    from valid_call ctxt this P t_notin_F
2273    show ?thesis
2274      by (rule cvalidt_postD)
2275  qed
2276next
2277  fix s
2278  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2279  hence "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A"
2280    by (auto simp add: validt_def)
2281  then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/UNIV\<^esub> P (Call p) Q,A"
2282    by (auto intro: valid_augment_Faults)
2283  assume P: "s \<in> P"
2284  from valid_call ctxt P
2285  have call: "\<Gamma>\<turnstile>call init p return' c\<down> Normal s"
2286    by (rule cvalidt_termD)
2287  show "\<Gamma>\<turnstile>call init p return c \<down> Normal s"
2288  proof (cases "p \<in> dom \<Gamma>")
2289    case True
2290    with call obtain bdy where
2291      bdy: "\<Gamma> p = Some bdy" and termi_bdy: "\<Gamma>\<turnstile>bdy \<down> Normal (init s)" and
2292      termi_c: "\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow>
2293                    \<Gamma>\<turnstile>c s t \<down> Normal (return' s t)"
2294      by cases auto
2295    {
2296      fix t
2297      assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t"
2298      hence "\<Gamma>\<turnstile>c s t \<down> Normal (return s t)"
2299      proof -
2300        from exec_bdy bdy
2301        have "\<Gamma>\<turnstile>\<langle>(Call p ),Normal (init s)\<rangle> \<Rightarrow> Normal t"
2302          by (auto simp add: intro: exec.intros)
2303        from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
2304          res_modif
2305        have "return' s t = return s t"
2306          by auto
2307        with termi_c exec_bdy show ?thesis by auto
2308      qed
2309    }
2310    with bdy termi_bdy
2311    show ?thesis
2312      by (iprover intro: terminates_call)
2313  next
2314    case False
2315    thus ?thesis
2316      by (auto intro: terminates_callUndefined)
2317  qed
2318qed
2319
2320lemma ProcModifyReturn:
2321  assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return' c) Q,A"
2322  assumes res_modif:
2323  "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)"
2324  assumes ret_modifAbr:
2325  "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> (return' s t) = (return s t)"
2326  assumes modifies_spec:
2327  "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call p) (Modif \<sigma>),(ModifAbr \<sigma>)"
2328  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A"
2329apply (rule hoaret_complete')
2330apply (rule ProcModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr,
2331        OF _ _ res_modif ret_modifAbr])
2332apply (rule hoaret_sound [OF spec])
2333using modifies_spec
2334apply (blast intro: hoare_sound)
2335done
2336
2337lemma ProcModifyReturnSameFaults_sound:
2338  assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P call init p return' c Q,A"
2339  assumes valid_modif:
2340  "\<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
2341  assumes res_modif:
2342  "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t"
2343  assumes ret_modifAbr:
2344  "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t"
2345  shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A"
2346proof (rule cvalidtI)
2347  fix s t
2348  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2349  hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A"
2350    by (auto simp add: validt_def)
2351  assume exec: "\<Gamma>\<turnstile>\<langle>call init p return c,Normal s\<rangle> \<Rightarrow> t"
2352  assume P: "s \<in> P"
2353  assume t_notin_F: "t \<notin> Fault ` F"
2354  from exec
2355  show "t \<in> Normal ` Q \<union> Abrupt ` A"
2356  proof (cases rule: exec_call_Normal_elim)
2357    fix bdy t'
2358    assume bdy: "\<Gamma> p = Some bdy"
2359    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t'"
2360    assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t"
2361    from exec_body bdy
2362    have "\<Gamma>\<turnstile>\<langle>(Call p) ,Normal (init s)\<rangle> \<Rightarrow> Normal t'"
2363      by (auto simp add: intro: exec.intros)
2364    from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
2365    have "t' \<in> Modif (init s)"
2366      by auto
2367    with res_modif have "Normal (return' s t') = Normal (return s t')"
2368      by simp
2369    with exec_body exec_c bdy
2370    have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> \<Rightarrow> t"
2371      by (auto intro: exec_call)
2372    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
2373    show ?thesis
2374      by simp
2375  next
2376    fix bdy t'
2377    assume bdy: "\<Gamma> p = Some bdy"
2378    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'"
2379    assume t: "t = Abrupt (return s t')"
2380    also
2381    from exec_body bdy
2382    have "\<Gamma>\<turnstile>\<langle>Call p ,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'"
2383      by (auto simp add: intro: exec.intros)
2384    from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
2385    have "t' \<in> ModifAbr (init s)"
2386      by auto
2387    with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
2388      by simp
2389    finally have "t = Abrupt (return' s t')" .
2390    with exec_body bdy
2391    have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> \<Rightarrow> t"
2392      by (auto intro: exec_callAbrupt)
2393    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
2394    show ?thesis
2395      by simp
2396  next
2397    fix bdy f
2398    assume bdy: "\<Gamma> p = Some bdy"
2399    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f"  and
2400      t: "t = Fault f"
2401    with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> \<Rightarrow> t"
2402      by (auto intro: exec_callFault)
2403    from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F
2404    show ?thesis
2405      by simp
2406  next
2407    fix bdy
2408    assume bdy: "\<Gamma> p = Some bdy"
2409    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck"
2410      "t = Stuck"
2411    with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> \<Rightarrow> t"
2412      by (auto intro: exec_callStuck)
2413    from valid_call ctxt this P t_notin_F
2414    show ?thesis
2415      by (rule cvalidt_postD)
2416  next
2417    assume "\<Gamma> p = None" "t=Stuck"
2418    hence "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> \<Rightarrow> t"
2419      by (auto intro: exec_callUndefined)
2420    from valid_call ctxt this P t_notin_F
2421    show ?thesis
2422      by (rule cvalidt_postD)
2423  qed
2424next
2425  fix s
2426  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2427  hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A"
2428    by (auto simp add: validt_def)
2429  assume P: "s \<in> P"
2430  from valid_call ctxt P
2431  have call: "\<Gamma>\<turnstile>call init p return' c\<down> Normal s"
2432    by (rule cvalidt_termD)
2433  show "\<Gamma>\<turnstile>call init p return c \<down> Normal s"
2434  proof (cases "p \<in> dom \<Gamma>")
2435    case True
2436    with call obtain bdy where
2437      bdy: "\<Gamma> p = Some bdy" and termi_bdy: "\<Gamma>\<turnstile>bdy \<down> Normal (init s)" and
2438      termi_c: "\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow>
2439                    \<Gamma>\<turnstile>c s t \<down> Normal (return' s t)"
2440      by cases auto
2441    {
2442      fix t
2443      assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t"
2444      hence "\<Gamma>\<turnstile>c s t \<down> Normal (return s t)"
2445      proof -
2446        from exec_bdy bdy
2447        have "\<Gamma>\<turnstile>\<langle>(Call p ),Normal (init s)\<rangle> \<Rightarrow> Normal t"
2448          by (auto simp add: intro: exec.intros)
2449        from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P
2450          res_modif
2451        have "return' s t = return s t"
2452          by auto
2453        with termi_c exec_bdy show ?thesis by auto
2454      qed
2455    }
2456    with bdy termi_bdy
2457    show ?thesis
2458      by (iprover intro: terminates_call)
2459  next
2460    case False
2461    thus ?thesis
2462      by (auto intro: terminates_callUndefined)
2463  qed
2464qed
2465
2466lemma ProcModifyReturnSameFaults:
2467  assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return' c) Q,A"
2468  assumes res_modif:
2469  "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)"
2470  assumes ret_modifAbr:
2471  "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> (return' s t) = (return s t)"
2472  assumes modifies_spec:
2473  "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call p) (Modif \<sigma>),(ModifAbr \<sigma>)"
2474  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A"
2475apply (rule hoaret_complete')
2476apply (rule ProcModifyReturnSameFaults_sound [where Modif=Modif and ModifAbr=ModifAbr,
2477          OF _ _ res_modif ret_modifAbr])
2478apply (rule hoaret_sound [OF spec])
2479using modifies_spec
2480apply (blast intro: hoare_sound)
2481done
2482
2483
2484subsubsection \<open>DynCall\<close>
2485
2486
2487lemma dynProcModifyReturn_sound:
2488assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
2489assumes valid_modif:
2490    "\<forall>s\<in>P. \<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call (p s)) (Modif \<sigma>),(ModifAbr \<sigma>)"
2491assumes ret_modif:
2492    "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t"
2493assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t"
2494shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
2495proof (rule cvalidtI)
2496  fix s t
2497  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2498  hence "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A"
2499    by (auto simp add: validt_def)
2500  then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/UNIV\<^esub> P (Call p) Q,A"
2501    by (auto intro: valid_augment_Faults)
2502  assume exec: "\<Gamma>\<turnstile>\<langle>dynCall init p return c,Normal s\<rangle> \<Rightarrow> t"
2503  assume t_notin_F: "t \<notin> Fault ` F"
2504  assume P: "s \<in> P"
2505  with valid_modif
2506  have valid_modif':
2507    "\<forall>\<sigma>. \<Gamma>,\<Theta>\<Turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call (p s)) (Modif \<sigma>),(ModifAbr \<sigma>)"
2508    by blast
2509  from exec
2510  have "\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> \<Rightarrow> t"
2511    by (cases rule: exec_dynCall_Normal_elim)
2512  then show "t \<in> Normal ` Q \<union> Abrupt ` A"
2513  proof (cases rule: exec_call_Normal_elim)
2514    fix bdy t'
2515    assume bdy: "\<Gamma> (p s) = Some bdy"
2516    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t'"
2517    assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t"
2518    from exec_body bdy
2519    have "\<Gamma>\<turnstile>\<langle>Call (p s),Normal (init s)\<rangle> \<Rightarrow> Normal t'"
2520      by (auto simp add: intro: exec.Call)
2521    from cvalidD [OF valid_modif' [rule_format, of "init s"] ctxt' this] P
2522    have "t' \<in> Modif (init s)"
2523      by auto
2524    with ret_modif have "Normal (return' s t') =
2525      Normal (return s t')"
2526      by simp
2527    with exec_body exec_c bdy
2528    have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> \<Rightarrow> t"
2529      by (auto intro: exec_call)
2530    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t"
2531      by (rule exec_dynCall)
2532    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
2533    show ?thesis
2534      by simp
2535  next
2536    fix bdy t'
2537    assume bdy: "\<Gamma> (p s) = Some bdy"
2538    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'"
2539    assume t: "t = Abrupt (return s t')"
2540    also from exec_body bdy
2541    have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'"
2542      by (auto simp add: intro: exec.intros)
2543    from cvalidD [OF valid_modif' [rule_format, of "init s"] ctxt' this] P
2544    have "t' \<in> ModifAbr (init s)"
2545      by auto
2546    with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
2547      by simp
2548    finally have "t = Abrupt (return' s t')" .
2549    with exec_body bdy
2550    have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> \<Rightarrow> t"
2551      by (auto intro: exec_callAbrupt)
2552    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t"
2553      by (rule exec_dynCall)
2554    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
2555    show ?thesis
2556      by simp
2557  next
2558    fix bdy f
2559    assume bdy: "\<Gamma> (p s) = Some bdy"
2560    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f"  and
2561      t: "t = Fault f"
2562    with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> \<Rightarrow> t"
2563      by (auto intro: exec_callFault)
2564    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t"
2565      by (rule exec_dynCall)
2566    from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F
2567    show ?thesis
2568      by blast
2569  next
2570    fix bdy
2571    assume bdy: "\<Gamma> (p s) = Some bdy"
2572    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck"
2573      "t = Stuck"
2574    with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> \<Rightarrow> t"
2575      by (auto intro: exec_callStuck)
2576    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t"
2577      by (rule exec_dynCall)
2578    from valid_call ctxt this P t_notin_F
2579    show ?thesis
2580      by (rule cvalidt_postD)
2581  next
2582    fix bdy
2583    assume "\<Gamma> (p s) = None" "t=Stuck"
2584    hence "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> \<Rightarrow> t"
2585      by (auto intro: exec_callUndefined)
2586    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t"
2587      by (rule exec_dynCall)
2588    from valid_call ctxt this P t_notin_F
2589    show ?thesis
2590      by (rule cvalidt_postD)
2591  qed
2592next
2593  fix s
2594  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2595  hence "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A"
2596    by (auto simp add: validt_def)
2597  then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/UNIV\<^esub> P (Call p) Q,A"
2598    by (auto intro: valid_augment_Faults)
2599  assume P: "s \<in> P"
2600  from valid_call ctxt P
2601  have "\<Gamma>\<turnstile>dynCall init p return' c\<down> Normal s"
2602    by (rule cvalidt_termD)
2603  hence call: "\<Gamma>\<turnstile>call init (p s) return' c\<down> Normal s"
2604    by cases
2605  have "\<Gamma>\<turnstile>call init (p s) return c \<down> Normal s"
2606  proof (cases "p s \<in> dom \<Gamma>")
2607    case True
2608    with call obtain bdy where
2609      bdy: "\<Gamma> (p s) = Some bdy" and termi_bdy: "\<Gamma>\<turnstile>bdy \<down> Normal (init s)" and
2610      termi_c: "\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow>
2611                    \<Gamma>\<turnstile>c s t \<down> Normal (return' s t)"
2612      by cases auto
2613    {
2614      fix t
2615      assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t"
2616      hence "\<Gamma>\<turnstile>c s t \<down> Normal (return s t)"
2617      proof -
2618        from exec_bdy bdy
2619        have "\<Gamma>\<turnstile>\<langle>Call (p s),Normal (init s)\<rangle> \<Rightarrow> Normal t"
2620          by (auto simp add: intro: exec.intros)
2621        from cvalidD [OF valid_modif [rule_format, of s "init s"] ctxt' this] P
2622          ret_modif
2623        have "return' s t = return s t"
2624          by auto
2625        with termi_c exec_bdy show ?thesis by auto
2626      qed
2627    }
2628    with bdy termi_bdy
2629    show ?thesis
2630      by (iprover intro: terminates_call)
2631  next
2632    case False
2633    thus ?thesis
2634      by (auto intro: terminates_callUndefined)
2635  qed
2636  thus "\<Gamma>\<turnstile>dynCall init p return c \<down> Normal s"
2637    by (iprover intro: terminates_dynCall)
2638qed
2639
2640lemma dynProcModifyReturn:
2641assumes dyn_call: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
2642assumes ret_modif:
2643    "\<forall>s t. t \<in> Modif (init s)
2644           \<longrightarrow> return' s t = return s t"
2645assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
2646                             \<longrightarrow> return' s t = return s t"
2647assumes modif:
2648    "\<forall>s \<in> P. \<forall>\<sigma>.
2649       \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
2650shows "\<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
2651apply (rule hoaret_complete')
2652apply (rule dynProcModifyReturn_sound
2653        [where Modif=Modif and ModifAbr=ModifAbr,
2654            OF hoaret_sound [OF dyn_call] _ ret_modif ret_modifAbr])
2655apply (intro ballI allI)
2656apply (rule hoare_sound [OF modif [rule_format]])
2657apply assumption
2658done
2659
2660lemma dynProcModifyReturnSameFaults_sound:
2661assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
2662assumes valid_modif:
2663    "\<forall>s\<in>P. \<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
2664assumes ret_modif:
2665    "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t"
2666assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t"
2667shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
2668proof (rule cvalidtI)
2669  fix s t
2670  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2671  hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A"
2672    by (auto simp add: validt_def)
2673  assume exec: "\<Gamma>\<turnstile>\<langle>dynCall init p return c,Normal s\<rangle> \<Rightarrow> t"
2674  assume t_notin_F: "t \<notin> Fault ` F"
2675  assume P: "s \<in> P"
2676  with valid_modif
2677  have valid_modif':
2678    "\<forall>\<sigma>. \<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call (p s)) (Modif \<sigma>),(ModifAbr \<sigma>)"
2679    by blast
2680  from exec
2681  have "\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> \<Rightarrow> t"
2682    by (cases rule: exec_dynCall_Normal_elim)
2683  then show "t \<in> Normal ` Q \<union> Abrupt ` A"
2684  proof (cases rule: exec_call_Normal_elim)
2685    fix bdy t'
2686    assume bdy: "\<Gamma> (p s) = Some bdy"
2687    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t'"
2688    assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t"
2689    from exec_body bdy
2690    have "\<Gamma>\<turnstile>\<langle>Call (p s),Normal (init s)\<rangle> \<Rightarrow> Normal t'"
2691      by (auto simp add: intro: exec.intros)
2692    from cvalidD [OF valid_modif' [rule_format, of "init s"] ctxt' this] P
2693    have "t' \<in> Modif (init s)"
2694      by auto
2695    with ret_modif have "Normal (return' s t') =
2696      Normal (return s t')"
2697      by simp
2698    with exec_body exec_c bdy
2699    have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> \<Rightarrow> t"
2700      by (auto intro: exec_call)
2701    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t"
2702      by (rule exec_dynCall)
2703    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
2704    show ?thesis
2705      by simp
2706  next
2707    fix bdy t'
2708    assume bdy: "\<Gamma> (p s) = Some bdy"
2709    assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'"
2710    assume t: "t = Abrupt (return s t')"
2711    also from exec_body bdy
2712    have "\<Gamma>\<turnstile>\<langle>Call (p s)  ,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'"
2713      by (auto simp add: intro: exec.intros)
2714    from cvalidD [OF valid_modif' [rule_format, of "init s"] ctxt' this] P
2715    have "t' \<in> ModifAbr (init s)"
2716      by auto
2717    with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
2718      by simp
2719    finally have "t = Abrupt (return' s t')" .
2720    with exec_body bdy
2721    have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> \<Rightarrow> t"
2722      by (auto intro: exec_callAbrupt)
2723    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t"
2724      by (rule exec_dynCall)
2725    from cvalidt_postD [OF valid_call ctxt this] P t_notin_F
2726    show ?thesis
2727      by simp
2728  next
2729    fix bdy f
2730    assume bdy: "\<Gamma> (p s) = Some bdy"
2731    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f"  and
2732      t: "t = Fault f"
2733    with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> \<Rightarrow> t"
2734      by (auto intro: exec_callFault)
2735    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t"
2736      by (rule exec_dynCall)
2737    from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F
2738    show ?thesis
2739      by simp
2740  next
2741    fix bdy
2742    assume bdy: "\<Gamma> (p s) = Some bdy"
2743    assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck"
2744      "t = Stuck"
2745    with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> \<Rightarrow> t"
2746      by (auto intro: exec_callStuck)
2747    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t"
2748      by (rule exec_dynCall)
2749    from valid_call ctxt this P t_notin_F
2750    show ?thesis
2751      by (rule cvalidt_postD)
2752  next
2753    fix bdy
2754    assume "\<Gamma> (p s) = None" "t=Stuck"
2755    hence "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> \<Rightarrow> t"
2756      by (auto intro: exec_callUndefined)
2757    hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t"
2758      by (rule exec_dynCall)
2759    from valid_call ctxt this P t_notin_F
2760    show ?thesis
2761      by (rule cvalidt_postD)
2762  qed
2763next
2764  fix s
2765  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2766  hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A"
2767    by (auto simp add: validt_def)
2768  assume P: "s \<in> P"
2769  from valid_call ctxt P
2770  have "\<Gamma>\<turnstile>dynCall init p return' c\<down> Normal s"
2771    by (rule cvalidt_termD)
2772  hence call: "\<Gamma>\<turnstile>call init (p s) return' c\<down> Normal s"
2773    by cases
2774  have "\<Gamma>\<turnstile>call init (p s) return c \<down> Normal s"
2775  proof (cases "p s \<in> dom \<Gamma>")
2776    case True
2777    with call obtain bdy where
2778      bdy: "\<Gamma> (p s) = Some bdy" and termi_bdy: "\<Gamma>\<turnstile>bdy \<down> Normal (init s)" and
2779      termi_c: "\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow>
2780                    \<Gamma>\<turnstile>c s t \<down> Normal (return' s t)"
2781      by cases auto
2782    {
2783      fix t
2784      assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t"
2785      hence "\<Gamma>\<turnstile>c s t \<down> Normal (return s t)"
2786      proof -
2787        from exec_bdy bdy
2788        have "\<Gamma>\<turnstile>\<langle>Call (p s),Normal (init s)\<rangle> \<Rightarrow> Normal t"
2789          by (auto simp add: intro: exec.intros)
2790        from cvalidD [OF valid_modif [rule_format, of s "init s"] ctxt' this] P
2791          ret_modif
2792        have "return' s t = return s t"
2793          by auto
2794        with termi_c exec_bdy show ?thesis by auto
2795      qed
2796    }
2797    with bdy termi_bdy
2798    show ?thesis
2799      by (iprover intro: terminates_call)
2800  next
2801    case False
2802    thus ?thesis
2803      by (auto intro: terminates_callUndefined)
2804  qed
2805  thus "\<Gamma>\<turnstile>dynCall init p return c \<down> Normal s"
2806    by (iprover intro: terminates_dynCall)
2807qed
2808
2809lemma dynProcModifyReturnSameFaults:
2810assumes dyn_call: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
2811assumes ret_modif:
2812    "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t"
2813assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t"
2814assumes modif:
2815    "\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
2816shows "\<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
2817apply (rule hoaret_complete')
2818apply (rule dynProcModifyReturnSameFaults_sound
2819        [where Modif=Modif and ModifAbr=ModifAbr,
2820          OF hoaret_sound [OF dyn_call] _ ret_modif ret_modifAbr])
2821apply (intro ballI allI)
2822apply (rule hoare_sound [OF modif [rule_format]])
2823apply assumption
2824done
2825
2826subsubsection \<open>Conjunction of Postcondition\<close>
2827
2828lemma PostConjI_sound:
2829  assumes valid_Q: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
2830  assumes valid_R: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c R,B"
2831  shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> B)"
2832proof (rule cvalidtI)
2833  fix s t
2834  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2835  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
2836  assume P: "s \<in> P"
2837  assume t_notin_F: "t \<notin> Fault ` F"
2838  from valid_Q ctxt exec P t_notin_F have "t \<in> Normal ` Q \<union> Abrupt ` A"
2839    by (rule cvalidt_postD)
2840  moreover
2841  from valid_R ctxt exec P t_notin_F have "t \<in> Normal ` R \<union> Abrupt ` B"
2842    by (rule cvalidt_postD)
2843  ultimately show "t \<in> Normal ` (Q \<inter> R) \<union> Abrupt ` (A \<inter> B)"
2844    by blast
2845next
2846  fix s
2847  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2848  assume P: "s \<in> P"
2849  from valid_Q ctxt P
2850  show "\<Gamma>\<turnstile>c \<down> Normal s"
2851    by (rule cvalidt_termD)
2852qed
2853
2854lemma PostConjI:
2855  assumes deriv_Q: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
2856  assumes deriv_R: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c R,B"
2857  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> B)"
2858apply (rule hoaret_complete')
2859apply (rule PostConjI_sound)
2860apply (rule hoaret_sound [OF deriv_Q])
2861apply (rule hoaret_sound [OF deriv_R])
2862done
2863
2864
2865lemma Merge_PostConj_sound:
2866  assumes validF: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
2867  assumes validG: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/G\<^esub> P' c R,X"
2868  assumes F_G: "F \<subseteq> G"
2869  assumes P_P': "P \<subseteq> P'"
2870  shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> X)"
2871proof (rule cvalidtI)
2872  fix s t
2873  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2874  with F_G have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/G\<^esub> P (Call p) Q,A"
2875    by (auto intro: validt_augment_Faults)
2876  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
2877  assume P: "s \<in> P"
2878  with P_P' have P': "s \<in> P'"
2879    by auto
2880  assume t_noFault: "t \<notin> Fault ` F"
2881  show "t \<in> Normal ` (Q \<inter> R) \<union> Abrupt ` (A \<inter> X)"
2882  proof -
2883    from cvalidt_postD [OF validF [rule_format] ctxt exec P t_noFault]
2884    have t: "t \<in> Normal ` Q \<union> Abrupt ` A".
2885    then have "t \<notin> Fault ` G"
2886      by auto
2887    from cvalidt_postD [OF validG [rule_format] ctxt' exec P' this]
2888    have "t \<in> Normal ` R \<union> Abrupt ` X" .
2889    with t show ?thesis by auto
2890  qed
2891next
2892  fix s
2893  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2894  assume P: "s \<in> P"
2895  from validF ctxt P
2896  show "\<Gamma>\<turnstile>c \<down> Normal s"
2897    by (rule cvalidt_termD)
2898qed
2899
2900
2901
2902lemma Merge_PostConj:
2903  assumes validF: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
2904  assumes validG: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/G\<^esub> P' c R,X"
2905  assumes F_G: "F \<subseteq> G"
2906  assumes P_P': "P \<subseteq> P'"
2907  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> X)"
2908apply (rule hoaret_complete')
2909apply (rule Merge_PostConj_sound [OF _ _ F_G P_P'])
2910using validF apply (blast intro:hoaret_sound)
2911using validG apply (blast intro:hoaret_sound)
2912done
2913
2914
2915subsubsection \<open>Guards and Guarantees\<close>
2916
2917lemma SplitGuards_sound:
2918  assumes valid_c1: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c\<^sub>1 Q,A"
2919  assumes valid_c2: "\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c\<^sub>2 UNIV,UNIV"
2920  assumes c: "(c\<^sub>1 \<inter>\<^sub>g c\<^sub>2) = Some c"
2921  shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
2922proof (rule cvalidtI)
2923  fix s t
2924  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2925  hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A"
2926    by (auto simp add: validt_def)
2927  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
2928  assume P: "s \<in> P"
2929  assume t_notin_F: "t \<notin> Fault ` F"
2930  show "t \<in> Normal ` Q \<union> Abrupt ` A"
2931  proof (cases t)
2932    case Normal
2933    with inter_guards_exec_noFault [OF c exec]
2934    have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t" by simp
2935    from valid_c1 ctxt this P t_notin_F
2936    show ?thesis
2937      by (rule cvalidt_postD)
2938  next
2939    case Abrupt
2940    with inter_guards_exec_noFault [OF c exec]
2941    have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t" by simp
2942    from valid_c1 ctxt this P t_notin_F
2943    show ?thesis
2944      by (rule cvalidt_postD)
2945  next
2946    case (Fault f)
2947    assume t: "t=Fault f"
2948    with exec inter_guards_exec_Fault [OF c]
2949    have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault f \<or> \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault f"
2950      by auto
2951    then show ?thesis
2952    proof (cases rule: disjE [consumes 1])
2953      assume "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault f"
2954      from cvalidt_postD [OF valid_c1 ctxt this P] t t_notin_F
2955      show ?thesis
2956        by blast
2957    next
2958      assume "\<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault f"
2959      from cvalidD [OF valid_c2 ctxt' this P] t t_notin_F
2960      show ?thesis
2961        by blast
2962    qed
2963  next
2964    case Stuck
2965    with inter_guards_exec_noFault [OF c exec]
2966    have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t" by simp
2967    from valid_c1 ctxt this P t_notin_F
2968    show ?thesis
2969      by (rule cvalidt_postD)
2970  qed
2971next
2972  fix s
2973  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
2974  assume P: "s \<in> P"
2975  show "\<Gamma>\<turnstile>c \<down> Normal s"
2976  proof -
2977    from valid_c1 ctxt P
2978    have "\<Gamma>\<turnstile>c\<^sub>1 \<down> Normal s"
2979      by (rule cvalidt_termD)
2980    with c show ?thesis
2981      by (rule inter_guards_terminates)
2982  qed
2983qed
2984
2985lemma SplitGuards:
2986  assumes c: "(c\<^sub>1 \<inter>\<^sub>g c\<^sub>2) = Some c"
2987  assumes deriv_c1: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c\<^sub>1 Q,A"
2988  assumes deriv_c2: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>2 UNIV,UNIV"
2989  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
2990apply (rule hoaret_complete')
2991apply (rule SplitGuards_sound [OF _ _ c])
2992apply (rule hoaret_sound [OF deriv_c1])
2993apply (rule hoare_sound [OF deriv_c2])
2994done
2995
2996lemma CombineStrip_sound:
2997  assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
2998  assumes valid_strip: "\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/{}\<^esub> P (strip_guards (-F) c) UNIV,UNIV"
2999  shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A"
3000proof (rule cvalidtI)
3001  fix s t
3002  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A"
3003  hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^bsub>/{}\<^esub> P (Call p) Q,A"
3004    by (auto simp add: validt_def)
3005  from ctxt have ctxt'': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
3006    by (auto intro: valid_augment_Faults simp add: validt_def)
3007  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
3008  assume P: "s \<in> P"
3009  assume t_noFault: "t \<notin> Fault ` {}"
3010  show "t \<in> Normal ` Q \<union> Abrupt ` A"
3011  proof (cases t)
3012    case (Normal t')
3013    from cvalidt_postD [OF valid ctxt'' exec P] Normal
3014    show ?thesis
3015      by auto
3016  next
3017    case (Abrupt t')
3018    from cvalidt_postD [OF valid ctxt'' exec P] Abrupt
3019    show ?thesis
3020      by auto
3021  next
3022    case (Fault f)
3023    show ?thesis
3024    proof (cases "f \<in> F")
3025      case True
3026      hence "f \<notin> -F" by simp
3027      with exec Fault
3028      have "\<Gamma>\<turnstile>\<langle>strip_guards (-F) c,Normal s\<rangle> \<Rightarrow> Fault f"
3029        by (auto intro: exec_to_exec_strip_guards_Fault)
3030      from cvalidD [OF valid_strip ctxt' this P] Fault
3031      have False
3032        by auto
3033      thus ?thesis ..
3034    next
3035      case False
3036      with cvalidt_postD [OF valid ctxt'' exec P] Fault
3037      show ?thesis
3038        by auto
3039    qed
3040  next
3041    case Stuck
3042    from cvalidt_postD [OF valid ctxt'' exec P] Stuck
3043    show ?thesis
3044      by auto
3045  qed
3046next
3047  fix s
3048  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A"
3049  hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
3050    by (auto intro: valid_augment_Faults simp add: validt_def)
3051  assume P: "s \<in> P"
3052  show "\<Gamma>\<turnstile>c \<down> Normal s"
3053  proof -
3054    from valid ctxt' P
3055    show "\<Gamma>\<turnstile>c \<down> Normal s"
3056      by (rule cvalidt_termD)
3057  qed
3058qed
3059
3060lemma CombineStrip:
3061  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3062  assumes deriv_strip: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P (strip_guards (-F) c) UNIV,UNIV"
3063  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A"
3064apply (rule hoaret_complete')
3065apply (rule CombineStrip_sound)
3066apply  (iprover intro: hoaret_sound [OF deriv])
3067apply (iprover intro: hoare_sound [OF deriv_strip])
3068done
3069
3070lemma GuardsFlip_sound:
3071  assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3072  assumes validFlip: "\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/-F\<^esub> P c UNIV,UNIV"
3073  shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A"
3074proof (rule cvalidtI)
3075  fix s t
3076  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A"
3077  from ctxt have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
3078    by (auto intro: valid_augment_Faults simp add: validt_def)
3079  from ctxt have ctxtFlip: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^bsub>/-F\<^esub> P (Call p) Q,A"
3080    by (auto intro: valid_augment_Faults simp add: validt_def)
3081  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
3082  assume P: "s \<in> P"
3083  assume t_noFault: "t \<notin> Fault ` {}"
3084  show "t \<in> Normal ` Q \<union> Abrupt ` A"
3085  proof (cases t)
3086    case (Normal t')
3087    from cvalidt_postD [OF valid ctxt' exec P] Normal
3088    show ?thesis
3089      by auto
3090  next
3091    case (Abrupt t')
3092    from cvalidt_postD [OF valid ctxt' exec P] Abrupt
3093    show ?thesis
3094      by auto
3095  next
3096    case (Fault f)
3097    show ?thesis
3098    proof (cases "f \<in> F")
3099      case True
3100      hence "f \<notin> -F" by simp
3101      with cvalidD [OF validFlip ctxtFlip exec P] Fault
3102      have False
3103        by auto
3104      thus ?thesis ..
3105    next
3106      case False
3107      with cvalidt_postD [OF valid ctxt' exec P] Fault
3108      show ?thesis
3109        by auto
3110    qed
3111  next
3112    case Stuck
3113    from cvalidt_postD [OF valid ctxt' exec P] Stuck
3114    show ?thesis
3115      by auto
3116  qed
3117next
3118  fix s
3119  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A"
3120  hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
3121    by (auto intro: valid_augment_Faults simp add: validt_def)
3122  assume P: "s \<in> P"
3123  show "\<Gamma>\<turnstile>c \<down> Normal s"
3124  proof -
3125    from valid ctxt' P
3126    show "\<Gamma>\<turnstile>c \<down> Normal s"
3127      by (rule cvalidt_termD)
3128  qed
3129qed
3130
3131
3132lemma GuardsFlip:
3133  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3134  assumes derivFlip: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/-F\<^esub> P c UNIV,UNIV"
3135  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A"
3136apply (rule hoaret_complete')
3137apply (rule GuardsFlip_sound)
3138apply  (iprover intro: hoaret_sound [OF deriv])
3139apply (iprover intro: hoare_sound [OF derivFlip])
3140done
3141
3142lemma MarkGuardsI_sound:
3143  assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A"
3144  shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P mark_guards f c Q,A"
3145proof (rule cvalidtI)
3146  fix s t
3147  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A"
3148  assume exec: "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s\<rangle> \<Rightarrow> t"
3149  from exec_mark_guards_to_exec [OF exec] obtain t' where
3150    exec_c: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t'" and
3151    t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t"
3152    by blast
3153  assume P: "s \<in> P"
3154  assume t_noFault: "t \<notin> Fault ` {}"
3155  show "t \<in> Normal ` Q \<union> Abrupt ` A"
3156  proof -
3157    from cvalidt_postD [OF valid [rule_format] ctxt exec_c P]
3158    have "t' \<in> Normal ` Q \<union> Abrupt ` A"
3159      by blast
3160    with t'_noFault
3161    show ?thesis
3162      by auto
3163  qed
3164next
3165  fix s
3166  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A"
3167  assume P: "s \<in> P"
3168  from cvalidt_termD [OF valid ctxt P]
3169  have "\<Gamma>\<turnstile>c \<down> Normal s".
3170  thus "\<Gamma>\<turnstile>mark_guards f c \<down> Normal s"
3171    by (rule terminates_to_terminates_mark_guards)
3172qed
3173
3174lemma MarkGuardsI:
3175  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A"
3176  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P mark_guards f c Q,A"
3177apply (rule hoaret_complete')
3178apply (rule MarkGuardsI_sound)
3179apply (iprover intro: hoaret_sound [OF deriv])
3180done
3181
3182
3183lemma MarkGuardsD_sound:
3184  assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P mark_guards f c Q,A"
3185  shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A"
3186proof (rule cvalidtI)
3187  fix s t
3188  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A"
3189  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
3190  assume P: "s \<in> P"
3191  assume t_noFault: "t \<notin> Fault ` {}"
3192  show "t \<in> Normal ` Q \<union> Abrupt ` A"
3193  proof (cases "isFault t")
3194    case True
3195    with exec_to_exec_mark_guards_Fault exec
3196    obtain f' where "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s\<rangle> \<Rightarrow> Fault f'"
3197      by (fastforce elim: isFaultE)
3198    from cvalidt_postD [OF valid [rule_format] ctxt this P]
3199    have False
3200      by auto
3201    thus ?thesis ..
3202  next
3203    case False
3204    from exec_to_exec_mark_guards [OF exec False]
3205    obtain f' where "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s\<rangle> \<Rightarrow> t"
3206      by auto
3207    from cvalidt_postD [OF valid [rule_format] ctxt this P]
3208    show ?thesis
3209      by auto
3210  qed
3211next
3212  fix s
3213  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A"
3214  assume P: "s \<in> P"
3215  from cvalidt_termD [OF valid ctxt P]
3216  have "\<Gamma>\<turnstile>mark_guards f c \<down> Normal s".
3217  thus "\<Gamma>\<turnstile>c \<down> Normal s"
3218    by (rule terminates_mark_guards_to_terminates)
3219qed
3220
3221lemma MarkGuardsD:
3222  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P mark_guards f c Q,A"
3223  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A"
3224apply (rule hoaret_complete')
3225apply (rule MarkGuardsD_sound)
3226apply (iprover intro: hoaret_sound [OF deriv])
3227done
3228
3229lemma MergeGuardsI_sound:
3230  assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3231  shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P merge_guards c Q,A"
3232proof (rule cvalidtI)
3233  fix s t
3234  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
3235  assume exec_merge: "\<Gamma>\<turnstile>\<langle>merge_guards c,Normal s\<rangle> \<Rightarrow> t"
3236  from exec_merge_guards_to_exec [OF exec_merge]
3237  have exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" .
3238  assume P: "s \<in> P"
3239  assume t_notin_F: "t \<notin> Fault ` F"
3240  from cvalidt_postD [OF valid [rule_format] ctxt exec P t_notin_F]
3241  show "t \<in> Normal ` Q \<union> Abrupt ` A".
3242next
3243  fix s
3244  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
3245  assume P: "s \<in> P"
3246  from cvalidt_termD [OF valid ctxt P]
3247  have "\<Gamma>\<turnstile>c \<down> Normal s".
3248  thus "\<Gamma>\<turnstile>merge_guards c \<down> Normal s"
3249    by (rule terminates_to_terminates_merge_guards)
3250qed
3251
3252lemma MergeGuardsI:
3253  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3254  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P merge_guards c Q,A"
3255apply (rule hoaret_complete')
3256apply (rule MergeGuardsI_sound)
3257apply (iprover intro: hoaret_sound [OF deriv])
3258done
3259
3260lemma MergeGuardsD_sound:
3261  assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P merge_guards c Q,A"
3262  shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3263proof (rule cvalidtI)
3264  fix s t
3265  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
3266  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
3267  from exec_to_exec_merge_guards [OF exec]
3268  have exec_merge: "\<Gamma>\<turnstile>\<langle>merge_guards c,Normal s\<rangle> \<Rightarrow> t".
3269  assume P: "s \<in> P"
3270  assume t_notin_F: "t \<notin> Fault ` F"
3271  from cvalidt_postD [OF valid [rule_format] ctxt exec_merge P t_notin_F]
3272  show "t \<in> Normal ` Q \<union> Abrupt ` A".
3273next
3274  fix s
3275  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
3276  assume P: "s \<in> P"
3277  from cvalidt_termD [OF valid ctxt P]
3278  have "\<Gamma>\<turnstile>merge_guards c \<down> Normal s".
3279  thus "\<Gamma>\<turnstile>c \<down> Normal s"
3280    by (rule terminates_merge_guards_to_terminates)
3281qed
3282
3283lemma MergeGuardsD:
3284  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P merge_guards c Q,A"
3285  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3286apply (rule hoaret_complete')
3287apply (rule MergeGuardsD_sound)
3288apply (iprover intro: hoaret_sound [OF deriv])
3289done
3290
3291
3292lemma SubsetGuards_sound:
3293  assumes c_c': "c \<subseteq>\<^sub>g c'"
3294  assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c' Q,A"
3295  shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A"
3296proof (rule cvalidtI)
3297  fix s t
3298  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A"
3299  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
3300  from exec_to_exec_subseteq_guards [OF c_c' exec] obtain t' where
3301    exec_c': "\<Gamma>\<turnstile>\<langle>c',Normal s\<rangle> \<Rightarrow> t'" and
3302    t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t"
3303    by blast
3304  assume P: "s \<in> P"
3305  assume t_noFault: "t \<notin> Fault ` {}"
3306  from cvalidt_postD [OF valid [rule_format] ctxt exec_c' P] t'_noFault t_noFault
3307  show "t \<in> Normal ` Q \<union> Abrupt ` A"
3308    by auto
3309next
3310  fix s
3311  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A"
3312  assume P: "s \<in> P"
3313  from cvalidt_termD [OF valid ctxt P]
3314  have termi_c': "\<Gamma>\<turnstile>c' \<down> Normal s".
3315  from cvalidt_postD [OF valid ctxt _ P]
3316  have noFault_c': "\<Gamma>\<turnstile>\<langle>c',Normal s\<rangle> \<Rightarrow>\<notin>Fault ` UNIV"
3317    by (auto simp add: final_notin_def)
3318  from termi_c' c_c' noFault_c'
3319  show "\<Gamma>\<turnstile>c \<down> Normal s"
3320    by (rule terminates_fewer_guards)
3321qed
3322
3323lemma SubsetGuards:
3324  assumes c_c': "c \<subseteq>\<^sub>g c'"
3325  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c' Q,A"
3326  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A"
3327apply (rule hoaret_complete')
3328apply (rule SubsetGuards_sound [OF c_c'])
3329apply (iprover intro: hoaret_sound [OF deriv])
3330done
3331
3332lemma NormalizeD_sound:
3333  assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (normalize c) Q,A"
3334  shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3335proof (rule cvalidtI)
3336  fix s t
3337  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
3338  assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
3339  hence exec_norm: "\<Gamma>\<turnstile>\<langle>normalize c,Normal s\<rangle> \<Rightarrow> t"
3340    by (rule exec_to_exec_normalize)
3341  assume P: "s \<in> P"
3342  assume noFault: "t \<notin> Fault ` F"
3343  from cvalidt_postD [OF valid [rule_format] ctxt exec_norm P noFault]
3344  show "t \<in> Normal ` Q \<union> Abrupt ` A".
3345next
3346  fix s
3347  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
3348  assume P: "s \<in> P"
3349  from cvalidt_termD [OF valid ctxt P]
3350  have "\<Gamma>\<turnstile>normalize c \<down> Normal s".
3351  thus "\<Gamma>\<turnstile>c \<down> Normal s"
3352    by (rule terminates_normalize_to_terminates)
3353qed
3354
3355lemma NormalizeD:
3356  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (normalize c) Q,A"
3357  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3358apply (rule hoaret_complete')
3359apply (rule NormalizeD_sound)
3360apply (iprover intro: hoaret_sound [OF deriv])
3361done
3362
3363lemma NormalizeI_sound:
3364  assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3365  shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (normalize c) Q,A"
3366proof (rule cvalidtI)
3367  fix s t
3368  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
3369  assume "\<Gamma>\<turnstile>\<langle>normalize c,Normal s\<rangle> \<Rightarrow> t"
3370  hence exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
3371    by (rule exec_normalize_to_exec)
3372  assume P: "s \<in> P"
3373  assume noFault: "t \<notin> Fault ` F"
3374  from cvalidt_postD [OF valid [rule_format] ctxt exec P noFault]
3375  show "t \<in> Normal ` Q \<union> Abrupt ` A".
3376next
3377  fix s
3378  assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
3379  assume P: "s \<in> P"
3380  from cvalidt_termD [OF valid ctxt P]
3381  have "\<Gamma>\<turnstile> c \<down> Normal s".
3382  thus "\<Gamma>\<turnstile>normalize c \<down> Normal s"
3383    by (rule terminates_to_terminates_normalize)
3384qed
3385
3386lemma NormalizeI:
3387  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3388  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (normalize c) Q,A"
3389apply (rule hoaret_complete')
3390apply (rule NormalizeI_sound)
3391apply (iprover intro: hoaret_sound [OF deriv])
3392done
3393
3394subsubsection \<open>Restricting the Procedure Environment\<close>
3395
3396lemma validt_restrict_to_validt:
3397assumes validt_c: "\<Gamma>|\<^bsub>M\<^esub>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3398shows "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3399proof -
3400  from validt_c
3401  have valid_c: "\<Gamma>|\<^bsub>M\<^esub>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" by (simp add: validt_def)
3402  hence "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" by (rule valid_restrict_to_valid)
3403  moreover
3404  {
3405    fix s
3406    assume P: "s \<in> P"
3407    have "\<Gamma>\<turnstile>c\<down>Normal s"
3408    proof -
3409      from P validt_c have "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>c\<down>Normal s"
3410        by (auto simp add: validt_def)
3411      moreover
3412      from P valid_c
3413      have "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck}"
3414        by (auto simp add: valid_def  final_notin_def)
3415      ultimately show ?thesis
3416        by (rule terminates_restrict_to_terminates)
3417    qed
3418   }
3419   ultimately show ?thesis
3420     by (auto simp add: validt_def)
3421qed
3422
3423
3424lemma augment_procs:
3425assumes deriv_c: "\<Gamma>|\<^bsub>M\<^esub>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3426shows "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3427  apply (rule hoaret_complete)
3428  apply (rule validt_restrict_to_validt)
3429  apply (insert hoaret_sound [OF deriv_c])
3430  by (simp add: cvalidt_def)
3431
3432subsubsection \<open>Miscellaneous\<close>
3433
3434lemma augment_Faults:
3435assumes deriv_c: "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3436assumes F: "F \<subseteq> F'"
3437shows "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F'\<^esub> P c Q,A"
3438  apply (rule hoaret_complete)
3439  apply (rule validt_augment_Faults [OF _ F])
3440  apply (insert hoaret_sound [OF deriv_c])
3441  by (simp add: cvalidt_def)
3442
3443lemma TerminationPartial_sound:
3444  assumes "termination": "\<forall>s \<in> P. \<Gamma>\<turnstile>c\<down>Normal s"
3445  assumes partial_corr: "\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A"
3446  shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3447using "termination" partial_corr
3448by (auto simp add: cvalidt_def validt_def cvalid_def)
3449
3450lemma TerminationPartial:
3451  assumes partial_deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
3452  assumes "termination": "\<forall>s \<in> P. \<Gamma>\<turnstile>c\<down>Normal s"
3453  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3454  apply (rule hoaret_complete')
3455  apply (rule TerminationPartial_sound [OF "termination"])
3456  apply (rule hoare_sound [OF partial_deriv])
3457  done
3458
3459lemma TerminationPartialStrip:
3460  assumes partial_deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
3461  assumes "termination": "\<forall>s \<in> P. strip F' \<Gamma>\<turnstile>strip_guards F' c\<down>Normal s"
3462  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3463proof -
3464  from "termination" have "\<forall>s \<in> P. \<Gamma>\<turnstile>c\<down>Normal s"
3465    by (auto intro: terminates_strip_guards_to_terminates
3466      terminates_strip_to_terminates)
3467  with partial_deriv
3468  show ?thesis
3469    by (rule TerminationPartial)
3470qed
3471
3472lemma SplitTotalPartial:
3473  assumes termi: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q',A'"
3474  assumes part: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
3475  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3476proof -
3477  from hoaret_sound [OF termi] hoare_sound [OF part]
3478  have "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3479    by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def)
3480  thus ?thesis
3481    by (rule hoaret_complete')
3482qed
3483
3484lemma SplitTotalPartial':
3485  assumes termi: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/UNIV\<^esub> P c Q',A'"
3486  assumes part: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
3487  shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3488proof -
3489  from hoaret_sound [OF termi] hoare_sound [OF part]
3490  have "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
3491    by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def)
3492  thus ?thesis
3493    by (rule hoaret_complete')
3494qed
3495
3496end
3497