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