--- a/src/HOL/Data_Structures/Binomial_Heap.thy Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Tue May 08 10:14:36 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 Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/Data_Structures/Sorted_Less.thy Tue May 08 10:14:36 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)
--- a/src/HOL/Data_Structures/Tree234_Set.thy Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/Data_Structures/Tree234_Set.thy Tue May 08 10:14:36 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 Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Tue May 08 10:14:36 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/Library/RBT_Impl.thy Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/Library/RBT_Impl.thy Tue May 08 10:14:36 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 Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/Library/RBT_Set.thy Tue May 08 10:14:36 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
--- a/src/HOL/Library/Tree.thy Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/Library/Tree.thy Tue May 08 10:14:36 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 Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/List.thy Tue May 08 10:14:36 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,17 @@
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)
-*)
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 +5010,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 +5022,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 +5037,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 +5059,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 +5094,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 +5140,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 +5221,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 +5240,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 +5251,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 +5322,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 +5344,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 +5354,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 +6240,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 +6811,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 Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/ex/Bubblesort.thy Tue May 08 10:14:36 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 Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/ex/MergeSort.thy Tue May 08 10:14:36 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 Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/ex/Quicksort.thy Tue May 08 10:14:36 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"