removed further legacy rules from Complete_Lattices
authorhoelzl
Thu Sep 15 12:40:08 2011 -0400 (2011-09-15)
changeset 4493722c0857b8aab
parent 44936 e1139e612b55
child 44938 98e05fc1ce7d
child 44942 a05ab4d803f2
removed further legacy rules from Complete_Lattices
NEWS
src/HOL/Big_Operators.thy
src/HOL/Complete_Lattices.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/RealVector.thy
src/HOL/Wellfounded.thy
     1.1 --- a/NEWS	Thu Sep 15 17:06:00 2011 +0200
     1.2 +++ b/NEWS	Thu Sep 15 12:40:08 2011 -0400
     1.3 @@ -115,7 +115,7 @@
     1.4  
     1.5  Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
     1.6  INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
     1.7 -INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union,
     1.8 +INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset,
     1.9  UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been
    1.10  discarded.
    1.11  
     2.1 --- a/src/HOL/Big_Operators.thy	Thu Sep 15 17:06:00 2011 +0200
     2.2 +++ b/src/HOL/Big_Operators.thy	Thu Sep 15 12:40:08 2011 -0400
     2.3 @@ -312,14 +312,14 @@
     2.4  text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
     2.5  directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
     2.6  lemma setsum_Union_disjoint:
     2.7 -  "[| (ALL A:C. finite A);
     2.8 -      (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
     2.9 -   ==> setsum f (Union C) = setsum (setsum f) C"
    2.10 -apply (cases "finite C") 
    2.11 - prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
    2.12 -  apply (frule setsum_UN_disjoint [of C id f])
    2.13 - apply (unfold Union_def id_def, assumption+)
    2.14 -done
    2.15 +  assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
    2.16 +  shows "setsum f (Union C) = setsum (setsum f) C"
    2.17 +proof cases
    2.18 +  assume "finite C"
    2.19 +  from setsum_UN_disjoint[OF this assms]
    2.20 +  show ?thesis
    2.21 +    by (simp add: SUP_def)
    2.22 +qed (force dest: finite_UnionD simp add: setsum_def)
    2.23  
    2.24  (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
    2.25    the rhs need not be, since SIGMA A B could still be finite.*)
    2.26 @@ -801,7 +801,7 @@
    2.27     (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
    2.28     ==> card (Union C) = setsum card C"
    2.29  apply (frule card_UN_disjoint [of C id])
    2.30 -apply (unfold Union_def id_def, assumption+)
    2.31 +apply (simp_all add: SUP_def id_def)
    2.32  done
    2.33  
    2.34  text{*The image of a finite set can be expressed using @{term fold_image}.*}
    2.35 @@ -996,14 +996,14 @@
    2.36    by (simp add: setprod_def fold_image_UN_disjoint)
    2.37  
    2.38  lemma setprod_Union_disjoint:
    2.39 -  "[| (ALL A:C. finite A);
    2.40 -      (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] 
    2.41 -   ==> setprod f (Union C) = setprod (setprod f) C"
    2.42 -apply (cases "finite C") 
    2.43 - prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
    2.44 -  apply (frule setprod_UN_disjoint [of C id f])
    2.45 - apply (unfold Union_def id_def, assumption+)
    2.46 -done
    2.47 +  assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}" 
    2.48 +  shows "setprod f (Union C) = setprod (setprod f) C"
    2.49 +proof cases
    2.50 +  assume "finite C"
    2.51 +  from setprod_UN_disjoint[OF this assms]
    2.52 +  show ?thesis
    2.53 +    by (simp add: SUP_def)
    2.54 +qed (force dest: finite_UnionD simp add: setprod_def)
    2.55  
    2.56  lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
    2.57      (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
     3.1 --- a/src/HOL/Complete_Lattices.thy	Thu Sep 15 17:06:00 2011 +0200
     3.2 +++ b/src/HOL/Complete_Lattices.thy	Thu Sep 15 12:40:08 2011 -0400
     3.3 @@ -1131,7 +1131,6 @@
     3.4    "\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
     3.5    by auto
     3.6  
     3.7 -
     3.8  text {* Legacy names *}
     3.9  
    3.10  lemma (in complete_lattice) Inf_singleton [simp]:
    3.11 @@ -1142,68 +1141,9 @@
    3.12    "\<Squnion>{a} = a"
    3.13    by simp
    3.14  
    3.15 -lemma (in complete_lattice) Inf_binary:
    3.16 -  "\<Sqinter>{a, b} = a \<sqinter> b"
    3.17 -  by simp
    3.18 -
    3.19 -lemma (in complete_lattice) Sup_binary:
    3.20 -  "\<Squnion>{a, b} = a \<squnion> b"
    3.21 -  by simp
    3.22 -
    3.23 -text {* Grep and put to news from here *}
    3.24 -
    3.25 -lemma (in complete_lattice) INF_eq:
    3.26 -  "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
    3.27 -  by (simp add: INF_def image_def)
    3.28 -
    3.29 -lemma (in complete_lattice) SUP_eq:
    3.30 -  "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
    3.31 -  by (simp add: SUP_def image_def)
    3.32 -
    3.33 -lemma (in complete_lattice) INF_subset:
    3.34 -  "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
    3.35 -  by (rule INF_superset_mono) auto
    3.36 -
    3.37 -lemma (in complete_lattice) INF_UNIV_range:
    3.38 -  "(\<Sqinter>x. f x) = \<Sqinter>range f"
    3.39 -  by (fact INF_def)
    3.40 -
    3.41 -lemma (in complete_lattice) SUP_UNIV_range:
    3.42 -  "(\<Squnion>x. f x) = \<Squnion>range f"
    3.43 -  by (fact SUP_def)
    3.44 -
    3.45 -lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
    3.46 -  by simp
    3.47 -
    3.48 -lemma INTER_eq_Inter_image:
    3.49 -  "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
    3.50 -  by (fact INF_def)
    3.51 -  
    3.52 -lemma Inter_def:
    3.53 -  "\<Inter>S = (\<Inter>x\<in>S. x)"
    3.54 -  by (simp add: INTER_eq_Inter_image image_def)
    3.55 -
    3.56 -lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
    3.57 -  by (fact INF_eq)
    3.58 -
    3.59 -lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
    3.60 -  by blast
    3.61 -
    3.62 -lemma UNION_eq_Union_image:
    3.63 -  "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
    3.64 -  by (fact SUP_def)
    3.65 -
    3.66 -lemma Union_def:
    3.67 -  "\<Union>S = (\<Union>x\<in>S. x)"
    3.68 -  by (simp add: UNION_eq_Union_image image_def)
    3.69 -
    3.70  lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
    3.71    by blast
    3.72  
    3.73 -lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
    3.74 -  by (fact SUP_eq)
    3.75 -
    3.76 -
    3.77  text {* Finally *}
    3.78  
    3.79  no_notation
     4.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Sep 15 17:06:00 2011 +0200
     4.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Sep 15 12:40:08 2011 -0400
     4.3 @@ -1419,7 +1419,7 @@
     4.4      (SUP n. \<integral>\<^isup>+ x. (INF i:{n..}. u i x) \<partial>M)"
     4.5      unfolding liminf_SUPR_INFI using pos u
     4.6      by (intro positive_integral_monotone_convergence_SUP_AE)
     4.7 -       (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_subset)
     4.8 +       (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_superset_mono)
     4.9    also have "\<dots> \<le> liminf (\<lambda>n. integral\<^isup>P M (u n))"
    4.10      unfolding liminf_SUPR_INFI
    4.11      by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower)
     5.1 --- a/src/HOL/RealVector.thy	Thu Sep 15 17:06:00 2011 +0200
     5.2 +++ b/src/HOL/RealVector.thy	Thu Sep 15 12:40:08 2011 -0400
     5.3 @@ -452,13 +452,13 @@
     5.4    using open_Union [of "{S, T}"] by simp
     5.5  
     5.6  lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
     5.7 -  unfolding UN_eq by (rule open_Union) auto
     5.8 +  unfolding SUP_def by (rule open_Union) auto
     5.9 +
    5.10 +lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
    5.11 +  by (induct set: finite) auto
    5.12  
    5.13  lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
    5.14 -  by (induct set: finite) auto
    5.15 -
    5.16 -lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
    5.17 -  unfolding Inter_def by (rule open_INT)
    5.18 +  unfolding INF_def by (rule open_Inter) auto
    5.19  
    5.20  lemma closed_empty [intro, simp]:  "closed {}"
    5.21    unfolding closed_def by simp
    5.22 @@ -466,9 +466,6 @@
    5.23  lemma closed_Un [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"
    5.24    unfolding closed_def by auto
    5.25  
    5.26 -lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
    5.27 -  unfolding closed_def Inter_def by auto
    5.28 -
    5.29  lemma closed_UNIV [intro, simp]: "closed UNIV"
    5.30    unfolding closed_def by simp
    5.31  
    5.32 @@ -478,11 +475,14 @@
    5.33  lemma closed_INT [intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
    5.34    unfolding closed_def by auto
    5.35  
    5.36 -lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
    5.37 +lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
    5.38 +  unfolding closed_def uminus_Inf by auto
    5.39 +
    5.40 +lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
    5.41    by (induct set: finite) auto
    5.42  
    5.43 -lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
    5.44 -  unfolding Union_def by (rule closed_UN)
    5.45 +lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
    5.46 +  unfolding SUP_def by (rule closed_Union) auto
    5.47  
    5.48  lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
    5.49    unfolding closed_def by simp
     6.1 --- a/src/HOL/Wellfounded.thy	Thu Sep 15 17:06:00 2011 +0200
     6.2 +++ b/src/HOL/Wellfounded.thy	Thu Sep 15 12:40:08 2011 -0400
     6.3 @@ -305,9 +305,7 @@
     6.4   "[| ALL r:R. wf r;  
     6.5       ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
     6.6    |] ==> wf(Union R)"
     6.7 -apply (simp add: Union_def)
     6.8 -apply (blast intro: wf_UN)
     6.9 -done
    6.10 +  using wf_UN[of R "\<lambda>i. i"] by (simp add: SUP_def)
    6.11  
    6.12  (*Intuition: we find an (R u S)-min element of a nonempty subset A
    6.13               by case distinction.