1(* 2 Author: Norbert Schirmer 3 Maintainer: Norbert Schirmer, norbert.schirmer at web de 4 License: LGPL 5*) 6 7(* Title: HoarePartialDef.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 Partial Correctness\<close> 30theory HoarePartialDef imports Semantic begin 31 32type_synonym ('s,'p) quadruple = "('s assn \<times> 'p \<times> 's assn \<times> 's assn)" 33 34subsection \<open>Validity of Hoare Tuples: \<open>\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A\<close>\<close> 35 36definition 37 valid :: "[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com,'s assn,'s assn] => bool" 38 ("_\<Turnstile>\<^bsub>'/_\<^esub>/ _ _ _,_" [61,60,1000, 20, 1000,1000] 60) 39where 40 "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A \<equiv> \<forall>s t. \<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F 41 \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A" 42 43definition 44 cvalid:: 45 "[('s,'p,'f) body,('s,'p) quadruple set,'f set, 46 's assn,('s,'p,'f) com,'s assn,'s assn] =>bool" 47 ("_,_\<Turnstile>\<^bsub>'/_\<^esub>/ _ _ _,_" [61,60,60,1000, 20, 1000,1000] 60) 48where 49 "\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A \<equiv> (\<forall>(P,p,Q,A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A) \<longrightarrow> \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 50 51 52definition 53 nvalid :: "[('s,'p,'f) body,nat,'f set, 54 's assn,('s,'p,'f) com,'s assn,'s assn] => bool" 55 ("_\<Turnstile>_:\<^bsub>'/_\<^esub>/ _ _ _,_" [61,60,60,1000, 20, 1000,1000] 60) 56where 57 "\<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A \<equiv> \<forall>s t. \<Gamma>\<turnstile>\<langle>c,s \<rangle> =n\<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F 58 \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A" 59 60 61definition 62 cnvalid:: 63 "[('s,'p,'f) body,('s,'p) quadruple set,nat,'f set, 64 's assn,('s,'p,'f) com,'s assn,'s assn] \<Rightarrow> bool" 65 ("_,_\<Turnstile>_:\<^bsub>'/_\<^esub>/ _ _ _,_" [61,60,60,60,1000, 20, 1000,1000] 60) 66where 67 "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A \<equiv> (\<forall>(P,p,Q,A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A) \<longrightarrow> \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 68 69 70notation (ASCII) 71 valid ("_|='/_/ _ _ _,_" [61,60,1000, 20, 1000,1000] 60) and 72 cvalid ("_,_|='/_/ _ _ _,_" [61,60,60,1000, 20, 1000,1000] 60) and 73 nvalid ("_|=_:'/_/ _ _ _,_" [61,60,60,1000, 20, 1000,1000] 60) and 74 cnvalid ("_,_|=_:'/_/ _ _ _,_" [61,60,60,60,1000, 20, 1000,1000] 60) 75 76 77subsection \<open>Properties of Validity\<close> 78 79lemma valid_iff_nvalid: "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A = (\<forall>n. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A)" 80 apply (simp only: valid_def nvalid_def exec_iff_execn ) 81 apply (blast dest: exec_final_notin_to_execn) 82 done 83 84lemma cnvalid_to_cvalid: "(\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A) \<Longrightarrow> \<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 85 apply (unfold cvalid_def cnvalid_def valid_iff_nvalid [THEN eq_reflection]) 86 apply fast 87 done 88 89lemma nvalidI: 90 "\<lbrakk>\<And>s t. \<lbrakk>\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> =n\<Rightarrow> t;s \<in> P; t\<notin> Fault ` F\<rbrakk> \<Longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A\<rbrakk> 91 \<Longrightarrow> \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 92 by (auto simp add: nvalid_def) 93 94lemma validI: 95 "\<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\<rbrakk> 96 \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 97 by (auto simp add: valid_def) 98 99lemma cvalidI: 100 "\<lbrakk>\<And>s t. \<lbrakk>\<forall>(P,p,Q,A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A;\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t;s \<in> P;t\<notin>Fault ` F\<rbrakk> 101 \<Longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A\<rbrakk> 102 \<Longrightarrow> \<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 103 by (auto simp add: cvalid_def valid_def) 104 105lemma cvalidD: 106 "\<lbrakk>\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A;\<forall>(P,p,Q,A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A;\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t;s \<in> P;t\<notin>Fault ` F\<rbrakk> 107 \<Longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A" 108 by (auto simp add: cvalid_def valid_def) 109 110lemma cnvalidI: 111 "\<lbrakk>\<And>s t. \<lbrakk>\<forall>(P,p,Q,A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A; 112 \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> =n\<Rightarrow> t;s \<in> P;t\<notin>Fault ` F\<rbrakk> 113 \<Longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A\<rbrakk> 114 \<Longrightarrow> \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 115 by (auto simp add: cnvalid_def nvalid_def) 116 117 118lemma cnvalidD: 119 "\<lbrakk>\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A;\<forall>(P,p,Q,A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A; 120 \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> =n\<Rightarrow> t;s \<in> P; 121 t\<notin>Fault ` F\<rbrakk> 122 \<Longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A" 123 by (auto simp add: cnvalid_def nvalid_def) 124 125lemma nvalid_augment_Faults: 126 assumes validn:"\<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 127 assumes F': "F \<subseteq> F'" 128 shows "\<Gamma>\<Turnstile>n:\<^bsub>/F'\<^esub> P c Q,A" 129proof (rule nvalidI) 130 fix s t 131 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> =n\<Rightarrow> t" 132 assume P: "s \<in> P" 133 assume F: "t \<notin> Fault ` F'" 134 with F' have "t \<notin> Fault ` F" 135 by blast 136 with exec P validn 137 show "t \<in> Normal ` Q \<union> Abrupt ` A" 138 by (auto simp add: nvalid_def) 139qed 140 141lemma valid_augment_Faults: 142 assumes validn:"\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 143 assumes F': "F \<subseteq> F'" 144 shows "\<Gamma>\<Turnstile>\<^bsub>/F'\<^esub> P c Q,A" 145proof (rule validI) 146 fix s t 147 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> t" 148 assume P: "s \<in> P" 149 assume F: "t \<notin> Fault ` F'" 150 with F' have "t \<notin> Fault ` F" 151 by blast 152 with exec P validn 153 show "t \<in> Normal ` Q \<union> Abrupt ` A" 154 by (auto simp add: valid_def) 155qed 156 157lemma nvalid_to_nvalid_strip: 158 assumes validn:"\<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 159 assumes F': "F' \<subseteq> -F" 160 shows "strip F' \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 161proof (rule nvalidI) 162 fix s t 163 assume exec_strip: "strip F' \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> =n\<Rightarrow> t" 164 assume P: "s \<in> P" 165 assume F: "t \<notin> Fault ` F" 166 from exec_strip obtain t' where 167 exec: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> =n\<Rightarrow> t'" and 168 t': "t' \<in> Fault ` (-F') \<longrightarrow> t'=t" "\<not> isFault t' \<longrightarrow> t'=t" 169 by (blast dest: execn_strip_to_execn) 170 show "t \<in> Normal ` Q \<union> Abrupt ` A" 171 proof (cases "t' \<in> Fault ` F") 172 case True 173 with t' F F' have False 174 by blast 175 thus ?thesis .. 176 next 177 case False 178 with exec P validn 179 have *: "t' \<in> Normal ` Q \<union> Abrupt ` A" 180 by (auto simp add: nvalid_def) 181 with t' have "t'=t" 182 by auto 183 with * show ?thesis 184 by simp 185 qed 186qed 187 188 189lemma valid_to_valid_strip: 190 assumes valid:"\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 191 assumes F': "F' \<subseteq> -F" 192 shows "strip F' \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 193proof (rule validI) 194 fix s t 195 assume exec_strip: "strip F' \<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> t" 196 assume P: "s \<in> P" 197 assume F: "t \<notin> Fault ` F" 198 from exec_strip obtain t' where 199 exec: "\<Gamma>\<turnstile>\<langle>c,Normal s \<rangle> \<Rightarrow> t'" and 200 t': "t' \<in> Fault ` (-F') \<longrightarrow> t'=t" "\<not> isFault t' \<longrightarrow> t'=t" 201 by (blast dest: exec_strip_to_exec) 202 show "t \<in> Normal ` Q \<union> Abrupt ` A" 203 proof (cases "t' \<in> Fault ` F") 204 case True 205 with t' F F' have False 206 by blast 207 thus ?thesis .. 208 next 209 case False 210 with exec P valid 211 have *: "t' \<in> Normal ` Q \<union> Abrupt ` A" 212 by (auto simp add: valid_def) 213 with t' have "t'=t" 214 by auto 215 with * show ?thesis 216 by simp 217 qed 218qed 219 220 221subsection \<open>The Hoare Rules: \<open>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A\<close>\<close> 222 223lemma mono_WeakenContext: "A \<subseteq> B \<Longrightarrow> 224 (\<lambda>(P, c, Q, A'). (\<Gamma>, \<Theta>, F, P, c, Q, A') \<in> A) x \<longrightarrow> 225 (\<lambda>(P, c, Q, A'). (\<Gamma>, \<Theta>, F, P, c, Q, A') \<in> B) x" 226apply blast 227done 228 229 230inductive "hoarep"::"[('s,'p,'f) body,('s,'p) quadruple set,'f set, 231 's assn,('s,'p,'f) com, 's assn,'s assn] => bool" 232 ("(3_,_/\<turnstile>\<^bsub>'/_ \<^esub>(_/ (_)/ _,/_))" [60,60,60,1000,20,1000,1000]60) 233 for \<Gamma>::"('s,'p,'f) body" 234where 235 Skip: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> Q Skip Q,A" 236 237| Basic: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. f s \<in> Q} (Basic f) Q,A" 238 239| Spec: "\<Gamma>,\<Theta>\<turnstile>\<^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" 240 241| Seq: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>1 R,A; \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> R c\<^sub>2 Q,A\<rbrakk> 242 \<Longrightarrow> 243 \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (Seq c\<^sub>1 c\<^sub>2) Q,A" 244 245| Cond: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P \<inter> b) c\<^sub>1 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P \<inter> - b) c\<^sub>2 Q,A\<rbrakk> 246 \<Longrightarrow> 247 \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (Cond b c\<^sub>1 c\<^sub>2) Q,A" 248 249| While: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P \<inter> b) c P,A 250 \<Longrightarrow> 251 \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (While b c) (P \<inter> - b),A" 252 253| Guard: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (g \<inter> P) c Q,A 254 \<Longrightarrow> 255 \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (g \<inter> P) (Guard f g c) Q,A" 256 257| Guarantee: "\<lbrakk>f \<in> F; \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (g \<inter> P) c Q,A\<rbrakk> 258 \<Longrightarrow> 259 \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (Guard f g c) Q,A" 260 261| CallRec: 262 "\<lbrakk>(P,p,Q,A) \<in> Specs; 263 \<forall>(P,p,Q,A) \<in> Specs. p \<in> dom \<Gamma> \<and> \<Gamma>,\<Theta>\<union>Specs\<turnstile>\<^bsub>/F\<^esub> P (the (\<Gamma> p)) Q,A \<rbrakk> 264 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" 265 266| DynCom: 267 "\<forall>s \<in> P. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (c s) Q,A 268 \<Longrightarrow> 269 \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (DynCom c) Q,A" 270 271| Throw: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> A Throw Q,A" 272 273| Catch: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>1 Q,R; \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> R c\<^sub>2 Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P Catch c\<^sub>1 c\<^sub>2 Q,A" 274 275| Conseq: "\<forall>s \<in> P. \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' c Q',A' \<and> s \<in> P' \<and> Q' \<subseteq> Q \<and> A' \<subseteq> A 276 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 277 278 279| Asm: "\<lbrakk>(P,p,Q,A) \<in> \<Theta>\<rbrakk> 280 \<Longrightarrow> 281 \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" 282 283 284| ExFalso: "\<lbrakk>\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A; \<not> \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 285 \<comment> \<open>This is a hack rule that enables us to derive completeness for 286 an arbitrary context \<open>\<Theta>\<close>, from completeness for an empty context.\<close> 287 288 289 290text \<open>Does not work, because of rule ExFalso, the context \<open>\<Theta>\<close> is to blame. 291 A weaker version with empty context can be derived from soundness 292 and completeness later on.\<close> 293lemma hoare_strip_\<Gamma>: 294 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P p Q,A" 295 shows "strip (-F) \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P p Q,A" 296using deriv 297proof induct 298 case Skip thus ?case by (iprover intro: hoarep.Skip) 299next 300 case Basic thus ?case by (iprover intro: hoarep.Basic) 301next 302 case Spec thus ?case by (iprover intro: hoarep.Spec) 303next 304 case Seq thus ?case by (iprover intro: hoarep.Seq) 305next 306 case Cond thus ?case by (iprover intro: hoarep.Cond) 307next 308 case While thus ?case by (iprover intro: hoarep.While) 309next 310 case Guard thus ?case by (iprover intro: hoarep.Guard) 311(*next 312 case CallSpec thus ?case by (iprover intro: hoarep.CallSpec) 313next 314 case (CallRec A Abr Abr' Init P Post Pre Procs Q R Result Return Z \<Gamma> \<Theta> init p 315 result return ) 316 from CallRec.hyps 317 have "\<forall>p\<in>Procs. \<forall>Z. (strip \<Gamma>),\<Theta> \<union> 318 (\<Union>\<^bsub>p\<in>Procs\<^esub> 319 \<Union>\<^bsub>Z\<^esub> {(Pre p Z, Call (Init p) p (Return p) (Result p), 320 Post p Z, Abr p Z)})\<turnstile> 321 (Pre p Z) (the (\<Gamma> p)) (R p Z),(Abr' p Z)" by blast 322 hence "\<forall>p\<in>Procs. \<forall>Z. (strip \<Gamma>),\<Theta> \<union> 323 (\<Union>\<^bsub>p\<in>Procs\<^esub> 324 \<Union>\<^bsub>Z\<^esub> {(Pre p Z, Call (Init p) p (Return p) (Result p), 325 Post p Z, Abr p Z)})\<turnstile> 326 (Pre p Z) (the ((strip \<Gamma>) p)) (R p Z),(Abr' p Z)" 327 by (auto intro: hoarep.StripI) 328 then show ?case 329 apply - 330 apply (rule hoarep.CallRec) 331 apply (assumption | simp only:dom_strip)+ 332 done*) 333next 334 case DynCom 335 thus ?case 336 by - (rule hoarep.DynCom,best elim!: ballE exE) 337next 338 case Throw thus ?case by (iprover intro: hoarep.Throw) 339next 340 case Catch thus ?case by (iprover intro: hoarep.Catch) 341(*next 342 case CONSEQ thus ?case apply (auto intro: hoarep.CONSEQ)*) 343next 344 case Asm thus ?case by (iprover intro: hoarep.Asm) 345next 346 case ExFalso 347 thus ?case 348 oops 349 350lemma hoare_augment_context: 351 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P p Q,A" 352 shows "\<And>\<Theta>'. \<Theta> \<subseteq> \<Theta>' \<Longrightarrow> \<Gamma>,\<Theta>'\<turnstile>\<^bsub>/F\<^esub> P p Q,A" 353using deriv 354proof (induct) 355 case CallRec 356 case (CallRec P p Q A Specs \<Theta> F \<Theta>') 357 from CallRec.prems 358 have "\<Theta>\<union>Specs 359 \<subseteq> \<Theta>'\<union>Specs" 360 by blast 361 with CallRec.hyps (2) 362 have "\<forall>(P,p,Q,A)\<in>Specs. p \<in> dom \<Gamma> \<and> \<Gamma>,\<Theta>'\<union>Specs \<turnstile>\<^bsub>/F\<^esub> P (the (\<Gamma> p)) Q,A" 363 by fastforce 364 365 with CallRec show ?case by - (rule hoarep.CallRec) 366next 367 case DynCom thus ?case by (blast intro: hoarep.DynCom) 368next 369 case (Conseq P \<Theta> F c Q A \<Theta>') 370 from Conseq 371 have "\<forall>s \<in> P. 372 (\<exists>P' Q' A'. \<Gamma>,\<Theta>' \<turnstile>\<^bsub>/F\<^esub> P' c Q',A' \<and> s \<in> P' \<and> Q' \<subseteq> Q \<and> A' \<subseteq> A)" 373 by blast 374 with Conseq show ?case by - (rule hoarep.Conseq) 375next 376 case (ExFalso \<Theta> F P c Q A \<Theta>') 377 have valid_ctxt: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" "\<Theta> \<subseteq> \<Theta>'" by fact+ 378 hence "\<forall>n. \<Gamma>,\<Theta>'\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 379 by (simp add: cnvalid_def) blast 380 moreover have invalid: "\<not> \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" by fact 381 ultimately show ?case 382 by (rule hoarep.ExFalso) 383qed (blast intro: hoarep.intros)+ 384 385 386subsection \<open>Some Derived Rules\<close> 387 388lemma Conseq': "\<forall>s. s \<in> P \<longrightarrow> 389 (\<exists>P' Q' A'. 390 (\<forall> Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)) \<and> 391 (\<exists>Z. s \<in> P' Z \<and> (Q' Z \<subseteq> Q) \<and> (A' Z \<subseteq> A))) 392 \<Longrightarrow> 393 \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 394apply (rule Conseq) 395apply (rule ballI) 396apply (erule_tac x=s in allE) 397apply (clarify) 398apply (rule_tac x="P' Z" in exI) 399apply (rule_tac x="Q' Z" in exI) 400apply (rule_tac x="A' Z" in exI) 401apply blast 402done 403 404lemma conseq:"\<lbrakk>\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z); 405 \<forall>s. s \<in> P \<longrightarrow> (\<exists> Z. s\<in>P' Z \<and> (Q' Z \<subseteq> Q) \<and> (A' Z \<subseteq> A))\<rbrakk> 406 \<Longrightarrow> 407 \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 408 by (rule Conseq) blast 409 410theorem conseqPrePost [trans]: 411 "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' c Q',A' \<Longrightarrow> P \<subseteq> P' \<Longrightarrow> Q' \<subseteq> Q \<Longrightarrow> A' \<subseteq> A \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 412 by (rule conseq [where ?P'="\<lambda>Z. P'" and ?Q'="\<lambda>Z. Q'"]) auto 413 414lemma conseqPre [trans]: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' c Q,A \<Longrightarrow> P \<subseteq> P' \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 415by (rule conseq) auto 416 417lemma conseqPost [trans]: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q',A' \<Longrightarrow> Q' \<subseteq> Q \<Longrightarrow> A' \<subseteq> A 418 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 419 by (rule conseq) auto 420 421 422lemma CallRec': 423 "\<lbrakk>p\<in>Procs; Procs \<subseteq> dom \<Gamma>; 424 \<forall>p\<in>Procs. 425 \<forall>Z. \<Gamma>,\<Theta> \<union> (\<Union>p\<in>Procs. \<Union>Z. {((P p Z),p,Q p Z,A p Z)}) 426 \<turnstile>\<^bsub>/F\<^esub> (P p Z) (the (\<Gamma> p)) (Q p Z),(A p Z)\<rbrakk> 427 \<Longrightarrow> 428 \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P p Z) (Call p) (Q p Z),(A p Z)" 429apply (rule CallRec [where Specs="\<Union>p\<in>Procs. \<Union>Z. {((P p Z),p,Q p Z,A p Z)}"]) 430apply blast 431apply blast 432done 433 434end 435