src/HOL/List.thy
changeset 40210 aee7ef725330
parent 40195 430fff4a9167
child 40230 be5c622e1de2
     1.1 --- a/src/HOL/List.thy	Wed Oct 27 08:58:03 2010 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Oct 27 16:40:31 2010 +0200
     1.3 @@ -303,11 +303,12 @@
     1.4  definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
     1.5  "sort_key f xs = foldr (insort_key f) xs []"
     1.6  
     1.7 +definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
     1.8 +  "insort_insert_key f x xs = (if f x \<in> f ` set xs then xs else insort_key f x xs)"
     1.9 +
    1.10  abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
    1.11  abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
    1.12 -
    1.13 -definition insort_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.14 -  "insort_insert x xs = (if x \<in> set xs then xs else insort x xs)"
    1.15 +abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)"
    1.16  
    1.17  end
    1.18  
    1.19 @@ -757,6 +758,14 @@
    1.20  
    1.21  subsubsection {* @{text map} *}
    1.22  
    1.23 +lemma hd_map:
    1.24 +  "xs \<noteq> [] \<Longrightarrow> hd (map f xs) = f (hd xs)"
    1.25 +  by (cases xs) simp_all
    1.26 +
    1.27 +lemma map_tl:
    1.28 +  "map f (tl xs) = tl (map f xs)"
    1.29 +  by (cases xs) simp_all
    1.30 +
    1.31  lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"
    1.32  by (induct xs) simp_all
    1.33  
    1.34 @@ -2669,6 +2678,10 @@
    1.35  
    1.36  subsubsection {* @{text "distinct"} and @{text remdups} *}
    1.37  
    1.38 +lemma distinct_tl:
    1.39 +  "distinct xs \<Longrightarrow> distinct (tl xs)"
    1.40 +  by (cases xs) simp_all
    1.41 +
    1.42  lemma distinct_append [simp]:
    1.43  "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
    1.44  by (induct xs) auto
    1.45 @@ -3629,12 +3642,18 @@
    1.46  context linorder
    1.47  begin
    1.48  
    1.49 -lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
    1.50 -by (induct xs, auto)
    1.51 +lemma length_insort [simp]:
    1.52 +  "length (insort_key f x xs) = Suc (length xs)"
    1.53 +  by (induct xs) simp_all
    1.54 +
    1.55 +lemma insort_key_left_comm:
    1.56 +  assumes "f x \<noteq> f y"
    1.57 +  shows "insort_key f y (insort_key f x xs) = insort_key f x (insort_key f y xs)"
    1.58 +  by (induct xs) (auto simp add: assms dest: antisym)
    1.59  
    1.60  lemma insort_left_comm:
    1.61    "insort x (insort y xs) = insort y (insort x xs)"
    1.62 -  by (induct xs) auto
    1.63 +  by (cases "x = y") (auto intro: insort_key_left_comm)
    1.64  
    1.65  lemma fun_left_comm_insort:
    1.66    "fun_left_comm insort"
    1.67 @@ -3657,6 +3676,10 @@
    1.68  apply(induct xs arbitrary: x) apply simp
    1.69  by simp (blast intro: order_trans)
    1.70  
    1.71 +lemma sorted_tl:
    1.72 +  "sorted xs \<Longrightarrow> sorted (tl xs)"
    1.73 +  by (cases xs) (simp_all add: sorted_Cons)
    1.74 +
    1.75  lemma sorted_append:
    1.76    "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
    1.77  by (induct xs) (auto simp add:sorted_Cons)
    1.78 @@ -3712,16 +3735,16 @@
    1.79  by(induct xs)(simp_all add:distinct_insort set_sort)
    1.80  
    1.81  lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
    1.82 -by(induct xs)(auto simp:sorted_Cons set_insort)
    1.83 +  by (induct xs) (auto simp:sorted_Cons set_insort)
    1.84  
    1.85  lemma sorted_insort: "sorted (insort x xs) = sorted xs"
    1.86 -using sorted_insort_key[where f="\<lambda>x. x"] by simp
    1.87 -
    1.88 -theorem sorted_sort_key[simp]: "sorted (map f (sort_key f xs))"
    1.89 -by(induct xs)(auto simp:sorted_insort_key)
    1.90 -
    1.91 -theorem sorted_sort[simp]: "sorted (sort xs)"
    1.92 -by(induct xs)(auto simp:sorted_insort)
    1.93 +  using sorted_insort_key [where f="\<lambda>x. x"] by simp
    1.94 +
    1.95 +theorem sorted_sort_key [simp]: "sorted (map f (sort_key f xs))"
    1.96 +  by (induct xs) (auto simp:sorted_insort_key)
    1.97 +
    1.98 +theorem sorted_sort [simp]: "sorted (sort xs)"
    1.99 +  using sorted_sort_key [where f="\<lambda>x. x"] by simp
   1.100  
   1.101  lemma sorted_butlast:
   1.102    assumes "xs \<noteq> []" and "sorted xs"
   1.103 @@ -3870,32 +3893,53 @@
   1.104    finally show "\<not> t < f x" by simp
   1.105  qed
   1.106  
   1.107 +lemma insort_insert_key_triv:
   1.108 +  "f x \<in> f ` set xs \<Longrightarrow> insort_insert_key f x xs = xs"
   1.109 +  by (simp add: insort_insert_key_def)
   1.110 +
   1.111 +lemma insort_insert_triv:
   1.112 +  "x \<in> set xs \<Longrightarrow> insort_insert x xs = xs"
   1.113 +  using insort_insert_key_triv [of "\<lambda>x. x"] by simp
   1.114 +
   1.115 +lemma insort_insert_insort_key:
   1.116 +  "f x \<notin> f ` set xs \<Longrightarrow> insort_insert_key f x xs = insort_key f x xs"
   1.117 +  by (simp add: insort_insert_key_def)
   1.118 +
   1.119 +lemma insort_insert_insort:
   1.120 +  "x \<notin> set xs \<Longrightarrow> insort_insert x xs = insort x xs"
   1.121 +  using insort_insert_insort_key [of "\<lambda>x. x"] by simp
   1.122 +
   1.123  lemma set_insort_insert:
   1.124    "set (insort_insert x xs) = insert x (set xs)"
   1.125 -  by (auto simp add: insort_insert_def set_insort)
   1.126 +  by (auto simp add: insort_insert_key_def set_insort)
   1.127  
   1.128  lemma distinct_insort_insert:
   1.129    assumes "distinct xs"
   1.130 -  shows "distinct (insort_insert x xs)"
   1.131 -  using assms by (induct xs) (auto simp add: insort_insert_def set_insort)
   1.132 +  shows "distinct (insort_insert_key f x xs)"
   1.133 +  using assms by (induct xs) (auto simp add: insort_insert_key_def set_insort)
   1.134 +
   1.135 +lemma sorted_insort_insert_key:
   1.136 +  assumes "sorted (map f xs)"
   1.137 +  shows "sorted (map f (insort_insert_key f x xs))"
   1.138 +  using assms by (simp add: insort_insert_key_def sorted_insort_key)
   1.139  
   1.140  lemma sorted_insort_insert:
   1.141    assumes "sorted xs"
   1.142    shows "sorted (insort_insert x xs)"
   1.143 -  using assms by (simp add: insort_insert_def sorted_insort)
   1.144 -
   1.145 -lemma filter_insort_key_triv:
   1.146 +  using assms sorted_insort_insert_key [of "\<lambda>x. x"] by simp
   1.147 +
   1.148 +lemma filter_insort_triv:
   1.149    "\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"
   1.150    by (induct xs) simp_all
   1.151  
   1.152 -lemma filter_insort_key:
   1.153 +lemma filter_insort:
   1.154    "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
   1.155    using assms by (induct xs)
   1.156      (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
   1.157  
   1.158 -lemma filter_sort_key:
   1.159 +lemma filter_sort:
   1.160    "filter P (sort_key f xs) = sort_key f (filter P xs)"
   1.161 -  by (induct xs) (simp_all add: filter_insort_key_triv filter_insort_key)
   1.162 +  by (induct xs) (simp_all add: filter_insort_triv filter_insort)
   1.163  
   1.164  lemma sorted_same [simp]:
   1.165    "sorted [x\<leftarrow>xs. x = f xs]"