1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory NonDetMonadLemmaBucket 8imports 9 NonDetMonadVCG 10 MonadEq 11 WhileLoopRulesCompleteness 12 "Word_Lib.Distinct_Prop" 13begin 14setup \<open>AutoLevity_Base.add_attribute_test "wp" WeakestPre.is_wp_rule\<close> 15 16lemma no_fail_assume_pre: 17 "(\<And>s. P s \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail P f" 18 by (simp add: no_fail_def) 19 20lemma no_fail_liftM_eq [simp]: 21 "no_fail P (liftM f m) = no_fail P m" 22 by (auto simp: liftM_def no_fail_def bind_def return_def) 23 24lemma mapME_Cons: 25 "mapME m (x # xs) = (doE y \<leftarrow> m x; ys \<leftarrow> (mapME m xs); returnOk (y # ys) odE)" 26 by (simp add: mapME_def sequenceE_def Let_def) 27 28 29lemma mapME_Nil : "mapME f [] = returnOk []" 30 unfolding mapME_def by (simp add: sequenceE_def) 31 32lemma hoare_take_disjunct: 33 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s \<and> (False \<or> P'' rv s)\<rbrace> 34 \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>P''\<rbrace>" 35 by (erule hoare_strengthen_post, simp) 36 37lemma hoare_post_add: 38 "\<lbrace>P\<rbrace> S \<lbrace>\<lambda>r s. R r s \<and> Q r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> S \<lbrace>Q\<rbrace>" 39 by (erule hoare_strengthen_post, simp) 40 41lemma hoare_disjI1: 42 "\<lbrace>R\<rbrace> f \<lbrace>P\<rbrace> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>\<lambda>r s. P r s \<or> Q r s\<rbrace>" 43 apply (erule hoare_post_imp [rotated]) 44 apply simp 45 done 46 47lemma hoare_disjI2: 48 "\<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>\<lambda>r s. P r s \<or> Q r s \<rbrace>" 49 by (rule hoare_post_imp [OF _ hoare_disjI1, where P1=Q], auto) 50 51lemma hoare_name_pre_state: 52 "\<lbrakk> \<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 53 by (clarsimp simp: valid_def) 54 55lemma hoare_name_pre_stateE: 56 "\<lbrakk>\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" 57 by (clarsimp simp: validE_def2) 58 59lemma valid_prove_more: 60 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>" 61 by (erule hoare_strengthen_post, simp) 62 63lemma hoare_vcg_if_lift: 64 "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow> 65 \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P then X rv s else Y rv s\<rbrace>" 66 67 "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow> 68 \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P then X rv else Y rv\<rbrace>" 69 by (auto simp: valid_def split_def) 70 71lemma hoare_lift_Pf2: 72 assumes P: "\<And>x. \<lbrace>Q x\<rbrace> m \<lbrace>\<lambda>_. P x\<rbrace>" 73 assumes f: "\<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>" 74 shows "\<lbrace>\<lambda>s. Q (f s) s\<rbrace> m \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>" 75 apply (clarsimp simp add: valid_def) 76 apply (frule (1) use_valid [OF _ P], drule (2) use_valid [OF _ f]) 77 done 78 79lemma hoare_lift_Pf3: 80 assumes P: "\<And>x. \<lbrace>Q x\<rbrace> m \<lbrace>P x\<rbrace>" 81 assumes f: "\<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>" 82 shows "\<lbrace>\<lambda>s. Q (f s) s\<rbrace> m \<lbrace>\<lambda>rv s. P (f s) rv s\<rbrace>" 83 apply (clarsimp simp add: valid_def) 84 apply (frule (1) use_valid [OF _ P], drule (2) use_valid [OF _ f]) 85 done 86 87lemma no_fail_select_f [wp]: 88 "no_fail (\<lambda>s. \<not>snd S) (select_f S)" 89 by (simp add: select_f_def no_fail_def) 90 91lemma hoare_lift_Pf: 92 assumes P: "\<And>x. \<lbrace>P x\<rbrace> m \<lbrace>\<lambda>_. P x\<rbrace>" 93 assumes f: "\<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>" 94 shows "\<lbrace>\<lambda>s. P (f s) s\<rbrace> m \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>" 95 apply (clarsimp simp add: valid_def) 96 apply (frule (1) use_valid [OF _ P], drule (2) use_valid [OF _ f]) 97 done 98 99lemma assert_def2: "assert v = assert_opt (if v then Some () else None)" 100 by (cases v, simp_all add: assert_def assert_opt_def) 101 102lemma hoare_if_r_and: 103 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. if R r then Q r else Q' r\<rbrace> 104 = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. (R r \<longrightarrow> Q r s) \<and> (\<not>R r \<longrightarrow> Q' r s)\<rbrace>" 105 by (fastforce simp: valid_def) 106 107 108lemma no_fail_liftM [wp]: 109 "no_fail P m \<Longrightarrow> no_fail P (liftM f m)" 110 by (simp) 111 112lemma no_fail_pre_and: 113 "no_fail P f \<Longrightarrow> no_fail (P and Q) f" 114 by (erule no_fail_pre) simp 115 116lemma hoare_convert_imp: 117 "\<lbrakk> \<lbrace>\<lambda>s. \<not> P s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> Q s\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk> \<Longrightarrow> 118 \<lbrace>\<lambda>s. P s \<longrightarrow> R s\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> S rv s\<rbrace>" 119 apply (simp only: imp_conv_disj) 120 apply (erule(1) hoare_vcg_disj_lift) 121 done 122 123lemma hoare_vcg_ex_lift_R: 124 "\<lbrakk> \<And>v. \<lbrace>P v\<rbrace> f \<lbrace>Q v\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>v. P v s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>v. Q v rv s\<rbrace>,-" 125 apply (simp add: validE_R_def validE_def) 126 apply (rule hoare_strengthen_post, erule hoare_vcg_ex_lift) 127 apply (auto split: sum.split) 128 done 129 130lemma hoare_case_option_wpR: 131 "\<lbrakk>\<lbrace>P\<rbrace> f None \<lbrace>Q\<rbrace>,-; \<And>x. \<lbrace>P' x\<rbrace> f (Some x) \<lbrace>Q' x\<rbrace>,-\<rbrakk> \<Longrightarrow> 132 \<lbrace>case_option P P' v\<rbrace> f v \<lbrace>\<lambda>rv. case v of None \<Rightarrow> Q rv | Some x \<Rightarrow> Q' x rv\<rbrace>,-" 133 by (cases v) auto 134 135 136lemma hoare_vcg_conj_liftE_R: 137 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>,-; \<lbrace>Q\<rbrace> f \<lbrace>Q'\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s \<and> Q' rv s\<rbrace>, -" 138 apply (simp add: validE_R_def validE_def valid_def split: sum.splits) 139 apply blast 140 done 141 142lemma zipWithM_x_inv: 143 assumes x: "\<And>x y. \<lbrace>P\<rbrace> m x y \<lbrace>\<lambda>rv. P\<rbrace>" 144 shows "length xs = length ys \<Longrightarrow> \<lbrace>P\<rbrace> zipWithM_x m xs ys \<lbrace>\<lambda>rv. P\<rbrace>" 145proof (induct xs ys rule: list_induct2) 146 case Nil 147 show ?case 148 by (simp add: zipWithM_x_def sequence_x_def zipWith_def) 149next 150 case (Cons a as b bs) 151 have zipWithM_x_Cons: 152 "\<And>m x xs y ys. zipWithM_x m (x # xs) (y # ys) 153 = do m x y; zipWithM_x m xs ys od" 154 by (simp add: zipWithM_x_def sequence_x_def zipWith_def) 155 have IH: "\<lbrace>P\<rbrace> zipWithM_x m as bs \<lbrace>\<lambda>rv. P\<rbrace>" 156 by fact 157 show ?case 158 by (simp add: zipWithM_x_Cons) (wp IH x) 159qed 160 161lemma K_valid[wp]: 162 "\<lbrace>K P\<rbrace> f \<lbrace>\<lambda>_. K P\<rbrace>" 163 by (simp add: valid_def) 164 165lemma mapME_wp: 166 assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>" 167 shows "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>" 168 apply (induct xs) 169 apply (simp add: mapME_def sequenceE_def) 170 apply wp 171 apply simp 172 apply (simp add: mapME_Cons) 173 apply (wp x|simp)+ 174 done 175 176lemmas mapME_wp' = mapME_wp [OF _ subset_refl] 177 178lemma sequence_x_Cons: "\<And>x xs. sequence_x (x # xs) = (x >>= (\<lambda>_. sequence_x xs))" 179 by (simp add: sequence_x_def) 180 181lemma mapM_Cons: "mapM m (x # xs) = (do y \<leftarrow> m x; ys \<leftarrow> (mapM m xs); return (y # ys) od)" 182 by (simp add: mapM_def sequence_def Let_def) 183 184lemma mapM_simps: 185 "mapM m [] = return []" 186 "mapM m (x#xs) = do r \<leftarrow> m x; rs \<leftarrow> (mapM m xs); return (r#rs) od" 187 by (simp_all add: mapM_def sequence_def) 188 189lemma zipWithM_x_mapM: 190 "zipWithM_x f as bs = (mapM (split f) (zip as bs) >>= (\<lambda>_. return ()))" 191 apply (simp add: zipWithM_x_def zipWith_def) 192 apply (induct ("zip as bs")) 193 apply (simp add: sequence_x_def mapM_def sequence_def) 194 apply (simp add: sequence_x_Cons mapM_Cons bind_assoc) 195 done 196 197(* zipWithM_x and mapM_ *) 198 199lemma mapM_wp: 200 assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>" 201 shows "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>" 202 apply (induct xs) 203 apply (simp add: mapM_def sequence_def) 204 apply (simp add: mapM_Cons) 205 apply wp 206 apply (rule x, clarsimp) 207 apply simp 208 done 209 210lemma mapM_x_mapM: 211 "mapM_x m l = (mapM m l >>= (\<lambda>x. return ()))" 212 apply (simp add: mapM_x_def sequence_x_def mapM_def sequence_def) 213 apply (induct l, simp_all add: Let_def bind_assoc) 214 done 215 216lemma mapM_x_wp: 217 assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>" 218 shows "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv. P\<rbrace>" 219 by (subst mapM_x_mapM) (wp mapM_wp x) 220 221lemma mapM_x_Nil: 222 "mapM_x f [] = return ()" 223 unfolding mapM_x_def sequence_x_def 224 by simp 225 226lemma sequence_xappend1: 227 "sequence_x (xs @ [x]) = (sequence_x xs >>= (\<lambda>_. x))" 228 by (induct xs) (simp add: sequence_x_def, simp add: sequence_x_Cons bind_assoc) 229 230lemma mapM_append_single: 231 "mapM_x f (xs @ [y]) = (mapM_x f xs >>= (\<lambda>_. f y))" 232 unfolding mapM_x_def 233 by (simp add: sequence_xappend1) 234 235lemma mapM_x_Cons: 236 "mapM_x m (x # xs) = (do m x; mapM_x m xs od)" 237 by (simp add: mapM_x_def sequence_x_def) 238 239lemma mapM_x_inv_wp2: 240 assumes post: "\<And>s. \<lbrakk> I s; V [] s \<rbrakk> \<Longrightarrow> Q s" 241 and hr: "\<And>a as. suffix (a # as) xs \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> V (a # as) s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V as s\<rbrace>" 242 shows "\<lbrace>I and V xs\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv. Q\<rbrace>" 243proof (induct xs rule: list_induct_suffix) 244 case Nil thus ?case 245 apply (simp add: mapM_x_Nil) 246 apply wp 247 apply (clarsimp intro!: post) 248 done 249next 250 case (Cons x xs) 251 thus ?case 252 apply (simp add: mapM_x_Cons) 253 apply wp 254 apply (wp hr) 255 apply assumption 256 done 257qed 258 259lemma zipWithM_x_mapM_x: 260 "zipWithM_x f as bs = mapM_x (\<lambda>(x, y). f x y) (zip as bs)" 261 apply (subst zipWithM_x_mapM) 262 apply (subst mapM_x_mapM) 263 apply (rule refl) 264 done 265 266lemma zipWithM_x_append1: 267 fixes f :: "'b \<Rightarrow> 'c \<Rightarrow> ('a, unit) nondet_monad" 268 assumes ls: "length xs = length ys" 269 shows "(zipWithM_x f (xs @ [x]) (ys @ [y])) = (zipWithM_x f xs ys >>= (\<lambda>_. f x y))" 270 unfolding zipWithM_x_def zipWith_def 271 by (subst zip_append [OF ls], simp, rule sequence_xappend1) 272 273lemma zipWithM_x_Cons: 274 assumes ls: "length xs = length ys" 275 shows "(zipWithM_x f (x # xs) (y # ys)) = (f x y >>= (\<lambda>_. zipWithM_x f xs ys))" 276 unfolding zipWithM_x_def zipWith_def 277 by (simp, rule sequence_x_Cons) 278 279lemma mapM_x_inv_wp3: 280 fixes m :: "'b \<Rightarrow> ('a, unit) nondet_monad" 281 assumes hr: "\<And>a as bs. xs = as @ [a] @ bs \<Longrightarrow> 282 \<lbrace>\<lambda>s. I s \<and> V as s\<rbrace> m a \<lbrace>\<lambda>r s. I s \<and> V (as @ [a]) s\<rbrace>" 283 shows "\<lbrace>\<lambda>s. I s \<and> V [] s\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv s. I s \<and> V xs s\<rbrace>" 284 using hr 285proof (induct xs rule: rev_induct) 286 case Nil thus ?case 287 apply (simp add: mapM_x_Nil) 288 done 289next 290 case (snoc x xs) 291 show ?case 292 apply (simp add: mapM_append_single) 293 apply (wp snoc.prems) 294 apply simp 295 apply (rule snoc.hyps [OF snoc.prems]) 296 apply simp 297 apply assumption 298 done 299qed 300 301 302lemma mapME_x_map_simp: 303 "mapME_x m (map f xs) = mapME_x (m o f) xs" 304 by (simp add: mapME_x_def sequenceE_x_def) 305 306lemma mapM_return: 307 "mapM (\<lambda>x. return (f x)) xs = return (map f xs)" 308 apply (induct xs) 309 apply (simp add: mapM_def sequence_def) 310 apply (simp add: mapM_Cons) 311 done 312 313lemma mapME_x_inv_wp: 314 assumes x: "\<And>x. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>,\<lbrace>E\<rbrace>" 315 shows "\<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>,\<lbrace>E\<rbrace>" 316 apply (induct xs) 317 apply (simp add: mapME_x_def sequenceE_x_def) 318 apply wp 319 apply (simp add: mapME_x_def sequenceE_x_def) 320 apply (fold mapME_x_def sequenceE_x_def) 321 apply wp 322 apply (rule x) 323 apply assumption 324 done 325 326lemma liftM_return [simp]: 327 "liftM f (return x) = return (f x)" 328 by (simp add: liftM_def) 329 330lemma mapM_x_return : 331 "mapM_x (\<lambda>_. return v) xs = return v" 332 by (induct xs) (auto simp: mapM_x_Nil mapM_x_Cons) 333 334lemma hoare_imp_eq_substR: 335 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<longrightarrow> Q x s\<rbrace>,-" 336 by (fastforce simp add: valid_def validE_R_def validE_def split: sum.splits) 337 338lemma hoare_split_bind_case_sum: 339 assumes x: "\<And>rv. \<lbrace>R rv\<rbrace> g rv \<lbrace>Q\<rbrace>" 340 "\<And>rv. \<lbrace>S rv\<rbrace> h rv \<lbrace>Q\<rbrace>" 341 assumes y: "\<lbrace>P\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>" 342 shows "\<lbrace>P\<rbrace> f >>= case_sum g h \<lbrace>Q\<rbrace>" 343 apply (rule hoare_seq_ext [OF _ y[unfolded validE_def]]) 344 apply (case_tac x, simp_all add: x) 345 done 346 347lemma hoare_split_bind_case_sumE: 348 assumes x: "\<And>rv. \<lbrace>R rv\<rbrace> g rv \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 349 "\<And>rv. \<lbrace>S rv\<rbrace> h rv \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 350 assumes y: "\<lbrace>P\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>" 351 shows "\<lbrace>P\<rbrace> f >>= case_sum g h \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 352 apply (unfold validE_def) 353 apply (rule hoare_seq_ext [OF _ y[unfolded validE_def]]) 354 apply (case_tac x, simp_all add: x [unfolded validE_def]) 355 done 356 357lemma bind_comm_mapM_comm: 358 assumes bind_comm: 359 "\<And>n z. do x \<leftarrow> a; y \<leftarrow> b z; (n x y :: ('a, 's) nondet_monad) od = 360 do y \<leftarrow> b z; x \<leftarrow> a; n x y od" 361 shows "\<And>n'. do x \<leftarrow> a; ys \<leftarrow> mapM b zs; (n' x ys :: ('a, 's) nondet_monad) od = 362 do ys \<leftarrow> mapM b zs; x \<leftarrow> a; n' x ys od" 363proof (induct zs) 364 case Nil 365 thus ?case 366 by (simp add: mapM_def sequence_def) 367 next 368 case (Cons z zs') 369 thus ?case 370 by (clarsimp simp: mapM_Cons bind_assoc bind_comm intro!: bind_cong [OF refl]) 371qed 372 373lemma liftE_handle : 374 "(liftE f <handle> g) = liftE f" 375 by (simp add: handleE_def handleE'_def liftE_def) 376 377lemma mapM_empty: 378 "mapM f [] = return []" 379 unfolding mapM_def 380 by (simp add: sequence_def) 381 382lemma mapM_append: 383 "mapM f (xs @ ys) = 384 (do x \<leftarrow> mapM f xs; 385 y \<leftarrow> mapM f ys; 386 return (x @ y) 387 od)" 388proof (induct xs) 389 case Nil 390 thus ?case by (simp add: mapM_empty) 391next 392 case (Cons x xs) 393 394 show ?case 395 by (simp add: mapM_Cons bind_assoc Cons.hyps) 396qed 397 398lemma mapM_x_append: 399 "mapM_x f (xs @ ys) = 400 (do x \<leftarrow> mapM_x f xs; 401 y \<leftarrow> mapM_x f ys; 402 return () 403 od)" 404 by (simp add: mapM_x_mapM mapM_append bind_assoc) 405 406lemma mapM_singleton: 407 "mapM f [x] = (do r \<leftarrow> f x; return [r] od)" 408 by (simp add: mapM_def sequence_def) 409 410lemma mapM_x_singleton: 411 "mapM_x f [x] = f x" 412 by (simp add: mapM_x_mapM mapM_singleton) 413 414lemma return_returnOk: 415 "return (Inr x) = returnOk x" 416 unfolding returnOk_def by simp 417 418lemma mapME_x_sequenceE: 419 "mapME_x f xs \<equiv> doE _ \<leftarrow> sequenceE (map f xs); returnOk () odE" 420 apply (induct xs, simp_all add: mapME_x_def sequenceE_def sequenceE_x_def) 421 apply (simp add: Let_def bindE_assoc) 422 done 423 424lemma sequenceE_Cons: 425 "sequenceE (x # xs) = (doE v \<leftarrow> x; vs \<leftarrow> sequenceE xs; returnOk (v # vs) odE)" 426 by (simp add: sequenceE_def Let_def) 427 428lemma snd_return [monad_eq]: 429 "\<not> snd (return a b)" 430 unfolding return_def by simp 431 432lemma snd_throwError [monad_eq]: 433 "\<not> snd (throwError e s)" 434 unfolding throwError_def by (simp add: snd_return) 435 436lemma snd_lift_Inr [monad_eq]: 437 "snd (lift b (Inr r) t) = snd (b r t)" 438 unfolding lift_def by simp 439 440lemma snd_lift_Inl [monad_eq]: 441 "\<not> snd (lift b (Inl r) t)" 442 unfolding lift_def by (simp add: snd_throwError) 443 444lemma snd_fail [monad_eq]: 445 "snd (fail s)" 446 apply (clarsimp simp: fail_def) 447 done 448 449lemma not_snd_bindD: 450 "\<lbrakk> \<not> snd ((a >>= b) s); (rv, s') \<in> fst (a s) \<rbrakk> \<Longrightarrow> \<not> snd (a s) \<and> \<not> snd (b rv s')" 451 by (fastforce simp: bind_def) 452 453lemma whenE_bindE_throwError_to_if: 454 "whenE P (throwError e) >>=E (\<lambda>_. b) = (if P then (throwError e) else b)" 455 unfolding whenE_def bindE_def 456 by (auto simp: NonDetMonad.lift_def throwError_def returnOk_def) 457 458lemma not_snd_bindI1: 459 "\<not> snd ((a >>= b) s) \<Longrightarrow> \<not> snd (a s)" 460 by (fastforce simp: bind_def) 461 462lemma not_snd_bindI2: 463 "\<lbrakk> \<not> snd ((a >>= b) s); (rv, s') \<in> fst (a s) \<rbrakk> \<Longrightarrow> \<not> snd (b rv s')" 464 by (fastforce simp: bind_def) 465 466lemma empty_fail_not_snd: 467 "\<lbrakk> \<not> snd (m s); empty_fail m \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> fst (m s)" 468 by (fastforce simp: empty_fail_def) 469 470lemma mapM_Nil: 471 "mapM f [] = return []" 472 by (simp add: mapM_def sequence_def) 473 474lemma hoare_vcg_exI: 475 "\<lbrace>P\<rbrace> f \<lbrace>Q x\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>" 476 apply (simp add: valid_def split_def) 477 apply blast 478 done 479 480lemma hoare_exI_tuple: 481 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>(rv,rv') s. Q x rv rv' s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>(rv,rv') s. \<exists>x. Q x rv rv' s\<rbrace>" 482 by (fastforce simp: valid_def) 483 484lemma hoare_ex_all: 485 "(\<forall>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>) = \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>" 486 apply (rule iffI) 487 apply (fastforce simp: valid_def)+ 488 done 489 490lemma empty_fail_bindE: 491 "\<lbrakk> empty_fail f; \<And>rv. empty_fail (g rv) \<rbrakk> 492 \<Longrightarrow> empty_fail (f >>=E g)" 493 apply (simp add: bindE_def) 494 apply (erule empty_fail_bind) 495 apply (simp add: lift_def throwError_def split: sum.split) 496 done 497 498lemma empty_fail_error_bits: 499 "empty_fail (returnOk v)" 500 "empty_fail (throwError v)" 501 "empty_fail (liftE f) = empty_fail f" 502 apply (simp_all add: returnOk_def throwError_def) 503 apply (rule iffI, simp_all add: liftE_def) 504 apply (simp add: empty_fail_def bind_def return_def) 505 apply (erule allEI) 506 apply clarsimp 507 done 508 509 510lemma mapM_upd: 511 assumes "\<And>x rv s s'. (rv,s') \<in> fst (f x s) \<Longrightarrow> x \<in> set xs \<Longrightarrow> (rv, g s') \<in> fst (f x (g s))" 512 shows "(rv,s') \<in> fst (mapM f xs s) \<Longrightarrow> (rv, g s') \<in> fst (mapM f xs (g s))" 513 using assms 514proof (induct xs arbitrary: rv s s') 515 case Nil 516 thus ?case by (simp add: mapM_Nil return_def) 517next 518 case (Cons z zs) 519 from Cons.prems 520 show ?case 521 apply (clarsimp simp: mapM_Cons in_monad) 522 apply (drule Cons.prems, simp) 523 apply (rule exI, erule conjI) 524 apply (erule Cons.hyps) 525 apply (erule Cons.prems) 526 apply simp 527 done 528qed 529 530definition 531 cutMon :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad" where 532 "cutMon P f \<equiv> \<lambda>s. if P s then f s else fail s" 533 534lemma cutMon_walk_bind: 535 "(cutMon ((=) s) (f >>= g)) 536 = (cutMon ((=) s) f >>= (\<lambda>rv. cutMon (\<lambda>s'. (rv, s') \<in> fst (f s)) (g rv)))" 537 apply (rule ext, simp add: cutMon_def bind_def fail_def) 538 apply (auto simp: split_def) 539 done 540 541lemma cutMon_walk_bindE: 542 "(cutMon ((=) s) (f >>=E g)) 543 = (cutMon ((=) s) f >>=E (\<lambda>rv. cutMon (\<lambda>s'. (Inr rv, s') \<in> fst (f s)) (g rv)))" 544 apply (simp add: bindE_def cutMon_walk_bind) 545 apply (rule bind_cong, rule refl) 546 apply (simp add: cutMon_def lift_def fail_def 547 split: if_split_asm) 548 apply (clarsimp split: sum.split) 549 done 550 551lemma cutMon_walk_if: 552 "cutMon ((=) s) (if P then f else g) 553 = (if P then cutMon ((=) s) f else cutMon ((=) s) g)" 554 by (simp add: cutMon_def) 555 556lemma cutMon_valid_drop: 557 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> cutMon R f \<lbrace>Q\<rbrace>" 558 by (simp add: cutMon_def valid_def fail_def) 559 560lemma cutMon_validE_drop: 561 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> cutMon R f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 562 by (simp add: validE_def cutMon_valid_drop) 563 564lemma assertE_assert: 565 "assertE F = liftE (assert F)" 566 by (clarsimp simp: assertE_def assert_def liftE_def returnOk_def 567 split: if_split) 568 569lemma snd_cutMon: 570 "snd (cutMon P f s) = (P s \<longrightarrow> snd (f s))" 571 by (simp add: cutMon_def fail_def split: if_split) 572 573lemma exec_modify: 574 "(modify f >>= g) s = g () (f s)" 575 by (simp add: bind_def simpler_modify_def) 576 577lemma no_fail_spec: 578 "\<lbrakk> \<And>s. no_fail (((=) s) and P) f \<rbrakk> \<Longrightarrow> no_fail P f" 579 by (simp add: no_fail_def) 580 581lemma no_fail_assertE [wp]: 582 "no_fail (\<lambda>_. P) (assertE P)" 583 by (simp add: assertE_def split: if_split) 584 585lemma no_fail_spec_pre: 586 "\<lbrakk> no_fail (((=) s) and P') f; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> no_fail (((=) s) and P) f" 587 by (erule no_fail_pre, simp) 588 589lemma no_fail_whenE [wp]: 590 "\<lbrakk> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. G \<longrightarrow> P s) (whenE G f)" 591 by (simp add: whenE_def split: if_split) 592 593lemma no_fail_unlessE [wp]: 594 "\<lbrakk> \<not> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. \<not> G \<longrightarrow> P s) (unlessE G f)" 595 by (simp add: unlessE_def split: if_split) 596 597lemma no_fail_throwError [wp]: 598 "no_fail \<top> (throwError e)" 599 by (simp add: throwError_def) 600 601lemma no_fail_liftE [wp]: 602 "no_fail P f \<Longrightarrow> no_fail P (liftE f)" 603 unfolding liftE_def by wpsimp 604 605lemma bind_return_eq: 606 "(a >>= return) = (b >>= return) \<Longrightarrow> a = b" 607 apply (clarsimp simp:bind_def) 608 apply (rule ext) 609 apply (drule_tac x= x in fun_cong) 610 apply (auto simp:return_def split_def) 611 done 612 613lemma bindE_bind_linearise: 614 "((f >>=E g) >>= h) = 615 (f >>= case_sum (h o Inl) (\<lambda>rv. g rv >>= h))" 616 apply (simp add: bindE_def bind_assoc) 617 apply (rule ext, rule bind_apply_cong, rule refl) 618 apply (simp add: lift_def throwError_def split: sum.split) 619 done 620 621lemma throwError_bind: 622 "(throwError e >>= f) = (f (Inl e))" 623 by (simp add: throwError_def) 624 625lemma bind_bindE_assoc: 626 "((f >>= g) >>=E h) 627 = f >>= (\<lambda>rv. g rv >>=E h)" 628 by (simp add: bindE_def bind_assoc) 629 630lemma returnOk_bind: 631 "returnOk v >>= f = (f (Inr v))" 632 by (simp add: returnOk_def) 633 634lemma liftE_bind: 635 "(liftE m >>= m') = (m >>= (\<lambda>rv. m' (Inr rv)))" 636 by (simp add: liftE_def) 637 638lemma catch_throwError: "catch (throwError ft) g = g ft" 639 by (simp add: catch_def throwError_bind) 640 641lemma select_bind_eq2: 642 "\<lbrakk> v = v'; \<And>x. x \<in> fst v \<Longrightarrow> f x s = g x s' \<rbrakk> \<Longrightarrow> 643 (select_f v >>= f) s = (select_f v' >>= g) s'" 644 by (simp add: select_f_def bind_def split_def 645 cart_singleton_image image_image 646 cong: image_cong) 647 648lemmas select_bind_eq = select_bind_eq2[OF refl] 649 650lemma select_f_singleton_return: 651 "select_f ({v}, False) = return v" 652 by (simp add: select_f_def return_def) 653 654lemma select_f_returns: 655 "select_f (return v s) = return (v, s)" 656 "select_f (get s) = return (s, s)" 657 "select_f (gets f s) = return (f s, s)" 658 "select_f (modify g s) = return ((), g s)" 659 by (simp add: select_f_def return_def get_def 660 simpler_gets_def simpler_modify_def)+ 661 662lemma select_eq_select_f: 663 "select S = select_f (S, False)" 664 by (simp add: select_def select_f_def) 665 666lemma select_f_select_f: 667 "select_f (select_f v s) = liftM (swp Pair s) (select_f v)" 668 apply (rule ext) 669 apply (simp add: select_f_def liftM_def swp_def 670 bind_def return_def split_def 671 image_image image_constant_conv) 672 apply fastforce 673 done 674 675lemma select_f_select: 676 "select_f (select S s) = liftM (swp Pair s) (select S)" 677 unfolding select_eq_select_f by (rule select_f_select_f) 678 679lemmas select_f_selects = select_f_select_f select_f_select 680 681lemma select_f_asserts: 682 "select_f (fail s) = fail" 683 "select_f (assert P s) = do assert P; return ((), s) od" 684 "select_f (assert_opt v s) = do v' \<leftarrow> assert_opt v; return (v', s) od" 685 by (simp add: select_f_def fail_def assert_def return_def bind_def 686 assert_opt_def split: if_split option.split)+ 687 688lemma liftE_bindE_handle: 689 "((liftE f >>=E (\<lambda>x. g x)) <handle> h) 690 = f >>= (\<lambda>x. g x <handle> h)" 691 by (simp add: liftE_bindE handleE_def handleE'_def 692 bind_assoc) 693 694lemma in_returns [monad_eq]: 695 "(r, s) \<in> fst (return r s)" 696 "(Inr r, s) \<in> fst (returnOk r s)" 697 by (simp add: in_monad)+ 698 699lemma assertE_sp: 700 "\<lbrace>P\<rbrace> assertE Q \<lbrace>\<lambda>rv s. Q \<and> P s\<rbrace>,\<lbrace>E\<rbrace>" 701 by (clarsimp simp: assertE_def) wp 702 703lemma catch_liftE: 704 "catch (liftE g) h = g" 705 by (simp add: catch_def liftE_def) 706 707lemma catch_liftE_bindE: 708 "catch (liftE g >>=E (\<lambda>x. f x)) h = g >>= (\<lambda>x. catch (f x) h)" 709 by (simp add: liftE_bindE catch_def bind_assoc) 710 711lemma returnOk_catch_bind: 712 "catch (returnOk v) h >>= g = g v" 713 by (simp add: returnOk_liftE catch_liftE) 714 715lemma alternative_left_readonly_bind: 716 "\<lbrakk> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; fst (f s) \<noteq> {} \<rbrakk> \<Longrightarrow> 717 alternative (f >>= (\<lambda>x. g x)) h s 718 = (f >>= (\<lambda>x. alternative (g x) h)) s" 719 apply (subgoal_tac "\<forall>x \<in> fst (f s). snd x = s") 720 apply (clarsimp simp: alternative_def bind_def split_def) 721 apply fastforce 722 apply clarsimp 723 apply (drule(1) use_valid, simp_all) 724 done 725 726lemma liftE_bindE_assoc: 727 "(liftE f >>=E g) >>= h = f >>= (\<lambda>x. g x >>= h)" 728 by (simp add: liftE_bindE bind_assoc) 729 730lemma empty_fail_use_cutMon: 731 "\<lbrakk> \<And>s. empty_fail (cutMon ((=) s) f) \<rbrakk> \<Longrightarrow> empty_fail f" 732 apply (clarsimp simp add: empty_fail_def cutMon_def) 733 apply (fastforce split: if_split_asm) 734 done 735 736lemma empty_fail_drop_cutMon: 737 "empty_fail f \<Longrightarrow> empty_fail (cutMon P f)" 738 by (simp add: empty_fail_def fail_def cutMon_def split: if_split) 739 740lemma empty_fail_cutMon: 741 "\<lbrakk> \<And>s. P s \<Longrightarrow> empty_fail (cutMon ((=) s) f) \<rbrakk> 742 \<Longrightarrow> empty_fail (cutMon P f)" 743 apply (clarsimp simp: empty_fail_def cutMon_def fail_def 744 split: if_split) 745 apply (fastforce split: if_split_asm) 746 done 747 748lemma empty_fail_If: 749 "\<lbrakk> P \<Longrightarrow> empty_fail f; \<not> P \<Longrightarrow> empty_fail g \<rbrakk> \<Longrightarrow> empty_fail (if P then f else g)" 750 by (simp split: if_split) 751 752lemmas empty_fail_cutMon_intros = 753 cutMon_walk_bind[THEN arg_cong[where f=empty_fail], THEN iffD2, 754 OF empty_fail_bind, OF _ empty_fail_cutMon] 755 cutMon_walk_bindE[THEN arg_cong[where f=empty_fail], THEN iffD2, 756 OF empty_fail_bindE, OF _ empty_fail_cutMon] 757 cutMon_walk_if[THEN arg_cong[where f=empty_fail], THEN iffD2, 758 OF empty_fail_If] 759 760lemma empty_fail_whenEs: 761 "empty_fail f \<Longrightarrow> empty_fail (whenE P f)" 762 "empty_fail f \<Longrightarrow> empty_fail (unlessE P f)" 763 by (auto simp add: whenE_def unlessE_def empty_fail_error_bits split: if_split) 764 765lemma empty_fail_assertE: 766 "empty_fail (assertE P)" 767 by (simp add: assertE_def empty_fail_error_bits split: if_split) 768 769lemma unlessE_throw_catch_If: 770 "catch (unlessE P (throwError e) >>=E f) g 771 = (if P then catch (f ()) g else g e)" 772 by (simp add: unlessE_def catch_throwError split: if_split) 773 774lemma gets_the_return: 775 "(return x = gets_the f) = (\<forall>s. f s = Some x)" 776 apply (subst fun_eq_iff) 777 apply (simp add: return_def gets_the_def exec_gets 778 assert_opt_def fail_def 779 split: option.split) 780 apply auto 781 done 782 783lemma gets_the_returns[unfolded K_def]: 784 "(return x = gets_the f) = (\<forall>s. f s = Some x)" 785 "(returnOk x = gets_the g) = (\<forall>s. g s = Some (Inr x))" 786 "(throwError x = gets_the h) = (\<forall>s. h s = Some (Inl x))" 787 by (simp_all add: returnOk_def throwError_def 788 gets_the_return) 789 790lemma all_rv_choice_fn_eq: 791 "\<lbrakk> \<And>rv. \<exists>fn. f rv = g fn \<rbrakk> 792 \<Longrightarrow> \<exists>fn. f = (\<lambda>rv. g (fn rv))" 793 using all_rv_choice_fn_eq_pred[where f=f and g=g and P=\<top>] 794 by (simp add: fun_eq_iff) 795 796lemma cutMon_assert_opt: 797 "cutMon P (gets_the f >>= g) 798 = gets_the (\<lambda>s. if P s then f s else None) >>= g" 799 by (simp add: cutMon_def gets_the_def exec_gets 800 bind_assoc fun_eq_iff assert_opt_def 801 split: if_split) 802 803lemma gets_the_eq_bind: 804 "\<lbrakk> \<exists>fn. f = gets_the (fn o fn'); 805 \<And>rv. \<exists>fn. g rv 806 = gets_the (fn o fn') \<rbrakk> 807 \<Longrightarrow> \<exists>fn. (f >>= g) = gets_the (fn o fn')" 808 apply (clarsimp dest!: all_rv_choice_fn_eq) 809 apply (rule_tac x="\<lambda>s. case (fn s) of None \<Rightarrow> None | Some v \<Rightarrow> fna v s" in exI) 810 apply (simp add: gets_the_def bind_assoc exec_gets 811 assert_opt_def fun_eq_iff 812 split: option.split) 813 done 814 815lemma gets_the_eq_bindE: 816 "\<lbrakk> \<exists>fn. f = gets_the (fn o fn'); 817 \<And>rv. \<exists>fn. g rv = gets_the (fn o fn') \<rbrakk> 818 \<Longrightarrow> \<exists>fn. (f >>=E g) = gets_the (fn o fn')" 819 apply (simp add: bindE_def) 820 apply (erule gets_the_eq_bind) 821 apply (simp add: lift_def gets_the_returns split: sum.split) 822 apply fastforce 823 done 824 825lemma gets_the_fail: 826 "(fail = gets_the f) = (\<forall>s. f s = None)" 827 by (simp add: gets_the_def exec_gets assert_opt_def 828 fail_def return_def fun_eq_iff 829 split: option.split) 830 831lemma gets_the_asserts: 832 "(fail = gets_the f) = (\<forall>s. f s = None)" 833 "(assert P = gets_the g) = (\<forall>s. g s = (if P then Some () else None))" 834 "(assertE P = gets_the h) = (\<forall>s. h s = (if P then Some (Inr ()) else None))" 835 by (simp add: assert_def assertE_def 836 gets_the_fail gets_the_returns 837 split: if_split)+ 838 839lemma gets_the_condsE: 840 "(\<exists>fn. whenE P f = gets_the (fn o fn')) 841 = (P \<longrightarrow> (\<exists>fn. f = gets_the (fn o fn')))" 842 "(\<exists>fn. unlessE P g = gets_the (fn o fn')) 843 = (\<not> P \<longrightarrow> (\<exists>fn. g = gets_the (fn o fn')))" 844 by (simp add: whenE_def unlessE_def gets_the_returns 845 ex_const_function 846 split: if_split)+ 847 848lemma no_fail_gets_the [wp]: 849 "no_fail (\<lambda>s. f s \<noteq> None) (gets_the f)" 850 apply (simp add: gets_the_def) 851 apply (rule no_fail_pre, wp) 852 apply simp 853 done 854 855lemma gets_the_validE_R_wp: 856 "\<lbrace>\<lambda>s. f s \<noteq> None \<and> isRight (the (f s)) \<and> Q (theRight (the (f s))) s\<rbrace> 857 gets_the f 858 \<lbrace>Q\<rbrace>,-" 859 apply (simp add: gets_the_def validE_R_def validE_def) 860 apply (wp | wpc | simp add: assert_opt_def)+ 861 apply (clarsimp split: split: sum.splits) 862 done 863 864lemma return_bindE: 865 "isRight v \<Longrightarrow> return v >>=E f = f (theRight v)" 866 by (clarsimp simp: isRight_def return_returnOk) 867 868lemma assert_opt_If: 869 "assert_opt v = If (v = None) fail (return (the v))" 870 by (simp_all add: assert_opt_def split: option.split) 871 872lemma if_to_top_of_bind: 873 "(bind (If P x y) z) = If P (bind x z) (bind y z)" 874 by (simp split: if_split) 875 876lemma if_to_top_of_bindE: 877 "(bindE (If P x y) z) = If P (bindE x z) (bindE y z)" 878 by (simp split: if_split) 879 880lemma alternative_bind: 881 "((a \<sqinter> b) >>= c) = ((a >>= c) \<sqinter> (b >>= c))" 882 apply (rule ext, simp add: alternative_def bind_def split_def) 883 apply blast 884 done 885 886lemma alternative_refl: 887 "(a \<sqinter> a) = a" 888 by (rule ext, simp add: alternative_def) 889 890lemma alternative_com: 891 "(f \<sqinter> g) = (g \<sqinter> f)" 892 apply (rule ext) 893 apply (auto simp: alternative_def) 894 done 895 896lemma liftE_alternative: 897 "liftE (a \<sqinter> b) = (liftE a \<sqinter> liftE b)" 898 by (simp add: liftE_def alternative_bind) 899 900lemma fst_return: 901 "fst (return v s) = {(v, s)}" 902 by (simp add: return_def) 903 904(* FIXME: move *) 905lemma in_bind_split [monad_eq]: 906 "(rv \<in> fst ((f >>= g) s)) = 907 (\<exists>rv'. rv' \<in> fst (f s) \<and> rv \<in> fst (g (fst rv') (snd rv')))" 908 apply (cases rv) 909 apply (fastforce simp add: in_bind) 910 done 911 912lemma no_fail_mapM_wp: 913 assumes "\<And>x. x \<in> set xs \<Longrightarrow> no_fail (P x) (f x)" 914 assumes "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>P x\<rbrace> f y \<lbrace>\<lambda>_. P x\<rbrace>" 915 shows "no_fail (\<lambda>s. \<forall>x \<in> set xs. P x s) (mapM f xs)" 916 using assms 917proof (induct xs) 918 case Nil 919 thus ?case by (simp add: mapM_empty) 920next 921 case (Cons z zs) 922 show ?case 923 apply (clarsimp simp: mapM_Cons) 924 apply (wp Cons.prems Cons.hyps hoare_vcg_const_Ball_lift|simp)+ 925 done 926qed 927 928lemma zipWithM_Nil [simp]: 929 "zipWithM f xs [] = return []" 930 by (simp add: zipWithM_def zipWith_def sequence_def) 931 932lemma zipWithM_One: 933 "zipWithM f (x#xs) [a] = (do z \<leftarrow> f x a; return [z] od)" 934 by (simp add: zipWithM_def zipWith_def sequence_def) 935 936lemma zipWithM_x_Nil: 937 "zipWithM_x f xs [] = return ()" 938 by (simp add: zipWithM_x_def zipWith_def sequence_x_def) 939 940lemma zipWithM_x_One: 941 "zipWithM_x f (x#xs) [a] = f x a" 942 by (simp add: zipWithM_x_def zipWith_def sequence_x_def) 943 944lemma list_case_return: 945 "(case xs of [] \<Rightarrow> return v | y # ys \<Rightarrow> return (f y ys)) 946 = return (case xs of [] \<Rightarrow> v | y # ys \<Rightarrow> f y ys)" 947 by (simp split: list.split) 948 949lemma gets_exs_valid: 950 "\<lbrace>(=) s\<rbrace> gets f \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>" 951 apply (clarsimp simp: exs_valid_def split_def) 952 apply (rule bexI [where x = "(f s, s)"]) 953 apply simp 954 apply (simp add: in_monad) 955 done 956 957lemma empty_fail_get: 958 "empty_fail get" 959 by (simp add: empty_fail_def get_def) 960 961lemma alternative_liftE_returnOk: 962 "(liftE m \<sqinter> returnOk v) = liftE (m \<sqinter> return v)" 963 by (simp add: liftE_def alternative_def returnOk_def bind_def return_def) 964 965lemma bind_inv_inv_comm_weak: 966 "\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>_. (=) s\<rbrace>; 967 empty_fail f; empty_fail g \<rbrakk> \<Longrightarrow> 968 do x \<leftarrow> f; y \<leftarrow> g; n od = do y \<leftarrow> g; x \<leftarrow> f; n od" 969 apply (rule ext) 970 apply (fastforce simp: bind_def valid_def empty_fail_def split_def image_def) 971 done 972 973lemma mapM_last_Cons: 974 "\<lbrakk> xs = [] \<Longrightarrow> g v = y; 975 xs \<noteq> [] \<Longrightarrow> do x \<leftarrow> f (last xs); return (g x) od 976 = do x \<leftarrow> f (last xs); return y od \<rbrakk> \<Longrightarrow> 977 do ys \<leftarrow> mapM f xs; 978 return (g (last (v # ys))) od 979 = do mapM_x f xs; 980 return y od" 981 apply (cases "xs = []") 982 apply (simp add: mapM_x_Nil mapM_Nil) 983 apply (simp add: mapM_x_mapM) 984 apply (subst append_butlast_last_id[symmetric], assumption, 985 subst mapM_append)+ 986 apply (simp add: bind_assoc mapM_Cons mapM_Nil) 987 done 988 989lemma mapM_length_cong: 990 "\<lbrakk> length xs = length ys; \<And>x y. (x, y) \<in> set (zip xs ys) \<Longrightarrow> f x = g y \<rbrakk> 991 \<Longrightarrow> mapM f xs = mapM g ys" 992 by (simp add: mapM_def map_length_cong) 993 994(* FIXME: duplicate *) 995lemma zipWithM_mapM: 996 "zipWithM f xs ys = mapM (split f) (zip xs ys)" 997 by (simp add: zipWithM_def zipWith_def mapM_def) 998 999lemma zipWithM_If_cut: 1000 "zipWithM (\<lambda>a b. if a < n then f a b else g a b) [0 ..< m] xs 1001 = do ys \<leftarrow> zipWithM f [0 ..< min n m] xs; 1002 zs \<leftarrow> zipWithM g [n ..< m] (drop n xs); 1003 return (ys @ zs) od" 1004 apply (cases "n < m") 1005 apply (cut_tac i=0 and j=n and k="m - n" in upt_add_eq_append) 1006 apply simp 1007 apply (simp add: min.absorb1 zipWithM_mapM) 1008 apply (simp add: zip_append1 mapM_append zip_take_triv2 split_def) 1009 apply (intro bind_cong bind_apply_cong refl mapM_length_cong 1010 fun_cong[OF mapM_length_cong]) 1011 apply (clarsimp simp: set_zip) 1012 apply (clarsimp simp: set_zip) 1013 apply (simp add: min.absorb2 zipWithM_mapM mapM_Nil) 1014 apply (intro mapM_length_cong refl) 1015 apply (clarsimp simp: set_zip) 1016 done 1017 1018lemma mapM_liftM_const: 1019 "mapM (\<lambda>x. liftM (\<lambda>y. f x) (g x)) xs 1020 = liftM (\<lambda>ys. map f xs) (mapM g xs)" 1021 apply (induct xs) 1022 apply (simp add: mapM_Nil) 1023 apply (simp add: mapM_Cons) 1024 apply (simp add: liftM_def bind_assoc) 1025 done 1026 1027lemma empty_failD2: 1028 "\<lbrakk> empty_fail f; \<not> snd (f s) \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> fst (f s)" 1029 by (fastforce simp add: empty_fail_def) 1030 1031lemma empty_failD3: 1032 "\<lbrakk> empty_fail f; \<not> snd (f s) \<rbrakk> \<Longrightarrow> fst (f s) \<noteq> {}" 1033 by (drule(1) empty_failD2, clarsimp) 1034 1035lemma bind_inv_inv_comm: 1036 "\<lbrakk> \<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>; 1037 empty_fail f; empty_fail g \<rbrakk> \<Longrightarrow> 1038 do x \<leftarrow> f; y \<leftarrow> g; n x y od = do y \<leftarrow> g; x \<leftarrow> f; n x y od" 1039 apply (rule ext) 1040 apply (rename_tac s) 1041 apply (rule_tac s="(do (x, y) \<leftarrow> do x \<leftarrow> f; y \<leftarrow> (\<lambda>_. g s) ; (\<lambda>_. return (x, y) s) od; 1042 n x y od) s" in trans) 1043 apply (simp add: bind_assoc) 1044 apply (intro bind_apply_cong, simp_all)[1] 1045 apply (metis in_inv_by_hoareD) 1046 apply (simp add: return_def bind_def) 1047 apply (metis in_inv_by_hoareD) 1048 apply (rule_tac s="(do (x, y) \<leftarrow> do y \<leftarrow> g; x \<leftarrow> (\<lambda>_. f s) ; (\<lambda>_. return (x, y) s) od; 1049 n x y od) s" in trans[rotated]) 1050 apply (simp add: bind_assoc) 1051 apply (intro bind_apply_cong, simp_all)[1] 1052 apply (metis in_inv_by_hoareD) 1053 apply (simp add: return_def bind_def) 1054 apply (metis in_inv_by_hoareD) 1055 apply (rule bind_apply_cong, simp_all) 1056 apply (clarsimp simp: bind_def split_def return_def) 1057 apply (auto | drule(1) empty_failD3)+ 1058 done 1059 1060lemma throwErrorE_E [wp]: 1061 "\<lbrace>Q e\<rbrace> throwError e -, \<lbrace>Q\<rbrace>" 1062 by (simp add: validE_E_def) wp 1063 1064lemma no_fail_mapM: 1065 "\<forall>x. no_fail \<top> (f x) \<Longrightarrow> no_fail \<top> (mapM f xs)" 1066 apply (induct xs) 1067 apply (simp add: mapM_def sequence_def) 1068 apply (simp add: mapM_Cons) 1069 apply (wp|fastforce)+ 1070 done 1071 1072lemma gets_inv [simp]: 1073 "\<lbrace> P \<rbrace> gets f \<lbrace> \<lambda>r. P \<rbrace>" 1074 by (simp add: gets_def, wp) 1075 1076lemma select_inv: 1077 "\<lbrace> P \<rbrace> select S \<lbrace> \<lambda>r. P \<rbrace>" 1078 by (simp add: select_def valid_def) 1079 1080lemmas return_inv = hoare_return_drop_var 1081 1082lemma assert_inv: "\<lbrace>P\<rbrace> assert Q \<lbrace>\<lambda>r. P\<rbrace>" 1083 unfolding assert_def 1084 by (cases Q) simp+ 1085 1086lemma assert_opt_inv: "\<lbrace>P\<rbrace> assert_opt Q \<lbrace>\<lambda>r. P\<rbrace>" 1087 unfolding assert_opt_def 1088 by (cases Q) simp+ 1089 1090lemma let_into_return: 1091 "(let f = x in m f) = (do f \<leftarrow> return x; m f od)" 1092 by simp 1093 1094definition 1095 injection_handler :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s, 'a + 'c) nondet_monad 1096 \<Rightarrow> ('s, 'b + 'c) nondet_monad" 1097where 1098 "injection_handler f m \<equiv> m <handle2> (\<lambda>ft. throwError (f ft))" 1099 1100lemma injection_wp: 1101 "\<lbrakk> t = injection_handler f; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>ft. E (f ft)\<rbrace> \<rbrakk> 1102 \<Longrightarrow> \<lbrace>P\<rbrace> t m \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1103 apply (simp add: injection_handler_def) 1104 apply (wp|simp)+ 1105 done 1106 1107lemma injection_wp_E: 1108 "\<lbrakk> t = injection_handler f; \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>,- \<rbrakk> 1109 \<Longrightarrow> \<lbrace>P\<rbrace> t m \<lbrace>Q\<rbrace>,-" 1110 by (simp add: validE_R_def injection_wp) 1111 1112lemma injection_bindE: 1113 "\<lbrakk> t = injection_handler f; t2 = injection_handler f \<rbrakk> 1114 \<Longrightarrow> t (x >>=E y) = (t2 x) >>=E (\<lambda>rv. t (y rv))" 1115 apply (simp add: injection_handler_def) 1116 apply (simp add: bindE_def handleE'_def bind_assoc) 1117 apply (rule arg_cong [where f="\<lambda>y. x >>= y"]) 1118 apply (rule ext) 1119 apply (case_tac x, simp_all add: lift_def throwError_def) 1120 done 1121 1122lemma injection_liftE: 1123 "t = injection_handler f \<Longrightarrow> t (liftE x) = liftE x" 1124 apply (simp add: injection_handler_def handleE'_def liftE_def) 1125 done 1126 1127lemma id_injection: 1128 "id = injection_handler id" 1129proof - 1130 have P: "case_sum throwError (\<lambda>v. return (Inr v)) = return" 1131 by (auto simp: throwError_def split: sum.splits) 1132 show ?thesis 1133 by (auto simp: injection_handler_def handleE'_def P) 1134qed 1135 1136lemma injection_handler_assertE: 1137 "injection_handler inject (assertE f) = assertE f" 1138 by (simp add: assertE_liftE injection_liftE) 1139 1140lemma case_options_weak_wp: 1141 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P'\<rbrace> g x \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> case opt of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>Q\<rbrace>" 1142 apply (cases opt) 1143 apply (clarsimp elim!: hoare_weaken_pre) 1144 apply (rule hoare_weaken_pre [where Q=P']) 1145 apply simp+ 1146 done 1147 1148lemma case_option_wp_None_return: 1149 assumes [wp]: "\<And>x. \<lbrace>P' x\<rbrace> f x \<lbrace>\<lambda>_. Q\<rbrace>" 1150 shows "\<lbrakk>\<And>x s. (Q and P x) s \<Longrightarrow> P' x s \<rbrakk> 1151 \<Longrightarrow> \<lbrace>Q and (\<lambda>s. opt \<noteq> None \<longrightarrow> P (the opt) s)\<rbrace> 1152 (case opt of None \<Rightarrow> return () | Some x \<Rightarrow> f x) 1153 \<lbrace>\<lambda>_. Q\<rbrace>" 1154 by (cases opt; wpsimp) 1155 1156lemma case_option_wp_None_returnOk: 1157 assumes [wp]: "\<And>x. \<lbrace>P' x\<rbrace> f x \<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>E\<rbrace>" 1158 shows "\<lbrakk>\<And>x s. (Q and P x) s \<Longrightarrow> P' x s \<rbrakk> 1159 \<Longrightarrow> \<lbrace>Q and (\<lambda>s. opt \<noteq> None \<longrightarrow> P (the opt) s)\<rbrace> 1160 (case opt of None \<Rightarrow> returnOk () | Some x \<Rightarrow> f x) 1161 \<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>E\<rbrace>" 1162 by (cases opt; wpsimp) 1163 1164lemma list_cases_weak_wp: 1165 assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>" 1166 assumes "\<And>x xs. \<lbrace>P_B\<rbrace> b x xs \<lbrace>Q\<rbrace>" 1167 shows 1168 "\<lbrace>P_A and P_B\<rbrace> 1169 case ts of 1170 [] \<Rightarrow> a 1171 | x#xs \<Rightarrow> b x xs \<lbrace>Q\<rbrace>" 1172 apply (cases ts) 1173 apply (simp, rule hoare_weaken_pre, rule assms, simp)+ 1174 done 1175 1176 1177lemmas hoare_FalseE_R = hoare_FalseE[where E="\<top>\<top>", folded validE_R_def] 1178 1179lemma hoare_vcg_if_lift2: 1180 "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P rv s \<longrightarrow> X rv s) \<and> (\<not> P rv s \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow> 1181 \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>" 1182 1183 "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P' rv \<longrightarrow> X rv s) \<and> (\<not> P' rv \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow> 1184 \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>" 1185 by (auto simp: valid_def split_def) 1186 1187lemma hoare_vcg_if_lift_ER: (* Required because of lack of rv in lifting rules *) 1188 "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P rv s \<longrightarrow> X rv s) \<and> (\<not> P rv s \<longrightarrow> Y rv s)\<rbrace>, - \<Longrightarrow> 1189 \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>, -" 1190 1191 "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P' rv \<longrightarrow> X rv s) \<and> (\<not> P' rv \<longrightarrow> Y rv s)\<rbrace>, - \<Longrightarrow> 1192 \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>, -" 1193 by (auto simp: valid_def validE_R_def validE_def split_def) 1194 1195lemma liftME_return: 1196 "liftME f (returnOk v) = returnOk (f v)" 1197 by (simp add: liftME_def) 1198 1199lemma lifted_if_collapse: 1200 "(if P then \<top> else f) = (\<lambda>s. \<not>P \<longrightarrow> f s)" 1201 by auto 1202 1203lemma undefined_valid: "\<lbrace>\<bottom>\<rbrace> undefined \<lbrace>Q\<rbrace>" 1204 by (rule hoare_pre_cont) 1205 1206lemma Inr_in_liftE_simp [monad_eq]: 1207 "((Inr rv, x) \<in> fst (liftE fn s)) = ((rv, x) \<in> fst (fn s))" 1208 by (simp add: in_monad) 1209 1210lemma assertE_wp: 1211 "\<lbrace>\<lambda>s. F \<longrightarrow> Q () s\<rbrace> assertE F \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1212 apply (rule hoare_pre) 1213 apply (unfold assertE_def) 1214 apply wp 1215 apply simp 1216 done 1217 1218lemma doesn't_grow_proof: 1219 assumes y: "\<And>s. finite (S s)" 1220 assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>" 1221 shows "\<lbrace>\<lambda>s. card (S s) < n \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. card (S s) < n\<rbrace>" 1222 apply (clarsimp simp: valid_def) 1223 apply (subgoal_tac "S b \<subseteq> S s") 1224 apply (drule card_mono [OF y], simp) 1225 apply clarsimp 1226 apply (rule ccontr) 1227 apply (subgoal_tac "x \<notin> S b", simp) 1228 apply (erule use_valid [OF _ x]) 1229 apply simp 1230 done 1231 1232lemma fold_bindE_into_list_case: 1233 "(doE v \<leftarrow> f; case_list (g v) (h v) x odE) 1234 = (case_list (doE v \<leftarrow> f; g v odE) (\<lambda>x xs. doE v \<leftarrow> f; h v x xs odE) x)" 1235 by (simp split: list.split) 1236 1237lemma hoare_vcg_propE_R: 1238 "\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>, -" 1239 by (simp add: validE_R_def validE_def valid_def split_def split: sum.split) 1240 1241lemma set_preserved_proof: 1242 assumes y: "\<And>x. \<lbrace>\<lambda>s. Q s \<and> x \<in> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<in> S s\<rbrace>" 1243 assumes x: "\<And>x. \<lbrace>\<lambda>s. Q s \<and> x \<notin> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>" 1244 shows "\<lbrace>\<lambda>s. Q s \<and> P (S s)\<rbrace> f \<lbrace>\<lambda>rv s. P (S s)\<rbrace>" 1245 apply (clarsimp simp: valid_def) 1246 by (metis (mono_tags, lifting) equalityI post_by_hoare subsetI x y) 1247 1248lemma set_shrink_proof: 1249 assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>" 1250 shows 1251 "\<lbrace>\<lambda>s. \<forall>S'. S' \<subseteq> S s \<longrightarrow> P S'\<rbrace> 1252 f 1253 \<lbrace>\<lambda>rv s. P (S s)\<rbrace>" 1254 apply (clarsimp simp: valid_def) 1255 apply (drule spec, erule mp) 1256 apply (clarsimp simp: subset_iff) 1257 apply (rule ccontr) 1258 apply (drule(1) use_valid [OF _ x]) 1259 apply simp 1260 done 1261 1262lemma shrinks_proof: 1263 assumes y: "\<And>s. finite (S s)" 1264 assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>" 1265 assumes z: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>" 1266 assumes w: "\<And>s. P s \<Longrightarrow> x \<in> S s" 1267 shows "\<lbrace>\<lambda>s. card (S s) \<le> n \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. card (S s) < n\<rbrace>" 1268 apply (clarsimp simp: valid_def) 1269 apply (subgoal_tac "S b \<subset> S s") 1270 apply (drule psubset_card_mono [OF y], simp) 1271 apply (rule psubsetI) 1272 apply clarsimp 1273 apply (rule ccontr) 1274 apply (subgoal_tac "x \<notin> S b", simp) 1275 apply (erule use_valid [OF _ x]) 1276 apply simp 1277 apply (rule not_sym) 1278 apply (rule set_neqI[where x=x]) 1279 apply (erule w) 1280 apply (erule(1) use_valid [OF _ z]) 1281 done 1282 1283lemma unlessE_wp : 1284 "(\<not>P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then R () else Q\<rbrace> unlessE P f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>" 1285 apply (clarsimp simp: unlessE_whenE whenE_def) 1286 apply wp 1287 done 1288 1289lemma use_validE_R: 1290 "\<lbrakk> (Inr r, s') \<in> fst (f s); \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; P s \<rbrakk> \<Longrightarrow> Q r s'" 1291 unfolding validE_R_def validE_def 1292 by (frule(2) use_valid, simp) 1293 1294lemma valid_preservation_ex: 1295 assumes x: "\<And>x P. \<lbrace>\<lambda>s. P (f s x :: 'b)\<rbrace> m \<lbrace>\<lambda>rv s. P (f s x)\<rbrace>" 1296 shows "\<lbrace>\<lambda>s. P (f s :: 'a \<Rightarrow> 'b)\<rbrace> m \<lbrace>\<lambda>rv s. P (f s)\<rbrace>" 1297 apply (clarsimp simp: valid_def) 1298 apply (erule rsubst[where P=P]) 1299 apply (rule ext) 1300 apply (erule use_valid [OF _ x]) 1301 apply simp 1302 done 1303 1304lemmas valid_prove_more' = valid_prove_more[where Q="\<lambda>rv. Q" for Q] 1305 1306lemma whenE_inv: 1307 assumes a: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>" 1308 shows "\<lbrace>P\<rbrace> whenE Q f \<lbrace>\<lambda>_. P\<rbrace>" 1309 unfolding whenE_def 1310 apply (cases Q) 1311 apply simp 1312 apply (wp a) 1313 apply simp 1314 apply wp 1315 done 1316 1317lemma whenE_liftE: 1318 "whenE P (liftE f) = liftE (when P f)" 1319 by (simp add: whenE_def when_def returnOk_liftE) 1320 1321lemma whenE_throwError_wp: 1322 "\<lbrace>\<lambda>s. \<not> P \<longrightarrow> Q s\<rbrace> whenE P (throwError e) \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<top>\<top>\<rbrace>" 1323 unfolding whenE_def 1324 apply (cases P) 1325 apply simp 1326 apply wp 1327 apply simp 1328 apply wp 1329 done 1330 1331lemma whenE_whenE_body: 1332 "whenE P (throwError f) >>=E (\<lambda>_. whenE Q (throwError f) >>=E r) = whenE (P \<or> Q) (throwError f) >>=E r" 1333 apply (cases P) 1334 apply (simp add: whenE_def) 1335 apply simp 1336 done 1337 1338lemma whenE_whenE_same: 1339 "whenE P (throwError f) >>=E (\<lambda>_. whenE P (throwError g) >>=E r) = whenE P (throwError f) >>=E r" 1340 apply (cases P) 1341 apply (simp add: whenE_def) 1342 apply simp 1343 done 1344 1345lemma gets_the_inv: "\<lbrace>P\<rbrace> gets_the V \<lbrace>\<lambda>rv. P\<rbrace>" by wpsimp 1346 1347lemma select_f_inv: 1348 "\<lbrace>P\<rbrace> select_f S \<lbrace>\<lambda>_. P\<rbrace>" 1349 by (simp add: select_f_def valid_def) 1350 1351lemmas state_unchanged = in_inv_by_hoareD [THEN sym] 1352 1353lemma validI: 1354 assumes rl: "\<And>s r s'. \<lbrakk> P s; (r, s') \<in> fst (S s) \<rbrakk> \<Longrightarrow> Q r s'" 1355 shows "\<lbrace>P\<rbrace> S \<lbrace>Q\<rbrace>" 1356 unfolding valid_def using rl by safe 1357 1358lemma opt_return_pres_lift: 1359 assumes x: "\<And>v. \<lbrace>P\<rbrace> f v \<lbrace>\<lambda>rv. P\<rbrace>" 1360 shows "\<lbrace>P\<rbrace> case x of None \<Rightarrow> return () | Some v \<Rightarrow> f v \<lbrace>\<lambda>rv. P\<rbrace>" 1361 by (rule hoare_pre, (wpcw; wp x), simp) 1362 1363lemma exec_select_f_singleton: 1364 "(select_f ({v},False) >>= f) = f v" 1365 by (simp add: select_f_def bind_def) 1366 1367lemma mapM_discarded: 1368 "mapM f xs >>= (\<lambda>ys. g) = mapM_x f xs >>= (\<lambda>_. g)" 1369 by (simp add: mapM_x_mapM) 1370 1371lemma valid_return_unit: 1372 "\<lbrace>P\<rbrace> f >>= (\<lambda>_. return ()) \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>" 1373 apply (rule validI) 1374 apply (fastforce simp: valid_def return_def bind_def split_def) 1375 done 1376 1377lemma mapM_x_map: 1378 "mapM_x f (map g xs) = mapM_x (\<lambda>x. f (g x)) xs" 1379 by (simp add: mapM_x_def o_def) 1380 1381lemma maybe_fail_bind_fail: 1382 "unless P fail >>= (\<lambda>_. fail) = fail" 1383 "when P fail >>= (\<lambda>_. fail) = fail" 1384 by (clarsimp simp: bind_def fail_def return_def 1385 unless_def when_def)+ 1386 1387lemma unless_False: 1388 "unless False f = f" 1389 by (simp add: unless_def when_def) 1390 1391lemma unless_True: 1392 "unless True f = return ()" 1393 by (simp add: unless_def when_def) 1394 1395lemma filterM_preserved: 1396 "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> m x \<lbrace>\<lambda>rv. P\<rbrace> \<rbrakk> 1397 \<Longrightarrow> \<lbrace>P\<rbrace> filterM m xs \<lbrace>\<lambda>rv. P\<rbrace>" 1398 apply (induct xs) 1399 apply (wp | simp | erule meta_mp | drule meta_spec)+ 1400 done 1401 1402lemma filterM_append: 1403 "filterM f (xs @ ys) = (do 1404 xs' \<leftarrow> filterM f xs; 1405 ys' \<leftarrow> filterM f ys; 1406 return (xs' @ ys') 1407 od)" 1408 apply (induct xs) 1409 apply simp 1410 apply (simp add: bind_assoc) 1411 apply (rule ext bind_apply_cong [OF refl])+ 1412 apply simp 1413 done 1414 1415lemma filterM_distinct1: 1416 "\<lbrace>\<top> and K (P \<longrightarrow> distinct xs)\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. (P \<longrightarrow> distinct rv) \<and> set rv \<subseteq> set xs\<rbrace>" 1417 apply (rule hoare_gen_asm, erule rev_mp) 1418 apply (rule rev_induct [where xs=xs]) 1419 apply (clarsimp | wp)+ 1420 apply (simp add: filterM_append) 1421 apply (erule hoare_seq_ext[rotated]) 1422 apply (rule hoare_seq_ext[rotated], rule hoare_vcg_prop) 1423 apply (wp, clarsimp) 1424 apply blast 1425 done 1426 1427lemma filterM_subset: 1428 "\<lbrace>\<top>\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. set rv \<subseteq> set xs\<rbrace>" 1429 by (rule hoare_chain, rule filterM_distinct1[where P=False], simp_all) 1430 1431lemma filterM_all: 1432 "\<lbrakk> \<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>P y\<rbrace> m x \<lbrace>\<lambda>rv. P y\<rbrace> \<rbrakk> \<Longrightarrow> 1433 \<lbrace>\<lambda>s. \<forall>x \<in> set xs. P x s\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. P x s\<rbrace>" 1434 apply (rule_tac Q="\<lambda>rv s. set rv \<subseteq> set xs \<and> (\<forall>x \<in> set xs. P x s)" 1435 in hoare_strengthen_post) 1436 apply (wp filterM_subset hoare_vcg_const_Ball_lift filterM_preserved) 1437 apply simp+ 1438 apply blast 1439 done 1440 1441 1442lemma filterM_distinct: 1443 "\<lbrace>K (distinct xs)\<rbrace> filterM m xs \<lbrace>\<lambda>rv s. distinct rv\<rbrace>" 1444 by (rule hoare_chain, rule filterM_distinct1[where P=True], simp_all) 1445 1446lemma filterM_mapM: 1447 "filterM f xs = (do 1448 ys \<leftarrow> mapM (\<lambda>x. do v \<leftarrow> f x; return (x, v) od) xs; 1449 return (map fst (filter snd ys)) 1450 od)" 1451 apply (induct xs) 1452 apply (simp add: mapM_def sequence_def) 1453 apply (simp add: mapM_Cons bind_assoc) 1454 apply (rule bind_cong [OF refl] bind_apply_cong[OF refl])+ 1455 apply simp 1456 done 1457 1458lemma if_return_closure: 1459 "(if P then return x else return y) 1460 = (return (if P then x else y))" 1461 by simp 1462 1463lemma select_singleton: 1464 "select {x} = return x" 1465 by (fastforce simp add: fun_eq_iff select_def return_def) 1466 1467lemma static_imp_wp: 1468 "\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>" 1469 by (cases P, simp_all add: valid_def) 1470 1471lemma static_imp_wpE : 1472 "\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-" 1473 by (cases P, simp_all) 1474 1475lemma static_imp_conj_wp: 1476 "\<lbrakk> \<lbrace>Q\<rbrace> m \<lbrace>Q'\<rbrace>; \<lbrace>R\<rbrace> m \<lbrace>R'\<rbrace> \<rbrakk> 1477 \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. (P \<longrightarrow> Q' rv s) \<and> R' rv s\<rbrace>" 1478 apply (rule hoare_vcg_conj_lift) 1479 apply (rule static_imp_wp) 1480 apply assumption+ 1481 done 1482 1483lemma hoare_eq_P: 1484 assumes "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>" 1485 shows "\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>" 1486 by (rule assms) 1487 1488lemma hoare_validE_R_conj: 1489 "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q And R\<rbrace>, -" 1490 by (simp add: valid_def validE_def validE_R_def Let_def split_def split: sum.splits) 1491 1492lemma hoare_vcg_const_imp_lift_R: 1493 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. F \<longrightarrow> P s\<rbrace> f \<lbrace>\<lambda>rv s. F \<longrightarrow> Q rv s\<rbrace>,-" 1494 by (cases F, simp_all) 1495 1496lemma hoare_vcg_disj_lift_R: 1497 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" 1498 assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-" 1499 shows "\<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>,-" 1500 using assms 1501 by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits) 1502 1503lemmas throwError_validE_R = throwError_wp [where E="\<top>\<top>", folded validE_R_def] 1504 1505lemma valid_case_option_post_wp: 1506 "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>\<lambda>rv. Q x\<rbrace>) \<Longrightarrow> 1507 \<lbrace>\<lambda>s. case ep of Some x \<Rightarrow> P x s | _ \<Rightarrow> True\<rbrace> 1508 f \<lbrace>\<lambda>rv s. case ep of Some x \<Rightarrow> Q x s | _ \<Rightarrow> True\<rbrace>" 1509 by (cases ep, simp_all add: hoare_vcg_prop) 1510 1511lemma P_bool_lift: 1512 assumes t: "\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>" 1513 assumes f: "\<lbrace>\<lambda>s. \<not>Q s\<rbrace> f \<lbrace>\<lambda>r s. \<not>Q s\<rbrace>" 1514 shows "\<lbrace>\<lambda>s. P (Q s)\<rbrace> f \<lbrace>\<lambda>r s. P (Q s)\<rbrace>" 1515 apply (clarsimp simp: valid_def) 1516 apply (subgoal_tac "Q b = Q s") 1517 apply simp 1518 apply (rule iffI) 1519 apply (rule classical) 1520 apply (drule (1) use_valid [OF _ f]) 1521 apply simp 1522 apply (erule (1) use_valid [OF _ t]) 1523 done 1524 1525lemma fail_inv : 1526 "\<lbrace> P \<rbrace> fail \<lbrace> \<lambda>r. P \<rbrace>" 1527 by wp 1528 1529lemma gets_sp: "\<lbrace>P\<rbrace> gets f \<lbrace>\<lambda>rv. P and (\<lambda>s. f s = rv)\<rbrace>" 1530 by (wp, simp) 1531 1532lemma post_by_hoare2: 1533 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; (r, s') \<in> fst (f s); P s \<rbrakk> \<Longrightarrow> Q r s'" 1534 by (rule post_by_hoare, assumption+) 1535 1536lemma hoare_Ball_helper: 1537 assumes x: "\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>" 1538 assumes y: "\<And>P. \<lbrace>\<lambda>s. P (S s)\<rbrace> f \<lbrace>\<lambda>rv s. P (S s)\<rbrace>" 1539 shows "\<lbrace>\<lambda>s. \<forall>x \<in> S s. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> S s. Q x rv s\<rbrace>" 1540 apply (clarsimp simp: valid_def) 1541 apply (subgoal_tac "S b = S s") 1542 apply (erule post_by_hoare2 [OF x]) 1543 apply (clarsimp simp: Ball_def) 1544 apply (erule_tac P1="\<lambda>x. x = S s" in post_by_hoare2 [OF y]) 1545 apply (rule refl) 1546 done 1547 1548lemma hoare_gets_post: 1549 "\<lbrace> P \<rbrace> gets f \<lbrace> \<lambda>r s. r = f s \<and> P s \<rbrace>" 1550 by (simp add: valid_def get_def gets_def bind_def return_def) 1551 1552lemma hoare_return_post: 1553 "\<lbrace> P \<rbrace> return x \<lbrace> \<lambda>r s. r = x \<and> P s \<rbrace>" 1554 by (simp add: valid_def return_def) 1555 1556lemma mapM_wp': 1557 assumes x: "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>" 1558 shows "\<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>" 1559 apply (rule mapM_wp) 1560 apply (erule x) 1561 apply simp 1562 done 1563 1564lemma mapM_set: 1565 assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>" 1566 assumes "\<And>x y. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>" 1567 assumes "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>" 1568 shows "\<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. \<forall>x \<in> set xs. Q x s\<rbrace>" 1569using assms 1570proof (induct xs) 1571 case Nil show ?case 1572 by (simp add: mapM_def sequence_def) wp 1573next 1574 case (Cons y ys) 1575 have PQ_inv: "\<And>x. x \<in> set ys \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. P and Q y\<rbrace>" 1576 apply (simp add: pred_conj_def) 1577 apply (rule hoare_pre) 1578 apply (wp Cons|simp)+ 1579 done 1580 show ?case 1581 apply (simp add: mapM_Cons) 1582 apply wp 1583 apply (rule hoare_vcg_conj_lift) 1584 apply (rule hoare_strengthen_post) 1585 apply (rule mapM_wp') 1586 apply (erule PQ_inv) 1587 apply simp 1588 apply (wp Cons|simp)+ 1589 done 1590qed 1591 1592lemma case_option_fail_return_val: 1593 "(fst (case_option fail return v s) = {(rv, s')}) = (v = Some rv \<and> s = s')" 1594 by (cases v, simp_all add: fail_def return_def) 1595 1596lemma return_expanded_inv: 1597 "\<lbrace>P\<rbrace> \<lambda>s. ({(x, s)}, False) \<lbrace>\<lambda>rv. P\<rbrace>" 1598 by (simp add: valid_def) 1599 1600lemma empty_fail_assert : "empty_fail (assert P)" 1601 unfolding assert_def by simp 1602 1603lemma no_fail_mapM': 1604 assumes rl: "\<And>x. no_fail (\<lambda>_. P x) (f x)" 1605 shows "no_fail (\<lambda>_. \<forall>x \<in> set xs. P x) (mapM f xs)" 1606proof (induct xs) 1607 case Nil thus ?case by (simp add: mapM_def sequence_def) 1608next 1609 case (Cons x xs) 1610 1611 have nf: "no_fail (\<lambda>_. P x) (f x)" by (rule rl) 1612 have ih: "no_fail (\<lambda>_. \<forall>x \<in> set xs. P x) (mapM f xs)" by (rule Cons) 1613 1614 show ?case 1615 apply (simp add: mapM_Cons) 1616 apply (rule no_fail_pre) 1617 apply (wp nf ih) 1618 apply simp 1619 done 1620qed 1621 1622lemma handy_prop_divs: 1623 assumes x: "\<And>P. \<lbrace>\<lambda>s. P (Q s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s)\<rbrace>" 1624 "\<And>P. \<lbrace>\<lambda>s. P (R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (R' rv s)\<rbrace>" 1625 shows "\<lbrace>\<lambda>s. P (Q s \<and> R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s \<and> R' rv s)\<rbrace>" 1626 "\<lbrace>\<lambda>s. P (Q s \<or> R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s \<or> R' rv s)\<rbrace>" 1627 apply (clarsimp simp: valid_def 1628 elim!: rsubst[where P=P]) 1629 apply (rule use_valid [OF _ x(1)], assumption) 1630 apply (rule use_valid [OF _ x(2)], assumption) 1631 apply simp 1632 apply (clarsimp simp: valid_def 1633 elim!: rsubst[where P=P]) 1634 apply (rule use_valid [OF _ x(1)], assumption) 1635 apply (rule use_valid [OF _ x(2)], assumption) 1636 apply simp 1637 done 1638 1639lemma hoare_as_subst: 1640 "\<lbrakk> \<And>P. \<lbrace>\<lambda>s. P (fn s)\<rbrace> f \<lbrace>\<lambda>rv s. P (fn s)\<rbrace>; 1641 \<And>v :: 'a. \<lbrace>P v\<rbrace> f \<lbrace>Q v\<rbrace> \<rbrakk> \<Longrightarrow> 1642 \<lbrace>\<lambda>s. P (fn s) s\<rbrace> f \<lbrace>\<lambda>rv s. Q (fn s) rv s\<rbrace>" 1643 apply (rule_tac Q="\<lambda>rv s. \<exists>v. v = fn s \<and> Q v rv s" in hoare_chain) 1644 apply (rule hoare_vcg_ex_lift) 1645 apply (rule hoare_vcg_conj_lift) 1646 apply assumption+ 1647 apply simp 1648 apply simp 1649 done 1650 1651lemmas hoare_vcg_ball_lift = hoare_vcg_const_Ball_lift 1652 1653lemma select_singleton_is_return : "select {A} = return A" 1654 unfolding select_def return_def by (simp add: Sigma_def) 1655 1656lemma assert_opt_eq_singleton: 1657 "(assert_opt f s = ({(v, s')},False)) = (s = s' \<and> f = Some v)" 1658 by (case_tac f, simp_all add: assert_opt_def 1659 fail_def return_def conj_comms) 1660 1661lemma hoare_set_preserved: 1662 assumes x: "\<And>x. \<lbrace>fn' x\<rbrace> m \<lbrace>\<lambda>rv. fn x\<rbrace>" 1663 shows "\<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace>" 1664 apply (induct xs) 1665 apply simp 1666 apply wp 1667 apply simp 1668 apply (rule hoare_vcg_conj_lift) 1669 apply (rule x) 1670 apply assumption 1671 done 1672 1673lemma return_modify: 1674 "return () = modify id" 1675 by (simp add: return_def simpler_modify_def) 1676 1677lemma liftE_liftM_liftME: 1678 "liftE (liftM f m) = liftME f (liftE m)" 1679 by (simp add: liftE_liftM liftME_liftM liftM_def) 1680 1681 1682lemma assert_opt_member: 1683 "(x, s') \<in> fst (assert_opt y s) = (y = Some x \<and> s' = s)" 1684 apply (case_tac y, simp_all add: assert_opt_def fail_def return_def) 1685 apply safe 1686 done 1687 1688lemma bind_return_unit: 1689 "f = (f >>= (\<lambda>x. return ()))" 1690 by simp 1691 1692lemma det_mapM: 1693 assumes x: "\<And>x. x \<in> S \<Longrightarrow> det (f x)" 1694 shows "set xs \<subseteq> S \<Longrightarrow> det (mapM f xs)" 1695 apply (induct xs) 1696 apply (simp add: mapM_def sequence_def) 1697 apply (simp add: mapM_Cons x) 1698 done 1699 1700lemma det_zipWithM_x: 1701 assumes x: "\<And>x y. (x, y) \<in> set (zip xs ys) \<Longrightarrow> det (f x y)" 1702 shows "det (zipWithM_x f xs ys)" 1703 apply (simp add: zipWithM_x_mapM) 1704 apply (rule bind_detI) 1705 apply (rule det_mapM [where S="set (zip xs ys)"]) 1706 apply (clarsimp simp add: x) 1707 apply simp 1708 apply simp 1709 done 1710 1711lemma empty_fail_sequence_x : 1712 assumes "\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m" 1713 shows "empty_fail (sequence_x ms)" using assms 1714 by (induct ms) (auto simp: sequence_x_def) 1715 1716lemma gets_the_member: 1717 "(x, s') \<in> fst (gets_the f s) = (f s = Some x \<and> s' = s)" 1718 by (case_tac "f s", simp_all add: gets_the_def 1719 simpler_gets_def bind_def assert_opt_member) 1720 1721lemma hoare_ex_wp: 1722 assumes x: "\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>" 1723 shows "\<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>" 1724 apply (clarsimp simp: valid_def) 1725 apply (rule exI) 1726 apply (rule post_by_hoare [OF x]) 1727 apply assumption+ 1728 done 1729 1730lemma hoare_ex_pre: (* safe, unlike hoare_ex_wp *) 1731 "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>" 1732 by (fastforce simp: valid_def) 1733 1734lemma hoare_ex_pre_conj: 1735 "(\<And>x. \<lbrace>\<lambda>s. P x s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>) 1736 \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>x. P x s) \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>" 1737 by (fastforce simp: valid_def) 1738 1739lemma hoare_conj_lift_inv: 1740 "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s. P' s \<and> I s\<rbrace> f \<lbrace>\<lambda>rv. I\<rbrace>; 1741 \<And>s. P s \<Longrightarrow> P' s\<rbrakk> 1742 \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> I s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> I s\<rbrace>" 1743 by (fastforce simp: valid_def) 1744 1745lemma hoare_in_monad_post : 1746 assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x. P\<rbrace>" 1747 shows "\<lbrace>\<top>\<rbrace> f \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (f s)\<rbrace>" 1748 apply (clarsimp simp: valid_def) 1749 apply (subgoal_tac "s = b", simp) 1750 apply (simp add: state_unchanged [OF x]) 1751 done 1752 1753lemma mapM_gets: 1754 assumes P: "\<And>x. m x = gets (f x)" 1755 shows "mapM m xs = gets (\<lambda>s. map (\<lambda>x. f x s) xs)" 1756proof (induct xs) 1757 case Nil show ?case 1758 by (simp add: mapM_def sequence_def gets_def get_def bind_def) 1759next 1760 case (Cons y ys) thus ?case 1761 by (simp add: mapM_Cons P simpler_gets_def return_def bind_def) 1762qed 1763 1764lemma mapM_map_simp: 1765 "mapM m (map f xs) = mapM (m \<circ> f) xs" 1766 apply (induct xs) 1767 apply (simp add: mapM_def sequence_def) 1768 apply (simp add: mapM_Cons) 1769 done 1770 1771lemma modify_id_return: 1772 "modify id = return ()" 1773 by (simp add: simpler_modify_def return_def) 1774 1775definition 1776 oblivious :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) nondet_monad \<Rightarrow> bool" where 1777 "oblivious f m \<equiv> \<forall>s. (\<forall>(rv, s') \<in> fst (m s). (rv, f s') \<in> fst (m (f s))) 1778 \<and> (\<forall>(rv, s') \<in> fst (m (f s)). \<exists>s''. (rv, s'') \<in> fst (m s) \<and> s' = f s'') 1779 \<and> snd (m (f s)) = snd (m s)" 1780 1781lemma oblivious_return [simp]: 1782 "oblivious f (return x)" 1783 by (simp add: oblivious_def return_def) 1784 1785lemma oblivious_fail [simp]: 1786 "oblivious f fail" 1787 by (simp add: oblivious_def fail_def) 1788 1789lemma oblivious_assert [simp]: 1790 "oblivious f (assert x)" 1791 by (simp add: assert_def) 1792 1793lemma oblivious_assert_opt [simp]: 1794 "oblivious f (assert_opt fn)" 1795 by (simp add: assert_opt_def split: option.splits) 1796 1797lemma oblivious_bind: 1798 "\<lbrakk> oblivious f m; \<And>rv. oblivious f (m' rv) \<rbrakk> 1799 \<Longrightarrow> oblivious f (m >>= m')" 1800 apply atomize 1801 apply (simp add: oblivious_def) 1802 apply (erule allEI) 1803 apply (intro conjI) 1804 apply (drule conjunct1) 1805 apply (clarsimp simp: in_monad) 1806 apply fastforce 1807 apply (drule conjunct2, drule conjunct1) 1808 apply (clarsimp simp: in_monad) 1809 apply fastforce 1810 apply (clarsimp simp: bind_def disj_commute) 1811 apply (rule disj_cong [OF refl]) 1812 apply (rule iffI) 1813 apply (clarsimp simp: split_def) 1814 apply fastforce 1815 apply clarsimp 1816 apply (drule(1) bspec) 1817 apply (clarsimp simp: split_def) 1818 apply (erule (1) my_BallE) 1819 apply (rule bexI [rotated], assumption) 1820 apply clarsimp 1821 done 1822 1823lemma oblivious_gets [simp]: 1824 "oblivious f (gets f') = (\<forall>s. f' (f s) = f' s)" 1825 by (fastforce simp add: oblivious_def simpler_gets_def) 1826 1827lemma oblivious_liftM: 1828 "oblivious f m \<Longrightarrow> oblivious f (liftM g m)" 1829 by (simp add: liftM_def oblivious_bind) 1830 1831lemma oblivious_modify [simp]: 1832 "oblivious f (modify f') = (\<forall>s. f' (f s) = f (f' s))" 1833 apply (simp add: oblivious_def simpler_modify_def) 1834 apply (rule ball_cong[where A=UNIV, OF refl, simplified]) 1835 apply fastforce 1836 done 1837 1838lemma oblivious_modify_swap: 1839 "\<lbrakk> oblivious f m \<rbrakk> \<Longrightarrow> 1840 (modify f >>= (\<lambda>rv. m)) 1841 = (m >>= (\<lambda>rv. modify f))" 1842 apply (clarsimp simp: bind_def simpler_modify_def) 1843 apply (rule ext)+ 1844 apply (case_tac "m (f s)", clarsimp) 1845 apply (simp add: oblivious_def) 1846 apply (drule_tac x=s in spec) 1847 apply (rule conjI) 1848 apply (rule set_eqI) 1849 apply (rule iffI) 1850 apply (drule conjunct2, drule conjunct1) 1851 apply (drule_tac x=x in bspec, simp) 1852 apply clarsimp 1853 apply (rule_tac x="((), s'')" in bexI) 1854 apply simp 1855 apply simp 1856 apply (drule conjunct1) 1857 apply fastforce 1858 apply (drule conjunct2)+ 1859 apply fastforce 1860 done 1861 1862lemma univ_wp: 1863 "\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> fst (f s). Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>" 1864 by (simp add: valid_def) 1865 1866lemma univ_get_wp: 1867 assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>" 1868 shows "\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> fst (f s). s = s' \<longrightarrow> Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>" 1869 apply (rule hoare_pre_imp [OF _ univ_wp]) 1870 apply clarsimp 1871 apply (erule my_BallE, assumption, simp) 1872 apply (subgoal_tac "s = b", simp) 1873 apply (simp add: state_unchanged [OF x]) 1874 done 1875 1876lemma result_in_set_wp : 1877 assumes x: "\<And>P. \<lbrace>P\<rbrace> fn \<lbrace>\<lambda>rv. P\<rbrace>" 1878 shows "\<lbrace>\<lambda>s. True\<rbrace> fn \<lbrace>\<lambda>v s'. (v, s') \<in> fst (fn s')\<rbrace>" 1879 by (rule hoare_pre_imp [OF _ univ_get_wp], simp_all add: x split_def) clarsimp 1880 1881lemma other_result_in_set_wp: 1882 assumes x: "\<And>P. \<lbrace>P\<rbrace> fn \<lbrace>\<lambda>rv. P\<rbrace>" 1883 shows "\<lbrace>\<lambda>s. \<forall>(v, s) \<in> fst (fn s). F v = v\<rbrace> fn \<lbrace>\<lambda>v s'. (F v, s') \<in> fst (fn s')\<rbrace>" 1884 proof - 1885 have P: "\<And>v s. (F v = v) \<and> (v, s) \<in> fst (fn s) \<Longrightarrow> (F v, s) \<in> fst (fn s)" 1886 by simp 1887 show ?thesis 1888 apply (rule hoare_post_imp [OF P], assumption) 1889 apply (rule hoare_pre_imp) 1890 defer 1891 apply (rule hoare_vcg_conj_lift) 1892 apply (rule univ_get_wp [OF x]) 1893 apply (rule result_in_set_wp [OF x]) 1894 apply clarsimp 1895 apply (erule my_BallE, assumption, simp) 1896 done 1897 qed 1898 1899lemma weak_if_wp: 1900 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> 1901 \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>" 1902 by (auto simp add: valid_def split_def) 1903 1904lemma zipWithM_x_modify: 1905 "zipWithM_x (\<lambda>a b. modify (f a b)) as bs 1906 = modify (\<lambda>s. foldl (\<lambda>s (a, b). f a b s) s (zip as bs))" 1907 apply (simp add: zipWithM_x_def zipWith_def sequence_x_def) 1908 apply (induct ("zip as bs")) 1909 apply (simp add: simpler_modify_def return_def) 1910 apply (rule ext) 1911 apply (simp add: simpler_modify_def bind_def split_def) 1912 done 1913 1914lemma bindE_split_recursive_asm: 1915 assumes x: "\<And>x s'. \<lbrakk> (Inr x, s') \<in> fst (f s) \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. B x s \<and> s = s'\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>" 1916 shows "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>st. A st \<and> st = s\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>" 1917 apply (clarsimp simp: validE_def valid_def bindE_def bind_def lift_def) 1918 apply (erule allE, erule(1) impE) 1919 apply (erule(1) my_BallE, simp) 1920 apply (case_tac a, simp_all add: throwError_def return_def) 1921 apply (drule x) 1922 apply (clarsimp simp: validE_def valid_def) 1923 apply (erule(1) my_BallE, simp) 1924 done 1925 1926lemma bind_known_operation_eq: 1927 "\<lbrakk> no_fail P f; \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<and> s = t\<rbrace>; P s; Q s; empty_fail f \<rbrakk> 1928 \<Longrightarrow> (f >>= g) s = g x t" 1929 apply (drule(1) no_failD) 1930 apply (subgoal_tac "fst (f s) = {(x, t)}") 1931 apply (clarsimp simp: bind_def) 1932 apply (rule not_psubset_eq) 1933 apply (drule(1) empty_failD2, clarsimp) 1934 apply fastforce 1935 apply clarsimp 1936 apply (drule(1) use_valid, simp+) 1937 done 1938 1939 1940lemma gets_the_bind_eq: 1941 "\<lbrakk> f s = Some x; g x s = h s \<rbrakk> 1942 \<Longrightarrow> (gets_the f >>= g) s = h s" 1943 by (simp add: gets_the_def bind_assoc exec_gets assert_opt_def) 1944 1945lemma hoare_const_imp_R: 1946 "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> f \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-" 1947 by (cases P, simp_all) 1948 1949lemma hoare_vcg_imp_lift_R: 1950 "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, -; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, - \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, -" 1951 by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits) 1952 1953lemma hoare_disj_division: 1954 "\<lbrakk> P \<or> Q; P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk> 1955 \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace>" 1956 apply safe 1957 apply (rule hoare_pre_imp) 1958 prefer 2 1959 apply simp 1960 apply simp 1961 apply (rule hoare_pre_imp) 1962 prefer 2 1963 apply simp 1964 apply simp 1965 done 1966 1967lemma hoare_grab_asm: 1968 "\<lbrakk> G \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. G \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>" 1969 by (cases G, simp+) 1970 1971lemma hoare_grab_asm2: 1972 "(P' \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>) 1973 \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>" 1974 by (fastforce simp: valid_def) 1975 1976lemma hoare_grab_exs: 1977 assumes x: "\<And>x. P x \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>" 1978 shows "\<lbrace>\<lambda>s. \<exists>x. P x \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>" 1979 apply (clarsimp simp: valid_def) 1980 apply (erule(2) use_valid [OF _ x]) 1981 done 1982 1983lemma hoare_prop_E: "\<lbrace>\<lambda>rv. P\<rbrace> f -,\<lbrace>\<lambda>rv s. P\<rbrace>" 1984 unfolding validE_E_def 1985 by (rule hoare_pre, wp, simp) 1986 1987lemma hoare_vcg_conj_lift_R: 1988 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>,- \<rbrakk> \<Longrightarrow> 1989 \<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> S rv s\<rbrace>,-" 1990 apply (simp add: validE_R_def validE_def) 1991 apply (drule(1) hoare_vcg_conj_lift) 1992 apply (erule hoare_strengthen_post) 1993 apply (clarsimp split: sum.splits) 1994 done 1995 1996lemma hoare_walk_assmsE: 1997 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>" and y: "\<And>s. P s \<Longrightarrow> Q s" and z: "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. Q\<rbrace>" 1998 shows "\<lbrace>P\<rbrace> doE x \<leftarrow> f; g odE \<lbrace>\<lambda>rv. Q\<rbrace>" 1999 apply (wp z) 2000 apply (simp add: validE_def) 2001 apply (rule hoare_strengthen_post [OF x]) 2002 apply (case_tac r, simp_all add: y) 2003 done 2004 2005lemma mapME_set: 2006 assumes est: "\<And>x. \<lbrace>R\<rbrace> f x \<lbrace>P\<rbrace>, -" 2007 and invp: "\<And>x y. \<lbrace>R and P x\<rbrace> f y \<lbrace>\<lambda>_. P x\<rbrace>, -" 2008 and invr: "\<And>x. \<lbrace>R\<rbrace> f x \<lbrace>\<lambda>_. R\<rbrace>, -" 2009 shows "\<lbrace>R\<rbrace> mapME f xs \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. P x s\<rbrace>, -" 2010proof (rule hoare_post_imp_R [where Q' = "\<lambda>rv s. R s \<and> (\<forall>x \<in> set rv. P x s)"], induct xs) 2011 case Nil 2012 thus ?case by (simp add: mapME_Nil | wp returnOKE_R_wp)+ 2013next 2014 case (Cons y ys) 2015 2016 have minvp: "\<And>x. \<lbrace>R and P x\<rbrace> mapME f ys \<lbrace>\<lambda>_. P x\<rbrace>, -" 2017 apply (rule hoare_pre) 2018 apply (rule_tac Q' = "\<lambda>_ s. R s \<and> P x s" in hoare_post_imp_R) 2019 apply (wp mapME_wp' invr invp)+ 2020 apply simp 2021 apply simp 2022 apply simp 2023 done 2024 2025 show ?case 2026 apply (simp add: mapME_Cons) 2027 apply (wp) 2028 apply (rule_tac Q' = "\<lambda>xs s. (R s \<and> (\<forall>x \<in> set xs. P x s)) \<and> P x s" in hoare_post_imp_R) 2029 apply (wp Cons.hyps minvp) 2030 apply simp 2031 apply (fold validE_R_def) 2032 apply simp 2033 apply (wp invr est) 2034 apply simp 2035 done 2036qed clarsimp 2037 2038lemma unlessE_throwError_returnOk: 2039 "(if P then returnOk v else throwError x) 2040 = (unlessE P (throwError x) >>=E (\<lambda>_. returnOk v))" 2041 by (cases P, simp_all add: unlessE_def) 2042 2043lemma weaker_hoare_ifE: 2044 assumes x: "\<lbrace>P \<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 2045 assumes y: "\<lbrace>P'\<rbrace> b \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 2046 shows "\<lbrace>P and P'\<rbrace> if test then a else b \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 2047 apply (rule hoare_vcg_precond_impE) 2048 apply (wp x y) 2049 apply simp 2050 done 2051 2052lemma wp_split_const_if: 2053 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 2054 assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>" 2055 shows "\<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> f \<lbrace>\<lambda>rv s. (G \<longrightarrow> Q rv s) \<and> (\<not> G \<longrightarrow> Q' rv s)\<rbrace>" 2056 by (case_tac G, simp_all add: x y) 2057 2058lemma wp_split_const_if_R: 2059 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" 2060 assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-" 2061 shows "\<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> f \<lbrace>\<lambda>rv s. (G \<longrightarrow> Q rv s) \<and> (\<not> G \<longrightarrow> Q' rv s)\<rbrace>,-" 2062 by (case_tac G, simp_all add: x y) 2063 2064lemma wp_throw_const_imp: 2065 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 2066 shows "\<lbrace>\<lambda>s. G \<longrightarrow> P s\<rbrace> f \<lbrace>\<lambda>rv s. G \<longrightarrow> Q rv s\<rbrace>" 2067 by (case_tac G, simp_all add: x hoare_vcg_prop) 2068 2069lemma wp_throw_const_impE: 2070 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 2071 shows "\<lbrace>\<lambda>s. G \<longrightarrow> P s\<rbrace> f \<lbrace>\<lambda>rv s. G \<longrightarrow> Q rv s\<rbrace>,\<lbrace>\<lambda>rv s. G \<longrightarrow> E rv s\<rbrace>" 2072 apply (case_tac G, simp_all add: x) 2073 apply wp 2074 done 2075 2076lemma distinct_tuple_helper: 2077 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. distinct (x # xs rv s)\<rbrace> \<Longrightarrow> 2078 \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. distinct (x # (map fst (zip (xs rv s) (ys rv s))))\<rbrace>" 2079 apply (erule hoare_strengthen_post) 2080 apply (erule distinct_prefix) 2081 apply (simp add: map_fst_zip_prefix) 2082 done 2083 2084lemma list_case_throw_validE_R: 2085 "\<lbrakk> \<And>y ys. xs = y # ys \<Longrightarrow> \<lbrace>P\<rbrace> f y ys \<lbrace>Q\<rbrace>,- \<rbrakk> \<Longrightarrow> 2086 \<lbrace>P\<rbrace> case xs of [] \<Rightarrow> throwError e | x # xs \<Rightarrow> f x xs \<lbrace>Q\<rbrace>,-" 2087 apply (case_tac xs, simp_all) 2088 apply wp 2089 done 2090 2091lemma validE_R_sp: 2092 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" 2093 assumes y: "\<And>x. \<lbrace>Q x\<rbrace> g x \<lbrace>R\<rbrace>,-" 2094 shows "\<lbrace>P\<rbrace> f >>=E (\<lambda>x. g x) \<lbrace>R\<rbrace>,-" 2095 by (rule hoare_pre, wp x y, simp) 2096 2097lemma valid_set_take_helper: 2098 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (xs rv s). Q x rv s\<rbrace> 2099 \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (take (n rv s) (xs rv s)). Q x rv s\<rbrace>" 2100 apply (erule hoare_strengthen_post) 2101 apply (clarsimp dest!: in_set_takeD) 2102 done 2103 2104lemma whenE_throwError_sp: 2105 "\<lbrace>P\<rbrace> whenE Q (throwError e) \<lbrace>\<lambda>rv s. \<not> Q \<and> P s\<rbrace>, -" 2106 apply (simp add: whenE_def validE_R_def) 2107 apply (intro conjI impI; wp) 2108 done 2109 2110lemma no_fail_bindE [wp]: 2111 "\<lbrakk> no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<rbrakk> 2112 \<Longrightarrow> no_fail (P and Q) (f >>=E g)" 2113 apply (simp add: bindE_def) 2114 apply (erule no_fail_bind) 2115 apply (simp add: lift_def) 2116 apply wpc 2117 apply (simp add: throwError_def) 2118 apply wp 2119 apply assumption 2120 apply (simp add: validE_R_def validE_def) 2121 apply (erule hoare_strengthen_post) 2122 apply clarsimp 2123 done 2124 2125lemma empty_fail_mapM_x [simp]: 2126 "(\<And>x. empty_fail (a x)) \<Longrightarrow> empty_fail (mapM_x a xs)" 2127 apply (induct_tac xs) 2128 apply (clarsimp simp: mapM_x_Nil) 2129 apply (clarsimp simp: mapM_x_Cons) 2130 done 2131 2132lemma fst_throwError_returnOk: 2133 "fst (throwError e s) = {(Inl e, s)}" 2134 "fst (returnOk v s) = {(Inr v, s)}" 2135 by (simp add: throwError_def returnOk_def return_def)+ 2136 2137lemma liftE_bind_return_bindE_returnOk: 2138 "liftE (v >>= (\<lambda>rv. return (f rv))) 2139 = (liftE v >>=E (\<lambda>rv. returnOk (f rv)))" 2140 by (simp add: liftE_bindE, simp add: liftE_def returnOk_def) 2141 2142lemma bind_eqI: 2143 "g = g' \<Longrightarrow> f >>= g = f >>= g'" by simp 2144 2145lemma not_snd_bindE_I1: 2146 "\<not> snd ((a >>=E b) s) \<Longrightarrow> \<not> snd (a s)" 2147 unfolding bindE_def 2148 by (erule not_snd_bindI1) 2149 2150lemma snd_assert [monad_eq]: 2151 "snd (assert P s) = (\<not> P)" 2152 apply (clarsimp simp: fail_def return_def assert_def) 2153 done 2154 2155lemma not_snd_assert : 2156 "(\<not> snd (assert P s)) = P" 2157 by (metis snd_assert) 2158 2159lemma snd_assert_opt [monad_eq]: 2160 "snd (assert_opt f s) = (f = None)" 2161 by (monad_eq simp: assert_opt_def split: option.splits) 2162 2163declare in_assert_opt [monad_eq] 2164 2165lemma empty_fail_catch: 2166 "\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catch f g)" 2167 apply (simp add: catch_def) 2168 apply (erule empty_fail_bind) 2169 apply (simp split: sum.split) 2170 done 2171 2172lemma oblivious_returnOk [simp]: 2173 "oblivious f (returnOk e)" 2174 by (simp add: returnOk_def) 2175 2176lemma oblivious_assertE [simp]: 2177 "oblivious f (assertE P)" 2178 by (simp add: assertE_def split: if_split) 2179 2180 2181lemma oblivious_throwError [simp]: 2182 "oblivious f (throwError e)" 2183 by (simp add: throwError_def) 2184 2185lemma oblivious_bindE: 2186 "\<lbrakk> oblivious u f; \<And>v. oblivious u (g v) \<rbrakk> 2187 \<Longrightarrow> oblivious u (f >>=E (\<lambda>v. g v))" 2188 apply (simp add: bindE_def) 2189 apply (erule oblivious_bind) 2190 apply (simp add: lift_def split: sum.split) 2191 done 2192 2193lemma oblivious_catch: 2194 "\<lbrakk> oblivious u f; \<And>v. oblivious u (g v) \<rbrakk> 2195 \<Longrightarrow> oblivious u (catch f g)" 2196 apply (simp add: catch_def) 2197 apply (erule oblivious_bind) 2198 apply (simp split: sum.split) 2199 done 2200 2201lemma oblivious_when [simp]: 2202 "oblivious f (when P m) = (P \<longrightarrow> oblivious f m)" 2203 by (simp add: when_def split: if_split) 2204 2205lemma oblivious_whenE [simp]: 2206 "oblivious f (whenE P g) = (P \<longrightarrow> oblivious f g)" 2207 by (simp add: whenE_def split: if_split) 2208 2209lemma select_f_oblivious [simp]: 2210 "oblivious f (select_f v)" 2211 by (simp add: oblivious_def select_f_def) 2212 2213lemma oblivious_select: 2214 "oblivious f (select S)" 2215 by (simp add: oblivious_def select_def) 2216 2217lemma validE_R_abstract_rv: 2218 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>rv'. Q rv' s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" 2219 by (erule hoare_post_imp_R, simp) 2220 2221lemma validE_cases_valid: 2222 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q (Inr rv) s\<rbrace>,\<lbrace>\<lambda>rv s. Q (Inl rv) s\<rbrace> 2223 \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 2224 apply (simp add: validE_def) 2225 apply (erule hoare_strengthen_post) 2226 apply (simp split: sum.split_asm) 2227 done 2228 2229lemma valid_isRight_theRight_split: 2230 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q True rv s\<rbrace>,\<lbrace>\<lambda>e s. \<forall>v. Q False v s\<rbrace> \<Longrightarrow> 2231 \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q (isRight rv) (theRight rv) s\<rbrace>" 2232 apply (simp add: validE_def) 2233 apply (erule hoare_strengthen_post) 2234 apply (simp add: isRight_def split: sum.split_asm) 2235 done 2236 2237lemma bind_return_subst: 2238 assumes r: "\<And>r. \<lbrace>\<lambda>s. P x = r\<rbrace> f x \<lbrace>\<lambda>rv s. Q rv = r\<rbrace>" 2239 shows 2240 "do a \<leftarrow> f x; 2241 g (Q a) 2242 od = 2243 do _ \<leftarrow> f x; 2244 g (P x) 2245 od" 2246proof - 2247 have "do a \<leftarrow> f x; 2248 return (Q a) 2249 od = 2250 do _ \<leftarrow> f x; 2251 return (P x) 2252 od" 2253 using r 2254 apply (subst fun_eq_iff) 2255 apply (fastforce simp: bind_def valid_def return_def) 2256 done 2257 hence "do a \<leftarrow> f x; 2258 return (Q a) 2259 od >>= g = 2260 do _ \<leftarrow> f x; 2261 return (P x) 2262 od >>= g" 2263 by (rule bind_cong, simp) 2264 thus ?thesis 2265 by simp 2266qed 2267 2268lemma zipWithM_x_Nil2 : 2269 "zipWithM_x f xs [] = return ()" 2270 by (simp add: zipWithM_x_mapM mapM_Nil) 2271 2272lemma assert2: 2273 "(do v1 \<leftarrow> assert P; v2 \<leftarrow> assert Q; c od) 2274 = (do v \<leftarrow> assert (P \<and> Q); c od)" 2275 by (simp add: assert_def split: if_split) 2276 2277lemma assert_opt_def2: 2278 "assert_opt v = (do assert (v \<noteq> None); return (the v) od)" 2279 by (simp add: assert_opt_def split: option.split) 2280 2281lemma filterM_voodoo: 2282 "\<forall>ys. P ys (do zs \<leftarrow> filterM m xs; return (ys @ zs) od) 2283 \<Longrightarrow> P [] (filterM m xs)" 2284 by (drule spec[where x=Nil], simp) 2285 2286lemma gets_assert: 2287 "(do v1 \<leftarrow> assert v; v2 \<leftarrow> gets f; c v1 v2 od) 2288 = (do v2 \<leftarrow> gets f; v1 \<leftarrow> assert v; c v1 v2 od)" 2289 by (simp add: simpler_gets_def return_def assert_def fail_def bind_def 2290 split: if_split) 2291 2292lemma list_case_return2: 2293 "(case x of [] \<Rightarrow> return v | y # ys \<Rightarrow> return (f y ys)) 2294 = return (case x of [] \<Rightarrow> v | y # ys \<Rightarrow> f y ys)" 2295 by (simp split: list.split) 2296 2297lemma modify_assert: 2298 "(do v2 \<leftarrow> modify f; v1 \<leftarrow> assert v; c v1 od) 2299 = (do v1 \<leftarrow> assert v; v2 \<leftarrow> modify f; c v1 od)" 2300 by (simp add: simpler_modify_def return_def assert_def fail_def bind_def 2301 split: if_split) 2302 2303lemma gets_fold_into_modify: 2304 "do x \<leftarrow> gets f; modify (g x) od = modify (\<lambda>s. g (f s) s)" 2305 "do x \<leftarrow> gets f; _ \<leftarrow> modify (g x); h od 2306 = do modify (\<lambda>s. g (f s) s); h od" 2307 by (simp_all add: fun_eq_iff modify_def bind_assoc exec_gets 2308 exec_get exec_put) 2309 2310lemma bind_assoc2: 2311 "(do x \<leftarrow> a; _ \<leftarrow> b; c x od) = (do x \<leftarrow> (do x' \<leftarrow> a; _ \<leftarrow> b; return x' od); c x od)" 2312 by (simp add: bind_assoc) 2313 2314lemma liftM_pre: 2315 assumes rl: "\<lbrace>\<lambda>s. \<not> P s \<rbrace> a \<lbrace> \<lambda>_ _. False \<rbrace>" 2316 shows "\<lbrace>\<lambda>s. \<not> P s \<rbrace> liftM f a \<lbrace> \<lambda>_ _. False \<rbrace>" 2317 unfolding liftM_def 2318 apply (rule seq) 2319 apply (rule rl) 2320 apply wp 2321 apply simp 2322 done 2323 2324lemma not_snd_bindD': 2325 "\<lbrakk>\<not> snd ((a >>= b) s); \<not> snd (a s) \<Longrightarrow> (rv, s') \<in> fst (a s)\<rbrakk> \<Longrightarrow> \<not> snd (a s) \<and> \<not> snd (b rv s')" 2326 apply (frule not_snd_bindI1) 2327 apply (erule not_snd_bindD) 2328 apply simp 2329 done 2330 2331lemma snd_bind [monad_eq]: 2332 "snd ((a >>= b) s) = (snd (a s) \<or> (\<exists>r s'. (r, s') \<in> fst (a s) \<and> snd (b r s')))" 2333 apply (clarsimp simp add: bind_def Bex_def image_def) 2334 apply (subst surjective_pairing, subst prod.inject, force) 2335 done 2336 2337lemma in_lift [monad_eq]: 2338 "(rv, s') \<in> fst (lift M v s) = 2339 (case v of Inl x \<Rightarrow> rv = Inl x \<and> s' = s 2340 | Inr x \<Rightarrow> (rv, s') \<in> fst (M x s))" 2341 apply (clarsimp simp: lift_def throwError_def return_def split: sum.splits) 2342 done 2343 2344lemma snd_lift [monad_eq]: 2345 "snd (lift M a b) = (\<exists>x. a = Inr x \<and> snd (M x b))" 2346 apply (clarsimp simp: lift_def throwError_def return_def split: sum.splits) 2347 done 2348 2349lemma snd_bindE [monad_eq]: 2350 "snd ((a >>=E b) s) = (snd (a s) \<or> (\<exists>r s'. (r, s') \<in> fst (a s) \<and> (\<exists>a. r = Inr a \<and> snd (b a s'))))" 2351 apply (clarsimp simp: bindE_def) 2352 apply monad_eq 2353 done 2354 2355lemma snd_get [monad_eq]: 2356 shows "(snd (get s)) = False" 2357 by (simp add: get_def) 2358 2359lemma snd_gets [monad_eq]: 2360 shows "(snd (gets f s)) = False" 2361 by (simp add: gets_def snd_bind snd_get snd_return) 2362 2363lemma mapME_x_Cons: 2364 "mapME_x f (x # xs) = (doE f x; mapME_x f xs odE)" 2365 by (simp add: mapME_x_def sequenceE_x_def) 2366 2367lemma liftME_map_mapME: 2368 "liftME (map f) (mapME m xs) 2369 = mapME (liftME f o m) xs" 2370 apply (rule sym) 2371 apply (induct xs) 2372 apply (simp add: liftME_def mapME_Nil) 2373 apply (simp add: mapME_Cons liftME_def bindE_assoc) 2374 done 2375 2376lemma mapM_upd_inv: 2377 assumes f: "\<And>x rv. (rv,s) \<in> fst (f x s) \<Longrightarrow> x \<in> set xs \<Longrightarrow> (rv, g s) \<in> fst (f x (g s))" 2378 assumes inv: "\<And>x. \<lbrace>(=) s\<rbrace> f x \<lbrace>\<lambda>_. (=) s\<rbrace>" 2379 shows "(rv,s) \<in> fst (mapM f xs s) \<Longrightarrow> (rv, g s) \<in> fst (mapM f xs (g s))" 2380 using f inv 2381proof (induct xs arbitrary: rv s) 2382 case Nil 2383 thus ?case by (simp add: mapM_Nil return_def) 2384next 2385 case (Cons z zs) 2386 from Cons.prems 2387 show ?case 2388 apply (clarsimp simp: mapM_Cons in_monad) 2389 apply (frule use_valid, assumption, rule refl) 2390 apply clarsimp 2391 apply (drule Cons.prems, simp) 2392 apply (rule exI, erule conjI) 2393 apply (drule Cons.hyps) 2394 apply simp 2395 apply assumption 2396 apply simp 2397 done 2398qed 2399 2400 2401(* FUXME: duplicate *) 2402lemma mapM_x_append2: 2403 "mapM_x f (xs @ ys) = do mapM_x f xs; mapM_x f ys od" 2404 apply (simp add: mapM_x_def sequence_x_def) 2405 apply (induct xs) 2406 apply simp 2407 apply (simp add: bind_assoc) 2408 done 2409 2410lemma mapM_x_split_append: 2411 "mapM_x f xs = do _ \<leftarrow> mapM_x f (take n xs); mapM_x f (drop n xs) od" 2412 using mapM_x_append[where f=f and xs="take n xs" and ys="drop n xs"] 2413 by simp 2414 2415lemma hoare_gen_asm': 2416 "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P' and (\<lambda>_. P)\<rbrace> f \<lbrace>Q\<rbrace>" 2417 apply (auto intro: hoare_assume_pre) 2418 done 2419 2420lemma hoare_gen_asm_conj: 2421 "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<and> P\<rbrace> f \<lbrace>Q\<rbrace>" 2422 by (fastforce simp: valid_def) 2423 2424 2425lemma hoare_add_K: 2426 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> I\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> I\<rbrace>" 2427 by (fastforce simp: valid_def) 2428 2429 2430lemma valid_rv_lift: 2431 "\<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q rv s\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> P \<and> Q rv s\<rbrace>" 2432 by (fastforce simp: valid_def) 2433 2434lemma valid_imp_ex: 2435 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. rv \<longrightarrow> Q rv s x\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (\<exists>x. Q rv s x)\<rbrace>" 2436 by (fastforce simp: valid_def) 2437 2438lemma valid_rv_split: 2439 "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<not>rv \<longrightarrow> Q' s\<rbrace>\<rbrakk> 2440 \<Longrightarrow> 2441 \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. if rv then Q s else Q' s\<rbrace>" 2442 by (fastforce simp: valid_def) 2443 2444lemma hoare_rv_split: 2445 "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (Q rv s)\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (\<not>rv) \<longrightarrow> (Q rv s)\<rbrace>\<rbrakk> 2446 \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 2447 apply (clarsimp simp: valid_def) 2448 apply (case_tac a, fastforce+) 2449 done 2450 2451lemma case_option_find_give_me_a_map: 2452 "case_option a return (find f xs) 2453 = liftM theLeft 2454 (mapME (\<lambda>x. if (f x) then throwError x else returnOk ()) xs 2455 >>=E (\<lambda>x. assert (\<forall>x \<in> set xs. \<not> f x) 2456 >>= (\<lambda>_. liftM (Inl :: 'a \<Rightarrow> 'a + unit) a)))" 2457 apply (induct xs) 2458 apply simp 2459 apply (simp add: liftM_def mapME_Nil) 2460 apply (simp add: mapME_Cons split: if_split) 2461 apply (clarsimp simp add: throwError_def bindE_def bind_assoc 2462 liftM_def) 2463 apply (rule bind_cong [OF refl]) 2464 apply (simp add: lift_def throwError_def returnOk_def split: sum.split) 2465 done 2466 2467lemma if_bind: 2468 "(if P then (a >>= (\<lambda>_. b)) else return ()) = 2469 (if P then a else return ()) >>= (\<lambda>_. if P then b else return ())" 2470 apply (cases P) 2471 apply simp 2472 apply simp 2473 done 2474 2475lemma in_handleE' [monad_eq]: 2476 "((rv, s') \<in> fst ((f <handle2> g) s)) = 2477 ((\<exists>ex. rv = Inr ex \<and> (Inr ex, s') \<in> fst (f s)) \<or> 2478 (\<exists>rv' s''. (rv, s') \<in> fst (g rv' s'') \<and> (Inl rv', s'') \<in> fst (f s)))" 2479 apply (clarsimp simp: handleE'_def) 2480 apply (rule iffI) 2481 apply (subst (asm) in_bind_split) 2482 apply (clarsimp simp: return_def split: sum.splits) 2483 apply (case_tac a) 2484 apply (erule allE, erule (1) impE) 2485 apply clarsimp 2486 apply (erule allE, erule (1) impE) 2487 apply clarsimp 2488 apply (subst in_bind_split) 2489 apply (clarsimp simp: return_def split: sum.splits) 2490 apply blast 2491 done 2492 2493lemma in_handleE [monad_eq]: 2494 "(a, b) \<in> fst ((A <handle> B) s) = 2495 ((\<exists>x. a = Inr x \<and> (Inr x, b) \<in> fst (A s)) 2496 \<or> (\<exists>r t. ((Inl r, t) \<in> fst (A s)) \<and> ((a, b) \<in> fst (B r t))))" 2497 apply (unfold handleE_def) 2498 apply (monad_eq split: sum.splits) 2499 apply blast 2500 done 2501 2502lemma snd_handleE' [monad_eq]: 2503 "snd ((A <handle2> B) s) = (snd (A s) \<or> (\<exists>r s'. (r, s')\<in>fst (A s) \<and> (\<exists>a. r = Inl a \<and> snd (B a s'))))" 2504 apply (clarsimp simp: handleE'_def) 2505 apply (monad_eq simp: Bex_def split: sum.splits) 2506 apply (metis sum.sel(1) sum.distinct(1) sumE) 2507 done 2508 2509lemma snd_handleE [monad_eq]: 2510 "snd ((A <handle> B) s) = (snd (A s) \<or> (\<exists>r s'. (r, s')\<in>fst (A s) \<and> (\<exists>a. r = Inl a \<and> snd (B a s'))))" 2511 apply (unfold handleE_def) 2512 apply (rule snd_handleE') 2513 done 2514 2515declare in_liftE [monad_eq] 2516 2517lemma snd_liftE [monad_eq]: 2518 "snd ((liftE x) s) = snd (x s)" 2519 apply (clarsimp simp: liftE_def snd_bind snd_return) 2520 done 2521 2522lemma snd_returnOk [monad_eq]: 2523 "\<not> snd (returnOk x s)" 2524 apply (clarsimp simp: returnOk_def return_def) 2525 done 2526 2527lemma snd_when [monad_eq]: 2528 "snd (when P M s) = (P \<and> snd (M s))" 2529 apply (clarsimp simp: when_def return_def) 2530 done 2531 2532lemma bind_liftE_distrib: "(liftE (A >>= (\<lambda>x. B x))) = (liftE A >>=E (\<lambda>x. liftE (\<lambda>s. B x s)))" 2533 apply (clarsimp simp: liftE_def bindE_def lift_def bind_assoc) 2534 done 2535 2536lemma in_condition [monad_eq]: 2537 "((a, b) \<in> fst (condition C L R s)) = ((C s \<longrightarrow> (a, b) \<in> fst (L s)) \<and> (\<not> C s \<longrightarrow> (a, b) \<in> fst (R s)))" 2538 by (rule condition_split) 2539 2540lemma snd_condition [monad_eq]: 2541 "(snd (condition C L R s)) = ((C s \<longrightarrow> snd (L s)) \<and> (\<not> C s \<longrightarrow> snd (R s)))" 2542 by (rule condition_split) 2543 2544lemma condition_apply_cong: 2545 "\<lbrakk> c s = c' s'; s = s'; \<And>s. c' s \<Longrightarrow> l s = l' s ; \<And>s. \<not> c' s \<Longrightarrow> r s = r' s \<rbrakk> \<Longrightarrow> condition c l r s = condition c' l' r' s'" 2546 apply (clarsimp split: condition_splits) 2547 done 2548 2549lemma condition_cong [cong, fundef_cong]: 2550 "\<lbrakk> c = c'; \<And>s. c' s \<Longrightarrow> l s = l' s; \<And>s. \<not> c' s \<Longrightarrow> r s = r' s \<rbrakk> \<Longrightarrow> condition c l r = condition c' l' r'" 2551 apply (rule ext) 2552 apply (clarsimp split: condition_splits) 2553 done 2554 2555(* Alternative definition of no_throw; easier to work with than unfolding validE. *) 2556lemma no_throw_def': "no_throw P A = (\<forall>s. P s \<longrightarrow> (\<forall>(r, t) \<in> fst (A s). (\<exists>x. r = Inr x)))" 2557 apply (clarsimp simp: no_throw_def validE_def2 split_def split: sum.splits) 2558 done 2559 2560lemma no_throw_returnOk [simp]: 2561 "no_throw P (returnOk a)" 2562 apply (clarsimp simp: no_throw_def) 2563 apply wp 2564 done 2565 2566lemma no_throw_liftE [simp]: 2567 "no_throw P (liftE x)" 2568 apply (clarsimp simp: liftE_def no_throw_def validE_def) 2569 apply (wp | simp)+ 2570 done 2571 2572lemma no_throw_bindE: "\<lbrakk> no_throw A X; \<And>a. no_throw B (Y a); \<lbrace> A \<rbrace> X \<lbrace> \<lambda>_. B \<rbrace>,\<lbrace> \<lambda>_ _. True \<rbrace> \<rbrakk> \<Longrightarrow> no_throw A (X >>=E Y)" 2573 apply atomize 2574 apply (clarsimp simp: no_throw_def) 2575 apply (rule seqE [rotated]) 2576 apply force 2577 apply (rule hoare_validE_cases) 2578 apply simp 2579 apply simp 2580 done 2581 2582lemma no_throw_bindE_simple: "\<lbrakk> no_throw \<top> L; \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L >>=E R)" 2583 apply (erule no_throw_bindE) 2584 apply assumption 2585 apply wp 2586 done 2587 2588lemma no_throw_handleE_simple: 2589 notes hoare_vcg_prop[wp del] 2590 shows "\<lbrakk> \<And>x. no_throw \<top> L \<or> no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)" 2591 apply (clarsimp simp: no_throw_def) 2592 apply atomize 2593 apply clarsimp 2594 apply (erule disjE) 2595 apply (wpsimp wp: hoare_vcg_prop[where f="R x" for x]) 2596 apply assumption 2597 apply simp 2598 apply (rule handleE_wp) 2599 apply (erule_tac x=x in allE) 2600 apply assumption 2601 apply wp 2602 done 2603 2604lemma no_throw_handle2: "\<lbrakk> \<And>a. no_throw Y (B a); \<lbrace> X \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_. Y \<rbrace> \<rbrakk> \<Longrightarrow> no_throw X (A <handle2> B)" 2605 apply atomize 2606 apply (clarsimp simp: no_throw_def' handleE'_def bind_def) 2607 apply (clarsimp simp: validE_def valid_def) 2608 apply (erule allE, erule (1) impE) 2609 apply (erule (1) my_BallE) 2610 apply (clarsimp simp: return_def split: sum.splits) 2611 apply force 2612 done 2613 2614lemma no_throw_handle: "\<lbrakk> \<And>a. no_throw Y (B a); \<lbrace> X \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_. Y \<rbrace> \<rbrakk> \<Longrightarrow> no_throw X (A <handle> B)" 2615 apply (unfold handleE_def) 2616 apply (erule (1) no_throw_handle2) 2617 done 2618 2619lemma no_throw_fail [simp]: "no_throw P fail" 2620 apply (clarsimp simp: no_throw_def) 2621 done 2622 2623lemma lift_Inr [simp]: "(lift X (Inr r)) = (X r)" 2624 apply (rule ext)+ 2625 apply (clarsimp simp: lift_def bind_def split_def image_def) 2626 done 2627 2628lemma lift_Inl [simp]: "lift C (Inl a) = throwError a" 2629 apply (clarsimp simp: lift_def throwError_def) 2630 done 2631 2632lemma returnOk_def2: "returnOk a = return (Inr a)" 2633 apply (clarsimp simp: returnOk_def return_def) 2634 done 2635 2636lemma empty_fail_spec [simp]: "empty_fail (state_select F)" 2637 apply (clarsimp simp: state_select_def empty_fail_def) 2638 done 2639 2640declare snd_fail [simp] 2641 2642lemma empty_fail_select [simp]: "empty_fail (select V) = (V \<noteq> {})" 2643 apply (clarsimp simp: select_def empty_fail_def) 2644 done 2645 2646lemma bind_fail_propagates: "\<lbrakk> empty_fail A \<rbrakk> \<Longrightarrow> A >>= (\<lambda>_. fail) = fail" 2647 apply (monad_eq simp: empty_fail_def) 2648 by fastforce 2649 2650lemma bindE_fail_propagates: "\<lbrakk> no_throw \<top> A; empty_fail A \<rbrakk> \<Longrightarrow> A >>=E (\<lambda>_. fail) = fail" 2651 apply (rule ext) 2652 apply (clarsimp simp: empty_fail_def) 2653 apply (clarsimp simp: no_throw_def validE_def valid_def bind_def 2654 bindE_def split_def fail_def NonDetMonad.lift_def throwError_def 2655 split:sum.splits) 2656 apply fastforce 2657 done 2658 2659lemma empty_fail_liftE [simp]: 2660 "empty_fail (liftE X) = empty_fail X" 2661 apply (simp add: empty_fail_error_bits) 2662 done 2663 2664declare snd_returnOk [simp, monad_eq] 2665 2666lemma liftE_fail [simp]: "liftE fail = fail" 2667 apply monad_eq 2668 done 2669 2670lemma in_catch [monad_eq]: 2671 "(r, t) \<in> fst ((M <catch> E) s) 2672 = ((Inr r, t) \<in> fst (M s) 2673 \<or> (\<exists>r' s'. ((Inl r', s') \<in> fst (M s)) \<and> (r, t) \<in> fst (E r' s')))" 2674 apply (rule iffI) 2675 apply (clarsimp simp: catch_def in_bind in_return split: sum.splits) 2676 apply (metis sumE) 2677 apply (clarsimp simp: catch_def in_bind in_return split: sum.splits) 2678 apply (metis sum.sel(1) sum.distinct(1) sum.inject(2)) 2679 done 2680 2681lemma snd_catch [monad_eq]: 2682 "snd ((M <catch> E) s) 2683 = (snd (M s) 2684 \<or> (\<exists>r' s'. ((Inl r', s') \<in> fst (M s)) \<and> snd (E r' s')))" 2685 apply (rule iffI) 2686 apply (clarsimp simp: catch_def snd_bind snd_return split: sum.splits) 2687 apply (clarsimp simp: catch_def snd_bind snd_return split: sum.splits) 2688 apply force 2689 done 2690 2691lemma in_get [monad_eq]: 2692 "(r, s') \<in> fst (get s) = (r = s \<and> s' = s)" 2693 apply (clarsimp simp: get_def) 2694 done 2695 2696lemma returnOk_cong: "\<lbrakk> \<And>s. B a s = B' a s \<rbrakk> \<Longrightarrow> ((returnOk a) >>=E B) = ((returnOk a) >>=E B')" 2697 apply monad_eq 2698 done 2699 2700lemma in_state_assert [monad_eq, simp]: 2701 "(rv, s') \<in> fst (state_assert P s) = (rv = () \<and> s' = s \<and> P s)" 2702 apply (monad_eq simp: state_assert_def) 2703 apply metis 2704 done 2705 2706lemma snd_state_assert [monad_eq]: 2707 "snd (state_assert P s) = (\<not> P s)" 2708 apply (monad_eq simp: state_assert_def Bex_def) 2709 done 2710 2711lemma state_assert_false [simp]: "state_assert (\<lambda>_. False) = fail" 2712 by monad_eq 2713 2714lemma no_fail_state_assert [wp]: "no_fail P (state_assert P)" 2715 by (monad_eq simp: no_fail_def state_assert_def) 2716 2717lemma no_fail_modify [wp]: "no_fail \<top> (modify M)" 2718 by (metis non_fail_modify) 2719 2720lemma combine_validE: "\<lbrakk> \<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; 2721 \<lbrace> P' \<rbrace> x \<lbrace> Q' \<rbrace>,\<lbrace> E' \<rbrace> \<rbrakk> \<Longrightarrow> 2722 \<lbrace> P and P' \<rbrace> x \<lbrace> \<lambda>r. (Q r) and (Q' r) \<rbrace>,\<lbrace>\<lambda>r. (E r) and (E' r) \<rbrace>" 2723 apply (clarsimp simp: validE_def valid_def split: sum.splits) 2724 apply (erule allE, erule (1) impE)+ 2725 apply (erule (1) my_BallE)+ 2726 apply clarsimp 2727 done 2728 2729lemma condition_swap: "(condition C A B) = (condition (\<lambda>s. \<not> C s) B A)" 2730 apply (rule ext) 2731 apply (clarsimp split: condition_splits) 2732 done 2733 2734lemma condition_fail_rhs: "(condition C X fail) = (state_assert C >>= (\<lambda>_. X))" 2735 apply (rule ext) 2736 apply (monad_eq simp: Bex_def) 2737 done 2738 2739lemma condition_fail_lhs: "(condition C fail X) = (state_assert (\<lambda>s. \<not> C s) >>= (\<lambda>_. X))" 2740 apply (metis condition_fail_rhs condition_swap) 2741 done 2742 2743lemma condition_bind_fail [simp]: 2744 "(condition C A B >>= (\<lambda>_. fail)) = condition C (A >>= (\<lambda>_. fail)) (B >>= (\<lambda>_. fail))" 2745 apply monad_eq 2746 apply blast 2747 done 2748 2749lemma no_throw_Inr: 2750 "\<lbrakk> x \<in> fst (A s); no_throw P A; P s \<rbrakk> \<Longrightarrow> \<exists>y. fst x = Inr y" 2751 apply (clarsimp simp: no_throw_def' split: sum.splits) 2752 apply (erule allE, erule (1) impE, erule (1) my_BallE) 2753 apply clarsimp 2754 done 2755 2756lemma no_throw_handleE': "no_throw \<top> A \<Longrightarrow> (A <handle2> B) = A" 2757 apply (rule monad_eqI) 2758 apply monad_eq 2759 apply (fastforce dest: no_throw_Inr) 2760 apply monad_eq 2761 apply (metis (lifting) fst_conv no_throw_Inr) 2762 apply monad_eq 2763 apply (fastforce dest: no_throw_Inr) 2764 done 2765 2766lemma no_throw_handleE: "no_throw \<top> A \<Longrightarrow> (A <handle> B) = A" 2767 apply (unfold handleE_def) 2768 apply (subst no_throw_handleE') 2769 apply auto 2770 done 2771 2772lemma whileLoopE_nothrow: 2773 "\<lbrakk> \<And>x. no_throw \<top> (B x) \<rbrakk> \<Longrightarrow> no_throw \<top> (whileLoopE C B x)" 2774 apply atomize 2775 apply (clarsimp simp: no_throw_def) 2776 apply (rule validE_whileLoopE [where I="\<lambda>_ _. True"]) 2777 apply simp 2778 apply (rule validE_weaken) 2779 apply force 2780 apply simp 2781 apply simp 2782 apply simp 2783 apply simp 2784 done 2785 2786lemma handleE'_nothrow_lhs: 2787 "\<lbrakk> no_throw \<top> L \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle2> R)" 2788 apply (clarsimp simp: no_throw_def) 2789 apply (rule handleE'_wp [rotated]) 2790 apply assumption 2791 apply simp 2792 done 2793 2794lemma handleE'_nothrow_rhs: 2795 "\<lbrakk> \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle2> R)" 2796 apply atomize 2797 apply (clarsimp simp: no_throw_def) 2798 apply (rule handleE'_wp) 2799 apply (erule allE) 2800 apply assumption 2801 apply (rule hoareE_TrueI) 2802 done 2803 2804lemma handleE_nothrow_lhs: 2805 "\<lbrakk> no_throw \<top> L \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)" 2806 by (metis handleE'_nothrow_lhs handleE_def) 2807 2808lemma handleE_nothrow_rhs: 2809 "\<lbrakk> \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)" 2810 by (metis no_throw_handleE_simple) 2811 2812lemma condition_nothrow: "\<lbrakk> no_throw \<top> L; no_throw \<top> R \<rbrakk> \<Longrightarrow> no_throw \<top> (condition C L R)" 2813 apply (clarsimp simp: condition_def no_throw_def validE_def2) 2814 done 2815 2816lemma empty_fail_guard [simp]: "empty_fail (state_assert G)" 2817 apply (clarsimp simp: state_assert_def assert_def empty_fail_def get_def return_def bind_def) 2818 done 2819 2820lemma simple_bind_fail [simp]: 2821 "(state_assert X >>= (\<lambda>_. fail)) = fail" 2822 "(modify M >>= (\<lambda>_. fail)) = fail" 2823 "(return X >>= (\<lambda>_. fail)) = fail" 2824 "(gets X >>= (\<lambda>_. fail)) = fail" 2825 apply (auto intro!: bind_fail_propagates) 2826 done 2827 2828lemma valid_case_prod: 2829 "\<lbrakk> \<And>x y. valid (P x y) (f x y) Q \<rbrakk> \<Longrightarrow> valid (case_prod P v) (case_prod (\<lambda>x y. f x y) v) Q" 2830 by (simp add: split_def) 2831 2832lemma validE_case_prod: 2833 "\<lbrakk> \<And>x y. validE (P x y) (f x y) Q E \<rbrakk> \<Longrightarrow> validE (case_prod P v) (case_prod (\<lambda>x y. f x y) v) Q E" 2834 by (simp add: split_def) 2835 2836lemma in_select [monad_eq]: 2837 "(rv, s') \<in> fst (select S s) = (s' = s \<and> rv \<in> S)" 2838 apply (clarsimp simp: select_def) 2839 apply blast 2840 done 2841 2842lemma snd_select [monad_eq]: 2843 "\<not> snd (select S s)" 2844 by (clarsimp simp: select_def) 2845 2846lemma bindE_handleE_join: 2847 "no_throw \<top> A \<Longrightarrow> (A >>=E (\<lambda>x. (B x) <handle> C)) = ((A >>=E B <handle> C))" 2848 apply (monad_eq simp: Bex_def Ball_def no_throw_def') 2849 apply blast 2850 done 2851 2852lemma catch_bind_distrib: 2853 "do _ <- m <catch> h; f od = (doE m; liftE f odE <catch> (\<lambda>x. do h x; f od))" 2854 by (force simp: catch_def bindE_def bind_assoc liftE_def NonDetMonad.lift_def bind_def 2855 split_def return_def throwError_def 2856 split: sum.splits) 2857 2858lemma if_catch_distrib: 2859 "((if P then f else g) <catch> h) = (if P then f <catch> h else g <catch> h)" 2860 by (simp split: if_split) 2861 2862lemma will_throw_and_catch: 2863 "f = throwError e \<Longrightarrow> (f <catch> (\<lambda>_. g)) = g" 2864 by (simp add: catch_def throwError_def) 2865 2866lemma catch_is_if: 2867 "(doE x <- f; g x odE <catch> h) = 2868 do 2869 rv <- f; 2870 if sum.isl rv then h (projl rv) else g (projr rv) <catch> h 2871 od" 2872 apply (simp add: bindE_def catch_def bind_assoc cong: if_cong) 2873 apply (rule bind_cong, rule refl) 2874 apply (clarsimp simp: NonDetMonad.lift_def throwError_def split: sum.splits) 2875 done 2876 2877lemma snd_put [monad_eq]: 2878 "\<not> snd (put t s)" 2879 by (clarsimp simp: put_def) 2880 2881lemma snd_modify [monad_eq]: 2882 "\<not> snd (modify t s)" 2883 by (clarsimp simp: modify_def put_def get_def bind_def) 2884 2885lemma no_fail_False [simp]: 2886 "no_fail (\<lambda>_. False) X" 2887 by (clarsimp simp: no_fail_def) 2888 2889lemma valid_pre_satisfies_post: 2890 "\<lbrakk> \<And>s r' s'. P s \<Longrightarrow> Q r' s' \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> m \<lbrace> Q \<rbrace>" 2891 by (clarsimp simp: valid_def) 2892 2893lemma validE_pre_satisfies_post: 2894 "\<lbrakk> \<And>s r' s'. P s \<Longrightarrow> Q r' s'; \<And>s r' s'. P s \<Longrightarrow> R r' s' \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> m \<lbrace> Q \<rbrace>,\<lbrace> R \<rbrace>" 2895 by (clarsimp simp: validE_def2 split: sum.splits) 2896 2897lemma snd_gets_the [monad_eq]: 2898 "snd (gets_the X s) = (X s = None)" 2899 by (monad_eq simp: gets_the_def gets_def get_def) 2900 2901lemma liftE_K_bind: "liftE ((K_bind (\<lambda>s. A s)) x) = K_bind (liftE (\<lambda>s. A s)) x" 2902 by clarsimp 2903 2904lemma hoare_assume_preNF: 2905 "(\<And>s. P s \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!" 2906 by (metis validNF_alt_def) 2907 2908lemma bexEI: "\<lbrakk>\<exists>x\<in>S. Q x; \<And>x. \<lbrakk>x \<in> S; Q x\<rbrakk> \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. P x" by blast 2909 2910lemma monad_eq_split: 2911 assumes "\<And>r s. Q r s \<Longrightarrow> f r s = f' r s" 2912 "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>r s. Q r s\<rbrace>" 2913 "P s" 2914 shows "(g >>= f) s = (g >>= f') s" 2915proof - 2916 have pre: "\<And>rv s'. \<lbrakk>(rv, s') \<in> fst (g s)\<rbrakk> \<Longrightarrow> f rv s' = f' rv s'" 2917 using assms unfolding valid_def 2918 by (erule_tac x=s in allE) auto 2919 show ?thesis 2920 apply (simp add: bind_def image_def) 2921 apply (intro conjI) 2922 apply (rule set_eqI) 2923 apply (clarsimp simp: Union_eq) 2924 apply (rule iffI; elim exEI conjE; simp; elim exEI bexEI; clarsimp simp: pre) 2925 apply (rule iffI; cases "snd (g s)"; simp; elim exEI bexEI; clarsimp simp: pre) 2926 done 2927qed 2928 2929lemma monad_eq_split2: 2930assumes eq: " g' s = g s" 2931assumes tail:"\<And>r s. Q r s \<Longrightarrow> f r s = f' r s" 2932and hoare: "\<lbrace>P\<rbrace>g\<lbrace>\<lambda>r s. Q r s\<rbrace>" "P s" 2933shows "(g>>=f) s = (g'>>= f') s" 2934proof - 2935have pre: "\<And>aa bb. \<lbrakk>(aa, bb) \<in> fst (g s)\<rbrakk> \<Longrightarrow> Q aa bb" 2936 using hoare by (auto simp: valid_def) 2937show ?thesis 2938 apply (simp add:bind_def eq split_def image_def) 2939 apply (rule conjI) 2940 apply (rule set_eqI) 2941 apply (clarsimp simp:Union_eq) 2942 apply (metis pre surjective_pairing tail) 2943 apply (metis pre surjective_pairing tail) 2944 done 2945qed 2946 2947lemma monad_eq_split_tail: 2948 "\<lbrakk>f = g;a s = b s\<rbrakk> \<Longrightarrow> (a >>= f) s = ((b >>= g) s)" 2949 by (simp add:bind_def) 2950 2951lemma double_gets_drop_regets: 2952 "(do x \<leftarrow> gets f; 2953 xa \<leftarrow> gets f; 2954 m xa x 2955 od) = 2956 (do xa \<leftarrow> gets f; 2957 m xa xa 2958 od)" 2959 by (simp add: gets_def get_def bind_def return_def) 2960 2961definition monad_commute where 2962 "monad_commute P a b \<equiv> 2963 (\<forall>s. (P s \<longrightarrow> ((do x\<leftarrow>a;y\<leftarrow>b; return (x, y) od) s) = ((do y\<leftarrow>b;x\<leftarrow>a; return (x, y) od) s)))" 2964 2965 2966lemma monad_eq: 2967 "a s = b s \<Longrightarrow> (a >>= g) s = (b >>= g) s" 2968 by (auto simp:bind_def) 2969 2970lemma monad_commute_simple: 2971 "\<lbrakk>monad_commute P a b;P s\<rbrakk> \<Longrightarrow> ((do x\<leftarrow>a;y\<leftarrow>b; g x y od) s) = ((do y\<leftarrow>b;x\<leftarrow>a; g x y od) s)" 2972 apply (clarsimp simp:monad_commute_def) 2973 apply (drule spec) 2974 apply (erule(1) impE) 2975 apply (drule_tac g = "(\<lambda>t. g (fst t) (snd t))" in monad_eq) 2976 apply (simp add:bind_assoc) 2977 done 2978 2979lemma commute_commute: 2980 "monad_commute P f h \<Longrightarrow> monad_commute P h f" 2981 apply (simp (no_asm) add: monad_commute_def) 2982 apply (clarsimp) 2983 apply (erule monad_commute_simple[symmetric]) 2984 apply simp 2985 done 2986 2987lemma assert_commute: "monad_commute (K G) (assert G) f" 2988 by (clarsimp simp:assert_def monad_commute_def) 2989 2990lemma cond_fail_commute: "monad_commute (K (\<not>G)) (when G fail) f" 2991 by (clarsimp simp:when_def fail_def monad_commute_def) 2992 2993lemma return_commute: "monad_commute \<top> (return a) f" 2994 by (clarsimp simp: return_def bind_def monad_commute_def) 2995 2996lemma monad_commute_guard_imp: 2997 "\<lbrakk>monad_commute P f h; \<And>s. Q s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> monad_commute Q f h" 2998 by (clarsimp simp:monad_commute_def) 2999 3000lemma monad_commute_split: 3001 "\<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; 3002 \<lbrace>P'\<rbrace> h \<lbrace>\<lambda>r. Q r\<rbrace>\<rbrakk> 3003 \<Longrightarrow> monad_commute (P and P') f (h>>=g)" 3004 apply (simp (no_asm) add:monad_commute_def) 3005 apply (clarsimp simp:bind_assoc) 3006 apply (subst monad_commute_simple) 3007 apply simp+ 3008 apply (rule_tac Q = "(\<lambda>x. Q x)" in monad_eq_split) 3009 apply (subst monad_commute_simple[where a = f]) 3010 apply assumption 3011 apply simp+ 3012 done 3013 3014lemma monad_commute_get: 3015 assumes hf: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. P\<rbrace>" 3016 and hg: "\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>r. P\<rbrace>" 3017 and eptyf: "empty_fail f" "empty_fail g" 3018 shows "monad_commute \<top> f g" 3019proof - 3020 have fsame: "\<And>a b s. (a,b) \<in> fst (f s) \<Longrightarrow> b = s" 3021 by (drule use_valid[OF _ hf],auto) 3022 have gsame: "\<And>a b s. (a,b) \<in> fst (g s) \<Longrightarrow> b = s" 3023 by (drule use_valid[OF _ hg],auto) 3024 note ef = empty_fail_not_snd[OF _ eptyf(1)] 3025 note eg = empty_fail_not_snd[OF _ eptyf(2)] 3026 show ?thesis 3027 apply (simp add:monad_commute_def) 3028 apply (clarsimp simp:bind_def split_def return_def) 3029 apply (intro conjI) 3030 apply (rule set_eqI) 3031 apply (rule iffI) 3032 apply (clarsimp simp:Union_eq dest!: singletonD) 3033 apply (frule fsame) 3034 apply clarsimp 3035 apply (frule gsame) 3036 apply (metis fst_conv snd_conv) 3037 apply (clarsimp simp:Union_eq dest!: singletonD) 3038 apply (frule gsame) 3039 apply clarsimp 3040 apply (frule fsame) 3041 apply clarsimp 3042 apply (metis fst_conv snd_conv) 3043 apply (rule iffI) 3044 apply (erule disjE) 3045 apply (clarsimp simp:image_def) 3046 apply (metis fsame) 3047 apply (clarsimp simp:image_def) 3048 apply (drule eg) 3049 apply clarsimp 3050 apply (rule bexI [rotated], assumption) 3051 apply (frule gsame) 3052 apply clarsimp 3053 apply (erule disjE) 3054 apply (clarsimp simp:image_def dest!:gsame) 3055 apply (clarsimp simp:image_def) 3056 apply (drule ef) 3057 apply clarsimp 3058 apply (frule fsame) 3059 apply (erule bexI[rotated]) 3060 apply simp 3061 done 3062qed 3063 3064lemma mapM_x_commute: 3065assumes commute: 3066 "\<And>r. monad_commute (P r) a (b r)" 3067and single: 3068 "\<And>r x. \<lbrace>P r and K (f r \<noteq> f x) and P x\<rbrace> b x \<lbrace>\<lambda>v. P r \<rbrace>" 3069shows 3070 "monad_commute (\<lambda>s. (distinct (map f list)) \<and> (\<forall>r\<in> set list. P r s)) a (mapM_x b list)" 3071 apply (induct list) 3072 apply (clarsimp simp:mapM_x_Nil return_def bind_def monad_commute_def) 3073 apply (clarsimp simp:mapM_x_Cons) 3074 apply (rule monad_commute_guard_imp) 3075 apply (rule monad_commute_split) 3076 apply assumption 3077 apply (rule monad_commute_guard_imp[OF commute]) 3078 apply assumption 3079 apply (wp hoare_vcg_ball_lift) 3080 apply (rule single) 3081 apply (clarsimp simp: image_def) 3082 apply auto 3083 done 3084 3085lemma commute_name_pre_state: 3086assumes "\<And>s. P s \<Longrightarrow> monad_commute ((=) s) f g" 3087shows "monad_commute P f g" 3088 using assms 3089 by (clarsimp simp:monad_commute_def) 3090 3091lemma commute_rewrite: 3092assumes rewrite: "\<And>s. Q s \<Longrightarrow> f s = t s" 3093 and hold : "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>x. Q\<rbrace>" 3094 shows "monad_commute R t g \<Longrightarrow> monad_commute (P and Q and R) f g" 3095 apply (clarsimp simp:monad_commute_def bind_def split_def return_def) 3096 apply (drule_tac x = s in spec) 3097 apply (clarsimp simp:rewrite[symmetric]) 3098 apply (intro conjI) 3099 apply (rule set_eqI) 3100 apply (rule iffI) 3101 apply clarsimp 3102 apply (rule bexI[rotated],assumption) 3103 apply (subst rewrite) 3104 apply (rule use_valid[OF _ hold]) 3105 apply simp+ 3106 apply (erule bexI[rotated],simp) 3107 apply clarsimp 3108 apply (rule bexI[rotated],assumption) 3109 apply (subst rewrite[symmetric]) 3110 apply (rule use_valid[OF _ hold]) 3111 apply simp+ 3112 apply (erule bexI[rotated],simp) 3113 apply (intro iffI) 3114 apply clarsimp 3115 apply (rule bexI[rotated],assumption) 3116 apply simp 3117 apply (subst rewrite) 3118 apply (erule(1) use_valid[OF _ hold]) 3119 apply simp 3120 apply (clarsimp) 3121 apply (drule bspec,assumption) 3122 apply clarsimp 3123 apply (metis rewrite use_valid[OF _ hold]) 3124 done 3125 3126 3127lemma commute_grab_asm: 3128 "(F \<Longrightarrow> monad_commute P f g) \<Longrightarrow> (monad_commute (P and (K F)) f g)" 3129 by (clarsimp simp: monad_commute_def) 3130 3131end 3132