1.1 --- a/src/HOL/Complete_Lattice.thy Mon Jul 18 21:34:01 2011 +0200
1.2 +++ b/src/HOL/Complete_Lattice.thy Mon Jul 18 21:49:39 2011 +0200
1.3 @@ -269,6 +269,12 @@
1.4 lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
1.5 by (auto intro: antisym SUP_leI le_SUP_I)
1.6
1.7 +lemma INF_top: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
1.8 + by (cases "A = {}") (simp_all add: INF_empty)
1.9 +
1.10 +lemma SUP_bot: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
1.11 + by (cases "A = {}") (simp_all add: SUP_empty)
1.12 +
1.13 lemma INF_cong:
1.14 "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Sqinter>x\<in>A. C x) = (\<Sqinter>x\<in>B. D x)"
1.15 by (simp add: INF_def image_def)
1.16 @@ -289,7 +295,7 @@
1.17 "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
1.18 by (rule INF_mono) auto
1.19
1.20 -lemma SUPO_subset_mono:
1.21 +lemma SUP_subset_mono:
1.22 "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
1.23 by (rule SUP_mono) auto
1.24
1.25 @@ -366,12 +372,12 @@
1.26 by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
1.27
1.28 lemma INF_mono':
1.29 - "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>B. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
1.30 + "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
1.31 -- {* The last inclusion is POSITIVE! *}
1.32 by (rule INF_mono) auto
1.33
1.34 lemma SUP_mono':
1.35 - "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>B. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
1.36 + "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
1.37 -- {* The last inclusion is POSITIVE! *}
1.38 by (blast intro: SUP_mono dest: subsetD)
1.39
1.40 @@ -680,7 +686,7 @@
1.41 by (fact INF_UNIV_bool_expand)
1.42
1.43 lemma INT_anti_mono:
1.44 - "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>B. g x)"
1.45 + "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
1.46 -- {* The last inclusion is POSITIVE! *}
1.47 by (fact INF_mono')
1.48
1.49 @@ -835,12 +841,12 @@
1.50 by (unfold UNION_def) blast
1.51
1.52 lemma UN_cong [cong]:
1.53 - "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.54 - by (simp add: UNION_def)
1.55 + "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.56 + by (fact SUP_cong)
1.57
1.58 lemma strong_UN_cong:
1.59 - "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.60 - by (simp add: UNION_def simp_implies_def)
1.61 + "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.62 + by (unfold simp_implies_def) (fact UN_cong)
1.63
1.64 lemma image_eq_UN: "f ` A = (\<Union>x\<in>A. {f x})"
1.65 by blast
1.66 @@ -849,7 +855,7 @@
1.67 by (fact le_SUP_I)
1.68
1.69 lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C"
1.70 - by (iprover intro: subsetI elim: UN_E dest: subsetD)
1.71 + by (fact SUP_leI)
1.72
1.73 lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
1.74 by blast
1.75 @@ -857,58 +863,58 @@
1.76 lemma UN_insert_distrib: "u \<in> A \<Longrightarrow> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
1.77 by blast
1.78
1.79 -lemma UN_empty [simp,no_atp]: "(\<Union>x\<in>{}. B x) = {}"
1.80 - by blast
1.81 +lemma UN_empty [simp, no_atp]: "(\<Union>x\<in>{}. B x) = {}"
1.82 + by (fact SUP_empty)
1.83
1.84 lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
1.85 - by blast
1.86 + by (fact SUP_bot)
1.87
1.88 lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
1.89 by blast
1.90
1.91 lemma UN_absorb: "k \<in> I \<Longrightarrow> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
1.92 - by auto
1.93 + by (fact SUP_absorb)
1.94
1.95 lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
1.96 - by blast
1.97 + by (fact SUP_insert)
1.98
1.99 lemma UN_Un[simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
1.100 - by blast
1.101 + by (fact SUP_union)
1.102
1.103 -lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)"
1.104 +lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)" -- "FIXME generalize"
1.105 by blast
1.106
1.107 lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
1.108 by (fact SUP_le_iff)
1.109
1.110 -lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
1.111 - by blast
1.112 -
1.113 lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
1.114 - by auto
1.115 + by (fact SUP_constant)
1.116
1.117 lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
1.118 + by (fact SUP_eq)
1.119 +
1.120 +lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)" -- "FIXME generalize"
1.121 by blast
1.122
1.123 lemma UNION_empty_conv[simp]:
1.124 "{} = (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = {})"
1.125 "(\<Union>x\<in>A. B x) = {} \<longleftrightarrow> (\<forall>x\<in>A. B x = {})"
1.126 -by blast+
1.127 + by (fact SUP_bot_conv)+
1.128
1.129 lemma Collect_ex_eq [no_atp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
1.130 by blast
1.131
1.132 -lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
1.133 +lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
1.134 by blast
1.135
1.136 -lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) = (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
1.137 +lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
1.138 by blast
1.139
1.140 lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
1.141 by (auto simp add: split_if_mem2)
1.142
1.143 lemma UN_bool_eq: "(\<Union>b. A b) = (A True \<union> A False)"
1.144 - by (auto intro: bool_contrapos)
1.145 + by (fact SUP_UNIV_bool_expand)
1.146
1.147 lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)"
1.148 by blast
1.149 @@ -916,7 +922,7 @@
1.150 lemma UN_mono:
1.151 "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow>
1.152 (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
1.153 - by (blast dest: subsetD)
1.154 + by (fact SUP_mono')
1.155
1.156 lemma vimage_Union: "f -` (\<Union>A) = (\<Union>X\<in>A. f -` X)"
1.157 by blast