# HG changeset patch
# User hoelzl
# Date 1258042911 -3600
# Node ID 0d82107dc07a939ebd972665cf3fcb34b6ff1d93
# Parent  603320b936689bafb1d85a337daab8de4005772e
Remove map_compose, replaced by map_map

diff -r 603320b93668 -r 0d82107dc07a src/HOL/Import/HOL/rich_list.imp
--- 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"
diff -r 603320b93668 -r 0d82107dc07a src/HOL/Integration.thy
--- 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)
diff -r 603320b93668 -r 0d82107dc07a src/HOL/Lambda/StrongNorm.thy
--- 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
diff -r 603320b93668 -r 0d82107dc07a src/HOL/Lambda/WeakNorm.thy
--- 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"
diff -r 603320b93668 -r 0d82107dc07a src/HOL/Library/Countable.thy
--- 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"
diff -r 603320b93668 -r 0d82107dc07a src/HOL/Library/Mapping.thy
--- 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 *}
diff -r 603320b93668 -r 0d82107dc07a src/HOL/List.thy
--- 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
 
diff -r 603320b93668 -r 0d82107dc07a src/HOL/MicroJava/Comp/CorrCompTp.thy
--- 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
diff -r 603320b93668 -r 0d82107dc07a src/HOL/MicroJava/Comp/LemmasComp.thy
--- 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
diff -r 603320b93668 -r 0d82107dc07a src/HOL/MicroJava/J/WellForm.thy
--- 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]:
diff -r 603320b93668 -r 0d82107dc07a src/HOL/Word/WordShift.thy
--- 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])