equal
deleted
inserted
replaced
2885 apply clarify |
2885 apply clarify |
2886 apply(rule_tac a="sort xs" in ex1I) |
2886 apply(rule_tac a="sort xs" in ex1I) |
2887 apply (auto simp: sorted_distinct_set_unique) |
2887 apply (auto simp: sorted_distinct_set_unique) |
2888 done |
2888 done |
2889 |
2889 |
|
2890 lemma sorted_take: |
|
2891 "sorted xs \<Longrightarrow> sorted (take n xs)" |
|
2892 proof (induct xs arbitrary: n rule: sorted.induct) |
|
2893 case 1 show ?case by simp |
|
2894 next |
|
2895 case 2 show ?case by (cases n) simp_all |
|
2896 next |
|
2897 case (3 x y xs) |
|
2898 then have "x \<le> y" by simp |
|
2899 show ?case proof (cases n) |
|
2900 case 0 then show ?thesis by simp |
|
2901 next |
|
2902 case (Suc m) |
|
2903 with 3 have "sorted (take m (y # xs))" by simp |
|
2904 with Suc `x \<le> y` show ?thesis by (cases m) simp_all |
|
2905 qed |
|
2906 qed |
|
2907 |
|
2908 lemma sorted_drop: |
|
2909 "sorted xs \<Longrightarrow> sorted (drop n xs)" |
|
2910 proof (induct xs arbitrary: n rule: sorted.induct) |
|
2911 case 1 show ?case by simp |
|
2912 next |
|
2913 case 2 show ?case by (cases n) simp_all |
|
2914 next |
|
2915 case 3 then show ?case by (cases n) simp_all |
|
2916 qed |
|
2917 |
|
2918 |
2890 end |
2919 end |
2891 |
2920 |
2892 lemma sorted_upt[simp]: "sorted[i..<j]" |
2921 lemma sorted_upt[simp]: "sorted[i..<j]" |
2893 by (induct j) (simp_all add:sorted_append) |
2922 by (induct j) (simp_all add:sorted_append) |
2894 |
2923 |