src/HOL/Complete_Lattice.thy
 author nipkow Fri Aug 28 18:52:41 2009 +0200 (2009-08-28) changeset 32436 10cd49e0c067 parent 32139 e271a64f03ff child 32587 caa5ada96a00 permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
     1 (*  Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)

     2

     3 header {* Complete lattices, with special focus on sets *}

     4

     5 theory Complete_Lattice

     6 imports Set

     7 begin

     8

     9 notation

    10   less_eq  (infix "\<sqsubseteq>" 50) and

    11   less (infix "\<sqsubset>" 50) and

    12   inf  (infixl "\<sqinter>" 70) and

    13   sup  (infixl "\<squnion>" 65)

    14

    15

    16 subsection {* Abstract complete lattices *}

    17

    18 class complete_lattice = lattice + bot + top +

    19   fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)

    20     and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)

    21   assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"

    22      and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"

    23   assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"

    24      and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"

    25 begin

    26

    27 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"

    28   by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)

    29

    30 lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"

    31   by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)

    32

    33 lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"

    34   unfolding Sup_Inf by auto

    35

    36 lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"

    37   unfolding Inf_Sup by auto

    38

    39 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"

    40   by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)

    41

    42 lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"

    43   by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)

    44

    45 lemma Inf_singleton [simp]:

    46   "\<Sqinter>{a} = a"

    47   by (auto intro: antisym Inf_lower Inf_greatest)

    48

    49 lemma Sup_singleton [simp]:

    50   "\<Squnion>{a} = a"

    51   by (auto intro: antisym Sup_upper Sup_least)

    52

    53 lemma Inf_insert_simp:

    54   "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"

    55   by (cases "A = {}") (simp_all, simp add: Inf_insert)

    56

    57 lemma Sup_insert_simp:

    58   "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"

    59   by (cases "A = {}") (simp_all, simp add: Sup_insert)

    60

    61 lemma Inf_binary:

    62   "\<Sqinter>{a, b} = a \<sqinter> b"

    63   by (auto simp add: Inf_insert_simp)

    64

    65 lemma Sup_binary:

    66   "\<Squnion>{a, b} = a \<squnion> b"

    67   by (auto simp add: Sup_insert_simp)

    68

    69 lemma bot_def:

    70   "bot = \<Squnion>{}"

    71   by (auto intro: antisym Sup_least)

    72

    73 lemma top_def:

    74   "top = \<Sqinter>{}"

    75   by (auto intro: antisym Inf_greatest)

    76

    77 lemma sup_bot [simp]:

    78   "x \<squnion> bot = x"

    79   using bot_least [of x] by (simp add: sup_commute)

    80

    81 lemma inf_top [simp]:

    82   "x \<sqinter> top = x"

    83   using top_greatest [of x] by (simp add: inf_commute)

    84

    85 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where

    86   "SUPR A f = \<Squnion> (f  A)"

    87

    88 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where

    89   "INFI A f = \<Sqinter> (f  A)"

    90

    91 end

    92

    93 syntax

    94   "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" [0, 10] 10)

    95   "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" [0, 10] 10)

    96   "_INF1"     :: "pttrns => 'b => 'b"           ("(3INF _./ _)" [0, 10] 10)

    97   "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3INF _:_./ _)" [0, 10] 10)

    98

    99 translations

   100   "SUP x y. B"   == "SUP x. SUP y. B"

   101   "SUP x. B"     == "CONST SUPR CONST UNIV (%x. B)"

   102   "SUP x. B"     == "SUP x:CONST UNIV. B"

   103   "SUP x:A. B"   == "CONST SUPR A (%x. B)"

   104   "INF x y. B"   == "INF x. INF y. B"

   105   "INF x. B"     == "CONST INFI CONST UNIV (%x. B)"

   106   "INF x. B"     == "INF x:CONST UNIV. B"

   107   "INF x:A. B"   == "CONST INFI A (%x. B)"

   108

   109 print_translation {* [

   110 Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} "_SUP",

   111 Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} "_INF"

   112 ] *} -- {* to avoid eta-contraction of body *}

   113

   114 context complete_lattice

   115 begin

   116

   117 lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"

   118   by (auto simp add: SUPR_def intro: Sup_upper)

   119

   120 lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"

   121   by (auto simp add: SUPR_def intro: Sup_least)

   122

   123 lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"

   124   by (auto simp add: INFI_def intro: Inf_lower)

   125

   126 lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"

   127   by (auto simp add: INFI_def intro: Inf_greatest)

   128

   129 lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"

   130   by (auto intro: antisym SUP_leI le_SUPI)

   131

   132 lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"

   133   by (auto intro: antisym INF_leI le_INFI)

   134

   135 end

   136

   137

   138 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}

   139

   140 instantiation bool :: complete_lattice

   141 begin

   142

   143 definition

   144   Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"

   145

   146 definition

   147   Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"

   148

   149 instance proof

   150 qed (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)

   151

   152 end

   153

   154 lemma Inf_empty_bool [simp]:

   155   "\<Sqinter>{}"

   156   unfolding Inf_bool_def by auto

   157

   158 lemma not_Sup_empty_bool [simp]:

   159   "\<not> \<Squnion>{}"

   160   unfolding Sup_bool_def by auto

   161

   162 lemma INFI_bool_eq:

   163   "INFI = Ball"

   164 proof (rule ext)+

   165   fix A :: "'a set"

   166   fix P :: "'a \<Rightarrow> bool"

   167   show "(INF x:A. P x) \<longleftrightarrow> (\<forall>x \<in> A. P x)"

   168     by (auto simp add: Ball_def INFI_def Inf_bool_def)

   169 qed

   170

   171 lemma SUPR_bool_eq:

   172   "SUPR = Bex"

   173 proof (rule ext)+

   174   fix A :: "'a set"

   175   fix P :: "'a \<Rightarrow> bool"

   176   show "(SUP x:A. P x) \<longleftrightarrow> (\<exists>x \<in> A. P x)"

   177     by (auto simp add: Bex_def SUPR_def Sup_bool_def)

   178 qed

   179

   180 instantiation "fun" :: (type, complete_lattice) complete_lattice

   181 begin

   182

   183 definition

   184   Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"

   185

   186 definition

   187   Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"

   188

   189 instance proof

   190 qed (auto simp add: Inf_fun_def Sup_fun_def le_fun_def

   191   intro: Inf_lower Sup_upper Inf_greatest Sup_least)

   192

   193 end

   194

   195 lemma Inf_empty_fun:

   196   "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"

   197   by (simp add: Inf_fun_def)

   198

   199 lemma Sup_empty_fun:

   200   "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"

   201   by (simp add: Sup_fun_def)

   202

   203

   204 subsection {* Union *}

   205

   206 definition Union :: "'a set set \<Rightarrow> 'a set" where

   207   Sup_set_eq [symmetric]: "Union S = \<Squnion>S"

   208

   209 notation (xsymbols)

   210   Union  ("\<Union>_" [90] 90)

   211

   212 lemma Union_eq:

   213   "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"

   214 proof (rule set_ext)

   215   fix x

   216   have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"

   217     by auto

   218   then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"

   219     by (simp add: Sup_set_eq [symmetric] Sup_fun_def Sup_bool_def) (simp add: mem_def)

   220 qed

   221

   222 lemma Union_iff [simp, noatp]:

   223   "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"

   224   by (unfold Union_eq) blast

   225

   226 lemma UnionI [intro]:

   227   "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"

   228   -- {* The order of the premises presupposes that @{term C} is rigid;

   229     @{term A} may be flexible. *}

   230   by auto

   231

   232 lemma UnionE [elim!]:

   233   "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A\<in>X \<Longrightarrow> X\<in>C \<Longrightarrow> R) \<Longrightarrow> R"

   234   by auto

   235

   236 lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"

   237   by (iprover intro: subsetI UnionI)

   238

   239 lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"

   240   by (iprover intro: subsetI elim: UnionE dest: subsetD)

   241

   242 lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"

   243   by blast

   244

   245 lemma Union_empty [simp]: "Union({}) = {}"

   246   by blast

   247

   248 lemma Union_UNIV [simp]: "Union UNIV = UNIV"

   249   by blast

   250

   251 lemma Union_insert [simp]: "Union (insert a B) = a \<union> \<Union>B"

   252   by blast

   253

   254 lemma Union_Un_distrib [simp]: "\<Union>(A Un B) = \<Union>A \<union> \<Union>B"

   255   by blast

   256

   257 lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"

   258   by blast

   259

   260 lemma Union_empty_conv [simp,noatp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"

   261   by blast

   262

   263 lemma empty_Union_conv [simp,noatp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"

   264   by blast

   265

   266 lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"

   267   by blast

   268

   269 lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"

   270   by blast

   271

   272 lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A"

   273   by blast

   274

   275 lemma Union_mono: "A \<subseteq> B ==> \<Union>A \<subseteq> \<Union>B"

   276   by blast

   277

   278

   279 subsection {* Unions of families *}

   280

   281 definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where

   282   SUPR_set_eq [symmetric]: "UNION S f = (SUP x:S. f x)"

   283

   284 syntax

   285   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)

   286   "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 10] 10)

   287

   288 syntax (xsymbols)

   289   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)

   290   "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 10] 10)

   291

   292 syntax (latex output)

   293   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)

   294   "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)

   295

   296 translations

   297   "UN x y. B"   == "UN x. UN y. B"

   298   "UN x. B"     == "CONST UNION CONST UNIV (%x. B)"

   299   "UN x. B"     == "UN x:CONST UNIV. B"

   300   "UN x:A. B"   == "CONST UNION A (%x. B)"

   301

   302 text {*

   303   Note the difference between ordinary xsymbol syntax of indexed

   304   unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})

   305   and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The

   306   former does not make the index expression a subscript of the

   307   union/intersection symbol because this leads to problems with nested

   308   subscripts in Proof General.

   309 *}

   310

   311 print_translation {* [

   312 Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} "@UNION"

   313 ] *} -- {* to avoid eta-contraction of body *}

   314

   315 lemma UNION_eq_Union_image:

   316   "(\<Union>x\<in>A. B x) = \<Union>(BA)"

   317   by (simp add: SUPR_def SUPR_set_eq [symmetric] Sup_set_eq)

   318

   319 lemma Union_def:

   320   "\<Union>S = (\<Union>x\<in>S. x)"

   321   by (simp add: UNION_eq_Union_image image_def)

   322

   323 lemma UNION_def [noatp]:

   324   "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"

   325   by (auto simp add: UNION_eq_Union_image Union_eq)

   326

   327 lemma Union_image_eq [simp]:

   328   "\<Union>(BA) = (\<Union>x\<in>A. B x)"

   329   by (rule sym) (fact UNION_eq_Union_image)

   330

   331 lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"

   332   by (unfold UNION_def) blast

   333

   334 lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)"

   335   -- {* The order of the premises presupposes that @{term A} is rigid;

   336     @{term b} may be flexible. *}

   337   by auto

   338

   339 lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R"

   340   by (unfold UNION_def) blast

   341

   342 lemma UN_cong [cong]:

   343     "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"

   344   by (simp add: UNION_def)

   345

   346 lemma strong_UN_cong:

   347     "A = B ==> (!!x. x:B =simp=> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"

   348   by (simp add: UNION_def simp_implies_def)

   349

   350 lemma image_eq_UN: "fA = (UN x:A. {f x})"

   351   by blast

   352

   353 lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"

   354   by blast

   355

   356 lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"

   357   by (iprover intro: subsetI elim: UN_E dest: subsetD)

   358

   359 lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"

   360   by blast

   361

   362 lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"

   363   by blast

   364

   365 lemma UN_empty [simp,noatp]: "(\<Union>x\<in>{}. B x) = {}"

   366   by blast

   367

   368 lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"

   369   by blast

   370

   371 lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"

   372   by blast

   373

   374 lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"

   375   by auto

   376

   377 lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"

   378   by blast

   379

   380 lemma UN_Un[simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"

   381   by blast

   382

   383 lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)"

   384   by blast

   385

   386 lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"

   387   by blast

   388

   389 lemma image_Union: "f  \<Union>S = (\<Union>x\<in>S. f  x)"

   390   by blast

   391

   392 lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"

   393   by auto

   394

   395 lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"

   396   by blast

   397

   398 lemma UNION_empty_conv[simp]:

   399   "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"

   400   "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"

   401 by blast+

   402

   403 lemma Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"

   404   by blast

   405

   406 lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"

   407   by blast

   408

   409 lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) = (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"

   410   by blast

   411

   412 lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"

   413   by (auto simp add: split_if_mem2)

   414

   415 lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True \<union> A False)"

   416   by (auto intro: bool_contrapos)

   417

   418 lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)"

   419   by blast

   420

   421 lemma UN_mono:

   422   "A \<subseteq> B ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>

   423     (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"

   424   by (blast dest: subsetD)

   425

   426 lemma vimage_Union: "f - (Union A) = (UN X:A. f - X)"

   427   by blast

   428

   429 lemma vimage_UN: "f-(UN x:A. B x) = (UN x:A. f - B x)"

   430   by blast

   431

   432 lemma vimage_eq_UN: "f-B = (UN y: B. f-{y})"

   433   -- {* NOT suitable for rewriting *}

   434   by blast

   435

   436 lemma image_UN: "(f  (UNION A B)) = (UN x:A.(f  (B x)))"

   437 by blast

   438

   439

   440 subsection {* Inter *}

   441

   442 definition Inter :: "'a set set \<Rightarrow> 'a set" where

   443   Inf_set_eq [symmetric]: "Inter S = \<Sqinter>S"

   444

   445 notation (xsymbols)

   446   Inter  ("\<Inter>_" [90] 90)

   447

   448 lemma Inter_eq [code del]:

   449   "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"

   450 proof (rule set_ext)

   451   fix x

   452   have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"

   453     by auto

   454   then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"

   455     by (simp add: Inf_fun_def Inf_bool_def Inf_set_eq [symmetric]) (simp add: mem_def)

   456 qed

   457

   458 lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"

   459   by (unfold Inter_eq) blast

   460

   461 lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"

   462   by (simp add: Inter_eq)

   463

   464 text {*

   465   \medskip A destruct'' rule -- every @{term X} in @{term C}

   466   contains @{term A} as an element, but @{prop "A:X"} can hold when

   467   @{prop "X:C"} does not!  This rule is analogous to @{text spec}.

   468 *}

   469

   470 lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"

   471   by auto

   472

   473 lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"

   474   -- {* Classical'' elimination rule -- does not require proving

   475     @{prop "X:C"}. *}

   476   by (unfold Inter_eq) blast

   477

   478 lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"

   479   by blast

   480

   481 lemma Inter_subset:

   482   "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"

   483   by blast

   484

   485 lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"

   486   by (iprover intro: InterI subsetI dest: subsetD)

   487

   488 lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"

   489   by blast

   490

   491 lemma Inter_empty [simp]: "\<Inter>{} = UNIV"

   492   by blast

   493

   494 lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"

   495   by blast

   496

   497 lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"

   498   by blast

   499

   500 lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"

   501   by blast

   502

   503 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"

   504   by blast

   505

   506 lemma Inter_UNIV_conv [simp,noatp]:

   507   "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"

   508   "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"

   509   by blast+

   510

   511 lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"

   512   by blast

   513

   514

   515 subsection {* Intersections of families *}

   516

   517 definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where

   518   INFI_set_eq [symmetric]: "INTER S f = (INF x:S. f x)"

   519

   520 syntax

   521   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)

   522   "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 10] 10)

   523

   524 syntax (xsymbols)

   525   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)

   526   "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)

   527

   528 syntax (latex output)

   529   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)

   530   "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)

   531

   532 translations

   533   "INT x y. B"  == "INT x. INT y. B"

   534   "INT x. B"    == "CONST INTER CONST UNIV (%x. B)"

   535   "INT x. B"    == "INT x:CONST UNIV. B"

   536   "INT x:A. B"  == "CONST INTER A (%x. B)"

   537

   538 print_translation {* [

   539 Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} "@INTER"

   540 ] *} -- {* to avoid eta-contraction of body *}

   541

   542 lemma INTER_eq_Inter_image:

   543   "(\<Inter>x\<in>A. B x) = \<Inter>(BA)"

   544   by (simp add: INFI_def INFI_set_eq [symmetric] Inf_set_eq)

   545

   546 lemma Inter_def:

   547   "\<Inter>S = (\<Inter>x\<in>S. x)"

   548   by (simp add: INTER_eq_Inter_image image_def)

   549

   550 lemma INTER_def:

   551   "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"

   552   by (auto simp add: INTER_eq_Inter_image Inter_eq)

   553

   554 lemma Inter_image_eq [simp]:

   555   "\<Inter>(BA) = (\<Inter>x\<in>A. B x)"

   556   by (rule sym) (fact INTER_eq_Inter_image)

   557

   558 lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"

   559   by (unfold INTER_def) blast

   560

   561 lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"

   562   by (unfold INTER_def) blast

   563

   564 lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"

   565   by auto

   566

   567 lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"

   568   -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}

   569   by (unfold INTER_def) blast

   570

   571 lemma INT_cong [cong]:

   572     "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"

   573   by (simp add: INTER_def)

   574

   575 lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"

   576   by blast

   577

   578 lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"

   579   by blast

   580

   581 lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"

   582   by blast

   583

   584 lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"

   585   by (iprover intro: INT_I subsetI dest: subsetD)

   586

   587 lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"

   588   by blast

   589

   590 lemma INT_absorb: "k \<in> I ==> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"

   591   by blast

   592

   593 lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"

   594   by blast

   595

   596 lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"

   597   by blast

   598

   599 lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"

   600   by blast

   601

   602 lemma INT_insert_distrib:

   603     "u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"

   604   by blast

   605

   606 lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"

   607   by auto

   608

   609 lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"

   610   -- {* Look: it has an \emph{existential} quantifier *}

   611   by blast

   612

   613 lemma INTER_UNIV_conv[simp]:

   614  "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"

   615  "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"

   616 by blast+

   617

   618 lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"

   619   by (auto intro: bool_induct)

   620

   621 lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"

   622   by blast

   623

   624 lemma INT_anti_mono:

   625   "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>

   626     (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"

   627   -- {* The last inclusion is POSITIVE! *}

   628   by (blast dest: subsetD)

   629

   630 lemma vimage_INT: "f-(INT x:A. B x) = (INT x:A. f - B x)"

   631   by blast

   632

   633

   634 subsection {* Distributive laws *}

   635

   636 lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"

   637   by blast

   638

   639 lemma Int_Union2: "\<Union>B \<inter> A = (\<Union>C\<in>B. C \<inter> A)"

   640   by blast

   641

   642 lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(AC) \<union> \<Union>(BC)"

   643   -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}

   644   -- {* Union of a family of unions *}

   645   by blast

   646

   647 lemma UN_Un_distrib: "(\<Union>i\<in>I. A i \<union> B i) = (\<Union>i\<in>I. A i) \<union> (\<Union>i\<in>I. B i)"

   648   -- {* Equivalent version *}

   649   by blast

   650

   651 lemma Un_Inter: "A \<union> \<Inter>B = (\<Inter>C\<in>B. A \<union> C)"

   652   by blast

   653

   654 lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(AC) \<inter> \<Inter>(BC)"

   655   by blast

   656

   657 lemma INT_Int_distrib: "(\<Inter>i\<in>I. A i \<inter> B i) = (\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i)"

   658   -- {* Equivalent version *}

   659   by blast

   660

   661 lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. B \<inter> A i)"

   662   -- {* Halmos, Naive Set Theory, page 35. *}

   663   by blast

   664

   665 lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"

   666   by blast

   667

   668 lemma Int_UN_distrib2: "(\<Union>i\<in>I. A i) \<inter> (\<Union>j\<in>J. B j) = (\<Union>i\<in>I. \<Union>j\<in>J. A i \<inter> B j)"

   669   by blast

   670

   671 lemma Un_INT_distrib2: "(\<Inter>i\<in>I. A i) \<union> (\<Inter>j\<in>J. B j) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A i \<union> B j)"

   672   by blast

   673

   674

   675 subsection {* Complement *}

   676

   677 lemma Compl_UN [simp]: "-(\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"

   678   by blast

   679

   680 lemma Compl_INT [simp]: "-(\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"

   681   by blast

   682

   683

   684 subsection {* Miniscoping and maxiscoping *}

   685

   686 text {* \medskip Miniscoping: pushing in quantifiers and big Unions

   687            and Intersections. *}

   688

   689 lemma UN_simps [simp]:

   690   "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))"

   691   "!!A B C. (UN x:C. A x Un B)   = ((if C={} then {} else (UN x:C. A x) Un B))"

   692   "!!A B C. (UN x:C. A Un B x)   = ((if C={} then {} else A Un (UN x:C. B x)))"

   693   "!!A B C. (UN x:C. A x Int B)  = ((UN x:C. A x) Int B)"

   694   "!!A B C. (UN x:C. A Int B x)  = (A Int (UN x:C. B x))"

   695   "!!A B C. (UN x:C. A x - B)    = ((UN x:C. A x) - B)"

   696   "!!A B C. (UN x:C. A - B x)    = (A - (INT x:C. B x))"

   697   "!!A B. (UN x: Union A. B x) = (UN y:A. UN x:y. B x)"

   698   "!!A B C. (UN z: UNION A B. C z) = (UN  x:A. UN z: B(x). C z)"

   699   "!!A B f. (UN x:fA. B x)     = (UN a:A. B (f a))"

   700   by auto

   701

   702 lemma INT_simps [simp]:

   703   "!!A B C. (INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)"

   704   "!!A B C. (INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))"

   705   "!!A B C. (INT x:C. A x - B)   = (if C={} then UNIV else (INT x:C. A x) - B)"

   706   "!!A B C. (INT x:C. A - B x)   = (if C={} then UNIV else A - (UN x:C. B x))"

   707   "!!a B C. (INT x:C. insert a (B x)) = insert a (INT x:C. B x)"

   708   "!!A B C. (INT x:C. A x Un B)  = ((INT x:C. A x) Un B)"

   709   "!!A B C. (INT x:C. A Un B x)  = (A Un (INT x:C. B x))"

   710   "!!A B. (INT x: Union A. B x) = (INT y:A. INT x:y. B x)"

   711   "!!A B C. (INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)"

   712   "!!A B f. (INT x:fA. B x)    = (INT a:A. B (f a))"

   713   by auto

   714

   715 lemma ball_simps [simp,noatp]:

   716   "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"

   717   "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"

   718   "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"

   719   "!!A P Q. (ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)"

   720   "!!P. (ALL x:{}. P x) = True"

   721   "!!P. (ALL x:UNIV. P x) = (ALL x. P x)"

   722   "!!a B P. (ALL x:insert a B. P x) = (P a & (ALL x:B. P x))"

   723   "!!A P. (ALL x:Union A. P x) = (ALL y:A. ALL x:y. P x)"

   724   "!!A B P. (ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)"

   725   "!!P Q. (ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"

   726   "!!A P f. (ALL x:fA. P x) = (ALL x:A. P (f x))"

   727   "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"

   728   by auto

   729

   730 lemma bex_simps [simp,noatp]:

   731   "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"

   732   "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"

   733   "!!P. (EX x:{}. P x) = False"

   734   "!!P. (EX x:UNIV. P x) = (EX x. P x)"

   735   "!!a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))"

   736   "!!A P. (EX x:Union A. P x) = (EX y:A. EX x:y. P x)"

   737   "!!A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)"

   738   "!!P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)"

   739   "!!A P f. (EX x:fA. P x) = (EX x:A. P (f x))"

   740   "!!A P. (~(EX x:A. P x)) = (ALL x:A. ~P x)"

   741   by auto

   742

   743 lemma ball_conj_distrib:

   744   "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))"

   745   by blast

   746

   747 lemma bex_disj_distrib:

   748   "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))"

   749   by blast

   750

   751

   752 text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}

   753

   754 lemma UN_extend_simps:

   755   "!!a B C. insert a (UN x:C. B x) = (if C={} then {a} else (UN x:C. insert a (B x)))"

   756   "!!A B C. (UN x:C. A x) Un B    = (if C={} then B else (UN x:C. A x Un B))"

   757   "!!A B C. A Un (UN x:C. B x)   = (if C={} then A else (UN x:C. A Un B x))"

   758   "!!A B C. ((UN x:C. A x) Int B) = (UN x:C. A x Int B)"

   759   "!!A B C. (A Int (UN x:C. B x)) = (UN x:C. A Int B x)"

   760   "!!A B C. ((UN x:C. A x) - B) = (UN x:C. A x - B)"

   761   "!!A B C. (A - (INT x:C. B x)) = (UN x:C. A - B x)"

   762   "!!A B. (UN y:A. UN x:y. B x) = (UN x: Union A. B x)"

   763   "!!A B C. (UN  x:A. UN z: B(x). C z) = (UN z: UNION A B. C z)"

   764   "!!A B f. (UN a:A. B (f a)) = (UN x:fA. B x)"

   765   by auto

   766

   767 lemma INT_extend_simps:

   768   "!!A B C. (INT x:C. A x) Int B = (if C={} then B else (INT x:C. A x Int B))"

   769   "!!A B C. A Int (INT x:C. B x) = (if C={} then A else (INT x:C. A Int B x))"

   770   "!!A B C. (INT x:C. A x) - B   = (if C={} then UNIV-B else (INT x:C. A x - B))"

   771   "!!A B C. A - (UN x:C. B x)   = (if C={} then A else (INT x:C. A - B x))"

   772   "!!a B C. insert a (INT x:C. B x) = (INT x:C. insert a (B x))"

   773   "!!A B C. ((INT x:C. A x) Un B)  = (INT x:C. A x Un B)"

   774   "!!A B C. A Un (INT x:C. B x)  = (INT x:C. A Un B x)"

   775   "!!A B. (INT y:A. INT x:y. B x) = (INT x: Union A. B x)"

   776   "!!A B C. (INT x:A. INT z: B(x). C z) = (INT z: UNION A B. C z)"

   777   "!!A B f. (INT a:A. B (f a))    = (INT x:fA. B x)"

   778   by auto

   779

   780

   781 no_notation

   782   less_eq  (infix "\<sqsubseteq>" 50) and

   783   less (infix "\<sqsubset>" 50) and

   784   inf  (infixl "\<sqinter>" 70) and

   785   sup  (infixl "\<squnion>" 65) and

   786   Inf  ("\<Sqinter>_" [900] 900) and

   787   Sup  ("\<Squnion>_" [900] 900)

   788

   789 lemmas mem_simps =

   790   insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff

   791   mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff

   792   -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}

   793

   794 end
`