1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6theory TraceMonadLemmas 7imports TraceMonadVCG 8begin 9 10lemma mapM_Cons: 11 "mapM f (x # xs) = do 12 y \<leftarrow> f x; 13 ys \<leftarrow> mapM f xs; 14 return (y # ys) 15 od" 16 and mapM_Nil: 17 "mapM f [] = return []" 18 by (simp_all add: mapM_def sequence_def) 19 20lemma mapM_x_Cons: 21 "mapM_x f (x # xs) = do 22 y \<leftarrow> f x; 23 mapM_x f xs 24 od" 25 and mapM_x_Nil: 26 "mapM_x f [] = return ()" 27 by (simp_all add: mapM_x_def sequence_x_def) 28 29lemma mapM_append: 30 "mapM f (xs @ ys) = (do 31 fxs \<leftarrow> mapM f xs; 32 fys \<leftarrow> mapM f ys; 33 return (fxs @ fys) 34 od)" 35 by (induct xs, simp_all add: mapM_Cons mapM_Nil bind_assoc) 36 37lemma mapM_x_append: 38 "mapM_x f (xs @ ys) = (do 39 x \<leftarrow> mapM_x f xs; 40 mapM_x f ys 41 od)" 42 by (induct xs, simp_all add: mapM_x_Cons mapM_x_Nil bind_assoc) 43 44lemma mapM_map: 45 "mapM f (map g xs) = mapM (f o g) xs" 46 by (induct xs; simp add: mapM_Nil mapM_Cons) 47 48lemma mapM_x_map: 49 "mapM_x f (map g xs) = mapM_x (f o g) xs" 50 by (induct xs; simp add: mapM_x_Nil mapM_x_Cons) 51 52primrec 53 repeat_n :: "nat \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" 54where 55 "repeat_n 0 f = return ()" 56 | "repeat_n (Suc n) f = do f; repeat_n n f od" 57 58lemma repeat_n_mapM_x: 59 "repeat_n n f = mapM_x (\<lambda>_. f) (replicate n ())" 60 by (induct n, simp_all add: mapM_x_Cons mapM_x_Nil) 61 62definition 63 repeat :: "('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" 64where 65 "repeat f = do n \<leftarrow> select UNIV; repeat_n n f od" 66 67definition 68 env_step :: "('s,unit) tmonad" 69where 70 "env_step = 71 (do 72 s' \<leftarrow> select UNIV; 73 put_trace_elem (Env, s'); 74 put s' 75 od)" 76 77abbreviation 78 "env_n_steps n \<equiv> repeat_n n env_step" 79 80lemma elem_select_bind: 81 "(tr, res) \<in> (do x \<leftarrow> select S; f x od) s 82 = (\<exists>x \<in> S. (tr, res) \<in> f x s)" 83 by (simp add: bind_def select_def) 84 85lemma select_bind_UN: 86 "(do x \<leftarrow> select S; f x od) = (\<lambda>s. \<Union>x \<in> S. f x s)" 87 by (rule ext, auto simp: elem_select_bind) 88 89lemma select_early: 90 "S \<noteq> {} 91 \<Longrightarrow> do x \<leftarrow> f; y \<leftarrow> select S; g x y od 92 = do y \<leftarrow> select S; x \<leftarrow> f; g x y od" 93 apply (simp add: bind_def select_def Sigma_def) 94 apply (rule ext) 95 apply (fastforce elim: rev_bexI image_eqI[rotated] split: tmres.split_asm) 96 done 97 98lemma repeat_n_choice: 99 "S \<noteq> {} 100 \<Longrightarrow> repeat_n n (do x \<leftarrow> select S; f x od) 101 = (do xs \<leftarrow> select {xs. set xs \<subseteq> S \<and> length xs = n}; mapM_x f xs od)" 102 apply (induct n; simp?) 103 apply (simp add: select_def bind_def mapM_x_Nil cong: conj_cong) 104 apply (simp add: select_early bind_assoc) 105 apply (subst select_early) 106 apply simp 107 apply (auto intro: exI[where x="replicate n xs" for n xs])[1] 108 apply (simp(no_asm) add: fun_eq_iff set_eq_iff elem_select_bind) 109 apply (simp only: conj_comms[where Q="length xs = n" for xs n]) 110 apply (simp only: ex_simps[symmetric] conj_assoc length_Suc_conv, simp) 111 apply (auto simp: mapM_x_Cons) 112 done 113 114lemma repeat_choice: 115 "S \<noteq> {} 116 \<Longrightarrow> repeat (do x \<leftarrow> select S; f x od) 117 = (do xs \<leftarrow> select {xs. set xs \<subseteq> S}; mapM_x f xs od)" 118 apply (simp add: repeat_def repeat_n_choice) 119 apply (simp(no_asm) add: fun_eq_iff set_eq_iff elem_select_bind) 120 done 121 122lemma put_trace_append: 123 "put_trace (xs @ ys) = do put_trace ys; put_trace xs od" 124 by (induct xs; simp add: bind_assoc) 125 126lemma put_trace_elem_put_comm: 127 "do y \<leftarrow> put_trace_elem x; put s od 128 = do y \<leftarrow> put s; put_trace_elem x od" 129 by (simp add: put_def put_trace_elem_def bind_def insert_commute) 130 131lemma put_trace_put_comm: 132 "do y \<leftarrow> put_trace xs; put s od 133 = do y \<leftarrow> put s; put_trace xs od" 134 apply (rule sym; induct xs; simp) 135 apply (simp add: bind_assoc put_trace_elem_put_comm) 136 apply (simp add: bind_assoc[symmetric]) 137 done 138 139lemma mapM_x_comm: 140 "(\<forall>x \<in> set xs. do y \<leftarrow> g; f x od = do y \<leftarrow> f x; g od) 141 \<Longrightarrow> do y \<leftarrow> g; mapM_x f xs od = do y \<leftarrow> mapM_x f xs; g od" 142 apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons) 143 apply (simp add: bind_assoc[symmetric], simp add: bind_assoc) 144 done 145 146lemma mapM_x_split: 147 "(\<forall>x \<in> set xs. \<forall>y \<in> set xs. do z \<leftarrow> g y; f x od = do (z :: unit) \<leftarrow> f x; g y od) 148 \<Longrightarrow> mapM_x (\<lambda>x. do z \<leftarrow> f x; g x od) xs = do y \<leftarrow> mapM_x f xs; mapM_x g xs od" 149 apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons bind_assoc) 150 apply (subst bind_assoc[symmetric], subst mapM_x_comm[where f=f and g="g x" for x]) 151 apply simp 152 apply (simp add: bind_assoc) 153 done 154 155lemma mapM_x_put: 156 "mapM_x put xs = unless (xs = []) (put (last xs))" 157 apply (induct xs rule: rev_induct) 158 apply (simp add: mapM_x_Nil unless_def when_def) 159 apply (simp add: mapM_x_append mapM_x_Cons mapM_x_Nil) 160 apply (simp add: bind_def unless_def when_def put_def return_def) 161 done 162 163lemma put_trace_mapM_x: 164 "put_trace xs = mapM_x put_trace_elem (rev xs)" 165 by (induct xs; simp add: mapM_x_Nil mapM_x_append mapM_x_Cons) 166 167lemma rev_surj: 168 "surj rev" 169 by (rule_tac f=rev in surjI, simp) 170 171lemma select_image: 172 "select (f ` S) = do x \<leftarrow> select S; return (f x) od" 173 by (auto simp add: bind_def select_def return_def Sigma_def) 174 175lemma env_steps_repeat: 176 "env_steps = repeat env_step" 177 apply (simp add: env_step_def repeat_choice env_steps_def 178 select_early) 179 apply (simp add: put_trace_elem_put_comm) 180 apply (simp add: mapM_x_split put_trace_elem_put_comm put_trace_put_comm 181 mapM_x_put) 182 apply (simp add: put_trace_mapM_x rev_map mapM_x_map o_def) 183 apply (subst rev_surj[symmetric], simp add: select_image bind_assoc) 184 apply (rule arg_cong2[where f=bind, OF refl ext]) 185 apply (simp add: bind_def get_def put_def unless_def when_def return_def) 186 apply (simp add: last_st_tr_def hd_map hd_rev) 187 done 188 189lemma repeat_n_plus: 190 "repeat_n (n + m) f = do repeat_n n f; repeat_n m f od" 191 by (induct n; simp add: bind_assoc) 192 193lemma repeat_eq_twice[simp]: 194 "(do x \<leftarrow> repeat f; repeat f od) = repeat f" 195 apply (simp add: repeat_def select_early) 196 apply (simp add: bind_assoc repeat_n_plus[symmetric, simplified]) 197 apply (simp add: bind_def select_def Sigma_def) 198 apply (rule ext, fastforce intro: exI[where x=0]) 199 done 200 201lemmas bind_then_eq = arg_cong2[where f=bind, OF _ refl] 202lemmas repeat_eq_twice_then[simp] 203 = repeat_eq_twice[THEN bind_then_eq, simplified bind_assoc] 204 205lemmas env_steps_eq_twice[simp] 206 = repeat_eq_twice[where f=env_step, folded env_steps_repeat] 207lemmas env_steps_eq_twice_then[simp] 208 = env_steps_eq_twice[THEN bind_then_eq, simplified bind_assoc] 209 210lemmas mapM_collapse_append = mapM_append[symmetric, THEN bind_then_eq, 211 simplified bind_assoc, simplified] 212 213lemma prefix_closed_mapM[rule_format, wp_split]: 214 "(\<forall>x \<in> set xs. prefix_closed (f x)) \<Longrightarrow> prefix_closed (mapM f xs)" 215 apply (induct xs) 216 apply (simp add: mapM_def sequence_def) 217 apply (clarsimp simp: mapM_Cons) 218 apply (intro prefix_closed_bind allI; clarsimp) 219 done 220 221lemma modify_id: 222 "modify id = return ()" 223 by (simp add: modify_def get_def bind_def put_def return_def) 224 225lemma modify_modify: 226 "(do x \<leftarrow> modify f; modify (g x) od) = modify (g () o f)" 227 by (simp add: bind_def simpler_modify_def) 228 229lemmas modify_modify_bind = arg_cong2[where f=bind, 230 OF modify_modify refl, simplified bind_assoc] 231 232lemma select_single: 233 "select {x} = return x" 234 by (simp add: select_def return_def) 235 236lemma put_then_get[unfolded K_bind_def]: 237 "do put s; get od = do put s; return s od" 238 by (simp add: put_def bind_def get_def return_def) 239 240lemmas put_then_get_then 241 = put_then_get[THEN bind_then_eq, simplified bind_assoc return_bind] 242 243lemmas bind_promote_If 244 = if_distrib[where f="\<lambda>f. bind f g" for g] 245 if_distrib[where f="\<lambda>g. bind f g" for f] 246 247lemma bind_promote_If2: 248 "do x \<leftarrow> f; if P then g x else h x od 249 = (if P then bind f g else bind f h)" 250 by simp 251 252lemma exec_put_trace[unfolded K_bind_def]: 253 "(do put_trace xs; f od) s 254 = (\<Union>n \<in> {n. 0 < n \<and> n \<le> length xs}. {(drop n xs, Incomplete)}) 255 \<union> ((\<lambda>(a, b). (a @ xs, b)) ` f s)" 256 apply (simp add: put_trace_eq_drop bind_def) 257 apply (safe; (clarsimp split: if_split_asm)?; 258 fastforce intro: bexI[where x=0] rev_bexI) 259 done 260 261lemma if_fun_lift: 262 "(if P then f else g) x = (if P then f x else g x)" 263 by simp 264 265lemma UN_If_distrib: 266 "(\<Union>x \<in> S. if P x then A x else B x) 267 = ((\<Union>x \<in> S \<inter> {x. P x}. A x) \<union> (\<Union>x \<in> S \<inter> {x. \<not> P x}. B x))" 268 by (fastforce split: if_split_asm) 269 270lemma Await_redef: 271 "Await P = do 272 s1 \<leftarrow> select {s. P s}; 273 env_steps; 274 s \<leftarrow> get; 275 select (if P s then {()} else {}) 276 od" 277 apply (simp add: Await_def env_steps_def bind_assoc) 278 apply (cases "{s. P s} = {}") 279 apply (simp add: select_def bind_def get_def) 280 apply (rule ext) 281 apply (simp add: exec_get select_bind_UN put_then_get_then) 282 apply (simp add: bind_promote_If2 if_fun_lift if_distrib[where f=select]) 283 apply (simp add: exec_put_trace cong: if_cong) 284 apply (simp add: put_def bind_def select_def cong: if_cong) 285 apply (strengthen equalityI) 286 apply clarsimp 287 apply (strengthen exI[where x="s # xs" for s xs]) 288 apply (strengthen exI[where x="Suc n" for n]) 289 apply simp 290 apply blast 291 done 292 293lemma bind_apply_cong': 294 "f s = f' s 295 \<Longrightarrow> (\<forall>rv s'. (rv, s') \<in> mres (f s) \<longrightarrow> g rv s' = g' rv s') 296 \<Longrightarrow> bind f g s = bind f' g' s" 297 apply (simp add: bind_def) 298 apply (rule SUP_cong; simp?) 299 apply (clarsimp split: tmres.split) 300 apply (drule spec2, drule mp, erule in_mres) 301 apply simp 302 done 303 304lemmas bind_apply_cong = bind_apply_cong'[rule_format] 305 306lemma select_empty_bind[simp]: 307 "select {} >>= f = select {}" 308 by (simp add: select_def bind_def) 309 310lemma fail_bind[simp]: 311 "fail >>= f = fail" 312 by (simp add: bind_def fail_def) 313 314lemma eq_Me_neq_Env: 315 "(x = Me) = (x \<noteq> Env)" 316 by (cases x; simp) 317 318lemma validI_invariant_imp: 319 assumes v: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" 320 and P: "\<forall>s0 s. P s0 s \<longrightarrow> I s0" 321 and R: "\<forall>s0 s. I s0 \<longrightarrow> R s0 s \<longrightarrow> I s" 322 and G: "\<forall>s0 s. I s0 \<longrightarrow> G s0 s \<longrightarrow> I s" 323 shows "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. I s0 \<and> I s \<and> G s0 s\<rbrace>,\<lbrace>\<lambda>rv s0 s. I s0 \<and> Q rv s0 s\<rbrace>" 324proof - 325 { fix tr s0 i 326 assume r: "rely_cond R s0 tr" and g: "guar_cond G s0 tr" 327 and I: "I s0" 328 hence imp: "\<forall>(_, s, s') \<in> trace_steps (rev tr) s0. I s \<longrightarrow> I s'" 329 apply (clarsimp simp: guar_cond_def rely_cond_def) 330 apply (drule(1) bspec)+ 331 apply (clarsimp simp: eq_Me_neq_Env) 332 apply (metis R G) 333 done 334 hence "i < length tr \<longrightarrow> I (snd (rev tr ! i))" 335 using I 336 apply (induct i) 337 apply (clarsimp simp: neq_Nil_conv[where xs="rev tr" for tr, simplified]) 338 apply clarsimp 339 apply (drule bspec, fastforce simp add: trace_steps_nth) 340 apply simp 341 done 342 } 343 note I = this 344 show ?thesis 345 using v 346 apply (clarsimp simp: validI_def rely_def imp_conjL) 347 apply (drule spec2, drule(1) mp)+ 348 apply clarsimp 349 apply (frule P[rule_format]) 350 apply (clarsimp simp: guar_cond_def trace_steps_nth I last_st_tr_def 351 hd_append last_rev[symmetric] 352 last_conv_nth rev_map) 353 done 354qed 355 356lemma validI_guar_post_conj_lift: 357 "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G1\<rbrace>,\<lbrace>Q1\<rbrace> 358 \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G2\<rbrace>,\<lbrace>Q2\<rbrace> 359 \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. G1 s0 s \<and> G2 s0 s\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q1 rv s0 s \<and> Q2 rv s0 s\<rbrace>" 360 apply (frule validI_prefix_closed) 361 apply (subst validI_def, clarsimp simp: rely_def) 362 apply (drule(3) validI_D)+ 363 apply (auto simp: guar_cond_def) 364 done 365 366lemmas modify_prefix_closed[simp] = 367 modify_wp[THEN valid_validI_wp[OF no_trace_all(3)], THEN validI_prefix_closed] 368lemmas await_prefix_closed[simp] = Await_sync_twp[THEN validI_prefix_closed] 369 370lemma repeat_prefix_closed[intro!]: 371 "prefix_closed f \<Longrightarrow> prefix_closed (repeat f)" 372 apply (simp add: repeat_def) 373 apply (rule prefix_closed_bind; clarsimp) 374 apply (rename_tac n) 375 apply (induct_tac n; simp) 376 apply (auto intro: prefix_closed_bind) 377 done 378 379end 380