# HG changeset patch
# User nipkow
# Date 1526211814 -7200
# Node ID efce008331f606ff9893c7b3841f6d4369748382
# Parent  620ca44d8b7df0edef00141464721cda7df1774b
mv lemma

diff -r 620ca44d8b7d -r efce008331f6 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Sun May 13 13:15:50 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Sun May 13 13:43:34 2018 +0200
@@ -1,28 +1,15 @@
 (* Author: Tobias Nipkow *)
 
-(* FIXME adjust List.sorted to work like below; [code] is different! *)
-
 theory Sorting
 imports
   Complex_Main
   "HOL-Library.Multiset"
 begin
 
-hide_const List.sorted List.insort
+hide_const List.insort
 
 declare Let_def [simp]
 
-fun sorted :: "'a::linorder list \<Rightarrow> bool" where
-"sorted [] = True" |
-"sorted (x # xs) = ((\<forall>y\<in>set xs. x \<le> y) & sorted xs)"
-
-lemma sorted_append:
-  "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
-by (induct xs) (auto)
-
-lemma sorted01: "length xs \<le> 1 \<Longrightarrow> sorted xs"
-by(auto simp: le_Suc_eq length_Suc_conv)
-
 
 subsection "Insertion Sort"
 
diff -r 620ca44d8b7d -r efce008331f6 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun May 13 13:15:50 2018 +0200
+++ b/src/HOL/List.thy	Sun May 13 13:43:34 2018 +0200
@@ -5021,6 +5021,9 @@
 
 lemmas [code] = sorted.simps(1) sorted2_simps
 
+lemma sorted01: "length xs \<le> 1 \<Longrightarrow> sorted xs"
+by (simp add: sorted_sorted_wrt sorted_wrt01)
+
 lemma sorted_tl:
   "sorted xs \<Longrightarrow> sorted (tl xs)"
 by (cases xs) (simp_all)