src/HOL/Set.thy
changeset 32115 8f10fb3bb46e
parent 32082 90d03908b3d7
child 32117 0762b9ad83df
     1.1 --- a/src/HOL/Set.thy	Mon Jul 20 16:50:59 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Jul 21 07:54:44 2009 +0200
     1.3 @@ -1136,10 +1136,43 @@
     1.4    by rule (simp add: Sup_fun_def, simp add: empty_def)
     1.5  
     1.6  
     1.7 +subsubsection {* Union *}
     1.8 +
     1.9 +definition Union :: "'a set set \<Rightarrow> 'a set" where
    1.10 +  Union_eq [code del]: "Union A = {x. \<exists>B \<in> A. x \<in> B}"
    1.11 +
    1.12 +notation (xsymbols)
    1.13 +  Union  ("\<Union>_" [90] 90)
    1.14 +
    1.15 +lemma Sup_set_eq:
    1.16 +  "\<Squnion>S = \<Union>S"
    1.17 +proof (rule set_ext)
    1.18 +  fix x
    1.19 +  have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
    1.20 +    by auto
    1.21 +  then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
    1.22 +    by (simp add: Sup_fun_def Sup_bool_def Union_eq) (simp add: mem_def)
    1.23 +qed
    1.24 +
    1.25 +lemma Union_iff [simp, noatp]:
    1.26 +  "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
    1.27 +  by (unfold Union_eq) blast
    1.28 +
    1.29 +lemma UnionI [intro]:
    1.30 +  "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
    1.31 +  -- {* The order of the premises presupposes that @{term C} is rigid;
    1.32 +    @{term A} may be flexible. *}
    1.33 +  by auto
    1.34 +
    1.35 +lemma UnionE [elim!]:
    1.36 +  "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A\<in>X \<Longrightarrow> X\<in>C \<Longrightarrow> R) \<Longrightarrow> R"
    1.37 +  by auto
    1.38 +
    1.39 +
    1.40  subsubsection {* Unions of families *}
    1.41  
    1.42  definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
    1.43 -  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
    1.44 +  UNION_eq_Union_image: "UNION A B = \<Union>(B`A)"
    1.45  
    1.46  syntax
    1.47    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
    1.48 @@ -1177,8 +1210,22 @@
    1.49  in [(@{const_syntax UNION}, btr' "@UNION")] end
    1.50  *}
    1.51  
    1.52 -declare UNION_def [noatp]
    1.53 -
    1.54 +lemma SUPR_set_eq:
    1.55 +  "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
    1.56 +  by (simp add: SUPR_def UNION_eq_Union_image Sup_set_eq)
    1.57 +
    1.58 +lemma Union_def:
    1.59 +  "\<Union>S \<equiv> \<Union>x\<in>S. x"
    1.60 +  by (simp add: UNION_eq_Union_image image_def)
    1.61 +
    1.62 +lemma UNION_def [noatp]:
    1.63 +  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
    1.64 +  by (rule eq_reflection) (auto simp add: UNION_eq_Union_image Union_eq)
    1.65 +  
    1.66 +lemma Union_image_eq [simp]:
    1.67 +  "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
    1.68 +  by (rule sym) (fact UNION_eq_Union_image)
    1.69 +  
    1.70  lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
    1.71    by (unfold UNION_def) blast
    1.72  
    1.73 @@ -1202,10 +1249,49 @@
    1.74    by blast
    1.75  
    1.76  
    1.77 +subsubsection {* Inter *}
    1.78 +
    1.79 +definition Inter :: "'a set set \<Rightarrow> 'a set" where
    1.80 +  Inter_eq [code del]: "Inter A = {x. \<forall>B \<in> A. x \<in> B}"
    1.81 +
    1.82 +notation (xsymbols)
    1.83 +  Inter  ("\<Inter>_" [90] 90)
    1.84 +
    1.85 +lemma Inf_set_eq:
    1.86 +  "\<Sqinter>S = \<Inter>S"
    1.87 +proof (rule set_ext)
    1.88 +  fix x
    1.89 +  have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
    1.90 +    by auto
    1.91 +  then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
    1.92 +    by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
    1.93 +qed
    1.94 +
    1.95 +lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
    1.96 +  by (unfold Inter_eq) blast
    1.97 +
    1.98 +lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
    1.99 +  by (simp add: Inter_eq)
   1.100 +
   1.101 +text {*
   1.102 +  \medskip A ``destruct'' rule -- every @{term X} in @{term C}
   1.103 +  contains @{term A} as an element, but @{prop "A:X"} can hold when
   1.104 +  @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
   1.105 +*}
   1.106 +
   1.107 +lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
   1.108 +  by auto
   1.109 +
   1.110 +lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
   1.111 +  -- {* ``Classical'' elimination rule -- does not require proving
   1.112 +    @{prop "X:C"}. *}
   1.113 +  by (unfold Inter_eq) blast
   1.114 +
   1.115 +
   1.116  subsubsection {* Intersections of families *}
   1.117  
   1.118  definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   1.119 -  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
   1.120 +  INTER_eq_Inter_image: "INTER A B = \<Inter>(B`A)"
   1.121  
   1.122  syntax
   1.123    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
   1.124 @@ -1234,6 +1320,22 @@
   1.125  in [(@{const_syntax INTER}, btr' "@INTER")] end
   1.126  *}
   1.127  
   1.128 +lemma INFI_set_eq:
   1.129 +  "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
   1.130 +  by (simp add: INFI_def INTER_eq_Inter_image Inf_set_eq)
   1.131 +
   1.132 +lemma Inter_def:
   1.133 +  "Inter S \<equiv> INTER S (\<lambda>x. x)"
   1.134 +  by (simp add: INTER_eq_Inter_image image_def)
   1.135 +
   1.136 +lemma INTER_def:
   1.137 +  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
   1.138 +  by (rule eq_reflection) (auto simp add: INTER_eq_Inter_image Inter_eq)
   1.139 +
   1.140 +lemma Inter_image_eq [simp]:
   1.141 +  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   1.142 +  by (rule sym) (fact INTER_eq_Inter_image)
   1.143 +
   1.144  lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
   1.145    by (unfold INTER_def) blast
   1.146  
   1.147 @@ -1252,99 +1354,6 @@
   1.148    by (simp add: INTER_def)
   1.149  
   1.150  
   1.151 -subsubsection {* Union *}
   1.152 -
   1.153 -definition Union :: "'a set set \<Rightarrow> 'a set" where
   1.154 -  "Union S \<equiv> UNION S (\<lambda>x. x)"
   1.155 -
   1.156 -notation (xsymbols)
   1.157 -  Union  ("\<Union>_" [90] 90)
   1.158 -
   1.159 -lemma Union_image_eq [simp]:
   1.160 -  "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
   1.161 -  by (auto simp add: Union_def UNION_def image_def)
   1.162 -
   1.163 -lemma Union_eq:
   1.164 -  "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
   1.165 -  by (simp add: Union_def UNION_def)
   1.166 -
   1.167 -lemma Sup_set_eq:
   1.168 -  "\<Squnion>S = \<Union>S"
   1.169 -proof (rule set_ext)
   1.170 -  fix x
   1.171 -  have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
   1.172 -    by auto
   1.173 -  then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
   1.174 -    by (simp add: Union_eq Sup_fun_def Sup_bool_def) (simp add: mem_def)
   1.175 -qed
   1.176 -
   1.177 -lemma SUPR_set_eq:
   1.178 -  "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
   1.179 -  by (simp add: SUPR_def Sup_set_eq)
   1.180 -
   1.181 -lemma Union_iff [simp,noatp]: "(A : Union C) = (EX X:C. A:X)"
   1.182 -  by (unfold Union_def) blast
   1.183 -
   1.184 -lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C"
   1.185 -  -- {* The order of the premises presupposes that @{term C} is rigid;
   1.186 -    @{term A} may be flexible. *}
   1.187 -  by auto
   1.188 -
   1.189 -lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R"
   1.190 -  by (unfold Union_def) blast
   1.191 -
   1.192 -
   1.193 -subsubsection {* Inter *}
   1.194 -
   1.195 -definition Inter :: "'a set set \<Rightarrow> 'a set" where
   1.196 -  "Inter S \<equiv> INTER S (\<lambda>x. x)"
   1.197 -
   1.198 -notation (xsymbols)
   1.199 -  Inter  ("\<Inter>_" [90] 90)
   1.200 -
   1.201 -lemma Inter_image_eq [simp]:
   1.202 -  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
   1.203 -  by (auto simp add: Inter_def INTER_def image_def)
   1.204 -
   1.205 -lemma Inter_eq:
   1.206 -  "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
   1.207 -  by (simp add: Inter_def INTER_def)
   1.208 -
   1.209 -lemma Inf_set_eq:
   1.210 -  "\<Sqinter>S = \<Inter>S"
   1.211 -proof (rule set_ext)
   1.212 -  fix x
   1.213 -  have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
   1.214 -    by auto
   1.215 -  then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
   1.216 -    by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
   1.217 -qed
   1.218 -
   1.219 -lemma INFI_set_eq:
   1.220 -  "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
   1.221 -  by (simp add: INFI_def Inf_set_eq)
   1.222 -
   1.223 -lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
   1.224 -  by (unfold Inter_def) blast
   1.225 -
   1.226 -lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
   1.227 -  by (simp add: Inter_def)
   1.228 -
   1.229 -text {*
   1.230 -  \medskip A ``destruct'' rule -- every @{term X} in @{term C}
   1.231 -  contains @{term A} as an element, but @{prop "A:X"} can hold when
   1.232 -  @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
   1.233 -*}
   1.234 -
   1.235 -lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
   1.236 -  by auto
   1.237 -
   1.238 -lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
   1.239 -  -- {* ``Classical'' elimination rule -- does not require proving
   1.240 -    @{prop "X:C"}. *}
   1.241 -  by (unfold Inter_def) blast
   1.242 -
   1.243 -
   1.244  no_notation
   1.245    less_eq  (infix "\<sqsubseteq>" 50) and
   1.246    less (infix "\<sqsubset>" 50) and