# HG changeset patch # User nipkow # Date 1526305046 -7200 # Node ID e0bd5089eabf244cbeec92abcbc21dc14486eb73 # Parent 7c4793e39dd54d797d87c554bd3d2f804c932f03 cleaning up sorted diff -r 7c4793e39dd5 -r e0bd5089eabf src/HOL/List.thy --- a/src/HOL/List.thy Sun May 13 21:59:41 2018 +0200 +++ b/src/HOL/List.thy Mon May 14 15:37:26 2018 +0200 @@ -4971,22 +4971,29 @@ lemma sorted_wrt01: "length xs \ 1 \ sorted_wrt P xs" by(auto simp: le_Suc_eq length_Suc_conv) -lemma sorted_wrt_iff_nth_Suc: +lemma sorted_wrt_iff_nth_less: "sorted_wrt P xs = (\i j. i < j \ j < length xs \ P (xs ! i) (xs ! j))" apply(induction xs) - apply simp -apply(force simp: in_set_conv_nth nth_Cons split: nat.split) +apply(auto simp add: in_set_conv_nth Ball_def nth_Cons split: nat.split) done lemma sorted_wrt_nth_less: "\ sorted_wrt P xs; i < j; j < length xs \ \ P (xs ! i) (xs ! j)" -by(auto simp: sorted_wrt_iff_nth_Suc) - -text \Strictly Ascending Sequences of Natural Numbers\ +by(auto simp: sorted_wrt_iff_nth_less) lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m.. n < m" + hence "m \ n" by simp + thus ?thesis + by(induction m rule:int_le_induct)(auto simp: upto_rec1) +qed + text \Each element is greater or equal to its index:\ lemma sorted_wrt_less_idx: @@ -5021,6 +5028,14 @@ lemmas [code] = sorted.simps(1) sorted2_simps +lemma sorted_append: + "sorted (xs@ys) = (sorted xs \ sorted ys \ (\x \ set xs. \y \ set ys. x\y))" +by (simp add: sorted_sorted_wrt sorted_wrt_append) + +lemma sorted_map: + "sorted (map f xs) = sorted_wrt (\x y. f x \ f y) xs" +by (simp add: sorted_sorted_wrt sorted_wrt_map) + lemma sorted01: "length xs \ 1 \ sorted xs" by (simp add: sorted_sorted_wrt sorted_wrt01) @@ -5028,45 +5043,28 @@ "sorted xs \ sorted (tl xs)" by (cases xs) (simp_all) -lemma sorted_append: - "sorted (xs@ys) = (sorted xs \ sorted ys \ (\x \ set xs. \y \ set ys. x\y))" -by (induct xs) (auto) +lemma sorted_iff_nth_mono: + "sorted xs = (\i j. i < j \ j < length xs \ xs ! i \ xs ! j)" +by (simp add: sorted_sorted_wrt sorted_wrt_iff_nth_less) lemma sorted_nth_mono: "sorted xs \ i \ j \ j < length xs \ xs!i \ xs!j" -by (induct xs arbitrary: i j) (auto simp:nth_Cons') +by (auto simp: sorted_iff_nth_mono nat_less_le) lemma sorted_rev_nth_mono: "sorted (rev xs) \ i \ j \ j < length xs \ xs!j \ xs!i" using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"] rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"] by auto - +(* lemma sorted_nth_monoI: "(\ i j. \ i \ j ; j < length xs \ \ xs ! i \ xs ! j) \ sorted xs" -proof (induct xs) - case (Cons x xs) - have "sorted xs" - proof (rule Cons.hyps) - fix i j assume "i \ j" and "j < length xs" - with Cons.prems[of "Suc i" "Suc j"] - show "xs ! i \ xs ! j" by auto - qed - moreover - { - fix y assume "y \ 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 \ y" by auto - } - ultimately - show ?case by auto -qed simp +by (simp add: sorted_iff_nth_less) lemma sorted_equals_nth_mono: "sorted xs = (\j < length xs. \i \ j. xs ! i \ xs ! j)" -by (auto intro: sorted_nth_monoI sorted_nth_mono) - +by (auto simp: sorted_iff_nth_less nat_less_le) +*) lemma sorted_map_remove1: "sorted (map f xs) \ sorted (map f (remove1 x xs))" by (induct xs) (auto) @@ -5446,7 +5444,7 @@ subsubsection \@{const transpose} on sorted lists\ lemma sorted_transpose[simp]: "sorted (rev (map length (transpose xs)))" -by (auto simp: sorted_equals_nth_mono rev_nth nth_transpose +by (auto simp: sorted_iff_nth_mono rev_nth nth_transpose length_filter_conv_card intro: card_mono) lemma transpose_max_length: @@ -5579,7 +5577,7 @@ (is "?trans = ?map") proof (rule nth_equalityI) have "sorted (rev (map length xs))" - by (auto simp: rev_nth rect intro!: sorted_nth_monoI) + by (auto simp: rev_nth rect sorted_iff_nth_mono) from foldr_max_sorted[OF this] assms show len: "length ?trans = length ?map" by (simp_all add: length_transpose foldr_map comp_def)