1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory ListLibLemmas 8imports List_Lib LemmaBucket 9begin 10 11(* This theory contains various list results that 12are used in proofs related to the abstract cdt_list.*) 13 14(* Sorting a list given a partial ordering, where 15 elements are only necessarily comparable if 16 relation R holds between them. *) 17locale partial_sort = 18 fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 19 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 20 21 assumes all_comp: "\<And>x y. R x y \<Longrightarrow> (less x y \<or> less y x)" 22 23 (*This is only necessary to guarantee the uniqueness of 24 sorted lists. *) 25 assumes antisym: "\<And>x y. R x y \<Longrightarrow> less x y \<and> less y x \<Longrightarrow> x = y" 26 27 assumes trans: "\<And>x y z. less x y \<Longrightarrow> less y z \<Longrightarrow> less x z" 28 29begin 30 31primrec pinsort :: " 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 32 "pinsort x [] = [x]" | 33 "pinsort x (y#ys) = (if (less x y) then (x#y#ys) else y#(pinsort x ys))" 34 35inductive psorted :: "'a list \<Rightarrow> bool" where 36 Nil [iff]: "psorted []" 37| Cons: "\<forall>y\<in>set xs. less x y \<Longrightarrow> psorted xs \<Longrightarrow> psorted (x # xs)" 38 39definition R_set where 40"R_set S \<equiv> \<forall>x y. x \<in> S \<longrightarrow> y \<in> S \<longrightarrow> R x y" 41 42abbreviation R_list where 43"R_list xs \<equiv> R_set (set xs)" 44 45definition psort :: "'a list \<Rightarrow> 'a list" where 46"psort xs = foldr pinsort xs []" 47 48end 49 50context partial_sort begin 51 52lemma psorted_Cons: "psorted (x#xs) = (psorted xs & (\<forall> y \<in> set xs. less x y))" 53 apply (rule iffI) 54 apply (erule psorted.cases,simp) 55 apply clarsimp 56 apply (rule psorted.Cons,clarsimp+) 57 done 58 59lemma psorted_distinct_set_unique: 60assumes "psorted xs" "distinct xs" "psorted ys" "distinct ys" "set xs = set ys" 61 "R_list xs" 62shows "xs = ys" 63proof - 64 from assms have 1: "length xs = length ys" by (auto dest!: distinct_card) 65 from assms show ?thesis 66 proof(induct rule:list_induct2[OF 1]) 67 case 1 show ?case by simp 68 next 69 case 2 thus ?case 70 by (simp add: psorted_Cons R_set_def) 71 (metis Diff_insert_absorb antisym insertE insert_iff) 72 qed 73qed 74 75 76lemma pinsort_set: "set (pinsort a xs) = insert a (set xs)" 77 apply (induct xs) 78 apply simp 79 apply simp 80 apply blast 81 done 82 83lemma all_comp': "R x y \<Longrightarrow> \<not>less x y \<Longrightarrow> less y x" 84 apply (cut_tac x=x and y=y in all_comp,simp+) 85 done 86 87lemma pinsort_sorted: "R_set (insert a (set xs)) \<Longrightarrow> psorted xs \<Longrightarrow> psorted (pinsort a xs)" 88 apply (induct xs arbitrary: a) 89 apply (simp add: psorted_Cons) 90 apply (simp add: psorted_Cons) 91 apply clarsimp 92 apply (simp add: pinsort_set) 93 apply (intro impI conjI) 94 apply (intro ballI) 95 apply (drule_tac x=x in bspec) 96 apply simp 97 apply (frule(1) trans) 98 apply simp 99 apply (simp add: R_set_def) 100 apply (rule all_comp') 101 apply (simp add: R_set_def) 102 apply simp 103 done 104 105lemma psort_set: "set (psort xs) = set xs" 106 apply (simp add: psort_def) 107 apply (induct xs) 108 apply simp 109 apply (simp add: pinsort_set) 110 done 111 112lemma psort_psorted: "R_list xs \<Longrightarrow> psorted (psort xs)" 113 apply (simp add: psort_def) 114 apply (induct xs) 115 apply simp 116 apply simp 117 apply (cut_tac xs =xs in psort_set) 118 apply (simp add: psort_def) 119 apply (rule pinsort_sorted) 120 apply simp 121 apply (simp add: R_set_def) 122 done 123 124 125lemma insort_length: "length (pinsort a xs) = Suc (length xs)" 126 apply (induct xs) 127 apply simp 128 apply simp 129 done 130 131lemma psort_length: "length (psort xs) = length xs" 132 apply (simp add: psort_def) 133 apply (induct xs) 134 apply simp 135 apply simp 136 apply (simp add: insort_length) 137 done 138 139lemma pinsort_distinct: "\<lbrakk>a \<notin> set xs; distinct xs\<rbrakk> 140 \<Longrightarrow> distinct (pinsort a xs)" 141 apply (induct xs) 142 apply simp 143 apply (clarsimp simp add: pinsort_set) 144 done 145 146lemma psort_distinct: "distinct xs \<Longrightarrow> distinct (psort xs)" 147 apply (simp add: psort_def) 148 apply (induct xs) 149 apply simp 150 apply simp 151 apply (rule pinsort_distinct) 152 apply (fold psort_def) 153 apply (simp add: psort_set)+ 154 done 155 156 157lemma in_can_split: "y \<in> set list \<Longrightarrow> \<exists>ys xs. list = xs @ (y # ys)" 158 apply (induct list) 159 apply simp 160 apply clarsimp 161 apply (elim disjE) 162 apply simp 163 apply force 164 apply simp 165 apply (elim exE) 166 apply simp 167 apply (rule_tac x=ys in exI) 168 apply force 169 done 170 171lemma lsorted_sorted: 172assumes lsorted: "\<And>x y xs ys . list = xs @ (x # y # ys) \<Longrightarrow> less x y" 173shows "psorted list" 174 apply (insert lsorted) 175 apply atomize 176 apply simp 177 apply (induct list) 178 apply simp 179 apply (simp add: psorted_Cons) 180 apply (rule context_conjI) 181 apply (erule meta_mp) 182 apply clarsimp 183 apply (drule_tac x="a#xs" in spec) 184 apply (drule_tac x=x in spec) 185 apply (drule_tac x=y in spec) 186 apply (erule mp) 187 apply force 188 apply (intro ballI) 189 apply clarsimp 190 apply (drule in_can_split) 191 apply (elim exE) 192 apply (drule_tac x="[]" in spec) 193 apply simp 194 apply (case_tac xs) 195 apply simp 196 apply (clarsimp simp add: psorted_Cons) 197 apply (blast intro: trans) 198 done 199 200 201lemma psorted_set: "finite A \<Longrightarrow> R_set A \<Longrightarrow> \<exists>!xs. set xs = A \<and> psorted xs \<and> distinct xs" 202 apply (drule finite_distinct_list) 203 apply clarify 204 apply (rule_tac a="psort xs" in ex1I) 205 apply (auto simp: psorted_distinct_set_unique psort_set psort_psorted psort_distinct) 206done 207 208end 209 210 211text \<open>These list operations roughly correspond to cdt 212 operations.\<close> 213 214lemma after_can_split: "after_in_list list x = Some y \<Longrightarrow> \<exists>ys xs. list = xs @ (x # y # ys)" 215 apply (induct list x rule: after_in_list.induct) 216 apply simp+ 217 apply (simp split: if_split_asm) 218 apply force 219 apply (elim exE) 220 apply simp 221 apply (rule_tac x="ys" in exI) 222 apply simp 223 done 224 225lemma distinct_inj_middle: "distinct list \<Longrightarrow> list = (xa @ x # xb) \<Longrightarrow> list = (ya @ x # yb) \<Longrightarrow> xa = ya \<and> xb = yb" 226 apply (induct list arbitrary: xa ya) 227 apply simp 228 apply clarsimp 229 apply (case_tac "xa") 230 apply simp 231 apply (case_tac "ya") 232 apply simp 233 apply clarsimp 234 apply clarsimp 235 apply (case_tac "ya") 236 apply (simp (no_asm_simp)) 237 apply simp 238 apply clarsimp 239 done 240 241 242lemma after_can_split_distinct: 243 "distinct list \<Longrightarrow> after_in_list list x = Some y \<Longrightarrow> \<exists>!ys. \<exists>!xs. list = xs @ (x # y # ys)" 244 apply (frule after_can_split) 245 apply (elim exE) 246 apply (rule ex1I) 247 apply (rule ex1I) 248 apply assumption 249 apply simp 250 apply (elim ex1E) 251 apply (thin_tac "\<forall>x. P x" for P) 252 apply (frule_tac yb="y#ysa" in distinct_inj_middle,assumption+) 253 apply simp 254 done 255 256 257lemma after_ignore_head: "x \<notin> set list \<Longrightarrow> after_in_list (list @ list') x = after_in_list list' x" 258 apply (induct list x rule: after_in_list.induct) 259 apply simp 260 apply simp 261 apply (case_tac list',simp+) 262 done 263 264 265lemma after_distinct_one_sibling: "distinct list \<Longrightarrow> list = xs @ x # y # ys \<Longrightarrow> after_in_list list x = Some y" 266 apply (induct xs) 267 apply simp 268 apply simp 269 apply clarsimp 270 apply (subgoal_tac "after_in_list ((a # xs) @ (x # y # ys)) x = after_in_list (x # y # ys) x") 271 apply simp 272 apply (rule after_ignore_head) 273 apply simp 274 done 275 276 277lemma (in partial_sort) after_order_sorted: 278assumes after_order: "\<And>x y. after_in_list list x = Some y \<Longrightarrow> less x y" 279assumes distinct: "distinct list" 280shows "psorted list" 281 apply (rule lsorted_sorted) 282 apply (rule after_order) 283 apply (erule after_distinct_one_sibling[OF distinct]) 284 done 285 286lemma hd_not_after_in_list: 287 "\<lbrakk>distinct xs; x \<notin> set xs\<rbrakk> \<Longrightarrow> after_in_list (x # xs) a \<noteq> Some x" 288 apply (induct xs a rule: after_in_list.induct) 289 apply simp+ 290 apply fastforce 291 done 292 293lemma after_in_list_inj: 294 "\<lbrakk>distinct list; after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk> 295 \<Longrightarrow> a = b" 296 apply(induct list) 297 apply(simp) 298 apply(simp) 299 apply(case_tac "a=aa") 300 apply(case_tac list, simp) 301 apply(simp add: hd_not_after_in_list split: if_split_asm) 302 apply(case_tac list, simp) 303 apply(simp add: hd_not_after_in_list split: if_split_asm) 304 done 305 306lemma list_replace_ignore:"a \<notin> set list \<Longrightarrow> list_replace list a b = list" 307 apply (simp add: list_replace_def) 308 apply (induct list,clarsimp+) 309 done 310 311lemma list_replace_empty[simp]: "list_replace [] a b = []" 312 by (simp add: list_replace_def) 313 314lemma list_replace_empty2[simp]: 315 "(list_replace list a b = []) = (list = [])" 316 by (simp add: list_replace_def) 317 318lemma after_in_list_list_replace: "\<lbrakk>p \<noteq> dest; p \<noteq> src; 319 after_in_list list p = Some src\<rbrakk> 320 \<Longrightarrow> after_in_list (list_replace list src dest) p = Some dest" 321 apply (simp add: list_replace_def) 322 apply (induct list) 323 apply simp+ 324 apply (case_tac list) 325 apply simp+ 326 apply (intro conjI impI,simp+) 327 done 328 329lemma replace_list_preserve_after: "dest \<notin> set list \<Longrightarrow> distinct list \<Longrightarrow> after_in_list (list_replace list src dest) dest = after_in_list list src" 330 apply (simp add: list_replace_def) 331 apply (induct list src rule: after_in_list.induct) 332 apply (simp+) 333 apply fastforce 334 done 335 336lemma replace_list_preserve_after': "\<lbrakk>p \<noteq> dest; p \<noteq> src; 337 after_in_list list p \<noteq> Some src\<rbrakk> 338 \<Longrightarrow> after_in_list (list_replace list src dest) p = after_in_list list p" 339 apply (simp add: list_replace_def) 340 apply (induct list p rule: after_in_list.induct) 341 apply (simp+) 342 apply fastforce 343 done 344 345lemma distinct_after_in_list_not_self: 346 "distinct list \<Longrightarrow> after_in_list list src \<noteq> Some src" 347 apply (induct list,simp+) 348 apply (case_tac list,clarsimp+) 349 done 350 351lemma set_list_insert_after: 352 "set (list_insert_after list a b) = set list \<union> (if a \<in> set list then {b} else {})" 353 apply(induct list) 354 apply(simp) 355 apply(simp) 356 done 357 358lemma distinct_list_insert_after: 359 "\<lbrakk>distinct list; b \<notin> set list \<or> a \<notin> set list\<rbrakk> \<Longrightarrow> distinct (list_insert_after list a b)" 360 apply(induct list) 361 apply(simp) 362 apply(fastforce simp: set_list_insert_after) 363 done 364 365lemma list_insert_after_after: 366 "\<lbrakk>distinct list; b \<notin> set list; a \<in> set list\<rbrakk> 367 \<Longrightarrow> after_in_list (list_insert_after list a b) p 368 = (if p = a then Some b else if p = b then after_in_list list a else after_in_list list p)" 369 apply(induct list p rule: after_in_list.induct) 370 apply (simp split: if_split_asm)+ 371 apply fastforce 372 done 373 374lemma list_remove_removed: 375 "set (list_remove list x) = (set list) - {x}" 376 apply (induct list,simp+) 377 apply blast 378 done 379 380 381lemma remove_distinct_helper: "\<lbrakk>distinct (list_remove list x); a \<noteq> x; a \<notin> set list; 382 distinct list\<rbrakk> 383 \<Longrightarrow> a \<notin> set (list_remove list x)" 384 apply (induct list) 385 apply (simp split: if_split_asm)+ 386 done 387 388 389lemma list_remove_distinct: 390 "distinct list \<Longrightarrow> distinct (list_remove list x)" 391 apply (induct list) 392 apply (simp add: remove_distinct_helper split: if_split_asm)+ 393 done 394 395lemma list_remove_none: "x \<notin> set list \<Longrightarrow> list_remove list x = list" 396 apply (induct list) 397 apply clarsimp+ 398 done 399 400lemma replace_distinct: "x \<notin> set list \<Longrightarrow> distinct list \<Longrightarrow> distinct (list_replace list y x)" 401 apply (induct list) 402 apply (simp add: list_replace_def)+ 403 apply blast 404 done 405 406lemma set_list_replace_list: 407 "\<lbrakk>distinct list; slot \<in> set list; slot \<notin> set list'\<rbrakk> 408 \<Longrightarrow> set (list_replace_list list slot list') = set list \<union> set list' - {slot}" 409 apply (induct list) 410 apply auto 411 done 412 413lemma after_in_list_in_list: 414 "after_in_list list a = Some b \<Longrightarrow> b \<in> set list" 415 apply(induct list a arbitrary: b rule: after_in_list.induct) 416 apply (simp split: if_split_asm)+ 417 done 418 419lemma list_replace_empty_after_empty: 420 "\<lbrakk>after_in_list list p = Some slot; distinct list\<rbrakk> 421 \<Longrightarrow> after_in_list (list_replace_list list slot []) p = after_in_list list slot" 422 apply(induct list slot rule: after_in_list.induct) 423 apply (simp split: if_split_asm)+ 424 apply (case_tac xs,simp+) 425 apply (case_tac xs,simp+) 426 apply (auto dest!: after_in_list_in_list) 427 done 428 429lemma list_replace_after_fst_list: 430 "\<lbrakk>after_in_list list p = Some slot; distinct list\<rbrakk> 431 \<Longrightarrow> after_in_list (list_replace_list list slot (x # xs)) p = Some x" 432 apply(induct list p rule: after_in_list.induct) 433 apply (simp split: if_split_asm)+ 434 apply (drule after_in_list_in_list)+ 435 apply force 436 done 437 438lemma after_in_list_append_notin_hd: 439 "p \<notin> set list' \<Longrightarrow> after_in_list (list' @ list) p = after_in_list list p" 440 apply(induct list', simp, simp) 441 apply(case_tac list', simp) 442 apply(case_tac list, simp+) 443 done 444 445lemma after_in_list_append_last_hd: 446 "\<lbrakk>p \<in> set list'; after_in_list list' p = None\<rbrakk> 447 \<Longrightarrow> after_in_list (list' @ x # xs) p = Some x" 448 apply(induct list' p rule: after_in_list.induct) 449 apply(simp) 450 apply(simp) 451 apply(simp split: if_split_asm) 452 done 453 454lemma after_in_list_append_in_hd: 455 "after_in_list list p = Some a \<Longrightarrow> after_in_list (list @ list') p = Some a" 456 apply(induct list p rule: after_in_list.induct) 457 apply(simp split: if_split_asm)+ 458 done 459 460lemma after_in_list_in_list': "after_in_list list a = Some y \<Longrightarrow> a \<in> set list" 461 apply (induct list a rule: after_in_list.induct) 462 apply simp+ 463 apply force 464 done 465 466lemma list_replace_after_None_notin_new: 467 "\<lbrakk>after_in_list list p = None; p \<notin> set list'\<rbrakk> 468 \<Longrightarrow> after_in_list (list_replace_list list slot list') p = None" 469 apply(induct list) 470 apply(simp) 471 apply(simp) 472 apply(intro conjI impI) 473 apply(simp) 474 apply(case_tac list, simp) 475 apply(induct list') 476 apply(simp) 477 apply(simp) 478 apply(case_tac list', simp, simp) 479 apply(simp split: if_split_asm) 480 apply(simp add: after_in_list_append_notin_hd) 481 apply(simp add: after_in_list_append_notin_hd) 482 apply(case_tac "list_replace_list list slot list'") 483 apply(simp) 484 apply(simp) 485 apply(case_tac list, simp, simp split: if_split_asm) 486 done 487 488lemma list_replace_after_notin_new: 489 "\<lbrakk>after_in_list list p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot\<rbrakk> 490 \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a" 491 apply(induct list) 492 apply(simp) 493 apply(simp) 494 apply(intro conjI impI) 495 apply(simp add: after_in_list_append_notin_hd) 496 apply(case_tac list, simp, simp) 497 apply(case_tac list, simp, simp split: if_split_asm) 498 apply(insert after_in_list_append_notin_hd) 499 apply(atomize) 500 apply(erule_tac x=p in allE, erule_tac x="[aa]" in allE, erule_tac x="list' @ lista" in allE) 501 apply(simp) 502 done 503 504lemma list_replace_after_None_notin_old: 505 "\<lbrakk>after_in_list list' p = None; p \<in> set list'; p \<notin> set list\<rbrakk> 506 \<Longrightarrow> after_in_list (list_replace_list list slot list') p = after_in_list list slot" 507 apply(induct list) 508 apply(simp) 509 apply(simp) 510 apply(intro conjI impI) 511 apply(simp) 512 apply(case_tac list) 513 apply(simp) 514 apply(simp add: after_in_list_append_last_hd) 515 apply(case_tac "list_replace_list list slot list'") 516 apply(simp) 517 apply(case_tac list, simp, simp) 518 apply(simp) 519 apply(case_tac list, simp, simp) 520 done 521 522lemma list_replace_after_notin_old: 523 "\<lbrakk>after_in_list list' p = Some a; p \<notin> set list; slot \<in> set list\<rbrakk> 524 \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a" 525 apply(induct list) 526 apply(simp) 527 apply(simp) 528 apply(intro conjI impI) 529 apply(simp add: after_in_list_append_in_hd) 530 apply(simp) 531 apply(case_tac "list_replace_list list slot list'") 532 apply(simp) 533 apply(simp) 534 done 535 536 537lemma list_replace_set: "x \<in> set list \<Longrightarrow> set (list_replace list x y) = insert y (set (list) - {x})" 538 apply (induct list) 539 apply (simp add: list_replace_def)+ 540 apply (intro impI conjI) 541 apply blast+ 542 done 543 544lemma list_swap_both: "x \<in> set list \<Longrightarrow> y \<in> set list \<Longrightarrow> set (list_swap list x y) = set (list)" 545 apply (induct list) 546 apply (simp add: list_swap_def)+ 547 apply (intro impI conjI) 548 apply blast+ 549 done 550 551lemma list_swap_self[simp]: "list_swap list x x = list" 552 apply (simp add: list_swap_def) 553 done 554 555lemma map_ignore: "x \<notin> set list \<Longrightarrow> (map (\<lambda>xa. if xa = x then y else xa) 556 list) = list" 557 apply (induct list) 558 apply simp+ 559 apply blast 560 done 561 562lemma map_ignore2: "y \<notin> set list \<Longrightarrow> (map (\<lambda>xa. if xa = x then y else if xa = y then x else xa) 563 list) = (map (\<lambda>xa. if xa = x then y else xa) list)" 564 apply (simp add: map_ignore) 565 done 566 567lemma map_ignore2': "y \<notin> set list \<Longrightarrow> (map (\<lambda>xa. if xa = y then x else if xa = x then y else xa) 568 list) = (map (\<lambda>xa. if xa = x then y else xa) list)" 569 apply (simp add: map_ignore) 570 apply force 571 done 572 573lemma swap_distinct_helper: "\<lbrakk>x \<in> set list; y \<noteq> x; y \<notin> set list; distinct list\<rbrakk> 574 \<Longrightarrow> distinct (map (\<lambda>xa. if xa = x then y else xa) list)" 575 apply (induct list) 576 apply (simp add: map_ignore | elim conjE | intro impI conjI | blast)+ 577 done 578 579lemma swap_distinct: "x \<in> set list \<Longrightarrow> y \<in> set list \<Longrightarrow> distinct list \<Longrightarrow> distinct (list_swap list x y)" 580 apply (induct list) 581 apply (simp add: list_swap_def)+ 582 apply (intro impI conjI,simp_all) 583 apply (simp add: map_ignore2 map_ignore2' swap_distinct_helper | elim conjE | force)+ 584 done 585 586 587lemma list_swap_none: "x \<notin> set list \<Longrightarrow> y \<notin> set list \<Longrightarrow> list_swap list x y = list" 588 apply (induct list) 589 apply (simp add: list_swap_def)+ 590 apply blast 591 done 592 593lemma list_swap_one: "x \<in> set list \<Longrightarrow> y \<notin> set list \<Longrightarrow> set (list_swap list x y) = insert y (set (list)) - {x}" 594 apply (induct list) 595 apply (simp add: list_swap_def)+ 596 apply (intro impI conjI) 597 apply blast+ 598 done 599 600lemma list_swap_one': "x \<notin> set list \<Longrightarrow> y \<in> set list \<Longrightarrow> set (list_swap list x y) = insert x (set (list)) - {y}" 601 apply (induct list) 602 apply (simp add: list_swap_def)+ 603 apply (intro impI conjI) 604 apply blast+ 605 done 606 607 608lemma in_swapped_list: "y \<in> set list \<Longrightarrow> x \<in> set (list_swap list x y)" 609 apply (case_tac "x \<in> set list") 610 apply (simp add: list_swap_both) 611 apply (simp add: list_swap_one') 612 apply (intro notI,simp) 613 done 614 615lemma list_swap_empty : "(list_swap list x y = []) = (list = [])" 616 by(simp add: list_swap_def) 617 618lemma distinct_after_in_list_antisym: 619 "distinct list \<Longrightarrow> after_in_list list a = Some b \<Longrightarrow> after_in_list list b \<noteq> Some a" 620 apply (induct list b arbitrary: a rule: after_in_list.induct) 621 apply simp+ 622 apply (case_tac xs) 623 apply (clarsimp split: if_split_asm | intro impI conjI)+ 624 done 625 626 627lemma after_in_listD: "after_in_list list x = Some y \<Longrightarrow> \<exists>xs ys. list = xs @ (x # y # ys) \<and> x \<notin> set xs" 628 apply (induct list x arbitrary: a rule: after_in_list.induct) 629 apply (simp split: if_split_asm | elim exE | force)+ 630 apply (rule_tac x="x # xsa" in exI) 631 apply simp 632 done 633 634lemma list_swap_symmetric: "list_swap list a b = list_swap list b a" 635 apply (simp add: list_swap_def) 636 done 637 638lemma list_swap_preserve_after: 639 "\<lbrakk>desta \<notin> set list; distinct list\<rbrakk> 640\<Longrightarrow> after_in_list (list_swap list srca desta) desta = 641 after_in_list list srca" 642 apply (induct list desta rule: after_in_list.induct) 643 apply (simp add: list_swap_def)+ 644 apply force 645 done 646 647lemma list_swap_preserve_after': 648 "\<lbrakk>p \<noteq> desta; p \<noteq> srca; after_in_list list p = Some srca\<rbrakk> 649\<Longrightarrow> after_in_list (list_swap list srca desta) p = Some desta" 650 apply (induct list p rule: after_in_list.induct) 651 apply (simp add: list_swap_def)+ 652 apply force 653 done 654 655lemma list_swap_does_swap: 656 "\<lbrakk>distinct list; after_in_list list desta = Some srca\<rbrakk> 657 \<Longrightarrow> after_in_list (list_swap list srca desta) srca = Some desta" 658 apply (induct list srca rule: after_in_list.induct) 659 apply (simp add: list_swap_def)+ 660 apply (elim conjE) 661 apply (intro impI conjI,simp_all) 662 apply (frule after_in_list_in_list,simp)+ 663 done 664 665lemma list_swap_does_swap': 666 "distinct list \<Longrightarrow> after_in_list list srca = Some desta \<Longrightarrow> 667 after_in_list (list_swap list srca desta) srca = 668 after_in_list list desta" 669 apply (induct list srca rule: after_in_list.induct) 670 apply (simp add: list_swap_def)+ 671 apply (elim conjE) 672 apply (intro impI conjI,simp_all) 673 apply (case_tac xs) 674 apply (clarsimp+)[2] 675 apply (case_tac xs) 676 apply clarsimp+ 677done 678 679lemmas list_swap_preserve_after'' = list_swap_preserve_after'[simplified list_swap_symmetric] 680 681lemma list_swap_preserve_Some_other: 682 "\<lbrakk>z \<noteq> desta; z \<noteq> srca; after_in_list list srca = Some z\<rbrakk> 683\<Longrightarrow> after_in_list (list_swap list srca desta) desta = Some z" 684 apply (induct list srca rule: after_in_list.induct) 685 apply (simp add: list_swap_def)+ 686 apply force 687 done 688 689 690lemmas list_swap_preserve_Some_other' = list_swap_preserve_Some_other[simplified list_swap_symmetric] 691 692lemma list_swap_preserve_None: 693 "\<lbrakk>after_in_list list srca = None\<rbrakk> 694\<Longrightarrow> after_in_list (list_swap list desta srca) desta = None" 695 apply (induct list srca rule: after_in_list.induct) 696 apply (simp add: list_swap_def)+ 697 apply force 698 done 699 700lemma list_swap_preserve_None': 701 "\<lbrakk>after_in_list list srca = None\<rbrakk> 702\<Longrightarrow> after_in_list (list_swap list srca desta) desta = None" 703 apply (subst list_swap_symmetric) 704 apply (erule list_swap_preserve_None) 705 done 706 707lemma list_swap_preserve_after_None: 708 "\<lbrakk>p \<noteq> desta; p \<noteq> srca; after_in_list list p = None\<rbrakk> 709\<Longrightarrow> after_in_list (list_swap list srca desta) p = None" 710 apply (induct list p rule: after_in_list.induct) 711 apply (simp add: list_swap_def)+ 712 apply force 713 done 714 715lemma list_swap_preserve_Some_other_distinct: 716 "\<lbrakk>distinct list; z \<noteq> desta; after_in_list list srca = Some z\<rbrakk> 717\<Longrightarrow> after_in_list (list_swap list srca desta) desta = Some z" 718 apply (rule list_swap_preserve_Some_other) 719 apply simp+ 720 apply (rule notI) 721 apply simp 722 apply (frule distinct_after_in_list_not_self[where src=srca]) 723 apply simp+ 724 done 725 726lemma list_swap_preserve_separate: 727 "\<lbrakk>p \<noteq> desta; p \<noteq> srca; z \<noteq> desta; z \<noteq> srca; after_in_list list p = Some z\<rbrakk> 728\<Longrightarrow> after_in_list (list_swap list srca desta) p = Some z" 729 apply (induct list p rule: after_in_list.induct) 730 apply (simp add: list_swap_def split: if_split_asm)+ 731 apply (intro impI conjI) 732 apply simp+ 733 done 734 735fun after_in_list_list where 736 "after_in_list_list [] a = []" | 737 "after_in_list_list (x # xs) a = (if a = x then xs else after_in_list_list xs a)" 738 739lemma after_in_list_list_in_list: 740 notes split_paired_All[simp del] split_paired_Ex[simp del] 741 shows "y \<in> set (after_in_list_list list x) \<Longrightarrow> y \<in> set list" 742 apply(induct list arbitrary:x y) 743 apply(simp) 744 apply(case_tac "x=a", simp+) 745done 746 747lemma range_nat_relation_induct: 748"\<lbrakk> m = Suc (n + k) ; m < cap ; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n ); 749 \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k \<rbrakk> \<Longrightarrow> P n m" 750 apply (clarify) 751 apply (thin_tac "m = t" for t) 752 apply (induct k) 753 apply (drule_tac x = "n" in spec) 754 apply (erule impE, simp, simp) 755 apply (frule_tac x = "Suc (n + k)" in spec) 756 apply (erule impE) 757 apply (simp only: add_Suc_right) 758 apply (rotate_tac 3, frule_tac x = n in spec) 759 apply (rotate_tac -1, drule_tac x = "Suc (n + k)" in spec) 760 apply (rotate_tac -1, drule_tac x = "Suc (n + Suc k) " in spec) 761 apply (erule impE) 762 apply (intro conjI) 763 apply (rule_tac y = "Suc (n + Suc k)" in less_trans) 764 apply (rule less_SucI) 765 apply (simp only: add_Suc_right)+ 766done 767 768lemma indexed_trancl_as_set_helper : "\<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; 769 q = Suc (p + k); Suc n < length list\<rbrakk> 770 \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p <length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+" 771 apply (induct k arbitrary: p q a b) 772 apply (rule r_into_trancl,simp, rule_tac x = p in exI, simp) 773 apply (atomize) 774 apply (erule_tac x = p in allE, erule_tac x = "Suc (p + k)" in allE, erule_tac x = "a" in allE, erule_tac x = "list ! Suc (p + k)" in allE) 775 apply (elim impE) 776 apply (simp)+ 777 apply (rule_tac b = "list ! Suc (p + k)" in trancl_into_trancl) 778 apply (simp)+ 779 apply (rule_tac x = "Suc (p + k)" in exI, simp) 780 done 781 782lemma indexed_trancl_as_set: "distinct list \<Longrightarrow> {(i, j). \<exists> p q. p < q \<and> q < length list \<and> list ! p = i \<and> list ! q = j } 783 = {(i, j). \<exists> p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j }\<^sup>+" 784 apply (rule equalityI) 785 apply (rule subsetI) 786 apply (case_tac x, simp) 787 apply (elim exE conjE) 788 apply (frule less_imp_Suc_add) 789 apply (erule exE) 790 apply (rule_tac cap = "length list" and m = q and n = p and k = k in range_nat_relation_induct) 791 apply (simp) 792 apply (simp) 793 apply (rule allI, rule impI) 794 apply (rule_tac p = p and q = q and k = k and n = n in indexed_trancl_as_set_helper) 795 apply (simp)+ 796 apply (rule subsetI) 797 apply (case_tac x, simp) 798 apply (erule trancl_induct) 799 apply (simp, elim exE conjE) 800 apply (rule_tac x = p in exI, rule_tac x = "Suc p" in exI, simp) 801 apply (simp) 802 apply (rotate_tac 4, erule exE, rule_tac x = p in exI) 803 apply (erule exE, rule_tac x = "Suc pa" in exI) 804 apply (intro conjI) 805 defer 806 apply (simp) 807 apply (erule exE, simp) 808 apply (simp) 809 apply (erule exE) 810 apply (subgoal_tac "pa = q") 811 apply (simp) 812 apply (frule_tac xs = list and i = pa and j = q in nth_eq_iff_index_eq) 813 apply (simp)+ 814done 815 816lemma indexed_trancl_irrefl: "distinct list \<Longrightarrow> (x,x) \<notin> {(i, j). \<exists> p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j }\<^sup>+" 817 apply (frule indexed_trancl_as_set [THEN sym]) 818 apply (simp) 819 apply (intro allI impI notI) 820 apply (frule_tac xs = list and i = p and j = q in nth_eq_iff_index_eq) 821 apply (simp+) 822done 823 824lemma after_in_list_trancl_indexed_trancl: "distinct list \<Longrightarrow> {(p, q). after_in_list list p = Some q}\<^sup>+ = {(i, j). \<exists> p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j }\<^sup>+" 825 apply (rule_tac f = "\<lambda> x. x\<^sup>+" in arg_cong) 826 apply (intro equalityI subsetI) 827 828 apply (case_tac x, simp) 829 apply (induct list) 830 apply (simp) 831 apply (case_tac "a = aa") 832 apply (rule_tac x = 0 in exI, case_tac list, simp, simp) 833 apply (case_tac list, simp, simp) 834 apply (atomize, drule_tac x = x in spec, drule_tac x = aa in spec, drule_tac x = b in spec, simp) 835 apply (erule exE, rule_tac x = "Suc p" in exI, simp) 836 837 apply (case_tac x, simp) 838 apply (induct list) 839 apply (simp) 840 apply (case_tac "a = aa") 841 apply (erule exE) 842 apply (subgoal_tac "p = 0") 843 apply (case_tac list, simp, simp) 844 apply (subgoal_tac "distinct (aa # list)") 845 apply (frule_tac i = 0 and j = p and xs = "aa # list" in nth_eq_iff_index_eq) 846 apply (simp, simp, simp, simp) 847 apply (atomize, drule_tac x = x in spec, drule_tac x = aa in spec, drule_tac x = b in spec, simp) 848 apply (drule mp) 849 apply (erule exE) 850 apply (case_tac p, simp, simp) 851 apply (rule_tac x = nat in exI, simp) 852 apply (case_tac list, simp, simp) 853done 854 855lemma distinct_after_in_list_not_self_trancl: 856 notes split_paired_All[simp del] split_paired_Ex[simp del] 857 shows "distinct list \<Longrightarrow> (x, x) \<notin> {(p, q). after_in_list list p = Some q}\<^sup>+" 858 by (simp add: after_in_list_trancl_indexed_trancl indexed_trancl_irrefl) 859 860lemma distinct_after_in_list_in_list_trancl: 861 notes split_paired_All[simp del] split_paired_Ex[simp del] 862 shows "\<lbrakk>distinct list; (x, y) \<in> {(p, q). after_in_list list q = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> x \<in> set list" 863 by(erule tranclE2, (drule CollectD, simp, drule after_in_list_in_list, simp)+) 864 865 866lemma after_in_list_trancl_prepend: 867 notes split_paired_All[simp del] split_paired_Ex[simp del] 868 shows "\<lbrakk>distinct (y # list); x \<in> set list\<rbrakk> \<Longrightarrow> (y, x) \<in> {(n, p). after_in_list (y # list) n = Some p}\<^sup>+" 869 apply(induct list arbitrary:x y) 870 apply(simp) 871 apply(case_tac "x=a") 872 apply(rule r_into_trancl) 873 apply(simp) 874 apply(drule set_ConsD) 875 apply(elim disjE) 876 apply(simp) 877 apply(atomize) 878 apply(drule_tac x=x in spec) 879 apply(drule_tac x=y in spec) 880 apply(drule_tac mp) 881 apply(simp) 882 apply(drule_tac mp) 883 apply(simp) 884 apply(erule trancl_induct) 885 apply(drule CollectD, simp) 886 apply(rule_tac b = a in trancl_into_trancl2) 887 apply(simp) 888 apply(rule r_into_trancl) 889 apply(rule_tac a = "(a,ya)" in CollectI) 890 apply(clarsimp) 891 apply(case_tac list) 892 apply(simp) 893 apply(simp) 894 apply(case_tac "ya=a") 895 apply(drule CollectD) 896 apply(simp del:after_in_list.simps) 897 apply(drule after_in_list_in_list') 898 apply(simp) 899 apply(rule_tac b=ya in trancl_into_trancl) 900 apply(simp) 901 apply(drule CollectD) 902 apply(rule CollectI) 903 apply(case_tac "ya=y") 904 apply(frule_tac x=y in distinct_after_in_list_not_self_trancl) 905 apply(simp) 906 apply(case_tac list) 907 apply(simp) 908 apply(simp) 909done 910 911lemma after_in_list_append_not_hd: 912 notes split_paired_All[simp del] split_paired_Ex[simp del] 913 shows "a \<noteq> x \<Longrightarrow> after_in_list (a # list) x = after_in_list list x" 914by (case_tac list, simp, simp) 915 916lemma trancl_Collect_rev: 917 "(a, b) \<in> {(x, y). P x y}\<^sup>+ \<Longrightarrow> (b, a) \<in> {(x, y). P y x}\<^sup>+" 918 apply(induct rule: trancl_induct) 919 apply(fastforce intro: trancl_into_trancl2)+ 920 done 921 922 923lemma prepend_after_in_list_distinct : "distinct (a # list) \<Longrightarrow> {(next, p). after_in_list (a # list) p = Some next}\<^sup>+ = 924 {(next, p). after_in_list (list) p = Some next}\<^sup>+ \<union> 925 set list \<times> {a} " 926 apply (rule equalityI) 927 (* \<subseteq> direction *) 928 apply (rule subsetI, case_tac x) 929 apply (simp) 930 apply (erule trancl_induct) 931 (* base case *) 932 apply (drule CollectD, simp) 933 apply (case_tac list, simp) 934 apply (simp split:if_split_asm) 935 apply (rule r_into_trancl) 936 apply (rule CollectI, simp) 937 (* Inductive case *) 938 apply (drule CollectD, simp) 939 apply (erule disjE) 940 apply (case_tac "a \<noteq> z") 941 apply (rule disjI1) 942 apply (rule_tac b =y in trancl_into_trancl) 943 apply (simp, case_tac list, simp, simp) 944 945 apply (simp) 946 apply (rule disjI2) 947 apply (erule conjE) 948 apply (frule_tac x = aa and y = y in distinct_after_in_list_in_list_trancl) 949 apply (simp) 950 apply (simp) 951 apply (subgoal_tac "after_in_list (a # list) z \<noteq> Some a", simp) 952 apply (rule_tac hd_not_after_in_list, simp, simp) 953(* \<supseteq> direction *) 954 apply (rule subsetI) 955 apply (case_tac x) 956 apply (simp) 957 apply (erule disjE) 958 (* transitive case *) 959 apply (erule tranclE2) 960 apply (drule CollectD, simp) 961 apply (subgoal_tac "b \<noteq> a") 962 apply (rule r_into_trancl) 963 apply (rule CollectI, simp) 964 apply (case_tac list, simp, simp) 965 apply (frule after_in_list_in_list') 966 apply (erule conjE) 967 apply (blast) 968 apply (rule_tac y = c in trancl_trans) 969 apply (subgoal_tac "c \<noteq> a") 970 apply (case_tac list, simp, simp) 971 apply (case_tac "aaa = aa") 972 apply (rule r_into_trancl) 973 apply (rule CollectI, simp) 974 975 apply (rule r_into_trancl) 976 apply (rule CollectI, simp) 977 apply (erule CollectE, simp) 978 apply (frule after_in_list_in_list') 979 apply (erule conjE, blast) 980 apply (erule trancl_induct) 981 apply (simp) 982 apply (rule r_into_trancl, simp) 983 apply (subgoal_tac "y \<noteq> a") 984 apply (case_tac list, simp, simp) 985 apply (rotate_tac 3) 986 apply (frule after_in_list_in_list') 987 apply (erule conjE, blast) 988 apply (rule_tac b = y in trancl_into_trancl, simp) 989 apply (rule CollectI, simp) 990 apply (subgoal_tac "a \<noteq> z") 991 apply (case_tac list, simp, simp) 992 apply (rotate_tac 3) 993 apply (frule after_in_list_in_list') 994 apply (blast) 995(* not so transitive case *) 996 apply (subgoal_tac "distinct (a # list)") 997 apply (frule_tac x = aa in after_in_list_trancl_prepend, simp, simp) 998 apply (rule trancl_Collect_rev, simp) 999 apply (simp) 1000done 1001 1002lemma after_in_list_in_cons: 1003 notes split_paired_All[simp del] split_paired_Ex[simp del] 1004 shows "\<lbrakk>after_in_list (x # xs) y = Some z; distinct (x # xs); y \<in> set xs\<rbrakk> \<Longrightarrow> z \<in> set xs" 1005 apply(case_tac "y=x") 1006 apply(simp) 1007 apply(simp add:after_in_list_append_not_hd after_in_list_in_list) 1008done 1009 1010lemma after_in_list_list_set: 1011 notes split_paired_All[simp del] split_paired_Ex[simp del] 1012 shows "distinct list \<Longrightarrow> 1013 set (after_in_list_list list x) 1014 = {a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}" 1015 apply(intro equalityI) 1016 (* \<subseteq> *) 1017 apply(induct list arbitrary:x) 1018 apply(simp) 1019 apply(atomize) 1020 apply(simp) 1021 apply(rule conjI, rule impI, rule subsetI) 1022 apply(rule_tac a = xa in CollectI) 1023 apply(rule trancl_Collect_rev) 1024 apply(rule after_in_list_trancl_prepend) 1025 apply(simp) 1026 apply(simp) 1027 apply(clarify) 1028 apply(drule_tac x=x in spec) 1029 apply(drule_tac B="{a. (a, x) \<in> {(next, p). after_in_list list p = Some next}\<^sup>+}" in set_rev_mp) 1030 apply(simp) 1031 apply(drule CollectD) 1032 apply(simp add:prepend_after_in_list_distinct) 1033 (* \<supseteq> *) 1034 apply(clarsimp) 1035 apply(drule trancl_Collect_rev) 1036 apply(erule trancl_induct) 1037 (* base *) 1038 apply(simp) 1039 apply(induct list arbitrary:x) 1040 apply(simp) 1041 apply(case_tac "a=x") 1042 apply(frule_tac src=x in distinct_after_in_list_not_self) 1043 apply(simp) 1044 apply(drule after_in_list_in_list) 1045 apply(simp)+ 1046 apply(drule_tac list=list in after_in_list_append_not_hd) 1047 apply(simp) 1048 (* inductive *) 1049 apply(simp) 1050 apply(drule trancl_Collect_rev) 1051 apply(induct list arbitrary: x) 1052 apply(simp) 1053 apply(case_tac "a\<noteq>x") 1054 (* a\<noteq>x *) 1055 apply(atomize, drule_tac x=y in spec, drule_tac x=z in spec, drule_tac x=x in spec) 1056 apply(simp add:prepend_after_in_list_distinct) 1057 apply(case_tac "a=y") 1058 apply(simp add:after_in_list_list_in_list) 1059 apply(simp add:after_in_list_append_not_hd) 1060 (* a=x *) 1061 apply(frule after_in_list_in_cons, simp+) 1062done 1063 1064lemma list_eq_after_in_list': 1065 "\<lbrakk> distinct xs; p = xs ! i; i < length xs \<rbrakk> 1066 \<Longrightarrow> \<exists>list. xs = list @ p # after_in_list_list xs p" 1067 apply (induct xs arbitrary: i) 1068 apply (simp) 1069 apply (atomize) 1070 apply (case_tac i) 1071 apply (simp) 1072 apply (drule_tac x = nat in spec, simp) 1073 apply (erule exE, rule impI, rule_tac x = "a # list" in exI) 1074 apply (simp) 1075done 1076 1077lemma after_in_list_last_None: 1078 "distinct list \<Longrightarrow> after_in_list list (last list) = None" 1079 apply(induct list) 1080 apply(simp) 1081 apply(case_tac list) 1082 apply(simp) 1083 apply(fastforce split: if_split_asm) 1084 done 1085 1086lemma after_in_list_None_last: 1087 "\<lbrakk>after_in_list list x = None; x \<in> set list\<rbrakk> \<Longrightarrow> x = last list" 1088 by (induct list x rule: after_in_list.induct,(simp split: if_split_asm)+) 1089 1090end 1091