src/HOL/Set.thy
 changeset 32081 1b7a901e2edc parent 32078 1c14f77201d4 child 32082 90d03908b3d7
```     1.1 --- a/src/HOL/Set.thy	Mon Jul 20 09:52:09 2009 +0200
1.2 +++ b/src/HOL/Set.thy	Mon Jul 20 11:47:17 2009 +0200
1.3 @@ -8,9 +8,7 @@
1.4  imports Lattices
1.5  begin
1.6
1.7 -text {* A set in HOL is simply a predicate. *}
1.8 -
1.9 -subsection {* Basic definitions and syntax *}
1.10 +subsection {* Sets as predicates *}
1.11
1.12  global
1.13
1.14 @@ -49,34 +47,48 @@
1.15    not_mem  ("op \<notin>") and
1.16    not_mem  ("(_/ \<notin> _)" [50, 51] 50)
1.17
1.18 +text {* Set comprehensions *}
1.19 +
1.20  syntax
1.21    "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
1.22
1.23  translations
1.24    "{x. P}"      == "Collect (%x. P)"
1.25
1.26 -definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
1.27 -  "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
1.28 -
1.29 -definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
1.30 -  "A Un B \<equiv> {x. x \<in> A \<or> x \<in> B}"
1.31 -
1.32 -notation (xsymbols)
1.33 -  "Int"  (infixl "\<inter>" 70) and
1.34 -  "Un"  (infixl "\<union>" 65)
1.35 -
1.36 -notation (HTML output)
1.37 -  "Int"  (infixl "\<inter>" 70) and
1.38 -  "Un"  (infixl "\<union>" 65)
1.39 +syntax
1.40 +  "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
1.41 +  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ :/ _./ _})")
1.42 +
1.43 +syntax (xsymbols)
1.44 +  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ \<in>/ _./ _})")
1.45 +
1.46 +translations
1.47 +  "{x:A. P}"    => "{x. x:A & P}"
1.48 +
1.49 +lemma mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
1.50 +  by (simp add: Collect_def mem_def)
1.51 +
1.52 +lemma Collect_mem_eq [simp]: "{x. x:A} = A"
1.53 +  by (simp add: Collect_def mem_def)
1.54 +
1.55 +lemma CollectI: "P(a) ==> a : {x. P(x)}"
1.56 +  by simp
1.57 +
1.58 +lemma CollectD: "a : {x. P(x)} ==> P(a)"
1.59 +  by simp
1.60 +
1.61 +lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
1.62 +  by simp
1.63 +
1.64 +lemmas CollectE = CollectD [elim_format]
1.65 +
1.66 +text {* Set enumerations *}
1.67
1.68  definition empty :: "'a set" ("{}") where
1.69    "empty \<equiv> {x. False}"
1.70
1.71  definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
1.72 -  "insert a B \<equiv> {x. x = a} \<union> B"
1.73 -
1.74 -definition UNIV :: "'a set" where
1.75 -  "UNIV \<equiv> {x. True}"
1.76 +  insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
1.77
1.78  syntax
1.79    "@Finset"     :: "args => 'a set"                       ("{(_)}")
1.80 @@ -85,6 +97,49 @@
1.81    "{x, xs}"     == "CONST insert x {xs}"
1.82    "{x}"         == "CONST insert x {}"
1.83
1.84 +
1.85 +subsection {* Subsets and bounded quantifiers *}
1.86 +
1.87 +abbreviation
1.88 +  subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
1.89 +  "subset \<equiv> less"
1.90 +
1.91 +abbreviation
1.92 +  subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
1.93 +  "subset_eq \<equiv> less_eq"
1.94 +
1.95 +notation (output)
1.96 +  subset  ("op <") and
1.97 +  subset  ("(_/ < _)" [50, 51] 50) and
1.98 +  subset_eq  ("op <=") and
1.99 +  subset_eq  ("(_/ <= _)" [50, 51] 50)
1.100 +
1.101 +notation (xsymbols)
1.102 +  subset  ("op \<subset>") and
1.103 +  subset  ("(_/ \<subset> _)" [50, 51] 50) and
1.104 +  subset_eq  ("op \<subseteq>") and
1.105 +  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
1.106 +
1.107 +notation (HTML output)
1.108 +  subset  ("op \<subset>") and
1.109 +  subset  ("(_/ \<subset> _)" [50, 51] 50) and
1.110 +  subset_eq  ("op \<subseteq>") and
1.111 +  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
1.112 +
1.113 +abbreviation (input)
1.114 +  supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
1.115 +  "supset \<equiv> greater"
1.116 +
1.117 +abbreviation (input)
1.118 +  supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
1.119 +  "supset_eq \<equiv> greater_eq"
1.120 +
1.121 +notation (xsymbols)
1.122 +  supset  ("op \<supset>") and
1.123 +  supset  ("(_/ \<supset> _)" [50, 51] 50) and
1.124 +  supset_eq  ("op \<supseteq>") and
1.125 +  supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
1.126 +
1.127  global
1.128
1.129  consts
1.130 @@ -127,63 +182,6 @@
1.131    "EX! x:A. P"  == "Bex1 A (%x. P)"
1.132    "LEAST x:A. P" => "LEAST x. x:A & P"
1.133
1.134 -
1.135 -subsection {* Additional concrete syntax *}
1.136 -
1.137 -syntax
1.138 -  "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
1.139 -  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ :/ _./ _})")
1.140 -
1.141 -syntax (xsymbols)
1.142 -  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ \<in>/ _./ _})")
1.143 -
1.144 -translations
1.145 -  "{x:A. P}"    => "{x. x:A & P}"
1.146 -
1.147 -abbreviation
1.148 -  subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
1.149 -  "subset \<equiv> less"
1.150 -
1.151 -abbreviation
1.152 -  subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
1.153 -  "subset_eq \<equiv> less_eq"
1.154 -
1.155 -notation (output)
1.156 -  subset  ("op <") and
1.157 -  subset  ("(_/ < _)" [50, 51] 50) and
1.158 -  subset_eq  ("op <=") and
1.159 -  subset_eq  ("(_/ <= _)" [50, 51] 50)
1.160 -
1.161 -notation (xsymbols)
1.162 -  subset  ("op \<subset>") and
1.163 -  subset  ("(_/ \<subset> _)" [50, 51] 50) and
1.164 -  subset_eq  ("op \<subseteq>") and
1.165 -  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
1.166 -
1.167 -notation (HTML output)
1.168 -  subset  ("op \<subset>") and
1.169 -  subset  ("(_/ \<subset> _)" [50, 51] 50) and
1.170 -  subset_eq  ("op \<subseteq>") and
1.171 -  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
1.172 -
1.173 -abbreviation (input)
1.174 -  supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
1.175 -  "supset \<equiv> greater"
1.176 -
1.177 -abbreviation (input)
1.178 -  supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
1.179 -  "supset_eq \<equiv> greater_eq"
1.180 -
1.181 -notation (xsymbols)
1.182 -  supset  ("op \<supset>") and
1.183 -  supset  ("(_/ \<supset> _)" [50, 51] 50) and
1.184 -  supset_eq  ("op \<supseteq>") and
1.185 -  supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
1.186 -
1.187 -
1.188 -
1.189 -subsubsection "Bounded quantifiers"
1.190 -
1.191  syntax (output)
1.192    "_setlessAll" :: "[idt, 'a, bool] => bool"  ("(3ALL _<_./ _)"  [0, 0, 10] 10)
1.193    "_setlessEx"  :: "[idt, 'a, bool] => bool"  ("(3EX _<_./ _)"  [0, 0, 10] 10)
1.194 @@ -313,31 +311,6 @@
1.195    in [("Collect", setcompr_tr')] end;
1.196  *}
1.197
1.198 -
1.199 -subsection {* Lemmas and proof tool setup *}
1.200 -
1.201 -subsubsection {* Relating predicates and sets *}
1.202 -
1.203 -lemma mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
1.204 -  by (simp add: Collect_def mem_def)
1.205 -
1.206 -lemma Collect_mem_eq [simp]: "{x. x:A} = A"
1.207 -  by (simp add: Collect_def mem_def)
1.208 -
1.209 -lemma CollectI: "P(a) ==> a : {x. P(x)}"
1.210 -  by simp
1.211 -
1.212 -lemma CollectD: "a : {x. P(x)} ==> P(a)"
1.213 -  by simp
1.214 -
1.215 -lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
1.216 -  by simp
1.217 -
1.218 -lemmas CollectE = CollectD [elim_format]
1.219 -
1.220 -
1.221 -subsubsection {* Bounded quantifiers *}
1.222 -
1.223  lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
1.224    by (simp add: Ball_def)
1.225
1.226 @@ -428,8 +401,7 @@
1.227    Addsimprocs [defBALL_regroup, defBEX_regroup];
1.228  *}
1.229
1.230 -
1.231 -subsubsection {* Congruence rules *}
1.232 +text {* Congruence rules *}
1.233
1.234  lemma ball_cong:
1.235    "A = B ==> (!!x. x:B ==> P x = Q x) ==>
1.236 @@ -452,6 +424,8 @@
1.237    by (simp add: simp_implies_def Bex_def cong: conj_cong)
1.238
1.239
1.240 +subsection {* Basic operations *}
1.241 +
1.242  subsubsection {* Subsets *}
1.243
1.244  lemma subsetI [atp,intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B"
1.245 @@ -499,10 +473,19 @@
1.246    by blast
1.247
1.248  lemma subset_refl [simp,atp]: "A \<subseteq> A"
1.249 -  by fast
1.250 +  by (fact order_refl)
1.251
1.252  lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
1.253 -  by blast
1.254 +  by (fact order_trans)
1.255 +
1.256 +lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B"
1.257 +  by (rule subsetD)
1.258 +
1.259 +lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
1.260 +  by (rule subsetD)
1.261 +
1.262 +lemmas basic_trans_rules [trans] =
1.263 +  order_trans_rules set_rev_mp set_mp
1.264
1.265
1.266  subsubsection {* Equality *}
1.267 @@ -554,6 +537,9 @@
1.268
1.269  subsubsection {* The universal set -- UNIV *}
1.270
1.271 +definition UNIV :: "'a set" where
1.272 +  "UNIV \<equiv> {x. True}"
1.273 +
1.274  lemma UNIV_I [simp]: "x : UNIV"
1.275    by (simp add: UNIV_def)
1.276
1.277 @@ -565,6 +551,9 @@
1.278  lemma subset_UNIV [simp]: "A \<subseteq> UNIV"
1.279    by (rule subsetI) (rule UNIV_I)
1.280
1.281 +lemma top_set_eq: "top = UNIV"
1.282 +  by (iprover intro!: subset_antisym subset_UNIV top_greatest)
1.283 +
1.284  text {*
1.285    \medskip Eta-contracting these two rules (to remove @{text P})
1.286    causes them to be ignored because of their interaction with
1.287 @@ -593,6 +582,9 @@
1.288      -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
1.289    by blast
1.290
1.291 +lemma bot_set_eq: "bot = {}"
1.292 +  by (iprover intro!: subset_antisym empty_subsetI bot_least)
1.293 +
1.294  lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
1.295    by blast
1.296
1.297 @@ -654,6 +646,18 @@
1.298
1.299  subsubsection {* Binary union -- Un *}
1.300
1.301 +definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
1.302 +  "A Un B \<equiv> {x. x \<in> A \<or> x \<in> B}"
1.303 +
1.304 +notation (xsymbols)
1.305 +  "Un"  (infixl "\<union>" 65)
1.306 +
1.307 +notation (HTML output)
1.308 +  "Un"  (infixl "\<union>" 65)
1.309 +
1.310 +lemma sup_set_eq: "sup A B = A \<union> B"
1.311 +  by (simp add: sup_fun_eq sup_bool_eq Un_def Collect_def mem_def)
1.312 +
1.313  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
1.314    by (unfold Un_def) blast
1.315
1.316 @@ -674,9 +678,29 @@
1.317  lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
1.318    by (unfold Un_def) blast
1.319
1.320 +lemma insert_def: "insert a B \<equiv> {x. x = a} \<union> B"
1.321 +  by (simp add: Collect_def mem_def insert_compr Un_def)
1.322 +
1.323 +lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
1.324 +  apply (fold sup_set_eq)
1.325 +  apply (erule mono_sup)
1.326 +  done
1.327 +
1.328
1.329  subsubsection {* Binary intersection -- Int *}
1.330
1.331 +definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
1.332 +  "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
1.333 +
1.334 +notation (xsymbols)
1.335 +  "Int"  (infixl "\<inter>" 70)
1.336 +
1.337 +notation (HTML output)
1.338 +  "Int"  (infixl "\<inter>" 70)
1.339 +
1.340 +lemma inf_set_eq: "inf A B = A \<inter> B"
1.341 +  by (simp add: inf_fun_eq inf_bool_eq Int_def Collect_def mem_def)
1.342 +
1.343  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
1.344    by (unfold Int_def) blast
1.345
1.346 @@ -692,6 +716,11 @@
1.347  lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
1.348    by simp
1.349
1.350 +lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
1.351 +  apply (fold inf_set_eq)
1.352 +  apply (erule mono_inf)
1.353 +  done
1.354 +
1.355
1.356  subsubsection {* Set difference *}
1.357
1.358 @@ -854,6 +883,76 @@
1.359    by blast
1.360
1.361
1.362 +subsubsection {* Some proof tools *}
1.363 +
1.364 +text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
1.365 +
1.366 +lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
1.367 +by auto
1.368 +
1.369 +lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
1.370 +by auto
1.371 +
1.372 +text {*
1.373 +Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
1.374 +to the front (and similarly for @{text "t=x"}):
1.375 +*}
1.376 +
1.377 +ML{*
1.378 +  local
1.379 +    val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
1.380 +    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
1.381 +                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
1.382 +  in
1.383 +    val defColl_regroup = Simplifier.simproc @{theory}
1.384 +      "defined Collect" ["{x. P x & Q x}"]
1.385 +      (Quantifier1.rearrange_Coll Coll_perm_tac)
1.386 +  end;
1.387 +
1.388 +  Addsimprocs [defColl_regroup];
1.389 +*}
1.390 +
1.391 +text {*
1.392 +  Rewrite rules for boolean case-splitting: faster than @{text
1.393 +  "split_if [split]"}.
1.394 +*}
1.395 +
1.396 +lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"
1.397 +  by (rule split_if)
1.398 +
1.399 +lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"
1.400 +  by (rule split_if)
1.401 +
1.402 +text {*
1.403 +  Split ifs on either side of the membership relation.  Not for @{text
1.404 +  "[simp]"} -- can cause goals to blow up!
1.405 +*}
1.406 +
1.407 +lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"
1.408 +  by (rule split_if)
1.409 +
1.410 +lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"
1.411 +  by (rule split_if [where P="%S. a : S"])
1.412 +
1.413 +lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
1.414 +
1.415 +(*Would like to add these, but the existing code only searches for the
1.416 +  outer-level constant, which in this case is just "op :"; we instead need
1.417 +  to use term-nets to associate patterns with rules.  Also, if a rule fails to
1.418 +  apply, then the formula should be kept.
1.419 +  [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]),
1.420 +   ("Int", [IntD1,IntD2]),
1.421 +   ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
1.422 + *)
1.423 +
1.424 +ML {*
1.425 +  val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
1.426 +*}
1.427 +declaration {* fn _ =>
1.428 +  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
1.429 +*}
1.430 +
1.431 +
1.432  subsection {* Complete lattices *}
1.433
1.434  notation
1.435 @@ -989,7 +1088,7 @@
1.436  end
1.437
1.438
1.439 -subsection {* Bool as complete lattice *}
1.440 +subsubsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
1.441
1.442  instantiation bool :: complete_lattice
1.443  begin
1.444 @@ -1013,9 +1112,6 @@
1.445    "\<not> \<Squnion>{}"
1.446    unfolding Sup_bool_def by auto
1.447
1.448 -
1.449 -subsection {* Fun as complete lattice *}
1.450 -
1.451  instantiation "fun" :: (type, complete_lattice) complete_lattice
1.452  begin
1.453
1.454 @@ -1040,47 +1136,24 @@
1.455    by rule (simp add: Sup_fun_def, simp add: empty_def)
1.456
1.457
1.458 -subsection {* Set as lattice *}
1.459 -
1.460 -definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
1.461 -  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
1.462 +subsubsection {* Unions of families *}
1.463
1.464  definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
1.465    "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
1.466
1.467 -definition Inter :: "'a set set \<Rightarrow> 'a set" where
1.468 -  "Inter S \<equiv> INTER S (\<lambda>x. x)"
1.469 -
1.470 -definition Union :: "'a set set \<Rightarrow> 'a set" where
1.471 -  "Union S \<equiv> UNION S (\<lambda>x. x)"
1.472 -
1.473 -notation (xsymbols)
1.474 -  Inter  ("\<Inter>_" [90] 90) and
1.475 -  Union  ("\<Union>_" [90] 90)
1.476 -
1.477  syntax
1.478 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
1.479    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
1.480 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
1.481    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)
1.482
1.483  syntax (xsymbols)
1.484 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
1.485    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
1.486 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
1.487    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
1.488
1.489  syntax (latex output)
1.490 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
1.491    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
1.492 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
1.493    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
1.494
1.495  translations
1.496 -  "INT x y. B"  == "INT x. INT y. B"
1.497 -  "INT x. B"    == "CONST INTER CONST UNIV (%x. B)"
1.498 -  "INT x. B"    == "INT x:CONST UNIV. B"
1.499 -  "INT x:A. B"  == "CONST INTER A (%x. B)"
1.500    "UN x y. B"   == "UN x. UN y. B"
1.501    "UN x. B"     == "CONST UNION CONST UNIV (%x. B)"
1.502    "UN x. B"     == "UN x:CONST UNIV. B"
1.503 @@ -1101,86 +1174,9 @@
1.504    fun btr' syn [A, Abs abs] =
1.505      let val (x, t) = atomic_abs_tr' abs
1.506      in Syntax.const syn \$ x \$ A \$ t end
1.507 -in [(@{const_syntax UNION}, btr' "@UNION"),(@{const_syntax INTER}, btr' "@INTER")] end
1.508 +in [(@{const_syntax UNION}, btr' "@UNION")] end
1.509  *}
1.510
1.511 -lemma Inter_image_eq [simp]:
1.512 -  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
1.513 -  by (auto simp add: Inter_def INTER_def image_def)
1.514 -
1.515 -lemma Union_image_eq [simp]:
1.516 -  "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
1.517 -  by (auto simp add: Union_def UNION_def image_def)
1.518 -
1.519 -lemma inf_set_eq: "A \<sqinter> B = A \<inter> B"
1.520 -  by (simp add: inf_fun_eq inf_bool_eq Int_def Collect_def mem_def)
1.521 -
1.522 -lemma sup_set_eq: "A \<squnion> B = A \<union> B"
1.523 -  by (simp add: sup_fun_eq sup_bool_eq Un_def Collect_def mem_def)
1.524 -
1.525 -lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
1.526 -  apply (fold inf_set_eq sup_set_eq)
1.527 -  apply (erule mono_inf)
1.528 -  done
1.529 -
1.530 -lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
1.531 -  apply (fold inf_set_eq sup_set_eq)
1.532 -  apply (erule mono_sup)
1.533 -  done
1.534 -
1.535 -lemma top_set_eq: "top = UNIV"
1.536 -  by (iprover intro!: subset_antisym subset_UNIV top_greatest)
1.537 -
1.538 -lemma bot_set_eq: "bot = {}"
1.539 -  by (iprover intro!: subset_antisym empty_subsetI bot_least)
1.540 -
1.541 -lemma Inter_eq:
1.542 -  "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
1.543 -  by (simp add: Inter_def INTER_def)
1.544 -
1.545 -lemma Union_eq:
1.546 -  "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
1.547 -  by (simp add: Union_def UNION_def)
1.548 -
1.549 -lemma Inf_set_eq:
1.550 -  "\<Sqinter>S = \<Inter>S"
1.551 -proof (rule set_ext)
1.552 -  fix x
1.553 -  have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
1.554 -    by auto
1.555 -  then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
1.556 -    by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
1.557 -qed
1.558 -
1.559 -lemma Sup_set_eq:
1.560 -  "\<Squnion>S = \<Union>S"
1.561 -proof (rule set_ext)
1.562 -  fix x
1.563 -  have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
1.564 -    by auto
1.565 -  then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
1.566 -    by (simp add: Union_eq Sup_fun_def Sup_bool_def) (simp add: mem_def)
1.567 -qed
1.568 -
1.569 -lemma INFI_set_eq:
1.570 -  "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
1.571 -  by (simp add: INFI_def Inf_set_eq)
1.572 -
1.573 -lemma SUPR_set_eq:
1.574 -  "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
1.575 -  by (simp add: SUPR_def Sup_set_eq)
1.576 -
1.577 -no_notation
1.578 -  less_eq  (infix "\<sqsubseteq>" 50) and
1.579 -  less (infix "\<sqsubset>" 50) and
1.580 -  inf  (infixl "\<sqinter>" 70) and
1.581 -  sup  (infixl "\<squnion>" 65) and
1.582 -  Inf  ("\<Sqinter>_" [900] 900) and
1.583 -  Sup  ("\<Squnion>_" [900] 900)
1.584 -
1.585 -
1.586 -subsubsection {* Unions of families *}
1.587 -
1.588  declare UNION_def [noatp]
1.589
1.590  lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
1.591 @@ -1208,6 +1204,36 @@
1.592
1.593  subsubsection {* Intersections of families *}
1.594
1.595 +definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
1.596 +  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
1.597 +
1.598 +syntax
1.599 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
1.600 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)
1.601 +
1.602 +syntax (xsymbols)
1.603 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
1.604 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
1.605 +
1.606 +syntax (latex output)
1.607 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
1.608 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
1.609 +
1.610 +translations
1.611 +  "INT x y. B"  == "INT x. INT y. B"
1.612 +  "INT x. B"    == "CONST INTER CONST UNIV (%x. B)"
1.613 +  "INT x. B"    == "INT x:CONST UNIV. B"
1.614 +  "INT x:A. B"  == "CONST INTER A (%x. B)"
1.615 +
1.616 +(* To avoid eta-contraction of body: *)
1.617 +print_translation {*
1.618 +let
1.619 +  fun btr' syn [A, Abs abs] =
1.620 +    let val (x, t) = atomic_abs_tr' abs
1.621 +    in Syntax.const syn \$ x \$ A \$ t end
1.622 +in [(@{const_syntax INTER}, btr' "@INTER")] end
1.623 +*}
1.624 +
1.625  lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
1.626    by (unfold INTER_def) blast
1.627
1.628 @@ -1228,6 +1254,34 @@
1.629
1.630  subsubsection {* Union *}
1.631
1.632 +definition Union :: "'a set set \<Rightarrow> 'a set" where
1.633 +  "Union S \<equiv> UNION S (\<lambda>x. x)"
1.634 +
1.635 +notation (xsymbols)
1.636 +  Union  ("\<Union>_" [90] 90)
1.637 +
1.638 +lemma Union_image_eq [simp]:
1.639 +  "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
1.640 +  by (auto simp add: Union_def UNION_def image_def)
1.641 +
1.642 +lemma Union_eq:
1.643 +  "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
1.644 +  by (simp add: Union_def UNION_def)
1.645 +
1.646 +lemma Sup_set_eq:
1.647 +  "\<Squnion>S = \<Union>S"
1.648 +proof (rule set_ext)
1.649 +  fix x
1.650 +  have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
1.651 +    by auto
1.652 +  then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
1.653 +    by (simp add: Union_eq Sup_fun_def Sup_bool_def) (simp add: mem_def)
1.654 +qed
1.655 +
1.656 +lemma SUPR_set_eq:
1.657 +  "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
1.658 +  by (simp add: SUPR_def Sup_set_eq)
1.659 +
1.660  lemma Union_iff [simp,noatp]: "(A : Union C) = (EX X:C. A:X)"
1.661    by (unfold Union_def) blast
1.662
1.663 @@ -1242,6 +1296,34 @@
1.664
1.665  subsubsection {* Inter *}
1.666
1.667 +definition Inter :: "'a set set \<Rightarrow> 'a set" where
1.668 +  "Inter S \<equiv> INTER S (\<lambda>x. x)"
1.669 +
1.670 +notation (xsymbols)
1.671 +  Inter  ("\<Inter>_" [90] 90)
1.672 +
1.673 +lemma Inter_image_eq [simp]:
1.674 +  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
1.675 +  by (auto simp add: Inter_def INTER_def image_def)
1.676 +
1.677 +lemma Inter_eq:
1.678 +  "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
1.679 +  by (simp add: Inter_def INTER_def)
1.680 +
1.681 +lemma Inf_set_eq:
1.682 +  "\<Sqinter>S = \<Inter>S"
1.683 +proof (rule set_ext)
1.684 +  fix x
1.685 +  have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
1.686 +    by auto
1.687 +  then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
1.688 +    by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
1.689 +qed
1.690 +
1.691 +lemma INFI_set_eq:
1.692 +  "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
1.693 +  by (simp add: INFI_def Inf_set_eq)
1.694 +
1.695  lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
1.696    by (unfold Inter_def) blast
1.697
1.698 @@ -1263,75 +1345,16 @@
1.699    by (unfold Inter_def) blast
1.700
1.701
1.702 -subsubsection {* Set reasoning tools *}
1.703 -
1.704 -text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
1.705 -
1.706 -lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
1.707 -by auto
1.708 -
1.709 -lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
1.710 -by auto
1.711 -
1.712 -text {*
1.713 -Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
1.714 -to the front (and similarly for @{text "t=x"}):
1.715 -*}
1.716 -
1.717 -ML{*
1.718 -  local
1.719 -    val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
1.720 -    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
1.721 -                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
1.722 -  in
1.723 -    val defColl_regroup = Simplifier.simproc @{theory}
1.724 -      "defined Collect" ["{x. P x & Q x}"]
1.725 -      (Quantifier1.rearrange_Coll Coll_perm_tac)
1.726 -  end;
1.727 -
1.728 -  Addsimprocs [defColl_regroup];
1.729 -*}
1.730 -
1.731 -text {*
1.732 -  Rewrite rules for boolean case-splitting: faster than @{text
1.733 -  "split_if [split]"}.
1.734 -*}
1.735 -
1.736 -lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"
1.737 -  by (rule split_if)
1.738 -
1.739 -lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"
1.740 -  by (rule split_if)
1.741 -
1.742 -text {*
1.743 -  Split ifs on either side of the membership relation.  Not for @{text
1.744 -  "[simp]"} -- can cause goals to blow up!
1.745 -*}
1.746 -
1.747 -lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"
1.748 -  by (rule split_if)
1.749 -
1.750 -lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"
1.751 -  by (rule split_if [where P="%S. a : S"])
1.752 -
1.753 -lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
1.754 -
1.755 -(*Would like to add these, but the existing code only searches for the
1.756 -  outer-level constant, which in this case is just "op :"; we instead need
1.757 -  to use term-nets to associate patterns with rules.  Also, if a rule fails to
1.758 -  apply, then the formula should be kept.
1.759 -  [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]),
1.760 -   ("Int", [IntD1,IntD2]),
1.761 -   ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
1.762 - *)
1.763 -
1.764 -ML {*
1.765 -  val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
1.766 -*}
1.767 -declaration {* fn _ =>
1.768 -  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
1.769 -*}
1.770 -
1.771 +no_notation
1.772 +  less_eq  (infix "\<sqsubseteq>" 50) and
1.773 +  less (infix "\<sqsubset>" 50) and
1.774 +  inf  (infixl "\<sqinter>" 70) and
1.775 +  sup  (infixl "\<squnion>" 65) and
1.776 +  Inf  ("\<Sqinter>_" [900] 900) and
1.777 +  Sup  ("\<Squnion>_" [900] 900)
1.778 +
1.779 +
1.780 +subsection {* Further operations and lemmas *}
1.781
1.782  subsubsection {* The ``proper subset'' relation *}
1.783
1.784 @@ -1378,9 +1401,6 @@
1.785  lemmas [symmetric, rulify] = atomize_ball
1.786    and [symmetric, defn] = atomize_ball
1.787
1.788 -
1.789 -subsection {* Further set-theory lemmas *}
1.790 -
1.791  subsubsection {* Derived rules involving subsets. *}
1.792
1.793  text {* @{text insert}. *}
1.794 @@ -2334,15 +2354,12 @@
1.795    by iprover
1.796
1.797
1.798 -subsection {* Inverse image of a function *}
1.799 +subsubsection {* Inverse image of a function *}
1.800
1.801  constdefs
1.802    vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
1.803    [code del]: "f -` B == {x. f x : B}"
1.804
1.805 -
1.806 -subsubsection {* Basic rules *}
1.807 -
1.808  lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
1.809    by (unfold vimage_def) blast
1.810
1.811 @@ -2361,9 +2378,6 @@
1.812  lemma vimageD: "a : f -` A ==> f a : A"
1.813    by (unfold vimage_def) fast
1.814
1.815 -
1.816 -subsubsection {* Equations *}
1.817 -
1.818  lemma vimage_empty [simp]: "f -` {} = {}"
1.819    by blast
1.820
1.821 @@ -2428,7 +2442,7 @@
1.822  by blast
1.823
1.824
1.825 -subsection {* Getting the Contents of a Singleton Set *}
1.826 +subsubsection {* Getting the Contents of a Singleton Set *}
1.827
1.828  definition contents :: "'a set \<Rightarrow> 'a" where
1.829    [code del]: "contents X = (THE x. X = {x})"
1.830 @@ -2437,19 +2451,7 @@
1.831    by (simp add: contents_def)
1.832
1.833
1.834 -subsection {* Transitivity rules for calculational reasoning *}
1.835 -
1.836 -lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B"
1.837 -  by (rule subsetD)
1.838 -
1.839 -lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
1.840 -  by (rule subsetD)
1.841 -
1.842 -lemmas basic_trans_rules [trans] =
1.843 -  order_trans_rules set_rev_mp set_mp
1.844 -
1.845 -
1.846 -subsection {* Least value operator *}
1.847 +subsubsection {* Least value operator *}
1.848
1.849  lemma Least_mono:
1.850    "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
1.851 @@ -2461,8 +2463,9 @@
1.852    apply (auto elim: monoD intro!: order_antisym)
1.853    done
1.854
1.855 -
1.856 -subsection {* Rudimentary code generation *}
1.857 +subsection {* Misc *}
1.858 +
1.859 +text {* Rudimentary code generation *}
1.860
1.861  lemma empty_code [code]: "{} x \<longleftrightarrow> False"
1.862    unfolding empty_def Collect_def ..
1.863 @@ -2482,8 +2485,7 @@
1.864  lemma vimage_code [code]: "(f -` A) x = A (f x)"
1.865    unfolding vimage_def Collect_def mem_def ..
1.866
1.867 -
1.868 -subsection {* Misc theorem and ML bindings *}
1.869 +text {* Misc theorem and ML bindings *}
1.870
1.871  lemmas equalityI = subset_antisym
1.872  lemmas mem_simps =
```