swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
authorhaftmann
Tue Jul 21 07:54:44 2009 +0200 (2009-07-21)
changeset 321158f10fb3bb46e
parent 32114 35084ad81bd4
child 32116 045e7ca3ea74
swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
src/HOL/PReal.thy
src/HOL/Set.thy
     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.4    by rule (simp add: Sup_fun_def, simp add: empty_def)
     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.22 +    by (simp add: Sup_fun_def Sup_bool_def Union_eq) (simp add: mem_def)
    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.92 +    by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
    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.148    by (simp add: INTER_def)
   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.174 -    by (simp add: Union_eq Sup_fun_def Sup_bool_def) (simp add: mem_def)
   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.216 -    by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
   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