--- a/src/HOL/Import/HOL/rich_list.imp Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/Import/HOL/rich_list.imp Thu Nov 12 17:21:51 2009 +0100
@@ -130,7 +130,7 @@
"MAP_o" > "HOL4Base.rich_list.MAP_o"
"MAP_SNOC" > "HOL4Base.rich_list.MAP_SNOC"
"MAP_REVERSE" > "List.rev_map"
- "MAP_MAP_o" > "List.map_compose"
+ "MAP_MAP_o" > "List.map_map"
"MAP_FOLDR" > "HOL4Base.rich_list.MAP_FOLDR"
"MAP_FOLDL" > "HOL4Base.rich_list.MAP_FOLDL"
"MAP_FLAT" > "List.map_concat"
--- a/src/HOL/Integration.thy Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/Integration.thy Thu Nov 12 17:21:51 2009 +0100
@@ -542,7 +542,7 @@
apply (erule subst)
apply (subst listsum_subtractf [symmetric])
apply (rule listsum_abs [THEN order_trans])
- apply (subst map_compose [symmetric, unfolded o_def])
+ apply (subst map_map [unfolded o_def])
apply (subgoal_tac "e = (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))")
apply (erule ssubst)
apply (simp add: abs_minus_commute)
--- a/src/HOL/Lambda/StrongNorm.thy Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/Lambda/StrongNorm.thy Thu Nov 12 17:21:51 2009 +0100
@@ -186,7 +186,7 @@
by (rule typing.App)
qed
with Cons True show ?thesis
- by (simp add: map_compose [symmetric] comp_def)
+ by (simp add: comp_def)
qed
next
case False
--- a/src/HOL/Lambda/WeakNorm.thy Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy Thu Nov 12 17:21:51 2009 +0100
@@ -148,7 +148,7 @@
hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) : Ts"
by (rule lift_types)
thus "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift (t[u/i]) 0) as : Ts"
- by (simp_all add: map_compose [symmetric] o_def)
+ by (simp_all add: o_def)
qed
with asred show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' : T'"
by (rule subject_reduction')
@@ -167,7 +167,7 @@
also note rred
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" .
with rnf Cons eq show ?thesis
- by (simp add: map_compose [symmetric] o_def) iprover
+ by (simp add: o_def) iprover
qed
next
assume neq: "x \<noteq> i"
--- a/src/HOL/Library/Countable.thy Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/Library/Countable.thy Thu Nov 12 17:21:51 2009 +0100
@@ -165,7 +165,7 @@
text {* Lists *}
lemma from_nat_to_nat_map [simp]: "map from_nat (map to_nat xs) = xs"
- by (simp add: comp_def map_compose [symmetric])
+ by (simp add: comp_def)
primrec
list_encode :: "'a\<Colon>countable list \<Rightarrow> nat"
--- a/src/HOL/Library/Mapping.thy Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/Library/Mapping.thy Thu Nov 12 17:21:51 2009 +0100
@@ -128,7 +128,7 @@
lemma bulkload_tabulate:
"bulkload xs = tabulate [0..<length xs] (nth xs)"
by (rule sym)
- (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def)
+ (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff comp_def)
subsection {* Some technical code lemmas *}
--- a/src/HOL/List.thy Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/List.thy Thu Nov 12 17:21:51 2009 +0100
@@ -704,9 +704,6 @@
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
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Nov 12 17:21:51 2009 +0100
@@ -132,7 +132,7 @@
apply (case_tac "vname = This")
apply (simp add: inited_LT_def)
apply (simp add: inited_LT_def)
-apply (simp (no_asm_simp) only: map_compose map_append [THEN sym] map.simps [THEN sym])
+apply (simp (no_asm_simp) only: map_map [symmetric] map_append [symmetric] map.simps [symmetric])
apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars)")
apply (simp (no_asm_simp) only: List.nth_map ok_val.simps)
apply (subgoal_tac "map_of lvars = map_of (map (\<lambda> p. (fst p, snd p)) lvars)")
@@ -166,7 +166,7 @@
lemma inited_LT_at_index_no_err: " i < length (inited_LT C pTs lvars)
\<Longrightarrow> inited_LT C pTs lvars ! i \<noteq> Err"
apply (simp only: inited_LT_def)
-apply (simp only: map_compose map_append [THEN sym] map.simps [THEN sym] length_map)
+apply (simp only: map_map [symmetric] map_append [symmetric] map.simps [symmetric] length_map)
apply (simp only: nth_map)
apply simp
done
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Nov 12 17:21:51 2009 +0100
@@ -311,7 +311,7 @@
apply (simp add: split_beta compMethod_def)
apply (simp add: map_of_map [THEN sym])
apply (simp add: split_beta)
-apply (simp add: map_compose [THEN sym] Fun.comp_def split_beta)
+apply (simp add: Fun.comp_def split_beta)
apply (subgoal_tac "(\<lambda>x\<Colon>(vname list \<times> fdecl list \<times> stmt \<times> expr) mdecl.
(fst x, Object,
snd (compMethod G Object
--- a/src/HOL/MicroJava/J/WellForm.thy Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Thu Nov 12 17:21:51 2009 +0100
@@ -284,8 +284,7 @@
apply (frule fields_rec, assumption)
apply (rule HOL.trans)
apply (simp add: o_def)
-apply (simp (no_asm_use)
- add: split_beta split_def o_def map_compose [THEN sym] del: map_compose)
+apply (simp (no_asm_use) add: split_beta split_def o_def)
done
lemma method_Object [simp]:
--- a/src/HOL/Word/WordShift.thy Thu Nov 12 17:21:48 2009 +0100
+++ b/src/HOL/Word/WordShift.thy Thu Nov 12 17:21:51 2009 +0100
@@ -1102,7 +1102,7 @@
apply simp
apply (rule bin_nth_rsplit)
apply simp_all
- apply (simp add : word_size rev_map map_compose [symmetric])
+ apply (simp add : word_size rev_map)
apply (rule trans)
defer
apply (rule map_ident [THEN fun_cong])