1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory HaskellLemmaBucket 8imports 9 HaskellLib_H 10 NonDetMonadLemmaBucket 11begin 12 13lemma map_bits_to_bl: 14 "map ((!!) x) [0..<size x] = reverse (to_bl x)" 15 by (simp add: map_bits_rev_to_bl) 16 17lemma not_orList_is_replicate: 18 "\<not> orList ls \<Longrightarrow> ls = replicate (length ls) False" 19proof (induct ls rule: rev_induct) 20 case Nil thus ?case unfolding orList_def by simp 21next 22 case (snoc l ls) 23 24 from snoc.prems have ol: "\<not> orList ls" and nl: "\<not> l" unfolding orList_def by auto 25 have "ls = replicate (length ls) False" by (rule snoc.hyps [OF ol]) 26 thus ?case 27 by (rule ssubst) (simp add: nl replicate_app_Cons_same [where xs = "[]", simplified]) 28qed 29 30lemma andList_Cons: 31 assumes al: "andList $ map P (y # ys)" 32 shows "P y" 33 using al unfolding andList_def 34 by simp (induct rule: rev_induct, simp+) 35 36lemma andList_mapE: 37 assumes al: "andList $ map P xs" 38 and xv: "x \<in> set xs" 39 shows "P x" 40 using al xv 41proof (induct xs arbitrary: x rule: rev_induct) 42 case Nil thus ?case by simp 43next 44 case (snoc y ys) 45 46 show ?case 47 proof (cases "x = y") 48 case True 49 with snoc.prems show ?thesis by (simp add: andList_def) 50 next 51 case False 52 with snoc.prems show ?thesis 53 by (auto simp: andList_def intro!: snoc.hyps) 54 qed 55qed 56 57lemma andList_to_aligned: 58 assumes al: "andList $ map (\<lambda>x. x && mask pageBits = 0) xs" 59 and xv: "x \<in> set xs" 60 shows "is_aligned x pageBits" 61proof (subst is_aligned_mask) 62 from al show "x && mask pageBits = 0" by (rule andList_mapE) fact 63qed 64 65(* minimum/maximum *) 66 67lemma maximum_ge: "x \<in> set b \<Longrightarrow> x \<le> maximum b" 68 unfolding maximum_def by (auto intro: Max_ge) 69 70lemma less_minimum_not_in: 71 "\<lbrakk> ls \<noteq> []; x < minimum ls \<rbrakk> \<Longrightarrow> x \<notin> set ls" 72 unfolding minimum_def by auto 73 74lemma minimum_le_member: 75 "\<lbrakk> x \<in> set ls; ls \<noteq> []\<rbrakk> \<Longrightarrow> minimum ls \<le> x" 76 unfolding minimum_def 77 apply (rule Min_le) 78 apply simp 79 apply simp 80 done 81 82lemma minimum_map_distrib: 83 fixes f :: "('a :: linorder) \<Rightarrow> 'a" and ls :: "'a list" 84 assumes minf: "\<And>x y. \<lbrakk>x \<in> set ls; y \<in> set ls\<rbrakk> \<Longrightarrow> min (f x) (f y) = f (min x y)" 85 and lsn: "ls \<noteq> []" 86 shows "minimum (map f ls) = f (minimum ls)" 87 unfolding minimum_def 88 apply simp 89 apply (rule Min_image_distrib) 90 apply (erule (1) minf) 91 apply simp 92 apply (simp add: lsn) 93 done 94 95lemma minimum_enum_upto: 96 fixes x :: "'a::len word" 97 assumes le: "x \<le> y" 98 shows "minimum [x .e. y] = x" 99 unfolding minimum_def using le by (auto intro!: MinI) 100 101lemma break_subsetsD: 102 "break f xs = (ys, zs) \<Longrightarrow> set ys \<subseteq> set xs \<and> set zs \<subseteq> set xs" 103 apply (induct xs arbitrary: ys zs) 104 apply simp 105 apply (case_tac "break f xs") 106 apply (elim meta_allE, drule(1) meta_mp) 107 apply (fastforce simp: split_def split: if_split_asm) 108 done 109 110lemma distinct_prop_breakD: 111 "\<lbrakk> distinct_prop P xs; break f xs = (ys, zs) \<rbrakk> 112 \<Longrightarrow> \<forall>y \<in> set ys. \<forall>z \<in> set zs. P y z" 113 apply (induct xs arbitrary: ys zs) 114 apply simp 115 apply (simp add: split_def split: if_split_asm) 116 apply (case_tac "break f xs") 117 apply (elim meta_allE, drule(1) meta_mp) 118 apply (frule break_subsetsD) 119 apply fastforce 120 done 121 122lemma stateAssert_wp: 123 "\<lbrace>\<lambda>s. P s \<longrightarrow> Q () s\<rbrace> stateAssert P e \<lbrace>Q\<rbrace>" 124 by (clarsimp simp: stateAssert_def) wp 125 126lemma haskell_assert_wp: 127 "\<lbrace>\<lambda>s. Q \<longrightarrow> P s\<rbrace> haskell_assert Q xs \<lbrace>\<lambda>_. P\<rbrace>" 128 by simp wp 129 130lemma init_append_last: 131 "xs \<noteq> [] \<Longrightarrow> init xs @ [last xs] = xs" 132 apply (induct xs rule: rev_induct) 133 apply simp 134 apply (simp add: init_def) 135 done 136 137lemma init_Snoc[simp]: 138 "init (xs @ [x]) = xs" 139 by (induct xs) (auto simp: init_def) 140 141lemma init_upto_enum_upt[simp]: 142 "init [0.e.n] = [0..<n]" 143 by (induct n) (auto simp: init_def) 144 145lemma no_fail_stateAssert: 146 "no_fail P (stateAssert P xs)" 147 apply (simp add: stateAssert_def) 148 apply (rule no_fail_pre, wp no_fail_bind) 149 apply simp 150 done 151 152lemma empty_fail_stateAssert: 153 "empty_fail (stateAssert P s)" 154 by (simp add: stateAssert_def assert_def empty_fail_get) 155 156lemma haskell_fail_wp: 157 "\<lbrace>\<top>\<rbrace> haskell_fail x \<lbrace>P\<rbrace>" 158 by simp 159 160lemma no_fail_haskell_fail [simp, wp]: 161 "no_fail \<bottom> (haskell_fail xs)" 162 by simp 163 164lemma in_assocs_is_fun: 165 "(x \<in> set (assocs f)) = (f (fst x) = snd x)" 166 by (cases x) (auto simp add: assocs_def) 167 168lemma fun_is_in_assocs: 169 "(f x = y) = ((x,y) \<in> set (assocs f))" 170 by (simp add: in_assocs_is_fun) 171 172lemma empty_set_is_null: 173 "(set xs = {}) = null xs" 174 by (clarsimp simp: null_def) 175 176lemma assert_into_when: 177 "(assert P) = (when (\<not> P) (haskell_fail []))" 178 by (simp add: assert_def when_def) 179 180lemma const_apply: 181 "const x y = x" 182 by (simp add: const_def) 183 184lemma const_None_empty: 185 "const None = Map.empty" 186 by (rule ext, simp add: const_apply) 187 188lemma headM_tailM_Cons: 189 "headM (x # xs) = return x" 190 "tailM (x # xs) = return xs" 191 by (simp add: headM_def tailM_def)+ 192 193lemma replicateM_mapM: 194 "replicateM n f = mapM (\<lambda>x. f) (replicate n ())" 195 by (simp add: replicateM_def mapM_def) 196 197lemma orList_False: 198 "(\<not> orList bs) = (set bs \<subseteq> {False})" 199 apply (induct bs) 200 apply (simp_all add: orList_def foldl_True) 201 apply (case_tac a) 202 apply (simp_all add: orList_def foldl_True) 203 done 204 205lemma Cons_eq_tails: 206 "((xs # xxs) = tails ys) = (ys = xs \<and> xxs = tl (tails ys))" 207 by (case_tac ys, auto) 208 209lemma findM_on_outcome': 210 assumes x: "\<And>x xs. \<lbrace>\<lambda>s. Q None s \<and> x \<in> fn s \<and> set xs \<subseteq> fn s\<rbrace> f x 211 \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> set xs \<subseteq> fn s)\<rbrace>" 212 shows "\<lbrace>\<lambda>s. Q None s \<and> set xs \<subseteq> fn s\<rbrace> findM f xs \<lbrace>Q\<rbrace>" 213 apply (induct xs) 214 apply (simp, wp) 215 apply (simp, wp) 216 apply (rule x) 217 apply simp 218 done 219 220 221lemma findM_on_outcome: 222 assumes x: "\<And>x ys. x \<in> set xs \<Longrightarrow> \<lbrace>Q None and I\<rbrace> f x \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> I s)\<rbrace>" 223 shows "\<lbrace>Q None and I\<rbrace> findM f xs \<lbrace>Q\<rbrace>" 224 apply (rule hoare_vcg_precond_imp) 225 apply (rule findM_on_outcome' [where fn="\<lambda>s. if I s then set xs else {}"]) 226 apply (case_tac "x \<notin> set xs") 227 apply simp 228 apply (simp cong: rev_conj_cong) 229 apply (case_tac "\<not> set xsa \<subseteq> set xs") 230 apply simp 231 apply simp 232 apply (rule hoare_vcg_precond_imp) 233 apply (rule hoare_post_imp [OF _ x]) 234 apply clarsimp 235 apply assumption 236 apply simp 237 apply simp 238 done 239 240lemma in_set_tailsD: "xs \<in> set (tails ys) \<Longrightarrow> set xs \<subseteq> set ys" 241 apply (induct ys) 242 apply simp 243 apply simp 244 apply (erule disjE) 245 apply simp 246 apply simp 247 apply blast 248 done 249 250lemma notin_set_tails_set: 251 "x \<notin> set xs \<Longrightarrow> \<forall>xs' \<in> set (tails xs). \<forall>x' \<in> set xs'. x \<noteq> x'" 252 by (fastforce dest!: in_set_tailsD) 253 254lemma set_tails_set: "(set (tails v) \<subseteq> {x. set x \<subseteq> S}) = (set v \<subseteq> S)" 255 apply (induct v, simp_all) 256 done 257 258lemma filter_assocs_Cons: 259 fixes v :: "('a :: len) word" shows 260 "\<lbrakk> f (v, g v); \<forall>x < v. \<not> f (x, g x) \<rbrakk> \<Longrightarrow> 261 filter f (assocs g) = (v, g v) # tl (filter f (assocs g))" 262 apply (simp add: assocs_def) 263 apply (cut_tac v=v in enum_word_div) 264 apply clarsimp 265 apply (subst map_cong [OF _ refl], assumption)+ 266 apply (simp(no_asm)) 267 apply simp 268 done 269 270lemma snd_stateAssert_after: 271 "\<not> snd ((do _ \<leftarrow> f; stateAssert R vs od) s) \<Longrightarrow> 272 \<not>snd (f s) \<and> (\<forall>(rv, s') \<in> fst (f s). R s')" 273 apply (clarsimp simp: bind_def stateAssert_def get_def assert_def 274 return_def fail_def split_def split: if_split_asm) 275 done 276 277lemma oblivious_stateAssert [simp]: 278 "oblivious f (stateAssert g xs) = (\<forall>s. g (f s) = g s)" 279 apply (simp add: oblivious_def stateAssert_def exec_get 280 assert_def return_def fail_def split: if_split) 281 apply auto 282 done 283 284lemma stateAssert_def2: 285 "stateAssert f xs = do v \<leftarrow> gets f; if v then return () else fail od" 286 by (simp add: stateAssert_def gets_def assert_def) 287 288lemma findM_is_mapME: 289 "(findM f xs >>= g) 290 = liftM (\<lambda>_. ()) 291 (doE ys \<leftarrow> mapME_x (\<lambda>x. do v \<leftarrow> f x; 292 if v then do g (Some x); throwError () od 293 else returnOk () od) xs; 294 liftE (g None) odE)" 295 apply (induct xs) 296 apply (simp add: mapME_x_def sequenceE_x_def liftM_def returnOk_bind) 297 apply (simp add: liftE_def) 298 apply (simp add: mapME_x_Cons bindE_assoc liftE_bindE[symmetric] 299 liftM_def cong: if_cong) 300 apply (simp add: liftE_bindE bind_assoc) 301 apply (rule bind_cong[OF refl]) 302 apply (simp add: bindE_assoc split: if_split) 303 apply (simp add: liftE_bindE bind_assoc throwError_bind) 304 done 305 306 307(* FIXME word_eqI: move up *) 308add_try_method word_eqI_solve 309 310end 311