# HG changeset patch
# User haftmann
# Date 1394868693 -3600
# Node ID f0a927235162c77db3f8634a9d7078434cdcceff
# Parent  2008f1cf3030e67a6fe68c79d828576fc72d2c03
more complete set of lemmas wrt. image and composition

diff -r 2008f1cf3030 -r f0a927235162 NEWS
--- a/NEWS	Sat Mar 15 03:37:22 2014 +0100
+++ b/NEWS	Sat Mar 15 08:31:33 2014 +0100
@@ -98,6 +98,13 @@
 
 *** HOL ***
 
+* Swapped orientation of facts image_comp and vimage_comp:
+  image_compose ~> image_comp [symmetric]
+  image_comp ~> image_comp [symmetric]
+  vimage_compose ~> vimage_comp [symmetric]
+  vimage_comp ~> vimage_comp [symmetric]
+  INCOMPATIBILITY.
+
 * Simplifier: Enhanced solver of preconditions of rewrite rules
   can now deal with conjunctions.
   For help with converting proofs, the old behaviour of the simplifier
diff -r 2008f1cf3030 -r f0a927235162 src/Doc/Tutorial/Sets/Functions.thy
--- a/src/Doc/Tutorial/Sets/Functions.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/Doc/Tutorial/Sets/Functions.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -100,8 +100,8 @@
 *}
 
 text{*
-@{thm[display] image_compose[no_vars]}
-\rulename{image_compose}
+@{thm[display] image_comp[no_vars]}
+\rulename{image_comp}
 
 @{thm[display] image_Int[no_vars]}
 \rulename{image_Int}
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy
--- a/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -480,7 +480,7 @@
 proof-
   {fix tr assume "\<exists> n. tr = deftr n" hence "wf tr"
    apply(induct rule: wf_raw_coind) apply safe
-   unfolding deftr_simps image_compose[symmetric] map_sum.comp id_comp
+   unfolding deftr_simps image_comp map_sum.comp id_comp
    root_o_deftr map_sum.id image_id id_apply apply(rule S_P)
    unfolding inj_on_def by auto
   }
@@ -565,7 +565,7 @@
        show "(root (hsubst tr), prodOf (hsubst tr)) \<in> P"
        unfolding tr1 apply(cases "root tr = root tr0")
        using  wf_P[OF dtr] wf_P[OF tr0]
-       by (auto simp add: image_compose[symmetric] map_sum.comp)
+       by (auto simp add: image_comp map_sum.comp)
        show "inj_on root (Inr -` cont (hsubst tr))"
        apply(cases "root tr = root tr0") using wf_inj_on[OF dtr] wf_inj_on[OF tr0]
        unfolding inj_on_def by (auto, blast)
@@ -959,8 +959,8 @@
 lemma cont_H[simp]:
 "cont (H n) = (id \<oplus> (H o root)) ` cont (pick n)"
 apply(subst id_comp[symmetric, of id]) unfolding map_sum.comp[symmetric]
-unfolding image_compose unfolding H_c_def[symmetric]
-using unfold(2)[of H_c n H_r, OF finite_H_c]
+unfolding image_comp [symmetric] H_c_def [symmetric]
+using unfold(2) [of H_c n H_r, OF finite_H_c]
 unfolding H_def ..
 
 lemma Inl_cont_H[simp]:
@@ -1011,7 +1011,7 @@
 shows "(n, (id \<oplus> root) ` cont (H n)) \<in> P" (is "?L \<in> P")
 proof-
   have "?L = (n, (id \<oplus> root) ` cont (pick n))"
-  unfolding cont_H image_compose[symmetric] map_sum.comp id_comp comp_assoc[symmetric]
+  unfolding cont_H image_comp map_sum.comp id_comp comp_assoc[symmetric]
   unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
   by (rule root_H_root[OF n])
   moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -1863,12 +1863,12 @@
      from simp_num_pair_ci[where bs="x#bs"] have 
     "\<forall>x. (?f o simp_num_pair) x = ?f x" by auto
      hence th: "?f o simp_num_pair = ?f" using ext by blast
-    have "(?f ` set ?Y) = ((?f o simp_num_pair) ` set ?S)" by (simp add: image_compose)
+    have "(?f ` set ?Y) = ((?f o simp_num_pair) ` set ?S)" by (simp add: comp_assoc image_comp)
     also have "\<dots> = (?f ` set ?S)" by (simp add: th)
     also have "\<dots> = ((?f o ?g) ` set ?Up)" 
-      by (simp only: set_map o_def image_compose[symmetric])
+      by (simp only: set_map o_def image_comp)
     also have "\<dots> = (?h ` (set ?U \<times> set ?U))"
-      using uset_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_compose[symmetric]] by blast
+      using uset_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_comp] by blast
     finally show ?thesis .
   qed
   have "\<forall> (t,n) \<in> set ?Y. bound0 (simpfm (usubst ?q (t,n)))"
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -5050,12 +5050,12 @@
      from simp_num_pair_ci[where bs="x#bs"] have 
     "\<forall>x. (?f o simp_num_pair) x = ?f x" by auto
      hence th: "?f o simp_num_pair = ?f" using ext by blast
-    have "(?f ` set ?Y) = ((?f o simp_num_pair) ` set ?S)" by (simp add: image_compose)
+    have "(?f ` set ?Y) = ((?f o simp_num_pair) ` set ?S)" by (simp add: image_comp comp_assoc)
     also have "\<dots> = (?f ` set ?S)" by (simp add: th)
     also have "\<dots> = ((?f o ?g) ` set ?Up)" 
-      by (simp only: set_map o_def image_compose[symmetric])
+      by (simp only: set_map o_def image_comp)
     also have "\<dots> = (?h ` (set ?U \<times> set ?U))"
-      using \<Upsilon>_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_compose[symmetric]] by blast
+      using \<Upsilon>_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_comp] by blast
     finally show ?thesis .
   qed
   have "\<forall> (t,n) \<in> set ?Y. bound0 (\<upsilon> ?q (t,n))"
@@ -5122,10 +5122,10 @@
     by (auto simp add: isint_def)
   from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
   let ?N = "\<lambda> t. Inum (real (i::int)#bs) t"
-  have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by (simp add:image_compose) 
+  have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by (simp add:image_comp) 
   also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="real i #bs"] by auto
   finally have BB': "?N ` set ?B' = ?N ` ?B" .
-  have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by (simp add:image_compose) 
+  have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by (simp add:image_comp) 
   also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="real i #bs"] by auto
   finally have AA': "?N ` set ?A' = ?N ` ?A" .
   from \<beta>_numbound0[OF lq] have B_nb:"\<forall> b\<in> set ?B'. numbound0 b"
@@ -5327,13 +5327,13 @@
   have lq: "iszlfm ?q (real (i::int)#bs)" . 
   from \<delta>[OF lq] have dp:"?d >0" by blast
   let ?N = "\<lambda> (t,c). (Inum (real (i::int)#bs) t,c)"
-  have "?N ` set ?B' = ((?N o ?f) ` ?B)" by (simp add: split_def image_compose)
+  have "?N ` set ?B' = ((?N o ?f) ` ?B)" by (simp add: split_def image_comp)
   also have "\<dots> = ?N ` ?B"
-    by(simp add: split_def image_compose simpnum_ci[where bs="real i #bs"] image_def)
+    by(simp add: split_def image_comp simpnum_ci[where bs="real i #bs"] image_def)
   finally have BB': "?N ` set ?B' = ?N ` ?B" .
-  have "?N ` set ?A' = ((?N o ?f) ` ?A)" by (simp add: split_def image_compose) 
+  have "?N ` set ?A' = ((?N o ?f) ` ?A)" by (simp add: split_def image_comp) 
   also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="real i #bs"]
-    by(simp add: split_def image_compose simpnum_ci[where bs="real i #bs"] image_def) 
+    by(simp add: split_def image_comp simpnum_ci[where bs="real i #bs"] image_def) 
   finally have AA': "?N ` set ?A' = ?N ` ?A" .
   from \<rho>_l[OF lq] have B_nb:"\<forall> (e,c)\<in> set ?B'. numbound0 e \<and> c > 0"
     by (simp add: split_def)
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -395,7 +395,7 @@
     by (auto simp add: finite_conv_nat_seg_image)
   then have "fst ` (A \<times> B) = fst ` f ` {i::nat. i < n}" by simp
   with `B \<noteq> {}` have "A = (fst \<circ> f) ` {i::nat. i < n}"
-    by (simp add: image_compose)
+    by (simp add: image_comp)
   then have "\<exists>n f. A = f ` {i::nat. i < n}" by blast
   then show ?thesis
     by (auto simp add: finite_conv_nat_seg_image)
@@ -409,7 +409,7 @@
     by (auto simp add: finite_conv_nat_seg_image)
   then have "snd ` (A \<times> B) = snd ` f ` {i::nat. i < n}" by simp
   with `A \<noteq> {}` have "B = (snd \<circ> f) ` {i::nat. i < n}"
-    by (simp add: image_compose)
+    by (simp add: image_comp)
   then have "\<exists>n f. B = f ` {i::nat. i < n}" by blast
   then show ?thesis
     by (auto simp add: finite_conv_nat_seg_image)
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Fun.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -72,11 +72,11 @@
   by clarsimp
 
 lemma image_comp:
-  "(f o g) ` r = f ` (g ` r)"
+  "f ` (g ` r) = (f o g) ` r"
   by auto
 
 lemma vimage_comp:
-  "(g \<circ> f) -` x = f -` (g -` x)"
+  "f -` (g -` x) = (g \<circ> f) -` x"
   by auto
 
 code_printing
@@ -835,8 +835,6 @@
 lemmas o_eq_elim = comp_eq_elim
 lemmas o_eq_dest_lhs = comp_eq_dest_lhs
 lemmas o_eq_id_dest = comp_eq_id_dest
-lemmas image_compose = image_comp
-lemmas vimage_compose = vimage_comp
 
 end
 
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -250,7 +250,7 @@
   proof -
     have "\<exists>sup. is_Sup (undual ` A') sup" by (rule ex_Sup)
     then have "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
-    then show ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
+    then show ?thesis by (simp add: dual_ex [symmetric] image_comp)
   qed
 qed
 
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Lattice/Orders.thy
--- a/src/HOL/Lattice/Orders.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Lattice/Orders.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -102,7 +102,7 @@
     have "undual x' \<in> A"
     proof -
       from x' have "undual x' \<in> undual ` dual ` A" by simp
-      thus "undual x' \<in> A" by (simp add: image_compose [symmetric])
+      thus "undual x' \<in> A" by (simp add: image_comp)
     qed
     with a have "P (dual (undual x'))" ..
     also have "\<dots> = x'" by simp
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -418,7 +418,7 @@
 
   show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
     unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]
-    by(simp add: image_comp inj_on_Abs_bit0 card_image image_int_atLeastLessThan)
+    by(simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeastLessThan)
       (auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def mod_pos_pos_trivial)
 
   fix P :: "'a bit0 \<Rightarrow> bool"
@@ -442,7 +442,7 @@
 
   show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum"
     unfolding enum_bit1_def type_definition.Abs_image[OF type_definition_bit1, symmetric]
-    by(simp add: image_comp inj_on_Abs_bit1 card_image image_int_atLeastLessThan)
+    by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeastLessThan)
       (auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def mod_pos_pos_trivial)
 
   fix P :: "'a bit1 \<Rightarrow> bool"
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Library/Permutation.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -211,7 +211,7 @@
     proof (rule bij_betw_combine)
       show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
         using bij unfolding bij_betw_def
-        by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def)
+        by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def)
     qed (auto simp: bij_betw_def)
     fix i
     assume "i < length (z#xs)"
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Library/Product_Order.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -225,10 +225,10 @@
 by (auto simp: Sup_prod_def SUP_def)
 
 lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
-by (auto simp: INF_def Inf_prod_def image_compose)
+by (auto simp: INF_def Inf_prod_def image_comp)
 
 lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
-by (auto simp: SUP_def Sup_prod_def image_compose)
+by (auto simp: SUP_def Sup_prod_def image_comp)
 
 lemma INF_prod_alt_def:
   "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -644,8 +644,7 @@
 apply (simp add: eff_def nth_append norm_eff_def)
 apply (frule_tac x="(pc', None)" and  f=fst and b=pc' in rev_image_eqI) 
   apply (simp (no_asm_simp))
-  apply (simp only: fst_conv image_compose [THEN sym] Fun.comp_def)
-  apply simp
+  apply (simp add: image_comp Fun.comp_def)
   apply (frule pc_succs_shift)
 apply (drule bspec, assumption)
 apply arith
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Sat Mar 15 08:31:33 2014 +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 image_compose)
+      by (simp add: unique_def fst_set image_comp)
   qed
 qed
 
@@ -95,7 +95,7 @@
 "(class G C = None) = (class (comp G) C = None)"
 apply (simp add: class_def comp_def compClass_def)
 apply (simp add: map_of_in_set)
-apply (simp add: image_compose [THEN sym] o_def split_beta)
+apply (simp add: image_comp [THEN sym] o_def split_beta)
 done
 
 lemma comp_is_class: "is_class (comp G) C = is_class G C"
@@ -174,7 +174,7 @@
 
 lemma comp_wf_syscls: "wf_syscls (comp G) = wf_syscls G"
 apply (simp add: wf_syscls_def comp_def compClass_def split_beta)
-apply (simp only: image_compose [THEN sym])
+apply (simp add: image_comp)
 apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
   (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
 apply simp
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -4182,7 +4182,6 @@
     apply (rule continuous_on_compose assms)+
     apply ((rule continuous_on_subset)?, rule assms)+
     using assms(2,4,8)
-    unfolding image_compose
     apply auto
     apply blast
     done
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -280,10 +280,10 @@
   obtain f' where f': "linear f' \<and> f \<circ> f' = id \<and> f' \<circ> f = id"
     using assms linear_injective_isomorphism[of f] isomorphism_expand by auto
   then have "f' ` closure (f ` S) \<le> closure (S)"
-    using closure_linear_image[of f' "f ` S"] image_compose[of f' f] by auto
+    using closure_linear_image[of f' "f ` S"] image_comp[of f' f] by auto
   then have "f ` f' ` closure (f ` S) \<le> f ` closure S" by auto
   then have "closure (f ` S) \<le> f ` closure S"
-    using image_compose[of f f' "closure (f ` S)"] f' by auto
+    using image_comp[of f f' "closure (f ` S)"] f' by auto
   then show ?thesis using closure_linear_image[of f S] assms by auto
 qed
 
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -302,7 +302,7 @@
   have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
   proof (rule fashoda_unit)
     show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}"
-      using isc and assms(3-4) unfolding image_compose by auto
+      using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
     have *: "continuous_on {- 1..1} iscale"
       unfolding iscale_def by (rule continuous_on_intros)+
     show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -3798,8 +3798,10 @@
 proof
   fix f :: "nat \<Rightarrow> 'a \<times> 'b"
   assume f: "bounded (range f)"
-  from f have s1: "bounded (range (fst \<circ> f))"
-    unfolding image_comp by (rule bounded_fst)
+  then have "bounded (fst ` range f)"
+    by (rule bounded_fst)
+  then have s1: "bounded (range (fst \<circ> f))"
+    by (simp add: image_comp)
   obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) ----> l1"
     using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
   from f have s2: "bounded (range (snd \<circ> f \<circ> r1))"
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Predicate.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -85,11 +85,11 @@
 
 lemma eval_INFI [simp]:
   "eval (INFI A f) = INFI A (eval \<circ> f)"
-  by (simp only: INF_def eval_Inf image_compose)
+  by (simp only: INF_def eval_Inf image_comp)
 
 lemma eval_SUPR [simp]:
   "eval (SUPR A f) = SUPR A (eval \<circ> f)"
-  by (simp only: SUP_def eval_Sup image_compose)
+  by (simp only: SUP_def eval_Sup image_comp)
 
 instantiation pred :: (type) complete_boolean_algebra
 begin
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -936,7 +936,7 @@
 
   show ?B
     using IJ.measurable_emeasure_Pair1[OF merge]
-    by (simp add: vimage_compose[symmetric] comp_def space_pair_measure cong: measurable_cong)
+    by (simp add: vimage_comp comp_def space_pair_measure cong: measurable_cong)
 qed
 
 lemma (in product_sigma_finite) product_integral_insert:
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -794,10 +794,10 @@
     { fix A assume "A \<in> sets (N i)"
       then have "\<exists>B. (Y i \<circ> X i) -` A \<inter> space M = X i -` B \<inter> space M \<and> B \<in> sets (M' i)"
         by (intro exI[of _ "Y i -` A \<inter> space (M' i)"])
-           (auto simp: vimage_compose intro!: measurable_sets rv `i \<in> I` funcset_mem[OF X]) }
+           (auto simp: vimage_comp intro!: measurable_sets rv `i \<in> I` funcset_mem[OF X]) }
     then show "sigma_sets (space M) {(Y i \<circ> X i) -` A \<inter> space M |A. A \<in> sets (N i)} \<subseteq>
       sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
-      by (intro sigma_sets_subseteq) (auto simp: vimage_compose)
+      by (intro sigma_sets_subseteq) (auto simp: vimage_comp)
   qed
 qed
 
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Probability/Information.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -1640,7 +1640,7 @@
     using XY unfolding simple_distributed_def by auto
   from finite_imageI[OF this, of fst]
   have [simp]: "finite (X`space M)"
-    by (simp add: image_compose[symmetric] comp_def)
+    by (simp add: image_comp comp_def)
   note Y[THEN simple_distributed_finite, simp]
   show "sigma_finite_measure (count_space (X ` space M))"
     by (simp add: sigma_finite_measure_count_space_finite)
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -144,7 +144,7 @@
   unfolding simple_function_def
 proof safe
   show "finite ((g \<circ> f) ` space M)"
-    using assms unfolding simple_function_def by (auto simp: image_compose)
+    using assms unfolding simple_function_def by (auto simp: image_comp [symmetric])
 next
   fix x assume "x \<in> space M"
   let ?G = "g -` {g (f x)} \<inter> (f`space M)"
@@ -2542,7 +2542,7 @@
   from f have "bij_betw (from_nat_into I) UNIV I"
     using bij_betw_from_nat_into[OF I] by simp
   then have "(\<Union>i\<in>I. X i) = (\<Union>i. (X \<circ> from_nat_into I) i)"
-    unfolding SUP_def image_compose by (simp add: bij_betw_def)
+    unfolding SUP_def image_comp [symmetric] by (simp add: bij_betw_def)
   then have "emeasure M (UNION I X) = emeasure M (\<Union>i. X (from_nat_into I i))"
     by simp
   also have "\<dots> = (\<Sum>i. emeasure M (X (from_nat_into I i)))"
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -795,9 +795,9 @@
 
 lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))"
 proof -
-  have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
-    unfolding SUP_def image_compose
-    unfolding surj_from_nat ..
+  have "\<Union>range N = \<Union>(N ` range from_nat)" by simp
+  then have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
+    by (simp only: SUP_def image_comp)
   then show ?thesis by simp
 qed
 
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -297,7 +297,7 @@
   qed
   have **: "range ?A' = range A"
     using surj_from_nat
-    by (auto simp: image_compose intro!: imageI)
+    by (auto simp: image_comp [symmetric] intro!: imageI)
   show ?thesis unfolding * ** ..
 qed
 
@@ -1493,12 +1493,13 @@
   have fab: "f \<in> (space a -> space b)"
    and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
      by (auto simp add: measurable_def)
-  have eq: "\<And>y. f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
+  have eq: "\<And>y. (g \<circ> f) -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
     by force
   show ?thesis
-    apply (auto simp add: measurable_def vimage_compose)
+    apply (auto simp add: measurable_def vimage_comp)
     apply (metis funcset_mem fab g)
-    apply (subst eq, metis ba cb)
+    apply (subst eq)
+    apply (metis ba cb)
     done
 qed
 
diff -r 2008f1cf3030 -r f0a927235162 src/HOL/ZF/Zet.thy
--- a/src/HOL/ZF/Zet.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/ZF/Zet.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -37,7 +37,7 @@
   apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
   apply (simp add: explode_Repl_eq)
   apply (subgoal_tac "explode z = f ` A")
-  apply (simp_all add: image_compose)
+  apply (simp_all add: image_comp [symmetric])
   done
 
 lemma zet_image_mem:
@@ -58,7 +58,7 @@
     apply (auto simp add: subset injf)
     done
   show ?thesis
-    apply (simp add: zet_def' image_compose[symmetric])
+    apply (simp add: zet_def' image_comp)
     apply (rule exI[where x="?w"])
     apply (simp add: injw image_zet_rep Azet)
     done
@@ -110,7 +110,7 @@
 lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A"
   apply (simp add: zimage_def)
   apply (subst Abs_zet_inverse)
-  apply (simp_all add: image_compose zet_image_mem Rep_zet)
+  apply (simp_all add: image_comp zet_image_mem Rep_zet)
   done
     
 definition zunion :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> 'a zet" where