1(*
2    Author:      Norbert Schirmer
3    Maintainer:  Norbert Schirmer, norbert.schirmer at web de
4    License:     LGPL
5*)
6
7(*  Title:      HoareTotalDef.thy
8    Author:     Norbert Schirmer, TU Muenchen
9
10Copyright (C) 2004-2008 Norbert Schirmer
11Some rights reserved, TU Muenchen
12
13This library is free software; you can redistribute it and/or modify
14it under the terms of the GNU Lesser General Public License as
15published by the Free Software Foundation; either version 2.1 of the
16License, or (at your option) any later version.
17
18This library is distributed in the hope that it will be useful, but
19WITHOUT ANY WARRANTY; without even the implied warranty of
20MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
21Lesser General Public License for more details.
22
23You should have received a copy of the GNU Lesser General Public
24License along with this library; if not, write to the Free Software
25Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
26USA
27*)
28
29section \<open>Hoare Logic for Total Correctness\<close>
30
31theory HoareTotalDef imports HoarePartialDef Termination begin
32
33subsection \<open>Validity of Hoare Tuples: \<open>\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A\<close>\<close>
34
35definition
36  validt :: "[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com,'s assn,'s assn] \<Rightarrow> bool"
37                ("_\<Turnstile>\<^sub>t\<^bsub>'/_\<^esub>/ _ _ _,_"  [61,60,1000, 20, 1000,1000] 60)
38where
39 "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<equiv> \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A \<and> (\<forall>s \<in> Normal ` P. \<Gamma>\<turnstile>c\<down>s)"
40
41definition
42  cvalidt::
43  "[('s,'p,'f) body,('s,'p) quadruple set,'f set,
44    's assn,('s,'p,'f) com,'s assn,'s assn] \<Rightarrow> bool"
45                ("_,_\<Turnstile>\<^sub>t\<^bsub>'/_\<^esub>/ _ _ _,_"  [61,60, 60,1000, 20, 1000,1000] 60)
46where
47 "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<equiv> (\<forall>(P,p,Q,A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A) \<longrightarrow> \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
48
49
50
51notation (ASCII)
52  validt  ("_|=t'/_/ _ _ _,_"  [61,60,1000, 20, 1000,1000] 60) and
53  cvalidt  ("_,_|=t'/_ / _ _ _,_"  [61,60,60,1000, 20, 1000,1000] 60)
54
55subsection \<open>Properties of Validity\<close>
56
57lemma validtI:
58 "\<lbrakk>\<And>s t. \<lbrakk>\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t;s \<in> P;t \<notin> Fault ` F\<rbrakk> \<Longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A;
59   \<And>s. s \<in> P \<Longrightarrow> \<Gamma>\<turnstile> c\<down>(Normal s) \<rbrakk>
60  \<Longrightarrow> \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
61  by (auto simp add: validt_def valid_def)
62
63lemma cvalidtI:
64 "\<lbrakk>\<And>s t. \<lbrakk>\<forall>(P,p,Q,A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A;\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t;s \<in> P;
65          t \<notin> Fault ` F\<rbrakk>
66          \<Longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A;
67   \<And>s. \<lbrakk>\<forall>(P,p,Q,A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A; s\<in>P\<rbrakk> \<Longrightarrow>  \<Gamma>\<turnstile>c\<down>(Normal s)\<rbrakk>
68  \<Longrightarrow> \<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
69  by (auto simp add: cvalidt_def validt_def valid_def)
70
71lemma cvalidt_postD:
72 "\<lbrakk>\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A; \<forall>(P,p,Q,A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A;\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> t;
73   s \<in> P;t \<notin> Fault ` F\<rbrakk>
74  \<Longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A"
75  by (simp add: cvalidt_def validt_def valid_def)
76
77lemma cvalidt_termD:
78 "\<lbrakk>\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A; \<forall>(P,p,Q,A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A;s \<in> P\<rbrakk>
79  \<Longrightarrow> \<Gamma>\<turnstile>c\<down>(Normal s)"
80  by (simp add: cvalidt_def validt_def valid_def)
81
82
83lemma validt_augment_Faults:
84  assumes valid:"\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
85  assumes F': "F \<subseteq> F'"
86  shows "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F'\<^esub> P c Q,A"
87  using valid F'
88  by (auto intro: valid_augment_Faults simp add: validt_def)
89
90subsection \<open>The Hoare Rules: \<open>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A\<close>\<close>
91
92inductive "hoaret"::"[('s,'p,'f) body,('s,'p) quadruple set,'f set,
93                        's assn,('s,'p,'f) com,'s assn,'s assn]
94                       => bool"
95    ("(3_,_/\<turnstile>\<^sub>t\<^bsub>'/_\<^esub> (_/ (_)/ _,_))" [61,60,60,1000,20,1000,1000]60)
96   for \<Gamma>::"('s,'p,'f) body"
97where
98  Skip: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> Q Skip Q,A"
99
100| Basic: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. f s \<in> Q} (Basic f) Q,A"
101
102| Spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. (\<forall>t. (s,t) \<in> r \<longrightarrow> t \<in> Q) \<and> (\<exists>t. (s,t) \<in> r)} (Spec r) Q,A"
103
104| Seq: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c\<^sub>1 R,A; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c\<^sub>2 Q,A\<rbrakk>
105        \<Longrightarrow>
106        \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Seq c\<^sub>1 c\<^sub>2 Q,A"
107
108| Cond: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P \<inter> b) c\<^sub>1 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P \<inter> - b) c\<^sub>2 Q,A\<rbrakk>
109         \<Longrightarrow>
110         \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Cond b c\<^sub>1 c\<^sub>2) Q,A"
111
112| While: "\<lbrakk>wf r; \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> P \<inter> b) c ({t. (t,\<sigma>)\<in>r} \<inter> P),A\<rbrakk>
113          \<Longrightarrow>
114          \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (While b c) (P \<inter> - b),A"
115
116| Guard: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> P) c Q,A
117          \<Longrightarrow>
118          \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> P) Guard f g c Q,A"
119
120| Guarantee: "\<lbrakk>f \<in> F; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> P) c Q,A\<rbrakk>
121              \<Longrightarrow>
122              \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Guard f g c) Q,A"
123
124| CallRec:
125  "\<lbrakk>(P,p,Q,A) \<in> Specs;
126    wf r;
127    Specs_wf = (\<lambda>p \<sigma>. (\<lambda>(P,q,Q,A). (P \<inter> {s. ((s,q),(\<sigma>,p)) \<in> r},q,Q,A)) ` Specs);
128    \<forall>(P,p,Q,A)\<in> Specs.
129      p \<in> dom \<Gamma> \<and> (\<forall>\<sigma>. \<Gamma>,\<Theta> \<union> Specs_wf p \<sigma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> P) (the (\<Gamma> p)) Q,A)
130    \<rbrakk>
131    \<Longrightarrow>
132    \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
133
134
135| DynCom:  "\<forall>s \<in> P. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (c s) Q,A
136            \<Longrightarrow>
137            \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (DynCom c) Q,A"
138
139
140| Throw: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> A Throw Q,A"
141
142| Catch: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c\<^sub>1 Q,R; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c\<^sub>2 Q,A\<rbrakk> \<Longrightarrow>  \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Catch c\<^sub>1 c\<^sub>2 Q,A"
143
144| Conseq: "\<forall>s \<in> P. \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q',A' \<and> s \<in> P' \<and> Q' \<subseteq> Q \<and> A' \<subseteq> A
145           \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
146
147
148| Asm: "(P,p,Q,A) \<in> \<Theta>
149        \<Longrightarrow>
150        \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A"
151
152| ExFalso: "\<lbrakk>\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A; \<not> \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
153  \<comment> \<open>This is a hack rule that enables us to derive completeness for
154        an arbitrary context \<open>\<Theta>\<close>, from completeness for an empty context.\<close>
155
156
157text \<open>Does not work, because of rule ExFalso, the context \<open>\<Theta>\<close> is to blame.
158 A weaker version with empty context can be derived from soundness
159 later on.\<close>
160lemma hoaret_to_hoarep:
161  assumes hoaret: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P p Q,A"
162  shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P p Q,A"
163using hoaret
164proof (induct)
165  case Skip thus ?case by (rule hoarep.intros)
166next
167  case Basic thus ?case by (rule hoarep.intros)
168next
169  case Seq thus ?case by - (rule hoarep.intros)
170next
171  case Cond thus ?case by - (rule hoarep.intros)
172next
173  case (While r \<Theta> F P b c A)
174  hence "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({\<sigma>} \<inter> P \<inter> b) c ({t. (t, \<sigma>) \<in> r} \<inter> P),A"
175    by iprover
176  hence "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P \<inter> b) c P,A"
177    by (rule HoarePartialDef.conseq) blast
178  then show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P While b c (P \<inter> - b),A"
179    by (rule hoarep.While)
180next
181  case Guard thus ?case by - (rule hoarep.intros)
182(*next
183  case (CallRec A F P Procs Q Z \<Theta>  p r)
184  hence hyp: "\<forall>p\<in>Procs. \<forall>\<tau> Z.
185           \<Gamma>,\<Theta> \<union> (\<Union>q\<in>Procs. \<Union>Z. {(P q Z \<inter> {s. ((s, q), \<tau>, p) \<in> r},
186                      Call q, Q q Z,A q Z)})\<turnstile>\<^bsub>/F\<^esub>
187              ({\<tau>} \<inter> P p Z) (the (\<Gamma> p)) (Q p Z),(A p Z)"
188    by blast
189  have "\<forall>p\<in>Procs. \<forall>Z.
190           \<Gamma>,\<Theta> \<union> (\<Union>q\<in>Procs. \<Union>Z. {(P q Z,
191                      Call q, Q q Z,A q Z)})\<turnstile>\<^bsub>/F\<^esub>
192              (P p Z) (the (\<Gamma> p)) (Q p Z),(A p Z)"
193  proof (intro ballI allI)
194    fix p Z
195    assume "p \<in> Procs"
196    with hyp
197    have hyp': "\<And> \<tau>.
198           \<Gamma>,\<Theta> \<union> (\<Union>q\<in>Procs. \<Union>Z. {(P q Z \<inter> {s. ((s, q), \<tau>, p) \<in> r},
199                      Call q, Q q Z, A q Z)})\<turnstile>\<^bsub>/F\<^esub>
200              ({\<tau>} \<inter> P p Z) (the (\<Gamma> p)) (Q p Z),(A p Z)"
201      by blast
202    have "\<forall>\<tau>.
203           \<Gamma>,\<Theta> \<union> (\<Union>q\<in>Procs. \<Union>Z. {(P q Z,
204                      Call q, Q q Z,A q Z)})\<turnstile>\<^bsub>/F\<^esub>
205              ({\<tau>} \<inter> P p Z) (the (\<Gamma> p)) (Q p Z),(A p Z)"
206      (is "\<forall>\<tau>. \<Gamma>,?\<Theta>'\<turnstile>\<^bsub>/F\<^esub> ({\<tau>} \<inter> P p Z) (the (\<Gamma> p)) (Q p Z),(A p Z)")
207    proof (rule allI, rule WeakenContext [OF hyp'],clarify)
208      fix \<tau> P' c Q' A'
209      assume "(P', c, Q', A') \<in> \<Theta> \<union>
210         (\<Union>q\<in>Procs.
211             \<Union>Z. {(P q Z \<inter> {s. ((s, q), \<tau>, p) \<in> r},
212                  Call q, Q q Z,
213                  A q Z)})" (is "(P', c, Q', A') \<in> \<Theta> \<union> ?Spec")
214      then show "\<Gamma>,?\<Theta>'\<turnstile>\<^bsub>/F\<^esub> P' c Q',A'"
215      proof (cases rule: UnE [consumes 1])
216        assume "(P',c,Q',A') \<in> \<Theta>"
217        then show ?thesis
218          by (blast intro: HoarePartialDef.Asm)
219      next
220        assume "(P',c,Q',A') \<in> ?Spec"
221        then show ?thesis
222        proof (clarify)
223          fix q Z
224          assume q: "q \<in> Procs"
225          show "\<Gamma>,?\<Theta>'\<turnstile>\<^bsub>/F\<^esub> (P q Z \<inter> {s. ((s, q), \<tau>, p) \<in> r})
226                         Call  q
227                        (Q q Z),(A q Z)"
228          proof -
229            from q
230            have "\<Gamma>,?\<Theta>'\<turnstile>\<^bsub>/F\<^esub> (P q Z) Call q (Q q Z),(A q Z)"
231              by - (rule HoarePartialDef.Asm,blast)
232            thus ?thesis
233              by (rule HoarePartialDef.conseqPre) blast
234          qed
235        qed
236      qed
237    qed
238    then show "\<Gamma>,\<Theta> \<union> (\<Union>q\<in>Procs. \<Union>Z. {(P q Z, Call q, Q q Z,A q Z)})
239                \<turnstile>\<^bsub>/F\<^esub> (P p Z) (the (\<Gamma> p)) (Q p Z),(A p Z)"
240      by (rule HoarePartialDef.conseq) blast
241  qed
242  thus ?case
243    by - (rule hoarep.CallRec)*)
244next
245  case DynCom thus ?case by (blast intro: hoarep.DynCom)
246next
247  case Throw thus ?case by - (rule hoarep.Throw)
248next
249  case Catch thus ?case by - (rule hoarep.Catch)
250next
251  case Conseq thus ?case by - (rule hoarep.Conseq,blast)
252next
253  case Asm thus ?case by (rule HoarePartialDef.Asm)
254next
255  case (ExFalso \<Theta> F P c Q A)
256  assume "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
257  hence "\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A"
258    oops
259
260
261lemma hoaret_augment_context:
262  assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P p Q,A"
263  shows "\<And>\<Theta>'. \<Theta> \<subseteq> \<Theta>' \<Longrightarrow> \<Gamma>,\<Theta>'\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P p Q,A"
264using deriv
265proof (induct)
266  case (CallRec P p Q A Specs r Specs_wf \<Theta> F \<Theta>')
267  have aug: "\<Theta> \<subseteq> \<Theta>'" by fact
268  then
269  have h: "\<And>\<tau> p. \<Theta> \<union> Specs_wf p \<tau>
270       \<subseteq> \<Theta>' \<union> Specs_wf p \<tau>"
271    by blast
272  have "\<forall>(P,p,Q,A)\<in>Specs. p \<in> dom \<Gamma> \<and>
273     (\<forall>\<tau>. \<Gamma>,\<Theta> \<union> Specs_wf p \<tau>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> P) (the (\<Gamma> p)) Q,A \<and>
274           (\<forall>x. \<Theta> \<union> Specs_wf p \<tau>
275                 \<subseteq> x \<longrightarrow>
276                 \<Gamma>,x\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> P) (the (\<Gamma> p)) Q,A))" by fact
277  hence "\<forall>(P,p,Q,A)\<in>Specs. p \<in> dom \<Gamma> \<and>
278         (\<forall>\<tau>. \<Gamma>,\<Theta>'\<union> Specs_wf p \<tau> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> P) (the (\<Gamma> p)) Q,A)"
279    apply (clarify)
280    apply (rename_tac P p Q A)
281    apply (drule (1) bspec)
282    apply (clarsimp)
283    apply (erule_tac x=\<tau> in allE)
284    apply clarify
285    apply (erule_tac x="\<Theta>' \<union> Specs_wf p \<tau>" in allE)
286    apply (insert aug)
287    apply auto
288    done
289  with CallRec show ?case by - (rule hoaret.CallRec)
290next
291  case DynCom thus ?case by (blast intro: hoaret.DynCom)
292next
293  case (Conseq P \<Theta> F c Q A \<Theta>')
294  from Conseq
295  have "\<forall>s \<in> P. (\<exists>P' Q' A'. (\<Gamma>,\<Theta>' \<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q',A') \<and> s \<in> P'\<and> Q' \<subseteq> Q \<and> A' \<subseteq> A)"
296    by blast
297  with Conseq show ?case by - (rule hoaret.Conseq)
298next
299  case (ExFalso \<Theta> F P  c Q A \<Theta>')
300  have "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" "\<not> \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" "\<Theta> \<subseteq> \<Theta>'"  by fact+
301  then show ?case
302    by (fastforce intro: hoaret.ExFalso simp add: cvalidt_def)
303qed (blast intro: hoaret.intros)+
304
305subsection \<open>Some Derived Rules\<close>
306
307
308lemma  Conseq': "\<forall>s. s \<in> P \<longrightarrow>
309            (\<exists>P' Q' A'.
310              (\<forall> Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)) \<and>
311                    (\<exists>Z. s \<in> P' Z \<and> (Q' Z \<subseteq> Q) \<and> (A' Z \<subseteq> A)))
312           \<Longrightarrow>
313           \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
314apply (rule Conseq)
315apply (rule ballI)
316apply (erule_tac x=s in allE)
317apply (clarify)
318apply (rule_tac x="P' Z" in exI)
319apply (rule_tac x="Q' Z" in exI)
320apply (rule_tac x="A' Z" in exI)
321apply blast
322done
323
324lemma conseq:"\<lbrakk>\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z);
325              \<forall>s. s \<in> P \<longrightarrow> (\<exists> Z. s\<in>P' Z \<and> (Q' Z \<subseteq> Q)\<and> (A' Z \<subseteq> A))\<rbrakk>
326              \<Longrightarrow>
327              \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
328  by (rule Conseq) blast
329
330theorem conseqPrePost:
331  "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q',A' \<Longrightarrow> P \<subseteq> P' \<Longrightarrow>  Q' \<subseteq> Q \<Longrightarrow> A' \<subseteq> A \<Longrightarrow>  \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
332  by (rule conseq [where ?P'="\<lambda>Z. P'" and ?Q'="\<lambda>Z. Q'"]) auto
333
334lemma conseqPre: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q,A \<Longrightarrow> P \<subseteq> P' \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
335by (rule conseq) auto
336
337lemma conseqPost: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q',A'\<Longrightarrow> Q' \<subseteq> Q \<Longrightarrow> A' \<subseteq> A \<Longrightarrow>   \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
338  by (rule conseq) auto
339
340
341lemma Spec_wf_conv:
342  "(\<lambda>(P, q, Q, A). (P \<inter> {s. ((s, q), \<tau>, p) \<in> r}, q, Q, A)) `
343                (\<Union>p\<in>Procs. \<Union>Z. {(P p Z, p, Q p Z, A p Z)}) =
344        (\<Union>q\<in>Procs. \<Union>Z. {(P q Z \<inter> {s. ((s, q), \<tau>, p) \<in> r}, q, Q q Z, A q Z)})"
345  by (auto intro!: image_eqI)
346
347lemma CallRec':
348  "\<lbrakk>p\<in>Procs; Procs \<subseteq> dom \<Gamma>;
349    wf r;
350   \<forall>p\<in>Procs. \<forall>\<tau> Z.
351   \<Gamma>,\<Theta>\<union>(\<Union>q\<in>Procs. \<Union>Z.
352    {((P q Z) \<inter> {s. ((s,q),(\<tau>,p)) \<in> r},q,Q q Z,(A q Z))})
353     \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> (P p Z)) (the (\<Gamma> p)) (Q p Z),(A p Z)\<rbrakk>
354   \<Longrightarrow>
355   \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P p Z) (Call p) (Q p Z),(A p Z)"
356apply (rule CallRec [where Specs="\<Union>p\<in>Procs. \<Union>Z. {((P p Z),p,Q p Z,A p Z)}" and
357         r=r])
358apply    blast
359apply   assumption
360apply  (rule refl)
361apply (clarsimp)
362apply (rename_tac p')
363apply (rule conjI)
364apply  blast
365apply (intro allI)
366apply (rename_tac Z \<tau>)
367apply (drule_tac x=p' in bspec, assumption)
368apply (erule_tac x=\<tau> in allE)
369apply (erule_tac x=Z in allE)
370apply (fastforce simp add: Spec_wf_conv)
371done
372
373end
374
375