1(* 2 Author: Norbert Schirmer 3 Maintainer: Norbert Schirmer, norbert.schirmer at web de 4 License: LGPL 5*) 6 7(* Title: HoareTotal.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>Derived Hoare Rules for Total Correctness\<close> 30 31theory HoareTotal imports HoareTotalProps begin 32 33lemma conseq_no_aux: 34 "\<lbrakk>\<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q',A'; 35 \<forall>s. s \<in> P \<longrightarrow> (s\<in>P' \<and> (Q' \<subseteq> Q)\<and> (A' \<subseteq> A))\<rbrakk> 36 \<Longrightarrow> 37 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 38 by (rule conseq [where P'="\<lambda>Z. P'" and Q'="\<lambda>Z. Q'" and A'="\<lambda>Z. A'"]) auto 39 40text \<open>If for example a specification for a "procedure pointer" parameter 41is in the precondition we can extract it with this rule\<close> 42lemma conseq_exploit_pre: 43 "\<lbrakk>\<forall>s \<in> P. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s} \<inter> P) c Q,A\<rbrakk> 44 \<Longrightarrow> 45 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 46 apply (rule Conseq) 47 apply clarify 48 apply (rule_tac x="{s} \<inter> P" in exI) 49 apply (rule_tac x="Q" in exI) 50 apply (rule_tac x="A" in exI) 51 by simp 52 53 54lemma conseq:"\<lbrakk>\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z); 55 \<forall>s. s \<in> P \<longrightarrow> (\<exists> Z. s\<in>P' Z \<and> (Q' Z \<subseteq> Q)\<and> (A' Z \<subseteq> A))\<rbrakk> 56 \<Longrightarrow> 57 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 58 by (rule Conseq') blast 59 60 61lemma Lem:"\<lbrakk>\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z); 62 P \<subseteq> {s. \<exists> Z. s\<in>P' Z \<and> (Q' Z \<subseteq> Q) \<and> (A' Z \<subseteq> A)}\<rbrakk> 63 \<Longrightarrow> 64 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (lem x c) Q,A" 65 apply (unfold lem_def) 66 apply (erule conseq) 67 apply blast 68 done 69 70 71lemma LemAnno: 72assumes conseq: "P \<subseteq> {s. \<exists>Z. s\<in>P' Z \<and> 73 (\<forall>t. t \<in> Q' Z \<longrightarrow> t \<in> Q) \<and> (\<forall>t. t \<in> A' Z \<longrightarrow> t \<in> A)}" 74assumes lem: "\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)" 75shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (lem x c) Q,A" 76 apply (rule Lem [OF lem]) 77 using conseq 78 by blast 79 80lemma LemAnnoNoAbrupt: 81assumes conseq: "P \<subseteq> {s. \<exists>Z. s\<in>P' Z \<and> (\<forall>t. t \<in> Q' Z \<longrightarrow> t \<in> Q)}" 82assumes lem: "\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) c (Q' Z),{}" 83shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (lem x c) Q,{}" 84 apply (rule Lem [OF lem]) 85 using conseq 86 by blast 87 88lemma TrivPost: "\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z) 89 \<Longrightarrow> 90 \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) c UNIV,UNIV" 91apply (rule allI) 92apply (erule conseq) 93apply auto 94done 95 96lemma TrivPostNoAbr: "\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) c (Q' Z),{} 97 \<Longrightarrow> 98 \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) c UNIV,{}" 99apply (rule allI) 100apply (erule conseq) 101apply auto 102done 103 104lemma DynComConseq: 105 assumes "P \<subseteq> {s. \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>P' (c s) Q',A' \<and> P \<subseteq> P' \<and> Q' \<subseteq> Q \<and> A' \<subseteq> A}" 106 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>P DynCom c Q,A" 107 using assms 108 apply - 109 apply (rule hoaret.DynCom) 110 apply clarsimp 111 apply (rule hoaret.Conseq) 112 apply clarsimp 113 apply blast 114 done 115 116lemma SpecAnno: 117 assumes consequence: "P \<subseteq> {s. (\<exists> Z. s\<in>P' Z \<and> (Q' Z \<subseteq> Q) \<and> (A' Z \<subseteq> A))}" 118 assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) (c Z) (Q' Z),(A' Z)" 119 assumes bdy_constant: "\<forall>Z. c Z = c undefined" 120 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (specAnno P' c Q' A') Q,A" 121proof - 122 from spec bdy_constant 123 have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) (c undefined) (Q' Z),(A' Z)" 124 apply - 125 apply (rule allI) 126 apply (erule_tac x=Z in allE) 127 apply (erule_tac x=Z in allE) 128 apply simp 129 done 130 with consequence show ?thesis 131 apply (simp add: specAnno_def) 132 apply (erule conseq) 133 apply blast 134 done 135qed 136 137 138 139lemma SpecAnno': 140 "\<lbrakk>P \<subseteq> {s. \<exists> Z. s\<in>P' Z \<and> 141 (\<forall>t. t \<in> Q' Z \<longrightarrow> t \<in> Q) \<and> (\<forall>t. t \<in> A' Z \<longrightarrow> t \<in> A)}; 142 \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) (c Z) (Q' Z),(A' Z); 143 \<forall>Z. c Z = c undefined 144 \<rbrakk> \<Longrightarrow> 145 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (specAnno P' c Q' A') Q,A" 146apply (simp only: subset_iff [THEN sym]) 147apply (erule (1) SpecAnno) 148apply assumption 149done 150 151lemma SpecAnnoNoAbrupt: 152 "\<lbrakk>P \<subseteq> {s. \<exists> Z. s\<in>P' Z \<and> 153 (\<forall>t. t \<in> Q' Z \<longrightarrow> t \<in> Q)}; 154 \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) (c Z) (Q' Z),{}; 155 \<forall>Z. c Z = c undefined 156 \<rbrakk> \<Longrightarrow> 157 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (specAnno P' c Q' (\<lambda>s. {})) Q,A" 158apply (rule SpecAnno') 159apply auto 160done 161 162lemma Skip: "P \<subseteq> Q \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Skip Q,A" 163 by (rule hoaret.Skip [THEN conseqPre],simp) 164 165lemma Basic: "P \<subseteq> {s. (f s) \<in> Q} \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Basic f) Q,A" 166 by (rule hoaret.Basic [THEN conseqPre]) 167 168lemma BasicCond: 169 "\<lbrakk>P \<subseteq> {s. (b s \<longrightarrow> f s\<in>Q) \<and> (\<not> b s \<longrightarrow> g s\<in>Q)}\<rbrakk> \<Longrightarrow> 170 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Basic (\<lambda>s. if b s then f s else g s) Q,A" 171 apply (rule Basic) 172 apply auto 173 done 174 175lemma Spec: "P \<subseteq> {s. (\<forall>t. (s,t) \<in> r \<longrightarrow> t \<in> Q) \<and> (\<exists>t. (s,t) \<in> r)} 176 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Spec r) Q,A" 177by (rule hoaret.Spec [THEN conseqPre]) 178 179lemma SpecIf: 180 "\<lbrakk>P \<subseteq> {s. (b s \<longrightarrow> f s \<in> Q) \<and> (\<not> b s \<longrightarrow> g s \<in> Q \<and> h s \<in> Q)}\<rbrakk> \<Longrightarrow> 181 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Spec (if_rel b f g h) Q,A" 182 apply (rule Spec) 183 apply (auto simp add: if_rel_def) 184 done 185 186lemma Seq [trans, intro?]: 187 "\<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> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Seq c\<^sub>1 c\<^sub>2 Q,A" 188 by (rule hoaret.Seq) 189 190lemma SeqSwap: 191 "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c2 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c1 R,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Seq c1 c2 Q,A" 192 by (rule Seq) 193 194lemma BSeq: 195 "\<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> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (bseq c\<^sub>1 c\<^sub>2) Q,A" 196 by (unfold bseq_def) (rule Seq) 197 198lemma Cond: 199 assumes wp: "P \<subseteq> {s. (s\<in>b \<longrightarrow> s\<in>P\<^sub>1) \<and> (s\<notin>b \<longrightarrow> s\<in>P\<^sub>2)}" 200 assumes deriv_c1: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P\<^sub>1 c\<^sub>1 Q,A" 201 assumes deriv_c2: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P\<^sub>2 c\<^sub>2 Q,A" 202 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Cond b c\<^sub>1 c\<^sub>2) Q,A" 203proof (rule hoaret.Cond [THEN conseqPre]) 204 from deriv_c1 205 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. (s \<in> b \<longrightarrow> s \<in> P\<^sub>1) \<and> (s \<notin> b \<longrightarrow> s \<in> P\<^sub>2)} \<inter> b) c\<^sub>1 Q,A" 206 by (rule conseqPre) blast 207next 208 from deriv_c2 209 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. (s \<in> b \<longrightarrow> s \<in> P\<^sub>1) \<and> (s \<notin> b \<longrightarrow> s \<in> P\<^sub>2)} \<inter> - b) c\<^sub>2 Q,A" 210 by (rule conseqPre) blast 211qed (insert wp) 212 213 214lemma CondSwap: 215 "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P1 c1 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P2 c2 Q,A; 216 P \<subseteq> {s. (s\<in>b \<longrightarrow> s\<in>P1) \<and> (s\<notin>b \<longrightarrow> s\<in>P2)}\<rbrakk> 217 \<Longrightarrow> 218 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Cond b c1 c2) Q,A" 219 by (rule Cond) 220 221lemma Cond': 222 "\<lbrakk>P \<subseteq> {s. (b \<subseteq> P1) \<and> (- b \<subseteq> P2)};\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P1 c1 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P2 c2 Q,A\<rbrakk> 223 \<Longrightarrow> 224 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Cond b c1 c2) Q,A" 225 by (rule CondSwap) blast+ 226 227lemma CondInv: 228 assumes wp: "P \<subseteq> Q" 229 assumes inv: "Q \<subseteq> {s. (s\<in>b \<longrightarrow> s\<in>P\<^sub>1) \<and> (s\<notin>b \<longrightarrow> s\<in>P\<^sub>2)}" 230 assumes deriv_c1: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P\<^sub>1 c\<^sub>1 Q,A" 231 assumes deriv_c2: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P\<^sub>2 c\<^sub>2 Q,A" 232 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Cond b c\<^sub>1 c\<^sub>2) Q,A" 233proof - 234 from wp inv 235 have "P \<subseteq> {s. (s\<in>b \<longrightarrow> s\<in>P\<^sub>1) \<and> (s\<notin>b \<longrightarrow> s\<in>P\<^sub>2)}" 236 by blast 237 from Cond [OF this deriv_c1 deriv_c2] 238 show ?thesis . 239qed 240 241lemma CondInv': 242 assumes wp: "P \<subseteq> I" 243 assumes inv: "I \<subseteq> {s. (s\<in>b \<longrightarrow> s\<in>P\<^sub>1) \<and> (s\<notin>b \<longrightarrow> s\<in>P\<^sub>2)}" 244 assumes wp': "I \<subseteq> Q" 245 assumes deriv_c1: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P\<^sub>1 c\<^sub>1 I,A" 246 assumes deriv_c2: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P\<^sub>2 c\<^sub>2 I,A" 247 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Cond b c\<^sub>1 c\<^sub>2) Q,A" 248proof - 249 from CondInv [OF wp inv deriv_c1 deriv_c2] 250 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Cond b c\<^sub>1 c\<^sub>2) I,A" . 251 from conseqPost [OF this wp' subset_refl] 252 show ?thesis . 253qed 254 255 256lemma switchNil: 257 "P \<subseteq> Q \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>P (switch v []) Q,A" 258 by (simp add: Skip) 259 260lemma switchCons: 261 "\<lbrakk>P \<subseteq> {s. (v s \<in> V \<longrightarrow> s \<in> P\<^sub>1) \<and> (v s \<notin> V \<longrightarrow> s \<in> P\<^sub>2)}; 262 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>P\<^sub>1 c Q,A; 263 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>P\<^sub>2 (switch v vs) Q,A\<rbrakk> 264\<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>P (switch v ((V,c)#vs)) Q,A" 265 by (simp add: Cond) 266 267 268lemma Guard: 269 "\<lbrakk>P \<subseteq> g \<inter> R; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c Q,A\<rbrakk> 270 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Guard f g c Q,A" 271apply (rule HoareTotalDef.Guard [THEN conseqPre, of _ _ _ _ R]) 272apply (erule conseqPre) 273apply auto 274done 275 276lemma GuardSwap: 277 "\<lbrakk> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c Q,A; P \<subseteq> g \<inter> R\<rbrakk> 278 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Guard f g c Q,A" 279 by (rule Guard) 280 281lemma Guarantee: 282 "\<lbrakk>P \<subseteq> {s. s \<in> g \<longrightarrow> s \<in> R}; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c Q,A; f \<in> F\<rbrakk> 283 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Guard f g c) Q,A" 284apply (rule Guarantee [THEN conseqPre, of _ _ _ _ _ "{s. s \<in> g \<longrightarrow> s \<in> R}"]) 285apply assumption 286apply (erule conseqPre) 287apply auto 288done 289 290lemma GuaranteeSwap: 291 "\<lbrakk> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c Q,A; P \<subseteq> {s. s \<in> g \<longrightarrow> s \<in> R}; f \<in> F\<rbrakk> 292 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Guard f g c) Q,A" 293 by (rule Guarantee) 294 295 296lemma GuardStrip: 297 "\<lbrakk>P \<subseteq> R; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c Q,A; f \<in> F\<rbrakk> 298 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Guard f g c) Q,A" 299apply (rule Guarantee [THEN conseqPre]) 300apply auto 301done 302 303lemma GuardStripSwap: 304 "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c Q,A; P \<subseteq> R; f \<in> F\<rbrakk> 305 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Guard f g c) Q,A" 306 by (rule GuardStrip) 307 308lemma GuaranteeStrip: 309 "\<lbrakk>P \<subseteq> R; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c Q,A; f \<in> F\<rbrakk> 310 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (guaranteeStrip f g c) Q,A" 311 by (unfold guaranteeStrip_def) (rule GuardStrip) 312 313lemma GuaranteeStripSwap: 314 "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c Q,A; P \<subseteq> R; f \<in> F\<rbrakk> 315 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (guaranteeStrip f g c) Q,A" 316 by (unfold guaranteeStrip_def) (rule GuardStrip) 317 318lemma GuaranteeAsGuard: 319 "\<lbrakk>P \<subseteq> g \<inter> R; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c Q,A\<rbrakk> 320 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P guaranteeStrip f g c Q,A" 321 by (unfold guaranteeStrip_def) (rule Guard) 322 323lemma GuaranteeAsGuardSwap: 324 "\<lbrakk> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c Q,A; P \<subseteq> g \<inter> R\<rbrakk> 325 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P guaranteeStrip f g c Q,A" 326 by (rule GuaranteeAsGuard) 327 328lemma GuardsNil: 329 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> 330 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (guards [] c) Q,A" 331 by simp 332 333lemma GuardsCons: 334 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Guard f g (guards gs c) Q,A \<Longrightarrow> 335 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (guards ((f,g)#gs) c) Q,A" 336 by simp 337 338lemma GuardsConsGuaranteeStrip: 339 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P guaranteeStrip f g (guards gs c) Q,A \<Longrightarrow> 340 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (guards (guaranteeStripPair f g#gs) c) Q,A" 341 by (simp add: guaranteeStripPair_def guaranteeStrip_def) 342 343lemma While: 344 assumes P_I: "P \<subseteq> I" 345 assumes deriv_body: 346 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I \<inter> b) c ({t. (t, \<sigma>) \<in> V} \<inter> I),A" 347 assumes I_Q: "I \<inter> -b \<subseteq> Q" 348 assumes wf: "wf V" 349 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnno b I V c) Q,A" 350proof - 351 from wf deriv_body P_I I_Q 352 show ?thesis 353 apply (unfold whileAnno_def) 354 apply (erule conseqPrePost [OF HoareTotalDef.While]) 355 apply auto 356 done 357qed 358 359 360 361lemma WhileInvPost: 362 assumes P_I: "P \<subseteq> I" 363 assumes termi_body: 364 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/UNIV\<^esub> ({\<sigma>} \<inter> I \<inter> b) c ({t. (t, \<sigma>) \<in> V} \<inter> P),A" 365 assumes deriv_body: 366 "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (I \<inter> b) c I,A" 367 assumes I_Q: "I \<inter> -b \<subseteq> Q" 368 assumes wf: "wf V" 369 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnno b I V c) Q,A" 370proof - 371 have "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I \<inter> b) c ({t. (t, \<sigma>) \<in> V} \<inter> I),A" 372 proof 373 fix \<sigma> 374 from hoare_sound [OF deriv_body] hoaret_sound [OF termi_body [rule_format, of \<sigma>]] 375 have "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I \<inter> b) c ({t. (t, \<sigma>) \<in> V} \<inter> I),A" 376 by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def) 377 then 378 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I \<inter> b) c ({t. (t, \<sigma>) \<in> V} \<inter> I),A" 379 by (rule hoaret_complete') 380 qed 381 382 from While [OF P_I this I_Q wf] 383 show ?thesis . 384qed 385 386(* *) 387lemma "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P \<inter> b) c Q,A \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P \<inter> b) (Seq c (Guard f Q Skip)) Q,A" 388oops 389 390text \<open>@{term "J"} will be instantiated by tactic with @{term "gs' \<inter> I"} for 391 those guards that are not stripped.\<close> 392lemma WhileAnnoG: 393 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (guards gs 394 (whileAnno b J V (Seq c (guards gs Skip)))) Q,A 395 \<Longrightarrow> 396 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnnoG gs b I V c) Q,A" 397 by (simp add: whileAnnoG_def whileAnno_def while_def) 398 399text \<open>This form stems from @{term "strip_guards F (whileAnnoG gs b I V c)"}\<close> 400lemma WhileNoGuard': 401 assumes P_I: "P \<subseteq> I" 402 assumes deriv_body: "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I \<inter> b) c ({t. (t, \<sigma>) \<in> V} \<inter> I),A" 403 assumes I_Q: "I \<inter> -b \<subseteq> Q" 404 assumes wf: "wf V" 405 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnno b I V (Seq c Skip)) Q,A" 406 apply (rule While [OF P_I _ I_Q wf]) 407 apply (rule allI) 408 apply (rule Seq) 409 apply (rule deriv_body [rule_format]) 410 apply (rule hoaret.Skip) 411 done 412 413lemma WhileAnnoFix: 414assumes consequence: "P \<subseteq> {s. (\<exists> Z. s\<in>I Z \<and> (I Z \<inter> -b \<subseteq> Q)) }" 415assumes bdy: "\<forall>Z \<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I Z \<inter> b) (c Z) ({t. (t, \<sigma>) \<in> V Z} \<inter> I Z),A" 416assumes bdy_constant: "\<forall>Z. c Z = c undefined" 417assumes wf: "\<forall>Z. wf (V Z)" 418shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnnoFix b I V c) Q,A" 419proof - 420 from bdy bdy_constant 421 have bdy': "\<And>Z. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I Z \<inter> b) (c undefined) 422 ({t. (t, \<sigma>) \<in> V Z} \<inter> I Z),A" 423 apply - 424 apply (erule_tac x=Z in allE) 425 apply (erule_tac x=Z in allE) 426 apply simp 427 done 428 have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (I Z) (whileAnnoFix b I V c) (I Z \<inter> -b),A" 429 apply rule 430 apply (unfold whileAnnoFix_def) 431 apply (rule hoaret.While) 432 apply (rule wf [rule_format]) 433 apply (rule bdy') 434 done 435 then 436 show ?thesis 437 apply (rule conseq) 438 using consequence 439 by blast 440qed 441 442lemma WhileAnnoFix': 443assumes consequence: "P \<subseteq> {s. (\<exists> Z. s\<in>I Z \<and> 444 (\<forall>t. t \<in> I Z \<inter> -b \<longrightarrow> t \<in> Q)) }" 445assumes bdy: "\<forall>Z \<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> I Z \<inter> b) (c Z) ({t. (t, \<sigma>) \<in> V Z} \<inter> I Z),A" 446assumes bdy_constant: "\<forall>Z. c Z = c undefined" 447assumes wf: "\<forall>Z. wf (V Z)" 448shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnnoFix b I V c) Q,A" 449 apply (rule WhileAnnoFix [OF _ bdy bdy_constant wf]) 450 using consequence by blast 451 452lemma WhileAnnoGFix: 453assumes whileAnnoFix: 454 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (guards gs 455 (whileAnnoFix b J V (\<lambda>Z. (Seq (c Z) (guards gs Skip))))) Q,A" 456shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnnoGFix gs b I V c) Q,A" 457 using whileAnnoFix 458 by (simp add: whileAnnoGFix_def whileAnnoFix_def while_def) 459 460lemma Bind: 461 assumes adapt: "P \<subseteq> {s. s \<in> P' s}" 462 assumes c: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s) (c (e s)) Q,A" 463 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (bind e c) Q,A" 464apply (rule conseq [where P'="\<lambda>Z. {s. s=Z \<and> s \<in> P' Z}" and Q'="\<lambda>Z. Q" and 465A'="\<lambda>Z. A"]) 466apply (rule allI) 467apply (unfold bind_def) 468apply (rule HoareTotalDef.DynCom) 469apply (rule ballI) 470apply clarsimp 471apply (rule conseqPre) 472apply (rule c [rule_format]) 473apply blast 474using adapt 475apply blast 476done 477 478lemma Block: 479assumes adapt: "P \<subseteq> {s. init s \<in> P' s}" 480assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s) bdy {t. return s t \<in> R s t},{t. return s t \<in> A}" 481assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A" 482shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (block init bdy return c) Q,A" 483apply (rule conseq [where P'="\<lambda>Z. {s. s=Z \<and> init s \<in> P' Z}" and Q'="\<lambda>Z. Q" and 484A'="\<lambda>Z. A"]) 485prefer 2 486using adapt 487apply blast 488apply (rule allI) 489apply (unfold block_def) 490apply (rule HoareTotalDef.DynCom) 491apply (rule ballI) 492apply clarsimp 493apply (rule_tac R="{t. return Z t \<in> R Z t}" in SeqSwap ) 494apply (rule_tac P'="\<lambda>Z'. {t. t=Z' \<and> return Z t \<in> R Z t}" and 495 Q'="\<lambda>Z'. Q" and A'="\<lambda>Z'. A" in conseq) 496prefer 2 apply simp 497apply (rule allI) 498apply (rule HoareTotalDef.DynCom) 499apply (clarsimp) 500apply (rule SeqSwap) 501apply (rule c [rule_format]) 502apply (rule Basic) 503apply clarsimp 504apply (rule_tac R="{t. return Z t \<in> A}" in HoareTotalDef.Catch) 505apply (rule_tac R="{i. i \<in> P' Z}" in Seq) 506apply (rule Basic) 507apply clarsimp 508apply simp 509apply (rule bdy [rule_format]) 510apply (rule SeqSwap) 511apply (rule Throw) 512apply (rule Basic) 513apply simp 514done 515 516lemma BlockSwap: 517assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A" 518assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s) bdy {t. return s t \<in> R s t},{t. return s t \<in> A}" 519assumes adapt: "P \<subseteq> {s. init s \<in> P' s}" 520shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (block init bdy return c) Q,A" 521 using adapt bdy c 522 by (rule Block) 523 524lemma BlockSpec: 525 assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and> 526 (\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and> 527 (\<forall>t. t \<in> A' Z \<longrightarrow> return s t \<in> A)}" 528 assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A" 529 assumes bdy: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) bdy (Q' Z),(A' Z)" 530 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (block init bdy return c) Q,A" 531apply (rule conseq [where P'="\<lambda>Z. {s. init s \<in> P' Z \<and> 532 (\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and> 533 (\<forall>t. t \<in> A' Z \<longrightarrow> return s t \<in> A)}" and Q'="\<lambda>Z. Q" and 534A'="\<lambda>Z. A"]) 535prefer 2 536using adapt 537apply blast 538apply (rule allI) 539apply (unfold block_def) 540apply (rule HoareTotalDef.DynCom) 541apply (rule ballI) 542apply clarsimp 543apply (rule_tac R="{t. return s t \<in> R s t}" in SeqSwap ) 544apply (rule_tac P'="\<lambda>Z'. {t. t=Z' \<and> return s t \<in> R s t}" and 545 Q'="\<lambda>Z'. Q" and A'="\<lambda>Z'. A" in conseq) 546prefer 2 apply simp 547apply (rule allI) 548apply (rule HoareTotalDef.DynCom) 549apply (clarsimp) 550apply (rule SeqSwap) 551apply (rule c [rule_format]) 552apply (rule Basic) 553apply clarsimp 554apply (rule_tac R="{t. return s t \<in> A}" in HoareTotalDef.Catch) 555apply (rule_tac R="{i. i \<in> P' Z}" in Seq) 556apply (rule Basic) 557apply clarsimp 558apply simp 559apply (rule conseq [OF bdy]) 560apply clarsimp 561apply blast 562apply (rule SeqSwap) 563apply (rule Throw) 564apply (rule Basic) 565apply simp 566done 567 568 569lemma Throw: "P \<subseteq> A \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Throw Q,A" 570 by (rule hoaret.Throw [THEN conseqPre]) 571 572lemmas Catch = hoaret.Catch 573lemma CatchSwap: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c\<^sub>2 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c\<^sub>1 Q,R\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Catch c\<^sub>1 c\<^sub>2 Q,A" 574 by (rule hoaret.Catch) 575 576lemma raise: "P \<subseteq> {s. f s \<in> A} \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P raise f Q,A" 577 apply (simp add: raise_def) 578 apply (rule Seq) 579 apply (rule Basic) 580 apply (assumption) 581 apply (rule Throw) 582 apply (rule subset_refl) 583 done 584 585lemma condCatch: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c\<^sub>1 Q,((b \<inter> R) \<union> (-b \<inter> A));\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c\<^sub>2 Q,A\<rbrakk> 586 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P condCatch c\<^sub>1 b c\<^sub>2 Q,A" 587 apply (simp add: condCatch_def) 588 apply (rule Catch) 589 apply assumption 590 apply (rule CondSwap) 591 apply (assumption) 592 apply (rule hoaret.Throw) 593 apply blast 594 done 595 596lemma condCatchSwap: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> R c\<^sub>2 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c\<^sub>1 Q,((b \<inter> R) \<union> (-b \<inter> A))\<rbrakk> 597 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P condCatch c\<^sub>1 b c\<^sub>2 Q,A" 598 by (rule condCatch) 599 600 601lemma ProcSpec: 602 assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and> 603 (\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and> 604 (\<forall>t. t \<in> A' Z \<longrightarrow> return s t \<in> A)}" 605 assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A" 606 assumes p: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call p (Q' Z),(A' Z)" 607 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" 608using adapt c p 609apply (unfold call_def) 610by (rule BlockSpec) 611 612lemma ProcSpec': 613 assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and> 614 (\<forall>t \<in> Q' Z. return s t \<in> R s t) \<and> 615 (\<forall>t \<in> A' Z. return s t \<in> A)}" 616 assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A" 617 assumes p: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call p (Q' Z),(A' Z)" 618 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" 619apply (rule ProcSpec [OF _ c p]) 620apply (insert adapt) 621apply clarsimp 622apply (drule (1) subsetD) 623apply (clarsimp) 624apply (rule_tac x=Z in exI) 625apply blast 626done 627 628 629lemma ProcSpecNoAbrupt: 630 assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and> 631 (\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t)}" 632 assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A" 633 assumes p: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call p (Q' Z),{}" 634 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" 635apply (rule ProcSpec [OF _ c p]) 636using adapt 637apply simp 638done 639 640lemma FCall: 641"\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return (\<lambda>s t. c (result t))) Q,A 642\<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (fcall init p return result c) Q,A" 643 by (simp add: fcall_def) 644 645lemma ProcRec: 646 assumes deriv_bodies: 647 "\<forall>p\<in>Procs. 648 \<forall>\<sigma> Z. \<Gamma>,\<Theta>\<union>(\<Union>q\<in>Procs. \<Union>Z. 649 {(P q Z \<inter> {s. ((s,q), \<sigma>,p) \<in> r},q,Q q Z,A q Z)}) 650 \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> P p Z) (the (\<Gamma> p)) (Q p Z),(A p Z)" 651 assumes wf: "wf r" 652 assumes Procs_defined: "Procs \<subseteq> dom \<Gamma>" 653 shows "\<forall>p\<in>Procs. \<forall>Z. 654 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>(P p Z) Call p (Q p Z),(A p Z)" 655 by (intro strip) 656 (rule HoareTotalDef.CallRec' 657 [OF _ Procs_defined wf deriv_bodies], 658 simp_all) 659 660lemma ProcRec': 661 assumes ctxt: 662 "\<Theta>'=(\<lambda>\<sigma> p. \<Theta>\<union>(\<Union>q\<in>Procs. 663 \<Union>Z. {(P q Z \<inter> {s. ((s,q), \<sigma>,p) \<in> r},q,Q q Z,A q Z)}))" 664 assumes deriv_bodies: 665 "\<forall>p\<in>Procs. 666 \<forall>\<sigma> Z. \<Gamma>,\<Theta>' \<sigma> p\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> P p Z) (the (\<Gamma> p)) (Q p Z),(A p Z)" 667 assumes wf: "wf r" 668 assumes Procs_defined: "Procs \<subseteq> dom \<Gamma>" 669 shows "\<forall>p\<in>Procs. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>(P p Z) Call p (Q p Z),(A p Z)" 670 using ctxt deriv_bodies 671 apply simp 672 apply (erule ProcRec [OF _ wf Procs_defined]) 673 done 674 675 676lemma ProcRecList: 677 assumes deriv_bodies: 678 "\<forall>p\<in>set Procs. 679 \<forall>\<sigma> Z. \<Gamma>,\<Theta>\<union>(\<Union>q\<in>set Procs. \<Union>Z. 680 {(P q Z \<inter> {s. ((s,q), \<sigma>,p) \<in> r},q,Q q Z,A q Z)}) 681 \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> P p Z) (the (\<Gamma> p)) (Q p Z),(A p Z)" 682 assumes wf: "wf r" 683 assumes dist: "distinct Procs" 684 assumes Procs_defined: "set Procs \<subseteq> dom \<Gamma>" 685 shows "\<forall>p\<in>set Procs. \<forall>Z. 686 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>(P p Z) Call p (Q p Z),(A p Z)" 687 using deriv_bodies wf Procs_defined 688 by (rule ProcRec) 689 690lemma ProcRecSpecs: 691 "\<lbrakk>\<forall>\<sigma>. \<forall>(P,p,Q,A) \<in> Specs. 692 \<Gamma>,\<Theta>\<union> ((\<lambda>(P,q,Q,A). (P \<inter> {s. ((s,q),(\<sigma>,p)) \<in> r},q,Q,A)) ` Specs) 693 \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> P) (the (\<Gamma> p)) Q,A; 694 wf r; 695 \<forall>(P,p,Q,A) \<in> Specs. p \<in> dom \<Gamma>\<rbrakk> 696 \<Longrightarrow> \<forall>(P,p,Q,A) \<in> Specs. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 697apply (rule ballI) 698apply (case_tac x) 699apply (rename_tac x P p Q A) 700apply simp 701apply (rule hoaret.CallRec) 702apply auto 703done 704 705lemma ProcRec1: 706 assumes deriv_body: 707 "\<forall>\<sigma> Z. \<Gamma>,\<Theta>\<union>(\<Union>Z. {(P Z \<inter> {s. ((s,p), \<sigma>,p) \<in> r},p,Q Z,A Z)}) 708 \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> P Z) (the (\<Gamma> p)) (Q Z),(A Z)" 709 assumes wf: "wf r" 710 assumes p_defined: "p \<in> dom \<Gamma>" 711 shows "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P Z) Call p (Q Z),(A Z)" 712proof - 713 from deriv_body wf p_defined 714 have "\<forall>p\<in>{p}. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P Z) Call p (Q Z),(A Z)" 715 apply - 716 apply (rule ProcRec [where A="\<lambda>p. A" and P="\<lambda>p. P" and Q="\<lambda>p. Q"]) 717 apply simp_all 718 done 719 thus ?thesis 720 by simp 721qed 722 723lemma ProcNoRec1: 724 assumes deriv_body: 725 "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P Z) (the (\<Gamma> p)) (Q Z),(A Z)" 726 assumes p_defined: "p \<in> dom \<Gamma>" 727 shows "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P Z) Call p (Q Z),(A Z)" 728proof - 729 have "\<forall>\<sigma> Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> P Z) (the (\<Gamma> p)) (Q Z),(A Z)" 730 by (blast intro: conseqPre deriv_body [rule_format]) 731 with p_defined have "\<forall>\<sigma> Z. \<Gamma>,\<Theta>\<union>(\<Union>Z. {(P Z \<inter> {s. ((s,p), \<sigma>,p) \<in> {}}, 732 p,Q Z,A Z)}) 733 \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> P Z) (the (\<Gamma> p)) (Q Z),(A Z)" 734 by (blast intro: hoaret_augment_context) 735 from this 736 show ?thesis 737 by (rule ProcRec1) (auto simp add: p_defined) 738qed 739 740lemma ProcBody: 741 assumes WP: "P \<subseteq> P'" 742 assumes deriv_body: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' body Q,A" 743 assumes body: "\<Gamma> p = Some body" 744 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Call p Q,A" 745apply (rule conseqPre [OF _ WP]) 746apply (rule ProcNoRec1 [rule_format, where P="\<lambda>Z. P'" and Q="\<lambda>Z. Q" and A="\<lambda>Z. A"]) 747apply (insert body) 748apply simp 749apply (rule hoaret_augment_context [OF deriv_body]) 750apply blast 751apply fastforce 752done 753 754lemma CallBody: 755assumes adapt: "P \<subseteq> {s. init s \<in> P' s}" 756assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s) body {t. return s t \<in> R s t},{t. return s t \<in> A}" 757assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A" 758assumes body: "\<Gamma> p = Some body" 759shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" 760apply (unfold call_def) 761apply (rule Block [OF adapt _ c]) 762apply (rule allI) 763apply (rule ProcBody [where \<Gamma>=\<Gamma>, OF _ bdy [rule_format] body]) 764apply simp 765done 766 767lemmas ProcModifyReturn = HoareTotalProps.ProcModifyReturn 768lemmas ProcModifyReturnSameFaults = HoareTotalProps.ProcModifyReturnSameFaults 769 770lemma ProcModifyReturnNoAbr: 771 assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return' c) Q,A" 772 assumes result_conform: 773 "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)" 774 assumes modifies_spec: 775 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call p (Modif \<sigma>),{}" 776 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" 777by (rule ProcModifyReturn [OF spec result_conform _ modifies_spec]) simp 778 779 780lemma ProcModifyReturnNoAbrSameFaults: 781 assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return' c) Q,A" 782 assumes result_conform: 783 "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)" 784 assumes modifies_spec: 785 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),{}" 786 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" 787by (rule ProcModifyReturnSameFaults [OF spec result_conform _ modifies_spec]) simp 788 789 790lemma DynProc: 791 assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and> 792 (\<forall>t. t \<in> Q' s Z \<longrightarrow> return s t \<in> R s t) \<and> 793 (\<forall>t. t \<in> A' s Z \<longrightarrow> return s t \<in> A)}" 794 assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A" 795 assumes p: "\<forall>s\<in> P. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s Z) Call (p s) (Q' s Z),(A' s Z)" 796 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return c Q,A" 797apply (rule conseq [where P'="\<lambda>Z. {s. s=Z \<and> s \<in> P}" 798 and Q'="\<lambda>Z. Q" and A'="\<lambda>Z. A"]) 799prefer 2 800using adapt 801apply blast 802apply (rule allI) 803apply (unfold dynCall_def call_def block_def) 804apply (rule HoareTotalDef.DynCom) 805apply clarsimp 806apply (rule HoareTotalDef.DynCom) 807apply clarsimp 808apply (frule in_mono [rule_format, OF adapt]) 809apply clarsimp 810apply (rename_tac Z') 811apply (rule_tac R="Q' Z Z'" in Seq) 812apply (rule CatchSwap) 813apply (rule SeqSwap) 814apply (rule Throw) 815apply (rule subset_refl) 816apply (rule Basic) 817apply (rule subset_refl) 818apply (rule_tac R="{i. i \<in> P' Z Z'}" in Seq) 819apply (rule Basic) 820apply clarsimp 821apply simp 822apply (rule_tac Q'="Q' Z Z'" and A'="A' Z Z'" in conseqPost) 823using p 824apply clarsimp 825apply simp 826apply clarsimp 827apply (rule_tac P'="\<lambda>Z''. {t. t=Z'' \<and> return Z t \<in> R Z t}" and 828 Q'="\<lambda>Z''. Q" and A'="\<lambda>Z''. A" in conseq) 829prefer 2 apply simp 830apply (rule allI) 831apply (rule HoareTotalDef.DynCom) 832apply clarsimp 833apply (rule SeqSwap) 834apply (rule c [rule_format]) 835apply (rule Basic) 836apply clarsimp 837done 838 839lemma DynProc': 840 assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and> 841 (\<forall>t \<in> Q' s Z. return s t \<in> R s t) \<and> 842 (\<forall>t \<in> A' s Z. return s t \<in> A)}" 843 assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A" 844 assumes p: "\<forall>s\<in> P. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s Z) Call (p s) (Q' s Z),(A' s Z)" 845 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return c Q,A" 846proof - 847 from adapt have "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and> 848 (\<forall>t. t \<in> Q' s Z \<longrightarrow> return s t \<in> R s t) \<and> 849 (\<forall>t. t \<in> A' s Z \<longrightarrow> return s t \<in> A)}" 850 by blast 851 from this c p show ?thesis 852 by (rule DynProc) 853qed 854 855lemma DynProcStaticSpec: 856assumes adapt: "P \<subseteq> {s. s \<in> S \<and> (\<exists>Z. init s \<in> P' Z \<and> 857 (\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>) \<and> 858 (\<forall>\<tau>. \<tau> \<in> A' Z \<longrightarrow> return s \<tau> \<in> A))}" 859assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A" 860assumes spec: "\<forall>s\<in>S. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call (p s) (Q' Z),(A' Z)" 861shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 862proof - 863 from adapt have P_S: "P \<subseteq> S" 864 by blast 865 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P \<inter> S) (dynCall init p return c) Q,A" 866 apply (rule DynProc [where P'="\<lambda>s Z. P' Z" and Q'="\<lambda>s Z. Q' Z" 867 and A'="\<lambda>s Z. A' Z", OF _ c]) 868 apply clarsimp 869 apply (frule in_mono [rule_format, OF adapt]) 870 apply clarsimp 871 using spec 872 apply clarsimp 873 done 874 thus ?thesis 875 by (rule conseqPre) (insert P_S,blast) 876qed 877 878 879 880lemma DynProcProcPar: 881assumes adapt: "P \<subseteq> {s. p s = q \<and> (\<exists>Z. init s \<in> P' Z \<and> 882 (\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>) \<and> 883 (\<forall>\<tau>. \<tau> \<in> A' Z \<longrightarrow> return s \<tau> \<in> A))}" 884assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A" 885assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call q (Q' Z),(A' Z)" 886shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 887 apply (rule DynProcStaticSpec [where S="{s. p s = q}",simplified, OF adapt c]) 888 using spec 889 apply simp 890 done 891 892 893lemma DynProcProcParNoAbrupt: 894assumes adapt: "P \<subseteq> {s. p s = q \<and> (\<exists>Z. init s \<in> P' Z \<and> 895 (\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>))}" 896assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A" 897assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call q (Q' Z),{}" 898shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 899proof - 900 have "P \<subseteq> {s. p s = q \<and> (\<exists> Z. init s \<in> P' Z \<and> 901 (\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and> 902 (\<forall>t. t \<in> {} \<longrightarrow> return s t \<in> A))}" 903 (is "P \<subseteq> ?P'") 904 proof 905 fix s 906 assume P: "s\<in>P" 907 with adapt obtain Z where 908 Pre: "p s = q \<and> init s \<in> P' Z" and 909 adapt_Norm: "\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>" 910 by blast 911 from adapt_Norm 912 have "\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t" 913 by auto 914 then 915 show "s\<in>?P'" 916 using Pre by blast 917 qed 918 note P = this 919 show ?thesis 920 apply - 921 apply (rule DynProcStaticSpec [where S="{s. p s = q}",simplified, OF P c]) 922 apply (insert spec) 923 apply auto 924 done 925qed 926 927lemma DynProcModifyReturnNoAbr: 928 assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return' c) Q,A" 929 assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s)) 930 \<longrightarrow> return' s t = return s t" 931 assumes modif_clause: 932 "\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),{}" 933 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 934proof - 935 from ret_nrm_modif 936 have "\<forall>s t. t \<in> (Modif (init s)) 937 \<longrightarrow> return' s t = return s t" 938 by iprover 939 then 940 have ret_nrm_modif': "\<forall>s t. t \<in> (Modif (init s)) 941 \<longrightarrow> return' s t = return s t" 942 by simp 943 have ret_abr_modif': "\<forall>s t. t \<in> {} 944 \<longrightarrow> return' s t = return s t" 945 by simp 946 from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis 947 by (rule dynProcModifyReturn) 948qed 949 950lemma ProcDynModifyReturnNoAbrSameFaults: 951 assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return' c) Q,A" 952 assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s)) 953 \<longrightarrow> return' s t = return s t" 954 assumes modif_clause: 955 "\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call (p s)) (Modif \<sigma>),{}" 956 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 957proof - 958 from ret_nrm_modif 959 have "\<forall>s t. t \<in> (Modif (init s)) 960 \<longrightarrow> return' s t = return s t" 961 by iprover 962 then 963 have ret_nrm_modif': "\<forall>s t. t \<in> (Modif (init s)) 964 \<longrightarrow> return' s t = return s t" 965 by simp 966 have ret_abr_modif': "\<forall>s t. t \<in> {} 967 \<longrightarrow> return' s t = return s t" 968 by simp 969 from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis 970 by (rule dynProcModifyReturnSameFaults) 971qed 972 973lemma ProcProcParModifyReturn: 974 assumes q: "P \<subseteq> {s. p s = q} \<inter> P'" 975 \<comment> \<open>@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in 976 @{term P'}, so the vcg can simplify it.\<close> 977 assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A" 978 assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s)) 979 \<longrightarrow> return' s t = return s t" 980 assumes ret_abr_modif: "\<forall>s t. t \<in> (ModifAbr (init s)) 981 \<longrightarrow> return' s t = return s t" 982 assumes modif_clause: 983 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),(ModifAbr \<sigma>)" 984 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 985proof - 986 from to_prove have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return' c) Q,A" 987 by (rule conseqPre) blast 988 from this ret_nrm_modif 989 ret_abr_modif 990 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return c) Q,A" 991 by (rule dynProcModifyReturn) (insert modif_clause,auto) 992 from this q show ?thesis 993 by (rule conseqPre) 994qed 995 996 997 998lemma ProcProcParModifyReturnSameFaults: 999 assumes q: "P \<subseteq> {s. p s = q} \<inter> P'" 1000 \<comment> \<open>@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in 1001 @{term P'}, so the vcg can simplify it.\<close> 1002 assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A" 1003 assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s)) 1004 \<longrightarrow> return' s t = return s t" 1005 assumes ret_abr_modif: "\<forall>s t. t \<in> (ModifAbr (init s)) 1006 \<longrightarrow> return' s t = return s t" 1007 assumes modif_clause: 1008 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call q (Modif \<sigma>),(ModifAbr \<sigma>)" 1009 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 1010proof - 1011 from to_prove 1012 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return' c) Q,A" 1013 by (rule conseqPre) blast 1014 from this ret_nrm_modif 1015 ret_abr_modif 1016 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return c) Q,A" 1017 by (rule dynProcModifyReturnSameFaults) (insert modif_clause,auto) 1018 from this q show ?thesis 1019 by (rule conseqPre) 1020qed 1021 1022lemma ProcProcParModifyReturnNoAbr: 1023 assumes q: "P \<subseteq> {s. p s = q} \<inter> P'" 1024 \<comment> \<open>@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as 1025 first conjunction in @{term P'}, so the vcg can simplify it.\<close> 1026 assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A" 1027 assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s)) 1028 \<longrightarrow> return' s t = return s t" 1029 assumes modif_clause: 1030 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),{}" 1031 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 1032proof - 1033 from to_prove have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return' c) Q,A" 1034 by (rule conseqPre) blast 1035 from this ret_nrm_modif 1036 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return c) Q,A" 1037 by (rule DynProcModifyReturnNoAbr) (insert modif_clause,auto) 1038 from this q show ?thesis 1039 by (rule conseqPre) 1040qed 1041 1042 1043lemma ProcProcParModifyReturnNoAbrSameFaults: 1044 assumes q: "P \<subseteq> {s. p s = q} \<inter> P'" 1045 \<comment> \<open>@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as 1046 first conjunction in @{term P'}, so the vcg can simplify it.\<close> 1047 assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' (dynCall init p return' c) Q,A" 1048 assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s)) 1049 \<longrightarrow> return' s t = return s t" 1050 assumes modif_clause: 1051 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),{}" 1052 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 1053proof - 1054 from to_prove have 1055 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return' c) Q,A" 1056 by (rule conseqPre) blast 1057 from this ret_nrm_modif 1058 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return c) Q,A" 1059 by (rule ProcDynModifyReturnNoAbrSameFaults) (insert modif_clause,auto) 1060 from this q show ?thesis 1061 by (rule conseqPre) 1062qed 1063 1064lemma MergeGuards_iff: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P merge_guards c Q,A = \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 1065 by (auto intro: MergeGuardsI MergeGuardsD) 1066 1067lemma CombineStrip': 1068 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c' Q,A" 1069 assumes deriv_strip_triv: "\<Gamma>,{}\<turnstile>\<^bsub>/{}\<^esub> P c'' UNIV,UNIV" 1070 assumes c'': "c''= mark_guards False (strip_guards (-F) c')" 1071 assumes c: "merge_guards c = merge_guards (mark_guards False c')" 1072 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 1073proof - 1074 from deriv_strip_triv have deriv_strip: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c'' UNIV,UNIV" 1075 by (auto intro: hoare_augment_context) 1076 from deriv_strip [simplified c''] 1077 have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P (strip_guards (- F) c') UNIV,UNIV" 1078 by (rule HoarePartialProps.MarkGuardsD) 1079 with deriv 1080 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c' Q,A" 1081 by (rule CombineStrip) 1082 hence "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P mark_guards False c' Q,A" 1083 by (rule MarkGuardsI) 1084 hence "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P merge_guards (mark_guards False c') Q,A" 1085 by (rule MergeGuardsI) 1086 hence "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P merge_guards c Q,A" 1087 by (simp add: c) 1088 thus ?thesis 1089 by (rule MergeGuardsD) 1090qed 1091 1092lemma CombineStrip'': 1093 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{True}\<^esub> P c' Q,A" 1094 assumes deriv_strip_triv: "\<Gamma>,{}\<turnstile>\<^bsub>/{}\<^esub> P c'' UNIV,UNIV" 1095 assumes c'': "c''= mark_guards False (strip_guards ({False}) c')" 1096 assumes c: "merge_guards c = merge_guards (mark_guards False c')" 1097 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 1098 apply (rule CombineStrip' [OF deriv deriv_strip_triv _ c]) 1099 apply (insert c'') 1100 apply (subgoal_tac "- {True} = {False}") 1101 apply auto 1102 done 1103 1104lemma AsmUN: 1105 "(\<Union>Z. {(P Z, p, Q Z,A Z)}) \<subseteq> \<Theta> 1106 \<Longrightarrow> 1107 \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P Z) (Call p) (Q Z),(A Z)" 1108 by (blast intro: hoaret.Asm) 1109 1110 1111lemma hoaret_to_hoarep': 1112 "\<forall>Z. \<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P Z) p (Q Z),(A Z) \<Longrightarrow> \<forall>Z. \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> (P Z) p (Q Z),(A Z)" 1113 by (iprover intro: total_to_partial) 1114 1115lemma augment_context': 1116 "\<lbrakk>\<Theta> \<subseteq> \<Theta>'; \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P Z) p (Q Z),(A Z)\<rbrakk> 1117 \<Longrightarrow> \<forall>Z. \<Gamma>,\<Theta>'\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P Z) p (Q Z),(A Z)" 1118 by (iprover intro: hoaret_augment_context) 1119 1120 1121lemma augment_emptyFaults: 1122 "\<lbrakk>\<forall>Z. \<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> (P Z) p (Q Z),(A Z)\<rbrakk> \<Longrightarrow> 1123 \<forall>Z. \<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P Z) p (Q Z),(A Z)" 1124 by (blast intro: augment_Faults) 1125 1126lemma augment_FaultsUNIV: 1127 "\<lbrakk>\<forall>Z. \<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P Z) p (Q Z),(A Z)\<rbrakk> \<Longrightarrow> 1128 \<forall>Z. \<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/UNIV\<^esub> (P Z) p (Q Z),(A Z)" 1129 by (blast intro: augment_Faults) 1130 1131lemma PostConjI [trans]: 1132 "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c R,B\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> B)" 1133 by (rule PostConjI) 1134 1135lemma PostConjI' : 1136 "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c R,B\<rbrakk> 1137 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> B)" 1138 by (rule PostConjI) iprover+ 1139 1140lemma PostConjE [consumes 1]: 1141 assumes conj: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> B)" 1142 assumes E: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c R,B\<rbrakk> \<Longrightarrow> S" 1143 shows "S" 1144proof - 1145 from conj have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" by (rule conseqPost) blast+ 1146 moreover 1147 from conj have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c R,B" by (rule conseqPost) blast+ 1148 ultimately show "S" 1149 by (rule E) 1150qed 1151 1152subsubsection \<open>Rules for Single-Step Proof \label{sec:hoare-isar}\<close> 1153 1154text \<open> 1155 We are now ready to introduce a set of Hoare rules to be used in 1156 single-step structured proofs in Isabelle/Isar. 1157 1158 \medskip Assertions of Hoare Logic may be manipulated in 1159 calculational proofs, with the inclusion expressed in terms of sets 1160 or predicates. Reversed order is supported as well. 1161\<close> 1162 1163 1164lemma annotateI [trans]: 1165"\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P anno Q,A; c = anno\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 1166 by (simp) 1167 1168lemma annotate_normI: 1169 assumes deriv_anno: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>P anno Q,A" 1170 assumes norm_eq: "normalize c = normalize anno" 1171 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>P c Q,A" 1172proof - 1173 from HoareTotalProps.NormalizeI [OF deriv_anno] norm_eq 1174 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>P normalize c Q,A" 1175 by simp 1176 from NormalizeD [OF this] 1177 show ?thesis . 1178qed 1179 1180 1181lemma annotateWhile: 1182"\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnnoG gs b I V c) Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (while gs b c) Q,A" 1183 by (simp add: whileAnnoG_def) 1184 1185 1186lemma reannotateWhile: 1187"\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnnoG gs b I V c) Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnnoG gs b J V c) Q,A" 1188 by (simp add: whileAnnoG_def) 1189 1190lemma reannotateWhileNoGuard: 1191"\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnno b I V c) Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (whileAnno b J V c) Q,A" 1192 by (simp add: whileAnno_def) 1193 1194lemma [trans] : "P' \<subseteq> P \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q,A" 1195 by (rule conseqPre) 1196 1197lemma [trans]: "Q \<subseteq> Q' \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q',A" 1198 by (rule conseqPost) blast+ 1199 1200lemma [trans]: 1201 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. P s} c Q,A \<Longrightarrow> (\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. P' s} c Q,A" 1202 by (rule conseqPre) auto 1203 1204lemma [trans]: 1205 "(\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. P s} c Q,A \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. P' s} c Q,A" 1206 by (rule conseqPre) auto 1207 1208lemma [trans]: 1209 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c {s. Q s},A \<Longrightarrow> (\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c {s. Q' s},A" 1210 by (rule conseqPost) auto 1211 1212lemma [trans]: 1213 "(\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c {s. Q s},A \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c {s. Q' s},A" 1214 by (rule conseqPost) auto 1215 1216lemma [intro?]: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Skip P,A" 1217 by (rule Skip) auto 1218 1219lemma CondInt [trans,intro?]: 1220 "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P \<inter> b) c1 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P \<inter> - b) c2 Q,A\<rbrakk> 1221 \<Longrightarrow> 1222 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Cond b c1 c2) Q,A" 1223 by (rule Cond) auto 1224 1225lemma CondConj [trans, intro?]: 1226 "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. P s \<and> b s} c1 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. P s \<and> \<not> b s} c2 Q,A\<rbrakk> 1227 \<Longrightarrow> 1228 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. P s} (Cond {s. b s} c1 c2) Q,A" 1229 by (rule Cond) auto 1230end 1231 1232