src/CCL/Set.thy
author wenzelm
Tue Jul 18 02:22:38 2006 +0200 (2006-07-18)
changeset 20140 98acc6d0fab6
parent 17456 bcf7544875b2
child 24825 c4f13ab78f9d
permissions -rw-r--r--
removed obsolete ML files;
wenzelm@17456
     1
(*  Title:      CCL/Set.thy
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
*)
clasohm@0
     4
wenzelm@17456
     5
header {* Extending FOL by a modified version of HOL set theory *}
wenzelm@17456
     6
wenzelm@17456
     7
theory Set
wenzelm@17456
     8
imports FOL
wenzelm@17456
     9
begin
clasohm@0
    10
wenzelm@3935
    11
global
wenzelm@3935
    12
wenzelm@17456
    13
typedecl 'a set
wenzelm@17456
    14
arities set :: ("term") "term"
clasohm@0
    15
clasohm@0
    16
consts
clasohm@0
    17
  Collect       :: "['a => o] => 'a set"                    (*comprehension*)
clasohm@0
    18
  Compl         :: "('a set) => 'a set"                     (*complement*)
clasohm@0
    19
  Int           :: "['a set, 'a set] => 'a set"         (infixl 70)
clasohm@0
    20
  Un            :: "['a set, 'a set] => 'a set"         (infixl 65)
wenzelm@17456
    21
  Union         :: "(('a set)set) => 'a set"                (*...of a set*)
wenzelm@17456
    22
  Inter         :: "(('a set)set) => 'a set"                (*...of a set*)
wenzelm@17456
    23
  UNION         :: "['a set, 'a => 'b set] => 'b set"       (*general*)
wenzelm@17456
    24
  INTER         :: "['a set, 'a => 'b set] => 'b set"       (*general*)
wenzelm@17456
    25
  Ball          :: "['a set, 'a => o] => o"                 (*bounded quants*)
wenzelm@17456
    26
  Bex           :: "['a set, 'a => o] => o"                 (*bounded quants*)
clasohm@0
    27
  mono          :: "['a set => 'b set] => o"                (*monotonicity*)
clasohm@0
    28
  ":"           :: "['a, 'a set] => o"                  (infixl 50) (*membership*)
clasohm@0
    29
  "<="          :: "['a set, 'a set] => o"              (infixl 50)
clasohm@0
    30
  singleton     :: "'a => 'a set"                       ("{_}")
clasohm@0
    31
  empty         :: "'a set"                             ("{}")
clasohm@0
    32
  "oo"          :: "['b => 'c, 'a => 'b, 'a] => 'c"     (infixr 50) (*composition*)
clasohm@0
    33
wenzelm@3935
    34
syntax
clasohm@0
    35
  "@Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
clasohm@0
    36
clasohm@0
    37
  (* Big Intersection / Union *)
clasohm@0
    38
clasohm@0
    39
  "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(INT _:_./ _)" [0, 0, 0] 10)
clasohm@0
    40
  "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(UN _:_./ _)" [0, 0, 0] 10)
clasohm@0
    41
clasohm@0
    42
  (* Bounded Quantifiers *)
clasohm@0
    43
clasohm@0
    44
  "@Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
clasohm@0
    45
  "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
clasohm@0
    46
clasohm@0
    47
translations
clasohm@0
    48
  "{x. P}"      == "Collect(%x. P)"
clasohm@0
    49
  "INT x:A. B"  == "INTER(A, %x. B)"
clasohm@0
    50
  "UN x:A. B"   == "UNION(A, %x. B)"
clasohm@0
    51
  "ALL x:A. P"  == "Ball(A, %x. P)"
clasohm@0
    52
  "EX x:A. P"   == "Bex(A, %x. P)"
clasohm@0
    53
wenzelm@3935
    54
local
clasohm@0
    55
wenzelm@17456
    56
axioms
wenzelm@17456
    57
  mem_Collect_iff:       "(a : {x. P(x)}) <-> P(a)"
wenzelm@17456
    58
  set_extension:         "A=B <-> (ALL x. x:A <-> x:B)"
clasohm@0
    59
wenzelm@17456
    60
defs
wenzelm@17456
    61
  Ball_def:      "Ball(A, P)  == ALL x. x:A --> P(x)"
wenzelm@17456
    62
  Bex_def:       "Bex(A, P)   == EX x. x:A & P(x)"
wenzelm@17456
    63
  mono_def:      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
wenzelm@17456
    64
  subset_def:    "A <= B      == ALL x:A. x:B"
wenzelm@17456
    65
  singleton_def: "{a}         == {x. x=a}"
wenzelm@17456
    66
  empty_def:     "{}          == {x. False}"
wenzelm@17456
    67
  Un_def:        "A Un B      == {x. x:A | x:B}"
wenzelm@17456
    68
  Int_def:       "A Int B     == {x. x:A & x:B}"
wenzelm@17456
    69
  Compl_def:     "Compl(A)    == {x. ~x:A}"
wenzelm@17456
    70
  INTER_def:     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
wenzelm@17456
    71
  UNION_def:     "UNION(A, B) == {y. EX x:A. y: B(x)}"
wenzelm@17456
    72
  Inter_def:     "Inter(S)    == (INT x:S. x)"
wenzelm@17456
    73
  Union_def:     "Union(S)    == (UN x:S. x)"
wenzelm@17456
    74
wenzelm@20140
    75
wenzelm@20140
    76
lemma CollectI: "[| P(a) |] ==> a : {x. P(x)}"
wenzelm@20140
    77
  apply (rule mem_Collect_iff [THEN iffD2])
wenzelm@20140
    78
  apply assumption
wenzelm@20140
    79
  done
wenzelm@20140
    80
wenzelm@20140
    81
lemma CollectD: "[| a : {x. P(x)} |] ==> P(a)"
wenzelm@20140
    82
  apply (erule mem_Collect_iff [THEN iffD1])
wenzelm@20140
    83
  done
wenzelm@20140
    84
wenzelm@20140
    85
lemmas CollectE = CollectD [elim_format]
wenzelm@20140
    86
wenzelm@20140
    87
lemma set_ext: "[| !!x. x:A <-> x:B |] ==> A = B"
wenzelm@20140
    88
  apply (rule set_extension [THEN iffD2])
wenzelm@20140
    89
  apply simp
wenzelm@20140
    90
  done
wenzelm@20140
    91
wenzelm@20140
    92
wenzelm@20140
    93
subsection {* Bounded quantifiers *}
wenzelm@20140
    94
wenzelm@20140
    95
lemma ballI: "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"
wenzelm@20140
    96
  by (simp add: Ball_def)
wenzelm@20140
    97
wenzelm@20140
    98
lemma bspec: "[| ALL x:A. P(x);  x:A |] ==> P(x)"
wenzelm@20140
    99
  by (simp add: Ball_def)
wenzelm@20140
   100
wenzelm@20140
   101
lemma ballE: "[| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q"
wenzelm@20140
   102
  unfolding Ball_def by blast
wenzelm@20140
   103
wenzelm@20140
   104
lemma bexI: "[| P(x);  x:A |] ==> EX x:A. P(x)"
wenzelm@20140
   105
  unfolding Bex_def by blast
wenzelm@20140
   106
wenzelm@20140
   107
lemma bexCI: "[| EX x:A. ~P(x) ==> P(a);  a:A |] ==> EX x:A. P(x)"
wenzelm@20140
   108
  unfolding Bex_def by blast
wenzelm@20140
   109
wenzelm@20140
   110
lemma bexE: "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q"
wenzelm@20140
   111
  unfolding Bex_def by blast
wenzelm@20140
   112
wenzelm@20140
   113
(*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
wenzelm@20140
   114
lemma ball_rew: "(ALL x:A. True) <-> True"
wenzelm@20140
   115
  by (blast intro: ballI)
wenzelm@20140
   116
wenzelm@20140
   117
wenzelm@20140
   118
subsection {* Congruence rules *}
wenzelm@20140
   119
wenzelm@20140
   120
lemma ball_cong:
wenzelm@20140
   121
  "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==>
wenzelm@20140
   122
    (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"
wenzelm@20140
   123
  by (blast intro: ballI elim: ballE)
wenzelm@20140
   124
wenzelm@20140
   125
lemma bex_cong:
wenzelm@20140
   126
  "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==>
wenzelm@20140
   127
    (EX x:A. P(x)) <-> (EX x:A'. P'(x))"
wenzelm@20140
   128
  by (blast intro: bexI elim: bexE)
wenzelm@20140
   129
wenzelm@20140
   130
wenzelm@20140
   131
subsection {* Rules for subsets *}
wenzelm@20140
   132
wenzelm@20140
   133
lemma subsetI: "(!!x. x:A ==> x:B) ==> A <= B"
wenzelm@20140
   134
  unfolding subset_def by (blast intro: ballI)
wenzelm@20140
   135
wenzelm@20140
   136
(*Rule in Modus Ponens style*)
wenzelm@20140
   137
lemma subsetD: "[| A <= B;  c:A |] ==> c:B"
wenzelm@20140
   138
  unfolding subset_def by (blast elim: ballE)
wenzelm@20140
   139
wenzelm@20140
   140
(*Classical elimination rule*)
wenzelm@20140
   141
lemma subsetCE: "[| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P"
wenzelm@20140
   142
  by (blast dest: subsetD)
wenzelm@20140
   143
wenzelm@20140
   144
lemma subset_refl: "A <= A"
wenzelm@20140
   145
  by (blast intro: subsetI)
wenzelm@20140
   146
wenzelm@20140
   147
lemma subset_trans: "[| A<=B;  B<=C |] ==> A<=C"
wenzelm@20140
   148
  by (blast intro: subsetI dest: subsetD)
wenzelm@20140
   149
wenzelm@20140
   150
wenzelm@20140
   151
subsection {* Rules for equality *}
wenzelm@20140
   152
wenzelm@20140
   153
(*Anti-symmetry of the subset relation*)
wenzelm@20140
   154
lemma subset_antisym: "[| A <= B;  B <= A |] ==> A = B"
wenzelm@20140
   155
  by (blast intro: set_ext dest: subsetD)
wenzelm@20140
   156
wenzelm@20140
   157
lemmas equalityI = subset_antisym
wenzelm@20140
   158
wenzelm@20140
   159
(* Equality rules from ZF set theory -- are they appropriate here? *)
wenzelm@20140
   160
lemma equalityD1: "A = B ==> A<=B"
wenzelm@20140
   161
  and equalityD2: "A = B ==> B<=A"
wenzelm@20140
   162
  by (simp_all add: subset_refl)
wenzelm@20140
   163
wenzelm@20140
   164
lemma equalityE: "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
wenzelm@20140
   165
  by (simp add: subset_refl)
wenzelm@20140
   166
wenzelm@20140
   167
lemma equalityCE:
wenzelm@20140
   168
    "[| A = B;  [| c:A; c:B |] ==> P;  [| ~ c:A; ~ c:B |] ==> P |]  ==>  P"
wenzelm@20140
   169
  by (blast elim: equalityE subsetCE)
wenzelm@20140
   170
wenzelm@20140
   171
lemma trivial_set: "{x. x:A} = A"
wenzelm@20140
   172
  by (blast intro: equalityI subsetI CollectI dest: CollectD)
wenzelm@20140
   173
wenzelm@20140
   174
wenzelm@20140
   175
subsection {* Rules for binary union *}
wenzelm@20140
   176
wenzelm@20140
   177
lemma UnI1: "c:A ==> c : A Un B"
wenzelm@20140
   178
  and UnI2: "c:B ==> c : A Un B"
wenzelm@20140
   179
  unfolding Un_def by (blast intro: CollectI)+
wenzelm@20140
   180
wenzelm@20140
   181
(*Classical introduction rule: no commitment to A vs B*)
wenzelm@20140
   182
lemma UnCI: "(~c:B ==> c:A) ==> c : A Un B"
wenzelm@20140
   183
  by (blast intro: UnI1 UnI2)
wenzelm@20140
   184
wenzelm@20140
   185
lemma UnE: "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
wenzelm@20140
   186
  unfolding Un_def by (blast dest: CollectD)
wenzelm@20140
   187
wenzelm@20140
   188
wenzelm@20140
   189
subsection {* Rules for small intersection *}
wenzelm@20140
   190
wenzelm@20140
   191
lemma IntI: "[| c:A;  c:B |] ==> c : A Int B"
wenzelm@20140
   192
  unfolding Int_def by (blast intro: CollectI)
wenzelm@20140
   193
wenzelm@20140
   194
lemma IntD1: "c : A Int B ==> c:A"
wenzelm@20140
   195
  and IntD2: "c : A Int B ==> c:B"
wenzelm@20140
   196
  unfolding Int_def by (blast dest: CollectD)+
wenzelm@20140
   197
wenzelm@20140
   198
lemma IntE: "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
wenzelm@20140
   199
  by (blast dest: IntD1 IntD2)
wenzelm@20140
   200
wenzelm@20140
   201
wenzelm@20140
   202
subsection {* Rules for set complement *}
wenzelm@20140
   203
wenzelm@20140
   204
lemma ComplI: "[| c:A ==> False |] ==> c : Compl(A)"
wenzelm@20140
   205
  unfolding Compl_def by (blast intro: CollectI)
wenzelm@20140
   206
wenzelm@20140
   207
(*This form, with negated conclusion, works well with the Classical prover.
wenzelm@20140
   208
  Negated assumptions behave like formulae on the right side of the notional
wenzelm@20140
   209
  turnstile...*)
wenzelm@20140
   210
lemma ComplD: "[| c : Compl(A) |] ==> ~c:A"
wenzelm@20140
   211
  unfolding Compl_def by (blast dest: CollectD)
wenzelm@20140
   212
wenzelm@20140
   213
lemmas ComplE = ComplD [elim_format]
wenzelm@20140
   214
wenzelm@20140
   215
wenzelm@20140
   216
subsection {* Empty sets *}
wenzelm@20140
   217
wenzelm@20140
   218
lemma empty_eq: "{x. False} = {}"
wenzelm@20140
   219
  by (simp add: empty_def)
wenzelm@20140
   220
wenzelm@20140
   221
lemma emptyD: "a : {} ==> P"
wenzelm@20140
   222
  unfolding empty_def by (blast dest: CollectD)
wenzelm@20140
   223
wenzelm@20140
   224
lemmas emptyE = emptyD [elim_format]
wenzelm@20140
   225
wenzelm@20140
   226
lemma not_emptyD:
wenzelm@20140
   227
  assumes "~ A={}"
wenzelm@20140
   228
  shows "EX x. x:A"
wenzelm@20140
   229
proof -
wenzelm@20140
   230
  have "\<not> (EX x. x:A) \<Longrightarrow> A = {}"
wenzelm@20140
   231
    by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+
wenzelm@20140
   232
  with prems show ?thesis by blast
wenzelm@20140
   233
qed
wenzelm@20140
   234
wenzelm@20140
   235
wenzelm@20140
   236
subsection {* Singleton sets *}
wenzelm@20140
   237
wenzelm@20140
   238
lemma singletonI: "a : {a}"
wenzelm@20140
   239
  unfolding singleton_def by (blast intro: CollectI)
wenzelm@20140
   240
wenzelm@20140
   241
lemma singletonD: "b : {a} ==> b=a"
wenzelm@20140
   242
  unfolding singleton_def by (blast dest: CollectD)
wenzelm@20140
   243
wenzelm@20140
   244
lemmas singletonE = singletonD [elim_format]
wenzelm@20140
   245
wenzelm@20140
   246
wenzelm@20140
   247
subsection {* Unions of families *}
wenzelm@20140
   248
wenzelm@20140
   249
(*The order of the premises presupposes that A is rigid; b may be flexible*)
wenzelm@20140
   250
lemma UN_I: "[| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))"
wenzelm@20140
   251
  unfolding UNION_def by (blast intro: bexI CollectI)
wenzelm@20140
   252
wenzelm@20140
   253
lemma UN_E: "[| b : (UN x:A. B(x));  !!x.[| x:A;  b: B(x) |] ==> R |] ==> R"
wenzelm@20140
   254
  unfolding UNION_def by (blast dest: CollectD elim: bexE)
wenzelm@20140
   255
wenzelm@20140
   256
lemma UN_cong:
wenzelm@20140
   257
  "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==>
wenzelm@20140
   258
    (UN x:A. C(x)) = (UN x:B. D(x))"
wenzelm@20140
   259
  by (simp add: UNION_def cong: bex_cong)
wenzelm@20140
   260
wenzelm@20140
   261
wenzelm@20140
   262
subsection {* Intersections of families *}
wenzelm@20140
   263
wenzelm@20140
   264
lemma INT_I: "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"
wenzelm@20140
   265
  unfolding INTER_def by (blast intro: CollectI ballI)
wenzelm@20140
   266
wenzelm@20140
   267
lemma INT_D: "[| b : (INT x:A. B(x));  a:A |] ==> b: B(a)"
wenzelm@20140
   268
  unfolding INTER_def by (blast dest: CollectD bspec)
wenzelm@20140
   269
wenzelm@20140
   270
(*"Classical" elimination rule -- does not require proving X:C *)
wenzelm@20140
   271
lemma INT_E: "[| b : (INT x:A. B(x));  b: B(a) ==> R;  ~ a:A ==> R |] ==> R"
wenzelm@20140
   272
  unfolding INTER_def by (blast dest: CollectD bspec)
wenzelm@20140
   273
wenzelm@20140
   274
lemma INT_cong:
wenzelm@20140
   275
  "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==>
wenzelm@20140
   276
    (INT x:A. C(x)) = (INT x:B. D(x))"
wenzelm@20140
   277
  by (simp add: INTER_def cong: ball_cong)
wenzelm@20140
   278
wenzelm@20140
   279
wenzelm@20140
   280
subsection {* Rules for Unions *}
wenzelm@20140
   281
wenzelm@20140
   282
(*The order of the premises presupposes that C is rigid; A may be flexible*)
wenzelm@20140
   283
lemma UnionI: "[| X:C;  A:X |] ==> A : Union(C)"
wenzelm@20140
   284
  unfolding Union_def by (blast intro: UN_I)
wenzelm@20140
   285
wenzelm@20140
   286
lemma UnionE: "[| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R"
wenzelm@20140
   287
  unfolding Union_def by (blast elim: UN_E)
wenzelm@20140
   288
wenzelm@20140
   289
wenzelm@20140
   290
subsection {* Rules for Inter *}
wenzelm@20140
   291
wenzelm@20140
   292
lemma InterI: "[| !!X. X:C ==> A:X |] ==> A : Inter(C)"
wenzelm@20140
   293
  unfolding Inter_def by (blast intro: INT_I)
wenzelm@20140
   294
wenzelm@20140
   295
(*A "destruct" rule -- every X in C contains A as an element, but
wenzelm@20140
   296
  A:X can hold when X:C does not!  This rule is analogous to "spec". *)
wenzelm@20140
   297
lemma InterD: "[| A : Inter(C);  X:C |] ==> A:X"
wenzelm@20140
   298
  unfolding Inter_def by (blast dest: INT_D)
wenzelm@20140
   299
wenzelm@20140
   300
(*"Classical" elimination rule -- does not require proving X:C *)
wenzelm@20140
   301
lemma InterE: "[| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R"
wenzelm@20140
   302
  unfolding Inter_def by (blast elim: INT_E)
wenzelm@20140
   303
wenzelm@20140
   304
wenzelm@20140
   305
section {* Derived rules involving subsets; Union and Intersection as lattice operations *}
wenzelm@20140
   306
wenzelm@20140
   307
subsection {* Big Union -- least upper bound of a set *}
wenzelm@20140
   308
wenzelm@20140
   309
lemma Union_upper: "B:A ==> B <= Union(A)"
wenzelm@20140
   310
  by (blast intro: subsetI UnionI)
wenzelm@20140
   311
wenzelm@20140
   312
lemma Union_least: "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"
wenzelm@20140
   313
  by (blast intro: subsetI dest: subsetD elim: UnionE)
wenzelm@20140
   314
wenzelm@20140
   315
wenzelm@20140
   316
subsection {* Big Intersection -- greatest lower bound of a set *}
wenzelm@20140
   317
wenzelm@20140
   318
lemma Inter_lower: "B:A ==> Inter(A) <= B"
wenzelm@20140
   319
  by (blast intro: subsetI dest: InterD)
wenzelm@20140
   320
wenzelm@20140
   321
lemma Inter_greatest: "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"
wenzelm@20140
   322
  by (blast intro: subsetI InterI dest: subsetD)
wenzelm@20140
   323
wenzelm@20140
   324
wenzelm@20140
   325
subsection {* Finite Union -- the least upper bound of 2 sets *}
wenzelm@20140
   326
wenzelm@20140
   327
lemma Un_upper1: "A <= A Un B"
wenzelm@20140
   328
  by (blast intro: subsetI UnI1)
wenzelm@20140
   329
wenzelm@20140
   330
lemma Un_upper2: "B <= A Un B"
wenzelm@20140
   331
  by (blast intro: subsetI UnI2)
wenzelm@20140
   332
wenzelm@20140
   333
lemma Un_least: "[| A<=C;  B<=C |] ==> A Un B <= C"
wenzelm@20140
   334
  by (blast intro: subsetI elim: UnE dest: subsetD)
wenzelm@20140
   335
wenzelm@20140
   336
wenzelm@20140
   337
subsection {* Finite Intersection -- the greatest lower bound of 2 sets *}
wenzelm@20140
   338
wenzelm@20140
   339
lemma Int_lower1: "A Int B <= A"
wenzelm@20140
   340
  by (blast intro: subsetI elim: IntE)
wenzelm@20140
   341
wenzelm@20140
   342
lemma Int_lower2: "A Int B <= B"
wenzelm@20140
   343
  by (blast intro: subsetI elim: IntE)
wenzelm@20140
   344
wenzelm@20140
   345
lemma Int_greatest: "[| C<=A;  C<=B |] ==> C <= A Int B"
wenzelm@20140
   346
  by (blast intro: subsetI IntI dest: subsetD)
wenzelm@20140
   347
wenzelm@20140
   348
wenzelm@20140
   349
subsection {* Monotonicity *}
wenzelm@20140
   350
wenzelm@20140
   351
lemma monoI: "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"
wenzelm@20140
   352
  unfolding mono_def by blast
wenzelm@20140
   353
wenzelm@20140
   354
lemma monoD: "[| mono(f);  A <= B |] ==> f(A) <= f(B)"
wenzelm@20140
   355
  unfolding mono_def by blast
wenzelm@20140
   356
wenzelm@20140
   357
lemma mono_Un: "mono(f) ==> f(A) Un f(B) <= f(A Un B)"
wenzelm@20140
   358
  by (blast intro: Un_least dest: monoD intro: Un_upper1 Un_upper2)
wenzelm@20140
   359
wenzelm@20140
   360
lemma mono_Int: "mono(f) ==> f(A Int B) <= f(A) Int f(B)"
wenzelm@20140
   361
  by (blast intro: Int_greatest dest: monoD intro: Int_lower1 Int_lower2)
wenzelm@20140
   362
wenzelm@20140
   363
wenzelm@20140
   364
subsection {* Automated reasoning setup *}
wenzelm@20140
   365
wenzelm@20140
   366
lemmas [intro!] = ballI subsetI InterI INT_I CollectI ComplI IntI UnCI singletonI
wenzelm@20140
   367
  and [intro] = bexI UnionI UN_I
wenzelm@20140
   368
  and [elim!] = bexE UnionE UN_E CollectE ComplE IntE UnE emptyE singletonE
wenzelm@20140
   369
  and [elim] = ballE InterD InterE INT_D INT_E subsetD subsetCE
wenzelm@20140
   370
wenzelm@20140
   371
lemma mem_rews:
wenzelm@20140
   372
  "(a : A Un B)   <->  (a:A | a:B)"
wenzelm@20140
   373
  "(a : A Int B)  <->  (a:A & a:B)"
wenzelm@20140
   374
  "(a : Compl(B)) <->  (~a:B)"
wenzelm@20140
   375
  "(a : {b})      <->  (a=b)"
wenzelm@20140
   376
  "(a : {})       <->   False"
wenzelm@20140
   377
  "(a : {x. P(x)}) <->  P(a)"
wenzelm@20140
   378
  by blast+
wenzelm@20140
   379
wenzelm@20140
   380
lemmas [simp] = trivial_set empty_eq mem_rews
wenzelm@20140
   381
  and [cong] = ball_cong bex_cong INT_cong UN_cong
wenzelm@20140
   382
wenzelm@20140
   383
wenzelm@20140
   384
section {* Equalities involving union, intersection, inclusion, etc. *}
wenzelm@20140
   385
wenzelm@20140
   386
subsection {* Binary Intersection *}
wenzelm@20140
   387
wenzelm@20140
   388
lemma Int_absorb: "A Int A = A"
wenzelm@20140
   389
  by (blast intro: equalityI)
wenzelm@20140
   390
wenzelm@20140
   391
lemma Int_commute: "A Int B  =  B Int A"
wenzelm@20140
   392
  by (blast intro: equalityI)
wenzelm@20140
   393
wenzelm@20140
   394
lemma Int_assoc: "(A Int B) Int C  =  A Int (B Int C)"
wenzelm@20140
   395
  by (blast intro: equalityI)
wenzelm@20140
   396
wenzelm@20140
   397
lemma Int_Un_distrib: "(A Un B) Int C  =  (A Int C) Un (B Int C)"
wenzelm@20140
   398
  by (blast intro: equalityI)
wenzelm@20140
   399
wenzelm@20140
   400
lemma subset_Int_eq: "(A<=B) <-> (A Int B = A)"
wenzelm@20140
   401
  by (blast intro: equalityI elim: equalityE)
wenzelm@20140
   402
wenzelm@20140
   403
wenzelm@20140
   404
subsection {* Binary Union *}
wenzelm@20140
   405
wenzelm@20140
   406
lemma Un_absorb: "A Un A = A"
wenzelm@20140
   407
  by (blast intro: equalityI)
wenzelm@20140
   408
wenzelm@20140
   409
lemma Un_commute: "A Un B  =  B Un A"
wenzelm@20140
   410
  by (blast intro: equalityI)
wenzelm@20140
   411
wenzelm@20140
   412
lemma Un_assoc: "(A Un B) Un C  =  A Un (B Un C)"
wenzelm@20140
   413
  by (blast intro: equalityI)
wenzelm@20140
   414
wenzelm@20140
   415
lemma Un_Int_distrib: "(A Int B) Un C  =  (A Un C) Int (B Un C)"
wenzelm@20140
   416
  by (blast intro: equalityI)
wenzelm@20140
   417
wenzelm@20140
   418
lemma Un_Int_crazy:
wenzelm@20140
   419
    "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"
wenzelm@20140
   420
  by (blast intro: equalityI)
wenzelm@20140
   421
wenzelm@20140
   422
lemma subset_Un_eq: "(A<=B) <-> (A Un B = B)"
wenzelm@20140
   423
  by (blast intro: equalityI elim: equalityE)
wenzelm@20140
   424
wenzelm@20140
   425
wenzelm@20140
   426
subsection {* Simple properties of @{text "Compl"} -- complement of a set *}
wenzelm@20140
   427
wenzelm@20140
   428
lemma Compl_disjoint: "A Int Compl(A) = {x. False}"
wenzelm@20140
   429
  by (blast intro: equalityI)
wenzelm@20140
   430
wenzelm@20140
   431
lemma Compl_partition: "A Un Compl(A) = {x. True}"
wenzelm@20140
   432
  by (blast intro: equalityI)
wenzelm@20140
   433
wenzelm@20140
   434
lemma double_complement: "Compl(Compl(A)) = A"
wenzelm@20140
   435
  by (blast intro: equalityI)
wenzelm@20140
   436
wenzelm@20140
   437
lemma Compl_Un: "Compl(A Un B) = Compl(A) Int Compl(B)"
wenzelm@20140
   438
  by (blast intro: equalityI)
wenzelm@20140
   439
wenzelm@20140
   440
lemma Compl_Int: "Compl(A Int B) = Compl(A) Un Compl(B)"
wenzelm@20140
   441
  by (blast intro: equalityI)
wenzelm@20140
   442
wenzelm@20140
   443
lemma Compl_UN: "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))"
wenzelm@20140
   444
  by (blast intro: equalityI)
wenzelm@20140
   445
wenzelm@20140
   446
lemma Compl_INT: "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))"
wenzelm@20140
   447
  by (blast intro: equalityI)
wenzelm@20140
   448
wenzelm@20140
   449
(*Halmos, Naive Set Theory, page 16.*)
wenzelm@20140
   450
lemma Un_Int_assoc_eq: "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)"
wenzelm@20140
   451
  by (blast intro: equalityI elim: equalityE)
wenzelm@20140
   452
wenzelm@20140
   453
wenzelm@20140
   454
subsection {* Big Union and Intersection *}
wenzelm@20140
   455
wenzelm@20140
   456
lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)"
wenzelm@20140
   457
  by (blast intro: equalityI)
wenzelm@20140
   458
wenzelm@20140
   459
lemma Union_disjoint:
wenzelm@20140
   460
    "(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})"
wenzelm@20140
   461
  by (blast intro: equalityI elim: equalityE)
wenzelm@20140
   462
wenzelm@20140
   463
lemma Inter_Un_distrib: "Inter(A Un B) = Inter(A) Int Inter(B)"
wenzelm@20140
   464
  by (blast intro: equalityI)
wenzelm@20140
   465
wenzelm@20140
   466
wenzelm@20140
   467
subsection {* Unions and Intersections of Families *}
wenzelm@20140
   468
wenzelm@20140
   469
lemma UN_eq: "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})"
wenzelm@20140
   470
  by (blast intro: equalityI)
wenzelm@20140
   471
wenzelm@20140
   472
(*Look: it has an EXISTENTIAL quantifier*)
wenzelm@20140
   473
lemma INT_eq: "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})"
wenzelm@20140
   474
  by (blast intro: equalityI)
wenzelm@20140
   475
wenzelm@20140
   476
lemma Int_Union_image: "A Int Union(B) = (UN C:B. A Int C)"
wenzelm@20140
   477
  by (blast intro: equalityI)
wenzelm@20140
   478
wenzelm@20140
   479
lemma Un_Inter_image: "A Un Inter(B) = (INT C:B. A Un C)"
wenzelm@20140
   480
  by (blast intro: equalityI)
wenzelm@20140
   481
wenzelm@20140
   482
wenzelm@20140
   483
section {* Monotonicity of various operations *}
wenzelm@20140
   484
wenzelm@20140
   485
lemma Union_mono: "A<=B ==> Union(A) <= Union(B)"
wenzelm@20140
   486
  by blast
wenzelm@20140
   487
wenzelm@20140
   488
lemma Inter_anti_mono: "[| B<=A |] ==> Inter(A) <= Inter(B)"
wenzelm@20140
   489
  by blast
wenzelm@20140
   490
wenzelm@20140
   491
lemma UN_mono:
wenzelm@20140
   492
  "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==>  
wenzelm@20140
   493
    (UN x:A. f(x)) <= (UN x:B. g(x))"
wenzelm@20140
   494
  by blast
wenzelm@20140
   495
wenzelm@20140
   496
lemma INT_anti_mono:
wenzelm@20140
   497
  "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==>  
wenzelm@20140
   498
    (INT x:A. f(x)) <= (INT x:A. g(x))"
wenzelm@20140
   499
  by blast
wenzelm@20140
   500
wenzelm@20140
   501
lemma Un_mono: "[| A<=C;  B<=D |] ==> A Un B <= C Un D"
wenzelm@20140
   502
  by blast
wenzelm@20140
   503
wenzelm@20140
   504
lemma Int_mono: "[| A<=C;  B<=D |] ==> A Int B <= C Int D"
wenzelm@20140
   505
  by blast
wenzelm@20140
   506
wenzelm@20140
   507
lemma Compl_anti_mono: "[| A<=B |] ==> Compl(B) <= Compl(A)"
wenzelm@20140
   508
  by blast
clasohm@0
   509
clasohm@0
   510
end