1(*
2    Author:      Norbert Schirmer
3    Maintainer:  Norbert Schirmer, norbert.schirmer at web de
4    License:     LGPL
5*)
6
7(*  Title:      Termination.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*)
28section \<open>Terminating Programs\<close>
29
30theory Termination imports Semantic begin
31
32subsection \<open>Inductive Characterisation: \<open>\<Gamma>\<turnstile>c\<down>s\<close>\<close>
33
34inductive "terminates"::"('s,'p,'f) body \<Rightarrow> ('s,'p,'f) com \<Rightarrow> ('s,'f) xstate \<Rightarrow> bool"
35  ("_\<turnstile>_ \<down> _" [60,20,60] 89)
36  for  \<Gamma>::"('s,'p,'f) body"
37where
38  Skip: "\<Gamma>\<turnstile>Skip \<down>(Normal s)"
39
40| Basic: "\<Gamma>\<turnstile>Basic f \<down>(Normal s)"
41
42| Spec: "\<Gamma>\<turnstile>Spec r \<down>(Normal s)"
43
44| Guard: "\<lbrakk>s\<in>g; \<Gamma>\<turnstile>c\<down>(Normal s)\<rbrakk>
45          \<Longrightarrow>
46          \<Gamma>\<turnstile>Guard f g c\<down>(Normal s)"
47
48| GuardFault: "s\<notin>g
49               \<Longrightarrow>
50               \<Gamma>\<turnstile>Guard f g c\<down>(Normal s)"
51
52
53| Fault [intro,simp]: "\<Gamma>\<turnstile>c\<down>Fault f"
54
55
56| Seq: "\<lbrakk>\<Gamma>\<turnstile>c\<^sub>1\<down>Normal s; \<forall>s'. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>c\<^sub>2\<down>s'\<rbrakk>
57        \<Longrightarrow>
58        \<Gamma>\<turnstile>Seq c\<^sub>1 c\<^sub>2\<down>(Normal s)"
59
60| CondTrue: "\<lbrakk>s \<in> b; \<Gamma>\<turnstile>c\<^sub>1\<down>(Normal s)\<rbrakk>
61             \<Longrightarrow>
62             \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2\<down>(Normal s)"
63
64
65| CondFalse: "\<lbrakk>s \<notin> b; \<Gamma>\<turnstile>c\<^sub>2\<down>(Normal s)\<rbrakk>
66             \<Longrightarrow>
67             \<Gamma>\<turnstile>Cond b c\<^sub>1 c\<^sub>2\<down>(Normal s)"
68
69
70| WhileTrue: "\<lbrakk>s \<in> b; \<Gamma>\<turnstile>c\<down>(Normal s);
71               \<forall>s'. \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>While b c\<down>s'\<rbrakk>
72              \<Longrightarrow>
73              \<Gamma>\<turnstile>While b c\<down>(Normal s)"
74
75| WhileFalse: "\<lbrakk>s \<notin> b\<rbrakk>
76               \<Longrightarrow>
77               \<Gamma>\<turnstile>While b c\<down>(Normal s)"
78
79| Call:  "\<lbrakk>\<Gamma> p=Some bdy;\<Gamma>\<turnstile>bdy\<down>(Normal s)\<rbrakk>
80          \<Longrightarrow>
81          \<Gamma>\<turnstile>Call p\<down>(Normal s)"
82
83| CallUndefined:  "\<lbrakk>\<Gamma> p = None\<rbrakk>
84                   \<Longrightarrow>
85                   \<Gamma>\<turnstile>Call p\<down>(Normal s)"
86
87| Stuck [intro,simp]: "\<Gamma>\<turnstile>c\<down>Stuck"
88
89| DynCom:  "\<lbrakk>\<Gamma>\<turnstile>(c s)\<down>(Normal s)\<rbrakk>
90             \<Longrightarrow>
91             \<Gamma>\<turnstile>DynCom c\<down>(Normal s)"
92
93| Throw: "\<Gamma>\<turnstile>Throw\<down>(Normal s)"
94
95| Abrupt [intro,simp]: "\<Gamma>\<turnstile>c\<down>Abrupt s"
96
97| Catch: "\<lbrakk>\<Gamma>\<turnstile>c\<^sub>1\<down>Normal s;
98           \<forall>s'. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s \<rangle> \<Rightarrow> Abrupt s' \<longrightarrow> \<Gamma>\<turnstile>c\<^sub>2\<down>Normal s'\<rbrakk>
99          \<Longrightarrow>
100          \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2\<down>Normal s"
101
102
103inductive_cases terminates_elim_cases [cases set]:
104  "\<Gamma>\<turnstile>Skip \<down> s"
105  "\<Gamma>\<turnstile>Guard f g c \<down> s"
106  "\<Gamma>\<turnstile>Basic f \<down> s"
107  "\<Gamma>\<turnstile>Spec r \<down> s"
108  "\<Gamma>\<turnstile>Seq c1 c2 \<down> s"
109  "\<Gamma>\<turnstile>Cond b c1 c2 \<down> s"
110  "\<Gamma>\<turnstile>While b c \<down> s"
111  "\<Gamma>\<turnstile>Call p \<down> s"
112  "\<Gamma>\<turnstile>DynCom c \<down> s"
113  "\<Gamma>\<turnstile>Throw \<down> s"
114  "\<Gamma>\<turnstile>Catch c1 c2 \<down> s"
115
116inductive_cases terminates_Normal_elim_cases [cases set]:
117  "\<Gamma>\<turnstile>Skip \<down> Normal s"
118  "\<Gamma>\<turnstile>Guard f g c \<down> Normal s"
119  "\<Gamma>\<turnstile>Basic f \<down> Normal s"
120  "\<Gamma>\<turnstile>Spec r \<down> Normal s"
121  "\<Gamma>\<turnstile>Seq c1 c2 \<down> Normal s"
122  "\<Gamma>\<turnstile>Cond b c1 c2 \<down> Normal s"
123  "\<Gamma>\<turnstile>While b c \<down> Normal s"
124  "\<Gamma>\<turnstile>Call p \<down> Normal s"
125  "\<Gamma>\<turnstile>DynCom c \<down> Normal s"
126  "\<Gamma>\<turnstile>Throw \<down> Normal s"
127  "\<Gamma>\<turnstile>Catch c1 c2 \<down> Normal s"
128
129lemma terminates_Skip': "\<Gamma>\<turnstile>Skip \<down> s"
130  by (cases s) (auto intro: terminates.intros)
131
132lemma terminates_Call_body:
133 "\<Gamma> p=Some bdy\<Longrightarrow>\<Gamma>\<turnstile>Call  p \<down>s = \<Gamma>\<turnstile>(the (\<Gamma> p))\<down>s"
134  by (cases s)
135     (auto elim: terminates_Normal_elim_cases intro: terminates.intros)
136
137lemma terminates_Normal_Call_body:
138 "p \<in> dom \<Gamma> \<Longrightarrow>
139  \<Gamma>\<turnstile>Call p \<down>Normal s = \<Gamma>\<turnstile>(the (\<Gamma> p))\<down>Normal s"
140  by (auto elim: terminates_Normal_elim_cases intro: terminates.intros)
141
142lemma terminates_implies_exec:
143  assumes terminates: "\<Gamma>\<turnstile>c\<down>s"
144  shows "\<exists>t. \<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t"
145using terminates
146proof (induct)
147  case Skip thus ?case by (iprover intro: exec.intros)
148next
149  case Basic thus ?case by (iprover intro: exec.intros)
150next
151  case (Spec r s) thus ?case
152    by (cases "\<exists>t. (s,t)\<in> r") (auto intro: exec.intros)
153next
154  case Guard thus ?case by (iprover intro: exec.intros)
155next
156  case GuardFault thus ?case by (iprover intro: exec.intros)
157next
158  case Fault thus ?case by (iprover intro: exec.intros)
159next
160  case Seq thus ?case by (iprover intro: exec_Seq')
161next
162  case CondTrue thus ?case by (iprover intro: exec.intros)
163next
164  case CondFalse thus ?case by (iprover intro: exec.intros)
165next
166  case WhileTrue thus ?case by (iprover intro: exec.intros)
167next
168  case WhileFalse thus ?case by (iprover intro: exec.intros)
169next
170  case (Call p bdy s)
171  then obtain s' where
172    "\<Gamma>\<turnstile>\<langle>bdy,Normal s \<rangle> \<Rightarrow> s'"
173    by iprover
174  moreover have "\<Gamma> p = Some bdy" by fact
175  ultimately show ?case
176    by (cases s') (iprover intro: exec.intros)+
177next
178  case CallUndefined thus ?case by (iprover intro: exec.intros)
179next
180  case Stuck thus ?case by (iprover intro: exec.intros)
181next
182  case DynCom thus ?case by (iprover intro: exec.intros)
183next
184  case Throw thus ?case by (iprover intro: exec.intros)
185next
186  case Abrupt thus ?case by (iprover intro: exec.intros)
187next
188  case (Catch c1 s c2)
189  then obtain s' where exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'"
190    by iprover
191  thus ?case
192  proof (cases s')
193    case (Normal s'')
194    with exec_c1 show ?thesis by (auto intro!: exec.intros)
195  next
196    case (Abrupt s'')
197    with exec_c1 Catch.hyps
198    obtain t where "\<Gamma>\<turnstile>\<langle>c2,Normal s'' \<rangle> \<Rightarrow> t"
199      by auto
200    with exec_c1 Abrupt show ?thesis by (auto intro: exec.intros)
201  next
202    case Fault
203    with exec_c1 show ?thesis by (auto intro!: exec.CatchMiss)
204  next
205    case Stuck
206    with exec_c1 show ?thesis by (auto intro!: exec.CatchMiss)
207  qed
208qed
209
210lemma terminates_block:
211"\<lbrakk>\<Gamma>\<turnstile>bdy \<down> Normal (init s);
212  \<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)\<rbrakk>
213 \<Longrightarrow> \<Gamma>\<turnstile>block init bdy return c \<down> Normal s"
214apply (unfold block_def)
215apply (fastforce intro: terminates.intros elim!: exec_Normal_elim_cases
216        dest!: not_isAbrD)
217done
218
219lemma terminates_block_elim [cases set, consumes 1]:
220assumes termi: "\<Gamma>\<turnstile>block init bdy return c \<down> Normal s"
221assumes e: "\<lbrakk>\<Gamma>\<turnstile>bdy \<down> Normal (init s);
222          \<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)
223         \<rbrakk> \<Longrightarrow> P"
224shows P
225proof -
226  have "\<Gamma>\<turnstile>\<langle>Basic init,Normal s\<rangle> \<Rightarrow> Normal (init s)"
227    by (auto intro: exec.intros)
228  with termi
229  have "\<Gamma>\<turnstile>bdy \<down> Normal (init s)"
230    apply (unfold block_def)
231    apply (elim terminates_Normal_elim_cases)
232    by simp
233  moreover
234  {
235    fix t
236    assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t"
237    have "\<Gamma>\<turnstile>c s t \<down> Normal (return s t)"
238    proof -
239      from exec_bdy
240      have "\<Gamma>\<turnstile>\<langle>Catch (Seq (Basic init) bdy)
241                               (Seq (Basic (return s)) Throw),Normal s\<rangle> \<Rightarrow> Normal t"
242        by (fastforce intro: exec.intros)
243      with termi have "\<Gamma>\<turnstile>DynCom (\<lambda>t. Seq (Basic (return s)) (c s t)) \<down> Normal t"
244        apply (unfold block_def)
245        apply (elim terminates_Normal_elim_cases)
246        by simp
247      thus ?thesis
248        apply (elim terminates_Normal_elim_cases)
249        apply (auto intro: exec.intros)
250        done
251    qed
252  }
253  ultimately show P by (iprover intro: e)
254qed
255
256
257lemma terminates_call:
258"\<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>bdy \<down> Normal (init s);
259  \<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)\<rbrakk>
260 \<Longrightarrow> \<Gamma>\<turnstile>call init p return c \<down> Normal s"
261  apply (unfold call_def)
262  apply (rule terminates_block)
263  apply  (iprover intro: terminates.intros)
264  apply (auto elim: exec_Normal_elim_cases)
265  done
266
267lemma terminates_callUndefined:
268"\<lbrakk>\<Gamma> p = None\<rbrakk>
269 \<Longrightarrow> \<Gamma>\<turnstile>call init p return result \<down> Normal s"
270  apply (unfold call_def)
271  apply (rule terminates_block)
272  apply  (iprover intro: terminates.intros)
273  apply (auto elim: exec_Normal_elim_cases)
274  done
275
276lemma terminates_call_elim [cases set, consumes 1]:
277assumes termi: "\<Gamma>\<turnstile>call init p return c \<down> Normal s"
278assumes bdy: "\<And>bdy. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>bdy \<down> Normal (init s);
279     \<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)\<rbrakk> \<Longrightarrow> P"
280assumes undef: "\<lbrakk>\<Gamma> p = None\<rbrakk> \<Longrightarrow> P"
281shows P
282apply (cases "\<Gamma> p")
283apply  (erule undef)
284using termi
285apply (unfold call_def)
286apply (erule terminates_block_elim)
287apply (erule terminates_Normal_elim_cases)
288apply  simp
289apply  (frule (1) bdy)
290apply   (fastforce intro: exec.intros)
291apply  assumption
292apply simp
293done
294
295lemma terminates_dynCall:
296"\<lbrakk>\<Gamma>\<turnstile>call init (p s) return c \<down> Normal s\<rbrakk>
297 \<Longrightarrow> \<Gamma>\<turnstile>dynCall init p return c \<down> Normal s"
298  apply (unfold dynCall_def)
299  apply (auto intro: terminates.intros terminates_call)
300  done
301
302lemma terminates_dynCall_elim [cases set, consumes 1]:
303assumes termi: "\<Gamma>\<turnstile>dynCall init p return c \<down> Normal s"
304assumes "\<lbrakk>\<Gamma>\<turnstile>call init (p s) return c \<down> Normal s\<rbrakk> \<Longrightarrow> P"
305shows P
306using termi
307apply (unfold dynCall_def)
308apply (elim terminates_Normal_elim_cases)
309apply fact
310done
311
312
313(* ************************************************************************* *)
314subsection \<open>Lemmas about @{const "sequence"}, @{const "flatten"} and
315 @{const "normalize"}\<close>
316(* ************************************************************************ *)
317
318lemma terminates_sequence_app:
319  "\<And>s. \<lbrakk>\<Gamma>\<turnstile>sequence Seq xs \<down> Normal s;
320        \<forall>s'. \<Gamma>\<turnstile>\<langle>sequence Seq xs,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow>  \<Gamma>\<turnstile>sequence Seq ys \<down> s'\<rbrakk>
321\<Longrightarrow> \<Gamma>\<turnstile>sequence Seq (xs @ ys) \<down> Normal s"
322proof (induct xs)
323  case Nil
324  thus ?case by (auto intro: exec.intros)
325next
326  case (Cons x xs)
327  have termi_x_xs: "\<Gamma>\<turnstile>sequence Seq (x # xs) \<down> Normal s" by fact
328  have termi_ys: "\<forall>s'. \<Gamma>\<turnstile>\<langle>sequence Seq (x # xs),Normal s \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>sequence Seq ys \<down> s'" by fact
329  show ?case
330  proof (cases xs)
331    case Nil
332    with termi_x_xs termi_ys show ?thesis
333      by (cases ys) (auto intro: terminates.intros)
334  next
335    case Cons
336    from termi_x_xs Cons
337    have "\<Gamma>\<turnstile>x \<down> Normal s"
338      by (auto elim: terminates_Normal_elim_cases)
339    moreover
340    {
341      fix s'
342      assume exec_x: "\<Gamma>\<turnstile>\<langle>x,Normal s \<rangle> \<Rightarrow> s'"
343      have "\<Gamma>\<turnstile>sequence Seq (xs @ ys) \<down> s'"
344      proof -
345        from exec_x termi_x_xs Cons
346        have termi_xs: "\<Gamma>\<turnstile>sequence Seq xs \<down> s'"
347          by (auto elim: terminates_Normal_elim_cases)
348        show ?thesis
349        proof (cases s')
350          case (Normal s'')
351          with exec_x termi_ys Cons
352          have "\<forall>s'. \<Gamma>\<turnstile>\<langle>sequence Seq xs,Normal s'' \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>sequence Seq ys \<down> s'"
353            by (auto intro: exec.intros)
354          from Cons.hyps [OF termi_xs [simplified Normal] this]
355          have "\<Gamma>\<turnstile>sequence Seq (xs @ ys) \<down> Normal s''".
356          with Normal show ?thesis by simp
357        next
358          case Abrupt thus ?thesis by (auto intro: terminates.intros)
359        next
360          case Fault thus ?thesis by (auto intro: terminates.intros)
361        next
362          case Stuck thus ?thesis by (auto intro: terminates.intros)
363        qed
364      qed
365    }
366    ultimately show ?thesis
367      using Cons
368      by (auto intro: terminates.intros)
369  qed
370qed
371
372lemma terminates_sequence_appD:
373  "\<And>s. \<Gamma>\<turnstile>sequence Seq (xs @ ys) \<down> Normal s
374   \<Longrightarrow> \<Gamma>\<turnstile>sequence Seq xs \<down> Normal s \<and>
375       (\<forall>s'. \<Gamma>\<turnstile>\<langle>sequence Seq xs,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow>  \<Gamma>\<turnstile>sequence Seq ys \<down> s')"
376proof (induct xs)
377  case Nil
378  thus ?case
379    by (auto elim: terminates_Normal_elim_cases exec_Normal_elim_cases
380         intro: terminates.intros)
381next
382  case (Cons x xs)
383  have termi_x_xs_ys: "\<Gamma>\<turnstile>sequence Seq ((x # xs) @ ys) \<down> Normal s" by fact
384  show ?case
385  proof (cases xs)
386    case Nil
387    with termi_x_xs_ys show ?thesis
388      by (cases ys)
389         (auto elim: terminates_Normal_elim_cases exec_Normal_elim_cases
390           intro:  terminates_Skip')
391  next
392    case Cons
393    with termi_x_xs_ys
394    obtain termi_x: "\<Gamma>\<turnstile>x \<down> Normal s" and
395           termi_xs_ys: "\<forall>s'. \<Gamma>\<turnstile>\<langle>x,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow>  \<Gamma>\<turnstile>sequence Seq (xs@ys) \<down> s'"
396      by (auto elim: terminates_Normal_elim_cases)
397
398    have "\<Gamma>\<turnstile>Seq x (sequence Seq xs) \<down> Normal s"
399    proof (rule terminates.Seq [rule_format])
400      show "\<Gamma>\<turnstile>x \<down> Normal s" by (rule termi_x)
401    next
402      fix s'
403      assume exec_x: "\<Gamma>\<turnstile>\<langle>x,Normal s \<rangle> \<Rightarrow> s'"
404      show "\<Gamma>\<turnstile>sequence Seq xs \<down> s'"
405      proof -
406        from termi_xs_ys [rule_format, OF exec_x]
407        have termi_xs_ys': "\<Gamma>\<turnstile>sequence Seq (xs@ys) \<down> s'" .
408        show ?thesis
409        proof (cases s')
410          case (Normal s'')
411          from Cons.hyps [OF termi_xs_ys' [simplified Normal]]
412          show ?thesis
413            using Normal by auto
414        next
415          case Abrupt thus ?thesis by (auto intro: terminates.intros)
416        next
417          case Fault thus ?thesis by (auto intro: terminates.intros)
418        next
419          case Stuck thus ?thesis by (auto intro: terminates.intros)
420        qed
421      qed
422    qed
423    moreover
424    {
425      fix s'
426      assume exec_x_xs: "\<Gamma>\<turnstile>\<langle>Seq x (sequence Seq xs),Normal s \<rangle> \<Rightarrow> s'"
427      have "\<Gamma>\<turnstile>sequence Seq ys \<down> s'"
428      proof -
429        from exec_x_xs obtain t where
430          exec_x: "\<Gamma>\<turnstile>\<langle>x,Normal s \<rangle> \<Rightarrow> t" and
431          exec_xs: "\<Gamma>\<turnstile>\<langle>sequence Seq xs,t \<rangle> \<Rightarrow> s'"
432          by cases
433        show ?thesis
434        proof (cases t)
435          case (Normal t')
436          with exec_x termi_xs_ys have "\<Gamma>\<turnstile>sequence Seq (xs@ys) \<down> Normal t'"
437            by auto
438          from Cons.hyps [OF this] exec_xs Normal
439          show ?thesis
440            by auto
441        next
442          case (Abrupt t')
443          with exec_xs have "s'=Abrupt t'"
444            by (auto dest: Abrupt_end)
445          thus ?thesis by (auto intro: terminates.intros)
446        next
447          case (Fault f)
448          with exec_xs have "s'=Fault f"
449            by (auto dest: Fault_end)
450          thus ?thesis by (auto intro: terminates.intros)
451        next
452          case Stuck
453          with exec_xs have "s'=Stuck"
454            by (auto dest: Stuck_end)
455          thus ?thesis by (auto intro: terminates.intros)
456        qed
457      qed
458    }
459    ultimately show ?thesis
460      using Cons
461      by auto
462  qed
463qed
464
465lemma terminates_sequence_appE [consumes 1]:
466  "\<lbrakk>\<Gamma>\<turnstile>sequence Seq (xs @ ys) \<down> Normal s;
467    \<lbrakk>\<Gamma>\<turnstile>sequence Seq xs \<down> Normal s;
468     \<forall>s'. \<Gamma>\<turnstile>\<langle>sequence Seq xs,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow>  \<Gamma>\<turnstile>sequence Seq ys \<down> s'\<rbrakk> \<Longrightarrow> P\<rbrakk>
469   \<Longrightarrow> P"
470  by (auto dest: terminates_sequence_appD)
471
472lemma terminates_to_terminates_sequence_flatten:
473  assumes termi: "\<Gamma>\<turnstile>c\<down>s"
474  shows "\<Gamma>\<turnstile>sequence Seq (flatten c)\<down>s"
475using termi
476by (induct)
477   (auto intro: terminates.intros terminates_sequence_app
478     exec_sequence_flatten_to_exec)
479
480lemma terminates_to_terminates_normalize:
481  assumes termi: "\<Gamma>\<turnstile>c\<down>s"
482  shows "\<Gamma>\<turnstile>normalize c\<down>s"
483using termi
484proof induct
485  case Seq
486  thus ?case
487    by (fastforce intro: terminates.intros terminates_sequence_app
488                 terminates_to_terminates_sequence_flatten
489        dest: exec_sequence_flatten_to_exec exec_normalize_to_exec)
490next
491  case WhileTrue
492  thus ?case
493    by (fastforce intro: terminates.intros terminates_sequence_app
494                 terminates_to_terminates_sequence_flatten
495        dest: exec_sequence_flatten_to_exec exec_normalize_to_exec)
496next
497  case Catch
498  thus ?case
499    by (fastforce intro: terminates.intros terminates_sequence_app
500                 terminates_to_terminates_sequence_flatten
501        dest: exec_sequence_flatten_to_exec exec_normalize_to_exec)
502qed (auto intro: terminates.intros)
503
504lemma terminates_sequence_flatten_to_terminates:
505  shows "\<And>s. \<Gamma>\<turnstile>sequence Seq (flatten c)\<down>s \<Longrightarrow> \<Gamma>\<turnstile>c\<down>s"
506proof (induct c)
507  case (Seq c1 c2)
508  have "\<Gamma>\<turnstile>sequence Seq (flatten (Seq c1 c2)) \<down> s" by fact
509  hence termi_app: "\<Gamma>\<turnstile>sequence Seq (flatten c1 @ flatten c2) \<down> s" by simp
510  show ?case
511  proof (cases s)
512    case (Normal s')
513    have "\<Gamma>\<turnstile>Seq c1 c2 \<down> Normal s'"
514    proof (rule terminates.Seq [rule_format])
515      from termi_app [simplified Normal]
516      have "\<Gamma>\<turnstile>sequence Seq (flatten c1) \<down> Normal s'"
517        by (cases rule: terminates_sequence_appE)
518      with Seq.hyps
519      show "\<Gamma>\<turnstile>c1 \<down> Normal s'"
520        by simp
521    next
522      fix s''
523      assume "\<Gamma>\<turnstile>\<langle>c1,Normal s' \<rangle> \<Rightarrow> s''"
524      from termi_app [simplified Normal] exec_to_exec_sequence_flatten [OF this]
525      have "\<Gamma>\<turnstile>sequence Seq (flatten c2) \<down> s''"
526        by (cases rule: terminates_sequence_appE) auto
527      with Seq.hyps
528      show "\<Gamma>\<turnstile>c2 \<down> s''"
529        by simp
530    qed
531    with Normal show ?thesis
532      by simp
533  qed (auto intro: terminates.intros)
534qed (auto intro: terminates.intros)
535
536lemma terminates_normalize_to_terminates:
537  shows "\<And>s. \<Gamma>\<turnstile>normalize c\<down>s \<Longrightarrow> \<Gamma>\<turnstile>c\<down>s"
538proof (induct c)
539  case Skip thus ?case by (auto intro:  terminates_Skip')
540next
541  case Basic thus ?case by (cases s) (auto intro: terminates.intros)
542next
543  case Spec thus ?case by (cases s) (auto intro: terminates.intros)
544next
545  case (Seq c1 c2)
546  have "\<Gamma>\<turnstile>normalize (Seq c1 c2) \<down> s" by fact
547  hence termi_app: "\<Gamma>\<turnstile>sequence Seq (flatten (normalize c1) @ flatten (normalize c2)) \<down> s"
548    by simp
549  show ?case
550  proof (cases s)
551    case (Normal s')
552    have "\<Gamma>\<turnstile>Seq c1 c2 \<down> Normal s'"
553    proof (rule terminates.Seq [rule_format])
554      from termi_app [simplified Normal]
555      have "\<Gamma>\<turnstile>sequence Seq (flatten (normalize c1))  \<down> Normal s'"
556        by (cases rule: terminates_sequence_appE)
557      from terminates_sequence_flatten_to_terminates [OF this] Seq.hyps
558      show "\<Gamma>\<turnstile>c1 \<down> Normal s'"
559        by simp
560    next
561      fix s''
562      assume "\<Gamma>\<turnstile>\<langle>c1,Normal s' \<rangle> \<Rightarrow> s''"
563      from exec_to_exec_normalize [OF this]
564      have "\<Gamma>\<turnstile>\<langle>normalize c1,Normal s' \<rangle> \<Rightarrow> s''" .
565      from termi_app [simplified Normal] exec_to_exec_sequence_flatten [OF this]
566      have "\<Gamma>\<turnstile>sequence Seq (flatten (normalize c2))  \<down> s''"
567        by (cases rule: terminates_sequence_appE) auto
568      from terminates_sequence_flatten_to_terminates [OF this] Seq.hyps
569      show "\<Gamma>\<turnstile>c2 \<down> s''"
570        by simp
571    qed
572    with Normal show ?thesis by simp
573  qed (auto intro: terminates.intros)
574next
575  case (Cond b c1 c2)
576  thus ?case
577    by (cases s)
578       (auto intro: terminates.intros elim!: terminates_Normal_elim_cases)
579next
580  case (While b c)
581  have "\<Gamma>\<turnstile>normalize (While b c) \<down> s" by fact
582  hence termi_norm_w: "\<Gamma>\<turnstile>While b (normalize c) \<down> s" by simp
583  {
584    fix t w
585    assume termi_w: "\<Gamma>\<turnstile> w \<down> t"
586    have "w=While b (normalize c) \<Longrightarrow> \<Gamma>\<turnstile>While b c \<down> t"
587      using termi_w
588    proof (induct)
589      case (WhileTrue t' b' c')
590      from WhileTrue obtain
591        t'_b: "t' \<in> b" and
592        termi_norm_c: "\<Gamma>\<turnstile>normalize c \<down> Normal t'" and
593        termi_norm_w': "\<forall>s'. \<Gamma>\<turnstile>\<langle>normalize c,Normal t' \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>While b c \<down> s'"
594        by auto
595      from While.hyps [OF termi_norm_c]
596      have "\<Gamma>\<turnstile>c \<down> Normal t'".
597      moreover
598      from termi_norm_w'
599      have "\<forall>s'. \<Gamma>\<turnstile>\<langle>c,Normal t' \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>While b c \<down> s'"
600        by (auto intro: exec_to_exec_normalize)
601      ultimately show ?case
602        using t'_b
603        by (auto intro: terminates.intros)
604    qed (auto intro: terminates.intros)
605  }
606  from this [OF termi_norm_w]
607  show ?case
608    by auto
609next
610  case Call thus ?case by simp
611next
612  case DynCom thus ?case
613    by (cases s) (auto intro: terminates.intros rangeI elim: terminates_Normal_elim_cases)
614next
615  case Guard thus ?case
616    by (cases s) (auto intro: terminates.intros elim: terminates_Normal_elim_cases)
617next
618  case Throw thus ?case by (cases s) (auto intro: terminates.intros)
619next
620  case Catch
621  thus ?case
622    by (cases s)
623       (auto dest: exec_to_exec_normalize elim!: terminates_Normal_elim_cases
624         intro!: terminates.Catch)
625qed
626
627lemma terminates_iff_terminates_normalize:
628"\<Gamma>\<turnstile>normalize c\<down>s = \<Gamma>\<turnstile>c\<down>s"
629  by (auto intro: terminates_to_terminates_normalize
630    terminates_normalize_to_terminates)
631
632(* ************************************************************************* *)
633subsection \<open>Lemmas about @{const "strip_guards"}\<close>
634(* ************************************************************************* *)
635
636lemma terminates_strip_guards_to_terminates: "\<And>s. \<Gamma>\<turnstile>strip_guards F c\<down>s  \<Longrightarrow> \<Gamma>\<turnstile>c\<down>s"
637proof (induct c)
638  case Skip thus ?case by simp
639next
640  case Basic thus ?case by simp
641next
642  case Spec thus ?case by simp
643next
644  case (Seq c1 c2)
645  hence "\<Gamma>\<turnstile>Seq (strip_guards F c1) (strip_guards F c2) \<down> s" by simp
646  thus "\<Gamma>\<turnstile>Seq c1 c2 \<down> s"
647  proof (cases)
648    fix f assume "s=Fault f" thus ?thesis by simp
649  next
650    assume "s=Stuck" thus ?thesis by simp
651  next
652    fix s' assume "s=Abrupt s'" thus ?thesis by simp
653  next
654    fix s'
655    assume s: "s=Normal s'"
656    assume "\<Gamma>\<turnstile>strip_guards F c1 \<down> Normal s'"
657    hence "\<Gamma>\<turnstile>c1 \<down> Normal s'"
658      by (rule Seq.hyps)
659    moreover
660    assume c2:
661      "\<forall>s''. \<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s'\<rangle> \<Rightarrow> s'' \<longrightarrow> \<Gamma>\<turnstile>strip_guards F c2\<down>s''"
662    {
663      fix s'' assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s' \<rangle> \<Rightarrow> s''"
664      have " \<Gamma>\<turnstile>c2 \<down> s''"
665      proof (cases s'')
666        case (Normal s''')
667        with exec_c1
668        have "\<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s' \<rangle> \<Rightarrow> s''"
669          by (auto intro: exec_to_exec_strip_guards)
670        with c2
671        show ?thesis
672          by (iprover intro: Seq.hyps)
673      next
674        case (Abrupt s''')
675        with exec_c1
676        have "\<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s' \<rangle> \<Rightarrow> s''"
677          by (auto intro: exec_to_exec_strip_guards )
678        with c2
679        show ?thesis
680          by (iprover intro: Seq.hyps)
681      next
682        case Fault thus ?thesis by simp
683      next
684        case Stuck thus ?thesis by simp
685      qed
686    }
687    ultimately show ?thesis
688      using s
689      by (iprover intro: terminates.intros)
690  qed
691next
692  case (Cond b c1 c2)
693  hence "\<Gamma>\<turnstile>Cond b (strip_guards F c1) (strip_guards F c2) \<down> s" by simp
694  thus "\<Gamma>\<turnstile>Cond b c1 c2 \<down> s"
695  proof (cases)
696    fix f assume "s=Fault f" thus ?thesis by simp
697  next
698    assume "s=Stuck" thus ?thesis by simp
699  next
700    fix s' assume "s=Abrupt s'" thus ?thesis by simp
701  next
702    fix s'
703    assume "s'\<in>b" "\<Gamma>\<turnstile>strip_guards F c1 \<down> Normal s'" "s = Normal s'"
704    thus ?thesis
705      by (iprover intro: terminates.intros Cond.hyps)
706  next
707    fix s'
708    assume "s'\<notin>b" "\<Gamma>\<turnstile>strip_guards F c2 \<down> Normal s'" "s = Normal s'"
709    thus ?thesis
710      by (iprover intro: terminates.intros Cond.hyps)
711  qed
712next
713  case (While b c)
714  have hyp_c: "\<And>s. \<Gamma>\<turnstile>strip_guards F c \<down> s \<Longrightarrow> \<Gamma>\<turnstile>c \<down> s" by fact
715  have "\<Gamma>\<turnstile>While b (strip_guards F c) \<down> s" using While.prems by simp
716  moreover
717  {
718    fix sw
719    assume "\<Gamma>\<turnstile>sw\<down>s"
720    then have "sw=While b (strip_guards F c) \<Longrightarrow>
721      \<Gamma>\<turnstile>While b c \<down> s"
722    proof (induct)
723      case (WhileTrue s b' c')
724      have eqs: "While b' c' = While b (strip_guards F c)" by fact
725      with \<open>s\<in>b'\<close> have b: "s\<in>b" by simp
726      from eqs \<open>\<Gamma>\<turnstile>c' \<down> Normal s\<close> have "\<Gamma>\<turnstile>strip_guards F c \<down> Normal s"
727        by simp
728      hence term_c: "\<Gamma>\<turnstile>c \<down> Normal s"
729        by (rule hyp_c)
730      moreover
731      {
732        fix t
733        assume exec_c: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> t"
734        have "\<Gamma>\<turnstile>While b c \<down> t"
735        proof (cases t)
736          case Fault
737          thus ?thesis by simp
738        next
739          case Stuck
740          thus ?thesis by simp
741        next
742          case (Abrupt t')
743          thus ?thesis by simp
744        next
745          case (Normal t')
746          with exec_c
747          have "\<Gamma>\<turnstile>\<langle>strip_guards F c,Normal s \<rangle> \<Rightarrow> Normal t'"
748            by (auto intro: exec_to_exec_strip_guards)
749          with WhileTrue.hyps eqs Normal
750          show ?thesis
751            by fastforce
752        qed
753      }
754      ultimately
755      show ?case
756        using b
757        by (auto intro: terminates.intros)
758    next
759      case WhileFalse thus ?case by (auto intro: terminates.intros)
760    qed simp_all
761  }
762  ultimately show "\<Gamma>\<turnstile>While b c \<down> s"
763    by auto
764next
765  case Call thus ?case by simp
766next
767  case DynCom thus ?case
768     by (cases s) (auto elim: terminates_Normal_elim_cases intro: terminates.intros rangeI)
769next
770  case Guard
771  thus ?case
772    by (cases s) (auto elim: terminates_Normal_elim_cases intro: terminates.intros
773                  split: if_split_asm)
774next
775  case Throw thus ?case by simp
776next
777  case (Catch c1 c2)
778  hence "\<Gamma>\<turnstile>Catch (strip_guards F c1) (strip_guards F c2) \<down> s" by simp
779  thus "\<Gamma>\<turnstile>Catch c1 c2 \<down> s"
780  proof (cases)
781    fix f assume "s=Fault f" thus ?thesis by simp
782  next
783    assume "s=Stuck" thus ?thesis by simp
784  next
785    fix s' assume "s=Abrupt s'" thus ?thesis by simp
786  next
787    fix s'
788    assume s: "s=Normal s'"
789    assume "\<Gamma>\<turnstile>strip_guards F c1 \<down> Normal s'"
790    hence "\<Gamma>\<turnstile>c1 \<down> Normal s'"
791      by (rule Catch.hyps)
792    moreover
793    assume c2:
794      "\<forall>s''. \<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s'\<rangle> \<Rightarrow> Abrupt s''
795             \<longrightarrow> \<Gamma>\<turnstile>strip_guards F c2\<down>Normal s''"
796    {
797      fix s'' assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s' \<rangle> \<Rightarrow> Abrupt s''"
798      have " \<Gamma>\<turnstile>c2 \<down> Normal s''"
799      proof -
800        from exec_c1
801        have "\<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s' \<rangle> \<Rightarrow> Abrupt s''"
802          by (auto intro: exec_to_exec_strip_guards)
803        with c2
804        show ?thesis
805          by (auto intro: Catch.hyps)
806      qed
807    }
808    ultimately show ?thesis
809      using s
810      by (iprover intro: terminates.intros)
811  qed
812qed
813
814lemma terminates_strip_to_terminates:
815  assumes termi_strip: "strip F \<Gamma>\<turnstile>c\<down>s"
816  shows "\<Gamma>\<turnstile>c\<down>s"
817using termi_strip
818proof induct
819  case (Seq c1 s c2)
820  have "\<Gamma>\<turnstile>c1 \<down> Normal s" by fact
821  moreover
822  {
823    fix s'
824    assume exec: "\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> s'"
825    have "\<Gamma>\<turnstile>c2 \<down> s'"
826    proof (cases "isFault s'")
827      case True
828      thus ?thesis
829        by (auto elim: isFaultE)
830    next
831      case False
832      from exec_to_exec_strip [OF exec this] Seq.hyps
833      show ?thesis
834        by auto
835    qed
836  }
837  ultimately show ?case
838    by (auto intro: terminates.intros)
839next
840  case (WhileTrue s b c)
841  have "\<Gamma>\<turnstile>c \<down> Normal s" by fact
842  moreover
843  {
844    fix s'
845    assume exec: "\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'"
846    have "\<Gamma>\<turnstile>While b c \<down> s'"
847    proof (cases "isFault s'")
848      case True
849      thus ?thesis
850        by (auto elim: isFaultE)
851    next
852      case False
853      from exec_to_exec_strip [OF exec this] WhileTrue.hyps
854      show ?thesis
855        by auto
856    qed
857  }
858  ultimately show ?case
859    by (auto intro: terminates.intros)
860next
861  case (Catch c1 s c2)
862  have "\<Gamma>\<turnstile>c1 \<down> Normal s" by fact
863  moreover
864  {
865    fix s'
866    assume exec: "\<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> Abrupt s'"
867    from exec_to_exec_strip [OF exec] Catch.hyps
868    have "\<Gamma>\<turnstile>c2 \<down> Normal s'"
869      by auto
870  }
871  ultimately show ?case
872    by (auto intro: terminates.intros)
873next
874  case Call thus ?case
875    by (auto intro: terminates.intros terminates_strip_guards_to_terminates)
876qed (auto intro: terminates.intros)
877
878(* ************************************************************************* *)
879subsection \<open>Lemmas about @{term "c\<^sub>1 \<inter>\<^sub>g c\<^sub>2"}\<close>
880(* ************************************************************************* *)
881
882lemma inter_guards_terminates:
883  "\<And>c c2 s. \<lbrakk>(c1 \<inter>\<^sub>g c2) = Some c; \<Gamma>\<turnstile>c1\<down>s \<rbrakk>
884        \<Longrightarrow> \<Gamma>\<turnstile>c\<down>s"
885proof (induct c1)
886  case Skip thus ?case by (fastforce simp add: inter_guards_Skip)
887next
888  case (Basic f) thus ?case by (fastforce simp add: inter_guards_Basic)
889next
890  case (Spec r) thus ?case by (fastforce simp add: inter_guards_Spec)
891next
892  case (Seq a1 a2)
893  have "(Seq a1 a2 \<inter>\<^sub>g c2) = Some c" by fact
894  then obtain b1 b2 d1 d2 where
895    c2: "c2=Seq b1 b2" and
896    d1: "(a1 \<inter>\<^sub>g b1) = Some d1" and d2: "(a2 \<inter>\<^sub>g b2) = Some d2" and
897    c: "c=Seq d1 d2"
898    by (auto simp add: inter_guards_Seq)
899  have termi_c1: "\<Gamma>\<turnstile>Seq a1 a2 \<down> s" by fact
900  have "\<Gamma>\<turnstile>Seq d1 d2 \<down> s"
901  proof (cases s)
902    case Fault thus ?thesis by simp
903  next
904    case Stuck thus ?thesis by simp
905  next
906    case Abrupt thus ?thesis by simp
907  next
908    case (Normal s')
909    note Normal_s = this
910    with d1 termi_c1
911    have "\<Gamma>\<turnstile>d1 \<down> Normal s'"
912      by (auto elim: terminates_Normal_elim_cases intro: Seq.hyps)
913    moreover
914    {
915      fix t
916      assume exec_d1: "\<Gamma>\<turnstile>\<langle>d1,Normal s' \<rangle> \<Rightarrow> t"
917      have "\<Gamma>\<turnstile>d2 \<down> t"
918      proof (cases t)
919        case Fault thus ?thesis by simp
920      next
921        case Stuck thus ?thesis by simp
922      next
923        case Abrupt thus ?thesis by simp
924      next
925        case (Normal t')
926        with inter_guards_exec_noFault [OF d1 exec_d1]
927        have "\<Gamma>\<turnstile>\<langle>a1,Normal s' \<rangle> \<Rightarrow> Normal t'"
928          by simp
929        with termi_c1 Normal_s have "\<Gamma>\<turnstile>a2 \<down> Normal t'"
930          by (auto elim: terminates_Normal_elim_cases)
931        with d2 have "\<Gamma>\<turnstile>d2 \<down> Normal t'"
932          by (auto intro: Seq.hyps)
933        with Normal show ?thesis by simp
934      qed
935    }
936    ultimately have "\<Gamma>\<turnstile>Seq d1 d2 \<down> Normal s'"
937      by (fastforce intro: terminates.intros)
938    with Normal show ?thesis by simp
939  qed
940  with c show ?case by simp
941next
942  case Cond thus ?case
943    by - (cases s,
944          auto intro: terminates.intros elim!: terminates_Normal_elim_cases
945               simp add: inter_guards_Cond)
946next
947  case (While b bdy1)
948  have "(While b bdy1 \<inter>\<^sub>g c2) = Some c" by fact
949  then obtain bdy2 bdy where
950    c2: "c2=While b bdy2" and
951    bdy: "(bdy1 \<inter>\<^sub>g bdy2) = Some bdy" and
952    c: "c=While b bdy"
953    by (auto simp add: inter_guards_While)
954  have "\<Gamma>\<turnstile>While b bdy1 \<down> s" by fact
955  moreover
956  {
957    fix s w w1 w2
958    assume termi_w:  "\<Gamma>\<turnstile>w \<down> s"
959    assume w: "w=While b bdy1"
960    from termi_w w
961    have "\<Gamma>\<turnstile>While b bdy \<down> s"
962    proof (induct)
963      case (WhileTrue s b' bdy1')
964      have eqs: "While b' bdy1' = While b bdy1" by fact
965      from WhileTrue have s_in_b: "s \<in> b" by simp
966      from WhileTrue have termi_bdy1: "\<Gamma>\<turnstile>bdy1 \<down> Normal s" by simp
967      show ?case
968      proof -
969        from bdy termi_bdy1
970        have "\<Gamma>\<turnstile>bdy\<down>(Normal s)"
971          by (rule While.hyps)
972        moreover
973        {
974          fix t
975          assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal s \<rangle> \<Rightarrow> t"
976          have "\<Gamma>\<turnstile>While b bdy\<down>t"
977          proof (cases t)
978            case Fault thus ?thesis by simp
979          next
980            case Stuck thus ?thesis by simp
981          next
982            case Abrupt thus ?thesis by simp
983          next
984            case (Normal t')
985            with inter_guards_exec_noFault [OF bdy exec_bdy]
986            have "\<Gamma>\<turnstile>\<langle>bdy1,Normal s \<rangle> \<Rightarrow> Normal t'"
987              by simp
988            with WhileTrue have "\<Gamma>\<turnstile>While b bdy \<down> Normal t'"
989              by simp
990            with Normal show ?thesis by simp
991          qed
992        }
993        ultimately show ?thesis
994          using s_in_b
995          by (blast intro: terminates.WhileTrue)
996      qed
997    next
998      case WhileFalse thus ?case
999        by (blast intro: terminates.WhileFalse)
1000    qed (simp_all)
1001  }
1002  ultimately
1003  show ?case using c by simp
1004next
1005  case Call thus ?case by (simp add: inter_guards_Call)
1006next
1007  case (DynCom f1)
1008  have "(DynCom f1 \<inter>\<^sub>g c2) = Some c" by fact
1009  then obtain f2 f where
1010    c2: "c2=DynCom f2" and
1011    f_defined: "\<forall>s. ((f1 s) \<inter>\<^sub>g (f2 s)) \<noteq> None" and
1012    c: "c=DynCom (\<lambda>s. the ((f1 s) \<inter>\<^sub>g (f2 s)))"
1013    by (auto simp add: inter_guards_DynCom)
1014  have termi: "\<Gamma>\<turnstile>DynCom f1 \<down> s" by fact
1015  show ?case
1016  proof (cases s)
1017    case Fault thus ?thesis by simp
1018  next
1019    case Stuck thus ?thesis by simp
1020  next
1021    case Abrupt thus ?thesis by simp
1022  next
1023    case (Normal s')
1024    from f_defined obtain f where f: "((f1 s') \<inter>\<^sub>g (f2 s')) = Some f"
1025      by auto
1026    from Normal termi
1027    have "\<Gamma>\<turnstile>f1 s'\<down> (Normal s')"
1028      by (auto elim: terminates_Normal_elim_cases)
1029    from DynCom.hyps f this
1030    have "\<Gamma>\<turnstile>f\<down> (Normal s')"
1031      by blast
1032    with c f Normal
1033    show ?thesis
1034      by (auto intro: terminates.intros)
1035  qed
1036next
1037  case (Guard f g1 bdy1)
1038  have "(Guard f g1 bdy1 \<inter>\<^sub>g c2) = Some c" by fact
1039  then obtain g2 bdy2 bdy where
1040    c2: "c2=Guard f g2 bdy2" and
1041    bdy: "(bdy1 \<inter>\<^sub>g bdy2) = Some bdy" and
1042    c: "c=Guard f (g1 \<inter> g2) bdy"
1043    by (auto simp add: inter_guards_Guard)
1044  have termi_c1: "\<Gamma>\<turnstile>Guard f g1 bdy1 \<down> s" by fact
1045  show ?case
1046  proof (cases s)
1047    case Fault thus ?thesis by simp
1048  next
1049    case Stuck thus ?thesis by simp
1050  next
1051    case Abrupt thus ?thesis by simp
1052  next
1053    case (Normal s')
1054    show ?thesis
1055    proof (cases "s' \<in> g1")
1056      case False
1057      with Normal c show ?thesis by (auto intro: terminates.GuardFault)
1058    next
1059      case True
1060      note s_in_g1 = this
1061      show ?thesis
1062      proof (cases "s' \<in> g2")
1063        case False
1064        with Normal c show ?thesis by (auto intro: terminates.GuardFault)
1065      next
1066        case True
1067        with termi_c1 s_in_g1 Normal have "\<Gamma>\<turnstile>bdy1 \<down> Normal s'"
1068          by (auto elim: terminates_Normal_elim_cases)
1069        with c bdy Guard.hyps Normal True s_in_g1
1070        show ?thesis by (auto intro: terminates.Guard)
1071      qed
1072    qed
1073  qed
1074next
1075  case Throw thus ?case
1076    by (auto simp add: inter_guards_Throw)
1077next
1078  case (Catch a1 a2)
1079  have "(Catch a1 a2 \<inter>\<^sub>g c2) = Some c" by fact
1080  then obtain b1 b2 d1 d2 where
1081    c2: "c2=Catch b1 b2" and
1082    d1: "(a1 \<inter>\<^sub>g b1) = Some d1" and d2: "(a2 \<inter>\<^sub>g b2) = Some d2" and
1083    c: "c=Catch d1 d2"
1084    by (auto simp add: inter_guards_Catch)
1085  have termi_c1: "\<Gamma>\<turnstile>Catch a1 a2 \<down> s" by fact
1086  have "\<Gamma>\<turnstile>Catch d1 d2 \<down> s"
1087  proof (cases s)
1088    case Fault thus ?thesis by simp
1089  next
1090    case Stuck thus ?thesis by simp
1091  next
1092    case Abrupt thus ?thesis by simp
1093  next
1094    case (Normal s')
1095    note Normal_s = this
1096    with d1 termi_c1
1097    have "\<Gamma>\<turnstile>d1 \<down> Normal s'"
1098      by (auto elim: terminates_Normal_elim_cases intro: Catch.hyps)
1099    moreover
1100    {
1101      fix t
1102      assume exec_d1: "\<Gamma>\<turnstile>\<langle>d1,Normal s' \<rangle> \<Rightarrow> Abrupt t"
1103      have "\<Gamma>\<turnstile>d2 \<down> Normal t"
1104      proof -
1105        from inter_guards_exec_noFault [OF d1 exec_d1]
1106        have "\<Gamma>\<turnstile>\<langle>a1,Normal s' \<rangle> \<Rightarrow> Abrupt t"
1107          by simp
1108        with termi_c1 Normal_s have "\<Gamma>\<turnstile>a2 \<down> Normal t"
1109          by (auto elim: terminates_Normal_elim_cases)
1110        with d2 have "\<Gamma>\<turnstile>d2 \<down> Normal t"
1111          by (auto intro: Catch.hyps)
1112        with Normal show ?thesis by simp
1113      qed
1114    }
1115    ultimately have "\<Gamma>\<turnstile>Catch d1 d2 \<down> Normal s'"
1116      by (fastforce intro: terminates.intros)
1117    with Normal show ?thesis by simp
1118  qed
1119  with c show ?case by simp
1120qed
1121
1122lemma inter_guards_terminates':
1123  assumes c: "(c1 \<inter>\<^sub>g c2) = Some c"
1124  assumes termi_c2: "\<Gamma>\<turnstile>c2\<down>s"
1125  shows "\<Gamma>\<turnstile>c\<down>s"
1126proof -
1127  from c have "(c2 \<inter>\<^sub>g c1) = Some c"
1128    by (rule inter_guards_sym)
1129  from this termi_c2 show ?thesis
1130    by (rule inter_guards_terminates)
1131qed
1132
1133(* ************************************************************************* *)
1134subsection \<open>Lemmas about @{const "mark_guards"}\<close>
1135(* ************************************************************************ *)
1136
1137lemma terminates_to_terminates_mark_guards:
1138  assumes termi: "\<Gamma>\<turnstile>c\<down>s"
1139  shows "\<Gamma>\<turnstile>mark_guards f c\<down>s"
1140using termi
1141proof (induct)
1142  case Skip thus ?case by (fastforce intro: terminates.intros)
1143next
1144  case Basic thus ?case by (fastforce intro: terminates.intros)
1145next
1146  case Spec thus ?case by (fastforce intro: terminates.intros)
1147next
1148  case Guard thus ?case by (fastforce intro: terminates.intros)
1149next
1150  case GuardFault thus ?case by (fastforce intro: terminates.intros)
1151next
1152  case Fault thus ?case by (fastforce intro: terminates.intros)
1153next
1154  case (Seq c1 s c2)
1155  have "\<Gamma>\<turnstile>mark_guards f c1 \<down> Normal s" by fact
1156  moreover
1157  {
1158    fix t
1159    assume exec_mark: "\<Gamma>\<turnstile>\<langle>mark_guards f c1,Normal s \<rangle> \<Rightarrow> t"
1160    have "\<Gamma>\<turnstile>mark_guards f c2 \<down> t"
1161    proof -
1162      from exec_mark_guards_to_exec [OF exec_mark] obtain t' where
1163        exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> t'" and
1164        t_Fault: "isFault t \<longrightarrow> isFault t'" and
1165        t'_Fault_f: "t' = Fault f \<longrightarrow> t' = t" and
1166        t'_Fault: "isFault t' \<longrightarrow> isFault t" and
1167        t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t"
1168        by blast
1169      show ?thesis
1170      proof (cases "isFault t'")
1171        case True
1172        with t'_Fault have "isFault t" by simp
1173        thus ?thesis
1174          by (auto elim: isFaultE)
1175      next
1176        case False
1177        with t'_noFault have "t'=t" by simp
1178        with exec_c1 Seq.hyps
1179        show ?thesis
1180          by auto
1181      qed
1182    qed
1183  }
1184  ultimately show ?case
1185    by (auto intro: terminates.intros)
1186next
1187  case CondTrue thus ?case by (fastforce intro: terminates.intros)
1188next
1189  case CondFalse thus ?case by (fastforce intro: terminates.intros)
1190next
1191  case (WhileTrue s b c)
1192  have s_in_b: "s \<in> b" by fact
1193  have "\<Gamma>\<turnstile>mark_guards f c \<down> Normal s" by fact
1194  moreover
1195  {
1196    fix t
1197    assume exec_mark: "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s \<rangle> \<Rightarrow> t"
1198    have "\<Gamma>\<turnstile>mark_guards f (While b c) \<down> t"
1199    proof -
1200      from exec_mark_guards_to_exec [OF exec_mark] obtain t' where
1201        exec_c1: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> t'" and
1202        t_Fault: "isFault t \<longrightarrow> isFault t'" and
1203        t'_Fault_f: "t' = Fault f \<longrightarrow> t' = t" and
1204        t'_Fault: "isFault t' \<longrightarrow> isFault t" and
1205        t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t"
1206        by blast
1207      show ?thesis
1208      proof (cases "isFault t'")
1209        case True
1210        with t'_Fault have "isFault t" by simp
1211        thus ?thesis
1212          by (auto elim: isFaultE)
1213      next
1214        case False
1215        with t'_noFault have "t'=t" by simp
1216        with exec_c1 WhileTrue.hyps
1217        show ?thesis
1218          by auto
1219      qed
1220    qed
1221  }
1222  ultimately show ?case
1223    by (auto intro: terminates.intros)
1224next
1225  case WhileFalse thus ?case by (fastforce intro: terminates.intros)
1226next
1227  case Call thus ?case by (fastforce intro: terminates.intros)
1228next
1229  case CallUndefined thus ?case by (fastforce intro: terminates.intros)
1230next
1231  case Stuck thus ?case by (fastforce intro: terminates.intros)
1232next
1233  case DynCom thus ?case by (fastforce intro: terminates.intros)
1234next
1235  case Throw thus ?case by (fastforce intro: terminates.intros)
1236next
1237  case Abrupt thus ?case by (fastforce intro: terminates.intros)
1238next
1239  case (Catch c1 s c2)
1240  have "\<Gamma>\<turnstile>mark_guards f c1 \<down> Normal s" by fact
1241  moreover
1242  {
1243    fix t
1244    assume exec_mark: "\<Gamma>\<turnstile>\<langle>mark_guards f c1,Normal s \<rangle> \<Rightarrow> Abrupt t"
1245    have "\<Gamma>\<turnstile>mark_guards f c2 \<down> Normal t"
1246    proof -
1247      from exec_mark_guards_to_exec [OF exec_mark] obtain t' where
1248        exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> t'" and
1249        t'_Fault_f: "t' = Fault f \<longrightarrow> t' = Abrupt t" and
1250        t'_Fault: "isFault t' \<longrightarrow> isFault (Abrupt t)" and
1251        t'_noFault: "\<not> isFault t' \<longrightarrow> t' = Abrupt t"
1252        by fastforce
1253      show ?thesis
1254      proof (cases "isFault t'")
1255        case True
1256        with t'_Fault have "isFault (Abrupt t)" by simp
1257        thus ?thesis by simp
1258      next
1259        case False
1260        with t'_noFault have "t'=Abrupt t" by simp
1261        with exec_c1 Catch.hyps
1262        show ?thesis
1263          by auto
1264      qed
1265    qed
1266  }
1267  ultimately show ?case
1268    by (auto intro: terminates.intros)
1269qed
1270
1271lemma terminates_mark_guards_to_terminates_Normal:
1272  "\<And>s. \<Gamma>\<turnstile>mark_guards f c\<down>Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<down>Normal s"
1273proof (induct c)
1274  case Skip thus ?case by (fastforce intro: terminates.intros)
1275next
1276  case Basic thus ?case by (fastforce intro: terminates.intros)
1277next
1278  case Spec thus ?case by (fastforce intro: terminates.intros)
1279next
1280  case (Seq c1 c2)
1281  have "\<Gamma>\<turnstile>mark_guards f (Seq c1 c2) \<down> Normal s" by fact
1282  then obtain
1283    termi_merge_c1: "\<Gamma>\<turnstile>mark_guards f c1 \<down> Normal s" and
1284    termi_merge_c2: "\<forall>s'. \<Gamma>\<turnstile>\<langle>mark_guards f c1,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow>
1285                           \<Gamma>\<turnstile>mark_guards f c2 \<down> s'"
1286    by (auto elim: terminates_Normal_elim_cases)
1287  from termi_merge_c1 Seq.hyps
1288  have "\<Gamma>\<turnstile>c1 \<down> Normal s" by iprover
1289  moreover
1290  {
1291    fix s'
1292    assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'"
1293    have "\<Gamma>\<turnstile> c2 \<down> s'"
1294    proof (cases "isFault s'")
1295      case True
1296      thus ?thesis by (auto elim: isFaultE)
1297    next
1298      case False
1299      from exec_to_exec_mark_guards [OF exec_c1 False]
1300      have "\<Gamma>\<turnstile>\<langle>mark_guards f c1,Normal s \<rangle> \<Rightarrow> s'" .
1301      from termi_merge_c2 [rule_format, OF this] Seq.hyps
1302      show ?thesis
1303        by (cases s') (auto)
1304    qed
1305  }
1306  ultimately show ?case by (auto intro: terminates.intros)
1307next
1308  case Cond thus ?case
1309    by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
1310next
1311  case (While b c)
1312  {
1313    fix u c'
1314    assume termi_c': "\<Gamma>\<turnstile>c' \<down> Normal u"
1315    assume c': "c' = mark_guards f (While b c)"
1316    have "\<Gamma>\<turnstile>While b c \<down> Normal u"
1317      using termi_c' c'
1318    proof (induct)
1319      case (WhileTrue s b' c')
1320      have s_in_b: "s \<in> b" using WhileTrue by simp
1321      have "\<Gamma>\<turnstile>mark_guards f c \<down> Normal s"
1322        using WhileTrue by (auto elim: terminates_Normal_elim_cases)
1323      with While.hyps have "\<Gamma>\<turnstile>c \<down> Normal s"
1324        by auto
1325      moreover
1326      have hyp_w: "\<forall>w. \<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s \<rangle> \<Rightarrow> w \<longrightarrow> \<Gamma>\<turnstile>While b c \<down> w"
1327        using WhileTrue by simp
1328      hence "\<forall>w. \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> w \<longrightarrow> \<Gamma>\<turnstile>While b c \<down> w"
1329        apply -
1330        apply (rule allI)
1331        apply (case_tac "w")
1332        apply (auto dest: exec_to_exec_mark_guards)
1333        done
1334      ultimately show ?case
1335        using s_in_b
1336        by (auto intro: terminates.intros)
1337    next
1338      case WhileFalse thus ?case by (auto intro: terminates.intros)
1339    qed auto
1340  }
1341  with While show ?case by simp
1342next
1343  case Call thus ?case
1344    by (fastforce intro: terminates.intros )
1345next
1346  case DynCom thus ?case
1347    by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
1348next
1349  case (Guard f g c)
1350  thus ?case by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
1351next
1352  case Throw thus ?case
1353    by (fastforce intro: terminates.intros )
1354next
1355  case (Catch c1 c2)
1356  have "\<Gamma>\<turnstile>mark_guards f (Catch c1 c2) \<down> Normal s" by fact
1357  then obtain
1358    termi_merge_c1: "\<Gamma>\<turnstile>mark_guards f c1 \<down> Normal s" and
1359    termi_merge_c2: "\<forall>s'. \<Gamma>\<turnstile>\<langle>mark_guards f c1,Normal s \<rangle> \<Rightarrow> Abrupt s' \<longrightarrow>
1360                           \<Gamma>\<turnstile>mark_guards f c2 \<down> Normal s'"
1361    by (auto elim: terminates_Normal_elim_cases)
1362  from termi_merge_c1 Catch.hyps
1363  have "\<Gamma>\<turnstile>c1 \<down> Normal s" by iprover
1364  moreover
1365  {
1366    fix s'
1367    assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'"
1368    have "\<Gamma>\<turnstile> c2 \<down> Normal s'"
1369    proof -
1370      from exec_to_exec_mark_guards [OF exec_c1]
1371      have "\<Gamma>\<turnstile>\<langle>mark_guards f c1,Normal s \<rangle> \<Rightarrow> Abrupt s'" by simp
1372      from termi_merge_c2 [rule_format, OF this] Catch.hyps
1373      show ?thesis
1374        by iprover
1375    qed
1376  }
1377  ultimately show ?case by (auto intro: terminates.intros)
1378qed
1379
1380lemma terminates_mark_guards_to_terminates:
1381  "\<Gamma>\<turnstile>mark_guards f c\<down>s \<Longrightarrow> \<Gamma>\<turnstile>c\<down> s"
1382  by (cases s) (auto intro: terminates_mark_guards_to_terminates_Normal)
1383
1384
1385(* ************************************************************************* *)
1386subsection \<open>Lemmas about @{const "merge_guards"}\<close>
1387(* ************************************************************************ *)
1388
1389lemma terminates_to_terminates_merge_guards:
1390  assumes termi: "\<Gamma>\<turnstile>c\<down>s"
1391  shows "\<Gamma>\<turnstile>merge_guards c\<down>s"
1392using termi
1393proof (induct)
1394  case (Guard s g c f)
1395  have s_in_g: "s \<in> g" by fact
1396  have termi_merge_c: "\<Gamma>\<turnstile>merge_guards c \<down> Normal s" by fact
1397  show ?case
1398  proof (cases "\<exists>f' g' c'. merge_guards c = Guard f' g' c'")
1399    case False
1400    hence "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
1401      by (cases "merge_guards c") (auto simp add: Let_def)
1402    with s_in_g termi_merge_c show ?thesis
1403      by (auto intro: terminates.intros)
1404  next
1405    case True
1406    then obtain f' g' c' where
1407      mc: "merge_guards c = Guard f' g' c'"
1408      by blast
1409    show ?thesis
1410    proof (cases "f=f'")
1411      case False
1412      with mc have "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
1413        by (simp add: Let_def)
1414      with s_in_g termi_merge_c show ?thesis
1415        by (auto intro: terminates.intros)
1416    next
1417      case True
1418      with mc have "merge_guards (Guard f g c) = Guard f (g \<inter> g') c'"
1419        by simp
1420      with s_in_g mc True termi_merge_c
1421      show ?thesis
1422        by (cases "s \<in> g'")
1423           (auto intro: terminates.intros elim: terminates_Normal_elim_cases)
1424    qed
1425  qed
1426next
1427  case (GuardFault s g f c)
1428  have "s \<notin> g" by fact
1429  thus ?case
1430    by (cases "merge_guards c")
1431       (auto intro: terminates.intros split: if_split_asm simp add: Let_def)
1432qed (fastforce intro: terminates.intros dest: exec_merge_guards_to_exec)+
1433
1434lemma terminates_merge_guards_to_terminates_Normal:
1435  shows "\<And>s. \<Gamma>\<turnstile>merge_guards c\<down>Normal s \<Longrightarrow> \<Gamma>\<turnstile>c\<down>Normal s"
1436proof (induct c)
1437  case Skip thus ?case by (fastforce intro: terminates.intros)
1438next
1439  case Basic thus ?case by (fastforce intro: terminates.intros)
1440next
1441  case Spec thus ?case by (fastforce intro: terminates.intros)
1442next
1443  case (Seq c1 c2)
1444  have "\<Gamma>\<turnstile>merge_guards (Seq c1 c2) \<down> Normal s" by fact
1445  then obtain
1446    termi_merge_c1: "\<Gamma>\<turnstile>merge_guards c1 \<down> Normal s" and
1447    termi_merge_c2: "\<forall>s'. \<Gamma>\<turnstile>\<langle>merge_guards c1,Normal s \<rangle> \<Rightarrow> s' \<longrightarrow>
1448                           \<Gamma>\<turnstile>merge_guards c2 \<down> s'"
1449    by (auto elim: terminates_Normal_elim_cases)
1450  from termi_merge_c1 Seq.hyps
1451  have "\<Gamma>\<turnstile>c1 \<down> Normal s" by iprover
1452  moreover
1453  {
1454    fix s'
1455    assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'"
1456    have "\<Gamma>\<turnstile> c2 \<down> s'"
1457    proof -
1458      from exec_to_exec_merge_guards [OF exec_c1]
1459      have "\<Gamma>\<turnstile>\<langle>merge_guards c1,Normal s \<rangle> \<Rightarrow> s'" .
1460      from termi_merge_c2 [rule_format, OF this] Seq.hyps
1461      show ?thesis
1462        by (cases s') (auto)
1463    qed
1464  }
1465  ultimately show ?case by (auto intro: terminates.intros)
1466next
1467  case Cond thus ?case
1468    by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
1469next
1470  case (While b c)
1471  {
1472    fix u c'
1473    assume termi_c': "\<Gamma>\<turnstile>c' \<down> Normal u"
1474    assume c': "c' = merge_guards (While b c)"
1475    have "\<Gamma>\<turnstile>While b c \<down> Normal u"
1476      using termi_c' c'
1477    proof (induct)
1478      case (WhileTrue s b' c')
1479      have s_in_b: "s \<in> b" using WhileTrue by simp
1480      have "\<Gamma>\<turnstile>merge_guards c \<down> Normal s"
1481        using WhileTrue by (auto elim: terminates_Normal_elim_cases)
1482      with While.hyps have "\<Gamma>\<turnstile>c \<down> Normal s"
1483        by auto
1484      moreover
1485      have hyp_w: "\<forall>w. \<Gamma>\<turnstile>\<langle>merge_guards c,Normal s \<rangle> \<Rightarrow> w \<longrightarrow> \<Gamma>\<turnstile>While b c \<down> w"
1486        using WhileTrue by simp
1487      hence "\<forall>w. \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> w \<longrightarrow> \<Gamma>\<turnstile>While b c \<down> w"
1488        by (simp add: exec_iff_exec_merge_guards [symmetric])
1489      ultimately show ?case
1490        using s_in_b
1491        by (auto intro: terminates.intros)
1492    next
1493      case WhileFalse thus ?case by (auto intro: terminates.intros)
1494    qed auto
1495  }
1496  with While show ?case by simp
1497next
1498  case Call thus ?case
1499    by (fastforce intro: terminates.intros )
1500next
1501  case DynCom thus ?case
1502    by (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
1503next
1504  case (Guard f g c)
1505  have termi_merge: "\<Gamma>\<turnstile>merge_guards (Guard f g c) \<down> Normal s" by fact
1506  show ?case
1507  proof (cases "\<exists>f' g' c'. merge_guards c = Guard f' g' c'")
1508    case False
1509    hence m: "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
1510      by (cases "merge_guards c") (auto simp add: Let_def)
1511    from termi_merge Guard.hyps show ?thesis
1512      by (simp only: m)
1513         (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
1514  next
1515    case True
1516    then obtain f' g' c' where
1517      mc: "merge_guards c = Guard f' g' c'"
1518      by blast
1519    show ?thesis
1520    proof (cases "f=f'")
1521      case False
1522      with mc have m: "merge_guards (Guard f g c) = Guard f g (merge_guards c)"
1523        by (simp add: Let_def)
1524      from termi_merge Guard.hyps show ?thesis
1525      by (simp only: m)
1526         (fastforce intro: terminates.intros elim: terminates_Normal_elim_cases)
1527    next
1528      case True
1529      with mc have m: "merge_guards (Guard f g c) = Guard f (g \<inter> g') c'"
1530        by simp
1531      from termi_merge Guard.hyps
1532      show ?thesis
1533        by (simp only: m mc)
1534           (auto intro: terminates.intros elim: terminates_Normal_elim_cases)
1535    qed
1536  qed
1537next
1538  case Throw thus ?case
1539    by (fastforce intro: terminates.intros )
1540next
1541  case (Catch c1 c2)
1542  have "\<Gamma>\<turnstile>merge_guards (Catch c1 c2) \<down> Normal s" by fact
1543  then obtain
1544    termi_merge_c1: "\<Gamma>\<turnstile>merge_guards c1 \<down> Normal s" and
1545    termi_merge_c2: "\<forall>s'. \<Gamma>\<turnstile>\<langle>merge_guards c1,Normal s \<rangle> \<Rightarrow> Abrupt s' \<longrightarrow>
1546                           \<Gamma>\<turnstile>merge_guards c2 \<down> Normal s'"
1547    by (auto elim: terminates_Normal_elim_cases)
1548  from termi_merge_c1 Catch.hyps
1549  have "\<Gamma>\<turnstile>c1 \<down> Normal s" by iprover
1550  moreover
1551  {
1552    fix s'
1553    assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'"
1554    have "\<Gamma>\<turnstile> c2 \<down> Normal s'"
1555    proof -
1556      from exec_to_exec_merge_guards [OF exec_c1]
1557      have "\<Gamma>\<turnstile>\<langle>merge_guards c1,Normal s \<rangle> \<Rightarrow> Abrupt s'" .
1558      from termi_merge_c2 [rule_format, OF this] Catch.hyps
1559      show ?thesis
1560        by iprover
1561    qed
1562  }
1563  ultimately show ?case by (auto intro: terminates.intros)
1564qed
1565
1566lemma terminates_merge_guards_to_terminates:
1567   "\<Gamma>\<turnstile>merge_guards c\<down> s \<Longrightarrow> \<Gamma>\<turnstile>c\<down> s"
1568by (cases s) (auto intro: terminates_merge_guards_to_terminates_Normal)
1569
1570theorem terminates_iff_terminates_merge_guards:
1571  "\<Gamma>\<turnstile>c\<down> s = \<Gamma>\<turnstile>merge_guards c\<down> s"
1572  by (iprover intro: terminates_to_terminates_merge_guards
1573    terminates_merge_guards_to_terminates)
1574
1575(* ************************************************************************* *)
1576subsection \<open>Lemmas about @{term "c\<^sub>1 \<subseteq>\<^sub>g c\<^sub>2"}\<close>
1577(* ************************************************************************ *)
1578
1579lemma terminates_fewer_guards_Normal:
1580  shows "\<And>c s. \<lbrakk>\<Gamma>\<turnstile>c'\<down>Normal s; c \<subseteq>\<^sub>g c'; \<Gamma>\<turnstile>\<langle>c',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV\<rbrakk>
1581              \<Longrightarrow> \<Gamma>\<turnstile>c\<down>Normal s"
1582proof (induct c')
1583  case Skip thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
1584next
1585  case Basic thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
1586next
1587  case Spec thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
1588next
1589  case (Seq c1' c2')
1590  have termi: "\<Gamma>\<turnstile>Seq c1' c2' \<down> Normal s" by fact
1591  then obtain
1592    termi_c1': "\<Gamma>\<turnstile>c1'\<down> Normal s" and
1593    termi_c2': "\<forall>s'. \<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>c2'\<down> s'"
1594    by (auto elim: terminates_Normal_elim_cases)
1595  have noFault: "\<Gamma>\<turnstile>\<langle>Seq c1' c2',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" by fact
1596  hence noFault_c1': "\<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV"
1597    by (auto intro: exec.intros simp add: final_notin_def)
1598  have "c \<subseteq>\<^sub>g Seq c1' c2'" by fact
1599  from subseteq_guards_Seq [OF this] obtain c1 c2 where
1600    c: "c = Seq c1 c2" and
1601    c1_c1': "c1 \<subseteq>\<^sub>g c1'" and
1602    c2_c2': "c2 \<subseteq>\<^sub>g c2'"
1603    by blast
1604  from termi_c1' c1_c1' noFault_c1'
1605  have "\<Gamma>\<turnstile>c1\<down> Normal s"
1606    by (rule Seq.hyps)
1607  moreover
1608  {
1609    fix t
1610    assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> t"
1611    have "\<Gamma>\<turnstile>c2\<down> t"
1612    proof -
1613      from exec_to_exec_subseteq_guards [OF c1_c1' exec_c1] obtain t' where
1614        exec_c1': "\<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow> t'" and
1615        t_Fault: "isFault t \<longrightarrow> isFault t'" and
1616        t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t"
1617        by blast
1618      show ?thesis
1619      proof (cases "isFault t'")
1620        case True
1621        with exec_c1' noFault_c1'
1622        have False
1623          by (fastforce elim: isFaultE dest: Fault_end simp add: final_notin_def)
1624        thus ?thesis ..
1625      next
1626        case False
1627        with t'_noFault have t': "t'=t" by simp
1628        with termi_c2' exec_c1'
1629        have termi_c2': "\<Gamma>\<turnstile>c2'\<down> t"
1630          by auto
1631        show ?thesis
1632        proof (cases t)
1633          case Fault thus ?thesis by auto
1634        next
1635          case Abrupt thus ?thesis by auto
1636        next
1637          case Stuck thus ?thesis by auto
1638        next
1639          case (Normal u)
1640          with noFault exec_c1' t'
1641          have "\<Gamma>\<turnstile>\<langle>c2',Normal u \<rangle> \<Rightarrow>\<notin>Fault ` UNIV"
1642            by (auto intro: exec.intros simp add: final_notin_def)
1643          from termi_c2' [simplified Normal] c2_c2' this
1644          have "\<Gamma>\<turnstile>c2 \<down> Normal u"
1645            by (rule Seq.hyps)
1646          with Normal exec_c1
1647          show ?thesis by simp
1648        qed
1649      qed
1650    qed
1651  }
1652  ultimately show ?case using c by (auto intro: terminates.intros)
1653next
1654  case (Cond b c1' c2')
1655  have noFault: "\<Gamma>\<turnstile>\<langle>Cond b c1' c2',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" by fact
1656  have termi: "\<Gamma>\<turnstile>Cond b c1' c2' \<down> Normal s" by fact
1657  have "c \<subseteq>\<^sub>g Cond b c1' c2'" by fact
1658  from subseteq_guards_Cond [OF this] obtain c1 c2 where
1659    c: "c = Cond b c1 c2" and
1660    c1_c1': "c1 \<subseteq>\<^sub>g c1'" and
1661    c2_c2': "c2 \<subseteq>\<^sub>g c2'"
1662    by blast
1663  thus ?case
1664  proof (cases "s \<in> b")
1665    case True
1666    with termi have termi_c1': "\<Gamma>\<turnstile>c1' \<down> Normal s"
1667      by (auto elim: terminates_Normal_elim_cases)
1668    from True noFault have "\<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV"
1669      by (auto intro: exec.intros simp add: final_notin_def)
1670    from termi_c1' c1_c1' this
1671    have "\<Gamma>\<turnstile>c1 \<down> Normal s"
1672      by (rule Cond.hyps)
1673    with True c show ?thesis
1674      by (auto intro: terminates.intros)
1675  next
1676    case False
1677    with termi have termi_c2': "\<Gamma>\<turnstile>c2' \<down> Normal s"
1678      by (auto elim: terminates_Normal_elim_cases)
1679    from False noFault have "\<Gamma>\<turnstile>\<langle>c2',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV"
1680      by (auto intro: exec.intros simp add: final_notin_def)
1681    from termi_c2' c2_c2' this
1682    have "\<Gamma>\<turnstile>c2 \<down> Normal s"
1683      by (rule Cond.hyps)
1684    with False c show ?thesis
1685      by (auto intro: terminates.intros)
1686  qed
1687next
1688  case (While b c')
1689  have noFault: "\<Gamma>\<turnstile>\<langle>While b c',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" by fact
1690  have termi: "\<Gamma>\<turnstile>While b c' \<down> Normal s" by fact
1691  have "c \<subseteq>\<^sub>g While b c'" by fact
1692  from subseteq_guards_While [OF this]
1693  obtain c'' where
1694    c: "c = While b c''" and
1695    c''_c': "c'' \<subseteq>\<^sub>g c'"
1696    by blast
1697  {
1698    fix d u
1699    assume termi: "\<Gamma>\<turnstile>d \<down> u"
1700    assume d: "d = While b c'"
1701    assume noFault: "\<Gamma>\<turnstile>\<langle>While b c',u \<rangle> \<Rightarrow>\<notin>Fault ` UNIV"
1702    have "\<Gamma>\<turnstile>While b c'' \<down> u"
1703    using termi d noFault
1704    proof (induct)
1705      case (WhileTrue u b' c''')
1706      have u_in_b: "u \<in> b" using WhileTrue by simp
1707      have termi_c': "\<Gamma>\<turnstile>c' \<down> Normal u" using WhileTrue by simp
1708      have noFault: "\<Gamma>\<turnstile>\<langle>While b c',Normal u \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" using WhileTrue by simp
1709      hence noFault_c': "\<Gamma>\<turnstile>\<langle>c',Normal u \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" using u_in_b
1710        by (auto intro: exec.intros simp add: final_notin_def)
1711      from While.hyps [OF termi_c' c''_c' this]
1712      have "\<Gamma>\<turnstile>c'' \<down> Normal u".
1713      moreover
1714      from WhileTrue
1715      have hyp_w: "\<forall>s'. \<Gamma>\<turnstile>\<langle>c',Normal u \<rangle> \<Rightarrow> s'  \<longrightarrow> \<Gamma>\<turnstile>\<langle>While b c',s' \<rangle> \<Rightarrow>\<notin>Fault ` UNIV
1716                        \<longrightarrow> \<Gamma>\<turnstile>While b c'' \<down> s'"
1717        by simp
1718      {
1719        fix v
1720        assume exec_c'': "\<Gamma>\<turnstile>\<langle>c'',Normal u \<rangle> \<Rightarrow> v"
1721        have "\<Gamma>\<turnstile>While b c'' \<down> v"
1722        proof -
1723          from exec_to_exec_subseteq_guards [OF c''_c' exec_c''] obtain v' where
1724            exec_c': "\<Gamma>\<turnstile>\<langle>c',Normal u \<rangle> \<Rightarrow> v'" and
1725            v_Fault: "isFault v \<longrightarrow> isFault v'" and
1726            v'_noFault: "\<not> isFault v' \<longrightarrow> v' = v"
1727            by auto
1728          show ?thesis
1729          proof (cases "isFault v'")
1730            case True
1731            with exec_c' noFault u_in_b
1732            have False
1733              by (fastforce
1734                   simp add: final_notin_def intro: exec.intros elim: isFaultE)
1735            thus ?thesis ..
1736          next
1737            case False
1738            with v'_noFault have v': "v'=v"
1739              by simp
1740            with noFault exec_c' u_in_b
1741            have "\<Gamma>\<turnstile>\<langle>While b c',v \<rangle> \<Rightarrow>\<notin>Fault ` UNIV"
1742              by (fastforce simp add: final_notin_def intro: exec.intros)
1743            from hyp_w [rule_format, OF exec_c' [simplified v'] this]
1744            show "\<Gamma>\<turnstile>While b c'' \<down> v" .
1745          qed
1746        qed
1747      }
1748      ultimately
1749      show ?case using u_in_b
1750        by (auto intro: terminates.intros)
1751    next
1752      case WhileFalse thus ?case by (auto intro: terminates.intros)
1753    qed auto
1754  }
1755  with c noFault termi show ?case
1756    by auto
1757next
1758  case Call thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
1759next
1760  case (DynCom C')
1761  have termi: "\<Gamma>\<turnstile>DynCom C' \<down> Normal s" by fact
1762  hence termi_C': "\<Gamma>\<turnstile>C' s \<down> Normal s"
1763    by cases
1764  have noFault: "\<Gamma>\<turnstile>\<langle>DynCom C',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" by fact
1765  hence noFault_C': "\<Gamma>\<turnstile>\<langle>C' s,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV"
1766    by (auto intro: exec.intros simp add: final_notin_def)
1767  have "c \<subseteq>\<^sub>g DynCom C'" by fact
1768  from subseteq_guards_DynCom [OF this] obtain C where
1769    c: "c = DynCom C" and
1770    C_C': "\<forall>s. C s \<subseteq>\<^sub>g C' s"
1771    by blast
1772  from DynCom.hyps termi_C' C_C' [rule_format] noFault_C'
1773  have "\<Gamma>\<turnstile>C s \<down> Normal s"
1774    by fast
1775  with c show ?case
1776    by (auto intro: terminates.intros)
1777next
1778  case (Guard f' g' c')
1779  have noFault: "\<Gamma>\<turnstile>\<langle>Guard f' g' c',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" by fact
1780  have termi: "\<Gamma>\<turnstile>Guard f' g' c' \<down> Normal s" by fact
1781  have "c \<subseteq>\<^sub>g Guard f' g' c'" by fact
1782  hence c_cases: "(c \<subseteq>\<^sub>g c') \<or> (\<exists>c''. c = Guard f' g' c'' \<and> (c'' \<subseteq>\<^sub>g c'))"
1783    by (rule subseteq_guards_Guard)
1784  thus ?case
1785  proof (cases "s \<in> g'")
1786    case True
1787    note s_in_g' = this
1788    with noFault have noFault_c': "\<Gamma>\<turnstile>\<langle>c',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV"
1789      by (auto simp add: final_notin_def intro: exec.intros)
1790    from termi s_in_g' have termi_c': "\<Gamma>\<turnstile>c' \<down> Normal s"
1791      by cases auto
1792    from c_cases show ?thesis
1793    proof
1794      assume "c \<subseteq>\<^sub>g c'"
1795      from termi_c' this noFault_c'
1796      show "\<Gamma>\<turnstile>c \<down> Normal s"
1797        by (rule Guard.hyps)
1798    next
1799      assume "\<exists>c''. c = Guard f' g' c'' \<and> (c'' \<subseteq>\<^sub>g c')"
1800      then obtain c'' where
1801        c: "c = Guard f' g' c''" and c''_c': "c'' \<subseteq>\<^sub>g c'"
1802        by blast
1803      from termi_c' c''_c' noFault_c'
1804      have "\<Gamma>\<turnstile>c'' \<down> Normal s"
1805        by (rule Guard.hyps)
1806      with s_in_g' c
1807      show ?thesis
1808        by (auto intro: terminates.intros)
1809    qed
1810  next
1811    case False
1812    with noFault have False
1813      by (auto intro: exec.intros simp add: final_notin_def)
1814    thus ?thesis ..
1815  qed
1816next
1817  case Throw thus ?case by (auto intro: terminates.intros dest: subseteq_guardsD)
1818next
1819  case (Catch c1' c2')
1820  have termi: "\<Gamma>\<turnstile>Catch c1' c2' \<down> Normal s" by fact
1821  then obtain
1822    termi_c1': "\<Gamma>\<turnstile>c1'\<down> Normal s" and
1823    termi_c2': "\<forall>s'. \<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow> Abrupt s' \<longrightarrow> \<Gamma>\<turnstile>c2'\<down> Normal s'"
1824    by (auto elim: terminates_Normal_elim_cases)
1825  have noFault: "\<Gamma>\<turnstile>\<langle>Catch c1' c2',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV" by fact
1826  hence noFault_c1': "\<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV"
1827    by (fastforce intro: exec.intros simp add: final_notin_def)
1828  have "c \<subseteq>\<^sub>g Catch c1' c2'"  by fact
1829  from subseteq_guards_Catch [OF this] obtain c1 c2 where
1830    c: "c = Catch c1 c2" and
1831    c1_c1': "c1 \<subseteq>\<^sub>g c1'" and
1832    c2_c2': "c2 \<subseteq>\<^sub>g c2'"
1833    by blast
1834  from termi_c1' c1_c1' noFault_c1'
1835  have "\<Gamma>\<turnstile>c1\<down> Normal s"
1836    by (rule Catch.hyps)
1837  moreover
1838  {
1839    fix t
1840    assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt t"
1841    have "\<Gamma>\<turnstile>c2\<down> Normal t"
1842    proof -
1843      from exec_to_exec_subseteq_guards [OF c1_c1' exec_c1] obtain t' where
1844        exec_c1': "\<Gamma>\<turnstile>\<langle>c1',Normal s \<rangle> \<Rightarrow> t'" and
1845        t'_noFault: "\<not> isFault t' \<longrightarrow> t' = Abrupt t"
1846        by blast
1847      show ?thesis
1848      proof (cases "isFault t'")
1849        case True
1850        with exec_c1' noFault_c1'
1851        have False
1852          by (fastforce elim: isFaultE dest: Fault_end simp add: final_notin_def)
1853        thus ?thesis ..
1854      next
1855        case False
1856        with t'_noFault have t': "t'=Abrupt t" by simp
1857        with termi_c2' exec_c1'
1858        have termi_c2': "\<Gamma>\<turnstile>c2'\<down> Normal t"
1859          by auto
1860        with noFault exec_c1' t'
1861        have "\<Gamma>\<turnstile>\<langle>c2',Normal t \<rangle> \<Rightarrow>\<notin>Fault ` UNIV"
1862          by (auto intro: exec.intros simp add: final_notin_def)
1863        from termi_c2' c2_c2' this
1864        show "\<Gamma>\<turnstile>c2 \<down> Normal t"
1865          by (rule Catch.hyps)
1866      qed
1867    qed
1868  }
1869  ultimately show ?case using c by (auto intro: terminates.intros)
1870qed
1871
1872theorem terminates_fewer_guards:
1873  shows "\<lbrakk>\<Gamma>\<turnstile>c'\<down>s; c \<subseteq>\<^sub>g c'; \<Gamma>\<turnstile>\<langle>c',s \<rangle> \<Rightarrow>\<notin>Fault ` UNIV\<rbrakk>
1874         \<Longrightarrow> \<Gamma>\<turnstile>c\<down>s"
1875  by (cases s) (auto intro: terminates_fewer_guards_Normal)
1876
1877lemma terminates_noFault_strip_guards:
1878  assumes termi: "\<Gamma>\<turnstile>c\<down>Normal s"
1879  shows "\<lbrakk>\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>strip_guards F c\<down>Normal s"
1880using termi
1881proof (induct)
1882  case Skip thus ?case by (auto intro: terminates.intros)
1883next
1884  case Basic thus ?case by (auto intro: terminates.intros)
1885next
1886  case Spec thus ?case by (auto intro: terminates.intros)
1887next
1888  case (Guard s g c f)
1889  have s_in_g: "s \<in> g" by fact
1890  have "\<Gamma>\<turnstile>c \<down> Normal s" by fact
1891  have "\<Gamma>\<turnstile>\<langle>Guard f g c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact
1892  with s_in_g have "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F"
1893    by (fastforce simp add: final_notin_def intro: exec.intros)
1894  with Guard.hyps have "\<Gamma>\<turnstile>strip_guards F c \<down> Normal s" by simp
1895  with s_in_g show ?case
1896    by (auto intro: terminates.intros)
1897next
1898  case GuardFault thus ?case
1899    by (auto intro: terminates.intros exec.intros simp add: final_notin_def )
1900next
1901  case Fault thus ?case by (auto intro: terminates.intros)
1902next
1903  case (Seq c1 s c2)
1904  have noFault_Seq: "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact
1905  hence noFault_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F"
1906    by (auto simp add: final_notin_def intro: exec.intros)
1907  with Seq.hyps have "\<Gamma>\<turnstile>strip_guards F c1 \<down> Normal s" by simp
1908  moreover
1909  {
1910    fix s'
1911    assume exec_strip_guards_c1: "\<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s \<rangle> \<Rightarrow> s'"
1912    have "\<Gamma>\<turnstile>strip_guards F c2 \<down> s'"
1913    proof (cases "isFault s'")
1914      case True
1915      thus ?thesis by (auto elim: isFaultE intro: terminates.intros)
1916    next
1917      case False
1918      with exec_strip_guards_to_exec [OF exec_strip_guards_c1] noFault_c1
1919      have *: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'"
1920        by (auto simp add: final_notin_def elim!: isFaultE)
1921      with noFault_Seq have "\<Gamma>\<turnstile>\<langle>c2,s' \<rangle> \<Rightarrow>\<notin>Fault ` F"
1922        by (auto simp add: final_notin_def intro: exec.intros)
1923      with * show ?thesis
1924        using Seq.hyps by simp
1925    qed
1926  }
1927  ultimately show ?case
1928    by (auto intro: terminates.intros)
1929next
1930  case CondTrue thus ?case
1931    by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def )
1932next
1933  case CondFalse thus ?case
1934    by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def )
1935next
1936  case (WhileTrue s b c)
1937  have s_in_b: "s \<in> b" by fact
1938  have noFault_while: "\<Gamma>\<turnstile>\<langle>While b c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact
1939  with s_in_b have noFault_c: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F"
1940    by (auto simp add: final_notin_def intro: exec.intros)
1941  with WhileTrue.hyps have "\<Gamma>\<turnstile>strip_guards F c \<down> Normal s" by simp
1942  moreover
1943  {
1944    fix s'
1945    assume exec_strip_guards_c: "\<Gamma>\<turnstile>\<langle>strip_guards F c,Normal s \<rangle> \<Rightarrow> s'"
1946    have "\<Gamma>\<turnstile>strip_guards F (While b c) \<down> s'"
1947    proof (cases "isFault s'")
1948      case True
1949      thus ?thesis by (auto elim: isFaultE intro: terminates.intros)
1950    next
1951      case False
1952      with exec_strip_guards_to_exec [OF exec_strip_guards_c] noFault_c
1953      have *: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s'"
1954        by (auto simp add: final_notin_def elim!: isFaultE)
1955      with s_in_b noFault_while have "\<Gamma>\<turnstile>\<langle>While b c,s' \<rangle> \<Rightarrow>\<notin>Fault ` F"
1956        by (auto simp add: final_notin_def intro: exec.intros)
1957      with * show ?thesis
1958        using WhileTrue.hyps by simp
1959    qed
1960  }
1961  ultimately show ?case
1962    using WhileTrue.hyps by (auto intro: terminates.intros)
1963next
1964  case WhileFalse thus ?case by (auto intro: terminates.intros)
1965next
1966  case Call thus ?case by (auto intro: terminates.intros)
1967next
1968  case CallUndefined thus ?case by (auto intro: terminates.intros)
1969next
1970  case Stuck thus ?case by (auto intro: terminates.intros)
1971next
1972  case DynCom thus ?case
1973    by (auto intro: terminates.intros exec.intros simp add: final_notin_def )
1974next
1975  case Throw thus ?case by (auto intro: terminates.intros)
1976next
1977  case Abrupt thus ?case by (auto intro: terminates.intros)
1978next
1979  case (Catch c1 s c2)
1980  have noFault_Catch: "\<Gamma>\<turnstile>\<langle>Catch c1 c2,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact
1981  hence noFault_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F"
1982    by (fastforce simp add: final_notin_def intro: exec.intros)
1983  with Catch.hyps have "\<Gamma>\<turnstile>strip_guards F c1 \<down> Normal s" by simp
1984  moreover
1985  {
1986    fix s'
1987    assume exec_strip_guards_c1: "\<Gamma>\<turnstile>\<langle>strip_guards F c1,Normal s \<rangle> \<Rightarrow> Abrupt s'"
1988    have "\<Gamma>\<turnstile>strip_guards F c2 \<down> Normal s'"
1989    proof -
1990      from exec_strip_guards_to_exec [OF exec_strip_guards_c1] noFault_c1
1991      have *: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'"
1992        by (auto simp add: final_notin_def elim!: isFaultE)
1993      with noFault_Catch have "\<Gamma>\<turnstile>\<langle>c2,Normal s' \<rangle> \<Rightarrow>\<notin>Fault ` F"
1994        by (auto simp add: final_notin_def intro: exec.intros)
1995      with * show ?thesis
1996        using Catch.hyps by simp
1997    qed
1998  }
1999  ultimately show ?case
2000    using Catch.hyps by (auto intro: terminates.intros)
2001qed
2002
2003(* ************************************************************************* *)
2004subsection \<open>Lemmas about @{const "strip_guards"}\<close>
2005(* ************************************************************************* *)
2006
2007lemma terminates_noFault_strip:
2008  assumes termi: "\<Gamma>\<turnstile>c\<down>Normal s"
2009  shows "\<lbrakk>\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F\<rbrakk> \<Longrightarrow> strip F \<Gamma>\<turnstile>c\<down>Normal s"
2010using termi
2011proof (induct)
2012  case Skip thus ?case by (auto intro: terminates.intros)
2013next
2014  case Basic thus ?case by (auto intro: terminates.intros)
2015next
2016  case Spec thus ?case by (auto intro: terminates.intros)
2017next
2018  case (Guard s g c f)
2019  have s_in_g: "s \<in> g" by fact
2020  have "\<Gamma>\<turnstile>\<langle>Guard f g c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact
2021  with s_in_g have "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F"
2022    by (fastforce simp add: final_notin_def intro: exec.intros)
2023  then have "strip F \<Gamma>\<turnstile>c \<down> Normal s" by (simp add: Guard.hyps)
2024  with s_in_g show ?case
2025    by (auto intro: terminates.intros simp del: strip_simp)
2026next
2027  case GuardFault thus ?case
2028    by (auto intro: terminates.intros exec.intros simp add: final_notin_def )
2029next
2030  case Fault thus ?case by (auto intro: terminates.intros)
2031next
2032  case (Seq c1 s c2)
2033  have noFault_Seq: "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact
2034  hence noFault_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F"
2035    by (auto simp add: final_notin_def intro: exec.intros)
2036  then have "strip F \<Gamma>\<turnstile>c1 \<down> Normal s" by (simp add: Seq.hyps)
2037  moreover
2038  {
2039    fix s'
2040    assume exec_strip_c1: "strip F \<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'"
2041    have "strip F \<Gamma>\<turnstile>c2 \<down> s'"
2042    proof (cases "isFault s'")
2043      case True
2044      thus ?thesis by (auto elim: isFaultE intro: terminates.intros)
2045    next
2046      case False
2047      with exec_strip_to_exec [OF exec_strip_c1] noFault_c1
2048      have *: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'"
2049        by (auto simp add: final_notin_def elim!: isFaultE)
2050      with noFault_Seq have "\<Gamma>\<turnstile>\<langle>c2,s' \<rangle> \<Rightarrow>\<notin>Fault ` F"
2051        by (auto simp add: final_notin_def intro: exec.intros)
2052      with * show ?thesis
2053        using Seq.hyps by (simp del: strip_simp)
2054    qed
2055  }
2056  ultimately show ?case
2057    by (fastforce intro: terminates.intros)
2058next
2059  case CondTrue thus ?case
2060    by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def )
2061next
2062  case CondFalse thus ?case
2063    by (fastforce intro: terminates.intros exec.intros simp add: final_notin_def )
2064next
2065  case (WhileTrue s b c)
2066  have s_in_b: "s \<in> b" by fact
2067  have noFault_while: "\<Gamma>\<turnstile>\<langle>While b c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact
2068  with s_in_b have noFault_c: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F"
2069    by (auto simp add: final_notin_def intro: exec.intros)
2070  then have "strip F \<Gamma>\<turnstile>c \<down> Normal s" by (simp add: WhileTrue.hyps)
2071  moreover
2072  {
2073    fix s'
2074    assume exec_strip_c: "strip F \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s'"
2075    have "strip F \<Gamma>\<turnstile>While b c \<down> s'"
2076    proof (cases "isFault s'")
2077      case True
2078      thus ?thesis by (auto elim: isFaultE intro: terminates.intros)
2079    next
2080      case False
2081      with exec_strip_to_exec [OF exec_strip_c] noFault_c
2082      have *: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s'"
2083        by (auto simp add: final_notin_def elim!: isFaultE)
2084      with s_in_b noFault_while have "\<Gamma>\<turnstile>\<langle>While b c,s' \<rangle> \<Rightarrow>\<notin>Fault ` F"
2085        by (auto simp add: final_notin_def intro: exec.intros)
2086      with * show ?thesis
2087        using WhileTrue.hyps by (simp del: strip_simp)
2088    qed
2089  }
2090  ultimately show ?case
2091    using WhileTrue.hyps by (auto intro: terminates.intros simp del: strip_simp)
2092next
2093  case WhileFalse thus ?case by (auto intro: terminates.intros)
2094next
2095  case (Call p bdy s)
2096  have bdy: "\<Gamma> p = Some bdy" by fact
2097  have "\<Gamma>\<turnstile>\<langle>Call p,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact
2098  with bdy have bdy_noFault: "\<Gamma>\<turnstile>\<langle>bdy,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F"
2099    by (auto intro: exec.intros simp add: final_notin_def)
2100  then have strip_bdy_noFault: "strip F \<Gamma>\<turnstile>\<langle>bdy,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F"
2101    by (auto simp add: final_notin_def dest!: exec_strip_to_exec elim!: isFaultE)
2102
2103  from bdy_noFault have "strip F \<Gamma>\<turnstile>bdy \<down> Normal s" by (simp add: Call.hyps)
2104  from terminates_noFault_strip_guards [OF this strip_bdy_noFault]
2105  have "strip F \<Gamma>\<turnstile>strip_guards F bdy \<down> Normal s".
2106  with bdy show ?case
2107    by (fastforce intro: terminates.Call)
2108next
2109  case CallUndefined thus ?case by (auto intro: terminates.intros)
2110next
2111  case Stuck thus ?case by (auto intro: terminates.intros)
2112next
2113  case DynCom thus ?case
2114    by (auto intro: terminates.intros exec.intros simp add: final_notin_def )
2115next
2116  case Throw thus ?case by (auto intro: terminates.intros)
2117next
2118  case Abrupt thus ?case by (auto intro: terminates.intros)
2119next
2120  case (Catch c1 s c2)
2121  have noFault_Catch: "\<Gamma>\<turnstile>\<langle>Catch c1 c2,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F" by fact
2122  hence noFault_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow>\<notin>Fault ` F"
2123    by (fastforce simp add: final_notin_def intro: exec.intros)
2124  then have "strip F \<Gamma>\<turnstile>c1 \<down> Normal s" by (simp add: Catch.hyps)
2125  moreover
2126  {
2127    fix s'
2128    assume exec_strip_c1: "strip F \<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'"
2129    have "strip F \<Gamma>\<turnstile>c2 \<down> Normal s'"
2130    proof -
2131      from exec_strip_to_exec [OF exec_strip_c1] noFault_c1
2132      have *: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'"
2133        by (auto simp add: final_notin_def elim!: isFaultE)
2134      with * noFault_Catch have "\<Gamma>\<turnstile>\<langle>c2,Normal s' \<rangle> \<Rightarrow>\<notin>Fault ` F"
2135        by (auto simp add: final_notin_def intro: exec.intros)
2136      with * show ?thesis
2137        using Catch.hyps by (simp del: strip_simp)
2138    qed
2139  }
2140  ultimately show ?case
2141    using Catch.hyps by (auto intro: terminates.intros simp del: strip_simp)
2142qed
2143
2144
2145(* ************************************************************************* *)
2146subsection \<open>Miscellaneous\<close>
2147(* ************************************************************************* *)
2148
2149lemma terminates_while_lemma:
2150  assumes termi: "\<Gamma>\<turnstile>w\<down>fk"
2151  shows "\<And>k b c. \<lbrakk>fk = Normal (f k); w=While b c;
2152                       \<forall>i. \<Gamma>\<turnstile>\<langle>c,Normal (f i) \<rangle> \<Rightarrow> Normal (f (Suc i))\<rbrakk>
2153         \<Longrightarrow> \<exists>i. f i \<notin> b"
2154using termi
2155proof (induct)
2156  case WhileTrue thus ?case by blast
2157next
2158  case WhileFalse thus ?case by blast
2159qed simp_all
2160
2161lemma terminates_while:
2162  "\<lbrakk>\<Gamma>\<turnstile>(While b c)\<down>Normal (f k);
2163    \<forall>i. \<Gamma>\<turnstile>\<langle>c,Normal (f i) \<rangle> \<Rightarrow> Normal (f (Suc i))\<rbrakk>
2164         \<Longrightarrow> \<exists>i. f i \<notin> b"
2165  by (blast intro: terminates_while_lemma)
2166
2167lemma wf_terminates_while:
2168 "wf {(t,s). \<Gamma>\<turnstile>(While b c)\<down>Normal s \<and> s\<in>b \<and>
2169             \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> Normal t}"
2170apply(subst wf_iff_no_infinite_down_chain)
2171apply(rule notI)
2172apply clarsimp
2173apply(insert terminates_while)
2174apply blast
2175done
2176
2177lemma terminates_restrict_to_terminates:
2178  assumes terminates_res: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile> c \<down> s"
2179  assumes not_Stuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c,s \<rangle> \<Rightarrow>\<notin>{Stuck}"
2180  shows "\<Gamma>\<turnstile> c \<down> s"
2181using terminates_res not_Stuck
2182proof (induct)
2183  case Skip show ?case by (rule terminates.Skip)
2184next
2185  case Basic show ?case by (rule terminates.Basic)
2186next
2187  case Spec show ?case by (rule terminates.Spec)
2188next
2189  case Guard thus ?case
2190    by (auto intro: terminates.Guard dest: notStuck_GuardD)
2191next
2192  case GuardFault thus ?case by (auto intro: terminates.GuardFault)
2193next
2194  case Fault show ?case by (rule terminates.Fault)
2195next
2196  case (Seq c1 s c2)
2197  have not_Stuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>Seq c1 c2,Normal s \<rangle> \<Rightarrow>\<notin>{Stuck}" by fact
2198  hence c1_notStuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow>\<notin>{Stuck}"
2199    by (rule notStuck_SeqD1)
2200  show "\<Gamma>\<turnstile>Seq c1 c2 \<down> Normal s"
2201  proof (rule terminates.Seq,safe)
2202    from c1_notStuck
2203    show "\<Gamma>\<turnstile>c1 \<down> Normal s"
2204      by (rule Seq.hyps)
2205  next
2206    fix s'
2207    assume exec: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> s'"
2208    show "\<Gamma>\<turnstile>c2 \<down> s'"
2209    proof -
2210      from exec_to_exec_restrict [OF exec] obtain t' where
2211        exec_res: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> t'" and
2212        t'_notStuck: "t' \<noteq> Stuck \<longrightarrow> t' = s'"
2213        by blast
2214      show ?thesis
2215      proof (cases "t'=Stuck")
2216        case True
2217        with c1_notStuck exec_res have "False"
2218          by (auto simp add: final_notin_def)
2219        thus ?thesis ..
2220      next
2221        case False
2222        with t'_notStuck have t': "t'=s'" by simp
2223        with not_Stuck exec_res
2224        have "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c2,s' \<rangle> \<Rightarrow>\<notin>{Stuck}"
2225          by (auto dest: notStuck_SeqD2)
2226        with exec_res t' Seq.hyps
2227        show ?thesis
2228          by auto
2229      qed
2230    qed
2231  qed
2232next
2233  case CondTrue thus ?case
2234    by (auto intro: terminates.CondTrue dest: notStuck_CondTrueD)
2235next
2236  case CondFalse thus ?case
2237    by (auto intro: terminates.CondFalse dest: notStuck_CondFalseD)
2238next
2239  case (WhileTrue s b c)
2240  have s: "s \<in> b" by fact
2241  have not_Stuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>While b c,Normal s \<rangle> \<Rightarrow>\<notin>{Stuck}" by fact
2242  with WhileTrue have c_notStuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow>\<notin>{Stuck}"
2243    by (iprover intro:  notStuck_WhileTrueD1)
2244  show ?case
2245  proof (rule terminates.WhileTrue [OF s],safe)
2246    from c_notStuck
2247    show "\<Gamma>\<turnstile>c \<down> Normal s"
2248      by (rule WhileTrue.hyps)
2249  next
2250    fix s'
2251    assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> s'"
2252    show "\<Gamma>\<turnstile>While b c \<down> s'"
2253    proof -
2254      from exec_to_exec_restrict [OF exec] obtain t' where
2255        exec_res: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> t'" and
2256        t'_notStuck: "t' \<noteq> Stuck \<longrightarrow> t' = s'"
2257        by blast
2258      show ?thesis
2259      proof (cases "t'=Stuck")
2260        case True
2261        with c_notStuck exec_res have "False"
2262          by (auto simp add: final_notin_def)
2263        thus ?thesis ..
2264      next
2265        case False
2266        with t'_notStuck have t': "t'=s'" by simp
2267        with not_Stuck exec_res s
2268        have "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>While b c,s' \<rangle> \<Rightarrow>\<notin>{Stuck}"
2269          by (auto dest: notStuck_WhileTrueD2)
2270        with exec_res t' WhileTrue.hyps
2271        show ?thesis
2272          by auto
2273      qed
2274    qed
2275  qed
2276next
2277  case WhileFalse then show ?case by (iprover intro: terminates.WhileFalse)
2278next
2279  case Call thus ?case
2280    by (auto intro: terminates.Call dest: notStuck_CallD restrict_SomeD)
2281next
2282  case CallUndefined
2283  thus ?case
2284    by (auto dest: notStuck_CallDefinedD)
2285next
2286  case Stuck show ?case by (rule terminates.Stuck)
2287next
2288  case DynCom
2289  thus ?case
2290    by (auto intro: terminates.DynCom dest: notStuck_DynComD)
2291next
2292  case Throw show ?case by (rule terminates.Throw)
2293next
2294  case Abrupt show ?case by (rule terminates.Abrupt)
2295next
2296  case (Catch c1 s c2)
2297  have not_Stuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>Catch c1 c2,Normal s \<rangle> \<Rightarrow>\<notin>{Stuck}" by fact
2298  hence c1_notStuck: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow>\<notin>{Stuck}"
2299    by (rule notStuck_CatchD1)
2300  show "\<Gamma>\<turnstile>Catch c1 c2 \<down> Normal s"
2301  proof (rule terminates.Catch,safe)
2302    from c1_notStuck
2303    show "\<Gamma>\<turnstile>c1 \<down> Normal s"
2304      by (rule Catch.hyps)
2305  next
2306    fix s'
2307    assume exec: "\<Gamma>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> Abrupt s'"
2308    show "\<Gamma>\<turnstile>c2 \<down> Normal s'"
2309    proof -
2310      from exec_to_exec_restrict [OF exec] obtain t' where
2311        exec_res: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c1,Normal s \<rangle> \<Rightarrow> t'" and
2312        t'_notStuck: "t' \<noteq> Stuck \<longrightarrow> t' = Abrupt s'"
2313        by blast
2314      show ?thesis
2315      proof (cases "t'=Stuck")
2316        case True
2317        with c1_notStuck exec_res have "False"
2318          by (auto simp add: final_notin_def)
2319        thus ?thesis ..
2320      next
2321        case False
2322        with t'_notStuck have t': "t'=Abrupt s'" by simp
2323        with not_Stuck exec_res
2324        have "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c2,Normal s' \<rangle> \<Rightarrow>\<notin>{Stuck}"
2325          by (auto dest: notStuck_CatchD2)
2326        with exec_res t' Catch.hyps
2327        show ?thesis
2328          by auto
2329      qed
2330    qed
2331  qed
2332qed
2333
2334end
2335