equal
deleted
inserted
replaced
3661 lemma remdups_adj_map_injective: |
3661 lemma remdups_adj_map_injective: |
3662 assumes "inj f" |
3662 assumes "inj f" |
3663 shows "remdups_adj (map f xs) = map f (remdups_adj xs)" |
3663 shows "remdups_adj (map f xs) = map f (remdups_adj xs)" |
3664 by (induct xs rule: remdups_adj.induct) (auto simp add: injD[OF assms]) |
3664 by (induct xs rule: remdups_adj.induct) (auto simp add: injD[OF assms]) |
3665 |
3665 |
|
3666 lemma remdups_adj_replicate: |
|
3667 "remdups_adj (replicate n x) = (if n = 0 then [] else [x])" |
|
3668 by (induction n) (auto simp: remdups_adj_Cons) |
|
3669 |
3666 lemma remdups_upt [simp]: "remdups [m..<n] = [m..<n]" |
3670 lemma remdups_upt [simp]: "remdups [m..<n] = [m..<n]" |
3667 proof (cases "m \<le> n") |
3671 proof (cases "m \<le> n") |
3668 case False then show ?thesis by simp |
3672 case False then show ?thesis by simp |
3669 next |
3673 next |
3670 case True then obtain q where "n = m + q" |
3674 case True then obtain q where "n = m + q" |