New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key

--- a/NEWS	Thu Nov 12 17:21:43 2009 +0100
+++ b/NEWS	Thu Nov 12 17:21:48 2009 +0100
@@ -94,6 +94,9 @@
 zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
 INCOMPATIBILITY.
 
+* Added theorem List.map_map as [simp]. Removed List.map_compose.
+INCOMPATIBILITY.
+
 * New testing tool "Mirabelle" for automated (proof) tools. Applies
 several tools and tactics like sledgehammer, metis, or quickcheck, to
 every proof step in a theory. To be used in batch mode via the

--- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -1928,7 +1928,8 @@
     { fix t n assume tnY: "(t,n) \<in> set ?Y" 
       hence "(t,n) \<in> set ?SS" by simp
       hence "\<exists> (t',n') \<in> set ?S. simp_num_pair (t',n') = (t,n)"
-        by (auto simp add: split_def) (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
+        by (auto simp add: split_def simp del: map_map)
+           (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
       then obtain t' n' where tn'S: "(t',n') \<in> set ?S" and tns: "simp_num_pair (t',n') = (t,n)" by blast
       from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" by auto
       from simp_num_pair_l[OF tnb np tns]

--- a/src/HOL/Decision_Procs/MIR.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -1522,7 +1522,7 @@
   also fix y have "\<dots> = (\<exists>x. (Ifm (y#bs) ?cyes) \<and> (Ifm (x#bs) ?cno))"
     using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
   also have "\<dots> = (Ifm bs (decr ?cyes) \<and> Ifm bs (E ?cno))"
-    by (auto simp add: decr[OF yes_nb])
+    by (auto simp add: decr[OF yes_nb] simp del: partition_filter_conv)
   also have "\<dots> = (Ifm bs (conj (decr ?cyes) (qe ?cno)))"
     using qe[rule_format, OF no_qf] by auto
   finally have "Ifm bs (E p) = Ifm bs (CJNB qe p)" 
@@ -5298,7 +5298,8 @@
     { fix t n assume tnY: "(t,n) \<in> set ?Y" 
       hence "(t,n) \<in> set ?SS" by simp
       hence "\<exists> (t',n') \<in> set ?S. simp_num_pair (t',n') = (t,n)"
-        by (auto simp add: split_def) (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
+        by (auto simp add: split_def simp del: map_map)
+           (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
       then obtain t' n' where tn'S: "(t',n') \<in> set ?S" and tns: "simp_num_pair (t',n') = (t,n)" by blast
       from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" by auto
       from simp_num_pair_l[OF tnb np tns]

--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -1233,7 +1233,7 @@
   also have "\<dots> = (\<exists>x. (Ifm vs (y#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
     using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
   also have "\<dots> = (Ifm vs bs (decr0 ?cyes) \<and> Ifm vs bs (E ?cno))"
-    by (auto simp add: decr0[OF yes_nb])
+    by (auto simp add: decr0[OF yes_nb] simp del: partition_filter_conv)
   also have "\<dots> = (Ifm vs bs (conj (decr0 ?cyes) (qe ?cno)))"
     using qe[rule_format, OF no_qf] by auto
   finally have "Ifm vs bs (E p) = Ifm vs bs (CJNB qe p)" 

--- a/src/HOL/Imperative_HOL/Heap.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/Imperative_HOL/Heap.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -231,7 +231,7 @@
 the literature?  *}
 
 lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
-  by (simp add: get_array_def set_array_def)
+  by (simp add: get_array_def set_array_def o_def)
 
 lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
   by (simp add: noteq_arrs_def get_array_def set_array_def)

--- a/src/HOL/Library/Enum.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/Library/Enum.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -72,7 +72,7 @@
   by (induct n) simp_all
 
 lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
-  by (induct n) (auto simp add: length_concat map_compose [symmetric] o_def listsum_triv)
+  by (induct n) (auto simp add: length_concat o_def listsum_triv)
 
 lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
   by (induct n arbitrary: ys) auto
@@ -246,7 +246,7 @@
     by (auto simp add: image_def)
   have "set (map set (sublists xs)) = Pow (set xs)"
     by (induct xs)
-      (simp_all add: aux Let_def Pow_insert Un_commute)
+      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
   then show ?thesis by simp
 qed
 

--- a/src/HOL/List.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/List.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -272,13 +272,16 @@
 "sorted [x] \<longleftrightarrow> True" |
 "sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
 
-primrec insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"insort x [] = [x]" |
-"insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))"
-
-primrec sort :: "'a list \<Rightarrow> 'a list" where
-"sort [] = []" |
-"sort (x#xs) = insort x (sort xs)"
+primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
+"insort_key f x [] = [x]" |
+"insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
+
+primrec sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
+"sort_key f [] = []" |
+"sort_key f (x#xs) = insort_key f x (sort_key f xs)"
+
+abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
+abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
 
 end
 
@@ -698,8 +701,11 @@
 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"
 by (induct xs) auto
 
-lemma map_compose: "map (f o g) xs = map f (map g xs)"
-by (induct xs) (auto simp add: o_def)
+lemma map_map [simp]: "map f (map g xs) = map (f \<circ> g) xs"
+by (induct xs) auto
+
+lemma map_compose: "map (f \<circ> g) xs = map f (map g xs)"
+by simp
 
 lemma rev_map: "rev (map f xs) = map f (rev xs)"
 by (induct xs) auto
@@ -1183,6 +1189,12 @@
   then show ?thesis by (auto simp add: partition_filter1 partition_filter2) 
 qed
 
+lemma partition_filter_conv[simp]:
+  "partition f xs = (filter f xs,filter (Not o f) xs)"
+unfolding partition_filter2[symmetric]
+unfolding partition_filter1[symmetric] by simp
+
+declare partition.simps[simp del]
 
 subsubsection {* @{text concat} *}
 
@@ -1722,6 +1734,9 @@
 
 subsubsection {* @{text takeWhile} and @{text dropWhile} *}
 
+lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
+  by (induct xs) auto
+
 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
 by (induct xs) auto
 
@@ -1736,6 +1751,15 @@
 lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
 by (induct xs) auto
 
+lemma takeWhile_nth: "j < length (takeWhile P xs) \<Longrightarrow> takeWhile P xs ! j = xs ! j"
+apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto
+
+lemma dropWhile_nth: "j < length (dropWhile P xs) \<Longrightarrow> dropWhile P xs ! j = xs ! (j + length (takeWhile P xs))"
+apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto
+
+lemma length_dropWhile_le: "length (dropWhile P xs) \<le> length xs"
+by (induct xs) auto
+
 lemma dropWhile_append1 [simp]:
 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
 by (induct xs) auto
@@ -1765,6 +1789,66 @@
 lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
 by (induct xs) auto
 
+lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \<circ> f) xs)"
+by (induct xs) auto
+
+lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \<circ> f) xs)"
+by (induct xs) auto
+
+lemma takeWhile_eq_take: "takeWhile P xs = take (length (takeWhile P xs)) xs"
+by (induct xs) auto
+
+lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs"
+by (induct xs) auto
+
+lemma hd_dropWhile:
+  "dropWhile P xs \<noteq> [] \<Longrightarrow> \<not> P (hd (dropWhile P xs))"
+using assms by (induct xs) auto
+
+lemma takeWhile_eq_filter:
+  assumes "\<And> x. x \<in> set (dropWhile P xs) \<Longrightarrow> \<not> P x"
+  shows "takeWhile P xs = filter P xs"
+proof -
+  have A: "filter P xs = filter P (takeWhile P xs @ dropWhile P xs)"
+    by simp
+  have B: "filter P (dropWhile P xs) = []"
+    unfolding filter_empty_conv using assms by blast
+  have "filter P xs = takeWhile P xs"
+    unfolding A filter_append B
+    by (auto simp add: filter_id_conv dest: set_takeWhileD)
+  thus ?thesis ..
+qed
+
+lemma takeWhile_eq_take_P_nth:
+  "\<lbrakk> \<And> i. \<lbrakk> i < n ; i < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) ; n < length xs \<Longrightarrow> \<not> P (xs ! n) \<rbrakk> \<Longrightarrow>
+  takeWhile P xs = take n xs"
+proof (induct xs arbitrary: n)
+  case (Cons x xs)
+  thus ?case
+  proof (cases n)
+    case (Suc n') note this[simp]
+    have "P x" using Cons.prems(1)[of 0] by simp
+    moreover have "takeWhile P xs = take n' xs"
+    proof (rule Cons.hyps)
+      case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
+    next case goal2 thus ?case using Cons by auto
+    qed
+    ultimately show ?thesis by simp
+   qed simp
+qed simp
+
+lemma nth_length_takeWhile:
+  "length (takeWhile P xs) < length xs \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"
+by (induct xs) auto
+
+lemma length_takeWhile_less_P_nth:
+  assumes all: "\<And> i. i < j \<Longrightarrow> P (xs ! i)" and "j \<le> length xs"
+  shows "j \<le> length (takeWhile P xs)"
+proof (rule classical)
+  assume "\<not> ?thesis"
+  hence "length (takeWhile P xs) < length xs" using assms by simp
+  thus ?thesis using all `\<not> ?thesis` nth_length_takeWhile[of P xs] by auto
+qed
 
 text{* The following two lemmmas could be generalized to an arbitrary
 property. *}
@@ -1838,19 +1922,32 @@
 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
 by (induct rule:list_induct2, simp_all)
 
+lemma zip_map_map:
+  "zip (map f xs) (map g ys) = map (\<lambda> (x, y). (f x, g y)) (zip xs ys)"
+proof (induct xs arbitrary: ys)
+  case (Cons x xs) note Cons_x_xs = Cons.hyps
+  show ?case
+  proof (cases ys)
+    case (Cons y ys')
+    show ?thesis unfolding Cons using Cons_x_xs by simp
+  qed simp
+qed simp
+
+lemma zip_map1:
+  "zip (map f xs) ys = map (\<lambda>(x, y). (f x, y)) (zip xs ys)"
+using zip_map_map[of f xs "\<lambda>x. x" ys] by simp
+
+lemma zip_map2:
+  "zip xs (map f ys) = map (\<lambda>(x, y). (x, f y)) (zip xs ys)"
+using zip_map_map[of "\<lambda>x. x" xs f ys] by simp
+
 lemma map_zip_map:
- "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
-apply(induct xs arbitrary:ys) apply simp
-apply(case_tac ys)
-apply simp_all
-done
+  "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
+unfolding zip_map1 by auto
 
 lemma map_zip_map2:
- "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
-apply(induct xs arbitrary:ys) apply simp
-apply(case_tac ys)
-apply simp_all
-done
+  "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
+unfolding zip_map2 by auto
 
 text{* Courtesy of Andreas Lochbihler: *}
 lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
@@ -1867,6 +1964,9 @@
 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
 by(simp add: set_conv_nth cong: rev_conj_cong)
 
+lemma zip_same: "((a,b) \<in> set (zip xs xs)) = (a \<in> set xs \<and> a = b)"
+by(induct xs) auto
+
 lemma zip_update:
   "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
 by(rule sym, simp add: update_zip)
@@ -1893,6 +1993,16 @@
 apply (case_tac ys, simp_all)
 done
 
+lemma zip_takeWhile_fst: "zip (takeWhile P xs) ys = takeWhile (P \<circ> fst) (zip xs ys)"
+proof (induct xs arbitrary: ys)
+  case (Cons x xs) thus ?case by (cases ys) auto
+qed simp
+
+lemma zip_takeWhile_snd: "zip xs (takeWhile P ys) = takeWhile (P \<circ> snd) (zip xs ys)"
+proof (induct xs arbitrary: ys)
+  case (Cons x xs) thus ?case by (cases ys) auto
+qed simp
+
 lemma set_zip_leftD:
   "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
 by (induct xs ys rule:list_induct2') auto
@@ -1913,6 +2023,35 @@
   "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
   by (auto simp add: zip_map_fst_snd)
 
+lemma distinct_zipI1:
+  "distinct xs \<Longrightarrow> distinct (zip xs ys)"
+proof (induct xs arbitrary: ys)
+  case (Cons x xs)
+  show ?case
+  proof (cases ys)
+    case (Cons y ys')
+    have "(x, y) \<notin> set (zip xs ys')"
+      using Cons.prems by (auto simp: set_zip)
+    thus ?thesis
+      unfolding Cons zip_Cons_Cons distinct.simps
+      using Cons.hyps Cons.prems by simp
+  qed simp
+qed simp
+
+lemma distinct_zipI2:
+  "distinct xs \<Longrightarrow> distinct (zip xs ys)"
+proof (induct xs arbitrary: ys)
+  case (Cons x xs)
+  show ?case
+  proof (cases ys)
+    case (Cons y ys')
+     have "(x, y) \<notin> set (zip xs ys')"
+      using Cons.prems by (auto simp: set_zip)
+    thus ?thesis
+      unfolding Cons zip_Cons_Cons distinct.simps
+      using Cons.hyps Cons.prems by simp
+  qed simp
+qed simp
 
 subsubsection {* @{text list_all2} *}
 
@@ -2259,6 +2398,12 @@
 lemma length_concat: "length (concat xss) = listsum (map length xss)"
 by (induct xss) simp_all
 
+lemma listsum_map_filter:
+  fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add"
+  assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0"
+  shows "listsum (map f (filter P xs)) = listsum (map f xs)"
+using assms by (induct xs) auto
+
 text{* For efficient code generation ---
        @{const listsum} is not tail recursive but @{const foldl} is. *}
 lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
@@ -2640,6 +2785,11 @@
  "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
 by(simp add: set_concat distinct_card[symmetric])
 
+lemma length_remdups_card_conv: "length(remdups xs) = card(set xs)"
+proof -
+  have xs: "concat[xs] = xs" by simp
+  from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp
+qed
 
 subsubsection {* @{text remove1} *}
 
@@ -3083,6 +3233,12 @@
 context linorder
 begin
 
+lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
+by (induct xs, auto)
+
+lemma length_sort[simp]: "length (sort_key f xs) = length xs"
+by (induct xs, auto)
+
 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
 apply(induct xs arbitrary: x) apply simp
 by simp (blast intro: order_trans)
@@ -3092,37 +3248,88 @@
 by (induct xs) (auto simp add:sorted_Cons)
 
 lemma sorted_nth_mono:
-  "sorted xs \<Longrightarrow> i <= j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i <= xs!j"
+  "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)
 
-lemma set_insort: "set(insort x xs) = insert x (set xs)"
+lemma sorted_rev_nth_mono:
+  "sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> 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:
+  "(\<And> i j. \<lbrakk> i \<le> j ; j < length xs \<rbrakk> \<Longrightarrow> xs ! i \<le> xs ! j) \<Longrightarrow> sorted xs"
+proof (induct xs)
+  case (Cons x xs)
+  have "sorted xs"
+  proof (rule Cons.hyps)
+    fix i j assume "i \<le> j" and "j < length xs"
+    with Cons.prems[of "Suc i" "Suc j"]
+    show "xs ! i \<le> xs ! j" by auto
+  qed
+  moreover
+  {
+    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
+  }
+  ultimately
+  show ?case
+    unfolding sorted_Cons by auto
+qed simp
+
+lemma sorted_equals_nth_mono:
+  "sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"
+by (auto intro: sorted_nth_monoI sorted_nth_mono)
+
+lemma set_insort: "set(insort_key f x xs) = insert x (set xs)"
 by (induct xs) auto
 
-lemma set_sort[simp]: "set(sort xs) = set xs"
+lemma set_sort[simp]: "set(sort_key f xs) = set xs"
 by (induct xs) (simp_all add:set_insort)
 
-lemma distinct_insort: "distinct (insort x xs) = (x \<notin> set xs \<and> distinct xs)"
+lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
 by(induct xs)(auto simp:set_insort)
 
-lemma distinct_sort[simp]: "distinct (sort xs) = distinct xs"
+lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
 by(induct xs)(simp_all add:distinct_insort set_sort)
 
+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)
+
 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
-apply (induct xs)
- apply(auto simp:sorted_Cons set_insort)
-done
+using sorted_insort_key[where f="\<lambda>x. x"] by simp
+
+theorem sorted_sort_key[simp]: "sorted (map f (sort_key f xs))"
+by(induct xs)(auto simp:sorted_insort_key)
 
 theorem sorted_sort[simp]: "sorted (sort xs)"
-by (induct xs) (auto simp:sorted_insort)
-
-lemma insort_is_Cons: "\<forall>x\<in>set xs. a \<le> x \<Longrightarrow> insort a xs = a # xs"
+by(induct xs)(auto simp:sorted_insort)
+
+lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
 by (cases xs) auto
 
 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
-by (induct xs, auto simp add: sorted_Cons)
+by(induct xs)(auto simp add: sorted_Cons)
+
+lemma insort_key_remove1: "\<lbrakk> a \<in> set xs; sorted (map f xs) ; inj_on f (set xs) \<rbrakk>
+  \<Longrightarrow> insort_key f a (remove1 a xs) = xs"
+proof (induct xs)
+  case (Cons x xs)
+  thus ?case
+  proof (cases "x = a")
+    case False
+    hence "f x \<noteq> f a" using Cons.prems by auto
+    hence "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
+    thus ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
+  qed (auto simp: sorted_Cons insort_is_Cons)
+qed simp
 
 lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
-by (induct xs, auto simp add: sorted_Cons insort_is_Cons)
+using insort_key_remove1[where f="\<lambda>x. x"] by simp
 
 lemma sorted_remdups[simp]:
   "sorted l \<Longrightarrow> sorted (remdups l)"
@@ -3178,6 +3385,11 @@
   case 3 then show ?case by (cases n) simp_all
 qed
 
+lemma sorted_dropWhile: "sorted xs \<Longrightarrow> sorted (dropWhile P xs)"
+  unfolding dropWhile_eq_drop by (rule sorted_drop)
+
+lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
+  apply (subst takeWhile_eq_take) by (rule sorted_take)
 
 end
 
@@ -3772,6 +3984,12 @@
   | "length_unique (x#xs) =
       (if x \<in> set xs then length_unique xs else Suc (length_unique xs))"
 
+primrec
+  concat_map :: "('a => 'b list) => 'a list => 'b list"
+where
+  "concat_map f [] = []"
+  | "concat_map f (x#xs) = f x @ concat_map f xs"
+
 text {*
   Only use @{text mem} for generating executable code.  Otherwise use
   @{prop "x : set xs"} instead --- it is much easier to reason about.
@@ -3865,7 +4083,11 @@
 
 lemma length_remdups_length_unique [code_unfold]:
   "length (remdups xs) = length_unique xs"
-  by (induct xs) simp_all
+by (induct xs) simp_all
+
+lemma concat_map_code[code_unfold]:
+  "concat(map f xs) = concat_map f xs"
+by (induct xs) simp_all
 
 declare INFI_def [code_unfold]
 declare SUPR_def [code_unfold]
@@ -3923,6 +4145,11 @@
   "setsum f (set [m..<n]) = listsum (map f [m..<n])"
 by (rule setsum_set_distinct_conv_listsum) simp
 
+text {* General equivalence between @{const listsum} and @{const setsum} *}
+lemma listsum_setsum_nth:
+  "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
+using setsum_set_upt_conv_listsum[of "op ! xs" 0 "length xs"]
+by (simp add: map_nth)
 
 text {* Code for summation over ints. *}
 

--- a/src/HOL/MicroJava/BV/JVM.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -117,11 +117,7 @@
 
   from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)
   also from w have "phi' = map OK (map ok_val phi')" 
-    apply (clarsimp simp add: wt_step_def not_Err_eq) 
-    apply (rule map_id [symmetric])
-    apply (erule allE, erule impE, assumption)
-    apply clarsimp
-    done    
+    by (auto simp add: wt_step_def not_Err_eq intro!: nth_equalityI)
   finally 
   have check_types:
     "check_types G maxs maxr (map OK (map ok_val phi'))" .

--- a/src/HOL/MicroJava/BV/LBVJVM.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -166,7 +166,7 @@
       by (simp add: check_types_def)
     also from step
     have [symmetric]: "map OK (map ok_val phi) = phi" 
-      by (auto intro!: map_id simp add: wt_step_def)
+      by (auto intro!: nth_equalityI simp add: wt_step_def)
     finally have "check_types G mxs ?mxr (map OK (map ok_val phi))" .
   }
   moreover {  

--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -269,12 +269,6 @@
   (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"
   by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def)
 
-
-lemma map_id [rule_format]:
-  "(\<forall>n < length xs. f (g (xs!n)) = xs!n) \<longrightarrow> map f (map g xs) = xs"
-  by (induct xs, auto)
-
-
 lemma is_type_pTs:
   "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; ((mn,pTs),rT,code) \<in> set mdecls \<rbrakk>
   \<Longrightarrow> set pTs \<subseteq> types G"

--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -552,7 +552,7 @@
 
 apply (simp only: wf_java_mdecl_def)
 apply (subgoal_tac "(\<forall>y\<in>set pns. y \<notin> set (map fst lvars))")
-apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd)
+apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd del: map_map)
 apply (intro strip)
 apply (simp (no_asm_simp) only: append_Cons [THEN sym])
 apply (rule progression_lvar_init_aux)

--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -68,7 +68,7 @@
 
     with fst_eq Cons 
     show "unique (map f (a # list)) = unique (a # list)"
-      by (simp add: unique_def fst_set)
+      by (simp add: unique_def fst_set image_compose)
   qed
 qed
 
@@ -292,7 +292,7 @@
 apply (simp add: method_def)
 apply (frule wf_subcls1)
 apply (simp add: comp_class_rec)
-apply (simp add: map_compose [THEN sym] split_iter split_compose del: map_compose)
+apply (simp add: split_iter split_compose map_map[symmetric] del: map_map)
 apply (rule_tac R="%x y. ((x S) = (Option.map (\<lambda>(D, rT, b). 
   (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))" 
   in class_rec_relation)

--- a/src/HOL/Word/WordShift.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/Word/WordShift.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -1113,7 +1113,7 @@
 
 lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))"
   unfolding word_rcat_def to_bl_def' of_bl_def
-  by (clarsimp simp add : bin_rcat_bl map_compose)
+  by (clarsimp simp add : bin_rcat_bl)
 
 lemma size_rcat_lem':
   "size (concat (map to_bl wl)) = length wl * size (hd wl)"