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