set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
authorhaftmann
Wed Jul 22 14:20:32 2009 +0200 (2009-07-22)
changeset 32135f645b51e8e54
parent 32134 ee143615019c
child 32136 672dfd59ff03
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
src/HOL/Set.thy
src/HOL/Tools/Function/fundef_lib.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/res_clause.ML
src/HOL/ex/Meson_Test.thy
     1.1 --- a/src/HOL/Set.thy	Wed Jul 22 14:20:32 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Wed Jul 22 14:20:32 2009 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4  text {* Set enumerations *}
     1.5  
     1.6  definition empty :: "'a set" ("{}") where
     1.7 -  "empty = {x. False}"
     1.8 +  bot_set_eq [symmetric]: "{} = bot"
     1.9  
    1.10  definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.11    insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
    1.12 @@ -544,7 +544,11 @@
    1.13  subsubsection {* The universal set -- UNIV *}
    1.14  
    1.15  definition UNIV :: "'a set" where
    1.16 +  top_set_eq [symmetric]: "UNIV = top"
    1.17 +
    1.18 +lemma UNIV_def:
    1.19    "UNIV = {x. True}"
    1.20 +  by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq Collect_def)
    1.21  
    1.22  lemma UNIV_I [simp]: "x : UNIV"
    1.23    by (simp add: UNIV_def)
    1.24 @@ -557,9 +561,6 @@
    1.25  lemma subset_UNIV [simp]: "A \<subseteq> UNIV"
    1.26    by (rule subsetI) (rule UNIV_I)
    1.27  
    1.28 -lemma top_set_eq: "top = UNIV"
    1.29 -  by (iprover intro!: subset_antisym subset_UNIV top_greatest)
    1.30 -
    1.31  text {*
    1.32    \medskip Eta-contracting these two rules (to remove @{text P})
    1.33    causes them to be ignored because of their interaction with
    1.34 @@ -578,6 +579,10 @@
    1.35  
    1.36  subsubsection {* The empty set *}
    1.37  
    1.38 +lemma empty_def:
    1.39 +  "{} = {x. False}"
    1.40 +  by (simp add: bot_set_eq [symmetric] bot_fun_eq bot_bool_eq Collect_def)
    1.41 +
    1.42  lemma empty_iff [simp]: "(c : {}) = False"
    1.43    by (simp add: empty_def)
    1.44  
    1.45 @@ -588,9 +593,6 @@
    1.46      -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
    1.47    by blast
    1.48  
    1.49 -lemma bot_set_eq: "bot = {}"
    1.50 -  by (iprover intro!: subset_antisym empty_subsetI bot_least)
    1.51 -
    1.52  lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
    1.53    by blast
    1.54  
    1.55 @@ -652,17 +654,18 @@
    1.56  
    1.57  subsubsection {* Binary union -- Un *}
    1.58  
    1.59 -definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
    1.60 -  "A Un B = {x. x \<in> A \<or> x \<in> B}"
    1.61 +definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
    1.62 +  sup_set_eq [symmetric]: "A Un B = sup A B"
    1.63  
    1.64  notation (xsymbols)
    1.65 -  "Un"  (infixl "\<union>" 65)
    1.66 +  union  (infixl "\<union>" 65)
    1.67  
    1.68  notation (HTML output)
    1.69 -  "Un"  (infixl "\<union>" 65)
    1.70 -
    1.71 -lemma sup_set_eq: "sup A B = A \<union> B"
    1.72 -  by (simp add: sup_fun_eq sup_bool_eq Un_def Collect_def mem_def)
    1.73 +  union  (infixl "\<union>" 65)
    1.74 +
    1.75 +lemma Un_def:
    1.76 +  "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
    1.77 +  by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
    1.78  
    1.79  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
    1.80    by (unfold Un_def) blast
    1.81 @@ -695,17 +698,18 @@
    1.82  
    1.83  subsubsection {* Binary intersection -- Int *}
    1.84  
    1.85 -definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    1.86 -  "A Int B = {x. x \<in> A \<and> x \<in> B}"
    1.87 +definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    1.88 +  inf_set_eq [symmetric]: "A Int B = inf A B"
    1.89  
    1.90  notation (xsymbols)
    1.91 -  "Int"  (infixl "\<inter>" 70)
    1.92 +  inter  (infixl "\<inter>" 70)
    1.93  
    1.94  notation (HTML output)
    1.95 -  "Int"  (infixl "\<inter>" 70)
    1.96 -
    1.97 -lemma inf_set_eq: "inf A B = A \<inter> B"
    1.98 -  by (simp add: inf_fun_eq inf_bool_eq Int_def Collect_def mem_def)
    1.99 +  inter  (infixl "\<inter>" 70)
   1.100 +
   1.101 +lemma Int_def:
   1.102 +  "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
   1.103 +  by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
   1.104  
   1.105  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   1.106    by (unfold Int_def) blast
   1.107 @@ -933,6 +937,803 @@
   1.108   *)
   1.109  
   1.110  
   1.111 +subsection {* Further operations and lemmas *}
   1.112 +
   1.113 +subsubsection {* The ``proper subset'' relation *}
   1.114 +
   1.115 +lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
   1.116 +  by (unfold less_le) blast
   1.117 +
   1.118 +lemma psubsetE [elim!,noatp]: 
   1.119 +    "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
   1.120 +  by (unfold less_le) blast
   1.121 +
   1.122 +lemma psubset_insert_iff:
   1.123 +  "(A \<subset> insert x B) = (if x \<in> B then A \<subset> B else if x \<in> A then A - {x} \<subset> B else A \<subseteq> B)"
   1.124 +  by (auto simp add: less_le subset_insert_iff)
   1.125 +
   1.126 +lemma psubset_eq: "(A \<subset> B) = (A \<subseteq> B & A \<noteq> B)"
   1.127 +  by (simp only: less_le)
   1.128 +
   1.129 +lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
   1.130 +  by (simp add: psubset_eq)
   1.131 +
   1.132 +lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C"
   1.133 +apply (unfold less_le)
   1.134 +apply (auto dest: subset_antisym)
   1.135 +done
   1.136 +
   1.137 +lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B"
   1.138 +apply (unfold less_le)
   1.139 +apply (auto dest: subsetD)
   1.140 +done
   1.141 +
   1.142 +lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
   1.143 +  by (auto simp add: psubset_eq)
   1.144 +
   1.145 +lemma subset_psubset_trans: "A \<subseteq> B ==> B \<subset> C ==> A \<subset> C"
   1.146 +  by (auto simp add: psubset_eq)
   1.147 +
   1.148 +lemma psubset_imp_ex_mem: "A \<subset> B ==> \<exists>b. b \<in> (B - A)"
   1.149 +  by (unfold less_le) blast
   1.150 +
   1.151 +lemma atomize_ball:
   1.152 +    "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"
   1.153 +  by (simp only: Ball_def atomize_all atomize_imp)
   1.154 +
   1.155 +lemmas [symmetric, rulify] = atomize_ball
   1.156 +  and [symmetric, defn] = atomize_ball
   1.157 +
   1.158 +subsubsection {* Derived rules involving subsets. *}
   1.159 +
   1.160 +text {* @{text insert}. *}
   1.161 +
   1.162 +lemma subset_insertI: "B \<subseteq> insert a B"
   1.163 +  by (rule subsetI) (erule insertI2)
   1.164 +
   1.165 +lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B"
   1.166 +  by blast
   1.167 +
   1.168 +lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
   1.169 +  by blast
   1.170 +
   1.171 +
   1.172 +text {* \medskip Finite Union -- the least upper bound of two sets. *}
   1.173 +
   1.174 +lemma Un_upper1: "A \<subseteq> A \<union> B"
   1.175 +  by blast
   1.176 +
   1.177 +lemma Un_upper2: "B \<subseteq> A \<union> B"
   1.178 +  by blast
   1.179 +
   1.180 +lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"
   1.181 +  by blast
   1.182 +
   1.183 +
   1.184 +text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}
   1.185 +
   1.186 +lemma Int_lower1: "A \<inter> B \<subseteq> A"
   1.187 +  by blast
   1.188 +
   1.189 +lemma Int_lower2: "A \<inter> B \<subseteq> B"
   1.190 +  by blast
   1.191 +
   1.192 +lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"
   1.193 +  by blast
   1.194 +
   1.195 +
   1.196 +text {* \medskip Set difference. *}
   1.197 +
   1.198 +lemma Diff_subset: "A - B \<subseteq> A"
   1.199 +  by blast
   1.200 +
   1.201 +lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)"
   1.202 +by blast
   1.203 +
   1.204 +
   1.205 +subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
   1.206 +
   1.207 +text {* @{text "{}"}. *}
   1.208 +
   1.209 +lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
   1.210 +  -- {* supersedes @{text "Collect_False_empty"} *}
   1.211 +  by auto
   1.212 +
   1.213 +lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
   1.214 +  by blast
   1.215 +
   1.216 +lemma not_psubset_empty [iff]: "\<not> (A < {})"
   1.217 +  by (unfold less_le) blast
   1.218 +
   1.219 +lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"
   1.220 +by blast
   1.221 +
   1.222 +lemma empty_Collect_eq [simp]: "({} = Collect P) = (\<forall>x. \<not> P x)"
   1.223 +by blast
   1.224 +
   1.225 +lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}"
   1.226 +  by blast
   1.227 +
   1.228 +lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \<union> {x. Q x}"
   1.229 +  by blast
   1.230 +
   1.231 +lemma Collect_imp_eq: "{x. P x --> Q x} = -{x. P x} \<union> {x. Q x}"
   1.232 +  by blast
   1.233 +
   1.234 +lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
   1.235 +  by blast
   1.236 +
   1.237 +
   1.238 +text {* \medskip @{text insert}. *}
   1.239 +
   1.240 +lemma insert_is_Un: "insert a A = {a} Un A"
   1.241 +  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *}
   1.242 +  by blast
   1.243 +
   1.244 +lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
   1.245 +  by blast
   1.246 +
   1.247 +lemmas empty_not_insert = insert_not_empty [symmetric, standard]
   1.248 +declare empty_not_insert [simp]
   1.249 +
   1.250 +lemma insert_absorb: "a \<in> A ==> insert a A = A"
   1.251 +  -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}
   1.252 +  -- {* with \emph{quadratic} running time *}
   1.253 +  by blast
   1.254 +
   1.255 +lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
   1.256 +  by blast
   1.257 +
   1.258 +lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"
   1.259 +  by blast
   1.260 +
   1.261 +lemma insert_subset [simp]: "(insert x A \<subseteq> B) = (x \<in> B & A \<subseteq> B)"
   1.262 +  by blast
   1.263 +
   1.264 +lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
   1.265 +  -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}
   1.266 +  apply (rule_tac x = "A - {a}" in exI, blast)
   1.267 +  done
   1.268 +
   1.269 +lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}"
   1.270 +  by auto
   1.271 +
   1.272 +lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
   1.273 +  by blast
   1.274 +
   1.275 +lemma insert_disjoint [simp,noatp]:
   1.276 + "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
   1.277 + "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
   1.278 +  by auto
   1.279 +
   1.280 +lemma disjoint_insert [simp,noatp]:
   1.281 + "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
   1.282 + "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
   1.283 +  by auto
   1.284 +
   1.285 +text {* \medskip @{text image}. *}
   1.286 +
   1.287 +lemma image_empty [simp]: "f`{} = {}"
   1.288 +  by blast
   1.289 +
   1.290 +lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)"
   1.291 +  by blast
   1.292 +
   1.293 +lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
   1.294 +  by auto
   1.295 +
   1.296 +lemma image_constant_conv: "(%x. c) ` A = (if A = {} then {} else {c})"
   1.297 +by auto
   1.298 +
   1.299 +lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
   1.300 +by blast
   1.301 +
   1.302 +lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
   1.303 +by blast
   1.304 +
   1.305 +lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
   1.306 +by blast
   1.307 +
   1.308 +lemma empty_is_image[iff]: "({} = f ` A) = (A = {})"
   1.309 +by blast
   1.310 +
   1.311 +
   1.312 +lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
   1.313 +  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
   1.314 +      with its implicit quantifier and conjunction.  Also image enjoys better
   1.315 +      equational properties than does the RHS. *}
   1.316 +  by blast
   1.317 +
   1.318 +lemma if_image_distrib [simp]:
   1.319 +  "(\<lambda>x. if P x then f x else g x) ` S
   1.320 +    = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
   1.321 +  by (auto simp add: image_def)
   1.322 +
   1.323 +lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
   1.324 +  by (simp add: image_def)
   1.325 +
   1.326 +
   1.327 +text {* \medskip @{text range}. *}
   1.328 +
   1.329 +lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
   1.330 +  by auto
   1.331 +
   1.332 +lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
   1.333 +by (subst image_image, simp)
   1.334 +
   1.335 +
   1.336 +text {* \medskip @{text Int} *}
   1.337 +
   1.338 +lemma Int_absorb [simp]: "A \<inter> A = A"
   1.339 +  by blast
   1.340 +
   1.341 +lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
   1.342 +  by blast
   1.343 +
   1.344 +lemma Int_commute: "A \<inter> B = B \<inter> A"
   1.345 +  by blast
   1.346 +
   1.347 +lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
   1.348 +  by blast
   1.349 +
   1.350 +lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)"
   1.351 +  by blast
   1.352 +
   1.353 +lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
   1.354 +  -- {* Intersection is an AC-operator *}
   1.355 +
   1.356 +lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
   1.357 +  by blast
   1.358 +
   1.359 +lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
   1.360 +  by blast
   1.361 +
   1.362 +lemma Int_empty_left [simp]: "{} \<inter> B = {}"
   1.363 +  by blast
   1.364 +
   1.365 +lemma Int_empty_right [simp]: "A \<inter> {} = {}"
   1.366 +  by blast
   1.367 +
   1.368 +lemma disjoint_eq_subset_Compl: "(A \<inter> B = {}) = (A \<subseteq> -B)"
   1.369 +  by blast
   1.370 +
   1.371 +lemma disjoint_iff_not_equal: "(A \<inter> B = {}) = (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
   1.372 +  by blast
   1.373 +
   1.374 +lemma Int_UNIV_left [simp]: "UNIV \<inter> B = B"
   1.375 +  by blast
   1.376 +
   1.377 +lemma Int_UNIV_right [simp]: "A \<inter> UNIV = A"
   1.378 +  by blast
   1.379 +
   1.380 +lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
   1.381 +  by blast
   1.382 +
   1.383 +lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
   1.384 +  by blast
   1.385 +
   1.386 +lemma Int_UNIV [simp,noatp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
   1.387 +  by blast
   1.388 +
   1.389 +lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
   1.390 +  by blast
   1.391 +
   1.392 +lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
   1.393 +  by blast
   1.394 +
   1.395 +
   1.396 +text {* \medskip @{text Un}. *}
   1.397 +
   1.398 +lemma Un_absorb [simp]: "A \<union> A = A"
   1.399 +  by blast
   1.400 +
   1.401 +lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
   1.402 +  by blast
   1.403 +
   1.404 +lemma Un_commute: "A \<union> B = B \<union> A"
   1.405 +  by blast
   1.406 +
   1.407 +lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
   1.408 +  by blast
   1.409 +
   1.410 +lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)"
   1.411 +  by blast
   1.412 +
   1.413 +lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
   1.414 +  -- {* Union is an AC-operator *}
   1.415 +
   1.416 +lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
   1.417 +  by blast
   1.418 +
   1.419 +lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
   1.420 +  by blast
   1.421 +
   1.422 +lemma Un_empty_left [simp]: "{} \<union> B = B"
   1.423 +  by blast
   1.424 +
   1.425 +lemma Un_empty_right [simp]: "A \<union> {} = A"
   1.426 +  by blast
   1.427 +
   1.428 +lemma Un_UNIV_left [simp]: "UNIV \<union> B = UNIV"
   1.429 +  by blast
   1.430 +
   1.431 +lemma Un_UNIV_right [simp]: "A \<union> UNIV = UNIV"
   1.432 +  by blast
   1.433 +
   1.434 +lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"
   1.435 +  by blast
   1.436 +
   1.437 +lemma Un_insert_right [simp]: "A \<union> (insert a B) = insert a (A \<union> B)"
   1.438 +  by blast
   1.439 +
   1.440 +lemma Int_insert_left:
   1.441 +    "(insert a B) Int C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"
   1.442 +  by auto
   1.443 +
   1.444 +lemma Int_insert_right:
   1.445 +    "A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"
   1.446 +  by auto
   1.447 +
   1.448 +lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
   1.449 +  by blast
   1.450 +
   1.451 +lemma Un_Int_distrib2: "(B \<inter> C) \<union> A = (B \<union> A) \<inter> (C \<union> A)"
   1.452 +  by blast
   1.453 +
   1.454 +lemma Un_Int_crazy:
   1.455 +    "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
   1.456 +  by blast
   1.457 +
   1.458 +lemma subset_Un_eq: "(A \<subseteq> B) = (A \<union> B = B)"
   1.459 +  by blast
   1.460 +
   1.461 +lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
   1.462 +  by blast
   1.463 +
   1.464 +lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
   1.465 +  by blast
   1.466 +
   1.467 +lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
   1.468 +  by blast
   1.469 +
   1.470 +lemma Diff_Int2: "A \<inter> C - B \<inter> C = A \<inter> C - B"
   1.471 +  by blast
   1.472 +
   1.473 +
   1.474 +text {* \medskip Set complement *}
   1.475 +
   1.476 +lemma Compl_disjoint [simp]: "A \<inter> -A = {}"
   1.477 +  by blast
   1.478 +
   1.479 +lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"
   1.480 +  by blast
   1.481 +
   1.482 +lemma Compl_partition: "A \<union> -A = UNIV"
   1.483 +  by blast
   1.484 +
   1.485 +lemma Compl_partition2: "-A \<union> A = UNIV"
   1.486 +  by blast
   1.487 +
   1.488 +lemma double_complement [simp]: "- (-A) = (A::'a set)"
   1.489 +  by blast
   1.490 +
   1.491 +lemma Compl_Un [simp]: "-(A \<union> B) = (-A) \<inter> (-B)"
   1.492 +  by blast
   1.493 +
   1.494 +lemma Compl_Int [simp]: "-(A \<inter> B) = (-A) \<union> (-B)"
   1.495 +  by blast
   1.496 +
   1.497 +lemma subset_Compl_self_eq: "(A \<subseteq> -A) = (A = {})"
   1.498 +  by blast
   1.499 +
   1.500 +lemma Un_Int_assoc_eq: "((A \<inter> B) \<union> C = A \<inter> (B \<union> C)) = (C \<subseteq> A)"
   1.501 +  -- {* Halmos, Naive Set Theory, page 16. *}
   1.502 +  by blast
   1.503 +
   1.504 +lemma Compl_UNIV_eq [simp]: "-UNIV = {}"
   1.505 +  by blast
   1.506 +
   1.507 +lemma Compl_empty_eq [simp]: "-{} = UNIV"
   1.508 +  by blast
   1.509 +
   1.510 +lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
   1.511 +  by blast
   1.512 +
   1.513 +lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
   1.514 +  by blast
   1.515 +
   1.516 +text {* \medskip Bounded quantifiers.
   1.517 +
   1.518 +  The following are not added to the default simpset because
   1.519 +  (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}
   1.520 +
   1.521 +lemma ball_Un: "(\<forall>x \<in> A \<union> B. P x) = ((\<forall>x\<in>A. P x) & (\<forall>x\<in>B. P x))"
   1.522 +  by blast
   1.523 +
   1.524 +lemma bex_Un: "(\<exists>x \<in> A \<union> B. P x) = ((\<exists>x\<in>A. P x) | (\<exists>x\<in>B. P x))"
   1.525 +  by blast
   1.526 +
   1.527 +
   1.528 +text {* \medskip Set difference. *}
   1.529 +
   1.530 +lemma Diff_eq: "A - B = A \<inter> (-B)"
   1.531 +  by blast
   1.532 +
   1.533 +lemma Diff_eq_empty_iff [simp,noatp]: "(A - B = {}) = (A \<subseteq> B)"
   1.534 +  by blast
   1.535 +
   1.536 +lemma Diff_cancel [simp]: "A - A = {}"
   1.537 +  by blast
   1.538 +
   1.539 +lemma Diff_idemp [simp]: "(A - B) - B = A - (B::'a set)"
   1.540 +by blast
   1.541 +
   1.542 +lemma Diff_triv: "A \<inter> B = {} ==> A - B = A"
   1.543 +  by (blast elim: equalityE)
   1.544 +
   1.545 +lemma empty_Diff [simp]: "{} - A = {}"
   1.546 +  by blast
   1.547 +
   1.548 +lemma Diff_empty [simp]: "A - {} = A"
   1.549 +  by blast
   1.550 +
   1.551 +lemma Diff_UNIV [simp]: "A - UNIV = {}"
   1.552 +  by blast
   1.553 +
   1.554 +lemma Diff_insert0 [simp,noatp]: "x \<notin> A ==> A - insert x B = A - B"
   1.555 +  by blast
   1.556 +
   1.557 +lemma Diff_insert: "A - insert a B = A - B - {a}"
   1.558 +  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
   1.559 +  by blast
   1.560 +
   1.561 +lemma Diff_insert2: "A - insert a B = A - {a} - B"
   1.562 +  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
   1.563 +  by blast
   1.564 +
   1.565 +lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))"
   1.566 +  by auto
   1.567 +
   1.568 +lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B"
   1.569 +  by blast
   1.570 +
   1.571 +lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A"
   1.572 +by blast
   1.573 +
   1.574 +lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A"
   1.575 +  by blast
   1.576 +
   1.577 +lemma Diff_insert_absorb: "x \<notin> A ==> (insert x A) - {x} = A"
   1.578 +  by auto
   1.579 +
   1.580 +lemma Diff_disjoint [simp]: "A \<inter> (B - A) = {}"
   1.581 +  by blast
   1.582 +
   1.583 +lemma Diff_partition: "A \<subseteq> B ==> A \<union> (B - A) = B"
   1.584 +  by blast
   1.585 +
   1.586 +lemma double_diff: "A \<subseteq> B ==> B \<subseteq> C ==> B - (C - A) = A"
   1.587 +  by blast
   1.588 +
   1.589 +lemma Un_Diff_cancel [simp]: "A \<union> (B - A) = A \<union> B"
   1.590 +  by blast
   1.591 +
   1.592 +lemma Un_Diff_cancel2 [simp]: "(B - A) \<union> A = B \<union> A"
   1.593 +  by blast
   1.594 +
   1.595 +lemma Diff_Un: "A - (B \<union> C) = (A - B) \<inter> (A - C)"
   1.596 +  by blast
   1.597 +
   1.598 +lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"
   1.599 +  by blast
   1.600 +
   1.601 +lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
   1.602 +  by blast
   1.603 +
   1.604 +lemma Int_Diff: "(A \<inter> B) - C = A \<inter> (B - C)"
   1.605 +  by blast
   1.606 +
   1.607 +lemma Diff_Int_distrib: "C \<inter> (A - B) = (C \<inter> A) - (C \<inter> B)"
   1.608 +  by blast
   1.609 +
   1.610 +lemma Diff_Int_distrib2: "(A - B) \<inter> C = (A \<inter> C) - (B \<inter> C)"
   1.611 +  by blast
   1.612 +
   1.613 +lemma Diff_Compl [simp]: "A - (- B) = A \<inter> B"
   1.614 +  by auto
   1.615 +
   1.616 +lemma Compl_Diff_eq [simp]: "- (A - B) = -A \<union> B"
   1.617 +  by blast
   1.618 +
   1.619 +
   1.620 +text {* \medskip Quantification over type @{typ bool}. *}
   1.621 +
   1.622 +lemma bool_induct: "P True \<Longrightarrow> P False \<Longrightarrow> P x"
   1.623 +  by (cases x) auto
   1.624 +
   1.625 +lemma all_bool_eq: "(\<forall>b. P b) \<longleftrightarrow> P True \<and> P False"
   1.626 +  by (auto intro: bool_induct)
   1.627 +
   1.628 +lemma bool_contrapos: "P x \<Longrightarrow> \<not> P False \<Longrightarrow> P True"
   1.629 +  by (cases x) auto
   1.630 +
   1.631 +lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
   1.632 +  by (auto intro: bool_contrapos)
   1.633 +
   1.634 +text {* \medskip @{text Pow} *}
   1.635 +
   1.636 +lemma Pow_empty [simp]: "Pow {} = {{}}"
   1.637 +  by (auto simp add: Pow_def)
   1.638 +
   1.639 +lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
   1.640 +  by (blast intro: image_eqI [where ?x = "u - {a}", standard])
   1.641 +
   1.642 +lemma Pow_Compl: "Pow (- A) = {-B | B. A \<in> Pow B}"
   1.643 +  by (blast intro: exI [where ?x = "- u", standard])
   1.644 +
   1.645 +lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
   1.646 +  by blast
   1.647 +
   1.648 +lemma Un_Pow_subset: "Pow A \<union> Pow B \<subseteq> Pow (A \<union> B)"
   1.649 +  by blast
   1.650 +
   1.651 +lemma Pow_Int_eq [simp]: "Pow (A \<inter> B) = Pow A \<inter> Pow B"
   1.652 +  by blast
   1.653 +
   1.654 +
   1.655 +text {* \medskip Miscellany. *}
   1.656 +
   1.657 +lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
   1.658 +  by blast
   1.659 +
   1.660 +lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
   1.661 +  by blast
   1.662 +
   1.663 +lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
   1.664 +  by (unfold less_le) blast
   1.665 +
   1.666 +lemma all_not_in_conv [simp]: "(\<forall>x. x \<notin> A) = (A = {})"
   1.667 +  by blast
   1.668 +
   1.669 +lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
   1.670 +  by blast
   1.671 +
   1.672 +lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
   1.673 +  by iprover
   1.674 +
   1.675 +
   1.676 +subsubsection {* Monotonicity of various operations *}
   1.677 +
   1.678 +lemma image_mono: "A \<subseteq> B ==> f`A \<subseteq> f`B"
   1.679 +  by blast
   1.680 +
   1.681 +lemma Pow_mono: "A \<subseteq> B ==> Pow A \<subseteq> Pow B"
   1.682 +  by blast
   1.683 +
   1.684 +lemma insert_mono: "C \<subseteq> D ==> insert a C \<subseteq> insert a D"
   1.685 +  by blast
   1.686 +
   1.687 +lemma Un_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<union> B \<subseteq> C \<union> D"
   1.688 +  by blast
   1.689 +
   1.690 +lemma Int_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<inter> B \<subseteq> C \<inter> D"
   1.691 +  by blast
   1.692 +
   1.693 +lemma Diff_mono: "A \<subseteq> C ==> D \<subseteq> B ==> A - B \<subseteq> C - D"
   1.694 +  by blast
   1.695 +
   1.696 +lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"
   1.697 +  by blast
   1.698 +
   1.699 +text {* \medskip Monotonicity of implications. *}
   1.700 +
   1.701 +lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B"
   1.702 +  apply (rule impI)
   1.703 +  apply (erule subsetD, assumption)
   1.704 +  done
   1.705 +
   1.706 +lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
   1.707 +  by iprover
   1.708 +
   1.709 +lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"
   1.710 +  by iprover
   1.711 +
   1.712 +lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"
   1.713 +  by iprover
   1.714 +
   1.715 +lemma imp_refl: "P --> P" ..
   1.716 +
   1.717 +lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
   1.718 +  by iprover
   1.719 +
   1.720 +lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"
   1.721 +  by iprover
   1.722 +
   1.723 +lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \<subseteq> Collect Q"
   1.724 +  by blast
   1.725 +
   1.726 +lemma Int_Collect_mono:
   1.727 +    "A \<subseteq> B ==> (!!x. x \<in> A ==> P x --> Q x) ==> A \<inter> Collect P \<subseteq> B \<inter> Collect Q"
   1.728 +  by blast
   1.729 +
   1.730 +lemmas basic_monos =
   1.731 +  subset_refl imp_refl disj_mono conj_mono
   1.732 +  ex_mono Collect_mono in_mono
   1.733 +
   1.734 +lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
   1.735 +  by iprover
   1.736 +
   1.737 +lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
   1.738 +  by iprover
   1.739 +
   1.740 +
   1.741 +subsubsection {* Inverse image of a function *}
   1.742 +
   1.743 +constdefs
   1.744 +  vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
   1.745 +  [code del]: "f -` B == {x. f x : B}"
   1.746 +
   1.747 +lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
   1.748 +  by (unfold vimage_def) blast
   1.749 +
   1.750 +lemma vimage_singleton_eq: "(a : f -` {b}) = (f a = b)"
   1.751 +  by simp
   1.752 +
   1.753 +lemma vimageI [intro]: "f a = b ==> b:B ==> a : f -` B"
   1.754 +  by (unfold vimage_def) blast
   1.755 +
   1.756 +lemma vimageI2: "f a : A ==> a : f -` A"
   1.757 +  by (unfold vimage_def) fast
   1.758 +
   1.759 +lemma vimageE [elim!]: "a: f -` B ==> (!!x. f a = x ==> x:B ==> P) ==> P"
   1.760 +  by (unfold vimage_def) blast
   1.761 +
   1.762 +lemma vimageD: "a : f -` A ==> f a : A"
   1.763 +  by (unfold vimage_def) fast
   1.764 +
   1.765 +lemma vimage_empty [simp]: "f -` {} = {}"
   1.766 +  by blast
   1.767 +
   1.768 +lemma vimage_Compl: "f -` (-A) = -(f -` A)"
   1.769 +  by blast
   1.770 +
   1.771 +lemma vimage_Un [simp]: "f -` (A Un B) = (f -` A) Un (f -` B)"
   1.772 +  by blast
   1.773 +
   1.774 +lemma vimage_Int [simp]: "f -` (A Int B) = (f -` A) Int (f -` B)"
   1.775 +  by fast
   1.776 +
   1.777 +lemma vimage_Collect_eq [simp]: "f -` Collect P = {y. P (f y)}"
   1.778 +  by blast
   1.779 +
   1.780 +lemma vimage_Collect: "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q"
   1.781 +  by blast
   1.782 +
   1.783 +lemma vimage_insert: "f-`(insert a B) = (f-`{a}) Un (f-`B)"
   1.784 +  -- {* NOT suitable for rewriting because of the recurrence of @{term "{a}"}. *}
   1.785 +  by blast
   1.786 +
   1.787 +lemma vimage_Diff: "f -` (A - B) = (f -` A) - (f -` B)"
   1.788 +  by blast
   1.789 +
   1.790 +lemma vimage_UNIV [simp]: "f -` UNIV = UNIV"
   1.791 +  by blast
   1.792 +
   1.793 +lemma vimage_mono: "A \<subseteq> B ==> f -` A \<subseteq> f -` B"
   1.794 +  -- {* monotonicity *}
   1.795 +  by blast
   1.796 +
   1.797 +lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
   1.798 +by (blast intro: sym)
   1.799 +
   1.800 +lemma image_vimage_subset: "f ` (f -` A) <= A"
   1.801 +by blast
   1.802 +
   1.803 +lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
   1.804 +by blast
   1.805 +
   1.806 +lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
   1.807 +by blast
   1.808 +
   1.809 +lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
   1.810 +by blast
   1.811 +
   1.812 +
   1.813 +subsubsection {* Getting the Contents of a Singleton Set *}
   1.814 +
   1.815 +definition contents :: "'a set \<Rightarrow> 'a" where
   1.816 +  [code del]: "contents X = (THE x. X = {x})"
   1.817 +
   1.818 +lemma contents_eq [simp]: "contents {x} = x"
   1.819 +  by (simp add: contents_def)
   1.820 +
   1.821 +
   1.822 +subsubsection {* Least value operator *}
   1.823 +
   1.824 +lemma Least_mono:
   1.825 +  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
   1.826 +    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
   1.827 +    -- {* Courtesy of Stephan Merz *}
   1.828 +  apply clarify
   1.829 +  apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
   1.830 +  apply (rule LeastI2_order)
   1.831 +  apply (auto elim: monoD intro!: order_antisym)
   1.832 +  done
   1.833 +
   1.834 +subsection {* Misc *}
   1.835 +
   1.836 +text {* Rudimentary code generation *}
   1.837 +
   1.838 +lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
   1.839 +  by (auto simp add: insert_compr Collect_def mem_def)
   1.840 +
   1.841 +lemma vimage_code [code]: "(f -` A) x = A (f x)"
   1.842 +  by (simp add: vimage_def Collect_def mem_def)
   1.843 +
   1.844 +
   1.845 +text {* Misc theorem and ML bindings *}
   1.846 +
   1.847 +lemmas equalityI = subset_antisym
   1.848 +
   1.849 +ML {*
   1.850 +val Ball_def = @{thm Ball_def}
   1.851 +val Bex_def = @{thm Bex_def}
   1.852 +val CollectD = @{thm CollectD}
   1.853 +val CollectE = @{thm CollectE}
   1.854 +val CollectI = @{thm CollectI}
   1.855 +val Collect_conj_eq = @{thm Collect_conj_eq}
   1.856 +val Collect_mem_eq = @{thm Collect_mem_eq}
   1.857 +val IntD1 = @{thm IntD1}
   1.858 +val IntD2 = @{thm IntD2}
   1.859 +val IntE = @{thm IntE}
   1.860 +val IntI = @{thm IntI}
   1.861 +val Int_Collect = @{thm Int_Collect}
   1.862 +val UNIV_I = @{thm UNIV_I}
   1.863 +val UNIV_witness = @{thm UNIV_witness}
   1.864 +val UnE = @{thm UnE}
   1.865 +val UnI1 = @{thm UnI1}
   1.866 +val UnI2 = @{thm UnI2}
   1.867 +val ballE = @{thm ballE}
   1.868 +val ballI = @{thm ballI}
   1.869 +val bexCI = @{thm bexCI}
   1.870 +val bexE = @{thm bexE}
   1.871 +val bexI = @{thm bexI}
   1.872 +val bex_triv = @{thm bex_triv}
   1.873 +val bspec = @{thm bspec}
   1.874 +val contra_subsetD = @{thm contra_subsetD}
   1.875 +val distinct_lemma = @{thm distinct_lemma}
   1.876 +val eq_to_mono = @{thm eq_to_mono}
   1.877 +val eq_to_mono2 = @{thm eq_to_mono2}
   1.878 +val equalityCE = @{thm equalityCE}
   1.879 +val equalityD1 = @{thm equalityD1}
   1.880 +val equalityD2 = @{thm equalityD2}
   1.881 +val equalityE = @{thm equalityE}
   1.882 +val equalityI = @{thm equalityI}
   1.883 +val imageE = @{thm imageE}
   1.884 +val imageI = @{thm imageI}
   1.885 +val image_Un = @{thm image_Un}
   1.886 +val image_insert = @{thm image_insert}
   1.887 +val insert_commute = @{thm insert_commute}
   1.888 +val insert_iff = @{thm insert_iff}
   1.889 +val mem_Collect_eq = @{thm mem_Collect_eq}
   1.890 +val rangeE = @{thm rangeE}
   1.891 +val rangeI = @{thm rangeI}
   1.892 +val range_eqI = @{thm range_eqI}
   1.893 +val subsetCE = @{thm subsetCE}
   1.894 +val subsetD = @{thm subsetD}
   1.895 +val subsetI = @{thm subsetI}
   1.896 +val subset_refl = @{thm subset_refl}
   1.897 +val subset_trans = @{thm subset_trans}
   1.898 +val vimageD = @{thm vimageD}
   1.899 +val vimageE = @{thm vimageE}
   1.900 +val vimageI = @{thm vimageI}
   1.901 +val vimageI2 = @{thm vimageI2}
   1.902 +val vimage_Collect = @{thm vimage_Collect}
   1.903 +val vimage_Int = @{thm vimage_Int}
   1.904 +val vimage_Un = @{thm vimage_Un}
   1.905 +*}
   1.906 +
   1.907 +
   1.908  subsection {* Complete lattices *}
   1.909  
   1.910  notation
   1.911 @@ -957,10 +1758,10 @@
   1.912    by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
   1.913  
   1.914  lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
   1.915 -  unfolding Sup_Inf by (auto simp add: UNIV_def)
   1.916 +  unfolding Sup_Inf by auto
   1.917  
   1.918  lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
   1.919 -  unfolding Inf_Sup by (auto simp add: UNIV_def)
   1.920 +  unfolding Inf_Sup by auto
   1.921  
   1.922  lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   1.923    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
   1.924 @@ -1120,29 +1921,29 @@
   1.925  
   1.926  lemma Inf_empty_fun:
   1.927    "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
   1.928 -  by rule (simp add: Inf_fun_def, simp add: empty_def)
   1.929 +  by (simp add: Inf_fun_def)
   1.930  
   1.931  lemma Sup_empty_fun:
   1.932    "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
   1.933 -  by rule (simp add: Sup_fun_def, simp add: empty_def)
   1.934 +  by (simp add: Sup_fun_def)
   1.935  
   1.936  
   1.937  subsubsection {* Union *}
   1.938  
   1.939  definition Union :: "'a set set \<Rightarrow> 'a set" where
   1.940 -  Union_eq [code del]: "Union A = {x. \<exists>B \<in> A. x \<in> B}"
   1.941 +  Sup_set_eq [symmetric]: "Union S = \<Squnion>S"
   1.942  
   1.943  notation (xsymbols)
   1.944    Union  ("\<Union>_" [90] 90)
   1.945  
   1.946 -lemma Sup_set_eq:
   1.947 -  "\<Squnion>S = \<Union>S"
   1.948 +lemma Union_eq:
   1.949 +  "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
   1.950  proof (rule set_ext)
   1.951    fix x
   1.952 -  have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
   1.953 +  have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
   1.954      by auto
   1.955 -  then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
   1.956 -    by (simp add: Sup_fun_def Sup_bool_def Union_eq) (simp add: mem_def)
   1.957 +  then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
   1.958 +    by (simp add: Sup_set_eq [symmetric] Sup_fun_def Sup_bool_def) (simp add: mem_def)
   1.959  qed
   1.960  
   1.961  lemma Union_iff [simp, noatp]:
   1.962 @@ -1159,11 +1960,53 @@
   1.963    "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A\<in>X \<Longrightarrow> X\<in>C \<Longrightarrow> R) \<Longrightarrow> R"
   1.964    by auto
   1.965  
   1.966 +lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"
   1.967 +  by (iprover intro: subsetI UnionI)
   1.968 +
   1.969 +lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
   1.970 +  by (iprover intro: subsetI elim: UnionE dest: subsetD)
   1.971 +
   1.972 +lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
   1.973 +  by blast
   1.974 +
   1.975 +lemma Union_empty [simp]: "Union({}) = {}"
   1.976 +  by blast
   1.977 +
   1.978 +lemma Union_UNIV [simp]: "Union UNIV = UNIV"
   1.979 +  by blast
   1.980 +
   1.981 +lemma Union_insert [simp]: "Union (insert a B) = a \<union> \<Union>B"
   1.982 +  by blast
   1.983 +
   1.984 +lemma Union_Un_distrib [simp]: "\<Union>(A Un B) = \<Union>A \<union> \<Union>B"
   1.985 +  by blast
   1.986 +
   1.987 +lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
   1.988 +  by blast
   1.989 +
   1.990 +lemma Union_empty_conv [simp,noatp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
   1.991 +  by blast
   1.992 +
   1.993 +lemma empty_Union_conv [simp,noatp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
   1.994 +  by blast
   1.995 +
   1.996 +lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
   1.997 +  by blast
   1.998 +
   1.999 +lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
  1.1000 +  by blast
  1.1001 +
  1.1002 +lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A"
  1.1003 +  by blast
  1.1004 +
  1.1005 +lemma Union_mono: "A \<subseteq> B ==> \<Union>A \<subseteq> \<Union>B"
  1.1006 +  by blast
  1.1007 +
  1.1008  
  1.1009  subsubsection {* Unions of families *}
  1.1010  
  1.1011  definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
  1.1012 -  UNION_eq_Union_image: "UNION A B = \<Union>(B`A)"
  1.1013 +  SUPR_set_eq [symmetric]: "UNION S f = (SUP x:S. f x)"
  1.1014  
  1.1015  syntax
  1.1016    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
  1.1017 @@ -1196,16 +2039,16 @@
  1.1018  Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} "@UNION"
  1.1019  ] *} -- {* to avoid eta-contraction of body *}
  1.1020  
  1.1021 -lemma SUPR_set_eq:
  1.1022 -  "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
  1.1023 -  by (simp add: SUPR_def UNION_eq_Union_image Sup_set_eq)
  1.1024 +lemma UNION_eq_Union_image:
  1.1025 +  "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
  1.1026 +  by (simp add: SUPR_def SUPR_set_eq [symmetric] Sup_set_eq)
  1.1027  
  1.1028  lemma Union_def:
  1.1029    "\<Union>S = (\<Union>x\<in>S. x)"
  1.1030    by (simp add: UNION_eq_Union_image image_def)
  1.1031  
  1.1032  lemma UNION_def [noatp]:
  1.1033 -  "UNION A B = {y. \<exists>x\<in>A. y \<in> B x}"
  1.1034 +  "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
  1.1035    by (auto simp add: UNION_eq_Union_image Union_eq)
  1.1036    
  1.1037  lemma Union_image_eq [simp]:
  1.1038 @@ -1234,23 +2077,109 @@
  1.1039  lemma image_eq_UN: "f`A = (UN x:A. {f x})"
  1.1040    by blast
  1.1041  
  1.1042 +lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
  1.1043 +  by blast
  1.1044 +
  1.1045 +lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
  1.1046 +  by (iprover intro: subsetI elim: UN_E dest: subsetD)
  1.1047 +
  1.1048 +lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
  1.1049 +  by blast
  1.1050 +
  1.1051 +lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
  1.1052 +  by blast
  1.1053 +
  1.1054 +lemma UN_empty [simp,noatp]: "(\<Union>x\<in>{}. B x) = {}"
  1.1055 +  by blast
  1.1056 +
  1.1057 +lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
  1.1058 +  by blast
  1.1059 +
  1.1060 +lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
  1.1061 +  by blast
  1.1062 +
  1.1063 +lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
  1.1064 +  by auto
  1.1065 +
  1.1066 +lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
  1.1067 +  by blast
  1.1068 +
  1.1069 +lemma UN_Un[simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
  1.1070 +  by blast
  1.1071 +
  1.1072 +lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)"
  1.1073 +  by blast
  1.1074 +
  1.1075 +lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
  1.1076 +  by blast
  1.1077 +
  1.1078 +lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
  1.1079 +  by blast
  1.1080 +
  1.1081 +lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
  1.1082 +  by auto
  1.1083 +
  1.1084 +lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
  1.1085 +  by blast
  1.1086 +
  1.1087 +lemma UNION_empty_conv[simp]:
  1.1088 +  "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
  1.1089 +  "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
  1.1090 +by blast+
  1.1091 +
  1.1092 +lemma Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
  1.1093 +  by blast
  1.1094 +
  1.1095 +lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
  1.1096 +  by blast
  1.1097 +
  1.1098 +lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) = (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
  1.1099 +  by blast
  1.1100 +
  1.1101 +lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
  1.1102 +  by (auto simp add: split_if_mem2)
  1.1103 +
  1.1104 +lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True \<union> A False)"
  1.1105 +  by (auto intro: bool_contrapos)
  1.1106 +
  1.1107 +lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)"
  1.1108 +  by blast
  1.1109 +
  1.1110 +lemma UN_mono:
  1.1111 +  "A \<subseteq> B ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
  1.1112 +    (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
  1.1113 +  by (blast dest: subsetD)
  1.1114 +
  1.1115 +lemma vimage_Union: "f -` (Union A) = (UN X:A. f -` X)"
  1.1116 +  by blast
  1.1117 +
  1.1118 +lemma vimage_UN: "f-`(UN x:A. B x) = (UN x:A. f -` B x)"
  1.1119 +  by blast
  1.1120 +
  1.1121 +lemma vimage_eq_UN: "f-`B = (UN y: B. f-`{y})"
  1.1122 +  -- {* NOT suitable for rewriting *}
  1.1123 +  by blast
  1.1124 +
  1.1125 +lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"
  1.1126 +by blast
  1.1127 +
  1.1128  
  1.1129  subsubsection {* Inter *}
  1.1130  
  1.1131  definition Inter :: "'a set set \<Rightarrow> 'a set" where
  1.1132 -  Inter_eq [code del]: "Inter A = {x. \<forall>B \<in> A. x \<in> B}"
  1.1133 -
  1.1134 +  Inf_set_eq [symmetric]: "Inter S = \<Sqinter>S"
  1.1135 +  
  1.1136  notation (xsymbols)
  1.1137    Inter  ("\<Inter>_" [90] 90)
  1.1138  
  1.1139 -lemma Inf_set_eq:
  1.1140 -  "\<Sqinter>S = \<Inter>S"
  1.1141 +lemma Inter_eq [code del]:
  1.1142 +  "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
  1.1143  proof (rule set_ext)
  1.1144    fix x
  1.1145 -  have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
  1.1146 +  have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
  1.1147      by auto
  1.1148 -  then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
  1.1149 -    by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
  1.1150 +  then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
  1.1151 +    by (simp add: Inf_fun_def Inf_bool_def Inf_set_eq [symmetric]) (simp add: mem_def)
  1.1152  qed
  1.1153  
  1.1154  lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
  1.1155 @@ -1273,11 +2202,47 @@
  1.1156      @{prop "X:C"}. *}
  1.1157    by (unfold Inter_eq) blast
  1.1158  
  1.1159 +lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
  1.1160 +  by blast
  1.1161 +
  1.1162 +lemma Inter_subset:
  1.1163 +  "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
  1.1164 +  by blast
  1.1165 +
  1.1166 +lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
  1.1167 +  by (iprover intro: InterI subsetI dest: subsetD)
  1.1168 +
  1.1169 +lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
  1.1170 +  by blast
  1.1171 +
  1.1172 +lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
  1.1173 +  by blast
  1.1174 +
  1.1175 +lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
  1.1176 +  by blast
  1.1177 +
  1.1178 +lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
  1.1179 +  by blast
  1.1180 +
  1.1181 +lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
  1.1182 +  by blast
  1.1183 +
  1.1184 +lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
  1.1185 +  by blast
  1.1186 +
  1.1187 +lemma Inter_UNIV_conv [simp,noatp]:
  1.1188 +  "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
  1.1189 +  "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
  1.1190 +  by blast+
  1.1191 +
  1.1192 +lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
  1.1193 +  by blast
  1.1194 +
  1.1195  
  1.1196  subsubsection {* Intersections of families *}
  1.1197  
  1.1198  definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
  1.1199 -  INTER_eq_Inter_image: "INTER A B = \<Inter>(B`A)"
  1.1200 +  INFI_set_eq [symmetric]: "INTER S f = (INF x:S. f x)"
  1.1201  
  1.1202  syntax
  1.1203    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
  1.1204 @@ -1301,16 +2266,16 @@
  1.1205  Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} "@INTER"
  1.1206  ] *} -- {* to avoid eta-contraction of body *}
  1.1207  
  1.1208 -lemma INFI_set_eq:
  1.1209 -  "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
  1.1210 -  by (simp add: INFI_def INTER_eq_Inter_image Inf_set_eq)
  1.1211 -
  1.1212 +lemma INTER_eq_Inter_image:
  1.1213 +  "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
  1.1214 +  by (simp add: INFI_def INFI_set_eq [symmetric] Inf_set_eq)
  1.1215 +  
  1.1216  lemma Inter_def:
  1.1217 -  "Inter S = INTER S (\<lambda>x. x)"
  1.1218 +  "\<Inter>S = (\<Inter>x\<in>S. x)"
  1.1219    by (simp add: INTER_eq_Inter_image image_def)
  1.1220  
  1.1221  lemma INTER_def:
  1.1222 -  "INTER A B = {y. \<forall>x\<in>A. y \<in> B x}"
  1.1223 +  "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
  1.1224    by (auto simp add: INTER_eq_Inter_image Inter_eq)
  1.1225  
  1.1226  lemma Inter_image_eq [simp]:
  1.1227 @@ -1334,571 +2299,24 @@
  1.1228      "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"
  1.1229    by (simp add: INTER_def)
  1.1230  
  1.1231 -
  1.1232 -no_notation
  1.1233 -  less_eq  (infix "\<sqsubseteq>" 50) and
  1.1234 -  less (infix "\<sqsubset>" 50) and
  1.1235 -  inf  (infixl "\<sqinter>" 70) and
  1.1236 -  sup  (infixl "\<squnion>" 65) and
  1.1237 -  Inf  ("\<Sqinter>_" [900] 900) and
  1.1238 -  Sup  ("\<Squnion>_" [900] 900)
  1.1239 -
  1.1240 -
  1.1241 -subsection {* Further operations and lemmas *}
  1.1242 -
  1.1243 -subsubsection {* The ``proper subset'' relation *}
  1.1244 -
  1.1245 -lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
  1.1246 -  by (unfold less_le) blast
  1.1247 -
  1.1248 -lemma psubsetE [elim!,noatp]: 
  1.1249 -    "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
  1.1250 -  by (unfold less_le) blast
  1.1251 -
  1.1252 -lemma psubset_insert_iff:
  1.1253 -  "(A \<subset> insert x B) = (if x \<in> B then A \<subset> B else if x \<in> A then A - {x} \<subset> B else A \<subseteq> B)"
  1.1254 -  by (auto simp add: less_le subset_insert_iff)
  1.1255 -
  1.1256 -lemma psubset_eq: "(A \<subset> B) = (A \<subseteq> B & A \<noteq> B)"
  1.1257 -  by (simp only: less_le)
  1.1258 -
  1.1259 -lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
  1.1260 -  by (simp add: psubset_eq)
  1.1261 -
  1.1262 -lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C"
  1.1263 -apply (unfold less_le)
  1.1264 -apply (auto dest: subset_antisym)
  1.1265 -done
  1.1266 -
  1.1267 -lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B"
  1.1268 -apply (unfold less_le)
  1.1269 -apply (auto dest: subsetD)
  1.1270 -done
  1.1271 -
  1.1272 -lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
  1.1273 -  by (auto simp add: psubset_eq)
  1.1274 -
  1.1275 -lemma subset_psubset_trans: "A \<subseteq> B ==> B \<subset> C ==> A \<subset> C"
  1.1276 -  by (auto simp add: psubset_eq)
  1.1277 -
  1.1278 -lemma psubset_imp_ex_mem: "A \<subset> B ==> \<exists>b. b \<in> (B - A)"
  1.1279 -  by (unfold less_le) blast
  1.1280 -
  1.1281 -lemma atomize_ball:
  1.1282 -    "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"
  1.1283 -  by (simp only: Ball_def atomize_all atomize_imp)
  1.1284 -
  1.1285 -lemmas [symmetric, rulify] = atomize_ball
  1.1286 -  and [symmetric, defn] = atomize_ball
  1.1287 -
  1.1288 -subsubsection {* Derived rules involving subsets. *}
  1.1289 -
  1.1290 -text {* @{text insert}. *}
  1.1291 -
  1.1292 -lemma subset_insertI: "B \<subseteq> insert a B"
  1.1293 -  by (rule subsetI) (erule insertI2)
  1.1294 -
  1.1295 -lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B"
  1.1296 +lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
  1.1297    by blast
  1.1298  
  1.1299 -lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
  1.1300 -  by blast
  1.1301 -
  1.1302 -
  1.1303 -text {* \medskip Big Union -- least upper bound of a set. *}
  1.1304 -
  1.1305 -lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"
  1.1306 -  by (iprover intro: subsetI UnionI)
  1.1307 -
  1.1308 -lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
  1.1309 -  by (iprover intro: subsetI elim: UnionE dest: subsetD)
  1.1310 -
  1.1311 -
  1.1312 -text {* \medskip General union. *}
  1.1313 -
  1.1314 -lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
  1.1315 +lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
  1.1316    by blast
  1.1317  
  1.1318 -lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
  1.1319 -  by (iprover intro: subsetI elim: UN_E dest: subsetD)
  1.1320 -
  1.1321 -
  1.1322 -text {* \medskip Big Intersection -- greatest lower bound of a set. *}
  1.1323 -
  1.1324 -lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
  1.1325 -  by blast
  1.1326 -
  1.1327 -lemma Inter_subset:
  1.1328 -  "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
  1.1329 -  by blast
  1.1330 -
  1.1331 -lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
  1.1332 -  by (iprover intro: InterI subsetI dest: subsetD)
  1.1333 -
  1.1334  lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
  1.1335    by blast
  1.1336  
  1.1337  lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
  1.1338    by (iprover intro: INT_I subsetI dest: subsetD)
  1.1339  
  1.1340 -
  1.1341 -text {* \medskip Finite Union -- the least upper bound of two sets. *}
  1.1342 -
  1.1343 -lemma Un_upper1: "A \<subseteq> A \<union> B"
  1.1344 -  by blast
  1.1345 -
  1.1346 -lemma Un_upper2: "B \<subseteq> A \<union> B"
  1.1347 -  by blast
  1.1348 -
  1.1349 -lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"
  1.1350 -  by blast
  1.1351 -
  1.1352 -
  1.1353 -text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}
  1.1354 -
  1.1355 -lemma Int_lower1: "A \<inter> B \<subseteq> A"
  1.1356 -  by blast
  1.1357 -
  1.1358 -lemma Int_lower2: "A \<inter> B \<subseteq> B"
  1.1359 -  by blast
  1.1360 -
  1.1361 -lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"
  1.1362 -  by blast
  1.1363 -
  1.1364 -
  1.1365 -text {* \medskip Set difference. *}
  1.1366 -
  1.1367 -lemma Diff_subset: "A - B \<subseteq> A"
  1.1368 -  by blast
  1.1369 -
  1.1370 -lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)"
  1.1371 -by blast
  1.1372 -
  1.1373 -
  1.1374 -subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
  1.1375 -
  1.1376 -text {* @{text "{}"}. *}
  1.1377 -
  1.1378 -lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
  1.1379 -  -- {* supersedes @{text "Collect_False_empty"} *}
  1.1380 -  by auto
  1.1381 -
  1.1382 -lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
  1.1383 -  by blast
  1.1384 -
  1.1385 -lemma not_psubset_empty [iff]: "\<not> (A < {})"
  1.1386 -  by (unfold less_le) blast
  1.1387 -
  1.1388 -lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"
  1.1389 -by blast
  1.1390 -
  1.1391 -lemma empty_Collect_eq [simp]: "({} = Collect P) = (\<forall>x. \<not> P x)"
  1.1392 -by blast
  1.1393 -
  1.1394 -lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}"
  1.1395 -  by blast
  1.1396 -
  1.1397 -lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \<union> {x. Q x}"
  1.1398 -  by blast
  1.1399 -
  1.1400 -lemma Collect_imp_eq: "{x. P x --> Q x} = -{x. P x} \<union> {x. Q x}"
  1.1401 -  by blast
  1.1402 -
  1.1403 -lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
  1.1404 -  by blast
  1.1405 -
  1.1406 -lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
  1.1407 -  by blast
  1.1408 -
  1.1409 -lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
  1.1410 -  by blast
  1.1411 -
  1.1412 -lemma Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
  1.1413 -  by blast
  1.1414 -
  1.1415 -lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
  1.1416 -  by blast
  1.1417 -
  1.1418 -
  1.1419 -text {* \medskip @{text insert}. *}
  1.1420 -
  1.1421 -lemma insert_is_Un: "insert a A = {a} Un A"
  1.1422 -  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *}
  1.1423 -  by blast
  1.1424 -
  1.1425 -lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
  1.1426 -  by blast
  1.1427 -
  1.1428 -lemmas empty_not_insert = insert_not_empty [symmetric, standard]
  1.1429 -declare empty_not_insert [simp]
  1.1430 -
  1.1431 -lemma insert_absorb: "a \<in> A ==> insert a A = A"
  1.1432 -  -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}
  1.1433 -  -- {* with \emph{quadratic} running time *}
  1.1434 -  by blast
  1.1435 -
  1.1436 -lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
  1.1437 -  by blast
  1.1438 -
  1.1439 -lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"
  1.1440 -  by blast
  1.1441 -
  1.1442 -lemma insert_subset [simp]: "(insert x A \<subseteq> B) = (x \<in> B & A \<subseteq> B)"
  1.1443 -  by blast
  1.1444 -
  1.1445 -lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
  1.1446 -  -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}
  1.1447 -  apply (rule_tac x = "A - {a}" in exI, blast)
  1.1448 -  done
  1.1449 -
  1.1450 -lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}"
  1.1451 -  by auto
  1.1452 -
  1.1453 -lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
  1.1454 -  by blast
  1.1455 -
  1.1456 -lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
  1.1457 -  by blast
  1.1458 -
  1.1459 -lemma insert_disjoint [simp,noatp]:
  1.1460 - "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
  1.1461 - "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
  1.1462 -  by auto
  1.1463 -
  1.1464 -lemma disjoint_insert [simp,noatp]:
  1.1465 - "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
  1.1466 - "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
  1.1467 -  by auto
  1.1468 -
  1.1469 -text {* \medskip @{text image}. *}
  1.1470 -
  1.1471 -lemma image_empty [simp]: "f`{} = {}"
  1.1472 -  by blast
  1.1473 -
  1.1474 -lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)"
  1.1475 -  by blast
  1.1476 -
  1.1477 -lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
  1.1478 -  by auto
  1.1479 -
  1.1480 -lemma image_constant_conv: "(%x. c) ` A = (if A = {} then {} else {c})"
  1.1481 -by auto
  1.1482 -
  1.1483 -lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
  1.1484 -by blast
  1.1485 -
  1.1486 -lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
  1.1487 -by blast
  1.1488 -
  1.1489 -lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
  1.1490 -by blast
  1.1491 -
  1.1492 -lemma empty_is_image[iff]: "({} = f ` A) = (A = {})"
  1.1493 -by blast
  1.1494 -
  1.1495 -
  1.1496 -lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
  1.1497 -  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
  1.1498 -      with its implicit quantifier and conjunction.  Also image enjoys better
  1.1499 -      equational properties than does the RHS. *}
  1.1500 -  by blast
  1.1501 -
  1.1502 -lemma if_image_distrib [simp]:
  1.1503 -  "(\<lambda>x. if P x then f x else g x) ` S
  1.1504 -    = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
  1.1505 -  by (auto simp add: image_def)
  1.1506 -
  1.1507 -lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
  1.1508 -  by (simp add: image_def)
  1.1509 -
  1.1510 -
  1.1511 -text {* \medskip @{text range}. *}
  1.1512 -
  1.1513 -lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
  1.1514 -  by auto
  1.1515 -
  1.1516 -lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
  1.1517 -by (subst image_image, simp)
  1.1518 -
  1.1519 -
  1.1520 -text {* \medskip @{text Int} *}
  1.1521 -
  1.1522 -lemma Int_absorb [simp]: "A \<inter> A = A"
  1.1523 -  by blast
  1.1524 -
  1.1525 -lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
  1.1526 -  by blast
  1.1527 -
  1.1528 -lemma Int_commute: "A \<inter> B = B \<inter> A"
  1.1529 -  by blast
  1.1530 -
  1.1531 -lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
  1.1532 -  by blast
  1.1533 -
  1.1534 -lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)"
  1.1535 -  by blast
  1.1536 -
  1.1537 -lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
  1.1538 -  -- {* Intersection is an AC-operator *}
  1.1539 -
  1.1540 -lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
  1.1541 -  by blast
  1.1542 -
  1.1543 -lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
  1.1544 -  by blast
  1.1545 -
  1.1546 -lemma Int_empty_left [simp]: "{} \<inter> B = {}"
  1.1547 -  by blast
  1.1548 -
  1.1549 -lemma Int_empty_right [simp]: "A \<inter> {} = {}"
  1.1550 -  by blast
  1.1551 -
  1.1552 -lemma disjoint_eq_subset_Compl: "(A \<inter> B = {}) = (A \<subseteq> -B)"
  1.1553 -  by blast
  1.1554 -
  1.1555 -lemma disjoint_iff_not_equal: "(A \<inter> B = {}) = (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
  1.1556 -  by blast
  1.1557 -
  1.1558 -lemma Int_UNIV_left [simp]: "UNIV \<inter> B = B"
  1.1559 -  by blast
  1.1560 -
  1.1561 -lemma Int_UNIV_right [simp]: "A \<inter> UNIV = A"
  1.1562 -  by blast
  1.1563 -
  1.1564 -lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
  1.1565 -  by blast
  1.1566 -
  1.1567 -lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
  1.1568 -  by blast
  1.1569 -
  1.1570 -lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
  1.1571 -  by blast
  1.1572 -
  1.1573 -lemma Int_UNIV [simp,noatp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
  1.1574 -  by blast
  1.1575 -
  1.1576 -lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
  1.1577 -  by blast
  1.1578 -
  1.1579 -lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
  1.1580 -  by blast
  1.1581 -
  1.1582 -
  1.1583 -text {* \medskip @{text Un}. *}
  1.1584 -
  1.1585 -lemma Un_absorb [simp]: "A \<union> A = A"
  1.1586 -  by blast
  1.1587 -
  1.1588 -lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
  1.1589 -  by blast
  1.1590 -
  1.1591 -lemma Un_commute: "A \<union> B = B \<union> A"
  1.1592 -  by blast
  1.1593 -
  1.1594 -lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
  1.1595 -  by blast
  1.1596 -
  1.1597 -lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)"
  1.1598 -  by blast
  1.1599 -
  1.1600 -lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
  1.1601 -  -- {* Union is an AC-operator *}
  1.1602 -
  1.1603 -lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
  1.1604 -  by blast
  1.1605 -
  1.1606 -lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
  1.1607 -  by blast
  1.1608 -
  1.1609 -lemma Un_empty_left [simp]: "{} \<union> B = B"
  1.1610 -  by blast
  1.1611 -
  1.1612 -lemma Un_empty_right [simp]: "A \<union> {} = A"
  1.1613 -  by blast
  1.1614 -
  1.1615 -lemma Un_UNIV_left [simp]: "UNIV \<union> B = UNIV"
  1.1616 -  by blast
  1.1617 -
  1.1618 -lemma Un_UNIV_right [simp]: "A \<union> UNIV = UNIV"
  1.1619 -  by blast
  1.1620 -
  1.1621 -lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
  1.1622 -  by blast
  1.1623 -
  1.1624 -lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"
  1.1625 -  by blast
  1.1626 -
  1.1627 -lemma Un_insert_right [simp]: "A \<union> (insert a B) = insert a (A \<union> B)"
  1.1628 -  by blast
  1.1629 -
  1.1630 -lemma Int_insert_left:
  1.1631 -    "(insert a B) Int C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"
  1.1632 -  by auto
  1.1633 -
  1.1634 -lemma Int_insert_right:
  1.1635 -    "A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"
  1.1636 -  by auto
  1.1637 -
  1.1638 -lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
  1.1639 -  by blast
  1.1640 -
  1.1641 -lemma Un_Int_distrib2: "(B \<inter> C) \<union> A = (B \<union> A) \<inter> (C \<union> A)"
  1.1642 -  by blast
  1.1643 -
  1.1644 -lemma Un_Int_crazy:
  1.1645 -    "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
  1.1646 -  by blast
  1.1647 -
  1.1648 -lemma subset_Un_eq: "(A \<subseteq> B) = (A \<union> B = B)"
  1.1649 -  by blast
  1.1650 -
  1.1651 -lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
  1.1652 -  by blast
  1.1653 -
  1.1654 -lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
  1.1655 -  by blast
  1.1656 -
  1.1657 -lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
  1.1658 -  by blast
  1.1659 -
  1.1660 -lemma Diff_Int2: "A \<inter> C - B \<inter> C = A \<inter> C - B"
  1.1661 -  by blast
  1.1662 -
  1.1663 -
  1.1664 -text {* \medskip Set complement *}
  1.1665 -
  1.1666 -lemma Compl_disjoint [simp]: "A \<inter> -A = {}"
  1.1667 -  by blast
  1.1668 -
  1.1669 -lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"
  1.1670 -  by blast
  1.1671 -
  1.1672 -lemma Compl_partition: "A \<union> -A = UNIV"
  1.1673 -  by blast
  1.1674 -
  1.1675 -lemma Compl_partition2: "-A \<union> A = UNIV"
  1.1676 -  by blast
  1.1677 -
  1.1678 -lemma double_complement [simp]: "- (-A) = (A::'a set)"
  1.1679 -  by blast
  1.1680 -
  1.1681 -lemma Compl_Un [simp]: "-(A \<union> B) = (-A) \<inter> (-B)"
  1.1682 -  by blast
  1.1683 -
  1.1684 -lemma Compl_Int [simp]: "-(A \<inter> B) = (-A) \<union> (-B)"
  1.1685 -  by blast
  1.1686 -
  1.1687 -lemma Compl_UN [simp]: "-(\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
  1.1688 -  by blast
  1.1689 -
  1.1690 -lemma Compl_INT [simp]: "-(\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
  1.1691 -  by blast
  1.1692 -
  1.1693 -lemma subset_Compl_self_eq: "(A \<subseteq> -A) = (A = {})"
  1.1694 -  by blast
  1.1695 -
  1.1696 -lemma Un_Int_assoc_eq: "((A \<inter> B) \<union> C = A \<inter> (B \<union> C)) = (C \<subseteq> A)"
  1.1697 -  -- {* Halmos, Naive Set Theory, page 16. *}
  1.1698 -  by blast
  1.1699 -
  1.1700 -lemma Compl_UNIV_eq [simp]: "-UNIV = {}"
  1.1701 -  by blast
  1.1702 -
  1.1703 -lemma Compl_empty_eq [simp]: "-{} = UNIV"
  1.1704 -  by blast
  1.1705 -
  1.1706 -lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
  1.1707 -  by blast
  1.1708 -
  1.1709 -lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
  1.1710 -  by blast
  1.1711 -
  1.1712 -
  1.1713 -text {* \medskip @{text Union}. *}
  1.1714 -
  1.1715 -lemma Union_empty [simp]: "Union({}) = {}"
  1.1716 -  by blast
  1.1717 -
  1.1718 -lemma Union_UNIV [simp]: "Union UNIV = UNIV"
  1.1719 -  by blast
  1.1720 -
  1.1721 -lemma Union_insert [simp]: "Union (insert a B) = a \<union> \<Union>B"
  1.1722 -  by blast
  1.1723 -
  1.1724 -lemma Union_Un_distrib [simp]: "\<Union>(A Un B) = \<Union>A \<union> \<Union>B"
  1.1725 -  by blast
  1.1726 -
  1.1727 -lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
  1.1728 -  by blast
  1.1729 -
  1.1730 -lemma Union_empty_conv [simp,noatp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
  1.1731 -  by blast
  1.1732 -
  1.1733 -lemma empty_Union_conv [simp,noatp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
  1.1734 -  by blast
  1.1735 -
  1.1736 -lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
  1.1737 -  by blast
  1.1738 -
  1.1739 -
  1.1740 -text {* \medskip @{text Inter}. *}
  1.1741 -
  1.1742 -lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
  1.1743 -  by blast
  1.1744 -
  1.1745 -lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
  1.1746 -  by blast
  1.1747 -
  1.1748 -lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
  1.1749 -  by blast
  1.1750 -
  1.1751 -lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
  1.1752 -  by blast
  1.1753 -
  1.1754 -lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
  1.1755 -  by blast
  1.1756 -
  1.1757 -lemma Inter_UNIV_conv [simp,noatp]:
  1.1758 -  "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
  1.1759 -  "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
  1.1760 -  by blast+
  1.1761 -
  1.1762 -
  1.1763 -text {*
  1.1764 -  \medskip @{text UN} and @{text INT}.
  1.1765 -
  1.1766 -  Basic identities: *}
  1.1767 -
  1.1768 -lemma UN_empty [simp,noatp]: "(\<Union>x\<in>{}. B x) = {}"
  1.1769 -  by blast
  1.1770 -
  1.1771 -lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
  1.1772 -  by blast
  1.1773 -
  1.1774 -lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
  1.1775 -  by blast
  1.1776 -
  1.1777 -lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
  1.1778 -  by auto
  1.1779 -
  1.1780  lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
  1.1781    by blast
  1.1782  
  1.1783  lemma INT_absorb: "k \<in> I ==> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
  1.1784    by blast
  1.1785  
  1.1786 -lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
  1.1787 -  by blast
  1.1788 -
  1.1789 -lemma UN_Un[simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
  1.1790 -  by blast
  1.1791 -
  1.1792 -lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)"
  1.1793 -  by blast
  1.1794 -
  1.1795 -lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
  1.1796 -  by blast
  1.1797 -
  1.1798  lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
  1.1799    by blast
  1.1800  
  1.1801 @@ -1912,34 +2330,35 @@
  1.1802      "u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
  1.1803    by blast
  1.1804  
  1.1805 -lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
  1.1806 -  by blast
  1.1807 -
  1.1808 -lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
  1.1809 -  by auto
  1.1810 -
  1.1811  lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
  1.1812    by auto
  1.1813  
  1.1814 -lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
  1.1815 -  by blast
  1.1816 -
  1.1817  lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
  1.1818    -- {* Look: it has an \emph{existential} quantifier *}
  1.1819    by blast
  1.1820  
  1.1821 -lemma UNION_empty_conv[simp]:
  1.1822 -  "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
  1.1823 -  "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
  1.1824 -by blast+
  1.1825 -
  1.1826  lemma INTER_UNIV_conv[simp]:
  1.1827   "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
  1.1828   "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
  1.1829  by blast+
  1.1830  
  1.1831 -
  1.1832 -text {* \medskip Distributive laws: *}
  1.1833 +lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"
  1.1834 +  by (auto intro: bool_induct)
  1.1835 +
  1.1836 +lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
  1.1837 +  by blast
  1.1838 +
  1.1839 +lemma INT_anti_mono:
  1.1840 +  "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
  1.1841 +    (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
  1.1842 +  -- {* The last inclusion is POSITIVE! *}
  1.1843 +  by (blast dest: subsetD)
  1.1844 +
  1.1845 +lemma vimage_INT: "f-`(INT x:A. B x) = (INT x:A. f -` B x)"
  1.1846 +  by blast
  1.1847 +
  1.1848 +
  1.1849 +subsubsection {* Distributive laws *}
  1.1850  
  1.1851  lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
  1.1852    by blast
  1.1853 @@ -1980,192 +2399,16 @@
  1.1854    by blast
  1.1855  
  1.1856  
  1.1857 -text {* \medskip Bounded quantifiers.
  1.1858 -
  1.1859 -  The following are not added to the default simpset because
  1.1860 -  (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}
  1.1861 -
  1.1862 -lemma ball_Un: "(\<forall>x \<in> A \<union> B. P x) = ((\<forall>x\<in>A. P x) & (\<forall>x\<in>B. P x))"
  1.1863 -  by blast
  1.1864 -
  1.1865 -lemma bex_Un: "(\<exists>x \<in> A \<union> B. P x) = ((\<exists>x\<in>A. P x) | (\<exists>x\<in>B. P x))"
  1.1866 -  by blast
  1.1867 -
  1.1868 -lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
  1.1869 -  by blast
  1.1870 -
  1.1871 -lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) = (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
  1.1872 -  by blast
  1.1873 -
  1.1874 -
  1.1875 -text {* \medskip Set difference. *}
  1.1876 -
  1.1877 -lemma Diff_eq: "A - B = A \<inter> (-B)"
  1.1878 -  by blast
  1.1879 -
  1.1880 -lemma Diff_eq_empty_iff [simp,noatp]: "(A - B = {}) = (A \<subseteq> B)"
  1.1881 -  by blast
  1.1882 -
  1.1883 -lemma Diff_cancel [simp]: "A - A = {}"
  1.1884 -  by blast
  1.1885 -
  1.1886 -lemma Diff_idemp [simp]: "(A - B) - B = A - (B::'a set)"
  1.1887 -by blast
  1.1888 -
  1.1889 -lemma Diff_triv: "A \<inter> B = {} ==> A - B = A"
  1.1890 -  by (blast elim: equalityE)
  1.1891 -
  1.1892 -lemma empty_Diff [simp]: "{} - A = {}"
  1.1893 -  by blast
  1.1894 -
  1.1895 -lemma Diff_empty [simp]: "A - {} = A"
  1.1896 -  by blast
  1.1897 -
  1.1898 -lemma Diff_UNIV [simp]: "A - UNIV = {}"
  1.1899 -  by blast
  1.1900 -
  1.1901 -lemma Diff_insert0 [simp,noatp]: "x \<notin> A ==> A - insert x B = A - B"
  1.1902 -  by blast
  1.1903 -
  1.1904 -lemma Diff_insert: "A - insert a B = A - B - {a}"
  1.1905 -  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
  1.1906 -  by blast
  1.1907 -
  1.1908 -lemma Diff_insert2: "A - insert a B = A - {a} - B"
  1.1909 -  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
  1.1910 -  by blast
  1.1911 -
  1.1912 -lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))"
  1.1913 -  by auto
  1.1914 -
  1.1915 -lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B"
  1.1916 -  by blast
  1.1917 -
  1.1918 -lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A"
  1.1919 -by blast
  1.1920 -
  1.1921 -lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A"
  1.1922 -  by blast
  1.1923 -
  1.1924 -lemma Diff_insert_absorb: "x \<notin> A ==> (insert x A) - {x} = A"
  1.1925 -  by auto
  1.1926 -
  1.1927 -lemma Diff_disjoint [simp]: "A \<inter> (B - A) = {}"
  1.1928 -  by blast
  1.1929 -
  1.1930 -lemma Diff_partition: "A \<subseteq> B ==> A \<union> (B - A) = B"
  1.1931 -  by blast
  1.1932 -
  1.1933 -lemma double_diff: "A \<subseteq> B ==> B \<subseteq> C ==> B - (C - A) = A"
  1.1934 -  by blast
  1.1935 -
  1.1936 -lemma Un_Diff_cancel [simp]: "A \<union> (B - A) = A \<union> B"
  1.1937 -  by blast
  1.1938 -
  1.1939 -lemma Un_Diff_cancel2 [simp]: "(B - A) \<union> A = B \<union> A"
  1.1940 -  by blast
  1.1941 -
  1.1942 -lemma Diff_Un: "A - (B \<union> C) = (A - B) \<inter> (A - C)"
  1.1943 -  by blast
  1.1944 -
  1.1945 -lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"
  1.1946 -  by blast
  1.1947 -
  1.1948 -lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
  1.1949 +subsubsection {* Complement *}
  1.1950 +
  1.1951 +lemma Compl_UN [simp]: "-(\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
  1.1952    by blast
  1.1953  
  1.1954 -lemma Int_Diff: "(A \<inter> B) - C = A \<inter> (B - C)"
  1.1955 -  by blast
  1.1956 -
  1.1957 -lemma Diff_Int_distrib: "C \<inter> (A - B) = (C \<inter> A) - (C \<inter> B)"
  1.1958 -  by blast
  1.1959 -
  1.1960 -lemma Diff_Int_distrib2: "(A - B) \<inter> C = (A \<inter> C) - (B \<inter> C)"
  1.1961 -  by blast
  1.1962 -
  1.1963 -lemma Diff_Compl [simp]: "A - (- B) = A \<inter> B"
  1.1964 -  by auto
  1.1965 -
  1.1966 -lemma Compl_Diff_eq [simp]: "- (A - B) = -A \<union> B"
  1.1967 +lemma Compl_INT [simp]: "-(\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
  1.1968    by blast
  1.1969  
  1.1970  
  1.1971 -text {* \medskip Quantification over type @{typ bool}. *}
  1.1972 -
  1.1973 -lemma bool_induct: "P True \<Longrightarrow> P False \<Longrightarrow> P x"
  1.1974 -  by (cases x) auto
  1.1975 -
  1.1976 -lemma all_bool_eq: "(\<forall>b. P b) \<longleftrightarrow> P True \<and> P False"
  1.1977 -  by (auto intro: bool_induct)
  1.1978 -
  1.1979 -lemma bool_contrapos: "P x \<Longrightarrow> \<not> P False \<Longrightarrow> P True"
  1.1980 -  by (cases x) auto
  1.1981 -
  1.1982 -lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
  1.1983 -  by (auto intro: bool_contrapos)
  1.1984 -
  1.1985 -lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
  1.1986 -  by (auto simp add: split_if_mem2)
  1.1987 -
  1.1988 -lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True \<union> A False)"
  1.1989 -  by (auto intro: bool_contrapos)
  1.1990 -
  1.1991 -lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"
  1.1992 -  by (auto intro: bool_induct)
  1.1993 -
  1.1994 -text {* \medskip @{text Pow} *}
  1.1995 -
  1.1996 -lemma Pow_empty [simp]: "Pow {} = {{}}"
  1.1997 -  by (auto simp add: Pow_def)
  1.1998 -
  1.1999 -lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
  1.2000 -  by (blast intro: image_eqI [where ?x = "u - {a}", standard])
  1.2001 -
  1.2002 -lemma Pow_Compl: "Pow (- A) = {-B | B. A \<in> Pow B}"
  1.2003 -  by (blast intro: exI [where ?x = "- u", standard])
  1.2004 -
  1.2005 -lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
  1.2006 -  by blast
  1.2007 -
  1.2008 -lemma Un_Pow_subset: "Pow A \<union> Pow B \<subseteq> Pow (A \<union> B)"
  1.2009 -  by blast
  1.2010 -
  1.2011 -lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)"
  1.2012 -  by blast
  1.2013 -
  1.2014 -lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
  1.2015 -  by blast
  1.2016 -
  1.2017 -lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A"
  1.2018 -  by blast
  1.2019 -
  1.2020 -lemma Pow_Int_eq [simp]: "Pow (A \<inter> B) = Pow A \<inter> Pow B"
  1.2021 -  by blast
  1.2022 -
  1.2023 -lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
  1.2024 -  by blast
  1.2025 -
  1.2026 -
  1.2027 -text {* \medskip Miscellany. *}
  1.2028 -
  1.2029 -lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
  1.2030 -  by blast
  1.2031 -
  1.2032 -lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
  1.2033 -  by blast
  1.2034 -
  1.2035 -lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
  1.2036 -  by (unfold less_le) blast
  1.2037 -
  1.2038 -lemma all_not_in_conv [simp]: "(\<forall>x. x \<notin> A) = (A = {})"
  1.2039 -  by blast
  1.2040 -
  1.2041 -lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
  1.2042 -  by blast
  1.2043 -
  1.2044 -lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
  1.2045 -  by iprover
  1.2046 -
  1.2047 +subsubsection {* Miniscoping and maxiscoping *}
  1.2048  
  1.2049  text {* \medskip Miniscoping: pushing in quantifiers and big Unions
  1.2050             and Intersections. *}
  1.2051 @@ -2262,284 +2505,17 @@
  1.2052    by auto
  1.2053  
  1.2054  
  1.2055 -subsubsection {* Monotonicity of various operations *}
  1.2056 -
  1.2057 -lemma image_mono: "A \<subseteq> B ==> f`A \<subseteq> f`B"
  1.2058 -  by blast
  1.2059 -
  1.2060 -lemma Pow_mono: "A \<subseteq> B ==> Pow A \<subseteq> Pow B"
  1.2061 -  by blast
  1.2062 -
  1.2063 -lemma Union_mono: "A \<subseteq> B ==> \<Union>A \<subseteq> \<Union>B"
  1.2064 -  by blast
  1.2065 -
  1.2066 -lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
  1.2067 -  by blast
  1.2068 -
  1.2069 -lemma UN_mono:
  1.2070 -  "A \<subseteq> B ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
  1.2071 -    (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
  1.2072 -  by (blast dest: subsetD)
  1.2073 -
  1.2074 -lemma INT_anti_mono:
  1.2075 -  "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
  1.2076 -    (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
  1.2077 -  -- {* The last inclusion is POSITIVE! *}
  1.2078 -  by (blast dest: subsetD)
  1.2079 -
  1.2080 -lemma insert_mono: "C \<subseteq> D ==> insert a C \<subseteq> insert a D"
  1.2081 -  by blast
  1.2082 -
  1.2083 -lemma Un_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<union> B \<subseteq> C \<union> D"
  1.2084 -  by blast
  1.2085 -
  1.2086 -lemma Int_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<inter> B \<subseteq> C \<inter> D"
  1.2087 -  by blast
  1.2088 -
  1.2089 -lemma Diff_mono: "A \<subseteq> C ==> D \<subseteq> B ==> A - B \<subseteq> C - D"
  1.2090 -  by blast
  1.2091 -
  1.2092 -lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"
  1.2093 -  by blast
  1.2094 -
  1.2095 -text {* \medskip Monotonicity of implications. *}
  1.2096 -
  1.2097 -lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B"
  1.2098 -  apply (rule impI)
  1.2099 -  apply (erule subsetD, assumption)
  1.2100 -  done
  1.2101 -
  1.2102 -lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
  1.2103 -  by iprover
  1.2104 -
  1.2105 -lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"
  1.2106 -  by iprover
  1.2107 -
  1.2108 -lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"
  1.2109 -  by iprover
  1.2110 -
  1.2111 -lemma imp_refl: "P --> P" ..
  1.2112 -
  1.2113 -lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
  1.2114 -  by iprover
  1.2115 -
  1.2116 -lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"
  1.2117 -  by iprover
  1.2118 -
  1.2119 -lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \<subseteq> Collect Q"
  1.2120 -  by blast
  1.2121 -
  1.2122 -lemma Int_Collect_mono:
  1.2123 -    "A \<subseteq> B ==> (!!x. x \<in> A ==> P x --> Q x) ==> A \<inter> Collect P \<subseteq> B \<inter> Collect Q"
  1.2124 -  by blast
  1.2125 -
  1.2126 -lemmas basic_monos =
  1.2127 -  subset_refl imp_refl disj_mono conj_mono
  1.2128 -  ex_mono Collect_mono in_mono
  1.2129 -
  1.2130 -lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
  1.2131 -  by iprover
  1.2132 -
  1.2133 -lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
  1.2134 -  by iprover
  1.2135 -
  1.2136 -
  1.2137 -subsubsection {* Inverse image of a function *}
  1.2138 -
  1.2139 -constdefs
  1.2140 -  vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
  1.2141 -  [code del]: "f -` B == {x. f x : B}"
  1.2142 -
  1.2143 -lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
  1.2144 -  by (unfold vimage_def) blast
  1.2145 -
  1.2146 -lemma vimage_singleton_eq: "(a : f -` {b}) = (f a = b)"
  1.2147 -  by simp
  1.2148 -
  1.2149 -lemma vimageI [intro]: "f a = b ==> b:B ==> a : f -` B"
  1.2150 -  by (unfold vimage_def) blast
  1.2151 -
  1.2152 -lemma vimageI2: "f a : A ==> a : f -` A"
  1.2153 -  by (unfold vimage_def) fast
  1.2154 -
  1.2155 -lemma vimageE [elim!]: "a: f -` B ==> (!!x. f a = x ==> x:B ==> P) ==> P"
  1.2156 -  by (unfold vimage_def) blast
  1.2157 -
  1.2158 -lemma vimageD: "a : f -` A ==> f a : A"
  1.2159 -  by (unfold vimage_def) fast
  1.2160 -
  1.2161 -lemma vimage_empty [simp]: "f -` {} = {}"
  1.2162 -  by blast
  1.2163 -
  1.2164 -lemma vimage_Compl: "f -` (-A) = -(f -` A)"
  1.2165 -  by blast
  1.2166 -
  1.2167 -lemma vimage_Un [simp]: "f -` (A Un B) = (f -` A) Un (f -` B)"
  1.2168 -  by blast
  1.2169 -
  1.2170 -lemma vimage_Int [simp]: "f -` (A Int B) = (f -` A) Int (f -` B)"
  1.2171 -  by fast
  1.2172 -
  1.2173 -lemma vimage_Union: "f -` (Union A) = (UN X:A. f -` X)"
  1.2174 -  by blast
  1.2175 -
  1.2176 -lemma vimage_UN: "f-`(UN x:A. B x) = (UN x:A. f -` B x)"
  1.2177 -  by blast
  1.2178 -
  1.2179 -lemma vimage_INT: "f-`(INT x:A. B x) = (INT x:A. f -` B x)"
  1.2180 -  by blast
  1.2181 -
  1.2182 -lemma vimage_Collect_eq [simp]: "f -` Collect P = {y. P (f y)}"
  1.2183 -  by blast
  1.2184 -
  1.2185 -lemma vimage_Collect: "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q"
  1.2186 -  by blast
  1.2187 -
  1.2188 -lemma vimage_insert: "f-`(insert a B) = (f-`{a}) Un (f-`B)"
  1.2189 -  -- {* NOT suitable for rewriting because of the recurrence of @{term "{a}"}. *}
  1.2190 -  by blast
  1.2191 -
  1.2192 -lemma vimage_Diff: "f -` (A - B) = (f -` A) - (f -` B)"
  1.2193 -  by blast
  1.2194 -
  1.2195 -lemma vimage_UNIV [simp]: "f -` UNIV = UNIV"
  1.2196 -  by blast
  1.2197 -
  1.2198 -lemma vimage_eq_UN: "f-`B = (UN y: B. f-`{y})"
  1.2199 -  -- {* NOT suitable for rewriting *}
  1.2200 -  by blast
  1.2201 -
  1.2202 -lemma vimage_mono: "A \<subseteq> B ==> f -` A \<subseteq> f -` B"
  1.2203 -  -- {* monotonicity *}
  1.2204 -  by blast
  1.2205 -
  1.2206 -lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
  1.2207 -by (blast intro: sym)
  1.2208 -
  1.2209 -lemma image_vimage_subset: "f ` (f -` A) <= A"
  1.2210 -by blast
  1.2211 -
  1.2212 -lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
  1.2213 -by blast
  1.2214 -
  1.2215 -lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
  1.2216 -by blast
  1.2217 -
  1.2218 -lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
  1.2219 -by blast
  1.2220 -
  1.2221 -lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"
  1.2222 -by blast
  1.2223 -
  1.2224 -
  1.2225 -subsubsection {* Getting the Contents of a Singleton Set *}
  1.2226 -
  1.2227 -definition contents :: "'a set \<Rightarrow> 'a" where
  1.2228 -  [code del]: "contents X = (THE x. X = {x})"
  1.2229 -
  1.2230 -lemma contents_eq [simp]: "contents {x} = x"
  1.2231 -  by (simp add: contents_def)
  1.2232 -
  1.2233 -
  1.2234 -subsubsection {* Least value operator *}
  1.2235 -
  1.2236 -lemma Least_mono:
  1.2237 -  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
  1.2238 -    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
  1.2239 -    -- {* Courtesy of Stephan Merz *}
  1.2240 -  apply clarify
  1.2241 -  apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
  1.2242 -  apply (rule LeastI2_order)
  1.2243 -  apply (auto elim: monoD intro!: order_antisym)
  1.2244 -  done
  1.2245 -
  1.2246 -subsection {* Misc *}
  1.2247 -
  1.2248 -text {* Rudimentary code generation *}
  1.2249 -
  1.2250 -lemma [code]: "{} = bot"
  1.2251 -  by (rule sym) (fact bot_set_eq)
  1.2252 -
  1.2253 -lemma [code]: "UNIV = top"
  1.2254 -  by (rule sym) (fact top_set_eq)
  1.2255 -
  1.2256 -lemma [code]: "op \<inter> = inf"
  1.2257 -  by (rule ext)+ (simp add: inf_set_eq)
  1.2258 -
  1.2259 -lemma [code]: "op \<union> = sup"
  1.2260 -  by (rule ext)+ (simp add: sup_set_eq)
  1.2261 -
  1.2262 -lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
  1.2263 -  by (auto simp add: insert_compr Collect_def mem_def)
  1.2264 -
  1.2265 -lemma vimage_code [code]: "(f -` A) x = A (f x)"
  1.2266 -  by (simp add: vimage_def Collect_def mem_def)
  1.2267 -
  1.2268 -
  1.2269 -text {* Misc theorem and ML bindings *}
  1.2270 -
  1.2271 -lemmas equalityI = subset_antisym
  1.2272 +no_notation
  1.2273 +  less_eq  (infix "\<sqsubseteq>" 50) and
  1.2274 +  less (infix "\<sqsubset>" 50) and
  1.2275 +  inf  (infixl "\<sqinter>" 70) and
  1.2276 +  sup  (infixl "\<squnion>" 65) and
  1.2277 +  Inf  ("\<Sqinter>_" [900] 900) and
  1.2278 +  Sup  ("\<Squnion>_" [900] 900)
  1.2279 +
  1.2280  lemmas mem_simps =
  1.2281    insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
  1.2282    mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
  1.2283    -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
  1.2284  
  1.2285 -ML {*
  1.2286 -val Ball_def = @{thm Ball_def}
  1.2287 -val Bex_def = @{thm Bex_def}
  1.2288 -val CollectD = @{thm CollectD}
  1.2289 -val CollectE = @{thm CollectE}
  1.2290 -val CollectI = @{thm CollectI}
  1.2291 -val Collect_conj_eq = @{thm Collect_conj_eq}
  1.2292 -val Collect_mem_eq = @{thm Collect_mem_eq}
  1.2293 -val IntD1 = @{thm IntD1}
  1.2294 -val IntD2 = @{thm IntD2}
  1.2295 -val IntE = @{thm IntE}
  1.2296 -val IntI = @{thm IntI}
  1.2297 -val Int_Collect = @{thm Int_Collect}
  1.2298 -val UNIV_I = @{thm UNIV_I}
  1.2299 -val UNIV_witness = @{thm UNIV_witness}
  1.2300 -val UnE = @{thm UnE}
  1.2301 -val UnI1 = @{thm UnI1}
  1.2302 -val UnI2 = @{thm UnI2}
  1.2303 -val ballE = @{thm ballE}
  1.2304 -val ballI = @{thm ballI}
  1.2305 -val bexCI = @{thm bexCI}
  1.2306 -val bexE = @{thm bexE}
  1.2307 -val bexI = @{thm bexI}
  1.2308 -val bex_triv = @{thm bex_triv}
  1.2309 -val bspec = @{thm bspec}
  1.2310 -val contra_subsetD = @{thm contra_subsetD}
  1.2311 -val distinct_lemma = @{thm distinct_lemma}
  1.2312 -val eq_to_mono = @{thm eq_to_mono}
  1.2313 -val eq_to_mono2 = @{thm eq_to_mono2}
  1.2314 -val equalityCE = @{thm equalityCE}
  1.2315 -val equalityD1 = @{thm equalityD1}
  1.2316 -val equalityD2 = @{thm equalityD2}
  1.2317 -val equalityE = @{thm equalityE}
  1.2318 -val equalityI = @{thm equalityI}
  1.2319 -val imageE = @{thm imageE}
  1.2320 -val imageI = @{thm imageI}
  1.2321 -val image_Un = @{thm image_Un}
  1.2322 -val image_insert = @{thm image_insert}
  1.2323 -val insert_commute = @{thm insert_commute}
  1.2324 -val insert_iff = @{thm insert_iff}
  1.2325 -val mem_Collect_eq = @{thm mem_Collect_eq}
  1.2326 -val rangeE = @{thm rangeE}
  1.2327 -val rangeI = @{thm rangeI}
  1.2328 -val range_eqI = @{thm range_eqI}
  1.2329 -val subsetCE = @{thm subsetCE}
  1.2330 -val subsetD = @{thm subsetD}
  1.2331 -val subsetI = @{thm subsetI}
  1.2332 -val subset_refl = @{thm subset_refl}
  1.2333 -val subset_trans = @{thm subset_trans}
  1.2334 -val vimageD = @{thm vimageD}
  1.2335 -val vimageE = @{thm vimageE}
  1.2336 -val vimageI = @{thm vimageI}
  1.2337 -val vimageI2 = @{thm vimageI2}
  1.2338 -val vimage_Collect = @{thm vimage_Collect}
  1.2339 -val vimage_Int = @{thm vimage_Int}
  1.2340 -val vimage_Un = @{thm vimage_Un}
  1.2341 -*}
  1.2342 -
  1.2343  end
     2.1 --- a/src/HOL/Tools/Function/fundef_lib.ML	Wed Jul 22 14:20:32 2009 +0200
     2.2 +++ b/src/HOL/Tools/Function/fundef_lib.ML	Wed Jul 22 14:20:32 2009 +0200
     2.3 @@ -167,10 +167,10 @@
     2.4   end
     2.5  
     2.6  (* instance for unions *)
     2.7 -fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Un}
     2.8 -  (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @
     2.9 -                                     @{thms "Un_empty_right"} @
    2.10 -                                     @{thms "Un_empty_left"})) t
    2.11 +fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Set.union}
    2.12 +  (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
    2.13 +                                     @{thms Un_empty_right} @
    2.14 +                                     @{thms Un_empty_left})) t
    2.15  
    2.16  
    2.17  end
     3.1 --- a/src/HOL/Tools/Function/termination.ML	Wed Jul 22 14:20:32 2009 +0200
     3.2 +++ b/src/HOL/Tools/Function/termination.ML	Wed Jul 22 14:20:32 2009 +0200
     3.3 @@ -145,7 +145,7 @@
     3.4  
     3.5  fun mk_sum_skel rel =
     3.6    let
     3.7 -    val cs = FundefLib.dest_binop_list @{const_name Un} rel
     3.8 +    val cs = FundefLib.dest_binop_list @{const_name union} rel
     3.9      fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) =
    3.10        let
    3.11          val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
    3.12 @@ -233,7 +233,7 @@
    3.13  fun CALLS tac i st =
    3.14    if Thm.no_prems st then all_tac st
    3.15    else case Thm.term_of (Thm.cprem_of st i) of
    3.16 -    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Un} rel, i) st
    3.17 +    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name union} rel, i) st
    3.18    |_ => no_tac st
    3.19  
    3.20  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
    3.21 @@ -293,7 +293,7 @@
    3.22            if null ineqs then
    3.23                Const (@{const_name Set.empty}, fastype_of rel)
    3.24            else
    3.25 -              foldr1 (HOLogic.mk_binop @{const_name Un}) (map mk_compr ineqs)
    3.26 +              foldr1 (HOLogic.mk_binop @{const_name union}) (map mk_compr ineqs)
    3.27  
    3.28        fun solve_membership_tac i =
    3.29            (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
     4.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Jul 22 14:20:32 2009 +0200
     4.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Jul 22 14:20:32 2009 +0200
     4.3 @@ -73,8 +73,8 @@
     4.4          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
     4.5            (p (fold (Logic.all o Var) vs t) f)
     4.6          end;
     4.7 -      fun mkop "op &" T x = SOME (Const (@{const_name "Int"}, T --> T --> T), x)
     4.8 -        | mkop "op |" T x = SOME (Const (@{const_name "Un"}, T --> T --> T), x)
     4.9 +      fun mkop "op &" T x = SOME (Const (@{const_name inter}, T --> T --> T), x)
    4.10 +        | mkop "op |" T x = SOME (Const (@{const_name union}, T --> T --> T), x)
    4.11          | mkop _ _ _ = NONE;
    4.12        fun mk_collect p T t =
    4.13          let val U = HOLogic.dest_setT T
     5.1 --- a/src/HOL/Tools/res_clause.ML	Wed Jul 22 14:20:32 2009 +0200
     5.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Jul 22 14:20:32 2009 +0200
     5.3 @@ -110,8 +110,8 @@
     5.4                     (@{const_name "op -->"}, "implies"),
     5.5                     (@{const_name Set.empty}, "emptyset"),
     5.6                     (@{const_name "op :"}, "in"),
     5.7 -                   (@{const_name Un}, "union"),
     5.8 -                   (@{const_name Int}, "inter"),
     5.9 +                   (@{const_name union}, "union"),
    5.10 +                   (@{const_name inter}, "inter"),
    5.11                     ("List.append", "append"),
    5.12                     ("ATP_Linkup.fequal", "fequal"),
    5.13                     ("ATP_Linkup.COMBI", "COMBI"),
     6.1 --- a/src/HOL/ex/Meson_Test.thy	Wed Jul 22 14:20:32 2009 +0200
     6.2 +++ b/src/HOL/ex/Meson_Test.thy	Wed Jul 22 14:20:32 2009 +0200
     6.3 @@ -1,4 +1,3 @@
     6.4 -(*ID:         $Id$*)
     6.5  
     6.6  header {* Meson test cases *}
     6.7  
     6.8 @@ -11,7 +10,7 @@
     6.9    below and constants declared in HOL!
    6.10  *}
    6.11  
    6.12 -hide const subset member quotient
    6.13 +hide (open) const subset member quotient union inter
    6.14  
    6.15  text {*
    6.16    Test data for the MESON proof procedure