1(* 2 Author: Norbert Schirmer 3 Maintainer: Norbert Schirmer, norbert.schirmer at web de 4 License: LGPL 5*) 6 7(* Title: Hoare.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>Auxiliary Definitions/Lemmas to Facilitate Hoare Logic\<close> 30theory Hoare imports HoarePartial HoareTotal begin 31 32 33syntax 34 35"_hoarep_emptyFaults":: 36"[('s,'p,'f) body,('s,'p) quadruple set, 37 'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool" 38 ("(3_,_/\<turnstile> (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60) 39 40"_hoarep_emptyCtx":: 41"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool" 42 ("(3_/\<turnstile>\<^bsub>'/_\<^esub> (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60) 43 44"_hoarep_emptyCtx_emptyFaults":: 45"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool" 46 ("(3_/\<turnstile> (_/ (_)/ _,/_))" [61,1000,20,1000,1000]60) 47 48"_hoarep_noAbr":: 49"[('s,'p,'f) body,('s,'p) quadruple set,'f set, 50 's assn,('s,'p,'f) com, 's assn] => bool" 51 ("(3_,_/\<turnstile>\<^bsub>'/_\<^esub> (_/ (_)/ _))" [61,60,60,1000,20,1000]60) 52 53"_hoarep_noAbr_emptyFaults":: 54"[('s,'p,'f) body,('s,'p) quadruple set,'s assn,('s,'p,'f) com, 's assn] => bool" 55 ("(3_,_/\<turnstile> (_/ (_)/ _))" [61,60,1000,20,1000]60) 56 57"_hoarep_emptyCtx_noAbr":: 58"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn] => bool" 59 ("(3_/\<turnstile>\<^bsub>'/_\<^esub> (_/ (_)/ _))" [61,60,1000,20,1000]60) 60 61"_hoarep_emptyCtx_noAbr_emptyFaults":: 62"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn] => bool" 63 ("(3_/\<turnstile> (_/ (_)/ _))" [61,1000,20,1000]60) 64 65 66 67"_hoaret_emptyFaults":: 68"[('s,'p,'f) body,('s,'p) quadruple set, 69 's assn,('s,'p,'f) com, 's assn,'s assn] => bool" 70 ("(3_,_/\<turnstile>\<^sub>t (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60) 71 72"_hoaret_emptyCtx":: 73"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool" 74 ("(3_/\<turnstile>\<^sub>t\<^bsub>'/_\<^esub> (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60) 75 76"_hoaret_emptyCtx_emptyFaults":: 77"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool" 78 ("(3_/\<turnstile>\<^sub>t (_/ (_)/ _,/_))" [61,1000,20,1000,1000]60) 79 80"_hoaret_noAbr":: 81"[('s,'p,'f) body,'f set, ('s,'p) quadruple set, 82 's assn,('s,'p,'f) com, 's assn] => bool" 83 ("(3_,_/\<turnstile>\<^sub>t\<^bsub>'/_\<^esub> (_/ (_)/ _))" [61,60,60,1000,20,1000]60) 84 85"_hoaret_noAbr_emptyFaults":: 86"[('s,'p,'f) body,('s,'p) quadruple set,'s assn,('s,'p,'f) com, 's assn] => bool" 87 ("(3_,_/\<turnstile>\<^sub>t (_/ (_)/ _))" [61,60,1000,20,1000]60) 88 89"_hoaret_emptyCtx_noAbr":: 90"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn] => bool" 91 ("(3_/\<turnstile>\<^sub>t\<^bsub>'/_\<^esub> (_/ (_)/ _))" [61,60,1000,20,1000]60) 92 93"_hoaret_emptyCtx_noAbr_emptyFaults":: 94"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn] => bool" 95 ("(3_/\<turnstile>\<^sub>t (_/ (_)/ _))" [61,1000,20,1000]60) 96 97 98syntax (ASCII) 99 100"_hoarep_emptyFaults":: 101"[('s,'p,'f) body,('s,'p) quadruple set, 102 's assn,('s,'p,'f) com, 's assn,'s assn] \<Rightarrow> bool" 103 ("(3_,_/|- (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60) 104 105"_hoarep_emptyCtx":: 106"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool" 107 ("(3_/|-'/_ (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60) 108 109"_hoarep_emptyCtx_emptyFaults":: 110"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool" 111 ("(3_/|-(_/ (_)/ _,/_))" [61,1000,20,1000,1000]60) 112 113"_hoarep_noAbr":: 114"[('s,'p,'f) body,('s,'p) quadruple set,'f set, 115 's assn,('s,'p,'f) com, 's assn] => bool" 116 ("(3_,_/|-'/_ (_/ (_)/ _))" [61,60,60,1000,20,1000]60) 117 118"_hoarep_noAbr_emptyFaults":: 119"[('s,'p,'f) body,('s,'p) quadruple set,'s assn,('s,'p,'f) com, 's assn] => bool" 120 ("(3_,_/|-(_/ (_)/ _))" [61,60,1000,20,1000]60) 121 122"_hoarep_emptyCtx_noAbr":: 123"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn] => bool" 124 ("(3_/|-'/_ (_/ (_)/ _))" [61,60,1000,20,1000]60) 125 126"_hoarep_emptyCtx_noAbr_emptyFaults":: 127"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn] => bool" 128 ("(3_/|-(_/ (_)/ _))" [61,1000,20,1000]60) 129 130"_hoaret_emptyFault":: 131"[('s,'p,'f) body,('s,'p) quadruple set, 132 's assn,('s,'p,'f) com, 's assn,'s assn] => bool" 133 ("(3_,_/|-t (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60) 134 135"_hoaret_emptyCtx":: 136"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool" 137 ("(3_/|-t'/_ (_/ (_)/ _,/_))" [61,60,1000,20,1000,1000]60) 138 139"_hoaret_emptyCtx_emptyFaults":: 140"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn,'s assn] => bool" 141 ("(3_/|-t(_/ (_)/ _,/_))" [61,1000,20,1000,1000]60) 142 143"_hoaret_noAbr":: 144"[('s,'p,'f) body,('s,'p) quadruple set,'f set, 145 's assn,('s,'p,'f) com, 's assn] => bool" 146 ("(3_,_/|-t'/_ (_/ (_)/ _))" [61,60,60,1000,20,1000]60) 147 148"_hoaret_noAbr_emptyFaults":: 149"[('s,'p,'f) body,('s,'p) quadruple set,'s assn,('s,'p,'f) com, 's assn] => bool" 150 ("(3_,_/|-t(_/ (_)/ _))" [61,60,1000,20,1000]60) 151 152"_hoaret_emptyCtx_noAbr":: 153"[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com, 's assn] => bool" 154 ("(3_/|-t'/_ (_/ (_)/ _))" [61,60,1000,20,1000]60) 155 156"_hoaret_emptyCtx_noAbr_emptyFaults":: 157"[('s,'p,'f) body,'s assn,('s,'p,'f) com, 's assn] => bool" 158 ("(3_/|-t(_/ (_)/ _))" [61,1000,20,1000]60) 159 160translations 161 162 163 "\<Gamma>\<turnstile> P c Q,A" == "\<Gamma>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A" 164 "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" == "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 165 166 "\<Gamma>,\<Theta>\<turnstile> P c Q" == "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q" 167 "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q" == "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,{}" 168 "\<Gamma>,\<Theta>\<turnstile> P c Q,A" == "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A" 169 170 "\<Gamma>\<turnstile> P c Q" == "\<Gamma>\<turnstile>\<^bsub>/{}\<^esub> P c Q" 171 "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q" == "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q" 172 "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q" <= "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,{}" 173 "\<Gamma>\<turnstile> P c Q" <= "\<Gamma>\<turnstile> P c Q,{}" 174 175 176 177 178 "\<Gamma>\<turnstile>\<^sub>t P c Q,A" == "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 179 "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" == "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 180 181 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t P c Q" == "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q" 182 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q" == "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,{}" 183 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t P c Q,A" == "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 184 185 "\<Gamma>\<turnstile>\<^sub>t P c Q" == "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q" 186 "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q" == "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q" 187 "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q" <= "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,{}" 188 "\<Gamma>\<turnstile>\<^sub>t P c Q" <= "\<Gamma>\<turnstile>\<^sub>t P c Q,{}" 189 190 191term "\<Gamma>\<turnstile> P c Q" 192term "\<Gamma>\<turnstile> P c Q,A" 193 194term "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q" 195term "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 196 197term "\<Gamma>,\<Theta>\<turnstile> P c Q" 198term "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q" 199 200term "\<Gamma>,\<Theta>\<turnstile> P c Q,A" 201term "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 202 203 204term "\<Gamma>\<turnstile>\<^sub>t P c Q" 205term "\<Gamma>\<turnstile>\<^sub>t P c Q,A" 206 207term "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q" 208term "\<Gamma>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 209 210term "\<Gamma>,\<Theta>\<turnstile> P c Q" 211term "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q" 212 213term "\<Gamma>,\<Theta>\<turnstile> P c Q,A" 214term "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 215 216 217locale hoare = 218 fixes \<Gamma>::"('s,'p,'f) body" 219 220 221primrec assoc:: "('a \<times>'b) list \<Rightarrow> 'a \<Rightarrow> 'b " 222where 223"assoc [] x = undefined" | 224"assoc (p#ps) x = (if fst p = x then (snd p) else assoc ps x)" 225 226lemma conjE_simp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)" 227 by rule simp_all 228 229lemma CollectInt_iff: "{s. P s} \<inter> {s. Q s} = {s. P s \<and> Q s}" 230 by auto 231 232lemma Compl_Collect:"-(Collect b) = {x. \<not>(b x)}" 233 by fastforce 234 235lemma Collect_False: "{s. False} = {}" 236 by simp 237 238lemma Collect_True: "{s. True} = UNIV" 239 by simp 240 241lemma triv_All_eq: "\<forall>x. P \<equiv> P" 242 by simp 243 244lemma triv_Ex_eq: "\<exists>x. P \<equiv> P" 245 by simp 246 247lemma Ex_True: "\<exists>b. b" 248 by blast 249 250lemma Ex_False: "\<exists>b. \<not>b" 251 by blast 252 253definition mex::"('a \<Rightarrow> bool) \<Rightarrow> bool" 254 where "mex P = Ex P" 255 256definition meq::"'a \<Rightarrow> 'a \<Rightarrow> bool" 257 where "meq s Z = (s = Z)" 258 259lemma subset_unI1: "A \<subseteq> B \<Longrightarrow> A \<subseteq> B \<union> C" 260 by blast 261 262lemma subset_unI2: "A \<subseteq> C \<Longrightarrow> A \<subseteq> B \<union> C" 263 by blast 264 265lemma split_paired_UN: "(\<Union>p. (P p)) = (\<Union>a b. (P (a,b)))" 266 by auto 267 268lemma in_insert_hd: "f \<in> insert f X" 269 by simp 270 271lemma lookup_Some_in_dom: "\<Gamma> p = Some bdy \<Longrightarrow> p \<in> dom \<Gamma>" 272 by auto 273 274lemma unit_object: "(\<forall>u::unit. P u) = P ()" 275 by auto 276 277lemma unit_ex: "(\<exists>u::unit. P u) = P ()" 278 by auto 279 280lemma unit_meta: "(\<And>(u::unit). PROP P u) \<equiv> PROP P ()" 281 by auto 282 283lemma unit_UN: "(\<Union>z::unit. P z) = P ()" 284 by auto 285 286lemma subset_singleton_insert1: "y = x \<Longrightarrow> {y} \<subseteq> insert x A" 287 by auto 288 289lemma subset_singleton_insert2: "{y} \<subseteq> A \<Longrightarrow> {y} \<subseteq> insert x A" 290 by auto 291 292lemma in_Specs_simp: "(\<forall>x\<in>\<Union>Z. {(P Z, p, Q Z, A Z)}. Prop x) = 293 (\<forall>Z. Prop (P Z,p,Q Z,A Z))" 294 by auto 295 296lemma in_set_Un_simp: "(\<forall>x\<in>A \<union> B. P x) = ((\<forall>x \<in> A. P x) \<and> (\<forall>x \<in> B. P x))" 297 by auto 298 299lemma split_all_conj: "(\<forall>x. P x \<and> Q x) = ((\<forall>x. P x) \<and> (\<forall>x. Q x))" 300 by blast 301 302lemma image_Un_single_simp: "f ` (\<Union>Z. {P Z}) = (\<Union>Z. {f (P Z)}) " 303 by auto 304 305 306 307lemma measure_lex_prod_def': 308 "f <*mlex*> r \<equiv> ({(x,y). (x,y) \<in> measure f \<or> f x=f y \<and> (x,y) \<in> r})" 309 by (auto simp add: mlex_prod_def inv_image_def) 310 311lemma in_measure_iff: "(x,y) \<in> measure f = (f x < f y)" 312 by (simp add: measure_def inv_image_def) 313 314lemma in_lex_iff: 315 "((a,b),(x,y)) \<in> r <*lex*> s = ((a,x) \<in> r \<or> (a=x \<and> (b,y)\<in>s))" 316 by (simp add: lex_prod_def) 317 318lemma in_mlex_iff: 319 "(x,y) \<in> f <*mlex*> r = (f x < f y \<or> (f x=f y \<and> (x,y) \<in> r))" 320 by (simp add: measure_lex_prod_def' in_measure_iff) 321 322lemma in_inv_image_iff: "(x,y) \<in> inv_image r f = ((f x, f y) \<in> r)" 323 by (simp add: inv_image_def) 324 325text \<open>This is actually the same as @{thm [source] wf_mlex}. However, this basic 326proof took me so long that I'm not willing to delete it. 327\<close> 328lemma wf_measure_lex_prod [simp,intro]: 329 assumes wf_r: "wf r" 330 shows "wf (f <*mlex*> r)" 331proof (rule ccontr) 332 assume " \<not> wf (f <*mlex*> r)" 333 then 334 obtain g where "\<forall>i. (g (Suc i), g i) \<in> f <*mlex*> r" 335 by (auto simp add: wf_iff_no_infinite_down_chain) 336 hence g: "\<forall>i. (g (Suc i), g i) \<in> measure f \<or> 337 f (g (Suc i)) = f (g i) \<and> (g (Suc i), g i) \<in> r" 338 by (simp add: measure_lex_prod_def') 339 hence le_g: "\<forall>i. f (g (Suc i)) \<le> f (g i)" 340 by (auto simp add: in_measure_iff order_le_less) 341 have "wf (measure f)" 342 by simp 343 hence " \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> measure f \<longrightarrow> y \<notin> Q)" 344 by (simp add: wf_eq_minimal) 345 from this [rule_format, of "g ` UNIV"] 346 have "\<exists>z. z \<in> range g \<and> (\<forall>y. (y, z) \<in> measure f \<longrightarrow> y \<notin> range g)" 347 by auto 348 then obtain z where 349 z: "z \<in> range g" and 350 min_z: "\<forall>y. f y < f z \<longrightarrow> y \<notin> range g" 351 by (auto simp add: in_measure_iff) 352 from z obtain k where 353 k: "z = g k" 354 by auto 355 have "\<forall>i. k \<le> i \<longrightarrow> f (g i) = f (g k)" 356 proof (intro allI impI) 357 fix i 358 assume "k \<le> i" then show "f (g i) = f (g k)" 359 proof (induct i) 360 case 0 361 have "k \<le> 0" by fact hence "k = 0" by simp 362 thus "f (g 0) = f (g k)" 363 by simp 364 next 365 case (Suc n) 366 have k_Suc_n: "k \<le> Suc n" by fact 367 then show "f (g (Suc n)) = f (g k)" 368 proof (cases "k = Suc n") 369 case True 370 thus ?thesis by simp 371 next 372 case False 373 with k_Suc_n 374 have "k \<le> n" 375 by simp 376 with Suc.hyps 377 have n_k: "f (g n) = f (g k)" by simp 378 from le_g have le: "f (g (Suc n)) \<le> f (g n)" 379 by simp 380 show ?thesis 381 proof (cases "f (g (Suc n)) = f (g n)") 382 case True with n_k show ?thesis by simp 383 next 384 case False 385 with le have "f (g (Suc n)) < f (g n)" 386 by simp 387 with n_k k have "f (g (Suc n)) < f z" 388 by simp 389 with min_z have "g (Suc n) \<notin> range g" 390 by blast 391 hence False by simp 392 thus ?thesis 393 by simp 394 qed 395 qed 396 qed 397 qed 398 with k [symmetric] have "\<forall>i. k \<le> i \<longrightarrow> f (g i) = f z" 399 by simp 400 hence "\<forall>i. k \<le> i \<longrightarrow> f (g (Suc i)) = f (g i)" 401 by simp 402 with g have "\<forall>i. k \<le> i \<longrightarrow> (g (Suc i),(g i)) \<in> r" 403 by (auto simp add: in_measure_iff order_less_le ) 404 hence "\<forall>i. (g (Suc (i+k)),(g (i+k))) \<in> r" 405 by simp 406 then 407 have "\<exists>f. \<forall>i. (f (Suc i), f i) \<in> r" 408 by - (rule exI [where x="\<lambda>i. g (i+k)"],simp) 409 with wf_r show False 410 by (simp add: wf_iff_no_infinite_down_chain) 411qed 412 413lemmas all_imp_to_ex = all_simps (5) 414(*"\<And>P Q. (\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)" 415 416 Avoid introduction of existential quantification of states on negative 417 position. 418*) 419 420lemma all_imp_eq_triv: "(\<forall>x. x = k \<longrightarrow> Q) = Q" 421 "(\<forall>x. k = x \<longrightarrow> Q) = Q" 422 by auto 423 424end 425