# HG changeset patch
# User nipkow
# Date 1525784779 -7200
# Node ID 6a63a4ce756bb6d81a93af2e66391ce4736bb11e
# Parent  2277fe496d787f9fc4ba82b5e7e4be3f901fd07c# Parent  bdbf759ddbac3939a0bd9ec748b68c42bbcdd887
merged

diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Tue May 08 15:06:19 2018 +0200
@@ -133,7 +133,7 @@
 lemma invar_bheap_Cons[simp]:
   "invar_bheap (t#ts)
   \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
-by (auto simp: sorted_wrt_Cons invar_bheap_def)
+by (auto simp: invar_bheap_def)
 
 lemma invar_btree_ins_tree:
   assumes "invar_btree t"
diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/Data_Structures/Sorted_Less.thy
--- a/src/HOL/Data_Structures/Sorted_Less.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/Data_Structures/Sorted_Less.thy	Tue May 08 15:06:19 2018 +0200
@@ -8,12 +8,24 @@
 
 hide_const sorted
 
-text \<open>Is a list sorted without duplicates, i.e., wrt @{text"<"}?
-Could go into theory List under a name like @{term sorted_less}.\<close>
+text \<open>Is a list sorted without duplicates, i.e., wrt @{text"<"}?.\<close>
 
 abbreviation sorted :: "'a::linorder list \<Rightarrow> bool" where
 "sorted \<equiv> sorted_wrt (<)"
 
+text \<open>The definition of @{const sorted_wrt} relates each element to all the elements after it.
+This causes a blowup of the formulas. Thus we simplify matters by only comparing adjacent elements.\<close>
+
+lemma sorted_wrt1 [simp]: "sorted_wrt P [x]"
+by simp
+
+lemma sorted2 [simp]: "sorted (x # y # zs) = (x < y \<and> sorted (y # zs))"
+by(induction zs) auto
+
+lemmas sorted_wrt_Cons = sorted_wrt.simps(2)
+
+declare sorted_wrt.simps(2)[simp del]
+
 lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
 by(simp add: sorted_wrt_Cons)
 
diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/Data_Structures/Tree234_Set.thy
--- a/src/HOL/Data_Structures/Tree234_Set.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/Data_Structures/Tree234_Set.thy	Tue May 08 15:06:19 2018 +0200
@@ -9,6 +9,8 @@
   Set_Specs
 begin
 
+declare sorted_wrt.simps(2)[simp del]
+
 subsection \<open>Set operations on 2-3-4 trees\<close>
 
 fun isin :: "'a::linorder tree234 \<Rightarrow> 'a \<Rightarrow> bool" where
diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Tue May 08 15:06:19 2018 +0200
@@ -9,6 +9,8 @@
   Set_Specs
 begin
 
+declare sorted_wrt.simps(2)[simp del]
+
 fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
 "isin Leaf x = False" |
 "isin (Node2 l a r) x =
diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue May 08 15:06:19 2018 +0200
@@ -556,7 +556,7 @@
         by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
       with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
         unfolding subarray_def
-        apply (auto simp add: sorted_append sorted_Cons all_in_set_nths'_conv)
+        apply (auto simp add: sorted_append all_in_set_nths'_conv)
         by (auto simp add: set_nths' dest: order.trans [of _ "Array.get h' a ! p"])
     }
     with True cr show ?thesis
diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/Imperative_HOL/ex/Sorted_List.thy
--- a/src/HOL/Imperative_HOL/ex/Sorted_List.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sorted_List.thy	Tue May 08 15:06:19 2018 +0200
@@ -26,10 +26,10 @@
 
 lemma sorted_merge[simp]:
      "List.sorted (merge xs ys) = (List.sorted xs \<and> List.sorted ys)"
-by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons)
+by (induct xs ys rule: merge.induct, auto)
 
 lemma distinct_merge[simp]: "\<lbrakk> distinct xs; distinct ys; List.sorted xs; List.sorted ys \<rbrakk> \<Longrightarrow> distinct (merge xs ys)"
-by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons)
+by (induct xs ys rule: merge.induct, auto)
 
 text \<open>The remove function removes an element from a sorted list\<close>
 
@@ -40,7 +40,7 @@
 
 lemma remove': "sorted xs \<and> distinct xs \<Longrightarrow> sorted (remove a xs) \<and> distinct (remove a xs) \<and> set (remove a xs) = set xs - {a}"
 apply (induct xs)
-apply (auto simp add: sorted_Cons)
+apply (auto)
 done
 
 lemma set_remove[simp]: "\<lbrakk> sorted xs; distinct xs \<rbrakk> \<Longrightarrow> set (remove a xs) = set xs - {a}"
@@ -61,7 +61,6 @@
 lemma remove_insort_commute: "\<lbrakk> a \<noteq> b; sorted xs \<rbrakk> \<Longrightarrow> remove b (insort a xs) = insort a (remove b xs)"
 apply (induct xs)
 apply auto
-apply (auto simp add: sorted_Cons)
 apply (case_tac xs)
 apply auto
 done
@@ -74,7 +73,7 @@
 lemma remove1_eq_remove:
   "sorted xs \<Longrightarrow> distinct xs \<Longrightarrow> remove1 x xs = remove x xs"
 apply (induct xs)
-apply (auto simp add: sorted_Cons)
+apply (auto)
 apply (subgoal_tac "x \<notin> set xs")
 apply (simp add: notinset_remove)
 apply fastforce
@@ -83,7 +82,7 @@
 lemma sorted_remove1:
   "sorted xs \<Longrightarrow> sorted (remove1 x xs)"
 apply (induct xs)
-apply (auto simp add: sorted_Cons)
+apply (auto)
 done
 
 subsection \<open>Efficient member function for sorted lists\<close>
@@ -93,6 +92,6 @@
 | "smember (y#ys) x \<longleftrightarrow> x = y \<or> (x > y \<and> smember ys x)"
 
 lemma "sorted xs \<Longrightarrow> smember xs x \<longleftrightarrow> (x \<in> set xs)" 
-  by (induct xs) (auto simp add: sorted_Cons)
+  by (induct xs) (auto)
 
 end
diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Tue May 08 15:06:19 2018 +0200
@@ -114,15 +114,11 @@
 
 lemma rbt_sorted_entries:
   "rbt_sorted t \<Longrightarrow> List.sorted (map fst (entries t))"
-by (induct t) 
-  (force simp: sorted_append sorted_Cons rbt_ord_props 
-      dest!: entry_in_tree_keys)+
+by (induct t)  (force simp: sorted_append rbt_ord_props dest!: entry_in_tree_keys)+
 
 lemma distinct_entries:
   "rbt_sorted t \<Longrightarrow> distinct (map fst (entries t))"
-by (induct t) 
-  (force simp: sorted_append sorted_Cons rbt_ord_props 
-      dest!: entry_in_tree_keys)+
+by (induct t) (force simp: sorted_append rbt_ord_props dest!: entry_in_tree_keys)+
 
 lemma distinct_keys:
   "rbt_sorted t \<Longrightarrow> distinct (keys t)"
@@ -1604,7 +1600,7 @@
   hence unfold: "kvs = take n kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   from \<open>sorted (map fst kvs)\<close> kvs'
   have "(\<forall>(x, y) \<in> set (take n kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
-    by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
+    by(subst (asm) unfold)(auto simp add: sorted_append)
   moreover from \<open>distinct (map fst kvs)\<close> kvs'
   have "(\<forall>(x, y) \<in> set (take n kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
     by(subst (asm) unfold)(auto intro: rev_image_eqI)
@@ -1617,7 +1613,7 @@
   have "rbt_sorted (fst (rbtreeify_f n kvs))" by(rule f_even.IH)
   moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
     using \<open>sorted (map fst kvs)\<close> \<open>distinct (map fst kvs)\<close>
-    by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
+    by(subst (asm) (1 2) unfold, simp add: sorted_append)+
   hence "rbt_sorted (fst (rbtreeify_g n kvs'))" by(rule f_even.IH)
   ultimately show ?case
     using \<open>0 < n\<close> \<open>rbtreeify_f n kvs = (t, (k, v) # kvs')\<close> by simp
@@ -1629,7 +1625,7 @@
   hence unfold: "kvs = take n kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   from \<open>sorted (map fst kvs)\<close> kvs'
   have "(\<forall>(x, y) \<in> set (take n kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
-    by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
+    by(subst (asm) unfold)(auto simp add: sorted_append)
   moreover from \<open>distinct (map fst kvs)\<close> kvs'
   have "(\<forall>(x, y) \<in> set (take n kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
     by(subst (asm) unfold)(auto intro: rev_image_eqI)
@@ -1642,7 +1638,7 @@
   have "rbt_sorted (fst (rbtreeify_f n kvs))" by(rule f_odd.IH)
   moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
     using \<open>sorted (map fst kvs)\<close> \<open>distinct (map fst kvs)\<close>
-    by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
+    by(subst (asm) (1 2) unfold, simp add: sorted_append)+
   hence "rbt_sorted (fst (rbtreeify_f n kvs'))" by(rule f_odd.IH)
   ultimately show ?case 
     using \<open>0 < n\<close> \<open>rbtreeify_f n kvs = (t, (k, v) # kvs')\<close> by simp
@@ -1654,7 +1650,7 @@
   hence unfold: "kvs = take (n - 1) kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   from \<open>sorted (map fst kvs)\<close> kvs'
   have "(\<forall>(x, y) \<in> set (take (n - 1) kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
-    by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
+    by(subst (asm) unfold)(auto simp add: sorted_append)
   moreover from \<open>distinct (map fst kvs)\<close> kvs'
   have "(\<forall>(x, y) \<in> set (take (n - 1) kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
     by(subst (asm) unfold)(auto intro: rev_image_eqI)
@@ -1667,7 +1663,7 @@
   have "rbt_sorted (fst (rbtreeify_g n kvs))" by(rule g_even.IH)
   moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
     using \<open>sorted (map fst kvs)\<close> \<open>distinct (map fst kvs)\<close>
-    by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
+    by(subst (asm) (1 2) unfold, simp add: sorted_append)+
   hence "rbt_sorted (fst (rbtreeify_g n kvs'))" by(rule g_even.IH)
   ultimately show ?case using \<open>0 < n\<close> \<open>rbtreeify_g n kvs = (t, (k, v) # kvs')\<close> by simp
 next
@@ -1678,7 +1674,7 @@
   hence unfold: "kvs = take n kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   from \<open>sorted (map fst kvs)\<close> kvs'
   have "(\<forall>(x, y) \<in> set (take n kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
-    by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
+    by(subst (asm) unfold)(auto simp add: sorted_append)
   moreover from \<open>distinct (map fst kvs)\<close> kvs'
   have "(\<forall>(x, y) \<in> set (take n kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
     by(subst (asm) unfold)(auto intro: rev_image_eqI)
@@ -1691,7 +1687,7 @@
   have "rbt_sorted (fst (rbtreeify_f n kvs))" by(rule g_odd.IH)
   moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
     using \<open>sorted (map fst kvs)\<close> \<open>distinct (map fst kvs)\<close>
-    by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
+    by(subst (asm) (1 2) unfold, simp add: sorted_append)+
   hence "rbt_sorted (fst (rbtreeify_g n kvs'))" by(rule g_odd.IH)
   ultimately show ?case
     using \<open>0 < n\<close> \<open>rbtreeify_f n kvs = (t, (k, v) # kvs')\<close> by simp
@@ -1800,7 +1796,7 @@
   "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk> 
   \<Longrightarrow> sorted (map fst (sunion_with f xs ys))"
 by(induct f xs ys rule: sunion_with.induct)
-  (auto simp add: sorted_Cons set_fst_sunion_with simp del: set_map)
+  (auto simp add: set_fst_sunion_with simp del: set_map)
 
 lemma distinct_sunion_with [simp]:
   "\<lbrakk> distinct (map fst xs); distinct (map fst ys); sorted (map fst xs); sorted (map fst ys) \<rbrakk>
@@ -1809,7 +1805,7 @@
   case (1 f k v xs k' v' ys)
   have "\<lbrakk> \<not> k < k'; \<not> k' < k \<rbrakk> \<Longrightarrow> k = k'" by simp
   thus ?case using "1"
-    by(auto simp add: set_fst_sunion_with sorted_Cons simp del: set_map)
+    by(auto simp add: set_fst_sunion_with simp del: set_map)
 qed simp_all
 
 lemma map_of_sunion_with: 
@@ -1818,12 +1814,12 @@
   (case map_of xs k of None \<Rightarrow> map_of ys k 
   | Some v \<Rightarrow> case map_of ys k of None \<Rightarrow> Some v 
               | Some w \<Rightarrow> Some (f k v w))"
-by(induct f xs ys rule: sunion_with.induct)(auto simp add: sorted_Cons split: option.split dest: map_of_SomeD bspec)
+by(induct f xs ys rule: sunion_with.induct)(auto split: option.split dest: map_of_SomeD bspec)
 
 lemma set_fst_sinter_with [simp]:
   "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   \<Longrightarrow> set (map fst (sinter_with f xs ys)) = set (map fst xs) \<inter> set (map fst ys)"
-by(induct f xs ys rule: sinter_with.induct)(auto simp add: sorted_Cons simp del: set_map)
+by(induct f xs ys rule: sinter_with.induct)(auto simp del: set_map)
 
 lemma set_fst_sinter_with_subset1:
   "set (map fst (sinter_with f xs ys)) \<subseteq> set (map fst xs)"
@@ -1836,7 +1832,7 @@
 lemma sorted_sinter_with [simp]:
   "\<lbrakk> sorted (map fst xs); sorted (map fst ys) \<rbrakk>
   \<Longrightarrow> sorted (map fst (sinter_with f xs ys))"
-by(induct f xs ys rule: sinter_with.induct)(auto simp add: sorted_Cons simp del: set_map)
+by(induct f xs ys rule: sinter_with.induct)(auto simp del: set_map)
 
 lemma distinct_sinter_with [simp]:
   "\<lbrakk> distinct (map fst xs); distinct (map fst ys) \<rbrakk>
@@ -1854,7 +1850,7 @@
   \<Longrightarrow> map_of (sinter_with f xs ys) k = 
   (case map_of xs k of None \<Rightarrow> None | Some v \<Rightarrow> map_option (f k v) (map_of ys k))"
 apply(induct f xs ys rule: sinter_with.induct)
-apply(auto simp add: sorted_Cons map_option_case split: option.splits dest: map_of_SomeD bspec)
+apply(auto simp add: map_option_case split: option.splits dest: map_of_SomeD bspec)
 done
 
 end
diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Tue May 08 15:06:19 2018 +0200
@@ -790,7 +790,7 @@
       then show "x \<le> y"
         using Cons[symmetric]
         by(auto simp add: set_keys Cons_eq_filter_iff)
-          (metis sorted_Cons sorted_append sorted_keys)
+          (metis sorted.simps(2) sorted_append sorted_keys)
   qed
   thus ?thesis using Cons by (simp add: Bleast_def)
 qed
diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/Library/Tree.thy	Tue May 08 15:06:19 2018 +0200
@@ -446,12 +446,12 @@
 lemma bst_wrt_le_iff_sorted: "bst_wrt (\<le>) t \<longleftrightarrow> sorted (inorder t)"
 apply (induction t)
  apply(simp)
-by (fastforce simp: sorted_append sorted_Cons intro: less_imp_le less_trans)
+by (fastforce simp: sorted_append intro: less_imp_le less_trans)
 
 lemma bst_iff_sorted_wrt_less: "bst t \<longleftrightarrow> sorted_wrt (<) (inorder t)"
 apply (induction t)
  apply simp
-apply (fastforce simp: sorted_wrt_Cons sorted_wrt_append)
+apply (fastforce simp: sorted_wrt_append)
 done
 
 
diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/List.thy
--- a/src/HOL/List.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/List.thy	Tue May 08 15:06:19 2018 +0200
@@ -351,8 +351,7 @@
 
 fun sorted_wrt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
 "sorted_wrt P [] = True" |
-"sorted_wrt P [x] = True" |
-"sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))"
+"sorted_wrt P (x # ys) = ((\<forall>y \<in> set ys. P x y) \<and> sorted_wrt P ys)"
 
 (* FIXME: define sorted in terms of sorted_wrt *)
 
@@ -363,8 +362,7 @@
 
 fun sorted :: "'a list \<Rightarrow> bool" where
 "sorted [] = True" |
-"sorted [x] = True" |
-"sorted (x # y # zs) = (x \<le> y \<and> sorted (y # zs))"
+"sorted (x # ys) = ((\<forall>y \<in> set ys. x \<le> y) \<and> sorted ys)"
 
 lemma sorted_sorted_wrt: "sorted = sorted_wrt (\<le>)"
 proof (rule ext)
@@ -4935,32 +4933,22 @@
 
 subsubsection \<open>@{const sorted_wrt}\<close>
 
-lemma sorted_wrt_Cons:
-assumes "transp P"
-shows   "sorted_wrt P (x # xs) = ((\<forall>y \<in> set xs. P x y) \<and> sorted_wrt P xs)"
-by(induction xs arbitrary: x)(auto intro: transpD[OF assms])
-
 lemma sorted_wrt_ConsI:
   "\<lbrakk> \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow> sorted_wrt P (x # xs)"
-by (induction xs rule: induct_list012) simp_all
+by (induction xs) simp_all
 
 lemma sorted_wrt_append:
-assumes "transp P"
-shows "sorted_wrt P (xs @ ys) \<longleftrightarrow>
+  "sorted_wrt P (xs @ ys) \<longleftrightarrow>
   sorted_wrt P xs \<and> sorted_wrt P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y)"
-by (induction xs) (auto simp: sorted_wrt_Cons[OF assms])
-
-lemma sorted_wrt_backwards:
-  "sorted_wrt P (xs @ [y, z]) = (P y z \<and> sorted_wrt P (xs @ [y]))"
-by (induction xs rule: induct_list012) auto
+by (induction xs) auto
 
 lemma sorted_wrt_rev:
   "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
-by (induction xs rule: induct_list012) (simp_all add: sorted_wrt_backwards)
+by (induction xs) (auto simp add: sorted_wrt_append)
 
 lemma sorted_wrt_mono:
   "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
-by(induction xs rule: induct_list012)(auto)
+by(induction xs)(auto)
 
 lemma sorted_wrt01: "length xs \<le> 1 \<Longrightarrow> sorted_wrt P xs"
 by(auto simp: le_Suc_eq length_Suc_conv)
@@ -4989,30 +4977,29 @@
 context linorder
 begin
 
-lemma sorted_Cons: "sorted (x#xs) = (sorted xs \<and> (\<forall>y \<in> set xs. x \<le> y))"
-apply(induction xs arbitrary: x)
- apply simp
-by simp (blast intro: order_trans)
-(*
-lemma sorted_iff_wrt: "sorted xs = sorted_wrt (\<le>) xs"
-proof
-  assume "sorted xs" thus "sorted_wrt (\<le>) xs"
-  proof (induct xs rule: sorted.induct)
-    case (Cons xs x) thus ?case by (cases xs) simp_all
-  qed simp
-qed (induct xs rule: induct_list012, simp_all)
-*)
+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 add: sorted_Cons)
+by (cases xs) (simp_all)
 
 lemma sorted_append:
   "sorted (xs@ys) = (sorted xs \<and> sorted ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
-by (induct xs) (auto simp add:sorted_Cons)
+by (induct xs) (auto)
 
 lemma sorted_nth_mono:
   "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
-by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)
+by (induct xs arbitrary: i j) (auto simp:nth_Cons')
 
 lemma sorted_rev_nth_mono:
   "sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"
@@ -5035,13 +5022,10 @@
     fix y assume "y \<in> set xs"
     then obtain j where "j < length xs" and "xs ! j = y"
       unfolding in_set_conv_nth by blast
-    with Cons.prems[of 0 "Suc j"]
-    have "x \<le> y"
-      by auto
+    with Cons.prems[of 0 "Suc j"] have "x \<le> y" by auto
   }
   ultimately
-  show ?case
-    unfolding sorted_Cons by auto
+  show ?case by auto
 qed simp
 
 lemma sorted_equals_nth_mono:
@@ -5050,7 +5034,7 @@
 
 lemma sorted_map_remove1:
   "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
-by (induct xs) (auto simp add: sorted_Cons)
+by (induct xs) (auto)
 
 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
 using sorted_map_remove1 [of "\<lambda>x. x"] by simp
@@ -5065,18 +5049,18 @@
 qed
 
 lemma sorted_replicate [simp]: "sorted(replicate n x)"
-by(induction n) (auto simp: sorted_Cons)
+by(induction n) (auto)
 
 lemma sorted_remdups[simp]:
-  "sorted l \<Longrightarrow> sorted (remdups l)"
-by (induct l) (auto simp: sorted_Cons)
+  "sorted xs \<Longrightarrow> sorted (remdups xs)"
+by (induct xs) (auto)
 
 lemma sorted_remdups_adj[simp]:
   "sorted xs \<Longrightarrow> sorted (remdups_adj xs)"
-by (induct xs rule: remdups_adj.induct, simp_all split: if_split_asm add: sorted_Cons)
+by (induct xs rule: remdups_adj.induct, simp_all split: if_split_asm)
 
 lemma sorted_nths: "sorted xs \<Longrightarrow> sorted (nths xs I)"
-by(induction xs arbitrary: I)(auto simp: sorted_Cons nths_Cons)
+by(induction xs arbitrary: I)(auto simp: nths_Cons)
 
 lemma sorted_distinct_set_unique:
 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
@@ -5087,8 +5071,7 @@
   proof(induct rule:list_induct2[OF 1])
     case 1 show ?case by simp
   next
-    case 2 thus ?case by (simp add: sorted_Cons)
-       (metis Diff_insert_absorb antisym insertE insert_iff)
+    case 2 thus ?case by simp (metis Diff_insert_absorb antisym insertE insert_iff)
   qed
 qed
 
@@ -5123,7 +5106,7 @@
 
 lemma sorted_filter:
   "sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"
-  by (induct xs) (simp_all add: sorted_Cons)
+  by (induct xs) simp_all
 
 lemma foldr_max_sorted:
   assumes "sorted (rev xs)"
@@ -5169,7 +5152,7 @@
   case (Cons x xs)
   then have "sorted (map f [y\<leftarrow>xs . f y = (\<lambda>xs. f x) xs])" .
   moreover from Cons have "sorted (map f [y\<leftarrow>xs . f y = (g \<circ> Cons x) xs])" .
-  ultimately show ?case by (simp_all add: sorted_Cons)
+  ultimately show ?case by simp_all
 qed
 
 lemma sorted_same:
@@ -5250,7 +5233,7 @@
 by (induct xs) (simp_all add: distinct_insort)
 
 lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
-by (induct xs) (auto simp: sorted_Cons set_insort_key)
+by (induct xs) (auto simp: set_insort_key)
 
 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
 using sorted_insort_key [where f="\<lambda>x. x"] by simp
@@ -5269,7 +5252,7 @@
 by (cases xs) auto
 
 lemma sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
-by (induct xs) (auto simp add: sorted_Cons insort_is_Cons)
+by (induct xs) (auto simp add: insort_is_Cons)
 
 lemma insort_key_remove1:
   assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"
@@ -5280,9 +5263,9 @@
   proof (cases "x = a")
     case False
     then have "f x \<noteq> f a" using Cons.prems by auto
-    then have "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
-    with \<open>f x \<noteq> f a\<close> show ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
-  qed (auto simp: sorted_Cons insort_is_Cons)
+    then have "f x < f a" using Cons.prems by auto
+    with \<open>f x \<noteq> f a\<close> show ?thesis using Cons by (auto simp: insort_is_Cons)
+  qed (auto simp: insort_is_Cons)
 qed simp
 
 lemma insort_remove1:
@@ -5351,7 +5334,7 @@
 
 lemma filter_insort:
   "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
-  by (induct xs) (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
+  by (induct xs) (auto, subst insort_is_Cons, auto)
 
 lemma filter_sort:
   "filter P (sort_key f xs) = sort_key f (filter P xs)"
@@ -5373,7 +5356,7 @@
 lemma sorted_upto[simp]: "sorted[i..j]"
 apply(induct i j rule:upto.induct)
 apply(subst upto.simps)
-apply(simp add:sorted_Cons)
+apply(simp)
 done
 
 lemma sorted_find_Min:
@@ -5383,11 +5366,11 @@
 next
   case (Cons x xs) show ?case proof (cases "P x")
     case True
-    with Cons show ?thesis by (auto simp: sorted_Cons intro: Min_eqI [symmetric])
+    with Cons show ?thesis by (auto intro: Min_eqI [symmetric])
   next
     case False then have "{y. (y = x \<or> y \<in> set xs) \<and> P y} = {y \<in> set xs. P y}"
       by auto
-    with Cons False show ?thesis by (simp_all add: sorted_Cons)
+    with Cons False show ?thesis by (simp_all)
   qed
 qed
 
@@ -6269,7 +6252,7 @@
 end
 
 lemma sorted_insort_is_snoc: "sorted xs \<Longrightarrow> \<forall>x \<in> set xs. a \<ge> x \<Longrightarrow> insort a xs = xs @ [a]"
- by (induct xs) (auto dest!: insort_is_Cons simp: sorted_Cons)
+ by (induct xs) (auto dest!: insort_is_Cons)
 
 
 subsubsection \<open>Lexicographic combination of measure functions\<close>
@@ -6840,7 +6823,7 @@
       fix y assume "y \<in> set xs \<and> P y"
       hence "y \<in> set (filter P xs)" by auto
       thus "x \<le> y"
-        by (metis Cons eq_iff filter_sort set_ConsD set_sort sorted_Cons sorted_sort)
+        by (metis Cons eq_iff filter_sort set_ConsD set_sort sorted.simps(2) sorted_sort)
   qed
   thus ?thesis using Cons by (simp add: Bleast_def)
 qed
diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/ex/Bubblesort.thy
--- a/src/HOL/ex/Bubblesort.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/ex/Bubblesort.thy	Tue May 08 15:06:19 2018 +0200
@@ -73,7 +73,7 @@
 apply(induction xs rule: bubblesort.induct)
   apply simp
  apply simp
-apply (fastforce simp: set_bubblesort sorted_Cons split: list.split if_splits dest: bubble_min_min)
+apply (fastforce simp: set_bubblesort split: list.split if_splits dest: bubble_min_min)
 done
 
 end
diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/ex/MergeSort.thy
--- a/src/HOL/ex/MergeSort.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/ex/MergeSort.thy	Tue May 08 15:06:19 2018 +0200
@@ -29,7 +29,7 @@
 
 lemma sorted_merge [simp]:
   "sorted (merge xs ys) \<longleftrightarrow> sorted xs \<and> sorted ys"
-  by (induct xs ys rule: merge.induct) (auto simp add: ball_Un not_le less_le sorted_Cons)
+  by (induct xs ys rule: merge.induct) (auto simp add: ball_Un not_le less_le)
 
 fun msort :: "'a list \<Rightarrow> 'a list"
 where
@@ -45,7 +45,7 @@
 lemma mset_msort:
   "mset (msort xs) = mset xs"
   by (induct xs rule: msort.induct)
-    (simp_all, metis append_take_drop_id drop_Suc_Cons mset.simps(2) mset_append take_Suc_Cons)
+    (simp_all, metis append_take_drop_id mset.simps(2) mset_append)
 
 theorem msort_sort:
   "sort = msort"
diff -r 2277fe496d78 -r 6a63a4ce756b src/HOL/ex/Quicksort.thy
--- a/src/HOL/ex/Quicksort.thy	Mon May 07 23:08:22 2018 +0200
+++ b/src/HOL/ex/Quicksort.thy	Tue May 08 15:06:19 2018 +0200
@@ -32,7 +32,7 @@
 qed
 
 lemma sorted_quicksort: "sorted (quicksort xs)"
-  by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
+  by (induct xs rule: quicksort.induct) (auto simp add: sorted_append not_le less_imp_le)
 
 theorem sort_quicksort:
   "sort = quicksort"