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