1(* Title: ZF/List.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1994 University of Cambridge 4*) 5 6section\<open>Lists in Zermelo-Fraenkel Set Theory\<close> 7 8theory List imports Datatype ArithSimp begin 9 10consts 11 list :: "i=>i" 12 13datatype 14 "list(A)" = Nil | Cons ("a \<in> A", "l \<in> list(A)") 15 16 17syntax 18 "_Nil" :: i (\<open>[]\<close>) 19 "_List" :: "is => i" (\<open>[(_)]\<close>) 20 21translations 22 "[x, xs]" == "CONST Cons(x, [xs])" 23 "[x]" == "CONST Cons(x, [])" 24 "[]" == "CONST Nil" 25 26 27consts 28 length :: "i=>i" 29 hd :: "i=>i" 30 tl :: "i=>i" 31 32primrec 33 "length([]) = 0" 34 "length(Cons(a,l)) = succ(length(l))" 35 36primrec 37 "hd([]) = 0" 38 "hd(Cons(a,l)) = a" 39 40primrec 41 "tl([]) = []" 42 "tl(Cons(a,l)) = l" 43 44 45consts 46 map :: "[i=>i, i] => i" 47 set_of_list :: "i=>i" 48 app :: "[i,i]=>i" (infixr \<open>@\<close> 60) 49 50(*map is a binding operator -- it applies to meta-level functions, not 51object-level functions. This simplifies the final form of term_rec_conv, 52although complicating its derivation.*) 53primrec 54 "map(f,[]) = []" 55 "map(f,Cons(a,l)) = Cons(f(a), map(f,l))" 56 57primrec 58 "set_of_list([]) = 0" 59 "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))" 60 61primrec 62 app_Nil: "[] @ ys = ys" 63 app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)" 64 65 66consts 67 rev :: "i=>i" 68 flat :: "i=>i" 69 list_add :: "i=>i" 70 71primrec 72 "rev([]) = []" 73 "rev(Cons(a,l)) = rev(l) @ [a]" 74 75primrec 76 "flat([]) = []" 77 "flat(Cons(l,ls)) = l @ flat(ls)" 78 79primrec 80 "list_add([]) = 0" 81 "list_add(Cons(a,l)) = a #+ list_add(l)" 82 83consts 84 drop :: "[i,i]=>i" 85 86primrec 87 drop_0: "drop(0,l) = l" 88 drop_succ: "drop(succ(i), l) = tl (drop(i,l))" 89 90 91(*** Thanks to Sidi Ehmety for the following ***) 92 93definition 94(* Function `take' returns the first n elements of a list *) 95 take :: "[i,i]=>i" where 96 "take(n, as) == list_rec(\<lambda>n\<in>nat. [], 97 %a l r. \<lambda>n\<in>nat. nat_case([], %m. Cons(a, r`m), n), as)`n" 98 99definition 100 nth :: "[i, i]=>i" where 101 \<comment> \<open>returns the (n+1)th element of a list, or 0 if the 102 list is too short.\<close> 103 "nth(n, as) == list_rec(\<lambda>n\<in>nat. 0, 104 %a l r. \<lambda>n\<in>nat. nat_case(a, %m. r`m, n), as) ` n" 105 106definition 107 list_update :: "[i, i, i]=>i" where 108 "list_update(xs, i, v) == list_rec(\<lambda>n\<in>nat. Nil, 109 %u us vs. \<lambda>n\<in>nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i" 110 111consts 112 filter :: "[i=>o, i] => i" 113 upt :: "[i, i] =>i" 114 115primrec 116 "filter(P, Nil) = Nil" 117 "filter(P, Cons(x, xs)) = 118 (if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))" 119 120primrec 121 "upt(i, 0) = Nil" 122 "upt(i, succ(j)) = (if i \<le> j then upt(i, j)@[j] else Nil)" 123 124definition 125 min :: "[i,i] =>i" where 126 "min(x, y) == (if x \<le> y then x else y)" 127 128definition 129 max :: "[i, i] =>i" where 130 "max(x, y) == (if x \<le> y then y else x)" 131 132(*** Aspects of the datatype definition ***) 133 134declare list.intros [simp,TC] 135 136(*An elimination rule, for type-checking*) 137inductive_cases ConsE: "Cons(a,l) \<in> list(A)" 138 139lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) \<longleftrightarrow> a \<in> A & l \<in> list(A)" 140by (blast elim: ConsE) 141 142(*Proving freeness results*) 143lemma Cons_iff: "Cons(a,l)=Cons(a',l') \<longleftrightarrow> a=a' & l=l'" 144by auto 145 146lemma Nil_Cons_iff: "~ Nil=Cons(a,l)" 147by auto 148 149lemma list_unfold: "list(A) = {0} + (A * list(A))" 150by (blast intro!: list.intros [unfolded list.con_defs] 151 elim: list.cases [unfolded list.con_defs]) 152 153 154(** Lemmas to justify using "list" in other recursive type definitions **) 155 156lemma list_mono: "A<=B ==> list(A) \<subseteq> list(B)" 157apply (unfold list.defs ) 158apply (rule lfp_mono) 159apply (simp_all add: list.bnd_mono) 160apply (assumption | rule univ_mono basic_monos)+ 161done 162 163(*There is a similar proof by list induction.*) 164lemma list_univ: "list(univ(A)) \<subseteq> univ(A)" 165apply (unfold list.defs list.con_defs) 166apply (rule lfp_lowerbound) 167apply (rule_tac [2] A_subset_univ [THEN univ_mono]) 168apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ) 169done 170 171(*These two theorems justify datatypes involving list(nat), list(A), ...*) 172lemmas list_subset_univ = subset_trans [OF list_mono list_univ] 173 174lemma list_into_univ: "[| l \<in> list(A); A \<subseteq> univ(B) |] ==> l \<in> univ(B)" 175by (blast intro: list_subset_univ [THEN subsetD]) 176 177lemma list_case_type: 178 "[| l \<in> list(A); 179 c \<in> C(Nil); 180 !!x y. [| x \<in> A; y \<in> list(A) |] ==> h(x,y): C(Cons(x,y)) 181 |] ==> list_case(c,h,l) \<in> C(l)" 182by (erule list.induct, auto) 183 184lemma list_0_triv: "list(0) = {Nil}" 185apply (rule equalityI, auto) 186apply (induct_tac x, auto) 187done 188 189 190(*** List functions ***) 191 192lemma tl_type: "l \<in> list(A) ==> tl(l) \<in> list(A)" 193apply (induct_tac "l") 194apply (simp_all (no_asm_simp) add: list.intros) 195done 196 197(** drop **) 198 199lemma drop_Nil [simp]: "i \<in> nat ==> drop(i, Nil) = Nil" 200apply (induct_tac "i") 201apply (simp_all (no_asm_simp)) 202done 203 204lemma drop_succ_Cons [simp]: "i \<in> nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)" 205apply (rule sym) 206apply (induct_tac "i") 207apply (simp (no_asm)) 208apply (simp (no_asm_simp)) 209done 210 211lemma drop_type [simp,TC]: "[| i \<in> nat; l \<in> list(A) |] ==> drop(i,l) \<in> list(A)" 212apply (induct_tac "i") 213apply (simp_all (no_asm_simp) add: tl_type) 214done 215 216declare drop_succ [simp del] 217 218 219(** Type checking -- proved by induction, as usual **) 220 221lemma list_rec_type [TC]: 222 "[| l \<in> list(A); 223 c \<in> C(Nil); 224 !!x y r. [| x \<in> A; y \<in> list(A); r \<in> C(y) |] ==> h(x,y,r): C(Cons(x,y)) 225 |] ==> list_rec(c,h,l) \<in> C(l)" 226by (induct_tac "l", auto) 227 228(** map **) 229 230lemma map_type [TC]: 231 "[| l \<in> list(A); !!x. x \<in> A ==> h(x): B |] ==> map(h,l) \<in> list(B)" 232apply (simp add: map_list_def) 233apply (typecheck add: list.intros list_rec_type, blast) 234done 235 236lemma map_type2 [TC]: "l \<in> list(A) ==> map(h,l) \<in> list({h(u). u \<in> A})" 237apply (erule map_type) 238apply (erule RepFunI) 239done 240 241(** length **) 242 243lemma length_type [TC]: "l \<in> list(A) ==> length(l) \<in> nat" 244by (simp add: length_list_def) 245 246lemma lt_length_in_nat: 247 "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat" 248by (frule lt_nat_in_nat, typecheck) 249 250(** app **) 251 252lemma app_type [TC]: "[| xs: list(A); ys: list(A) |] ==> xs@ys \<in> list(A)" 253by (simp add: app_list_def) 254 255(** rev **) 256 257lemma rev_type [TC]: "xs: list(A) ==> rev(xs) \<in> list(A)" 258by (simp add: rev_list_def) 259 260 261(** flat **) 262 263lemma flat_type [TC]: "ls: list(list(A)) ==> flat(ls) \<in> list(A)" 264by (simp add: flat_list_def) 265 266 267(** set_of_list **) 268 269lemma set_of_list_type [TC]: "l \<in> list(A) ==> set_of_list(l) \<in> Pow(A)" 270apply (unfold set_of_list_list_def) 271apply (erule list_rec_type, auto) 272done 273 274lemma set_of_list_append: 275 "xs: list(A) ==> set_of_list (xs@ys) = set_of_list(xs) \<union> set_of_list(ys)" 276apply (erule list.induct) 277apply (simp_all (no_asm_simp) add: Un_cons) 278done 279 280 281(** list_add **) 282 283lemma list_add_type [TC]: "xs: list(nat) ==> list_add(xs) \<in> nat" 284by (simp add: list_add_list_def) 285 286 287(*** theorems about map ***) 288 289lemma map_ident [simp]: "l \<in> list(A) ==> map(%u. u, l) = l" 290apply (induct_tac "l") 291apply (simp_all (no_asm_simp)) 292done 293 294lemma map_compose: "l \<in> list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)" 295apply (induct_tac "l") 296apply (simp_all (no_asm_simp)) 297done 298 299lemma map_app_distrib: "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)" 300apply (induct_tac "xs") 301apply (simp_all (no_asm_simp)) 302done 303 304lemma map_flat: "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))" 305apply (induct_tac "ls") 306apply (simp_all (no_asm_simp) add: map_app_distrib) 307done 308 309lemma list_rec_map: 310 "l \<in> list(A) ==> 311 list_rec(c, d, map(h,l)) = 312 list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)" 313apply (induct_tac "l") 314apply (simp_all (no_asm_simp)) 315done 316 317(** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **) 318 319(* @{term"c \<in> list(Collect(B,P)) ==> c \<in> list"} *) 320lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD] 321 322lemma map_list_Collect: "l \<in> list({x \<in> A. h(x)=j(x)}) ==> map(h,l) = map(j,l)" 323apply (induct_tac "l") 324apply (simp_all (no_asm_simp)) 325done 326 327(*** theorems about length ***) 328 329lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)" 330by (induct_tac "xs", simp_all) 331 332lemma length_app [simp]: 333 "[| xs: list(A); ys: list(A) |] 334 ==> length(xs@ys) = length(xs) #+ length(ys)" 335by (induct_tac "xs", simp_all) 336 337lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)" 338apply (induct_tac "xs") 339apply (simp_all (no_asm_simp) add: length_app) 340done 341 342lemma length_flat: 343 "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))" 344apply (induct_tac "ls") 345apply (simp_all (no_asm_simp) add: length_app) 346done 347 348(** Length and drop **) 349 350(*Lemma for the inductive step of drop_length*) 351lemma drop_length_Cons [rule_format]: 352 "xs: list(A) ==> 353 \<forall>x. \<exists>z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)" 354by (erule list.induct, simp_all) 355 356lemma drop_length [rule_format]: 357 "l \<in> list(A) ==> \<forall>i \<in> length(l). (\<exists>z zs. drop(i,l) = Cons(z,zs))" 358apply (erule list.induct, simp_all, safe) 359apply (erule drop_length_Cons) 360apply (rule natE) 361apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all) 362apply (blast intro: succ_in_naturalD length_type) 363done 364 365 366(*** theorems about app ***) 367 368lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs" 369by (erule list.induct, simp_all) 370 371lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)" 372by (induct_tac "xs", simp_all) 373 374lemma flat_app_distrib: "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)" 375apply (induct_tac "ls") 376apply (simp_all (no_asm_simp) add: app_assoc) 377done 378 379(*** theorems about rev ***) 380 381lemma rev_map_distrib: "l \<in> list(A) ==> rev(map(h,l)) = map(h,rev(l))" 382apply (induct_tac "l") 383apply (simp_all (no_asm_simp) add: map_app_distrib) 384done 385 386(*Simplifier needs the premises as assumptions because rewriting will not 387 instantiate the variable ?A in the rules' typing conditions; note that 388 rev_type does not instantiate ?A. Only the premises do. 389*) 390lemma rev_app_distrib: 391 "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)" 392apply (erule list.induct) 393apply (simp_all add: app_assoc) 394done 395 396lemma rev_rev_ident [simp]: "l \<in> list(A) ==> rev(rev(l))=l" 397apply (induct_tac "l") 398apply (simp_all (no_asm_simp) add: rev_app_distrib) 399done 400 401lemma rev_flat: "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))" 402apply (induct_tac "ls") 403apply (simp_all add: map_app_distrib flat_app_distrib rev_app_distrib) 404done 405 406 407(*** theorems about list_add ***) 408 409lemma list_add_app: 410 "[| xs: list(nat); ys: list(nat) |] 411 ==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)" 412apply (induct_tac "xs", simp_all) 413done 414 415lemma list_add_rev: "l \<in> list(nat) ==> list_add(rev(l)) = list_add(l)" 416apply (induct_tac "l") 417apply (simp_all (no_asm_simp) add: list_add_app) 418done 419 420lemma list_add_flat: 421 "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))" 422apply (induct_tac "ls") 423apply (simp_all (no_asm_simp) add: list_add_app) 424done 425 426(** New induction rules **) 427 428lemma list_append_induct [case_names Nil snoc, consumes 1]: 429 "[| l \<in> list(A); 430 P(Nil); 431 !!x y. [| x \<in> A; y \<in> list(A); P(y) |] ==> P(y @ [x]) 432 |] ==> P(l)" 433apply (subgoal_tac "P(rev(rev(l)))", simp) 434apply (erule rev_type [THEN list.induct], simp_all) 435done 436 437lemma list_complete_induct_lemma [rule_format]: 438 assumes ih: 439 "\<And>l. [| l \<in> list(A); 440 \<forall>l' \<in> list(A). length(l') < length(l) \<longrightarrow> P(l')|] 441 ==> P(l)" 442 shows "n \<in> nat ==> \<forall>l \<in> list(A). length(l) < n \<longrightarrow> P(l)" 443apply (induct_tac n, simp) 444apply (blast intro: ih elim!: leE) 445done 446 447theorem list_complete_induct: 448 "[| l \<in> list(A); 449 \<And>l. [| l \<in> list(A); 450 \<forall>l' \<in> list(A). length(l') < length(l) \<longrightarrow> P(l')|] 451 ==> P(l) 452 |] ==> P(l)" 453apply (rule list_complete_induct_lemma [of A]) 454 prefer 4 apply (rule le_refl, simp) 455 apply blast 456 apply simp 457apply assumption 458done 459 460 461(*** Thanks to Sidi Ehmety for these results about min, take, etc. ***) 462 463(** min FIXME: replace by Int! **) 464(* Min theorems are also true for i, j ordinals *) 465lemma min_sym: "[| i \<in> nat; j \<in> nat |] ==> min(i,j)=min(j,i)" 466apply (unfold min_def) 467apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym) 468done 469 470lemma min_type [simp,TC]: "[| i \<in> nat; j \<in> nat |] ==> min(i,j):nat" 471by (unfold min_def, auto) 472 473lemma min_0 [simp]: "i \<in> nat ==> min(0,i) = 0" 474apply (unfold min_def) 475apply (auto dest: not_lt_imp_le) 476done 477 478lemma min_02 [simp]: "i \<in> nat ==> min(i, 0) = 0" 479apply (unfold min_def) 480apply (auto dest: not_lt_imp_le) 481done 482 483lemma lt_min_iff: "[| i \<in> nat; j \<in> nat; k \<in> nat |] ==> i<min(j,k) \<longleftrightarrow> i<j & i<k" 484apply (unfold min_def) 485apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans) 486done 487 488lemma min_succ_succ [simp]: 489 "[| i \<in> nat; j \<in> nat |] ==> min(succ(i), succ(j))= succ(min(i, j))" 490apply (unfold min_def, auto) 491done 492 493(*** more theorems about lists ***) 494 495(** filter **) 496 497lemma filter_append [simp]: 498 "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)" 499by (induct_tac "xs", auto) 500 501lemma filter_type [simp,TC]: "xs:list(A) ==> filter(P, xs):list(A)" 502by (induct_tac "xs", auto) 503 504lemma length_filter: "xs:list(A) ==> length(filter(P, xs)) \<le> length(xs)" 505apply (induct_tac "xs", auto) 506apply (rule_tac j = "length (l) " in le_trans) 507apply (auto simp add: le_iff) 508done 509 510lemma filter_is_subset: "xs:list(A) ==> set_of_list(filter(P,xs)) \<subseteq> set_of_list(xs)" 511by (induct_tac "xs", auto) 512 513lemma filter_False [simp]: "xs:list(A) ==> filter(%p. False, xs) = Nil" 514by (induct_tac "xs", auto) 515 516lemma filter_True [simp]: "xs:list(A) ==> filter(%p. True, xs) = xs" 517by (induct_tac "xs", auto) 518 519(** length **) 520 521lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 \<longleftrightarrow> xs=Nil" 522by (erule list.induct, auto) 523 524lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) \<longleftrightarrow> xs=Nil" 525by (erule list.induct, auto) 526 527lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1" 528by (erule list.induct, auto) 529 530lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) \<longleftrightarrow> xs \<noteq> Nil" 531by (erule list.induct, auto) 532 533lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) \<longleftrightarrow> (\<exists>y ys. xs=Cons(y, ys) & length(ys)=n)" 534by (erule list.induct, auto) 535 536(** more theorems about append **) 537 538lemma append_is_Nil_iff [simp]: 539 "xs:list(A) ==> (xs@ys = Nil) \<longleftrightarrow> (xs=Nil & ys = Nil)" 540by (erule list.induct, auto) 541 542lemma append_is_Nil_iff2 [simp]: 543 "xs:list(A) ==> (Nil = xs@ys) \<longleftrightarrow> (xs=Nil & ys = Nil)" 544by (erule list.induct, auto) 545 546lemma append_left_is_self_iff [simp]: 547 "xs:list(A) ==> (xs@ys = xs) \<longleftrightarrow> (ys = Nil)" 548by (erule list.induct, auto) 549 550lemma append_left_is_self_iff2 [simp]: 551 "xs:list(A) ==> (xs = xs@ys) \<longleftrightarrow> (ys = Nil)" 552by (erule list.induct, auto) 553 554(*TOO SLOW as a default simprule!*) 555lemma append_left_is_Nil_iff [rule_format]: 556 "[| xs:list(A); ys:list(A); zs:list(A) |] ==> 557 length(ys)=length(zs) \<longrightarrow> (xs@ys=zs \<longleftrightarrow> (xs=Nil & ys=zs))" 558apply (erule list.induct) 559apply (auto simp add: length_app) 560done 561 562(*TOO SLOW as a default simprule!*) 563lemma append_left_is_Nil_iff2 [rule_format]: 564 "[| xs:list(A); ys:list(A); zs:list(A) |] ==> 565 length(ys)=length(zs) \<longrightarrow> (zs=ys@xs \<longleftrightarrow> (xs=Nil & ys=zs))" 566apply (erule list.induct) 567apply (auto simp add: length_app) 568done 569 570lemma append_eq_append_iff [rule_format]: 571 "xs:list(A) ==> \<forall>ys \<in> list(A). 572 length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) \<longleftrightarrow> (xs=ys & us=vs)" 573apply (erule list.induct) 574apply (simp (no_asm_simp)) 575apply clarify 576apply (erule_tac a = ys in list.cases, auto) 577done 578declare append_eq_append_iff [simp] 579 580lemma append_eq_append [rule_format]: 581 "xs:list(A) ==> 582 \<forall>ys \<in> list(A). \<forall>us \<in> list(A). \<forall>vs \<in> list(A). 583 length(us) = length(vs) \<longrightarrow> (xs@us = ys@vs) \<longrightarrow> (xs=ys & us=vs)" 584apply (induct_tac "xs") 585apply (force simp add: length_app, clarify) 586apply (erule_tac a = ys in list.cases, simp) 587apply (subgoal_tac "Cons (a, l) @ us =vs") 588 apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all, blast) 589done 590 591lemma append_eq_append_iff2 [simp]: 592 "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |] 593 ==> xs@us = ys@vs \<longleftrightarrow> (xs=ys & us=vs)" 594apply (rule iffI) 595apply (rule append_eq_append, auto) 596done 597 598lemma append_self_iff [simp]: 599 "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs \<longleftrightarrow> ys=zs" 600by simp 601 602lemma append_self_iff2 [simp]: 603 "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs \<longleftrightarrow> ys=zs" 604by simp 605 606(* Can also be proved from append_eq_append_iff2, 607but the proof requires two more hypotheses: x \<in> A and y \<in> A *) 608lemma append1_eq_iff [rule_format]: 609 "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys & x=y)" 610apply (erule list.induct) 611 apply clarify 612 apply (erule list.cases) 613 apply simp_all 614txt\<open>Inductive step\<close> 615apply clarify 616apply (erule_tac a=ys in list.cases, simp_all) 617done 618declare append1_eq_iff [simp] 619 620lemma append_right_is_self_iff [simp]: 621 "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) \<longleftrightarrow> (xs=Nil)" 622by (simp (no_asm_simp) add: append_left_is_Nil_iff) 623 624lemma append_right_is_self_iff2 [simp]: 625 "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) \<longleftrightarrow> (xs=Nil)" 626apply (rule iffI) 627apply (drule sym, auto) 628done 629 630lemma hd_append [rule_format]: 631 "xs:list(A) ==> xs \<noteq> Nil \<longrightarrow> hd(xs @ ys) = hd(xs)" 632by (induct_tac "xs", auto) 633declare hd_append [simp] 634 635lemma tl_append [rule_format]: 636 "xs:list(A) ==> xs\<noteq>Nil \<longrightarrow> tl(xs @ ys) = tl(xs)@ys" 637by (induct_tac "xs", auto) 638declare tl_append [simp] 639 640(** rev **) 641lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil \<longleftrightarrow> xs = Nil)" 642by (erule list.induct, auto) 643 644lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) \<longleftrightarrow> xs = Nil)" 645by (erule list.induct, auto) 646 647lemma rev_is_rev_iff [rule_format]: 648 "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) \<longleftrightarrow> xs=ys" 649apply (erule list.induct, force, clarify) 650apply (erule_tac a = ys in list.cases, auto) 651done 652declare rev_is_rev_iff [simp] 653 654lemma rev_list_elim [rule_format]: 655 "xs:list(A) ==> 656 (xs=Nil \<longrightarrow> P) \<longrightarrow> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] \<longrightarrow>P)\<longrightarrow>P" 657by (erule list_append_induct, auto) 658 659 660(** more theorems about drop **) 661 662lemma length_drop [rule_format]: 663 "n \<in> nat ==> \<forall>xs \<in> list(A). length(drop(n, xs)) = length(xs) #- n" 664apply (erule nat_induct) 665apply (auto elim: list.cases) 666done 667declare length_drop [simp] 668 669lemma drop_all [rule_format]: 670 "n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n \<longrightarrow> drop(n, xs)=Nil" 671apply (erule nat_induct) 672apply (auto elim: list.cases) 673done 674declare drop_all [simp] 675 676lemma drop_append [rule_format]: 677 "n \<in> nat ==> 678 \<forall>xs \<in> list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n #- length(xs), ys)" 679apply (induct_tac "n") 680apply (auto elim: list.cases) 681done 682 683lemma drop_drop: 684 "m \<in> nat ==> \<forall>xs \<in> list(A). \<forall>n \<in> nat. drop(n, drop(m, xs))=drop(n #+ m, xs)" 685apply (induct_tac "m") 686apply (auto elim: list.cases) 687done 688 689(** take **) 690 691lemma take_0 [simp]: "xs:list(A) ==> take(0, xs) = Nil" 692apply (unfold take_def) 693apply (erule list.induct, auto) 694done 695 696lemma take_succ_Cons [simp]: 697 "n \<in> nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))" 698by (simp add: take_def) 699 700(* Needed for proving take_all *) 701lemma take_Nil [simp]: "n \<in> nat ==> take(n, Nil) = Nil" 702by (unfold take_def, auto) 703 704lemma take_all [rule_format]: 705 "n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n \<longrightarrow> take(n, xs) = xs" 706apply (erule nat_induct) 707apply (auto elim: list.cases) 708done 709declare take_all [simp] 710 711lemma take_type [rule_format]: 712 "xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)" 713apply (erule list.induct, simp, clarify) 714apply (erule natE, auto) 715done 716declare take_type [simp,TC] 717 718lemma take_append [rule_format]: 719 "xs:list(A) ==> 720 \<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) = 721 take(n, xs) @ take(n #- length(xs), ys)" 722apply (erule list.induct, simp, clarify) 723apply (erule natE, auto) 724done 725declare take_append [simp] 726 727lemma take_take [rule_format]: 728 "m \<in> nat ==> 729 \<forall>xs \<in> list(A). \<forall>n \<in> nat. take(n, take(m,xs))= take(min(n, m), xs)" 730apply (induct_tac "m", auto) 731apply (erule_tac a = xs in list.cases) 732apply (auto simp add: take_Nil) 733apply (erule_tac n=n in natE) 734apply (auto intro: take_0 take_type) 735done 736 737(** nth **) 738 739lemma nth_0 [simp]: "nth(0, Cons(a, l)) = a" 740by (simp add: nth_def) 741 742lemma nth_Cons [simp]: "n \<in> nat ==> nth(succ(n), Cons(a,l)) = nth(n,l)" 743by (simp add: nth_def) 744 745lemma nth_empty [simp]: "nth(n, Nil) = 0" 746by (simp add: nth_def) 747 748lemma nth_type [rule_format]: 749 "xs:list(A) ==> \<forall>n. n < length(xs) \<longrightarrow> nth(n,xs) \<in> A" 750apply (erule list.induct, simp, clarify) 751apply (subgoal_tac "n \<in> nat") 752 apply (erule natE, auto dest!: le_in_nat) 753done 754declare nth_type [simp,TC] 755 756lemma nth_eq_0 [rule_format]: 757 "xs:list(A) ==> \<forall>n \<in> nat. length(xs) \<le> n \<longrightarrow> nth(n,xs) = 0" 758apply (erule list.induct, simp, clarify) 759apply (erule natE, auto) 760done 761 762lemma nth_append [rule_format]: 763 "xs:list(A) ==> 764 \<forall>n \<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs) 765 else nth(n #- length(xs), ys))" 766apply (induct_tac "xs", simp, clarify) 767apply (erule natE, auto) 768done 769 770lemma set_of_list_conv_nth: 771 "xs:list(A) 772 ==> set_of_list(xs) = {x \<in> A. \<exists>i\<in>nat. i<length(xs) & x = nth(i,xs)}" 773apply (induct_tac "xs", simp_all) 774apply (rule equalityI, auto) 775apply (rule_tac x = 0 in bexI, auto) 776apply (erule natE, auto) 777done 778 779(* Other theorems about lists *) 780 781lemma nth_take_lemma [rule_format]: 782 "k \<in> nat ==> 783 \<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k \<le> length(xs) \<longrightarrow> k \<le> length(ys) \<longrightarrow> 784 (\<forall>i \<in> nat. i<k \<longrightarrow> nth(i,xs) = nth(i,ys))\<longrightarrow> take(k,xs) = take(k,ys))" 785apply (induct_tac "k") 786apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib) 787apply clarify 788(*Both lists are non-empty*) 789apply (erule_tac a=xs in list.cases, simp) 790apply (erule_tac a=ys in list.cases, clarify) 791apply (simp (no_asm_use) ) 792apply clarify 793apply (simp (no_asm_simp)) 794apply (rule conjI, force) 795apply (rename_tac y ys z zs) 796apply (drule_tac x = zs and x1 = ys in bspec [THEN bspec], auto) 797done 798 799lemma nth_equalityI [rule_format]: 800 "[| xs:list(A); ys:list(A); length(xs) = length(ys); 801 \<forall>i \<in> nat. i < length(xs) \<longrightarrow> nth(i,xs) = nth(i,ys) |] 802 ==> xs = ys" 803apply (subgoal_tac "length (xs) \<le> length (ys) ") 804apply (cut_tac k="length(xs)" and xs=xs and ys=ys in nth_take_lemma) 805apply (simp_all add: take_all) 806done 807 808(*The famous take-lemma*) 809 810lemma take_equalityI [rule_format]: 811 "[| xs:list(A); ys:list(A); (\<forall>i \<in> nat. take(i, xs) = take(i,ys)) |] 812 ==> xs = ys" 813apply (case_tac "length (xs) \<le> length (ys) ") 814apply (drule_tac x = "length (ys) " in bspec) 815apply (drule_tac [3] not_lt_imp_le) 816apply (subgoal_tac [5] "length (ys) \<le> length (xs) ") 817apply (rule_tac [6] j = "succ (length (ys))" in le_trans) 818apply (rule_tac [6] leI) 819apply (drule_tac [5] x = "length (xs) " in bspec) 820apply (simp_all add: take_all) 821done 822 823lemma nth_drop [rule_format]: 824 "n \<in> nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). nth(i, drop(n, xs)) = nth(n #+ i, xs)" 825apply (induct_tac "n", simp_all, clarify) 826apply (erule list.cases, auto) 827done 828 829lemma take_succ [rule_format]: 830 "xs\<in>list(A) 831 ==> \<forall>i. i < length(xs) \<longrightarrow> take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]" 832apply (induct_tac "xs", auto) 833apply (subgoal_tac "i\<in>nat") 834apply (erule natE) 835apply (auto simp add: le_in_nat) 836done 837 838lemma take_add [rule_format]: 839 "[|xs\<in>list(A); j\<in>nat|] 840 ==> \<forall>i\<in>nat. take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))" 841apply (induct_tac "xs", simp_all, clarify) 842apply (erule_tac n = i in natE, simp_all) 843done 844 845lemma length_take: 846 "l\<in>list(A) ==> \<forall>n\<in>nat. length(take(n,l)) = min(n, length(l))" 847apply (induct_tac "l", safe, simp_all) 848apply (erule natE, simp_all) 849done 850 851subsection\<open>The function zip\<close> 852 853text\<open>Crafty definition to eliminate a type argument\<close> 854 855consts 856 zip_aux :: "[i,i]=>i" 857 858primrec (*explicit lambda is required because both arguments of "un" vary*) 859 "zip_aux(B,[]) = 860 (\<lambda>ys \<in> list(B). list_case([], %y l. [], ys))" 861 862 "zip_aux(B,Cons(x,l)) = 863 (\<lambda>ys \<in> list(B). 864 list_case(Nil, %y zs. Cons(<x,y>, zip_aux(B,l)`zs), ys))" 865 866definition 867 zip :: "[i, i]=>i" where 868 "zip(xs, ys) == zip_aux(set_of_list(ys),xs)`ys" 869 870 871(* zip equations *) 872 873lemma list_on_set_of_list: "xs \<in> list(A) ==> xs \<in> list(set_of_list(xs))" 874apply (induct_tac xs, simp_all) 875apply (blast intro: list_mono [THEN subsetD]) 876done 877 878lemma zip_Nil [simp]: "ys:list(A) ==> zip(Nil, ys)=Nil" 879apply (simp add: zip_def list_on_set_of_list [of _ A]) 880apply (erule list.cases, simp_all) 881done 882 883lemma zip_Nil2 [simp]: "xs:list(A) ==> zip(xs, Nil)=Nil" 884apply (simp add: zip_def list_on_set_of_list [of _ A]) 885apply (erule list.cases, simp_all) 886done 887 888lemma zip_aux_unique [rule_format]: 889 "[|B<=C; xs \<in> list(A)|] 890 ==> \<forall>ys \<in> list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys" 891apply (induct_tac xs) 892 apply simp_all 893 apply (blast intro: list_mono [THEN subsetD], clarify) 894apply (erule_tac a=ys in list.cases, auto) 895apply (blast intro: list_mono [THEN subsetD]) 896done 897 898lemma zip_Cons_Cons [simp]: 899 "[| xs:list(A); ys:list(B); x \<in> A; y \<in> B |] ==> 900 zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))" 901apply (simp add: zip_def, auto) 902apply (rule zip_aux_unique, auto) 903apply (simp add: list_on_set_of_list [of _ B]) 904apply (blast intro: list_on_set_of_list list_mono [THEN subsetD]) 905done 906 907lemma zip_type [rule_format]: 908 "xs:list(A) ==> \<forall>ys \<in> list(B). zip(xs, ys):list(A*B)" 909apply (induct_tac "xs") 910apply (simp (no_asm)) 911apply clarify 912apply (erule_tac a = ys in list.cases, auto) 913done 914declare zip_type [simp,TC] 915 916(* zip length *) 917lemma length_zip [rule_format]: 918 "xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) = 919 min(length(xs), length(ys))" 920apply (unfold min_def) 921apply (induct_tac "xs", simp_all, clarify) 922apply (erule_tac a = ys in list.cases, auto) 923done 924declare length_zip [simp] 925 926lemma zip_append1 [rule_format]: 927 "[| ys:list(A); zs:list(B) |] ==> 928 \<forall>xs \<in> list(A). zip(xs @ ys, zs) = 929 zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))" 930apply (induct_tac "zs", force, clarify) 931apply (erule_tac a = xs in list.cases, simp_all) 932done 933 934lemma zip_append2 [rule_format]: 935 "[| xs:list(A); zs:list(B) |] ==> \<forall>ys \<in> list(B). zip(xs, ys@zs) = 936 zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)" 937apply (induct_tac "xs", force, clarify) 938apply (erule_tac a = ys in list.cases, auto) 939done 940 941lemma zip_append [simp]: 942 "[| length(xs) = length(us); length(ys) = length(vs); 943 xs:list(A); us:list(B); ys:list(A); vs:list(B) |] 944 ==> zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)" 945by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0) 946 947 948lemma zip_rev [rule_format]: 949 "ys:list(B) ==> \<forall>xs \<in> list(A). 950 length(xs) = length(ys) \<longrightarrow> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))" 951apply (induct_tac "ys", force, clarify) 952apply (erule_tac a = xs in list.cases) 953apply (auto simp add: length_rev) 954done 955declare zip_rev [simp] 956 957lemma nth_zip [rule_format]: 958 "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). 959 i < length(xs) \<longrightarrow> i < length(ys) \<longrightarrow> 960 nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>" 961apply (induct_tac "ys", force, clarify) 962apply (erule_tac a = xs in list.cases, simp) 963apply (auto elim: natE) 964done 965declare nth_zip [simp] 966 967lemma set_of_list_zip [rule_format]: 968 "[| xs:list(A); ys:list(B); i \<in> nat |] 969 ==> set_of_list(zip(xs, ys)) = 970 {<x, y>:A*B. \<exists>i\<in>nat. i < min(length(xs), length(ys)) 971 & x = nth(i, xs) & y = nth(i, ys)}" 972by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth) 973 974(** list_update **) 975 976lemma list_update_Nil [simp]: "i \<in> nat ==>list_update(Nil, i, v) = Nil" 977by (unfold list_update_def, auto) 978 979lemma list_update_Cons_0 [simp]: "list_update(Cons(x, xs), 0, v)= Cons(v, xs)" 980by (unfold list_update_def, auto) 981 982lemma list_update_Cons_succ [simp]: 983 "n \<in> nat ==> 984 list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))" 985apply (unfold list_update_def, auto) 986done 987 988lemma list_update_type [rule_format]: 989 "[| xs:list(A); v \<in> A |] ==> \<forall>n \<in> nat. list_update(xs, n, v):list(A)" 990apply (induct_tac "xs") 991apply (simp (no_asm)) 992apply clarify 993apply (erule natE, auto) 994done 995declare list_update_type [simp,TC] 996 997lemma length_list_update [rule_format]: 998 "xs:list(A) ==> \<forall>i \<in> nat. length(list_update(xs, i, v))=length(xs)" 999apply (induct_tac "xs") 1000apply (simp (no_asm)) 1001apply clarify 1002apply (erule natE, auto) 1003done 1004declare length_list_update [simp] 1005 1006lemma nth_list_update [rule_format]: 1007 "[| xs:list(A) |] ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i < length(xs) \<longrightarrow> 1008 nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))" 1009apply (induct_tac "xs") 1010 apply simp_all 1011apply clarify 1012apply (rename_tac i j) 1013apply (erule_tac n=i in natE) 1014apply (erule_tac [2] n=j in natE) 1015apply (erule_tac n=j in natE, simp_all, force) 1016done 1017 1018lemma nth_list_update_eq [simp]: 1019 "[| i < length(xs); xs:list(A) |] ==> nth(i, list_update(xs, i,x)) = x" 1020by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update) 1021 1022 1023lemma nth_list_update_neq [rule_format]: 1024 "xs:list(A) ==> 1025 \<forall>i \<in> nat. \<forall>j \<in> nat. i \<noteq> j \<longrightarrow> nth(j, list_update(xs,i,x)) = nth(j,xs)" 1026apply (induct_tac "xs") 1027 apply (simp (no_asm)) 1028apply clarify 1029apply (erule natE) 1030apply (erule_tac [2] natE, simp_all) 1031apply (erule natE, simp_all) 1032done 1033declare nth_list_update_neq [simp] 1034 1035lemma list_update_overwrite [rule_format]: 1036 "xs:list(A) ==> \<forall>i \<in> nat. i < length(xs) 1037 \<longrightarrow> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)" 1038apply (induct_tac "xs") 1039 apply (simp (no_asm)) 1040apply clarify 1041apply (erule natE, auto) 1042done 1043declare list_update_overwrite [simp] 1044 1045lemma list_update_same_conv [rule_format]: 1046 "xs:list(A) ==> 1047 \<forall>i \<in> nat. i < length(xs) \<longrightarrow> 1048 (list_update(xs, i, x) = xs) \<longleftrightarrow> (nth(i, xs) = x)" 1049apply (induct_tac "xs") 1050 apply (simp (no_asm)) 1051apply clarify 1052apply (erule natE, auto) 1053done 1054 1055lemma update_zip [rule_format]: 1056 "ys:list(B) ==> 1057 \<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A). 1058 length(xs) = length(ys) \<longrightarrow> 1059 list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)), 1060 list_update(ys, i, snd(xy)))" 1061apply (induct_tac "ys") 1062 apply auto 1063apply (erule_tac a = xs in list.cases) 1064apply (auto elim: natE) 1065done 1066 1067lemma set_update_subset_cons [rule_format]: 1068 "xs:list(A) ==> 1069 \<forall>i \<in> nat. set_of_list(list_update(xs, i, x)) \<subseteq> cons(x, set_of_list(xs))" 1070apply (induct_tac "xs") 1071 apply simp 1072apply (rule ballI) 1073apply (erule natE, simp_all, auto) 1074done 1075 1076lemma set_of_list_update_subsetI: 1077 "[| set_of_list(xs) \<subseteq> A; xs:list(A); x \<in> A; i \<in> nat|] 1078 ==> set_of_list(list_update(xs, i,x)) \<subseteq> A" 1079apply (rule subset_trans) 1080apply (rule set_update_subset_cons, auto) 1081done 1082 1083(** upt **) 1084 1085lemma upt_rec: 1086 "j \<in> nat ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)" 1087apply (induct_tac "j", auto) 1088apply (drule not_lt_imp_le) 1089apply (auto simp: lt_Ord intro: le_anti_sym) 1090done 1091 1092lemma upt_conv_Nil [simp]: "[| j \<le> i; j \<in> nat |] ==> upt(i,j) = Nil" 1093apply (subst upt_rec, auto) 1094apply (auto simp add: le_iff) 1095apply (drule lt_asym [THEN notE], auto) 1096done 1097 1098(*Only needed if upt_Suc is deleted from the simpset*) 1099lemma upt_succ_append: 1100 "[| i \<le> j; j \<in> nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]" 1101by simp 1102 1103lemma upt_conv_Cons: 1104 "[| i<j; j \<in> nat |] ==> upt(i,j) = Cons(i,upt(succ(i),j))" 1105apply (rule trans) 1106apply (rule upt_rec, auto) 1107done 1108 1109lemma upt_type [simp,TC]: "j \<in> nat ==> upt(i,j):list(nat)" 1110by (induct_tac "j", auto) 1111 1112(*LOOPS as a simprule, since j<=j*) 1113lemma upt_add_eq_append: 1114 "[| i \<le> j; j \<in> nat; k \<in> nat |] ==> upt(i, j #+k) = upt(i,j)@upt(j,j#+k)" 1115apply (induct_tac "k") 1116apply (auto simp add: app_assoc app_type) 1117apply (rule_tac j = j in le_trans, auto) 1118done 1119 1120lemma length_upt [simp]: "[| i \<in> nat; j \<in> nat |] ==>length(upt(i,j)) = j #- i" 1121apply (induct_tac "j") 1122apply (rule_tac [2] sym) 1123apply (auto dest!: not_lt_imp_le simp add: diff_succ diff_is_0_iff) 1124done 1125 1126lemma nth_upt [simp]: 1127 "[| i \<in> nat; j \<in> nat; k \<in> nat; i #+ k < j |] ==> nth(k, upt(i,j)) = i #+ k" 1128apply (rotate_tac -1, erule rev_mp) 1129apply (induct_tac "j", simp) 1130apply (auto dest!: not_lt_imp_le 1131 simp add: nth_append le_iff less_diff_conv add_commute) 1132done 1133 1134lemma take_upt [rule_format]: 1135 "[| m \<in> nat; n \<in> nat |] ==> 1136 \<forall>i \<in> nat. i #+ m \<le> n \<longrightarrow> take(m, upt(i,n)) = upt(i,i#+m)" 1137apply (induct_tac "m") 1138apply (simp (no_asm_simp) add: take_0) 1139apply clarify 1140apply (subst upt_rec, simp) 1141apply (rule sym) 1142apply (subst upt_rec, simp) 1143apply (simp_all del: upt.simps) 1144apply (rule_tac j = "succ (i #+ x) " in lt_trans2) 1145apply auto 1146done 1147declare take_upt [simp] 1148 1149lemma map_succ_upt: 1150 "[| m \<in> nat; n \<in> nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))" 1151apply (induct_tac "n") 1152apply (auto simp add: map_app_distrib) 1153done 1154 1155lemma nth_map [rule_format]: 1156 "xs:list(A) ==> 1157 \<forall>n \<in> nat. n < length(xs) \<longrightarrow> nth(n, map(f, xs)) = f(nth(n, xs))" 1158apply (induct_tac "xs", simp) 1159apply (rule ballI) 1160apply (induct_tac "n", auto) 1161done 1162declare nth_map [simp] 1163 1164lemma nth_map_upt [rule_format]: 1165 "[| m \<in> nat; n \<in> nat |] ==> 1166 \<forall>i \<in> nat. i < n #- m \<longrightarrow> nth(i, map(f, upt(m,n))) = f(m #+ i)" 1167apply (rule_tac n = m and m = n in diff_induct, typecheck, simp, simp) 1168apply (subst map_succ_upt [symmetric], simp_all, clarify) 1169apply (subgoal_tac "i < length (upt (0, x))") 1170 prefer 2 1171 apply (simp add: less_diff_conv) 1172 apply (rule_tac j = "succ (i #+ y) " in lt_trans2) 1173 apply simp 1174 apply simp 1175apply (subgoal_tac "i < length (upt (y, x))") 1176 apply (simp_all add: add_commute less_diff_conv) 1177done 1178 1179(** sublist (a generalization of nth to sets) **) 1180 1181definition 1182 sublist :: "[i, i] => i" where 1183 "sublist(xs, A)== 1184 map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))" 1185 1186lemma sublist_0 [simp]: "xs:list(A) ==>sublist(xs, 0) =Nil" 1187by (unfold sublist_def, auto) 1188 1189lemma sublist_Nil [simp]: "sublist(Nil, A) = Nil" 1190by (unfold sublist_def, auto) 1191 1192lemma sublist_shift_lemma: 1193 "[| xs:list(B); i \<in> nat |] ==> 1194 map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) = 1195 map(fst, filter(%p. snd(p):nat & snd(p) #+ i \<in> A, zip(xs,upt(0,length(xs)))))" 1196apply (erule list_append_induct) 1197apply (simp (no_asm_simp)) 1198apply (auto simp add: add_commute length_app filter_append map_app_distrib) 1199done 1200 1201lemma sublist_type [simp,TC]: 1202 "xs:list(B) ==> sublist(xs, A):list(B)" 1203apply (unfold sublist_def) 1204apply (induct_tac "xs") 1205apply (auto simp add: filter_append map_app_distrib) 1206done 1207 1208lemma upt_add_eq_append2: 1209 "[| i \<in> nat; j \<in> nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)" 1210by (simp add: upt_add_eq_append [of 0] nat_0_le) 1211 1212lemma sublist_append: 1213 "[| xs:list(B); ys:list(B) |] ==> 1214 sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j \<in> nat. j #+ length(xs): A})" 1215apply (unfold sublist_def) 1216apply (erule_tac l = ys in list_append_induct, simp) 1217apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric]) 1218apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc) 1219apply (simp_all add: add_commute) 1220done 1221 1222 1223lemma sublist_Cons: 1224 "[| xs:list(B); x \<in> B |] ==> 1225 sublist(Cons(x, xs), A) = 1226 (if 0 \<in> A then [x] else []) @ sublist(xs, {j \<in> nat. succ(j) \<in> A})" 1227apply (erule_tac l = xs in list_append_induct) 1228apply (simp (no_asm_simp) add: sublist_def) 1229apply (simp del: app_Cons add: app_Cons [symmetric] sublist_append, simp) 1230done 1231 1232lemma sublist_singleton [simp]: 1233 "sublist([x], A) = (if 0 \<in> A then [x] else [])" 1234by (simp add: sublist_Cons) 1235 1236lemma sublist_upt_eq_take [rule_format]: 1237 "xs:list(A) ==> \<forall>n\<in>nat. sublist(xs,n) = take(n,xs)" 1238apply (erule list.induct, simp) 1239apply (clarify ) 1240apply (erule natE) 1241apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons) 1242done 1243declare sublist_upt_eq_take [simp] 1244 1245lemma sublist_Int_eq: 1246 "xs \<in> list(B) ==> sublist(xs, A \<inter> nat) = sublist(xs, A)" 1247apply (erule list.induct) 1248apply (simp_all add: sublist_Cons) 1249done 1250 1251text\<open>Repetition of a List Element\<close> 1252 1253consts repeat :: "[i,i]=>i" 1254primrec 1255 "repeat(a,0) = []" 1256 1257 "repeat(a,succ(n)) = Cons(a,repeat(a,n))" 1258 1259lemma length_repeat: "n \<in> nat ==> length(repeat(a,n)) = n" 1260by (induct_tac n, auto) 1261 1262lemma repeat_succ_app: "n \<in> nat ==> repeat(a,succ(n)) = repeat(a,n) @ [a]" 1263apply (induct_tac n) 1264apply (simp_all del: app_Cons add: app_Cons [symmetric]) 1265done 1266 1267lemma repeat_type [TC]: "[|a \<in> A; n \<in> nat|] ==> repeat(a,n) \<in> list(A)" 1268by (induct_tac n, auto) 1269 1270end 1271