added lemmas
authornipkow
Tue May 15 20:34:46 2018 +0200 (12 months ago)
changeset 68190695ff8a207b0
parent 68189 6163c90694ef
child 68191 4ac04fe61e98
added lemmas
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Tue May 15 13:57:39 2018 +0200
     1.2 +++ b/src/HOL/List.thy	Tue May 15 20:34:46 2018 +0200
     1.3 @@ -5190,6 +5190,12 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma sorted_upt[simp]: "sorted [m..<n]"
     1.8 +by(simp add: sorted_sorted_wrt sorted_wrt_mono_rel[OF _ sorted_wrt_upt])
     1.9 +
    1.10 +lemma sorted_upto[simp]: "sorted [m..n]"
    1.11 +by(simp add: sorted_sorted_wrt sorted_wrt_mono_rel[OF _ sorted_wrt_upto])
    1.12 +
    1.13  
    1.14  subsubsection \<open>Sorting functions\<close>
    1.15