1.1 --- a/src/HOL/Complete_Lattice.thy Sat Jul 16 00:01:17 2011 +0200
1.2 +++ b/src/HOL/Complete_Lattice.thy Sat Jul 16 21:53:50 2011 +0200
1.3 @@ -256,7 +256,7 @@
1.4 "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
1.5
1.6 instance proof
1.7 -qed (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
1.8 +qed (auto simp add: Inf_bool_def Sup_bool_def)
1.9
1.10 end
1.11
1.12 @@ -475,15 +475,15 @@
1.13 lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
1.14 by (unfold INTER_def) blast
1.15
1.16 -lemma INT_D [elim, Pure.elim]: "b : (\<Inter>x\<in>A. B x) \<Longrightarrow> a:A \<Longrightarrow> b: B a"
1.17 +lemma INT_D [elim, Pure.elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> B a"
1.18 by auto
1.19
1.20 -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.21 - -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}
1.22 +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.23 + -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
1.24 by (unfold INTER_def) blast
1.25
1.26 lemma INT_cong [cong]:
1.27 - "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.28 + "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.29 by (simp add: INTER_def)
1.30
1.31 lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
1.32 @@ -672,23 +672,23 @@
1.33 "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
1.34 by (rule sym) (fact UNION_eq_Union_image)
1.35
1.36 -lemma UN_iff [simp]: "(b: (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b: B x)"
1.37 +lemma UN_iff [simp]: "(b \<in> (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b \<in> B x)"
1.38 by (unfold UNION_def) blast
1.39
1.40 -lemma UN_I [intro]: "a:A \<Longrightarrow> b: B a \<Longrightarrow> b: (\<Union>x\<in>A. B x)"
1.41 +lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"
1.42 -- {* The order of the premises presupposes that @{term A} is rigid;
1.43 @{term b} may be flexible. *}
1.44 by auto
1.45
1.46 -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.47 +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.48 by (unfold UNION_def) blast
1.49
1.50 lemma UN_cong [cong]:
1.51 - "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.52 + "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.53 by (simp add: UNION_def)
1.54
1.55 lemma strong_UN_cong:
1.56 - "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.57 + "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.58 by (simp add: UNION_def simp_implies_def)
1.59
1.60 lemma image_eq_UN: "f ` A = (\<Union>x\<in>A. {f x})"
1.61 @@ -838,84 +838,84 @@
1.62
1.63 lemma UN_simps [simp]:
1.64 "\<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.65 - "\<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.66 - "\<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.67 - "\<And>A B C. (\<Union>x\<in>C. A x \<inter> B) = ((\<Union>x\<in>C. A x) \<inter>B)"
1.68 - "\<And>A B C. (\<Union>x\<in>C. A \<inter> B x) = (A \<inter>(\<Union>x\<in>C. B x))"
1.69 - "\<And>A B C. (\<Union>x\<in>C. A x - B) = ((\<Union>x\<in>C. A x) - B)"
1.70 - "\<And>A B C. (\<Union>x\<in>C. A - B x) = (A - (\<Inter>x\<in>C. B x))"
1.71 - "\<And>A B. (UN x: \<Union>A. B x) = (\<Union>y\<in>A. UN x:y. B x)"
1.72 - "\<And>A B C. (UN z: UNION A B. C z) = (\<Union>x\<in>A. UN z: B(x). C z)"
1.73 + "\<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.74 + "\<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.75 + "\<And>A B C. (\<Union>x\<in>C. A x \<inter> B) = ((\<Union>x\<in>C. A x) \<inter>B)"
1.76 + "\<And>A B C. (\<Union>x\<in>C. A \<inter> B x) = (A \<inter>(\<Union>x\<in>C. B x))"
1.77 + "\<And>A B C. (\<Union>x\<in>C. A x - B) = ((\<Union>x\<in>C. A x) - B)"
1.78 + "\<And>A B C. (\<Union>x\<in>C. A - B x) = (A - (\<Inter>x\<in>C. B x))"
1.79 + "\<And>A B. (\<Union>x\<in>\<Union>A. B x) = (\<Union>y\<in>A. \<Union>x\<in>y. B x)"
1.80 + "\<And>A B C. (\<Union>z\<in>UNION A B. C z) = (\<Union>x\<in>A. \<Union>z\<in>B x. C z)"
1.81 "\<And>A B f. (\<Union>x\<in>f`A. B x) = (\<Union>a\<in>A. B (f a))"
1.82 by auto
1.83
1.84 lemma INT_simps [simp]:
1.85 "\<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.86 "\<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.87 - "\<And>A B C. (\<Inter>x\<in>C. A x - B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) - B)"
1.88 - "\<And>A B C. (\<Inter>x\<in>C. A - B x) = (if C={} then UNIV else A - (\<Union>x\<in>C. B x))"
1.89 + "\<And>A B C. (\<Inter>x\<in>C. A x - B) = (if C={} then UNIV else (\<Inter>x\<in>C. A x) - B)"
1.90 + "\<And>A B C. (\<Inter>x\<in>C. A - B x) = (if C={} then UNIV else A - (\<Union>x\<in>C. B x))"
1.91 "\<And>a B C. (\<Inter>x\<in>C. insert a (B x)) = insert a (\<Inter>x\<in>C. B x)"
1.92 - "\<And>A B C. (\<Inter>x\<in>C. A x \<union> B) = ((\<Inter>x\<in>C. A x) \<union> B)"
1.93 - "\<And>A B C. (\<Inter>x\<in>C. A \<union> B x) = (A \<union> (\<Inter>x\<in>C. B x))"
1.94 - "\<And>A B. (INT x: \<Union>A. B x) = (\<Inter>y\<in>A. INT x:y. B x)"
1.95 - "\<And>A B C. (INT z: UNION A B. C z) = (\<Inter>x\<in>A. INT z: B(x). C z)"
1.96 - "\<And>A B f. (INT x:f`A. B x) = (INT a:A. B (f a))"
1.97 + "\<And>A B C. (\<Inter>x\<in>C. A x \<union> B) = ((\<Inter>x\<in>C. A x) \<union> B)"
1.98 + "\<And>A B C. (\<Inter>x\<in>C. A \<union> B x) = (A \<union> (\<Inter>x\<in>C. B x))"
1.99 + "\<And>A B. (\<Inter>x\<in>\<Union>A. B x) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B x)"
1.100 + "\<And>A B C. (\<Inter>z\<in>UNION A B. C z) = (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z)"
1.101 + "\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))"
1.102 by auto
1.103
1.104 lemma ball_simps [simp,no_atp]:
1.105 - "\<And>A P Q. (\<forall>x\<in>A. P x | Q) = ((\<forall>x\<in>A. P x) | Q)"
1.106 - "\<And>A P Q. (\<forall>x\<in>A. P | Q x) = (P | (\<forall>x\<in>A. Q x))"
1.107 - "\<And>A P Q. (\<forall>x\<in>A. P --> Q x) = (P --> (\<forall>x\<in>A. Q x))"
1.108 - "\<And>A P Q. (\<forall>x\<in>A. P x --> Q) = ((\<exists>x\<in>A. P x) --> Q)"
1.109 - "\<And>P. (\<forall> x\<in>{}. P x) = True"
1.110 - "\<And>P. (\<forall> x\<in>UNIV. P x) = (ALL x. P x)"
1.111 - "\<And>a B P. (\<forall> x\<in>insert a B. P x) = (P a & (\<forall> x\<in>B. P x))"
1.112 - "\<And>A P. (\<forall> x\<in>\<Union>A. P x) = (\<forall>y\<in>A. \<forall> x\<in>y. P x)"
1.113 - "\<And>A B P. (\<forall> x\<in> UNION A B. P x) = (\<forall>a\<in>A. \<forall> x\<in> B a. P x)"
1.114 - "\<And>P Q. (\<forall> x\<in>Collect Q. P x) = (ALL x. Q x --> P x)"
1.115 - "\<And>A P f. (\<forall> x\<in>f`A. P x) = (\<forall>x\<in>A. P (f x))"
1.116 - "\<And>A P. (~(\<forall>x\<in>A. P x)) = (\<exists>x\<in>A. ~P x)"
1.117 + "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)"
1.118 + "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))"
1.119 + "\<And>A P Q. (\<forall>x\<in>A. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q x))"
1.120 + "\<And>A P Q. (\<forall>x\<in>A. P x \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<longrightarrow> Q)"
1.121 + "\<And>P. (\<forall>x\<in>{}. P x) \<longleftrightarrow> True"
1.122 + "\<And>P. (\<forall>x\<in>UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"
1.123 + "\<And>a B P. (\<forall>x\<in>insert a B. P x) \<longleftrightarrow> (P a \<and> (\<forall>x\<in>B. P x))"
1.124 + "\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)"
1.125 + "\<And>A B P. (\<forall>x\<in> UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
1.126 + "\<And>P Q. (\<forall>x\<in>Collect Q. P x) \<longleftrightarrow> (\<forall>x. Q x \<longrightarrow> P x)"
1.127 + "\<And>A P f. (\<forall>x\<in>f`A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P (f x))"
1.128 + "\<And>A P. (\<not> (\<forall>x\<in>A. P x)) \<longleftrightarrow> (\<exists>x\<in>A. \<not> P x)"
1.129 by auto
1.130
1.131 lemma bex_simps [simp,no_atp]:
1.132 - "\<And>A P Q. (\<exists>x\<in>A. P x & Q) = ((\<exists>x\<in>A. P x) & Q)"
1.133 - "\<And>A P Q. (\<exists>x\<in>A. P & Q x) = (P & (\<exists>x\<in>A. Q x))"
1.134 - "\<And>P. (EX x:{}. P x) = False"
1.135 - "\<And>P. (EX x:UNIV. P x) = (EX x. P x)"
1.136 - "\<And>a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))"
1.137 - "\<And>A P. (EX x:\<Union>A. P x) = (EX y:A. EX x:y. P x)"
1.138 - "\<And>A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)"
1.139 - "\<And>P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)"
1.140 - "\<And>A P f. (EX x:f`A. P x) = (\<exists>x\<in>A. P (f x))"
1.141 - "\<And>A P. (~(\<exists>x\<in>A. P x)) = (\<forall>x\<in>A. ~P x)"
1.142 + "\<And>A P Q. (\<exists>x\<in>A. P x \<and> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<and> Q)"
1.143 + "\<And>A P Q. (\<exists>x\<in>A. P \<and> Q x) \<longleftrightarrow> (P \<and> (\<exists>x\<in>A. Q x))"
1.144 + "\<And>P. (\<exists>x\<in>{}. P x) \<longleftrightarrow> False"
1.145 + "\<And>P. (\<exists>x\<in>UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"
1.146 + "\<And>a B P. (\<exists>x\<in>insert a B. P x) \<longleftrightarrow> (P a | (\<exists>x\<in>B. P x))"
1.147 + "\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)"
1.148 + "\<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.149 + "\<And>P Q. (\<exists>x\<in>Collect Q. P x) \<longleftrightarrow> (\<exists>x. Q x \<and> P x)"
1.150 + "\<And>A P f. (\<exists>x\<in>f`A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))"
1.151 + "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
1.152 by auto
1.153
1.154 text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
1.155
1.156 lemma UN_extend_simps:
1.157 "\<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.158 - "\<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.159 - "\<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.160 - "\<And>A B C. ((\<Union>x\<in>C. A x) \<inter>B) = (\<Union>x\<in>C. A x \<inter> B)"
1.161 - "\<And>A B C. (A \<inter>(\<Union>x\<in>C. B x)) = (\<Union>x\<in>C. A \<inter> B x)"
1.162 + "\<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.163 + "\<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.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. (A \<inter> (\<Union>x\<in>C. B x)) = (\<Union>x\<in>C. A \<inter> 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. (A - (\<Inter>x\<in>C. B x)) = (\<Union>x\<in>C. A - B x)"
1.168 - "\<And>A B. (\<Union>y\<in>A. UN x:y. B x) = (UN x: \<Union>A. B x)"
1.169 - "\<And>A B C. (\<Union>x\<in>A. UN z: B(x). C z) = (UN z: UNION A B. C z)"
1.170 + "\<And>A B. (\<Union>y\<in>A. \<Union>x\<in>y. B x) = (\<Union>x\<in>\<Union>A. B x)"
1.171 + "\<And>A B C. (\<Union>x\<in>A. \<Union>z\<in>B x. C z) = (\<Union>z\<in>UNION A B. C z)"
1.172 "\<And>A B f. (\<Union>a\<in>A. B (f a)) = (\<Union>x\<in>f`A. B x)"
1.173 by auto
1.174
1.175 lemma INT_extend_simps:
1.176 - "\<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.177 - "\<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.178 - "\<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.179 - "\<And>A B C. A - (\<Union>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A - B x))"
1.180 + "\<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.181 + "\<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.182 + "\<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.183 + "\<And>A B C. A - (\<Union>x\<in>C. B x) = (if C={} then A else (\<Inter>x\<in>C. A - B x))"
1.184 "\<And>a B C. insert a (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. insert a (B x))"
1.185 - "\<And>A B C. ((\<Inter>x\<in>C. A x) \<union> B) = (\<Inter>x\<in>C. A x \<union> B)"
1.186 - "\<And>A B C. A \<union> (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. A \<union> B x)"
1.187 - "\<And>A B. (\<Inter>y\<in>A. INT x:y. B x) = (INT x: \<Union>A. B x)"
1.188 - "\<And>A B C. (\<Inter>x\<in>A. INT z: B(x). C z) = (INT z: UNION A B. C z)"
1.189 - "\<And>A B f. (INT a:A. B (f a)) = (INT x:f`A. B x)"
1.190 + "\<And>A B C. ((\<Inter>x\<in>C. A x) \<union> B) = (\<Inter>x\<in>C. A x \<union> B)"
1.191 + "\<And>A B C. A \<union> (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. A \<union> B x)"
1.192 + "\<And>A B. (\<Inter>y\<in>A. \<Inter>x\<in>y. B x) = (\<Inter>x\<in>\<Union>A. B x)"
1.193 + "\<And>A B C. (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z) = (\<Inter>z\<in>UNION A B. C z)"
1.194 + "\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
1.195 by auto
1.196
1.197