equal
deleted
inserted
replaced
1386 done |
1386 done |
1387 |
1387 |
1388 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)" |
1388 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)" |
1389 by(induct xs)(auto simp:neq_Nil_conv) |
1389 by(induct xs)(auto simp:neq_Nil_conv) |
1390 |
1390 |
|
1391 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs" |
|
1392 by (induct xs, simp, case_tac xs, simp_all) |
|
1393 |
1391 |
1394 |
1392 subsubsection {* @{text take} and @{text drop} *} |
1395 subsubsection {* @{text take} and @{text drop} *} |
1393 |
1396 |
1394 lemma take_0 [simp]: "take 0 xs = []" |
1397 lemma take_0 [simp]: "take 0 xs = []" |
1395 by (induct xs) auto |
1398 by (induct xs) auto |
1409 by(clarsimp simp add:neq_Nil_conv) |
1412 by(clarsimp simp add:neq_Nil_conv) |
1410 |
1413 |
1411 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)" |
1414 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)" |
1412 by(cases xs, simp_all) |
1415 by(cases xs, simp_all) |
1413 |
1416 |
|
1417 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)" |
|
1418 by (induct xs arbitrary: n) simp_all |
|
1419 |
1414 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)" |
1420 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)" |
1415 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split) |
1421 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split) |
|
1422 |
|
1423 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)" |
|
1424 by (cases n, simp, cases xs, auto) |
|
1425 |
|
1426 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)" |
|
1427 by (simp only: drop_tl) |
1416 |
1428 |
1417 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y" |
1429 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y" |
1418 apply (induct xs arbitrary: n, simp) |
1430 apply (induct xs arbitrary: n, simp) |
1419 apply(simp add:drop_Cons nth_Cons split:nat.splits) |
1431 apply(simp add:drop_Cons nth_Cons split:nat.splits) |
1420 done |
1432 done |
1519 lemma nth_drop [simp]: |
1531 lemma nth_drop [simp]: |
1520 "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)" |
1532 "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)" |
1521 apply (induct n arbitrary: xs i, auto) |
1533 apply (induct n arbitrary: xs i, auto) |
1522 apply (case_tac xs, auto) |
1534 apply (case_tac xs, auto) |
1523 done |
1535 done |
|
1536 |
|
1537 lemma butlast_take: |
|
1538 "n <= length xs ==> butlast (take n xs) = take (n - 1) xs" |
|
1539 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2) |
|
1540 |
|
1541 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)" |
|
1542 by (simp add: butlast_conv_take drop_take) |
|
1543 |
|
1544 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs" |
|
1545 by (simp add: butlast_conv_take min_max.inf_absorb1) |
|
1546 |
|
1547 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)" |
|
1548 by (simp add: butlast_conv_take drop_take) |
1524 |
1549 |
1525 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n" |
1550 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n" |
1526 by(simp add: hd_conv_nth) |
1551 by(simp add: hd_conv_nth) |
1527 |
1552 |
1528 lemma set_take_subset: "set(take n xs) \<subseteq> set xs" |
1553 lemma set_take_subset: "set(take n xs) \<subseteq> set xs" |