1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* 8 Miscellaneous library definitions and lemmas. 9*) 10 11chapter "Library" 12 13theory Lib 14imports 15 Value_Abbreviation 16 Match_Abbreviation 17 Try_Methods 18 Extract_Conjunct 19 ML_Goal 20 Eval_Bool 21 NICTATools 22 "HOL-Library.Prefix_Order" 23 "HOL-Word.Word" 24begin 25 26(* FIXME: eliminate *) 27abbreviation (input) 28 split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" 29where 30 "split == case_prod" 31 32(* FIXME: eliminate *) 33lemma hd_map_simp: 34 "b \<noteq> [] \<Longrightarrow> hd (map a b) = a (hd b)" 35 by (rule hd_map) 36 37lemma tl_map_simp: 38 "tl (map a b) = map a (tl b)" 39 by (induct b,auto) 40 41(* FIXME: could be added to Set.thy *) 42lemma Collect_eq: 43 "{x. P x} = {x. Q x} \<longleftrightarrow> (\<forall>x. P x = Q x)" 44 by (rule iffI) auto 45 46(* FIXME: move next to HOL.iff_allI *) 47lemma iff_impI: "\<lbrakk>P \<Longrightarrow> Q = R\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) = (P \<longrightarrow> R)" by blast 48 49(* Long ago, I, fun_app, the verification master of darkness, unleashed an unspeakable evil 50upon the world. But a foolish proof engineer wielding an input abbreviation stepped forth 51to oppose me. Before the final blow was struck, I tore open a hole in a number of refinement 52proofs, and flung him into a broken proof state, where my evil is law. *) 53 54definition 55 fun_app :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" (infixr "$" 10) where 56 "f $ x \<equiv> f x" 57 58declare fun_app_def [iff] 59 60lemma fun_app_cong[fundef_cong]: 61 "\<lbrakk> f x = f' x' \<rbrakk> \<Longrightarrow> (f $ x) = (f' $ x')" 62 by simp 63 64lemma fun_app_apply_cong[fundef_cong]: 65 "f x y = f' x' y' \<Longrightarrow> (f $ x) y = (f' $ x') y'" 66 by simp 67 68lemma if_apply_cong[fundef_cong]: 69 "\<lbrakk> P = P'; x = x'; P' \<Longrightarrow> f x' = f' x'; \<not> P' \<Longrightarrow> g x' = g' x' \<rbrakk> 70 \<Longrightarrow> (if P then f else g) x = (if P' then f' else g') x'" 71 by simp 72 73lemma case_prod_apply_cong[fundef_cong]: 74 "\<lbrakk> f (fst p) (snd p) s = f' (fst p') (snd p') s' \<rbrakk> \<Longrightarrow> case_prod f p s = case_prod f' p' s'" 75 by (simp add: split_def) 76 77lemma prod_injects: 78 "(x,y) = p \<Longrightarrow> x = fst p \<and> y = snd p" 79 "p = (x,y) \<Longrightarrow> x = fst p \<and> y = snd p" 80 by auto 81 82definition 83 pred_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixl "and" 35) 84where 85 "pred_conj P Q \<equiv> \<lambda>x. P x \<and> Q x" 86 87definition 88 pred_disj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixl "or" 30) 89where 90 "pred_disj P Q \<equiv> \<lambda>x. P x \<or> Q x" 91 92definition 93 pred_neg :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" ("not _" [40] 40) 94where 95 "pred_neg P \<equiv> \<lambda>x. \<not> P x" 96 97definition "K \<equiv> \<lambda>x y. x" 98 99definition 100 zipWith :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where 101 "zipWith f xs ys \<equiv> map (case_prod f) (zip xs ys)" 102 103primrec 104 delete :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" 105where 106 "delete y [] = []" 107| "delete y (x#xs) = (if y=x then xs else x # delete y xs)" 108 109definition 110 "swp f \<equiv> \<lambda>x y. f y x" 111 112lemma swp_apply[simp]: "swp f y x = f x y" 113 by (simp add: swp_def) 114 115primrec (nonexhaustive) 116 theRight :: "'a + 'b \<Rightarrow> 'b" where 117 "theRight (Inr x) = x" 118 119primrec (nonexhaustive) 120 theLeft :: "'a + 'b \<Rightarrow> 'a" where 121 "theLeft (Inl x) = x" 122 123definition 124 "isLeft x \<equiv> (\<exists>y. x = Inl y)" 125 126definition 127 "isRight x \<equiv> (\<exists>y. x = Inr y)" 128 129definition 130 "const x \<equiv> \<lambda>y. x" 131 132primrec 133 opt_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool" 134where 135 "opt_rel f None y = (y = None)" 136| "opt_rel f (Some x) y = (\<exists>y'. y = Some y' \<and> f x y')" 137 138 139lemma opt_rel_None_rhs[simp]: 140 "opt_rel f x None = (x = None)" 141 by (cases x, simp_all) 142 143lemma opt_rel_Some_rhs[simp]: 144 "opt_rel f x (Some y) = (\<exists>x'. x = Some x' \<and> f x' y)" 145 by (cases x, simp_all) 146 147lemma tranclD2: 148 "(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R" 149 by (erule tranclE) auto 150 151lemma linorder_min_same1 [simp]: 152 "(min y x = y) = (y \<le> (x::'a::linorder))" 153 by (auto simp: min_def linorder_not_less) 154 155lemma linorder_min_same2 [simp]: 156 "(min x y = y) = (y \<le> (x::'a::linorder))" 157 by (auto simp: min_def linorder_not_le) 158 159text \<open>A combinator for pairing up well-formed relations. 160 The divisor function splits the population in halves, 161 with the True half greater than the False half, and 162 the supplied relations control the order within the halves.\<close> 163 164definition 165 wf_sum :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" 166where 167 "wf_sum divisor r r' \<equiv> 168 ({(x, y). \<not> divisor x \<and> \<not> divisor y} \<inter> r') 169 \<union> {(x, y). \<not> divisor x \<and> divisor y} 170 \<union> ({(x, y). divisor x \<and> divisor y} \<inter> r)" 171 172lemma wf_sum_wf: 173 "\<lbrakk> wf r; wf r' \<rbrakk> \<Longrightarrow> wf (wf_sum divisor r r')" 174 apply (simp add: wf_sum_def) 175 apply (rule wf_Un)+ 176 apply (erule wf_Int2) 177 apply (rule wf_subset 178 [where r="measure (\<lambda>x. If (divisor x) 1 0)"]) 179 apply simp 180 apply clarsimp 181 apply blast 182 apply (erule wf_Int2) 183 apply blast 184 done 185 186abbreviation(input) 187 "option_map == map_option" 188 189lemmas option_map_def = map_option_case 190 191lemma False_implies_equals [simp]: 192 "((False \<Longrightarrow> P) \<Longrightarrow> PROP Q) \<equiv> PROP Q" 193 apply (rule equal_intr_rule) 194 apply (erule meta_mp) 195 apply simp 196 apply simp 197 done 198 199lemma split_paired_Ball: 200 "(\<forall>x \<in> A. P x) = (\<forall>x y. (x,y) \<in> A \<longrightarrow> P (x,y))" 201 by auto 202 203lemma split_paired_Bex: 204 "(\<exists>x \<in> A. P x) = (\<exists>x y. (x,y) \<in> A \<and> P (x,y))" 205 by auto 206 207lemma delete_remove1: 208 "delete x xs = remove1 x xs" 209 by (induct xs, auto) 210 211lemma ignore_if: 212 "(y and z) s \<Longrightarrow> (if x then y else z) s" 213 by (clarsimp simp: pred_conj_def) 214 215lemma zipWith_Nil2 : 216 "zipWith f xs [] = []" 217 unfolding zipWith_def by simp 218 219lemma isRight_right_map: 220 "isRight (case_sum Inl (Inr o f) v) = isRight v" 221 by (simp add: isRight_def split: sum.split) 222 223lemma zipWith_nth: 224 "\<lbrakk> n < min (length xs) (length ys) \<rbrakk> \<Longrightarrow> zipWith f xs ys ! n = f (xs ! n) (ys ! n)" 225 unfolding zipWith_def by simp 226 227lemma length_zipWith [simp]: 228 "length (zipWith f xs ys) = min (length xs) (length ys)" 229 unfolding zipWith_def by simp 230 231 232lemma first_in_uptoD: 233 "a \<le> b \<Longrightarrow> (a::'a::order) \<in> {a..b}" 234 by simp 235 236lemma construct_singleton: 237 "\<lbrakk> S \<noteq> {}; \<forall>s\<in>S. \<forall>s'. s \<noteq> s' \<longrightarrow> s' \<notin> S \<rbrakk> \<Longrightarrow> \<exists>x. S = {x}" 238 by blast 239 240lemmas insort_com = insort_left_comm 241 242lemma bleeding_obvious: 243 "(P \<Longrightarrow> True) \<equiv> (Trueprop True)" 244 by (rule, simp_all) 245 246lemma Some_helper: 247 "x = Some y \<Longrightarrow> x \<noteq> None" 248 by simp 249 250lemma in_empty_interE: 251 "\<lbrakk> A \<inter> B = {}; x \<in> A; x \<in> B \<rbrakk> \<Longrightarrow> False" 252 by blast 253 254lemma None_upd_eq: 255 "g x = None \<Longrightarrow> g(x := None) = g" 256 by (rule ext) simp 257 258lemma exx [iff]: "\<exists>x. x" by blast 259lemma ExNot [iff]: "Ex Not" by blast 260 261lemma cases_simp2 [simp]: 262 "((\<not> P \<longrightarrow> Q) \<and> (P \<longrightarrow> Q)) = Q" 263 by blast 264 265lemma a_imp_b_imp_b: 266 "((a \<longrightarrow> b) \<longrightarrow> b) = (a \<or> b)" 267 by blast 268 269lemma length_neq: 270 "length as \<noteq> length bs \<Longrightarrow> as \<noteq> bs" by auto 271 272lemma take_neq_length: 273 "\<lbrakk> x \<noteq> y; x \<le> length as; y \<le> length bs\<rbrakk> \<Longrightarrow> take x as \<noteq> take y bs" 274 by (rule length_neq, simp) 275 276lemma eq_concat_lenD: 277 "xs = ys @ zs \<Longrightarrow> length xs = length ys + length zs" 278 by simp 279 280lemma map_upt_reindex': "map f [a ..< b] = map (\<lambda>n. f (n + a - x)) [x ..< x + b - a]" 281 by (rule nth_equalityI; clarsimp simp: add.commute) 282 283lemma map_upt_reindex: "map f [a ..< b] = map (\<lambda>n. f (n + a)) [0 ..< b - a]" 284 by (subst map_upt_reindex' [where x=0]) clarsimp 285 286lemma notemptyI: 287 "x \<in> S \<Longrightarrow> S \<noteq> {}" 288 by clarsimp 289 290lemma setcomp_Max_has_prop: 291 assumes a: "P x" 292 shows "P (Max {(x::'a::{finite,linorder}). P x})" 293proof - 294 from a have "Max {x. P x} \<in> {x. P x}" 295 by - (rule Max_in, auto intro: notemptyI) 296 thus ?thesis by auto 297qed 298 299lemma cons_set_intro: 300 "lst = x # xs \<Longrightarrow> x \<in> set lst" 301 by fastforce 302 303lemma list_all2_conj_nth: 304 assumes lall: "list_all2 P as cs" 305 and rl: "\<And>n. \<lbrakk>P (as ! n) (cs ! n); n < length as\<rbrakk> \<Longrightarrow> Q (as ! n) (cs ! n)" 306 shows "list_all2 (\<lambda>a b. P a b \<and> Q a b) as cs" 307proof (rule list_all2_all_nthI) 308 from lall show "length as = length cs" .. 309next 310 fix n 311 assume "n < length as" 312 313 show "P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n)" 314 proof 315 from lall show "P (as ! n) (cs ! n)" by (rule list_all2_nthD) fact 316 thus "Q (as ! n) (cs ! n)" by (rule rl) fact 317 qed 318qed 319 320lemma list_all2_conj: 321 assumes lall1: "list_all2 P as cs" 322 and lall2: "list_all2 Q as cs" 323 shows "list_all2 (\<lambda>a b. P a b \<and> Q a b) as cs" 324proof (rule list_all2_all_nthI) 325 from lall1 show "length as = length cs" .. 326next 327 fix n 328 assume "n < length as" 329 330 show "P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n)" 331 proof 332 from lall1 show "P (as ! n) (cs ! n)" by (rule list_all2_nthD) fact 333 from lall2 show "Q (as ! n) (cs ! n)" by (rule list_all2_nthD) fact 334 qed 335qed 336 337lemma all_set_into_list_all2: 338 assumes lall: "\<forall>x \<in> set ls. P x" 339 and "length ls = length ls'" 340 shows "list_all2 (\<lambda>a b. P a) ls ls'" 341proof (rule list_all2_all_nthI) 342 fix n 343 assume "n < length ls" 344 from lall show "P (ls ! n)" 345 by (rule bspec [OF _ nth_mem]) fact 346qed fact 347 348lemma GREATEST_lessE: 349 fixes x :: "'a :: order" 350 assumes gts: "(GREATEST x. P x) < X" 351 and px: "P x" 352 and gtst: "\<exists>max. P max \<and> (\<forall>z. P z \<longrightarrow> (z \<le> max))" 353 shows "x < X" 354proof - 355 from gtst obtain max where pm: "P max" and g': "\<And>z. P z \<Longrightarrow> z \<le> max" 356 by auto 357 358 hence "(GREATEST x. P x) = max" 359 by (auto intro: Greatest_equality) 360 361 moreover have "x \<le> max" using px by (rule g') 362 363 ultimately show ?thesis using gts by simp 364qed 365 366lemma set_has_max: 367 fixes ls :: "('a :: linorder) list" 368 assumes ls: "ls \<noteq> []" 369 shows "\<exists>max \<in> set ls. \<forall>z \<in> set ls. z \<le> max" 370 using ls 371proof (induct ls) 372 case Nil thus ?case by simp 373next 374 case (Cons l ls) 375 376 show ?case 377 proof (cases "ls = []") 378 case True 379 thus ?thesis by simp 380 next 381 case False 382 then obtain max where mv: "max \<in> set ls" and mm: "\<forall>z \<in> set ls. z \<le> max" using Cons.hyps 383 by auto 384 show ?thesis 385 proof (cases "max \<le> l") 386 case True 387 have "l \<in> set (l # ls)" by simp 388 thus ?thesis 389 proof 390 from mm show "\<forall>z \<in> set (l # ls). z \<le> l" using True by auto 391 qed 392 next 393 case False 394 from mv have "max \<in> set (l # ls)" by simp 395 thus ?thesis 396 proof 397 from mm show "\<forall>z \<in> set (l # ls). z \<le> max" using False by auto 398 qed 399 qed 400 qed 401qed 402 403lemma True_notin_set_replicate_conv: 404 "True \<notin> set ls = (ls = replicate (length ls) False)" 405 by (induct ls) simp+ 406 407lemma Collect_singleton_eqI: 408 "(\<And>x. P x = (x = v)) \<Longrightarrow> {x. P x} = {v}" 409 by auto 410 411lemma exEI: 412 "\<lbrakk> \<exists>y. P y; \<And>x. P x \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> \<exists>z. Q z" 413 by (rule ex_forward) 414 415lemma allEI: 416 assumes "\<forall>x. P x" 417 assumes "\<And>x. P x \<Longrightarrow> Q x" 418 shows "\<forall>x. Q x" 419 using assms by (rule all_forward) 420 421text \<open>General lemmas that should be in the library\<close> 422 423lemma dom_ran: 424 "x \<in> dom f \<Longrightarrow> the (f x) \<in> ran f" 425 by (simp add: dom_def ran_def, erule exE, simp, rule exI, simp) 426 427lemma orthD1: 428 "\<lbrakk> S \<inter> S' = {}; x \<in> S\<rbrakk> \<Longrightarrow> x \<notin> S'" by auto 429 430lemma orthD2: 431 "\<lbrakk> S \<inter> S' = {}; x \<in> S'\<rbrakk> \<Longrightarrow> x \<notin> S" by auto 432 433lemma distinct_element: 434 "\<lbrakk> b \<inter> d = {}; a \<in> b; c \<in> d\<rbrakk>\<Longrightarrow> a \<noteq> c" 435 by auto 436 437lemma ball_reorder: 438 "(\<forall>x \<in> A. \<forall>y \<in> B. P x y) = (\<forall>y \<in> B. \<forall>x \<in> A. P x y)" 439 by auto 440 441lemma hd_map: "ls \<noteq> [] \<Longrightarrow> hd (map f ls) = f (hd ls)" 442 by (cases ls) auto 443 444lemma tl_map: "tl (map f ls) = map f (tl ls)" 445 by (cases ls) auto 446 447lemma not_NilE: 448 "\<lbrakk> xs \<noteq> []; \<And>x xs'. xs = x # xs' \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 449 by (cases xs) auto 450 451lemma length_SucE: 452 "\<lbrakk> length xs = Suc n; \<And>x xs'. xs = x # xs' \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 453 by (cases xs) auto 454 455lemma map_upt_unfold: 456 assumes ab: "a < b" 457 shows "map f [a ..< b] = f a # map f [Suc a ..< b]" 458 using assms upt_conv_Cons by auto 459 460lemma tl_nat_list_simp: 461 "tl [a..<b] = [a + 1 ..<b]" 462 by (induct b, auto) 463 464lemma image_Collect2: 465 "case_prod f ` {x. P (fst x) (snd x)} = {f x y |x y. P x y}" 466 by (subst image_Collect) simp 467 468lemma image_id': 469 "id ` Y = Y" 470 by clarsimp 471 472lemma image_invert: 473 assumes r: "f \<circ> g = id" 474 and g: "B = g ` A" 475 shows "A = f ` B" 476 by (simp add: g image_comp r) 477 478lemma Collect_image_fun_cong: 479 assumes rl: "\<And>a. P a \<Longrightarrow> f a = g a" 480 shows "{f x | x. P x} = {g x | x. P x}" 481 using rl by force 482 483lemma inj_on_take: 484 shows "inj_on (take n) {x. drop n x = k}" 485proof (rule inj_onI) 486 fix x y 487 assume xv: "x \<in> {x. drop n x = k}" 488 and yv: "y \<in> {x. drop n x = k}" 489 and tk: "take n x = take n y" 490 491 from xv have "take n x @ k = x" 492 using append_take_drop_id mem_Collect_eq by auto 493 moreover from yv tk 494 have "take n x @ k = y" 495 using append_take_drop_id mem_Collect_eq by auto 496 ultimately show "x = y" by simp 497qed 498 499lemma foldr_upd_dom: 500 "dom (foldr (\<lambda>p ps. ps (p \<mapsto> f p)) as g) = dom g \<union> set as" 501proof (induct as) 502 case Nil thus ?case by simp 503next 504 case (Cons a as) 505 show ?case 506 proof (cases "a \<in> set as \<or> a \<in> dom g") 507 case True 508 hence ain: "a \<in> dom g \<union> set as" by auto 509 hence "dom g \<union> set (a # as) = dom g \<union> set as" by auto 510 thus ?thesis using Cons by fastforce 511 next 512 case False 513 hence "a \<notin> (dom g \<union> set as)" by simp 514 hence "dom g \<union> set (a # as) = insert a (dom g \<union> set as)" by simp 515 thus ?thesis using Cons by fastforce 516 qed 517qed 518 519lemma foldr_upd_app: 520 assumes xin: "x \<in> set as" 521 shows "(foldr (\<lambda>p ps. ps (p \<mapsto> f p)) as g) x = Some (f x)" 522 (is "(?f as g) x = Some (f x)") 523 using xin 524proof (induct as arbitrary: x) 525 case Nil thus ?case by simp 526next 527 case (Cons a as) 528 from Cons.prems show ?case by (subst foldr.simps) (auto intro: Cons.hyps) 529qed 530 531lemma foldr_upd_app_other: 532 assumes xin: "x \<notin> set as" 533 shows "(foldr (\<lambda>p ps. ps (p \<mapsto> f p)) as g) x = g x" 534 (is "(?f as g) x = g x") 535 using xin 536proof (induct as arbitrary: x) 537 case Nil thus ?case by simp 538next 539 case (Cons a as) 540 from Cons.prems show ?case 541 by (subst foldr.simps) (auto intro: Cons.hyps) 542qed 543 544lemma foldr_upd_app_if: 545 "foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g = (\<lambda>x. if x \<in> set as then Some (f x) else g x)" 546 by (auto simp: foldr_upd_app foldr_upd_app_other) 547 548lemma foldl_fun_upd_value: 549 "\<And>Y. foldl (\<lambda>f p. f(p := X p)) Y e p = (if p\<in>set e then X p else Y p)" 550 by (induct e) simp_all 551 552lemma foldr_fun_upd_value: 553 "\<And>Y. foldr (\<lambda>p f. f(p := X p)) e Y p = (if p\<in>set e then X p else Y p)" 554 by (induct e) simp_all 555 556lemma foldl_fun_upd_eq_foldr: 557 "!!m. foldl (\<lambda>f p. f(p := g p)) m xs = foldr (\<lambda>p f. f(p := g p)) xs m" 558 by (rule ext) (simp add: foldl_fun_upd_value foldr_fun_upd_value) 559 560lemma Cons_eq_neq: 561 "\<lbrakk> y = x; x # xs \<noteq> y # ys \<rbrakk> \<Longrightarrow> xs \<noteq> ys" 562 by simp 563 564lemma map_upt_append: 565 assumes lt: "x \<le> y" 566 and lt2: "a \<le> x" 567 shows "map f [a ..< y] = map f [a ..< x] @ map f [x ..< y]" 568proof (subst map_append [symmetric], rule arg_cong [where f = "map f"]) 569 from lt obtain k where ky: "x + k = y" 570 by (auto simp: le_iff_add) 571 572 thus "[a ..< y] = [a ..< x] @ [x ..< y]" 573 using lt2 574 by (auto intro: upt_add_eq_append) 575qed 576 577lemma Min_image_distrib: 578 assumes minf: "\<And>x y. \<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> min (f x) (f y) = f (min x y)" 579 and fa: "finite A" 580 and ane: "A \<noteq> {}" 581 shows "Min (f ` A) = f (Min A)" 582proof - 583 have rl: "\<And>F. \<lbrakk> F \<subseteq> A; F \<noteq> {} \<rbrakk> \<Longrightarrow> Min (f ` F) = f (Min F)" 584 proof - 585 fix F 586 assume fa: "F \<subseteq> A" and fne: "F \<noteq> {}" 587 have "finite F" by (rule finite_subset) fact+ 588 589 thus "?thesis F" 590 unfolding min_def using fa fne fa 591 proof (induct rule: finite_subset_induct) 592 case empty 593 thus ?case by simp 594 next 595 case (insert x F) 596 thus ?case 597 by (cases "F = {}") (auto dest: Min_in intro: minf) 598 qed 599 qed 600 601 show ?thesis by (rule rl [OF order_refl]) fact+ 602qed 603 604 605lemma min_of_mono': 606 assumes "(f a \<le> f c) = (a \<le> c)" 607 shows "min (f a) (f c) = f (min a c)" 608 unfolding min_def 609 by (subst if_distrib [where f = f, symmetric], rule arg_cong [where f = f], rule if_cong [OF _ refl refl]) fact+ 610 611lemma nat_diff_less: 612 fixes x :: nat 613 shows "\<lbrakk> x < y + z; z \<le> x\<rbrakk> \<Longrightarrow> x - z < y" 614 using less_diff_conv2 by blast 615 616lemma take_map_Not: 617 "(take n (map Not xs) = take n xs) = (n = 0 \<or> xs = [])" 618 by (cases n; simp) (cases xs; simp) 619 620lemma union_trans: 621 assumes SR: "\<And>x y z. \<lbrakk> (x,y) \<in> S; (y,z) \<in> R \<rbrakk> \<Longrightarrow> (x,z) \<in> S^*" 622 shows "(R \<union> S)^* = R^* \<union> R^* O S^*" 623 apply (rule set_eqI) 624 apply clarsimp 625 apply (rule iffI) 626 apply (erule rtrancl_induct; simp) 627 apply (erule disjE) 628 apply (erule disjE) 629 apply (drule (1) rtrancl_into_rtrancl) 630 apply blast 631 apply clarsimp 632 apply (drule rtranclD [where R=S]) 633 apply (erule disjE) 634 apply simp 635 apply (erule conjE) 636 apply (drule tranclD2) 637 apply (elim exE conjE) 638 apply (drule (1) SR) 639 apply (drule (1) rtrancl_trans) 640 apply blast 641 apply (rule disjI2) 642 apply (erule disjE) 643 apply (blast intro: in_rtrancl_UnI) 644 apply clarsimp 645 apply (drule (1) rtrancl_into_rtrancl) 646 apply (erule (1) relcompI) 647 apply (erule disjE) 648 apply (blast intro: in_rtrancl_UnI) 649 apply clarsimp 650 apply (blast intro: in_rtrancl_UnI rtrancl_trans) 651 done 652 653lemma trancl_trancl: 654 "(R\<^sup>+)\<^sup>+ = R\<^sup>+" 655 by auto 656 657text \<open>Some rules for showing that the reflexive transitive closure of a 658relation/predicate doesn't add much if it was already transitively 659closed.\<close> 660 661lemma rtrancl_eq_reflc_trans: 662 assumes trans: "trans X" 663 shows "rtrancl X = X \<union> Id" 664 by (simp only: rtrancl_trancl_reflcl trancl_id[OF trans]) 665 666lemma rtrancl_id: 667 assumes refl: "Id \<subseteq> X" 668 assumes trans: "trans X" 669 shows "rtrancl X = X" 670 using refl rtrancl_eq_reflc_trans[OF trans] 671 by blast 672 673lemma rtranclp_eq_reflcp_transp: 674 assumes trans: "transp X" 675 shows "rtranclp X = (\<lambda>x y. X x y \<or> x = y)" 676 by (simp add: Enum.rtranclp_rtrancl_eq fun_eq_iff 677 rtrancl_eq_reflc_trans trans[unfolded transp_trans]) 678 679lemma rtranclp_id: 680 shows "reflp X \<Longrightarrow> transp X \<Longrightarrow> rtranclp X = X" 681 apply (simp add: rtranclp_eq_reflcp_transp) 682 apply (auto simp: fun_eq_iff elim: reflpD) 683 done 684 685lemmas rtranclp_id2 = rtranclp_id[unfolded reflp_def transp_relcompp le_fun_def] 686 687lemma if_1_0_0: 688 "((if P then 1 else 0) = (0 :: ('a :: zero_neq_one))) = (\<not> P)" 689 by (simp split: if_split) 690 691lemma neq_Nil_lengthI: 692 "Suc 0 \<le> length xs \<Longrightarrow> xs \<noteq> []" 693 by (cases xs, auto) 694 695lemmas ex_with_length = Ex_list_of_length 696 697lemma in_singleton: 698 "S = {x} \<Longrightarrow> x \<in> S" 699 by simp 700 701lemma singleton_set: 702 "x \<in> set [a] \<Longrightarrow> x = a" 703 by auto 704 705lemma take_drop_eqI: 706 assumes t: "take n xs = take n ys" 707 assumes d: "drop n xs = drop n ys" 708 shows "xs = ys" 709proof - 710 have "xs = take n xs @ drop n xs" by simp 711 with t d 712 have "xs = take n ys @ drop n ys" by simp 713 moreover 714 have "ys = take n ys @ drop n ys" by simp 715 ultimately 716 show ?thesis by simp 717qed 718 719lemma append_len2: 720 "zs = xs @ ys \<Longrightarrow> length xs = length zs - length ys" 721 by auto 722 723lemma if_flip: 724 "(if \<not>P then T else F) = (if P then F else T)" 725 by simp 726 727lemma not_in_domIff:"f x = None = (x \<notin> dom f)" 728 by blast 729 730lemma not_in_domD: 731 "x \<notin> dom f \<Longrightarrow> f x = None" 732 by (simp add:not_in_domIff) 733 734definition 735 "graph_of f \<equiv> {(x,y). f x = Some y}" 736 737lemma graph_of_None_update: 738 "graph_of (f (p := None)) = graph_of f - {p} \<times> UNIV" 739 by (auto simp: graph_of_def split: if_split_asm) 740 741lemma graph_of_Some_update: 742 "graph_of (f (p \<mapsto> v)) = (graph_of f - {p} \<times> UNIV) \<union> {(p,v)}" 743 by (auto simp: graph_of_def split: if_split_asm) 744 745lemma graph_of_restrict_map: 746 "graph_of (m |` S) \<subseteq> graph_of m" 747 by (simp add: graph_of_def restrict_map_def subset_iff) 748 749lemma graph_ofD: 750 "(x,y) \<in> graph_of f \<Longrightarrow> f x = Some y" 751 by (simp add: graph_of_def) 752 753lemma graph_ofI: 754 "m x = Some y \<Longrightarrow> (x, y) \<in> graph_of m" 755 by (simp add: graph_of_def) 756 757lemma graph_of_empty : 758 "graph_of Map.empty = {}" 759 by (simp add: graph_of_def) 760 761lemma graph_of_in_ranD: "\<forall>y \<in> ran f. P y \<Longrightarrow> (x,y) \<in> graph_of f \<Longrightarrow> P y" 762 by (auto simp: graph_of_def ran_def) 763 764lemma graph_of_SomeD: 765 "\<lbrakk> graph_of f \<subseteq> graph_of g; f x = Some y \<rbrakk> \<Longrightarrow> g x = Some y" 766 unfolding graph_of_def 767 by auto 768 769lemma in_set_zip_refl : 770 "(x,y) \<in> set (zip xs xs) = (y = x \<and> x \<in> set xs)" 771 by (induct xs) auto 772 773lemma map_conv_upd: 774 "m v = None \<Longrightarrow> m o (f (x := v)) = (m o f) (x := None)" 775 by (rule ext) (clarsimp simp: o_def) 776 777lemma sum_all_ex [simp]: 778 "(\<forall>a. x \<noteq> Inl a) = (\<exists>a. x = Inr a)" 779 "(\<forall>a. x \<noteq> Inr a) = (\<exists>a. x = Inl a)" 780 by (metis Inr_not_Inl sum.exhaust)+ 781 782lemma split_distrib: "case_prod (\<lambda>a b. T (f a b)) = (\<lambda>x. T (case_prod (\<lambda>a b. f a b) x))" 783 by (clarsimp simp: split_def) 784 785lemma case_sum_triv [simp]: 786 "(case x of Inl x \<Rightarrow> Inl x | Inr x \<Rightarrow> Inr x) = x" 787 by (clarsimp split: sum.splits) 788 789lemma set_eq_UNIV: "({a. P a} = UNIV) = (\<forall>a. P a)" 790 by force 791 792lemma allE2: 793 "\<lbrakk>\<forall>x y. P x y; P x y \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 794 by blast 795 796lemma allE3: "\<lbrakk> \<forall>x y z. P x y z; P x y z \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 797 by auto 798 799lemma my_BallE: "\<lbrakk> \<forall>x \<in> A. P x; y \<in> A; P y \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" 800 by (simp add: Ball_def) 801 802lemma unit_Inl_or_Inr [simp]: 803 "\<And>a. (a \<noteq> Inl ()) = (a = Inr ())" 804 "\<And>a. (a \<noteq> Inr ()) = (a = Inl ())" 805 by (case_tac a; clarsimp)+ 806 807lemma disjE_L: "\<lbrakk> a \<or> b; a \<Longrightarrow> R; \<lbrakk> \<not> a; b \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 808 by blast 809 810lemma disjE_R: "\<lbrakk> a \<or> b; \<lbrakk> \<not> b; a \<rbrakk> \<Longrightarrow> R; \<lbrakk> b \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 811 by blast 812 813lemma int_max_thms: 814 "(a :: int) \<le> max a b" 815 "(b :: int) \<le> max a b" 816 by (auto simp: max_def) 817 818lemma sgn_negation [simp]: 819 "sgn (-(x::int)) = - sgn x" 820 by (clarsimp simp: sgn_if) 821 822lemma sgn_sgn_nonneg [simp]: 823 "sgn (a :: int) * sgn a \<noteq> -1" 824 by (clarsimp simp: sgn_if) 825 826 827lemma inj_inj_on: 828 "inj f \<Longrightarrow> inj_on f A" 829 by (metis injD inj_onI) 830 831lemma ex_eqI: 832 "\<lbrakk>\<And>x. f x = g x\<rbrakk> \<Longrightarrow> (\<exists>x. f x) = (\<exists>x. g x)" 833 by simp 834 835lemma pre_post_ex: 836 "\<lbrakk>\<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> \<exists>x. Q x" 837 by auto 838 839lemma ex_conj_increase: 840 "((\<exists>x. P x) \<and> Q) = (\<exists>x. P x \<and> Q)" 841 "(R \<and> (\<exists>x. S x)) = (\<exists>x. R \<and> S x)" 842 by simp+ 843 844lemma all_conj_increase: 845 "(( \<forall>x. P x) \<and> Q) = (\<forall>x. P x \<and> Q)" 846 "(R \<and> (\<forall>x. S x)) = (\<forall>x. R \<and> S x)" 847 by simp+ 848 849lemma Ball_conj_increase: 850 "xs \<noteq> {} \<Longrightarrow> (( \<forall>x \<in> xs. P x) \<and> Q) = (\<forall>x \<in> xs. P x \<and> Q)" 851 "xs \<noteq> {} \<Longrightarrow> (R \<and> (\<forall>x \<in> xs. S x)) = (\<forall>x \<in> xs. R \<and> S x)" 852 by auto 853 854(*************** 855 * Union rules * 856 ***************) 857 858lemma disjoint_subset: 859 assumes "A' \<subseteq> A" and "A \<inter> B = {}" 860 shows "A' \<inter> B = {}" 861 using assms by auto 862 863lemma disjoint_subset2: 864 assumes "B' \<subseteq> B" and "A \<inter> B = {}" 865 shows "A \<inter> B' = {}" 866 using assms by auto 867 868lemma UN_nth_mem: 869 "i < length xs \<Longrightarrow> f (xs ! i) \<subseteq> (\<Union>x\<in>set xs. f x)" 870 by (metis UN_upper nth_mem) 871 872lemma Union_equal: 873 "f ` A = f ` B \<Longrightarrow> (\<Union>x \<in> A. f x) = (\<Union>x \<in> B. f x)" 874 by blast 875 876lemma UN_Diff_disjoint: 877 "i < length xs \<Longrightarrow> (A - (\<Union>x\<in>set xs. f x)) \<inter> f (xs ! i) = {}" 878 by (metis Diff_disjoint Int_commute UN_nth_mem disjoint_subset) 879 880lemma image_list_update: 881 "f a = f (xs ! i) 882 \<Longrightarrow> f ` set (xs [i := a]) = f ` set xs" 883 by (metis list_update_id map_update set_map) 884 885lemma Union_list_update_id: 886 "f a = f (xs ! i) \<Longrightarrow> (\<Union>x\<in>set (xs [i := a]). f x) = (\<Union>x\<in>set xs. f x)" 887 by (rule Union_equal) (erule image_list_update) 888 889lemma Union_list_update_id': 890 "\<lbrakk>i < length xs; \<And>x. g (f x) = g x\<rbrakk> 891 \<Longrightarrow> (\<Union>x\<in>set (xs [i := f (xs ! i)]). g x) = (\<Union>x\<in>set xs. g x)" 892 by (metis Union_list_update_id) 893 894lemma Union_subset: 895 "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> (f x) \<subseteq> (g x)\<rbrakk> \<Longrightarrow> (\<Union>x \<in> A. f x) \<subseteq> (\<Union>x \<in> A. g x)" 896 by (metis UN_mono order_refl) 897 898lemma UN_sub_empty: 899 "\<lbrakk>list_all P xs; \<And>x. P x \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> (\<Union>x\<in>set xs. f x) - (\<Union>x\<in>set xs. g x) = {}" 900 by (simp add: Ball_set_list_all[symmetric] Union_subset) 901 902(******************* 903 * bij_betw rules. * 904 *******************) 905 906lemma bij_betw_fun_updI: 907 "\<lbrakk>x \<notin> A; y \<notin> B; bij_betw f A B\<rbrakk> \<Longrightarrow> bij_betw (f(x := y)) (insert x A) (insert y B)" 908 by (clarsimp simp: bij_betw_def fun_upd_image inj_on_fun_updI split: if_split_asm; blast) 909 910definition 911 "bij_betw_map f A B \<equiv> bij_betw f A (Some ` B)" 912 913lemma bij_betw_map_fun_updI: 914 "\<lbrakk>x \<notin> A; y \<notin> B; bij_betw_map f A B\<rbrakk> 915 \<Longrightarrow> bij_betw_map (f(x \<mapsto> y)) (insert x A) (insert y B)" 916 unfolding bij_betw_map_def by clarsimp (erule bij_betw_fun_updI; clarsimp) 917 918lemma bij_betw_map_imp_inj_on: 919 "bij_betw_map f A B \<Longrightarrow> inj_on f A" 920 by (simp add: bij_betw_map_def bij_betw_imp_inj_on) 921 922lemma bij_betw_empty_dom_exists: 923 "r = {} \<Longrightarrow> \<exists>t. bij_betw t {} r" 924 by (clarsimp simp: bij_betw_def) 925 926lemma bij_betw_map_empty_dom_exists: 927 "r = {} \<Longrightarrow> \<exists>t. bij_betw_map t {} r" 928 by (clarsimp simp: bij_betw_map_def bij_betw_empty_dom_exists) 929 930(* 931 * Function and Relation Powers. 932 *) 933 934lemma funpow_add [simp]: 935 fixes f :: "'a \<Rightarrow> 'a" 936 shows "(f ^^ a) ((f ^^ b) s) = (f ^^ (a + b)) s" 937 by (metis comp_apply funpow_add) 938 939lemma funpow_unfold: 940 fixes f :: "'a \<Rightarrow> 'a" 941 assumes "n > 0" 942 shows "f ^^ n = (f ^^ (n - 1)) \<circ> f" 943 by (metis Suc_diff_1 assms funpow_Suc_right) 944 945lemma relpow_unfold: "n > 0 \<Longrightarrow> S ^^ n = (S ^^ (n - 1)) O S" 946 by (cases n, auto) 947 948 949(* 950 * Equivalence relations. 951 *) 952 953(* Convert a projection into an equivalence relation. *) 954definition 955 equiv_of :: "('s \<Rightarrow> 't) \<Rightarrow> ('s \<times> 's) set" 956where 957 "equiv_of proj \<equiv> {(a, b). proj a = proj b}" 958 959lemma equiv_of_is_equiv_relation [simp]: 960 "equiv UNIV (equiv_of proj)" 961 by (auto simp: equiv_of_def intro!: equivI refl_onI symI transI) 962 963lemma in_equiv_of [simp]: 964 "((a, b) \<in> equiv_of f) \<longleftrightarrow> (f a = f b)" 965 by (clarsimp simp: equiv_of_def) 966 967(* For every equivalence relation R, there exists a projection function 968 * "f" such that "f x = f y \<longleftrightarrow> (x, y) \<in> R". That is, you can reason 969 * about projections instead of equivalence relations if you so wish. *) 970lemma equiv_relation_to_projection: 971 fixes R :: "('a \<times> 'a) set" 972 assumes equiv: "equiv UNIV R" 973 shows "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>x y. f x = f y \<longleftrightarrow> (x, y) \<in> R" 974 apply (rule exI [of _ "\<lambda>x. {y. (x, y) \<in> R}"]) 975 apply clarsimp 976 apply (case_tac "(x, y) \<in> R") 977 apply clarsimp 978 apply (rule set_eqI) 979 apply clarsimp 980 apply (metis equivE sym_def trans_def equiv) 981 apply (clarsimp) 982 apply (metis UNIV_I equiv equivE mem_Collect_eq refl_on_def) 983 done 984 985lemma range_constant [simp]: 986 "range (\<lambda>_. k) = {k}" 987 by (clarsimp simp: image_def) 988 989lemma dom_unpack: 990 "dom (map_of (map (\<lambda>x. (f x, g x)) xs)) = set (map (\<lambda>x. f x) xs)" 991 by (simp add: dom_map_of_conv_image_fst image_image) 992 993lemma fold_to_disj: 994"fold (++) ms a x = Some y \<Longrightarrow> (\<exists>b \<in> set ms. b x = Some y) \<or> a x = Some y" 995 by (induct ms arbitrary:a x y; clarsimp) blast 996 997lemma fold_ignore1: 998 "a x = Some y \<Longrightarrow> fold (++) ms a x = Some y" 999 by (induct ms arbitrary:a x y; clarsimp) 1000 1001lemma fold_ignore2: 1002 "fold (++) ms a x = None \<Longrightarrow> a x = None" 1003 by (metis fold_ignore1 option.collapse) 1004 1005lemma fold_ignore3: 1006 "fold (++) ms a x = None \<Longrightarrow> (\<forall>b \<in> set ms. b x = None)" 1007 by (induct ms arbitrary:a x; clarsimp) (meson fold_ignore2 map_add_None) 1008 1009lemma fold_ignore4: 1010 "b \<in> set ms \<Longrightarrow> b x = Some y \<Longrightarrow> \<exists>y. fold (++) ms a x = Some y" 1011 using fold_ignore3 by fastforce 1012 1013lemma dom_unpack2: 1014 "dom (fold (++) ms Map.empty) = \<Union>(set (map dom ms))" 1015 apply (induct ms; clarsimp simp:dom_def) 1016 apply (rule equalityI; clarsimp) 1017 apply (drule fold_to_disj) 1018 apply (erule disjE) 1019 apply clarsimp 1020 apply (rename_tac b) 1021 apply (erule_tac x=b in ballE; clarsimp) 1022 apply clarsimp 1023 apply (rule conjI) 1024 apply clarsimp 1025 apply (rule_tac x=y in exI) 1026 apply (erule fold_ignore1) 1027 apply clarsimp 1028 apply (rename_tac y) 1029 apply (erule_tac y=y in fold_ignore4; clarsimp) 1030 done 1031 1032lemma fold_ignore5:"fold (++) ms a x = Some y \<Longrightarrow> a x = Some y \<or> (\<exists>b \<in> set ms. b x = Some y)" 1033 by (induct ms arbitrary:a x y; clarsimp) blast 1034 1035lemma dom_inter_nothing:"dom f \<inter> dom g = {} \<Longrightarrow> \<forall>x. f x = None \<or> g x = None" 1036 by auto 1037 1038lemma fold_ignore6: 1039 "f x = None \<Longrightarrow> fold (++) ms f x = fold (++) ms Map.empty x" 1040 apply (induct ms arbitrary:f x; clarsimp simp:map_add_def) 1041 by (metis (no_types, lifting) fold_ignore1 option.collapse option.simps(4)) 1042 1043lemma fold_ignore7: 1044 "m x = m' x \<Longrightarrow> fold (++) ms m x = fold (++) ms m' x" 1045 apply (case_tac "m x") 1046 apply (frule_tac ms=ms in fold_ignore6) 1047 apply (cut_tac f=m' and ms=ms and x=x in fold_ignore6) 1048 apply clarsimp+ 1049 apply (rename_tac a) 1050 apply (cut_tac ms=ms and a=m and x=x and y=a in fold_ignore1, clarsimp) 1051 apply (cut_tac ms=ms and a=m' and x=x and y=a in fold_ignore1; clarsimp) 1052 done 1053 1054lemma fold_ignore8: 1055 "fold (++) ms [x \<mapsto> y] = (fold (++) ms Map.empty)(x \<mapsto> y)" 1056 apply (rule ext) 1057 apply (rename_tac xa) 1058 apply (case_tac "xa = x") 1059 apply clarsimp 1060 apply (rule fold_ignore1) 1061 apply clarsimp 1062 apply (subst fold_ignore6; clarsimp) 1063 done 1064 1065lemma fold_ignore9: 1066 "\<lbrakk>fold (++) ms [x \<mapsto> y] x' = Some z; x = x'\<rbrakk> \<Longrightarrow> y = z" 1067 by (subst (asm) fold_ignore8) clarsimp 1068 1069lemma fold_to_map_of: 1070 "fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) Map.empty = map_of (map (\<lambda>x. (f x, g x)) xs)" 1071 apply (rule ext) 1072 apply (rename_tac x) 1073 apply (case_tac "fold (++) (map (\<lambda>x. [f x \<mapsto> g x]) xs) Map.empty x") 1074 apply clarsimp 1075 apply (drule fold_ignore3) 1076 apply (clarsimp split:if_split_asm) 1077 apply (rule sym) 1078 apply (subst map_of_eq_None_iff) 1079 apply clarsimp 1080 apply (rename_tac xa) 1081 apply (erule_tac x=xa in ballE; clarsimp) 1082 apply clarsimp 1083 apply (frule fold_ignore5; clarsimp split:if_split_asm) 1084 apply (subst map_add_map_of_foldr[where m=Map.empty, simplified]) 1085 apply (induct xs arbitrary:f g; clarsimp split:if_split) 1086 apply (rule conjI; clarsimp) 1087 apply (drule fold_ignore9; clarsimp) 1088 apply (cut_tac ms="map (\<lambda>x. [f x \<mapsto> g x]) xs" and f="[f a \<mapsto> g a]" and x="f b" in fold_ignore6, clarsimp) 1089 apply auto 1090 done 1091 1092lemma if_n_0_0: 1093 "((if P then n else 0) \<noteq> 0) = (P \<and> n \<noteq> 0)" 1094 by (simp split: if_split) 1095 1096lemma insert_dom: 1097 assumes fx: "f x = Some y" 1098 shows "insert x (dom f) = dom f" 1099 unfolding dom_def using fx by auto 1100 1101lemma map_comp_subset_dom: 1102 "dom (prj \<circ>\<^sub>m f) \<subseteq> dom f" 1103 unfolding dom_def 1104 by (auto simp: map_comp_Some_iff) 1105 1106lemmas map_comp_subset_domD = subsetD [OF map_comp_subset_dom] 1107 1108lemma dom_map_comp: 1109 "x \<in> dom (prj \<circ>\<^sub>m f) = (\<exists>y z. f x = Some y \<and> prj y = Some z)" 1110 by (fastforce simp: dom_def map_comp_Some_iff) 1111 1112lemma map_option_Some_eq2: 1113 "(Some y = map_option f x) = (\<exists>z. x = Some z \<and> f z = y)" 1114 by (metis map_option_eq_Some) 1115 1116lemma map_option_eq_dom_eq: 1117 assumes ome: "map_option f \<circ> g = map_option f \<circ> g'" 1118 shows "dom g = dom g'" 1119proof (rule set_eqI) 1120 fix x 1121 { 1122 assume "x \<in> dom g" 1123 hence "Some (f (the (g x))) = (map_option f \<circ> g) x" 1124 by (auto simp: map_option_case split: option.splits) 1125 also have "\<dots> = (map_option f \<circ> g') x" by (simp add: ome) 1126 finally have "x \<in> dom g'" 1127 by (auto simp: map_option_case split: option.splits) 1128 } moreover 1129 { 1130 assume "x \<in> dom g'" 1131 hence "Some (f (the (g' x))) = (map_option f \<circ> g') x" 1132 by (auto simp: map_option_case split: option.splits) 1133 also have "\<dots> = (map_option f \<circ> g) x" by (simp add: ome) 1134 finally have "x \<in> dom g" 1135 by (auto simp: map_option_case split: option.splits) 1136 } ultimately show "(x \<in> dom g) = (x \<in> dom g')" by auto 1137qed 1138 1139 1140lemma cart_singleton_image: 1141 "S \<times> {s} = (\<lambda>v. (v, s)) ` S" 1142 by auto 1143 1144lemma singleton_eq_o2s: 1145 "({x} = set_option v) = (v = Some x)" 1146 by (cases v, auto) 1147 1148lemma option_set_singleton_eq: 1149 "(set_option opt = {v}) = (opt = Some v)" 1150 by (cases opt, simp_all) 1151 1152lemmas option_set_singleton_eqs 1153 = option_set_singleton_eq 1154 trans[OF eq_commute option_set_singleton_eq] 1155 1156lemma map_option_comp2: 1157 "map_option (f o g) = map_option f o map_option g" 1158 by (simp add: option.map_comp fun_eq_iff) 1159 1160lemma compD: 1161 "\<lbrakk>f \<circ> g = f \<circ> g'; g x = v \<rbrakk> \<Longrightarrow> f (g' x) = f v" 1162 by (metis comp_apply) 1163 1164lemma map_option_comp_eqE: 1165 assumes om: "map_option f \<circ> mp = map_option f \<circ> mp'" 1166 and p1: "\<lbrakk> mp x = None; mp' x = None \<rbrakk> \<Longrightarrow> P" 1167 and p2: "\<And>v v'. \<lbrakk> mp x = Some v; mp' x = Some v'; f v = f v' \<rbrakk> \<Longrightarrow> P" 1168 shows "P" 1169proof (cases "mp x") 1170 case None 1171 hence "x \<notin> dom mp" by (simp add: domIff) 1172 hence "mp' x = None" by (simp add: map_option_eq_dom_eq [OF om] domIff) 1173 with None show ?thesis by (rule p1) 1174next 1175 case (Some v) 1176 hence "x \<in> dom mp" by clarsimp 1177 then obtain v' where Some': "mp' x = Some v'" by (clarsimp simp add: map_option_eq_dom_eq [OF om]) 1178 with Some show ?thesis 1179 proof (rule p2) 1180 show "f v = f v'" using Some' compD [OF om, OF Some] by simp 1181 qed 1182qed 1183 1184lemma Some_the: 1185 "x \<in> dom f \<Longrightarrow> f x = Some (the (f x))" 1186 by clarsimp 1187 1188lemma map_comp_update: 1189 "f \<circ>\<^sub>m (g(x \<mapsto> v)) = (f \<circ>\<^sub>m g)(x := f v)" 1190 by (rule ext, rename_tac y) (case_tac "g y"; simp) 1191 1192lemma restrict_map_eqI: 1193 assumes req: "A |` S = B |` S" 1194 and mem: "x \<in> S" 1195 shows "A x = B x" 1196proof - 1197 from mem have "A x = (A |` S) x" by simp 1198 also have "\<dots> = (B |` S) x" using req by simp 1199 also have "\<dots> = B x" using mem by simp 1200 finally show ?thesis . 1201qed 1202 1203lemma map_comp_eqI: 1204 assumes dm: "dom g = dom g'" 1205 and fg: "\<And>x. x \<in> dom g' \<Longrightarrow> f (the (g' x)) = f (the (g x))" 1206 shows "f \<circ>\<^sub>m g = f \<circ>\<^sub>m g'" 1207 apply (rule ext) 1208 apply (case_tac "x \<in> dom g") 1209 apply (frule subst [OF dm]) 1210 apply (clarsimp split: option.splits) 1211 apply (frule domI [where m = g']) 1212 apply (drule fg) 1213 apply simp 1214 apply (frule subst [OF dm]) 1215 apply clarsimp 1216 apply (drule not_sym) 1217 apply (clarsimp simp: map_comp_Some_iff) 1218 done 1219 1220 1221definition 1222 "modify_map m p f \<equiv> m (p := map_option f (m p))" 1223 1224lemma modify_map_id: 1225 "modify_map m p id = m" 1226 by (auto simp add: modify_map_def map_option_case split: option.splits) 1227 1228lemma modify_map_addr_com: 1229 assumes com: "x \<noteq> y" 1230 shows "modify_map (modify_map m x g) y f = modify_map (modify_map m y f) x g" 1231 by (rule ext) (simp add: modify_map_def map_option_case com split: option.splits) 1232 1233lemma modify_map_dom : 1234 "dom (modify_map m p f) = dom m" 1235 unfolding modify_map_def by (auto simp: dom_def) 1236 1237lemma modify_map_None: 1238 "m x = None \<Longrightarrow> modify_map m x f = m" 1239 by (rule ext) (simp add: modify_map_def) 1240 1241lemma modify_map_ndom : 1242 "x \<notin> dom m \<Longrightarrow> modify_map m x f = m" 1243 by (rule modify_map_None) clarsimp 1244 1245lemma modify_map_app: 1246 "(modify_map m p f) q = (if p = q then map_option f (m p) else m q)" 1247 unfolding modify_map_def by simp 1248 1249lemma modify_map_apply: 1250 "m p = Some x \<Longrightarrow> modify_map m p f = m (p \<mapsto> f x)" 1251 by (simp add: modify_map_def) 1252 1253lemma modify_map_com: 1254 assumes com: "\<And>x. f (g x) = g (f x)" 1255 shows "modify_map (modify_map m x g) y f = modify_map (modify_map m y f) x g" 1256 using assms by (auto simp: modify_map_def map_option_case split: option.splits) 1257 1258lemma modify_map_comp: 1259 "modify_map m x (f o g) = modify_map (modify_map m x g) x f" 1260 by (rule ext) (simp add: modify_map_def option.map_comp) 1261 1262lemma modify_map_exists_eq: 1263 "(\<exists>cte. modify_map m p' f p= Some cte) = (\<exists>cte. m p = Some cte)" 1264 by (auto simp: modify_map_def split: if_splits) 1265 1266lemma modify_map_other: 1267 "p \<noteq> q \<Longrightarrow> (modify_map m p f) q = (m q)" 1268 by (simp add: modify_map_app) 1269 1270lemma modify_map_same: 1271 "modify_map m p f p = map_option f (m p)" 1272 by (simp add: modify_map_app) 1273 1274lemma next_update_is_modify: 1275 "\<lbrakk> m p = Some cte'; cte = f cte' \<rbrakk> \<Longrightarrow> (m(p \<mapsto> cte)) = modify_map m p f" 1276 unfolding modify_map_def by simp 1277 1278lemma nat_power_minus_less: 1279 "a < 2 ^ (x - n) \<Longrightarrow> (a :: nat) < 2 ^ x" 1280 by (erule order_less_le_trans) simp 1281 1282lemma neg_rtranclI: 1283 "\<lbrakk> x \<noteq> y; (x, y) \<notin> R\<^sup>+ \<rbrakk> \<Longrightarrow> (x, y) \<notin> R\<^sup>*" 1284 by (meson rtranclD) 1285 1286lemma neg_rtrancl_into_trancl: 1287 "\<not> (x, y) \<in> R\<^sup>* \<Longrightarrow> \<not> (x, y) \<in> R\<^sup>+" 1288 by (erule contrapos_nn, erule trancl_into_rtrancl) 1289 1290lemma set_neqI: 1291 "\<lbrakk> x \<in> S; x \<notin> S' \<rbrakk> \<Longrightarrow> S \<noteq> S'" 1292 by clarsimp 1293 1294lemma set_pair_UN: 1295 "{x. P x} = \<Union> ((\<lambda>xa. {xa} \<times> {xb. P (xa, xb)}) ` {xa. \<exists>xb. P (xa, xb)})" 1296 by fastforce 1297 1298lemma singleton_elemD: "S = {x} \<Longrightarrow> x \<in> S" 1299 by simp 1300 1301lemma singleton_eqD: "A = {x} \<Longrightarrow> x \<in> A" 1302 by blast 1303 1304lemma ball_ran_fun_updI: 1305 "\<lbrakk> \<forall>v \<in> ran m. P v; \<forall>v. y = Some v \<longrightarrow> P v \<rbrakk> \<Longrightarrow> \<forall>v \<in> ran (m (x := y)). P v" 1306 by (auto simp add: ran_def) 1307 1308lemma ball_ran_eq: 1309 "(\<forall>y \<in> ran m. P y) = (\<forall>x y. m x = Some y \<longrightarrow> P y)" 1310 by (auto simp add: ran_def) 1311 1312lemma cart_helper: 1313 "({} = {x} \<times> S) = (S = {})" 1314 by blast 1315 1316lemmas converse_trancl_induct' = converse_trancl_induct [consumes 1, case_names base step] 1317 1318lemma disjCI2: "(\<not> P \<Longrightarrow> Q) \<Longrightarrow> P \<or> Q" by blast 1319 1320lemma insert_UNIV : 1321 "insert x UNIV = UNIV" 1322 by blast 1323 1324lemma not_singletonE: 1325 "\<lbrakk> \<forall>p. S \<noteq> {p}; S \<noteq> {}; \<And>p p'. \<lbrakk> p \<noteq> p'; p \<in> S; p' \<in> S \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 1326 by blast 1327 1328lemma not_singleton_oneE: 1329 "\<lbrakk> \<forall>p. S \<noteq> {p}; p \<in> S; \<And>p'. \<lbrakk> p \<noteq> p'; p' \<in> S \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 1330 using not_singletonE by fastforce 1331 1332lemma ball_ran_modify_map_eq: 1333 "\<lbrakk> \<forall>v. m x = Some v \<longrightarrow> P (f v) = P v \<rbrakk> 1334 \<Longrightarrow> (\<forall>v \<in> ran (modify_map m x f). P v) = (\<forall>v \<in> ran m. P v)" 1335 by (auto simp: modify_map_def ball_ran_eq) 1336 1337lemma eq_singleton_redux: 1338 "\<lbrakk> S = {x} \<rbrakk> \<Longrightarrow> x \<in> S" 1339 by simp 1340 1341lemma if_eq_elem_helperE: 1342 "\<lbrakk> x \<in> (if P then S else S'); \<lbrakk> P; x \<in> S \<rbrakk> \<Longrightarrow> a = b; \<lbrakk> \<not> P; x \<in> S' \<rbrakk> \<Longrightarrow> a = c \<rbrakk> 1343 \<Longrightarrow> a = (if P then b else c)" 1344 by fastforce 1345 1346lemma if_option_Some: 1347 "((if P then None else Some x) = Some y) = (\<not>P \<and> x = y)" 1348 by simp 1349 1350lemma insert_minus_eq: 1351 "x \<notin> A \<Longrightarrow> A - S = (A - (S - {x}))" 1352 by auto 1353 1354lemma modify_map_K_D: 1355 "modify_map m p (\<lambda>x. y) p' = Some v \<Longrightarrow> (m (p \<mapsto> y)) p' = Some v" 1356 by (simp add: modify_map_def split: if_split_asm) 1357 1358lemma tranclE2: 1359 assumes trancl: "(a, b) \<in> r\<^sup>+" 1360 and base: "(a, b) \<in> r \<Longrightarrow> P" 1361 and step: "\<And>c. \<lbrakk>(a, c) \<in> r; (c, b) \<in> r\<^sup>+\<rbrakk> \<Longrightarrow> P" 1362 shows "P" 1363 using trancl base step 1364proof - 1365 note rl = converse_trancl_induct [where P = "\<lambda>x. x = a \<longrightarrow> P"] 1366 from trancl have "a = a \<longrightarrow> P" 1367 by (rule rl, (iprover intro: base step)+) 1368 thus ?thesis by simp 1369qed 1370 1371lemmas tranclE2' = tranclE2 [consumes 1, case_names base trancl] 1372 1373lemma weak_imp_cong: 1374 "\<lbrakk> P = R; Q = S \<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) = (R \<longrightarrow> S)" 1375 by simp 1376 1377lemma Collect_Diff_restrict_simp: 1378 "T - {x \<in> T. Q x} = T - {x. Q x}" 1379 by (auto intro: Collect_cong) 1380 1381lemma Collect_Int_pred_eq: 1382 "{x \<in> S. P x} \<inter> {x \<in> T. P x} = {x \<in> (S \<inter> T). P x}" 1383 by (simp add: Collect_conj_eq [symmetric] conj_comms) 1384 1385lemma Collect_restrict_predR: 1386 "{x. P x} \<inter> T = {} \<Longrightarrow> {x. P x} \<inter> {x \<in> T. Q x} = {}" 1387 by (fastforce simp: disjoint_iff_not_equal) 1388 1389lemma Diff_Un2: 1390 assumes emptyad: "A \<inter> D = {}" 1391 and emptybc: "B \<inter> C = {}" 1392 shows "(A \<union> B) - (C \<union> D) = (A - C) \<union> (B - D)" 1393proof - 1394 have "(A \<union> B) - (C \<union> D) = (A \<union> B - C) \<inter> (A \<union> B - D)" 1395 by (rule Diff_Un) 1396 also have "\<dots> = ((A - C) \<union> B) \<inter> (A \<union> (B - D))" using emptyad emptybc 1397 by (simp add: Un_Diff Diff_triv) 1398 also have "\<dots> = (A - C) \<union> (B - D)" 1399 proof - 1400 have "(A - C) \<inter> (A \<union> (B - D)) = A - C" using emptyad emptybc 1401 by (metis Diff_Int2 Diff_Int_distrib2 inf_sup_absorb) 1402 moreover 1403 have "B \<inter> (A \<union> (B - D)) = B - D" using emptyad emptybc 1404 by (metis Int_Diff Un_Diff Un_Diff_Int Un_commute Un_empty_left inf_sup_absorb) 1405 ultimately show ?thesis 1406 by (simp add: Int_Un_distrib2) 1407 qed 1408 finally show ?thesis . 1409qed 1410 1411lemma ballEI: 1412 "\<lbrakk> \<forall>x \<in> S. Q x; \<And>x. \<lbrakk> x \<in> S; Q x \<rbrakk> \<Longrightarrow> P x \<rbrakk> \<Longrightarrow> \<forall>x \<in> S. P x" 1413 by auto 1414 1415lemma dom_if_None: 1416 "dom (\<lambda>x. if P x then None else f x) = dom f - {x. P x}" 1417 by (simp add: dom_def) fastforce 1418 1419lemma restrict_map_Some_iff: 1420 "((m |` S) x = Some y) = (m x = Some y \<and> x \<in> S)" 1421 by (cases "x \<in> S", simp_all) 1422 1423lemma context_case_bools: 1424 "\<lbrakk> \<And>v. P v \<Longrightarrow> R v; \<lbrakk> \<not> P v; \<And>v. P v \<Longrightarrow> R v \<rbrakk> \<Longrightarrow> R v \<rbrakk> \<Longrightarrow> R v" 1425 by (cases "P v", simp_all) 1426 1427lemma inj_on_fun_upd_strongerI: 1428 "\<lbrakk>inj_on f A; y \<notin> f ` (A - {x})\<rbrakk> \<Longrightarrow> inj_on (f(x := y)) A" 1429 by (fastforce simp: inj_on_def) 1430 1431lemma less_handy_casesE: 1432 "\<lbrakk> m < n; m = 0 \<Longrightarrow> R; \<And>m' n'. \<lbrakk> n = Suc n'; m = Suc m'; m < n \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 1433 by (case_tac n; simp) (case_tac m; simp) 1434 1435lemma subset_drop_Diff_strg: 1436 "(A \<subseteq> C) \<longrightarrow> (A - B \<subseteq> C)" 1437 by blast 1438 1439lemma inj_case_bool: 1440 "inj (case_bool a b) = (a \<noteq> b)" 1441 by (auto dest: inj_onD[where x=True and y=False] intro: inj_onI split: bool.split_asm) 1442 1443lemma foldl_fun_upd: 1444 "foldl (\<lambda>s r. s (r := g r)) f rs = (\<lambda>x. if x \<in> set rs then g x else f x)" 1445 by (induct rs arbitrary: f) (auto simp: fun_eq_iff) 1446 1447lemma all_rv_choice_fn_eq_pred: 1448 "\<lbrakk> \<And>rv. P rv \<Longrightarrow> \<exists>fn. f rv = g fn \<rbrakk> \<Longrightarrow> \<exists>fn. \<forall>rv. P rv \<longrightarrow> f rv = g (fn rv)" 1449 apply (rule_tac x="\<lambda>rv. SOME h. f rv = g h" in exI) 1450 apply (clarsimp split: if_split) 1451 by (meson someI_ex) 1452 1453lemma ex_const_function: 1454 "\<exists>f. \<forall>s. f (f' s) = v" 1455 by force 1456 1457lemma if_Const_helper: 1458 "If P (Con x) (Con y) = Con (If P x y)" 1459 by (simp split: if_split) 1460 1461lemmas if_Some_helper = if_Const_helper[where Con=Some] 1462 1463lemma expand_restrict_map_eq: 1464 "(m |` S = m' |` S) = (\<forall>x. x \<in> S \<longrightarrow> m x = m' x)" 1465 by (simp add: fun_eq_iff restrict_map_def split: if_split) 1466 1467lemma disj_imp_rhs: 1468 "(P \<Longrightarrow> Q) \<Longrightarrow> (P \<or> Q) = Q" 1469 by blast 1470 1471lemma remove1_filter: 1472 "distinct xs \<Longrightarrow> remove1 x xs = filter (\<lambda>y. x \<noteq> y) xs" 1473 by (induct xs) (auto intro!: filter_True [symmetric]) 1474 1475lemma Int_Union_empty: 1476 "(\<And>x. x \<in> S \<Longrightarrow> A \<inter> P x = {}) \<Longrightarrow> A \<inter> (\<Union>x \<in> S. P x) = {}" 1477 by auto 1478 1479lemma UN_Int_empty: 1480 "(\<And>x. x \<in> S \<Longrightarrow> P x \<inter> T = {}) \<Longrightarrow> (\<Union>x \<in> S. P x) \<inter> T = {}" 1481 by auto 1482 1483lemma disjointI: 1484 "\<lbrakk>\<And>x y. \<lbrakk> x \<in> A; y \<in> B \<rbrakk> \<Longrightarrow> x \<noteq> y \<rbrakk> \<Longrightarrow> A \<inter> B = {}" 1485 by auto 1486 1487lemma UN_disjointI: 1488 assumes rl: "\<And>x y. \<lbrakk> x \<in> A; y \<in> B \<rbrakk> \<Longrightarrow> P x \<inter> Q y = {}" 1489 shows "(\<Union>x \<in> A. P x) \<inter> (\<Union>x \<in> B. Q x) = {}" 1490 by (auto dest: rl) 1491 1492lemma UN_set_member: 1493 assumes sub: "A \<subseteq> (\<Union>x \<in> S. P x)" 1494 and nz: "A \<noteq> {}" 1495 shows "\<exists>x \<in> S. P x \<inter> A \<noteq> {}" 1496proof - 1497 from nz obtain z where zA: "z \<in> A" by fastforce 1498 with sub obtain x where "x \<in> S" and "z \<in> P x" by auto 1499 hence "P x \<inter> A \<noteq> {}" using zA by auto 1500 thus ?thesis using sub nz by auto 1501qed 1502 1503lemma append_Cons_cases [consumes 1, case_names pre mid post]: 1504 "\<lbrakk>(x, y) \<in> set (as @ b # bs); 1505 (x, y) \<in> set as \<Longrightarrow> R; 1506 \<lbrakk>(x, y) \<notin> set as; (x, y) \<notin> set bs; (x, y) = b\<rbrakk> \<Longrightarrow> R; 1507 (x, y) \<in> set bs \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 1508 by auto 1509 1510lemma cart_singletons: 1511 "{a} \<times> {b} = {(a, b)}" 1512 by blast 1513 1514lemma disjoint_subset_neg1: 1515 "\<lbrakk> B \<inter> C = {}; A \<subseteq> B; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<not> A \<subseteq> C" 1516 by auto 1517 1518lemma disjoint_subset_neg2: 1519 "\<lbrakk> B \<inter> C = {}; A \<subseteq> C; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<not> A \<subseteq> B" 1520 by auto 1521 1522lemma iffE2: 1523 "\<lbrakk> P = Q; \<lbrakk> P; Q \<rbrakk> \<Longrightarrow> R; \<lbrakk> \<not> P; \<not> Q \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 1524 by blast 1525 1526lemma list_case_If: 1527 "(case xs of [] \<Rightarrow> P | _ \<Rightarrow> Q) = (if xs = [] then P else Q)" 1528 by (rule list.case_eq_if) 1529 1530lemma remove1_Nil_in_set: 1531 "\<lbrakk> remove1 x xs = []; xs \<noteq> [] \<rbrakk> \<Longrightarrow> x \<in> set xs" 1532 by (induct xs) (auto split: if_split_asm) 1533 1534lemma remove1_empty: 1535 "(remove1 v xs = []) = (xs = [v] \<or> xs = [])" 1536 by (cases xs; simp) 1537 1538lemma set_remove1: 1539 "x \<in> set (remove1 y xs) \<Longrightarrow> x \<in> set xs" 1540 by (induct xs) (auto split: if_split_asm) 1541 1542lemma If_rearrage: 1543 "(if P then if Q then x else y else z) = (if P \<and> Q then x else if P then y else z)" 1544 by simp 1545 1546lemma disjI2_strg: 1547 "Q \<longrightarrow> (P \<or> Q)" 1548 by simp 1549 1550lemma eq_imp_strg: 1551 "P t \<longrightarrow> (t = s \<longrightarrow> P s)" 1552 by clarsimp 1553 1554lemma if_both_strengthen: 1555 "P \<and> Q \<longrightarrow> (if G then P else Q)" 1556 by simp 1557 1558lemma if_both_strengthen2: 1559 "P s \<and> Q s \<longrightarrow> (if G then P else Q) s" 1560 by simp 1561 1562lemma if_swap: 1563 "(if P then Q else R) = (if \<not>P then R else Q)" by simp 1564 1565lemma imp_consequent: 1566 "P \<longrightarrow> Q \<longrightarrow> P" by simp 1567 1568lemma list_case_helper: 1569 "xs \<noteq> [] \<Longrightarrow> case_list f g xs = g (hd xs) (tl xs)" 1570 by (cases xs, simp_all) 1571 1572lemma list_cons_rewrite: 1573 "(\<forall>x xs. L = x # xs \<longrightarrow> P x xs) = (L \<noteq> [] \<longrightarrow> P (hd L) (tl L))" 1574 by (auto simp: neq_Nil_conv) 1575 1576lemma list_not_Nil_manip: 1577 "\<lbrakk> xs = y # ys; case xs of [] \<Rightarrow> False | (y # ys) \<Rightarrow> P y ys \<rbrakk> \<Longrightarrow> P y ys" 1578 by simp 1579 1580lemma ran_ball_triv: 1581 "\<And>P m S. \<lbrakk> \<forall>x \<in> (ran S). P x ; m \<in> (ran S) \<rbrakk> \<Longrightarrow> P m" 1582 by blast 1583 1584lemma singleton_tuple_cartesian: 1585 "({(a, b)} = S \<times> T) = ({a} = S \<and> {b} = T)" 1586 "(S \<times> T = {(a, b)}) = ({a} = S \<and> {b} = T)" 1587 by blast+ 1588 1589lemma strengthen_ignore_if: 1590 "A s \<and> B s \<longrightarrow> (if P then A else B) s" 1591 by clarsimp 1592 1593lemma case_sum_True : 1594 "(case r of Inl a \<Rightarrow> True | Inr b \<Rightarrow> f b) = (\<forall>b. r = Inr b \<longrightarrow> f b)" 1595 by (cases r) auto 1596 1597lemma sym_ex_elim: 1598 "F x = y \<Longrightarrow> \<exists>x. y = F x" 1599 by auto 1600 1601lemma tl_drop_1 : 1602 "tl xs = drop 1 xs" 1603 by (simp add: drop_Suc) 1604 1605lemma upt_lhs_sub_map: 1606 "[x ..< y] = map ((+) x) [0 ..< y - x]" 1607 by (induct y) (auto simp: Suc_diff_le) 1608 1609lemma upto_0_to_4: 1610 "[0..<4] = 0 # [1..<4]" 1611 by (subst upt_rec) simp 1612 1613lemma disjEI: 1614 "\<lbrakk> P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> S \<rbrakk> 1615 \<Longrightarrow> R \<or> S" 1616 by fastforce 1617 1618lemma dom_fun_upd2: 1619 "s x = Some z \<Longrightarrow> dom (s (x \<mapsto> y)) = dom s" 1620 by (simp add: insert_absorb domI) 1621 1622lemma foldl_True : 1623 "foldl (\<or>) True bs" 1624 by (induct bs) auto 1625 1626lemma image_set_comp: 1627 "f ` {g x | x. Q x} = (f \<circ> g) ` {x. Q x}" 1628 by fastforce 1629 1630lemma mutual_exE: 1631 "\<lbrakk> \<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> \<exists>x. Q x" 1632 by blast 1633 1634lemma nat_diff_eq: 1635 fixes x :: nat 1636 shows "\<lbrakk> x - y = x - z; y < x\<rbrakk> \<Longrightarrow> y = z" 1637 by arith 1638 1639lemma comp_upd_simp: 1640 "(f \<circ> (g (x := y))) = ((f \<circ> g) (x := f y))" 1641 by (rule fun_upd_comp) 1642 1643lemma dom_option_map: 1644 "dom (map_option f o m) = dom m" 1645 by (rule dom_map_option_comp) 1646 1647lemma drop_imp: 1648 "P \<Longrightarrow> (A \<longrightarrow> P) \<and> (B \<longrightarrow> P)" by blast 1649 1650lemma inj_on_fun_updI2: 1651 "\<lbrakk> inj_on f A; y \<notin> f ` (A - {x}) \<rbrakk> \<Longrightarrow> inj_on (f(x := y)) A" 1652 by (rule inj_on_fun_upd_strongerI) 1653 1654lemma inj_on_fun_upd_elsewhere: 1655 "x \<notin> S \<Longrightarrow> inj_on (f (x := y)) S = inj_on f S" 1656 by (simp add: inj_on_def) blast 1657 1658lemma not_Some_eq_tuple: 1659 "(\<forall>y z. x \<noteq> Some (y, z)) = (x = None)" 1660 by (cases x, simp_all) 1661 1662lemma ran_option_map: 1663 "ran (map_option f o m) = f ` ran m" 1664 by (auto simp add: ran_def) 1665 1666lemma All_less_Ball: 1667 "(\<forall>x < n. P x) = (\<forall>x\<in>{..< n}. P x)" 1668 by fastforce 1669 1670lemma Int_image_empty: 1671 "\<lbrakk> \<And>x y. f x \<noteq> g y \<rbrakk> 1672 \<Longrightarrow> f ` S \<inter> g ` T = {}" 1673 by auto 1674 1675lemma Max_prop: 1676 "\<lbrakk> Max S \<in> S \<Longrightarrow> P (Max S); (S :: ('a :: {finite, linorder}) set) \<noteq> {} \<rbrakk> \<Longrightarrow> P (Max S)" 1677 by auto 1678 1679lemma Min_prop: 1680 "\<lbrakk> Min S \<in> S \<Longrightarrow> P (Min S); (S :: ('a :: {finite, linorder}) set) \<noteq> {} \<rbrakk> \<Longrightarrow> P (Min S)" 1681 by auto 1682 1683lemma findSomeD: 1684 "find P xs = Some x \<Longrightarrow> P x \<and> x \<in> set xs" 1685 by (induct xs) (auto split: if_split_asm) 1686 1687lemma findNoneD: 1688 "find P xs = None \<Longrightarrow> \<forall>x \<in> set xs. \<not>P x" 1689 by (induct xs) (auto split: if_split_asm) 1690 1691lemma dom_upd: 1692 "dom (\<lambda>x. if x = y then None else f x) = dom f - {y}" 1693 by (rule set_eqI) (auto split: if_split_asm) 1694 1695 1696definition 1697 is_inv :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('b \<rightharpoonup> 'a) \<Rightarrow> bool" where 1698 "is_inv f g \<equiv> ran f = dom g \<and> (\<forall>x y. f x = Some y \<longrightarrow> g y = Some x)" 1699 1700lemma is_inv_NoneD: 1701 assumes "g x = None" 1702 assumes "is_inv f g" 1703 shows "x \<notin> ran f" 1704proof - 1705 from assms 1706 have "x \<notin> dom g" by (auto simp: ran_def) 1707 moreover 1708 from assms 1709 have "ran f = dom g" 1710 by (simp add: is_inv_def) 1711 ultimately 1712 show ?thesis by simp 1713qed 1714 1715lemma is_inv_SomeD: 1716 "\<lbrakk> f x = Some y; is_inv f g \<rbrakk> \<Longrightarrow> g y = Some x" 1717 by (simp add: is_inv_def) 1718 1719lemma is_inv_com: 1720 "is_inv f g \<Longrightarrow> is_inv g f" 1721 apply (unfold is_inv_def) 1722 apply safe 1723 apply (clarsimp simp: ran_def dom_def set_eq_iff) 1724 apply (erule_tac x=a in allE) 1725 apply clarsimp 1726 apply (clarsimp simp: ran_def dom_def set_eq_iff) 1727 apply blast 1728 apply (clarsimp simp: ran_def dom_def set_eq_iff) 1729 apply (erule_tac x=x in allE) 1730 apply clarsimp 1731 done 1732 1733lemma is_inv_inj: 1734 "is_inv f g \<Longrightarrow> inj_on f (dom f)" 1735 apply (frule is_inv_com) 1736 apply (clarsimp simp: inj_on_def) 1737 apply (drule (1) is_inv_SomeD) 1738 apply (auto dest: is_inv_SomeD) 1739 done 1740 1741lemma ran_upd': 1742 "\<lbrakk>inj_on f (dom f); f y = Some z\<rbrakk> \<Longrightarrow> ran (f (y := None)) = ran f - {z}" 1743 by (force simp: ran_def inj_on_def dom_def intro!: set_eqI) 1744 1745lemma is_inv_None_upd: 1746 "\<lbrakk> is_inv f g; g x = Some y\<rbrakk> \<Longrightarrow> is_inv (f(y := None)) (g(x := None))" 1747 apply (subst is_inv_def) 1748 apply (clarsimp simp: dom_upd) 1749 apply (drule is_inv_SomeD, erule is_inv_com) 1750 apply (frule is_inv_inj) 1751 apply (auto simp: ran_upd' is_inv_def dest: is_inv_SomeD is_inv_inj) 1752 done 1753 1754lemma is_inv_inj2: 1755 "is_inv f g \<Longrightarrow> inj_on g (dom g)" 1756 using is_inv_com is_inv_inj by blast 1757 1758text \<open>Map inversion (implicitly assuming injectivity).\<close> 1759definition 1760 "the_inv_map m = (\<lambda>s. if s\<in>ran m then Some (THE x. m x = Some s) else None)" 1761 1762text \<open>Map inversion can be expressed by function inversion.\<close> 1763lemma the_inv_map_def2: 1764 "the_inv_map m = (Some \<circ> the_inv_into (dom m) (the \<circ> m)) |` (ran m)" 1765 apply (rule ext) 1766 apply (clarsimp simp: the_inv_map_def the_inv_into_def dom_def) 1767 apply (rule_tac f=The in arg_cong) 1768 apply (rule ext) 1769 apply auto 1770 done 1771 1772text \<open>The domain of a function composition with Some is the universal set.\<close> 1773lemma dom_comp_Some[simp]: "dom (comp Some f) = UNIV" by (simp add: dom_def) 1774 1775text \<open>Assuming injectivity, map inversion produces an inversive map.\<close> 1776lemma is_inv_the_inv_map: 1777 "inj_on m (dom m) \<Longrightarrow> is_inv m (the_inv_map m)" 1778 apply (simp add: is_inv_def) 1779 apply (intro conjI allI impI) 1780 apply (simp add: the_inv_map_def2) 1781 apply (auto simp add: the_inv_map_def inj_on_def dom_def intro: ranI) 1782 done 1783 1784lemma the_the_inv_mapI: 1785 "inj_on m (dom m) \<Longrightarrow> m x = Some y \<Longrightarrow> the (the_inv_map m y) = x" 1786 by (auto simp: the_inv_map_def ran_def inj_on_def dom_def) 1787 1788lemma eq_restrict_map_None: 1789 "restrict_map m A x = None \<longleftrightarrow> x ~: (A \<inter> dom m)" 1790 by (auto simp: restrict_map_def split: if_split_asm) 1791 1792lemma eq_the_inv_map_None[simp]: "the_inv_map m x = None \<longleftrightarrow> x\<notin>ran m" 1793 by (simp add: the_inv_map_def2 eq_restrict_map_None) 1794 1795lemma is_inv_unique: 1796 "is_inv f g \<Longrightarrow> is_inv f h \<Longrightarrow> g=h" 1797 apply (rule ext) 1798 apply (clarsimp simp: is_inv_def dom_def Collect_eq ran_def) 1799 apply (drule_tac x=x in spec)+ 1800 apply (case_tac "g x", clarsimp+) 1801 done 1802 1803lemma range_convergence1: 1804 "\<lbrakk> \<forall>z. x < z \<and> z \<le> y \<longrightarrow> P z; \<forall>z > y. P (z :: 'a :: linorder) \<rbrakk> \<Longrightarrow> \<forall>z > x. P z" 1805 using not_le by blast 1806 1807lemma range_convergence2: 1808 "\<lbrakk> \<forall>z. x < z \<and> z \<le> y \<longrightarrow> P z; \<forall>z. z > y \<and> z < w \<longrightarrow> P (z :: 'a :: linorder) \<rbrakk> 1809 \<Longrightarrow> \<forall>z. z > x \<and> z < w \<longrightarrow> P z" 1810 using range_convergence1[where P="\<lambda>z. z < w \<longrightarrow> P z" and x=x and y=y] 1811 by auto 1812 1813lemma zip_upt_Cons: 1814 "a < b \<Longrightarrow> zip [a ..< b] (x # xs) = (a, x) # zip [Suc a ..< b] xs" 1815 by (simp add: upt_conv_Cons) 1816 1817lemma map_comp_eq: 1818 "f \<circ>\<^sub>m g = case_option None f \<circ> g" 1819 apply (rule ext) 1820 apply (case_tac "g x") 1821 by auto 1822 1823lemma dom_If_Some: 1824 "dom (\<lambda>x. if x \<in> S then Some v else f x) = (S \<union> dom f)" 1825 by (auto split: if_split) 1826 1827lemma foldl_fun_upd_const: 1828 "foldl (\<lambda>s x. s(f x := v)) s xs 1829 = (\<lambda>x. if x \<in> f ` set xs then v else s x)" 1830 by (induct xs arbitrary: s) auto 1831 1832lemma foldl_id: 1833 "foldl (\<lambda>s x. s) s xs = s" 1834 by (induct xs) auto 1835 1836lemma SucSucMinus: "2 \<le> n \<Longrightarrow> Suc (Suc (n - 2)) = n" by arith 1837 1838lemma ball_to_all: 1839 "(\<And>x. (x \<in> A) = (P x)) \<Longrightarrow> (\<forall>x \<in> A. B x) = (\<forall>x. P x \<longrightarrow> B x)" 1840 by blast 1841 1842lemma case_option_If: 1843 "case_option P (\<lambda>x. Q) v = (if v = None then P else Q)" 1844 by clarsimp 1845 1846lemma case_option_If2: 1847 "case_option P Q v = If (v \<noteq> None) (Q (the v)) P" 1848 by (simp split: option.split) 1849 1850lemma if3_fold: 1851 "(if P then x else if Q then y else x) = (if P \<or> \<not> Q then x else y)" 1852 by simp 1853 1854lemma rtrancl_insert: 1855 assumes x_new: "\<And>y. (x,y) \<notin> R" 1856 shows "R^* `` insert x S = insert x (R^* `` S)" 1857proof - 1858 have "R^* `` insert x S = R^* `` ({x} \<union> S)" by simp 1859 also 1860 have "R^* `` ({x} \<union> S) = R^* `` {x} \<union> R^* `` S" 1861 by (subst Image_Un) simp 1862 also 1863 have "R^* `` {x} = {x}" 1864 by (meson Image_closed_trancl Image_singleton_iff subsetI x_new) 1865 finally 1866 show ?thesis by simp 1867qed 1868 1869lemma ran_del_subset: 1870 "y \<in> ran (f (x := None)) \<Longrightarrow> y \<in> ran f" 1871 by (auto simp: ran_def split: if_split_asm) 1872 1873lemma trancl_sub_lift: 1874 assumes sub: "\<And>p p'. (p,p') \<in> r \<Longrightarrow> (p,p') \<in> r'" 1875 shows "(p,p') \<in> r^+ \<Longrightarrow> (p,p') \<in> r'^+" 1876 by (fastforce intro: trancl_mono sub) 1877 1878lemma trancl_step_lift: 1879 assumes x_step: "\<And>p p'. (p,p') \<in> r' \<Longrightarrow> (p,p') \<in> r \<or> (p = x \<and> p' = y)" 1880 assumes y_new: "\<And>p'. \<not>(y,p') \<in> r" 1881 shows "(p,p') \<in> r'^+ \<Longrightarrow> (p,p') \<in> r^+ \<or> ((p,x) \<in> r^+ \<and> p' = y) \<or> (p = x \<and> p' = y)" 1882 apply (erule trancl_induct) 1883 apply (drule x_step) 1884 apply fastforce 1885 apply (erule disjE) 1886 apply (drule x_step) 1887 apply (erule disjE) 1888 apply (drule trancl_trans, drule r_into_trancl, assumption) 1889 apply blast 1890 apply fastforce 1891 apply (fastforce simp: y_new dest: x_step) 1892 done 1893 1894lemma rtrancl_simulate_weak: 1895 assumes r: "(x,z) \<in> R\<^sup>*" 1896 assumes s: "\<And>y. (x,y) \<in> R \<Longrightarrow> (y,z) \<in> R\<^sup>* \<Longrightarrow> (x,y) \<in> R' \<and> (y,z) \<in> R'\<^sup>*" 1897 shows "(x,z) \<in> R'\<^sup>*" 1898 apply (rule converse_rtranclE[OF r]) 1899 apply simp 1900 apply (frule (1) s) 1901 apply clarsimp 1902 by (rule converse_rtrancl_into_rtrancl) 1903 1904lemma list_case_If2: 1905 "case_list f g xs = If (xs = []) f (g (hd xs) (tl xs))" 1906 by (simp split: list.split) 1907 1908lemma length_ineq_not_Nil: 1909 "length xs > n \<Longrightarrow> xs \<noteq> []" 1910 "length xs \<ge> n \<Longrightarrow> n \<noteq> 0 \<longrightarrow> xs \<noteq> []" 1911 "\<not> length xs < n \<Longrightarrow> n \<noteq> 0 \<longrightarrow> xs \<noteq> []" 1912 "\<not> length xs \<le> n \<Longrightarrow> xs \<noteq> []" 1913 by auto 1914 1915lemma numeral_eqs: 1916 "2 = Suc (Suc 0)" 1917 "3 = Suc (Suc (Suc 0))" 1918 "4 = Suc (Suc (Suc (Suc 0)))" 1919 "5 = Suc (Suc (Suc (Suc (Suc 0))))" 1920 "6 = Suc (Suc (Suc (Suc (Suc (Suc 0)))))" 1921 by simp+ 1922 1923lemma psubset_singleton: 1924 "(S \<subset> {x}) = (S = {})" 1925 by blast 1926 1927lemma length_takeWhile_ge: 1928 "length (takeWhile f xs) = n \<Longrightarrow> length xs = n \<or> (length xs > n \<and> \<not> f (xs ! n))" 1929 by (induct xs arbitrary: n) (auto split: if_split_asm) 1930 1931lemma length_takeWhile_le: 1932 "\<not> f (xs ! n) \<Longrightarrow> length (takeWhile f xs) \<le> n" 1933 by (induct xs arbitrary: n; simp) (case_tac n; simp) 1934 1935lemma length_takeWhile_gt: 1936 "n < length (takeWhile f xs) 1937 \<Longrightarrow> (\<exists>ys zs. length ys = Suc n \<and> xs = ys @ zs \<and> takeWhile f xs = ys @ takeWhile f zs)" 1938 apply (induct xs arbitrary: n; simp split: if_split_asm) 1939 apply (case_tac n; simp) 1940 apply (rule_tac x="[a]" in exI) 1941 apply simp 1942 apply (erule meta_allE, drule(1) meta_mp) 1943 apply clarsimp 1944 apply (rule_tac x="a # ys" in exI) 1945 apply simp 1946 done 1947 1948lemma hd_drop_conv_nth2: 1949 "n < length xs \<Longrightarrow> hd (drop n xs) = xs ! n" 1950 by (rule hd_drop_conv_nth) clarsimp 1951 1952lemma map_upt_eq_vals_D: 1953 "\<lbrakk> map f [0 ..< n] = ys; m < length ys \<rbrakk> \<Longrightarrow> f m = ys ! m" 1954 by clarsimp 1955 1956lemma length_le_helper: 1957 "\<lbrakk> n \<le> length xs; n \<noteq> 0 \<rbrakk> \<Longrightarrow> xs \<noteq> [] \<and> n - 1 \<le> length (tl xs)" 1958 by (cases xs, simp_all) 1959 1960lemma all_ex_eq_helper: 1961 "(\<forall>v. (\<exists>v'. v = f v' \<and> P v v') \<longrightarrow> Q v) 1962 = (\<forall>v'. P (f v') v' \<longrightarrow> Q (f v'))" 1963 by auto 1964 1965lemma nat_less_cases': 1966 "(x::nat) < y \<Longrightarrow> x = y - 1 \<or> x < y - 1" 1967 by auto 1968 1969lemma filter_to_shorter_upto: 1970 "n \<le> m \<Longrightarrow> filter (\<lambda>x. x < n) [0 ..< m] = [0 ..< n]" 1971 by (induct m) (auto elim: le_SucE) 1972 1973lemma in_emptyE: "\<lbrakk> A = {}; x \<in> A \<rbrakk> \<Longrightarrow> P" by blast 1974 1975lemma Ball_emptyI: 1976 "S = {} \<Longrightarrow> (\<forall>x \<in> S. P x)" 1977 by simp 1978 1979lemma allfEI: 1980 "\<lbrakk> \<forall>x. P x; \<And>x. P (f x) \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> \<forall>x. Q x" 1981 by fastforce 1982 1983lemma cart_singleton_empty2: 1984 "({x} \<times> S = {}) = (S = {})" 1985 "({} = S \<times> {e}) = (S = {})" 1986 by auto 1987 1988lemma cases_simp_conj: 1989 "((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<and> R) = (Q \<and> R)" 1990 by fastforce 1991 1992lemma domE : 1993 "\<lbrakk> x \<in> dom m; \<And>r. \<lbrakk>m x = Some r\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 1994 by clarsimp 1995 1996lemma dom_eqD: 1997 "\<lbrakk> f x = Some v; dom f = S \<rbrakk> \<Longrightarrow> x \<in> S" 1998 by clarsimp 1999 2000lemma exception_set_finite1: 2001 "finite {x. P x} \<Longrightarrow> finite {x. (x = y \<longrightarrow> Q x) \<and> P x}" 2002 by (simp add: Collect_conj_eq) 2003 2004lemma exception_set_finite2: 2005 "finite {x. P x} \<Longrightarrow> finite {x. x \<noteq> y \<longrightarrow> P x}" 2006 by (simp add: imp_conv_disj) 2007 2008lemmas exception_set_finite = exception_set_finite1 exception_set_finite2 2009 2010lemma exfEI: 2011 "\<lbrakk> \<exists>x. P x; \<And>x. P x \<Longrightarrow> Q (f x) \<rbrakk> \<Longrightarrow> \<exists>x. Q x" 2012 by fastforce 2013 2014lemma Collect_int_vars: 2015 "{s. P rv s} \<inter> {s. rv = xf s} = {s. P (xf s) s} \<inter> {s. rv = xf s}" 2016 by auto 2017 2018lemma if_0_1_eq: 2019 "((if P then 1 else 0) = (case Q of True \<Rightarrow> of_nat 1 | False \<Rightarrow> of_nat 0)) = (P = Q)" 2020 by (simp split: if_split bool.split) 2021 2022lemma modify_map_exists_cte : 2023 "(\<exists>cte. modify_map m p f p' = Some cte) = (\<exists>cte. m p' = Some cte)" 2024 by (simp add: modify_map_def) 2025 2026lemma dom_eqI: 2027 assumes c1: "\<And>x y. P x = Some y \<Longrightarrow> \<exists>y. Q x = Some y" 2028 and c2: "\<And>x y. Q x = Some y \<Longrightarrow> \<exists>y. P x = Some y" 2029 shows "dom P = dom Q" 2030 unfolding dom_def by (auto simp: c1 c2) 2031 2032lemma dvd_reduce_multiple: 2033 fixes k :: nat 2034 shows "(k dvd k * m + n) = (k dvd n)" 2035 by (induct m) (auto simp: add_ac) 2036 2037lemma image_iff2: 2038 "inj f \<Longrightarrow> f x \<in> f ` S = (x \<in> S)" 2039 by (rule inj_image_mem_iff) 2040 2041lemma map_comp_restrict_map_Some_iff: 2042 "((g \<circ>\<^sub>m (m |` S)) x = Some y) = ((g \<circ>\<^sub>m m) x = Some y \<and> x \<in> S)" 2043 by (auto simp add: map_comp_Some_iff restrict_map_Some_iff) 2044 2045lemma range_subsetD: 2046 fixes a :: "'a :: order" 2047 shows "\<lbrakk> {a..b} \<subseteq> {c..d}; a \<le> b \<rbrakk> \<Longrightarrow> c \<le> a \<and> b \<le> d" 2048 by simp 2049 2050lemma case_option_dom: 2051 "(case f x of None \<Rightarrow> a | Some v \<Rightarrow> b v) = (if x \<in> dom f then b (the (f x)) else a)" 2052 by (auto split: option.split) 2053 2054lemma contrapos_imp: 2055 "P \<longrightarrow> Q \<Longrightarrow> \<not> Q \<longrightarrow> \<not> P" 2056 by clarsimp 2057 2058lemma filter_eq_If: 2059 "distinct xs \<Longrightarrow> filter (\<lambda>v. v = x) xs = (if x \<in> set xs then [x] else [])" 2060 by (induct xs) auto 2061 2062lemma (in semigroup_add) foldl_assoc: 2063shows "foldl (+) (x+y) zs = x + (foldl (+) y zs)" 2064 by (induct zs arbitrary: y) (simp_all add:add.assoc) 2065 2066lemma (in monoid_add) foldl_absorb0: 2067shows "x + (foldl (+) 0 zs) = foldl (+) x zs" 2068 by (induct zs) (simp_all add:foldl_assoc) 2069 2070lemma foldl_conv_concat: 2071 "foldl (@) xs xss = xs @ concat xss" 2072proof (induct xss arbitrary: xs) 2073 case Nil show ?case by simp 2074next 2075 interpret monoid_add "(@)" "[]" proof qed simp_all 2076 case Cons then show ?case by (simp add: foldl_absorb0) 2077qed 2078 2079lemma foldl_concat_concat: 2080 "foldl (@) [] (xs @ ys) = foldl (@) [] xs @ foldl (@) [] ys" 2081 by (simp add: foldl_conv_concat) 2082 2083lemma foldl_does_nothing: 2084 "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f s x = s \<rbrakk> \<Longrightarrow> foldl f s xs = s" 2085 by (induct xs) auto 2086 2087lemma foldl_use_filter: 2088 "\<lbrakk> \<And>v x. \<lbrakk> \<not> g x; x \<in> set xs \<rbrakk> \<Longrightarrow> f v x = v \<rbrakk> \<Longrightarrow> foldl f v xs = foldl f v (filter g xs)" 2089 by (induct xs arbitrary: v) auto 2090 2091lemma map_comp_update_lift: 2092 assumes fv: "f v = Some v'" 2093 shows "(f \<circ>\<^sub>m (g(ptr \<mapsto> v))) = ((f \<circ>\<^sub>m g)(ptr \<mapsto> v'))" 2094 by (simp add: fv map_comp_update) 2095 2096lemma restrict_map_cong: 2097 assumes sv: "S = S'" 2098 and rl: "\<And>p. p \<in> S' \<Longrightarrow> mp p = mp' p" 2099 shows "mp |` S = mp' |` S'" 2100 using expand_restrict_map_eq rl sv by auto 2101 2102lemma case_option_over_if: 2103 "case_option P Q (if G then None else Some v) 2104 = (if G then P else Q v)" 2105 "case_option P Q (if G then Some v else None) 2106 = (if G then Q v else P)" 2107 by (simp split: if_split)+ 2108 2109lemma map_length_cong: 2110 "\<lbrakk> length xs = length ys; \<And>x y. (x, y) \<in> set (zip xs ys) \<Longrightarrow> f x = g y \<rbrakk> 2111 \<Longrightarrow> map f xs = map g ys" 2112 apply atomize 2113 apply (erule rev_mp, erule list_induct2) 2114 apply auto 2115 done 2116 2117lemma take_min_len: 2118 "take (min (length xs) n) xs = take n xs" 2119 by (simp add: min_def) 2120 2121lemmas interval_empty = atLeastatMost_empty_iff 2122 2123lemma fold_and_false[simp]: 2124 "\<not>(fold (\<and>) xs False)" 2125 apply clarsimp 2126 apply (induct xs) 2127 apply simp 2128 apply simp 2129 done 2130 2131lemma fold_and_true: 2132 "fold (\<and>) xs True \<Longrightarrow> \<forall>i < length xs. xs ! i" 2133 apply clarsimp 2134 apply (induct xs) 2135 apply simp 2136 apply (case_tac "i = 0"; simp) 2137 apply (case_tac a; simp) 2138 apply (case_tac a; simp) 2139 done 2140 2141lemma fold_or_true[simp]: 2142 "fold (\<or>) xs True" 2143 by (induct xs, simp+) 2144 2145lemma fold_or_false: 2146 "\<not>(fold (\<or>) xs False) \<Longrightarrow> \<forall>i < length xs. \<not>(xs ! i)" 2147 apply (induct xs, simp+) 2148 apply (case_tac a, simp+) 2149 apply (rule allI, case_tac "i = 0", simp+) 2150 done 2151 2152 2153 2154section \<open> Take, drop, zip, list_all etc rules \<close> 2155 2156method two_induct for xs ys = 2157 ((induct xs arbitrary: ys; simp?), (case_tac ys; simp)?) 2158 2159lemma map_fst_zip_prefix: 2160 "map fst (zip xs ys) \<le> xs" 2161 by (two_induct xs ys) 2162 2163lemma map_snd_zip_prefix: 2164 "map snd (zip xs ys) \<le> ys" 2165 by (two_induct xs ys) 2166 2167lemma nth_upt_0 [simp]: 2168 "i < length xs \<Longrightarrow> [0..<length xs] ! i = i" 2169 by simp 2170 2171lemma take_insert_nth: 2172 "i < length xs\<Longrightarrow> insert (xs ! i) (set (take i xs)) = set (take (Suc i) xs)" 2173 by (subst take_Suc_conv_app_nth, assumption, fastforce) 2174 2175lemma zip_take_drop: 2176 "\<lbrakk>n < length xs; length ys = length xs\<rbrakk> \<Longrightarrow> 2177 zip xs (take n ys @ a # drop (Suc n) ys) = 2178 zip (take n xs) (take n ys) @ (xs ! n, a) # zip (drop (Suc n) xs) (drop (Suc n) ys)" 2179 by (subst id_take_nth_drop, assumption, simp) 2180 2181lemma take_nth_distinct: 2182 "\<lbrakk>distinct xs; n < length xs; xs ! n \<in> set (take n xs)\<rbrakk> \<Longrightarrow> False" 2183 by (fastforce simp: distinct_conv_nth in_set_conv_nth) 2184 2185lemma take_drop_append: 2186 "drop a xs = take b (drop a xs) @ drop (a + b) xs" 2187 by (metis append_take_drop_id drop_drop add.commute) 2188 2189lemma drop_take_drop: 2190 "drop a (take (b + a) xs) @ drop (b + a) xs = drop a xs" 2191 by (metis add.commute take_drop take_drop_append) 2192 2193lemma not_prefixI: 2194 "\<lbrakk> xs \<noteq> ys; length xs = length ys\<rbrakk> \<Longrightarrow> \<not> xs \<le> ys" 2195 by (auto elim: prefixE) 2196 2197lemma map_fst_zip': 2198 "length xs \<le> length ys \<Longrightarrow> map fst (zip xs ys) = xs" 2199 by (metis length_map length_zip map_fst_zip_prefix min_absorb1 not_prefixI) 2200 2201lemma zip_take_triv: 2202 "n \<ge> length bs \<Longrightarrow> zip (take n as) bs = zip as bs" 2203 apply (induct bs arbitrary: n as; simp) 2204 apply (case_tac n; simp) 2205 apply (case_tac as; simp) 2206 done 2207 2208lemma zip_take_triv2: 2209 "length as \<le> n \<Longrightarrow> zip as (take n bs) = zip as bs" 2210 apply (induct as arbitrary: n bs; simp) 2211 apply (case_tac n; simp) 2212 apply (case_tac bs; simp) 2213 done 2214 2215lemma zip_take_length: 2216 "zip xs (take (length xs) ys) = zip xs ys" 2217 by (metis order_refl zip_take_triv2) 2218 2219lemma zip_singleton: 2220 "ys \<noteq> [] \<Longrightarrow> zip [a] ys = [(a, ys ! 0)]" 2221 by (case_tac ys, simp_all) 2222 2223lemma zip_append_singleton: 2224 "\<lbrakk>i = length xs; length xs < length ys\<rbrakk> \<Longrightarrow> zip (xs @ [a]) ys = (zip xs ys) @ [(a,ys ! i)]" 2225 by (induct xs; case_tac ys; simp) 2226 (clarsimp simp: zip_append1 zip_take_length zip_singleton) 2227 2228lemma ranE: 2229 "\<lbrakk> v \<in> ran f; \<And>x. f x = Some v \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 2230 by (auto simp: ran_def) 2231 2232lemma ran_map_option_restrict_eq: 2233 "\<lbrakk> x \<in> ran (map_option f o g); x \<notin> ran (map_option f o (g |` (- {y}))) \<rbrakk> 2234 \<Longrightarrow> \<exists>v. g y = Some v \<and> f v = x" 2235 apply (clarsimp simp: elim!: ranE) 2236 apply (rename_tac w z) 2237 apply (case_tac "w = y") 2238 apply clarsimp 2239 apply (erule notE, rule_tac a=w in ranI) 2240 apply (simp add: restrict_map_def) 2241 done 2242 2243lemma map_of_zip_range: 2244 "\<lbrakk>length xs = length ys; distinct xs\<rbrakk> \<Longrightarrow> (\<lambda>x. (the (map_of (zip xs ys) x))) ` set xs = set ys" 2245 apply (clarsimp simp: image_def) 2246 apply (subst ran_map_of_zip [symmetric, where xs=xs and ys=ys]; simp?) 2247 apply (clarsimp simp: ran_def) 2248 apply (rule equalityI) 2249 apply clarsimp 2250 apply (rename_tac x) 2251 apply (frule_tac x=x in map_of_zip_is_Some; fastforce) 2252 apply (clarsimp simp: set_zip) 2253 by (metis domI dom_map_of_zip nth_mem ranE ran_map_of_zip option.sel) 2254 2255lemma map_zip_fst: 2256 "length xs = length ys \<Longrightarrow> map (\<lambda>(x, y). f x) (zip xs ys) = map f xs" 2257 by (two_induct xs ys) 2258 2259lemma map_zip_fst': 2260 "length xs \<le> length ys \<Longrightarrow> map (\<lambda>(x, y). f x) (zip xs ys) = map f xs" 2261 by (metis length_map map_fst_zip' map_zip_fst zip_map_fst_snd) 2262 2263lemma map_zip_snd: 2264 "length xs = length ys \<Longrightarrow> map (\<lambda>(x, y). f y) (zip xs ys) = map f ys" 2265 by (two_induct xs ys) 2266 2267lemma map_zip_snd': 2268 "length ys \<le> length xs \<Longrightarrow> map (\<lambda>(x, y). f y) (zip xs ys) = map f ys" 2269 by (two_induct xs ys) 2270 2271lemma map_of_zip_tuple_in: 2272 "\<lbrakk>(x, y) \<in> set (zip xs ys); distinct xs\<rbrakk> \<Longrightarrow> map_of (zip xs ys) x = Some y" 2273 by (two_induct xs ys) (auto intro: in_set_zipE) 2274 2275lemma in_set_zip1: 2276 "(x, y) \<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs" 2277 by (erule in_set_zipE) 2278 2279lemma in_set_zip2: 2280 "(x, y) \<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys" 2281 by (erule in_set_zipE) 2282 2283lemma map_zip_snd_take: 2284 "map (\<lambda>(x, y). f y) (zip xs ys) = map f (take (length xs) ys)" 2285 apply (subst map_zip_snd' [symmetric, where xs=xs and ys="take (length xs) ys"], simp) 2286 apply (subst zip_take_length [symmetric], simp) 2287 done 2288 2289lemma map_of_zip_is_index: 2290 "\<lbrakk>length xs = length ys; x \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>i. (map_of (zip xs ys)) x = Some (ys ! i)" 2291 apply (induct rule: list_induct2; simp) 2292 apply (rule conjI; clarsimp) 2293 apply (metis nth_Cons_0) 2294 apply (metis nth_Cons_Suc) 2295 done 2296 2297lemma map_of_zip_take_update: 2298 "\<lbrakk>i < length xs; length xs \<le> length ys; distinct xs\<rbrakk> 2299 \<Longrightarrow> map_of (zip (take i xs) ys)(xs ! i \<mapsto> (ys ! i)) = map_of (zip (take (Suc i) xs) ys)" 2300 apply (rule ext, rename_tac x) 2301 apply (case_tac "x=xs ! i"; clarsimp) 2302 apply (rule map_of_is_SomeI[symmetric]) 2303 apply (simp add: map_fst_zip') 2304 apply (force simp add: set_zip) 2305 apply (clarsimp simp: take_Suc_conv_app_nth zip_append_singleton map_add_def split: option.splits) 2306 done 2307 2308(* A weaker version of map_of_zip_is_Some (from HOL). *) 2309lemma map_of_zip_is_Some': 2310 "length xs \<le> length ys \<Longrightarrow> (x \<in> set xs) = (\<exists>y. map_of (zip xs ys) x = Some y)" 2311 apply (subst zip_take_length[symmetric]) 2312 apply (rule map_of_zip_is_Some) 2313 by (metis length_take min_absorb2) 2314 2315lemma map_of_zip_inj: 2316 "\<lbrakk>distinct xs; distinct ys; length xs = length ys\<rbrakk> 2317 \<Longrightarrow> inj_on (\<lambda>x. (the (map_of (zip xs ys) x))) (set xs)" 2318 apply (clarsimp simp: inj_on_def) 2319 apply (subst (asm) map_of_zip_is_Some, assumption)+ 2320 apply clarsimp 2321 apply (clarsimp simp: set_zip) 2322 by (metis nth_eq_iff_index_eq) 2323 2324lemma map_of_zip_inj': 2325 "\<lbrakk>distinct xs; distinct ys; length xs \<le> length ys\<rbrakk> 2326 \<Longrightarrow> inj_on (\<lambda>x. (the (map_of (zip xs ys) x))) (set xs)" 2327 apply (subst zip_take_length[symmetric]) 2328 apply (erule map_of_zip_inj, simp) 2329 by (metis length_take min_absorb2) 2330 2331lemma list_all_nth: 2332 "\<lbrakk>list_all P xs; i < length xs\<rbrakk> \<Longrightarrow> P (xs ! i)" 2333 by (metis list_all_length) 2334 2335lemma list_all_update: 2336 "\<lbrakk>list_all P xs; i < length xs; \<And>x. P x \<Longrightarrow> P (f x)\<rbrakk> 2337 \<Longrightarrow> list_all P (xs [i := f (xs ! i)])" 2338 by (metis length_list_update list_all_length nth_list_update) 2339 2340lemma list_allI: 2341 "\<lbrakk>list_all P xs; \<And>x. P x \<Longrightarrow> P' x\<rbrakk> \<Longrightarrow> list_all P' xs" 2342 by (metis list_all_length) 2343 2344lemma list_all_imp_filter: 2345 "list_all (\<lambda>x. f x \<longrightarrow> g x) xs = list_all (\<lambda>x. g x) [x\<leftarrow>xs . f x]" 2346 by (fastforce simp: Ball_set_list_all[symmetric]) 2347 2348lemma list_all_imp_filter2: 2349 "list_all (\<lambda>x. f x \<longrightarrow> g x) xs = list_all (\<lambda>x. \<not>f x) [x\<leftarrow>xs . (\<lambda>x. \<not>g x) x]" 2350 by (fastforce simp: Ball_set_list_all[symmetric]) 2351 2352lemma list_all_imp_chain: 2353 "\<lbrakk>list_all (\<lambda>x. f x \<longrightarrow> g x) xs; list_all (\<lambda>x. f' x \<longrightarrow> f x) xs\<rbrakk> 2354 \<Longrightarrow> list_all (\<lambda>x. f' x \<longrightarrow> g x) xs" 2355 by (clarsimp simp: Ball_set_list_all [symmetric]) 2356 2357 2358 2359 2360 2361lemma inj_Pair: 2362 "inj_on (Pair x) S" 2363 by (rule inj_onI, simp) 2364 2365lemma inj_on_split: 2366 "inj_on f S \<Longrightarrow> inj_on (\<lambda>x. (z, f x)) S" 2367 by (auto simp: inj_on_def) 2368 2369lemma split_state_strg: 2370 "(\<exists>x. f s = x \<and> P x s) \<longrightarrow> P (f s) s" by clarsimp 2371 2372lemma theD: 2373 "\<lbrakk>the (f x) = y; x \<in> dom f \<rbrakk> \<Longrightarrow> f x = Some y" 2374 by (auto simp add: dom_def) 2375 2376lemma bspec_split: 2377 "\<lbrakk> \<forall>(a, b) \<in> S. P a b; (a, b) \<in> S \<rbrakk> \<Longrightarrow> P a b" 2378 by fastforce 2379 2380lemma set_zip_same: 2381 "set (zip xs xs) = Id \<inter> (set xs \<times> set xs)" 2382 by (induct xs) auto 2383 2384lemma ball_ran_updI: 2385 "(\<forall>x \<in> ran m. P x) \<Longrightarrow> P v \<Longrightarrow> (\<forall>x \<in> ran (m (y \<mapsto> v)). P x)" 2386 by (auto simp add: ran_def) 2387 2388lemma not_psubset_eq: 2389 "\<lbrakk> \<not> A \<subset> B; A \<subseteq> B \<rbrakk> \<Longrightarrow> A = B" 2390 by blast 2391 2392lemma set_as_imp: 2393 "(A \<inter> P \<union> B \<inter> -P) = {s. (s \<in> P \<longrightarrow> s \<in> A) \<and> (s \<notin> P \<longrightarrow> s \<in> B)}" 2394 by auto 2395 2396 2397lemma in_image_op_plus: 2398 "(x + y \<in> (+) x ` S) = ((y :: 'a :: ring) \<in> S)" 2399 by (simp add: image_def) 2400 2401lemma insert_subtract_new: 2402 "x \<notin> S \<Longrightarrow> (insert x S - S) = {x}" 2403 by auto 2404 2405lemma zip_is_empty: 2406 "(zip xs ys = []) = (xs = [] \<or> ys = [])" 2407 by (cases xs; simp) (cases ys; simp) 2408 2409lemma minus_Suc_0_lt: 2410 "a \<noteq> 0 \<Longrightarrow> a - Suc 0 < a" 2411 by simp 2412 2413lemma fst_last_zip_upt: 2414 "zip [0 ..< m] xs \<noteq> [] \<Longrightarrow> 2415 fst (last (zip [0 ..< m] xs)) = (if length xs < m then length xs - 1 else m - 1)" 2416 apply (subst last_conv_nth, assumption) 2417 apply (simp only: One_nat_def) 2418 apply (subst nth_zip) 2419 apply (rule order_less_le_trans[OF minus_Suc_0_lt]) 2420 apply (simp add: zip_is_empty) 2421 apply simp 2422 apply (rule order_less_le_trans[OF minus_Suc_0_lt]) 2423 apply (simp add: zip_is_empty) 2424 apply simp 2425 apply (simp add: min_def zip_is_empty) 2426 done 2427 2428lemma neq_into_nprefix: 2429 "\<lbrakk> x \<noteq> take (length x) y \<rbrakk> \<Longrightarrow> \<not> x \<le> y" 2430 by (clarsimp simp: prefix_def less_eq_list_def) 2431 2432lemma suffix_eqI: 2433 "\<lbrakk> suffix xs as; suffix xs bs; length as = length bs; 2434 take (length as - length xs) as \<le> take (length bs - length xs) bs\<rbrakk> \<Longrightarrow> as = bs" 2435 by (clarsimp elim!: prefixE suffixE) 2436 2437lemma suffix_Cons_mem: 2438 "suffix (x # xs) as \<Longrightarrow> x \<in> set as" 2439 by (metis in_set_conv_decomp suffix_def) 2440 2441lemma distinct_imply_not_in_tail: 2442 "\<lbrakk> distinct list; suffix (y # ys) list\<rbrakk> \<Longrightarrow> y \<notin> set ys" 2443 by (clarsimp simp:suffix_def) 2444 2445lemma list_induct_suffix [case_names Nil Cons]: 2446 assumes nilr: "P []" 2447 and consr: "\<And>x xs. \<lbrakk>P xs; suffix (x # xs) as \<rbrakk> \<Longrightarrow> P (x # xs)" 2448 shows "P as" 2449proof - 2450 define as' where "as' == as" 2451 2452 have "suffix as as'" unfolding as'_def by simp 2453 then show ?thesis 2454 proof (induct as) 2455 case Nil show ?case by fact 2456 next 2457 case (Cons x xs) 2458 2459 show ?case 2460 proof (rule consr) 2461 from Cons.prems show "suffix (x # xs) as" unfolding as'_def . 2462 then have "suffix xs as'" by (auto dest: suffix_ConsD simp: as'_def) 2463 then show "P xs" using Cons.hyps by simp 2464 qed 2465 qed 2466qed 2467 2468text \<open>Parallel etc. and lemmas for list prefix\<close> 2469 2470lemma prefix_induct [consumes 1, case_names Nil Cons]: 2471 fixes prefix 2472 assumes np: "prefix \<le> lst" 2473 and base: "\<And>xs. P [] xs" 2474 and rl: "\<And>x xs y ys. \<lbrakk> x = y; xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)" 2475 shows "P prefix lst" 2476 using np 2477proof (induct prefix arbitrary: lst) 2478 case Nil show ?case by fact 2479next 2480 case (Cons x xs) 2481 2482 have prem: "(x # xs) \<le> lst" by fact 2483 then obtain y ys where lv: "lst = y # ys" 2484 by (rule prefixE, auto) 2485 2486 have ih: "\<And>lst. xs \<le> lst \<Longrightarrow> P xs lst" by fact 2487 2488 show ?case using prem 2489 by (auto simp: lv intro!: rl ih) 2490qed 2491 2492lemma not_prefix_cases: 2493 fixes prefix 2494 assumes pfx: "\<not> prefix \<le> lst" 2495 and c1: "\<lbrakk> prefix \<noteq> []; lst = [] \<rbrakk> \<Longrightarrow> R" 2496 and c2: "\<And>a as x xs. \<lbrakk> prefix = a#as; lst = x#xs; x = a; \<not> as \<le> xs\<rbrakk> \<Longrightarrow> R" 2497 and c3: "\<And>a as x xs. \<lbrakk> prefix = a#as; lst = x#xs; x \<noteq> a\<rbrakk> \<Longrightarrow> R" 2498 shows "R" 2499proof (cases prefix) 2500 case Nil then show ?thesis using pfx by simp 2501next 2502 case (Cons a as) 2503 2504 have c: "prefix = a#as" by fact 2505 2506 show ?thesis 2507 proof (cases lst) 2508 case Nil then show ?thesis 2509 by (intro c1, simp add: Cons) 2510 next 2511 case (Cons x xs) 2512 show ?thesis 2513 proof (cases "x = a") 2514 case True 2515 show ?thesis 2516 proof (intro c2) 2517 show "\<not> as \<le> xs" using pfx c Cons True 2518 by simp 2519 qed fact+ 2520 next 2521 case False 2522 show ?thesis by (rule c3) fact+ 2523 qed 2524 qed 2525qed 2526 2527lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]: 2528 fixes prefix 2529 assumes np: "\<not> prefix \<le> lst" 2530 and base: "\<And>x xs. P (x#xs) []" 2531 and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)" 2532 and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)" 2533 shows "P prefix lst" 2534 using np 2535proof (induct lst arbitrary: prefix) 2536 case Nil then show ?case 2537 by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base) 2538next 2539 case (Cons y ys) 2540 2541 have npfx: "\<not> prefix \<le> (y # ys)" by fact 2542 then obtain x xs where pv: "prefix = x # xs" 2543 by (rule not_prefix_cases) auto 2544 2545 have ih: "\<And>prefix. \<not> prefix \<le> ys \<Longrightarrow> P prefix ys" by fact 2546 2547 show ?case using npfx 2548 by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih) 2549qed 2550 2551lemma rsubst: 2552 "\<lbrakk> P s; s = t \<rbrakk> \<Longrightarrow> P t" 2553 by simp 2554 2555lemma ex_impE: "((\<exists>x. P x) \<longrightarrow> Q) \<Longrightarrow> P x \<Longrightarrow> Q" 2556 by blast 2557 2558lemma option_Some_value_independent: 2559 "\<lbrakk> f x = Some v; \<And>v'. f x = Some v' \<Longrightarrow> f y = Some v' \<rbrakk> \<Longrightarrow> f y = Some v" 2560 by blast 2561 2562text \<open>Some int bitwise lemmas. Helpers for proofs about \<^file>\<open>NatBitwise.thy\<close>\<close> 2563lemma int_2p_eq_shiftl: 2564 "(2::int)^x = 1 << x" 2565 by (simp add: shiftl_int_def) 2566 2567lemma nat_int_mul: 2568 "nat (int a * b) = a * nat b" 2569 by (simp add: nat_mult_distrib) 2570 2571lemma int_shiftl_less_cancel: 2572 "n \<le> m \<Longrightarrow> ((x :: int) << n < y << m) = (x < y << (m - n))" 2573 apply (drule le_Suc_ex) 2574 apply (clarsimp simp: shiftl_int_def power_add) 2575 done 2576 2577lemma int_shiftl_lt_2p_bits: 2578 "0 \<le> (x::int) \<Longrightarrow> x < 1 << n \<Longrightarrow> \<forall>i \<ge> n. \<not> x !! i" 2579 apply (clarsimp simp: shiftl_int_def) 2580 apply (clarsimp simp: bin_nth_eq_mod even_iff_mod_2_eq_zero) 2581 apply (drule_tac z="2^i" in less_le_trans) 2582 apply simp 2583 apply simp 2584 done 2585\<comment> \<open>TODO: The converse should be true as well, but seems hard to prove.\<close> 2586 2587lemma int_eq_test_bit: 2588 "((x :: int) = y) = (\<forall>i. test_bit x i = test_bit y i)" 2589 apply simp 2590 apply (metis bin_eqI) 2591 done 2592lemmas int_eq_test_bitI = int_eq_test_bit[THEN iffD2, rule_format] 2593 2594lemma le_nat_shrink_left: 2595 "y \<le> z \<Longrightarrow> y = Suc x \<Longrightarrow> x < z" 2596 by simp 2597 2598lemma length_ge_split: 2599 "n < length xs \<Longrightarrow> \<exists>x xs'. xs = x # xs' \<and> n \<le> length xs'" 2600 by (cases xs) auto 2601 2602text \<open>Support for defining enumerations on datatypes derived from enumerations\<close> 2603lemma distinct_map_enum: 2604 "\<lbrakk> (\<forall> x y. (F x = F y \<longrightarrow> x = y )) \<rbrakk> 2605 \<Longrightarrow> distinct (map F (enum_class.enum :: 'a :: enum list))" 2606 by (simp add: distinct_map enum_distinct inj_onI) 2607 2608lemma if_option_None_eq: 2609 "((if P then None else Some x) = None) = P" 2610 by (auto split: if_splits) 2611 2612lemma not_in_ran_None_upd: 2613 "x \<notin> ran m \<Longrightarrow> x \<notin> ran (m(y := None))" 2614 by (auto simp: ran_def split: if_split) 2615 2616text \<open>Prevent clarsimp and others from creating Some from not None by folding this and unfolding 2617 again when safe.\<close> 2618 2619definition 2620 "not_None x = (x \<noteq> None)" 2621 2622end 2623