summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Thu, 12 Nov 2009 17:21:48 +0100 | |

changeset 33639 | 603320b93668 |

parent 33638 | 548a34929e98 |

child 33640 | 0d82107dc07a |

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)"