prefer abbreviations for compound operators INFIMUM and SUPREMUM
authorhaftmann
Wed Feb 17 21:51:56 2016 +0100 (2016-02-17)
changeset 6234324106dc44def
parent 62342 1cf129590be8
child 62344 759d684c0e60
prefer abbreviations for compound operators INFIMUM and SUPREMUM
CONTRIBUTORS
NEWS
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Coset.thy
src/HOL/Auth/Guard/Proto.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/Recur.thy
src/HOL/Auth/Smartcard/ShoupRubin.thy
src/HOL/Auth/Smartcard/ShoupRubinBella.thy
src/HOL/Auth/Smartcard/Smartcard.thy
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/Cardinals/Wellorder_Relation.thy
src/HOL/Complete_Lattices.thy
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Enum.thy
src/HOL/Filter.thy
src/HOL/GCD.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hoare_Parallel/OG_Hoare.thy
src/HOL/Hoare_Parallel/RG_Hoare.thy
src/HOL/IMP/Denotational.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Finite_Lattice.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Library/Lub_Glb.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/Product_Order.thy
src/HOL/Lifting_Set.thy
src/HOL/List.thy
src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Number_Theory/MiscAlgebra.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Complete_Measure.thy
src/HOL/Probability/Embed_Measure.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measurable.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Regularity.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Relation.thy
src/HOL/Set_Interval.thy
src/HOL/Tools/BNF/bnf_comp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/BNF/bnf_util.ML
src/HOL/Topological_Spaces.thy
src/HOL/Transitive_Closure.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/ProgressSets.thy
src/HOL/UNITY/Rename.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/Transformers.thy
src/HOL/UNITY/Union.thy
src/HOL/UNITY/WFair.thy
     1.1 --- a/CONTRIBUTORS	Wed Feb 17 21:51:55 2016 +0100
     1.2 +++ b/CONTRIBUTORS	Wed Feb 17 21:51:56 2016 +0100
     1.3 @@ -6,6 +6,10 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* January 2016: Florian Haftmann
     1.8 +  Abolition of compound operators INFIMUM and SUPREMUM
     1.9 +  for complete lattices.
    1.10 +
    1.11  
    1.12  Contributions to Isabelle2016
    1.13  -----------------------------
     2.1 --- a/NEWS	Wed Feb 17 21:51:55 2016 +0100
     2.2 +++ b/NEWS	Wed Feb 17 21:51:56 2016 +0100
     2.3 @@ -32,6 +32,9 @@
     2.4        pred_prod_apply ~> pred_prod_inject
     2.5      INCOMPATIBILITY.
     2.6  
     2.7 +* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
     2.8 +INCOMPATIBILITY.
     2.9 +
    2.10  
    2.11  New in Isabelle2016 (February 2016)
    2.12  -----------------------------------
     3.1 --- a/src/HOL/Algebra/AbelCoset.thy	Wed Feb 17 21:51:55 2016 +0100
     3.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Wed Feb 17 21:51:56 2016 +0100
     3.3 @@ -258,7 +258,7 @@
     3.4      from a_subgroup have Hcarr: "H \<subseteq> carrier G"
     3.5        unfolding subgroup_def by simp
     3.6      from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
     3.7 -      using m_comm [simplified] by fast
     3.8 +      using m_comm [simplified] by fastforce
     3.9    qed
    3.10  qed
    3.11  
     4.1 --- a/src/HOL/Algebra/Coset.thy	Wed Feb 17 21:51:55 2016 +0100
     4.2 +++ b/src/HOL/Algebra/Coset.thy	Wed Feb 17 21:51:56 2016 +0100
     4.3 @@ -517,7 +517,7 @@
     4.4  by (auto simp add: set_mult_def subsetD)
     4.5  
     4.6  lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H"
     4.7 -apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def)
     4.8 +apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def)
     4.9  apply (rule_tac x = x in bexI)
    4.10  apply (rule bexI [of _ "\<one>"])
    4.11  apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD])
    4.12 @@ -932,10 +932,22 @@
    4.13    obtain g where g: "g \<in> carrier G" 
    4.14               and "X = kernel G H h #> g"
    4.15      by (auto simp add: FactGroup_def RCOSETS_def)
    4.16 -  hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g)
    4.17 +  hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def g intro!: imageI)
    4.18    thus ?thesis by (auto simp add: g)
    4.19  qed
    4.20  
    4.21 +lemma the_elem_image_unique: -- {* FIXME move *}
    4.22 +  assumes "A \<noteq> {}"
    4.23 +  assumes *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
    4.24 +  shows "the_elem (f ` A) = f x"
    4.25 +unfolding the_elem_def proof (rule the1_equality)
    4.26 +  from `A \<noteq> {}` obtain y where "y \<in> A" by auto
    4.27 +  with * have "f x = f y" by simp
    4.28 +  with `y \<in> A` have "f x \<in> f ` A" by blast
    4.29 +  with * show "f ` A = {f x}" by auto
    4.30 +  then show "\<exists>!x. f ` A = {x}" by auto
    4.31 +qed
    4.32 +
    4.33  lemma (in group_hom) FactGroup_hom:
    4.34       "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
    4.35  apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
    4.36 @@ -952,11 +964,11 @@
    4.37      and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
    4.38      by (force simp add: kernel_def r_coset_def image_def)+
    4.39    hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
    4.40 -    by (auto dest!: FactGroup_nonempty
    4.41 -             simp add: set_mult_def image_eq_UN 
    4.42 +    by (auto dest!: FactGroup_nonempty intro!: image_eqI
    4.43 +             simp add: set_mult_def 
    4.44                         subsetD [OF Xsub] subsetD [OF X'sub]) 
    4.45 -  thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
    4.46 -    by (simp add: all image_eq_UN FactGroup_nonempty X X')
    4.47 +  then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
    4.48 +    by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
    4.49  qed
    4.50  
    4.51  
    4.52 @@ -964,7 +976,7 @@
    4.53  lemma (in group_hom) FactGroup_subset:
    4.54       "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
    4.55        \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
    4.56 -apply (clarsimp simp add: kernel_def r_coset_def image_def)
    4.57 +apply (clarsimp simp add: kernel_def r_coset_def)
    4.58  apply (rename_tac y)  
    4.59  apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) 
    4.60  apply (simp add: G.m_assoc) 
    4.61 @@ -985,7 +997,7 @@
    4.62      by (force simp add: kernel_def r_coset_def image_def)+
    4.63    assume "the_elem (h ` X) = the_elem (h ` X')"
    4.64    hence h: "h g = h g'"
    4.65 -    by (simp add: image_eq_UN all FactGroup_nonempty X X') 
    4.66 +    by (simp add: all FactGroup_nonempty X X' the_elem_image_unique) 
    4.67    show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
    4.68  qed
    4.69  
    4.70 @@ -1006,7 +1018,10 @@
    4.71      hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
    4.72        by (auto simp add: y kernel_def r_coset_def) 
    4.73      with g show "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)" 
    4.74 -      by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
    4.75 +      apply (auto intro!: bexI image_eqI simp add: FactGroup_def RCOSETS_def)
    4.76 +      apply (subst the_elem_image_unique)
    4.77 +      apply auto
    4.78 +      done
    4.79    qed
    4.80  qed
    4.81  
    4.82 @@ -1019,5 +1034,4 @@
    4.83  by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
    4.84                FactGroup_onto) 
    4.85  
    4.86 -
    4.87  end
     5.1 --- a/src/HOL/Auth/Guard/Proto.thy	Wed Feb 17 21:51:55 2016 +0100
     5.2 +++ b/src/HOL/Auth/Guard/Proto.thy	Wed Feb 17 21:51:56 2016 +0100
     5.3 @@ -56,7 +56,7 @@
     5.4  Nonce n ~:parts (apm s `(msg `(fst R))) |] ==>
     5.5  (EX k. Nonce k:parts {X} & nonce s k = n)"
     5.6  apply (erule Nonce_apm, unfold wdef_def)
     5.7 -apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp simp: image_eq_UN)
     5.8 +apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp)
     5.9  apply (drule_tac x=x in bspec, simp)
    5.10  apply (drule_tac Y="msg x" and s=s in apm_parts, simp)
    5.11  by (blast dest: parts_parts)
    5.12 @@ -134,7 +134,7 @@
    5.13  
    5.14  lemma ok_not_used: "[| Nonce n ~:used evs; ok evs R s;
    5.15  ALL x. x:fst R --> is_Says x |] ==> Nonce n ~:parts (apm s `(msg `(fst R)))"
    5.16 -apply (unfold ok_def, clarsimp simp: image_eq_UN)
    5.17 +apply (unfold ok_def, clarsimp)
    5.18  apply (drule_tac x=x in spec, drule_tac x=x in spec)
    5.19  by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts)
    5.20  
    5.21 @@ -188,10 +188,10 @@
    5.22  apply (drule wdef_Nonce, simp+)
    5.23  apply (frule ok_not_used, simp+)
    5.24  apply (clarify, erule ok_is_Says, simp+)
    5.25 -apply (clarify, rule_tac x=k in exI, simp add: newn_def image_eq_UN)
    5.26 +apply (clarify, rule_tac x=k in exI, simp add: newn_def)
    5.27  apply (clarify, drule_tac Y="msg x" and s=s in apm_parts)
    5.28  apply (drule ok_not_used, simp+)
    5.29 -by (clarify, erule ok_is_Says, simp_all add: image_eq_UN)
    5.30 +by (clarify, erule ok_is_Says, simp_all)
    5.31  
    5.32  lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs;
    5.33  Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev"
     6.1 --- a/src/HOL/Auth/Message.thy	Wed Feb 17 21:51:55 2016 +0100
     6.2 +++ b/src/HOL/Auth/Message.thy	Wed Feb 17 21:51:56 2016 +0100
     6.3 @@ -207,8 +207,16 @@
     6.4  apply (erule parts.induct, blast+)
     6.5  done
     6.6  
     6.7 -lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))"
     6.8 -by (intro equalityI parts_UN_subset1 parts_UN_subset2)
     6.9 +lemma parts_UN [simp]:
    6.10 +  "parts (\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts (H x))"
    6.11 +  by (intro equalityI parts_UN_subset1 parts_UN_subset2)
    6.12 +
    6.13 +lemma parts_image [simp]:
    6.14 +  "parts (f ` A) = (\<Union>x\<in>A. parts {f x})"
    6.15 +  apply auto
    6.16 +  apply (metis (mono_tags, hide_lams) image_iff parts_singleton)
    6.17 +  apply (metis empty_subsetI image_eqI insert_absorb insert_subset parts_mono)
    6.18 +  done
    6.19  
    6.20  text\<open>Added to simplify arguments to parts, analz and synth.
    6.21    NOTE: the UN versions are no longer used!\<close>
    6.22 @@ -299,10 +307,7 @@
    6.23  done
    6.24  
    6.25  lemma parts_image_Key [simp]: "parts (Key`N) = Key`N"
    6.26 -apply auto
    6.27 -apply (erule parts.induct, auto)
    6.28 -done
    6.29 -
    6.30 +by auto
    6.31  
    6.32  text\<open>In any message, there is an upper bound N on its greatest nonce.\<close>
    6.33  lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
     7.1 --- a/src/HOL/Auth/Recur.thy	Wed Feb 17 21:51:55 2016 +0100
     7.2 +++ b/src/HOL/Auth/Recur.thy	Wed Feb 17 21:51:56 2016 +0100
     7.3 @@ -337,7 +337,7 @@
     7.4           RB \<in> responses evs |]
     7.5       ==> (Key K \<in> parts{RB} | Key K \<in> analz H)"
     7.6  apply (erule rev_mp, erule responses.induct)
     7.7 -apply (simp_all del: image_insert
     7.8 +apply (simp_all del: image_insert parts_image
     7.9               add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
    7.10  txt\<open>Simplification using two distinct treatments of "image"\<close>
    7.11  apply (simp add: parts_insert2, blast)
    7.12 @@ -389,7 +389,7 @@
    7.13  apply (erule respond.induct)
    7.14  apply (frule_tac [2] respond_imp_responses)
    7.15  apply (frule_tac [2] respond_imp_not_used)
    7.16 -apply (simp_all del: image_insert
    7.17 +apply (simp_all del: image_insert parts_image
    7.18                  add: analz_image_freshK_simps split_ifs shrK_in_analz_respond
    7.19                       resp_analz_image_freshK parts_insert2)
    7.20  txt\<open>Base case of respond\<close>
     8.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Wed Feb 17 21:51:55 2016 +0100
     8.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Wed Feb 17 21:51:56 2016 +0100
     8.3 @@ -809,9 +809,9 @@
     8.4  
     8.5  (*Because initState contains a set of nonces, this is needed for base case of
     8.6    analz_image_freshK*)
     8.7 -lemma analz_image_Key_Un_Nonce: "analz (Key`K \<union> Nonce`N) = Key`K \<union> Nonce`N"
     8.8 -apply auto
     8.9 -done
    8.10 +lemma analz_image_Key_Un_Nonce:
    8.11 +  "analz (Key ` K \<union> Nonce ` N) = Key ` K \<union> Nonce ` N"
    8.12 +  by (auto simp del: parts_image)
    8.13  
    8.14  method_setup sc_analz_freshK = \<open>
    8.15      Scan.succeed (fn ctxt =>
     9.1 --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Wed Feb 17 21:51:55 2016 +0100
     9.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Wed Feb 17 21:51:56 2016 +0100
     9.3 @@ -819,9 +819,9 @@
     9.4  
     9.5  (*Because initState contains a set of nonces, this is needed for base case of
     9.6    analz_image_freshK*)
     9.7 -lemma analz_image_Key_Un_Nonce: "analz (Key`K \<union> Nonce`N) = Key`K \<union> Nonce`N"
     9.8 -apply auto
     9.9 -done
    9.10 +lemma analz_image_Key_Un_Nonce:
    9.11 +  "analz (Key ` K \<union> Nonce ` N) = Key ` K \<union> Nonce ` N"
    9.12 +  by (auto simp del: parts_image)
    9.13  
    9.14  method_setup sc_analz_freshK = \<open>
    9.15      Scan.succeed (fn ctxt =>
    10.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Feb 17 21:51:55 2016 +0100
    10.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Feb 17 21:51:56 2016 +0100
    10.3 @@ -115,10 +115,7 @@
    10.4  
    10.5  text\<open>Added to extend initstate with set of nonces\<close>
    10.6  lemma parts_image_Nonce [simp]: "parts (Nonce`N) = Nonce`N"
    10.7 -apply auto
    10.8 -apply (erule parts.induct)
    10.9 -apply auto
   10.10 -done
   10.11 +  by auto
   10.12  
   10.13  lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
   10.14  apply (unfold keysFor_def)
    11.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Wed Feb 17 21:51:55 2016 +0100
    11.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Wed Feb 17 21:51:56 2016 +0100
    11.3 @@ -711,7 +711,7 @@
    11.4  
    11.5  lemma card_of_UNION_Sigma:
    11.6  "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
    11.7 -using Ex_inj_on_UNION_Sigma[of I A] card_of_ordLeq by blast
    11.8 +using Ex_inj_on_UNION_Sigma [of A I] card_of_ordLeq by blast
    11.9  
   11.10  lemma card_of_bool:
   11.11  assumes "a1 \<noteq> a2"
    12.1 --- a/src/HOL/Cardinals/Wellorder_Relation.thy	Wed Feb 17 21:51:55 2016 +0100
    12.2 +++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Wed Feb 17 21:51:56 2016 +0100
    12.3 @@ -450,8 +450,7 @@
    12.4  
    12.5  lemma ofilter_under_Union:
    12.6  "ofilter A \<Longrightarrow> A = \<Union>{under a| a. a \<in> A}"
    12.7 -using ofilter_under_UNION[of A]
    12.8 -by(unfold Union_eq, auto)
    12.9 +using ofilter_under_UNION [of A] by auto
   12.10  
   12.11  
   12.12  subsubsection {* Other properties *}
    13.1 --- a/src/HOL/Complete_Lattices.thy	Wed Feb 17 21:51:55 2016 +0100
    13.2 +++ b/src/HOL/Complete_Lattices.thy	Wed Feb 17 21:51:56 2016 +0100
    13.3 @@ -17,28 +17,25 @@
    13.4    fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
    13.5  begin
    13.6  
    13.7 -definition INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    13.8 -  INF_def: "INFIMUM A f = \<Sqinter>(f ` A)"
    13.9 -
   13.10 -lemma Inf_image_eq [simp]:
   13.11 -  "\<Sqinter>(f ` A) = INFIMUM A f"
   13.12 -  by (simp add: INF_def)
   13.13 +abbreviation INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
   13.14 +where
   13.15 +  "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
   13.16  
   13.17  lemma INF_image [simp]:
   13.18    "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
   13.19 -  by (simp only: INF_def image_comp)
   13.20 +  by (simp add: image_comp)
   13.21  
   13.22  lemma INF_identity_eq [simp]:
   13.23    "INFIMUM A (\<lambda>x. x) = \<Sqinter>A"
   13.24 -  by (simp add: INF_def)
   13.25 +  by simp
   13.26  
   13.27  lemma INF_id_eq [simp]:
   13.28    "INFIMUM A id = \<Sqinter>A"
   13.29 -  by (simp add: id_def)
   13.30 +  by simp
   13.31  
   13.32  lemma INF_cong:
   13.33    "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
   13.34 -  by (simp add: INF_def image_def)
   13.35 +  by (simp add: image_def)
   13.36  
   13.37  lemma strong_INF_cong [cong]:
   13.38    "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
   13.39 @@ -50,20 +47,17 @@
   13.40    fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
   13.41  begin
   13.42  
   13.43 -definition SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   13.44 -  SUP_def: "SUPREMUM A f = \<Squnion>(f ` A)"
   13.45 -
   13.46 -lemma Sup_image_eq [simp]:
   13.47 -  "\<Squnion>(f ` A) = SUPREMUM A f"
   13.48 -  by (simp add: SUP_def)
   13.49 +abbreviation SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
   13.50 +where
   13.51 +  "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
   13.52  
   13.53  lemma SUP_image [simp]:
   13.54    "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
   13.55 -  by (simp only: SUP_def image_comp)
   13.56 +  by (simp add: image_comp)
   13.57  
   13.58  lemma SUP_identity_eq [simp]:
   13.59    "SUPREMUM A (\<lambda>x. x) = \<Squnion>A"
   13.60 -  by (simp add: SUP_def)
   13.61 +  by simp
   13.62  
   13.63  lemma SUP_id_eq [simp]:
   13.64    "SUPREMUM A id = \<Squnion>A"
   13.65 @@ -71,7 +65,7 @@
   13.66  
   13.67  lemma SUP_cong:
   13.68    "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
   13.69 -  by (simp add: SUP_def image_def)
   13.70 +  by (simp add: image_def)
   13.71  
   13.72  lemma strong_SUP_cong [cong]:
   13.73    "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
   13.74 @@ -153,14 +147,6 @@
   13.75  context complete_lattice
   13.76  begin
   13.77  
   13.78 -lemma INF_foundation_dual:
   13.79 -  "Sup.SUPREMUM Inf = INFIMUM"
   13.80 -  by (simp add: fun_eq_iff Sup.SUP_def)
   13.81 -
   13.82 -lemma SUP_foundation_dual:
   13.83 -  "Inf.INFIMUM Sup = SUPREMUM"
   13.84 -  by (simp add: fun_eq_iff Inf.INF_def)
   13.85 -
   13.86  lemma Sup_eqI:
   13.87    "(\<And>y. y \<in> A \<Longrightarrow> y \<le> x) \<Longrightarrow> (\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> \<Squnion>A = x"
   13.88    by (blast intro: antisym Sup_least Sup_upper)
   13.89 @@ -217,19 +203,19 @@
   13.90    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
   13.91  
   13.92  lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFIMUM A f"
   13.93 -  unfolding INF_def Inf_insert by simp
   13.94 +  by (simp cong del: strong_INF_cong)
   13.95  
   13.96  lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   13.97    by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
   13.98  
   13.99  lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPREMUM A f"
  13.100 -  unfolding SUP_def Sup_insert by simp
  13.101 +  by (simp cong del: strong_SUP_cong)
  13.102  
  13.103  lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
  13.104 -  by (simp add: INF_def)
  13.105 +  by (simp cong del: strong_INF_cong)
  13.106  
  13.107  lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
  13.108 -  by (simp add: SUP_def)
  13.109 +  by (simp cong del: strong_SUP_cong)
  13.110  
  13.111  lemma Inf_UNIV [simp]:
  13.112    "\<Sqinter>UNIV = \<bottom>"
  13.113 @@ -308,18 +294,18 @@
  13.114    ultimately show ?thesis by (rule Sup_upper2)
  13.115  qed
  13.116  
  13.117 +lemma INF_eq:
  13.118 +  assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
  13.119 +  assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
  13.120 +  shows "INFIMUM A f = INFIMUM B g"
  13.121 +  by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
  13.122 +
  13.123  lemma SUP_eq:
  13.124    assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
  13.125    assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
  13.126 -  shows "(\<Squnion>i\<in>A. f i) = (\<Squnion>j\<in>B. g j)"
  13.127 +  shows "SUPREMUM A f = SUPREMUM B g"
  13.128    by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
  13.129  
  13.130 -lemma INF_eq:
  13.131 -  assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
  13.132 -  assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
  13.133 -  shows "(\<Sqinter>i\<in>A. f i) = (\<Sqinter>j\<in>B. g j)"
  13.134 -  by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
  13.135 -
  13.136  lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
  13.137    by (auto intro: Inf_greatest Inf_lower)
  13.138  
  13.139 @@ -498,24 +484,24 @@
  13.140  
  13.141  lemma sup_INF:
  13.142    "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
  13.143 -  by (simp only: INF_def sup_Inf image_image)
  13.144 +  unfolding sup_Inf by simp
  13.145  
  13.146  lemma inf_SUP:
  13.147    "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
  13.148 -  by (simp only: SUP_def inf_Sup image_image)
  13.149 +  unfolding inf_Sup by simp
  13.150  
  13.151  lemma dual_complete_distrib_lattice:
  13.152    "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
  13.153    apply (rule class.complete_distrib_lattice.intro)
  13.154    apply (fact dual_complete_lattice)
  13.155    apply (rule class.complete_distrib_lattice_axioms.intro)
  13.156 -  apply (simp_all only: INF_foundation_dual SUP_foundation_dual inf_Sup sup_Inf)
  13.157 +  apply (simp_all add: inf_Sup sup_Inf)
  13.158    done
  13.159  
  13.160  subclass distrib_lattice proof
  13.161    fix a b c
  13.162    from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
  13.163 -  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def)
  13.164 +  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by simp
  13.165  qed
  13.166  
  13.167  lemma Inf_sup:
  13.168 @@ -592,7 +578,7 @@
  13.169  qed
  13.170  
  13.171  lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
  13.172 -  by (simp only: INF_def SUP_def uminus_Inf image_image)
  13.173 +  by (simp add: uminus_Inf image_image)
  13.174  
  13.175  lemma uminus_Sup:
  13.176    "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
  13.177 @@ -602,7 +588,7 @@
  13.178  qed
  13.179    
  13.180  lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
  13.181 -  by (simp only: INF_def SUP_def uminus_Sup image_image)
  13.182 +  by (simp add: uminus_Sup image_image)
  13.183  
  13.184  end
  13.185  
  13.186 @@ -731,11 +717,11 @@
  13.187  
  13.188  lemma INF_bool_eq [simp]:
  13.189    "INFIMUM = Ball"
  13.190 -  by (simp add: fun_eq_iff INF_def)
  13.191 +  by (simp add: fun_eq_iff)
  13.192  
  13.193  lemma SUP_bool_eq [simp]:
  13.194    "SUPREMUM = Bex"
  13.195 -  by (simp add: fun_eq_iff SUP_def)
  13.196 +  by (simp add: fun_eq_iff)
  13.197  
  13.198  instance bool :: complete_boolean_algebra proof
  13.199  qed (auto intro: bool_induct)
  13.200 @@ -788,8 +774,7 @@
  13.201    using Sup_apply [of "f ` A"] by (simp add: comp_def)
  13.202  
  13.203  instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
  13.204 -qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf fun_eq_iff image_image
  13.205 -  simp del: Inf_image_eq Sup_image_eq)
  13.206 +qed (auto simp add: inf_Sup sup_Inf fun_eq_iff image_image)
  13.207  
  13.208  instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
  13.209  
  13.210 @@ -903,7 +888,7 @@
  13.211  
  13.212  instance "set" :: (type) complete_boolean_algebra
  13.213  proof
  13.214 -qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def)
  13.215 +qed (auto simp add: Inf_set_def Sup_set_def image_def)
  13.216    
  13.217  
  13.218  subsubsection \<open>Inter\<close>
  13.219 @@ -1011,22 +996,18 @@
  13.220    "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
  13.221    by (auto intro!: INF_eqI)
  13.222  
  13.223 -lemma Inter_image_eq:
  13.224 -  "\<Inter>(B ` A) = (\<Inter>x\<in>A. B x)"
  13.225 -  by (fact Inf_image_eq)
  13.226 -
  13.227  lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
  13.228    using Inter_iff [of _ "B ` A"] by simp
  13.229  
  13.230  lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
  13.231 -  by (auto simp add: INF_def image_def)
  13.232 +  by auto
  13.233  
  13.234  lemma INT_D [elim, Pure.elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> B a"
  13.235    by auto
  13.236  
  13.237  lemma INT_E [elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> (b \<in> B a \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
  13.238    \<comment> \<open>"Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}.\<close>
  13.239 -  by (auto simp add: INF_def image_def)
  13.240 +  by auto
  13.241  
  13.242  lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
  13.243    by blast
  13.244 @@ -1198,10 +1179,6 @@
  13.245    "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
  13.246    by (simp add: bind_UNION)
  13.247  
  13.248 -lemma Union_image_eq:
  13.249 -  "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
  13.250 -  by (fact Sup_image_eq)
  13.251 -
  13.252  lemma Union_SetCompr_eq: "\<Union>{f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
  13.253    by blast
  13.254  
  13.255 @@ -1214,10 +1191,7 @@
  13.256    by auto
  13.257  
  13.258  lemma UN_E [elim!]: "b \<in> (\<Union>x\<in>A. B x) \<Longrightarrow> (\<And>x. x\<in>A \<Longrightarrow> b \<in> B x \<Longrightarrow> R) \<Longrightarrow> R"
  13.259 -  by (auto simp add: SUP_def image_def)
  13.260 -
  13.261 -lemma image_eq_UN: "f ` A = (\<Union>x\<in>A. {f x})"
  13.262 -  by blast
  13.263 +  by auto
  13.264  
  13.265  lemma UN_upper: "a \<in> A \<Longrightarrow> B a \<subseteq> (\<Union>x\<in>A. B x)"
  13.266    by (fact SUP_upper)
  13.267 @@ -1273,7 +1247,7 @@
  13.268    by blast
  13.269  
  13.270  lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
  13.271 -  by (auto simp add: split_if_mem2)
  13.272 +  by safe (auto simp add: split_if_mem2)
  13.273  
  13.274  lemma UN_bool_eq: "(\<Union>b. A b) = (A True \<union> A False)"
  13.275    by (fact SUP_UNIV_bool_expand)
  13.276 @@ -1355,7 +1329,7 @@
  13.277  
  13.278  lemma inj_on_INTER:
  13.279    "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)) \<Longrightarrow> inj_on f (\<Inter>i \<in> I. A i)"
  13.280 -  unfolding inj_on_def by blast
  13.281 +  unfolding inj_on_def by safe simp
  13.282  
  13.283  lemma inj_on_UNION_chain:
  13.284    assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
  13.285 @@ -1414,20 +1388,19 @@
  13.286  lemma image_INT:
  13.287     "[| inj_on f C;  ALL x:A. B x <= C;  j:A |]
  13.288      ==> f ` (INTER A B) = (INT x:A. f ` B x)"
  13.289 -apply (simp add: inj_on_def, blast)
  13.290 -done
  13.291 +  by (simp add: inj_on_def, auto) blast
  13.292  
  13.293 -(*Compare with image_INT: no use of inj_on, and if f is surjective then
  13.294 -  it doesn't matter whether A is empty*)
  13.295  lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)"
  13.296 -apply (simp add: bij_def)
  13.297 -apply (simp add: inj_on_def surj_def, blast)
  13.298 -done
  13.299 +  apply (simp add: bij_def)
  13.300 +  apply (simp add: inj_on_def surj_def)
  13.301 +  apply auto
  13.302 +  apply blast
  13.303 +  done
  13.304  
  13.305  lemma UNION_fun_upd:
  13.306 -  "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
  13.307 -by (auto split: if_splits)
  13.308 -
  13.309 +  "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
  13.310 +  by (auto simp add: set_eq_iff)
  13.311 +  
  13.312  
  13.313  subsubsection \<open>Complement\<close>
  13.314  
    14.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Feb 17 21:51:55 2016 +0100
    14.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Wed Feb 17 21:51:56 2016 +0100
    14.3 @@ -321,10 +321,10 @@
    14.4    by (metis cSUP_upper le_less_trans)
    14.5  
    14.6  lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFIMUM (insert a A) f = inf (f a) (INFIMUM A f)"
    14.7 -  by (metis cInf_insert Inf_image_eq image_insert image_is_empty)
    14.8 +  by (metis cInf_insert image_insert image_is_empty)
    14.9  
   14.10  lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM (insert a A) f = sup (f a) (SUPREMUM A f)"
   14.11 -  by (metis cSup_insert Sup_image_eq image_insert image_is_empty)
   14.12 +  by (metis cSup_insert image_insert image_is_empty)
   14.13  
   14.14  lemma cINF_mono: "B \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> INFIMUM A f \<le> INFIMUM B g"
   14.15    using cInf_mono [of "g ` B" "f ` A"] by auto
    15.1 --- a/src/HOL/Enum.thy	Wed Feb 17 21:51:55 2016 +0100
    15.2 +++ b/src/HOL/Enum.thy	Wed Feb 17 21:51:56 2016 +0100
    15.3 @@ -556,7 +556,7 @@
    15.4  end
    15.5  
    15.6  instance finite_1 :: complete_distrib_lattice
    15.7 -by intro_classes(simp_all add: INF_def SUP_def)
    15.8 +  by standard simp_all
    15.9  
   15.10  instance finite_1 :: complete_linorder ..
   15.11  
   15.12 @@ -679,7 +679,7 @@
   15.13  end
   15.14  
   15.15  instance finite_2 :: complete_distrib_lattice
   15.16 -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)
   15.17 +  by standard (auto simp add: sup_finite_2_def inf_finite_2_def Inf_finite_2_def Sup_finite_2_def)
   15.18  
   15.19  instance finite_2 :: complete_linorder ..
   15.20  
   15.21 @@ -797,11 +797,11 @@
   15.22      then have "\<And>x. x \<in> B \<Longrightarrow> x = a\<^sub>3"
   15.23        by(case_tac x)(auto simp add: Inf_finite_3_def split: split_if_asm)
   15.24      then show ?thesis using a\<^sub>2_a\<^sub>3
   15.25 -      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)
   15.26 -  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)
   15.27 +      by(auto simp add: Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: split_if_asm)
   15.28 +  qed (auto simp add: Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
   15.29    show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   15.30 -    by(cases a "\<Squnion>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
   15.31 -      (auto simp add: SUP_def Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
   15.32 +    by (cases a "\<Squnion>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
   15.33 +      (auto simp add: Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
   15.34  qed
   15.35  
   15.36  instance finite_3 :: complete_linorder ..
   15.37 @@ -920,10 +920,10 @@
   15.38    fix a :: finite_4 and B
   15.39    show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   15.40      by(cases a "\<Sqinter>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
   15.41 -      (auto simp add: sup_finite_4_def Inf_finite_4_def INF_def split: finite_4.splits split_if_asm)
   15.42 +      (auto simp add: sup_finite_4_def Inf_finite_4_def split: finite_4.splits split_if_asm)
   15.43    show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   15.44      by(cases a "\<Squnion>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
   15.45 -      (auto simp add: inf_finite_4_def Sup_finite_4_def SUP_def split: finite_4.splits split_if_asm)
   15.46 +      (auto simp add: inf_finite_4_def Sup_finite_4_def split: finite_4.splits split_if_asm)
   15.47  qed
   15.48  
   15.49  instantiation finite_4 :: complete_boolean_algebra begin
    16.1 --- a/src/HOL/Filter.thy	Wed Feb 17 21:51:55 2016 +0100
    16.2 +++ b/src/HOL/Filter.thy	Wed Feb 17 21:51:56 2016 +0100
    16.3 @@ -437,8 +437,8 @@
    16.4  qed
    16.5  
    16.6  lemma eventually_INF: "eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (INF b:X. F b))"
    16.7 -  unfolding INF_def[of B] eventually_Inf[of P "F`B"]
    16.8 -  by (metis Inf_image_eq finite_imageI image_mono finite_subset_image)
    16.9 +  unfolding eventually_Inf [of P "F`B"]
   16.10 +  by (metis finite_imageI image_mono finite_subset_image)
   16.11  
   16.12  lemma Inf_filter_not_bot:
   16.13    fixes B :: "'a filter set"
   16.14 @@ -449,7 +449,7 @@
   16.15  lemma INF_filter_not_bot:
   16.16    fixes F :: "'i \<Rightarrow> 'a filter"
   16.17    shows "(\<And>X. X \<subseteq> B \<Longrightarrow> finite X \<Longrightarrow> (INF b:X. F b) \<noteq> bot) \<Longrightarrow> (INF b:B. F b) \<noteq> bot"
   16.18 -  unfolding trivial_limit_def eventually_INF[of _ B]
   16.19 +  unfolding trivial_limit_def eventually_INF [of _ _ B]
   16.20      bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
   16.21  
   16.22  lemma eventually_Inf_base:
   16.23 @@ -477,7 +477,7 @@
   16.24  lemma eventually_INF_base:
   16.25    "B \<noteq> {} \<Longrightarrow> (\<And>a b. a \<in> B \<Longrightarrow> b \<in> B \<Longrightarrow> \<exists>x\<in>B. F x \<le> inf (F a) (F b)) \<Longrightarrow>
   16.26      eventually P (INF b:B. F b) \<longleftrightarrow> (\<exists>b\<in>B. eventually P (F b))"
   16.27 -  unfolding INF_def by (subst eventually_Inf_base) auto
   16.28 +  by (subst eventually_Inf_base) auto
   16.29  
   16.30  
   16.31  subsubsection \<open>Map function for filters\<close>
   16.32 @@ -573,7 +573,7 @@
   16.33    by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
   16.34  
   16.35  lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
   16.36 -  unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
   16.37 +  unfolding filter_eq_iff eventually_Sup by (auto simp: eventually_principal)
   16.38  
   16.39  lemma INF_principal_finite: "finite X \<Longrightarrow> (INF x:X. principal (f x)) = principal (\<Inter>x\<in>X. f x)"
   16.40    by (induct X rule: finite_induct) auto
    17.1 --- a/src/HOL/GCD.thy	Wed Feb 17 21:51:55 2016 +0100
    17.2 +++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:56 2016 +0100
    17.3 @@ -1990,6 +1990,8 @@
    17.4  definition
    17.5    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
    17.6  
    17.7 +interpretation bla: semilattice_neutr_set gcd "0::nat" ..
    17.8 +
    17.9  instance ..
   17.10  
   17.11  end
   17.12 @@ -2012,19 +2014,7 @@
   17.13  
   17.14  interpretation gcd_lcm_complete_lattice_nat:
   17.15    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
   17.16 -rewrites "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
   17.17 -  and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
   17.18 -proof -
   17.19 -  show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
   17.20 -    by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
   17.21 -  then interpret gcd_lcm_complete_lattice_nat:
   17.22 -    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
   17.23 -  from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
   17.24 -  from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" .
   17.25 -qed
   17.26 -
   17.27 -declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
   17.28 -declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del]
   17.29 +  by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
   17.30  
   17.31  lemma Lcm_empty_nat:
   17.32    "Lcm {} = (1::nat)"
    18.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Feb 17 21:51:55 2016 +0100
    18.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Feb 17 21:51:56 2016 +0100
    18.3 @@ -253,10 +253,10 @@
    18.4  done
    18.5  
    18.6  lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A"
    18.7 -by (simp add: image_eq_UN surj_f_inv_f)
    18.8 +  by (simp add: surj_f_inv_f image_comp comp_def)
    18.9  
   18.10  lemma image_inv_f_f: "inj f ==> inv f ` (f ` A) = A"
   18.11 -  by (simp add: image_eq_UN)
   18.12 +  by simp
   18.13  
   18.14  lemma inv_image_comp: "inj f ==> inv f ` (f ` X) = X"
   18.15    by (fact image_inv_f_f)
    19.1 --- a/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Feb 17 21:51:55 2016 +0100
    19.2 +++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Feb 17 21:51:56 2016 +0100
    19.3 @@ -111,7 +111,8 @@
    19.4  apply(rule conjI)
    19.5   apply (blast dest: L3_5i)
    19.6  apply(simp add: SEM_def sem_def id_def)
    19.7 -apply (blast dest: Basic_ntran rtrancl_imp_UN_relpow)
    19.8 +apply (auto dest: Basic_ntran rtrancl_imp_UN_relpow)
    19.9 +apply blast
   19.10  done
   19.11  
   19.12  lemma atom_hoare_sound [rule_format]:
    20.1 --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Feb 17 21:51:55 2016 +0100
    20.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Feb 17 21:51:56 2016 +0100
    20.3 @@ -1266,23 +1266,23 @@
    20.4  apply simp
    20.5  apply clarify
    20.6  apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))")
    20.7 - apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> \<Turnstile> (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption)
    20.8 + apply(erule_tac x=xa and P="\<lambda>i. H i \<longrightarrow> \<Turnstile> (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption)
    20.9   apply(simp add:com_validity_def)
   20.10   apply(erule_tac x=s in allE)
   20.11 - apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (I j) \<in> cp (J j) s" for H I J in allE,simp)
   20.12 - apply(drule_tac c="clist!i" in subsetD)
   20.13 + apply(erule_tac x=xa and P="\<lambda>j. H j \<longrightarrow> (I j) \<in> cp (J j) s" for H I J in allE,simp)
   20.14 + apply(drule_tac c="clist!xa" in subsetD)
   20.15    apply (force simp add:Com_def)
   20.16   apply(simp add:comm_def conjoin_def same_program_def del:last.simps)
   20.17   apply clarify
   20.18   apply(erule_tac x="length x - 1" and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in allE)
   20.19   apply (simp add:All_None_def same_length_def)
   20.20 - apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> length(J j)=(K j)" for H J K in allE)
   20.21 + apply(erule_tac x=xa and P="\<lambda>j. H j \<longrightarrow> length(J j)=(K j)" for H J K in allE)
   20.22   apply(subgoal_tac "length x - 1 < length x",simp)
   20.23    apply(case_tac "x\<noteq>[]")
   20.24     apply(simp add: last_conv_nth)
   20.25 -   apply(erule_tac x="clist!i" in ballE)
   20.26 +   apply(erule_tac x="clist!xa" in ballE)
   20.27      apply(simp add:same_state_def)
   20.28 -    apply(subgoal_tac "clist!i\<noteq>[]")
   20.29 +    apply(subgoal_tac "clist!xa\<noteq>[]")
   20.30       apply(simp add: last_conv_nth)
   20.31      apply(case_tac x)
   20.32       apply (force simp add:par_cp_def)
   20.33 @@ -1297,19 +1297,19 @@
   20.34  apply(rule conjI)
   20.35   apply(simp add:conjoin_def same_state_def par_cp_def)
   20.36   apply clarify
   20.37 - apply(erule_tac x=ia and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
   20.38 + apply(erule_tac x=i and P="\<lambda>j. T j \<longrightarrow> (\<forall>i. H j i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for T H d e in allE,simp)
   20.39   apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
   20.40   apply(case_tac x,simp+)
   20.41   apply (simp add:par_assum_def)
   20.42   apply clarify
   20.43 - apply(drule_tac c="snd (clist ! ia ! 0)" in subsetD)
   20.44 + apply(drule_tac c="snd (clist ! i ! 0)" in subsetD)
   20.45   apply assumption
   20.46   apply simp
   20.47  apply clarify
   20.48 -apply(erule_tac x=ia in all_dupE)
   20.49 +apply(erule_tac x=i in all_dupE)
   20.50  apply(rule subsetD, erule mp, assumption)
   20.51  apply(erule_tac pre=pre and rely=rely and x=x and s=s in  three)
   20.52 - apply(erule_tac x=ic in allE,erule mp)
   20.53 + apply(erule_tac x=ib in allE,erule mp)
   20.54   apply simp_all
   20.55   apply(simp add:ParallelCom_def)
   20.56   apply(force simp add:Com_def)
    21.1 --- a/src/HOL/IMP/Denotational.thy	Wed Feb 17 21:51:55 2016 +0100
    21.2 +++ b/src/HOL/IMP/Denotational.thy	Wed Feb 17 21:51:56 2016 +0100
    21.3 @@ -98,6 +98,9 @@
    21.4  theorem lfp_if_cont:
    21.5    assumes "cont f" shows "lfp f = (UN n. (f^^n) {})" (is "_ = ?U")
    21.6  proof
    21.7 +  from assms mono_if_cont
    21.8 +  have mono: "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" for n
    21.9 +    using funpow_decreasing [of n "Suc n"] by auto
   21.10    show "lfp f \<subseteq> ?U"
   21.11    proof (rule lfp_lowerbound)
   21.12      have "f ?U = (UN n. (f^^Suc n){})"
   21.13 @@ -105,7 +108,7 @@
   21.14        by(simp add: cont_def)
   21.15      also have "\<dots> = (f^^0){} \<union> \<dots>" by simp
   21.16      also have "\<dots> = ?U"
   21.17 -      using assms funpow_decreasing le_SucI mono_if_cont by blast
   21.18 +      using mono by auto (metis funpow_simps_right(2) funpow_swap1 o_apply)
   21.19      finally show "f ?U \<subseteq> ?U" by simp
   21.20    qed
   21.21  next
    22.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Wed Feb 17 21:51:55 2016 +0100
    22.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Wed Feb 17 21:51:56 2016 +0100
    22.3 @@ -123,7 +123,11 @@
    22.4  
    22.5  lemma cUnion_transfer [transfer_rule]:
    22.6    "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) Union cUnion"
    22.7 -unfolding cUnion_def[abs_def] Union_conv_UNION[abs_def] by transfer_prover
    22.8 +proof -
    22.9 +  have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. UNION A id) (\<lambda>A. cUNION A id)"
   22.10 +    by transfer_prover
   22.11 +  then show ?thesis by (simp add: cUnion_def [symmetric])
   22.12 +qed
   22.13  
   22.14  lemmas cset_eqI = set_eqI[Transfer.transferred]
   22.15  lemmas cset_eq_iff[no_atp] = set_eq_iff[Transfer.transferred]
   22.16 @@ -342,11 +346,9 @@
   22.17  lemmas cin_mono = in_mono[Transfer.transferred]
   22.18  lemmas cLeast_mono = Least_mono[Transfer.transferred]
   22.19  lemmas cequalityI = equalityI[Transfer.transferred]
   22.20 -lemmas cUnion_cimage_eq [simp] = Union_image_eq[Transfer.transferred]
   22.21  lemmas cUN_iff [simp] = UN_iff[Transfer.transferred]
   22.22  lemmas cUN_I [intro] = UN_I[Transfer.transferred]
   22.23  lemmas cUN_E [elim!] = UN_E[Transfer.transferred]
   22.24 -lemmas cimage_eq_cUN = image_eq_UN[Transfer.transferred]
   22.25  lemmas cUN_upper = UN_upper[Transfer.transferred]
   22.26  lemmas cUN_least = UN_least[Transfer.transferred]
   22.27  lemmas cUN_cinsert_distrib = UN_insert_distrib[Transfer.transferred]
    23.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Feb 17 21:51:55 2016 +0100
    23.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Feb 17 21:51:56 2016 +0100
    23.3 @@ -2002,12 +2002,11 @@
    23.4  proof cases
    23.5    assume "(SUP i:I. f i) = - \<infinity>"
    23.6    moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
    23.7 -    unfolding Sup_eq_MInfty Sup_image_eq[symmetric] by auto
    23.8 +    unfolding Sup_eq_MInfty by auto
    23.9    ultimately show ?thesis
   23.10      by (cases c) (auto simp: \<open>I \<noteq> {}\<close>)
   23.11  next
   23.12    assume "(SUP i:I. f i) \<noteq> - \<infinity>" then show ?thesis
   23.13 -    unfolding Sup_image_eq[symmetric]
   23.14      by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
   23.15         (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>)
   23.16  qed
   23.17 @@ -2130,7 +2129,6 @@
   23.18      by simp
   23.19  next
   23.20    assume "(SUP i:I. f i) \<noteq> 0" then show ?thesis
   23.21 -    unfolding SUP_def
   23.22      by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
   23.23         (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close>
   23.24               intro!: ereal_mult_left_mono c)
    24.1 --- a/src/HOL/Library/FSet.thy	Wed Feb 17 21:51:55 2016 +0100
    24.2 +++ b/src/HOL/Library/FSet.thy	Wed Feb 17 21:51:56 2016 +0100
    24.3 @@ -147,7 +147,7 @@
    24.4    parametric right_total_Compl_transfer Compl_transfer by simp
    24.5  
    24.6  instance
    24.7 -  by (standard, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
    24.8 +  by (standard; transfer) (simp_all add: Diff_eq)
    24.9  
   24.10  end
   24.11  
    25.1 --- a/src/HOL/Library/Finite_Lattice.thy	Wed Feb 17 21:51:55 2016 +0100
    25.2 +++ b/src/HOL/Library/Finite_Lattice.thy	Wed Feb 17 21:51:56 2016 +0100
    25.3 @@ -116,12 +116,12 @@
    25.4  lemma finite_Inf_prod:
    25.5    "Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
    25.6      Finite_Set.fold inf top A"
    25.7 -  by (metis Inf_fold_inf finite_code)
    25.8 +  by (metis Inf_fold_inf finite)
    25.9  
   25.10  lemma finite_Sup_prod:
   25.11    "Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
   25.12      Finite_Set.fold sup bot A"
   25.13 -  by (metis Sup_fold_sup finite_code)
   25.14 +  by (metis Sup_fold_sup finite)
   25.15  
   25.16  instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
   25.17    by standard (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
   25.18 @@ -130,20 +130,20 @@
   25.19  already form a finite lattice.\<close>
   25.20  
   25.21  lemma finite_bot_fun: "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
   25.22 -  by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
   25.23 +  by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite)
   25.24  
   25.25  lemma finite_top_fun: "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
   25.26 -  by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
   25.27 +  by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite)
   25.28  
   25.29  lemma finite_Inf_fun:
   25.30    "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
   25.31      Finite_Set.fold inf top A"
   25.32 -  by (metis Inf_fold_inf finite_code)
   25.33 +  by (metis Inf_fold_inf finite)
   25.34  
   25.35  lemma finite_Sup_fun:
   25.36    "Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
   25.37      Finite_Set.fold sup bot A"
   25.38 -  by (metis Sup_fold_sup finite_code)
   25.39 +  by (metis Sup_fold_sup finite)
   25.40  
   25.41  instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
   25.42    by standard (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
   25.43 @@ -165,11 +165,7 @@
   25.44  
   25.45  lemma finite_distrib_lattice_complete_inf_Sup:
   25.46    "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
   25.47 -  apply (rule finite_induct)
   25.48 -  apply (metis finite_code)
   25.49 -  apply (metis SUP_empty Sup_empty inf_bot_right)
   25.50 -  apply (metis SUP_insert Sup_insert inf_sup_distrib1)
   25.51 -  done
   25.52 +  using finite [of A] by induct (simp_all add: inf_sup_distrib1)
   25.53  
   25.54  instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
   25.55  proof
    26.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Wed Feb 17 21:51:55 2016 +0100
    26.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Feb 17 21:51:56 2016 +0100
    26.3 @@ -3181,7 +3181,7 @@
    26.4    let ?KM = "{(k,m). k + m \<le> n}"
    26.5    let ?f = "\<lambda>s. UNION {(0::nat)..s} (\<lambda>i. {(i,s - i)})"
    26.6    have th0: "?KM = UNION {0..n} ?f"
    26.7 -    by (auto simp add: set_eq_iff Bex_def)
    26.8 +    by auto
    26.9    show "?l = ?r "
   26.10      unfolding th0
   26.11      apply (subst setsum.UNION_disjoint)
    27.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Wed Feb 17 21:51:55 2016 +0100
    27.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Wed Feb 17 21:51:56 2016 +0100
    27.3 @@ -380,7 +380,7 @@
    27.4    note * = this
    27.5  
    27.6    have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))"
    27.7 -    unfolding Liminf_def SUP_def
    27.8 +    unfolding Liminf_def
    27.9      by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
   27.10         (auto intro: eventually_True)
   27.11    also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
   27.12 @@ -405,7 +405,7 @@
   27.13    note * = this
   27.14  
   27.15    have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))"
   27.16 -    unfolding Limsup_def INF_def
   27.17 +    unfolding Limsup_def
   27.18      by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
   27.19         (auto intro: eventually_True)
   27.20    also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
   27.21 @@ -429,7 +429,7 @@
   27.22        by auto
   27.23    qed
   27.24    have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
   27.25 -    unfolding Limsup_def INF_def
   27.26 +    unfolding Limsup_def
   27.27      by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   27.28         (auto intro: eventually_True)
   27.29    also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
   27.30 @@ -455,7 +455,7 @@
   27.31    note * = this
   27.32  
   27.33    have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))"
   27.34 -    unfolding Liminf_def SUP_def
   27.35 +    unfolding Liminf_def
   27.36      by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   27.37         (auto intro: eventually_True)
   27.38    also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
    28.1 --- a/src/HOL/Library/Lub_Glb.thy	Wed Feb 17 21:51:55 2016 +0100
    28.2 +++ b/src/HOL/Library/Lub_Glb.thy	Wed Feb 17 21:51:56 2016 +0100
    28.3 @@ -230,7 +230,7 @@
    28.4      by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle)
    28.5    also have "(SUP i. X i) = u"
    28.6      using isLub_cSup[of "range X"] u[THEN isLubD1]
    28.7 -    by (intro isLub_unique[OF _ u]) (auto simp add: SUP_def image_def eq_commute)
    28.8 +    by (intro isLub_unique[OF _ u]) (auto simp add: image_def eq_commute)
    28.9    finally show ?thesis .
   28.10  qed
   28.11  
    29.1 --- a/src/HOL/Library/Option_ord.thy	Wed Feb 17 21:51:55 2016 +0100
    29.2 +++ b/src/HOL/Library/Option_ord.thy	Wed Feb 17 21:51:56 2016 +0100
    29.3 @@ -289,7 +289,7 @@
    29.4    show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
    29.5    proof (cases a)
    29.6      case None
    29.7 -    then show ?thesis by (simp add: INF_def)
    29.8 +    then show ?thesis by simp
    29.9    next
   29.10      case (Some c)
   29.11      show ?thesis
   29.12 @@ -303,13 +303,13 @@
   29.13        from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b\<in>Option.these B. c \<squnion> b)" by simp
   29.14        then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x\<in>Some ` Option.these B. Some c \<squnion> x)"
   29.15          by (simp add: Some_INF Some_Inf comp_def)
   29.16 -      with Some B show ?thesis by (simp add: Some_image_these_eq)
   29.17 +      with Some B show ?thesis by (simp add: Some_image_these_eq cong del: strong_INF_cong)
   29.18      qed
   29.19    qed
   29.20    show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   29.21    proof (cases a)
   29.22      case None
   29.23 -    then show ?thesis by (simp add: SUP_def image_constant_conv bot_option_def)
   29.24 +    then show ?thesis by (simp add: image_constant_conv bot_option_def cong del: strong_SUP_cong)
   29.25    next
   29.26      case (Some c)
   29.27      show ?thesis
   29.28 @@ -332,7 +332,7 @@
   29.29        ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x\<in>Some ` Option.these B. Some c \<sqinter> x)"
   29.30          by (simp add: Some_SUP Some_Sup comp_def)
   29.31        with Some show ?thesis
   29.32 -        by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib)
   29.33 +        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)
   29.34      qed
   29.35    qed
   29.36  qed
    30.1 --- a/src/HOL/Library/Product_Order.thy	Wed Feb 17 21:51:55 2016 +0100
    30.2 +++ b/src/HOL/Library/Product_Order.thy	Wed Feb 17 21:51:56 2016 +0100
    30.3 @@ -179,7 +179,6 @@
    30.4  instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
    30.5      conditionally_complete_lattice
    30.6    by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
    30.7 -    INF_def SUP_def simp del: Inf_image_eq Sup_image_eq
    30.8      intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
    30.9  
   30.10  instance prod :: (complete_lattice, complete_lattice) complete_lattice
   30.11 @@ -211,10 +210,10 @@
   30.12    using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def)
   30.13  
   30.14  lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
   30.15 -  unfolding SUP_def Sup_prod_def by (simp add: comp_def)
   30.16 +  unfolding Sup_prod_def by (simp add: comp_def)
   30.17  
   30.18  lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
   30.19 -  unfolding INF_def Inf_prod_def by (simp add: comp_def)
   30.20 +  unfolding Inf_prod_def by (simp add: comp_def)
   30.21  
   30.22  
   30.23  text \<open>Alternative formulations for set infima and suprema over the product
   30.24 @@ -222,11 +221,11 @@
   30.25  
   30.26  lemma INF_prod_alt_def:
   30.27    "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))"
   30.28 -  unfolding INF_def Inf_prod_def by simp
   30.29 +  unfolding Inf_prod_def by simp
   30.30  
   30.31  lemma SUP_prod_alt_def:
   30.32    "SUPREMUM A f = (SUPREMUM A (fst o f), SUPREMUM A (snd o f))"
   30.33 -  unfolding SUP_def Sup_prod_def by simp
   30.34 +  unfolding Sup_prod_def by simp
   30.35  
   30.36  
   30.37  subsection \<open>Complete distributive lattices\<close>
    31.1 --- a/src/HOL/Lifting_Set.thy	Wed Feb 17 21:51:55 2016 +0100
    31.2 +++ b/src/HOL/Lifting_Set.thy	Wed Feb 17 21:51:56 2016 +0100
    31.3 @@ -138,7 +138,7 @@
    31.4  
    31.5  lemma UNION_transfer [transfer_rule]:
    31.6    "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
    31.7 -  unfolding Union_image_eq [symmetric, abs_def] by transfer_prover
    31.8 +  by transfer_prover
    31.9  
   31.10  lemma Ball_transfer [transfer_rule]:
   31.11    "(rel_set A ===> (A ===> op =) ===> op =) Ball Ball"
   31.12 @@ -176,11 +176,11 @@
   31.13  
   31.14  lemma INF_parametric [transfer_rule]:
   31.15    "(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) INFIMUM INFIMUM"
   31.16 -  unfolding INF_def [abs_def] by transfer_prover
   31.17 +  by transfer_prover
   31.18  
   31.19  lemma SUP_parametric [transfer_rule]:
   31.20    "(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) SUPREMUM SUPREMUM"
   31.21 -  unfolding SUP_def [abs_def] by transfer_prover
   31.22 +  by transfer_prover
   31.23  
   31.24  
   31.25  subsubsection \<open>Rules requiring bi-unique, bi-total or right-total relations\<close>
    32.1 --- a/src/HOL/List.thy	Wed Feb 17 21:51:55 2016 +0100
    32.2 +++ b/src/HOL/List.thy	Wed Feb 17 21:51:56 2016 +0100
    32.3 @@ -6774,7 +6774,7 @@
    32.4  
    32.5  lemma set_relcomp [code]:
    32.6    "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
    32.7 -  by (auto simp add: Bex_def)
    32.8 +  by auto (auto simp add: Bex_def image_def)
    32.9  
   32.10  lemma wf_set [code]:
   32.11    "wf (set xs) = acyclic (set xs)"
    33.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Wed Feb 17 21:51:55 2016 +0100
    33.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Wed Feb 17 21:51:56 2016 +0100
    33.3 @@ -116,7 +116,7 @@
    33.4      also assume "dist f g = 0"
    33.5      finally show "f = g"
    33.6        by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse)
    33.7 -  qed (auto simp: dist_bcontfun_def SUP_def simp del: Sup_image_eq intro!: cSup_eq)
    33.8 +  qed (auto simp: dist_bcontfun_def intro!: cSup_eq)
    33.9    show "dist f g \<le> dist f h + dist g h"
   33.10    proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
   33.11      fix x
   33.12 @@ -374,7 +374,7 @@
   33.13      ultimately
   33.14      show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
   33.15        by (simp add: norm_bcontfun_def dist_bcontfun_def norm_conv_dist Abs_bcontfun_inverse
   33.16 -                    zero_bcontfun_def const_bcontfun SUP_def del: Sup_image_eq)
   33.17 +        zero_bcontfun_def const_bcontfun image_image) presburger
   33.18    qed
   33.19  qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
   33.20  
    34.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Feb 17 21:51:55 2016 +0100
    34.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Feb 17 21:51:56 2016 +0100
    34.3 @@ -6690,7 +6690,7 @@
    34.4      using \<open>open s\<close>
    34.5      apply (simp add: open_contains_ball Ball_def)
    34.6      apply (erule all_forward)
    34.7 -    using "*" by blast
    34.8 +    using "*" by auto blast+
    34.9    have 2: "closedin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
   34.10      using assms
   34.11      by (auto intro: continuous_closed_in_preimage_constant holomorphic_on_imp_continuous_on holomorphic_higher_deriv)
    35.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Feb 17 21:51:55 2016 +0100
    35.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Feb 17 21:51:56 2016 +0100
    35.3 @@ -421,13 +421,13 @@
    35.4  lemma interval_upperbound[simp]:
    35.5    "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
    35.6      interval_upperbound (cbox a b) = (b::'a::euclidean_space)"
    35.7 -  unfolding interval_upperbound_def euclidean_representation_setsum cbox_def SUP_def
    35.8 +  unfolding interval_upperbound_def euclidean_representation_setsum cbox_def
    35.9    by (safe intro!: cSup_eq) auto
   35.10  
   35.11  lemma interval_lowerbound[simp]:
   35.12    "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
   35.13      interval_lowerbound (cbox a b) = (a::'a::euclidean_space)"
   35.14 -  unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def INF_def
   35.15 +  unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def
   35.16    by (safe intro!: cInf_eq) auto
   35.17  
   35.18  lemmas interval_bounds = interval_upperbound interval_lowerbound
   35.19 @@ -436,7 +436,7 @@
   35.20    fixes X::"real set"
   35.21    shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X"
   35.22      and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X"
   35.23 -  by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def)
   35.24 +  by (auto simp: interval_upperbound_def interval_lowerbound_def)
   35.25  
   35.26  lemma interval_bounds'[simp]:
   35.27    assumes "cbox a b \<noteq> {}"
   35.28 @@ -496,7 +496,7 @@
   35.29      using assms box_ne_empty(1) content_cbox by blast
   35.30  
   35.31  lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
   35.32 -  by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def content_def)
   35.33 +  by (auto simp: interval_upperbound_def interval_lowerbound_def content_def)
   35.34  
   35.35  lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})"
   35.36    by (auto simp: content_real)
   35.37 @@ -856,7 +856,7 @@
   35.38        by auto
   35.39      show "\<Union>?A = s1 \<inter> s2"
   35.40        apply (rule set_eqI)
   35.41 -      unfolding * and Union_image_eq UN_iff
   35.42 +      unfolding * and UN_iff
   35.43        using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)]
   35.44        apply auto
   35.45        done
   35.46 @@ -9394,7 +9394,6 @@
   35.47      prefer 3
   35.48      apply assumption
   35.49      apply rule
   35.50 -    apply (rule finite_imageI)
   35.51      apply (rule r)
   35.52      apply safe
   35.53      apply (drule qq)
    36.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Feb 17 21:51:55 2016 +0100
    36.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Feb 17 21:51:56 2016 +0100
    36.3 @@ -2752,7 +2752,7 @@
    36.4  lemma infnorm_Max:
    36.5    fixes x :: "'a::euclidean_space"
    36.6    shows "infnorm x = Max ((\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis)"
    36.7 -  by (simp add: infnorm_def infnorm_set_image cSup_eq_Max del: Sup_image_eq)
    36.8 +  by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)
    36.9  
   36.10  lemma infnorm_set_lemma:
   36.11    fixes x :: "'a::euclidean_space"
    37.1 --- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Wed Feb 17 21:51:55 2016 +0100
    37.2 +++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Wed Feb 17 21:51:56 2016 +0100
    37.3 @@ -38,13 +38,11 @@
    37.4    assume "X \<noteq> {}"
    37.5    hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
    37.6    thus "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
    37.7 -    by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
    37.8 -      simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq
    37.9 +    by (auto simp: eucl_Inf eucl_Sup eucl_le
   37.10        intro!: cInf_greatest cSup_least)
   37.11  qed (force intro!: cInf_lower cSup_upper
   37.12        simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
   37.13 -        eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
   37.14 -      simp del: Inf_class.Inf_image_eq Sup_class.Sup_image_eq)+
   37.15 +        eucl_Inf eucl_Sup eucl_le)+
   37.16  
   37.17  lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
   37.18    and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
   37.19 @@ -89,7 +87,7 @@
   37.20    shows "Sup s = X"
   37.21    using assms
   37.22    unfolding eucl_Sup euclidean_representation_setsum
   37.23 -  by (auto simp: Sup_class.SUP_def simp del: Sup_class.Sup_image_eq intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
   37.24 +  by (auto intro!: conditionally_complete_lattice_class.cSup_eq_maximum)
   37.25  
   37.26  lemma Inf_eq_minimum_componentwise:
   37.27    assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b"
   37.28 @@ -98,7 +96,7 @@
   37.29    shows "Inf s = X"
   37.30    using assms
   37.31    unfolding eucl_Inf euclidean_representation_setsum
   37.32 -  by (auto simp: Inf_class.INF_def simp del: Inf_class.Inf_image_eq intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
   37.33 +  by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
   37.34  
   37.35  end
   37.36  
   37.37 @@ -117,10 +115,9 @@
   37.38        and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b"
   37.39      by auto
   37.40    hence "Inf ?proj = x \<bullet> b"
   37.41 -    by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum simp del: Inf_class.Inf_image_eq)
   37.42 +    by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum)
   37.43    hence "x \<bullet> b = Inf X \<bullet> b"
   37.44 -    by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> setsum.delta
   37.45 -      simp del: Inf_class.Inf_image_eq
   37.46 +    by (auto simp: eucl_Inf inner_setsum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> setsum.delta
   37.47        cong: if_cong)
   37.48    with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast
   37.49  qed
   37.50 @@ -140,10 +137,10 @@
   37.51        and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b"
   37.52      by auto
   37.53    hence "Sup ?proj = x \<bullet> b"
   37.54 -    by (auto intro!: cSup_eq_maximum simp del: Sup_image_eq)
   37.55 +    by (auto intro!: cSup_eq_maximum)
   37.56    hence "x \<bullet> b = Sup X \<bullet> b"
   37.57 -    by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> setsum.delta
   37.58 -      simp del: Sup_image_eq cong: if_cong)
   37.59 +    by (auto simp: eucl_Sup[where 'a='a] inner_setsum_left inner_Basis if_distrib \<open>b \<in> Basis\<close> setsum.delta
   37.60 +      cong: if_cong)
   37.61    with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast
   37.62  qed
   37.63  
   37.64 @@ -152,7 +149,7 @@
   37.65    by (auto)
   37.66  
   37.67  instance real :: ordered_euclidean_space
   37.68 -  by standard (auto simp: INF_def SUP_def)
   37.69 +  by standard auto
   37.70  
   37.71  lemma in_Basis_prod_iff:
   37.72    fixes i::"'a::euclidean_space*'b::euclidean_space"
    38.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 17 21:51:55 2016 +0100
    38.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 17 21:51:56 2016 +0100
    38.3 @@ -532,7 +532,6 @@
    38.4  lemma closedin_INT[intro]:
    38.5    assumes "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> closedin U (B x)"
    38.6    shows "closedin U (\<Inter>x\<in>A. B x)"
    38.7 -  unfolding Inter_image_eq [symmetric]
    38.8    apply (rule closedin_Inter)
    38.9    using assms
   38.10    apply auto
   38.11 @@ -605,7 +604,7 @@
   38.12      ultimately have "?L (\<Union>K)" by blast
   38.13    }
   38.14    ultimately show ?thesis
   38.15 -    unfolding subset_eq mem_Collect_eq istopology_def by blast
   38.16 +    unfolding subset_eq mem_Collect_eq istopology_def by auto
   38.17  qed
   38.18  
   38.19  lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)"
   38.20 @@ -2426,7 +2425,7 @@
   38.21        fix y
   38.22        assume "y \<in> {x<..} \<inter> I"
   38.23        with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
   38.24 -        by (auto intro!: cInf_lower bdd_belowI2 simp del: Inf_image_eq)
   38.25 +        by (auto intro!: cInf_lower bdd_belowI2)
   38.26        with a have "a < f y"
   38.27          by (blast intro: less_le_trans)
   38.28      }
   38.29 @@ -3802,7 +3801,7 @@
   38.30  
   38.31  lemma compact_UN [intro]:
   38.32    "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
   38.33 -  unfolding SUP_def by (rule compact_Union) auto
   38.34 +  by (rule compact_Union) auto
   38.35  
   38.36  lemma closed_inter_compact [intro]:
   38.37    assumes "closed s"
   38.38 @@ -4090,7 +4089,7 @@
   38.39          by metis
   38.40        def X \<equiv> "\<lambda>n. X' (from_nat_into A ` {.. n})"
   38.41        have X: "\<And>n. X n \<in> U - (\<Union>i\<le>n. from_nat_into A i)"
   38.42 -        using \<open>A \<noteq> {}\<close> unfolding X_def SUP_def by (intro T) (auto intro: from_nat_into)
   38.43 +        using \<open>A \<noteq> {}\<close> unfolding X_def by (intro T) (auto intro: from_nat_into)
   38.44        then have "range X \<subseteq> U"
   38.45          by auto
   38.46        with subseq[of X] obtain r x where "x \<in> U" and r: "subseq r" "(X \<circ> r) \<longlonglongrightarrow> x"
   38.47 @@ -4198,7 +4197,7 @@
   38.48    then have s: "\<And>x. x \<in> s \<Longrightarrow> \<exists>U. x\<in>U \<and> open U \<and> finite (U \<inter> t)" by metis
   38.49    have "s \<subseteq> \<Union>C"
   38.50      using \<open>t \<subseteq> s\<close>
   38.51 -    unfolding C_def Union_image_eq
   38.52 +    unfolding C_def
   38.53      apply (safe dest!: s)
   38.54      apply (rule_tac a="U \<inter> t" in UN_I)
   38.55      apply (auto intro!: interiorI simp add: finite_subset)
   38.56 @@ -4211,7 +4210,7 @@
   38.57      by (rule countably_compactE)
   38.58    then obtain E where E: "E \<subseteq> {F. finite F \<and> F \<subseteq> t }" "finite E"
   38.59      and s: "s \<subseteq> (\<Union>F\<in>E. interior (F \<union> (- t)))"
   38.60 -    by (metis (lifting) Union_image_eq finite_subset_image C_def)
   38.61 +    by (metis (lifting) finite_subset_image C_def)
   38.62    from s \<open>t \<subseteq> s\<close> have "t \<subseteq> \<Union>E"
   38.63      using interior_subset by blast
   38.64    moreover have "finite (\<Union>E)"
   38.65 @@ -4348,7 +4347,7 @@
   38.66      from Rats_dense_in_real[OF \<open>0 < e / 2\<close>] obtain r where "r \<in> \<rat>" "0 < r" "r < e / 2"
   38.67        by auto
   38.68      from f[rule_format, of r] \<open>0 < r\<close> \<open>x \<in> s\<close> obtain k where "k \<in> f r" "x \<in> ball k r"
   38.69 -      unfolding Union_image_eq by auto
   38.70 +      by auto
   38.71      from \<open>r \<in> \<rat>\<close> \<open>0 < r\<close> \<open>k \<in> f r\<close> have "ball k r \<in> K"
   38.72        by (auto simp: K_def)
   38.73      then show "\<exists>b\<in>K. x \<in> b \<and> b \<inter> s \<subseteq> T"
   38.74 @@ -7412,7 +7411,7 @@
   38.75  lemma diameter_cbox:
   38.76    fixes a b::"'a::euclidean_space"
   38.77    shows "(\<forall>i \<in> Basis. a \<bullet> i \<le> b \<bullet> i) \<Longrightarrow> diameter (cbox a b) = dist a b"
   38.78 -  by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono
   38.79 +  by (force simp add: diameter_def intro!: cSup_eq_maximum setL2_mono
   38.80       simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
   38.81  
   38.82  lemma eucl_less_eq_halfspaces:
    39.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Wed Feb 17 21:51:55 2016 +0100
    39.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Wed Feb 17 21:51:56 2016 +0100
    39.3 @@ -259,7 +259,7 @@
    39.4        (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
    39.5     ==> finprod G f (\<Union>C) = finprod G (finprod G f) C"
    39.6    apply (frule finprod_UN_disjoint [of C id f])
    39.7 -  apply (auto simp add: SUP_def)
    39.8 +  apply auto
    39.9    done
   39.10  
   39.11  lemma (in comm_monoid) finprod_one:
    40.1 --- a/src/HOL/Probability/Caratheodory.thy	Wed Feb 17 21:51:55 2016 +0100
    40.2 +++ b/src/HOL/Probability/Caratheodory.thy	Wed Feb 17 21:51:56 2016 +0100
    40.3 @@ -396,8 +396,8 @@
    40.4    from \<open>outer_measure M f X \<noteq> \<infinity>\<close> have fin: "\<bar>outer_measure M f X\<bar> \<noteq> \<infinity>"
    40.5      using outer_measure_nonneg[OF posf, of X] by auto
    40.6    show ?thesis
    40.7 -    using Inf_ereal_close[OF fin[unfolded outer_measure_def INF_def], OF \<open>0 < e\<close>]
    40.8 -    unfolding INF_def[symmetric] outer_measure_def[symmetric] by (auto intro: less_imp_le)
    40.9 +    using Inf_ereal_close [OF fin [unfolded outer_measure_def], OF \<open>0 < e\<close>]
   40.10 +    by (auto intro: less_imp_le simp add: outer_measure_def)
   40.11  qed
   40.12  
   40.13  lemma (in ring_of_sets) countably_subadditive_outer_measure:
   40.14 @@ -574,7 +574,7 @@
   40.15    shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
   40.16  proof -
   40.17    have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M"
   40.18 -    using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image)
   40.19 +    using A by (auto simp: disjoint_family_on_disjoint_image)
   40.20    with \<open>volume M f\<close> have "f (\<Union>(A`I)) = (\<Sum>a\<in>A`I. f a)"
   40.21      unfolding volume_def by blast
   40.22    also have "\<dots> = (\<Sum>i\<in>I. f (A i))"
   40.23 @@ -713,7 +713,7 @@
   40.24      then have "disjoint_family F"
   40.25        using F'_disj by (auto simp: disjoint_family_on_def)
   40.26      moreover from F' have "(\<Union>i. F i) = \<Union>C"
   40.27 -      by (auto simp: F_def set_eq_iff split: split_if_asm)
   40.28 +      by (auto simp add: F_def split: split_if_asm) blast
   40.29      moreover have sets_F: "\<And>i. F i \<in> M"
   40.30        using F' sets_C by (auto simp: F_def)
   40.31      moreover note sets_C
   40.32 @@ -783,9 +783,10 @@
   40.33            by (auto simp: disjoint_family_on_def f_def)
   40.34          moreover
   40.35          have Ai_eq: "A i = (\<Union>x<card C. f x)"
   40.36 -          using f C Ai unfolding bij_betw_def by (simp add: Union_image_eq[symmetric])
   40.37 +          using f C Ai unfolding bij_betw_def by auto
   40.38          then have "\<Union>range f = A i"
   40.39 -          using f C Ai unfolding bij_betw_def by (auto simp: f_def)
   40.40 +          using f C Ai unfolding bij_betw_def
   40.41 +            by (auto simp add: f_def cong del: strong_SUP_cong)
   40.42          moreover 
   40.43          { have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
   40.44              using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
   40.45 @@ -841,7 +842,7 @@
   40.46      have "(\<Sum>n. \<mu>_r (A' n)) = (\<Sum>n. \<Sum>c\<in>C'. \<mu>_r (A' n \<inter> c))"
   40.47        using C' A'
   40.48        by (subst volume_finite_additive[symmetric, OF V(1)])
   40.49 -         (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq
   40.50 +         (auto simp: disjoint_def disjoint_family_on_def
   40.51                 intro!: G.Int G.finite_Union arg_cong[where f="\<lambda>X. suminf (\<lambda>i. \<mu>_r (X i))"] ext
   40.52                 intro: generated_ringI_Basic)
   40.53      also have "\<dots> = (\<Sum>c\<in>C'. \<Sum>n. \<mu>_r (A' n \<inter> c))"
   40.54 @@ -853,7 +854,7 @@
   40.55      also have "\<dots> = \<mu>_r (\<Union>C')"
   40.56        using C' Un_A
   40.57        by (subst volume_finite_additive[symmetric, OF V(1)])
   40.58 -         (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq 
   40.59 +         (auto simp: disjoint_family_on_def disjoint_def
   40.60                 intro: generated_ringI_Basic)
   40.61      finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)"
   40.62        using C' by simp
    41.1 --- a/src/HOL/Probability/Complete_Measure.thy	Wed Feb 17 21:51:55 2016 +0100
    41.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Wed Feb 17 21:51:56 2016 +0100
    41.3 @@ -205,7 +205,7 @@
    41.4      unfolding binary_def by (auto split: split_if_asm)
    41.5    show "emeasure M (main_part M (S \<union> T)) = emeasure M (main_part M S \<union> main_part M T)"
    41.6      using emeasure_main_part_UN[of "binary S T" M] assms
    41.7 -    unfolding range_binary_eq Un_range_binary UN by auto
    41.8 +    by (simp add: range_binary_eq, simp add: Un_range_binary UN)
    41.9  qed (auto intro: S T)
   41.10  
   41.11  lemma sets_completionI_sub:
    42.1 --- a/src/HOL/Probability/Embed_Measure.thy	Wed Feb 17 21:51:55 2016 +0100
    42.2 +++ b/src/HOL/Probability/Embed_Measure.thy	Wed Feb 17 21:51:56 2016 +0100
    42.3 @@ -36,7 +36,8 @@
    42.4    then obtain A' where "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M"
    42.5      by (auto simp: subset_eq choice_iff)
    42.6    moreover from this have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast
    42.7 -  ultimately show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}" by blast
    42.8 +  ultimately show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}"
    42.9 +    by simp blast
   42.10  qed (auto dest: sets.sets_into_space)
   42.11  
   42.12  lemma the_inv_into_vimage:
    43.1 --- a/src/HOL/Probability/Fin_Map.thy	Wed Feb 17 21:51:55 2016 +0100
    43.2 +++ b/src/HOL/Probability/Fin_Map.thy	Wed Feb 17 21:51:56 2016 +0100
    43.3 @@ -696,7 +696,7 @@
    43.4    have "A -` y \<inter> space (PiF I M) = (\<Union>J\<in>I. A -` y \<inter> space (PiF {J} M))"
    43.5      by (auto simp: space_PiF)
    43.6    also have "\<dots> \<in> sets (PiF I M)"
    43.7 -  proof
    43.8 +  proof (rule sets.finite_UN)
    43.9      show "finite I" by fact
   43.10      fix J assume "J \<in> I"
   43.11      with assms have "finite J" by simp
   43.12 @@ -1055,8 +1055,8 @@
   43.13            by (intro Pi'_cong) (simp_all add: S_union)
   43.14          also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>' j\<in>I. if i = j then A else S j (xs ! T j))"
   43.15            using T
   43.16 -          apply auto
   43.17 -          apply (simp_all add: Pi'_iff bchoice_iff)
   43.18 +          apply (auto simp del: Union_iff)
   43.19 +          apply (simp_all add: Pi'_iff bchoice_iff del: Union_iff)
   43.20            apply (erule conjE exE)+
   43.21            apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
   43.22            apply (auto simp: bij_betw_def)
    44.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Feb 17 21:51:55 2016 +0100
    44.2 +++ b/src/HOL/Probability/Independent_Family.thy	Wed Feb 17 21:51:56 2016 +0100
    44.3 @@ -491,11 +491,18 @@
    44.4          where a: "a = (\<Inter>k\<in>Ka. Ea k)" "finite Ka" "Ka \<noteq> {}" "Ka \<subseteq> I j" "\<And>k. k\<in>Ka \<Longrightarrow> Ea k \<in> E k" by auto
    44.5        fix b assume "b \<in> ?E j" then obtain Kb Eb
    44.6          where b: "b = (\<Inter>k\<in>Kb. Eb k)" "finite Kb" "Kb \<noteq> {}" "Kb \<subseteq> I j" "\<And>k. k\<in>Kb \<Longrightarrow> Eb k \<in> E k" by auto
    44.7 -      let ?A = "\<lambda>k. (if k \<in> Ka \<inter> Kb then Ea k \<inter> Eb k else if k \<in> Kb then Eb k else if k \<in> Ka then Ea k else {})"
    44.8 -      have "a \<inter> b = INTER (Ka \<union> Kb) ?A"
    44.9 -        by (simp add: a b set_eq_iff) auto
   44.10 +      let ?f = "\<lambda>k. (if k \<in> Ka \<inter> Kb then Ea k \<inter> Eb k else if k \<in> Kb then Eb k else if k \<in> Ka then Ea k else {})"
   44.11 +      have "Ka \<union> Kb = (Ka \<inter> Kb) \<union> (Kb - Ka) \<union> (Ka - Kb)"
   44.12 +        by blast
   44.13 +      moreover have "(\<Inter>x\<in>Ka \<inter> Kb. Ea x \<inter> Eb x) \<inter>
   44.14 +        (\<Inter>x\<in>Kb - Ka. Eb x) \<inter> (\<Inter>x\<in>Ka - Kb. Ea x) = (\<Inter>k\<in>Ka. Ea k) \<inter> (\<Inter>k\<in>Kb. Eb k)"
   44.15 +        by auto
   44.16 +      ultimately have "(\<Inter>k\<in>Ka \<union> Kb. ?f k) = (\<Inter>k\<in>Ka. Ea k) \<inter> (\<Inter>k\<in>Kb. Eb k)" (is "?lhs = ?rhs")
   44.17 +        by (simp only: image_Un Inter_Un_distrib) simp
   44.18 +      then have "a \<inter> b = (\<Inter>k\<in>Ka \<union> Kb. ?f k)"
   44.19 +        by (simp only: a(1) b(1))
   44.20        with a b \<open>j \<in> J\<close> Int_stableD[OF Int_stable] show "a \<inter> b \<in> ?E j"
   44.21 -        by (intro CollectI exI[of _ "Ka \<union> Kb"] exI[of _ ?A]) auto
   44.22 +        by (intro CollectI exI[of _ "Ka \<union> Kb"] exI[of _ ?f]) auto
   44.23      qed
   44.24    qed
   44.25    ultimately show ?thesis
   44.26 @@ -804,14 +811,18 @@
   44.27  proof -
   44.28    have [measurable]: "\<And>m. {x\<in>space M. P m x} \<in> sets M"
   44.29      using assms by (auto simp: indep_events_def)
   44.30 -  have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1"
   44.31 -    by (rule borel_0_1_law) fact
   44.32 +  have *: "(\<Inter>n. \<Union>m\<in>{n..}. {x \<in> space M. P m x}) \<in> events"
   44.33 +    by simp
   44.34 +  from assms have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 0 \<or> prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1"
   44.35 +    by (rule borel_0_1_law)
   44.36 +  also have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1 \<longleftrightarrow> (AE x in M. infinite {m. P m x})"
   44.37 +    using * by (simp add: prob_eq_1)
   44.38 +      (simp add: Bex_def infinite_nat_iff_unbounded_le)
   44.39    also have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 0 \<longleftrightarrow> (AE x in M. finite {m. P m x})"
   44.40 -    by (subst prob_eq_0) (auto simp add: finite_nat_iff_bounded Ball_def not_less[symmetric])
   44.41 -  also have "prob (\<Inter>n. \<Union>m\<in>{n..}. ?P m) = 1 \<longleftrightarrow> (AE x in M. infinite {m. P m x})"
   44.42 -    by (subst prob_eq_1) (simp_all add: Bex_def infinite_nat_iff_unbounded_le)
   44.43 +    using * by (simp add: prob_eq_0)
   44.44 +      (auto simp add: Ball_def finite_nat_iff_bounded not_less [symmetric])
   44.45    finally show ?thesis
   44.46 -    by metis
   44.47 +    by blast
   44.48  qed
   44.49  
   44.50  lemma (in prob_space) indep_sets_finite:
    45.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Feb 17 21:51:55 2016 +0100
    45.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Feb 17 21:51:56 2016 +0100
    45.3 @@ -181,7 +181,7 @@
    45.4  proof -
    45.5    have "Pi UNIV E = (\<Inter>i. emb UNIV {..i} (\<Pi>\<^sub>E j\<in>{..i}. E j))"
    45.6      using E E[THEN sets.sets_into_space]
    45.7 -    by (auto simp: prod_emb_def Pi_iff extensional_def) blast
    45.8 +    by (auto simp: prod_emb_def Pi_iff extensional_def)
    45.9    with E show ?thesis by auto
   45.10  qed
   45.11  
   45.12 @@ -194,7 +194,7 @@
   45.13      using E by (simp add: measure_PiM_emb)
   45.14    moreover have "Pi UNIV E = (\<Inter>n. ?E n)"
   45.15      using E E[THEN sets.sets_into_space]
   45.16 -    by (auto simp: prod_emb_def extensional_def Pi_iff) blast
   45.17 +    by (auto simp: prod_emb_def extensional_def Pi_iff)
   45.18    moreover have "range ?E \<subseteq> sets S"
   45.19      using E by auto
   45.20    moreover have "decseq ?E"
    46.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Feb 17 21:51:55 2016 +0100
    46.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Feb 17 21:51:56 2016 +0100
    46.3 @@ -536,7 +536,7 @@
    46.4    moreover have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0"
    46.5      by (rule emeasure_UN_eq_0) auto
    46.6    ultimately have "emeasure lborel A \<le> 0" using emeasure_mono
    46.7 -    by (metis assms bot.extremum_unique emeasure_empty image_eq_UN range_from_nat_into sets.empty_sets)
    46.8 +    by (smt UN_E emeasure_empty equalityI from_nat_into order_refl singletonD subsetI)
    46.9    thus ?thesis by (auto simp add: emeasure_le_0_iff)
   46.10  qed
   46.11  
    47.1 --- a/src/HOL/Probability/Measurable.thy	Wed Feb 17 21:51:55 2016 +0100
    47.2 +++ b/src/HOL/Probability/Measurable.thy	Wed Feb 17 21:51:56 2016 +0100
    47.3 @@ -152,7 +152,7 @@
    47.4      "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Union>i\<in>X. N x i))"
    47.5      "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<forall>i\<in>X. P x i)"
    47.6      "(\<And>i. i \<in> X \<Longrightarrow> pred M (\<lambda>x. P x i)) \<Longrightarrow> pred M (\<lambda>x. \<exists>i\<in>X. P x i)"
    47.7 -  by (auto simp: Bex_def Ball_def)
    47.8 +  by simp_all (auto simp: Bex_def Ball_def)
    47.9  
   47.10  lemma pred_intros_finite[measurable (raw)]:
   47.11    "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> pred M (\<lambda>x. x \<in> N x i)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (\<Inter>i\<in>I. N x i))"
    48.1 --- a/src/HOL/Probability/Measure_Space.thy	Wed Feb 17 21:51:55 2016 +0100
    48.2 +++ b/src/HOL/Probability/Measure_Space.thy	Wed Feb 17 21:51:56 2016 +0100
    48.3 @@ -884,7 +884,7 @@
    48.4    have "(\<Union>i\<in>I. N i) = \<Union>(N ` range (from_nat_into I))"
    48.5      using I by simp
    48.6    also have "\<dots> = (\<Union>i. (N \<circ> from_nat_into I) i)"
    48.7 -    by (simp only: SUP_def image_comp)
    48.8 +    by simp
    48.9    finally show ?thesis by simp
   48.10  qed
   48.11  
   48.12 @@ -1228,7 +1228,7 @@
   48.13      range: "range A \<subseteq> sets M" and
   48.14      space: "(\<Union>i. A i) = space M" and
   48.15      measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
   48.16 -    using sigma_finite by auto
   48.17 +    using sigma_finite by blast
   48.18    show thesis
   48.19    proof (rule that[of "disjointed A"])
   48.20      show "range (disjointed A) \<subseteq> sets M"
   48.21 @@ -1252,7 +1252,7 @@
   48.22  proof -
   48.23    obtain F :: "nat \<Rightarrow> 'a set" where
   48.24      F: "range F \<subseteq> sets M" "(\<Union>i. F i) = space M" "\<And>i. emeasure M (F i) \<noteq> \<infinity>"
   48.25 -    using sigma_finite by auto
   48.26 +    using sigma_finite by blast
   48.27    show thesis
   48.28    proof (rule that[of "\<lambda>n. \<Union>i\<le>n. F i"])
   48.29      show "range (\<lambda>n. \<Union>i\<le>n. F i) \<subseteq> sets M"
   48.30 @@ -1731,8 +1731,10 @@
   48.31    assumes upper: "space M \<subseteq> (\<Union>i \<in> s. f i)"
   48.32    shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
   48.33  proof -
   48.34 -  have e: "e = (\<Union>i \<in> s. e \<inter> f i)"
   48.35 +  have "e \<subseteq> (\<Union>i\<in>s. f i)"
   48.36      using \<open>e \<in> sets M\<close> sets.sets_into_space upper by blast
   48.37 +  then have e: "e = (\<Union>i \<in> s. e \<inter> f i)"
   48.38 +    by auto
   48.39    hence "measure M e = measure M (\<Union>i \<in> s. e \<inter> f i)" by simp
   48.40    also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
   48.41    proof (rule finite_measure_finite_Union)
   48.42 @@ -2074,7 +2076,7 @@
   48.43        using E \<Omega> by (subst (1 2) emeasure_restrict_space) (auto simp: sets_eq sets_eq[THEN sets_eq_imp_space_eq])
   48.44    next
   48.45      show "range (from_nat_into A) \<subseteq> E" "(\<Union>i. from_nat_into A i) = \<Omega>"
   48.46 -      unfolding Sup_image_eq[symmetric, where f="from_nat_into A"] using A by auto
   48.47 +      using A by (auto cong del: strong_SUP_cong)
   48.48    next
   48.49      fix i
   48.50      have "emeasure (restrict_space M \<Omega>) (from_nat_into A i) = emeasure M (from_nat_into A i)"
   48.51 @@ -2333,12 +2335,12 @@
   48.52    assumes A: "Complete_Partial_Order.chain op \<le> (f ` A)" and a: "a \<in> A" "f a \<noteq> bot"
   48.53    shows space_SUP: "space (SUP M:A. f M) = space (f a)"
   48.54      and sets_SUP: "sets (SUP M:A. f M) = sets (f a)"
   48.55 -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)]])+
   48.56 +by(rule space_Sup[OF A a(2) imageI[OF a(1)]] sets_Sup[OF A a(2) imageI[OF a(1)]])+
   48.57  
   48.58  lemma emeasure_SUP:
   48.59    assumes A: "Complete_Partial_Order.chain op \<le> (f ` A)" "A \<noteq> {}"
   48.60    assumes "X \<in> sets (SUP M:A. f M)"
   48.61    shows "emeasure (SUP M:A. f M) X = (SUP M:A. emeasure (f M)) X"
   48.62 -using \<open>X \<in> _\<close> unfolding SUP_def by(subst emeasure_Sup[OF A(1)]; simp add: A)
   48.63 +using \<open>X \<in> _\<close> by(subst emeasure_Sup[OF A(1)]; simp add: A)
   48.64  
   48.65  end
    49.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Feb 17 21:51:55 2016 +0100
    49.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Feb 17 21:51:56 2016 +0100
    49.3 @@ -932,7 +932,7 @@
    49.4          have "a * u x < 1 * u x"
    49.5            by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)
    49.6          also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def)
    49.7 -        finally obtain i where "a * u x < f i x" unfolding SUP_def
    49.8 +        finally obtain i where "a * u x < f i x"
    49.9            by (auto simp add: less_SUP_iff)
   49.10          hence "a * u x \<le> f i x" by auto
   49.11          thus ?thesis using \<open>x \<in> space M\<close> by auto
   49.12 @@ -2042,7 +2042,7 @@
   49.13      by (auto intro!: SUP_least SUP_upper nn_integral_mono)
   49.14  next
   49.15    have "\<And>x. \<exists>g. incseq g \<and> range g \<subseteq> (\<lambda>i. f i x) ` Y \<and> (SUP i:Y. f i x) = (SUP i. g i)"
   49.16 -    unfolding Sup_class.SUP_def by(rule Sup_countable_SUP[unfolded Sup_class.SUP_def])(simp add: nonempty)
   49.17 +    by (rule Sup_countable_SUP) (simp add: nonempty)
   49.18    then obtain g where incseq: "\<And>x. incseq (g x)"
   49.19      and range: "\<And>x. range (g x) \<subseteq> (\<lambda>i. f i x) ` Y"
   49.20      and sup: "\<And>x. (SUP i:Y. f i x) = (SUP i. g x i)" by moura
   49.21 @@ -2088,8 +2088,8 @@
   49.22            assume "x \<in> {..<m}"
   49.23            hence "x < m" by simp
   49.24            have "g x n = f (I x) x" by(simp add: I)
   49.25 -          also have "\<dots> \<le> (SUP i:?Y. f i) x" unfolding SUP_def Sup_fun_def image_image
   49.26 -            using \<open>x \<in> {..<m}\<close> by(rule Sup_upper[OF imageI])
   49.27 +          also have "\<dots> \<le> (SUP i:?Y. f i) x" unfolding Sup_fun_def image_image
   49.28 +            using \<open>x \<in> {..<m}\<close> by (rule Sup_upper [OF imageI])
   49.29            also have "\<dots> = f (I m') x" unfolding m' by simp
   49.30            finally show "g x n \<le> f (I m') x" .
   49.31          qed
   49.32 @@ -2264,7 +2264,7 @@
   49.33        by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm)
   49.34    qed
   49.35    then show ?thesis
   49.36 -    unfolding nn_integral_def_finite SUP_def by simp
   49.37 +    unfolding nn_integral_def_finite by (simp cong del: strong_SUP_cong)
   49.38  qed
   49.39  
   49.40  lemma nn_integral_count_space_indicator:
    50.1 --- a/src/HOL/Probability/Probability_Measure.thy	Wed Feb 17 21:51:55 2016 +0100
    50.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Wed Feb 17 21:51:56 2016 +0100
    50.3 @@ -247,7 +247,7 @@
    50.4    moreover
    50.5    { fix y assume y: "y \<in> I"
    50.6      with q(2) \<open>open I\<close> have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
    50.7 -      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) }
    50.8 +      by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open) }
    50.9    ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
   50.10      by simp
   50.11    also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
    51.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 17 21:51:55 2016 +0100
    51.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 17 21:51:56 2016 +0100
    51.3 @@ -51,7 +51,7 @@
    51.4      space: "(\<Union>i. A i) = space M" and
    51.5      measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>" and
    51.6      disjoint: "disjoint_family A"
    51.7 -    using sigma_finite_disjoint by auto
    51.8 +    using sigma_finite_disjoint by blast
    51.9    let ?B = "\<lambda>i. 2^Suc i * emeasure M (A i)"
   51.10    have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
   51.11    proof
   51.12 @@ -560,7 +560,7 @@
   51.13    proof (rule antisym)
   51.14      show "?a \<le> (SUP i. emeasure M (?O i))" unfolding a_Lim
   51.15        using Q' by (auto intro!: SUP_mono emeasure_mono)
   51.16 -    show "(SUP i. emeasure M (?O i)) \<le> ?a" unfolding SUP_def
   51.17 +    show "(SUP i. emeasure M (?O i)) \<le> ?a"
   51.18      proof (safe intro!: Sup_mono, unfold bex_simps)
   51.19        fix i
   51.20        have *: "(\<Union>(Q' ` {..i})) = ?O i" by auto
    52.1 --- a/src/HOL/Probability/Regularity.thy	Wed Feb 17 21:51:55 2016 +0100
    52.2 +++ b/src/HOL/Probability/Regularity.thy	Wed Feb 17 21:51:56 2016 +0100
    52.3 @@ -138,7 +138,8 @@
    52.4      proof safe
    52.5        fix x from X(2)[OF open_ball[of x r]] \<open>r > 0\<close> obtain d where d: "d\<in>X" "d \<in> ball x r" by auto
    52.6        show "x \<in> ?U"
    52.7 -        using X(1) d by (auto intro!: exI[where x="to_nat_on X d"] simp: dist_commute Bex_def)
    52.8 +        using X(1) d
    52.9 +        by simp (auto intro!: exI [where x = "to_nat_on X d"] simp: dist_commute Bex_def)
   52.10      qed (simp add: sU)
   52.11      finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) \<longlonglongrightarrow> M (space M)" .
   52.12    } note M_space = this
   52.13 @@ -319,8 +320,8 @@
   52.14        by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
   52.15      also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
   52.16          (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
   52.17 -      by (subst INF_image [of "\<lambda>u. space M - u", symmetric, unfolded comp_def])
   52.18 -        (rule INF_cong, auto simp add: sU intro!: INF_cong)
   52.19 +      unfolding INF_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]
   52.20 +        by (rule INF_cong) (auto simp add: sU open_Compl Compl_eq_Diff_UNIV [symmetric, simp])
   52.21      finally have
   52.22        "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
   52.23      moreover have
   52.24 @@ -335,8 +336,8 @@
   52.25      also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
   52.26        by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
   52.27      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
   52.28 -      by (subst SUP_image [of "\<lambda>u. space M - u", symmetric, simplified comp_def])
   52.29 -         (rule SUP_cong, auto simp: sU)
   52.30 +      unfolding SUP_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]
   52.31 +        by (rule SUP_cong) (auto simp add: sU)
   52.32      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
   52.33      proof (safe intro!: antisym SUP_least)
   52.34        fix K assume "closed K" "K \<subseteq> space M - B"
    53.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Feb 17 21:51:55 2016 +0100
    53.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Feb 17 21:51:56 2016 +0100
    53.3 @@ -432,10 +432,10 @@
    53.4    by (auto simp add: binary_def)
    53.5  
    53.6  lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
    53.7 -  by (simp add: SUP_def range_binary_eq)
    53.8 +  by (simp add: range_binary_eq cong del: strong_SUP_cong)
    53.9  
   53.10  lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
   53.11 -  by (simp add: INF_def range_binary_eq)
   53.12 +  by (simp add: range_binary_eq cong del: strong_INF_cong)
   53.13  
   53.14  lemma sigma_algebra_iff2:
   53.15       "sigma_algebra \<Omega> M \<longleftrightarrow>
   53.16 @@ -535,11 +535,14 @@
   53.17    finally show ?thesis .
   53.18  qed
   53.19  
   53.20 -lemma sigma_sets_UNION: "countable B \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets X A) \<Longrightarrow> (\<Union>B) \<in> sigma_sets X A"
   53.21 -  using from_nat_into[of B] range_from_nat_into[of B] sigma_sets.Union[of "from_nat_into B" X A]
   53.22 +lemma sigma_sets_UNION:
   53.23 +  "countable B \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets X A) \<Longrightarrow> (\<Union>B) \<in> sigma_sets X A"
   53.24    apply (cases "B = {}")
   53.25    apply (simp add: sigma_sets.Empty)
   53.26 -  apply (simp del: Union_image_eq add: Union_image_eq[symmetric])
   53.27 +  using from_nat_into [of B] range_from_nat_into [of B] sigma_sets.Union [of "from_nat_into B" X A]
   53.28 +  apply simp
   53.29 +  apply auto
   53.30 +  apply (metis Sup_bot_conv(1) Union_empty `\<lbrakk>B \<noteq> {}; countable B\<rbrakk> \<Longrightarrow> range (from_nat_into B) = B`)
   53.31    done
   53.32  
   53.33  lemma (in sigma_algebra) sigma_sets_eq:
   53.34 @@ -835,7 +838,7 @@
   53.35  
   53.36  lemma (in semiring_of_sets) generated_ring_disjoint_UNION:
   53.37    "finite I \<Longrightarrow> disjoint (A ` I) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> UNION I A \<in> generated_ring"
   53.38 -  unfolding SUP_def by (intro generated_ring_disjoint_Union) auto
   53.39 +  by (intro generated_ring_disjoint_Union) auto
   53.40  
   53.41  lemma (in semiring_of_sets) generated_ring_Int:
   53.42    assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring"
   53.43 @@ -873,7 +876,7 @@
   53.44  
   53.45  lemma (in semiring_of_sets) generated_ring_INTER:
   53.46    "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> INTER I A \<in> generated_ring"
   53.47 -  unfolding INF_def by (intro generated_ring_Inter) auto
   53.48 +  by (intro generated_ring_Inter) auto
   53.49  
   53.50  lemma (in semiring_of_sets) generating_ring:
   53.51    "ring_of_sets \<Omega> generated_ring"
   53.52 @@ -898,6 +901,7 @@
   53.53          fix a b assume "a \<in> Ca" "b \<in> Cb"
   53.54          with Ca Cb Diff_cover[of a b] show "a - b \<in> ?R"
   53.55            by (auto simp add: generated_ring_def)
   53.56 +            (metis DiffI Diff_eq_empty_iff empty_iff)
   53.57        next
   53.58          show "disjoint ((\<lambda>a'. \<Inter>b'\<in>Cb. a' - b')`Ca)"
   53.59            using Ca by (auto simp add: disjoint_def \<open>Cb \<noteq> {}\<close>)
   53.60 @@ -935,7 +939,7 @@
   53.61    done
   53.62  
   53.63  lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
   53.64 -  by (simp add: SUP_def range_binaryset_eq)
   53.65 +  by (simp add: range_binaryset_eq cong del: strong_SUP_cong)
   53.66  
   53.67  subsubsection \<open>Closed CDI\<close>
   53.68  
    54.1 --- a/src/HOL/Relation.thy	Wed Feb 17 21:51:55 2016 +0100
    54.2 +++ b/src/HOL/Relation.thy	Wed Feb 17 21:51:56 2016 +0100
    54.3 @@ -1060,10 +1060,11 @@
    54.4  
    54.5  text\<open>Converse inclusion requires some assumptions\<close>
    54.6  lemma Image_INT_eq:
    54.7 -     "[|single_valued (r\<inverse>); A\<noteq>{}|] ==> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)"
    54.8 +  "single_valued (r\<inverse>) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)"
    54.9  apply (rule equalityI)
   54.10   apply (rule Image_INT_subset) 
   54.11 -apply  (simp add: single_valued_def, blast)
   54.12 +apply (auto simp add: single_valued_def)
   54.13 +apply blast
   54.14  done
   54.15  
   54.16  lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"
    55.1 --- a/src/HOL/Set_Interval.thy	Wed Feb 17 21:51:55 2016 +0100
    55.2 +++ b/src/HOL/Set_Interval.thy	Wed Feb 17 21:51:56 2016 +0100
    55.3 @@ -1085,26 +1085,33 @@
    55.4    qed
    55.5  qed
    55.6  
    55.7 -lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
    55.8 +lemma UN_UN_finite_eq:
    55.9 +  "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
   55.10    by (auto simp add: atLeast0LessThan) 
   55.11  
   55.12 -lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
   55.13 +lemma UN_finite_subset:
   55.14 +  "(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
   55.15    by (subst UN_UN_finite_eq [symmetric]) blast
   55.16  
   55.17  lemma UN_finite2_subset: 
   55.18 -     "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
   55.19 -  apply (rule UN_finite_subset)
   55.20 -  apply (subst UN_UN_finite_eq [symmetric, of B]) 
   55.21 -  apply blast
   55.22 -  done
   55.23 +  assumes "\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n + k}. B i)"
   55.24 +  shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
   55.25 +proof (rule UN_finite_subset, rule)
   55.26 +  fix n and a
   55.27 +  from assms have "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n + k}. B i)" .
   55.28 +  moreover assume "a \<in> (\<Union>i\<in>{0..<n}. A i)"
   55.29 +  ultimately have "a \<in> (\<Union>i\<in>{0..<n + k}. B i)" by blast
   55.30 +  then show "a \<in> (\<Union>i. B i)" by (auto simp add: UN_UN_finite_eq)
   55.31 +qed
   55.32  
   55.33  lemma UN_finite2_eq:
   55.34 -  "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) = (\<Union>n. B n)"
   55.35 +  "(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n + k}. B i)) \<Longrightarrow>
   55.36 +    (\<Union>n. A n) = (\<Union>n. B n)"
   55.37    apply (rule subset_antisym)
   55.38     apply (rule UN_finite2_subset, blast)
   55.39 - apply (rule UN_finite2_subset [where k=k])
   55.40 - apply (force simp add: atLeastLessThan_add_Un [of 0])
   55.41 - done
   55.42 +  apply (rule UN_finite2_subset [where k=k])
   55.43 +  apply (force simp add: atLeastLessThan_add_Un [of 0])
   55.44 +  done
   55.45  
   55.46  
   55.47  subsubsection \<open>Cardinality\<close>
    56.1 --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Wed Feb 17 21:51:55 2016 +0100
    56.2 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Wed Feb 17 21:51:56 2016 +0100
    56.3 @@ -251,7 +251,7 @@
    56.4  
    56.5  val simplified_set_simps =
    56.6    @{thms collect_def[abs_def] UN_insert UN_empty Un_empty_right Un_empty_left
    56.7 -    o_def Union_Un_distrib Union_image_eq UN_empty2 UN_singleton id_bnf_def};
    56.8 +    o_def Union_Un_distrib UN_empty2 UN_singleton id_bnf_def};
    56.9  
   56.10  fun mk_simplified_set_tac ctxt collect_set_map =
   56.11    unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN
    57.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Feb 17 21:51:55 2016 +0100
    57.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Feb 17 21:51:56 2016 +0100
    57.3 @@ -540,8 +540,8 @@
    57.4  fun mk_ctor_set_tac ctxt set set_map set_maps =
    57.5    let
    57.6      val n = length set_maps;
    57.7 -    fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN'
    57.8 -      rtac ctxt @{thm Union_image_eq};
    57.9 +    fun mk_UN thm = rtac ctxt (thm RS @{thm arg_cong[of _ _ Union]} RS trans)
   57.10 +      THEN' rtac ctxt @{thm refl};
   57.11    in
   57.12      EVERY' [rtac ctxt (set RS @{thm comp_eq_dest} RS trans), rtac ctxt Un_cong,
   57.13        rtac ctxt (trans OF [set_map, trans_fun_cong_image_id_id_apply]),
    58.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Wed Feb 17 21:51:55 2016 +0100
    58.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Wed Feb 17 21:51:56 2016 +0100
    58.3 @@ -257,8 +257,12 @@
    58.4    Const (@{const_name Bex}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f;
    58.5  
    58.6  fun mk_UNION X f =
    58.7 -  let val (T, U) = dest_funT (fastype_of f);
    58.8 -  in Const (@{const_name SUPREMUM}, fastype_of X --> (T --> U) --> U) $ X $ f end;
    58.9 +  let
   58.10 +    val (T, U) = dest_funT (fastype_of f);
   58.11 +  in
   58.12 +    Const (@{const_name Sup}, HOLogic.mk_setT U --> U)
   58.13 +      $ (Const (@{const_name image}, (T --> U) --> fastype_of X --> HOLogic.mk_setT U) $ f $ X)
   58.14 +  end;
   58.15  
   58.16  fun mk_Union T =
   58.17    Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T);
    59.1 --- a/src/HOL/Topological_Spaces.thy	Wed Feb 17 21:51:55 2016 +0100
    59.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Feb 17 21:51:56 2016 +0100
    59.3 @@ -1133,10 +1133,11 @@
    59.4        using A by auto
    59.5      show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))"
    59.6        using A unfolding nhds_def
    59.7 -      apply (intro INF_eq)
    59.8 +      apply -
    59.9 +      apply (rule INF_eq)
   59.10        apply simp_all
   59.11 -      apply force
   59.12 -      apply (intro exI[of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
   59.13 +      apply fastforce
   59.14 +      apply (intro exI [of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
   59.15        apply auto
   59.16        done
   59.17    qed
   59.18 @@ -1464,7 +1465,7 @@
   59.19  
   59.20  lemma continuous_on_open_UN:
   59.21    "(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
   59.22 -  unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
   59.23 +  by (rule continuous_on_open_Union) auto
   59.24  
   59.25  lemma continuous_on_open_Un:
   59.26    "open s \<Longrightarrow> open t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
   59.27 @@ -1689,7 +1690,7 @@
   59.28  lemma compactE_image:
   59.29    assumes "compact s" and "\<forall>t\<in>C. open (f t)" and "s \<subseteq> (\<Union>c\<in>C. f c)"
   59.30    obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> (\<Union>c\<in>C'. f c)"
   59.31 -  using assms unfolding ball_simps[symmetric] SUP_def
   59.32 +  using assms unfolding ball_simps [symmetric]
   59.33    by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
   59.34  
   59.35  lemma compact_inter_closed [intro]:
    60.1 --- a/src/HOL/Transitive_Closure.thy	Wed Feb 17 21:51:55 2016 +0100
    60.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Feb 17 21:51:56 2016 +0100
    60.3 @@ -946,7 +946,7 @@
    60.4    apply (rule iffI)
    60.5     apply (drule tranclD2)
    60.6     apply (clarsimp simp: rtrancl_is_UN_relpow)
    60.7 -   apply (rule_tac x="Suc n" in exI)
    60.8 +   apply (rule_tac x="Suc x" in exI)
    60.9     apply (clarsimp simp: relcomp_unfold)
   60.10     apply fastforce
   60.11    apply clarsimp
   60.12 @@ -1093,9 +1093,9 @@
   60.13  assumes "finite R" and "finite S"
   60.14  shows "finite(R O S)"
   60.15  proof-
   60.16 -  have "R O S = (UN (x,y) : R. \<Union>((%(u,v). if u=y then {(x,v)} else {}) ` S))"
   60.17 -    by(force simp add: split_def)
   60.18 -  thus ?thesis using assms by(clarsimp)
   60.19 +  have "R O S = (\<Union>(x, y)\<in>R. \<Union>(u, v)\<in>S. if u = y then {(x, v)} else {})"
   60.20 +    by (force simp add: split_def image_constant_conv split: if_splits)
   60.21 +  then show ?thesis using assms by clarsimp
   60.22  qed
   60.23  
   60.24  lemma finite_relpow[simp,intro]:
    61.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Wed Feb 17 21:51:55 2016 +0100
    61.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Wed Feb 17 21:51:56 2016 +0100
    61.3 @@ -1035,7 +1035,7 @@
    61.4    apply (simp only: o_apply sub_def)
    61.5    apply (insert Alloc_Progress [THEN rename_guarantees_sysOfAlloc_I])
    61.6    apply (simp add: o_def del: INT_iff)
    61.7 -  apply (erule component_guaranteesD)
    61.8 +  apply (drule component_guaranteesD)
    61.9    apply (auto simp add:
   61.10      System_Increasing_allocRel [simplified sub_apply o_def]
   61.11      System_Increasing_allocAsk [simplified sub_apply o_def]
   61.12 @@ -1047,6 +1047,7 @@
   61.13  lemma System_Progress: "System : system_progress"
   61.14    apply (unfold system_progress_def)
   61.15    apply (cut_tac System_Alloc_Progress)
   61.16 +  apply auto
   61.17    apply (blast intro: LeadsTo_Trans
   61.18      System_Follows_allocGiv [THEN Follows_LeadsTo_pfixLe]
   61.19      System_Follows_ask [THEN Follows_LeadsTo])
    62.1 --- a/src/HOL/UNITY/ELT.thy	Wed Feb 17 21:51:55 2016 +0100
    62.2 +++ b/src/HOL/UNITY/ELT.thy	Wed Feb 17 21:51:56 2016 +0100
    62.3 @@ -141,7 +141,6 @@
    62.4  lemma leadsETo_UN:
    62.5      "(!!i. i : I ==> F : (A i) leadsTo[CC] B)  
    62.6       ==> F : (UN i:I. A i) leadsTo[CC] B"
    62.7 -apply (subst Union_image_eq [symmetric])
    62.8  apply (blast intro: leadsETo_Union)
    62.9  done
   62.10  
   62.11 @@ -397,7 +396,6 @@
   62.12  lemma LeadsETo_UN:
   62.13       "(!!i. i : I ==> F : (A i) LeadsTo[CC] B)  
   62.14        ==> F : (UN i:I. A i) LeadsTo[CC] B"
   62.15 -apply (simp only: Union_image_eq [symmetric])
   62.16  apply (blast intro: LeadsETo_Union)
   62.17  done
   62.18  
    63.1 --- a/src/HOL/UNITY/Extend.thy	Wed Feb 17 21:51:55 2016 +0100
    63.2 +++ b/src/HOL/UNITY/Extend.thy	Wed Feb 17 21:51:56 2016 +0100
    63.3 @@ -382,21 +382,25 @@
    63.4                                       (project_act h -` AllowedActs F)})"
    63.5  apply (rule program_equalityI)
    63.6    apply simp
    63.7 - apply (simp add: image_eq_UN)
    63.8 + apply (simp add: image_image)
    63.9  apply (simp add: project_def)
   63.10  done
   63.11  
   63.12  lemma extend_inverse [simp]:
   63.13       "project h UNIV (extend h F) = F"
   63.14 -apply (simp (no_asm_simp) add: project_extend_eq image_eq_UN
   63.15 +apply (simp (no_asm_simp) add: project_extend_eq
   63.16            subset_UNIV [THEN subset_trans, THEN Restrict_triv])
   63.17  apply (rule program_equalityI)
   63.18  apply (simp_all (no_asm))
   63.19  apply (subst insert_absorb)
   63.20  apply (simp (no_asm) add: bexI [of _ Id])
   63.21  apply auto
   63.22 +apply (simp add: image_def)
   63.23 +using project_act_Id apply blast
   63.24 +apply (simp add: image_def)
   63.25  apply (rename_tac "act")
   63.26 -apply (rule_tac x = "extend_act h act" in bexI, auto)
   63.27 +apply (rule_tac x = "extend_act h act" in exI)
   63.28 +apply simp
   63.29  done
   63.30  
   63.31  lemma inj_extend: "inj (extend h)"
   63.32 @@ -641,11 +645,12 @@
   63.33  subsection{*Guarantees*}
   63.34  
   63.35  lemma project_extend_Join: "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
   63.36 -apply (rule program_equalityI)
   63.37 -  apply (simp add: project_set_extend_set_Int)
   63.38 - apply (auto simp add: image_eq_UN)
   63.39 -done
   63.40 -
   63.41 +  apply (rule program_equalityI)
   63.42 +  apply (auto simp add: project_set_extend_set_Int image_iff)
   63.43 +  apply (metis Un_iff extend_act_inverse image_iff)
   63.44 +  apply (metis Un_iff extend_act_inverse image_iff)
   63.45 +  done
   63.46 +  
   63.47  lemma extend_Join_eq_extend_D:
   63.48       "(extend h F)\<squnion>G = extend h H ==> H = F\<squnion>(project h UNIV G)"
   63.49  apply (drule_tac f = "project h UNIV" in arg_cong)
    64.1 --- a/src/HOL/UNITY/ProgressSets.thy	Wed Feb 17 21:51:55 2016 +0100
    64.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Wed Feb 17 21:51:56 2016 +0100
    64.3 @@ -42,13 +42,11 @@
    64.4  
    64.5  lemma UN_in_lattice:
    64.6       "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
    64.7 -apply (unfold SUP_def)
    64.8  apply (blast intro: Union_in_lattice) 
    64.9  done
   64.10  
   64.11  lemma INT_in_lattice:
   64.12       "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i)  \<in> L"
   64.13 -apply (unfold INF_def)
   64.14  apply (blast intro: Inter_in_lattice) 
   64.15  done
   64.16  
    65.1 --- a/src/HOL/UNITY/Rename.thy	Wed Feb 17 21:51:55 2016 +0100
    65.2 +++ b/src/HOL/UNITY/Rename.thy	Wed Feb 17 21:51:56 2016 +0100
    65.3 @@ -272,7 +272,7 @@
    65.4                  (F \<in> (rename (inv h) ` X) guarantees  
    65.5                       (rename (inv h) ` Y))"
    65.6  apply (subst rename_rename_guarantees_eq [symmetric], assumption)
    65.7 -apply (simp add: image_eq_UN o_def bij_is_surj [THEN surj_f_inv_f])
    65.8 +apply (simp add: o_def bij_is_surj [THEN surj_f_inv_f] image_comp)
    65.9  done
   65.10  
   65.11  lemma rename_preserves:
    66.1 --- a/src/HOL/UNITY/SubstAx.thy	Wed Feb 17 21:51:55 2016 +0100
    66.2 +++ b/src/HOL/UNITY/SubstAx.thy	Wed Feb 17 21:51:56 2016 +0100
    66.3 @@ -84,7 +84,6 @@
    66.4  
    66.5  lemma LeadsTo_UN: 
    66.6       "(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B"
    66.7 -apply (unfold SUP_def)
    66.8  apply (blast intro: LeadsTo_Union)
    66.9  done
   66.10  
   66.11 @@ -188,7 +187,6 @@
   66.12  lemma LeadsTo_UN_UN: 
   66.13       "(!! i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i))  
   66.14        ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo (\<Union>i \<in> I. A' i)"
   66.15 -apply (simp only: Union_image_eq [symmetric])
   66.16  apply (blast intro: LeadsTo_Union LeadsTo_weaken_R)
   66.17  done
   66.18  
    67.1 --- a/src/HOL/UNITY/Transformers.thy	Wed Feb 17 21:51:55 2016 +0100
    67.2 +++ b/src/HOL/UNITY/Transformers.thy	Wed Feb 17 21:51:56 2016 +0100
    67.3 @@ -467,7 +467,7 @@
    67.4        "single_valued act
    67.5         ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq> 
    67.6             wens_set (mk_program (init, {act}, allowed)) B"
    67.7 -apply (simp add: SUP_def image_def wens_single_eq_Union) 
    67.8 +apply (simp add: image_def wens_single_eq_Union) 
    67.9  apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
   67.10  done
   67.11  
    68.1 --- a/src/HOL/UNITY/Union.thy	Wed Feb 17 21:51:55 2016 +0100
    68.2 +++ b/src/HOL/UNITY/Union.thy	Wed Feb 17 21:51:56 2016 +0100
    68.3 @@ -396,11 +396,30 @@
    68.4  
    68.5  lemma safety_prop_Int [simp]:
    68.6    "safety_prop X \<Longrightarrow> safety_prop Y \<Longrightarrow> safety_prop (X \<inter> Y)"
    68.7 -  by (simp add: safety_prop_def) blast
    68.8 +proof (clarsimp simp add: safety_prop_def)
    68.9 +  fix G
   68.10 +  assume "\<forall>G. Acts G \<subseteq> (\<Union>x\<in>X. Acts x) \<longrightarrow> G \<in> X"
   68.11 +  then have X: "Acts G \<subseteq> (\<Union>x\<in>X. Acts x) \<Longrightarrow> G \<in> X" by blast
   68.12 +  assume "\<forall>G. Acts G \<subseteq> (\<Union>x\<in>Y. Acts x) \<longrightarrow> G \<in> Y"
   68.13 +  then have Y: "Acts G \<subseteq> (\<Union>x\<in>Y. Acts x) \<Longrightarrow> G \<in> Y" by blast
   68.14 +  assume Acts: "Acts G \<subseteq> (\<Union>x\<in>X \<inter> Y. Acts x)"
   68.15 +  with X and Y show "G \<in> X \<and> G \<in> Y" by auto
   68.16 +qed  
   68.17  
   68.18  lemma safety_prop_INTER [simp]:
   68.19    "(\<And>i. i \<in> I \<Longrightarrow> safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i\<in>I. X i)"
   68.20 -  by (simp add: safety_prop_def) blast
   68.21 +proof (clarsimp simp add: safety_prop_def)
   68.22 +  fix G and i
   68.23 +  assume "\<And>i. i \<in> I \<Longrightarrow> \<bottom> \<in> X i \<and>
   68.24 +    (\<forall>G. Acts G \<subseteq> (\<Union>x\<in>X i. Acts x) \<longrightarrow> G \<in> X i)"
   68.25 +  then have *: "i \<in> I \<Longrightarrow> Acts G \<subseteq> (\<Union>x\<in>X i. Acts x) \<Longrightarrow> G \<in> X i"
   68.26 +    by blast
   68.27 +  assume "i \<in> I"
   68.28 +  moreover assume "Acts G \<subseteq> (\<Union>j\<in>\<Inter>i\<in>I. X i. Acts j)"
   68.29 +  ultimately have "Acts G \<subseteq> (\<Union>i\<in>X i. Acts i)"
   68.30 +    by auto
   68.31 +  with * `i \<in> I` show "G \<in> X i" by blast
   68.32 +qed
   68.33  
   68.34  lemma safety_prop_INTER1 [simp]:
   68.35    "(\<And>i. safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i. X i)"
    69.1 --- a/src/HOL/UNITY/WFair.thy	Wed Feb 17 21:51:55 2016 +0100
    69.2 +++ b/src/HOL/UNITY/WFair.thy	Wed Feb 17 21:51:56 2016 +0100
    69.3 @@ -203,7 +203,6 @@
    69.4  
    69.5  lemma leadsTo_UN: 
    69.6      "(!!i. i \<in> I ==> F \<in> (A i) leadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) leadsTo B"
    69.7 -apply (subst Union_image_eq [symmetric])
    69.8  apply (blast intro: leadsTo_Union)
    69.9  done
   69.10  
   69.11 @@ -310,7 +309,6 @@
   69.12  lemma leadsTo_UN_UN:
   69.13     "(!! i. i \<in> I ==> F \<in> (A i) leadsTo (A' i))  
   69.14      ==> F \<in> (\<Union>i \<in> I. A i) leadsTo (\<Union>i \<in> I. A' i)"
   69.15 -apply (simp only: Union_image_eq [symmetric])
   69.16  apply (blast intro: leadsTo_Union leadsTo_weaken_R)
   69.17  done
   69.18