# HG changeset patch # User haftmann # Date 1455742316 -3600 # Node ID 24106dc44def11185bb14534166b0f256565ca35 # Parent 1cf129590be80ec93bfa233085599654265a77a8 prefer abbreviations for compound operators INFIMUM and SUPREMUM diff -r 1cf129590be8 -r 24106dc44def CONTRIBUTORS --- a/CONTRIBUTORS Wed Feb 17 21:51:55 2016 +0100 +++ b/CONTRIBUTORS Wed Feb 17 21:51:56 2016 +0100 @@ -6,6 +6,10 @@ Contributions to this Isabelle version -------------------------------------- +* January 2016: Florian Haftmann + Abolition of compound operators INFIMUM and SUPREMUM + for complete lattices. + Contributions to Isabelle2016 ----------------------------- diff -r 1cf129590be8 -r 24106dc44def NEWS --- a/NEWS Wed Feb 17 21:51:55 2016 +0100 +++ b/NEWS Wed Feb 17 21:51:56 2016 +0100 @@ -32,6 +32,9 @@ pred_prod_apply ~> pred_prod_inject INCOMPATIBILITY. +* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. +INCOMPATIBILITY. + New in Isabelle2016 (February 2016) ----------------------------------- diff -r 1cf129590be8 -r 24106dc44def src/HOL/Algebra/AbelCoset.thy --- a/src/HOL/Algebra/AbelCoset.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Algebra/AbelCoset.thy Wed Feb 17 21:51:56 2016 +0100 @@ -258,7 +258,7 @@ from a_subgroup have Hcarr: "H \ carrier G" unfolding subgroup_def by simp from xcarr Hcarr show "(\h\H. {h \\<^bsub>G\<^esub> x}) = (\h\H. {x \\<^bsub>G\<^esub> h})" - using m_comm [simplified] by fast + using m_comm [simplified] by fastforce qed qed diff -r 1cf129590be8 -r 24106dc44def src/HOL/Algebra/Coset.thy --- a/src/HOL/Algebra/Coset.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Algebra/Coset.thy Wed Feb 17 21:51:56 2016 +0100 @@ -517,7 +517,7 @@ by (auto simp add: set_mult_def subsetD) lemma (in group) subgroup_mult_id: "subgroup H G \ H <#> H = H" -apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def) +apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def) apply (rule_tac x = x in bexI) apply (rule bexI [of _ "\"]) apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD]) @@ -932,10 +932,22 @@ obtain g where g: "g \ carrier G" and "X = kernel G H h #> g" by (auto simp add: FactGroup_def RCOSETS_def) - hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g) + hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def g intro!: imageI) thus ?thesis by (auto simp add: g) qed +lemma the_elem_image_unique: -- {* FIXME move *} + assumes "A \ {}" + assumes *: "\y. y \ A \ f y = f x" + shows "the_elem (f ` A) = f x" +unfolding the_elem_def proof (rule the1_equality) + from `A \ {}` obtain y where "y \ A" by auto + with * have "f x = f y" by simp + with `y \ A` have "f x \ f ` A" by blast + with * show "f ` A = {f x}" by auto + then show "\!x. f ` A = {x}" by auto +qed + lemma (in group_hom) FactGroup_hom: "(\X. the_elem (h`X)) \ hom (G Mod (kernel G H h)) H" apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed) @@ -952,11 +964,11 @@ and Xsub: "X \ carrier G" and X'sub: "X' \ carrier G" by (force simp add: kernel_def r_coset_def image_def)+ hence "h ` (X <#> X') = {h g \\<^bsub>H\<^esub> h g'}" using X X' - by (auto dest!: FactGroup_nonempty - simp add: set_mult_def image_eq_UN + by (auto dest!: FactGroup_nonempty intro!: image_eqI + simp add: set_mult_def subsetD [OF Xsub] subsetD [OF X'sub]) - thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) \\<^bsub>H\<^esub> the_elem (h ` X')" - by (simp add: all image_eq_UN FactGroup_nonempty X X') + then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \\<^bsub>H\<^esub> the_elem (h ` X')" + by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique) qed @@ -964,7 +976,7 @@ lemma (in group_hom) FactGroup_subset: "\g \ carrier G; g' \ carrier G; h g = h g'\ \ kernel G H h #> g \ kernel G H h #> g'" -apply (clarsimp simp add: kernel_def r_coset_def image_def) +apply (clarsimp simp add: kernel_def r_coset_def) apply (rename_tac y) apply (rule_tac x="y \ g \ inv g'" in exI) apply (simp add: G.m_assoc) @@ -985,7 +997,7 @@ by (force simp add: kernel_def r_coset_def image_def)+ assume "the_elem (h ` X) = the_elem (h ` X')" hence h: "h g = h g'" - by (simp add: image_eq_UN all FactGroup_nonempty X X') + by (simp add: all FactGroup_nonempty X X' the_elem_image_unique) show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) qed @@ -1006,7 +1018,10 @@ hence "(\x\kernel G H h #> g. {h x}) = {y}" by (auto simp add: y kernel_def r_coset_def) with g show "y \ (\X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)" - by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN) + apply (auto intro!: bexI image_eqI simp add: FactGroup_def RCOSETS_def) + apply (subst the_elem_image_unique) + apply auto + done qed qed @@ -1019,5 +1034,4 @@ by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def FactGroup_onto) - end diff -r 1cf129590be8 -r 24106dc44def src/HOL/Auth/Guard/Proto.thy --- a/src/HOL/Auth/Guard/Proto.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Auth/Guard/Proto.thy Wed Feb 17 21:51:56 2016 +0100 @@ -56,7 +56,7 @@ Nonce n ~:parts (apm s `(msg `(fst R))) |] ==> (EX k. Nonce k:parts {X} & nonce s k = n)" apply (erule Nonce_apm, unfold wdef_def) -apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp simp: image_eq_UN) +apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp) apply (drule_tac x=x in bspec, simp) apply (drule_tac Y="msg x" and s=s in apm_parts, simp) by (blast dest: parts_parts) @@ -134,7 +134,7 @@ lemma ok_not_used: "[| Nonce n ~:used evs; ok evs R s; ALL x. x:fst R --> is_Says x |] ==> Nonce n ~:parts (apm s `(msg `(fst R)))" -apply (unfold ok_def, clarsimp simp: image_eq_UN) +apply (unfold ok_def, clarsimp) apply (drule_tac x=x in spec, drule_tac x=x in spec) by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts) @@ -188,10 +188,10 @@ apply (drule wdef_Nonce, simp+) apply (frule ok_not_used, simp+) apply (clarify, erule ok_is_Says, simp+) -apply (clarify, rule_tac x=k in exI, simp add: newn_def image_eq_UN) +apply (clarify, rule_tac x=k in exI, simp add: newn_def) apply (clarify, drule_tac Y="msg x" and s=s in apm_parts) apply (drule ok_not_used, simp+) -by (clarify, erule ok_is_Says, simp_all add: image_eq_UN) +by (clarify, erule ok_is_Says, simp_all) lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs; Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev" diff -r 1cf129590be8 -r 24106dc44def src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Auth/Message.thy Wed Feb 17 21:51:56 2016 +0100 @@ -207,8 +207,16 @@ apply (erule parts.induct, blast+) done -lemma parts_UN [simp]: "parts(\x\A. H x) = (\x\A. parts(H x))" -by (intro equalityI parts_UN_subset1 parts_UN_subset2) +lemma parts_UN [simp]: + "parts (\x\A. H x) = (\x\A. parts (H x))" + by (intro equalityI parts_UN_subset1 parts_UN_subset2) + +lemma parts_image [simp]: + "parts (f ` A) = (\x\A. parts {f x})" + apply auto + apply (metis (mono_tags, hide_lams) image_iff parts_singleton) + apply (metis empty_subsetI image_eqI insert_absorb insert_subset parts_mono) + done text\Added to simplify arguments to parts, analz and synth. NOTE: the UN versions are no longer used!\ @@ -299,10 +307,7 @@ done lemma parts_image_Key [simp]: "parts (Key`N) = Key`N" -apply auto -apply (erule parts.induct, auto) -done - +by auto text\In any message, there is an upper bound N on its greatest nonce.\ lemma msg_Nonce_supply: "\N. \n. N\n --> Nonce n \ parts {msg}" diff -r 1cf129590be8 -r 24106dc44def src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Auth/Recur.thy Wed Feb 17 21:51:56 2016 +0100 @@ -337,7 +337,7 @@ RB \ responses evs |] ==> (Key K \ parts{RB} | Key K \ analz H)" apply (erule rev_mp, erule responses.induct) -apply (simp_all del: image_insert +apply (simp_all del: image_insert parts_image add: analz_image_freshK_simps resp_analz_image_freshK_lemma) txt\Simplification using two distinct treatments of "image"\ apply (simp add: parts_insert2, blast) @@ -389,7 +389,7 @@ apply (erule respond.induct) apply (frule_tac [2] respond_imp_responses) apply (frule_tac [2] respond_imp_not_used) -apply (simp_all del: image_insert +apply (simp_all del: image_insert parts_image add: analz_image_freshK_simps split_ifs shrK_in_analz_respond resp_analz_image_freshK parts_insert2) txt\Base case of respond\ diff -r 1cf129590be8 -r 24106dc44def src/HOL/Auth/Smartcard/ShoupRubin.thy --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Wed Feb 17 21:51:56 2016 +0100 @@ -809,9 +809,9 @@ (*Because initState contains a set of nonces, this is needed for base case of analz_image_freshK*) -lemma analz_image_Key_Un_Nonce: "analz (Key`K \ Nonce`N) = Key`K \ Nonce`N" -apply auto -done +lemma analz_image_Key_Un_Nonce: + "analz (Key ` K \ Nonce ` N) = Key ` K \ Nonce ` N" + by (auto simp del: parts_image) method_setup sc_analz_freshK = \ Scan.succeed (fn ctxt => diff -r 1cf129590be8 -r 24106dc44def src/HOL/Auth/Smartcard/ShoupRubinBella.thy --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Wed Feb 17 21:51:56 2016 +0100 @@ -819,9 +819,9 @@ (*Because initState contains a set of nonces, this is needed for base case of analz_image_freshK*) -lemma analz_image_Key_Un_Nonce: "analz (Key`K \ Nonce`N) = Key`K \ Nonce`N" -apply auto -done +lemma analz_image_Key_Un_Nonce: + "analz (Key ` K \ Nonce ` N) = Key ` K \ Nonce ` N" + by (auto simp del: parts_image) method_setup sc_analz_freshK = \ Scan.succeed (fn ctxt => diff -r 1cf129590be8 -r 24106dc44def src/HOL/Auth/Smartcard/Smartcard.thy --- a/src/HOL/Auth/Smartcard/Smartcard.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy Wed Feb 17 21:51:56 2016 +0100 @@ -115,10 +115,7 @@ text\Added to extend initstate with set of nonces\ lemma parts_image_Nonce [simp]: "parts (Nonce`N) = Nonce`N" -apply auto -apply (erule parts.induct) -apply auto -done + by auto lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" apply (unfold keysFor_def) diff -r 1cf129590be8 -r 24106dc44def src/HOL/BNF_Cardinal_Order_Relation.thy --- a/src/HOL/BNF_Cardinal_Order_Relation.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Wed Feb 17 21:51:56 2016 +0100 @@ -711,7 +711,7 @@ lemma card_of_UNION_Sigma: "|\i \ I. A i| \o |SIGMA i : I. A i|" -using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by blast +using Ex_inj_on_UNION_Sigma [of A I] card_of_ordLeq by blast lemma card_of_bool: assumes "a1 \ a2" diff -r 1cf129590be8 -r 24106dc44def src/HOL/Cardinals/Wellorder_Relation.thy --- a/src/HOL/Cardinals/Wellorder_Relation.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Cardinals/Wellorder_Relation.thy Wed Feb 17 21:51:56 2016 +0100 @@ -450,8 +450,7 @@ lemma ofilter_under_Union: "ofilter A \ A = \{under a| a. a \ A}" -using ofilter_under_UNION[of A] -by(unfold Union_eq, auto) +using ofilter_under_UNION [of A] by auto subsubsection {* Other properties *} diff -r 1cf129590be8 -r 24106dc44def src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Complete_Lattices.thy Wed Feb 17 21:51:56 2016 +0100 @@ -17,28 +17,25 @@ fixes Inf :: "'a set \ 'a" ("\_" [900] 900) begin -definition INFIMUM :: "'b set \ ('b \ 'a) \ 'a" where - INF_def: "INFIMUM A f = \(f ` A)" - -lemma Inf_image_eq [simp]: - "\(f ` A) = INFIMUM A f" - by (simp add: INF_def) +abbreviation INFIMUM :: "'b set \ ('b \ 'a) \ 'a" +where + "INFIMUM A f \ \(f ` A)" lemma INF_image [simp]: "INFIMUM (f ` A) g = INFIMUM A (g \ f)" - by (simp only: INF_def image_comp) + by (simp add: image_comp) lemma INF_identity_eq [simp]: "INFIMUM A (\x. x) = \A" - by (simp add: INF_def) + by simp lemma INF_id_eq [simp]: "INFIMUM A id = \A" - by (simp add: id_def) + by simp lemma INF_cong: "A = B \ (\x. x \ B \ C x = D x) \ INFIMUM A C = INFIMUM B D" - by (simp add: INF_def image_def) + by (simp add: image_def) lemma strong_INF_cong [cong]: "A = B \ (\x. x \ B =simp=> C x = D x) \ INFIMUM A C = INFIMUM B D" @@ -50,20 +47,17 @@ fixes Sup :: "'a set \ 'a" ("\_" [900] 900) begin -definition SUPREMUM :: "'b set \ ('b \ 'a) \ 'a" where - SUP_def: "SUPREMUM A f = \(f ` A)" - -lemma Sup_image_eq [simp]: - "\(f ` A) = SUPREMUM A f" - by (simp add: SUP_def) +abbreviation SUPREMUM :: "'b set \ ('b \ 'a) \ 'a" +where + "SUPREMUM A f \ \(f ` A)" lemma SUP_image [simp]: "SUPREMUM (f ` A) g = SUPREMUM A (g \ f)" - by (simp only: SUP_def image_comp) + by (simp add: image_comp) lemma SUP_identity_eq [simp]: "SUPREMUM A (\x. x) = \A" - by (simp add: SUP_def) + by simp lemma SUP_id_eq [simp]: "SUPREMUM A id = \A" @@ -71,7 +65,7 @@ lemma SUP_cong: "A = B \ (\x. x \ B \ C x = D x) \ SUPREMUM A C = SUPREMUM B D" - by (simp add: SUP_def image_def) + by (simp add: image_def) lemma strong_SUP_cong [cong]: "A = B \ (\x. x \ B =simp=> C x = D x) \ SUPREMUM A C = SUPREMUM B D" @@ -153,14 +147,6 @@ context complete_lattice begin -lemma INF_foundation_dual: - "Sup.SUPREMUM Inf = INFIMUM" - by (simp add: fun_eq_iff Sup.SUP_def) - -lemma SUP_foundation_dual: - "Inf.INFIMUM Sup = SUPREMUM" - 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" by (blast intro: antisym Sup_least Sup_upper) @@ -217,19 +203,19 @@ by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower) lemma INF_insert [simp]: "(\x\insert a A. f x) = f a \ INFIMUM A f" - unfolding INF_def Inf_insert by simp + by (simp cong del: strong_INF_cong) 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 [simp]: "(\x\insert a A. f x) = f a \ SUPREMUM A f" - unfolding SUP_def Sup_insert by simp + by (simp cong del: strong_SUP_cong) lemma INF_empty [simp]: "(\x\{}. f x) = \" - by (simp add: INF_def) + by (simp cong del: strong_INF_cong) lemma SUP_empty [simp]: "(\x\{}. f x) = \" - by (simp add: SUP_def) + by (simp cong del: strong_SUP_cong) lemma Inf_UNIV [simp]: "\UNIV = \" @@ -308,18 +294,18 @@ ultimately show ?thesis by (rule Sup_upper2) qed +lemma INF_eq: + assumes "\i. i \ A \ \j\B. f i \ g j" + assumes "\j. j \ B \ \i\A. g j \ f i" + shows "INFIMUM A f = INFIMUM B g" + by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+ + lemma SUP_eq: assumes "\i. i \ A \ \j\B. f i \ g j" assumes "\j. j \ B \ \i\A. g j \ f i" - shows "(\i\A. f i) = (\j\B. g j)" + shows "SUPREMUM A f = SUPREMUM B g" by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+ -lemma INF_eq: - assumes "\i. i \ A \ \j\B. f i \ g j" - assumes "\j. j \ B \ \i\A. g j \ f i" - 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)" by (auto intro: Inf_greatest Inf_lower) @@ -498,24 +484,24 @@ lemma sup_INF: "a \ (\b\B. f b) = (\b\B. a \ f b)" - by (simp only: INF_def sup_Inf image_image) + unfolding sup_Inf by simp lemma inf_SUP: "a \ (\b\B. f b) = (\b\B. a \ f b)" - by (simp only: SUP_def inf_Sup image_image) + unfolding inf_Sup by simp lemma dual_complete_distrib_lattice: "class.complete_distrib_lattice Sup Inf sup (op \) (op >) inf \ \" apply (rule class.complete_distrib_lattice.intro) apply (fact dual_complete_lattice) apply (rule class.complete_distrib_lattice_axioms.intro) - apply (simp_all only: INF_foundation_dual SUP_foundation_dual inf_Sup sup_Inf) + apply (simp_all add: inf_Sup sup_Inf) done subclass distrib_lattice proof fix a b c from sup_Inf have "a \ \{b, c} = (\d\{b, c}. a \ d)" . - then show "a \ b \ c = (a \ b) \ (a \ c)" by (simp add: INF_def) + then show "a \ b \ c = (a \ b) \ (a \ c)" by simp qed lemma Inf_sup: @@ -592,7 +578,7 @@ qed lemma uminus_INF: "- (\x\A. B x) = (\x\A. - B x)" - by (simp only: INF_def SUP_def uminus_Inf image_image) + by (simp add: uminus_Inf image_image) lemma uminus_Sup: "- (\A) = \(uminus ` A)" @@ -602,7 +588,7 @@ qed lemma uminus_SUP: "- (\x\A. B x) = (\x\A. - B x)" - by (simp only: INF_def SUP_def uminus_Sup image_image) + by (simp add: uminus_Sup image_image) end @@ -731,11 +717,11 @@ lemma INF_bool_eq [simp]: "INFIMUM = Ball" - by (simp add: fun_eq_iff INF_def) + by (simp add: fun_eq_iff) lemma SUP_bool_eq [simp]: "SUPREMUM = Bex" - by (simp add: fun_eq_iff SUP_def) + by (simp add: fun_eq_iff) instance bool :: complete_boolean_algebra proof qed (auto intro: bool_induct) @@ -788,8 +774,7 @@ 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 fun_eq_iff image_image - simp del: Inf_image_eq Sup_image_eq) +qed (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image) instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra .. @@ -903,7 +888,7 @@ instance "set" :: (type) complete_boolean_algebra proof -qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def) +qed (auto simp add: Inf_set_def Sup_set_def image_def) subsubsection \Inter\ @@ -1011,22 +996,18 @@ "(\x\A. B x) = {y. \x\A. y \ B x}" by (auto intro!: INF_eqI) -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)" 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) + by auto lemma INT_D [elim, Pure.elim]: "b \ (\x\A. B x) \ a \ A \ b \ B a" by auto lemma INT_E [elim]: "b \ (\x\A. B x) \ (b \ B a \ R) \ (a \ A \ R) \ R" \ \"Classical" elimination -- by the Excluded Middle on @{prop "a\A"}.\ - by (auto simp add: INF_def image_def) + by auto lemma Collect_ball_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})" by blast @@ -1198,10 +1179,6 @@ "x \ Set.bind P f \ x \ UNION P f " by (simp add: bind_UNION) -lemma Union_image_eq: - "\(B ` A) = (\x\A. B x)" - by (fact Sup_image_eq) - lemma Union_SetCompr_eq: "\{f x| x. P x} = {a. \x. P x \ a \ f x}" by blast @@ -1214,10 +1191,7 @@ by auto lemma UN_E [elim!]: "b \ (\x\A. B x) \ (\x. x\A \ b \ B x \ R) \ R" - by (auto simp add: SUP_def image_def) - -lemma image_eq_UN: "f ` A = (\x\A. {f x})" - by blast + by auto lemma UN_upper: "a \ A \ B a \ (\x\A. B x)" by (fact SUP_upper) @@ -1273,7 +1247,7 @@ by blast lemma Un_eq_UN: "A \ B = (\b. if b then A else B)" - by (auto simp add: split_if_mem2) + by safe (auto simp add: split_if_mem2) lemma UN_bool_eq: "(\b. A b) = (A True \ A False)" by (fact SUP_UNIV_bool_expand) @@ -1355,7 +1329,7 @@ lemma inj_on_INTER: "I \ {} \ (\i. i \ I \ inj_on f (A i)) \ inj_on f (\i \ I. A i)" - unfolding inj_on_def by blast + unfolding inj_on_def by safe simp lemma inj_on_UNION_chain: assumes CH: "\ i j. \i \ I; j \ I\ \ A i \ A j \ A j \ A i" and @@ -1414,20 +1388,19 @@ lemma image_INT: "[| inj_on f C; ALL x:A. B x <= C; j:A |] ==> f ` (INTER A B) = (INT x:A. f ` B x)" -apply (simp add: inj_on_def, blast) -done + by (simp add: inj_on_def, auto) blast -(*Compare with image_INT: no use of inj_on, and if f is surjective then - it doesn't matter whether A is empty*) lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)" -apply (simp add: bij_def) -apply (simp add: inj_on_def surj_def, blast) -done + apply (simp add: bij_def) + apply (simp add: inj_on_def surj_def) + apply auto + apply blast + done lemma UNION_fun_upd: - "UNION J (A(i:=B)) = (UNION (J-{i}) A \ (if i\J then B else {}))" -by (auto split: if_splits) - + "UNION J (A(i := B)) = UNION (J - {i}) A \ (if i \ J then B else {})" + by (auto simp add: set_eq_iff) + subsubsection \Complement\ diff -r 1cf129590be8 -r 24106dc44def src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Wed Feb 17 21:51:56 2016 +0100 @@ -321,10 +321,10 @@ by (metis cSUP_upper le_less_trans) lemma cINF_insert: "A \ {} \ bdd_below (f ` A) \ INFIMUM (insert a A) f = inf (f a) (INFIMUM A f)" - by (metis cInf_insert Inf_image_eq image_insert image_is_empty) + by (metis cInf_insert image_insert image_is_empty) lemma cSUP_insert: "A \ {} \ bdd_above (f ` A) \ SUPREMUM (insert a A) f = sup (f a) (SUPREMUM A f)" - by (metis cSup_insert Sup_image_eq image_insert image_is_empty) + by (metis cSup_insert image_insert image_is_empty) lemma cINF_mono: "B \ {} \ bdd_below (f ` A) \ (\m. m \ B \ \n\A. f n \ g m) \ INFIMUM A f \ INFIMUM B g" using cInf_mono [of "g ` B" "f ` A"] by auto diff -r 1cf129590be8 -r 24106dc44def src/HOL/Enum.thy --- a/src/HOL/Enum.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Enum.thy Wed Feb 17 21:51:56 2016 +0100 @@ -556,7 +556,7 @@ end instance finite_1 :: complete_distrib_lattice -by intro_classes(simp_all add: INF_def SUP_def) + by standard simp_all instance finite_1 :: complete_linorder .. @@ -679,7 +679,7 @@ end instance finite_2 :: complete_distrib_lattice -by(intro_classes)(auto simp add: INF_def SUP_def sup_finite_2_def inf_finite_2_def Inf_finite_2_def Sup_finite_2_def) + by standard (auto simp add: sup_finite_2_def inf_finite_2_def Inf_finite_2_def Sup_finite_2_def) instance finite_2 :: complete_linorder .. @@ -797,11 +797,11 @@ then have "\x. x \ B \ x = a\<^sub>3" by(case_tac x)(auto simp add: Inf_finite_3_def split: split_if_asm) then show ?thesis using a\<^sub>2_a\<^sub>3 - by(auto simp add: INF_def Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: split_if_asm) - qed(auto simp add: INF_def Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: split_if_asm) + by(auto simp add: Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: split_if_asm) + qed (auto simp add: Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: split_if_asm) show "a \ \B = (\b\B. a \ b)" - by(cases a "\B" rule: finite_3.exhaust[case_product finite_3.exhaust]) - (auto simp add: SUP_def Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: split_if_asm) + by (cases a "\B" rule: finite_3.exhaust[case_product finite_3.exhaust]) + (auto simp add: Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: split_if_asm) qed instance finite_3 :: complete_linorder .. @@ -920,10 +920,10 @@ fix a :: finite_4 and B show "a \ \B = (\b\B. a \ b)" by(cases a "\B" rule: finite_4.exhaust[case_product finite_4.exhaust]) - (auto simp add: sup_finite_4_def Inf_finite_4_def INF_def split: finite_4.splits split_if_asm) + (auto simp add: sup_finite_4_def Inf_finite_4_def split: finite_4.splits split_if_asm) show "a \ \B = (\b\B. a \ b)" by(cases a "\B" rule: finite_4.exhaust[case_product finite_4.exhaust]) - (auto simp add: inf_finite_4_def Sup_finite_4_def SUP_def split: finite_4.splits split_if_asm) + (auto simp add: inf_finite_4_def Sup_finite_4_def split: finite_4.splits split_if_asm) qed instantiation finite_4 :: complete_boolean_algebra begin diff -r 1cf129590be8 -r 24106dc44def src/HOL/Filter.thy --- a/src/HOL/Filter.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Filter.thy Wed Feb 17 21:51:56 2016 +0100 @@ -437,8 +437,8 @@ qed lemma eventually_INF: "eventually P (INF b:B. F b) \ (\X\B. finite X \ eventually P (INF b:X. F b))" - unfolding INF_def[of B] eventually_Inf[of P "F`B"] - by (metis Inf_image_eq finite_imageI image_mono finite_subset_image) + unfolding eventually_Inf [of P "F`B"] + by (metis finite_imageI image_mono finite_subset_image) lemma Inf_filter_not_bot: fixes B :: "'a filter set" @@ -449,7 +449,7 @@ lemma INF_filter_not_bot: fixes F :: "'i \ 'a filter" shows "(\X. X \ B \ finite X \ (INF b:X. F b) \ bot) \ (INF b:B. F b) \ bot" - unfolding trivial_limit_def eventually_INF[of _ B] + unfolding trivial_limit_def eventually_INF [of _ _ B] bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp lemma eventually_Inf_base: @@ -477,7 +477,7 @@ lemma eventually_INF_base: "B \ {} \ (\a b. a \ B \ b \ B \ \x\B. F x \ inf (F a) (F b)) \ eventually P (INF b:B. F b) \ (\b\B. eventually P (F b))" - unfolding INF_def by (subst eventually_Inf_base) auto + by (subst eventually_Inf_base) auto subsubsection \Map function for filters\ @@ -573,7 +573,7 @@ by (auto intro: exI[of _ "\x. x \ A"] exI[of _ "\x. x \ B"]) lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\i\I. A i)" - unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal) + unfolding filter_eq_iff eventually_Sup by (auto simp: eventually_principal) lemma INF_principal_finite: "finite X \ (INF x:X. principal (f x)) = principal (\x\X. f x)" by (induct X rule: finite_induct) auto diff -r 1cf129590be8 -r 24106dc44def src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/GCD.thy Wed Feb 17 21:51:56 2016 +0100 @@ -1990,6 +1990,8 @@ definition "Gcd (M::nat set) = Lcm {d. \m\M. d dvd m}" +interpretation bla: semilattice_neutr_set gcd "0::nat" .. + instance .. end @@ -2012,19 +2014,7 @@ interpretation gcd_lcm_complete_lattice_nat: complete_lattice Gcd Lcm gcd Rings.dvd "\m n. m dvd n \ \ n dvd m" lcm 1 "0::nat" -rewrites "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)" - and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" -proof - - show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\m n. m dvd n \ \ n dvd m) lcm 1 (0::nat)" - by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite) - then interpret gcd_lcm_complete_lattice_nat: - complete_lattice Gcd Lcm gcd Rings.dvd "\m n. m dvd n \ \ n dvd m" lcm 1 "0::nat" . - from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" . - from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPREMUM 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] + by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite) lemma Lcm_empty_nat: "Lcm {} = (1::nat)" diff -r 1cf129590be8 -r 24106dc44def src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Hilbert_Choice.thy Wed Feb 17 21:51:56 2016 +0100 @@ -253,10 +253,10 @@ done lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A" -by (simp add: image_eq_UN surj_f_inv_f) + by (simp add: surj_f_inv_f image_comp comp_def) lemma image_inv_f_f: "inj f ==> inv f ` (f ` A) = A" - by (simp add: image_eq_UN) + by simp lemma inv_image_comp: "inj f ==> inv f ` (f ` X) = X" by (fact image_inv_f_f) diff -r 1cf129590be8 -r 24106dc44def src/HOL/Hoare_Parallel/OG_Hoare.thy --- a/src/HOL/Hoare_Parallel/OG_Hoare.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Wed Feb 17 21:51:56 2016 +0100 @@ -111,7 +111,8 @@ apply(rule conjI) apply (blast dest: L3_5i) apply(simp add: SEM_def sem_def id_def) -apply (blast dest: Basic_ntran rtrancl_imp_UN_relpow) +apply (auto dest: Basic_ntran rtrancl_imp_UN_relpow) +apply blast done lemma atom_hoare_sound [rule_format]: diff -r 1cf129590be8 -r 24106dc44def src/HOL/Hoare_Parallel/RG_Hoare.thy --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Feb 17 21:51:56 2016 +0100 @@ -1266,23 +1266,23 @@ apply simp apply clarify apply(subgoal_tac "\iassum(Pre(xs!i), Rely(xs!i))") - apply(erule_tac x=i and P="\i. H i \ \ (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption) + apply(erule_tac x=xa and P="\i. H i \ \ (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption) apply(simp add:com_validity_def) apply(erule_tac x=s in allE) - apply(erule_tac x=i and P="\j. H j \ (I j) \ cp (J j) s" for H I J in allE,simp) - apply(drule_tac c="clist!i" in subsetD) + apply(erule_tac x=xa and P="\j. H j \ (I j) \ cp (J j) s" for H I J in allE,simp) + apply(drule_tac c="clist!xa" in subsetD) apply (force simp add:Com_def) apply(simp add:comm_def conjoin_def same_program_def del:last.simps) apply clarify apply(erule_tac x="length x - 1" and P="\j. H j \ fst(I j)=(J j)" for H I J in allE) apply (simp add:All_None_def same_length_def) - apply(erule_tac x=i and P="\j. H j \ length(J j)=(K j)" for H J K in allE) + apply(erule_tac x=xa and P="\j. H j \ length(J j)=(K j)" for H J K in allE) apply(subgoal_tac "length x - 1 < length x",simp) apply(case_tac "x\[]") apply(simp add: last_conv_nth) - apply(erule_tac x="clist!i" in ballE) + apply(erule_tac x="clist!xa" in ballE) apply(simp add:same_state_def) - apply(subgoal_tac "clist!i\[]") + apply(subgoal_tac "clist!xa\[]") apply(simp add: last_conv_nth) apply(case_tac x) apply (force simp add:par_cp_def) @@ -1297,19 +1297,19 @@ apply(rule conjI) apply(simp add:conjoin_def same_state_def par_cp_def) apply clarify - apply(erule_tac x=ia and P="\j. T j \ (\i. H j i \ (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp) + apply(erule_tac x=i and P="\j. T j \ (\i. H j i \ (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp) apply(erule_tac x=0 and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE) apply(case_tac x,simp+) apply (simp add:par_assum_def) apply clarify - apply(drule_tac c="snd (clist ! ia ! 0)" in subsetD) + apply(drule_tac c="snd (clist ! i ! 0)" in subsetD) apply assumption apply simp apply clarify -apply(erule_tac x=ia in all_dupE) +apply(erule_tac x=i in all_dupE) apply(rule subsetD, erule mp, assumption) apply(erule_tac pre=pre and rely=rely and x=x and s=s in three) - apply(erule_tac x=ic in allE,erule mp) + apply(erule_tac x=ib in allE,erule mp) apply simp_all apply(simp add:ParallelCom_def) apply(force simp add:Com_def) diff -r 1cf129590be8 -r 24106dc44def src/HOL/IMP/Denotational.thy --- a/src/HOL/IMP/Denotational.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/IMP/Denotational.thy Wed Feb 17 21:51:56 2016 +0100 @@ -98,6 +98,9 @@ theorem lfp_if_cont: assumes "cont f" shows "lfp f = (UN n. (f^^n) {})" (is "_ = ?U") proof + from assms mono_if_cont + have mono: "(f ^^ n) {} \ (f ^^ Suc n) {}" for n + using funpow_decreasing [of n "Suc n"] by auto show "lfp f \ ?U" proof (rule lfp_lowerbound) have "f ?U = (UN n. (f^^Suc n){})" @@ -105,7 +108,7 @@ by(simp add: cont_def) also have "\ = (f^^0){} \ \" by simp also have "\ = ?U" - using assms funpow_decreasing le_SucI mono_if_cont by blast + using mono by auto (metis funpow_simps_right(2) funpow_swap1 o_apply) finally show "f ?U \ ?U" by simp qed next diff -r 1cf129590be8 -r 24106dc44def src/HOL/Library/Countable_Set_Type.thy --- a/src/HOL/Library/Countable_Set_Type.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Library/Countable_Set_Type.thy Wed Feb 17 21:51:56 2016 +0100 @@ -123,7 +123,11 @@ lemma cUnion_transfer [transfer_rule]: "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) Union cUnion" -unfolding cUnion_def[abs_def] Union_conv_UNION[abs_def] by transfer_prover +proof - + have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\A. UNION A id) (\A. cUNION A id)" + by transfer_prover + then show ?thesis by (simp add: cUnion_def [symmetric]) +qed lemmas cset_eqI = set_eqI[Transfer.transferred] lemmas cset_eq_iff[no_atp] = set_eq_iff[Transfer.transferred] @@ -342,11 +346,9 @@ lemmas cin_mono = in_mono[Transfer.transferred] lemmas cLeast_mono = Least_mono[Transfer.transferred] lemmas cequalityI = equalityI[Transfer.transferred] -lemmas cUnion_cimage_eq [simp] = Union_image_eq[Transfer.transferred] lemmas cUN_iff [simp] = UN_iff[Transfer.transferred] lemmas cUN_I [intro] = UN_I[Transfer.transferred] lemmas cUN_E [elim!] = UN_E[Transfer.transferred] -lemmas cimage_eq_cUN = image_eq_UN[Transfer.transferred] lemmas cUN_upper = UN_upper[Transfer.transferred] lemmas cUN_least = UN_least[Transfer.transferred] lemmas cUN_cinsert_distrib = UN_insert_distrib[Transfer.transferred] diff -r 1cf129590be8 -r 24106dc44def src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Library/Extended_Real.thy Wed Feb 17 21:51:56 2016 +0100 @@ -2002,12 +2002,11 @@ proof cases assume "(SUP i:I. f i) = - \" moreover then have "\i. i \ I \ f i = -\" - unfolding Sup_eq_MInfty Sup_image_eq[symmetric] by auto + unfolding Sup_eq_MInfty by auto ultimately show ?thesis by (cases c) (auto simp: \I \ {}\) next assume "(SUP i:I. f i) \ - \" then show ?thesis - unfolding Sup_image_eq[symmetric] by (subst continuous_at_Sup_mono[where f="\x. x + c"]) (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def ereal_add_mono \I \ {}\ \c \ -\\) qed @@ -2130,7 +2129,6 @@ by simp next assume "(SUP i:I. f i) \ 0" then show ?thesis - unfolding SUP_def by (subst continuous_at_Sup_mono[where f="\x. c * x"]) (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \I \ {}\ intro!: ereal_mult_left_mono c) diff -r 1cf129590be8 -r 24106dc44def src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Library/FSet.thy Wed Feb 17 21:51:56 2016 +0100 @@ -147,7 +147,7 @@ parametric right_total_Compl_transfer Compl_transfer by simp instance - by (standard, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+ + by (standard; transfer) (simp_all add: Diff_eq) end diff -r 1cf129590be8 -r 24106dc44def src/HOL/Library/Finite_Lattice.thy --- a/src/HOL/Library/Finite_Lattice.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Library/Finite_Lattice.thy Wed Feb 17 21:51:56 2016 +0100 @@ -116,12 +116,12 @@ lemma finite_Inf_prod: "Inf(A :: ('a::finite_lattice_complete \ 'b::finite_lattice_complete) set) = Finite_Set.fold inf top A" - by (metis Inf_fold_inf finite_code) + by (metis Inf_fold_inf finite) lemma finite_Sup_prod: "Sup (A :: ('a::finite_lattice_complete \ 'b::finite_lattice_complete) set) = Finite_Set.fold sup bot A" - by (metis Sup_fold_sup finite_code) + by (metis Sup_fold_sup finite) instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete by standard (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod) @@ -130,20 +130,20 @@ already form a finite lattice.\ lemma finite_bot_fun: "(bot :: ('a::finite \ 'b::finite_lattice_complete)) = Inf_fin UNIV" - by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code) + by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite) lemma finite_top_fun: "(top :: ('a::finite \ 'b::finite_lattice_complete)) = Sup_fin UNIV" - by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code) + by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite) lemma finite_Inf_fun: "Inf (A::('a::finite \ 'b::finite_lattice_complete) set) = Finite_Set.fold inf top A" - by (metis Inf_fold_inf finite_code) + by (metis Inf_fold_inf finite) lemma finite_Sup_fun: "Sup (A::('a::finite \ 'b::finite_lattice_complete) set) = Finite_Set.fold sup bot A" - by (metis Sup_fold_sup finite_code) + by (metis Sup_fold_sup finite) instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete by standard (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun) @@ -165,11 +165,7 @@ lemma finite_distrib_lattice_complete_inf_Sup: "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)" - apply (rule finite_induct) - apply (metis finite_code) - apply (metis SUP_empty Sup_empty inf_bot_right) - apply (metis SUP_insert Sup_insert inf_sup_distrib1) - done + using finite [of A] by induct (simp_all add: inf_sup_distrib1) instance finite_distrib_lattice_complete \ complete_distrib_lattice proof diff -r 1cf129590be8 -r 24106dc44def src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Library/Formal_Power_Series.thy Wed Feb 17 21:51:56 2016 +0100 @@ -3181,7 +3181,7 @@ let ?KM = "{(k,m). k + m \ n}" let ?f = "\s. UNION {(0::nat)..s} (\i. {(i,s - i)})" have th0: "?KM = UNION {0..n} ?f" - by (auto simp add: set_eq_iff Bex_def) + by auto show "?l = ?r " unfolding th0 apply (subst setsum.UNION_disjoint) diff -r 1cf129590be8 -r 24106dc44def src/HOL/Library/Liminf_Limsup.thy --- a/src/HOL/Library/Liminf_Limsup.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Library/Liminf_Limsup.thy Wed Feb 17 21:51:56 2016 +0100 @@ -380,7 +380,7 @@ note * = this have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))" - unfolding Liminf_def SUP_def + unfolding Liminf_def by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]]) (auto intro: eventually_True) also have "\ = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)" @@ -405,7 +405,7 @@ note * = this have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))" - unfolding Limsup_def INF_def + unfolding Limsup_def by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]]) (auto intro: eventually_True) also have "\ = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)" @@ -429,7 +429,7 @@ by auto qed have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))" - unfolding Limsup_def INF_def + unfolding Limsup_def by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]]) (auto intro: eventually_True) also have "\ = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)" @@ -455,7 +455,7 @@ note * = this have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))" - unfolding Liminf_def SUP_def + unfolding Liminf_def by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) (auto intro: eventually_True) also have "\ = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)" diff -r 1cf129590be8 -r 24106dc44def src/HOL/Library/Lub_Glb.thy --- a/src/HOL/Library/Lub_Glb.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Library/Lub_Glb.thy Wed Feb 17 21:51:56 2016 +0100 @@ -230,7 +230,7 @@ by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle) also have "(SUP i. X i) = u" using isLub_cSup[of "range X"] u[THEN isLubD1] - by (intro isLub_unique[OF _ u]) (auto simp add: SUP_def image_def eq_commute) + by (intro isLub_unique[OF _ u]) (auto simp add: image_def eq_commute) finally show ?thesis . qed diff -r 1cf129590be8 -r 24106dc44def src/HOL/Library/Option_ord.thy --- a/src/HOL/Library/Option_ord.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Library/Option_ord.thy Wed Feb 17 21:51:56 2016 +0100 @@ -289,7 +289,7 @@ show "a \ \B = (\b\B. a \ b)" proof (cases a) case None - then show ?thesis by (simp add: INF_def) + then show ?thesis by simp next case (Some c) show ?thesis @@ -303,13 +303,13 @@ 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 comp_def) - with Some B show ?thesis by (simp add: Some_image_these_eq) + with Some B show ?thesis by (simp add: Some_image_these_eq cong del: strong_INF_cong) qed qed show "a \ \B = (\b\B. a \ b)" proof (cases a) case None - then show ?thesis by (simp add: SUP_def image_constant_conv bot_option_def) + then show ?thesis by (simp add: image_constant_conv bot_option_def cong del: strong_SUP_cong) next case (Some c) show ?thesis @@ -332,7 +332,7 @@ ultimately have "Some c \ \(Some ` Option.these B) = (\x\Some ` Option.these B. Some c \ x)" 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) + by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib cong del: strong_SUP_cong) qed qed qed diff -r 1cf129590be8 -r 24106dc44def src/HOL/Library/Product_Order.thy --- a/src/HOL/Library/Product_Order.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Library/Product_Order.thy Wed Feb 17 21:51:56 2016 +0100 @@ -179,7 +179,6 @@ instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice) conditionally_complete_lattice by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def - 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 @@ -211,10 +210,10 @@ 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)" - unfolding SUP_def Sup_prod_def by (simp add: comp_def) + unfolding 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)" - unfolding INF_def Inf_prod_def by (simp add: comp_def) + unfolding Inf_prod_def by (simp add: comp_def) text \Alternative formulations for set infima and suprema over the product @@ -222,11 +221,11 @@ lemma INF_prod_alt_def: "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))" - unfolding INF_def Inf_prod_def by simp + unfolding Inf_prod_def by simp lemma SUP_prod_alt_def: "SUPREMUM A f = (SUPREMUM A (fst o f), SUPREMUM A (snd o f))" - unfolding SUP_def Sup_prod_def by simp + unfolding Sup_prod_def by simp subsection \Complete distributive lattices\ diff -r 1cf129590be8 -r 24106dc44def src/HOL/Lifting_Set.thy --- a/src/HOL/Lifting_Set.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Lifting_Set.thy Wed Feb 17 21:51:56 2016 +0100 @@ -138,7 +138,7 @@ lemma UNION_transfer [transfer_rule]: "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION" - unfolding Union_image_eq [symmetric, abs_def] by transfer_prover + by transfer_prover lemma Ball_transfer [transfer_rule]: "(rel_set A ===> (A ===> op =) ===> op =) Ball Ball" @@ -176,11 +176,11 @@ lemma INF_parametric [transfer_rule]: "(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) INFIMUM INFIMUM" - unfolding INF_def [abs_def] by transfer_prover + by transfer_prover lemma SUP_parametric [transfer_rule]: "(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) SUPREMUM SUPREMUM" - unfolding SUP_def [abs_def] by transfer_prover + by transfer_prover subsubsection \Rules requiring bi-unique, bi-total or right-total relations\ diff -r 1cf129590be8 -r 24106dc44def src/HOL/List.thy --- a/src/HOL/List.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/List.thy Wed Feb 17 21:51:56 2016 +0100 @@ -6774,7 +6774,7 @@ lemma set_relcomp [code]: "set xys O set yzs = set ([(fst xy, snd yz). xy \ xys, yz \ yzs, snd xy = fst yz])" - by (auto simp add: Bex_def) + by auto (auto simp add: Bex_def image_def) lemma wf_set [code]: "wf (set xs) = acyclic (set xs)" diff -r 1cf129590be8 -r 24106dc44def src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Wed Feb 17 21:51:56 2016 +0100 @@ -116,7 +116,7 @@ also assume "dist f g = 0" finally show "f = g" by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse) - qed (auto simp: dist_bcontfun_def SUP_def simp del: Sup_image_eq intro!: cSup_eq) + qed (auto simp: dist_bcontfun_def intro!: cSup_eq) show "dist f g \ dist f h + dist g h" proof (subst dist_bcontfun_def, safe intro!: cSUP_least) fix x @@ -374,7 +374,7 @@ ultimately show "norm (a *\<^sub>R f) = \a\ * norm f" by (simp add: norm_bcontfun_def dist_bcontfun_def norm_conv_dist Abs_bcontfun_inverse - zero_bcontfun_def const_bcontfun SUP_def del: Sup_image_eq) + zero_bcontfun_def const_bcontfun image_image) presburger qed qed (auto simp: norm_bcontfun_def sgn_bcontfun_def) diff -r 1cf129590be8 -r 24106dc44def src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Feb 17 21:51:56 2016 +0100 @@ -6690,7 +6690,7 @@ using \open s\ apply (simp add: open_contains_ball Ball_def) apply (erule all_forward) - using "*" by blast + using "*" by auto blast+ have 2: "closedin (subtopology euclidean s) (\n. {w \ s. (deriv ^^ n) f w = 0})" using assms by (auto intro: continuous_closed_in_preimage_constant holomorphic_on_imp_continuous_on holomorphic_higher_deriv) diff -r 1cf129590be8 -r 24106dc44def src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Feb 17 21:51:56 2016 +0100 @@ -421,13 +421,13 @@ lemma interval_upperbound[simp]: "\i\Basis. a\i \ b\i \ interval_upperbound (cbox a b) = (b::'a::euclidean_space)" - unfolding interval_upperbound_def euclidean_representation_setsum cbox_def SUP_def + unfolding interval_upperbound_def euclidean_representation_setsum cbox_def by (safe intro!: cSup_eq) auto lemma interval_lowerbound[simp]: "\i\Basis. a\i \ b\i \ interval_lowerbound (cbox a b) = (a::'a::euclidean_space)" - unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def INF_def + unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def by (safe intro!: cInf_eq) auto lemmas interval_bounds = interval_upperbound interval_lowerbound @@ -436,7 +436,7 @@ fixes X::"real set" shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X" and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X" - by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def) + by (auto simp: interval_upperbound_def interval_lowerbound_def) lemma interval_bounds'[simp]: assumes "cbox a b \ {}" @@ -496,7 +496,7 @@ using assms box_ne_empty(1) content_cbox by blast lemma content_real: "a \ b \ content {a..b} = b - a" - by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def content_def) + by (auto simp: interval_upperbound_def interval_lowerbound_def content_def) lemma abs_eq_content: "\y - x\ = (if x\y then content {x .. y} else content {y..x})" by (auto simp: content_real) @@ -856,7 +856,7 @@ by auto show "\?A = s1 \ s2" apply (rule set_eqI) - unfolding * and Union_image_eq UN_iff + unfolding * and UN_iff using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] apply auto done @@ -9394,7 +9394,6 @@ prefer 3 apply assumption apply rule - apply (rule finite_imageI) apply (rule r) apply safe apply (drule qq) diff -r 1cf129590be8 -r 24106dc44def src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Feb 17 21:51:56 2016 +0100 @@ -2752,7 +2752,7 @@ lemma infnorm_Max: fixes x :: "'a::euclidean_space" shows "infnorm x = Max ((\i. \x \ i\) ` Basis)" - by (simp add: infnorm_def infnorm_set_image cSup_eq_Max del: Sup_image_eq) + by (simp add: infnorm_def infnorm_set_image cSup_eq_Max) lemma infnorm_set_lemma: fixes x :: "'a::euclidean_space" diff -r 1cf129590be8 -r 24106dc44def src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Wed Feb 17 21:51:56 2016 +0100 @@ -38,13 +38,11 @@ assume "X \ {}" 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 + by (auto simp: eucl_Inf eucl_Sup eucl_le 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 - simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq)+ + eucl_Inf eucl_Sup eucl_le)+ 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)" @@ -89,7 +87,7 @@ shows "Sup s = X" using assms unfolding eucl_Sup euclidean_representation_setsum - by (auto simp: Sup_class.SUP_def simp del: Sup_class.Sup_image_eq intro!: conditionally_complete_lattice_class.cSup_eq_maximum) + by (auto intro!: conditionally_complete_lattice_class.cSup_eq_maximum) lemma Inf_eq_minimum_componentwise: assumes i: "\b. b \ Basis \ X \ b = i b \ b" @@ -98,7 +96,7 @@ shows "Inf s = X" using assms unfolding eucl_Inf euclidean_representation_setsum - by (auto simp: Inf_class.INF_def simp del: Inf_class.Inf_image_eq intro!: conditionally_complete_lattice_class.cInf_eq_minimum) + by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum) end @@ -117,10 +115,9 @@ 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 simp del: Inf_class.Inf_image_eq) + by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum) 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 - simp del: Inf_class.Inf_image_eq + by (auto simp: eucl_Inf inner_setsum_left inner_Basis if_distrib \b \ Basis\ setsum.delta cong: if_cong) with x show "\x. x \ X \ x \ b = Inf X \ b \ (\y. y \ X \ x \ b \ y \ b)" by blast qed @@ -140,10 +137,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 simp del: Sup_image_eq) + by (auto intro!: cSup_eq_maximum) 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 - simp del: Sup_image_eq cong: if_cong) + by (auto simp: eucl_Sup[where 'a='a] inner_setsum_left inner_Basis if_distrib \b \ Basis\ setsum.delta + cong: if_cong) with x show "\x. x \ X \ x \ b = Sup X \ b \ (\y. y \ X \ y \ b \ x \ b)" by blast qed @@ -152,7 +149,7 @@ by (auto) instance real :: ordered_euclidean_space - by standard (auto simp: INF_def SUP_def) + by standard auto lemma in_Basis_prod_iff: fixes i::"'a::euclidean_space*'b::euclidean_space" diff -r 1cf129590be8 -r 24106dc44def src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Feb 17 21:51:56 2016 +0100 @@ -532,7 +532,6 @@ lemma closedin_INT[intro]: assumes "A \ {}" "\x. x \ A \ closedin U (B x)" shows "closedin U (\x\A. B x)" - unfolding Inter_image_eq [symmetric] apply (rule closedin_Inter) using assms apply auto @@ -605,7 +604,7 @@ ultimately have "?L (\K)" by blast } ultimately show ?thesis - unfolding subset_eq mem_Collect_eq istopology_def by blast + unfolding subset_eq mem_Collect_eq istopology_def by auto qed lemma openin_subtopology: "openin (subtopology U V) S \ (\T. openin U T \ S = T \ V)" @@ -2426,7 +2425,7 @@ fix y assume "y \ {x<..} \ I" with False bnd have "Inf (f ` ({x<..} \ I)) \ f y" - by (auto intro!: cInf_lower bdd_belowI2 simp del: Inf_image_eq) + by (auto intro!: cInf_lower bdd_belowI2) with a have "a < f y" by (blast intro: less_le_trans) } @@ -3802,7 +3801,7 @@ lemma compact_UN [intro]: "finite A \ (\x. x \ A \ compact (B x)) \ compact (\x\A. B x)" - unfolding SUP_def by (rule compact_Union) auto + by (rule compact_Union) auto lemma closed_inter_compact [intro]: assumes "closed s" @@ -4090,7 +4089,7 @@ by metis def X \ "\n. X' (from_nat_into A ` {.. n})" have X: "\n. X n \ U - (\i\n. from_nat_into A i)" - using \A \ {}\ unfolding X_def SUP_def by (intro T) (auto intro: from_nat_into) + using \A \ {}\ unfolding X_def by (intro T) (auto intro: from_nat_into) then have "range X \ U" by auto with subseq[of X] obtain r x where "x \ U" and r: "subseq r" "(X \ r) \ x" @@ -4198,7 +4197,7 @@ then have s: "\x. x \ s \ \U. x\U \ open U \ finite (U \ t)" by metis have "s \ \C" using \t \ s\ - unfolding C_def Union_image_eq + unfolding C_def apply (safe dest!: s) apply (rule_tac a="U \ t" in UN_I) apply (auto intro!: interiorI simp add: finite_subset) @@ -4211,7 +4210,7 @@ by (rule countably_compactE) then obtain E where E: "E \ {F. finite F \ F \ t }" "finite E" and s: "s \ (\F\E. interior (F \ (- t)))" - by (metis (lifting) Union_image_eq finite_subset_image C_def) + by (metis (lifting) finite_subset_image C_def) from s \t \ s\ have "t \ \E" using interior_subset by blast moreover have "finite (\E)" @@ -4348,7 +4347,7 @@ from Rats_dense_in_real[OF \0 < e / 2\] obtain r where "r \ \" "0 < r" "r < e / 2" by auto from f[rule_format, of r] \0 < r\ \x \ s\ obtain k where "k \ f r" "x \ ball k r" - unfolding Union_image_eq by auto + by auto from \r \ \\ \0 < r\ \k \ f r\ have "ball k r \ K" by (auto simp: K_def) then show "\b\K. x \ b \ b \ s \ T" @@ -7412,7 +7411,7 @@ lemma diameter_cbox: fixes a b::"'a::euclidean_space" shows "(\i \ Basis. a \ i \ b \ i) \ diameter (cbox a b) = dist a b" - by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono + by (force simp add: diameter_def intro!: cSup_eq_maximum setL2_mono simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm) lemma eucl_less_eq_halfspaces: diff -r 1cf129590be8 -r 24106dc44def src/HOL/Number_Theory/MiscAlgebra.thy --- a/src/HOL/Number_Theory/MiscAlgebra.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy Wed Feb 17 21:51:56 2016 +0100 @@ -259,7 +259,7 @@ (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |] ==> finprod G f (\C) = finprod G (finprod G f) C" apply (frule finprod_UN_disjoint [of C id f]) - apply (auto simp add: SUP_def) + apply auto done lemma (in comm_monoid) finprod_one: diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Caratheodory.thy --- a/src/HOL/Probability/Caratheodory.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Caratheodory.thy Wed Feb 17 21:51:56 2016 +0100 @@ -396,8 +396,8 @@ from \outer_measure M f X \ \\ have fin: "\outer_measure M f X\ \ \" using outer_measure_nonneg[OF posf, of X] by auto show ?thesis - using Inf_ereal_close[OF fin[unfolded outer_measure_def INF_def], OF \0 < e\] - unfolding INF_def[symmetric] outer_measure_def[symmetric] by (auto intro: less_imp_le) + using Inf_ereal_close [OF fin [unfolded outer_measure_def], OF \0 < e\] + by (auto intro: less_imp_le simp add: outer_measure_def) qed lemma (in ring_of_sets) countably_subadditive_outer_measure: @@ -574,7 +574,7 @@ shows "f (UNION I A) = (\i\I. f (A i))" proof - have "A`I \ M" "disjoint (A`I)" "finite (A`I)" "\(A`I) \ M" - using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image) + using A by (auto simp: disjoint_family_on_disjoint_image) with \volume M f\ have "f (\(A`I)) = (\a\A`I. f a)" unfolding volume_def by blast also have "\ = (\i\I. f (A i))" @@ -713,7 +713,7 @@ then have "disjoint_family F" using F'_disj by (auto simp: disjoint_family_on_def) moreover from F' have "(\i. F i) = \C" - by (auto simp: F_def set_eq_iff split: split_if_asm) + by (auto simp add: F_def split: split_if_asm) blast moreover have sets_F: "\i. F i \ M" using F' sets_C by (auto simp: F_def) moreover note sets_C @@ -783,9 +783,10 @@ by (auto simp: disjoint_family_on_def f_def) moreover have Ai_eq: "A i = (\xrange f = A i" - using f C Ai unfolding bij_betw_def by (auto simp: f_def) + using f C Ai unfolding bij_betw_def + by (auto simp add: f_def cong del: strong_SUP_cong) moreover { have "(\j. \_r (f j)) = (\j. if j \ {..< card C} then \_r (f j) else 0)" using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def) @@ -841,7 +842,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: Sup_image_eq Union_image_eq + (auto simp: disjoint_def disjoint_family_on_def 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))" @@ -853,7 +854,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: Sup_image_eq Union_image_eq + (auto simp: disjoint_family_on_def disjoint_def intro: generated_ringI_Basic) finally show "(\n. \_r (A' n)) = \_r (\i. A' i)" using C' by simp diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Complete_Measure.thy --- a/src/HOL/Probability/Complete_Measure.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Complete_Measure.thy Wed Feb 17 21:51:56 2016 +0100 @@ -205,7 +205,7 @@ unfolding binary_def by (auto split: split_if_asm) show "emeasure M (main_part M (S \ T)) = emeasure M (main_part M S \ main_part M T)" using emeasure_main_part_UN[of "binary S T" M] assms - unfolding range_binary_eq Un_range_binary UN by auto + by (simp add: range_binary_eq, simp add: Un_range_binary UN) qed (auto intro: S T) lemma sets_completionI_sub: diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Embed_Measure.thy --- a/src/HOL/Probability/Embed_Measure.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Embed_Measure.thy Wed Feb 17 21:51:56 2016 +0100 @@ -36,7 +36,8 @@ then obtain A' where "\i. A i = f ` A' i" "\i. A' i \ sets M" by (auto simp: subset_eq choice_iff) moreover from this have "(\x. f ` A' x) = f ` (\x. A' x)" by blast - ultimately show "(\i. A i) \ {f ` A |A. A \ sets M}" by blast + ultimately show "(\i. A i) \ {f ` A |A. A \ sets M}" + by simp blast qed (auto dest: sets.sets_into_space) lemma the_inv_into_vimage: diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Fin_Map.thy --- a/src/HOL/Probability/Fin_Map.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Fin_Map.thy Wed Feb 17 21:51:56 2016 +0100 @@ -696,7 +696,7 @@ have "A -` y \ space (PiF I M) = (\J\I. A -` y \ space (PiF {J} M))" by (auto simp: space_PiF) also have "\ \ sets (PiF I M)" - proof + proof (rule sets.finite_UN) show "finite I" by fact fix J assume "J \ I" with assms have "finite J" by simp @@ -1055,8 +1055,8 @@ by (intro Pi'_cong) (simp_all add: S_union) also have "\ = (\xs\{xs. length xs = card I}. \' j\I. if i = j then A else S j (xs ! T j))" using T - apply auto - apply (simp_all add: Pi'_iff bchoice_iff) + apply (auto simp del: Union_iff) + apply (simp_all add: Pi'_iff bchoice_iff del: Union_iff) apply (erule conjE exE)+ apply (rule_tac x="map (\n. f (the_inv_into I T n)) [0..k\Ka. Ea k)" "finite Ka" "Ka \ {}" "Ka \ I j" "\k. k\Ka \ Ea k \ E k" by auto fix b assume "b \ ?E j" then obtain Kb Eb where b: "b = (\k\Kb. Eb k)" "finite Kb" "Kb \ {}" "Kb \ I j" "\k. k\Kb \ Eb k \ E k" by auto - let ?A = "\k. (if k \ Ka \ Kb then Ea k \ Eb k else if k \ Kb then Eb k else if k \ Ka then Ea k else {})" - have "a \ b = INTER (Ka \ Kb) ?A" - by (simp add: a b set_eq_iff) auto + let ?f = "\k. (if k \ Ka \ Kb then Ea k \ Eb k else if k \ Kb then Eb k else if k \ Ka then Ea k else {})" + have "Ka \ Kb = (Ka \ Kb) \ (Kb - Ka) \ (Ka - Kb)" + by blast + moreover have "(\x\Ka \ Kb. Ea x \ Eb x) \ + (\x\Kb - Ka. Eb x) \ (\x\Ka - Kb. Ea x) = (\k\Ka. Ea k) \ (\k\Kb. Eb k)" + by auto + ultimately have "(\k\Ka \ Kb. ?f k) = (\k\Ka. Ea k) \ (\k\Kb. Eb k)" (is "?lhs = ?rhs") + by (simp only: image_Un Inter_Un_distrib) simp + then have "a \ b = (\k\Ka \ Kb. ?f k)" + by (simp only: a(1) b(1)) with a b \j \ J\ Int_stableD[OF Int_stable] show "a \ b \ ?E j" - by (intro CollectI exI[of _ "Ka \ Kb"] exI[of _ ?A]) auto + by (intro CollectI exI[of _ "Ka \ Kb"] exI[of _ ?f]) auto qed qed ultimately show ?thesis @@ -804,14 +811,18 @@ proof - have [measurable]: "\m. {x\space M. P m x} \ sets M" using assms by (auto simp: indep_events_def) - have "prob (\n. \m\{n..}. ?P m) = 0 \ prob (\n. \m\{n..}. ?P m) = 1" - by (rule borel_0_1_law) fact + have *: "(\n. \m\{n..}. {x \ space M. P m x}) \ events" + by simp + from assms have "prob (\n. \m\{n..}. ?P m) = 0 \ prob (\n. \m\{n..}. ?P m) = 1" + by (rule borel_0_1_law) + also have "prob (\n. \m\{n..}. ?P m) = 1 \ (AE x in M. infinite {m. P m x})" + using * by (simp add: prob_eq_1) + (simp add: Bex_def infinite_nat_iff_unbounded_le) also have "prob (\n. \m\{n..}. ?P m) = 0 \ (AE x in M. finite {m. P m x})" - by (subst prob_eq_0) (auto simp add: finite_nat_iff_bounded Ball_def not_less[symmetric]) - also have "prob (\n. \m\{n..}. ?P m) = 1 \ (AE x in M. infinite {m. P m x})" - by (subst prob_eq_1) (simp_all add: Bex_def infinite_nat_iff_unbounded_le) + using * by (simp add: prob_eq_0) + (auto simp add: Ball_def finite_nat_iff_bounded not_less [symmetric]) finally show ?thesis - by metis + by blast qed lemma (in prob_space) indep_sets_finite: diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Infinite_Product_Measure.thy --- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Feb 17 21:51:56 2016 +0100 @@ -181,7 +181,7 @@ proof - have "Pi UNIV E = (\i. emb UNIV {..i} (\\<^sub>E j\{..i}. E j))" using E E[THEN sets.sets_into_space] - by (auto simp: prod_emb_def Pi_iff extensional_def) blast + by (auto simp: prod_emb_def Pi_iff extensional_def) with E show ?thesis by auto qed @@ -194,7 +194,7 @@ using E by (simp add: measure_PiM_emb) moreover have "Pi UNIV E = (\n. ?E n)" using E E[THEN sets.sets_into_space] - by (auto simp: prod_emb_def extensional_def Pi_iff) blast + by (auto simp: prod_emb_def extensional_def Pi_iff) moreover have "range ?E \ sets S" using E by auto moreover have "decseq ?E" diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Lebesgue_Measure.thy --- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Feb 17 21:51:56 2016 +0100 @@ -536,7 +536,7 @@ moreover have "emeasure lborel (\i. {from_nat_into A i}) = 0" by (rule emeasure_UN_eq_0) auto ultimately have "emeasure lborel A \ 0" using emeasure_mono - by (metis assms bot.extremum_unique emeasure_empty image_eq_UN range_from_nat_into sets.empty_sets) + by (smt UN_E emeasure_empty equalityI from_nat_into order_refl singletonD subsetI) thus ?thesis by (auto simp add: emeasure_le_0_iff) qed diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Measurable.thy --- a/src/HOL/Probability/Measurable.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Measurable.thy Wed Feb 17 21:51:56 2016 +0100 @@ -152,7 +152,7 @@ "(\i. i \ X \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\X. N x i))" "(\i. i \ X \ pred M (\x. P x i)) \ pred M (\x. \i\X. P x i)" "(\i. i \ X \ pred M (\x. P x i)) \ pred M (\x. \i\X. P x i)" - by (auto simp: Bex_def Ball_def) + by simp_all (auto simp: Bex_def Ball_def) lemma pred_intros_finite[measurable (raw)]: "finite I \ (\i. i \ I \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\I. N x i))" diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Measure_Space.thy --- a/src/HOL/Probability/Measure_Space.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Measure_Space.thy Wed Feb 17 21:51:56 2016 +0100 @@ -884,7 +884,7 @@ have "(\i\I. N i) = \(N ` range (from_nat_into I))" using I by simp also have "\ = (\i. (N \ from_nat_into I) i)" - by (simp only: SUP_def image_comp) + by simp finally show ?thesis by simp qed @@ -1228,7 +1228,7 @@ range: "range A \ sets M" and space: "(\i. A i) = space M" and measure: "\i. emeasure M (A i) \ \" - using sigma_finite by auto + using sigma_finite by blast show thesis proof (rule that[of "disjointed A"]) show "range (disjointed A) \ sets M" @@ -1252,7 +1252,7 @@ proof - obtain F :: "nat \ 'a set" where F: "range F \ sets M" "(\i. F i) = space M" "\i. emeasure M (F i) \ \" - using sigma_finite by auto + using sigma_finite by blast show thesis proof (rule that[of "\n. \i\n. F i"]) show "range (\n. \i\n. F i) \ sets M" @@ -1731,8 +1731,10 @@ assumes upper: "space M \ (\i \ s. f i)" shows "measure M e = (\ x \ s. measure M (e \ f x))" proof - - have e: "e = (\i \ s. e \ f i)" + have "e \ (\i\s. f i)" using \e \ sets M\ sets.sets_into_space upper by blast + then have e: "e = (\i \ s. e \ f i)" + by auto hence "measure M e = measure M (\i \ s. e \ f i)" by simp also have "\ = (\ x \ s. measure M (e \ f x))" proof (rule finite_measure_finite_Union) @@ -2074,7 +2076,7 @@ using E \ by (subst (1 2) emeasure_restrict_space) (auto simp: sets_eq sets_eq[THEN sets_eq_imp_space_eq]) next show "range (from_nat_into A) \ E" "(\i. from_nat_into A i) = \" - unfolding Sup_image_eq[symmetric, where f="from_nat_into A"] using A by auto + using A by (auto cong del: strong_SUP_cong) next fix i have "emeasure (restrict_space M \) (from_nat_into A i) = emeasure M (from_nat_into A i)" @@ -2333,12 +2335,12 @@ assumes A: "Complete_Partial_Order.chain op \ (f ` A)" and a: "a \ A" "f a \ bot" shows space_SUP: "space (SUP M:A. f M) = space (f a)" and sets_SUP: "sets (SUP M:A. f M) = sets (f a)" -unfolding SUP_def by(rule space_Sup[OF A a(2) imageI[OF a(1)]] sets_Sup[OF A a(2) imageI[OF a(1)]])+ +by(rule space_Sup[OF A a(2) imageI[OF a(1)]] sets_Sup[OF A a(2) imageI[OF a(1)]])+ lemma emeasure_SUP: assumes A: "Complete_Partial_Order.chain op \ (f ` A)" "A \ {}" assumes "X \ sets (SUP M:A. f M)" shows "emeasure (SUP M:A. f M) X = (SUP M:A. emeasure (f M)) X" -using \X \ _\ unfolding SUP_def by(subst emeasure_Sup[OF A(1)]; simp add: A) +using \X \ _\ by(subst emeasure_Sup[OF A(1)]; simp add: A) end diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Feb 17 21:51:56 2016 +0100 @@ -932,7 +932,7 @@ have "a * u x < 1 * u x" 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 + finally obtain i where "a * u x < f i x" by (auto simp add: less_SUP_iff) hence "a * u x \ f i x" by auto thus ?thesis using \x \ space M\ by auto @@ -2042,7 +2042,7 @@ by (auto intro!: SUP_least SUP_upper nn_integral_mono) next have "\x. \g. incseq g \ range g \ (\i. f i x) ` Y \ (SUP i:Y. f i x) = (SUP i. g i)" - unfolding Sup_class.SUP_def by(rule Sup_countable_SUP[unfolded Sup_class.SUP_def])(simp add: nonempty) + by (rule Sup_countable_SUP) (simp add: nonempty) then obtain g where incseq: "\x. incseq (g x)" and range: "\x. range (g x) \ (\i. f i x) ` Y" and sup: "\x. (SUP i:Y. f i x) = (SUP i. g x i)" by moura @@ -2088,8 +2088,8 @@ assume "x \ {.. \ (SUP i:?Y. f i) x" unfolding SUP_def Sup_fun_def image_image - using \x \ {.. by(rule Sup_upper[OF imageI]) + also have "\ \ (SUP i:?Y. f i) x" unfolding Sup_fun_def image_image + using \x \ {.. by (rule Sup_upper [OF imageI]) also have "\ = f (I m') x" unfolding m' by simp finally show "g x n \ f (I m') x" . qed @@ -2264,7 +2264,7 @@ by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm) qed then show ?thesis - unfolding nn_integral_def_finite SUP_def by simp + unfolding nn_integral_def_finite by (simp cong del: strong_SUP_cong) qed lemma nn_integral_count_space_indicator: diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Probability_Measure.thy Wed Feb 17 21:51:56 2016 +0100 @@ -247,7 +247,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 simp del: Sup_image_eq Inf_image_eq) } + by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open) } 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 1cf129590be8 -r 24106dc44def src/HOL/Probability/Radon_Nikodym.thy --- a/src/HOL/Probability/Radon_Nikodym.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Feb 17 21:51:56 2016 +0100 @@ -51,7 +51,7 @@ space: "(\i. A i) = space M" and measure: "\i. emeasure M (A i) \ \" and disjoint: "disjoint_family A" - using sigma_finite_disjoint by auto + using sigma_finite_disjoint by blast let ?B = "\i. 2^Suc i * emeasure M (A i)" have "\i. \x. 0 < x \ x < inverse (?B i)" proof @@ -560,7 +560,7 @@ proof (rule antisym) show "?a \ (SUP i. emeasure M (?O i))" unfolding a_Lim using Q' by (auto intro!: SUP_mono emeasure_mono) - show "(SUP i. emeasure M (?O i)) \ ?a" unfolding SUP_def + show "(SUP i. emeasure M (?O i)) \ ?a" proof (safe intro!: Sup_mono, unfold bex_simps) fix i have *: "(\(Q' ` {..i})) = ?O i" by auto diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Regularity.thy --- a/src/HOL/Probability/Regularity.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Regularity.thy Wed Feb 17 21:51:56 2016 +0100 @@ -138,7 +138,8 @@ proof safe fix x from X(2)[OF open_ball[of x r]] \r > 0\ obtain d where d: "d\X" "d \ ball x r" by auto show "x \ ?U" - using X(1) d by (auto intro!: exI[where x="to_nat_on X d"] simp: dist_commute Bex_def) + using X(1) d + by simp (auto intro!: exI [where x = "to_nat_on X d"] simp: dist_commute Bex_def) qed (simp add: sU) finally have "(\k. M (\n\{0..k}. cball (from_nat_into X n) r)) \ M (space M)" . } note M_space = this @@ -319,8 +320,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, unfolded comp_def]) - (rule INF_cong, auto simp add: sU intro!: INF_cong) + unfolding INF_image [of _ "\u. space M - u" _, symmetric, unfolded comp_def] + by (rule INF_cong) (auto simp add: sU open_Compl Compl_eq_Diff_UNIV [symmetric, simp]) finally have "(INF U:{U. space M - B \ U \ open U}. emeasure M U) \ emeasure M (space M - B)" . moreover have @@ -335,8 +336,8 @@ 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, simplified comp_def]) - (rule SUP_cong, auto simp: sU) + unfolding SUP_image [of _ "\u. space M - u" _, symmetric, unfolded comp_def] + by (rule SUP_cong) (auto simp add: sU) also have "\ = (SUP K:{K. K \ space M - B \ compact K}. emeasure M K)" proof (safe intro!: antisym SUP_least) fix K assume "closed K" "K \ space M - B" diff -r 1cf129590be8 -r 24106dc44def src/HOL/Probability/Sigma_Algebra.thy --- a/src/HOL/Probability/Sigma_Algebra.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Feb 17 21:51:56 2016 +0100 @@ -432,10 +432,10 @@ by (auto simp add: binary_def) lemma Un_range_binary: "a \ b = (\i::nat. binary a b i)" - by (simp add: SUP_def range_binary_eq) + by (simp add: range_binary_eq cong del: strong_SUP_cong) lemma Int_range_binary: "a \ b = (\i::nat. binary a b i)" - by (simp add: INF_def range_binary_eq) + by (simp add: range_binary_eq cong del: strong_INF_cong) lemma sigma_algebra_iff2: "sigma_algebra \ M \ @@ -535,11 +535,14 @@ finally show ?thesis . qed -lemma sigma_sets_UNION: "countable B \ (\b. b \ B \ b \ sigma_sets X A) \ (\B) \ sigma_sets X A" - using from_nat_into[of B] range_from_nat_into[of B] sigma_sets.Union[of "from_nat_into B" X A] +lemma sigma_sets_UNION: + "countable B \ (\b. b \ B \ b \ sigma_sets X A) \ (\B) \ sigma_sets X A" apply (cases "B = {}") apply (simp add: sigma_sets.Empty) - apply (simp del: Union_image_eq add: Union_image_eq[symmetric]) + using from_nat_into [of B] range_from_nat_into [of B] sigma_sets.Union [of "from_nat_into B" X A] + apply simp + apply auto + apply (metis Sup_bot_conv(1) Union_empty `\B \ {}; countable B\ \ range (from_nat_into B) = B`) done lemma (in sigma_algebra) sigma_sets_eq: @@ -835,7 +838,7 @@ lemma (in semiring_of_sets) generated_ring_disjoint_UNION: "finite I \ disjoint (A ` I) \ (\i. i \ I \ A i \ generated_ring) \ UNION I A \ generated_ring" - unfolding SUP_def by (intro generated_ring_disjoint_Union) auto + by (intro generated_ring_disjoint_Union) auto lemma (in semiring_of_sets) generated_ring_Int: assumes a: "a \ generated_ring" and b: "b \ generated_ring" @@ -873,7 +876,7 @@ lemma (in semiring_of_sets) generated_ring_INTER: "finite I \ I \ {} \ (\i. i \ I \ A i \ generated_ring) \ INTER I A \ generated_ring" - unfolding INF_def by (intro generated_ring_Inter) auto + by (intro generated_ring_Inter) auto lemma (in semiring_of_sets) generating_ring: "ring_of_sets \ generated_ring" @@ -898,6 +901,7 @@ fix a b assume "a \ Ca" "b \ Cb" with Ca Cb Diff_cover[of a b] show "a - b \ ?R" by (auto simp add: generated_ring_def) + (metis DiffI Diff_eq_empty_iff empty_iff) next show "disjoint ((\a'. \b'\Cb. a' - b')`Ca)" using Ca by (auto simp add: disjoint_def \Cb \ {}\) @@ -935,7 +939,7 @@ done lemma UN_binaryset_eq: "(\i. binaryset A B i) = A \ B" - by (simp add: SUP_def range_binaryset_eq) + by (simp add: range_binaryset_eq cong del: strong_SUP_cong) subsubsection \Closed CDI\ diff -r 1cf129590be8 -r 24106dc44def src/HOL/Relation.thy --- a/src/HOL/Relation.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Relation.thy Wed Feb 17 21:51:56 2016 +0100 @@ -1060,10 +1060,11 @@ text\Converse inclusion requires some assumptions\ lemma Image_INT_eq: - "[|single_valued (r\); A\{}|] ==> r `` INTER A B = (\x\A. r `` B x)" + "single_valued (r\) \ A \ {} \ r `` INTER A B = (\x\A. r `` B x)" apply (rule equalityI) apply (rule Image_INT_subset) -apply (simp add: single_valued_def, blast) +apply (auto simp add: single_valued_def) +apply blast done lemma Image_subset_eq: "(r``A \ B) = (A \ - ((r^-1) `` (-B)))" diff -r 1cf129590be8 -r 24106dc44def src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Set_Interval.thy Wed Feb 17 21:51:56 2016 +0100 @@ -1085,26 +1085,33 @@ qed qed -lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)" +lemma UN_UN_finite_eq: + "(\n::nat. \i\{0..n. A n)" by (auto simp add: atLeast0LessThan) -lemma UN_finite_subset: "(!!n::nat. (\i\{0.. C) \ (\n. A n) \ C" +lemma UN_finite_subset: + "(\n::nat. (\i\{0.. C) \ (\n. A n) \ C" by (subst UN_UN_finite_eq [symmetric]) blast lemma UN_finite2_subset: - "(!!n::nat. (\i\{0.. (\i\{0.. (\n. A n) \ (\n. B n)" - apply (rule UN_finite_subset) - apply (subst UN_UN_finite_eq [symmetric, of B]) - apply blast - done + assumes "\n::nat. (\i\{0.. (\i\{0..n. A n) \ (\n. B n)" +proof (rule UN_finite_subset, rule) + fix n and a + from assms have "(\i\{0.. (\i\{0.. (\i\{0.. (\i\{0.. (\i. B i)" by (auto simp add: UN_UN_finite_eq) +qed lemma UN_finite2_eq: - "(!!n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)" + "(\n::nat. (\i\{0..i\{0.. + (\n. A n) = (\n. B n)" apply (rule subset_antisym) apply (rule UN_finite2_subset, blast) - apply (rule UN_finite2_subset [where k=k]) - apply (force simp add: atLeastLessThan_add_Un [of 0]) - done + apply (rule UN_finite2_subset [where k=k]) + apply (force simp add: atLeastLessThan_add_Un [of 0]) + done subsubsection \Cardinality\ diff -r 1cf129590be8 -r 24106dc44def src/HOL/Tools/BNF/bnf_comp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Wed Feb 17 21:51:56 2016 +0100 @@ -251,7 +251,7 @@ val simplified_set_simps = @{thms collect_def[abs_def] UN_insert UN_empty Un_empty_right Un_empty_left - o_def Union_Un_distrib Union_image_eq UN_empty2 UN_singleton id_bnf_def}; + o_def Union_Un_distrib UN_empty2 UN_singleton id_bnf_def}; fun mk_simplified_set_tac ctxt collect_set_map = unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN diff -r 1cf129590be8 -r 24106dc44def src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Wed Feb 17 21:51:56 2016 +0100 @@ -540,8 +540,8 @@ fun mk_ctor_set_tac ctxt set set_map set_maps = let val n = length set_maps; - fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN' - rtac ctxt @{thm Union_image_eq}; + fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans) + THEN' rtac ctxt @{thm refl}; in EVERY' [rtac ctxt (set RS @{thm comp_eq_dest} RS trans), rtac ctxt Un_cong, rtac ctxt (trans OF [set_map, trans_fun_cong_image_id_id_apply]), diff -r 1cf129590be8 -r 24106dc44def src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Feb 17 21:51:56 2016 +0100 @@ -257,8 +257,12 @@ Const (@{const_name Bex}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f; fun mk_UNION X f = - let val (T, U) = dest_funT (fastype_of f); - in Const (@{const_name SUPREMUM}, fastype_of X --> (T --> U) --> U) $ X $ f end; + let + val (T, U) = dest_funT (fastype_of f); + in + Const (@{const_name Sup}, HOLogic.mk_setT U --> U) + $ (Const (@{const_name image}, (T --> U) --> fastype_of X --> HOLogic.mk_setT U) $ f $ X) + end; fun mk_Union T = Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T); diff -r 1cf129590be8 -r 24106dc44def src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Topological_Spaces.thy Wed Feb 17 21:51:56 2016 +0100 @@ -1133,10 +1133,11 @@ using A by auto show "nhds x = (INF n. principal (\i\n. A i))" using A unfolding nhds_def - apply (intro INF_eq) + apply - + apply (rule INF_eq) apply simp_all - apply force - apply (intro exI[of _ "\i\n. A i" for n] conjI open_INT) + apply fastforce + apply (intro exI [of _ "\i\n. A i" for n] conjI open_INT) apply auto done qed @@ -1464,7 +1465,7 @@ lemma continuous_on_open_UN: "(\s. s \ S \ open (A s)) \ (\s. s \ S \ continuous_on (A s) f) \ continuous_on (\s\S. A s) f" - unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto + by (rule continuous_on_open_Union) auto lemma continuous_on_open_Un: "open s \ open t \ continuous_on s f \ continuous_on t f \ continuous_on (s \ t) f" @@ -1689,7 +1690,7 @@ lemma compactE_image: assumes "compact s" and "\t\C. open (f t)" and "s \ (\c\C. f c)" obtains C' where "C' \ C" and "finite C'" and "s \ (\c\C'. f c)" - using assms unfolding ball_simps[symmetric] SUP_def + using assms unfolding ball_simps [symmetric] by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s]) lemma compact_inter_closed [intro]: diff -r 1cf129590be8 -r 24106dc44def src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Transitive_Closure.thy Wed Feb 17 21:51:56 2016 +0100 @@ -946,7 +946,7 @@ apply (rule iffI) apply (drule tranclD2) apply (clarsimp simp: rtrancl_is_UN_relpow) - apply (rule_tac x="Suc n" in exI) + apply (rule_tac x="Suc x" in exI) apply (clarsimp simp: relcomp_unfold) apply fastforce apply clarsimp @@ -1093,9 +1093,9 @@ assumes "finite R" and "finite S" shows "finite(R O S)" proof- - have "R O S = (UN (x,y) : R. \((%(u,v). if u=y then {(x,v)} else {}) ` S))" - by(force simp add: split_def) - thus ?thesis using assms by(clarsimp) + have "R O S = (\(x, y)\R. \(u, v)\S. if u = y then {(x, v)} else {})" + by (force simp add: split_def image_constant_conv split: if_splits) + then show ?thesis using assms by clarsimp qed lemma finite_relpow[simp,intro]: diff -r 1cf129590be8 -r 24106dc44def src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/UNITY/Comp/Alloc.thy Wed Feb 17 21:51:56 2016 +0100 @@ -1035,7 +1035,7 @@ apply (simp only: o_apply sub_def) apply (insert Alloc_Progress [THEN rename_guarantees_sysOfAlloc_I]) apply (simp add: o_def del: INT_iff) - apply (erule component_guaranteesD) + apply (drule component_guaranteesD) apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def] System_Increasing_allocAsk [simplified sub_apply o_def] @@ -1047,6 +1047,7 @@ lemma System_Progress: "System : system_progress" apply (unfold system_progress_def) apply (cut_tac System_Alloc_Progress) + apply auto apply (blast intro: LeadsTo_Trans System_Follows_allocGiv [THEN Follows_LeadsTo_pfixLe] System_Follows_ask [THEN Follows_LeadsTo]) diff -r 1cf129590be8 -r 24106dc44def src/HOL/UNITY/ELT.thy --- a/src/HOL/UNITY/ELT.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/UNITY/ELT.thy Wed Feb 17 21:51:56 2016 +0100 @@ -141,7 +141,6 @@ lemma leadsETo_UN: "(!!i. i : I ==> F : (A i) leadsTo[CC] B) ==> F : (UN i:I. A i) leadsTo[CC] B" -apply (subst Union_image_eq [symmetric]) apply (blast intro: leadsETo_Union) done @@ -397,7 +396,6 @@ lemma LeadsETo_UN: "(!!i. i : I ==> F : (A i) LeadsTo[CC] B) ==> F : (UN i:I. A i) LeadsTo[CC] B" -apply (simp only: Union_image_eq [symmetric]) apply (blast intro: LeadsETo_Union) done diff -r 1cf129590be8 -r 24106dc44def src/HOL/UNITY/Extend.thy --- a/src/HOL/UNITY/Extend.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/UNITY/Extend.thy Wed Feb 17 21:51:56 2016 +0100 @@ -382,21 +382,25 @@ (project_act h -` AllowedActs F)})" apply (rule program_equalityI) apply simp - apply (simp add: image_eq_UN) + apply (simp add: image_image) apply (simp add: project_def) done lemma extend_inverse [simp]: "project h UNIV (extend h F) = F" -apply (simp (no_asm_simp) add: project_extend_eq image_eq_UN +apply (simp (no_asm_simp) add: project_extend_eq subset_UNIV [THEN subset_trans, THEN Restrict_triv]) apply (rule program_equalityI) apply (simp_all (no_asm)) apply (subst insert_absorb) apply (simp (no_asm) add: bexI [of _ Id]) apply auto +apply (simp add: image_def) +using project_act_Id apply blast +apply (simp add: image_def) apply (rename_tac "act") -apply (rule_tac x = "extend_act h act" in bexI, auto) +apply (rule_tac x = "extend_act h act" in exI) +apply simp done lemma inj_extend: "inj (extend h)" @@ -641,11 +645,12 @@ subsection{*Guarantees*} lemma project_extend_Join: "project h UNIV ((extend h F)\G) = F\(project h UNIV G)" -apply (rule program_equalityI) - apply (simp add: project_set_extend_set_Int) - apply (auto simp add: image_eq_UN) -done - + apply (rule program_equalityI) + apply (auto simp add: project_set_extend_set_Int image_iff) + apply (metis Un_iff extend_act_inverse image_iff) + apply (metis Un_iff extend_act_inverse image_iff) + done + lemma extend_Join_eq_extend_D: "(extend h F)\G = extend h H ==> H = F\(project h UNIV G)" apply (drule_tac f = "project h UNIV" in arg_cong) diff -r 1cf129590be8 -r 24106dc44def src/HOL/UNITY/ProgressSets.thy --- a/src/HOL/UNITY/ProgressSets.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/UNITY/ProgressSets.thy Wed Feb 17 21:51:56 2016 +0100 @@ -42,13 +42,11 @@ lemma UN_in_lattice: "[|lattice L; !!i. i\I ==> r i \ L|] ==> (\i\I. r i) \ L" -apply (unfold SUP_def) apply (blast intro: Union_in_lattice) done lemma INT_in_lattice: "[|lattice L; !!i. i\I ==> r i \ L|] ==> (\i\I. r i) \ L" -apply (unfold INF_def) apply (blast intro: Inter_in_lattice) done diff -r 1cf129590be8 -r 24106dc44def src/HOL/UNITY/Rename.thy --- a/src/HOL/UNITY/Rename.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/UNITY/Rename.thy Wed Feb 17 21:51:56 2016 +0100 @@ -272,7 +272,7 @@ (F \ (rename (inv h) ` X) guarantees (rename (inv h) ` Y))" apply (subst rename_rename_guarantees_eq [symmetric], assumption) -apply (simp add: image_eq_UN o_def bij_is_surj [THEN surj_f_inv_f]) +apply (simp add: o_def bij_is_surj [THEN surj_f_inv_f] image_comp) done lemma rename_preserves: diff -r 1cf129590be8 -r 24106dc44def src/HOL/UNITY/SubstAx.thy --- a/src/HOL/UNITY/SubstAx.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/UNITY/SubstAx.thy Wed Feb 17 21:51:56 2016 +0100 @@ -84,7 +84,6 @@ lemma LeadsTo_UN: "(!!i. i \ I ==> F \ (A i) LeadsTo B) ==> F \ (\i \ I. A i) LeadsTo B" -apply (unfold SUP_def) apply (blast intro: LeadsTo_Union) done @@ -188,7 +187,6 @@ lemma LeadsTo_UN_UN: "(!! i. i \ I ==> F \ (A i) LeadsTo (A' i)) ==> F \ (\i \ I. A i) LeadsTo (\i \ I. A' i)" -apply (simp only: Union_image_eq [symmetric]) apply (blast intro: LeadsTo_Union LeadsTo_weaken_R) done diff -r 1cf129590be8 -r 24106dc44def src/HOL/UNITY/Transformers.thy --- a/src/HOL/UNITY/Transformers.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/UNITY/Transformers.thy Wed Feb 17 21:51:56 2016 +0100 @@ -467,7 +467,7 @@ "single_valued act ==> insert (wens_single act B) (range (wens_single_finite act B)) \ wens_set (mk_program (init, {act}, allowed)) B" -apply (simp add: SUP_def image_def wens_single_eq_Union) +apply (simp add: image_def wens_single_eq_Union) apply (blast intro: wens_set.Union wens_single_finite_in_wens_set) done diff -r 1cf129590be8 -r 24106dc44def src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/UNITY/Union.thy Wed Feb 17 21:51:56 2016 +0100 @@ -396,11 +396,30 @@ lemma safety_prop_Int [simp]: "safety_prop X \ safety_prop Y \ safety_prop (X \ Y)" - by (simp add: safety_prop_def) blast +proof (clarsimp simp add: safety_prop_def) + fix G + assume "\G. Acts G \ (\x\X. Acts x) \ G \ X" + then have X: "Acts G \ (\x\X. Acts x) \ G \ X" by blast + assume "\G. Acts G \ (\x\Y. Acts x) \ G \ Y" + then have Y: "Acts G \ (\x\Y. Acts x) \ G \ Y" by blast + assume Acts: "Acts G \ (\x\X \ Y. Acts x)" + with X and Y show "G \ X \ G \ Y" by auto +qed lemma safety_prop_INTER [simp]: "(\i. i \ I \ safety_prop (X i)) \ safety_prop (\i\I. X i)" - by (simp add: safety_prop_def) blast +proof (clarsimp simp add: safety_prop_def) + fix G and i + assume "\i. i \ I \ \ \ X i \ + (\G. Acts G \ (\x\X i. Acts x) \ G \ X i)" + then have *: "i \ I \ Acts G \ (\x\X i. Acts x) \ G \ X i" + by blast + assume "i \ I" + moreover assume "Acts G \ (\j\\i\I. X i. Acts j)" + ultimately have "Acts G \ (\i\X i. Acts i)" + by auto + with * `i \ I` show "G \ X i" by blast +qed lemma safety_prop_INTER1 [simp]: "(\i. safety_prop (X i)) \ safety_prop (\i. X i)" diff -r 1cf129590be8 -r 24106dc44def src/HOL/UNITY/WFair.thy --- a/src/HOL/UNITY/WFair.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/UNITY/WFair.thy Wed Feb 17 21:51:56 2016 +0100 @@ -203,7 +203,6 @@ lemma leadsTo_UN: "(!!i. i \ I ==> F \ (A i) leadsTo B) ==> F \ (\i \ I. A i) leadsTo B" -apply (subst Union_image_eq [symmetric]) apply (blast intro: leadsTo_Union) done @@ -310,7 +309,6 @@ lemma leadsTo_UN_UN: "(!! i. i \ I ==> F \ (A i) leadsTo (A' i)) ==> F \ (\i \ I. A i) leadsTo (\i \ I. A' i)" -apply (simp only: Union_image_eq [symmetric]) apply (blast intro: leadsTo_Union leadsTo_weaken_R) done