author haftmann Wed Jul 22 14:20:32 2009 +0200 (2009-07-22) changeset 32135 f645b51e8e54 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 file | annotate | diff | revisions src/HOL/Tools/Function/fundef_lib.ML file | annotate | diff | revisions src/HOL/Tools/Function/termination.ML file | annotate | diff | revisions src/HOL/Tools/inductive_set.ML file | annotate | diff | revisions src/HOL/Tools/res_clause.ML file | annotate | diff | revisions src/HOL/ex/Meson_Test.thy file | annotate | diff | revisions
     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.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.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) (fB)"
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) (fA) = fA"
1.303 +by blast
1.304 +
1.305 +lemma image_is_empty [iff]: "(fA = {}) = (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) ==> fM = gN"
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)) = frange 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 ==> fA \<subseteq> fB"
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) <= fA Int fB"
1.807 +by blast
1.808 +
1.809 +lemma image_diff_subset: "fA - fB <= 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.929 +  by (simp add: Inf_fun_def)
1.930
1.931  lemma Sup_empty_fun:
1.932    "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
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.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>(BA)"
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>(BA)"
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: "fA = (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.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>(BA)"
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>(BA)"
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.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) (fB)"
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) (fA) = fA"
1.1487 -by blast
1.1488 -
1.1489 -lemma image_is_empty [iff]: "(fA = {}) = (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) ==> fM = gN"
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)) = frange 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 ==> fA \<subseteq> fB"
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) <= fA Int fB"
1.2216 -by blast
1.2217 -
1.2218 -lemma image_diff_subset: "fA - fB <= 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
`