src/HOL/Complete_Lattice.thy
 author haftmann Sun Jul 17 19:55:17 2011 +0200 (2011-07-17) changeset 43867 771014555553 parent 43866 8a50dc70cbff child 43868 9684251c7ec1 permissions -rw-r--r--
generalized INT_anti_mono
 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@43831  79  by (simp add: Inf_insert)  haftmann@32077  80 haftmann@32077  81 lemma Sup_binary:  haftmann@32077  82  "\{a, b} = a \ b"  haftmann@43831  83  by (simp add: 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 haftmann@43741  111 lemma Sup_upper2: "u \ A \ v \ u \ v \ \A"  hoelzl@41971  112  using Sup_upper[of u A] by auto  hoelzl@41971  113 haftmann@43741  114 lemma Inf_lower2: "u \ A \ u \ v \ \A \ v"  hoelzl@41971  115  using Inf_lower[of u A] by auto  hoelzl@41971  116 haftmann@32077  117 definition INFI :: "'b set \ ('b \ 'a) \ 'a" where  haftmann@32117  118  "INFI A f = \ (f  A)"  haftmann@32077  119 haftmann@41082  120 definition SUPR :: "'b set \ ('b \ 'a) \ 'a" where  haftmann@41082  121  "SUPR A f = \ (f  A)"  haftmann@41082  122 haftmann@32077  123 end  haftmann@32077  124 haftmann@32077  125 syntax  haftmann@41082  126  "_INF1" :: "pttrns \ 'b \ 'b" ("(3INF _./ _)" [0, 10] 10)  haftmann@41082  127  "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3INF _:_./ _)" [0, 0, 10] 10)  haftmann@41080  128  "_SUP1" :: "pttrns \ 'b \ 'b" ("(3SUP _./ _)" [0, 10] 10)  haftmann@41080  129  "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3SUP _:_./ _)" [0, 0, 10] 10)  haftmann@41080  130 haftmann@41080  131 syntax (xsymbols)  haftmann@41082  132  "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)  haftmann@41082  133  "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)  haftmann@41080  134  "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)  haftmann@41080  135  "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)  haftmann@32077  136 haftmann@32077  137 translations  haftmann@41082  138  "INF x y. B" == "INF x. INF y. B"  haftmann@41082  139  "INF x. B" == "CONST INFI CONST UNIV (%x. B)"  haftmann@41082  140  "INF x. B" == "INF x:CONST UNIV. B"  haftmann@41082  141  "INF x:A. B" == "CONST INFI A (%x. B)"  haftmann@32077  142  "SUP x y. B" == "SUP x. SUP y. B"  haftmann@32077  143  "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)"  haftmann@32077  144  "SUP x. B" == "SUP x:CONST UNIV. B"  haftmann@32077  145  "SUP x:A. B" == "CONST SUPR A (%x. B)"  haftmann@32077  146 wenzelm@35115  147 print_translation {*  wenzelm@42284  148  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},  wenzelm@42284  149  Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]  wenzelm@35115  150 *} -- {* to avoid eta-contraction of body *}  wenzelm@11979  151 haftmann@32077  152 context complete_lattice  haftmann@32077  153 begin  haftmann@32077  154 haftmann@43865  155 lemma INF_empty: "(\x\{}. f x) = \"  haftmann@43865  156  by (simp add: INFI_def)  hoelzl@41971  157 haftmann@43865  158 lemma INF_insert: "(\x\insert a A. f x) = f a \ INFI A f"  haftmann@43865  159  by (simp add: INFI_def Inf_insert)  haftmann@32077  160 haftmann@43865  161 lemma INF_leI: "i \ A \ (\i\A. f i) \ f i"  haftmann@32077  162  by (auto simp add: INFI_def intro: Inf_lower)  haftmann@32077  163 haftmann@43865  164 lemma INF_leI2: "i \ A \ f i \ u \ (\i\A. f i) \ u"  haftmann@43865  165  using INF_leI [of i A f] by auto  hoelzl@41971  166 haftmann@43865  167 lemma le_INFI: "(\i. i \ A \ u \ f i) \ u \ (\i\A. f i)"  haftmann@32077  168  by (auto simp add: INFI_def intro: Inf_greatest)  haftmann@32077  169 haftmann@43865  170 lemma le_INF_iff: "u \ (\i\A. f i) \ (\i \ A. u \ f i)"  haftmann@43865  171  by (auto simp add: INFI_def le_Inf_iff)  huffman@35629  172 haftmann@43865  173 lemma INF_const [simp]: "A \ {} \ (\i\A. f) = f"  haftmann@32077  174  by (auto intro: antisym INF_leI le_INFI)  haftmann@32077  175 haftmann@43865  176 lemma INF_cong:  haftmann@43865  177  "A = B \ (\x. x \ B \ C x = D x) \ (\x\A. C x) = (\x\B. D x)"  haftmann@43865  178  by (simp add: INFI_def image_def)  hoelzl@38705  179 hoelzl@38705  180 lemma INF_mono:  haftmann@43753  181  "(\m. m \ B \ \n\A. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)"  hoelzl@38705  182  by (force intro!: Inf_mono simp: INFI_def)  hoelzl@38705  183 haftmann@43865  184 lemma INF_subset: "A \ B \ INFI B f \ INFI A f"  haftmann@43865  185  by (intro INF_mono) auto  haftmann@43865  186 haftmann@43865  187 lemma INF_commute: "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)"  haftmann@43865  188  by (iprover intro: INF_leI le_INFI order_trans antisym)  haftmann@43865  189 haftmann@43865  190 lemma SUP_cong:  haftmann@43865  191  "A = B \ (\x. x \ B \ C x = D x) \ (\x\A. C x) = (\x\B. D x)"  haftmann@43865  192  by (simp add: SUPR_def image_def)  haftmann@43865  193 haftmann@43865  194 lemma le_SUPI: "i \ A \ f i \ (\i\A. f i)"  haftmann@43865  195  by (auto simp add: SUPR_def intro: Sup_upper)  haftmann@43865  196 haftmann@43865  197 lemma le_SUPI2: "i \ A \ u \ f i \ u \ (\i\A. f i)"  haftmann@43865  198  using le_SUPI [of i A f] by auto  haftmann@43865  199 haftmann@43865  200 lemma SUP_leI: "(\i. i \ A \ f i \ u) \ (\i\A. f i) \ u"  haftmann@43865  201  by (auto simp add: SUPR_def intro: Sup_least)  haftmann@43865  202 haftmann@43865  203 lemma SUP_le_iff: "(\i\A. f i) \ u \ (\i \ A. f i \ u)"  haftmann@43865  204  unfolding SUPR_def by (auto simp add: Sup_le_iff)  haftmann@43865  205 haftmann@43865  206 lemma SUP_const [simp]: "A \ {} \ (\i\A. f) = f"  haftmann@43865  207  by (auto intro: antisym SUP_leI le_SUPI)  haftmann@43865  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 SUP_subset: "A \ B \ SUPR A f \ SUPR B f"  haftmann@41082  214  by (intro SUP_mono) auto  hoelzl@40872  215 haftmann@43753  216 lemma SUP_commute: "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)"  haftmann@41082  217  by (iprover intro: SUP_leI le_SUPI order_trans antisym)  haftmann@41082  218 haftmann@43865  219 lemma SUP_empty: "(\x\{}. f x) = \"  haftmann@43865  220  by (simp add: SUPR_def)  haftmann@43854  221 haftmann@43865  222 lemma SUP_insert: "(\x\insert a A. f x) = f a \ SUPR A f"  haftmann@43854  223  by (simp add: SUPR_def Sup_insert)  haftmann@43854  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 haftmann@43865  232 lemma INF_less_iff:  haftmann@43865  233  fixes a :: "'a::{complete_lattice,linorder}"  haftmann@43865  234  shows "(\i\A. f i) \ a \ (\x\A. f x \ a)"  haftmann@43865  235  unfolding INFI_def Inf_less_iff by auto  haftmann@43865  236 hoelzl@38705  237 lemma less_Sup_iff:  hoelzl@38705  238  fixes a :: "'a\{complete_lattice,linorder}"  haftmann@43753  239  shows "a \ \S \ (\x\S. a \ x)"  haftmann@43754  240  unfolding not_le [symmetric] Sup_le_iff by auto  hoelzl@38705  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@43852  259 qed (auto simp add: Inf_bool_def Sup_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@43756  389 lemma (in complete_lattice) Inf_union_distrib: "\(A \ B) = \A \ \B"  haftmann@43756  390  by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)  haftmann@41082  391 haftmann@41082  392 lemma Inter_Un_distrib: "\(A \ B) = \A \ \B"  haftmann@43756  393  by (fact Inf_union_distrib)  haftmann@43756  394 haftmann@43801  395 lemma (in complete_lattice) Inf_top_conv [no_atp]:  haftmann@43801  396  "\A = \ \ (\x\A. x =$$"  haftmann@43801  397  "\ = \A \ (\x\A. x = \)"  haftmann@43801  398 proof -  haftmann@43801  399  show "\A = \ \ (\x\A. x = \)"  haftmann@43801  400  proof  haftmann@43801  401  assume "\x\A. x = \"  haftmann@43801  402  then have "A = {} \ A = {\}" by auto  haftmann@43801  403  then show "\A = \" by auto  haftmann@43801  404  next  haftmann@43801  405  assume "\A = \"  haftmann@43801  406  show "\x\A. x = \"  haftmann@43801  407  proof (rule ccontr)  haftmann@43801  408  assume "\ (\x\A. x = \)"  haftmann@43801  409  then obtain x where "x \ A" and "x \ \" by blast  haftmann@43801  410  then obtain B where "A = insert x B" by blast  haftmann@43801  411  with \A = \ x \ \ show False by (simp add: Inf_insert)  haftmann@43801  412  qed  haftmann@43801  413  qed  haftmann@43801  414  then show "\ = \A \ (\x\A. x = \)" by auto  haftmann@43801  415 qed  haftmann@41082  416 haftmann@41082  417 lemma Inter_UNIV_conv [simp,no_atp]:  haftmann@43741  418  "\A = UNIV \ (\x\A. x = UNIV)"  haftmann@43741  419  "UNIV = \A \ (\x\A. x = UNIV)"  haftmann@43801  420  by (fact Inf_top_conv)+  haftmann@41082  421 haftmann@43756  422 lemma (in complete_lattice) Inf_anti_mono: "B \ A \ \A \ \B"  haftmann@43756  423  by (auto intro: Inf_greatest Inf_lower)  haftmann@43756  424 haftmann@43741  425 lemma Inter_anti_mono: "B \ A \ \A \ \B"  haftmann@43756  426  by (fact Inf_anti_mono)  haftmann@41082  427 haftmann@41082  428 haftmann@41082  429 subsection {* Intersections of families *}  haftmann@41082  430 haftmann@41082  431 abbreviation INTER :: "'a set \ ('a \ 'b set) \ 'b set" where  haftmann@41082  432  "INTER \ INFI"  haftmann@41082  433 haftmann@41082  434 syntax  haftmann@41082  435  "_INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)  haftmann@41082  436  "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10)  haftmann@41082  437 haftmann@41082  438 syntax (xsymbols)  haftmann@41082  439  "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" [0, 10] 10)  haftmann@41082  440  "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10)  haftmann@41082  441 haftmann@41082  442 syntax (latex output)  haftmann@41082  443  "_INTER1" :: "pttrns => 'b set => 'b set" ("(3$$00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)  haftmann@41082  444  "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^esub>)/ _)" [0, 0, 10] 10)  haftmann@41082  445 haftmann@41082  446 translations  haftmann@41082  447  "INT x y. B" == "INT x. INT y. B"  haftmann@41082  448  "INT x. B" == "CONST INTER CONST UNIV (%x. B)"  haftmann@41082  449  "INT x. B" == "INT x:CONST UNIV. B"  haftmann@41082  450  "INT x:A. B" == "CONST INTER A (%x. B)"  haftmann@41082  451 haftmann@41082  452 print_translation {*  wenzelm@42284  453  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]  haftmann@41082  454 *} -- {* to avoid eta-contraction of body *}  haftmann@41082  455 haftmann@41082  456 lemma INTER_eq_Inter_image:  haftmann@41082  457  "(\x\A. B x) = \(BA)"  haftmann@41082  458  by (fact INFI_def)  haftmann@41082  459   haftmann@41082  460 lemma Inter_def:  haftmann@41082  461  "\S = (\x\S. x)"  haftmann@41082  462  by (simp add: INTER_eq_Inter_image image_def)  haftmann@41082  463 haftmann@41082  464 lemma INTER_def:  haftmann@41082  465  "(\x\A. B x) = {y. \x\A. y \ B x}"  haftmann@41082  466  by (auto simp add: INTER_eq_Inter_image Inter_eq)  haftmann@41082  467 haftmann@41082  468 lemma Inter_image_eq [simp]:  haftmann@41082  469  "\(BA) = (\x\A. B x)"  haftmann@43801  470  by (rule sym) (fact INFI_def)  haftmann@41082  471 haftmann@43817  472 lemma INT_iff [simp]: "b \ (\x\A. B x) \ (\x\A. b \ B x)"  haftmann@41082  473  by (unfold INTER_def) blast  haftmann@41082  474 haftmann@43817  475 lemma INT_I [intro!]: "(\x. x \ A \ b \ B x) \ b \ (\x\A. B x)"  haftmann@41082  476  by (unfold INTER_def) blast  haftmann@41082  477 haftmann@43852  478 lemma INT_D [elim, Pure.elim]: "b \ (\x\A. B x) \ a \ A \ b \ B a"  haftmann@41082  479  by auto  haftmann@41082  480 haftmann@43852  481 lemma INT_E [elim]: "b \ (\x\A. B x) \ (b \ B a \ R) \ (a \ A \ R) \ R"  haftmann@43852  482  -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\A"}. *}  haftmann@41082  483  by (unfold INTER_def) blast  haftmann@41082  484 haftmann@41082  485 lemma INT_cong [cong]:  haftmann@43854  486  "A = B \ (\x. x \ B \ C x = D x) \ (\x\A. C x) = (\x\B. D x)"  haftmann@43865  487  by (fact INF_cong)  haftmann@41082  488 haftmann@41082  489 lemma Collect_ball_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})"  haftmann@41082  490  by blast  haftmann@41082  491 haftmann@41082  492 lemma Collect_all_eq: "{x. \y. P x y} = (\y. {x. P x y})"  haftmann@41082  493  by blast  haftmann@41082  494 haftmann@43817  495 lemma INT_lower: "a \ A \ (\x\A. B x) \ B a"  haftmann@41082  496  by (fact INF_leI)  haftmann@41082  497 haftmann@43817  498 lemma INT_greatest: "(\x. x \ A \ C \ B x) \ C \ (\x\A. B x)"  haftmann@41082  499  by (fact le_INFI)  haftmann@41082  500 haftmann@43854  501 lemma (in complete_lattice) INFI_empty:  haftmann@43854  502  "(\x\{}. B x) = \"  haftmann@43854  503  by (simp add: INFI_def)  haftmann@43854  504 haftmann@41082  505 lemma INT_empty [simp]: "(\x\{}. B x) = UNIV"  haftmann@43854  506  by (fact INFI_empty)  haftmann@43854  507 haftmann@43854  508 lemma (in complete_lattice) INFI_absorb:  haftmann@43854  509  assumes "k \ I"  haftmann@43854  510  shows "A k \ (\i\I. A i) = (\i\I. A i)"  haftmann@43854  511 proof -  haftmann@43854  512  from assms obtain J where "I = insert k J" by blast  haftmann@43865  513  then show ?thesis by (simp add: INF_insert)  haftmann@43854  514 qed  haftmann@41082  515 haftmann@43817  516 lemma INT_absorb: "k \ I \ A k \ (\i\I. A i) = (\i\I. A i)"  haftmann@43854  517  by (fact INFI_absorb)  haftmann@41082  518 haftmann@43854  519 lemma INT_subset_iff: "B \ (\i\I. A i) \ (\i\I. B \ A i)"  haftmann@41082  520  by (fact le_INF_iff)  haftmann@41082  521 haftmann@41082  522 lemma INT_insert [simp]: "(\x \ insert a A. B x) = B a \ INTER A B"  haftmann@43865  523  by (fact INF_insert)  haftmann@43865  524 haftmann@43865  525 lemma (in complete_lattice) INF_union:  haftmann@43865  526  "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)"  haftmann@43865  527  by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INFI INF_leI)  haftmann@43865  528 haftmann@43865  529 lemma INT_Un: "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)"  haftmann@43865  530  by (fact INF_union)  haftmann@43865  531 haftmann@43865  532 lemma INT_insert_distrib:  haftmann@43865  533  "u \ A \ (\x\A. insert a (B x)) = insert a (\x\A. B x)"  haftmann@43865  534  by blast  haftmann@43854  535 haftmann@43865  536 lemma (in complete_lattice) INF_constant:  haftmann@43865  537  "(\y\A. c) = (if A = {} then \ else c)"  haftmann@43865  538  by (simp add: INF_empty)  haftmann@41082  539 haftmann@41082  540 lemma INT_constant [simp]: "(\y\A. c) = (if A = {} then UNIV else c)"  haftmann@43865  541  by (fact INF_constant)  haftmann@43865  542 haftmann@43865  543 lemma (in complete_lattice) INF_eq:  haftmann@43865  544  "(\x\A. B x) = \({Y. \x\A. Y = B x})"  haftmann@43865  545  by (simp add: INFI_def image_def)  haftmann@41082  546 haftmann@41082  547 lemma INT_eq: "(\x\A. B x) = \({Y. \x\A. Y = B x})"  haftmann@41082  548  -- {* Look: it has an \emph{existential} quantifier *}  haftmann@43865  549  by (fact INF_eq)  haftmann@43865  550 haftmann@43865  551 lemma (in complete_lattice) INF_top_conv:  haftmann@43865  552  "\ = (\x\A. B x) \ (\x\A. B x =$$"  haftmann@43865  553  "(\x\A. B x) = \ \ (\x\A. B x = \)"  haftmann@43865  554  by (auto simp add: INFI_def Inf_top_conv)  haftmann@41082  555 haftmann@43854  556 lemma INTER_UNIV_conv [simp]:  haftmann@43817  557  "(UNIV = (\x\A. B x)) = (\x\A. B x = UNIV)"  haftmann@43817  558  "((\x\A. B x) = UNIV) = (\x\A. B x = UNIV)"  haftmann@43865  559  by (fact INF_top_conv)+  haftmann@43865  560 haftmann@43865  561 lemma (in complete_lattice) INFI_UNIV_range:  haftmann@43865  562  "(\x\UNIV. f x) = \range f"  haftmann@43865  563  by (simp add: INFI_def)  haftmann@43865  564 haftmann@43865  565 lemma (in complete_lattice) INF_bool_eq:  haftmann@43865  566  "(\b. A b) = A True \ A False"  haftmann@43865  567  by (simp add: UNIV_bool INF_empty INF_insert inf_commute)  haftmann@43865  568 haftmann@43865  569 lemma INT_bool_eq: "(\b. A b) = A True \ A False"  haftmann@43865  570  by (fact INF_bool_eq)  haftmann@43865  571 haftmann@43865  572 lemma (in complete_lattice) INF_anti_mono:  haftmann@43867  573  "B \ A \ (\x. x \ A \ f x \ g x) \ (\x\B. f x) \ (\x\B. g x)"  haftmann@43865  574  -- {* The last inclusion is POSITIVE! *}  haftmann@43867  575  by (blast intro: INF_mono dest: subsetD)  haftmann@43865  576 haftmann@43865  577 lemma INT_anti_mono:  haftmann@43867  578  "B \ A \ (\x. x \ A \ f x \ g x) \ (\x\B. f x) \ (\x\B. g x)"  haftmann@43865  579  -- {* The last inclusion is POSITIVE! *}  haftmann@43867  580  by (fact INF_anti_mono)  haftmann@41082  581 haftmann@41082  582 lemma Pow_INT_eq: "Pow (\x\A. B x) = (\x\A. Pow (B x))"  haftmann@41082  583  by blast  haftmann@41082  584 haftmann@43817  585 lemma vimage_INT: "f - (\x\A. B x) = (\x\A. f - B x)"  haftmann@41082  586  by blast  haftmann@41082  587 haftmann@41082  588 haftmann@32139  589 subsection {* Union *}  haftmann@32115  590 haftmann@32587  591 abbreviation Union :: "'a set set \ 'a set" where  haftmann@32587  592  "Union S \ \S"  haftmann@32115  593 haftmann@32115  594 notation (xsymbols)  haftmann@32115  595  Union ("\_" [90] 90)  haftmann@32115  596 haftmann@32135  597 lemma Union_eq:  haftmann@32135  598  "\A = {x. \B \ A. x \ B}"  nipkow@39302  599 proof (rule set_eqI)  haftmann@32115  600  fix x  haftmann@32135  601  have "(\Q\{P. \B\A. P \ x \ B}. Q) \ (\B\A. x \ B)"  haftmann@32115  602  by auto  haftmann@32135  603  then show "x \ \A \ x \ {x. \B\A. x \ B}"  haftmann@32587  604  by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)  haftmann@32115  605 qed  haftmann@32115  606 blanchet@35828  607 lemma Union_iff [simp, no_atp]:  haftmann@32115  608  "A \ \C \ (\X\C. A\X)"  haftmann@32115  609  by (unfold Union_eq) blast  haftmann@32115  610 haftmann@32115  611 lemma UnionI [intro]:  haftmann@32115  612  "X \ C \ A \ X \ A \ \C"  haftmann@32115  613  -- {* The order of the premises presupposes that @{term C} is rigid;  haftmann@32115  614  @{term A} may be flexible. *}  haftmann@32115  615  by auto  haftmann@32115  616 haftmann@32115  617 lemma UnionE [elim!]:  haftmann@43817  618  "A \ \C \ (\X. A \ X \ X \ C \ R) \ R"  haftmann@32115  619  by auto  haftmann@32115  620 haftmann@43817  621 lemma Union_upper: "B \ A \ B \ \A"  haftmann@32135  622  by (iprover intro: subsetI UnionI)  haftmann@32135  623 haftmann@43817  624 lemma Union_least: "(\X. X \ A \ X \ C) \ \A \ C"  haftmann@32135  625  by (iprover intro: subsetI elim: UnionE dest: subsetD)  haftmann@32135  626 haftmann@32135  627 lemma Un_eq_Union: "A \ B = \{A, B}"  haftmann@32135  628  by blast  haftmann@32135  629 haftmann@43817  630 lemma Union_empty [simp]: "\{} = {}"  haftmann@32135  631  by blast  haftmann@32135  632 haftmann@43817  633 lemma Union_UNIV [simp]: "\UNIV = UNIV"  haftmann@32135  634  by blast  haftmann@32135  635 haftmann@43817  636 lemma Union_insert [simp]: "\insert a B = a \ \B"  haftmann@32135  637  by blast  haftmann@32135  638 haftmann@43817  639 lemma Union_Un_distrib [simp]: "\(A \ B) = \A \ \B"  haftmann@32135  640  by blast  haftmann@32135  641 haftmann@32135  642 lemma Union_Int_subset: "\(A \ B) \ \A \ \B"  haftmann@32135  643  by blast  haftmann@32135  644 haftmann@43817  645 lemma Union_empty_conv [simp,no_atp]: "(\A = {}) \ (\x\A. x = {})"  haftmann@32135  646  by blast  haftmann@32135  647 haftmann@43817  648 lemma empty_Union_conv [simp,no_atp]: "({} = \A) \ (\x\A. x = {})"  haftmann@32135  649  by blast  haftmann@32135  650 haftmann@43817  651 lemma Union_disjoint: "(\C \ A = {}) \ (\B\C. B \ A = {})"  haftmann@32135  652  by blast  haftmann@32135  653 haftmann@32135  654 lemma subset_Pow_Union: "A \ Pow (\A)"  haftmann@32135  655  by blast  haftmann@32135  656 haftmann@32135  657 lemma Union_Pow_eq [simp]: "\(Pow A) = A"  haftmann@32135  658  by blast  haftmann@32135  659 haftmann@43817  660 lemma Union_mono: "A \ B \ \A \ \B"  haftmann@32135  661  by blast  haftmann@32135  662 haftmann@32115  663 haftmann@32139  664 subsection {* Unions of families *}  haftmann@32077  665 haftmann@32606  666 abbreviation UNION :: "'a set \ ('a \ 'b set) \ 'b set" where  haftmann@32606  667  "UNION \ SUPR"  haftmann@32077  668 haftmann@32077  669 syntax  wenzelm@35115  670  "_UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)  huffman@36364  671  "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 0, 10] 10)  haftmann@32077  672 haftmann@32077  673 syntax (xsymbols)  wenzelm@35115  674  "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" [0, 10] 10)  huffman@36364  675  "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10)  haftmann@32077  676 haftmann@32077  677 syntax (latex output)  wenzelm@35115  678  "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)  huffman@36364  679  "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^esub>)/ _)" [0, 0, 10] 10)  haftmann@32077  680 haftmann@32077  681 translations  haftmann@32077  682  "UN x y. B" == "UN x. UN y. B"  haftmann@32077  683  "UN x. B" == "CONST UNION CONST UNIV (%x. B)"  haftmann@32077  684  "UN x. B" == "UN x:CONST UNIV. B"  haftmann@32077  685  "UN x:A. B" == "CONST UNION A (%x. B)"  haftmann@32077  686 haftmann@32077  687 text {*  haftmann@32077  688  Note the difference between ordinary xsymbol syntax of indexed  haftmann@32077  689  unions and intersections (e.g.\ @{text"\a\<^isub>1\A\<^isub>1. B"})  haftmann@32077  690  and their \LaTeX\ rendition: @{term"\a\<^isub>1\A\<^isub>1. B"}. The  haftmann@32077  691  former does not make the index expression a subscript of the  haftmann@32077  692  union/intersection symbol because this leads to problems with nested  haftmann@32077  693  subscripts in Proof General.  haftmann@32077  694 *}  haftmann@32077  695 wenzelm@35115  696 print_translation {*  wenzelm@42284  697  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]  wenzelm@35115  698 *} -- {* to avoid eta-contraction of body *}  haftmann@32077  699 haftmann@32135  700 lemma UNION_eq_Union_image:  haftmann@43817  701  "(\x\A. B x) = \(B  A)"  haftmann@32606  702  by (fact SUPR_def)  haftmann@32115  703 haftmann@32115  704 lemma Union_def:  haftmann@32117  705  "\S = (\x\S. x)"  haftmann@32115  706  by (simp add: UNION_eq_Union_image image_def)  haftmann@32115  707 blanchet@35828  708 lemma UNION_def [no_atp]:  haftmann@32135  709  "(\x\A. B x) = {y. \x\A. y \ B x}"  haftmann@32117  710  by (auto simp add: UNION_eq_Union_image Union_eq)  haftmann@32115  711   haftmann@32115  712 lemma Union_image_eq [simp]:  haftmann@43817  713  "\(B  A) = (\x\A. B x)"  haftmann@32115  714  by (rule sym) (fact UNION_eq_Union_image)  haftmann@32115  715   haftmann@43852  716 lemma UN_iff [simp]: "(b \ (\x\A. B x)) = (\x\A. b \ B x)"  wenzelm@11979  717  by (unfold UNION_def) blast  wenzelm@11979  718 haftmann@43852  719 lemma UN_I [intro]: "a \ A \ b \ B a \ b \ (\x\A. B x)"  wenzelm@11979  720  -- {* The order of the premises presupposes that @{term A} is rigid;  wenzelm@11979  721  @{term b} may be flexible. *}  wenzelm@11979  722  by auto  wenzelm@11979  723 haftmann@43852  724 lemma UN_E [elim!]: "b \ (\x\A. B x) \ (\x. x\A \ b \ B x \ R) \ R"  wenzelm@11979  725  by (unfold UNION_def) blast  clasohm@923  726 wenzelm@11979  727 lemma UN_cong [cong]:  haftmann@43852  728  "A = B \ (\x. x \ B \ C x = D x) \ (\x\A. C x) = (\x\B. D x)"  wenzelm@11979  729  by (simp add: UNION_def)  wenzelm@11979  730 berghofe@29691  731 lemma strong_UN_cong:  haftmann@43852  732  "A = B \ (\x. x \ B =simp=> C x = D x) \ (\x\A. C x) = (\x\B. D x)"  berghofe@29691  733  by (simp add: UNION_def simp_implies_def)  berghofe@29691  734 haftmann@43817  735 lemma image_eq_UN: "f  A = (\x\A. {f x})"  haftmann@32077  736  by blast  haftmann@32077  737 haftmann@43817  738 lemma UN_upper: "a \ A \ B a \ (\x\A. B x)"  haftmann@32606  739  by (fact le_SUPI)  haftmann@32135  740 haftmann@43817  741 lemma UN_least: "(\x. x \ A \ B x \ C) \ (\x\A. B x) \ C"  haftmann@32135  742  by (iprover intro: subsetI elim: UN_E dest: subsetD)  haftmann@32135  743 blanchet@35828  744 lemma Collect_bex_eq [no_atp]: "{x. \y\A. P x y} = (\y\A. {x. P x y})"  haftmann@32135  745  by blast  haftmann@32135  746 haftmann@43817  747 lemma UN_insert_distrib: "u \ A \ (\x\A. insert a (B x)) = insert a (\x\A. B x)"  haftmann@32135  748  by blast  haftmann@32135  749 blanchet@35828  750 lemma UN_empty [simp,no_atp]: "(\x\{}. B x) = {}"  haftmann@32135  751  by blast  haftmann@32135  752 haftmann@32135  753 lemma UN_empty2 [simp]: "(\x\A. {}) = {}"  haftmann@32135  754  by blast  haftmann@32135  755 haftmann@32135  756 lemma UN_singleton [simp]: "(\x\A. {x}) = A"  haftmann@32135  757  by blast  haftmann@32135  758 haftmann@43817  759 lemma UN_absorb: "k \ I \ A k \ (\i\I. A i) = (\i\I. A i)"  haftmann@32135  760  by auto  haftmann@32135  761 haftmann@32135  762 lemma UN_insert [simp]: "(\x\insert a A. B x) = B a \ UNION A B"  haftmann@32135  763  by blast  haftmann@32135  764 haftmann@32135  765 lemma UN_Un[simp]: "(\i \ A \ B. M i) = (\i\A. M i) \ (\i\B. M i)"  haftmann@32135  766  by blast  haftmann@32135  767 haftmann@32135  768 lemma UN_UN_flatten: "(\x \ (\y\A. B y). C x) = (\y\A. \x\B y. C x)"  haftmann@32135  769  by blast  haftmann@32135  770 haftmann@32135  771 lemma UN_subset_iff: "((\i\I. A i) \ B) = (\i\I. A i \ B)"  huffman@35629  772  by (fact SUP_le_iff)  haftmann@32135  773 haftmann@32135  774 lemma image_Union: "f  \S = (\x\S. f  x)"  haftmann@32135  775  by blast  haftmann@32135  776 haftmann@32135  777 lemma UN_constant [simp]: "(\y\A. c) = (if A = {} then {} else c)"  haftmann@32135  778  by auto  haftmann@32135  779 haftmann@32135  780 lemma UN_eq: "(\x\A. B x) = \({Y. \x\A. Y = B x})"  haftmann@32135  781  by blast  haftmann@32135  782 haftmann@32135  783 lemma UNION_empty_conv[simp]:  haftmann@43817  784  "{} = (\x\A. B x) \ (\x\A. B x = {})"  haftmann@43817  785  "(\x\A. B x) = {} \ (\x\A. B x = {})"  haftmann@32135  786 by blast+  haftmann@32135  787 blanchet@35828  788 lemma Collect_ex_eq [no_atp]: "{x. \y. P x y} = (\y. {x. P x y})"  haftmann@32135  789  by blast  haftmann@32135  790 haftmann@32135  791 lemma ball_UN: "(\z \ UNION A B. P z) = (\x\A. \z \ B x. P z)"  haftmann@32135  792  by blast  haftmann@32135  793 haftmann@32135  794 lemma bex_UN: "(\z \ UNION A B. P z) = (\x\A. \z\B x. P z)"  haftmann@32135  795  by blast  haftmann@32135  796 haftmann@32135  797 lemma Un_eq_UN: "A \ B = (\b. if b then A else B)"  haftmann@32135  798  by (auto simp add: split_if_mem2)  haftmann@32135  799 haftmann@43817  800 lemma UN_bool_eq: "(\b. A b) = (A True \ A False)"  haftmann@32135  801  by (auto intro: bool_contrapos)  haftmann@32135  802 haftmann@32135  803 lemma UN_Pow_subset: "(\x\A. Pow (B x)) \ Pow (\x\A. B x)"  haftmann@32135  804  by blast  haftmann@32135  805 haftmann@32135  806 lemma UN_mono:  haftmann@43817  807  "A \ B \ (\x. x \ A \ f x \ g x) \  haftmann@32135  808  (\x\A. f x) \ (\x\B. g x)"  haftmann@32135  809  by (blast dest: subsetD)  haftmann@32135  810 haftmann@43817  811 lemma vimage_Union: "f - (\A) = (\X\A. f - X)"  haftmann@32135  812  by blast  haftmann@32135  813 haftmann@43817  814 lemma vimage_UN: "f - (\x\A. B x) = (\x\A. f - B x)"  haftmann@32135  815  by blast  haftmann@32135  816 haftmann@43817  817 lemma vimage_eq_UN: "f - B = (\y\B. f - {y})"  haftmann@32135  818  -- {* NOT suitable for rewriting *}  haftmann@32135  819  by blast  haftmann@32135  820 haftmann@43817  821 lemma image_UN: "f  UNION A B = (\x\A. f  B x)"  haftmann@43817  822  by blast  haftmann@32135  823 wenzelm@11979  824 haftmann@32139  825 subsection {* Distributive laws *}  wenzelm@12897  826 wenzelm@12897  827 lemma Int_Union: "A \ \B = (\C\B. A \ C)"  wenzelm@12897  828  by blast  wenzelm@12897  829 wenzelm@12897  830 lemma Int_Union2: "\B \ A = (\C\B. C \ A)"  wenzelm@12897  831  by blast  wenzelm@12897  832 haftmann@43817  833 lemma Un_Union_image: "(\x\C. A x \ B x) = \(A  C) \ \(B  C)"  wenzelm@12897  834  -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}  wenzelm@12897  835  -- {* Union of a family of unions *}  wenzelm@12897  836  by blast  wenzelm@12897  837 wenzelm@12897  838 lemma UN_Un_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)"  wenzelm@12897  839  -- {* Equivalent version *}  wenzelm@12897  840  by blast  wenzelm@12897  841 wenzelm@12897  842 lemma Un_Inter: "A \ \B = (\C\B. A \ C)"  wenzelm@12897  843  by blast  wenzelm@12897  844 haftmann@43817  845 lemma Int_Inter_image: "(\x\C. A x \ B x) = \(A  C) \ \(B  C)"  wenzelm@12897  846  by blast  wenzelm@12897  847 wenzelm@12897  848 lemma INT_Int_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)"  wenzelm@12897  849  -- {* Equivalent version *}  wenzelm@12897  850  by blast  wenzelm@12897  851 wenzelm@12897  852 lemma Int_UN_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)"  wenzelm@12897  853  -- {* Halmos, Naive Set Theory, page 35. *}  wenzelm@12897  854  by blast  wenzelm@12897  855 wenzelm@12897  856 lemma Un_INT_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)"  wenzelm@12897  857  by blast  wenzelm@12897  858 wenzelm@12897  859 lemma Int_UN_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)"  wenzelm@12897  860  by blast  wenzelm@12897  861 wenzelm@12897  862 lemma Un_INT_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)"  wenzelm@12897  863  by blast  wenzelm@12897  864 wenzelm@12897  865 haftmann@32139  866 subsection {* Complement *}  haftmann@32135  867 haftmann@43817  868 lemma Compl_UN [simp]: "- (\x\A. B x) = (\x\A. -B x)"  wenzelm@12897  869  by blast  wenzelm@12897  870 haftmann@43817  871 lemma Compl_INT [simp]: "- (\x\A. B x) = (\x\A. -B x)"  wenzelm@12897  872  by blast  wenzelm@12897  873 wenzelm@12897  874 haftmann@32139  875 subsection {* Miniscoping and maxiscoping *}  wenzelm@12897  876 paulson@13860  877 text {* \medskip Miniscoping: pushing in quantifiers and big Unions  paulson@13860  878  and Intersections. *}  wenzelm@12897  879 wenzelm@12897  880 lemma UN_simps [simp]:  haftmann@43817  881  "\a B C. (\x\C. insert a (B x)) = (if C={} then {} else insert a (\x\C. B x))"  haftmann@43852  882  "\A B C. (\x\C. A x \ B) = ((if C={} then {} else (\x\C. A x) \ B))"  haftmann@43852  883  "\A B C. (\x\C. A \ B x) = ((if C={} then {} else A \ (\x\C. B x)))"  haftmann@43852  884  "\A B C. (\x\C. A x \ B) = ((\x\C. A x) \B)"  haftmann@43852  885  "\A B C. (\x\C. A \ B x) = (A \(\x\C. B x))"  haftmann@43852  886  "\A B C. (\x\C. A x - B) = ((\x\C. A x) - B)"  haftmann@43852  887  "\A B C. (\x\C. A - B x) = (A - (\x\C. B x))"  haftmann@43852  888  "\A B. (\x\\A. B x) = (\y\A. \x\y. B x)"  haftmann@43852  889  "\A B C. (\z\UNION A B. C z) = (\x\A. \z\B x. C z)"  haftmann@43831  890  "\A B f. (\x\fA. B x) = (\a\A. B (f a))"  wenzelm@12897  891  by auto  wenzelm@12897  892 wenzelm@12897  893 lemma INT_simps [simp]:  haftmann@43831  894  "\A B C. (\x\C. A x \ B) = (if C={} then UNIV else (\x\C. A x) \B)"  haftmann@43831  895  "\A B C. (\x\C. A \ B x) = (if C={} then UNIV else A \(\x\C. B x))"  haftmann@43852  896  "\A B C. (\x\C. A x - B) = (if C={} then UNIV else (\x\C. A x) - B)"  haftmann@43852  897  "\A B C. (\x\C. A - B x) = (if C={} then UNIV else A - (\x\C. B x))"  haftmann@43817  898  "\a B C. (\x\C. insert a (B x)) = insert a (\x\C. B x)"  haftmann@43852  899  "\A B C. (\x\C. A x \ B) = ((\x\C. A x) \ B)"  haftmann@43852  900  "\A B C. (\x\C. A \ B x) = (A \ (\x\C. B x))"  haftmann@43852  901  "\A B. (\x\\A. B x) = (\y\A. \x\y. B x)"  haftmann@43852  902  "\A B C. (\z\UNION A B. C z) = (\x\A. \z\B x. C z)"  haftmann@43852  903  "\A B f. (\x\fA. B x) = (\a\A. B (f a))"  wenzelm@12897  904  by auto  wenzelm@12897  905 blanchet@35828  906 lemma ball_simps [simp,no_atp]:  haftmann@43852  907  "\A P Q. (\x\A. P x \ Q) \ ((\x\A. P x) \ Q)"  haftmann@43852  908  "\A P Q. (\x\A. P \ Q x) \ (P \ (\x\A. Q x))"  haftmann@43852  909  "\A P Q. (\x\A. P \ Q x) \ (P \ (\x\A. Q x))"  haftmann@43852  910  "\A P Q. (\x\A. P x \ Q) \ ((\x\A. P x) \ Q)"  haftmann@43852  911  "\P. (\x\{}. P x) \ True"  haftmann@43852  912  "\P. (\x\UNIV. P x) \ (\x. P x)"  haftmann@43852  913  "\a B P. (\x\insert a B. P x) \ (P a \ (\x\B. P x))"  haftmann@43852  914  "\A P. (\x\\A. P x) \ (\y\A. \x\y. P x)"  haftmann@43852  915  "\A B P. (\x\ UNION A B. P x) = (\a\A. \x\ B a. P x)"  haftmann@43852  916  "\P Q. (\x\Collect Q. P x) \ (\x. Q x \ P x)"  haftmann@43852  917  "\A P f. (\x\fA. P x) \ (\x\A. P (f x))"  haftmann@43852  918  "\A P. (\ (\x\A. P x)) \ (\x\A. \ P x)"  wenzelm@12897  919  by auto  wenzelm@12897  920 blanchet@35828  921 lemma bex_simps [simp,no_atp]:  haftmann@43852  922  "\A P Q. (\x\A. P x \ Q) \ ((\x\A. P x) \ Q)"  haftmann@43852  923  "\A P Q. (\x\A. P \ Q x) \ (P \ (\x\A. Q x))"  haftmann@43852  924  "\P. (\x\{}. P x) \ False"  haftmann@43852  925  "\P. (\x\UNIV. P x) \ (\x. P x)"  haftmann@43852  926  "\a B P. (\x\insert a B. P x) \ (P a | (\x\B. P x))"  haftmann@43852  927  "\A P. (\x\\A. P x) \ (\y\A. \x\y. P x)"  haftmann@43852  928  "\A B P. (\x\UNION A B. P x) \ (\a\A. \x\B a. P x)"  haftmann@43852  929  "\P Q. (\x\Collect Q. P x) \ (\x. Q x \ P x)"  haftmann@43852  930  "\A P f. (\x\fA. P x) \ (\x\A. P (f x))"  haftmann@43852  931  "\A P. (\(\x\A. P x)) \ (\x\A. \ P x)"  wenzelm@12897  932  by auto  wenzelm@12897  933 paulson@13860  934 text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}  paulson@13860  935 paulson@13860  936 lemma UN_extend_simps:  haftmann@43817  937  "\a B C. insert a (\x\C. B x) = (if C={} then {a} else (\x\C. insert a (B x)))"  haftmann@43852  938  "\A B C. (\x\C. A x) \ B = (if C={} then B else (\x\C. A x \ B))"  haftmann@43852  939  "\A B C. A \ (\x\C. B x) = (if C={} then A else (\x\C. A \ B x))"  haftmann@43852  940  "\A B C. ((\x\C. A x) \ B) = (\x\C. A x \ B)"  haftmann@43852  941  "\A B C. (A \ (\x\C. B x)) = (\x\C. A \ B x)"  haftmann@43817  942  "\A B C. ((\x\C. A x) - B) = (\x\C. A x - B)"  haftmann@43817  943  "\A B C. (A - (\x\C. B x)) = (\x\C. A - B x)"  haftmann@43852  944  "\A B. (\y\A. \x\y. B x) = (\x\\A. B x)"  haftmann@43852  945  "\A B C. (\x\A. \z\B x. C z) = (\z\UNION A B. C z)"  haftmann@43831  946  "\A B f. (\a\A. B (f a)) = (\x\fA. B x)"  paulson@13860  947  by auto  paulson@13860  948 paulson@13860  949 lemma INT_extend_simps:  haftmann@43852  950  "\A B C. (\x\C. A x) \ B = (if C={} then B else (\x\C. A x \ B))"  haftmann@43852  951  "\A B C. A \ (\x\C. B x) = (if C={} then A else (\x\C. A \ B x))"  haftmann@43852  952  "\A B C. (\x\C. A x) - B = (if C={} then UNIV - B else (\x\C. A x - B))"  haftmann@43852  953  "\A B C. A - (\x\C. B x) = (if C={} then A else (\x\C. A - B x))"  haftmann@43817  954  "\a B C. insert a (\x\C. B x) = (\x\C. insert a (B x))"  haftmann@43852  955  "\A B C. ((\x\C. A x) \ B) = (\x\C. A x \ B)"  haftmann@43852  956  "\A B C. A \ (\x\C. B x) = (\x\C. A \ B x)"  haftmann@43852  957  "\A B. (\y\A. \x\y. B x) = (\x\\A. B x)"  haftmann@43852  958  "\A B C. (\x\A. \z\B x. C z) = (\z\UNION A B. C z)"  haftmann@43852  959  "\A B f. (\a\A. B (f a)) = (\x\fA. B x)"  paulson@13860  960  by auto  paulson@13860  961 paulson@13860  962 haftmann@32135  963 no_notation  haftmann@32135  964  less_eq (infix "\" 50) and  haftmann@32135  965  less (infix "\" 50) and  haftmann@41082  966  bot ("\") and  haftmann@41082  967  top ("\") and  haftmann@32135  968  inf (infixl "\" 70) and  haftmann@32135  969  sup (infixl "\" 65) and  haftmann@32135  970  Inf ("\_" [900] 900) and  haftmann@41082  971  Sup ("\_" [900] 900)  haftmann@32135  972 haftmann@41080  973 no_syntax (xsymbols)  haftmann@41082  974  "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)  haftmann@41082  975  "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)  haftmann@41080  976  "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)  haftmann@41080  977  "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)  haftmann@41080  978 haftmann@30596  979 lemmas mem_simps =  haftmann@30596  980  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff  haftmann@30596  981  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff  haftmann@30596  982  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}  wenzelm@21669  983 wenzelm@11979  984 end `