1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory ExtraCorres 8imports Corres_UL 9begin 10 11lemma corres_mapM: 12 assumes x: "r [] []" 13 assumes y: "\<And>x xs y ys. \<lbrakk> r xs ys; r' x y \<rbrakk> \<Longrightarrow> r (x # xs) (y # ys)" 14 assumes z: "\<And>x y. (x, y) \<in> S \<Longrightarrow> corres_underlying R nf nf' r' P P' (f x) (f' y)" 15 assumes w: "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>" 16 "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>" 17 shows "\<lbrakk> length xs = length ys; set (zip xs ys) \<subseteq> S \<rbrakk> \<Longrightarrow> 18 corres_underlying R nf nf' r P P' (mapM f xs) (mapM f' ys)" 19proof (induct xs ys rule: list_induct2) 20 case Nil 21 show ?case 22 by (simp add: mapM_def sequence_def x) 23next 24 case (Cons a as b bs) 25 from Cons have P: "(a, b) \<in> S" 26 by simp 27 from Cons have Q: "corres_underlying R nf nf' r P P' (mapM f as) (mapM f' bs)" 28 by simp 29 show ?case 30 apply (simp add: mapM_Cons) 31 apply (rule corres_guard_imp) 32 apply (rule corres_split[OF _ z [OF P] w [OF P]]) 33 apply (rule corres_split' [OF Q]) 34 apply (rule corres_trivial, simp add: y) 35 apply (wp | simp)+ 36 done 37qed 38 39(* list_all2 has _much_ nicer simps than set (zip _ _). 40 See KernelInit_R: corres_init_objs for an example *) 41lemma corres_mapM_list_all2: 42 assumes rn: "r [] []" 43 and rc: "\<And>x xs y ys. \<lbrakk> r xs ys; r' x y \<rbrakk> \<Longrightarrow> r (x # xs) (y # ys)" 44 and corr: "\<And>x xs y ys. \<lbrakk> S x y; list_all2 S xs ys \<rbrakk> 45 \<Longrightarrow> corres_underlying sr nf nf' r' (Q (x # xs)) (Q' (y # ys)) (f x) (f' y)" 46 and ha: "\<And>x xs y. \<lbrakk> S x y; suffix (x#xs) as \<rbrakk> \<Longrightarrow> \<lbrace>Q (x # xs)\<rbrace> f x \<lbrace>\<lambda>r. Q xs\<rbrace>" 47 and hc: "\<And>x y ys. \<lbrakk> S x y; suffix (y#ys) cs \<rbrakk> \<Longrightarrow> \<lbrace>Q' (y # ys) \<rbrace> f' y \<lbrace>\<lambda>r. Q' ys\<rbrace>" 48 and lall: "list_all2 S as cs" 49 shows "corres_underlying sr nf nf' r (Q as) (Q' cs) (mapM f as) (mapM f' cs)" 50 using lall 51proof (induct rule: list_all2_induct_suffixeq) 52 case Nil 53 thus ?case 54 unfolding mapM_def sequence_def by (auto intro: rn) 55next 56 case (Cons x xs y ys) 57 58 have corr': "corres_underlying sr nf nf' r' (Q (x # xs)) (Q' (y # ys)) (f x) (f' y)" 59 proof (rule corr) 60 show "list_all2 S xs ys" by (simp add: Cons) 61 qed fact+ 62 63 show ?case 64 apply (simp add: mapM_Cons) 65 apply (rule corres_split' [OF corr' _ ha [OF Cons(2)] hc [OF Cons(2)]]) 66 apply (rule corres_split' [OF Cons(3) _ hoare_post_taut hoare_post_taut]) 67 apply (simp add: rc) 68 apply (rule Cons.hyps)+ 69 done 70qed 71 72lemma corres_mapM_x: 73 assumes x: "\<And>x y. (x, y) \<in> S \<Longrightarrow> corres_underlying sr nf nf' dc P P' (f x) (f' y)" 74 assumes y: "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>" 75 "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>" 76 assumes z: "length xs = length ys" 77 assumes w: "set (zip xs ys) \<subseteq> S" 78 shows "corres_underlying sr nf nf' dc P P' (mapM_x f xs) (mapM_x f' ys)" 79 apply (simp add: mapM_x_mapM) 80 apply (rule corres_guard_imp) 81 apply (rule corres_split_nor) 82 apply (rule corres_trivial, simp) 83 apply (rule corres_mapM [OF _ _ x y z w]) 84 apply (simp | wp)+ 85 done 86 87lemma corres_mapME: 88 assumes x: "r [] []" 89 assumes y: "\<And>x xs y ys. \<lbrakk> r xs ys; r' x y \<rbrakk> \<Longrightarrow> r (x # xs) (y # ys)" 90 assumes z: "\<And>x y. (x, y) \<in> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r') P P' (f x) (f' y)" 91 assumes w: "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>" 92 "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>" 93 shows "\<lbrakk> length xs = length ys; set (zip xs ys) \<subseteq> S \<rbrakk> \<Longrightarrow> 94 corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f xs) (mapME f' ys)" 95proof (induct xs ys rule: list_induct2) 96 case Nil 97 show ?case 98 by (simp add: mapME_def sequenceE_def x returnOk_def) 99next 100 case (Cons a as b bs) 101 from Cons have P: "(a, b) \<in> S" 102 by simp 103 from Cons have Q: "corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f as) (mapME f' bs)" 104 by simp 105 show ?case 106 apply (simp add: mapME_Cons) 107 apply (rule corres_guard_imp) 108 apply (unfold bindE_def validE_def) 109 apply (rule corres_underlying_split [OF z [OF P]]) 110 prefer 3 111 apply clarify 112 apply (simp add: lift_def) 113 apply (case_tac rv) 114 apply (clarsimp simp: throwError_def) 115 apply clarsimp 116 apply (rule corres_split[OF _ Q]) 117 apply (rule corres_trivial) 118 apply (case_tac rv) 119 apply (clarsimp simp add: lift_def throwError_def) 120 apply (clarsimp simp add: y lift_def returnOk_def throwError_def) 121 apply (wpsimp wp: w P)+ 122 done 123qed 124 125lemma corres_Id: 126 "\<lbrakk> f = g; \<And>rv. r rv rv; nf' \<Longrightarrow> no_fail P' g \<rbrakk> \<Longrightarrow> corres_underlying Id nf nf' r \<top> P' f g" 127 apply (clarsimp simp: corres_underlying_def Ball_def no_fail_def) 128 apply (rule rev_bexI, assumption) 129 apply simp 130 done 131 132lemma select_pick_corres_underlying: 133 "corres_underlying sr nf nf' r P Q (f x) g 134 \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (select S >>= f) g" 135 by (fastforce simp: corres_underlying_def select_def bind_def) 136 137lemma select_pick_corres: 138 "corres_underlying sr nf nf' r P Q (f x) g 139 \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (select S >>= f) g" 140 by (fastforce simp: intro: select_pick_corres_underlying) 141 142lemma select_pick_corresE: 143 "corres_underlying sr nf nf' r P Q (f x) g 144 \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (liftE (select S) >>=E f) g" 145 by (fastforce simp: liftE_bindE intro: select_pick_corres) 146 147lemma corres_modify: 148 assumes rl: 149 "\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> (f s, g s') \<in> sr" 150 shows "corres_underlying sr nf nf' dc P P' (modify f) (modify g)" 151 by (simp add: simpler_modify_def corres_singleton rl) 152 153lemma corres_gets_the: 154 assumes x: "corres_underlying sr nf nf' (r \<circ> the) P P' (gets f) y" 155 shows "corres_underlying sr nf nf' r (P and (\<lambda>s. f s \<noteq> None)) P' (gets_the f) y" 156proof - 157 have z: "corres_underlying sr nf nf' (\<lambda>x y. \<exists>x'. x = Some x' \<and> r x' y) 158 (P and (\<lambda>s. f s \<noteq> None)) P' (gets f) y" 159 apply (subst corres_cong [OF refl refl refl refl]) 160 defer 161 apply (rule corres_guard_imp[OF x], simp+) 162 apply (clarsimp simp: simpler_gets_def) 163 done 164 show ?thesis 165 apply (rule corres_guard_imp) 166 apply (unfold gets_the_def) 167 apply (subst bind_return[symmetric], rule corres_split [OF _ z]) 168 apply (rule corres_trivial, clarsimp simp: assert_opt_def) 169 apply (wp | simp)+ 170 done 171qed 172 173 174lemma corres_u_nofail: 175 "corres_underlying S nf True r P P' f g \<Longrightarrow> (nf \<Longrightarrow> no_fail P f) \<Longrightarrow> 176 no_fail (\<lambda>s'. \<exists>s. (s,s') \<in> S \<and> P s \<and> P' s') g" 177 apply (clarsimp simp add: corres_underlying_def no_fail_def) 178 apply fastforce 179 done 180 181lemma wp_from_corres_u: 182 "\<lbrakk> corres_underlying R nf nf' r G G' f f'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>; nf \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> 183 \<lbrace>\<lambda>s'. \<exists>s. (s,s') \<in> R \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace> f' \<lbrace>\<lambda>rv' s'. \<exists>rv s. (s,s') \<in> R \<and> r rv rv' \<and> Q rv s \<and> Q' rv' s'\<rbrace>" 184 apply (fastforce simp: corres_underlying_def valid_def no_fail_def) 185 done 186 187lemma wp_from_corres_u_unit: 188 "\<lbrakk> corres_underlying R nf nf' r G G' f f'; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>_. Q'\<rbrace>; nf \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> 189 \<lbrace>\<lambda>s'. \<exists>s. (s,s') \<in> R \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace> 190 f' \<lbrace>\<lambda>_ s'. \<exists>s. (s,s') \<in> R \<and> Q s \<and> Q' s'\<rbrace>" 191 apply (fastforce dest: wp_from_corres_u elim: hoare_strengthen_post) 192 done 193 194lemma corres_nofail: 195 "corres_underlying state_relation nf True r P P' f g \<Longrightarrow> (nf \<Longrightarrow> no_fail P f) \<Longrightarrow> 196 no_fail (\<lambda>s'. \<exists>s. (s,s') \<in> state_relation \<and> P s \<and> P' s') g" 197 by (rule corres_u_nofail) 198 199lemma wp_from_corres_unit: 200 "\<lbrakk> corres_underlying state_relation nf nf' r G G' f f'; 201 \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>_. Q'\<rbrace>; nf \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> 202 \<lbrace>\<lambda>s'. \<exists>s. (s,s') \<in> state_relation \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace> 203 f' \<lbrace>\<lambda>_ s'. \<exists>s. (s,s') \<in> state_relation \<and> Q s \<and> Q' s'\<rbrace>" 204 by (auto intro!: wp_from_corres_u_unit) 205 206end 207