more complete set of lemmas wrt. image and composition
--- 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
--- 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}
--- 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)
--- 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)))"
--- 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)
--- 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)
--- 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
--- 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
--- 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
--- 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"
--- 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)"
--- 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))"
--- 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
--- 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
--- 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
--- 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
--- 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)"
--- 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))"
--- 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
--- 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:
--- 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
--- 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)
--- 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)))"
--- 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
--- 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
--- 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