# HG changeset patch
# User nipkow
# Date 1526411962 -7200
# Node ID 4ac04fe61e9856d23aa30065ea3c55fff1d0daf2
# Parent  695ff8a207b0fd9a1847d0f4fed47666703b0c96
removed duplicates

diff -r 695ff8a207b0 -r 4ac04fe61e98 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue May 15 20:34:46 2018 +0200
+++ b/src/HOL/List.thy	Tue May 15 21:19:22 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>
 
@@ -5381,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})"