1.1 --- a/src/HOL/Complete_Lattice.thy Sat Jul 16 22:17:27 2011 +0200
1.2 +++ b/src/HOL/Complete_Lattice.thy Sun Jul 17 08:45:06 2011 +0200
1.3 @@ -108,20 +108,6 @@
1.4 with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto
1.5 qed
1.6
1.7 -lemma top_le:
1.8 - "\<top> \<sqsubseteq> x \<Longrightarrow> x = \<top>"
1.9 - by (rule antisym) auto
1.10 -
1.11 -lemma le_bot:
1.12 - "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
1.13 - by (rule antisym) auto
1.14 -
1.15 -lemma not_less_bot [simp]: "\<not> (x \<sqsubset> \<bottom>)"
1.16 - using bot_least [of x] by (auto simp: le_less)
1.17 -
1.18 -lemma not_top_less [simp]: "\<not> (\<top> \<sqsubset> x)"
1.19 - using top_greatest [of x] by (auto simp: le_less)
1.20 -
1.21 lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
1.22 using Sup_upper[of u A] by auto
1.23
1.24 @@ -222,6 +208,12 @@
1.25 lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)"
1.26 by (iprover intro: SUP_leI le_SUPI order_trans antisym)
1.27
1.28 +lemma INFI_insert: "(\<Sqinter>x\<in>insert a A. B x) = B a \<sqinter> INFI A B"
1.29 + by (simp add: INFI_def Inf_insert)
1.30 +
1.31 +lemma SUPR_insert: "(\<Squnion>x\<in>insert a A. B x) = B a \<squnion> SUPR A B"
1.32 + by (simp add: SUPR_def Sup_insert)
1.33 +
1.34 end
1.35
1.36 lemma Inf_less_iff:
1.37 @@ -256,7 +248,7 @@
1.38 "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
1.39
1.40 instance proof
1.41 -qed (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
1.42 +qed (auto simp add: Inf_bool_def Sup_bool_def)
1.43
1.44 end
1.45
1.46 @@ -475,16 +467,20 @@
1.47 lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
1.48 by (unfold INTER_def) blast
1.49
1.50 -lemma INT_D [elim, Pure.elim]: "b : (\<Inter>x\<in>A. B x) \<Longrightarrow> a:A \<Longrightarrow> b: B a"
1.51 +lemma INT_D [elim, Pure.elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> B a"
1.52 by auto
1.53
1.54 -lemma INT_E [elim]: "b : (\<Inter>x\<in>A. B x) \<Longrightarrow> (b: B a \<Longrightarrow> R) \<Longrightarrow> (a~:A \<Longrightarrow> R) \<Longrightarrow> R"
1.55 - -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}
1.56 +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"
1.57 + -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
1.58 by (unfold INTER_def) blast
1.59
1.60 +lemma (in complete_lattice) INFI_cong:
1.61 + "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.62 + by (simp add: INFI_def image_def)
1.63 +
1.64 lemma INT_cong [cong]:
1.65 - "A = B \<Longrightarrow> (\<And>x. x:B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Inter>x\<in>A. C x) = (\<Inter>x\<in>B. D x)"
1.66 - by (simp add: INTER_def)
1.67 + "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.68 + by (fact INFI_cong)
1.69
1.70 lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
1.71 by blast
1.72 @@ -498,17 +494,31 @@
1.73 lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
1.74 by (fact le_INFI)
1.75
1.76 +lemma (in complete_lattice) INFI_empty:
1.77 + "(\<Sqinter>x\<in>{}. B x) = \<top>"
1.78 + by (simp add: INFI_def)
1.79 +
1.80 lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
1.81 - by blast
1.82 + by (fact INFI_empty)
1.83 +
1.84 +lemma (in complete_lattice) INFI_absorb:
1.85 + assumes "k \<in> I"
1.86 + shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
1.87 +proof -
1.88 + from assms obtain J where "I = insert k J" by blast
1.89 + then show ?thesis by (simp add: INFI_insert)
1.90 +qed
1.91
1.92 lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
1.93 - by blast
1.94 + by (fact INFI_absorb)
1.95
1.96 -lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
1.97 +lemma INT_subset_iff: "B \<subseteq> (\<Inter>i\<in>I. A i) \<longleftrightarrow> (\<forall>i\<in>I. B \<subseteq> A i)"
1.98 by (fact le_INF_iff)
1.99
1.100 lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
1.101 - by blast
1.102 + by (fact INFI_insert)
1.103 +
1.104 +-- {* continue generalization from here *}
1.105
1.106 lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
1.107 by blast
1.108 @@ -524,10 +534,10 @@
1.109 -- {* Look: it has an \emph{existential} quantifier *}
1.110 by blast
1.111
1.112 -lemma INTER_UNIV_conv[simp]:
1.113 +lemma INTER_UNIV_conv [simp]:
1.114 "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
1.115 "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
1.116 -by blast+
1.117 + by blast+
1.118
1.119 lemma INT_bool_eq: "(\<Inter>b. A b) = (A True \<inter> A False)"
1.120 by (auto intro: bool_induct)
1.121 @@ -672,23 +682,23 @@
1.122 "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
1.123 by (rule sym) (fact UNION_eq_Union_image)
1.124
1.125 -lemma UN_iff [simp]: "(b: (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b: B x)"
1.126 +lemma UN_iff [simp]: "(b \<in> (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b \<in> B x)"
1.127 by (unfold UNION_def) blast
1.128
1.129 -lemma UN_I [intro]: "a:A \<Longrightarrow> b: B a \<Longrightarrow> b: (\<Union>x\<in>A. B x)"
1.130 +lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"
1.131 -- {* The order of the premises presupposes that @{term A} is rigid;
1.132 @{term b} may be flexible. *}
1.133 by auto
1.134
1.135 -lemma UN_E [elim!]: "b : (\<Union>x\<in>A. B x) \<Longrightarrow> (\<And>x. x:A \<Longrightarrow> b: B x \<Longrightarrow> R) \<Longrightarrow> R"
1.136 +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.137 by (unfold UNION_def) blast
1.138
1.139 lemma UN_cong [cong]:
1.140 - "A = B \<Longrightarrow> (\<And>x. x:B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
1.141 + "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.142 by (simp add: UNION_def)
1.143
1.144 lemma strong_UN_cong:
1.145 - "A = B \<Longrightarrow> (\<And>x. x:B =simp=> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
1.146 + "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.147 by (simp add: UNION_def simp_implies_def)
1.148
1.149 lemma image_eq_UN: "f ` A = (\<Union>x\<in>A. {f x})"
1.150 @@ -838,84 +848,84 @@
1.151
1.152 lemma UN_simps [simp]:
1.153 "\<And>a B C. (\<Union>x\<in>C. insert a (B x)) = (if C={} then {} else insert a (\<Union>x\<in>C. B x))"
1.154 - "\<And>A B C. (\<Union>x\<in>C. A x \<union> B) = ((if C={} then {} else (\<Union>x\<in>C. A x) \<union> B))"
1.155 - "\<And>A B C. (\<Union>x\<in>C. A \<union> B x) = ((if C={} then {} else A \<union> (\<Union>x\<in>C. B x)))"
1.156 - "\<And>A B C. (\<Union>x\<in>C. A x \<inter> B) = ((\<Union>x\<in>C. A x) \<inter>B)"
1.157 - "\<And>A B C. (\<Union>x\<in>C. A \<inter> B x) = (A \<inter>(\<Union>x\<in>C. B x))"
1.158 - "\<And>A B C. (\<Union>x\<in>C. A x - B) = ((\<Union>x\<in>C. A x) - B)"
1.159 - "\<And>A B C. (\<Union>x\<in>C. A - B x) = (A - (\<Inter>x\<in>C. B x))"
1.160 - "\<And>A B. (UN x: \<Union>A. B x) = (\<Union>y\<in>A. UN x:y. B x)"
1.161 - "\<And>A B C. (UN z: UNION A B. C z) = (\<Union>x\<in>A. UN z: B(x). C z)"
1.162 + "\<And>A B C. (\<Union>x\<in>C. A x \<union> B) = ((if C={} then {} else (\<Union>x\<in>C. A x) \<union> B))"
1.163 + "\<And>A B C. (\<Union>x\<in>C. A \<union> B x) = ((if C={} then {} else A \<union> (\<Union>x\<in>C. B x)))"
1.164 + "\<And>A B C. (\<Union>x\<in>C. A x \<inter> B) = ((\<Union>x\<in>C. A x) \<inter>B)"
1.165 + "\<And>A B C. (\<Union>x\<in>C. A \<inter> B x) = (A \<inter>(\<Union>x\<in>C. B x))"
1.166 + "\<And>A B C. (\<Union>x\<in>C. A x - B) = ((\<Union>x\<in>C. A x) - B)"
1.167 + "\<And>A B C. (\<Union>x\<in>C. A - B x) = (A - (\<Inter>x\<in>C. B x))"
1.168 + "\<And>A B. (\<Union>x\<in>\<Union>A. B x) = (\<Union>y\<in>A. \<Union>x\<in>y. B x)"
1.169 + "\<And>A B C. (\<Union>z\<in>UNION A B. C z) = (\<Union>x\<in>A. \<Union>z\<in>B x. C z)"
1.170 "\<And>A B f. (\<Union>x\<in>f`A. B x) = (\<Union>a\<in>A. B (f a))"
1.171 by auto
1.172
1.173 lemma INT_simps [simp]:
1.174 "\<And>A B C. (\<Inter>x\<in>C. A x \<inter> B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) \<inter>B)"
1.175 "\<And>A B C. (\<Inter>x\<in>C. A \<inter> B x) = (if C={} then UNIV else A \<inter>(\<Inter>x\<in>C. B x))"
1.176 - "\<And>A B C. (\<Inter>x\<in>C. A x - B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) - B)"
1.177 - "\<And>A B C. (\<Inter>x\<in>C. A - B x) = (if C={} then UNIV else A - (\<Union>x\<in>C. B x))"
1.178 + "\<And>A B C. (\<Inter>x\<in>C. A x - B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) - B)"
1.179 + "\<And>A B C. (\<Inter>x\<in>C. A - B x) = (if C={} then UNIV else A - (\<Union>x\<in>C. B x))"
1.180 "\<And>a B C. (\<Inter>x\<in>C. insert a (B x)) = insert a (\<Inter>x\<in>C. B x)"
1.181 - "\<And>A B C. (\<Inter>x\<in>C. A x \<union> B) = ((\<Inter>x\<in>C. A x) \<union> B)"
1.182 - "\<And>A B C. (\<Inter>x\<in>C. A \<union> B x) = (A \<union> (\<Inter>x\<in>C. B x))"
1.183 - "\<And>A B. (INT x: \<Union>A. B x) = (\<Inter>y\<in>A. INT x:y. B x)"
1.184 - "\<And>A B C. (INT z: UNION A B. C z) = (\<Inter>x\<in>A. INT z: B(x). C z)"
1.185 - "\<And>A B f. (INT x:f`A. B x) = (INT a:A. B (f a))"
1.186 + "\<And>A B C. (\<Inter>x\<in>C. A x \<union> B) = ((\<Inter>x\<in>C. A x) \<union> B)"
1.187 + "\<And>A B C. (\<Inter>x\<in>C. A \<union> B x) = (A \<union> (\<Inter>x\<in>C. B x))"
1.188 + "\<And>A B. (\<Inter>x\<in>\<Union>A. B x) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B x)"
1.189 + "\<And>A B C. (\<Inter>z\<in>UNION A B. C z) = (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z)"
1.190 + "\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))"
1.191 by auto
1.192
1.193 lemma ball_simps [simp,no_atp]:
1.194 - "\<And>A P Q. (\<forall>x\<in>A. P x | Q) = ((\<forall>x\<in>A. P x) | Q)"
1.195 - "\<And>A P Q. (\<forall>x\<in>A. P | Q x) = (P | (\<forall>x\<in>A. Q x))"
1.196 - "\<And>A P Q. (\<forall>x\<in>A. P --> Q x) = (P --> (\<forall>x\<in>A. Q x))"
1.197 - "\<And>A P Q. (\<forall>x\<in>A. P x --> Q) = ((\<exists>x\<in>A. P x) --> Q)"
1.198 - "\<And>P. (\<forall> x\<in>{}. P x) = True"
1.199 - "\<And>P. (\<forall> x\<in>UNIV. P x) = (ALL x. P x)"
1.200 - "\<And>a B P. (\<forall> x\<in>insert a B. P x) = (P a & (\<forall> x\<in>B. P x))"
1.201 - "\<And>A P. (\<forall> x\<in>\<Union>A. P x) = (\<forall>y\<in>A. \<forall> x\<in>y. P x)"
1.202 - "\<And>A B P. (\<forall> x\<in> UNION A B. P x) = (\<forall>a\<in>A. \<forall> x\<in> B a. P x)"
1.203 - "\<And>P Q. (\<forall> x\<in>Collect Q. P x) = (ALL x. Q x --> P x)"
1.204 - "\<And>A P f. (\<forall> x\<in>f`A. P x) = (\<forall>x\<in>A. P (f x))"
1.205 - "\<And>A P. (~(\<forall>x\<in>A. P x)) = (\<exists>x\<in>A. ~P x)"
1.206 + "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)"
1.207 + "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))"
1.208 + "\<And>A P Q. (\<forall>x\<in>A. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q x))"
1.209 + "\<And>A P Q. (\<forall>x\<in>A. P x \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<longrightarrow> Q)"
1.210 + "\<And>P. (\<forall>x\<in>{}. P x) \<longleftrightarrow> True"
1.211 + "\<And>P. (\<forall>x\<in>UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"
1.212 + "\<And>a B P. (\<forall>x\<in>insert a B. P x) \<longleftrightarrow> (P a \<and> (\<forall>x\<in>B. P x))"
1.213 + "\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)"
1.214 + "\<And>A B P. (\<forall>x\<in> UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
1.215 + "\<And>P Q. (\<forall>x\<in>Collect Q. P x) \<longleftrightarrow> (\<forall>x. Q x \<longrightarrow> P x)"
1.216 + "\<And>A P f. (\<forall>x\<in>f`A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P (f x))"
1.217 + "\<And>A P. (\<not> (\<forall>x\<in>A. P x)) \<longleftrightarrow> (\<exists>x\<in>A. \<not> P x)"
1.218 by auto
1.219
1.220 lemma bex_simps [simp,no_atp]:
1.221 - "\<And>A P Q. (\<exists>x\<in>A. P x & Q) = ((\<exists>x\<in>A. P x) & Q)"
1.222 - "\<And>A P Q. (\<exists>x\<in>A. P & Q x) = (P & (\<exists>x\<in>A. Q x))"
1.223 - "\<And>P. (EX x:{}. P x) = False"
1.224 - "\<And>P. (EX x:UNIV. P x) = (EX x. P x)"
1.225 - "\<And>a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))"
1.226 - "\<And>A P. (EX x:\<Union>A. P x) = (EX y:A. EX x:y. P x)"
1.227 - "\<And>A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)"
1.228 - "\<And>P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)"
1.229 - "\<And>A P f. (EX x:f`A. P x) = (\<exists>x\<in>A. P (f x))"
1.230 - "\<And>A P. (~(\<exists>x\<in>A. P x)) = (\<forall>x\<in>A. ~P x)"
1.231 + "\<And>A P Q. (\<exists>x\<in>A. P x \<and> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<and> Q)"
1.232 + "\<And>A P Q. (\<exists>x\<in>A. P \<and> Q x) \<longleftrightarrow> (P \<and> (\<exists>x\<in>A. Q x))"
1.233 + "\<And>P. (\<exists>x\<in>{}. P x) \<longleftrightarrow> False"
1.234 + "\<And>P. (\<exists>x\<in>UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"
1.235 + "\<And>a B P. (\<exists>x\<in>insert a B. P x) \<longleftrightarrow> (P a | (\<exists>x\<in>B. P x))"
1.236 + "\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)"
1.237 + "\<And>A B P. (\<exists>x\<in>UNION A B. P x) \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x\<in>B a. P x)"
1.238 + "\<And>P Q. (\<exists>x\<in>Collect Q. P x) \<longleftrightarrow> (\<exists>x. Q x \<and> P x)"
1.239 + "\<And>A P f. (\<exists>x\<in>f`A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))"
1.240 + "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
1.241 by auto
1.242
1.243 text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
1.244
1.245 lemma UN_extend_simps:
1.246 "\<And>a B C. insert a (\<Union>x\<in>C. B x) = (if C={} then {a} else (\<Union>x\<in>C. insert a (B x)))"
1.247 - "\<And>A B C. (\<Union>x\<in>C. A x) \<union> B = (if C={} then B else (\<Union>x\<in>C. A x \<union> B))"
1.248 - "\<And>A B C. A \<union> (\<Union>x\<in>C. B x) = (if C={} then A else (\<Union>x\<in>C. A \<union> B x))"
1.249 - "\<And>A B C. ((\<Union>x\<in>C. A x) \<inter>B) = (\<Union>x\<in>C. A x \<inter> B)"
1.250 - "\<And>A B C. (A \<inter>(\<Union>x\<in>C. B x)) = (\<Union>x\<in>C. A \<inter> B x)"
1.251 + "\<And>A B C. (\<Union>x\<in>C. A x) \<union> B = (if C={} then B else (\<Union>x\<in>C. A x \<union> B))"
1.252 + "\<And>A B C. A \<union> (\<Union>x\<in>C. B x) = (if C={} then A else (\<Union>x\<in>C. A \<union> B x))"
1.253 + "\<And>A B C. ((\<Union>x\<in>C. A x) \<inter> B) = (\<Union>x\<in>C. A x \<inter> B)"
1.254 + "\<And>A B C. (A \<inter> (\<Union>x\<in>C. B x)) = (\<Union>x\<in>C. A \<inter> B x)"
1.255 "\<And>A B C. ((\<Union>x\<in>C. A x) - B) = (\<Union>x\<in>C. A x - B)"
1.256 "\<And>A B C. (A - (\<Inter>x\<in>C. B x)) = (\<Union>x\<in>C. A - B x)"
1.257 - "\<And>A B. (\<Union>y\<in>A. UN x:y. B x) = (UN x: \<Union>A. B x)"
1.258 - "\<And>A B C. (\<Union>x\<in>A. UN z: B(x). C z) = (UN z: UNION A B. C z)"
1.259 + "\<And>A B. (\<Union>y\<in>A. \<Union>x\<in>y. B x) = (\<Union>x\<in>\<Union>A. B x)"
1.260 + "\<And>A B C. (\<Union>x\<in>A. \<Union>z\<in>B x. C z) = (\<Union>z\<in>UNION A B. C z)"
1.261 "\<And>A B f. (\<Union>a\<in>A. B (f a)) = (\<Union>x\<in>f`A. B x)"
1.262 by auto
1.263
1.264 lemma INT_extend_simps:
1.265 - "\<And>A B C. (\<Inter>x\<in>C. A x) \<inter>B = (if C={} then B else (\<Inter>x\<in>C. A x \<inter> B))"
1.266 - "\<And>A B C. A \<inter>(\<Inter>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A \<inter> B x))"
1.267 - "\<And>A B C. (\<Inter>x\<in>C. A x) - B = (if C={} then UNIV - B else (\<Inter>x\<in>C. A x - B))"
1.268 - "\<And>A B C. A - (\<Union>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A - B x))"
1.269 + "\<And>A B C. (\<Inter>x\<in>C. A x) \<inter> B = (if C={} then B else (\<Inter>x\<in>C. A x \<inter> B))"
1.270 + "\<And>A B C. A \<inter> (\<Inter>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A \<inter> B x))"
1.271 + "\<And>A B C. (\<Inter>x\<in>C. A x) - B = (if C={} then UNIV - B else (\<Inter>x\<in>C. A x - B))"
1.272 + "\<And>A B C. A - (\<Union>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A - B x))"
1.273 "\<And>a B C. insert a (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. insert a (B x))"
1.274 - "\<And>A B C. ((\<Inter>x\<in>C. A x) \<union> B) = (\<Inter>x\<in>C. A x \<union> B)"
1.275 - "\<And>A B C. A \<union> (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. A \<union> B x)"
1.276 - "\<And>A B. (\<Inter>y\<in>A. INT x:y. B x) = (INT x: \<Union>A. B x)"
1.277 - "\<And>A B C. (\<Inter>x\<in>A. INT z: B(x). C z) = (INT z: UNION A B. C z)"
1.278 - "\<And>A B f. (INT a:A. B (f a)) = (INT x:f`A. B x)"
1.279 + "\<And>A B C. ((\<Inter>x\<in>C. A x) \<union> B) = (\<Inter>x\<in>C. A x \<union> B)"
1.280 + "\<And>A B C. A \<union> (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. A \<union> B x)"
1.281 + "\<And>A B. (\<Inter>y\<in>A. \<Inter>x\<in>y. B x) = (\<Inter>x\<in>\<Union>A. B x)"
1.282 + "\<And>A B C. (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z) = (\<Inter>z\<in>UNION A B. C z)"
1.283 + "\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
1.284 by auto
1.285
1.286
2.1 --- a/src/HOL/Orderings.thy Sat Jul 16 22:17:27 2011 +0200
2.2 +++ b/src/HOL/Orderings.thy Sun Jul 17 08:45:06 2011 +0200
2.3 @@ -1084,35 +1084,54 @@
2.4 subsection {* (Unique) top and bottom elements *}
2.5
2.6 class bot = order +
2.7 - fixes bot :: 'a
2.8 - assumes bot_least [simp]: "bot \<le> x"
2.9 + fixes bot :: 'a ("\<bottom>")
2.10 + assumes bot_least [simp]: "\<bottom> \<le> a"
2.11 begin
2.12
2.13 +lemma le_bot:
2.14 + "a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
2.15 + by (auto intro: antisym)
2.16 +
2.17 lemma bot_unique:
2.18 - "a \<le> bot \<longleftrightarrow> a = bot"
2.19 - by (auto simp add: intro: antisym)
2.20 + "a \<le> \<bottom> \<longleftrightarrow> a = \<bottom>"
2.21 + by (auto intro: antisym)
2.22 +
2.23 +lemma not_less_bot [simp]:
2.24 + "\<not> (a < \<bottom>)"
2.25 + using bot_least [of a] by (auto simp: le_less)
2.26
2.27 lemma bot_less:
2.28 - "a \<noteq> bot \<longleftrightarrow> bot < a"
2.29 + "a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a"
2.30 by (auto simp add: less_le_not_le intro!: antisym)
2.31
2.32 end
2.33
2.34 class top = order +
2.35 - fixes top :: 'a
2.36 - assumes top_greatest [simp]: "x \<le> top"
2.37 + fixes top :: 'a ("\<top>")
2.38 + assumes top_greatest [simp]: "a \<le> \<top>"
2.39 begin
2.40
2.41 +lemma top_le:
2.42 + "\<top> \<le> a \<Longrightarrow> a = \<top>"
2.43 + by (rule antisym) auto
2.44 +
2.45 lemma top_unique:
2.46 - "top \<le> a \<longleftrightarrow> a = top"
2.47 - by (auto simp add: intro: antisym)
2.48 + "\<top> \<le> a \<longleftrightarrow> a = \<top>"
2.49 + by (auto intro: antisym)
2.50 +
2.51 +lemma not_top_less [simp]: "\<not> (\<top> < a)"
2.52 + using top_greatest [of a] by (auto simp: le_less)
2.53
2.54 lemma less_top:
2.55 - "a \<noteq> top \<longleftrightarrow> a < top"
2.56 + "a \<noteq> \<top> \<longleftrightarrow> a < \<top>"
2.57 by (auto simp add: less_le_not_le intro!: antisym)
2.58
2.59 end
2.60
2.61 +no_notation
2.62 + bot ("\<bottom>") and
2.63 + top ("\<top>")
2.64 +
2.65
2.66 subsection {* Dense orders *}
2.67