removed duplicates
authornipkow
Tue May 15 21:19:22 2018 +0200 (12 months ago)
changeset 681914ac04fe61e98
parent 68190 695ff8a207b0
child 68195 607957640057
removed duplicates
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Tue May 15 20:34:46 2018 +0200
     1.2 +++ b/src/HOL/List.thy	Tue May 15 21:19:22 2018 +0200
     1.3 @@ -4984,15 +4984,11 @@
     1.4  lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m..<n]"
     1.5  by(induction n) (auto simp: sorted_wrt_append)
     1.6  
     1.7 -lemma sorted_wrt_upto[simp]: "sorted_wrt (<) [m..n]"
     1.8 -proof cases
     1.9 -  assume "n < m" thus ?thesis by simp
    1.10 -next
    1.11 -  assume "\<not> n < m"
    1.12 -  hence "m \<le> n" by simp
    1.13 -  thus ?thesis
    1.14 -    by(induction m rule:int_le_induct)(auto simp: upto_rec1)
    1.15 -qed
    1.16 +lemma sorted_wrt_upto[simp]: "sorted_wrt (<) [i..j]"
    1.17 +apply(induction i j rule: upto.induct)
    1.18 +apply(subst upto.simps)
    1.19 +apply(simp)
    1.20 +done
    1.21  
    1.22  text \<open>Each element is greater or equal to its index:\<close>
    1.23  
    1.24 @@ -5381,18 +5377,11 @@
    1.25  
    1.26  end
    1.27  
    1.28 -lemma sorted_upt[simp]: "sorted[i..<j]"
    1.29 -by (induct j) (simp_all add:sorted_append)
    1.30 -
    1.31 -lemma sort_upt [simp]:
    1.32 -  "sort [m..<n] = [m..<n]"
    1.33 -  by (rule sorted_sort_id) simp
    1.34 -
    1.35 -lemma sorted_upto[simp]: "sorted[i..j]"
    1.36 -apply(induct i j rule:upto.induct)
    1.37 -apply(subst upto.simps)
    1.38 -apply(simp)
    1.39 -done
    1.40 +lemma sort_upt [simp]: "sort [m..<n] = [m..<n]"
    1.41 +by (rule sorted_sort_id) simp
    1.42 +
    1.43 +lemma sort_upto [simp]: "sort [i..j] = [i..j]"
    1.44 +by (rule sorted_sort_id) simp
    1.45  
    1.46  lemma sorted_find_Min:
    1.47    "sorted xs \<Longrightarrow> \<exists>x \<in> set xs. P x \<Longrightarrow> List.find P xs = Some (Min {x\<in>set xs. P x})"