merged
authorhaftmann
Wed Jul 22 14:21:52 2009 +0200 (2009-07-22)
changeset 32136672dfd59ff03
parent 32132 29aed5725acb
parent 32135 f645b51e8e54
child 32138 cabd6096892c
child 32139 e271a64f03ff
merged
NEWS
     1.1 --- a/NEWS	Wed Jul 22 11:48:04 2009 +0200
     1.2 +++ b/NEWS	Wed Jul 22 14:21:52 2009 +0200
     1.3 @@ -18,6 +18,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* More convenient names for set intersection and union.  INCOMPATIBILITY:
     1.8 +
     1.9 +    Set.Int ~>  Set.inter
    1.10 +    Set.Un ~>   Set.union
    1.11 +
    1.12  * Code generator attributes follow the usual underscore convention:
    1.13      code_unfold     replaces    code unfold
    1.14      code_post       replaces    code post
     2.1 --- a/src/HOL/Bali/DeclConcepts.thy	Wed Jul 22 11:48:04 2009 +0200
     2.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed Jul 22 14:21:52 2009 +0200
     2.3 @@ -648,7 +648,7 @@
     2.4             G \<turnstile>Method old member_of superNew
     2.5             \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
     2.6  
     2.7 -| Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S inter; G\<turnstile>inter overrides\<^sub>S old\<rbrakk>
     2.8 +| Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S intr; G\<turnstile>intr overrides\<^sub>S old\<rbrakk>
     2.9               \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
    2.10  
    2.11  text {* Dynamic overriding (used during the typecheck of the compiler) *}
    2.12 @@ -668,7 +668,7 @@
    2.13             G\<turnstile>resTy new \<preceq> resTy old
    2.14             \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides old"
    2.15  
    2.16 -| Indirect: "\<lbrakk>G\<turnstile>new overrides inter; G\<turnstile>inter overrides old\<rbrakk>
    2.17 +| Indirect: "\<lbrakk>G\<turnstile>new overrides intr; G\<turnstile>intr overrides old\<rbrakk>
    2.18              \<Longrightarrow> G\<turnstile>new overrides old"
    2.19  
    2.20  syntax
     3.1 --- a/src/HOL/Hoare/Hoare.thy	Wed Jul 22 11:48:04 2009 +0200
     3.2 +++ b/src/HOL/Hoare/Hoare.thy	Wed Jul 22 14:21:52 2009 +0200
     3.3 @@ -161,7 +161,7 @@
     3.4  (* assn_tr' & bexp_tr'*)
     3.5  ML{*  
     3.6  fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
     3.7 -  | assn_tr' (Const (@{const_name Set.Int}, _) $ (Const ("Collect",_) $ T1) $ 
     3.8 +  | assn_tr' (Const (@{const_name inter}, _) $ (Const ("Collect",_) $ T1) $ 
     3.9                                     (Const ("Collect",_) $ T2)) =  
    3.10              Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
    3.11    | assn_tr' t = t;
     4.1 --- a/src/HOL/Hoare/HoareAbort.thy	Wed Jul 22 11:48:04 2009 +0200
     4.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Wed Jul 22 14:21:52 2009 +0200
     4.3 @@ -163,7 +163,7 @@
     4.4  (* assn_tr' & bexp_tr'*)
     4.5  ML{*  
     4.6  fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
     4.7 -  | assn_tr' (Const (@{const_name Int},_) $ (Const ("Collect",_) $ T1) $ 
     4.8 +  | assn_tr' (Const (@{const_name inter},_) $ (Const ("Collect",_) $ T1) $ 
     4.9                                     (Const ("Collect",_) $ T2)) =  
    4.10              Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
    4.11    | assn_tr' t = t;
     5.1 --- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Wed Jul 22 11:48:04 2009 +0200
     5.2 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Wed Jul 22 14:21:52 2009 +0200
     5.3 @@ -1263,7 +1263,7 @@
     5.4   apply(simp add: Mul_Mutator_def mul_collector_defs mul_mutator_defs nth_append)
     5.5   apply force
     5.6  apply clarify
     5.7 -apply(case_tac xa)
     5.8 +apply(case_tac i)
     5.9   apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
    5.10  apply(simp add: Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append nth_map_upt)
    5.11  --{* Collector *}
     6.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Jul 22 11:48:04 2009 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Jul 22 14:21:52 2009 +0200
     6.3 @@ -1013,7 +1013,7 @@
     6.4                (HOLogic.mk_Trueprop (HOLogic.mk_eq
     6.5                  (supp c,
     6.6                   if null dts then HOLogic.mk_set atomT []
     6.7 -                 else foldr1 (HOLogic.mk_binop @{const_name Un}) (map supp args2)))))
     6.8 +                 else foldr1 (HOLogic.mk_binop @{const_name union}) (map supp args2)))))
     6.9              (fn _ =>
    6.10                simp_tac (HOL_basic_ss addsimps (supp_def ::
    6.11                   Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
     7.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Jul 22 11:48:04 2009 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Jul 22 14:21:52 2009 +0200
     7.3 @@ -196,7 +196,7 @@
     7.4            | add_set (t, T) ((u, U) :: ps) =
     7.5                if T = U then
     7.6                  let val S = HOLogic.mk_setT T
     7.7 -                in (Const (@{const_name "Un"}, S --> S --> S) $ u $ t, T) :: ps
     7.8 +                in (Const (@{const_name union}, S --> S --> S) $ u $ t, T) :: ps
     7.9                  end
    7.10                else (u, U) :: add_set (t, T) ps
    7.11        in
     8.1 --- a/src/HOL/Set.thy	Wed Jul 22 11:48:04 2009 +0200
     8.2 +++ b/src/HOL/Set.thy	Wed Jul 22 14:21:52 2009 +0200
     8.3 @@ -103,7 +103,7 @@
     8.4  text {* Set enumerations *}
     8.5  
     8.6  definition empty :: "'a set" ("{}") where
     8.7 -  "empty = {x. False}"
     8.8 +  bot_set_eq [symmetric]: "{} = bot"
     8.9  
    8.10  definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    8.11    insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
    8.12 @@ -544,7 +544,11 @@
    8.13  subsubsection {* The universal set -- UNIV *}
    8.14  
    8.15  definition UNIV :: "'a set" where
    8.16 +  top_set_eq [symmetric]: "UNIV = top"
    8.17 +
    8.18 +lemma UNIV_def:
    8.19    "UNIV = {x. True}"
    8.20 +  by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq Collect_def)
    8.21  
    8.22  lemma UNIV_I [simp]: "x : UNIV"
    8.23    by (simp add: UNIV_def)
    8.24 @@ -557,9 +561,6 @@
    8.25  lemma subset_UNIV [simp]: "A \<subseteq> UNIV"
    8.26    by (rule subsetI) (rule UNIV_I)
    8.27  
    8.28 -lemma top_set_eq: "top = UNIV"
    8.29 -  by (iprover intro!: subset_antisym subset_UNIV top_greatest)
    8.30 -
    8.31  text {*
    8.32    \medskip Eta-contracting these two rules (to remove @{text P})
    8.33    causes them to be ignored because of their interaction with
    8.34 @@ -578,6 +579,10 @@
    8.35  
    8.36  subsubsection {* The empty set *}
    8.37  
    8.38 +lemma empty_def:
    8.39 +  "{} = {x. False}"
    8.40 +  by (simp add: bot_set_eq [symmetric] bot_fun_eq bot_bool_eq Collect_def)
    8.41 +
    8.42  lemma empty_iff [simp]: "(c : {}) = False"
    8.43    by (simp add: empty_def)
    8.44  
    8.45 @@ -588,9 +593,6 @@
    8.46      -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
    8.47    by blast
    8.48  
    8.49 -lemma bot_set_eq: "bot = {}"
    8.50 -  by (iprover intro!: subset_antisym empty_subsetI bot_least)
    8.51 -
    8.52  lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
    8.53    by blast
    8.54  
    8.55 @@ -652,17 +654,18 @@
    8.56  
    8.57  subsubsection {* Binary union -- Un *}
    8.58  
    8.59 -definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
    8.60 -  "A Un B = {x. x \<in> A \<or> x \<in> B}"
    8.61 +definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
    8.62 +  sup_set_eq [symmetric]: "A Un B = sup A B"
    8.63  
    8.64  notation (xsymbols)
    8.65 -  "Un"  (infixl "\<union>" 65)
    8.66 +  union  (infixl "\<union>" 65)
    8.67  
    8.68  notation (HTML output)
    8.69 -  "Un"  (infixl "\<union>" 65)
    8.70 -
    8.71 -lemma sup_set_eq: "sup A B = A \<union> B"
    8.72 -  by (simp add: sup_fun_eq sup_bool_eq Un_def Collect_def mem_def)
    8.73 +  union  (infixl "\<union>" 65)
    8.74 +
    8.75 +lemma Un_def:
    8.76 +  "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
    8.77 +  by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
    8.78  
    8.79  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
    8.80    by (unfold Un_def) blast
    8.81 @@ -695,17 +698,18 @@
    8.82  
    8.83  subsubsection {* Binary intersection -- Int *}
    8.84  
    8.85 -definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    8.86 -  "A Int B = {x. x \<in> A \<and> x \<in> B}"
    8.87 +definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    8.88 +  inf_set_eq [symmetric]: "A Int B = inf A B"
    8.89  
    8.90  notation (xsymbols)
    8.91 -  "Int"  (infixl "\<inter>" 70)
    8.92 +  inter  (infixl "\<inter>" 70)
    8.93  
    8.94  notation (HTML output)
    8.95 -  "Int"  (infixl "\<inter>" 70)
    8.96 -
    8.97 -lemma inf_set_eq: "inf A B = A \<inter> B"
    8.98 -  by (simp add: inf_fun_eq inf_bool_eq Int_def Collect_def mem_def)
    8.99 +  inter  (infixl "\<inter>" 70)
   8.100 +
   8.101 +lemma Int_def:
   8.102 +  "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
   8.103 +  by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
   8.104  
   8.105  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   8.106    by (unfold Int_def) blast
   8.107 @@ -933,6 +937,803 @@
   8.108   *)
   8.109  
   8.110  
   8.111 +subsection {* Further operations and lemmas *}
   8.112 +
   8.113 +subsubsection {* The ``proper subset'' relation *}
   8.114 +
   8.115 +lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
   8.116 +  by (unfold less_le) blast
   8.117 +
   8.118 +lemma psubsetE [elim!,noatp]: 
   8.119 +    "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
   8.120 +  by (unfold less_le) blast
   8.121 +
   8.122 +lemma psubset_insert_iff:
   8.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)"
   8.124 +  by (auto simp add: less_le subset_insert_iff)
   8.125 +
   8.126 +lemma psubset_eq: "(A \<subset> B) = (A \<subseteq> B & A \<noteq> B)"
   8.127 +  by (simp only: less_le)
   8.128 +
   8.129 +lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
   8.130 +  by (simp add: psubset_eq)
   8.131 +
   8.132 +lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C"
   8.133 +apply (unfold less_le)
   8.134 +apply (auto dest: subset_antisym)
   8.135 +done
   8.136 +
   8.137 +lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B"
   8.138 +apply (unfold less_le)
   8.139 +apply (auto dest: subsetD)
   8.140 +done
   8.141 +
   8.142 +lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
   8.143 +  by (auto simp add: psubset_eq)
   8.144 +
   8.145 +lemma subset_psubset_trans: "A \<subseteq> B ==> B \<subset> C ==> A \<subset> C"
   8.146 +  by (auto simp add: psubset_eq)
   8.147 +
   8.148 +lemma psubset_imp_ex_mem: "A \<subset> B ==> \<exists>b. b \<in> (B - A)"
   8.149 +  by (unfold less_le) blast
   8.150 +
   8.151 +lemma atomize_ball:
   8.152 +    "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"
   8.153 +  by (simp only: Ball_def atomize_all atomize_imp)
   8.154 +
   8.155 +lemmas [symmetric, rulify] = atomize_ball
   8.156 +  and [symmetric, defn] = atomize_ball
   8.157 +
   8.158 +subsubsection {* Derived rules involving subsets. *}
   8.159 +
   8.160 +text {* @{text insert}. *}
   8.161 +
   8.162 +lemma subset_insertI: "B \<subseteq> insert a B"
   8.163 +  by (rule subsetI) (erule insertI2)
   8.164 +
   8.165 +lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B"
   8.166 +  by blast
   8.167 +
   8.168 +lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
   8.169 +  by blast
   8.170 +
   8.171 +
   8.172 +text {* \medskip Finite Union -- the least upper bound of two sets. *}
   8.173 +
   8.174 +lemma Un_upper1: "A \<subseteq> A \<union> B"
   8.175 +  by blast
   8.176 +
   8.177 +lemma Un_upper2: "B \<subseteq> A \<union> B"
   8.178 +  by blast
   8.179 +
   8.180 +lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"
   8.181 +  by blast
   8.182 +
   8.183 +
   8.184 +text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}
   8.185 +
   8.186 +lemma Int_lower1: "A \<inter> B \<subseteq> A"
   8.187 +  by blast
   8.188 +
   8.189 +lemma Int_lower2: "A \<inter> B \<subseteq> B"
   8.190 +  by blast
   8.191 +
   8.192 +lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"
   8.193 +  by blast
   8.194 +
   8.195 +
   8.196 +text {* \medskip Set difference. *}
   8.197 +
   8.198 +lemma Diff_subset: "A - B \<subseteq> A"
   8.199 +  by blast
   8.200 +
   8.201 +lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)"
   8.202 +by blast
   8.203 +
   8.204 +
   8.205 +subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
   8.206 +
   8.207 +text {* @{text "{}"}. *}
   8.208 +
   8.209 +lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
   8.210 +  -- {* supersedes @{text "Collect_False_empty"} *}
   8.211 +  by auto
   8.212 +
   8.213 +lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
   8.214 +  by blast
   8.215 +
   8.216 +lemma not_psubset_empty [iff]: "\<not> (A < {})"
   8.217 +  by (unfold less_le) blast
   8.218 +
   8.219 +lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"
   8.220 +by blast
   8.221 +
   8.222 +lemma empty_Collect_eq [simp]: "({} = Collect P) = (\<forall>x. \<not> P x)"
   8.223 +by blast
   8.224 +
   8.225 +lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}"
   8.226 +  by blast
   8.227 +
   8.228 +lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \<union> {x. Q x}"
   8.229 +  by blast
   8.230 +
   8.231 +lemma Collect_imp_eq: "{x. P x --> Q x} = -{x. P x} \<union> {x. Q x}"
   8.232 +  by blast
   8.233 +
   8.234 +lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
   8.235 +  by blast
   8.236 +
   8.237 +
   8.238 +text {* \medskip @{text insert}. *}
   8.239 +
   8.240 +lemma insert_is_Un: "insert a A = {a} Un A"
   8.241 +  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *}
   8.242 +  by blast
   8.243 +
   8.244 +lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
   8.245 +  by blast
   8.246 +
   8.247 +lemmas empty_not_insert = insert_not_empty [symmetric, standard]
   8.248 +declare empty_not_insert [simp]
   8.249 +
   8.250 +lemma insert_absorb: "a \<in> A ==> insert a A = A"
   8.251 +  -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}
   8.252 +  -- {* with \emph{quadratic} running time *}
   8.253 +  by blast
   8.254 +
   8.255 +lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
   8.256 +  by blast
   8.257 +
   8.258 +lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"
   8.259 +  by blast
   8.260 +
   8.261 +lemma insert_subset [simp]: "(insert x A \<subseteq> B) = (x \<in> B & A \<subseteq> B)"
   8.262 +  by blast
   8.263 +
   8.264 +lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
   8.265 +  -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}
   8.266 +  apply (rule_tac x = "A - {a}" in exI, blast)
   8.267 +  done
   8.268 +
   8.269 +lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}"
   8.270 +  by auto
   8.271 +
   8.272 +lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
   8.273 +  by blast
   8.274 +
   8.275 +lemma insert_disjoint [simp,noatp]:
   8.276 + "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
   8.277 + "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
   8.278 +  by auto
   8.279 +
   8.280 +lemma disjoint_insert [simp,noatp]:
   8.281 + "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
   8.282 + "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
   8.283 +  by auto
   8.284 +
   8.285 +text {* \medskip @{text image}. *}
   8.286 +
   8.287 +lemma image_empty [simp]: "f`{} = {}"
   8.288 +  by blast
   8.289 +
   8.290 +lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)"
   8.291 +  by blast
   8.292 +
   8.293 +lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
   8.294 +  by auto
   8.295 +
   8.296 +lemma image_constant_conv: "(%x. c) ` A = (if A = {} then {} else {c})"
   8.297 +by auto
   8.298 +
   8.299 +lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
   8.300 +by blast
   8.301 +
   8.302 +lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
   8.303 +by blast
   8.304 +
   8.305 +lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
   8.306 +by blast
   8.307 +
   8.308 +lemma empty_is_image[iff]: "({} = f ` A) = (A = {})"
   8.309 +by blast
   8.310 +
   8.311 +
   8.312 +lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
   8.313 +  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
   8.314 +      with its implicit quantifier and conjunction.  Also image enjoys better
   8.315 +      equational properties than does the RHS. *}
   8.316 +  by blast
   8.317 +
   8.318 +lemma if_image_distrib [simp]:
   8.319 +  "(\<lambda>x. if P x then f x else g x) ` S
   8.320 +    = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
   8.321 +  by (auto simp add: image_def)
   8.322 +
   8.323 +lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
   8.324 +  by (simp add: image_def)
   8.325 +
   8.326 +
   8.327 +text {* \medskip @{text range}. *}
   8.328 +
   8.329 +lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
   8.330 +  by auto
   8.331 +
   8.332 +lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
   8.333 +by (subst image_image, simp)
   8.334 +
   8.335 +
   8.336 +text {* \medskip @{text Int} *}
   8.337 +
   8.338 +lemma Int_absorb [simp]: "A \<inter> A = A"
   8.339 +  by blast
   8.340 +
   8.341 +lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
   8.342 +  by blast
   8.343 +
   8.344 +lemma Int_commute: "A \<inter> B = B \<inter> A"
   8.345 +  by blast
   8.346 +
   8.347 +lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
   8.348 +  by blast
   8.349 +
   8.350 +lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)"
   8.351 +  by blast
   8.352 +
   8.353 +lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
   8.354 +  -- {* Intersection is an AC-operator *}
   8.355 +
   8.356 +lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
   8.357 +  by blast
   8.358 +
   8.359 +lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
   8.360 +  by blast
   8.361 +
   8.362 +lemma Int_empty_left [simp]: "{} \<inter> B = {}"
   8.363 +  by blast
   8.364 +
   8.365 +lemma Int_empty_right [simp]: "A \<inter> {} = {}"
   8.366 +  by blast
   8.367 +
   8.368 +lemma disjoint_eq_subset_Compl: "(A \<inter> B = {}) = (A \<subseteq> -B)"
   8.369 +  by blast
   8.370 +
   8.371 +lemma disjoint_iff_not_equal: "(A \<inter> B = {}) = (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
   8.372 +  by blast
   8.373 +
   8.374 +lemma Int_UNIV_left [simp]: "UNIV \<inter> B = B"
   8.375 +  by blast
   8.376 +
   8.377 +lemma Int_UNIV_right [simp]: "A \<inter> UNIV = A"
   8.378 +  by blast
   8.379 +
   8.380 +lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
   8.381 +  by blast
   8.382 +
   8.383 +lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
   8.384 +  by blast
   8.385 +
   8.386 +lemma Int_UNIV [simp,noatp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
   8.387 +  by blast
   8.388 +
   8.389 +lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
   8.390 +  by blast
   8.391 +
   8.392 +lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
   8.393 +  by blast
   8.394 +
   8.395 +
   8.396 +text {* \medskip @{text Un}. *}
   8.397 +
   8.398 +lemma Un_absorb [simp]: "A \<union> A = A"
   8.399 +  by blast
   8.400 +
   8.401 +lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
   8.402 +  by blast
   8.403 +
   8.404 +lemma Un_commute: "A \<union> B = B \<union> A"
   8.405 +  by blast
   8.406 +
   8.407 +lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
   8.408 +  by blast
   8.409 +
   8.410 +lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)"
   8.411 +  by blast
   8.412 +
   8.413 +lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
   8.414 +  -- {* Union is an AC-operator *}
   8.415 +
   8.416 +lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
   8.417 +  by blast
   8.418 +
   8.419 +lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
   8.420 +  by blast
   8.421 +
   8.422 +lemma Un_empty_left [simp]: "{} \<union> B = B"
   8.423 +  by blast
   8.424 +
   8.425 +lemma Un_empty_right [simp]: "A \<union> {} = A"
   8.426 +  by blast
   8.427 +
   8.428 +lemma Un_UNIV_left [simp]: "UNIV \<union> B = UNIV"
   8.429 +  by blast
   8.430 +
   8.431 +lemma Un_UNIV_right [simp]: "A \<union> UNIV = UNIV"
   8.432 +  by blast
   8.433 +
   8.434 +lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"
   8.435 +  by blast
   8.436 +
   8.437 +lemma Un_insert_right [simp]: "A \<union> (insert a B) = insert a (A \<union> B)"
   8.438 +  by blast
   8.439 +
   8.440 +lemma Int_insert_left:
   8.441 +    "(insert a B) Int C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"
   8.442 +  by auto
   8.443 +
   8.444 +lemma Int_insert_right:
   8.445 +    "A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"
   8.446 +  by auto
   8.447 +
   8.448 +lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
   8.449 +  by blast
   8.450 +
   8.451 +lemma Un_Int_distrib2: "(B \<inter> C) \<union> A = (B \<union> A) \<inter> (C \<union> A)"
   8.452 +  by blast
   8.453 +
   8.454 +lemma Un_Int_crazy:
   8.455 +    "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
   8.456 +  by blast
   8.457 +
   8.458 +lemma subset_Un_eq: "(A \<subseteq> B) = (A \<union> B = B)"
   8.459 +  by blast
   8.460 +
   8.461 +lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
   8.462 +  by blast
   8.463 +
   8.464 +lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
   8.465 +  by blast
   8.466 +
   8.467 +lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
   8.468 +  by blast
   8.469 +
   8.470 +lemma Diff_Int2: "A \<inter> C - B \<inter> C = A \<inter> C - B"
   8.471 +  by blast
   8.472 +
   8.473 +
   8.474 +text {* \medskip Set complement *}
   8.475 +
   8.476 +lemma Compl_disjoint [simp]: "A \<inter> -A = {}"
   8.477 +  by blast
   8.478 +
   8.479 +lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"
   8.480 +  by blast
   8.481 +
   8.482 +lemma Compl_partition: "A \<union> -A = UNIV"
   8.483 +  by blast
   8.484 +
   8.485 +lemma Compl_partition2: "-A \<union> A = UNIV"
   8.486 +  by blast
   8.487 +
   8.488 +lemma double_complement [simp]: "- (-A) = (A::'a set)"
   8.489 +  by blast
   8.490 +
   8.491 +lemma Compl_Un [simp]: "-(A \<union> B) = (-A) \<inter> (-B)"
   8.492 +  by blast
   8.493 +
   8.494 +lemma Compl_Int [simp]: "-(A \<inter> B) = (-A) \<union> (-B)"
   8.495 +  by blast
   8.496 +
   8.497 +lemma subset_Compl_self_eq: "(A \<subseteq> -A) = (A = {})"
   8.498 +  by blast
   8.499 +
   8.500 +lemma Un_Int_assoc_eq: "((A \<inter> B) \<union> C = A \<inter> (B \<union> C)) = (C \<subseteq> A)"
   8.501 +  -- {* Halmos, Naive Set Theory, page 16. *}
   8.502 +  by blast
   8.503 +
   8.504 +lemma Compl_UNIV_eq [simp]: "-UNIV = {}"
   8.505 +  by blast
   8.506 +
   8.507 +lemma Compl_empty_eq [simp]: "-{} = UNIV"
   8.508 +  by blast
   8.509 +
   8.510 +lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
   8.511 +  by blast
   8.512 +
   8.513 +lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
   8.514 +  by blast
   8.515 +
   8.516 +text {* \medskip Bounded quantifiers.
   8.517 +
   8.518 +  The following are not added to the default simpset because
   8.519 +  (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}
   8.520 +
   8.521 +lemma ball_Un: "(\<forall>x \<in> A \<union> B. P x) = ((\<forall>x\<in>A. P x) & (\<forall>x\<in>B. P x))"
   8.522 +  by blast
   8.523 +
   8.524 +lemma bex_Un: "(\<exists>x \<in> A \<union> B. P x) = ((\<exists>x\<in>A. P x) | (\<exists>x\<in>B. P x))"
   8.525 +  by blast
   8.526 +
   8.527 +
   8.528 +text {* \medskip Set difference. *}
   8.529 +
   8.530 +lemma Diff_eq: "A - B = A \<inter> (-B)"
   8.531 +  by blast
   8.532 +
   8.533 +lemma Diff_eq_empty_iff [simp,noatp]: "(A - B = {}) = (A \<subseteq> B)"
   8.534 +  by blast
   8.535 +
   8.536 +lemma Diff_cancel [simp]: "A - A = {}"
   8.537 +  by blast
   8.538 +
   8.539 +lemma Diff_idemp [simp]: "(A - B) - B = A - (B::'a set)"
   8.540 +by blast
   8.541 +
   8.542 +lemma Diff_triv: "A \<inter> B = {} ==> A - B = A"
   8.543 +  by (blast elim: equalityE)
   8.544 +
   8.545 +lemma empty_Diff [simp]: "{} - A = {}"
   8.546 +  by blast
   8.547 +
   8.548 +lemma Diff_empty [simp]: "A - {} = A"
   8.549 +  by blast
   8.550 +
   8.551 +lemma Diff_UNIV [simp]: "A - UNIV = {}"
   8.552 +  by blast
   8.553 +
   8.554 +lemma Diff_insert0 [simp,noatp]: "x \<notin> A ==> A - insert x B = A - B"
   8.555 +  by blast
   8.556 +
   8.557 +lemma Diff_insert: "A - insert a B = A - B - {a}"
   8.558 +  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
   8.559 +  by blast
   8.560 +
   8.561 +lemma Diff_insert2: "A - insert a B = A - {a} - B"
   8.562 +  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
   8.563 +  by blast
   8.564 +
   8.565 +lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))"
   8.566 +  by auto
   8.567 +
   8.568 +lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B"
   8.569 +  by blast
   8.570 +
   8.571 +lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A"
   8.572 +by blast
   8.573 +
   8.574 +lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A"
   8.575 +  by blast
   8.576 +
   8.577 +lemma Diff_insert_absorb: "x \<notin> A ==> (insert x A) - {x} = A"
   8.578 +  by auto
   8.579 +
   8.580 +lemma Diff_disjoint [simp]: "A \<inter> (B - A) = {}"
   8.581 +  by blast
   8.582 +
   8.583 +lemma Diff_partition: "A \<subseteq> B ==> A \<union> (B - A) = B"
   8.584 +  by blast
   8.585 +
   8.586 +lemma double_diff: "A \<subseteq> B ==> B \<subseteq> C ==> B - (C - A) = A"
   8.587 +  by blast
   8.588 +
   8.589 +lemma Un_Diff_cancel [simp]: "A \<union> (B - A) = A \<union> B"
   8.590 +  by blast
   8.591 +
   8.592 +lemma Un_Diff_cancel2 [simp]: "(B - A) \<union> A = B \<union> A"
   8.593 +  by blast
   8.594 +
   8.595 +lemma Diff_Un: "A - (B \<union> C) = (A - B) \<inter> (A - C)"
   8.596 +  by blast
   8.597 +
   8.598 +lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"
   8.599 +  by blast
   8.600 +
   8.601 +lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
   8.602 +  by blast
   8.603 +
   8.604 +lemma Int_Diff: "(A \<inter> B) - C = A \<inter> (B - C)"
   8.605 +  by blast
   8.606 +
   8.607 +lemma Diff_Int_distrib: "C \<inter> (A - B) = (C \<inter> A) - (C \<inter> B)"
   8.608 +  by blast
   8.609 +
   8.610 +lemma Diff_Int_distrib2: "(A - B) \<inter> C = (A \<inter> C) - (B \<inter> C)"
   8.611 +  by blast
   8.612 +
   8.613 +lemma Diff_Compl [simp]: "A - (- B) = A \<inter> B"
   8.614 +  by auto
   8.615 +
   8.616 +lemma Compl_Diff_eq [simp]: "- (A - B) = -A \<union> B"
   8.617 +  by blast
   8.618 +
   8.619 +
   8.620 +text {* \medskip Quantification over type @{typ bool}. *}
   8.621 +
   8.622 +lemma bool_induct: "P True \<Longrightarrow> P False \<Longrightarrow> P x"
   8.623 +  by (cases x) auto
   8.624 +
   8.625 +lemma all_bool_eq: "(\<forall>b. P b) \<longleftrightarrow> P True \<and> P False"
   8.626 +  by (auto intro: bool_induct)
   8.627 +
   8.628 +lemma bool_contrapos: "P x \<Longrightarrow> \<not> P False \<Longrightarrow> P True"
   8.629 +  by (cases x) auto
   8.630 +
   8.631 +lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
   8.632 +  by (auto intro: bool_contrapos)
   8.633 +
   8.634 +text {* \medskip @{text Pow} *}
   8.635 +
   8.636 +lemma Pow_empty [simp]: "Pow {} = {{}}"
   8.637 +  by (auto simp add: Pow_def)
   8.638 +
   8.639 +lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
   8.640 +  by (blast intro: image_eqI [where ?x = "u - {a}", standard])
   8.641 +
   8.642 +lemma Pow_Compl: "Pow (- A) = {-B | B. A \<in> Pow B}"
   8.643 +  by (blast intro: exI [where ?x = "- u", standard])
   8.644 +
   8.645 +lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
   8.646 +  by blast
   8.647 +
   8.648 +lemma Un_Pow_subset: "Pow A \<union> Pow B \<subseteq> Pow (A \<union> B)"
   8.649 +  by blast
   8.650 +
   8.651 +lemma Pow_Int_eq [simp]: "Pow (A \<inter> B) = Pow A \<inter> Pow B"
   8.652 +  by blast
   8.653 +
   8.654 +
   8.655 +text {* \medskip Miscellany. *}
   8.656 +
   8.657 +lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
   8.658 +  by blast
   8.659 +
   8.660 +lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
   8.661 +  by blast
   8.662 +
   8.663 +lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
   8.664 +  by (unfold less_le) blast
   8.665 +
   8.666 +lemma all_not_in_conv [simp]: "(\<forall>x. x \<notin> A) = (A = {})"
   8.667 +  by blast
   8.668 +
   8.669 +lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
   8.670 +  by blast
   8.671 +
   8.672 +lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
   8.673 +  by iprover
   8.674 +
   8.675 +
   8.676 +subsubsection {* Monotonicity of various operations *}
   8.677 +
   8.678 +lemma image_mono: "A \<subseteq> B ==> f`A \<subseteq> f`B"
   8.679 +  by blast
   8.680 +
   8.681 +lemma Pow_mono: "A \<subseteq> B ==> Pow A \<subseteq> Pow B"
   8.682 +  by blast
   8.683 +
   8.684 +lemma insert_mono: "C \<subseteq> D ==> insert a C \<subseteq> insert a D"
   8.685 +  by blast
   8.686 +
   8.687 +lemma Un_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<union> B \<subseteq> C \<union> D"
   8.688 +  by blast
   8.689 +
   8.690 +lemma Int_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<inter> B \<subseteq> C \<inter> D"
   8.691 +  by blast
   8.692 +
   8.693 +lemma Diff_mono: "A \<subseteq> C ==> D \<subseteq> B ==> A - B \<subseteq> C - D"
   8.694 +  by blast
   8.695 +
   8.696 +lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"
   8.697 +  by blast
   8.698 +
   8.699 +text {* \medskip Monotonicity of implications. *}
   8.700 +
   8.701 +lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B"
   8.702 +  apply (rule impI)
   8.703 +  apply (erule subsetD, assumption)
   8.704 +  done
   8.705 +
   8.706 +lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
   8.707 +  by iprover
   8.708 +
   8.709 +lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"
   8.710 +  by iprover
   8.711 +
   8.712 +lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"
   8.713 +  by iprover
   8.714 +
   8.715 +lemma imp_refl: "P --> P" ..
   8.716 +
   8.717 +lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
   8.718 +  by iprover
   8.719 +
   8.720 +lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"
   8.721 +  by iprover
   8.722 +
   8.723 +lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \<subseteq> Collect Q"
   8.724 +  by blast
   8.725 +
   8.726 +lemma Int_Collect_mono:
   8.727 +    "A \<subseteq> B ==> (!!x. x \<in> A ==> P x --> Q x) ==> A \<inter> Collect P \<subseteq> B \<inter> Collect Q"
   8.728 +  by blast
   8.729 +
   8.730 +lemmas basic_monos =
   8.731 +  subset_refl imp_refl disj_mono conj_mono
   8.732 +  ex_mono Collect_mono in_mono
   8.733 +
   8.734 +lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
   8.735 +  by iprover
   8.736 +
   8.737 +lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
   8.738 +  by iprover
   8.739 +
   8.740 +
   8.741 +subsubsection {* Inverse image of a function *}
   8.742 +
   8.743 +constdefs
   8.744 +  vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
   8.745 +  [code del]: "f -` B == {x. f x : B}"
   8.746 +
   8.747 +lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
   8.748 +  by (unfold vimage_def) blast
   8.749 +
   8.750 +lemma vimage_singleton_eq: "(a : f -` {b}) = (f a = b)"
   8.751 +  by simp
   8.752 +
   8.753 +lemma vimageI [intro]: "f a = b ==> b:B ==> a : f -` B"
   8.754 +  by (unfold vimage_def) blast
   8.755 +
   8.756 +lemma vimageI2: "f a : A ==> a : f -` A"
   8.757 +  by (unfold vimage_def) fast
   8.758 +
   8.759 +lemma vimageE [elim!]: "a: f -` B ==> (!!x. f a = x ==> x:B ==> P) ==> P"
   8.760 +  by (unfold vimage_def) blast
   8.761 +
   8.762 +lemma vimageD: "a : f -` A ==> f a : A"
   8.763 +  by (unfold vimage_def) fast
   8.764 +
   8.765 +lemma vimage_empty [simp]: "f -` {} = {}"
   8.766 +  by blast
   8.767 +
   8.768 +lemma vimage_Compl: "f -` (-A) = -(f -` A)"
   8.769 +  by blast
   8.770 +
   8.771 +lemma vimage_Un [simp]: "f -` (A Un B) = (f -` A) Un (f -` B)"
   8.772 +  by blast
   8.773 +
   8.774 +lemma vimage_Int [simp]: "f -` (A Int B) = (f -` A) Int (f -` B)"
   8.775 +  by fast
   8.776 +
   8.777 +lemma vimage_Collect_eq [simp]: "f -` Collect P = {y. P (f y)}"
   8.778 +  by blast
   8.779 +
   8.780 +lemma vimage_Collect: "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q"
   8.781 +  by blast
   8.782 +
   8.783 +lemma vimage_insert: "f-`(insert a B) = (f-`{a}) Un (f-`B)"
   8.784 +  -- {* NOT suitable for rewriting because of the recurrence of @{term "{a}"}. *}
   8.785 +  by blast
   8.786 +
   8.787 +lemma vimage_Diff: "f -` (A - B) = (f -` A) - (f -` B)"
   8.788 +  by blast
   8.789 +
   8.790 +lemma vimage_UNIV [simp]: "f -` UNIV = UNIV"
   8.791 +  by blast
   8.792 +
   8.793 +lemma vimage_mono: "A \<subseteq> B ==> f -` A \<subseteq> f -` B"
   8.794 +  -- {* monotonicity *}
   8.795 +  by blast
   8.796 +
   8.797 +lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
   8.798 +by (blast intro: sym)
   8.799 +
   8.800 +lemma image_vimage_subset: "f ` (f -` A) <= A"
   8.801 +by blast
   8.802 +
   8.803 +lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
   8.804 +by blast
   8.805 +
   8.806 +lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
   8.807 +by blast
   8.808 +
   8.809 +lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
   8.810 +by blast
   8.811 +
   8.812 +
   8.813 +subsubsection {* Getting the Contents of a Singleton Set *}
   8.814 +
   8.815 +definition contents :: "'a set \<Rightarrow> 'a" where
   8.816 +  [code del]: "contents X = (THE x. X = {x})"
   8.817 +
   8.818 +lemma contents_eq [simp]: "contents {x} = x"
   8.819 +  by (simp add: contents_def)
   8.820 +
   8.821 +
   8.822 +subsubsection {* Least value operator *}
   8.823 +
   8.824 +lemma Least_mono:
   8.825 +  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
   8.826 +    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
   8.827 +    -- {* Courtesy of Stephan Merz *}
   8.828 +  apply clarify
   8.829 +  apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
   8.830 +  apply (rule LeastI2_order)
   8.831 +  apply (auto elim: monoD intro!: order_antisym)
   8.832 +  done
   8.833 +
   8.834 +subsection {* Misc *}
   8.835 +
   8.836 +text {* Rudimentary code generation *}
   8.837 +
   8.838 +lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
   8.839 +  by (auto simp add: insert_compr Collect_def mem_def)
   8.840 +
   8.841 +lemma vimage_code [code]: "(f -` A) x = A (f x)"
   8.842 +  by (simp add: vimage_def Collect_def mem_def)
   8.843 +
   8.844 +
   8.845 +text {* Misc theorem and ML bindings *}
   8.846 +
   8.847 +lemmas equalityI = subset_antisym
   8.848 +
   8.849 +ML {*
   8.850 +val Ball_def = @{thm Ball_def}
   8.851 +val Bex_def = @{thm Bex_def}
   8.852 +val CollectD = @{thm CollectD}
   8.853 +val CollectE = @{thm CollectE}
   8.854 +val CollectI = @{thm CollectI}
   8.855 +val Collect_conj_eq = @{thm Collect_conj_eq}
   8.856 +val Collect_mem_eq = @{thm Collect_mem_eq}
   8.857 +val IntD1 = @{thm IntD1}
   8.858 +val IntD2 = @{thm IntD2}
   8.859 +val IntE = @{thm IntE}
   8.860 +val IntI = @{thm IntI}
   8.861 +val Int_Collect = @{thm Int_Collect}
   8.862 +val UNIV_I = @{thm UNIV_I}
   8.863 +val UNIV_witness = @{thm UNIV_witness}
   8.864 +val UnE = @{thm UnE}
   8.865 +val UnI1 = @{thm UnI1}
   8.866 +val UnI2 = @{thm UnI2}
   8.867 +val ballE = @{thm ballE}
   8.868 +val ballI = @{thm ballI}
   8.869 +val bexCI = @{thm bexCI}
   8.870 +val bexE = @{thm bexE}
   8.871 +val bexI = @{thm bexI}
   8.872 +val bex_triv = @{thm bex_triv}
   8.873 +val bspec = @{thm bspec}
   8.874 +val contra_subsetD = @{thm contra_subsetD}
   8.875 +val distinct_lemma = @{thm distinct_lemma}
   8.876 +val eq_to_mono = @{thm eq_to_mono}
   8.877 +val eq_to_mono2 = @{thm eq_to_mono2}
   8.878 +val equalityCE = @{thm equalityCE}
   8.879 +val equalityD1 = @{thm equalityD1}
   8.880 +val equalityD2 = @{thm equalityD2}
   8.881 +val equalityE = @{thm equalityE}
   8.882 +val equalityI = @{thm equalityI}
   8.883 +val imageE = @{thm imageE}
   8.884 +val imageI = @{thm imageI}
   8.885 +val image_Un = @{thm image_Un}
   8.886 +val image_insert = @{thm image_insert}
   8.887 +val insert_commute = @{thm insert_commute}
   8.888 +val insert_iff = @{thm insert_iff}
   8.889 +val mem_Collect_eq = @{thm mem_Collect_eq}
   8.890 +val rangeE = @{thm rangeE}
   8.891 +val rangeI = @{thm rangeI}
   8.892 +val range_eqI = @{thm range_eqI}
   8.893 +val subsetCE = @{thm subsetCE}
   8.894 +val subsetD = @{thm subsetD}
   8.895 +val subsetI = @{thm subsetI}
   8.896 +val subset_refl = @{thm subset_refl}
   8.897 +val subset_trans = @{thm subset_trans}
   8.898 +val vimageD = @{thm vimageD}
   8.899 +val vimageE = @{thm vimageE}
   8.900 +val vimageI = @{thm vimageI}
   8.901 +val vimageI2 = @{thm vimageI2}
   8.902 +val vimage_Collect = @{thm vimage_Collect}
   8.903 +val vimage_Int = @{thm vimage_Int}
   8.904 +val vimage_Un = @{thm vimage_Un}
   8.905 +*}
   8.906 +
   8.907 +
   8.908  subsection {* Complete lattices *}
   8.909  
   8.910  notation
   8.911 @@ -957,10 +1758,10 @@
   8.912    by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
   8.913  
   8.914  lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
   8.915 -  unfolding Sup_Inf by (auto simp add: UNIV_def)
   8.916 +  unfolding Sup_Inf by auto
   8.917  
   8.918  lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
   8.919 -  unfolding Inf_Sup by (auto simp add: UNIV_def)
   8.920 +  unfolding Inf_Sup by auto
   8.921  
   8.922  lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   8.923    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
   8.924 @@ -1120,29 +1921,29 @@
   8.925  
   8.926  lemma Inf_empty_fun:
   8.927    "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
   8.928 -  by rule (simp add: Inf_fun_def, simp add: empty_def)
   8.929 +  by (simp add: Inf_fun_def)
   8.930  
   8.931  lemma Sup_empty_fun:
   8.932    "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
   8.933 -  by rule (simp add: Sup_fun_def, simp add: empty_def)
   8.934 +  by (simp add: Sup_fun_def)
   8.935  
   8.936  
   8.937  subsubsection {* Union *}
   8.938  
   8.939  definition Union :: "'a set set \<Rightarrow> 'a set" where
   8.940 -  Union_eq [code del]: "Union A = {x. \<exists>B \<in> A. x \<in> B}"
   8.941 +  Sup_set_eq [symmetric]: "Union S = \<Squnion>S"
   8.942  
   8.943  notation (xsymbols)
   8.944    Union  ("\<Union>_" [90] 90)
   8.945  
   8.946 -lemma Sup_set_eq:
   8.947 -  "\<Squnion>S = \<Union>S"
   8.948 +lemma Union_eq:
   8.949 +  "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
   8.950  proof (rule set_ext)
   8.951    fix x
   8.952 -  have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
   8.953 +  have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
   8.954      by auto
   8.955 -  then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
   8.956 -    by (simp add: Sup_fun_def Sup_bool_def Union_eq) (simp add: mem_def)
   8.957 +  then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
   8.958 +    by (simp add: Sup_set_eq [symmetric] Sup_fun_def Sup_bool_def) (simp add: mem_def)
   8.959  qed
   8.960  
   8.961  lemma Union_iff [simp, noatp]:
   8.962 @@ -1159,11 +1960,53 @@
   8.963    "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A\<in>X \<Longrightarrow> X\<in>C \<Longrightarrow> R) \<Longrightarrow> R"
   8.964    by auto
   8.965  
   8.966 +lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"
   8.967 +  by (iprover intro: subsetI UnionI)
   8.968 +
   8.969 +lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
   8.970 +  by (iprover intro: subsetI elim: UnionE dest: subsetD)
   8.971 +
   8.972 +lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
   8.973 +  by blast
   8.974 +
   8.975 +lemma Union_empty [simp]: "Union({}) = {}"
   8.976 +  by blast
   8.977 +
   8.978 +lemma Union_UNIV [simp]: "Union UNIV = UNIV"
   8.979 +  by blast
   8.980 +
   8.981 +lemma Union_insert [simp]: "Union (insert a B) = a \<union> \<Union>B"
   8.982 +  by blast
   8.983 +
   8.984 +lemma Union_Un_distrib [simp]: "\<Union>(A Un B) = \<Union>A \<union> \<Union>B"
   8.985 +  by blast
   8.986 +
   8.987 +lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
   8.988 +  by blast
   8.989 +
   8.990 +lemma Union_empty_conv [simp,noatp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
   8.991 +  by blast
   8.992 +
   8.993 +lemma empty_Union_conv [simp,noatp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
   8.994 +  by blast
   8.995 +
   8.996 +lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
   8.997 +  by blast
   8.998 +
   8.999 +lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
  8.1000 +  by blast
  8.1001 +
  8.1002 +lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A"
  8.1003 +  by blast
  8.1004 +
  8.1005 +lemma Union_mono: "A \<subseteq> B ==> \<Union>A \<subseteq> \<Union>B"
  8.1006 +  by blast
  8.1007 +
  8.1008  
  8.1009  subsubsection {* Unions of families *}
  8.1010  
  8.1011  definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
  8.1012 -  UNION_eq_Union_image: "UNION A B = \<Union>(B`A)"
  8.1013 +  SUPR_set_eq [symmetric]: "UNION S f = (SUP x:S. f x)"
  8.1014  
  8.1015  syntax
  8.1016    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
  8.1017 @@ -1196,16 +2039,16 @@
  8.1018  Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} "@UNION"
  8.1019  ] *} -- {* to avoid eta-contraction of body *}
  8.1020  
  8.1021 -lemma SUPR_set_eq:
  8.1022 -  "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
  8.1023 -  by (simp add: SUPR_def UNION_eq_Union_image Sup_set_eq)
  8.1024 +lemma UNION_eq_Union_image:
  8.1025 +  "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
  8.1026 +  by (simp add: SUPR_def SUPR_set_eq [symmetric] Sup_set_eq)
  8.1027  
  8.1028  lemma Union_def:
  8.1029    "\<Union>S = (\<Union>x\<in>S. x)"
  8.1030    by (simp add: UNION_eq_Union_image image_def)
  8.1031  
  8.1032  lemma UNION_def [noatp]:
  8.1033 -  "UNION A B = {y. \<exists>x\<in>A. y \<in> B x}"
  8.1034 +  "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
  8.1035    by (auto simp add: UNION_eq_Union_image Union_eq)
  8.1036    
  8.1037  lemma Union_image_eq [simp]:
  8.1038 @@ -1234,23 +2077,109 @@
  8.1039  lemma image_eq_UN: "f`A = (UN x:A. {f x})"
  8.1040    by blast
  8.1041  
  8.1042 +lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
  8.1043 +  by blast
  8.1044 +
  8.1045 +lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
  8.1046 +  by (iprover intro: subsetI elim: UN_E dest: subsetD)
  8.1047 +
  8.1048 +lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
  8.1049 +  by blast
  8.1050 +
  8.1051 +lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
  8.1052 +  by blast
  8.1053 +
  8.1054 +lemma UN_empty [simp,noatp]: "(\<Union>x\<in>{}. B x) = {}"
  8.1055 +  by blast
  8.1056 +
  8.1057 +lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
  8.1058 +  by blast
  8.1059 +
  8.1060 +lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
  8.1061 +  by blast
  8.1062 +
  8.1063 +lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
  8.1064 +  by auto
  8.1065 +
  8.1066 +lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
  8.1067 +  by blast
  8.1068 +
  8.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)"
  8.1070 +  by blast
  8.1071 +
  8.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)"
  8.1073 +  by blast
  8.1074 +
  8.1075 +lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
  8.1076 +  by blast
  8.1077 +
  8.1078 +lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
  8.1079 +  by blast
  8.1080 +
  8.1081 +lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
  8.1082 +  by auto
  8.1083 +
  8.1084 +lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
  8.1085 +  by blast
  8.1086 +
  8.1087 +lemma UNION_empty_conv[simp]:
  8.1088 +  "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
  8.1089 +  "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
  8.1090 +by blast+
  8.1091 +
  8.1092 +lemma Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
  8.1093 +  by blast
  8.1094 +
  8.1095 +lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
  8.1096 +  by blast
  8.1097 +
  8.1098 +lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) = (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
  8.1099 +  by blast
  8.1100 +
  8.1101 +lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
  8.1102 +  by (auto simp add: split_if_mem2)
  8.1103 +
  8.1104 +lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True \<union> A False)"
  8.1105 +  by (auto intro: bool_contrapos)
  8.1106 +
  8.1107 +lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)"
  8.1108 +  by blast
  8.1109 +
  8.1110 +lemma UN_mono:
  8.1111 +  "A \<subseteq> B ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
  8.1112 +    (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
  8.1113 +  by (blast dest: subsetD)
  8.1114 +
  8.1115 +lemma vimage_Union: "f -` (Union A) = (UN X:A. f -` X)"
  8.1116 +  by blast
  8.1117 +
  8.1118 +lemma vimage_UN: "f-`(UN x:A. B x) = (UN x:A. f -` B x)"
  8.1119 +  by blast
  8.1120 +
  8.1121 +lemma vimage_eq_UN: "f-`B = (UN y: B. f-`{y})"
  8.1122 +  -- {* NOT suitable for rewriting *}
  8.1123 +  by blast
  8.1124 +
  8.1125 +lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"
  8.1126 +by blast
  8.1127 +
  8.1128  
  8.1129  subsubsection {* Inter *}
  8.1130  
  8.1131  definition Inter :: "'a set set \<Rightarrow> 'a set" where
  8.1132 -  Inter_eq [code del]: "Inter A = {x. \<forall>B \<in> A. x \<in> B}"
  8.1133 -
  8.1134 +  Inf_set_eq [symmetric]: "Inter S = \<Sqinter>S"
  8.1135 +  
  8.1136  notation (xsymbols)
  8.1137    Inter  ("\<Inter>_" [90] 90)
  8.1138  
  8.1139 -lemma Inf_set_eq:
  8.1140 -  "\<Sqinter>S = \<Inter>S"
  8.1141 +lemma Inter_eq [code del]:
  8.1142 +  "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
  8.1143  proof (rule set_ext)
  8.1144    fix x
  8.1145 -  have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
  8.1146 +  have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
  8.1147      by auto
  8.1148 -  then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
  8.1149 -    by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
  8.1150 +  then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
  8.1151 +    by (simp add: Inf_fun_def Inf_bool_def Inf_set_eq [symmetric]) (simp add: mem_def)
  8.1152  qed
  8.1153  
  8.1154  lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
  8.1155 @@ -1273,11 +2202,47 @@
  8.1156      @{prop "X:C"}. *}
  8.1157    by (unfold Inter_eq) blast
  8.1158  
  8.1159 +lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
  8.1160 +  by blast
  8.1161 +
  8.1162 +lemma Inter_subset:
  8.1163 +  "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
  8.1164 +  by blast
  8.1165 +
  8.1166 +lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
  8.1167 +  by (iprover intro: InterI subsetI dest: subsetD)
  8.1168 +
  8.1169 +lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
  8.1170 +  by blast
  8.1171 +
  8.1172 +lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
  8.1173 +  by blast
  8.1174 +
  8.1175 +lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
  8.1176 +  by blast
  8.1177 +
  8.1178 +lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
  8.1179 +  by blast
  8.1180 +
  8.1181 +lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
  8.1182 +  by blast
  8.1183 +
  8.1184 +lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
  8.1185 +  by blast
  8.1186 +
  8.1187 +lemma Inter_UNIV_conv [simp,noatp]:
  8.1188 +  "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
  8.1189 +  "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
  8.1190 +  by blast+
  8.1191 +
  8.1192 +lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
  8.1193 +  by blast
  8.1194 +
  8.1195  
  8.1196  subsubsection {* Intersections of families *}
  8.1197  
  8.1198  definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
  8.1199 -  INTER_eq_Inter_image: "INTER A B = \<Inter>(B`A)"
  8.1200 +  INFI_set_eq [symmetric]: "INTER S f = (INF x:S. f x)"
  8.1201  
  8.1202  syntax
  8.1203    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
  8.1204 @@ -1301,16 +2266,16 @@
  8.1205  Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} "@INTER"
  8.1206  ] *} -- {* to avoid eta-contraction of body *}
  8.1207  
  8.1208 -lemma INFI_set_eq:
  8.1209 -  "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
  8.1210 -  by (simp add: INFI_def INTER_eq_Inter_image Inf_set_eq)
  8.1211 -
  8.1212 +lemma INTER_eq_Inter_image:
  8.1213 +  "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
  8.1214 +  by (simp add: INFI_def INFI_set_eq [symmetric] Inf_set_eq)
  8.1215 +  
  8.1216  lemma Inter_def:
  8.1217 -  "Inter S = INTER S (\<lambda>x. x)"
  8.1218 +  "\<Inter>S = (\<Inter>x\<in>S. x)"
  8.1219    by (simp add: INTER_eq_Inter_image image_def)
  8.1220  
  8.1221  lemma INTER_def:
  8.1222 -  "INTER A B = {y. \<forall>x\<in>A. y \<in> B x}"
  8.1223 +  "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
  8.1224    by (auto simp add: INTER_eq_Inter_image Inter_eq)
  8.1225  
  8.1226  lemma Inter_image_eq [simp]:
  8.1227 @@ -1334,571 +2299,24 @@
  8.1228      "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"
  8.1229    by (simp add: INTER_def)
  8.1230  
  8.1231 -
  8.1232 -no_notation
  8.1233 -  less_eq  (infix "\<sqsubseteq>" 50) and
  8.1234 -  less (infix "\<sqsubset>" 50) and
  8.1235 -  inf  (infixl "\<sqinter>" 70) and
  8.1236 -  sup  (infixl "\<squnion>" 65) and
  8.1237 -  Inf  ("\<Sqinter>_" [900] 900) and
  8.1238 -  Sup  ("\<Squnion>_" [900] 900)
  8.1239 -
  8.1240 -
  8.1241 -subsection {* Further operations and lemmas *}
  8.1242 -
  8.1243 -subsubsection {* The ``proper subset'' relation *}
  8.1244 -
  8.1245 -lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
  8.1246 -  by (unfold less_le) blast
  8.1247 -
  8.1248 -lemma psubsetE [elim!,noatp]: 
  8.1249 -    "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
  8.1250 -  by (unfold less_le) blast
  8.1251 -
  8.1252 -lemma psubset_insert_iff:
  8.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)"
  8.1254 -  by (auto simp add: less_le subset_insert_iff)
  8.1255 -
  8.1256 -lemma psubset_eq: "(A \<subset> B) = (A \<subseteq> B & A \<noteq> B)"
  8.1257 -  by (simp only: less_le)
  8.1258 -
  8.1259 -lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
  8.1260 -  by (simp add: psubset_eq)
  8.1261 -
  8.1262 -lemma psubset_trans: "[| A \<subset> B; B \<subset> C |] ==> A \<subset> C"
  8.1263 -apply (unfold less_le)
  8.1264 -apply (auto dest: subset_antisym)
  8.1265 -done
  8.1266 -
  8.1267 -lemma psubsetD: "[| A \<subset> B; c \<in> A |] ==> c \<in> B"
  8.1268 -apply (unfold less_le)
  8.1269 -apply (auto dest: subsetD)
  8.1270 -done
  8.1271 -
  8.1272 -lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
  8.1273 -  by (auto simp add: psubset_eq)
  8.1274 -
  8.1275 -lemma subset_psubset_trans: "A \<subseteq> B ==> B \<subset> C ==> A \<subset> C"
  8.1276 -  by (auto simp add: psubset_eq)
  8.1277 -
  8.1278 -lemma psubset_imp_ex_mem: "A \<subset> B ==> \<exists>b. b \<in> (B - A)"
  8.1279 -  by (unfold less_le) blast
  8.1280 -
  8.1281 -lemma atomize_ball:
  8.1282 -    "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"
  8.1283 -  by (simp only: Ball_def atomize_all atomize_imp)
  8.1284 -
  8.1285 -lemmas [symmetric, rulify] = atomize_ball
  8.1286 -  and [symmetric, defn] = atomize_ball
  8.1287 -
  8.1288 -subsubsection {* Derived rules involving subsets. *}
  8.1289 -
  8.1290 -text {* @{text insert}. *}
  8.1291 -
  8.1292 -lemma subset_insertI: "B \<subseteq> insert a B"
  8.1293 -  by (rule subsetI) (erule insertI2)
  8.1294 -
  8.1295 -lemma subset_insertI2: "A \<subseteq> B \<Longrightarrow> A \<subseteq> insert b B"
  8.1296 +lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
  8.1297    by blast
  8.1298  
  8.1299 -lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
  8.1300 -  by blast
  8.1301 -
  8.1302 -
  8.1303 -text {* \medskip Big Union -- least upper bound of a set. *}
  8.1304 -
  8.1305 -lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"
  8.1306 -  by (iprover intro: subsetI UnionI)
  8.1307 -
  8.1308 -lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
  8.1309 -  by (iprover intro: subsetI elim: UnionE dest: subsetD)
  8.1310 -
  8.1311 -
  8.1312 -text {* \medskip General union. *}
  8.1313 -
  8.1314 -lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
  8.1315 +lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
  8.1316    by blast
  8.1317  
  8.1318 -lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
  8.1319 -  by (iprover intro: subsetI elim: UN_E dest: subsetD)
  8.1320 -
  8.1321 -
  8.1322 -text {* \medskip Big Intersection -- greatest lower bound of a set. *}
  8.1323 -
  8.1324 -lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
  8.1325 -  by blast
  8.1326 -
  8.1327 -lemma Inter_subset:
  8.1328 -  "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
  8.1329 -  by blast
  8.1330 -
  8.1331 -lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
  8.1332 -  by (iprover intro: InterI subsetI dest: subsetD)
  8.1333 -
  8.1334  lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
  8.1335    by blast
  8.1336  
  8.1337  lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
  8.1338    by (iprover intro: INT_I subsetI dest: subsetD)
  8.1339  
  8.1340 -
  8.1341 -text {* \medskip Finite Union -- the least upper bound of two sets. *}
  8.1342 -
  8.1343 -lemma Un_upper1: "A \<subseteq> A \<union> B"
  8.1344 -  by blast
  8.1345 -
  8.1346 -lemma Un_upper2: "B \<subseteq> A \<union> B"
  8.1347 -  by blast
  8.1348 -
  8.1349 -lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"
  8.1350 -  by blast
  8.1351 -
  8.1352 -
  8.1353 -text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}
  8.1354 -
  8.1355 -lemma Int_lower1: "A \<inter> B \<subseteq> A"
  8.1356 -  by blast
  8.1357 -
  8.1358 -lemma Int_lower2: "A \<inter> B \<subseteq> B"
  8.1359 -  by blast
  8.1360 -
  8.1361 -lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"
  8.1362 -  by blast
  8.1363 -
  8.1364 -
  8.1365 -text {* \medskip Set difference. *}
  8.1366 -
  8.1367 -lemma Diff_subset: "A - B \<subseteq> A"
  8.1368 -  by blast
  8.1369 -
  8.1370 -lemma Diff_subset_conv: "(A - B \<subseteq> C) = (A \<subseteq> B \<union> C)"
  8.1371 -by blast
  8.1372 -
  8.1373 -
  8.1374 -subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
  8.1375 -
  8.1376 -text {* @{text "{}"}. *}
  8.1377 -
  8.1378 -lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
  8.1379 -  -- {* supersedes @{text "Collect_False_empty"} *}
  8.1380 -  by auto
  8.1381 -
  8.1382 -lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
  8.1383 -  by blast
  8.1384 -
  8.1385 -lemma not_psubset_empty [iff]: "\<not> (A < {})"
  8.1386 -  by (unfold less_le) blast
  8.1387 -
  8.1388 -lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"
  8.1389 -by blast
  8.1390 -
  8.1391 -lemma empty_Collect_eq [simp]: "({} = Collect P) = (\<forall>x. \<not> P x)"
  8.1392 -by blast
  8.1393 -
  8.1394 -lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}"
  8.1395 -  by blast
  8.1396 -
  8.1397 -lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \<union> {x. Q x}"
  8.1398 -  by blast
  8.1399 -
  8.1400 -lemma Collect_imp_eq: "{x. P x --> Q x} = -{x. P x} \<union> {x. Q x}"
  8.1401 -  by blast
  8.1402 -
  8.1403 -lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
  8.1404 -  by blast
  8.1405 -
  8.1406 -lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
  8.1407 -  by blast
  8.1408 -
  8.1409 -lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
  8.1410 -  by blast
  8.1411 -
  8.1412 -lemma Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
  8.1413 -  by blast
  8.1414 -
  8.1415 -lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
  8.1416 -  by blast
  8.1417 -
  8.1418 -
  8.1419 -text {* \medskip @{text insert}. *}
  8.1420 -
  8.1421 -lemma insert_is_Un: "insert a A = {a} Un A"
  8.1422 -  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *}
  8.1423 -  by blast
  8.1424 -
  8.1425 -lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
  8.1426 -  by blast
  8.1427 -
  8.1428 -lemmas empty_not_insert = insert_not_empty [symmetric, standard]
  8.1429 -declare empty_not_insert [simp]
  8.1430 -
  8.1431 -lemma insert_absorb: "a \<in> A ==> insert a A = A"
  8.1432 -  -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}
  8.1433 -  -- {* with \emph{quadratic} running time *}
  8.1434 -  by blast
  8.1435 -
  8.1436 -lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
  8.1437 -  by blast
  8.1438 -
  8.1439 -lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"
  8.1440 -  by blast
  8.1441 -
  8.1442 -lemma insert_subset [simp]: "(insert x A \<subseteq> B) = (x \<in> B & A \<subseteq> B)"
  8.1443 -  by blast
  8.1444 -
  8.1445 -lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
  8.1446 -  -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}
  8.1447 -  apply (rule_tac x = "A - {a}" in exI, blast)
  8.1448 -  done
  8.1449 -
  8.1450 -lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}"
  8.1451 -  by auto
  8.1452 -
  8.1453 -lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
  8.1454 -  by blast
  8.1455 -
  8.1456 -lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
  8.1457 -  by blast
  8.1458 -
  8.1459 -lemma insert_disjoint [simp,noatp]:
  8.1460 - "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
  8.1461 - "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
  8.1462 -  by auto
  8.1463 -
  8.1464 -lemma disjoint_insert [simp,noatp]:
  8.1465 - "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
  8.1466 - "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
  8.1467 -  by auto
  8.1468 -
  8.1469 -text {* \medskip @{text image}. *}
  8.1470 -
  8.1471 -lemma image_empty [simp]: "f`{} = {}"
  8.1472 -  by blast
  8.1473 -
  8.1474 -lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)"
  8.1475 -  by blast
  8.1476 -
  8.1477 -lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
  8.1478 -  by auto
  8.1479 -
  8.1480 -lemma image_constant_conv: "(%x. c) ` A = (if A = {} then {} else {c})"
  8.1481 -by auto
  8.1482 -
  8.1483 -lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
  8.1484 -by blast
  8.1485 -
  8.1486 -lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
  8.1487 -by blast
  8.1488 -
  8.1489 -lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
  8.1490 -by blast
  8.1491 -
  8.1492 -lemma empty_is_image[iff]: "({} = f ` A) = (A = {})"
  8.1493 -by blast
  8.1494 -
  8.1495 -
  8.1496 -lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
  8.1497 -  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
  8.1498 -      with its implicit quantifier and conjunction.  Also image enjoys better
  8.1499 -      equational properties than does the RHS. *}
  8.1500 -  by blast
  8.1501 -
  8.1502 -lemma if_image_distrib [simp]:
  8.1503 -  "(\<lambda>x. if P x then f x else g x) ` S
  8.1504 -    = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
  8.1505 -  by (auto simp add: image_def)
  8.1506 -
  8.1507 -lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
  8.1508 -  by (simp add: image_def)
  8.1509 -
  8.1510 -
  8.1511 -text {* \medskip @{text range}. *}
  8.1512 -
  8.1513 -lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
  8.1514 -  by auto
  8.1515 -
  8.1516 -lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
  8.1517 -by (subst image_image, simp)
  8.1518 -
  8.1519 -
  8.1520 -text {* \medskip @{text Int} *}
  8.1521 -
  8.1522 -lemma Int_absorb [simp]: "A \<inter> A = A"
  8.1523 -  by blast
  8.1524 -
  8.1525 -lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
  8.1526 -  by blast
  8.1527 -
  8.1528 -lemma Int_commute: "A \<inter> B = B \<inter> A"
  8.1529 -  by blast
  8.1530 -
  8.1531 -lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
  8.1532 -  by blast
  8.1533 -
  8.1534 -lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)"
  8.1535 -  by blast
  8.1536 -
  8.1537 -lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
  8.1538 -  -- {* Intersection is an AC-operator *}
  8.1539 -
  8.1540 -lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
  8.1541 -  by blast
  8.1542 -
  8.1543 -lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
  8.1544 -  by blast
  8.1545 -
  8.1546 -lemma Int_empty_left [simp]: "{} \<inter> B = {}"
  8.1547 -  by blast
  8.1548 -
  8.1549 -lemma Int_empty_right [simp]: "A \<inter> {} = {}"
  8.1550 -  by blast
  8.1551 -
  8.1552 -lemma disjoint_eq_subset_Compl: "(A \<inter> B = {}) = (A \<subseteq> -B)"
  8.1553 -  by blast
  8.1554 -
  8.1555 -lemma disjoint_iff_not_equal: "(A \<inter> B = {}) = (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
  8.1556 -  by blast
  8.1557 -
  8.1558 -lemma Int_UNIV_left [simp]: "UNIV \<inter> B = B"
  8.1559 -  by blast
  8.1560 -
  8.1561 -lemma Int_UNIV_right [simp]: "A \<inter> UNIV = A"
  8.1562 -  by blast
  8.1563 -
  8.1564 -lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
  8.1565 -  by blast
  8.1566 -
  8.1567 -lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
  8.1568 -  by blast
  8.1569 -
  8.1570 -lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
  8.1571 -  by blast
  8.1572 -
  8.1573 -lemma Int_UNIV [simp,noatp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
  8.1574 -  by blast
  8.1575 -
  8.1576 -lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
  8.1577 -  by blast
  8.1578 -
  8.1579 -lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
  8.1580 -  by blast
  8.1581 -
  8.1582 -
  8.1583 -text {* \medskip @{text Un}. *}
  8.1584 -
  8.1585 -lemma Un_absorb [simp]: "A \<union> A = A"
  8.1586 -  by blast
  8.1587 -
  8.1588 -lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
  8.1589 -  by blast
  8.1590 -
  8.1591 -lemma Un_commute: "A \<union> B = B \<union> A"
  8.1592 -  by blast
  8.1593 -
  8.1594 -lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
  8.1595 -  by blast
  8.1596 -
  8.1597 -lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)"
  8.1598 -  by blast
  8.1599 -
  8.1600 -lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
  8.1601 -  -- {* Union is an AC-operator *}
  8.1602 -
  8.1603 -lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
  8.1604 -  by blast
  8.1605 -
  8.1606 -lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
  8.1607 -  by blast
  8.1608 -
  8.1609 -lemma Un_empty_left [simp]: "{} \<union> B = B"
  8.1610 -  by blast
  8.1611 -
  8.1612 -lemma Un_empty_right [simp]: "A \<union> {} = A"
  8.1613 -  by blast
  8.1614 -
  8.1615 -lemma Un_UNIV_left [simp]: "UNIV \<union> B = UNIV"
  8.1616 -  by blast
  8.1617 -
  8.1618 -lemma Un_UNIV_right [simp]: "A \<union> UNIV = UNIV"
  8.1619 -  by blast
  8.1620 -
  8.1621 -lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
  8.1622 -  by blast
  8.1623 -
  8.1624 -lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"
  8.1625 -  by blast
  8.1626 -
  8.1627 -lemma Un_insert_right [simp]: "A \<union> (insert a B) = insert a (A \<union> B)"
  8.1628 -  by blast
  8.1629 -
  8.1630 -lemma Int_insert_left:
  8.1631 -    "(insert a B) Int C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"
  8.1632 -  by auto
  8.1633 -
  8.1634 -lemma Int_insert_right:
  8.1635 -    "A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"
  8.1636 -  by auto
  8.1637 -
  8.1638 -lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
  8.1639 -  by blast
  8.1640 -
  8.1641 -lemma Un_Int_distrib2: "(B \<inter> C) \<union> A = (B \<union> A) \<inter> (C \<union> A)"
  8.1642 -  by blast
  8.1643 -
  8.1644 -lemma Un_Int_crazy:
  8.1645 -    "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
  8.1646 -  by blast
  8.1647 -
  8.1648 -lemma subset_Un_eq: "(A \<subseteq> B) = (A \<union> B = B)"
  8.1649 -  by blast
  8.1650 -
  8.1651 -lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
  8.1652 -  by blast
  8.1653 -
  8.1654 -lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
  8.1655 -  by blast
  8.1656 -
  8.1657 -lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
  8.1658 -  by blast
  8.1659 -
  8.1660 -lemma Diff_Int2: "A \<inter> C - B \<inter> C = A \<inter> C - B"
  8.1661 -  by blast
  8.1662 -
  8.1663 -
  8.1664 -text {* \medskip Set complement *}
  8.1665 -
  8.1666 -lemma Compl_disjoint [simp]: "A \<inter> -A = {}"
  8.1667 -  by blast
  8.1668 -
  8.1669 -lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"
  8.1670 -  by blast
  8.1671 -
  8.1672 -lemma Compl_partition: "A \<union> -A = UNIV"
  8.1673 -  by blast
  8.1674 -
  8.1675 -lemma Compl_partition2: "-A \<union> A = UNIV"
  8.1676 -  by blast
  8.1677 -
  8.1678 -lemma double_complement [simp]: "- (-A) = (A::'a set)"
  8.1679 -  by blast
  8.1680 -
  8.1681 -lemma Compl_Un [simp]: "-(A \<union> B) = (-A) \<inter> (-B)"
  8.1682 -  by blast
  8.1683 -
  8.1684 -lemma Compl_Int [simp]: "-(A \<inter> B) = (-A) \<union> (-B)"
  8.1685 -  by blast
  8.1686 -
  8.1687 -lemma Compl_UN [simp]: "-(\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
  8.1688 -  by blast
  8.1689 -
  8.1690 -lemma Compl_INT [simp]: "-(\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
  8.1691 -  by blast
  8.1692 -
  8.1693 -lemma subset_Compl_self_eq: "(A \<subseteq> -A) = (A = {})"
  8.1694 -  by blast
  8.1695 -
  8.1696 -lemma Un_Int_assoc_eq: "((A \<inter> B) \<union> C = A \<inter> (B \<union> C)) = (C \<subseteq> A)"
  8.1697 -  -- {* Halmos, Naive Set Theory, page 16. *}
  8.1698 -  by blast
  8.1699 -
  8.1700 -lemma Compl_UNIV_eq [simp]: "-UNIV = {}"
  8.1701 -  by blast
  8.1702 -
  8.1703 -lemma Compl_empty_eq [simp]: "-{} = UNIV"
  8.1704 -  by blast
  8.1705 -
  8.1706 -lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
  8.1707 -  by blast
  8.1708 -
  8.1709 -lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
  8.1710 -  by blast
  8.1711 -
  8.1712 -
  8.1713 -text {* \medskip @{text Union}. *}
  8.1714 -
  8.1715 -lemma Union_empty [simp]: "Union({}) = {}"
  8.1716 -  by blast
  8.1717 -
  8.1718 -lemma Union_UNIV [simp]: "Union UNIV = UNIV"
  8.1719 -  by blast
  8.1720 -
  8.1721 -lemma Union_insert [simp]: "Union (insert a B) = a \<union> \<Union>B"
  8.1722 -  by blast
  8.1723 -
  8.1724 -lemma Union_Un_distrib [simp]: "\<Union>(A Un B) = \<Union>A \<union> \<Union>B"
  8.1725 -  by blast
  8.1726 -
  8.1727 -lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
  8.1728 -  by blast
  8.1729 -
  8.1730 -lemma Union_empty_conv [simp,noatp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
  8.1731 -  by blast
  8.1732 -
  8.1733 -lemma empty_Union_conv [simp,noatp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
  8.1734 -  by blast
  8.1735 -
  8.1736 -lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
  8.1737 -  by blast
  8.1738 -
  8.1739 -
  8.1740 -text {* \medskip @{text Inter}. *}
  8.1741 -
  8.1742 -lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
  8.1743 -  by blast
  8.1744 -
  8.1745 -lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
  8.1746 -  by blast
  8.1747 -
  8.1748 -lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
  8.1749 -  by blast
  8.1750 -
  8.1751 -lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
  8.1752 -  by blast
  8.1753 -
  8.1754 -lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
  8.1755 -  by blast
  8.1756 -
  8.1757 -lemma Inter_UNIV_conv [simp,noatp]:
  8.1758 -  "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
  8.1759 -  "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
  8.1760 -  by blast+
  8.1761 -
  8.1762 -
  8.1763 -text {*
  8.1764 -  \medskip @{text UN} and @{text INT}.
  8.1765 -
  8.1766 -  Basic identities: *}
  8.1767 -
  8.1768 -lemma UN_empty [simp,noatp]: "(\<Union>x\<in>{}. B x) = {}"
  8.1769 -  by blast
  8.1770 -
  8.1771 -lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
  8.1772 -  by blast
  8.1773 -
  8.1774 -lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
  8.1775 -  by blast
  8.1776 -
  8.1777 -lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
  8.1778 -  by auto
  8.1779 -
  8.1780  lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
  8.1781    by blast
  8.1782  
  8.1783  lemma INT_absorb: "k \<in> I ==> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
  8.1784    by blast
  8.1785  
  8.1786 -lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
  8.1787 -  by blast
  8.1788 -
  8.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)"
  8.1790 -  by blast
  8.1791 -
  8.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)"
  8.1793 -  by blast
  8.1794 -
  8.1795 -lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
  8.1796 -  by blast
  8.1797 -
  8.1798  lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
  8.1799    by blast
  8.1800  
  8.1801 @@ -1912,34 +2330,35 @@
  8.1802      "u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
  8.1803    by blast
  8.1804  
  8.1805 -lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
  8.1806 -  by blast
  8.1807 -
  8.1808 -lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
  8.1809 -  by auto
  8.1810 -
  8.1811  lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
  8.1812    by auto
  8.1813  
  8.1814 -lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
  8.1815 -  by blast
  8.1816 -
  8.1817  lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
  8.1818    -- {* Look: it has an \emph{existential} quantifier *}
  8.1819    by blast
  8.1820  
  8.1821 -lemma UNION_empty_conv[simp]:
  8.1822 -  "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
  8.1823 -  "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
  8.1824 -by blast+
  8.1825 -
  8.1826  lemma INTER_UNIV_conv[simp]:
  8.1827   "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
  8.1828   "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
  8.1829  by blast+
  8.1830  
  8.1831 -
  8.1832 -text {* \medskip Distributive laws: *}
  8.1833 +lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"
  8.1834 +  by (auto intro: bool_induct)
  8.1835 +
  8.1836 +lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
  8.1837 +  by blast
  8.1838 +
  8.1839 +lemma INT_anti_mono:
  8.1840 +  "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
  8.1841 +    (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
  8.1842 +  -- {* The last inclusion is POSITIVE! *}
  8.1843 +  by (blast dest: subsetD)
  8.1844 +
  8.1845 +lemma vimage_INT: "f-`(INT x:A. B x) = (INT x:A. f -` B x)"
  8.1846 +  by blast
  8.1847 +
  8.1848 +
  8.1849 +subsubsection {* Distributive laws *}
  8.1850  
  8.1851  lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
  8.1852    by blast
  8.1853 @@ -1980,192 +2399,16 @@
  8.1854    by blast
  8.1855  
  8.1856  
  8.1857 -text {* \medskip Bounded quantifiers.
  8.1858 -
  8.1859 -  The following are not added to the default simpset because
  8.1860 -  (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}
  8.1861 -
  8.1862 -lemma ball_Un: "(\<forall>x \<in> A \<union> B. P x) = ((\<forall>x\<in>A. P x) & (\<forall>x\<in>B. P x))"
  8.1863 -  by blast
  8.1864 -
  8.1865 -lemma bex_Un: "(\<exists>x \<in> A \<union> B. P x) = ((\<exists>x\<in>A. P x) | (\<exists>x\<in>B. P x))"
  8.1866 -  by blast
  8.1867 -
  8.1868 -lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
  8.1869 -  by blast
  8.1870 -
  8.1871 -lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) = (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
  8.1872 -  by blast
  8.1873 -
  8.1874 -
  8.1875 -text {* \medskip Set difference. *}
  8.1876 -
  8.1877 -lemma Diff_eq: "A - B = A \<inter> (-B)"
  8.1878 -  by blast
  8.1879 -
  8.1880 -lemma Diff_eq_empty_iff [simp,noatp]: "(A - B = {}) = (A \<subseteq> B)"
  8.1881 -  by blast
  8.1882 -
  8.1883 -lemma Diff_cancel [simp]: "A - A = {}"
  8.1884 -  by blast
  8.1885 -
  8.1886 -lemma Diff_idemp [simp]: "(A - B) - B = A - (B::'a set)"
  8.1887 -by blast
  8.1888 -
  8.1889 -lemma Diff_triv: "A \<inter> B = {} ==> A - B = A"
  8.1890 -  by (blast elim: equalityE)
  8.1891 -
  8.1892 -lemma empty_Diff [simp]: "{} - A = {}"
  8.1893 -  by blast
  8.1894 -
  8.1895 -lemma Diff_empty [simp]: "A - {} = A"
  8.1896 -  by blast
  8.1897 -
  8.1898 -lemma Diff_UNIV [simp]: "A - UNIV = {}"
  8.1899 -  by blast
  8.1900 -
  8.1901 -lemma Diff_insert0 [simp,noatp]: "x \<notin> A ==> A - insert x B = A - B"
  8.1902 -  by blast
  8.1903 -
  8.1904 -lemma Diff_insert: "A - insert a B = A - B - {a}"
  8.1905 -  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
  8.1906 -  by blast
  8.1907 -
  8.1908 -lemma Diff_insert2: "A - insert a B = A - {a} - B"
  8.1909 -  -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
  8.1910 -  by blast
  8.1911 -
  8.1912 -lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))"
  8.1913 -  by auto
  8.1914 -
  8.1915 -lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B"
  8.1916 -  by blast
  8.1917 -
  8.1918 -lemma insert_Diff_single[simp]: "insert a (A - {a}) = insert a A"
  8.1919 -by blast
  8.1920 -
  8.1921 -lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A"
  8.1922 -  by blast
  8.1923 -
  8.1924 -lemma Diff_insert_absorb: "x \<notin> A ==> (insert x A) - {x} = A"
  8.1925 -  by auto
  8.1926 -
  8.1927 -lemma Diff_disjoint [simp]: "A \<inter> (B - A) = {}"
  8.1928 -  by blast
  8.1929 -
  8.1930 -lemma Diff_partition: "A \<subseteq> B ==> A \<union> (B - A) = B"
  8.1931 -  by blast
  8.1932 -
  8.1933 -lemma double_diff: "A \<subseteq> B ==> B \<subseteq> C ==> B - (C - A) = A"
  8.1934 -  by blast
  8.1935 -
  8.1936 -lemma Un_Diff_cancel [simp]: "A \<union> (B - A) = A \<union> B"
  8.1937 -  by blast
  8.1938 -
  8.1939 -lemma Un_Diff_cancel2 [simp]: "(B - A) \<union> A = B \<union> A"
  8.1940 -  by blast
  8.1941 -
  8.1942 -lemma Diff_Un: "A - (B \<union> C) = (A - B) \<inter> (A - C)"
  8.1943 -  by blast
  8.1944 -
  8.1945 -lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"
  8.1946 -  by blast
  8.1947 -
  8.1948 -lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
  8.1949 +subsubsection {* Complement *}
  8.1950 +
  8.1951 +lemma Compl_UN [simp]: "-(\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
  8.1952    by blast
  8.1953  
  8.1954 -lemma Int_Diff: "(A \<inter> B) - C = A \<inter> (B - C)"
  8.1955 -  by blast
  8.1956 -
  8.1957 -lemma Diff_Int_distrib: "C \<inter> (A - B) = (C \<inter> A) - (C \<inter> B)"
  8.1958 -  by blast
  8.1959 -
  8.1960 -lemma Diff_Int_distrib2: "(A - B) \<inter> C = (A \<inter> C) - (B \<inter> C)"
  8.1961 -  by blast
  8.1962 -
  8.1963 -lemma Diff_Compl [simp]: "A - (- B) = A \<inter> B"
  8.1964 -  by auto
  8.1965 -
  8.1966 -lemma Compl_Diff_eq [simp]: "- (A - B) = -A \<union> B"
  8.1967 +lemma Compl_INT [simp]: "-(\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
  8.1968    by blast
  8.1969  
  8.1970  
  8.1971 -text {* \medskip Quantification over type @{typ bool}. *}
  8.1972 -
  8.1973 -lemma bool_induct: "P True \<Longrightarrow> P False \<Longrightarrow> P x"
  8.1974 -  by (cases x) auto
  8.1975 -
  8.1976 -lemma all_bool_eq: "(\<forall>b. P b) \<longleftrightarrow> P True \<and> P False"
  8.1977 -  by (auto intro: bool_induct)
  8.1978 -
  8.1979 -lemma bool_contrapos: "P x \<Longrightarrow> \<not> P False \<Longrightarrow> P True"
  8.1980 -  by (cases x) auto
  8.1981 -
  8.1982 -lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
  8.1983 -  by (auto intro: bool_contrapos)
  8.1984 -
  8.1985 -lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
  8.1986 -  by (auto simp add: split_if_mem2)
  8.1987 -
  8.1988 -lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True \<union> A False)"
  8.1989 -  by (auto intro: bool_contrapos)
  8.1990 -
  8.1991 -lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"
  8.1992 -  by (auto intro: bool_induct)
  8.1993 -
  8.1994 -text {* \medskip @{text Pow} *}
  8.1995 -
  8.1996 -lemma Pow_empty [simp]: "Pow {} = {{}}"
  8.1997 -  by (auto simp add: Pow_def)
  8.1998 -
  8.1999 -lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
  8.2000 -  by (blast intro: image_eqI [where ?x = "u - {a}", standard])
  8.2001 -
  8.2002 -lemma Pow_Compl: "Pow (- A) = {-B | B. A \<in> Pow B}"
  8.2003 -  by (blast intro: exI [where ?x = "- u", standard])
  8.2004 -
  8.2005 -lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
  8.2006 -  by blast
  8.2007 -
  8.2008 -lemma Un_Pow_subset: "Pow A \<union> Pow B \<subseteq> Pow (A \<union> B)"
  8.2009 -  by blast
  8.2010 -
  8.2011 -lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)"
  8.2012 -  by blast
  8.2013 -
  8.2014 -lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
  8.2015 -  by blast
  8.2016 -
  8.2017 -lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A"
  8.2018 -  by blast
  8.2019 -
  8.2020 -lemma Pow_Int_eq [simp]: "Pow (A \<inter> B) = Pow A \<inter> Pow B"
  8.2021 -  by blast
  8.2022 -
  8.2023 -lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
  8.2024 -  by blast
  8.2025 -
  8.2026 -
  8.2027 -text {* \medskip Miscellany. *}
  8.2028 -
  8.2029 -lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
  8.2030 -  by blast
  8.2031 -
  8.2032 -lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
  8.2033 -  by blast
  8.2034 -
  8.2035 -lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
  8.2036 -  by (unfold less_le) blast
  8.2037 -
  8.2038 -lemma all_not_in_conv [simp]: "(\<forall>x. x \<notin> A) = (A = {})"
  8.2039 -  by blast
  8.2040 -
  8.2041 -lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
  8.2042 -  by blast
  8.2043 -
  8.2044 -lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
  8.2045 -  by iprover
  8.2046 -
  8.2047 +subsubsection {* Miniscoping and maxiscoping *}
  8.2048  
  8.2049  text {* \medskip Miniscoping: pushing in quantifiers and big Unions
  8.2050             and Intersections. *}
  8.2051 @@ -2262,284 +2505,17 @@
  8.2052    by auto
  8.2053  
  8.2054  
  8.2055 -subsubsection {* Monotonicity of various operations *}
  8.2056 -
  8.2057 -lemma image_mono: "A \<subseteq> B ==> f`A \<subseteq> f`B"
  8.2058 -  by blast
  8.2059 -
  8.2060 -lemma Pow_mono: "A \<subseteq> B ==> Pow A \<subseteq> Pow B"
  8.2061 -  by blast
  8.2062 -
  8.2063 -lemma Union_mono: "A \<subseteq> B ==> \<Union>A \<subseteq> \<Union>B"
  8.2064 -  by blast
  8.2065 -
  8.2066 -lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
  8.2067 -  by blast
  8.2068 -
  8.2069 -lemma UN_mono:
  8.2070 -  "A \<subseteq> B ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
  8.2071 -    (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
  8.2072 -  by (blast dest: subsetD)
  8.2073 -
  8.2074 -lemma INT_anti_mono:
  8.2075 -  "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
  8.2076 -    (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
  8.2077 -  -- {* The last inclusion is POSITIVE! *}
  8.2078 -  by (blast dest: subsetD)
  8.2079 -
  8.2080 -lemma insert_mono: "C \<subseteq> D ==> insert a C \<subseteq> insert a D"
  8.2081 -  by blast
  8.2082 -
  8.2083 -lemma Un_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<union> B \<subseteq> C \<union> D"
  8.2084 -  by blast
  8.2085 -
  8.2086 -lemma Int_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<inter> B \<subseteq> C \<inter> D"
  8.2087 -  by blast
  8.2088 -
  8.2089 -lemma Diff_mono: "A \<subseteq> C ==> D \<subseteq> B ==> A - B \<subseteq> C - D"
  8.2090 -  by blast
  8.2091 -
  8.2092 -lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"
  8.2093 -  by blast
  8.2094 -
  8.2095 -text {* \medskip Monotonicity of implications. *}
  8.2096 -
  8.2097 -lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B"
  8.2098 -  apply (rule impI)
  8.2099 -  apply (erule subsetD, assumption)
  8.2100 -  done
  8.2101 -
  8.2102 -lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
  8.2103 -  by iprover
  8.2104 -
  8.2105 -lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"
  8.2106 -  by iprover
  8.2107 -
  8.2108 -lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"
  8.2109 -  by iprover
  8.2110 -
  8.2111 -lemma imp_refl: "P --> P" ..
  8.2112 -
  8.2113 -lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
  8.2114 -  by iprover
  8.2115 -
  8.2116 -lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"
  8.2117 -  by iprover
  8.2118 -
  8.2119 -lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \<subseteq> Collect Q"
  8.2120 -  by blast
  8.2121 -
  8.2122 -lemma Int_Collect_mono:
  8.2123 -    "A \<subseteq> B ==> (!!x. x \<in> A ==> P x --> Q x) ==> A \<inter> Collect P \<subseteq> B \<inter> Collect Q"
  8.2124 -  by blast
  8.2125 -
  8.2126 -lemmas basic_monos =
  8.2127 -  subset_refl imp_refl disj_mono conj_mono
  8.2128 -  ex_mono Collect_mono in_mono
  8.2129 -
  8.2130 -lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
  8.2131 -  by iprover
  8.2132 -
  8.2133 -lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
  8.2134 -  by iprover
  8.2135 -
  8.2136 -
  8.2137 -subsubsection {* Inverse image of a function *}
  8.2138 -
  8.2139 -constdefs
  8.2140 -  vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
  8.2141 -  [code del]: "f -` B == {x. f x : B}"
  8.2142 -
  8.2143 -lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
  8.2144 -  by (unfold vimage_def) blast
  8.2145 -
  8.2146 -lemma vimage_singleton_eq: "(a : f -` {b}) = (f a = b)"
  8.2147 -  by simp
  8.2148 -
  8.2149 -lemma vimageI [intro]: "f a = b ==> b:B ==> a : f -` B"
  8.2150 -  by (unfold vimage_def) blast
  8.2151 -
  8.2152 -lemma vimageI2: "f a : A ==> a : f -` A"
  8.2153 -  by (unfold vimage_def) fast
  8.2154 -
  8.2155 -lemma vimageE [elim!]: "a: f -` B ==> (!!x. f a = x ==> x:B ==> P) ==> P"
  8.2156 -  by (unfold vimage_def) blast
  8.2157 -
  8.2158 -lemma vimageD: "a : f -` A ==> f a : A"
  8.2159 -  by (unfold vimage_def) fast
  8.2160 -
  8.2161 -lemma vimage_empty [simp]: "f -` {} = {}"
  8.2162 -  by blast
  8.2163 -
  8.2164 -lemma vimage_Compl: "f -` (-A) = -(f -` A)"
  8.2165 -  by blast
  8.2166 -
  8.2167 -lemma vimage_Un [simp]: "f -` (A Un B) = (f -` A) Un (f -` B)"
  8.2168 -  by blast
  8.2169 -
  8.2170 -lemma vimage_Int [simp]: "f -` (A Int B) = (f -` A) Int (f -` B)"
  8.2171 -  by fast
  8.2172 -
  8.2173 -lemma vimage_Union: "f -` (Union A) = (UN X:A. f -` X)"
  8.2174 -  by blast
  8.2175 -
  8.2176 -lemma vimage_UN: "f-`(UN x:A. B x) = (UN x:A. f -` B x)"
  8.2177 -  by blast
  8.2178 -
  8.2179 -lemma vimage_INT: "f-`(INT x:A. B x) = (INT x:A. f -` B x)"
  8.2180 -  by blast
  8.2181 -
  8.2182 -lemma vimage_Collect_eq [simp]: "f -` Collect P = {y. P (f y)}"
  8.2183 -  by blast
  8.2184 -
  8.2185 -lemma vimage_Collect: "(!!x. P (f x) = Q x) ==> f -` (Collect P) = Collect Q"
  8.2186 -  by blast
  8.2187 -
  8.2188 -lemma vimage_insert: "f-`(insert a B) = (f-`{a}) Un (f-`B)"
  8.2189 -  -- {* NOT suitable for rewriting because of the recurrence of @{term "{a}"}. *}
  8.2190 -  by blast
  8.2191 -
  8.2192 -lemma vimage_Diff: "f -` (A - B) = (f -` A) - (f -` B)"
  8.2193 -  by blast
  8.2194 -
  8.2195 -lemma vimage_UNIV [simp]: "f -` UNIV = UNIV"
  8.2196 -  by blast
  8.2197 -
  8.2198 -lemma vimage_eq_UN: "f-`B = (UN y: B. f-`{y})"
  8.2199 -  -- {* NOT suitable for rewriting *}
  8.2200 -  by blast
  8.2201 -
  8.2202 -lemma vimage_mono: "A \<subseteq> B ==> f -` A \<subseteq> f -` B"
  8.2203 -  -- {* monotonicity *}
  8.2204 -  by blast
  8.2205 -
  8.2206 -lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
  8.2207 -by (blast intro: sym)
  8.2208 -
  8.2209 -lemma image_vimage_subset: "f ` (f -` A) <= A"
  8.2210 -by blast
  8.2211 -
  8.2212 -lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
  8.2213 -by blast
  8.2214 -
  8.2215 -lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
  8.2216 -by blast
  8.2217 -
  8.2218 -lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
  8.2219 -by blast
  8.2220 -
  8.2221 -lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"
  8.2222 -by blast
  8.2223 -
  8.2224 -
  8.2225 -subsubsection {* Getting the Contents of a Singleton Set *}
  8.2226 -
  8.2227 -definition contents :: "'a set \<Rightarrow> 'a" where
  8.2228 -  [code del]: "contents X = (THE x. X = {x})"
  8.2229 -
  8.2230 -lemma contents_eq [simp]: "contents {x} = x"
  8.2231 -  by (simp add: contents_def)
  8.2232 -
  8.2233 -
  8.2234 -subsubsection {* Least value operator *}
  8.2235 -
  8.2236 -lemma Least_mono:
  8.2237 -  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
  8.2238 -    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
  8.2239 -    -- {* Courtesy of Stephan Merz *}
  8.2240 -  apply clarify
  8.2241 -  apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
  8.2242 -  apply (rule LeastI2_order)
  8.2243 -  apply (auto elim: monoD intro!: order_antisym)
  8.2244 -  done
  8.2245 -
  8.2246 -subsection {* Misc *}
  8.2247 -
  8.2248 -text {* Rudimentary code generation *}
  8.2249 -
  8.2250 -lemma [code]: "{} = bot"
  8.2251 -  by (rule sym) (fact bot_set_eq)
  8.2252 -
  8.2253 -lemma [code]: "UNIV = top"
  8.2254 -  by (rule sym) (fact top_set_eq)
  8.2255 -
  8.2256 -lemma [code]: "op \<inter> = inf"
  8.2257 -  by (rule ext)+ (simp add: inf_set_eq)
  8.2258 -
  8.2259 -lemma [code]: "op \<union> = sup"
  8.2260 -  by (rule ext)+ (simp add: sup_set_eq)
  8.2261 -
  8.2262 -lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
  8.2263 -  by (auto simp add: insert_compr Collect_def mem_def)
  8.2264 -
  8.2265 -lemma vimage_code [code]: "(f -` A) x = A (f x)"
  8.2266 -  by (simp add: vimage_def Collect_def mem_def)
  8.2267 -
  8.2268 -
  8.2269 -text {* Misc theorem and ML bindings *}
  8.2270 -
  8.2271 -lemmas equalityI = subset_antisym
  8.2272 +no_notation
  8.2273 +  less_eq  (infix "\<sqsubseteq>" 50) and
  8.2274 +  less (infix "\<sqsubset>" 50) and
  8.2275 +  inf  (infixl "\<sqinter>" 70) and
  8.2276 +  sup  (infixl "\<squnion>" 65) and
  8.2277 +  Inf  ("\<Sqinter>_" [900] 900) and
  8.2278 +  Sup  ("\<Squnion>_" [900] 900)
  8.2279 +
  8.2280  lemmas mem_simps =
  8.2281    insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
  8.2282    mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
  8.2283    -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
  8.2284  
  8.2285 -ML {*
  8.2286 -val Ball_def = @{thm Ball_def}
  8.2287 -val Bex_def = @{thm Bex_def}
  8.2288 -val CollectD = @{thm CollectD}
  8.2289 -val CollectE = @{thm CollectE}
  8.2290 -val CollectI = @{thm CollectI}
  8.2291 -val Collect_conj_eq = @{thm Collect_conj_eq}
  8.2292 -val Collect_mem_eq = @{thm Collect_mem_eq}
  8.2293 -val IntD1 = @{thm IntD1}
  8.2294 -val IntD2 = @{thm IntD2}
  8.2295 -val IntE = @{thm IntE}
  8.2296 -val IntI = @{thm IntI}
  8.2297 -val Int_Collect = @{thm Int_Collect}
  8.2298 -val UNIV_I = @{thm UNIV_I}
  8.2299 -val UNIV_witness = @{thm UNIV_witness}
  8.2300 -val UnE = @{thm UnE}
  8.2301 -val UnI1 = @{thm UnI1}
  8.2302 -val UnI2 = @{thm UnI2}
  8.2303 -val ballE = @{thm ballE}
  8.2304 -val ballI = @{thm ballI}
  8.2305 -val bexCI = @{thm bexCI}
  8.2306 -val bexE = @{thm bexE}
  8.2307 -val bexI = @{thm bexI}
  8.2308 -val bex_triv = @{thm bex_triv}
  8.2309 -val bspec = @{thm bspec}
  8.2310 -val contra_subsetD = @{thm contra_subsetD}
  8.2311 -val distinct_lemma = @{thm distinct_lemma}
  8.2312 -val eq_to_mono = @{thm eq_to_mono}
  8.2313 -val eq_to_mono2 = @{thm eq_to_mono2}
  8.2314 -val equalityCE = @{thm equalityCE}
  8.2315 -val equalityD1 = @{thm equalityD1}
  8.2316 -val equalityD2 = @{thm equalityD2}
  8.2317 -val equalityE = @{thm equalityE}
  8.2318 -val equalityI = @{thm equalityI}
  8.2319 -val imageE = @{thm imageE}
  8.2320 -val imageI = @{thm imageI}
  8.2321 -val image_Un = @{thm image_Un}
  8.2322 -val image_insert = @{thm image_insert}
  8.2323 -val insert_commute = @{thm insert_commute}
  8.2324 -val insert_iff = @{thm insert_iff}
  8.2325 -val mem_Collect_eq = @{thm mem_Collect_eq}
  8.2326 -val rangeE = @{thm rangeE}
  8.2327 -val rangeI = @{thm rangeI}
  8.2328 -val range_eqI = @{thm range_eqI}
  8.2329 -val subsetCE = @{thm subsetCE}
  8.2330 -val subsetD = @{thm subsetD}
  8.2331 -val subsetI = @{thm subsetI}
  8.2332 -val subset_refl = @{thm subset_refl}
  8.2333 -val subset_trans = @{thm subset_trans}
  8.2334 -val vimageD = @{thm vimageD}
  8.2335 -val vimageE = @{thm vimageE}
  8.2336 -val vimageI = @{thm vimageI}
  8.2337 -val vimageI2 = @{thm vimageI2}
  8.2338 -val vimage_Collect = @{thm vimage_Collect}
  8.2339 -val vimage_Int = @{thm vimage_Int}
  8.2340 -val vimage_Un = @{thm vimage_Un}
  8.2341 -*}
  8.2342 -
  8.2343  end
     9.1 --- a/src/HOL/Tools/Function/fundef_lib.ML	Wed Jul 22 11:48:04 2009 +0200
     9.2 +++ b/src/HOL/Tools/Function/fundef_lib.ML	Wed Jul 22 14:21:52 2009 +0200
     9.3 @@ -167,10 +167,10 @@
     9.4   end
     9.5  
     9.6  (* instance for unions *)
     9.7 -fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Un}
     9.8 -  (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @
     9.9 -                                     @{thms "Un_empty_right"} @
    9.10 -                                     @{thms "Un_empty_left"})) t
    9.11 +fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Set.union}
    9.12 +  (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
    9.13 +                                     @{thms Un_empty_right} @
    9.14 +                                     @{thms Un_empty_left})) t
    9.15  
    9.16  
    9.17  end
    10.1 --- a/src/HOL/Tools/Function/termination.ML	Wed Jul 22 11:48:04 2009 +0200
    10.2 +++ b/src/HOL/Tools/Function/termination.ML	Wed Jul 22 14:21:52 2009 +0200
    10.3 @@ -145,7 +145,7 @@
    10.4  
    10.5  fun mk_sum_skel rel =
    10.6    let
    10.7 -    val cs = FundefLib.dest_binop_list @{const_name Un} rel
    10.8 +    val cs = FundefLib.dest_binop_list @{const_name union} rel
    10.9      fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) =
   10.10        let
   10.11          val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
   10.12 @@ -233,7 +233,7 @@
   10.13  fun CALLS tac i st =
   10.14    if Thm.no_prems st then all_tac st
   10.15    else case Thm.term_of (Thm.cprem_of st i) of
   10.16 -    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Un} rel, i) st
   10.17 +    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name union} rel, i) st
   10.18    |_ => no_tac st
   10.19  
   10.20  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
   10.21 @@ -293,7 +293,7 @@
   10.22            if null ineqs then
   10.23                Const (@{const_name Set.empty}, fastype_of rel)
   10.24            else
   10.25 -              foldr1 (HOLogic.mk_binop @{const_name Un}) (map mk_compr ineqs)
   10.26 +              foldr1 (HOLogic.mk_binop @{const_name union}) (map mk_compr ineqs)
   10.27  
   10.28        fun solve_membership_tac i =
   10.29            (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
    11.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Jul 22 11:48:04 2009 +0200
    11.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Jul 22 14:21:52 2009 +0200
    11.3 @@ -73,8 +73,8 @@
    11.4          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
    11.5            (p (fold (Logic.all o Var) vs t) f)
    11.6          end;
    11.7 -      fun mkop "op &" T x = SOME (Const (@{const_name "Int"}, T --> T --> T), x)
    11.8 -        | mkop "op |" T x = SOME (Const (@{const_name "Un"}, T --> T --> T), x)
    11.9 +      fun mkop "op &" T x = SOME (Const (@{const_name inter}, T --> T --> T), x)
   11.10 +        | mkop "op |" T x = SOME (Const (@{const_name union}, T --> T --> T), x)
   11.11          | mkop _ _ _ = NONE;
   11.12        fun mk_collect p T t =
   11.13          let val U = HOLogic.dest_setT T
    12.1 --- a/src/HOL/Tools/res_clause.ML	Wed Jul 22 11:48:04 2009 +0200
    12.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Jul 22 14:21:52 2009 +0200
    12.3 @@ -110,8 +110,8 @@
    12.4                     (@{const_name "op -->"}, "implies"),
    12.5                     (@{const_name Set.empty}, "emptyset"),
    12.6                     (@{const_name "op :"}, "in"),
    12.7 -                   (@{const_name Un}, "union"),
    12.8 -                   (@{const_name Int}, "inter"),
    12.9 +                   (@{const_name union}, "union"),
   12.10 +                   (@{const_name inter}, "inter"),
   12.11                     ("List.append", "append"),
   12.12                     ("ATP_Linkup.fequal", "fequal"),
   12.13                     ("ATP_Linkup.COMBI", "COMBI"),
    13.1 --- a/src/HOL/ex/Meson_Test.thy	Wed Jul 22 11:48:04 2009 +0200
    13.2 +++ b/src/HOL/ex/Meson_Test.thy	Wed Jul 22 14:21:52 2009 +0200
    13.3 @@ -1,4 +1,3 @@
    13.4 -(*ID:         $Id$*)
    13.5  
    13.6  header {* Meson test cases *}
    13.7  
    13.8 @@ -11,7 +10,7 @@
    13.9    below and constants declared in HOL!
   13.10  *}
   13.11  
   13.12 -hide const subset member quotient
   13.13 +hide (open) const subset member quotient union inter
   13.14  
   13.15  text {*
   13.16    Test data for the MESON proof procedure