src/HOL/Complete_Lattices.thy
changeset 56248 67dc9549fa15
parent 56218 1c3f1f2431f9
child 56741 2b3710a4fa94
     1.1 --- a/src/HOL/Complete_Lattices.thy	Fri Mar 21 22:54:16 2014 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Sat Mar 22 08:37:43 2014 +0100
     1.3 @@ -40,6 +40,10 @@
     1.4    "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
     1.5    by (simp add: INF_def image_def)
     1.6  
     1.7 +lemma strong_INF_cong [cong]:
     1.8 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
     1.9 +  unfolding simp_implies_def by (fact INF_cong)
    1.10 +
    1.11  end
    1.12  
    1.13  class Sup =
    1.14 @@ -69,6 +73,10 @@
    1.15    "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
    1.16    by (simp add: SUP_def image_def)
    1.17  
    1.18 +lemma strong_SUP_cong [cong]:
    1.19 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
    1.20 +  unfolding simp_implies_def by (fact SUP_cong)
    1.21 +
    1.22  end
    1.23  
    1.24  text {*
    1.25 @@ -447,21 +455,23 @@
    1.26  lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFIMUM A f \<le> SUPREMUM A f"
    1.27    using Inf_le_Sup [of "f ` A"] by simp
    1.28  
    1.29 -lemma SUP_eq_const:
    1.30 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
    1.31 -  by (auto intro: SUP_eqI)
    1.32 -
    1.33  lemma INF_eq_const:
    1.34    "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
    1.35    by (auto intro: INF_eqI)
    1.36  
    1.37 -lemma SUP_eq_iff:
    1.38 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPREMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
    1.39 -  using SUP_eq_const[of I f c] SUP_upper[of _ I f] by (auto intro: antisym)
    1.40 +lemma SUP_eq_const:
    1.41 +  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
    1.42 +  by (auto intro: SUP_eqI)
    1.43  
    1.44  lemma INF_eq_iff:
    1.45    "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> (INFIMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
    1.46 -  using INF_eq_const[of I f c] INF_lower[of _ I f] by (auto intro: antisym)
    1.47 +  using INF_eq_const [of I f c] INF_lower [of _ I f]
    1.48 +  by (auto intro: antisym cong del: strong_INF_cong)
    1.49 +
    1.50 +lemma SUP_eq_iff:
    1.51 +  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPREMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
    1.52 +  using SUP_eq_const [of I f c] SUP_upper [of _ I f]
    1.53 +  by (auto intro: antisym cong del: strong_SUP_cong)
    1.54  
    1.55  end
    1.56  
    1.57 @@ -937,10 +947,6 @@
    1.58    -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
    1.59    by (auto simp add: INF_def image_def)
    1.60  
    1.61 -lemma INT_cong [cong]:
    1.62 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Inter>x\<in>A. C x) = (\<Inter>x\<in>B. D x)"
    1.63 -  by (fact INF_cong)
    1.64 -
    1.65  lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
    1.66    by blast
    1.67  
    1.68 @@ -1132,14 +1138,6 @@
    1.69  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"
    1.70    by (auto simp add: SUP_def image_def)
    1.71  
    1.72 -lemma UN_cong [cong]:
    1.73 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
    1.74 -  by (fact SUP_cong)
    1.75 -
    1.76 -lemma strong_UN_cong:
    1.77 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
    1.78 -  by (unfold simp_implies_def) (fact UN_cong)
    1.79 -
    1.80  lemma image_eq_UN: "f ` A = (\<Union>x\<in>A. {f x})"
    1.81    by blast
    1.82