equal
deleted
inserted
replaced
1436 apply (induct xs arbitrary: n) |
1436 apply (induct xs arbitrary: n) |
1437 apply simp |
1437 apply simp |
1438 apply (auto split:nat.split) |
1438 apply (auto split:nat.split) |
1439 done |
1439 done |
1440 |
1440 |
1441 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)" |
1441 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - Suc 0)" |
1442 by(induct xs)(auto simp:neq_Nil_conv) |
1442 by(induct xs)(auto simp:neq_Nil_conv) |
1443 |
1443 |
1444 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs" |
1444 lemma butlast_conv_take: "butlast xs = take (length xs - Suc 0) xs" |
1445 by (induct xs, simp, case_tac xs, simp_all) |
1445 by (induct xs, simp, case_tac xs, simp_all) |
1446 |
1446 |
1447 |
1447 |
1448 subsubsection {* @{text take} and @{text drop} *} |
1448 subsubsection {* @{text take} and @{text drop} *} |
1449 |
1449 |
1586 apply (induct n arbitrary: xs i, auto) |
1586 apply (induct n arbitrary: xs i, auto) |
1587 apply (case_tac xs, auto) |
1587 apply (case_tac xs, auto) |
1588 done |
1588 done |
1589 |
1589 |
1590 lemma butlast_take: |
1590 lemma butlast_take: |
1591 "n <= length xs ==> butlast (take n xs) = take (n - 1) xs" |
1591 "n <= length xs ==> butlast (take n xs) = take (n - Suc 0) xs" |
1592 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2) |
1592 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2) |
1593 |
1593 |
1594 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)" |
1594 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)" |
1595 by (simp add: butlast_conv_take drop_take) |
1595 by (simp add: butlast_conv_take drop_take) |
1596 |
1596 |
1637 apply(case_tac ys\<^isub>1) |
1637 apply(case_tac ys\<^isub>1) |
1638 apply simp_all |
1638 apply simp_all |
1639 done |
1639 done |
1640 |
1640 |
1641 lemma take_hd_drop: |
1641 lemma take_hd_drop: |
1642 "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs" |
1642 "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (Suc n) xs" |
1643 apply(induct xs arbitrary: n) |
1643 apply(induct xs arbitrary: n) |
1644 apply simp |
1644 apply simp |
1645 apply(simp add:drop_Cons split:nat.split) |
1645 apply(simp add:drop_Cons split:nat.split) |
1646 done |
1646 done |
1647 |
1647 |
2456 apply simp |
2456 apply simp |
2457 apply blast |
2457 apply blast |
2458 done |
2458 done |
2459 |
2459 |
2460 lemma length_remove1: |
2460 lemma length_remove1: |
2461 "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)" |
2461 "length(remove1 x xs) = (if x : set xs then length xs - Suc 0 else length xs)" |
2462 apply (induct xs) |
2462 apply (induct xs) |
2463 apply (auto dest!:length_pos_if_in_set) |
2463 apply (auto dest!:length_pos_if_in_set) |
2464 done |
2464 done |
2465 |
2465 |
2466 lemma remove1_filter_not[simp]: |
2466 lemma remove1_filter_not[simp]: |