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