# HG changeset patch
# User nipkow
# Date 1525774570 -7200
# Node ID bdbf759ddbac3939a0bd9ec748b68c42bbcdd887
# Parent  29da75b7e352e89b133939d25393a49bb9651d66
more "sorted" changes

diff -r 29da75b7e352 -r bdbf759ddbac src/HOL/List.thy
--- a/src/HOL/List.thy	Tue May 08 10:22:58 2018 +0200
+++ b/src/HOL/List.thy	Tue May 08 12:16:10 2018 +0200
@@ -4977,6 +4977,18 @@
 context linorder
 begin
 
+text \<open>Sometimes the second equation in the definition of @{const sorted} is to aggressive
+because it relates each list element to \emph{all} its successors. Then this equation
+should be removed and \<open>sorted2_simps\<close> should be added instead:\<close>
+
+lemma sorted1: "sorted [x]"
+by simp
+
+lemma sorted2: "sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))"
+by(induction zs) auto
+
+lemmas sorted2_simps = sorted1 sorted2
+
 lemma sorted_tl:
   "sorted xs \<Longrightarrow> sorted (tl xs)"
 by (cases xs) (simp_all)