src/HOL/Complete_Lattice.thy
 author haftmann Sun Jul 10 14:26:07 2011 +0200 (2011-07-10) changeset 43740 3316e6831801 parent 43739 4529a3c56609 child 43741 fac11b64713c permissions -rw-r--r--
more succinct proofs
 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 huffman@35629  85 lemma le_Inf_iff: "b \ Inf A \ (\a\A. b \ a)"  huffman@35629  86  by (auto intro: Inf_greatest dest: Inf_lower)  huffman@35629  87 haftmann@41082  88 lemma Sup_le_iff: "Sup 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"  hoelzl@41971  93  shows "Inf A \ Inf 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  hoelzl@41971  97  from a \ A have "Inf A \ a" by (rule Inf_lower)  hoelzl@41971  98  with a \ b show "Inf 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"  hoelzl@41971  103  shows "Sup A \ Sup 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  hoelzl@41971  107  from b \ B have "b \ Sup B" by (rule Sup_upper)  hoelzl@41971  108  with a \ b show "a \ Sup B" by auto  haftmann@41082  109 qed  haftmann@32077  110 hoelzl@41971  111 lemma top_le:  hoelzl@41971  112  "top \ x \ x = top"  hoelzl@41971  113  by (rule antisym) auto  hoelzl@41971  114 hoelzl@41971  115 lemma le_bot:  hoelzl@41971  116  "x \ bot \ x = bot"  hoelzl@41971  117  by (rule antisym) auto  hoelzl@41971  118 hoelzl@41971  119 lemma not_less_bot[simp]: "\ (x \ bot)"  hoelzl@41971  120  using bot_least[of x] by (auto simp: le_less)  hoelzl@41971  121 hoelzl@41971  122 lemma not_top_less[simp]: "\ (top \ x)"  hoelzl@41971  123  using top_greatest[of x] by (auto simp: le_less)  hoelzl@41971  124 hoelzl@41971  125 lemma Sup_upper2: "u \ A \ v \ u \ v \ Sup A"  hoelzl@41971  126  using Sup_upper[of u A] by auto  hoelzl@41971  127 hoelzl@41971  128 lemma Inf_lower2: "u \ A \ u \ v \ Inf 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@34007  175 lemma le_SUPI: "i : A \ M i \ (SUP i:A. M i)"  haftmann@32077  176  by (auto simp add: SUPR_def intro: Sup_upper)  haftmann@32077  177 hoelzl@41971  178 lemma le_SUPI2: "i \ A \ u \ M i \ u \ (SUP i:A. M i)"  hoelzl@41971  179  using le_SUPI[of i A M] by auto  hoelzl@41971  180 haftmann@34007  181 lemma SUP_leI: "(\i. i : A \ M i \ u) \ (SUP i:A. M i) \ u"  haftmann@32077  182  by (auto simp add: SUPR_def intro: Sup_least)  haftmann@32077  183 haftmann@34007  184 lemma INF_leI: "i : A \ (INF i:A. M i) \ M i"  haftmann@32077  185  by (auto simp add: INFI_def intro: Inf_lower)  haftmann@32077  186 hoelzl@41971  187 lemma INF_leI2: "i \ A \ M i \ u \ (INF i:A. M i) \ u"  hoelzl@41971  188  using INF_leI[of i A M] by auto  hoelzl@41971  189 haftmann@34007  190 lemma le_INFI: "(\i. i : A \ u \ M i) \ u \ (INF i:A. M i)"  haftmann@32077  191  by (auto simp add: INFI_def intro: Inf_greatest)  haftmann@32077  192 huffman@35629  193 lemma SUP_le_iff: "(SUP 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 huffman@35629  196 lemma le_INF_iff: "u \ (INF 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@32077  199 lemma INF_const[simp]: "A \ {} \ (INF i:A. M) = M"  haftmann@32077  200  by (auto intro: antisym INF_leI le_INFI)  haftmann@32077  201 haftmann@41082  202 lemma SUP_const[simp]: "A \ {} \ (SUP i:A. M) = M"  haftmann@41082  203  by (auto intro: antisym SUP_leI le_SUPI)  hoelzl@38705  204 hoelzl@38705  205 lemma INF_mono:  hoelzl@38705  206  "(\m. m \ B \ \n\A. f n \ g m) \ (INF n:A. f n) \ (INF 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@41082  210  "(\n. n \ A \ \m\B. f n \ g m) \ (SUP n:A. f n) \ (SUP n:B. g n)"  haftmann@41082  211  by (force intro!: Sup_mono simp: SUPR_def)  hoelzl@40872  212 hoelzl@40872  213 lemma INF_subset: "A \ B \ INFI B f \ INFI A f"  hoelzl@40872  214  by (intro INF_mono) auto  hoelzl@40872  215 haftmann@41082  216 lemma SUP_subset: "A \ B \ SUPR A f \ SUPR B f"  haftmann@41082  217  by (intro SUP_mono) auto  hoelzl@40872  218 hoelzl@40872  219 lemma INF_commute: "(INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)"  hoelzl@40872  220  by (iprover intro: INF_leI le_INFI order_trans antisym)  hoelzl@40872  221 haftmann@41082  222 lemma SUP_commute: "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP 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@41082  229  shows "Inf S < a \ (\x\S. x < a)"  haftmann@41082  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}"  hoelzl@38705  234  shows "a < Sup S \ (\x\S. a < x)"  hoelzl@38705  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@41082  239  shows "(INF 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}"  hoelzl@40872  244  shows "a < (SUP 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@32120  268  show "(INF 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@32120  277  show "(SUP 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@41082  331 lemma Inter_iff [simp,no_atp]: "(A : Inter C) = (ALL X:C. A:X)"  haftmann@41082  332  by (unfold Inter_eq) blast  haftmann@41082  333 haftmann@41082  334 lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter 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@41082  339  contains @{term A} as an element, but @{prop "A:X"} can hold when  haftmann@41082  340  @{prop "X:C"} does not! This rule is analogous to @{text spec}.  haftmann@41082  341 *}  haftmann@41082  342 haftmann@41082  343 lemma InterD [elim, Pure.elim]: "A : Inter C ==> X:C ==> A:X"  haftmann@41082  344  by auto  haftmann@41082  345 haftmann@41082  346 lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"  haftmann@41082  347  -- {* Classical'' elimination rule -- does not require proving  haftmann@41082  348  @{prop "X:C"}. *}  haftmann@41082  349  by (unfold Inter_eq) blast  haftmann@41082  350 haftmann@41082  351 lemma Inter_lower: "B \ A ==> Inter 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@43740  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@41082  365  "[| !!X. X \ A ==> X \ B; A ~= {} |] ==> \A \ B"  haftmann@43740  366  by (fact Inf_less_eq)  haftmann@41082  367 haftmann@41082  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@41082  383 lemma Inter_Un_subset: "\A \ \B \ \(A \ B)"  haftmann@41082  384  by blast  haftmann@41082  385 haftmann@41082  386 lemma Inter_Un_distrib: "\(A \ B) = \A \ \B"  haftmann@41082  387  by blast  haftmann@41082  388 haftmann@41082  389 lemma Inter_UNIV_conv [simp,no_atp]:  haftmann@41082  390  "(\A = UNIV) = (\x\A. x = UNIV)"  haftmann@41082  391  "(UNIV = \A) = (\x\A. x = UNIV)"  haftmann@41082  392  by blast+  haftmann@41082  393 haftmann@41082  394 lemma Inter_anti_mono: "B \ A ==> \A \ \B"  haftmann@41082  395  by blast  haftmann@41082  396 haftmann@41082  397 haftmann@41082  398 subsection {* Intersections of families *}  haftmann@41082  399 haftmann@41082  400 abbreviation INTER :: "'a set \ ('a \ 'b set) \ 'b set" where  haftmann@41082  401  "INTER \ INFI"  haftmann@41082  402 haftmann@41082  403 syntax  haftmann@41082  404  "_INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)  haftmann@41082  405  "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10)  haftmann@41082  406 haftmann@41082  407 syntax (xsymbols)  haftmann@41082  408  "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" [0, 10] 10)  haftmann@41082  409  "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10)  haftmann@41082  410 haftmann@41082  411 syntax (latex output)  haftmann@41082  412  "_INTER1" :: "pttrns => 'b set => 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)  haftmann@41082  413  "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^esub>)/ _)" [0, 0, 10] 10)  haftmann@41082  414 haftmann@41082  415 translations  haftmann@41082  416  "INT x y. B" == "INT x. INT y. B"  haftmann@41082  417  "INT x. B" == "CONST INTER CONST UNIV (%x. B)"  haftmann@41082  418  "INT x. B" == "INT x:CONST UNIV. B"  haftmann@41082  419  "INT x:A. B" == "CONST INTER A (%x. B)"  haftmann@41082  420 haftmann@41082  421 print_translation {*  wenzelm@42284  422  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]  haftmann@41082  423 *} -- {* to avoid eta-contraction of body *}  haftmann@41082  424 haftmann@41082  425 lemma INTER_eq_Inter_image:  haftmann@41082  426  "(\x\A. B x) = \(BA)"  haftmann@41082  427  by (fact INFI_def)  haftmann@41082  428   haftmann@41082  429 lemma Inter_def:  haftmann@41082  430  "\S = (\x\S. x)"  haftmann@41082  431  by (simp add: INTER_eq_Inter_image image_def)  haftmann@41082  432 haftmann@41082  433 lemma INTER_def:  haftmann@41082  434  "(\x\A. B x) = {y. \x\A. y \ B x}"  haftmann@41082  435  by (auto simp add: INTER_eq_Inter_image Inter_eq)  haftmann@41082  436 haftmann@41082  437 lemma Inter_image_eq [simp]:  haftmann@41082  438  "\(BA) = (\x\A. B x)"  haftmann@41082  439  by (rule sym) (fact INTER_eq_Inter_image)  haftmann@41082  440 haftmann@41082  441 lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"  haftmann@41082  442  by (unfold INTER_def) blast  haftmann@41082  443 haftmann@41082  444 lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"  haftmann@41082  445  by (unfold INTER_def) blast  haftmann@41082  446 haftmann@41082  447 lemma INT_D [elim, Pure.elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"  haftmann@41082  448  by auto  haftmann@41082  449 haftmann@41082  450 lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"  haftmann@41082  451  -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}  haftmann@41082  452  by (unfold INTER_def) blast  haftmann@41082  453 haftmann@41082  454 lemma INT_cong [cong]:  haftmann@41082  455  "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"  haftmann@41082  456  by (simp add: INTER_def)  haftmann@41082  457 haftmann@41082  458 lemma Collect_ball_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})"  haftmann@41082  459  by blast  haftmann@41082  460 haftmann@41082  461 lemma Collect_all_eq: "{x. \y. P x y} = (\y. {x. P x y})"  haftmann@41082  462  by blast  haftmann@41082  463 haftmann@41082  464 lemma INT_lower: "a \ A ==> (\x\A. B x) \ B a"  haftmann@41082  465  by (fact INF_leI)  haftmann@41082  466 haftmann@41082  467 lemma INT_greatest: "(!!x. x \ A ==> C \ B x) ==> C \ (\x\A. B x)"  haftmann@41082  468  by (fact le_INFI)  haftmann@41082  469 haftmann@41082  470 lemma INT_empty [simp]: "(\x\{}. B x) = UNIV"  haftmann@41082  471  by blast  haftmann@41082  472 haftmann@41082  473 lemma INT_absorb: "k \ I ==> A k \ (\i\I. A i) = (\i\I. A i)"  haftmann@41082  474  by blast  haftmann@41082  475 haftmann@41082  476 lemma INT_subset_iff: "(B \ (\i\I. A i)) = (\i\I. B \ A i)"  haftmann@41082  477  by (fact le_INF_iff)  haftmann@41082  478 haftmann@41082  479 lemma INT_insert [simp]: "(\x \ insert a A. B x) = B a \ INTER A B"  haftmann@41082  480  by blast  haftmann@41082  481 haftmann@41082  482 lemma INT_Un: "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)"  haftmann@41082  483  by blast  haftmann@41082  484 haftmann@41082  485 lemma INT_insert_distrib:  haftmann@41082  486  "u \ A ==> (\x\A. insert a (B x)) = insert a (\x\A. B x)"  haftmann@41082  487  by blast  haftmann@41082  488 haftmann@41082  489 lemma INT_constant [simp]: "(\y\A. c) = (if A = {} then UNIV else c)"  haftmann@41082  490  by auto  haftmann@41082  491 haftmann@41082  492 lemma INT_eq: "(\x\A. B x) = \({Y. \x\A. Y = B x})"  haftmann@41082  493  -- {* Look: it has an \emph{existential} quantifier *}  haftmann@41082  494  by blast  haftmann@41082  495 haftmann@41082  496 lemma INTER_UNIV_conv[simp]:  haftmann@41082  497  "(UNIV = (INT x:A. B x)) = (\x\A. B x = UNIV)"  haftmann@41082  498  "((INT x:A. B x) = UNIV) = (\x\A. B x = UNIV)"  haftmann@41082  499 by blast+  haftmann@41082  500 haftmann@41082  501 lemma INT_bool_eq: "(\b::bool. A b) = (A True \ A False)"  haftmann@41082  502  by (auto intro: bool_induct)  haftmann@41082  503 haftmann@41082  504 lemma Pow_INT_eq: "Pow (\x\A. B x) = (\x\A. Pow (B x))"  haftmann@41082  505  by blast  haftmann@41082  506 haftmann@41082  507 lemma INT_anti_mono:  haftmann@41082  508  "B \ A ==> (!!x. x \ A ==> f x \ g x) ==>  haftmann@41082  509  (\x\A. f x) \ (\x\A. g x)"  haftmann@41082  510  -- {* The last inclusion is POSITIVE! *}  haftmann@41082  511  by (blast dest: subsetD)  haftmann@41082  512 haftmann@41082  513 lemma vimage_INT: "f-(INT x:A. B x) = (INT x:A. f - B x)"  haftmann@41082  514  by blast  haftmann@41082  515 haftmann@41082  516 haftmann@32139  517 subsection {* Union *}  haftmann@32115  518 haftmann@32587  519 abbreviation Union :: "'a set set \ 'a set" where  haftmann@32587  520  "Union S \ \S"  haftmann@32115  521 haftmann@32115  522 notation (xsymbols)  haftmann@32115  523  Union ("\_" [90] 90)  haftmann@32115  524 haftmann@32135  525 lemma Union_eq:  haftmann@32135  526  "\A = {x. \B \ A. x \ B}"  nipkow@39302  527 proof (rule set_eqI)  haftmann@32115  528  fix x  haftmann@32135  529  have "(\Q\{P. \B\A. P \ x \ B}. Q) \ (\B\A. x \ B)"  haftmann@32115  530  by auto  haftmann@32135  531  then show "x \ \A \ x \ {x. \B\A. x \ B}"  haftmann@32587  532  by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)  haftmann@32115  533 qed  haftmann@32115  534 blanchet@35828  535 lemma Union_iff [simp, no_atp]:  haftmann@32115  536  "A \ \C \ (\X\C. A\X)"  haftmann@32115  537  by (unfold Union_eq) blast  haftmann@32115  538 haftmann@32115  539 lemma UnionI [intro]:  haftmann@32115  540  "X \ C \ A \ X \ A \ \C"  haftmann@32115  541  -- {* The order of the premises presupposes that @{term C} is rigid;  haftmann@32115  542  @{term A} may be flexible. *}  haftmann@32115  543  by auto  haftmann@32115  544 haftmann@32115  545 lemma UnionE [elim!]:  haftmann@32115  546  "A \ \C \ (\X. A\X \ X\C \ R) \ R"  haftmann@32115  547  by auto  haftmann@32115  548 haftmann@32135  549 lemma Union_upper: "B \ A ==> B \ Union A"  haftmann@32135  550  by (iprover intro: subsetI UnionI)  haftmann@32135  551 haftmann@32135  552 lemma Union_least: "(!!X. X \ A ==> X \ C) ==> Union A \ C"  haftmann@32135  553  by (iprover intro: subsetI elim: UnionE dest: subsetD)  haftmann@32135  554 haftmann@32135  555 lemma Un_eq_Union: "A \ B = \{A, B}"  haftmann@32135  556  by blast  haftmann@32135  557 haftmann@32135  558 lemma Union_empty [simp]: "Union({}) = {}"  haftmann@32135  559  by blast  haftmann@32135  560 haftmann@32135  561 lemma Union_UNIV [simp]: "Union UNIV = UNIV"  haftmann@32135  562  by blast  haftmann@32135  563 haftmann@32135  564 lemma Union_insert [simp]: "Union (insert a B) = a \ \B"  haftmann@32135  565  by blast  haftmann@32135  566 haftmann@32135  567 lemma Union_Un_distrib [simp]: "\(A Un B) = \A \ \B"  haftmann@32135  568  by blast  haftmann@32135  569 haftmann@32135  570 lemma Union_Int_subset: "\(A \ B) \ \A \ \B"  haftmann@32135  571  by blast  haftmann@32135  572 blanchet@35828  573 lemma Union_empty_conv [simp,no_atp]: "(\A = {}) = (\x\A. x = {})"  haftmann@32135  574  by blast  haftmann@32135  575 blanchet@35828  576 lemma empty_Union_conv [simp,no_atp]: "({} = \A) = (\x\A. x = {})"  haftmann@32135  577  by blast  haftmann@32135  578 haftmann@32135  579 lemma Union_disjoint: "(\C \ A = {}) = (\B\C. B \ A = {})"  haftmann@32135  580  by blast  haftmann@32135  581 haftmann@32135  582 lemma subset_Pow_Union: "A \ Pow (\A)"  haftmann@32135  583  by blast  haftmann@32135  584 haftmann@32135  585 lemma Union_Pow_eq [simp]: "\(Pow A) = A"  haftmann@32135  586  by blast  haftmann@32135  587 haftmann@32135  588 lemma Union_mono: "A \ B ==> \A \ \B"  haftmann@32135  589  by blast  haftmann@32135  590 haftmann@32115  591 haftmann@32139  592 subsection {* Unions of families *}  haftmann@32077  593 haftmann@32606  594 abbreviation UNION :: "'a set \ ('a \ 'b set) \ 'b set" where  haftmann@32606  595  "UNION \ SUPR"  haftmann@32077  596 haftmann@32077  597 syntax  wenzelm@35115  598  "_UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)  huffman@36364  599  "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 0, 10] 10)  haftmann@32077  600 haftmann@32077  601 syntax (xsymbols)  wenzelm@35115  602  "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" [0, 10] 10)  huffman@36364  603  "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10)  haftmann@32077  604 haftmann@32077  605 syntax (latex output)  wenzelm@35115  606  "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)  huffman@36364  607  "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^esub>)/ _)" [0, 0, 10] 10)  haftmann@32077  608 haftmann@32077  609 translations  haftmann@32077  610  "UN x y. B" == "UN x. UN y. B"  haftmann@32077  611  "UN x. B" == "CONST UNION CONST UNIV (%x. B)"  haftmann@32077  612  "UN x. B" == "UN x:CONST UNIV. B"  haftmann@32077  613  "UN x:A. B" == "CONST UNION A (%x. B)"  haftmann@32077  614 haftmann@32077  615 text {*  haftmann@32077  616  Note the difference between ordinary xsymbol syntax of indexed  haftmann@32077  617  unions and intersections (e.g.\ @{text"\a\<^isub>1\A\<^isub>1. B"})  haftmann@32077  618  and their \LaTeX\ rendition: @{term"\a\<^isub>1\A\<^isub>1. B"}. The  haftmann@32077  619  former does not make the index expression a subscript of the  haftmann@32077  620  union/intersection symbol because this leads to problems with nested  haftmann@32077  621  subscripts in Proof General.  haftmann@32077  622 *}  haftmann@32077  623 wenzelm@35115  624 print_translation {*  wenzelm@42284  625  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]  wenzelm@35115  626 *} -- {* to avoid eta-contraction of body *}  haftmann@32077  627 haftmann@32135  628 lemma UNION_eq_Union_image:  haftmann@32135  629  "(\x\A. B x) = \(BA)"  haftmann@32606  630  by (fact SUPR_def)  haftmann@32115  631 haftmann@32115  632 lemma Union_def:  haftmann@32117  633  "\S = (\x\S. x)"  haftmann@32115  634  by (simp add: UNION_eq_Union_image image_def)  haftmann@32115  635 blanchet@35828  636 lemma UNION_def [no_atp]:  haftmann@32135  637  "(\x\A. B x) = {y. \x\A. y \ B x}"  haftmann@32117  638  by (auto simp add: UNION_eq_Union_image Union_eq)  haftmann@32115  639   haftmann@32115  640 lemma Union_image_eq [simp]:  haftmann@32115  641  "\(BA) = (\x\A. B x)"  haftmann@32115  642  by (rule sym) (fact UNION_eq_Union_image)  haftmann@32115  643   wenzelm@11979  644 lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"  wenzelm@11979  645  by (unfold UNION_def) blast  wenzelm@11979  646 wenzelm@11979  647 lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)"  wenzelm@11979  648  -- {* The order of the premises presupposes that @{term A} is rigid;  wenzelm@11979  649  @{term b} may be flexible. *}  wenzelm@11979  650  by auto  wenzelm@11979  651 wenzelm@11979  652 lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R"  wenzelm@11979  653  by (unfold UNION_def) blast  clasohm@923  654 wenzelm@11979  655 lemma UN_cong [cong]:  wenzelm@11979  656  "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"  wenzelm@11979  657  by (simp add: UNION_def)  wenzelm@11979  658 berghofe@29691  659 lemma strong_UN_cong:  berghofe@29691  660  "A = B ==> (!!x. x:B =simp=> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"  berghofe@29691  661  by (simp add: UNION_def simp_implies_def)  berghofe@29691  662 haftmann@32077  663 lemma image_eq_UN: "fA = (UN x:A. {f x})"  haftmann@32077  664  by blast  haftmann@32077  665 haftmann@32135  666 lemma UN_upper: "a \ A ==> B a \ (\x\A. B x)"  haftmann@32606  667  by (fact le_SUPI)  haftmann@32135  668 haftmann@32135  669 lemma UN_least: "(!!x. x \ A ==> B x \ C) ==> (\x\A. B x) \ C"  haftmann@32135  670  by (iprover intro: subsetI elim: UN_E dest: subsetD)  haftmann@32135  671 blanchet@35828  672 lemma Collect_bex_eq [no_atp]: "{x. \y\A. P x y} = (\y\A. {x. P x y})"  haftmann@32135  673  by blast  haftmann@32135  674 haftmann@32135  675 lemma UN_insert_distrib: "u \ A ==> (\x\A. insert a (B x)) = insert a (\x\A. B x)"  haftmann@32135  676  by blast  haftmann@32135  677 blanchet@35828  678 lemma UN_empty [simp,no_atp]: "(\x\{}. B x) = {}"  haftmann@32135  679  by blast  haftmann@32135  680 haftmann@32135  681 lemma UN_empty2 [simp]: "(\x\A. {}) = {}"  haftmann@32135  682  by blast  haftmann@32135  683 haftmann@32135  684 lemma UN_singleton [simp]: "(\x\A. {x}) = A"  haftmann@32135  685  by blast  haftmann@32135  686 haftmann@32135  687 lemma UN_absorb: "k \ I ==> A k \ (\i\I. A i) = (\i\I. A i)"  haftmann@32135  688  by auto  haftmann@32135  689 haftmann@32135  690 lemma UN_insert [simp]: "(\x\insert a A. B x) = B a \ UNION A B"  haftmann@32135  691  by blast  haftmann@32135  692 haftmann@32135  693 lemma UN_Un[simp]: "(\i \ A \ B. M i) = (\i\A. M i) \ (\i\B. M i)"  haftmann@32135  694  by blast  haftmann@32135  695 haftmann@32135  696 lemma UN_UN_flatten: "(\x \ (\y\A. B y). C x) = (\y\A. \x\B y. C x)"  haftmann@32135  697  by blast  haftmann@32135  698 haftmann@32135  699 lemma UN_subset_iff: "((\i\I. A i) \ B) = (\i\I. A i \ B)"  huffman@35629  700  by (fact SUP_le_iff)  haftmann@32135  701 haftmann@32135  702 lemma image_Union: "f  \S = (\x\S. f  x)"  haftmann@32135  703  by blast  haftmann@32135  704 haftmann@32135  705 lemma UN_constant [simp]: "(\y\A. c) = (if A = {} then {} else c)"  haftmann@32135  706  by auto  haftmann@32135  707 haftmann@32135  708 lemma UN_eq: "(\x\A. B x) = \({Y. \x\A. Y = B x})"  haftmann@32135  709  by blast  haftmann@32135  710 haftmann@32135  711 lemma UNION_empty_conv[simp]:  haftmann@32135  712  "({} = (UN x:A. B x)) = (\x\A. B x = {})"  haftmann@32135  713  "((UN x:A. B x) = {}) = (\x\A. B x = {})"  haftmann@32135  714 by blast+  haftmann@32135  715 blanchet@35828  716 lemma Collect_ex_eq [no_atp]: "{x. \y. P x y} = (\y. {x. P x y})"  haftmann@32135  717  by blast  haftmann@32135  718 haftmann@32135  719 lemma ball_UN: "(\z \ UNION A B. P z) = (\x\A. \z \ B x. P z)"  haftmann@32135  720  by blast  haftmann@32135  721 haftmann@32135  722 lemma bex_UN: "(\z \ UNION A B. P z) = (\x\A. \z\B x. P z)"  haftmann@32135  723  by blast  haftmann@32135  724 haftmann@32135  725 lemma Un_eq_UN: "A \ B = (\b. if b then A else B)"  haftmann@32135  726  by (auto simp add: split_if_mem2)  haftmann@32135  727 haftmann@32135  728 lemma UN_bool_eq: "(\b::bool. A b) = (A True \ A False)"  haftmann@32135  729  by (auto intro: bool_contrapos)  haftmann@32135  730 haftmann@32135  731 lemma UN_Pow_subset: "(\x\A. Pow (B x)) \ Pow (\x\A. B x)"  haftmann@32135  732  by blast  haftmann@32135  733 haftmann@32135  734 lemma UN_mono:  haftmann@32135  735  "A \ B ==> (!!x. x \ A ==> f x \ g x) ==>  haftmann@32135  736  (\x\A. f x) \ (\x\B. g x)"  haftmann@32135  737  by (blast dest: subsetD)  haftmann@32135  738 haftmann@32135  739 lemma vimage_Union: "f - (Union A) = (UN X:A. f - X)"  haftmann@32135  740  by blast  haftmann@32135  741 haftmann@32135  742 lemma vimage_UN: "f-(UN x:A. B x) = (UN x:A. f - B x)"  haftmann@32135  743  by blast  haftmann@32135  744 haftmann@32135  745 lemma vimage_eq_UN: "f-B = (UN y: B. f-{y})"  haftmann@32135  746  -- {* NOT suitable for rewriting *}  haftmann@32135  747  by blast  haftmann@32135  748 haftmann@32135  749 lemma image_UN: "(f  (UNION A B)) = (UN x:A.(f  (B x)))"  haftmann@32135  750 by blast  haftmann@32135  751 wenzelm@11979  752 haftmann@32139  753 subsection {* Distributive laws *}  wenzelm@12897  754 wenzelm@12897  755 lemma Int_Union: "A \ \B = (\C\B. A \ C)"  wenzelm@12897  756  by blast  wenzelm@12897  757 wenzelm@12897  758 lemma Int_Union2: "\B \ A = (\C\B. C \ A)"  wenzelm@12897  759  by blast  wenzelm@12897  760 wenzelm@12897  761 lemma Un_Union_image: "(\x\C. A x \ B x) = \(AC) \ \(BC)"  wenzelm@12897  762  -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}  wenzelm@12897  763  -- {* Union of a family of unions *}  wenzelm@12897  764  by blast  wenzelm@12897  765 wenzelm@12897  766 lemma UN_Un_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)"  wenzelm@12897  767  -- {* Equivalent version *}  wenzelm@12897  768  by blast  wenzelm@12897  769 wenzelm@12897  770 lemma Un_Inter: "A \ \B = (\C\B. A \ C)"  wenzelm@12897  771  by blast  wenzelm@12897  772 wenzelm@12897  773 lemma Int_Inter_image: "(\x\C. A x \ B x) = \(AC) \ \(BC)"  wenzelm@12897  774  by blast  wenzelm@12897  775 wenzelm@12897  776 lemma INT_Int_distrib: "(\i\I. A i \ B i) = (\i\I. A i) \ (\i\I. B i)"  wenzelm@12897  777  -- {* Equivalent version *}  wenzelm@12897  778  by blast  wenzelm@12897  779 wenzelm@12897  780 lemma Int_UN_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)"  wenzelm@12897  781  -- {* Halmos, Naive Set Theory, page 35. *}  wenzelm@12897  782  by blast  wenzelm@12897  783 wenzelm@12897  784 lemma Un_INT_distrib: "B \ (\i\I. A i) = (\i\I. B \ A i)"  wenzelm@12897  785  by blast  wenzelm@12897  786 wenzelm@12897  787 lemma Int_UN_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)"  wenzelm@12897  788  by blast  wenzelm@12897  789 wenzelm@12897  790 lemma Un_INT_distrib2: "(\i\I. A i) \ (\j\J. B j) = (\i\I. \j\J. A i \ B j)"  wenzelm@12897  791  by blast  wenzelm@12897  792 wenzelm@12897  793 haftmann@32139  794 subsection {* Complement *}  haftmann@32135  795 haftmann@32135  796 lemma Compl_UN [simp]: "-(\x\A. B x) = (\x\A. -B x)"  wenzelm@12897  797  by blast  wenzelm@12897  798 haftmann@32135  799 lemma Compl_INT [simp]: "-(\x\A. B x) = (\x\A. -B x)"  wenzelm@12897  800  by blast  wenzelm@12897  801 wenzelm@12897  802 haftmann@32139  803 subsection {* Miniscoping and maxiscoping *}  wenzelm@12897  804 paulson@13860  805 text {* \medskip Miniscoping: pushing in quantifiers and big Unions  paulson@13860  806  and Intersections. *}  wenzelm@12897  807 wenzelm@12897  808 lemma UN_simps [simp]:  wenzelm@12897  809  "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))"  wenzelm@12897  810  "!!A B C. (UN x:C. A x Un B) = ((if C={} then {} else (UN x:C. A x) Un B))"  wenzelm@12897  811  "!!A B C. (UN x:C. A Un B x) = ((if C={} then {} else A Un (UN x:C. B x)))"  wenzelm@12897  812  "!!A B C. (UN x:C. A x Int B) = ((UN x:C. A x) Int B)"  wenzelm@12897  813  "!!A B C. (UN x:C. A Int B x) = (A Int (UN x:C. B x))"  wenzelm@12897  814  "!!A B C. (UN x:C. A x - B) = ((UN x:C. A x) - B)"  wenzelm@12897  815  "!!A B C. (UN x:C. A - B x) = (A - (INT x:C. B x))"  wenzelm@12897  816  "!!A B. (UN x: Union A. B x) = (UN y:A. UN x:y. B x)"  wenzelm@12897  817  "!!A B C. (UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)"  wenzelm@12897  818  "!!A B f. (UN x:fA. B x) = (UN a:A. B (f a))"  wenzelm@12897  819  by auto  wenzelm@12897  820 wenzelm@12897  821 lemma INT_simps [simp]:  wenzelm@12897  822  "!!A B C. (INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)"  wenzelm@12897  823  "!!A B C. (INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))"  wenzelm@12897  824  "!!A B C. (INT x:C. A x - B) = (if C={} then UNIV else (INT x:C. A x) - B)"  wenzelm@12897  825  "!!A B C. (INT x:C. A - B x) = (if C={} then UNIV else A - (UN x:C. B x))"  wenzelm@12897  826  "!!a B C. (INT x:C. insert a (B x)) = insert a (INT x:C. B x)"  wenzelm@12897  827  "!!A B C. (INT x:C. A x Un B) = ((INT x:C. A x) Un B)"  wenzelm@12897  828  "!!A B C. (INT x:C. A Un B x) = (A Un (INT x:C. B x))"  wenzelm@12897  829  "!!A B. (INT x: Union A. B x) = (INT y:A. INT x:y. B x)"  wenzelm@12897  830  "!!A B C. (INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)"  wenzelm@12897  831  "!!A B f. (INT x:fA. B x) = (INT a:A. B (f a))"  wenzelm@12897  832  by auto  wenzelm@12897  833 blanchet@35828  834 lemma ball_simps [simp,no_atp]:  wenzelm@12897  835  "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"  wenzelm@12897  836  "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"  wenzelm@12897  837  "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"  wenzelm@12897  838  "!!A P Q. (ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)"  wenzelm@12897  839  "!!P. (ALL x:{}. P x) = True"  wenzelm@12897  840  "!!P. (ALL x:UNIV. P x) = (ALL x. P x)"  wenzelm@12897  841  "!!a B P. (ALL x:insert a B. P x) = (P a & (ALL x:B. P x))"  wenzelm@12897  842  "!!A P. (ALL x:Union A. P x) = (ALL y:A. ALL x:y. P x)"  wenzelm@12897  843  "!!A B P. (ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)"  wenzelm@12897  844  "!!P Q. (ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"  wenzelm@12897  845  "!!A P f. (ALL x:fA. P x) = (ALL x:A. P (f x))"  wenzelm@12897  846  "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"  wenzelm@12897  847  by auto  wenzelm@12897  848 blanchet@35828  849 lemma bex_simps [simp,no_atp]:  wenzelm@12897  850  "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"  wenzelm@12897  851  "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"  wenzelm@12897  852  "!!P. (EX x:{}. P x) = False"  wenzelm@12897  853  "!!P. (EX x:UNIV. P x) = (EX x. P x)"  wenzelm@12897  854  "!!a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))"  wenzelm@12897  855  "!!A P. (EX x:Union A. P x) = (EX y:A. EX x:y. P x)"  wenzelm@12897  856  "!!A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)"  wenzelm@12897  857  "!!P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)"  wenzelm@12897  858  "!!A P f. (EX x:fA. P x) = (EX x:A. P (f x))"  wenzelm@12897  859  "!!A P. (~(EX x:A. P x)) = (ALL x:A. ~P x)"  wenzelm@12897  860  by auto  wenzelm@12897  861 wenzelm@12897  862 lemma ball_conj_distrib:  wenzelm@12897  863  "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))"  wenzelm@12897  864  by blast  wenzelm@12897  865 wenzelm@12897  866 lemma bex_disj_distrib:  wenzelm@12897  867  "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))"  wenzelm@12897  868  by blast  wenzelm@12897  869 wenzelm@12897  870 paulson@13860  871 text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}  paulson@13860  872 paulson@13860  873 lemma UN_extend_simps:  paulson@13860  874  "!!a B C. insert a (UN x:C. B x) = (if C={} then {a} else (UN x:C. insert a (B x)))"  paulson@13860  875  "!!A B C. (UN x:C. A x) Un B = (if C={} then B else (UN x:C. A x Un B))"  paulson@13860  876  "!!A B C. A Un (UN x:C. B x) = (if C={} then A else (UN x:C. A Un B x))"  paulson@13860  877  "!!A B C. ((UN x:C. A x) Int B) = (UN x:C. A x Int B)"  paulson@13860  878  "!!A B C. (A Int (UN x:C. B x)) = (UN x:C. A Int B x)"  paulson@13860  879  "!!A B C. ((UN x:C. A x) - B) = (UN x:C. A x - B)"  paulson@13860  880  "!!A B C. (A - (INT x:C. B x)) = (UN x:C. A - B x)"  paulson@13860  881  "!!A B. (UN y:A. UN x:y. B x) = (UN x: Union A. B x)"  paulson@13860  882  "!!A B C. (UN x:A. UN z: B(x). C z) = (UN z: UNION A B. C z)"  paulson@13860  883  "!!A B f. (UN a:A. B (f a)) = (UN x:fA. B x)"  paulson@13860  884  by auto  paulson@13860  885 paulson@13860  886 lemma INT_extend_simps:  paulson@13860  887  "!!A B C. (INT x:C. A x) Int B = (if C={} then B else (INT x:C. A x Int B))"  paulson@13860  888  "!!A B C. A Int (INT x:C. B x) = (if C={} then A else (INT x:C. A Int B x))"  paulson@13860  889  "!!A B C. (INT x:C. A x) - B = (if C={} then UNIV-B else (INT x:C. A x - B))"  paulson@13860  890  "!!A B C. A - (UN x:C. B x) = (if C={} then A else (INT x:C. A - B x))"  paulson@13860  891  "!!a B C. insert a (INT x:C. B x) = (INT x:C. insert a (B x))"  paulson@13860  892  "!!A B C. ((INT x:C. A x) Un B) = (INT x:C. A x Un B)"  paulson@13860  893  "!!A B C. A Un (INT x:C. B x) = (INT x:C. A Un B x)"  paulson@13860  894  "!!A B. (INT y:A. INT x:y. B x) = (INT x: Union A. B x)"  paulson@13860  895  "!!A B C. (INT x:A. INT z: B(x). C z) = (INT z: UNION A B. C z)"  paulson@13860  896  "!!A B f. (INT a:A. B (f a)) = (INT x:fA. B x)"  paulson@13860  897  by auto  paulson@13860  898 paulson@13860  899 haftmann@32135  900 no_notation  haftmann@32135  901  less_eq (infix "\" 50) and  haftmann@32135  902  less (infix "\" 50) and  haftmann@41082  903  bot ("\") and  haftmann@41082  904  top ("\") and  haftmann@32135  905  inf (infixl "\" 70) and  haftmann@32135  906  sup (infixl "\" 65) and  haftmann@32135  907  Inf ("\_" [900] 900) and  haftmann@41082  908  Sup ("\_" [900] 900)  haftmann@32135  909 haftmann@41080  910 no_syntax (xsymbols)  haftmann@41082  911  "_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)  haftmann@41082  912  "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)  haftmann@41080  913  "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)  haftmann@41080  914  "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)  haftmann@41080  915 haftmann@30596  916 lemmas mem_simps =  haftmann@30596  917  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff  haftmann@30596  918  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff  haftmann@30596  919  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}  wenzelm@21669  920 wenzelm@11979  921 end `