author haftmann Tue Jul 21 07:54:44 2009 +0200 (2009-07-21) changeset 32115 8f10fb3bb46e parent 32114 35084ad81bd4 child 32116 045e7ca3ea74
swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
 src/HOL/PReal.thy file | annotate | diff | revisions src/HOL/Set.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/PReal.thy	Mon Jul 20 16:50:59 2009 +0200
1.2 +++ b/src/HOL/PReal.thy	Tue Jul 21 07:54:44 2009 +0200
1.3 @@ -52,7 +52,7 @@
1.4
1.5  definition
1.6    psup :: "preal set => preal" where
1.7 -  "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
1.8 +  [code del]: "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
1.9
1.10  definition
1.11    add_set :: "[rat set,rat set] => rat set" where
```
```     2.1 --- a/src/HOL/Set.thy	Mon Jul 20 16:50:59 2009 +0200
2.2 +++ b/src/HOL/Set.thy	Tue Jul 21 07:54:44 2009 +0200
2.3 @@ -1136,10 +1136,43 @@
2.5
2.6
2.7 +subsubsection {* Union *}
2.8 +
2.9 +definition Union :: "'a set set \<Rightarrow> 'a set" where
2.10 +  Union_eq [code del]: "Union A = {x. \<exists>B \<in> A. x \<in> B}"
2.11 +
2.12 +notation (xsymbols)
2.13 +  Union  ("\<Union>_" [90] 90)
2.14 +
2.15 +lemma Sup_set_eq:
2.16 +  "\<Squnion>S = \<Union>S"
2.17 +proof (rule set_ext)
2.18 +  fix x
2.19 +  have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
2.20 +    by auto
2.21 +  then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
2.23 +qed
2.24 +
2.25 +lemma Union_iff [simp, noatp]:
2.26 +  "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
2.27 +  by (unfold Union_eq) blast
2.28 +
2.29 +lemma UnionI [intro]:
2.30 +  "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
2.31 +  -- {* The order of the premises presupposes that @{term C} is rigid;
2.32 +    @{term A} may be flexible. *}
2.33 +  by auto
2.34 +
2.35 +lemma UnionE [elim!]:
2.36 +  "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A\<in>X \<Longrightarrow> X\<in>C \<Longrightarrow> R) \<Longrightarrow> R"
2.37 +  by auto
2.38 +
2.39 +
2.40  subsubsection {* Unions of families *}
2.41
2.42  definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
2.43 -  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
2.44 +  UNION_eq_Union_image: "UNION A B = \<Union>(B`A)"
2.45
2.46  syntax
2.47    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
2.48 @@ -1177,8 +1210,22 @@
2.49  in [(@{const_syntax UNION}, btr' "@UNION")] end
2.50  *}
2.51
2.52 -declare UNION_def [noatp]
2.53 -
2.54 +lemma SUPR_set_eq:
2.55 +  "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
2.56 +  by (simp add: SUPR_def UNION_eq_Union_image Sup_set_eq)
2.57 +
2.58 +lemma Union_def:
2.59 +  "\<Union>S \<equiv> \<Union>x\<in>S. x"
2.60 +  by (simp add: UNION_eq_Union_image image_def)
2.61 +
2.62 +lemma UNION_def [noatp]:
2.63 +  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
2.64 +  by (rule eq_reflection) (auto simp add: UNION_eq_Union_image Union_eq)
2.65 +
2.66 +lemma Union_image_eq [simp]:
2.67 +  "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
2.68 +  by (rule sym) (fact UNION_eq_Union_image)
2.69 +
2.70  lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
2.71    by (unfold UNION_def) blast
2.72
2.73 @@ -1202,10 +1249,49 @@
2.74    by blast
2.75
2.76
2.77 +subsubsection {* Inter *}
2.78 +
2.79 +definition Inter :: "'a set set \<Rightarrow> 'a set" where
2.80 +  Inter_eq [code del]: "Inter A = {x. \<forall>B \<in> A. x \<in> B}"
2.81 +
2.82 +notation (xsymbols)
2.83 +  Inter  ("\<Inter>_" [90] 90)
2.84 +
2.85 +lemma Inf_set_eq:
2.86 +  "\<Sqinter>S = \<Inter>S"
2.87 +proof (rule set_ext)
2.88 +  fix x
2.89 +  have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
2.90 +    by auto
2.91 +  then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
2.93 +qed
2.94 +
2.95 +lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
2.96 +  by (unfold Inter_eq) blast
2.97 +
2.98 +lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
2.99 +  by (simp add: Inter_eq)
2.100 +
2.101 +text {*
2.102 +  \medskip A ``destruct'' rule -- every @{term X} in @{term C}
2.103 +  contains @{term A} as an element, but @{prop "A:X"} can hold when
2.104 +  @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
2.105 +*}
2.106 +
2.107 +lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
2.108 +  by auto
2.109 +
2.110 +lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
2.111 +  -- {* ``Classical'' elimination rule -- does not require proving
2.112 +    @{prop "X:C"}. *}
2.113 +  by (unfold Inter_eq) blast
2.114 +
2.115 +
2.116  subsubsection {* Intersections of families *}
2.117
2.118  definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
2.119 -  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
2.120 +  INTER_eq_Inter_image: "INTER A B = \<Inter>(B`A)"
2.121
2.122  syntax
2.123    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
2.124 @@ -1234,6 +1320,22 @@
2.125  in [(@{const_syntax INTER}, btr' "@INTER")] end
2.126  *}
2.127
2.128 +lemma INFI_set_eq:
2.129 +  "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
2.130 +  by (simp add: INFI_def INTER_eq_Inter_image Inf_set_eq)
2.131 +
2.132 +lemma Inter_def:
2.133 +  "Inter S \<equiv> INTER S (\<lambda>x. x)"
2.134 +  by (simp add: INTER_eq_Inter_image image_def)
2.135 +
2.136 +lemma INTER_def:
2.137 +  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
2.138 +  by (rule eq_reflection) (auto simp add: INTER_eq_Inter_image Inter_eq)
2.139 +
2.140 +lemma Inter_image_eq [simp]:
2.141 +  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
2.142 +  by (rule sym) (fact INTER_eq_Inter_image)
2.143 +
2.144  lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
2.145    by (unfold INTER_def) blast
2.146
2.147 @@ -1252,99 +1354,6 @@
2.149
2.150
2.151 -subsubsection {* Union *}
2.152 -
2.153 -definition Union :: "'a set set \<Rightarrow> 'a set" where
2.154 -  "Union S \<equiv> UNION S (\<lambda>x. x)"
2.155 -
2.156 -notation (xsymbols)
2.157 -  Union  ("\<Union>_" [90] 90)
2.158 -
2.159 -lemma Union_image_eq [simp]:
2.160 -  "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
2.161 -  by (auto simp add: Union_def UNION_def image_def)
2.162 -
2.163 -lemma Union_eq:
2.164 -  "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
2.165 -  by (simp add: Union_def UNION_def)
2.166 -
2.167 -lemma Sup_set_eq:
2.168 -  "\<Squnion>S = \<Union>S"
2.169 -proof (rule set_ext)
2.170 -  fix x
2.171 -  have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
2.172 -    by auto
2.173 -  then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
2.175 -qed
2.176 -
2.177 -lemma SUPR_set_eq:
2.178 -  "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
2.179 -  by (simp add: SUPR_def Sup_set_eq)
2.180 -
2.181 -lemma Union_iff [simp,noatp]: "(A : Union C) = (EX X:C. A:X)"
2.182 -  by (unfold Union_def) blast
2.183 -
2.184 -lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C"
2.185 -  -- {* The order of the premises presupposes that @{term C} is rigid;
2.186 -    @{term A} may be flexible. *}
2.187 -  by auto
2.188 -
2.189 -lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R"
2.190 -  by (unfold Union_def) blast
2.191 -
2.192 -
2.193 -subsubsection {* Inter *}
2.194 -
2.195 -definition Inter :: "'a set set \<Rightarrow> 'a set" where
2.196 -  "Inter S \<equiv> INTER S (\<lambda>x. x)"
2.197 -
2.198 -notation (xsymbols)
2.199 -  Inter  ("\<Inter>_" [90] 90)
2.200 -
2.201 -lemma Inter_image_eq [simp]:
2.202 -  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
2.203 -  by (auto simp add: Inter_def INTER_def image_def)
2.204 -
2.205 -lemma Inter_eq:
2.206 -  "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
2.207 -  by (simp add: Inter_def INTER_def)
2.208 -
2.209 -lemma Inf_set_eq:
2.210 -  "\<Sqinter>S = \<Inter>S"
2.211 -proof (rule set_ext)
2.212 -  fix x
2.213 -  have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
2.214 -    by auto
2.215 -  then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
2.217 -qed
2.218 -
2.219 -lemma INFI_set_eq:
2.220 -  "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
2.221 -  by (simp add: INFI_def Inf_set_eq)
2.222 -
2.223 -lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
2.224 -  by (unfold Inter_def) blast
2.225 -
2.226 -lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
2.227 -  by (simp add: Inter_def)
2.228 -
2.229 -text {*
2.230 -  \medskip A ``destruct'' rule -- every @{term X} in @{term C}
2.231 -  contains @{term A} as an element, but @{prop "A:X"} can hold when
2.232 -  @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
2.233 -*}
2.234 -
2.235 -lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
2.236 -  by auto
2.237 -
2.238 -lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
2.239 -  -- {* ``Classical'' elimination rule -- does not require proving
2.240 -    @{prop "X:C"}. *}
2.241 -  by (unfold Inter_def) blast
2.242 -
2.243 -
2.244  no_notation
2.245    less_eq  (infix "\<sqsubseteq>" 50) and
2.246    less (infix "\<sqsubset>" 50) and
```