src/HOL/Complete_Lattice.thy
 author haftmann Wed Sep 16 13:43:05 2009 +0200 (2009-09-16) changeset 32587 caa5ada96a00 parent 32436 10cd49e0c067 child 32606 b5c3a8a75772 permissions -rw-r--r--
Inter and Union are mere abbreviations for Inf and Sup
 haftmann@32139  1 (* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)  wenzelm@11979  2 haftmann@32139  3 header {* Complete lattices, with special focus on sets *}  haftmann@32077  4 haftmann@32139  5 theory Complete_Lattice  haftmann@32139  6 imports Set  haftmann@32139  7 begin  haftmann@32077  8 haftmann@32077  9 notation  haftmann@32077  10  less_eq (infix "\" 50) and  haftmann@32077  11  less (infix "\" 50) and  haftmann@32077  12  inf (infixl "\" 70) and  haftmann@32077  13  sup (infixl "\" 65)  haftmann@32077  14 haftmann@32139  15 haftmann@32139  16 subsection {* Abstract complete lattices *}  haftmann@32139  17 haftmann@32077  18 class complete_lattice = lattice + bot + top +  haftmann@32077  19  fixes Inf :: "'a set \ 'a" ("\_" [900] 900)  haftmann@32077  20  and Sup :: "'a set \ 'a" ("\_" [900] 900)  haftmann@32077  21  assumes Inf_lower: "x \ A \ \A \ x"  haftmann@32077  22  and Inf_greatest: "(\x. x \ A \ z \ x) \ z \ \A"  haftmann@32077  23  assumes Sup_upper: "x \ A \ x \ \A"  haftmann@32077  24  and Sup_least: "(\x. x \ A \ x \ z) \ \A \ z"  haftmann@32077  25 begin  haftmann@32077  26 haftmann@32077  27 lemma Inf_Sup: "\A = \{b. \a \ A. b \ a}"  haftmann@32077  28  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)  haftmann@32077  29 haftmann@32077  30 lemma Sup_Inf: "\A = \{b. \a \ A. a \ b}"  haftmann@32077  31  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)  haftmann@32077  32 haftmann@32077  33 lemma Inf_Univ: "\UNIV = \{}"  haftmann@32135  34  unfolding Sup_Inf by auto  haftmann@32077  35 haftmann@32077  36 lemma Sup_Univ: "\UNIV = \{}"  haftmann@32135  37  unfolding Inf_Sup by auto  haftmann@32077  38 haftmann@32077  39 lemma Inf_insert: "\insert a A = a \ \A"  haftmann@32077  40  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)  haftmann@32077  41 haftmann@32077  42 lemma Sup_insert: "\insert a A = a \ \A"  haftmann@32077  43  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)  haftmann@32077  44 haftmann@32077  45 lemma Inf_singleton [simp]:  haftmann@32077  46  "\{a} = a"  haftmann@32077  47  by (auto intro: antisym Inf_lower Inf_greatest)  haftmann@32077  48 haftmann@32077  49 lemma Sup_singleton [simp]:  haftmann@32077  50  "\{a} = a"  haftmann@32077  51  by (auto intro: antisym Sup_upper Sup_least)  haftmann@32077  52 haftmann@32077  53 lemma Inf_insert_simp:  haftmann@32077  54  "\insert a A = (if A = {} then a else a \ \A)"  haftmann@32077  55  by (cases "A = {}") (simp_all, simp add: Inf_insert)  haftmann@32077  56 haftmann@32077  57 lemma Sup_insert_simp:  haftmann@32077  58  "\insert a A = (if A = {} then a else a \ \A)"  haftmann@32077  59  by (cases "A = {}") (simp_all, simp add: Sup_insert)  haftmann@32077  60 haftmann@32077  61 lemma Inf_binary:  haftmann@32077  62  "\{a, b} = a \ b"  haftmann@32077  63  by (auto simp add: Inf_insert_simp)  haftmann@32077  64 haftmann@32077  65 lemma Sup_binary:  haftmann@32077  66  "\{a, b} = a \ b"  haftmann@32077  67  by (auto simp add: Sup_insert_simp)  haftmann@32077  68 haftmann@32077  69 lemma bot_def:  haftmann@32077  70  "bot = \{}"  haftmann@32077  71  by (auto intro: antisym Sup_least)  haftmann@32077  72 haftmann@32077  73 lemma top_def:  haftmann@32077  74  "top = \{}"  haftmann@32077  75  by (auto intro: antisym Inf_greatest)  haftmann@32077  76 haftmann@32077  77 lemma sup_bot [simp]:  haftmann@32077  78  "x \ bot = x"  nipkow@32436  79  using bot_least [of x] by (simp add: sup_commute)  haftmann@32077  80 haftmann@32077  81 lemma inf_top [simp]:  haftmann@32077  82  "x \ top = x"  nipkow@32436  83  using top_greatest [of x] by (simp add: inf_commute)  haftmann@32077  84 haftmann@32077  85 definition SUPR :: "'b set \ ('b \ 'a) \ 'a" where  haftmann@32117  86  "SUPR A f = \ (f  A)"  haftmann@32077  87 haftmann@32077  88 definition INFI :: "'b set \ ('b \ 'a) \ 'a" where  haftmann@32117  89  "INFI A f = \ (f  A)"  haftmann@32077  90 haftmann@32077  91 end  haftmann@32077  92 haftmann@32077  93 syntax  haftmann@32077  94  "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10)  haftmann@32077  95  "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 10] 10)  haftmann@32077  96  "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10)  haftmann@32077  97  "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 10] 10)  haftmann@32077  98 haftmann@32077  99 translations  haftmann@32077  100  "SUP x y. B" == "SUP x. SUP y. B"  haftmann@32077  101  "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)"  haftmann@32077  102  "SUP x. B" == "SUP x:CONST UNIV. B"  haftmann@32077  103  "SUP x:A. B" == "CONST SUPR A (%x. B)"  haftmann@32077  104  "INF x y. B" == "INF x. INF y. B"  haftmann@32077  105  "INF x. B" == "CONST INFI CONST UNIV (%x. B)"  haftmann@32077  106  "INF x. B" == "INF x:CONST UNIV. B"  haftmann@32077  107  "INF x:A. B" == "CONST INFI A (%x. B)"  haftmann@32077  108 haftmann@32120  109 print_translation {* [  haftmann@32120  110 Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} "_SUP",  haftmann@32120  111 Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} "_INF"  haftmann@32120  112 ] *} -- {* to avoid eta-contraction of body *}  wenzelm@11979  113 haftmann@32077  114 context complete_lattice  haftmann@32077  115 begin  haftmann@32077  116 haftmann@32077  117 lemma le_SUPI: "i : A \ M i \ (SUP i:A. M i)"  haftmann@32077  118  by (auto simp add: SUPR_def intro: Sup_upper)  haftmann@32077  119 haftmann@32077  120 lemma SUP_leI: "(\i. i : A \ M i \ u) \ (SUP i:A. M i) \ u"  haftmann@32077  121  by (auto simp add: SUPR_def intro: Sup_least)  haftmann@32077  122 haftmann@32077  123 lemma INF_leI: "i : A \ (INF i:A. M i) \ M i"  haftmann@32077  124  by (auto simp add: INFI_def intro: Inf_lower)  haftmann@32077  125 haftmann@32077  126 lemma le_INFI: "(\i. i : A \ u \ M i) \ u \ (INF i:A. M i)"  haftmann@32077  127  by (auto simp add: INFI_def intro: Inf_greatest)  haftmann@32077  128 haftmann@32077  129 lemma SUP_const[simp]: "A \ {} \ (SUP i:A. M) = M"  haftmann@32077  130  by (auto intro: antisym SUP_leI le_SUPI)  haftmann@32077  131 haftmann@32077  132 lemma INF_const[simp]: "A \ {} \ (INF i:A. M) = M"  haftmann@32077  133  by (auto intro: antisym INF_leI le_INFI)  haftmann@32077  134 haftmann@32077  135 end  haftmann@32077  136 haftmann@32077  137 haftmann@32139  138 subsection {* @{typ bool} and @{typ "_ \ _"} as complete lattice *}  haftmann@32077  139 haftmann@32077  140 instantiation bool :: complete_lattice  haftmann@32077  141 begin  haftmann@32077  142 haftmann@32077  143 definition  haftmann@32077  144  Inf_bool_def: "\A \ (\x\A. x)"  haftmann@32077  145 haftmann@32077  146 definition  haftmann@32077  147  Sup_bool_def: "\A \ (\x\A. x)"  haftmann@32077  148 haftmann@32077  149 instance proof  haftmann@32077  150 qed (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)  haftmann@32077  151 haftmann@32077  152 end  haftmann@32077  153 haftmann@32077  154 lemma Inf_empty_bool [simp]:  haftmann@32077  155  "\{}"  haftmann@32077  156  unfolding Inf_bool_def by auto  haftmann@32077  157 haftmann@32077  158 lemma not_Sup_empty_bool [simp]:  haftmann@32077  159  "\ \{}"  haftmann@32077  160  unfolding Sup_bool_def by auto  haftmann@32077  161 haftmann@32120  162 lemma INFI_bool_eq:  haftmann@32120  163  "INFI = Ball"  haftmann@32120  164 proof (rule ext)+  haftmann@32120  165  fix A :: "'a set"  haftmann@32120  166  fix P :: "'a \ bool"  haftmann@32120  167  show "(INF x:A. P x) \ (\x \ A. P x)"  haftmann@32120  168  by (auto simp add: Ball_def INFI_def Inf_bool_def)  haftmann@32120  169 qed  haftmann@32120  170 haftmann@32120  171 lemma SUPR_bool_eq:  haftmann@32120  172  "SUPR = Bex"  haftmann@32120  173 proof (rule ext)+  haftmann@32120  174  fix A :: "'a set"  haftmann@32120  175  fix P :: "'a \ bool"  haftmann@32120  176  show "(SUP x:A. P x) \ (\x \ A. P x)"  haftmann@32120  177  by (auto simp add: Bex_def SUPR_def Sup_bool_def)  haftmann@32120  178 qed  haftmann@32120  179 haftmann@32077  180 instantiation "fun" :: (type, complete_lattice) complete_lattice  haftmann@32077  181 begin  haftmann@32077  182 haftmann@32077  183 definition  haftmann@32077  184  Inf_fun_def [code del]: "\A = (\x. \{y. \f\A. y = f x})"  haftmann@32077  185 haftmann@32077  186 definition  haftmann@32077  187  Sup_fun_def [code del]: "\A = (\x. \{y. \f\A. y = f x})"  haftmann@32077  188 haftmann@32077  189 instance proof  haftmann@32077  190 qed (auto simp add: Inf_fun_def Sup_fun_def le_fun_def  haftmann@32077  191  intro: Inf_lower Sup_upper Inf_greatest Sup_least)  haftmann@32077  192 haftmann@32077  193 end  haftmann@32077  194 haftmann@32077  195 lemma Inf_empty_fun:  haftmann@32077  196  "\{} = (\_. \{})"  haftmann@32135  197  by (simp add: Inf_fun_def)  haftmann@32077  198 haftmann@32077  199 lemma Sup_empty_fun:  haftmann@32077  200  "\{} = (\_. \{})"  haftmann@32135  201  by (simp add: Sup_fun_def)  haftmann@32077  202 haftmann@32077  203 haftmann@32139  204 subsection {* Union *}  haftmann@32115  205 haftmann@32587  206 abbreviation Union :: "'a set set \ 'a set" where  haftmann@32587  207  "Union S \ \S"  haftmann@32115  208 haftmann@32115  209 notation (xsymbols)  haftmann@32115  210  Union ("\_" [90] 90)  haftmann@32115  211 haftmann@32135  212 lemma Union_eq:  haftmann@32135  213  "\A = {x. \B \ A. x \ B}"  haftmann@32115  214 proof (rule set_ext)  haftmann@32115  215  fix x  haftmann@32135  216  have "(\Q\{P. \B\A. P \ x \ B}. Q) \ (\B\A. x \ B)"  haftmann@32115  217  by auto  haftmann@32135  218  then show "x \ \A \ x \ {x. \B\A. x \ B}"  haftmann@32587  219  by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)  haftmann@32115  220 qed  haftmann@32115  221 haftmann@32115  222 lemma Union_iff [simp, noatp]:  haftmann@32115  223  "A \ \C \ (\X\C. A\X)"  haftmann@32115  224  by (unfold Union_eq) blast  haftmann@32115  225 haftmann@32115  226 lemma UnionI [intro]:  haftmann@32115  227  "X \ C \ A \ X \ A \ \C"  haftmann@32115  228  -- {* The order of the premises presupposes that @{term C} is rigid;  haftmann@32115  229  @{term A} may be flexible. *}  haftmann@32115  230  by auto  haftmann@32115  231 haftmann@32115  232 lemma UnionE [elim!]:  haftmann@32115  233  "A \ \C \ (\X. A\X \ X\C \ R) \ R"  haftmann@32115  234  by auto  haftmann@32115  235 haftmann@32135  236 lemma Union_upper: "B \ A ==> B \ Union A"  haftmann@32135  237  by (iprover intro: subsetI UnionI)  haftmann@32135  238 haftmann@32135  239 lemma Union_least: "(!!X. X \ A ==> X \ C) ==> Union A \ C"  haftmann@32135  240  by (iprover intro: subsetI elim: UnionE dest: subsetD)  haftmann@32135  241 haftmann@32135  242 lemma Un_eq_Union: "A \ B = \{A, B}"  haftmann@32135  243  by blast  haftmann@32135  244 haftmann@32135  245 lemma Union_empty [simp]: "Union({}) = {}"  haftmann@32135  246  by blast  haftmann@32135  247 haftmann@32135  248 lemma Union_UNIV [simp]: "Union UNIV = UNIV"  haftmann@32135  249  by blast  haftmann@32135  250 haftmann@32135  251 lemma Union_insert [simp]: "Union (insert a B) = a \ \B"  haftmann@32135  252  by blast  haftmann@32135  253 haftmann@32135  254 lemma Union_Un_distrib [simp]: "\(A Un B) = \A \ \B"  haftmann@32135  255  by blast  haftmann@32135  256 haftmann@32135  257 lemma Union_Int_subset: "\(A \ B) \ \A \ \B"  haftmann@32135  258  by blast  haftmann@32135  259 haftmann@32135  260 lemma Union_empty_conv [simp,noatp]: "(\A = {}) = (\x\A. x = {})"  haftmann@32135  261  by blast  haftmann@32135  262 haftmann@32135  263 lemma empty_Union_conv [simp,noatp]: "({} = \A) = (\x\A. x = {})"  haftmann@32135  264  by blast  haftmann@32135  265 haftmann@32135  266 lemma Union_disjoint: "(\C \ A = {}) = (\B\C. B \ A = {})"  haftmann@32135  267  by blast  haftmann@32135  268 haftmann@32135  269 lemma subset_Pow_Union: "A \ Pow (\A)"  haftmann@32135  270  by blast  haftmann@32135  271 haftmann@32135  272 lemma Union_Pow_eq [simp]: "\(Pow A) = A"  haftmann@32135  273  by blast  haftmann@32135  274 haftmann@32135  275 lemma Union_mono: "A \ B ==> \A \ \B"  haftmann@32135  276  by blast  haftmann@32135  277 haftmann@32115  278 haftmann@32139  279 subsection {* Unions of families *}  haftmann@32077  280 haftmann@32077  281 definition UNION :: "'a set \ ('a \ 'b set) \ 'b set" where  haftmann@32135  282  SUPR_set_eq [symmetric]: "UNION S f = (SUP x:S. f x)"  haftmann@32077  283 haftmann@32077  284 syntax  haftmann@32077  285  "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)  haftmann@32077  286  "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 10] 10)  haftmann@32077  287 haftmann@32077  288 syntax (xsymbols)  haftmann@32077  289  "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" [0, 10] 10)  haftmann@32077  290  "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 10] 10)  haftmann@32077  291 haftmann@32077  292 syntax (latex output)  haftmann@32077  293  "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)  haftmann@32077  294  "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^esub>)/ _)" [0, 10] 10)  haftmann@32077  295 haftmann@32077  296 translations  haftmann@32077  297  "UN x y. B" == "UN x. UN y. B"  haftmann@32077  298  "UN x. B" == "CONST UNION CONST UNIV (%x. B)"  haftmann@32077  299  "UN x. B" == "UN x:CONST UNIV. B"  haftmann@32077  300  "UN x:A. B" == "CONST UNION A (%x. B)"  haftmann@32077  301 haftmann@32077  302 text {*  haftmann@32077  303  Note the difference between ordinary xsymbol syntax of indexed  haftmann@32077  304  unions and intersections (e.g.\ @{text"\a\<^isub>1\A\<^isub>1. B"})  haftmann@32077  305  and their \LaTeX\ rendition: @{term"\a\<^isub>1\A\<^isub>1. B"}. The  haftmann@32077  306  former does not make the index expression a subscript of the  haftmann@32077  307  union/intersection symbol because this leads to problems with nested  haftmann@32077  308  subscripts in Proof General.  haftmann@32077  309 *}  haftmann@32077  310 haftmann@32120  311 print_translation {* [  haftmann@32120  312 Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} "@UNION"  haftmann@32120  313 ] *} -- {* to avoid eta-contraction of body *}  haftmann@32077  314 haftmann@32135  315 lemma UNION_eq_Union_image:  haftmann@32135  316  "(\x\A. B x) = \(BA)"  haftmann@32587  317  by (simp add: SUPR_def SUPR_set_eq [symmetric])  haftmann@32115  318 haftmann@32115  319 lemma Union_def:  haftmann@32117  320  "\S = (\x\S. x)"  haftmann@32115  321  by (simp add: UNION_eq_Union_image image_def)  haftmann@32115  322 haftmann@32115  323 lemma UNION_def [noatp]:  haftmann@32135  324  "(\x\A. B x) = {y. \x\A. y \ B x}"  haftmann@32117  325  by (auto simp add: UNION_eq_Union_image Union_eq)  haftmann@32115  326   haftmann@32115  327 lemma Union_image_eq [simp]:  haftmann@32115  328  "\(BA) = (\x\A. B x)"  haftmann@32115  329  by (rule sym) (fact UNION_eq_Union_image)  haftmann@32115  330   wenzelm@11979  331 lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"  wenzelm@11979  332  by (unfold UNION_def) blast  wenzelm@11979  333 wenzelm@11979  334 lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)"  wenzelm@11979  335  -- {* The order of the premises presupposes that @{term A} is rigid;  wenzelm@11979  336  @{term b} may be flexible. *}  wenzelm@11979  337  by auto  wenzelm@11979  338 wenzelm@11979  339 lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R"  wenzelm@11979  340  by (unfold UNION_def) blast  clasohm@923  341 wenzelm@11979  342 lemma UN_cong [cong]:  wenzelm@11979  343  "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"  wenzelm@11979  344  by (simp add: UNION_def)  wenzelm@11979  345 berghofe@29691  346 lemma strong_UN_cong:  berghofe@29691  347  "A = B ==> (!!x. x:B =simp=> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"  berghofe@29691  348  by (simp add: UNION_def simp_implies_def)  berghofe@29691  349 haftmann@32077  350 lemma image_eq_UN: "fA = (UN x:A. {f x})"  haftmann@32077  351  by blast  haftmann@32077  352 haftmann@32135  353 lemma UN_upper: "a \ A ==> B a \ (\x\A. B x)"  haftmann@32135  354  by blast  haftmann@32135  355 haftmann@32135  356 lemma UN_least: "(!!x. x \ A ==> B x \ C) ==> (\x\A. B x) \ C"  haftmann@32135  357  by (iprover intro: subsetI elim: UN_E dest: subsetD)  haftmann@32135  358 haftmann@32135  359 lemma Collect_bex_eq [noatp]: "{x. \y\A. P x y} = (\y\A. {x. P x y})"  haftmann@32135  360  by blast  haftmann@32135  361 haftmann@32135  362 lemma UN_insert_distrib: "u \ A ==> (\x\A. insert a (B x)) = insert a (\x\A. B x)"  haftmann@32135  363  by blast  haftmann@32135  364 haftmann@32135  365 lemma UN_empty [simp,noatp]: "(\x\{}. B x) = {}"  haftmann@32135  366  by blast  haftmann@32135  367 haftmann@32135  368 lemma UN_empty2 [simp]: "(\x\A. {}) = {}"  haftmann@32135  369  by blast  haftmann@32135  370 haftmann@32135  371 lemma UN_singleton [simp]: "(\x\A. {x}) = A"  haftmann@32135  372  by blast  haftmann@32135  373 haftmann@32135  374 lemma UN_absorb: "k \ I ==> A k \ (\i\I. A i) = (\i\I. A i)"  haftmann@32135  375  by auto  haftmann@32135  376 haftmann@32135  377 lemma UN_insert [simp]: "(\x\insert a A. B x) = B a \ UNION A B"  haftmann@32135  378  by blast  haftmann@32135  379 haftmann@32135  380 lemma UN_Un[simp]: "(\i \ A \ B. M i) = (\i\A. M i) \ (\i\B. M i)"  haftmann@32135  381  by blast  haftmann@32135  382 haftmann@32135  383 lemma UN_UN_flatten: "(\x \ (\y\A. B y). C x) = (\y\A. \x\B y. C x)"  haftmann@32135  384  by blast  haftmann@32135  385 haftmann@32135  386 lemma UN_subset_iff: "((\i\I. A i) \ B) = (\i\I. A i \ B)"  haftmann@32135  387  by blast  haftmann@32135  388 haftmann@32135  389 lemma image_Union: "f  \S = (\x\S. f  x)"  haftmann@32135  390  by blast  haftmann@32135  391 haftmann@32135  392 lemma UN_constant [simp]: "(\y\A. c) = (if A = {} then {} else c)"  haftmann@32135  393  by auto  haftmann@32135  394 haftmann@32135  395 lemma UN_eq: "(\x\A. B x) = \({Y. \x\A. Y = B x})"  haftmann@32135  396  by blast  haftmann@32135  397 haftmann@32135  398 lemma UNION_empty_conv[simp]:  haftmann@32135  399  "({} = (UN x:A. B x)) = (\x\A. B x = {})"  haftmann@32135  400  "((UN x:A. B x) = {}) = (\x\A. B x = {})"  haftmann@32135  401 by blast+  haftmann@32135  402 haftmann@32135  403 lemma Collect_ex_eq [noatp]: "{x. \y. P x y} = (\y. {x. P x y})"  haftmann@32135  404  by blast  haftmann@32135  405 haftmann@32135  406 lemma ball_UN: "(\z \ UNION A B. P z) = (\x\A. \z \ B x. P z)"  haftmann@32135  407  by blast  haftmann@32135  408 haftmann@32135  409 lemma bex_UN: "(\z \ UNION A B. P z) = (\x\A. \z\B x. P z)"  haftmann@32135  410  by blast  haftmann@32135  411 haftmann@32135  412 lemma Un_eq_UN: "A \ B = (\b. if b then A else B)"  haftmann@32135  413  by (auto simp add: split_if_mem2)  haftmann@32135  414 haftmann@32135  415 lemma UN_bool_eq: "(\b::bool. A b) = (A True \ A False)"  haftmann@32135  416  by (auto intro: bool_contrapos)  haftmann@32135  417 haftmann@32135  418 lemma UN_Pow_subset: "(\x\A. Pow (B x)) \ Pow (\x\A. B x)"  haftmann@32135  419  by blast  haftmann@32135  420 haftmann@32135  421 lemma UN_mono:  haftmann@32135  422  "A \ B ==> (!!x. x \ A ==> f x \ g x) ==>  haftmann@32135  423  (\x\A. f x) \ (\x\B. g x)"  haftmann@32135  424  by (blast dest: subsetD)  haftmann@32135  425 haftmann@32135  426 lemma vimage_Union: "f - (Union A) = (UN X:A. f - X)"  haftmann@32135  427  by blast  haftmann@32135  428 haftmann@32135  429 lemma vimage_UN: "f-(UN x:A. B x) = (UN x:A. f - B x)"  haftmann@32135  430  by blast  haftmann@32135  431 haftmann@32135  432 lemma vimage_eq_UN: "f-B = (UN y: B. f-{y})"  haftmann@32135  433  -- {* NOT suitable for rewriting *}  haftmann@32135  434  by blast  haftmann@32135  435 haftmann@32135  436 lemma image_UN: "(f  (UNION A B)) = (UN x:A.(f  (B x)))"  haftmann@32135  437 by blast  haftmann@32135  438 wenzelm@11979  439 haftmann@32139  440 subsection {* Inter *}  haftmann@32115  441 haftmann@32587  442 abbreviation Inter :: "'a set set \ 'a set" where  haftmann@32587  443  "Inter S \ \S"  haftmann@32135  444   haftmann@32115  445 notation (xsymbols)  haftmann@32115  446  Inter ("\_" [90] 90)  haftmann@32115  447 haftmann@32135  448 lemma Inter_eq [code del]:  haftmann@32135  449  "\A = {x. \B \ A. x \ B}"  haftmann@32115  450 proof (rule set_ext)  haftmann@32115  451  fix x  haftmann@32135  452  have "(\Q\{P. \B\A. P \ x \ B}. Q) \ (\B\A. x \ B)"  haftmann@32115  453  by auto  haftmann@32135  454  then show "x \ \A \ x \ {x. \B \ A. x \ B}"  haftmann@32587  455  by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)  haftmann@32115  456 qed  haftmann@32115  457 haftmann@32115  458 lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"  haftmann@32115  459  by (unfold Inter_eq) blast  haftmann@32115  460 haftmann@32115  461 lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"  haftmann@32115  462  by (simp add: Inter_eq)  haftmann@32115  463 haftmann@32115  464 text {*  haftmann@32115  465  \medskip A destruct'' rule -- every @{term X} in @{term C}  haftmann@32115  466  contains @{term A} as an element, but @{prop "A:X"} can hold when  haftmann@32115  467  @{prop "X:C"} does not! This rule is analogous to @{text spec}.  haftmann@32115  468 *}  haftmann@32115  469 haftmann@32115  470 lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"  haftmann@32115  471  by auto  haftmann@32115  472 haftmann@32115  473 lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"  haftmann@32115  474  -- {* Classical'' elimination rule -- does not require proving  haftmann@32115  475  @{prop "X:C"}. *}  haftmann@32115  476  by (unfold Inter_eq) blast  haftmann@32115  477 haftmann@32135  478 lemma Inter_lower: "B \ A ==> Inter A \ B"  haftmann@32135  479  by blast  haftmann@32135  480 haftmann@32135  481 lemma Inter_subset:  haftmann@32135  482  "[| !!X. X \ A ==> X \ B; A ~= {} |] ==> \A \ B"  haftmann@32135  483  by blast  haftmann@32135  484 haftmann@32135  485 lemma Inter_greatest: "(!!X. X \ A ==> C \ X) ==> C \ Inter A"  haftmann@32135  486  by (iprover intro: InterI subsetI dest: subsetD)  haftmann@32135  487 haftmann@32135  488 lemma Int_eq_Inter: "A \ B = \{A, B}"  haftmann@32135  489  by blast  haftmann@32135  490 haftmann@32135  491 lemma Inter_empty [simp]: "\{} = UNIV"  haftmann@32135  492  by blast  haftmann@32135  493 haftmann@32135  494 lemma Inter_UNIV [simp]: "\UNIV = {}"  haftmann@32135  495  by blast  haftmann@32135  496 haftmann@32135  497 lemma Inter_insert [simp]: "\(insert a B) = a \ \B"  haftmann@32135  498  by blast  haftmann@32135  499 haftmann@32135  500 lemma Inter_Un_subset: "\A \ \B \ \(A \ B)"  haftmann@32135  501  by blast  haftmann@32135  502 haftmann@32135  503 lemma Inter_Un_distrib: "\(A \ B) = \A \ \B"  haftmann@32135  504  by blast  haftmann@32135  505 haftmann@32135  506 lemma Inter_UNIV_conv [simp,noatp]:  haftmann@32135  507  "(\A = UNIV) = (\x\A. x = UNIV)"  haftmann@32135  508  "(UNIV = \A) = (\x\A. x = UNIV)"  haftmann@32135  509  by blast+  haftmann@32135  510 haftmann@32135  511 lemma Inter_anti_mono: "B \ A ==> \A \ \B"  haftmann@32135  512  by blast  haftmann@32135  513 haftmann@32115  514 haftmann@32139  515 subsection {* Intersections of families *}  wenzelm@11979  516 haftmann@32081  517 definition INTER :: "'a set \ ('a \ 'b set) \ 'b set" where  haftmann@32135  518  INFI_set_eq [symmetric]: "INTER S f = (INF x:S. f x)"  haftmann@32081  519 haftmann@32081  520 syntax  haftmann@32081  521  "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)  haftmann@32081  522  "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 10] 10)  haftmann@32081  523 haftmann@32081  524 syntax (xsymbols)  haftmann@32081  525  "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" [0, 10] 10)  haftmann@32081  526  "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 10] 10)  haftmann@32081  527 haftmann@32081  528 syntax (latex output)  haftmann@32081  529  "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)  haftmann@32081  530  "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^esub>)/ _)" [0, 10] 10)  haftmann@32081  531 haftmann@32081  532 translations  haftmann@32081  533  "INT x y. B" == "INT x. INT y. B"  haftmann@32081  534  "INT x. B" == "CONST INTER CONST UNIV (%x. B)"  haftmann@32081  535  "INT x. B" == "INT x:CONST UNIV. B"  haftmann@32081  536  "INT x:A. B" == "CONST INTER A (%x. B)"  haftmann@32081  537 haftmann@32120  538 print_translation {* [  haftmann@32120  539 Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} "@INTER"  haftmann@32120  540 ] *} -- {* to avoid eta-contraction of body *}  haftmann@32081  541 haftmann@32135  542 lemma INTER_eq_Inter_image:  haftmann@32135  543  "(\x\A. B x) = \(BA)"  haftmann@32587  544  by (simp add: INFI_def INFI_set_eq [symmetric])  haftmann@32135  545   haftmann@32115  546 lemma Inter_def:  haftmann@32135  547  "\S = (\x\S. x)"  haftmann@32115  548  by (simp add: INTER_eq_Inter_image image_def)  haftmann@32115  549 haftmann@32115  550 lemma INTER_def:  haftmann@32135  551  "(\x\A. B x) = {y. \x\A. y \ B x}"  haftmann@32117  552  by (auto simp add: INTER_eq_Inter_image Inter_eq)  haftmann@32115  553 haftmann@32115  554 lemma Inter_image_eq [simp]:  haftmann@32115  555  "\(BA) = (\x\A. B x)"  haftmann@32115  556  by (rule sym) (fact INTER_eq_Inter_image)  haftmann@32115  557 wenzelm@11979  558 lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"  wenzelm@11979  559  by (unfold INTER_def) blast  clasohm@923  560 wenzelm@11979  561 lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"  wenzelm@11979  562  by (unfold INTER_def) blast  wenzelm@11979  563 wenzelm@11979  564 lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"  wenzelm@11979  565  by auto  wenzelm@11979  566 wenzelm@11979  567 lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"  wenzelm@11979  568  -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}  wenzelm@11979  569  by (unfold INTER_def) blast  wenzelm@11979  570 wenzelm@11979  571 lemma INT_cong [cong]:  wenzelm@11979  572  "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"  wenzelm@11979  573  by (simp add: INTER_def)  wenzelm@7238  574 haftmann@32135  575 lemma Collect_ball_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})"  haftmann@30531  576  by blast  haftmann@30531  577 haftmann@32135  578 lemma Collect_all_eq: "{x. \y. P x y} = (\y. {x. P x y})"  wenzelm@12897  579  by blast  wenzelm@12897  580 wenzelm@12897  581 lemma INT_lower: "a \ A ==> (\x\A. B x) \ B a"  wenzelm@12897  582  by blast  wenzelm@12897  583 wenzelm@12897  584 lemma INT_greatest: "(!!x. x \ A ==> C \ B x) ==> C \ (\x\A. B x)"  nipkow@17589  585  by (iprover intro: INT_I subsetI dest: subsetD)  wenzelm@12897  586 wenzelm@12897  587 lemma INT_empty [simp]: "(\x\{}. B x) = UNIV"  wenzelm@12897  588  by blast  wenzelm@12897  589 wenzelm@12897  590 lemma INT_absorb: "k \ I ==> A k \ (\i\I. A i) = (\i\I. A i)"  wenzelm@12897  591  by blast  wenzelm@12897  592 wenzelm@12897  593 lemma INT_subset_iff: "(B \ (\i\I. A i)) = (\i\I. B \ A i)"  wenzelm@12897  594  by blast  wenzelm@12897  595 wenzelm@12897  596 lemma INT_insert [simp]: "(\x \ insert a A. B x) = B a \ INTER A B"  wenzelm@12897  597  by blast  wenzelm@12897  598 wenzelm@12897  599 lemma INT_Un: "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)"  wenzelm@12897  600  by blast  wenzelm@12897  601 wenzelm@12897  602 lemma INT_insert_distrib:  wenzelm@12897  603  "u \ A ==> (\x\A. insert a (B x)) = insert a (\x\A. B x)"  wenzelm@12897  604  by blast  wenzelm@12897  605 wenzelm@12897  606 lemma INT_constant [simp]: "(\y\A. c) = (if A = {} then UNIV else c)"  wenzelm@12897  607  by auto  wenzelm@12897  608 wenzelm@12897  609 lemma INT_eq: "(\x\A. B x) = \({Y. \x\A. Y = B x})"  wenzelm@12897  610  -- {* Look: it has an \emph{existential} quantifier *}  wenzelm@12897  611  by blast  wenzelm@12897  612 paulson@18447  613 lemma INTER_UNIV_conv[simp]:  nipkow@13653  614  "(UNIV = (INT x:A. B x)) = (\x\A. B x = UNIV)"  nipkow@13653  615  "((INT x:A. B x) = UNIV) = (\x\A. B x = UNIV)"  nipkow@13653  616 by blast+  wenzelm@12897  617 haftmann@32135  618 lemma INT_bool_eq: "(\b::bool. A b) = (A True \ A False)"  haftmann@32135  619  by (auto intro: bool_induct)  haftmann@32135  620 haftmann@32135  621 lemma Pow_INT_eq: "Pow (\x\A. B x) = (\x\A. Pow (B x))"  haftmann@32135  622  by blast  haftmann@32135  623 haftmann@32135  624 lemma INT_anti_mono:  haftmann@32135  625  "B \ A ==> (!!x. x \ A ==> f x \ g x) ==>  haftmann@32135  626  (\x\A. f x) \ (\x\A. g x)"  haftmann@32135  627  -- {* The last inclusion is POSITIVE! *}  haftmann@32135  628  by (blast dest: subsetD)  haftmann@32135  629 haftmann@32135  630 lemma vimage_INT: "f-(INT x:A. B x) = (INT x:A. f - B x)"  haftmann@32135  631  by blast  haftmann@32135  632 haftmann@32135  633 haftmann@32139  634 subsection {* Distributive laws *}  wenzelm@12897  635 wenzelm@12897  636 lemma Int_Union: "A \ \B = (\C\B. A \ C)"  wenzelm@12897  637  by blast  wenzelm@12897  638 wenzelm@12897  639 lemma Int_Union2: "\B \ A = (\C\B. C \ A)"  wenzelm@12897  640  by blast  wenzelm@12897  641 wenzelm@12897  642 lemma Un_Union_image: "(\x\C. A x \ B x) = \(AC) \ \(BC)"  wenzelm@12897  643  -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}  wenzelm@12897  644  -- {* Union of a family of unions *}  wenzelm@12897  645  by blast  wenzelm@12897  646 wenzelm@12897  647 lemma UN_Un_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)"  wenzelm@12897  648  -- {* Equivalent version *}  wenzelm@12897  649  by blast  wenzelm@12897  650 wenzelm@12897  651 lemma Un_Inter: "A \ \B = (\C\B. A \ C)"  wenzelm@12897  652  by blast  wenzelm@12897  653 wenzelm@12897  654 lemma Int_Inter_image: "(\x\C. A x \ B x) = \(AC) \ \(BC)"  wenzelm@12897  655  by blast  wenzelm@12897  656 wenzelm@12897  657 lemma INT_Int_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)"  wenzelm@12897  658  -- {* Equivalent version *}  wenzelm@12897  659  by blast  wenzelm@12897  660 wenzelm@12897  661 lemma Int_UN_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)"  wenzelm@12897  662  -- {* Halmos, Naive Set Theory, page 35. *}  wenzelm@12897  663  by blast  wenzelm@12897  664 wenzelm@12897  665 lemma Un_INT_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)"  wenzelm@12897  666  by blast  wenzelm@12897  667 wenzelm@12897  668 lemma Int_UN_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)"  wenzelm@12897  669  by blast  wenzelm@12897  670 wenzelm@12897  671 lemma Un_INT_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)"  wenzelm@12897  672  by blast  wenzelm@12897  673 wenzelm@12897  674 haftmann@32139  675 subsection {* Complement *}  haftmann@32135  676 haftmann@32135  677 lemma Compl_UN [simp]: "-(\x\A. B x) = (\x\A. -B x)"  wenzelm@12897  678  by blast  wenzelm@12897  679 haftmann@32135  680 lemma Compl_INT [simp]: "-(\x\A. B x) = (\x\A. -B x)"  wenzelm@12897  681  by blast  wenzelm@12897  682 wenzelm@12897  683 haftmann@32139  684 subsection {* Miniscoping and maxiscoping *}  wenzelm@12897  685 paulson@13860  686 text {* \medskip Miniscoping: pushing in quantifiers and big Unions  paulson@13860  687  and Intersections. *}  wenzelm@12897  688 wenzelm@12897  689 lemma UN_simps [simp]:  wenzelm@12897  690  "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))"  wenzelm@12897  691  "!!A B C. (UN x:C. A x Un B) = ((if C={} then {} else (UN x:C. A x) Un B))"  wenzelm@12897  692  "!!A B C. (UN x:C. A Un B x) = ((if C={} then {} else A Un (UN x:C. B x)))"  wenzelm@12897  693  "!!A B C. (UN x:C. A x Int B) = ((UN x:C. A x) Int B)"  wenzelm@12897  694  "!!A B C. (UN x:C. A Int B x) = (A Int (UN x:C. B x))"  wenzelm@12897  695  "!!A B C. (UN x:C. A x - B) = ((UN x:C. A x) - B)"  wenzelm@12897  696  "!!A B C. (UN x:C. A - B x) = (A - (INT x:C. B x))"  wenzelm@12897  697  "!!A B. (UN x: Union A. B x) = (UN y:A. UN x:y. B x)"  wenzelm@12897  698  "!!A B C. (UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)"  wenzelm@12897  699  "!!A B f. (UN x:fA. B x) = (UN a:A. B (f a))"  wenzelm@12897  700  by auto  wenzelm@12897  701 wenzelm@12897  702 lemma INT_simps [simp]:  wenzelm@12897  703  "!!A B C. (INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)"  wenzelm@12897  704  "!!A B C. (INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))"  wenzelm@12897  705  "!!A B C. (INT x:C. A x - B) = (if C={} then UNIV else (INT x:C. A x) - B)"  wenzelm@12897  706  "!!A B C. (INT x:C. A - B x) = (if C={} then UNIV else A - (UN x:C. B x))"  wenzelm@12897  707  "!!a B C. (INT x:C. insert a (B x)) = insert a (INT x:C. B x)"  wenzelm@12897  708  "!!A B C. (INT x:C. A x Un B) = ((INT x:C. A x) Un B)"  wenzelm@12897  709  "!!A B C. (INT x:C. A Un B x) = (A Un (INT x:C. B x))"  wenzelm@12897  710  "!!A B. (INT x: Union A. B x) = (INT y:A. INT x:y. B x)"  wenzelm@12897  711  "!!A B C. (INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)"  wenzelm@12897  712  "!!A B f. (INT x:fA. B x) = (INT a:A. B (f a))"  wenzelm@12897  713  by auto  wenzelm@12897  714 paulson@24286  715 lemma ball_simps [simp,noatp]:  wenzelm@12897  716  "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"  wenzelm@12897  717  "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"  wenzelm@12897  718  "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"  wenzelm@12897  719  "!!A P Q. (ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)"  wenzelm@12897  720  "!!P. (ALL x:{}. P x) = True"  wenzelm@12897  721  "!!P. (ALL x:UNIV. P x) = (ALL x. P x)"  wenzelm@12897  722  "!!a B P. (ALL x:insert a B. P x) = (P a & (ALL x:B. P x))"  wenzelm@12897  723  "!!A P. (ALL x:Union A. P x) = (ALL y:A. ALL x:y. P x)"  wenzelm@12897  724  "!!A B P. (ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)"  wenzelm@12897  725  "!!P Q. (ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"  wenzelm@12897  726  "!!A P f. (ALL x:fA. P x) = (ALL x:A. P (f x))"  wenzelm@12897  727  "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"  wenzelm@12897  728  by auto  wenzelm@12897  729 paulson@24286  730 lemma bex_simps [simp,noatp]:  wenzelm@12897  731  "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"  wenzelm@12897  732  "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"  wenzelm@12897  733  "!!P. (EX x:{}. P x) = False"  wenzelm@12897  734  "!!P. (EX x:UNIV. P x) = (EX x. P x)"  wenzelm@12897  735  "!!a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))"  wenzelm@12897  736  "!!A P. (EX x:Union A. P x) = (EX y:A. EX x:y. P x)"  wenzelm@12897  737  "!!A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)"  wenzelm@12897  738  "!!P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)"  wenzelm@12897  739  "!!A P f. (EX x:fA. P x) = (EX x:A. P (f x))"  wenzelm@12897  740  "!!A P. (~(EX x:A. P x)) = (ALL x:A. ~P x)"  wenzelm@12897  741  by auto  wenzelm@12897  742 wenzelm@12897  743 lemma ball_conj_distrib:  wenzelm@12897  744  "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))"  wenzelm@12897  745  by blast  wenzelm@12897  746 wenzelm@12897  747 lemma bex_disj_distrib:  wenzelm@12897  748  "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))"  wenzelm@12897  749  by blast  wenzelm@12897  750 wenzelm@12897  751 paulson@13860  752 text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}  paulson@13860  753 paulson@13860  754 lemma UN_extend_simps:  paulson@13860  755  "!!a B C. insert a (UN x:C. B x) = (if C={} then {a} else (UN x:C. insert a (B x)))"  paulson@13860  756  "!!A B C. (UN x:C. A x) Un B = (if C={} then B else (UN x:C. A x Un B))"  paulson@13860  757  "!!A B C. A Un (UN x:C. B x) = (if C={} then A else (UN x:C. A Un B x))"  paulson@13860  758  "!!A B C. ((UN x:C. A x) Int B) = (UN x:C. A x Int B)"  paulson@13860  759  "!!A B C. (A Int (UN x:C. B x)) = (UN x:C. A Int B x)"  paulson@13860  760  "!!A B C. ((UN x:C. A x) - B) = (UN x:C. A x - B)"  paulson@13860  761  "!!A B C. (A - (INT x:C. B x)) = (UN x:C. A - B x)"  paulson@13860  762  "!!A B. (UN y:A. UN x:y. B x) = (UN x: Union A. B x)"  paulson@13860  763  "!!A B C. (UN x:A. UN z: B(x). C z) = (UN z: UNION A B. C z)"  paulson@13860  764  "!!A B f. (UN a:A. B (f a)) = (UN x:fA. B x)"  paulson@13860  765  by auto  paulson@13860  766 paulson@13860  767 lemma INT_extend_simps:  paulson@13860  768  "!!A B C. (INT x:C. A x) Int B = (if C={} then B else (INT x:C. A x Int B))"  paulson@13860  769  "!!A B C. A Int (INT x:C. B x) = (if C={} then A else (INT x:C. A Int B x))"  paulson@13860  770  "!!A B C. (INT x:C. A x) - B = (if C={} then UNIV-B else (INT x:C. A x - B))"  paulson@13860  771  "!!A B C. A - (UN x:C. B x) = (if C={} then A else (INT x:C. A - B x))"  paulson@13860  772  "!!a B C. insert a (INT x:C. B x) = (INT x:C. insert a (B x))"  paulson@13860  773  "!!A B C. ((INT x:C. A x) Un B) = (INT x:C. A x Un B)"  paulson@13860  774  "!!A B C. A Un (INT x:C. B x) = (INT x:C. A Un B x)"  paulson@13860  775  "!!A B. (INT y:A. INT x:y. B x) = (INT x: Union A. B x)"  paulson@13860  776  "!!A B C. (INT x:A. INT z: B(x). C z) = (INT z: UNION A B. C z)"  paulson@13860  777  "!!A B f. (INT a:A. B (f a)) = (INT x:fA. B x)"  paulson@13860  778  by auto  paulson@13860  779 paulson@13860  780 haftmann@32135  781 no_notation  haftmann@32135  782  less_eq (infix "\" 50) and  haftmann@32135  783  less (infix "\" 50) and  haftmann@32135  784  inf (infixl "\" 70) and  haftmann@32135  785  sup (infixl "\" 65) and  haftmann@32135  786  Inf ("\_" [900] 900) and  haftmann@32135  787  Sup ("\_" [900] 900)  haftmann@32135  788 haftmann@30596  789 lemmas mem_simps =  haftmann@30596  790  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff  haftmann@30596  791  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff  haftmann@30596  792  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}  wenzelm@21669  793 wenzelm@11979  794 end `