refined outline structure
authorhaftmann
Mon Jul 20 11:47:17 2009 +0200 (2009-07-20)
changeset 320811b7a901e2edc
parent 32078 1c14f77201d4
child 32082 90d03908b3d7
refined outline structure
src/HOL/Set.thy
     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 =