1.1 --- a/src/HOL/Import/HOL/rich_list.imp Thu Nov 12 17:21:48 2009 +0100
1.2 +++ b/src/HOL/Import/HOL/rich_list.imp Thu Nov 12 17:21:51 2009 +0100
1.3 @@ -130,7 +130,7 @@
1.4 "MAP_o" > "HOL4Base.rich_list.MAP_o"
1.5 "MAP_SNOC" > "HOL4Base.rich_list.MAP_SNOC"
1.6 "MAP_REVERSE" > "List.rev_map"
1.7 - "MAP_MAP_o" > "List.map_compose"
1.8 + "MAP_MAP_o" > "List.map_map"
1.9 "MAP_FOLDR" > "HOL4Base.rich_list.MAP_FOLDR"
1.10 "MAP_FOLDL" > "HOL4Base.rich_list.MAP_FOLDL"
1.11 "MAP_FLAT" > "List.map_concat"
2.1 --- a/src/HOL/Integration.thy Thu Nov 12 17:21:48 2009 +0100
2.2 +++ b/src/HOL/Integration.thy Thu Nov 12 17:21:51 2009 +0100
2.3 @@ -542,7 +542,7 @@
2.4 apply (erule subst)
2.5 apply (subst listsum_subtractf [symmetric])
2.6 apply (rule listsum_abs [THEN order_trans])
2.7 - apply (subst map_compose [symmetric, unfolded o_def])
2.8 + apply (subst map_map [unfolded o_def])
2.9 apply (subgoal_tac "e = (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))")
2.10 apply (erule ssubst)
2.11 apply (simp add: abs_minus_commute)
3.1 --- a/src/HOL/Lambda/StrongNorm.thy Thu Nov 12 17:21:48 2009 +0100
3.2 +++ b/src/HOL/Lambda/StrongNorm.thy Thu Nov 12 17:21:51 2009 +0100
3.3 @@ -186,7 +186,7 @@
3.4 by (rule typing.App)
3.5 qed
3.6 with Cons True show ?thesis
3.7 - by (simp add: map_compose [symmetric] comp_def)
3.8 + by (simp add: comp_def)
3.9 qed
3.10 next
3.11 case False
4.1 --- a/src/HOL/Lambda/WeakNorm.thy Thu Nov 12 17:21:48 2009 +0100
4.2 +++ b/src/HOL/Lambda/WeakNorm.thy Thu Nov 12 17:21:51 2009 +0100
4.3 @@ -148,7 +148,7 @@
4.4 hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) : Ts"
4.5 by (rule lift_types)
4.6 thus "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift (t[u/i]) 0) as : Ts"
4.7 - by (simp_all add: map_compose [symmetric] o_def)
4.8 + by (simp_all add: o_def)
4.9 qed
4.10 with asred show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' : T'"
4.11 by (rule subject_reduction')
4.12 @@ -167,7 +167,7 @@
4.13 also note rred
4.14 finally have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" .
4.15 with rnf Cons eq show ?thesis
4.16 - by (simp add: map_compose [symmetric] o_def) iprover
4.17 + by (simp add: o_def) iprover
4.18 qed
4.19 next
4.20 assume neq: "x \<noteq> i"
5.1 --- a/src/HOL/Library/Countable.thy Thu Nov 12 17:21:48 2009 +0100
5.2 +++ b/src/HOL/Library/Countable.thy Thu Nov 12 17:21:51 2009 +0100
5.3 @@ -165,7 +165,7 @@
5.4 text {* Lists *}
5.5
5.6 lemma from_nat_to_nat_map [simp]: "map from_nat (map to_nat xs) = xs"
5.7 - by (simp add: comp_def map_compose [symmetric])
5.8 + by (simp add: comp_def)
5.9
5.10 primrec
5.11 list_encode :: "'a\<Colon>countable list \<Rightarrow> nat"
6.1 --- a/src/HOL/Library/Mapping.thy Thu Nov 12 17:21:48 2009 +0100
6.2 +++ b/src/HOL/Library/Mapping.thy Thu Nov 12 17:21:51 2009 +0100
6.3 @@ -128,7 +128,7 @@
6.4 lemma bulkload_tabulate:
6.5 "bulkload xs = tabulate [0..<length xs] (nth xs)"
6.6 by (rule sym)
6.7 - (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def)
6.8 + (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff comp_def)
6.9
6.10
6.11 subsection {* Some technical code lemmas *}
7.1 --- a/src/HOL/List.thy Thu Nov 12 17:21:48 2009 +0100
7.2 +++ b/src/HOL/List.thy Thu Nov 12 17:21:51 2009 +0100
7.3 @@ -704,9 +704,6 @@
7.4 lemma map_map [simp]: "map f (map g xs) = map (f \<circ> g) xs"
7.5 by (induct xs) auto
7.6
7.7 -lemma map_compose: "map (f \<circ> g) xs = map f (map g xs)"
7.8 -by simp
7.9 -
7.10 lemma rev_map: "rev (map f xs) = map f (rev xs)"
7.11 by (induct xs) auto
7.12
8.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Nov 12 17:21:48 2009 +0100
8.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Nov 12 17:21:51 2009 +0100
8.3 @@ -132,7 +132,7 @@
8.4 apply (case_tac "vname = This")
8.5 apply (simp add: inited_LT_def)
8.6 apply (simp add: inited_LT_def)
8.7 -apply (simp (no_asm_simp) only: map_compose map_append [THEN sym] map.simps [THEN sym])
8.8 +apply (simp (no_asm_simp) only: map_map [symmetric] map_append [symmetric] map.simps [symmetric])
8.9 apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars)")
8.10 apply (simp (no_asm_simp) only: List.nth_map ok_val.simps)
8.11 apply (subgoal_tac "map_of lvars = map_of (map (\<lambda> p. (fst p, snd p)) lvars)")
8.12 @@ -166,7 +166,7 @@
8.13 lemma inited_LT_at_index_no_err: " i < length (inited_LT C pTs lvars)
8.14 \<Longrightarrow> inited_LT C pTs lvars ! i \<noteq> Err"
8.15 apply (simp only: inited_LT_def)
8.16 -apply (simp only: map_compose map_append [THEN sym] map.simps [THEN sym] length_map)
8.17 +apply (simp only: map_map [symmetric] map_append [symmetric] map.simps [symmetric] length_map)
8.18 apply (simp only: nth_map)
8.19 apply simp
8.20 done
9.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Nov 12 17:21:48 2009 +0100
9.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Nov 12 17:21:51 2009 +0100
9.3 @@ -311,7 +311,7 @@
9.4 apply (simp add: split_beta compMethod_def)
9.5 apply (simp add: map_of_map [THEN sym])
9.6 apply (simp add: split_beta)
9.7 -apply (simp add: map_compose [THEN sym] Fun.comp_def split_beta)
9.8 +apply (simp add: Fun.comp_def split_beta)
9.9 apply (subgoal_tac "(\<lambda>x\<Colon>(vname list \<times> fdecl list \<times> stmt \<times> expr) mdecl.
9.10 (fst x, Object,
9.11 snd (compMethod G Object
10.1 --- a/src/HOL/MicroJava/J/WellForm.thy Thu Nov 12 17:21:48 2009 +0100
10.2 +++ b/src/HOL/MicroJava/J/WellForm.thy Thu Nov 12 17:21:51 2009 +0100
10.3 @@ -284,8 +284,7 @@
10.4 apply (frule fields_rec, assumption)
10.5 apply (rule HOL.trans)
10.6 apply (simp add: o_def)
10.7 -apply (simp (no_asm_use)
10.8 - add: split_beta split_def o_def map_compose [THEN sym] del: map_compose)
10.9 +apply (simp (no_asm_use) add: split_beta split_def o_def)
10.10 done
10.11
10.12 lemma method_Object [simp]:
11.1 --- a/src/HOL/Word/WordShift.thy Thu Nov 12 17:21:48 2009 +0100
11.2 +++ b/src/HOL/Word/WordShift.thy Thu Nov 12 17:21:51 2009 +0100
11.3 @@ -1102,7 +1102,7 @@
11.4 apply simp
11.5 apply (rule bin_nth_rsplit)
11.6 apply simp_all
11.7 - apply (simp add : word_size rev_map map_compose [symmetric])
11.8 + apply (simp add : word_size rev_map)
11.9 apply (rule trans)
11.10 defer
11.11 apply (rule map_ident [THEN fun_cong])