author nipkow Tue, 08 May 2018 15:06:19 +0200 changeset 68112 6a63a4ce756b parent 68108 2277fe496d78 (current diff) parent 68111 bdbf759ddbac (diff) child 68117 7e349d1e3c95 child 68118 aedeef5e6858 child 68122 a49cf225fc97
merged
--- 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"
--- 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"

--- 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
--- 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 =
--- 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
--- 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)
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 (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)
apply (subgoal_tac "x \<notin> set xs")
apply fastforce
@@ -83,7 +82,7 @@
lemma sorted_remove1:
"sorted xs \<Longrightarrow> sorted (remove1 x xs)"
apply (induct xs)
+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
--- 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
--- 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]
-          (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
--- 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


--- 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
+
+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)

"sorted xs \<Longrightarrow> sorted (remdups_adj xs)"
+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)
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
--- 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
--- 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"
--- 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"