merged
authorhaftmann
Wed Oct 27 16:40:34 2010 +0200 (2010-10-27)
changeset 4021143916ac560a4
parent 40209 8ec474f94d61
parent 40210 aee7ef725330
child 40219 b283680d8044
merged
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Oct 27 13:46:30 2010 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Oct 27 16:40:34 2010 +0200
     1.3 @@ -837,11 +837,11 @@
     1.4  context linorder
     1.5  begin
     1.6  
     1.7 -lemma multiset_of_insort_key [simp]:
     1.8 +lemma multiset_of_insort [simp]:
     1.9    "multiset_of (insort_key k x xs) = {#x#} + multiset_of xs"
    1.10    by (induct xs) (simp_all add: ac_simps)
    1.11   
    1.12 -lemma multiset_of_sort_key [simp]:
    1.13 +lemma multiset_of_sort [simp]:
    1.14    "multiset_of (sort_key k xs) = multiset_of xs"
    1.15    by (induct xs) (simp_all add: ac_simps)
    1.16  
     2.1 --- a/src/HOL/List.thy	Wed Oct 27 13:46:30 2010 +0200
     2.2 +++ b/src/HOL/List.thy	Wed Oct 27 16:40:34 2010 +0200
     2.3 @@ -303,11 +303,12 @@
     2.4  definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
     2.5  "sort_key f xs = foldr (insort_key f) xs []"
     2.6  
     2.7 +definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
     2.8 +  "insort_insert_key f x xs = (if f x \<in> f ` set xs then xs else insort_key f x xs)"
     2.9 +
    2.10  abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
    2.11  abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
    2.12 -
    2.13 -definition insort_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    2.14 -  "insort_insert x xs = (if x \<in> set xs then xs else insort x xs)"
    2.15 +abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)"
    2.16  
    2.17  end
    2.18  
    2.19 @@ -757,6 +758,14 @@
    2.20  
    2.21  subsubsection {* @{text map} *}
    2.22  
    2.23 +lemma hd_map:
    2.24 +  "xs \<noteq> [] \<Longrightarrow> hd (map f xs) = f (hd xs)"
    2.25 +  by (cases xs) simp_all
    2.26 +
    2.27 +lemma map_tl:
    2.28 +  "map f (tl xs) = tl (map f xs)"
    2.29 +  by (cases xs) simp_all
    2.30 +
    2.31  lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"
    2.32  by (induct xs) simp_all
    2.33  
    2.34 @@ -2669,6 +2678,10 @@
    2.35  
    2.36  subsubsection {* @{text "distinct"} and @{text remdups} *}
    2.37  
    2.38 +lemma distinct_tl:
    2.39 +  "distinct xs \<Longrightarrow> distinct (tl xs)"
    2.40 +  by (cases xs) simp_all
    2.41 +
    2.42  lemma distinct_append [simp]:
    2.43  "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
    2.44  by (induct xs) auto
    2.45 @@ -3629,12 +3642,18 @@
    2.46  context linorder
    2.47  begin
    2.48  
    2.49 -lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
    2.50 -by (induct xs, auto)
    2.51 +lemma length_insort [simp]:
    2.52 +  "length (insort_key f x xs) = Suc (length xs)"
    2.53 +  by (induct xs) simp_all
    2.54 +
    2.55 +lemma insort_key_left_comm:
    2.56 +  assumes "f x \<noteq> f y"
    2.57 +  shows "insort_key f y (insort_key f x xs) = insort_key f x (insort_key f y xs)"
    2.58 +  by (induct xs) (auto simp add: assms dest: antisym)
    2.59  
    2.60  lemma insort_left_comm:
    2.61    "insort x (insort y xs) = insort y (insort x xs)"
    2.62 -  by (induct xs) auto
    2.63 +  by (cases "x = y") (auto intro: insort_key_left_comm)
    2.64  
    2.65  lemma fun_left_comm_insort:
    2.66    "fun_left_comm insort"
    2.67 @@ -3657,6 +3676,10 @@
    2.68  apply(induct xs arbitrary: x) apply simp
    2.69  by simp (blast intro: order_trans)
    2.70  
    2.71 +lemma sorted_tl:
    2.72 +  "sorted xs \<Longrightarrow> sorted (tl xs)"
    2.73 +  by (cases xs) (simp_all add: sorted_Cons)
    2.74 +
    2.75  lemma sorted_append:
    2.76    "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
    2.77  by (induct xs) (auto simp add:sorted_Cons)
    2.78 @@ -3712,16 +3735,16 @@
    2.79  by(induct xs)(simp_all add:distinct_insort set_sort)
    2.80  
    2.81  lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
    2.82 -by(induct xs)(auto simp:sorted_Cons set_insort)
    2.83 +  by (induct xs) (auto simp:sorted_Cons set_insort)
    2.84  
    2.85  lemma sorted_insort: "sorted (insort x xs) = sorted xs"
    2.86 -using sorted_insort_key[where f="\<lambda>x. x"] by simp
    2.87 -
    2.88 -theorem sorted_sort_key[simp]: "sorted (map f (sort_key f xs))"
    2.89 -by(induct xs)(auto simp:sorted_insort_key)
    2.90 -
    2.91 -theorem sorted_sort[simp]: "sorted (sort xs)"
    2.92 -by(induct xs)(auto simp:sorted_insort)
    2.93 +  using sorted_insort_key [where f="\<lambda>x. x"] by simp
    2.94 +
    2.95 +theorem sorted_sort_key [simp]: "sorted (map f (sort_key f xs))"
    2.96 +  by (induct xs) (auto simp:sorted_insort_key)
    2.97 +
    2.98 +theorem sorted_sort [simp]: "sorted (sort xs)"
    2.99 +  using sorted_sort_key [where f="\<lambda>x. x"] by simp
   2.100  
   2.101  lemma sorted_butlast:
   2.102    assumes "xs \<noteq> []" and "sorted xs"
   2.103 @@ -3870,32 +3893,53 @@
   2.104    finally show "\<not> t < f x" by simp
   2.105  qed
   2.106  
   2.107 +lemma insort_insert_key_triv:
   2.108 +  "f x \<in> f ` set xs \<Longrightarrow> insort_insert_key f x xs = xs"
   2.109 +  by (simp add: insort_insert_key_def)
   2.110 +
   2.111 +lemma insort_insert_triv:
   2.112 +  "x \<in> set xs \<Longrightarrow> insort_insert x xs = xs"
   2.113 +  using insort_insert_key_triv [of "\<lambda>x. x"] by simp
   2.114 +
   2.115 +lemma insort_insert_insort_key:
   2.116 +  "f x \<notin> f ` set xs \<Longrightarrow> insort_insert_key f x xs = insort_key f x xs"
   2.117 +  by (simp add: insort_insert_key_def)
   2.118 +
   2.119 +lemma insort_insert_insort:
   2.120 +  "x \<notin> set xs \<Longrightarrow> insort_insert x xs = insort x xs"
   2.121 +  using insort_insert_insort_key [of "\<lambda>x. x"] by simp
   2.122 +
   2.123  lemma set_insort_insert:
   2.124    "set (insort_insert x xs) = insert x (set xs)"
   2.125 -  by (auto simp add: insort_insert_def set_insort)
   2.126 +  by (auto simp add: insort_insert_key_def set_insort)
   2.127  
   2.128  lemma distinct_insort_insert:
   2.129    assumes "distinct xs"
   2.130 -  shows "distinct (insort_insert x xs)"
   2.131 -  using assms by (induct xs) (auto simp add: insort_insert_def set_insort)
   2.132 +  shows "distinct (insort_insert_key f x xs)"
   2.133 +  using assms by (induct xs) (auto simp add: insort_insert_key_def set_insort)
   2.134 +
   2.135 +lemma sorted_insort_insert_key:
   2.136 +  assumes "sorted (map f xs)"
   2.137 +  shows "sorted (map f (insort_insert_key f x xs))"
   2.138 +  using assms by (simp add: insort_insert_key_def sorted_insort_key)
   2.139  
   2.140  lemma sorted_insort_insert:
   2.141    assumes "sorted xs"
   2.142    shows "sorted (insort_insert x xs)"
   2.143 -  using assms by (simp add: insort_insert_def sorted_insort)
   2.144 -
   2.145 -lemma filter_insort_key_triv:
   2.146 +  using assms sorted_insort_insert_key [of "\<lambda>x. x"] by simp
   2.147 +
   2.148 +lemma filter_insort_triv:
   2.149    "\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"
   2.150    by (induct xs) simp_all
   2.151  
   2.152 -lemma filter_insort_key:
   2.153 +lemma filter_insort:
   2.154    "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
   2.155    using assms by (induct xs)
   2.156      (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
   2.157  
   2.158 -lemma filter_sort_key:
   2.159 +lemma filter_sort:
   2.160    "filter P (sort_key f xs) = sort_key f (filter P xs)"
   2.161 -  by (induct xs) (simp_all add: filter_insort_key_triv filter_insort_key)
   2.162 +  by (induct xs) (simp_all add: filter_insort_triv filter_insort)
   2.163  
   2.164  lemma sorted_same [simp]:
   2.165    "sorted [x\<leftarrow>xs. x = f xs]"