src/HOL/List.thy
changeset 68175 e0bd5089eabf
parent 68160 efce008331f6
child 68176 3e4af46a6f6a
     1.1 --- a/src/HOL/List.thy	Sun May 13 21:59:41 2018 +0200
     1.2 +++ b/src/HOL/List.thy	Mon May 14 15:37:26 2018 +0200
     1.3 @@ -4971,22 +4971,29 @@
     1.4  lemma sorted_wrt01: "length xs \<le> 1 \<Longrightarrow> sorted_wrt P xs"
     1.5  by(auto simp: le_Suc_eq length_Suc_conv)
     1.6  
     1.7 -lemma sorted_wrt_iff_nth_Suc:
     1.8 +lemma sorted_wrt_iff_nth_less:
     1.9    "sorted_wrt P xs = (\<forall>i j. i < j \<longrightarrow> j < length xs \<longrightarrow> P (xs ! i) (xs ! j))"
    1.10  apply(induction xs)
    1.11 - apply simp
    1.12 -apply(force simp: in_set_conv_nth nth_Cons split: nat.split)
    1.13 +apply(auto simp add: in_set_conv_nth Ball_def nth_Cons split: nat.split)
    1.14  done
    1.15  
    1.16  lemma sorted_wrt_nth_less:
    1.17    "\<lbrakk> sorted_wrt P xs; i < j; j < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) (xs ! j)"
    1.18 -by(auto simp: sorted_wrt_iff_nth_Suc)
    1.19 -
    1.20 -text \<open>Strictly Ascending Sequences of Natural Numbers\<close>
    1.21 +by(auto simp: sorted_wrt_iff_nth_less)
    1.22  
    1.23  lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m..<n]"
    1.24  by(induction n) (auto simp: sorted_wrt_append)
    1.25  
    1.26 +lemma sorted_wrt_upto[simp]: "sorted_wrt (<) [m..n]"
    1.27 +proof cases
    1.28 +  assume "n < m" thus ?thesis by simp
    1.29 +next
    1.30 +  assume "\<not> n < m"
    1.31 +  hence "m \<le> n" by simp
    1.32 +  thus ?thesis
    1.33 +    by(induction m rule:int_le_induct)(auto simp: upto_rec1)
    1.34 +qed
    1.35 +
    1.36  text \<open>Each element is greater or equal to its index:\<close>
    1.37  
    1.38  lemma sorted_wrt_less_idx:
    1.39 @@ -5021,6 +5028,14 @@
    1.40  
    1.41  lemmas [code] = sorted.simps(1) sorted2_simps
    1.42  
    1.43 +lemma sorted_append:
    1.44 +  "sorted (xs@ys) = (sorted xs \<and> sorted ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
    1.45 +by (simp add: sorted_sorted_wrt sorted_wrt_append)
    1.46 +
    1.47 +lemma sorted_map:
    1.48 +  "sorted (map f xs) = sorted_wrt (\<lambda>x y. f x \<le> f y) xs"
    1.49 +by (simp add: sorted_sorted_wrt sorted_wrt_map)
    1.50 +
    1.51  lemma sorted01: "length xs \<le> 1 \<Longrightarrow> sorted xs"
    1.52  by (simp add: sorted_sorted_wrt sorted_wrt01)
    1.53  
    1.54 @@ -5028,45 +5043,28 @@
    1.55    "sorted xs \<Longrightarrow> sorted (tl xs)"
    1.56  by (cases xs) (simp_all)
    1.57  
    1.58 -lemma sorted_append:
    1.59 -  "sorted (xs@ys) = (sorted xs \<and> sorted ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
    1.60 -by (induct xs) (auto)
    1.61 +lemma sorted_iff_nth_mono:
    1.62 +  "sorted xs = (\<forall>i j. i < j \<longrightarrow> j < length xs \<longrightarrow> xs ! i \<le> xs ! j)"
    1.63 +by (simp add: sorted_sorted_wrt sorted_wrt_iff_nth_less)
    1.64  
    1.65  lemma sorted_nth_mono:
    1.66    "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
    1.67 -by (induct xs arbitrary: i j) (auto simp:nth_Cons')
    1.68 +by (auto simp: sorted_iff_nth_mono nat_less_le)
    1.69  
    1.70  lemma sorted_rev_nth_mono:
    1.71    "sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"
    1.72  using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
    1.73        rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
    1.74  by auto
    1.75 -
    1.76 +(*
    1.77  lemma sorted_nth_monoI:
    1.78    "(\<And> i j. \<lbrakk> i \<le> j ; j < length xs \<rbrakk> \<Longrightarrow> xs ! i \<le> xs ! j) \<Longrightarrow> sorted xs"
    1.79 -proof (induct xs)
    1.80 -  case (Cons x xs)
    1.81 -  have "sorted xs"
    1.82 -  proof (rule Cons.hyps)
    1.83 -    fix i j assume "i \<le> j" and "j < length xs"
    1.84 -    with Cons.prems[of "Suc i" "Suc j"]
    1.85 -    show "xs ! i \<le> xs ! j" by auto
    1.86 -  qed
    1.87 -  moreover
    1.88 -  {
    1.89 -    fix y assume "y \<in> set xs"
    1.90 -    then obtain j where "j < length xs" and "xs ! j = y"
    1.91 -      unfolding in_set_conv_nth by blast
    1.92 -    with Cons.prems[of 0 "Suc j"] have "x \<le> y" by auto
    1.93 -  }
    1.94 -  ultimately
    1.95 -  show ?case by auto
    1.96 -qed simp
    1.97 +by (simp add: sorted_iff_nth_less)
    1.98  
    1.99  lemma sorted_equals_nth_mono:
   1.100    "sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"
   1.101 -by (auto intro: sorted_nth_monoI sorted_nth_mono)
   1.102 -
   1.103 +by (auto simp: sorted_iff_nth_less nat_less_le)
   1.104 +*)
   1.105  lemma sorted_map_remove1:
   1.106    "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
   1.107  by (induct xs) (auto)
   1.108 @@ -5446,7 +5444,7 @@
   1.109  subsubsection \<open>@{const transpose} on sorted lists\<close>
   1.110  
   1.111  lemma sorted_transpose[simp]: "sorted (rev (map length (transpose xs)))"
   1.112 -by (auto simp: sorted_equals_nth_mono rev_nth nth_transpose
   1.113 +by (auto simp: sorted_iff_nth_mono rev_nth nth_transpose
   1.114      length_filter_conv_card intro: card_mono)
   1.115  
   1.116  lemma transpose_max_length:
   1.117 @@ -5579,7 +5577,7 @@
   1.118      (is "?trans = ?map")
   1.119  proof (rule nth_equalityI)
   1.120    have "sorted (rev (map length xs))"
   1.121 -    by (auto simp: rev_nth rect intro!: sorted_nth_monoI)
   1.122 +    by (auto simp: rev_nth rect sorted_iff_nth_mono)
   1.123    from foldr_max_sorted[OF this] assms
   1.124    show len: "length ?trans = length ?map"
   1.125      by (simp_all add: length_transpose foldr_map comp_def)