1(* 2 * 3 * Copyright 2017, Data61, CSIRO 4 * 5 * This software may be distributed and modified according to the terms of 6 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 7 * See "LICENSE_BSD2.txt" for details. 8 * 9 * @TAG(DATA61_BSD) 10 *) 11 12 13theory CorresK_Lemmas 14imports 15 "Lib.Corres_Method" 16 "ExecSpec.Syscall_H" 17 "ASpec.Syscall_A" 18begin 19 20lemma corres_throwError_str [corres_concrete_rER]: 21 "corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throw b)" 22 "corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throwError b)" 23 by (simp add: corres_underlyingK_def)+ 24 25lemma corresK_use_guard: 26 "(F \<Longrightarrow> corres_underlyingK sr nf nf' F r Q Q' f g) \<Longrightarrow> corres_underlyingK sr nf nf' F r Q Q' f g" 27 by (simp add: corres_underlyingK_def) 28 29lemma mapME_x_corresK_inv: 30 assumes x: "\<And>x. corres_underlyingK sr nf nf' (F x) (f \<oplus> dc) (P x) (P' x) (m x) (m' x)" 31 assumes y: "\<And>x P. \<lbrace>P\<rbrace> m x \<lbrace>\<lambda>x. P\<rbrace>,-" "\<And>x P'. \<lbrace>P'\<rbrace> m' x \<lbrace>\<lambda>x. P'\<rbrace>,-" 32 shows "corres_underlyingK sr nf nf' (xs = ys \<and> (\<forall>x \<in> set xs. F x)) (f \<oplus> dc) (\<lambda>s. \<forall>x \<in> set xs. P x s) (\<lambda>s. \<forall>y \<in> set ys. P' y s) 33 (mapME_x m xs) (mapME_x m' ys)" 34 apply (rule corresK_use_guard, elim conjE) 35 subgoal premises prems 36 unfolding \<open>xs = ys\<close> 37 proof (induct ys) 38 case Nil 39 show ?case 40 by (simp add: mapME_x_def sequenceE_x_def returnOk_def corres_underlyingK_def) 41 next 42 case (Cons z zs) 43 from Cons have IH: 44 "corres_underlyingK sr nf nf' (\<forall>x\<in>set zs. F x) (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set zs. P x s) (\<lambda>s. \<forall>y\<in>set zs. P' y s) 45 (mapME_x m zs) (mapME_x m' zs)" by (auto simp add: dc_def) 46 show ?case 47 apply (simp add: mapME_x_def sequenceE_x_def) 48 apply (fold mapME_x_def sequenceE_x_def dc_def) 49 apply (corressimp corresK: x IH wp: y) 50 done 51 qed 52 done 53 54lemma corresK_mapM: 55 assumes S: "set (zip xs ys) \<subseteq> S" 56 assumes z: "\<And>x y. corres_protect ((x, y) \<in> S) \<Longrightarrow> corres_underlyingK R nf nf' (F x y) r' P P' (f x) (f' y)" 57 assumes w: "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>" 58 "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>" 59 shows "corres_underlyingK R nf nf' 60 ((length xs = length ys) \<and> 61 (r [] []) \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and> 62 (\<forall>(x,y)\<in>S. F x y)) r P P' (mapM f xs) (mapM f' ys)" 63 unfolding corres_underlyingK_def 64 apply (rule impI, rule corres_mapM[of r r' S]) 65 using assms unfolding corres_underlyingK_def by (auto simp: corres_protect_def) 66 67definition 68 "F_all2 F xs ys = 69 (\<exists>F'. 70 (\<forall>x y xs ys. 71 (F' x y \<longrightarrow> list_all2 F' xs ys \<longrightarrow> F x y xs ys)) \<and> list_all2 F' xs ys)" 72 73 74lemma F_all2_pointwise[simp]: 75 "F_all2 (\<lambda>x y _ _. F x y) xs ys = list_all2 F xs ys" 76 apply (rule iffI) 77 apply (clarsimp simp: F_all2_def) 78 subgoal for F' 79 apply (rule list_all2_induct_suffixeq[where Q=F']; simp) 80 apply (drule_tac x=x in spec) 81 apply (drule_tac x=y in spec) 82 apply fastforce 83 done 84 apply (clarsimp simp:F_all2_def) 85 apply (rule_tac x=F in exI) 86 apply clarsimp 87 done 88 89lemma F_all2_list: 90 "F xs ys \<Longrightarrow> \<exists>F'. (\<forall>xs ys. (F xs ys = list_all2 F' xs ys)) \<Longrightarrow> F_all2 (\<lambda>_ _ xs ys. F xs ys) xs ys" 91 apply (clarsimp simp: F_all2_def) 92 apply (rule_tac x=F' in exI) 93 by auto 94 95lemma list_all2_conjD: 96 "list_all2 (\<lambda>x y. Q x y \<and> P x y) xs ys \<Longrightarrow> list_all2 Q xs ys \<and> list_all2 P xs ys" 97 by (induct rule: list_all2_induct; simp) 98 99 100lemma 101 list_all2_to_list_all: 102 "list_all2 P xs xs = list_all (\<lambda>x. P x x) xs" 103 by (induct xs;simp) 104 105lemma list_all_mem_subset: 106 "list_all (\<lambda>y. y \<in> set xs) ys = (set ys \<subseteq> set xs)" 107 by (induct ys; simp) 108 109lemma F_all2_eq: 110 "(\<And>x xs'. x \<in> set xs \<Longrightarrow> set xs' \<subseteq> set xs \<Longrightarrow> F x x xs' xs') \<Longrightarrow> F_all2 F xs xs" 111 apply (simp add: F_all2_def) 112 apply (rule_tac x="\<lambda>x y. x \<in> set xs \<and> x = y" in exI) 113 apply (intro conjI impI allI) 114 apply (drule list_all2_conjD) 115 apply (simp add: list.rel_eq) 116 apply clarsimp 117 apply (simp add: list_all2_to_list_all list_all_mem_subset) 118 apply (rule list.rel_refl_strong;simp) 119 done 120 121lemma F_all2_conjI: 122 "F_all2 F xs ys \<Longrightarrow> F_all2 F' xs ys \<Longrightarrow> 123 F_all2 (\<lambda>x y xs ys. F x y xs ys \<and> F' x y xs ys) xs ys" 124 apply (clarsimp simp: F_all2_def) 125 apply (rule_tac x="\<lambda>x y. F'a x y \<and> F'aa x y" in exI) 126 by (auto dest: list_all2_conjD intro: list_all2_conj) 127 128lemma corresK_mapM_list_all2: 129 assumes x: "\<And>x y xs ys. corres_underlyingK sr nf nf' (F x y xs ys) r' (I (x#xs)) (I' (y#ys)) (f x) (f' y)" 130 assumes "\<And>x y xs. \<lbrakk> S x y; suffix (x#xs) as \<rbrakk> \<Longrightarrow> \<lbrace> I (x#xs) \<rbrace> f x \<lbrace> \<lambda>rv. I xs \<rbrace>" 131 assumes "\<And>x y ys. \<lbrakk> S x y; suffix (y#ys) cs \<rbrakk> \<Longrightarrow> \<lbrace> I' (y#ys) \<rbrace> f' y \<lbrace> \<lambda>rv. I' ys \<rbrace>" 132 shows "corres_underlyingK sr nf nf' 133 (r [] [] \<and> (\<forall> x y xs ys. r' x y \<longrightarrow> r xs ys \<longrightarrow> r (x # xs) (y # ys)) \<and> 134 list_all2 S as cs \<and> F_all2 F as cs) 135 r (I as) (I' cs) (mapM f as) (mapM f' cs)" 136 unfolding corres_underlyingK_def 137 apply (clarsimp simp: F_all2_def) 138 subgoal for F' 139 apply (rule corres_mapM_list_all2[of r r' "\<lambda>x y. S x y \<and> F' x y"]; (rule assms | assumption | clarsimp)?) 140 apply (rule x[THEN corresK_unlift]) 141 apply (drule list_all2_conjD) 142 apply (clarsimp simp: assms | assumption)+ 143 apply (rule list_all2_conj; simp) 144 done 145 done 146 147lemma corresK_discard_rv: 148 assumes A[corresK]: "corres_underlyingK sr nf nf' F r' P P' a c" 149 shows "corres_underlyingK sr nf nf' F dc P P' (do x \<leftarrow> a; return () od) (do x \<leftarrow> c; return () od)" 150 by corressimp 151 152lemma corresK_mapM_mapM_x: 153 assumes "corres_underlyingK sr nf nf' F r' P P' (mapM f as) (mapM f' cs)" 154 shows "corres_underlyingK sr nf nf' F dc P P' (mapM_x f as) (mapM_x f' cs)" 155 unfolding mapM_x_mapM by (rule corresK_discard_rv, rule assms) 156 157lemmas corresK_mapM_x_list_all2 158 = corresK_mapM_list_all2[where r'=dc, 159 THEN corresK_mapM_mapM_x[where r'=dc], 160 simplified] 161lemmas corresK_mapM_x 162 = corresK_mapM[where r'=dc, 163 THEN corresK_mapM_mapM_x[where r'=dc], 164 simplified] 165 166lemma corresK_subst_both: "g' = f' \<Longrightarrow> g = f \<Longrightarrow> 167 corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow> 168 corres_underlyingK sr nf nf' F r P P' g g'" by simp 169 170lemma if_fun_true: "(if A then B else (\<lambda>_. True)) = (\<lambda>s. (A \<longrightarrow> B s))" by simp 171 172lemmas corresK_whenE [corres_splits] = 173 corresK_if[THEN 174 corresK_subst_both[OF whenE_def[THEN meta_eq_to_obj_eq] whenE_def[THEN meta_eq_to_obj_eq]], 175 OF _ corresK_returnOk[where r="f \<oplus> dc" for f], simplified, simplified if_fun_true] 176 177lemmas corresK_head_splits[corres_splits] = 178 corresK_split[where d="return", simplified] 179 corresK_splitE[where d="returnOk", simplified] 180 corresK_split[where b="return", simplified] 181 corresK_splitE[where b="returnOk", simplified] 182 183lemmas corresK_modify = 184 corres_modify[atomized, @corresK_convert] 185 186lemmas corresK_modifyT = corresK_modify[where P=\<top> and P'=\<top>, simplified] 187 188lemma corresK_Id: 189 "(nf' \<Longrightarrow> no_fail P' g) \<Longrightarrow> 190 corres_underlyingK Id nf nf' (f = g \<and> (\<forall>rv. r rv rv)) r (\<lambda>_. True) P' f g" 191 apply (rule corresK_assume_guard) 192 apply (rule corres_Id;simp) 193 done 194 195lemmas [corresK] = 196 corresK_Id[where nf'=False and r="(=)",simplified] 197 corresK_Id[where nf'=False,simplified] 198 corresK_Id[where nf'=True and r="(=)", simplified] 199 corresK_Id[where nf'=True, simplified] 200 201lemma corresK_unit_rv_eq_any[corres_concrete_r]: 202 "corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow> 203 corres_underlyingK sr nf nf' F 204 (\<lambda>(x :: unit) (y :: unit). x = y) P P' f f'" 205 apply (clarsimp simp add: corres_underlyingK_def) 206 apply (erule corres_rel_imp) 207 apply simp 208 done 209 210lemma corresK_unit_rv_dc_any[corres_concrete_r]: 211 "corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow> 212 corres_underlyingK sr nf nf' F 213 (\<lambda>(x :: unit) (y :: unit). dc x y) P P' f f'" 214 apply (clarsimp simp add: corres_underlyingK_def) 215 apply (erule corres_rel_imp) 216 apply simp 217 done 218 219end 220