author haftmann Sat Jul 16 21:53:50 2011 +0200 (2011-07-16) changeset 43852 7411fbf0a325 parent 43843 16f2fd9103bd child 43853 020ddc6a9508
tuned notation
```     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.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.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
```