1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory LemmaBucket 8imports 9 HaskellLemmaBucket 10 SpecValid_R 11 SubMonadLib 12begin 13 14lemma corres_underlying_trivial: 15 "\<lbrakk> nf' \<Longrightarrow> no_fail P' f \<rbrakk> \<Longrightarrow> corres_underlying Id nf nf' (=) \<top> P' f f" 16 by (auto simp add: corres_underlying_def Id_def no_fail_def) 17 18lemma hoare_spec_gen_asm: 19 "\<lbrakk> F \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P and K F\<rbrace> f \<lbrace>Q\<rbrace>" 20 "\<lbrakk> F \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P and K F\<rbrace> f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 21 unfolding spec_valid_def spec_validE_def validE_def 22 apply (clarsimp simp only: pred_conj_def conj_assoc[symmetric] 23 intro!: hoare_gen_asm[unfolded pred_conj_def])+ 24 done 25 26lemma spec_validE_fail: 27 "s \<turnstile> \<lbrace>P\<rbrace> fail \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 28 by wp+ 29 30lemma mresults_fail: "mresults fail = {}" 31 by (simp add: mresults_def fail_def) 32 33lemma gets_symb_exec_l: 34 "corres_underlying sr nf nf' dc P P' (gets f) (return x)" 35 by (simp add: corres_underlying_def return_def simpler_gets_def split_def) 36 37lemmas mapM_x_wp_inv = mapM_x_wp[where S=UNIV, simplified] 38 39lemma mapM_wp_inv: 40 "(\<And>x. \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>rv. P\<rbrace>" 41 apply (rule valid_return_unit) 42 apply (fold mapM_x_mapM) 43 apply (erule mapM_x_wp_inv) 44 done 45 46lemmas mapM_x_wp' = mapM_x_wp [OF _ subset_refl] 47 48lemma corres_underlying_similar: 49 "\<lbrakk> a = a'; b = b'; nf' \<Longrightarrow> no_fail \<top> (f a b) \<rbrakk> 50 \<Longrightarrow> corres_underlying Id nf nf' dc \<top> \<top> (f a b) (f a' b')" 51 by (simp add: corres_underlying_def no_fail_def, blast) 52 53lemma corres_underlying_gets_pre_lhs: 54 "(\<And>x. corres_underlying S nf nf' r (P x) P' (g x) g') \<Longrightarrow> 55 corres_underlying S nf nf' r (\<lambda>s. P (f s) s) P' (gets f >>= (\<lambda>x. g x)) g'" 56 apply (simp add: simpler_gets_def bind_def split_def corres_underlying_def) 57 apply force 58 done 59 60lemma mapM_x_inv_wp: 61 assumes x: "\<And>s. I s \<Longrightarrow> Q s" 62 assumes y: "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> m x \<lbrace>\<lambda>rv. I\<rbrace>" 63 assumes z: "\<And>s. I s \<Longrightarrow> P s" 64 shows "\<lbrace>I\<rbrace> mapM_x m xs \<lbrace>\<lambda>rv. Q\<rbrace>" 65 apply (rule hoare_post_imp) 66 apply (erule x) 67 apply (rule mapM_x_wp) 68 apply (rule hoare_pre_imp [OF _ y]) 69 apply (erule z) 70 apply assumption 71 apply simp 72 done 73 74 75lemma mapM_x_accumulate_checks': 76 assumes P: "\<And>x. x \<in> set xs' \<Longrightarrow> \<lbrace>\<top>\<rbrace> f x \<lbrace>\<lambda>rv. P x\<rbrace>" 77 assumes P': "\<And>x y. \<lbrakk> x \<in> set xs'; y \<in> set xs' \<rbrakk> 78 \<Longrightarrow> \<lbrace>P y\<rbrace> f x \<lbrace>\<lambda>rv. P y\<rbrace>" 79 shows "set xs \<subseteq> set xs' \<Longrightarrow> 80 \<lbrace>\<top>\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv s. \<forall>x \<in> set xs. P x s\<rbrace>" 81 apply (induct xs) 82 apply (simp add: mapM_x_Nil) 83 apply (simp add: mapM_x_Cons) 84 apply (rule hoare_pre) 85 apply (wp mapM_x_wp'[OF P']) 86 apply blast 87 apply simp 88 apply assumption 89 apply simp 90 apply (rule P) 91 apply simp 92 apply simp 93 done 94 95lemmas mapM_x_accumulate_checks 96 = mapM_x_accumulate_checks'[OF _ _ subset_refl] 97 98(* Other *) 99 100lemma isRight_rel_sum_comb2: 101 "\<lbrakk> (f \<oplus> r) v v'; isRight v' \<rbrakk> 102 \<Longrightarrow> isRight v \<and> r (theRight v) (theRight v')" 103 by (clarsimp simp: isRight_def) 104 105lemma isRight_case_sum: "isRight x \<Longrightarrow> case_sum f g x = g (theRight x)" 106 by (clarsimp simp add: isRight_def) 107 108lemma enumerate_append:"enumerate i (xs @ ys) = enumerate i xs @ enumerate (i + length xs) ys" 109 apply (induct xs arbitrary:ys i) 110 apply clarsimp+ 111 done 112 113lemma enumerate_bound:"(a, b) \<in> set (enumerate n xs) \<Longrightarrow> a < n + length xs" 114 by (metis add.commute in_set_enumerate_eq prod.sel(1)) 115 116lemma enumerate_exceed:"(n + length xs, b) \<notin> set (enumerate n xs)" 117 by (metis enumerate_bound less_not_refl) 118 119lemma all_pair_unwrap:"(\<forall>a. P (fst a) (snd a)) = (\<forall>a b. P a b)" 120 by force 121 122lemma if_fold[simp]:"(if P then Q else if P then R else S) = (if P then Q else S)" 123 by presburger 124 125lemma disjoint_subset_both:"\<lbrakk>A' \<subseteq> A; B' \<subseteq> B; A \<inter> B = {}\<rbrakk> \<Longrightarrow> A' \<inter> B' = {}" 126 by blast 127 128lemma union_split: "\<lbrakk>A \<inter> C = {}; B \<inter> C = {}\<rbrakk> \<Longrightarrow> (A \<union> B) \<inter> C = {}" 129 by (simp add: inf_sup_distrib2) 130 131lemma dom_expand: "dom (\<lambda>x. if P x then Some y else None) = {x. P x}" 132 using if_option_Some by fastforce 133 134lemma range_translate: "(range f = range g) = ((\<forall>x. \<exists>y. f x = g y) \<and> (\<forall>x. \<exists>y. f y = g x))" 135 by (rule iffI, 136 rule conjI, 137 clarsimp, 138 blast, 139 clarsimp, 140 metis f_inv_into_f range_eqI, 141 clarsimp, 142 subst set_eq_subset, 143 rule conjI, 144 clarsimp, 145 rename_tac arg, 146 erule_tac x=arg and P="\<lambda>x. (\<exists>y. f x = g y)" in allE, 147 clarsimp, 148 clarsimp, 149 rename_tac arg, 150 erule_tac x=arg and P="\<lambda>x. (\<exists>y. f y = g x)" in allE, 151 clarsimp, 152 metis range_eqI) 153 154lemma ran_expand: "\<exists>x. P x \<Longrightarrow> ran (\<lambda>x. if P x then Some y else None) = {y}" 155 by (rule subset_antisym, 156 (clarsimp simp:ran_def)+) 157 158lemma map_upd_expand: "f(x \<mapsto> y) = f ++ (\<lambda>z. if z = x then Some y else None)" 159 by (rule ext, rename_tac w, 160 case_tac "w = x", 161 simp, 162 simp add:map_add_def) 163 164lemma map_upd_subI: "\<lbrakk>f \<subseteq>\<^sub>m g; f x = None\<rbrakk> \<Longrightarrow> f \<subseteq>\<^sub>m g(x \<mapsto> y)" 165 by (rule_tac f="\<lambda>i. if i = x then Some y else None" in map_add_le_mapE, 166 simp add:map_le_def, 167 rule ballI, rename_tac a, 168 rule conjI, 169 erule_tac x=x in ballE, 170 clarsimp, 171 erule disjE, 172 clarsimp, 173 clarsimp simp:map_add_def, 174 clarsimp, 175 erule disjE, 176 clarsimp, 177 clarsimp simp:map_add_def, 178 clarsimp simp:map_add_def, 179 erule_tac x=a in ballE, 180 erule disjE, 181 (case_tac "g a"; simp_all), 182 clarsimp+) 183 184lemma all_ext: "\<forall>x. f x = g x \<Longrightarrow> f = g" 185 by presburger 186 187lemma conjI2: "\<lbrakk>B; B \<longrightarrow> A\<rbrakk> \<Longrightarrow> A \<and> B" 188 by auto 189 190(* Trivial lemmas for dealing with messy CNode obligations. *) 191lemma Least2: "\<lbrakk>\<not>P 0; \<not>P 1; P (2::nat)\<rbrakk> \<Longrightarrow> Least P = 2" 192 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 193lemma Least3: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; P (3::nat)\<rbrakk> \<Longrightarrow> Least P = 3" 194 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 195lemma Least4: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; P (4::nat)\<rbrakk> \<Longrightarrow> Least P = 4" 196 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 197lemma Least5: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; P (5::nat)\<rbrakk> \<Longrightarrow> Least P = 5" 198 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 199lemma Least6: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; P (6::nat)\<rbrakk> \<Longrightarrow> Least P = 6" 200 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 201lemma Least7: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; P (7::nat)\<rbrakk> \<Longrightarrow> Least P = 7" 202 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 203lemma Least8: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; P (8::nat)\<rbrakk> \<Longrightarrow> Least P = 8" 204 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 205lemma Least9: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; P (9::nat)\<rbrakk> \<Longrightarrow> Least P = 9" 206 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 207lemma Least10: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; P (10::nat)\<rbrakk> \<Longrightarrow> Least P 208 = 10" 209 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 210lemma Least11: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; P (11::nat)\<rbrakk> \<Longrightarrow> 211 Least P = 11" 212 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 213lemma Least12: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; P 214 (12::nat)\<rbrakk> \<Longrightarrow> Least P = 12" 215 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 216lemma Least13: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; P 217 (13::nat)\<rbrakk> \<Longrightarrow> Least P = 13" 218 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 219lemma Least14: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 220 13; P (14::nat)\<rbrakk> \<Longrightarrow> Least P = 14" 221 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 222lemma Least15: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 223 13; \<not>P 14; P (15::nat)\<rbrakk> \<Longrightarrow> Least P = 15" 224 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 225lemma Least16: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 226 13; \<not>P 14; \<not>P 15; P (16::nat)\<rbrakk> \<Longrightarrow> Least P = 16" 227 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 228lemma Least17: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 229 13; \<not>P 14; \<not>P 15; \<not>P 16; P (17::nat)\<rbrakk> \<Longrightarrow> Least P = 17" 230 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 231lemma Least18: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 232 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; P (18::nat)\<rbrakk> \<Longrightarrow> Least P = 18" 233 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 234lemma Least19: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 235 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; P (19::nat)\<rbrakk> \<Longrightarrow> Least P = 19" 236 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 237lemma Least20: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 238 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; P (20::nat)\<rbrakk> \<Longrightarrow> Least P = 20" 239 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 240lemma Least21: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 241 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; P (21::nat)\<rbrakk> \<Longrightarrow> Least P = 21" 242 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 243lemma Least22: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 244 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; P (22::nat)\<rbrakk> \<Longrightarrow> Least P 245 = 22" 246 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 247lemma Least23: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 248 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; \<not>P 22; P (23::nat)\<rbrakk> \<Longrightarrow> 249 Least P = 23" 250 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 251lemma Least24: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 252 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; \<not>P 22; \<not>P 23; P 253 (24::nat)\<rbrakk> \<Longrightarrow> Least P = 24" 254 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 255lemma Least25: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 256 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; \<not>P 22; \<not>P 23; \<not>P 24; P 257 (25::nat)\<rbrakk> \<Longrightarrow> Least P = 25" 258 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 259lemma Least26: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 260 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; \<not>P 22; \<not>P 23; \<not>P 24; \<not>P 261 25; P (26::nat)\<rbrakk> \<Longrightarrow> Least P = 26" 262 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 263lemma Least27: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 264 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; \<not>P 22; \<not>P 23; \<not>P 24; \<not>P 265 25; \<not>P 26; P (27::nat)\<rbrakk> \<Longrightarrow> Least P = 27" 266 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 267lemma Least28: "\<lbrakk>\<not>P 0; \<not>P 1; \<not>P 2; \<not>P 3; \<not>P 4; \<not>P 5; \<not>P 6; \<not>P 7; \<not>P 8; \<not>P 9; \<not>P 10; \<not>P 11; \<not>P 12; \<not>P 268 13; \<not>P 14; \<not>P 15; \<not>P 16; \<not>P 17; \<not>P 18; \<not>P 19; \<not>P 20; \<not>P 21; \<not>P 22; \<not>P 23; \<not>P 24; \<not>P 269 25; \<not>P 26; \<not>P 27; P (28::nat)\<rbrakk> \<Longrightarrow> Least P = 28" 270 by (simp add: Least_Suc eval_nat_numeral(2) eval_nat_numeral(3)) 271 272lemma map_add_discard: "\<not> cond x \<Longrightarrow> (f ++ (\<lambda>x. if cond x then (g x) else None)) x = f x" 273 by (simp add: map_add_def) 274 275lemma dom_split:"\<lbrakk>\<forall>x \<in> S. \<exists>y. f x = Some y; \<forall>x. x \<notin> S \<longrightarrow> f x = None\<rbrakk> \<Longrightarrow> dom f = S" 276 by (auto simp:dom_def) 277 278lemma map_set_in: "x \<in> f ` S = (\<exists>y\<in>S. f y = x)" 279 by blast 280 281lemma map_length_split: 282 "map (length \<circ> (\<lambda>(a, b). P a b # map (f a b) (Q a b))) xs = map (\<lambda>(a, b). 1 + length (Q a b)) xs" 283 by clarsimp 284 285lemma sum_suc: "(\<Sum>x \<leftarrow> xs. Suc (f x)) = length xs + (\<Sum>x \<leftarrow> xs. f x)" 286 apply (induct xs) 287 by clarsimp+ 288 289lemma sum_suc_pair: "(\<Sum>(a, b) \<leftarrow> xs. Suc (f a b)) = length xs + (\<Sum>(a, b) \<leftarrow> xs. f a b)" 290 apply (induct xs) 291 by clarsimp+ 292 293lemma fold_add_sum: "fold (+) ((map (\<lambda>(a, b). f a b) xs)::nat list) 0 = (\<Sum>(a, b) \<leftarrow> xs. f a b)" 294 apply (subst fold_plus_sum_list_rev) 295 apply (subst sum_list_rev) 296 by clarsimp 297 298lemma set_of_enumerate:"card (set (enumerate n xs)) = length xs" 299 by (metis distinct_card distinct_enumerate length_enumerate) 300 301lemma collapse_fst: "fst ` (\<lambda>x. (f x, g x)) ` s = f ` s" 302 by force 303 304lemma collapse_fst2: "fst ` (\<lambda>(x, y). (f x, g y)) ` s = (\<lambda>x. f (fst x)) ` s" 305 by force 306 307lemma collapse_fst3: "(\<lambda>x. f (fst x)) ` set (enumerate n xs) = f ` set [n..<n + length xs]" 308 by (metis image_image list.set_map map_fst_enumerate) 309 310lemma card_of_dom_bounded: 311 fixes f :: "'a \<Rightarrow> 'b option" 312 assumes "finite (UNIV::'a set)" 313 shows "card (dom f) \<le> CARD('a)" 314 by (simp add: assms card_mono) 315 316lemma third_in: "(a, b, c) \<in> S \<Longrightarrow> c \<in> (snd \<circ> snd) ` S" 317 by (metis (erased, hide_lams) map_set_in image_comp snd_conv) 318 319lemma third_in2: "(a \<in> (snd \<circ> snd) ` (set (enumerate i xs))) = (a \<in> snd ` (set xs))" 320 by (metis map_map map_snd_enumerate set_map) 321 322lemma map_of_enum: "map_of (enumerate n xs) x = Some y \<Longrightarrow> y \<in> set xs" 323 apply (clarsimp) 324 by (metis enumerate_eq_zip in_set_zipE) 325 326lemma map_of_append: 327 "(map_of xs ++ map_of ys) x = (case map_of ys x of None \<Rightarrow> map_of xs x | Some x' \<Rightarrow> Some x')" 328 by (simp add: map_add_def) 329 330lemma map_of_append2: 331 "(map_of xs ++ map_of ys ++ map_of zs) x = 332 (case map_of zs x of None \<Rightarrow> (case map_of ys x of None \<Rightarrow> map_of xs x 333 | Some x' \<Rightarrow> Some x') 334 | Some x' \<Rightarrow> Some x')" 335 by (simp add: map_add_def) 336 337lemma map_of_in_set_map: "map_of (map (\<lambda>(n, y). (f n, y)) xs) x = Some z \<Longrightarrow> z \<in> snd ` set xs" 338 proof - 339 assume "map_of (map (\<lambda>(n, y). (f n, y)) xs) x = Some z" 340 hence "(x, z) \<in> (\<lambda>(uu, y). (f uu, y)) ` set xs" using map_of_SomeD by fastforce 341 thus "z \<in> snd ` set xs" using map_set_in by fastforce 342 qed 343 344lemma pair_in_enum: "(a, b) \<in> set (enumerate x ys) \<Longrightarrow> b \<in> set ys" 345 by (metis enumerate_eq_zip in_set_zip2) 346 347lemma distinct_inj: 348 "inj f \<Longrightarrow> distinct xs = distinct (map f xs)" 349 apply (induct xs) 350 apply simp 351 apply (simp add: inj_image_mem_iff) 352 done 353 354lemma distinct_map_via_ran: "distinct (map fst xs) \<Longrightarrow> ran (map_of xs) = set (map snd xs)" 355 apply (cut_tac xs="map fst xs" and ys="map snd xs" in ran_map_of_zip[symmetric]) 356 apply clarsimp+ 357 by (simp add: ran_distinct) 358 359lemma in_ran_in_set: "x \<in> ran (map_of xs) \<Longrightarrow> x \<in> set (map snd xs)" 360 by (metis (mono_tags, hide_lams) map_set_in map_of_SomeD ranE set_map snd_conv) 361 362lemma in_ran_map_app: "x \<in> ran (xs ++ ys ++ zs) \<Longrightarrow> x \<in> ran xs \<or> x \<in> ran ys \<or> x \<in> ran zs" 363 proof - 364 assume a1: "x \<in> ran (xs ++ ys ++ zs)" 365 obtain bb :: "'a \<Rightarrow> ('b \<Rightarrow> 'a option) \<Rightarrow> 'b" where 366 "\<forall>x0 x1. (\<exists>v2. x1 v2 = Some x0) = (x1 (bb x0 x1) = Some x0)" 367 by moura 368 hence f2: "\<forall>f a. (\<not> (\<exists>b. f b = Some a) \<or> f (bb a f) = Some a) \<and> ((\<exists>b. f b = Some a) \<or> (\<forall>b. f b \<noteq> Some a))" 369 by blast 370 have "\<exists>b. (xs ++ ys ++ zs) b = Some x" 371 using a1 by (simp add: ran_def) 372 hence f3: "(xs ++ ys ++ zs) (bb x (xs ++ ys ++ zs)) = Some x" 373 using f2 by meson 374 { assume "ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x" 375 { assume "ys (bb x (xs ++ ys ++ zs)) \<noteq> Some x \<and> (ys (bb x (xs ++ ys ++ zs)) \<noteq> None \<or> xs (bb x (xs ++ ys ++ zs)) \<noteq> Some x)" 376 hence "\<exists>b. zs b = Some x" 377 using f3 by auto 378 hence ?thesis 379 by (simp add: ran_def) } 380 hence ?thesis 381 using ran_def by fastforce } 382 thus ?thesis 383 using ran_def by fastforce 384 qed 385 386lemma none_some_map: "None \<notin> S \<Longrightarrow> Some x \<in> S = (x \<in> the ` S)" 387 apply (rule iffI) 388 apply force 389 apply (subst in_these_eq[symmetric]) 390 apply (clarsimp simp:Option.these_def) 391 apply (case_tac "\<exists>y. xa = Some y") 392 by clarsimp+ 393 394lemma none_some_map2: "the ` Set.filter (\<lambda>s. \<not> Option.is_none s) (range f) = ran f" 395 apply (rule subset_antisym) 396 apply clarsimp 397 apply (case_tac "f x", simp_all) 398 apply (simp add: ranI) 399 apply clarsimp 400 apply (subst none_some_map[symmetric]) 401 apply clarsimp+ 402 apply (erule ranE) 403 by (metis range_eqI) 404 405lemma prop_map_of_prop:"\<lbrakk>\<forall>z \<in> set xs. P (g z); map_of (map (\<lambda>x. (f x, g x)) xs) y = Some a\<rbrakk> \<Longrightarrow> P a" 406 using map_of_SomeD by fastforce 407 408lemma range_subsetI2: "\<forall>y\<in>A. \<exists>x. f x = y \<Longrightarrow> A \<subseteq> range f" 409 by fast 410 411lemma insert_strip: "x \<noteq> y \<Longrightarrow> (x \<in> insert y S) = (x \<in> S)" 412 by simp 413 414lemma dom_map_add: "dom ys = A \<Longrightarrow> dom (xs ++ ys) = A \<union> dom xs" 415 by simp 416 417lemma set_compre_unwrap: "({x. P x} \<subseteq> S) = (\<forall>x. P x \<longrightarrow> x \<in> S)" 418 by blast 419 420lemma map_add_same: "\<lbrakk>xs = ys; zs = ws\<rbrakk> \<Longrightarrow> xs ++ zs = ys ++ ws" 421 by simp 422 423lemma map_add_find_left: "n k = None \<Longrightarrow> (m ++ n) k = m k" 424 by (simp add:map_add_def) 425 426lemma map_length_split_triple: 427 "map (length \<circ> (\<lambda>(a, b, c). P a b c # map (f a b c) (Q a b c))) xs = 428 map (\<lambda>(a, b, c). 1 + length (Q a b c)) xs" 429 by fastforce 430 431lemma sum_suc_triple: "(\<Sum>(a, b, c)\<leftarrow>xs. Suc (f a b c)) = length xs + (\<Sum>(a, b, c)\<leftarrow>xs. f a b c)" 432 by (induct xs; clarsimp) 433 434lemma sum_enumerate: "(\<Sum>(a, b)\<leftarrow>enumerate n xs. P b) = (\<Sum>b\<leftarrow>xs. P b)" 435 by (induct xs arbitrary:n; clarsimp) 436 437lemma dom_map_fold:"dom (fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) ms) = dom ms \<union> set (map f xs)" 438 by (induct xs arbitrary:f g ms; clarsimp) 439 440lemma list_ran_prop:"map_of (map (\<lambda>x. (f x, g x)) xs) i = Some t \<Longrightarrow> \<exists>x \<in> set xs. g x = t" 441 by (induct xs arbitrary:f g t i; clarsimp split:if_split_asm) 442 443lemma in_set_enumerate_eq2:"(a, b) \<in> set (enumerate n xs) \<Longrightarrow> (b = xs ! (a - n))" 444 by (simp add: in_set_enumerate_eq) 445 446lemma subset_eq_notI: "\<lbrakk>a\<in> B;a\<notin> C\<rbrakk> \<Longrightarrow> \<not> B \<subseteq> C" 447 by auto 448 449lemma nat_divide_less_eq: 450 fixes b :: nat 451 shows "0 < c \<Longrightarrow> (b div c < a) = (b < a * c)" 452 using td_gal_lt by blast 453 454lemma strengthen_imp_same_first_conj: 455 "(b \<and> (a \<longrightarrow> c) \<and> (a' \<longrightarrow> c')) \<Longrightarrow> ((a \<longrightarrow> b \<and> c) \<and> (a' \<longrightarrow> b \<and> c'))" 456 by blast 457 458lemma conj_impD: 459 "a \<and> b \<Longrightarrow> a \<longrightarrow> b" 460 by blast 461 462lemma set_list_mem_nonempty: 463 "x \<in> set xs \<Longrightarrow> xs \<noteq> []" 464 by auto 465 466lemma strenghten_False_imp: 467 "\<not>P \<Longrightarrow> P \<longrightarrow> Q" 468 by blast 469 470lemma foldl_fun_or_alt: 471 "foldl (\<lambda>x y. x \<or> f y) b ls = foldl (\<or>) b (map f ls)" 472 apply (induct ls) 473 apply clarsimp 474 apply clarsimp 475 by (simp add: foldl_map) 476 477lemma sorted_imp_sorted_filter: 478 "sorted xs \<Longrightarrow> sorted (filter P xs)" 479 by (metis filter_sort sorted_sort sorted_sort_id) 480 481lemma sorted_list_of_set_already_sorted: 482 "\<lbrakk> distinct xs; sorted xs \<rbrakk> \<Longrightarrow> sorted_list_of_set (set xs) = xs" 483 by (simp add: sorted_list_of_set_sort_remdups distinct_remdups_id sorted_sort_id) 484 485end 486