--- a/src/HOL/List.thy Wed May 16 15:18:18 2018 +0200
+++ b/src/HOL/List.thy Wed May 16 15:52:15 2018 +0200
@@ -4984,15 +4984,11 @@
lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m..<n]"
by(induction n) (auto simp: sorted_wrt_append)
-lemma sorted_wrt_upto[simp]: "sorted_wrt (<) [m..n]"
-proof cases
- assume "n < m" thus ?thesis by simp
-next
- assume "\<not> n < m"
- hence "m \<le> n" by simp
- thus ?thesis
- by(induction m rule:int_le_induct)(auto simp: upto_rec1)
-qed
+lemma sorted_wrt_upto[simp]: "sorted_wrt (<) [i..j]"
+apply(induction i j rule: upto.induct)
+apply(subst upto.simps)
+apply(simp)
+done
text \<open>Each element is greater or equal to its index:\<close>
@@ -5190,6 +5186,12 @@
end
+lemma sorted_upt[simp]: "sorted [m..<n]"
+by(simp add: sorted_sorted_wrt sorted_wrt_mono_rel[OF _ sorted_wrt_upt])
+
+lemma sorted_upto[simp]: "sorted [m..n]"
+by(simp add: sorted_sorted_wrt sorted_wrt_mono_rel[OF _ sorted_wrt_upto])
+
subsubsection \<open>Sorting functions\<close>
@@ -5375,18 +5377,11 @@
end
-lemma sorted_upt[simp]: "sorted[i..<j]"
-by (induct j) (simp_all add:sorted_append)
-
-lemma sort_upt [simp]:
- "sort [m..<n] = [m..<n]"
- by (rule sorted_sort_id) simp
-
-lemma sorted_upto[simp]: "sorted[i..j]"
-apply(induct i j rule:upto.induct)
-apply(subst upto.simps)
-apply(simp)
-done
+lemma sort_upt [simp]: "sort [m..<n] = [m..<n]"
+by (rule sorted_sort_id) simp
+
+lemma sort_upto [simp]: "sort [i..j] = [i..j]"
+by (rule sorted_sort_id) simp
lemma sorted_find_Min:
"sorted xs \<Longrightarrow> \<exists>x \<in> set xs. P x \<Longrightarrow> List.find P xs = Some (Min {x\<in>set xs. P x})"