# HG changeset patch # User haftmann # Date 1394989744 -3600 # Node ID 9a241bc276cddb9c40dac2b59bead5489fdde197 # Parent dd89ce51d2c82ae1c98e0532bab826e5d46c895d normalising simp rules for compound operators diff -r dd89ce51d2c8 -r 9a241bc276cd NEWS --- a/NEWS Sat Mar 15 16:54:32 2014 +0100 +++ b/NEWS Sun Mar 16 18:09:04 2014 +0100 @@ -98,6 +98,12 @@ *** HOL *** +* More aggressive normalization of expressions involving INF and Inf +or SUP and Sup. INCOMPATIBILITY. + +* INF_image and SUP_image do not unfold composition. +INCOMPATIBILITY. + * Swapped orientation of facts image_comp and vimage_comp: image_compose ~> image_comp [symmetric] image_comp ~> image_comp [symmetric] diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/BNF_Comp.thy --- a/src/HOL/BNF_Comp.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/BNF_Comp.thy Sun Mar 16 18:09:04 2014 +0100 @@ -25,7 +25,7 @@ fset_bd: "\x. |fset x| \o fbd" and gset_bd: "\x. |gset x| \o gbd" shows "|\(fset ` gset x)| \o gbd *c fbd" -apply (subst sym[OF SUP_def]) +apply simp apply (rule ordLeq_transitive) apply (rule card_of_UNION_Sigma) apply (subst SIGMA_CSUM) @@ -69,7 +69,7 @@ by blast lemma comp_set_bd_Union_o_collect: "|\\((\f. f x) ` X)| \o hbd \ |(Union \ collect X) x| \o hbd" -by (unfold comp_apply collect_def SUP_def) +by (unfold comp_apply collect_def) simp lemma wpull_cong: "\A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\ \ wpull A' B1' B2' f1 f2 p1 p2" diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Complete_Lattices.thy Sun Mar 16 18:09:04 2014 +0100 @@ -1,4 +1,4 @@ - (* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *) +(* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *) header {* Complete lattices *} @@ -20,10 +20,24 @@ definition INFI :: "'b set \ ('b \ 'a) \ 'a" where INF_def: "INFI A f = \(f ` A)" -lemma INF_image [simp]: "INFI (f`A) g = INFI A (\x. g (f x))" - by (simp add: INF_def image_image) +lemma Inf_image_eq [simp]: + "\(f ` A) = INFI A f" + by (simp add: INF_def) + +lemma INF_image [simp]: + "INFI (f ` A) g = INFI A (g \ f)" + by (simp only: INF_def image_comp) -lemma INF_cong: "A = B \ (\x. x \ B \ C x = D x) \ INFI A C = INFI B D" +lemma INF_identity_eq [simp]: + "INFI A (\x. x) = \A" + by (simp add: INF_def) + +lemma INF_id_eq [simp]: + "INFI A id = \A" + by (simp add: id_def) + +lemma INF_cong: + "A = B \ (\x. x \ B \ C x = D x) \ INFI A C = INFI B D" by (simp add: INF_def image_def) end @@ -35,10 +49,24 @@ definition SUPR :: "'b set \ ('b \ 'a) \ 'a" where SUP_def: "SUPR A f = \(f ` A)" -lemma SUP_image [simp]: "SUPR (f`A) g = SUPR A (%x. g (f x))" - by (simp add: SUP_def image_image) +lemma Sup_image_eq [simp]: + "\(f ` A) = SUPR A f" + by (simp add: SUP_def) + +lemma SUP_image [simp]: + "SUPR (f ` A) g = SUPR A (g \ f)" + by (simp only: SUP_def image_comp) -lemma SUP_cong: "A = B \ (\x. x \ B \ C x = D x) \ SUPR A C = SUPR B D" +lemma SUP_identity_eq [simp]: + "SUPR A (\x. x) = \A" + by (simp add: SUP_def) + +lemma SUP_id_eq [simp]: + "SUPR A id = \A" + by (simp add: id_def) + +lemma SUP_cong: + "A = B \ (\x. x \ B \ C x = D x) \ SUPR A C = SUPR B D" by (simp add: SUP_def image_def) end @@ -112,10 +140,11 @@ lemma INF_foundation_dual: "Sup.SUPR Inf = INFI" - by (simp add: fun_eq_iff INF_def Sup.SUP_def) + by (simp add: fun_eq_iff Sup.SUP_def) lemma SUP_foundation_dual: - "Inf.INFI Sup = SUPR" by (simp add: fun_eq_iff SUP_def Inf.INF_def) + "Inf.INFI Sup = SUPR" + by (simp add: fun_eq_iff Inf.INF_def) lemma Sup_eqI: "(\y. y \ A \ y \ x) \ (\y. (\z. z \ A \ z \ y) \ x \ y) \ \A = x" @@ -127,23 +156,23 @@ lemma SUP_eqI: "(\i. i \ A \ f i \ x) \ (\y. (\i. i \ A \ f i \ y) \ x \ y) \ (\i\A. f i) = x" - unfolding SUP_def by (rule Sup_eqI) auto + using Sup_eqI [of "f ` A" x] by auto lemma INF_eqI: "(\i. i \ A \ x \ f i) \ (\y. (\i. i \ A \ f i \ y) \ x \ y) \ (\i\A. f i) = x" - unfolding INF_def by (rule Inf_eqI) auto + using Inf_eqI [of "f ` A" x] by auto lemma INF_lower: "i \ A \ (\i\A. f i) \ f i" - by (auto simp add: INF_def intro: Inf_lower) + using Inf_lower [of _ "f ` A"] by simp lemma INF_greatest: "(\i. i \ A \ u \ f i) \ u \ (\i\A. f i)" - by (auto simp add: INF_def intro: Inf_greatest) + using Inf_greatest [of "f ` A"] by auto lemma SUP_upper: "i \ A \ f i \ (\i\A. f i)" - by (auto simp add: SUP_def intro: Sup_upper) + using Sup_upper [of _ "f ` A"] by simp lemma SUP_least: "(\i. i \ A \ f i \ u) \ (\i\A. f i) \ u" - by (auto simp add: SUP_def intro: Sup_least) + using Sup_least [of "f ` A"] by auto lemma Inf_lower2: "u \ A \ u \ v \ \A \ v" using Inf_lower [of u A] by auto @@ -161,25 +190,25 @@ by (auto intro: Inf_greatest dest: Inf_lower) lemma le_INF_iff: "u \ (\i\A. f i) \ (\i\A. u \ f i)" - by (auto simp add: INF_def le_Inf_iff) + using le_Inf_iff [of _ "f ` A"] by simp lemma Sup_le_iff: "\A \ b \ (\a\A. a \ b)" by (auto intro: Sup_least dest: Sup_upper) lemma SUP_le_iff: "(\i\A. f i) \ u \ (\i\A. f i \ u)" - by (auto simp add: SUP_def Sup_le_iff) + using Sup_le_iff [of "f ` A"] by simp lemma Inf_insert [simp]: "\insert a A = a \ \A" by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower) -lemma INF_insert: "(\x\insert a A. f x) = f a \ INFI A f" - by (simp add: INF_def) +lemma INF_insert [simp]: "(\x\insert a A. f x) = f a \ INFI A f" + unfolding INF_def Inf_insert by simp lemma Sup_insert [simp]: "\insert a A = a \ \A" by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper) -lemma SUP_insert: "(\x\insert a A. f x) = f a \ SUPR A f" - by (simp add: SUP_def) +lemma SUP_insert [simp]: "(\x\insert a A. f x) = f a \ SUPR A f" + unfolding SUP_def Sup_insert by simp lemma INF_empty [simp]: "(\x\{}. f x) = \" by (simp add: INF_def) @@ -219,7 +248,7 @@ lemma INF_mono: "(\m. m \ B \ \n\A. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)" - unfolding INF_def by (rule Inf_mono) fast + using Inf_mono [of "g ` B" "f ` A"] by auto lemma Sup_mono: assumes "\a. a \ A \ \b\B. a \ b" @@ -233,7 +262,7 @@ lemma SUP_mono: "(\n. n \ A \ \m\B. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)" - unfolding SUP_def by (rule Sup_mono) fast + using Sup_mono [of "f ` A" "g ` B"] by auto lemma INF_superset_mono: "B \ A \ (\x. x \ B \ f x \ g x) \ (\x\A. f x) \ (\x\B. g x)" @@ -267,13 +296,13 @@ lemma SUPR_eq: assumes "\i. i \ A \ \j\B. f i \ g j" assumes "\j. j \ B \ \i\A. g j \ f i" - shows "(SUP i:A. f i) = (SUP j:B. g j)" + shows "(\i\A. f i) = (\j\B. g j)" by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+ lemma INFI_eq: assumes "\i. i \ A \ \j\B. f i \ g j" assumes "\j. j \ B \ \i\A. g j \ f i" - shows "(INF i:A. f i) = (INF j:B. g j)" + shows "(\i\A. f i) = (\j\B. g j)" by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+ lemma less_eq_Inf_inter: "\A \ \B \ \(A \ B)" @@ -329,9 +358,9 @@ qed lemma INF_top_conv [simp]: - "(\x\A. B x) = \ \ (\x\A. B x = \)" - "\ = (\x\A. B x) \ (\x\A. B x = \)" - by (auto simp add: INF_def) + "(\x\A. B x) = \ \ (\x\A. B x = \)" + "\ = (\x\A. B x) \ (\x\A. B x = \)" + using Inf_top_conv [of "B ` A"] by simp_all lemma Sup_bot_conv [simp]: "\A = \ \ (\x\A. x = \)" (is ?P) @@ -342,7 +371,7 @@ lemma SUP_bot_conv [simp]: "(\x\A. B x) = \ \ (\x\A. B x = \)" "\ = (\x\A. B x) \ (\x\A. B x = \)" - by (auto simp add: SUP_def) + using Sup_bot_conv [of "B ` A"] by simp_all lemma INF_const [simp]: "A \ {} \ (\i\A. f) = f" by (auto intro: antisym INF_lower INF_greatest) @@ -367,7 +396,7 @@ shows "A k \ (\i\I. A i) = (\i\I. A i)" proof - from assms obtain J where "I = insert k J" by blast - then show ?thesis by (simp add: INF_insert) + then show ?thesis by simp qed lemma SUP_absorb: @@ -375,7 +404,7 @@ shows "A k \ (\i\I. A i) = (\i\I. A i)" proof - from assms obtain J where "I = insert k J" by blast - then show ?thesis by (simp add: SUP_insert) + then show ?thesis by simp qed lemma INF_constant: @@ -406,17 +435,17 @@ lemma INF_UNIV_bool_expand: "(\b. A b) = A True \ A False" - by (simp add: UNIV_bool INF_insert inf_commute) + by (simp add: UNIV_bool inf_commute) lemma SUP_UNIV_bool_expand: "(\b. A b) = A True \ A False" - by (simp add: UNIV_bool SUP_insert sup_commute) + by (simp add: UNIV_bool sup_commute) lemma Inf_le_Sup: "A \ {} \ Inf A \ Sup A" by (blast intro: Sup_upper2 Inf_lower ex_in_conv) lemma INF_le_SUP: "A \ {} \ INFI A f \ SUPR A f" - unfolding INF_def SUP_def by (rule Inf_le_Sup) auto + using Inf_le_Sup [of "f ` A"] by simp lemma SUP_eq_const: "I \ {} \ (\i. i \ I \ f i = x) \ SUPR I f = x" @@ -443,11 +472,11 @@ lemma sup_INF: "a \ (\b\B. f b) = (\b\B. a \ f b)" - by (simp add: INF_def sup_Inf image_image) + by (simp only: INF_def sup_Inf image_image) lemma inf_SUP: "a \ (\b\B. f b) = (\b\B. a \ f b)" - by (simp add: SUP_def inf_Sup image_image) + by (simp only: SUP_def inf_Sup image_image) lemma dual_complete_distrib_lattice: "class.complete_distrib_lattice Sup Inf sup (op \) (op >) inf \ \" @@ -529,17 +558,17 @@ qed lemma uminus_INF: "- (\x\A. B x) = (\x\A. - B x)" - by (simp add: INF_def SUP_def uminus_Inf image_image) + by (simp only: INF_def SUP_def uminus_Inf image_image) lemma uminus_Sup: "- (\A) = \(uminus ` A)" proof - - have "\A = - \(uminus ` A)" by (simp add: image_image uminus_Inf) + have "\A = - \(uminus ` A)" by (simp add: image_image uminus_INF) then show ?thesis by simp qed lemma uminus_SUP: "- (\x\A. B x) = (\x\A. - B x)" - by (simp add: INF_def SUP_def uminus_Sup image_image) + by (simp only: INF_def SUP_def uminus_Sup image_image) end @@ -562,7 +591,7 @@ lemma INF_less_iff: "(\i\A. f i) \ a \ (\x\A. f x \ a)" - unfolding INF_def Inf_less_iff by auto + using Inf_less_iff [of "f ` A"] by simp lemma less_Sup_iff: "a \ \S \ (\x\S. a \ x)" @@ -570,7 +599,7 @@ lemma less_SUP_iff: "a \ (\i\A. f i) \ (\x\A. a \ f x)" - unfolding SUP_def less_Sup_iff by auto + using less_Sup_iff [of _ "f ` A"] by simp lemma Sup_eq_top_iff [simp]: "\A = \ \ (\x<\. \i\A. x < i)" @@ -596,7 +625,7 @@ lemma SUP_eq_top_iff [simp]: "(\i\A. f i) = \ \ (\x<\. \i\A. x < f i)" - unfolding SUP_def by auto + using Sup_eq_top_iff [of "f ` A"] by simp lemma Inf_eq_bot_iff [simp]: "\A = \ \ (\x>\. \i\A. i < x)" @@ -605,18 +634,7 @@ lemma INF_eq_bot_iff [simp]: "(\i\A. f i) = \ \ (\x>\. \i\A. f i < x)" - unfolding INF_def by auto - -lemma le_Sup_iff: "x \ \A \ (\ya\A. y < a)" -proof safe - fix y assume "x \ \A" "y < x" - then have "y < \A" by auto - then show "\a\A. y < a" - unfolding less_Sup_iff . -qed (auto elim!: allE[of _ "\A"] simp add: not_le[symmetric] Sup_upper) - -lemma le_SUP_iff: "x \ SUPR A f \ (\yi\A. y < f i)" - unfolding le_Sup_iff SUP_def by simp + using Inf_eq_bot_iff [of "f ` A"] by simp lemma Inf_le_iff: "\A \ x \ (\y>x. \a\A. y > a)" proof safe @@ -628,7 +646,18 @@ lemma INF_le_iff: "INFI A f \ x \ (\y>x. \i\A. y > f i)" - unfolding Inf_le_iff INF_def by simp + using Inf_le_iff [of "f ` A"] by simp + +lemma le_Sup_iff: "x \ \A \ (\ya\A. y < a)" +proof safe + fix y assume "x \ \A" "y < x" + then have "y < \A" by auto + then show "\a\A. y < a" + unfolding less_Sup_iff . +qed (auto elim!: allE[of _ "\A"] simp add: not_le[symmetric] Sup_upper) + +lemma le_SUP_iff: "x \ SUPR A f \ (\yi\A. y < f i)" + using le_Sup_iff [of _ "f ` A"] by simp subclass complete_distrib_lattice proof @@ -704,14 +733,15 @@ lemma INF_apply [simp]: "(\y\A. f y) x = (\y\A. f y x)" - by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def) + using Inf_apply [of "f ` A"] by (simp add: comp_def) lemma SUP_apply [simp]: "(\y\A. f y) x = (\y\A. f y x)" - by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def) + using Sup_apply [of "f ` A"] by (simp add: comp_def) instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof -qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf image_image) +qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf fun_eq_iff image_image + simp del: Inf_image_eq Sup_image_eq) instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra .. @@ -888,14 +918,14 @@ lemma INTER_eq: "(\x\A. B x) = {y. \x\A. y \ B x}" - by (auto simp add: INF_def) + by (auto intro!: INF_eqI) -lemma Inter_image_eq [simp]: - "\(B`A) = (\x\A. B x)" - by (rule sym) (fact INF_def) +lemma Inter_image_eq: + "\(B ` A) = (\x\A. B x)" + by (fact Inf_image_eq) lemma INT_iff [simp]: "b \ (\x\A. B x) \ (\x\A. b \ B x)" - by (auto simp add: INF_def image_def) + using Inter_iff [of _ "B ` A"] by simp lemma INT_I [intro!]: "(\x. x \ A \ b \ B x) \ b \ (\x\A. B x)" by (auto simp add: INF_def image_def) @@ -1077,7 +1107,7 @@ lemma UNION_eq: "(\x\A. B x) = {y. \x\A. y \ B x}" - by (auto simp add: SUP_def) + by (auto intro!: SUP_eqI) lemma bind_UNION [code]: "Set.bind A f = UNION A f" @@ -1087,12 +1117,12 @@ "x \ Set.bind P f \ x \ UNION P f " by (simp add: bind_UNION) -lemma Union_image_eq [simp]: +lemma Union_image_eq: "\(B ` A) = (\x\A. B x)" - by (rule sym) (fact SUP_def) + by (fact Sup_image_eq) lemma UN_iff [simp]: "b \ (\x\A. B x) \ (\x\A. b \ B x)" - by (auto simp add: SUP_def image_def) + using Union_iff [of _ "B ` A"] by simp lemma UN_I [intro]: "a \ A \ b \ B a \ b \ (\x\A. B x)" -- {* The order of the premises presupposes that @{term A} is rigid; @@ -1214,13 +1244,13 @@ lemma UN_Un_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)" by (rule sym) (rule SUP_sup_distrib) -lemma Int_Inter_image: "(\x\C. A x \ B x) = \(A ` C) \ \(B ` C)" - by (simp only: INT_Int_distrib INF_def) +lemma Int_Inter_image: "(\x\C. A x \ B x) = \(A ` C) \ \(B ` C)" -- {* FIXME drop *} + by (simp add: INT_Int_distrib) -lemma Un_Union_image: "(\x\C. A x \ B x) = \(A ` C) \ \(B ` C)" +lemma Un_Union_image: "(\x\C. A x \ B x) = \(A ` C) \ \(B ` C)" -- {* FIXME drop *} -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *} -- {* Union of a family of unions *} - by (simp only: UN_Un_distrib SUP_def) + by (simp add: UN_Un_distrib) lemma Un_INT_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)" by (fact sup_INF) diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Sun Mar 16 18:09:04 2014 +0100 @@ -275,16 +275,16 @@ by (auto intro!: cInf_eq_minimum) lemma cINF_lower: "bdd_below (f ` A) \ x \ A \ INFI A f \ f x" - unfolding INF_def by (rule cInf_lower) auto + using cInf_lower [of _ "f ` A"] by simp lemma cINF_greatest: "A \ {} \ (\x. x \ A \ m \ f x) \ m \ INFI A f" - unfolding INF_def by (rule cInf_greatest) auto + using cInf_greatest [of "f ` A"] by auto lemma cSUP_upper: "x \ A \ bdd_above (f ` A) \ f x \ SUPR A f" - unfolding SUP_def by (rule cSup_upper) auto + using cSup_upper [of _ "f ` A"] by simp lemma cSUP_least: "A \ {} \ (\x. x \ A \ f x \ M) \ SUPR A f \ M" - unfolding SUP_def by (rule cSup_least) auto + using cSup_least [of "f ` A"] by auto lemma cINF_lower2: "bdd_below (f ` A) \ x \ A \ f x \ u \ INFI A f \ u" by (auto intro: cINF_lower assms order_trans) @@ -311,16 +311,16 @@ by (metis cSUP_upper le_less_trans) lemma cINF_insert: "A \ {} \ bdd_below (f ` A) \ INFI (insert a A) f = inf (f a) (INFI A f)" - by (metis INF_def cInf_insert assms empty_is_image image_insert) + by (metis cInf_insert Inf_image_eq image_insert image_is_empty) lemma cSUP_insert: "A \ {} \ bdd_above (f ` A) \ SUPR (insert a A) f = sup (f a) (SUPR A f)" - by (metis SUP_def cSup_insert assms empty_is_image image_insert) + by (metis cSup_insert Sup_image_eq image_insert image_is_empty) lemma cINF_mono: "B \ {} \ bdd_below (f ` A) \ (\m. m \ B \ \n\A. f n \ g m) \ INFI A f \ INFI B g" - unfolding INF_def by (auto intro: cInf_mono) + using cInf_mono [of "g ` B" "f ` A"] by auto lemma cSUP_mono: "A \ {} \ bdd_above (g ` B) \ (\n. n \ A \ \m\B. f n \ g m) \ SUPR A f \ SUPR B g" - unfolding SUP_def by (auto intro: cSup_mono) + using cSup_mono [of "f ` A" "g ` B"] by auto lemma cINF_superset_mono: "A \ {} \ bdd_below (g ` B) \ A \ B \ (\x. x \ B \ g x \ f x) \ INFI B g \ INFI A f" by (rule cINF_mono) auto @@ -338,13 +338,13 @@ by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower) lemma cINF_union: "A \ {} \ bdd_below (f`A) \ B \ {} \ bdd_below (f`B) \ INFI (A \ B) f = inf (INFI A f) (INFI B f)" - unfolding INF_def using assms by (auto simp add: image_Un intro: cInf_union_distrib) + using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric]) lemma cSup_union_distrib: "A \ {} \ bdd_above A \ B \ {} \ bdd_above B \ Sup (A \ B) = sup (Sup A) (Sup B)" by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper) lemma cSUP_union: "A \ {} \ bdd_above (f`A) \ B \ {} \ bdd_above (f`B) \ SUPR (A \ B) f = sup (SUPR A f) (SUPR B f)" - unfolding SUP_def by (auto simp add: image_Un intro: cSup_union_distrib) + using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric]) lemma cINF_inf_distrib: "A \ {} \ bdd_below (f`A) \ bdd_below (g`A) \ inf (INFI A f) (INFI A g) = (INF a:A. inf (f a) (g a))" by (intro antisym le_infI cINF_greatest cINF_lower2) @@ -388,10 +388,10 @@ by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans) lemma cINF_less_iff: "A \ {} \ bdd_below (f`A) \ (INF i:A. f i) < a \ (\x\A. f x < a)" - unfolding INF_def using cInf_less_iff[of "f`A"] by auto + using cInf_less_iff[of "f`A"] by auto lemma less_cSUP_iff: "A \ {} \ bdd_above (f`A) \ a < (SUP i:A. f i) \ (\x\A. a < f x)" - unfolding SUP_def using less_cSup_iff[of "f`A"] by auto + using less_cSup_iff[of "f`A"] by auto lemma less_cSupE: assumes "y < Sup X" "X \ {}" obtains x where "x \ X" "y < x" diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Finite_Set.thy Sun Mar 16 18:09:04 2014 +0100 @@ -1041,7 +1041,7 @@ interpret comp_fun_idem "inf \ f" by (fact comp_comp_fun_idem) from `finite A` show "?fold = ?inf" by (induct A arbitrary: B) - (simp_all add: INF_def inf_left_commute) + (simp_all add: inf_left_commute) qed lemma sup_SUP_fold_sup: @@ -1052,7 +1052,7 @@ interpret comp_fun_idem "sup \ f" by (fact comp_comp_fun_idem) from `finite A` show "?fold = ?sup" by (induct A arbitrary: B) - (simp_all add: SUP_def sup_left_commute) + (simp_all add: sup_left_commute) qed lemma INF_fold_inf: diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/GCD.thy --- a/src/HOL/GCD.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/GCD.thy Sun Mar 16 18:09:04 2014 +0100 @@ -1581,6 +1581,9 @@ from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR Lcm A f = Lcm (f ` A)" . qed +declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del] +declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del] + lemma Lcm_empty_nat: "Lcm {} = (1::nat)" by (fact Lcm_nat_empty) @@ -1736,11 +1739,11 @@ lemma Lcm_set_int [code, code_unfold]: "Lcm (set xs) = fold lcm xs (1::int)" - by (induct xs rule: rev_induct, simp_all add: lcm_commute_int) + by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int) lemma Gcd_set_int [code, code_unfold]: "Gcd (set xs) = fold gcd xs (0::int)" - by (induct xs rule: rev_induct, simp_all add: gcd_commute_int) + by (induct xs rule: rev_induct) (simp_all add: gcd_commute_int) end diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Groups_Big.thy Sun Mar 16 18:09:04 2014 +0100 @@ -162,8 +162,7 @@ proof cases assume "finite C" from UNION_disjoint [OF this assms] - show ?thesis - by (simp add: SUP_def) + show ?thesis by simp qed (auto dest: finite_UnionD intro: infinite) lemma distrib: @@ -1020,7 +1019,7 @@ (ALL A:C. ALL B:C. A \ B --> A Int B = {}) ==> card (Union C) = setsum card C" apply (frule card_UN_disjoint [of C id]) -apply (simp_all add: SUP_def id_def) +apply simp_all done diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Library/Extended_Real.thy Sun Mar 16 18:09:04 2014 +0100 @@ -1389,16 +1389,26 @@ qed lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S" - by (auto intro!: Sup_eqI + by (auto intro!: SUP_eqI simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff intro!: complete_lattice_class.Inf_lower2) +lemma ereal_SUP_uminus_eq: + fixes f :: "'a \ ereal" + shows "(SUP x:S. uminus (f x)) = - (INF x:S. f x)" + using ereal_Sup_uminus_image_eq [of "f ` S"] by (simp add: comp_def) + lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)" by (auto intro!: inj_onI) lemma ereal_Inf_uminus_image_eq: "Inf (uminus ` S::ereal set) = - Sup S" using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp +lemma ereal_INF_uminus_eq: + fixes f :: "'a \ ereal" + shows "(INF x:S. uminus (f x)) = - (SUP x:S. f x)" + using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def) + lemma ereal_SUP_not_infty: fixes f :: "_ \ ereal" shows "A \ {} \ l \ -\ \ u \ \ \ \a\A. l \ f a \ f a \ u \ \SUPR A f\ \ \" @@ -1415,7 +1425,7 @@ fixes f :: "'a \ ereal" shows "(SUP i : R. -(f i)) = -(INF i : R. f i)" using ereal_Sup_uminus_image_eq[of "f`R"] - by (simp add: SUP_def INF_def image_image) + by (simp add: image_image) lemma ereal_INFI_uminus: fixes f :: "'a \ ereal" @@ -1763,7 +1773,7 @@ lemma SUPR_countable_SUPR: "A \ {} \ \f::nat \ ereal. range f \ g`A \ SUPR A g = SUPR UNIV f" using Sup_countable_SUPR[of "g`A"] - by (auto simp: SUP_def) + by auto lemma Sup_ereal_cadd: fixes A :: "ereal set" @@ -1772,7 +1782,7 @@ shows "Sup ((\x. a + x) ` A) = a + Sup A" proof (rule antisym) have *: "\a::ereal. \A. Sup ((\x. a + x) ` A) \ a + Sup A" - by (auto intro!: add_mono complete_lattice_class.Sup_least complete_lattice_class.Sup_upper) + by (auto intro!: add_mono complete_lattice_class.SUP_least complete_lattice_class.Sup_upper) then show "Sup ((\x. a + x) ` A) \ a + Sup A" . show "a + Sup A \ Sup ((\x. a + x) ` A)" proof (cases a) @@ -1794,8 +1804,8 @@ assumes "A \ {}" and "a \ -\" shows "Sup ((\x. a - x) ` A) = a - Inf A" - using Sup_ereal_cadd[of "uminus ` A" a] assms - by (simp add: comp_def image_image minus_ereal_def ereal_Sup_uminus_image_eq) + using Sup_ereal_cadd [of "uminus ` A" a] assms + unfolding image_image minus_ereal_def by (simp add: ereal_SUP_uminus_eq) lemma SUPR_ereal_cminus: fixes f :: "'i \ ereal" @@ -1820,8 +1830,8 @@ then have "(\x. -a - x)`uminus`A = uminus ` (\x. a - x) ` A" by (auto simp: image_image) with * show ?thesis - using Sup_ereal_cminus[of "uminus ` A" "-a"] assms - by (auto simp add: ereal_Sup_uminus_image_eq ereal_Inf_uminus_image_eq) + using Sup_ereal_cminus [of "uminus ` A" "- a"] assms + by (auto simp add: ereal_INF_uminus_eq ereal_SUP_uminus_eq) qed lemma INFI_ereal_cminus: diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Library/FSet.thy Sun Mar 16 18:09:04 2014 +0100 @@ -143,7 +143,7 @@ lift_definition uminus_fset :: "'a fset \ 'a fset" is uminus parametric right_total_Compl_transfer Compl_transfer by simp -instance by (default, simp_all only: INF_def SUP_def) (transfer, auto)+ +instance by (default, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+ end diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Library/Option_ord.thy --- a/src/HOL/Library/Option_ord.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Library/Option_ord.thy Sun Mar 16 18:09:04 2014 +0100 @@ -292,11 +292,11 @@ lemma Some_INF: "Some (\x\A. f x) = (\x\A. Some (f x))" - by (simp add: INF_def Some_Inf image_image) + using Some_Inf [of "f ` A"] by (simp add: comp_def) lemma Some_SUP: "A \ {} \ Some (\x\A. f x) = (\x\A. Some (f x))" - by (simp add: SUP_def Some_Sup image_image) + using Some_Sup [of "f ` A"] by (simp add: comp_def) instantiation option :: (complete_distrib_lattice) complete_distrib_lattice begin @@ -319,7 +319,7 @@ case False then have B: "{x \ B. \y. x = Some y} = B" by auto (metis not_Some_eq) from sup_Inf have "Some c \ Some (\Option.these B) = Some (\b\Option.these B. c \ b)" by simp then have "Some c \ \(Some ` Option.these B) = (\x\Some ` Option.these B. Some c \ x)" - by (simp add: Some_INF Some_Inf) + by (simp add: Some_INF Some_Inf comp_def) with Some B show ?thesis by (simp add: Some_image_these_eq) qed qed @@ -332,7 +332,7 @@ show ?thesis proof (cases "B = {} \ B = {None}") case True - then show ?thesis by (auto simp add: SUP_def) + then show ?thesis by auto next have B: "B = {x \ B. \y. x = Some y} \ {x \ B. x = None}" by auto @@ -347,7 +347,7 @@ moreover from inf_Sup have "Some c \ Some (\Option.these B) = Some (\b\Option.these B. c \ b)" by simp ultimately have "Some c \ \(Some ` Option.these B) = (\x\Some ` Option.these B. Some c \ x)" - by (simp add: Some_SUP Some_Sup) + by (simp add: Some_SUP Some_Sup comp_def) with Some show ?thesis by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib) qed diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Library/Product_Order.thy --- a/src/HOL/Library/Product_Order.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Library/Product_Order.thy Sun Mar 16 18:09:04 2014 +0100 @@ -178,7 +178,7 @@ instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice) conditionally_complete_lattice by default (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def - INF_def SUP_def intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+ + INF_def SUP_def simp del: Inf_image_eq Sup_image_eq intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+ instance prod :: (complete_lattice, complete_lattice) complete_lattice by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def @@ -197,46 +197,46 @@ unfolding Inf_prod_def by simp lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))" - by (simp add: SUP_def fst_Sup image_image) + using fst_Sup [of "f ` A", symmetric] by (simp add: comp_def) lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))" - by (simp add: SUP_def snd_Sup image_image) + using snd_Sup [of "f ` A", symmetric] by (simp add: comp_def) lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))" - by (simp add: INF_def fst_Inf image_image) + using fst_Inf [of "f ` A", symmetric] by (simp add: comp_def) lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))" - by (simp add: INF_def snd_Inf image_image) + using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def) lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)" - by (simp add: SUP_def Sup_prod_def image_image) + unfolding SUP_def Sup_prod_def by (simp add: comp_def) lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)" - by (simp add: INF_def Inf_prod_def image_image) + unfolding INF_def Inf_prod_def by (simp add: comp_def) text {* Alternative formulations for set infima and suprema over the product of two complete lattices: *} lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))" -by (auto simp: Inf_prod_def INF_def) +by (auto simp: Inf_prod_def) lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))" -by (auto simp: Sup_prod_def SUP_def) +by (auto simp: Sup_prod_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_comp) + unfolding INF_def Inf_prod_def by simp 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_comp) + unfolding SUP_def Sup_prod_def by simp lemma INF_prod_alt_def: "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))" -by (metis fst_INF snd_INF surjective_pairing) + by (simp add: INFI_prod_alt_def comp_def) lemma SUP_prod_alt_def: "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))" -by (metis fst_SUP snd_SUP surjective_pairing) + by (simp add: SUPR_prod_alt_def comp_def) subsection {* Complete distributive lattices *} diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Lifting_Set.thy --- a/src/HOL/Lifting_Set.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Lifting_Set.thy Sun Mar 16 18:09:04 2014 +0100 @@ -125,7 +125,7 @@ lemma UNION_transfer [transfer_rule]: "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION" - unfolding SUP_def [abs_def] by transfer_prover + unfolding Union_image_eq [symmetric, abs_def] by transfer_prover lemma Ball_transfer [transfer_rule]: "(rel_set A ===> (A ===> op =) ===> op =) Ball Ball" diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/List.thy --- a/src/HOL/List.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/List.thy Sun Mar 16 18:09:04 2014 +0100 @@ -2877,13 +2877,13 @@ lemma (in complete_lattice) INF_set_fold: "INFI (set xs) f = fold (inf \ f) xs top" - unfolding INF_def set_map [symmetric] Inf_set_fold fold_map .. + using Inf_set_fold [of "map f xs "] by (simp add: fold_map) declare INF_set_fold [code] lemma (in complete_lattice) SUP_set_fold: "SUPR (set xs) f = fold (sup \ f) xs bot" - unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map .. + using Sup_set_fold [of "map f xs "] by (simp add: fold_map) declare SUP_set_fold [code] diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Sun Mar 16 18:09:04 2014 +0100 @@ -917,8 +917,8 @@ fixes f :: "nat \ ereal" assumes "\n. 0 \ f n" shows "(\n (\n. f n)" - unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def - by (auto intro: complete_lattice_class.Sup_upper) + unfolding suminf_ereal_eq_SUPR[OF assms] + by (auto intro: complete_lattice_class.SUP_upper) lemma suminf_0_le: fixes f :: "nat \ ereal" @@ -1215,8 +1215,9 @@ apply (subst SUP_inf) apply (intro SUP_cong[OF refl]) apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union) - apply (simp add: INF_def del: inf_ereal_def) - done + apply (drule sym) + apply auto + by (metis INF_absorb centre_in_ball) subsection {* monoset *} diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Sun Mar 16 18:09:04 2014 +0100 @@ -18,7 +18,7 @@ lemma cInf_abs_ge: (* TODO: is this really needed? *) fixes S :: "real set" shows "S \ {} \ (\x\S. \x\ \ a) \ \Inf S\ \ a" - by (simp add: Inf_real_def) (rule cSup_abs_le, auto) + by (simp add: Inf_real_def) (insert cSup_abs_le [of "uminus ` S"], auto) lemma cSup_asclose: (* TODO: is this really needed? *) fixes S :: "real set" diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sun Mar 16 18:09:04 2014 +0100 @@ -2709,7 +2709,7 @@ lemma infnorm_Max: fixes x :: "'a::euclidean_space" shows "infnorm x = Max ((\i. abs (x \ i)) ` Basis)" - by (simp add: infnorm_def infnorm_set_image cSup_eq_Max) + by (simp add: infnorm_def infnorm_set_image cSup_eq_Max del: Sup_image_eq) lemma infnorm_set_lemma: fixes x :: "'a::euclidean_space" diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Sun Mar 16 18:09:04 2014 +0100 @@ -39,10 +39,12 @@ hence "\i. (\x. x \ i) ` X \ {}" by simp thus "(\x. x \ X \ z \ x) \ z \ Inf X" "(\x. x \ X \ x \ z) \ Sup X \ z" by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def + simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq intro!: cInf_greatest cSup_least) qed (force intro!: cInf_lower cSup_upper simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def - eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def)+ + eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def + simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq)+ lemma inner_Basis_inf_left: "i \ Basis \ inf x y \ i = inf (x \ i) (y \ i)" and inner_Basis_sup_left: "i \ Basis \ sup x y \ i = sup (x \ i) (y \ i)" @@ -51,7 +53,7 @@ lemma inner_Basis_INF_left: "i \ Basis \ (INF x:X. f x) \ i = (INF x:X. f x \ i)" and inner_Basis_SUP_left: "i \ Basis \ (SUP x:X. f x) \ i = (SUP x:X. f x \ i)" - by (simp_all add: INF_def SUP_def eucl_Sup eucl_Inf) + using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def) lemma abs_inner: "i \ Basis \ abs x \ i = abs (x \ i)" by (auto simp: eucl_abs) @@ -87,7 +89,7 @@ shows "Sup s = X" using assms unfolding eucl_Sup euclidean_representation_setsum - by (auto simp: Sup_class.SUP_def intro!: conditionally_complete_lattice_class.cSup_eq_maximum) + by (auto simp: Sup_class.SUP_def simp del: Sup_class.Sup_image_eq intro!: conditionally_complete_lattice_class.cSup_eq_maximum) lemma Inf_eq_minimum_componentwise: assumes i: "\b. b \ Basis \ X \ b = i b \ b" @@ -96,7 +98,7 @@ shows "Inf s = X" using assms unfolding eucl_Inf euclidean_representation_setsum - by (auto simp: Inf_class.INF_def intro!: conditionally_complete_lattice_class.cInf_eq_minimum) + by (auto simp: Inf_class.INF_def simp del: Inf_class.Inf_image_eq intro!: conditionally_complete_lattice_class.cInf_eq_minimum) end @@ -115,10 +117,11 @@ and x: "x \ X" "s = x \ b" "\y. y \ X \ x \ b \ y \ b" by auto hence "Inf ?proj = x \ b" - by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum) + by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq) hence "x \ b = Inf X \ b" - by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \ Basis` - setsum_delta cong: if_cong) + by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \ Basis` setsum_delta + simp del: Inf_class.Inf_image_eq + cong: if_cong) with x show "\x. x \ X \ x \ b = Inf X \ b \ (\y. y \ X \ x \ b \ y \ b)" by blast qed @@ -137,10 +140,10 @@ and x: "x \ X" "s = x \ b" "\y. y \ X \ y \ b \ x \ b" by auto hence "Sup ?proj = x \ b" - by (auto intro!: cSup_eq_maximum) + by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq) hence "x \ b = Sup X \ b" - by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \ Basis` - setsum_delta cong: if_cong) + by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \ Basis` setsum_delta + simp del: Sup_image_eq cong: if_cong) with x show "\x. x \ X \ x \ b = Sup X \ b \ (\y. y \ X \ y \ b \ x \ b)" by blast qed @@ -715,7 +718,7 @@ lemma diameter_closed_interval: fixes a b::"'a::ordered_euclidean_space" shows "a \ b \ diameter {a..b} = dist a b" - by (force simp add: diameter_def SUP_def intro!: cSup_eq_maximum setL2_mono + by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono simp: euclidean_dist_l2[where 'a='a] eucl_le[where 'a='a] dist_norm) text {* Intervals in general, including infinite and mixtures of open and closed. *} diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Mar 16 18:09:04 2014 +0100 @@ -1548,7 +1548,7 @@ fix y assume "y \ {x<..} \ I" with False bnd have "Inf (f ` ({x<..} \ I)) \ f y" - by (auto intro!: cInf_lower bdd_belowI2) + by (auto intro!: cInf_lower bdd_belowI2 simp del: Inf_image_eq) with a have "a < f y" by (blast intro: less_le_trans) } @@ -3116,7 +3116,7 @@ fix X assume "X \ P' ` insert U A" "finite X" "Inf X = bot" then obtain B where "B \ insert U A" "finite B" and B: "Inf (P' ` B) = bot" - unfolding subset_image_iff by (auto intro: inj_P' finite_imageD) + unfolding subset_image_iff by (auto intro: inj_P' finite_imageD simp del: Inf_image_eq) with A(2)[THEN spec, of "B - {U}"] have "U \ \(B - {U}) \ {}" by auto with B show False diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Predicate.thy Sun Mar 16 18:09:04 2014 +0100 @@ -85,11 +85,11 @@ lemma eval_INFI [simp]: "eval (INFI A f) = INFI A (eval \ f)" - by (simp only: INF_def eval_Inf image_comp) + using eval_Inf [of "f ` A"] by simp lemma eval_SUPR [simp]: "eval (SUPR A f) = SUPR A (eval \ f)" - by (simp only: SUP_def eval_Sup image_comp) + using eval_Sup [of "f ` A"] by simp instantiation pred :: (type) complete_boolean_algebra begin diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Probability/Caratheodory.thy --- a/src/HOL/Probability/Caratheodory.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Probability/Caratheodory.thy Sun Mar 16 18:09:04 2014 +0100 @@ -975,7 +975,7 @@ have "(\n. \_r (A' n)) = (\n. \c\C'. \_r (A' n \ c))" using C' A' by (subst volume_finite_additive[symmetric, OF V(1)]) - (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Union_image_eq + (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq intro!: G.Int G.finite_Union arg_cong[where f="\X. suminf (\i. \_r (X i))"] ext intro: generated_ringI_Basic) also have "\ = (\c\C'. \n. \_r (A' n \ c))" @@ -987,7 +987,7 @@ also have "\ = \_r (\C')" using C' Un_A by (subst volume_finite_additive[symmetric, OF V(1)]) - (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Union_image_eq + (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq intro: generated_ringI_Basic) finally show "(\n. \_r (A' n)) = \_r (\i. A' i)" using C' by simp diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Probability/Lebesgue_Integration.thy --- a/src/HOL/Probability/Lebesgue_Integration.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Sun Mar 16 18:09:04 2014 +0100 @@ -936,7 +936,7 @@ by (intro ereal_mult_strict_right_mono) (auto simp: image_iff) also have "\ \ (SUP i. f i x)" using u(2) by (auto simp: le_fun_def) finally obtain i where "a * u x < f i x" unfolding SUP_def - by (auto simp add: less_Sup_iff) + by (auto simp add: less_SUP_iff) hence "a * u x \ f i x" by auto thus ?thesis using `x \ space M` by auto qed diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Probability/Probability_Measure.thy Sun Mar 16 18:09:04 2014 +0100 @@ -159,7 +159,7 @@ moreover { fix y assume y: "y \ I" with q(2) `open I` have "Sup ((\x. q x + ?F x * (y - x)) ` I) = q y" - by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) } + by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open simp del: Sup_image_eq Inf_image_eq) } ultimately have "q (expectation X) = Sup ((\x. q x + ?F x * (expectation X - x)) ` I)" by simp also have "\ \ expectation (\w. q (X w))" diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Probability/Radon_Nikodym.thy --- a/src/HOL/Probability/Radon_Nikodym.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Probability/Radon_Nikodym.thy Sun Mar 16 18:09:04 2014 +0100 @@ -386,7 +386,7 @@ also have "\ = ?y" proof (rule antisym) show "(SUP i. integral\<^sup>P M (?g i)) \ ?y" - using g_in_G by (auto intro: Sup_mono simp: SUP_def) + using g_in_G by (auto intro: SUP_mono) show "?y \ (SUP i. integral\<^sup>P M (?g i))" unfolding y_eq by (auto intro!: SUP_mono positive_integral_mono Max_ge) qed diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Probability/Regularity.thy --- a/src/HOL/Probability/Regularity.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Probability/Regularity.thy Sun Mar 16 18:09:04 2014 +0100 @@ -319,8 +319,8 @@ by (rule INF_superset_mono) (auto simp add: compact_imp_closed) also have "(INF U:{U. U \ B \ closed U}. M (space M - U)) = (INF U:{U. space M - B \ U \ open U}. emeasure M U)" - by (subst INF_image[of "\u. space M - u", symmetric]) - (rule INF_cong, auto simp add: sU intro!: INF_cong) + by (subst INF_image [of "\u. space M - u", symmetric, unfolded comp_def]) + (rule INF_cong, auto simp add: sU intro!: INF_cong) finally have "(INF U:{U. space M - B \ U \ open U}. emeasure M U) \ emeasure M (space M - B)" . moreover have @@ -335,7 +335,7 @@ also have "\ = (SUP U:{U. B \ U \ open U}. M (space M - U))" by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed) also have "\ = (SUP K:{K. K \ space M - B \ closed K}. emeasure M K)" - by (subst SUP_image[of "\u. space M - u", symmetric]) + by (subst SUP_image [of "\u. space M - u", symmetric, simplified comp_def]) (rule SUP_cong, auto simp: sU) also have "\ = (SUP K:{K. K \ space M - B \ compact K}. emeasure M K)" proof (safe intro!: antisym SUP_least) diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Topological_Spaces.thy Sun Mar 16 18:09:04 2014 +0100 @@ -31,13 +31,13 @@ using open_Union [of "{S, T}"] by simp lemma open_UN [intro]: "\x\A. open (B x) \ open (\x\A. B x)" - unfolding SUP_def by (rule open_Union) auto + using open_Union [of "B ` A"] by simp lemma open_Inter [intro]: "finite S \ \T\S. open T \ open (\S)" by (induct set: finite) auto lemma open_INT [intro]: "finite A \ \x\A. open (B x) \ open (\x\A. B x)" - unfolding INF_def by (rule open_Inter) auto + using open_Inter [of "B ` A"] by simp lemma openI: assumes "\x. x \ S \ \T. open T \ x \ T \ T \ S" @@ -70,7 +70,7 @@ by (induct set: finite) auto lemma closed_UN [intro]: "finite A \ \x\A. closed (B x) \ closed (\x\A. B x)" - unfolding SUP_def by (rule closed_Union) auto + using closed_Union [of "B ` A"] by simp lemma open_closed: "open S \ closed (- S)" unfolding closed_def by simp @@ -169,7 +169,7 @@ lemma generate_topology_Union: "(\k. k \ I \ generate_topology S (K k)) \ generate_topology S (\k\I. K k)" - unfolding SUP_def by (intro generate_topology.UN) auto + using generate_topology.UN [of "K ` I"] by auto lemma topological_space_generate_topology: "class.topological_space (generate_topology S)" @@ -1952,10 +1952,25 @@ unfolding compact_fip by auto lemma compact_imp_fip_image: - "compact s \ (\i. i \ I \ closed (f i)) \ (\I'. finite I' \ I' \ I \ (s \ (\i\I'. f i) \ {})) \ - s \ (\i\I. f i) \ {}" - using finite_subset_image[of _ f I] compact_imp_fip[of s "f`I"] unfolding ball_simps[symmetric] INF_def - by (metis image_iff) + assumes "compact s" + and P: "\i. i \ I \ closed (f i)" + and Q: "\I'. finite I' \ I' \ I \ (s \ (\i\I'. f i) \ {})" + shows "s \ (\i\I. f i) \ {}" +proof - + note `compact s` + moreover from P have "\i \ f ` I. closed i" by blast + moreover have "\A. finite A \ A \ f ` I \ (s \ (\A) \ {})" + proof (rule, rule, erule conjE) + fix A :: "'a set set" + assume "finite A" + moreover assume "A \ f ` I" + ultimately obtain B where "B \ I" and "finite B" and "A = f ` B" + using finite_subset_image [of A f I] by blast + with Q [of B] show "s \ \A \ {}" by simp + qed + ultimately have "s \ (\(f ` I)) \ {}" by (rule compact_imp_fip) + then show ?thesis by simp +qed end diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/UNITY/ProgressSets.thy --- a/src/HOL/UNITY/ProgressSets.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/UNITY/ProgressSets.thy Sun Mar 16 18:09:04 2014 +0100 @@ -257,7 +257,7 @@ apply (simp add: progress_induction_step) txt{*Disjunctive case*} apply (subgoal_tac "(\U\W. T \ U) \ C") - apply (simp add: Int_Union) + apply simp apply (blast intro: UN_in_lattice) done diff -r dd89ce51d2c8 -r 9a241bc276cd src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Sat Mar 15 16:54:32 2014 +0100 +++ b/src/HOL/Wellfounded.thy Sun Mar 16 18:09:04 2014 +0100 @@ -306,7 +306,7 @@ "[| ALL r:R. wf r; ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {} |] ==> wf(Union R)" - using wf_UN[of R "\i. i"] by (simp add: SUP_def) + using wf_UN[of R "\i. i"] by simp (*Intuition: we find an (R u S)-min element of a nonempty subset A by case distinction.