more complete set of lemmas wrt. image and composition
authorhaftmann
Sat Mar 15 08:31:33 2014 +0100 (2014-03-15)
changeset 56154f0a927235162
parent 56153 2008f1cf3030
child 56155 1b9c089ed12d
more complete set of lemmas wrt. image and composition
NEWS
src/Doc/Tutorial/Sets/Functions.thy
src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Lattice/CompleteLattice.thy
src/HOL/Lattice/Orders.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Product_Order.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/MicroJava/Comp/LemmasComp.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Fashoda.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Predicate.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/ZF/Zet.thy
     1.1 --- a/NEWS	Sat Mar 15 03:37:22 2014 +0100
     1.2 +++ b/NEWS	Sat Mar 15 08:31:33 2014 +0100
     1.3 @@ -98,6 +98,13 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Swapped orientation of facts image_comp and vimage_comp:
     1.8 +  image_compose ~> image_comp [symmetric]
     1.9 +  image_comp ~> image_comp [symmetric]
    1.10 +  vimage_compose ~> vimage_comp [symmetric]
    1.11 +  vimage_comp ~> vimage_comp [symmetric]
    1.12 +  INCOMPATIBILITY.
    1.13 +
    1.14  * Simplifier: Enhanced solver of preconditions of rewrite rules
    1.15    can now deal with conjunctions.
    1.16    For help with converting proofs, the old behaviour of the simplifier
     2.1 --- a/src/Doc/Tutorial/Sets/Functions.thy	Sat Mar 15 03:37:22 2014 +0100
     2.2 +++ b/src/Doc/Tutorial/Sets/Functions.thy	Sat Mar 15 08:31:33 2014 +0100
     2.3 @@ -100,8 +100,8 @@
     2.4  *}
     2.5  
     2.6  text{*
     2.7 -@{thm[display] image_compose[no_vars]}
     2.8 -\rulename{image_compose}
     2.9 +@{thm[display] image_comp[no_vars]}
    2.10 +\rulename{image_comp}
    2.11  
    2.12  @{thm[display] image_Int[no_vars]}
    2.13  \rulename{image_Int}
     3.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Sat Mar 15 03:37:22 2014 +0100
     3.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Sat Mar 15 08:31:33 2014 +0100
     3.3 @@ -480,7 +480,7 @@
     3.4  proof-
     3.5    {fix tr assume "\<exists> n. tr = deftr n" hence "wf tr"
     3.6     apply(induct rule: wf_raw_coind) apply safe
     3.7 -   unfolding deftr_simps image_compose[symmetric] map_sum.comp id_comp
     3.8 +   unfolding deftr_simps image_comp map_sum.comp id_comp
     3.9     root_o_deftr map_sum.id image_id id_apply apply(rule S_P)
    3.10     unfolding inj_on_def by auto
    3.11    }
    3.12 @@ -565,7 +565,7 @@
    3.13         show "(root (hsubst tr), prodOf (hsubst tr)) \<in> P"
    3.14         unfolding tr1 apply(cases "root tr = root tr0")
    3.15         using  wf_P[OF dtr] wf_P[OF tr0]
    3.16 -       by (auto simp add: image_compose[symmetric] map_sum.comp)
    3.17 +       by (auto simp add: image_comp map_sum.comp)
    3.18         show "inj_on root (Inr -` cont (hsubst tr))"
    3.19         apply(cases "root tr = root tr0") using wf_inj_on[OF dtr] wf_inj_on[OF tr0]
    3.20         unfolding inj_on_def by (auto, blast)
    3.21 @@ -959,8 +959,8 @@
    3.22  lemma cont_H[simp]:
    3.23  "cont (H n) = (id \<oplus> (H o root)) ` cont (pick n)"
    3.24  apply(subst id_comp[symmetric, of id]) unfolding map_sum.comp[symmetric]
    3.25 -unfolding image_compose unfolding H_c_def[symmetric]
    3.26 -using unfold(2)[of H_c n H_r, OF finite_H_c]
    3.27 +unfolding image_comp [symmetric] H_c_def [symmetric]
    3.28 +using unfold(2) [of H_c n H_r, OF finite_H_c]
    3.29  unfolding H_def ..
    3.30  
    3.31  lemma Inl_cont_H[simp]:
    3.32 @@ -1011,7 +1011,7 @@
    3.33  shows "(n, (id \<oplus> root) ` cont (H n)) \<in> P" (is "?L \<in> P")
    3.34  proof-
    3.35    have "?L = (n, (id \<oplus> root) ` cont (pick n))"
    3.36 -  unfolding cont_H image_compose[symmetric] map_sum.comp id_comp comp_assoc[symmetric]
    3.37 +  unfolding cont_H image_comp map_sum.comp id_comp comp_assoc[symmetric]
    3.38    unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
    3.39    by (rule root_H_root[OF n])
    3.40    moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
     4.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Sat Mar 15 03:37:22 2014 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Sat Mar 15 08:31:33 2014 +0100
     4.3 @@ -1863,12 +1863,12 @@
     4.4       from simp_num_pair_ci[where bs="x#bs"] have 
     4.5      "\<forall>x. (?f o simp_num_pair) x = ?f x" by auto
     4.6       hence th: "?f o simp_num_pair = ?f" using ext by blast
     4.7 -    have "(?f ` set ?Y) = ((?f o simp_num_pair) ` set ?S)" by (simp add: image_compose)
     4.8 +    have "(?f ` set ?Y) = ((?f o simp_num_pair) ` set ?S)" by (simp add: comp_assoc image_comp)
     4.9      also have "\<dots> = (?f ` set ?S)" by (simp add: th)
    4.10      also have "\<dots> = ((?f o ?g) ` set ?Up)" 
    4.11 -      by (simp only: set_map o_def image_compose[symmetric])
    4.12 +      by (simp only: set_map o_def image_comp)
    4.13      also have "\<dots> = (?h ` (set ?U \<times> set ?U))"
    4.14 -      using uset_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_compose[symmetric]] by blast
    4.15 +      using uset_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_comp] by blast
    4.16      finally show ?thesis .
    4.17    qed
    4.18    have "\<forall> (t,n) \<in> set ?Y. bound0 (simpfm (usubst ?q (t,n)))"
     5.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sat Mar 15 03:37:22 2014 +0100
     5.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sat Mar 15 08:31:33 2014 +0100
     5.3 @@ -5050,12 +5050,12 @@
     5.4       from simp_num_pair_ci[where bs="x#bs"] have 
     5.5      "\<forall>x. (?f o simp_num_pair) x = ?f x" by auto
     5.6       hence th: "?f o simp_num_pair = ?f" using ext by blast
     5.7 -    have "(?f ` set ?Y) = ((?f o simp_num_pair) ` set ?S)" by (simp add: image_compose)
     5.8 +    have "(?f ` set ?Y) = ((?f o simp_num_pair) ` set ?S)" by (simp add: image_comp comp_assoc)
     5.9      also have "\<dots> = (?f ` set ?S)" by (simp add: th)
    5.10      also have "\<dots> = ((?f o ?g) ` set ?Up)" 
    5.11 -      by (simp only: set_map o_def image_compose[symmetric])
    5.12 +      by (simp only: set_map o_def image_comp)
    5.13      also have "\<dots> = (?h ` (set ?U \<times> set ?U))"
    5.14 -      using \<Upsilon>_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_compose[symmetric]] by blast
    5.15 +      using \<Upsilon>_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_comp] by blast
    5.16      finally show ?thesis .
    5.17    qed
    5.18    have "\<forall> (t,n) \<in> set ?Y. bound0 (\<upsilon> ?q (t,n))"
    5.19 @@ -5122,10 +5122,10 @@
    5.20      by (auto simp add: isint_def)
    5.21    from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
    5.22    let ?N = "\<lambda> t. Inum (real (i::int)#bs) t"
    5.23 -  have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by (simp add:image_compose) 
    5.24 +  have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by (simp add:image_comp) 
    5.25    also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="real i #bs"] by auto
    5.26    finally have BB': "?N ` set ?B' = ?N ` ?B" .
    5.27 -  have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by (simp add:image_compose) 
    5.28 +  have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by (simp add:image_comp) 
    5.29    also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="real i #bs"] by auto
    5.30    finally have AA': "?N ` set ?A' = ?N ` ?A" .
    5.31    from \<beta>_numbound0[OF lq] have B_nb:"\<forall> b\<in> set ?B'. numbound0 b"
    5.32 @@ -5327,13 +5327,13 @@
    5.33    have lq: "iszlfm ?q (real (i::int)#bs)" . 
    5.34    from \<delta>[OF lq] have dp:"?d >0" by blast
    5.35    let ?N = "\<lambda> (t,c). (Inum (real (i::int)#bs) t,c)"
    5.36 -  have "?N ` set ?B' = ((?N o ?f) ` ?B)" by (simp add: split_def image_compose)
    5.37 +  have "?N ` set ?B' = ((?N o ?f) ` ?B)" by (simp add: split_def image_comp)
    5.38    also have "\<dots> = ?N ` ?B"
    5.39 -    by(simp add: split_def image_compose simpnum_ci[where bs="real i #bs"] image_def)
    5.40 +    by(simp add: split_def image_comp simpnum_ci[where bs="real i #bs"] image_def)
    5.41    finally have BB': "?N ` set ?B' = ?N ` ?B" .
    5.42 -  have "?N ` set ?A' = ((?N o ?f) ` ?A)" by (simp add: split_def image_compose) 
    5.43 +  have "?N ` set ?A' = ((?N o ?f) ` ?A)" by (simp add: split_def image_comp) 
    5.44    also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="real i #bs"]
    5.45 -    by(simp add: split_def image_compose simpnum_ci[where bs="real i #bs"] image_def) 
    5.46 +    by(simp add: split_def image_comp simpnum_ci[where bs="real i #bs"] image_def) 
    5.47    finally have AA': "?N ` set ?A' = ?N ` ?A" .
    5.48    from \<rho>_l[OF lq] have B_nb:"\<forall> (e,c)\<in> set ?B'. numbound0 e \<and> c > 0"
    5.49      by (simp add: split_def)
     6.1 --- a/src/HOL/Finite_Set.thy	Sat Mar 15 03:37:22 2014 +0100
     6.2 +++ b/src/HOL/Finite_Set.thy	Sat Mar 15 08:31:33 2014 +0100
     6.3 @@ -395,7 +395,7 @@
     6.4      by (auto simp add: finite_conv_nat_seg_image)
     6.5    then have "fst ` (A \<times> B) = fst ` f ` {i::nat. i < n}" by simp
     6.6    with `B \<noteq> {}` have "A = (fst \<circ> f) ` {i::nat. i < n}"
     6.7 -    by (simp add: image_compose)
     6.8 +    by (simp add: image_comp)
     6.9    then have "\<exists>n f. A = f ` {i::nat. i < n}" by blast
    6.10    then show ?thesis
    6.11      by (auto simp add: finite_conv_nat_seg_image)
    6.12 @@ -409,7 +409,7 @@
    6.13      by (auto simp add: finite_conv_nat_seg_image)
    6.14    then have "snd ` (A \<times> B) = snd ` f ` {i::nat. i < n}" by simp
    6.15    with `A \<noteq> {}` have "B = (snd \<circ> f) ` {i::nat. i < n}"
    6.16 -    by (simp add: image_compose)
    6.17 +    by (simp add: image_comp)
    6.18    then have "\<exists>n f. B = f ` {i::nat. i < n}" by blast
    6.19    then show ?thesis
    6.20      by (auto simp add: finite_conv_nat_seg_image)
     7.1 --- a/src/HOL/Fun.thy	Sat Mar 15 03:37:22 2014 +0100
     7.2 +++ b/src/HOL/Fun.thy	Sat Mar 15 08:31:33 2014 +0100
     7.3 @@ -72,11 +72,11 @@
     7.4    by clarsimp
     7.5  
     7.6  lemma image_comp:
     7.7 -  "(f o g) ` r = f ` (g ` r)"
     7.8 +  "f ` (g ` r) = (f o g) ` r"
     7.9    by auto
    7.10  
    7.11  lemma vimage_comp:
    7.12 -  "(g \<circ> f) -` x = f -` (g -` x)"
    7.13 +  "f -` (g -` x) = (g \<circ> f) -` x"
    7.14    by auto
    7.15  
    7.16  code_printing
    7.17 @@ -835,8 +835,6 @@
    7.18  lemmas o_eq_elim = comp_eq_elim
    7.19  lemmas o_eq_dest_lhs = comp_eq_dest_lhs
    7.20  lemmas o_eq_id_dest = comp_eq_id_dest
    7.21 -lemmas image_compose = image_comp
    7.22 -lemmas vimage_compose = vimage_comp
    7.23  
    7.24  end
    7.25  
     8.1 --- a/src/HOL/Lattice/CompleteLattice.thy	Sat Mar 15 03:37:22 2014 +0100
     8.2 +++ b/src/HOL/Lattice/CompleteLattice.thy	Sat Mar 15 08:31:33 2014 +0100
     8.3 @@ -250,7 +250,7 @@
     8.4    proof -
     8.5      have "\<exists>sup. is_Sup (undual ` A') sup" by (rule ex_Sup)
     8.6      then have "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
     8.7 -    then show ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
     8.8 +    then show ?thesis by (simp add: dual_ex [symmetric] image_comp)
     8.9    qed
    8.10  qed
    8.11  
     9.1 --- a/src/HOL/Lattice/Orders.thy	Sat Mar 15 03:37:22 2014 +0100
     9.2 +++ b/src/HOL/Lattice/Orders.thy	Sat Mar 15 08:31:33 2014 +0100
     9.3 @@ -102,7 +102,7 @@
     9.4      have "undual x' \<in> A"
     9.5      proof -
     9.6        from x' have "undual x' \<in> undual ` dual ` A" by simp
     9.7 -      thus "undual x' \<in> A" by (simp add: image_compose [symmetric])
     9.8 +      thus "undual x' \<in> A" by (simp add: image_comp)
     9.9      qed
    9.10      with a have "P (dual (undual x'))" ..
    9.11      also have "\<dots> = x'" by simp
    10.1 --- a/src/HOL/Library/Numeral_Type.thy	Sat Mar 15 03:37:22 2014 +0100
    10.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sat Mar 15 08:31:33 2014 +0100
    10.3 @@ -418,7 +418,7 @@
    10.4  
    10.5    show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
    10.6      unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]
    10.7 -    by(simp add: image_comp inj_on_Abs_bit0 card_image image_int_atLeastLessThan)
    10.8 +    by(simp add: image_comp [symmetric] inj_on_Abs_bit0 card_image image_int_atLeastLessThan)
    10.9        (auto intro!: image_cong[OF refl] simp add: Abs_bit0'_def mod_pos_pos_trivial)
   10.10  
   10.11    fix P :: "'a bit0 \<Rightarrow> bool"
   10.12 @@ -442,7 +442,7 @@
   10.13  
   10.14    show univ_eq: "(UNIV :: 'a bit1 set) = set enum_class.enum"
   10.15      unfolding enum_bit1_def type_definition.Abs_image[OF type_definition_bit1, symmetric]
   10.16 -    by(simp add: image_comp inj_on_Abs_bit1 card_image image_int_atLeastLessThan)
   10.17 +    by(simp add: image_comp [symmetric] inj_on_Abs_bit1 card_image image_int_atLeastLessThan)
   10.18        (auto intro!: image_cong[OF refl] simp add: Abs_bit1'_def mod_pos_pos_trivial)
   10.19  
   10.20    fix P :: "'a bit1 \<Rightarrow> bool"
    11.1 --- a/src/HOL/Library/Permutation.thy	Sat Mar 15 03:37:22 2014 +0100
    11.2 +++ b/src/HOL/Library/Permutation.thy	Sat Mar 15 08:31:33 2014 +0100
    11.3 @@ -211,7 +211,7 @@
    11.4      proof (rule bij_betw_combine)
    11.5        show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
    11.6          using bij unfolding bij_betw_def
    11.7 -        by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def)
    11.8 +        by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def)
    11.9      qed (auto simp: bij_betw_def)
   11.10      fix i
   11.11      assume "i < length (z#xs)"
    12.1 --- a/src/HOL/Library/Product_Order.thy	Sat Mar 15 03:37:22 2014 +0100
    12.2 +++ b/src/HOL/Library/Product_Order.thy	Sat Mar 15 08:31:33 2014 +0100
    12.3 @@ -225,10 +225,10 @@
    12.4  by (auto simp: Sup_prod_def SUP_def)
    12.5  
    12.6  lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
    12.7 -by (auto simp: INF_def Inf_prod_def image_compose)
    12.8 +by (auto simp: INF_def Inf_prod_def image_comp)
    12.9  
   12.10  lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
   12.11 -by (auto simp: SUP_def Sup_prod_def image_compose)
   12.12 +by (auto simp: SUP_def Sup_prod_def image_comp)
   12.13  
   12.14  lemma INF_prod_alt_def:
   12.15    "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
    13.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sat Mar 15 03:37:22 2014 +0100
    13.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sat Mar 15 08:31:33 2014 +0100
    13.3 @@ -644,8 +644,7 @@
    13.4  apply (simp add: eff_def nth_append norm_eff_def)
    13.5  apply (frule_tac x="(pc', None)" and  f=fst and b=pc' in rev_image_eqI) 
    13.6    apply (simp (no_asm_simp))
    13.7 -  apply (simp only: fst_conv image_compose [THEN sym] Fun.comp_def)
    13.8 -  apply simp
    13.9 +  apply (simp add: image_comp Fun.comp_def)
   13.10    apply (frule pc_succs_shift)
   13.11  apply (drule bspec, assumption)
   13.12  apply arith
    14.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Sat Mar 15 03:37:22 2014 +0100
    14.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Sat Mar 15 08:31:33 2014 +0100
    14.3 @@ -68,7 +68,7 @@
    14.4  
    14.5      with fst_eq Cons 
    14.6      show "unique (map f (a # list)) = unique (a # list)"
    14.7 -      by (simp add: unique_def fst_set image_compose)
    14.8 +      by (simp add: unique_def fst_set image_comp)
    14.9    qed
   14.10  qed
   14.11  
   14.12 @@ -95,7 +95,7 @@
   14.13  "(class G C = None) = (class (comp G) C = None)"
   14.14  apply (simp add: class_def comp_def compClass_def)
   14.15  apply (simp add: map_of_in_set)
   14.16 -apply (simp add: image_compose [THEN sym] o_def split_beta)
   14.17 +apply (simp add: image_comp [THEN sym] o_def split_beta)
   14.18  done
   14.19  
   14.20  lemma comp_is_class: "is_class (comp G) C = is_class G C"
   14.21 @@ -174,7 +174,7 @@
   14.22  
   14.23  lemma comp_wf_syscls: "wf_syscls (comp G) = wf_syscls G"
   14.24  apply (simp add: wf_syscls_def comp_def compClass_def split_beta)
   14.25 -apply (simp only: image_compose [THEN sym])
   14.26 +apply (simp add: image_comp)
   14.27  apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
   14.28    (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
   14.29  apply simp
    15.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Mar 15 03:37:22 2014 +0100
    15.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Mar 15 08:31:33 2014 +0100
    15.3 @@ -4182,7 +4182,6 @@
    15.4      apply (rule continuous_on_compose assms)+
    15.5      apply ((rule continuous_on_subset)?, rule assms)+
    15.6      using assms(2,4,8)
    15.7 -    unfolding image_compose
    15.8      apply auto
    15.9      apply blast
   15.10      done
    16.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Mar 15 03:37:22 2014 +0100
    16.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Mar 15 08:31:33 2014 +0100
    16.3 @@ -280,10 +280,10 @@
    16.4    obtain f' where f': "linear f' \<and> f \<circ> f' = id \<and> f' \<circ> f = id"
    16.5      using assms linear_injective_isomorphism[of f] isomorphism_expand by auto
    16.6    then have "f' ` closure (f ` S) \<le> closure (S)"
    16.7 -    using closure_linear_image[of f' "f ` S"] image_compose[of f' f] by auto
    16.8 +    using closure_linear_image[of f' "f ` S"] image_comp[of f' f] by auto
    16.9    then have "f ` f' ` closure (f ` S) \<le> f ` closure S" by auto
   16.10    then have "closure (f ` S) \<le> f ` closure S"
   16.11 -    using image_compose[of f f' "closure (f ` S)"] f' by auto
   16.12 +    using image_comp[of f f' "closure (f ` S)"] f' by auto
   16.13    then show ?thesis using closure_linear_image[of f S] assms by auto
   16.14  qed
   16.15  
    17.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Sat Mar 15 03:37:22 2014 +0100
    17.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Sat Mar 15 08:31:33 2014 +0100
    17.3 @@ -302,7 +302,7 @@
    17.4    have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
    17.5    proof (rule fashoda_unit)
    17.6      show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}"
    17.7 -      using isc and assms(3-4) unfolding image_compose by auto
    17.8 +      using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
    17.9      have *: "continuous_on {- 1..1} iscale"
   17.10        unfolding iscale_def by (rule continuous_on_intros)+
   17.11      show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
    18.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Mar 15 03:37:22 2014 +0100
    18.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Mar 15 08:31:33 2014 +0100
    18.3 @@ -3798,8 +3798,10 @@
    18.4  proof
    18.5    fix f :: "nat \<Rightarrow> 'a \<times> 'b"
    18.6    assume f: "bounded (range f)"
    18.7 -  from f have s1: "bounded (range (fst \<circ> f))"
    18.8 -    unfolding image_comp by (rule bounded_fst)
    18.9 +  then have "bounded (fst ` range f)"
   18.10 +    by (rule bounded_fst)
   18.11 +  then have s1: "bounded (range (fst \<circ> f))"
   18.12 +    by (simp add: image_comp)
   18.13    obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) ----> l1"
   18.14      using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
   18.15    from f have s2: "bounded (range (snd \<circ> f \<circ> r1))"
    19.1 --- a/src/HOL/Predicate.thy	Sat Mar 15 03:37:22 2014 +0100
    19.2 +++ b/src/HOL/Predicate.thy	Sat Mar 15 08:31:33 2014 +0100
    19.3 @@ -85,11 +85,11 @@
    19.4  
    19.5  lemma eval_INFI [simp]:
    19.6    "eval (INFI A f) = INFI A (eval \<circ> f)"
    19.7 -  by (simp only: INF_def eval_Inf image_compose)
    19.8 +  by (simp only: INF_def eval_Inf image_comp)
    19.9  
   19.10  lemma eval_SUPR [simp]:
   19.11    "eval (SUPR A f) = SUPR A (eval \<circ> f)"
   19.12 -  by (simp only: SUP_def eval_Sup image_compose)
   19.13 +  by (simp only: SUP_def eval_Sup image_comp)
   19.14  
   19.15  instantiation pred :: (type) complete_boolean_algebra
   19.16  begin
    20.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Sat Mar 15 03:37:22 2014 +0100
    20.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Sat Mar 15 08:31:33 2014 +0100
    20.3 @@ -936,7 +936,7 @@
    20.4  
    20.5    show ?B
    20.6      using IJ.measurable_emeasure_Pair1[OF merge]
    20.7 -    by (simp add: vimage_compose[symmetric] comp_def space_pair_measure cong: measurable_cong)
    20.8 +    by (simp add: vimage_comp comp_def space_pair_measure cong: measurable_cong)
    20.9  qed
   20.10  
   20.11  lemma (in product_sigma_finite) product_integral_insert:
    21.1 --- a/src/HOL/Probability/Independent_Family.thy	Sat Mar 15 03:37:22 2014 +0100
    21.2 +++ b/src/HOL/Probability/Independent_Family.thy	Sat Mar 15 08:31:33 2014 +0100
    21.3 @@ -794,10 +794,10 @@
    21.4      { fix A assume "A \<in> sets (N i)"
    21.5        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)"
    21.6          by (intro exI[of _ "Y i -` A \<inter> space (M' i)"])
    21.7 -           (auto simp: vimage_compose intro!: measurable_sets rv `i \<in> I` funcset_mem[OF X]) }
    21.8 +           (auto simp: vimage_comp intro!: measurable_sets rv `i \<in> I` funcset_mem[OF X]) }
    21.9      then show "sigma_sets (space M) {(Y i \<circ> X i) -` A \<inter> space M |A. A \<in> sets (N i)} \<subseteq>
   21.10        sigma_sets (space M) {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
   21.11 -      by (intro sigma_sets_subseteq) (auto simp: vimage_compose)
   21.12 +      by (intro sigma_sets_subseteq) (auto simp: vimage_comp)
   21.13    qed
   21.14  qed
   21.15  
    22.1 --- a/src/HOL/Probability/Information.thy	Sat Mar 15 03:37:22 2014 +0100
    22.2 +++ b/src/HOL/Probability/Information.thy	Sat Mar 15 08:31:33 2014 +0100
    22.3 @@ -1640,7 +1640,7 @@
    22.4      using XY unfolding simple_distributed_def by auto
    22.5    from finite_imageI[OF this, of fst]
    22.6    have [simp]: "finite (X`space M)"
    22.7 -    by (simp add: image_compose[symmetric] comp_def)
    22.8 +    by (simp add: image_comp comp_def)
    22.9    note Y[THEN simple_distributed_finite, simp]
   22.10    show "sigma_finite_measure (count_space (X ` space M))"
   22.11      by (simp add: sigma_finite_measure_count_space_finite)
    23.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Sat Mar 15 03:37:22 2014 +0100
    23.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Sat Mar 15 08:31:33 2014 +0100
    23.3 @@ -144,7 +144,7 @@
    23.4    unfolding simple_function_def
    23.5  proof safe
    23.6    show "finite ((g \<circ> f) ` space M)"
    23.7 -    using assms unfolding simple_function_def by (auto simp: image_compose)
    23.8 +    using assms unfolding simple_function_def by (auto simp: image_comp [symmetric])
    23.9  next
   23.10    fix x assume "x \<in> space M"
   23.11    let ?G = "g -` {g (f x)} \<inter> (f`space M)"
   23.12 @@ -2542,7 +2542,7 @@
   23.13    from f have "bij_betw (from_nat_into I) UNIV I"
   23.14      using bij_betw_from_nat_into[OF I] by simp
   23.15    then have "(\<Union>i\<in>I. X i) = (\<Union>i. (X \<circ> from_nat_into I) i)"
   23.16 -    unfolding SUP_def image_compose by (simp add: bij_betw_def)
   23.17 +    unfolding SUP_def image_comp [symmetric] by (simp add: bij_betw_def)
   23.18    then have "emeasure M (UNION I X) = emeasure M (\<Union>i. X (from_nat_into I i))"
   23.19      by simp
   23.20    also have "\<dots> = (\<Sum>i. emeasure M (X (from_nat_into I i)))"
    24.1 --- a/src/HOL/Probability/Measure_Space.thy	Sat Mar 15 03:37:22 2014 +0100
    24.2 +++ b/src/HOL/Probability/Measure_Space.thy	Sat Mar 15 08:31:33 2014 +0100
    24.3 @@ -795,9 +795,9 @@
    24.4  
    24.5  lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))"
    24.6  proof -
    24.7 -  have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
    24.8 -    unfolding SUP_def image_compose
    24.9 -    unfolding surj_from_nat ..
   24.10 +  have "\<Union>range N = \<Union>(N ` range from_nat)" by simp
   24.11 +  then have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
   24.12 +    by (simp only: SUP_def image_comp)
   24.13    then show ?thesis by simp
   24.14  qed
   24.15  
    25.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Sat Mar 15 03:37:22 2014 +0100
    25.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Sat Mar 15 08:31:33 2014 +0100
    25.3 @@ -297,7 +297,7 @@
    25.4    qed
    25.5    have **: "range ?A' = range A"
    25.6      using surj_from_nat
    25.7 -    by (auto simp: image_compose intro!: imageI)
    25.8 +    by (auto simp: image_comp [symmetric] intro!: imageI)
    25.9    show ?thesis unfolding * ** ..
   25.10  qed
   25.11  
   25.12 @@ -1493,12 +1493,13 @@
   25.13    have fab: "f \<in> (space a -> space b)"
   25.14     and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
   25.15       by (auto simp add: measurable_def)
   25.16 -  have eq: "\<And>y. f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
   25.17 +  have eq: "\<And>y. (g \<circ> f) -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
   25.18      by force
   25.19    show ?thesis
   25.20 -    apply (auto simp add: measurable_def vimage_compose)
   25.21 +    apply (auto simp add: measurable_def vimage_comp)
   25.22      apply (metis funcset_mem fab g)
   25.23 -    apply (subst eq, metis ba cb)
   25.24 +    apply (subst eq)
   25.25 +    apply (metis ba cb)
   25.26      done
   25.27  qed
   25.28  
    26.1 --- a/src/HOL/ZF/Zet.thy	Sat Mar 15 03:37:22 2014 +0100
    26.2 +++ b/src/HOL/ZF/Zet.thy	Sat Mar 15 08:31:33 2014 +0100
    26.3 @@ -37,7 +37,7 @@
    26.4    apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
    26.5    apply (simp add: explode_Repl_eq)
    26.6    apply (subgoal_tac "explode z = f ` A")
    26.7 -  apply (simp_all add: image_compose)
    26.8 +  apply (simp_all add: image_comp [symmetric])
    26.9    done
   26.10  
   26.11  lemma zet_image_mem:
   26.12 @@ -58,7 +58,7 @@
   26.13      apply (auto simp add: subset injf)
   26.14      done
   26.15    show ?thesis
   26.16 -    apply (simp add: zet_def' image_compose[symmetric])
   26.17 +    apply (simp add: zet_def' image_comp)
   26.18      apply (rule exI[where x="?w"])
   26.19      apply (simp add: injw image_zet_rep Azet)
   26.20      done
   26.21 @@ -110,7 +110,7 @@
   26.22  lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A"
   26.23    apply (simp add: zimage_def)
   26.24    apply (subst Abs_zet_inverse)
   26.25 -  apply (simp_all add: image_compose zet_image_mem Rep_zet)
   26.26 +  apply (simp_all add: image_comp zet_image_mem Rep_zet)
   26.27    done
   26.28      
   26.29  definition zunion :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> 'a zet" where