New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
authorhoelzl
Thu Nov 12 17:21:48 2009 +0100 (2009-11-12)
changeset 33639603320b93668
parent 33638 548a34929e98
child 33640 0d82107dc07a
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
NEWS
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Imperative_HOL/Heap.thy
src/HOL/Library/Enum.thy
src/HOL/List.thy
src/HOL/MicroJava/BV/JVM.thy
src/HOL/MicroJava/BV/LBVJVM.thy
src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/MicroJava/Comp/LemmasComp.thy
src/HOL/Word/WordShift.thy
     1.1 --- a/NEWS	Thu Nov 12 17:21:43 2009 +0100
     1.2 +++ b/NEWS	Thu Nov 12 17:21:48 2009 +0100
     1.3 @@ -94,6 +94,9 @@
     1.4  zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Added theorem List.map_map as [simp]. Removed List.map_compose.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * New testing tool "Mirabelle" for automated (proof) tools. Applies
    1.11  several tools and tactics like sledgehammer, metis, or quickcheck, to
    1.12  every proof step in a theory. To be used in batch mode via the
     2.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Nov 12 17:21:43 2009 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Nov 12 17:21:48 2009 +0100
     2.3 @@ -1928,7 +1928,8 @@
     2.4      { fix t n assume tnY: "(t,n) \<in> set ?Y" 
     2.5        hence "(t,n) \<in> set ?SS" by simp
     2.6        hence "\<exists> (t',n') \<in> set ?S. simp_num_pair (t',n') = (t,n)"
     2.7 -        by (auto simp add: split_def) (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
     2.8 +        by (auto simp add: split_def simp del: map_map)
     2.9 +           (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
    2.10        then obtain t' n' where tn'S: "(t',n') \<in> set ?S" and tns: "simp_num_pair (t',n') = (t,n)" by blast
    2.11        from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" by auto
    2.12        from simp_num_pair_l[OF tnb np tns]
     3.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Nov 12 17:21:43 2009 +0100
     3.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Nov 12 17:21:48 2009 +0100
     3.3 @@ -1522,7 +1522,7 @@
     3.4    also fix y have "\<dots> = (\<exists>x. (Ifm (y#bs) ?cyes) \<and> (Ifm (x#bs) ?cno))"
     3.5      using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
     3.6    also have "\<dots> = (Ifm bs (decr ?cyes) \<and> Ifm bs (E ?cno))"
     3.7 -    by (auto simp add: decr[OF yes_nb])
     3.8 +    by (auto simp add: decr[OF yes_nb] simp del: partition_filter_conv)
     3.9    also have "\<dots> = (Ifm bs (conj (decr ?cyes) (qe ?cno)))"
    3.10      using qe[rule_format, OF no_qf] by auto
    3.11    finally have "Ifm bs (E p) = Ifm bs (CJNB qe p)" 
    3.12 @@ -5298,7 +5298,8 @@
    3.13      { fix t n assume tnY: "(t,n) \<in> set ?Y" 
    3.14        hence "(t,n) \<in> set ?SS" by simp
    3.15        hence "\<exists> (t',n') \<in> set ?S. simp_num_pair (t',n') = (t,n)"
    3.16 -        by (auto simp add: split_def) (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
    3.17 +        by (auto simp add: split_def simp del: map_map)
    3.18 +           (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all)
    3.19        then obtain t' n' where tn'S: "(t',n') \<in> set ?S" and tns: "simp_num_pair (t',n') = (t,n)" by blast
    3.20        from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" by auto
    3.21        from simp_num_pair_l[OF tnb np tns]
     4.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Nov 12 17:21:43 2009 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Nov 12 17:21:48 2009 +0100
     4.3 @@ -1233,7 +1233,7 @@
     4.4    also have "\<dots> = (\<exists>x. (Ifm vs (y#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
     4.5      using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
     4.6    also have "\<dots> = (Ifm vs bs (decr0 ?cyes) \<and> Ifm vs bs (E ?cno))"
     4.7 -    by (auto simp add: decr0[OF yes_nb])
     4.8 +    by (auto simp add: decr0[OF yes_nb] simp del: partition_filter_conv)
     4.9    also have "\<dots> = (Ifm vs bs (conj (decr0 ?cyes) (qe ?cno)))"
    4.10      using qe[rule_format, OF no_qf] by auto
    4.11    finally have "Ifm vs bs (E p) = Ifm vs bs (CJNB qe p)" 
     5.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Thu Nov 12 17:21:43 2009 +0100
     5.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Thu Nov 12 17:21:48 2009 +0100
     5.3 @@ -231,7 +231,7 @@
     5.4  the literature?  *}
     5.5  
     5.6  lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
     5.7 -  by (simp add: get_array_def set_array_def)
     5.8 +  by (simp add: get_array_def set_array_def o_def)
     5.9  
    5.10  lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
    5.11    by (simp add: noteq_arrs_def get_array_def set_array_def)
     6.1 --- a/src/HOL/Library/Enum.thy	Thu Nov 12 17:21:43 2009 +0100
     6.2 +++ b/src/HOL/Library/Enum.thy	Thu Nov 12 17:21:48 2009 +0100
     6.3 @@ -72,7 +72,7 @@
     6.4    by (induct n) simp_all
     6.5  
     6.6  lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
     6.7 -  by (induct n) (auto simp add: length_concat map_compose [symmetric] o_def listsum_triv)
     6.8 +  by (induct n) (auto simp add: length_concat o_def listsum_triv)
     6.9  
    6.10  lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
    6.11    by (induct n arbitrary: ys) auto
    6.12 @@ -246,7 +246,7 @@
    6.13      by (auto simp add: image_def)
    6.14    have "set (map set (sublists xs)) = Pow (set xs)"
    6.15      by (induct xs)
    6.16 -      (simp_all add: aux Let_def Pow_insert Un_commute)
    6.17 +      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
    6.18    then show ?thesis by simp
    6.19  qed
    6.20  
     7.1 --- a/src/HOL/List.thy	Thu Nov 12 17:21:43 2009 +0100
     7.2 +++ b/src/HOL/List.thy	Thu Nov 12 17:21:48 2009 +0100
     7.3 @@ -272,13 +272,16 @@
     7.4  "sorted [x] \<longleftrightarrow> True" |
     7.5  "sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
     7.6  
     7.7 -primrec insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
     7.8 -"insort x [] = [x]" |
     7.9 -"insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))"
    7.10 -
    7.11 -primrec sort :: "'a list \<Rightarrow> 'a list" where
    7.12 -"sort [] = []" |
    7.13 -"sort (x#xs) = insort x (sort xs)"
    7.14 +primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
    7.15 +"insort_key f x [] = [x]" |
    7.16 +"insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
    7.17 +
    7.18 +primrec sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
    7.19 +"sort_key f [] = []" |
    7.20 +"sort_key f (x#xs) = insort_key f x (sort_key f xs)"
    7.21 +
    7.22 +abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
    7.23 +abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
    7.24  
    7.25  end
    7.26  
    7.27 @@ -698,8 +701,11 @@
    7.28  lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"
    7.29  by (induct xs) auto
    7.30  
    7.31 -lemma map_compose: "map (f o g) xs = map f (map g xs)"
    7.32 -by (induct xs) (auto simp add: o_def)
    7.33 +lemma map_map [simp]: "map f (map g xs) = map (f \<circ> g) xs"
    7.34 +by (induct xs) auto
    7.35 +
    7.36 +lemma map_compose: "map (f \<circ> g) xs = map f (map g xs)"
    7.37 +by simp
    7.38  
    7.39  lemma rev_map: "rev (map f xs) = map f (rev xs)"
    7.40  by (induct xs) auto
    7.41 @@ -1183,6 +1189,12 @@
    7.42    then show ?thesis by (auto simp add: partition_filter1 partition_filter2) 
    7.43  qed
    7.44  
    7.45 +lemma partition_filter_conv[simp]:
    7.46 +  "partition f xs = (filter f xs,filter (Not o f) xs)"
    7.47 +unfolding partition_filter2[symmetric]
    7.48 +unfolding partition_filter1[symmetric] by simp
    7.49 +
    7.50 +declare partition.simps[simp del]
    7.51  
    7.52  subsubsection {* @{text concat} *}
    7.53  
    7.54 @@ -1722,6 +1734,9 @@
    7.55  
    7.56  subsubsection {* @{text takeWhile} and @{text dropWhile} *}
    7.57  
    7.58 +lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
    7.59 +  by (induct xs) auto
    7.60 +
    7.61  lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
    7.62  by (induct xs) auto
    7.63  
    7.64 @@ -1736,6 +1751,15 @@
    7.65  lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
    7.66  by (induct xs) auto
    7.67  
    7.68 +lemma takeWhile_nth: "j < length (takeWhile P xs) \<Longrightarrow> takeWhile P xs ! j = xs ! j"
    7.69 +apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto
    7.70 +
    7.71 +lemma dropWhile_nth: "j < length (dropWhile P xs) \<Longrightarrow> dropWhile P xs ! j = xs ! (j + length (takeWhile P xs))"
    7.72 +apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto
    7.73 +
    7.74 +lemma length_dropWhile_le: "length (dropWhile P xs) \<le> length xs"
    7.75 +by (induct xs) auto
    7.76 +
    7.77  lemma dropWhile_append1 [simp]:
    7.78  "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
    7.79  by (induct xs) auto
    7.80 @@ -1765,6 +1789,66 @@
    7.81  lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
    7.82  by (induct xs) auto
    7.83  
    7.84 +lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \<circ> f) xs)"
    7.85 +by (induct xs) auto
    7.86 +
    7.87 +lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \<circ> f) xs)"
    7.88 +by (induct xs) auto
    7.89 +
    7.90 +lemma takeWhile_eq_take: "takeWhile P xs = take (length (takeWhile P xs)) xs"
    7.91 +by (induct xs) auto
    7.92 +
    7.93 +lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs"
    7.94 +by (induct xs) auto
    7.95 +
    7.96 +lemma hd_dropWhile:
    7.97 +  "dropWhile P xs \<noteq> [] \<Longrightarrow> \<not> P (hd (dropWhile P xs))"
    7.98 +using assms by (induct xs) auto
    7.99 +
   7.100 +lemma takeWhile_eq_filter:
   7.101 +  assumes "\<And> x. x \<in> set (dropWhile P xs) \<Longrightarrow> \<not> P x"
   7.102 +  shows "takeWhile P xs = filter P xs"
   7.103 +proof -
   7.104 +  have A: "filter P xs = filter P (takeWhile P xs @ dropWhile P xs)"
   7.105 +    by simp
   7.106 +  have B: "filter P (dropWhile P xs) = []"
   7.107 +    unfolding filter_empty_conv using assms by blast
   7.108 +  have "filter P xs = takeWhile P xs"
   7.109 +    unfolding A filter_append B
   7.110 +    by (auto simp add: filter_id_conv dest: set_takeWhileD)
   7.111 +  thus ?thesis ..
   7.112 +qed
   7.113 +
   7.114 +lemma takeWhile_eq_take_P_nth:
   7.115 +  "\<lbrakk> \<And> i. \<lbrakk> i < n ; i < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) ; n < length xs \<Longrightarrow> \<not> P (xs ! n) \<rbrakk> \<Longrightarrow>
   7.116 +  takeWhile P xs = take n xs"
   7.117 +proof (induct xs arbitrary: n)
   7.118 +  case (Cons x xs)
   7.119 +  thus ?case
   7.120 +  proof (cases n)
   7.121 +    case (Suc n') note this[simp]
   7.122 +    have "P x" using Cons.prems(1)[of 0] by simp
   7.123 +    moreover have "takeWhile P xs = take n' xs"
   7.124 +    proof (rule Cons.hyps)
   7.125 +      case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
   7.126 +    next case goal2 thus ?case using Cons by auto
   7.127 +    qed
   7.128 +    ultimately show ?thesis by simp
   7.129 +   qed simp
   7.130 +qed simp
   7.131 +
   7.132 +lemma nth_length_takeWhile:
   7.133 +  "length (takeWhile P xs) < length xs \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"
   7.134 +by (induct xs) auto
   7.135 +
   7.136 +lemma length_takeWhile_less_P_nth:
   7.137 +  assumes all: "\<And> i. i < j \<Longrightarrow> P (xs ! i)" and "j \<le> length xs"
   7.138 +  shows "j \<le> length (takeWhile P xs)"
   7.139 +proof (rule classical)
   7.140 +  assume "\<not> ?thesis"
   7.141 +  hence "length (takeWhile P xs) < length xs" using assms by simp
   7.142 +  thus ?thesis using all `\<not> ?thesis` nth_length_takeWhile[of P xs] by auto
   7.143 +qed
   7.144  
   7.145  text{* The following two lemmmas could be generalized to an arbitrary
   7.146  property. *}
   7.147 @@ -1838,19 +1922,32 @@
   7.148  "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
   7.149  by (induct rule:list_induct2, simp_all)
   7.150  
   7.151 +lemma zip_map_map:
   7.152 +  "zip (map f xs) (map g ys) = map (\<lambda> (x, y). (f x, g y)) (zip xs ys)"
   7.153 +proof (induct xs arbitrary: ys)
   7.154 +  case (Cons x xs) note Cons_x_xs = Cons.hyps
   7.155 +  show ?case
   7.156 +  proof (cases ys)
   7.157 +    case (Cons y ys')
   7.158 +    show ?thesis unfolding Cons using Cons_x_xs by simp
   7.159 +  qed simp
   7.160 +qed simp
   7.161 +
   7.162 +lemma zip_map1:
   7.163 +  "zip (map f xs) ys = map (\<lambda>(x, y). (f x, y)) (zip xs ys)"
   7.164 +using zip_map_map[of f xs "\<lambda>x. x" ys] by simp
   7.165 +
   7.166 +lemma zip_map2:
   7.167 +  "zip xs (map f ys) = map (\<lambda>(x, y). (x, f y)) (zip xs ys)"
   7.168 +using zip_map_map[of "\<lambda>x. x" xs f ys] by simp
   7.169 +
   7.170  lemma map_zip_map:
   7.171 - "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
   7.172 -apply(induct xs arbitrary:ys) apply simp
   7.173 -apply(case_tac ys)
   7.174 -apply simp_all
   7.175 -done
   7.176 +  "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
   7.177 +unfolding zip_map1 by auto
   7.178  
   7.179  lemma map_zip_map2:
   7.180 - "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
   7.181 -apply(induct xs arbitrary:ys) apply simp
   7.182 -apply(case_tac ys)
   7.183 -apply simp_all
   7.184 -done
   7.185 +  "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
   7.186 +unfolding zip_map2 by auto
   7.187  
   7.188  text{* Courtesy of Andreas Lochbihler: *}
   7.189  lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
   7.190 @@ -1867,6 +1964,9 @@
   7.191  "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
   7.192  by(simp add: set_conv_nth cong: rev_conj_cong)
   7.193  
   7.194 +lemma zip_same: "((a,b) \<in> set (zip xs xs)) = (a \<in> set xs \<and> a = b)"
   7.195 +by(induct xs) auto
   7.196 +
   7.197  lemma zip_update:
   7.198    "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
   7.199  by(rule sym, simp add: update_zip)
   7.200 @@ -1893,6 +1993,16 @@
   7.201  apply (case_tac ys, simp_all)
   7.202  done
   7.203  
   7.204 +lemma zip_takeWhile_fst: "zip (takeWhile P xs) ys = takeWhile (P \<circ> fst) (zip xs ys)"
   7.205 +proof (induct xs arbitrary: ys)
   7.206 +  case (Cons x xs) thus ?case by (cases ys) auto
   7.207 +qed simp
   7.208 +
   7.209 +lemma zip_takeWhile_snd: "zip xs (takeWhile P ys) = takeWhile (P \<circ> snd) (zip xs ys)"
   7.210 +proof (induct xs arbitrary: ys)
   7.211 +  case (Cons x xs) thus ?case by (cases ys) auto
   7.212 +qed simp
   7.213 +
   7.214  lemma set_zip_leftD:
   7.215    "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
   7.216  by (induct xs ys rule:list_induct2') auto
   7.217 @@ -1913,6 +2023,35 @@
   7.218    "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
   7.219    by (auto simp add: zip_map_fst_snd)
   7.220  
   7.221 +lemma distinct_zipI1:
   7.222 +  "distinct xs \<Longrightarrow> distinct (zip xs ys)"
   7.223 +proof (induct xs arbitrary: ys)
   7.224 +  case (Cons x xs)
   7.225 +  show ?case
   7.226 +  proof (cases ys)
   7.227 +    case (Cons y ys')
   7.228 +    have "(x, y) \<notin> set (zip xs ys')"
   7.229 +      using Cons.prems by (auto simp: set_zip)
   7.230 +    thus ?thesis
   7.231 +      unfolding Cons zip_Cons_Cons distinct.simps
   7.232 +      using Cons.hyps Cons.prems by simp
   7.233 +  qed simp
   7.234 +qed simp
   7.235 +
   7.236 +lemma distinct_zipI2:
   7.237 +  "distinct xs \<Longrightarrow> distinct (zip xs ys)"
   7.238 +proof (induct xs arbitrary: ys)
   7.239 +  case (Cons x xs)
   7.240 +  show ?case
   7.241 +  proof (cases ys)
   7.242 +    case (Cons y ys')
   7.243 +     have "(x, y) \<notin> set (zip xs ys')"
   7.244 +      using Cons.prems by (auto simp: set_zip)
   7.245 +    thus ?thesis
   7.246 +      unfolding Cons zip_Cons_Cons distinct.simps
   7.247 +      using Cons.hyps Cons.prems by simp
   7.248 +  qed simp
   7.249 +qed simp
   7.250  
   7.251  subsubsection {* @{text list_all2} *}
   7.252  
   7.253 @@ -2259,6 +2398,12 @@
   7.254  lemma length_concat: "length (concat xss) = listsum (map length xss)"
   7.255  by (induct xss) simp_all
   7.256  
   7.257 +lemma listsum_map_filter:
   7.258 +  fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add"
   7.259 +  assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0"
   7.260 +  shows "listsum (map f (filter P xs)) = listsum (map f xs)"
   7.261 +using assms by (induct xs) auto
   7.262 +
   7.263  text{* For efficient code generation ---
   7.264         @{const listsum} is not tail recursive but @{const foldl} is. *}
   7.265  lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
   7.266 @@ -2640,6 +2785,11 @@
   7.267   "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
   7.268  by(simp add: set_concat distinct_card[symmetric])
   7.269  
   7.270 +lemma length_remdups_card_conv: "length(remdups xs) = card(set xs)"
   7.271 +proof -
   7.272 +  have xs: "concat[xs] = xs" by simp
   7.273 +  from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp
   7.274 +qed
   7.275  
   7.276  subsubsection {* @{text remove1} *}
   7.277  
   7.278 @@ -3083,6 +3233,12 @@
   7.279  context linorder
   7.280  begin
   7.281  
   7.282 +lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
   7.283 +by (induct xs, auto)
   7.284 +
   7.285 +lemma length_sort[simp]: "length (sort_key f xs) = length xs"
   7.286 +by (induct xs, auto)
   7.287 +
   7.288  lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
   7.289  apply(induct xs arbitrary: x) apply simp
   7.290  by simp (blast intro: order_trans)
   7.291 @@ -3092,37 +3248,88 @@
   7.292  by (induct xs) (auto simp add:sorted_Cons)
   7.293  
   7.294  lemma sorted_nth_mono:
   7.295 -  "sorted xs \<Longrightarrow> i <= j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i <= xs!j"
   7.296 +  "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
   7.297  by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)
   7.298  
   7.299 -lemma set_insort: "set(insort x xs) = insert x (set xs)"
   7.300 +lemma sorted_rev_nth_mono:
   7.301 +  "sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"
   7.302 +using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
   7.303 +      rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
   7.304 +by auto
   7.305 +
   7.306 +lemma sorted_nth_monoI:
   7.307 +  "(\<And> i j. \<lbrakk> i \<le> j ; j < length xs \<rbrakk> \<Longrightarrow> xs ! i \<le> xs ! j) \<Longrightarrow> sorted xs"
   7.308 +proof (induct xs)
   7.309 +  case (Cons x xs)
   7.310 +  have "sorted xs"
   7.311 +  proof (rule Cons.hyps)
   7.312 +    fix i j assume "i \<le> j" and "j < length xs"
   7.313 +    with Cons.prems[of "Suc i" "Suc j"]
   7.314 +    show "xs ! i \<le> xs ! j" by auto
   7.315 +  qed
   7.316 +  moreover
   7.317 +  {
   7.318 +    fix y assume "y \<in> set xs"
   7.319 +    then obtain j where "j < length xs" and "xs ! j = y"
   7.320 +      unfolding in_set_conv_nth by blast
   7.321 +    with Cons.prems[of 0 "Suc j"]
   7.322 +    have "x \<le> y"
   7.323 +      by auto
   7.324 +  }
   7.325 +  ultimately
   7.326 +  show ?case
   7.327 +    unfolding sorted_Cons by auto
   7.328 +qed simp
   7.329 +
   7.330 +lemma sorted_equals_nth_mono:
   7.331 +  "sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"
   7.332 +by (auto intro: sorted_nth_monoI sorted_nth_mono)
   7.333 +
   7.334 +lemma set_insort: "set(insort_key f x xs) = insert x (set xs)"
   7.335  by (induct xs) auto
   7.336  
   7.337 -lemma set_sort[simp]: "set(sort xs) = set xs"
   7.338 +lemma set_sort[simp]: "set(sort_key f xs) = set xs"
   7.339  by (induct xs) (simp_all add:set_insort)
   7.340  
   7.341 -lemma distinct_insort: "distinct (insort x xs) = (x \<notin> set xs \<and> distinct xs)"
   7.342 +lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
   7.343  by(induct xs)(auto simp:set_insort)
   7.344  
   7.345 -lemma distinct_sort[simp]: "distinct (sort xs) = distinct xs"
   7.346 +lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
   7.347  by(induct xs)(simp_all add:distinct_insort set_sort)
   7.348  
   7.349 +lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
   7.350 +by(induct xs)(auto simp:sorted_Cons set_insort)
   7.351 +
   7.352  lemma sorted_insort: "sorted (insort x xs) = sorted xs"
   7.353 -apply (induct xs)
   7.354 - apply(auto simp:sorted_Cons set_insort)
   7.355 -done
   7.356 +using sorted_insort_key[where f="\<lambda>x. x"] by simp
   7.357 +
   7.358 +theorem sorted_sort_key[simp]: "sorted (map f (sort_key f xs))"
   7.359 +by(induct xs)(auto simp:sorted_insort_key)
   7.360  
   7.361  theorem sorted_sort[simp]: "sorted (sort xs)"
   7.362 -by (induct xs) (auto simp:sorted_insort)
   7.363 -
   7.364 -lemma insort_is_Cons: "\<forall>x\<in>set xs. a \<le> x \<Longrightarrow> insort a xs = a # xs"
   7.365 +by(induct xs)(auto simp:sorted_insort)
   7.366 +
   7.367 +lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
   7.368  by (cases xs) auto
   7.369  
   7.370  lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
   7.371 -by (induct xs, auto simp add: sorted_Cons)
   7.372 +by(induct xs)(auto simp add: sorted_Cons)
   7.373 +
   7.374 +lemma insort_key_remove1: "\<lbrakk> a \<in> set xs; sorted (map f xs) ; inj_on f (set xs) \<rbrakk>
   7.375 +  \<Longrightarrow> insort_key f a (remove1 a xs) = xs"
   7.376 +proof (induct xs)
   7.377 +  case (Cons x xs)
   7.378 +  thus ?case
   7.379 +  proof (cases "x = a")
   7.380 +    case False
   7.381 +    hence "f x \<noteq> f a" using Cons.prems by auto
   7.382 +    hence "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
   7.383 +    thus ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
   7.384 +  qed (auto simp: sorted_Cons insort_is_Cons)
   7.385 +qed simp
   7.386  
   7.387  lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
   7.388 -by (induct xs, auto simp add: sorted_Cons insort_is_Cons)
   7.389 +using insort_key_remove1[where f="\<lambda>x. x"] by simp
   7.390  
   7.391  lemma sorted_remdups[simp]:
   7.392    "sorted l \<Longrightarrow> sorted (remdups l)"
   7.393 @@ -3178,6 +3385,11 @@
   7.394    case 3 then show ?case by (cases n) simp_all
   7.395  qed
   7.396  
   7.397 +lemma sorted_dropWhile: "sorted xs \<Longrightarrow> sorted (dropWhile P xs)"
   7.398 +  unfolding dropWhile_eq_drop by (rule sorted_drop)
   7.399 +
   7.400 +lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
   7.401 +  apply (subst takeWhile_eq_take) by (rule sorted_take)
   7.402  
   7.403  end
   7.404  
   7.405 @@ -3772,6 +3984,12 @@
   7.406    | "length_unique (x#xs) =
   7.407        (if x \<in> set xs then length_unique xs else Suc (length_unique xs))"
   7.408  
   7.409 +primrec
   7.410 +  concat_map :: "('a => 'b list) => 'a list => 'b list"
   7.411 +where
   7.412 +  "concat_map f [] = []"
   7.413 +  | "concat_map f (x#xs) = f x @ concat_map f xs"
   7.414 +
   7.415  text {*
   7.416    Only use @{text mem} for generating executable code.  Otherwise use
   7.417    @{prop "x : set xs"} instead --- it is much easier to reason about.
   7.418 @@ -3865,7 +4083,11 @@
   7.419  
   7.420  lemma length_remdups_length_unique [code_unfold]:
   7.421    "length (remdups xs) = length_unique xs"
   7.422 -  by (induct xs) simp_all
   7.423 +by (induct xs) simp_all
   7.424 +
   7.425 +lemma concat_map_code[code_unfold]:
   7.426 +  "concat(map f xs) = concat_map f xs"
   7.427 +by (induct xs) simp_all
   7.428  
   7.429  declare INFI_def [code_unfold]
   7.430  declare SUPR_def [code_unfold]
   7.431 @@ -3923,6 +4145,11 @@
   7.432    "setsum f (set [m..<n]) = listsum (map f [m..<n])"
   7.433  by (rule setsum_set_distinct_conv_listsum) simp
   7.434  
   7.435 +text {* General equivalence between @{const listsum} and @{const setsum} *}
   7.436 +lemma listsum_setsum_nth:
   7.437 +  "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
   7.438 +using setsum_set_upt_conv_listsum[of "op ! xs" 0 "length xs"]
   7.439 +by (simp add: map_nth)
   7.440  
   7.441  text {* Code for summation over ints. *}
   7.442  
     8.1 --- a/src/HOL/MicroJava/BV/JVM.thy	Thu Nov 12 17:21:43 2009 +0100
     8.2 +++ b/src/HOL/MicroJava/BV/JVM.thy	Thu Nov 12 17:21:48 2009 +0100
     8.3 @@ -117,11 +117,7 @@
     8.4  
     8.5    from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)
     8.6    also from w have "phi' = map OK (map ok_val phi')" 
     8.7 -    apply (clarsimp simp add: wt_step_def not_Err_eq) 
     8.8 -    apply (rule map_id [symmetric])
     8.9 -    apply (erule allE, erule impE, assumption)
    8.10 -    apply clarsimp
    8.11 -    done    
    8.12 +    by (auto simp add: wt_step_def not_Err_eq intro!: nth_equalityI)
    8.13    finally 
    8.14    have check_types:
    8.15      "check_types G maxs maxr (map OK (map ok_val phi'))" .
     9.1 --- a/src/HOL/MicroJava/BV/LBVJVM.thy	Thu Nov 12 17:21:43 2009 +0100
     9.2 +++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Thu Nov 12 17:21:48 2009 +0100
     9.3 @@ -166,7 +166,7 @@
     9.4        by (simp add: check_types_def)
     9.5      also from step
     9.6      have [symmetric]: "map OK (map ok_val phi) = phi" 
     9.7 -      by (auto intro!: map_id simp add: wt_step_def)
     9.8 +      by (auto intro!: nth_equalityI simp add: wt_step_def)
     9.9      finally have "check_types G mxs ?mxr (map OK (map ok_val phi))" .
    9.10    }
    9.11    moreover {  
    10.1 --- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Nov 12 17:21:43 2009 +0100
    10.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Nov 12 17:21:48 2009 +0100
    10.3 @@ -269,12 +269,6 @@
    10.4    (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"
    10.5    by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def)
    10.6  
    10.7 -
    10.8 -lemma map_id [rule_format]:
    10.9 -  "(\<forall>n < length xs. f (g (xs!n)) = xs!n) \<longrightarrow> map f (map g xs) = xs"
   10.10 -  by (induct xs, auto)
   10.11 -
   10.12 -
   10.13  lemma is_type_pTs:
   10.14    "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; ((mn,pTs),rT,code) \<in> set mdecls \<rbrakk>
   10.15    \<Longrightarrow> set pTs \<subseteq> types G"
    11.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Nov 12 17:21:43 2009 +0100
    11.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Nov 12 17:21:48 2009 +0100
    11.3 @@ -552,7 +552,7 @@
    11.4  
    11.5  apply (simp only: wf_java_mdecl_def)
    11.6  apply (subgoal_tac "(\<forall>y\<in>set pns. y \<notin> set (map fst lvars))")
    11.7 -apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd)
    11.8 +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)
    11.9  apply (intro strip)
   11.10  apply (simp (no_asm_simp) only: append_Cons [THEN sym])
   11.11  apply (rule progression_lvar_init_aux)
    12.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Thu Nov 12 17:21:43 2009 +0100
    12.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Thu Nov 12 17:21:48 2009 +0100
    12.3 @@ -68,7 +68,7 @@
    12.4  
    12.5      with fst_eq Cons 
    12.6      show "unique (map f (a # list)) = unique (a # list)"
    12.7 -      by (simp add: unique_def fst_set)
    12.8 +      by (simp add: unique_def fst_set image_compose)
    12.9    qed
   12.10  qed
   12.11  
   12.12 @@ -292,7 +292,7 @@
   12.13  apply (simp add: method_def)
   12.14  apply (frule wf_subcls1)
   12.15  apply (simp add: comp_class_rec)
   12.16 -apply (simp add: map_compose [THEN sym] split_iter split_compose del: map_compose)
   12.17 +apply (simp add: split_iter split_compose map_map[symmetric] del: map_map)
   12.18  apply (rule_tac R="%x y. ((x S) = (Option.map (\<lambda>(D, rT, b). 
   12.19    (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))" 
   12.20    in class_rec_relation)
    13.1 --- a/src/HOL/Word/WordShift.thy	Thu Nov 12 17:21:43 2009 +0100
    13.2 +++ b/src/HOL/Word/WordShift.thy	Thu Nov 12 17:21:48 2009 +0100
    13.3 @@ -1113,7 +1113,7 @@
    13.4  
    13.5  lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))"
    13.6    unfolding word_rcat_def to_bl_def' of_bl_def
    13.7 -  by (clarsimp simp add : bin_rcat_bl map_compose)
    13.8 +  by (clarsimp simp add : bin_rcat_bl)
    13.9  
   13.10  lemma size_rcat_lem':
   13.11    "size (concat (map to_bl wl)) = length wl * size (hd wl)"