src/HOL/Set.ML
author oheimb
Fri May 31 19:12:00 1996 +0200 (1996-05-31)
changeset 1776 d7e77cb8ce5c
parent 1762 6e481897a811
child 1816 b03dba9116d4
permissions -rw-r--r--
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
as there have been unnecessary proofs of anonymous thms, which could not be
removed (by name) from the !simpset where necessary. All these thms except
singleton_iff were already proved in Set.ML.
therefore in Set.ML: New version of singletonE, proof of new thm singleton_iff
clasohm@1465
     1
(*  Title:      HOL/set
clasohm@923
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1991  University of Cambridge
clasohm@923
     5
clasohm@923
     6
For set.thy.  Set theory for higher-order logic.  A set is simply a predicate.
clasohm@923
     7
*)
clasohm@923
     8
clasohm@923
     9
open Set;
clasohm@923
    10
nipkow@1548
    11
section "Relating predicates and sets";
nipkow@1548
    12
nipkow@1548
    13
val [prem] = goal Set.thy "P(a) ==> a : {x.P(x)}";
clasohm@923
    14
by (rtac (mem_Collect_eq RS ssubst) 1);
clasohm@923
    15
by (rtac prem 1);
clasohm@923
    16
qed "CollectI";
clasohm@923
    17
clasohm@923
    18
val prems = goal Set.thy "[| a : {x.P(x)} |] ==> P(a)";
clasohm@923
    19
by (resolve_tac (prems RL [mem_Collect_eq  RS subst]) 1);
clasohm@923
    20
qed "CollectD";
clasohm@923
    21
clasohm@923
    22
val [prem] = goal Set.thy "[| !!x. (x:A) = (x:B) |] ==> A = B";
clasohm@923
    23
by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
clasohm@923
    24
by (rtac Collect_mem_eq 1);
clasohm@923
    25
by (rtac Collect_mem_eq 1);
clasohm@923
    26
qed "set_ext";
clasohm@923
    27
clasohm@923
    28
val [prem] = goal Set.thy "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
clasohm@923
    29
by (rtac (prem RS ext RS arg_cong) 1);
clasohm@923
    30
qed "Collect_cong";
clasohm@923
    31
clasohm@923
    32
val CollectE = make_elim CollectD;
clasohm@923
    33
nipkow@1548
    34
section "Bounded quantifiers";
clasohm@923
    35
clasohm@923
    36
val prems = goalw Set.thy [Ball_def]
clasohm@923
    37
    "[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)";
clasohm@923
    38
by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
clasohm@923
    39
qed "ballI";
clasohm@923
    40
clasohm@923
    41
val [major,minor] = goalw Set.thy [Ball_def]
clasohm@923
    42
    "[| ! x:A. P(x);  x:A |] ==> P(x)";
clasohm@923
    43
by (rtac (minor RS (major RS spec RS mp)) 1);
clasohm@923
    44
qed "bspec";
clasohm@923
    45
clasohm@923
    46
val major::prems = goalw Set.thy [Ball_def]
clasohm@923
    47
    "[| ! x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q";
clasohm@923
    48
by (rtac (major RS spec RS impCE) 1);
clasohm@923
    49
by (REPEAT (eresolve_tac prems 1));
clasohm@923
    50
qed "ballE";
clasohm@923
    51
clasohm@923
    52
(*Takes assumptions ! x:A.P(x) and a:A; creates assumption P(a)*)
clasohm@923
    53
fun ball_tac i = etac ballE i THEN contr_tac (i+1);
clasohm@923
    54
clasohm@923
    55
val prems = goalw Set.thy [Bex_def]
clasohm@923
    56
    "[| P(x);  x:A |] ==> ? x:A. P(x)";
clasohm@923
    57
by (REPEAT (ares_tac (prems @ [exI,conjI]) 1));
clasohm@923
    58
qed "bexI";
clasohm@923
    59
clasohm@923
    60
qed_goal "bexCI" Set.thy 
clasohm@923
    61
   "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A.P(x)"
clasohm@923
    62
 (fn prems=>
clasohm@923
    63
  [ (rtac classical 1),
clasohm@923
    64
    (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ]);
clasohm@923
    65
clasohm@923
    66
val major::prems = goalw Set.thy [Bex_def]
clasohm@923
    67
    "[| ? x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q";
clasohm@923
    68
by (rtac (major RS exE) 1);
clasohm@923
    69
by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1));
clasohm@923
    70
qed "bexE";
clasohm@923
    71
clasohm@923
    72
(*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
paulson@1618
    73
goal Set.thy "(! x:A. True) = True";
clasohm@923
    74
by (REPEAT (ares_tac [TrueI,ballI,iffI] 1));
clasohm@923
    75
qed "ball_rew";
paulson@1618
    76
Addsimps [ball_rew];
clasohm@923
    77
clasohm@923
    78
(** Congruence rules **)
clasohm@923
    79
clasohm@923
    80
val prems = goal Set.thy
clasohm@923
    81
    "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
clasohm@923
    82
\    (! x:A. P(x)) = (! x:B. Q(x))";
clasohm@923
    83
by (resolve_tac (prems RL [ssubst]) 1);
clasohm@923
    84
by (REPEAT (ares_tac [ballI,iffI] 1
clasohm@923
    85
     ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1));
clasohm@923
    86
qed "ball_cong";
clasohm@923
    87
clasohm@923
    88
val prems = goal Set.thy
clasohm@923
    89
    "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
clasohm@923
    90
\    (? x:A. P(x)) = (? x:B. Q(x))";
clasohm@923
    91
by (resolve_tac (prems RL [ssubst]) 1);
clasohm@923
    92
by (REPEAT (etac bexE 1
clasohm@923
    93
     ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1));
clasohm@923
    94
qed "bex_cong";
clasohm@923
    95
nipkow@1548
    96
section "Subsets";
clasohm@923
    97
clasohm@923
    98
val prems = goalw Set.thy [subset_def] "(!!x.x:A ==> x:B) ==> A <= B";
clasohm@923
    99
by (REPEAT (ares_tac (prems @ [ballI]) 1));
clasohm@923
   100
qed "subsetI";
clasohm@923
   101
clasohm@923
   102
(*Rule in Modus Ponens style*)
clasohm@923
   103
val major::prems = goalw Set.thy [subset_def] "[| A <= B;  c:A |] ==> c:B";
clasohm@923
   104
by (rtac (major RS bspec) 1);
clasohm@923
   105
by (resolve_tac prems 1);
clasohm@923
   106
qed "subsetD";
clasohm@923
   107
clasohm@923
   108
(*The same, with reversed premises for use with etac -- cf rev_mp*)
clasohm@923
   109
qed_goal "rev_subsetD" Set.thy "[| c:A;  A <= B |] ==> c:B"
clasohm@923
   110
 (fn prems=>  [ (REPEAT (resolve_tac (prems@[subsetD]) 1)) ]);
clasohm@923
   111
clasohm@923
   112
(*Classical elimination rule*)
clasohm@923
   113
val major::prems = goalw Set.thy [subset_def] 
clasohm@923
   114
    "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P";
clasohm@923
   115
by (rtac (major RS ballE) 1);
clasohm@923
   116
by (REPEAT (eresolve_tac prems 1));
clasohm@923
   117
qed "subsetCE";
clasohm@923
   118
clasohm@923
   119
(*Takes assumptions A<=B; c:A and creates the assumption c:B *)
clasohm@923
   120
fun set_mp_tac i = etac subsetCE i  THEN  mp_tac i;
clasohm@923
   121
clasohm@923
   122
qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
clasohm@923
   123
 (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
clasohm@923
   124
clasohm@923
   125
val prems = goal Set.thy "[| A<=B;  B<=C |] ==> A<=(C::'a set)";
clasohm@923
   126
by (cut_facts_tac prems 1);
clasohm@923
   127
by (REPEAT (ares_tac [subsetI] 1 ORELSE set_mp_tac 1));
clasohm@923
   128
qed "subset_trans";
clasohm@923
   129
clasohm@923
   130
nipkow@1548
   131
section "Equality";
clasohm@923
   132
clasohm@923
   133
(*Anti-symmetry of the subset relation*)
clasohm@923
   134
val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = (B::'a set)";
clasohm@923
   135
by (rtac (iffI RS set_ext) 1);
clasohm@923
   136
by (REPEAT (ares_tac (prems RL [subsetD]) 1));
clasohm@923
   137
qed "subset_antisym";
clasohm@923
   138
val equalityI = subset_antisym;
clasohm@923
   139
berghofe@1762
   140
AddSIs [equalityI];
berghofe@1762
   141
clasohm@923
   142
(* Equality rules from ZF set theory -- are they appropriate here? *)
clasohm@923
   143
val prems = goal Set.thy "A = B ==> A<=(B::'a set)";
clasohm@923
   144
by (resolve_tac (prems RL [subst]) 1);
clasohm@923
   145
by (rtac subset_refl 1);
clasohm@923
   146
qed "equalityD1";
clasohm@923
   147
clasohm@923
   148
val prems = goal Set.thy "A = B ==> B<=(A::'a set)";
clasohm@923
   149
by (resolve_tac (prems RL [subst]) 1);
clasohm@923
   150
by (rtac subset_refl 1);
clasohm@923
   151
qed "equalityD2";
clasohm@923
   152
clasohm@923
   153
val prems = goal Set.thy
clasohm@923
   154
    "[| A = B;  [| A<=B; B<=(A::'a set) |] ==> P |]  ==>  P";
clasohm@923
   155
by (resolve_tac prems 1);
clasohm@923
   156
by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
clasohm@923
   157
qed "equalityE";
clasohm@923
   158
clasohm@923
   159
val major::prems = goal Set.thy
clasohm@923
   160
    "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
clasohm@923
   161
by (rtac (major RS equalityE) 1);
clasohm@923
   162
by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
clasohm@923
   163
qed "equalityCE";
clasohm@923
   164
clasohm@923
   165
(*Lemma for creating induction formulae -- for "pattern matching" on p
clasohm@923
   166
  To make the induction hypotheses usable, apply "spec" or "bspec" to
clasohm@923
   167
  put universal quantifiers over the free variables in p. *)
clasohm@923
   168
val prems = goal Set.thy 
clasohm@923
   169
    "[| p:A;  !!z. z:A ==> p=z --> R |] ==> R";
clasohm@923
   170
by (rtac mp 1);
clasohm@923
   171
by (REPEAT (resolve_tac (refl::prems) 1));
clasohm@923
   172
qed "setup_induction";
clasohm@923
   173
clasohm@923
   174
nipkow@1548
   175
section "Set complement -- Compl";
clasohm@923
   176
clasohm@923
   177
val prems = goalw Set.thy [Compl_def]
clasohm@923
   178
    "[| c:A ==> False |] ==> c : Compl(A)";
clasohm@923
   179
by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
clasohm@923
   180
qed "ComplI";
clasohm@923
   181
clasohm@923
   182
(*This form, with negated conclusion, works well with the Classical prover.
clasohm@923
   183
  Negated assumptions behave like formulae on the right side of the notional
clasohm@923
   184
  turnstile...*)
clasohm@923
   185
val major::prems = goalw Set.thy [Compl_def]
clasohm@923
   186
    "[| c : Compl(A) |] ==> c~:A";
clasohm@923
   187
by (rtac (major RS CollectD) 1);
clasohm@923
   188
qed "ComplD";
clasohm@923
   189
clasohm@923
   190
val ComplE = make_elim ComplD;
clasohm@923
   191
paulson@1640
   192
qed_goal "Compl_iff" Set.thy "(c : Compl(A)) = (c~:A)"
berghofe@1760
   193
 (fn _ => [ (fast_tac (!claset addSIs [ComplI] addSEs [ComplE]) 1) ]);
paulson@1640
   194
clasohm@923
   195
nipkow@1548
   196
section "Binary union -- Un";
clasohm@923
   197
clasohm@923
   198
val prems = goalw Set.thy [Un_def] "c:A ==> c : A Un B";
clasohm@923
   199
by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1));
clasohm@923
   200
qed "UnI1";
clasohm@923
   201
clasohm@923
   202
val prems = goalw Set.thy [Un_def] "c:B ==> c : A Un B";
clasohm@923
   203
by (REPEAT (resolve_tac (prems @ [CollectI,disjI2]) 1));
clasohm@923
   204
qed "UnI2";
clasohm@923
   205
clasohm@923
   206
(*Classical introduction rule: no commitment to A vs B*)
clasohm@923
   207
qed_goal "UnCI" Set.thy "(c~:B ==> c:A) ==> c : A Un B"
clasohm@923
   208
 (fn prems=>
clasohm@923
   209
  [ (rtac classical 1),
clasohm@923
   210
    (REPEAT (ares_tac (prems@[UnI1,notI]) 1)),
clasohm@923
   211
    (REPEAT (ares_tac (prems@[UnI2,notE]) 1)) ]);
clasohm@923
   212
clasohm@923
   213
val major::prems = goalw Set.thy [Un_def]
clasohm@923
   214
    "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P";
clasohm@923
   215
by (rtac (major RS CollectD RS disjE) 1);
clasohm@923
   216
by (REPEAT (eresolve_tac prems 1));
clasohm@923
   217
qed "UnE";
clasohm@923
   218
paulson@1640
   219
qed_goal "Un_iff" Set.thy "(c : A Un B) = (c:A | c:B)"
berghofe@1760
   220
 (fn _ => [ (fast_tac (!claset addSIs [UnCI] addSEs [UnE]) 1) ]);
paulson@1640
   221
clasohm@923
   222
nipkow@1548
   223
section "Binary intersection -- Int";
clasohm@923
   224
clasohm@923
   225
val prems = goalw Set.thy [Int_def]
clasohm@923
   226
    "[| c:A;  c:B |] ==> c : A Int B";
clasohm@923
   227
by (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1));
clasohm@923
   228
qed "IntI";
clasohm@923
   229
clasohm@923
   230
val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:A";
clasohm@923
   231
by (rtac (major RS CollectD RS conjunct1) 1);
clasohm@923
   232
qed "IntD1";
clasohm@923
   233
clasohm@923
   234
val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:B";
clasohm@923
   235
by (rtac (major RS CollectD RS conjunct2) 1);
clasohm@923
   236
qed "IntD2";
clasohm@923
   237
clasohm@923
   238
val [major,minor] = goal Set.thy
clasohm@923
   239
    "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P";
clasohm@923
   240
by (rtac minor 1);
clasohm@923
   241
by (rtac (major RS IntD1) 1);
clasohm@923
   242
by (rtac (major RS IntD2) 1);
clasohm@923
   243
qed "IntE";
clasohm@923
   244
paulson@1640
   245
qed_goal "Int_iff" Set.thy "(c : A Int B) = (c:A & c:B)"
berghofe@1760
   246
 (fn _ => [ (fast_tac (!claset addSIs [IntI] addSEs [IntE]) 1) ]);
paulson@1640
   247
clasohm@923
   248
nipkow@1548
   249
section "Set difference";
clasohm@923
   250
clasohm@923
   251
qed_goalw "DiffI" Set.thy [set_diff_def]
clasohm@923
   252
    "[| c : A;  c ~: B |] ==> c : A - B"
clasohm@923
   253
 (fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)) ]);
clasohm@923
   254
clasohm@923
   255
qed_goalw "DiffD1" Set.thy [set_diff_def]
clasohm@923
   256
    "c : A - B ==> c : A"
clasohm@923
   257
 (fn [major]=> [ (rtac (major RS CollectD RS conjunct1) 1) ]);
clasohm@923
   258
clasohm@923
   259
qed_goalw "DiffD2" Set.thy [set_diff_def]
clasohm@923
   260
    "[| c : A - B;  c : B |] ==> P"
clasohm@923
   261
 (fn [major,minor]=>
clasohm@923
   262
     [rtac (minor RS (major RS CollectD RS conjunct2 RS notE)) 1]);
clasohm@923
   263
clasohm@923
   264
qed_goal "DiffE" Set.thy
clasohm@923
   265
    "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
clasohm@923
   266
 (fn prems=>
clasohm@923
   267
  [ (resolve_tac prems 1),
clasohm@923
   268
    (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]);
clasohm@923
   269
clasohm@923
   270
qed_goal "Diff_iff" Set.thy "(c : A-B) = (c:A & c~:B)"
berghofe@1760
   271
 (fn _ => [ (fast_tac (!claset addSIs [DiffI] addSEs [DiffE]) 1) ]);
clasohm@923
   272
nipkow@1548
   273
section "The empty set -- {}";
clasohm@923
   274
clasohm@923
   275
qed_goalw "emptyE" Set.thy [empty_def] "a:{} ==> P"
clasohm@923
   276
 (fn [prem] => [rtac (prem RS CollectD RS FalseE) 1]);
clasohm@923
   277
clasohm@923
   278
qed_goal "empty_subsetI" Set.thy "{} <= A"
clasohm@923
   279
 (fn _ => [ (REPEAT (ares_tac [equalityI,subsetI,emptyE] 1)) ]);
clasohm@923
   280
clasohm@923
   281
qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
clasohm@923
   282
 (fn prems=>
clasohm@923
   283
  [ (REPEAT (ares_tac (prems@[empty_subsetI,subsetI,equalityI]) 1 
clasohm@923
   284
      ORELSE eresolve_tac (prems RL [FalseE]) 1)) ]);
clasohm@923
   285
clasohm@923
   286
qed_goal "equals0D" Set.thy "[| A={};  a:A |] ==> P"
clasohm@923
   287
 (fn [major,minor]=>
clasohm@923
   288
  [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
clasohm@923
   289
paulson@1640
   290
qed_goal "empty_iff" Set.thy "(c : {}) = False"
berghofe@1760
   291
 (fn _ => [ (fast_tac (!claset addSEs [emptyE]) 1) ]);
paulson@1640
   292
clasohm@923
   293
nipkow@1548
   294
section "Augmenting a set -- insert";
clasohm@923
   295
clasohm@923
   296
qed_goalw "insertI1" Set.thy [insert_def] "a : insert a B"
clasohm@923
   297
 (fn _ => [rtac (CollectI RS UnI1) 1, rtac refl 1]);
clasohm@923
   298
clasohm@923
   299
qed_goalw "insertI2" Set.thy [insert_def] "a : B ==> a : insert b B"
clasohm@923
   300
 (fn [prem]=> [ (rtac (prem RS UnI2) 1) ]);
clasohm@923
   301
clasohm@923
   302
qed_goalw "insertE" Set.thy [insert_def]
clasohm@923
   303
    "[| a : insert b A;  a=b ==> P;  a:A ==> P |] ==> P"
clasohm@923
   304
 (fn major::prems=>
clasohm@923
   305
  [ (rtac (major RS UnE) 1),
clasohm@923
   306
    (REPEAT (eresolve_tac (prems @ [CollectE]) 1)) ]);
clasohm@923
   307
clasohm@923
   308
qed_goal "insert_iff" Set.thy "a : insert b A = (a=b | a:A)"
berghofe@1760
   309
 (fn _ => [fast_tac (!claset addIs [insertI1,insertI2] addSEs [insertE]) 1]);
clasohm@923
   310
clasohm@923
   311
(*Classical introduction rule*)
clasohm@923
   312
qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert b B"
clasohm@923
   313
 (fn [prem]=>
clasohm@923
   314
  [ (rtac (disjCI RS (insert_iff RS iffD2)) 1),
clasohm@923
   315
    (etac prem 1) ]);
clasohm@923
   316
nipkow@1548
   317
section "Singletons, using insert";
clasohm@923
   318
clasohm@923
   319
qed_goal "singletonI" Set.thy "a : {a}"
clasohm@923
   320
 (fn _=> [ (rtac insertI1 1) ]);
clasohm@923
   321
clasohm@923
   322
goalw Set.thy [insert_def] "!!a. b : {a} ==> b=a";
berghofe@1760
   323
by (fast_tac (!claset addSEs [emptyE,CollectE,UnE]) 1);
clasohm@923
   324
qed "singletonD";
clasohm@923
   325
oheimb@1776
   326
bind_thm ("singletonE", make_elim singletonD);
oheimb@1776
   327
oheimb@1776
   328
qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" (fn _ => [
oheimb@1776
   329
	rtac iffI 1,
oheimb@1776
   330
	etac singletonD 1,
oheimb@1776
   331
	hyp_subst_tac 1,
oheimb@1776
   332
	rtac singletonI 1]);
clasohm@923
   333
clasohm@923
   334
val [major] = goal Set.thy "{a}={b} ==> a=b";
clasohm@923
   335
by (rtac (major RS equalityD1 RS subsetD RS singletonD) 1);
clasohm@923
   336
by (rtac singletonI 1);
clasohm@923
   337
qed "singleton_inject";
clasohm@923
   338
nipkow@1531
   339
nipkow@1548
   340
section "The universal set -- UNIV";
nipkow@1531
   341
nipkow@1531
   342
qed_goal "subset_UNIV" Set.thy "A <= UNIV"
nipkow@1531
   343
  (fn _ => [rtac subsetI 1, rtac ComplI 1, etac emptyE 1]);
nipkow@1531
   344
nipkow@1531
   345
nipkow@1548
   346
section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
clasohm@923
   347
clasohm@923
   348
(*The order of the premises presupposes that A is rigid; b may be flexible*)
clasohm@923
   349
val prems = goalw Set.thy [UNION_def]
clasohm@923
   350
    "[| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
clasohm@923
   351
by (REPEAT (resolve_tac (prems @ [bexI,CollectI]) 1));
clasohm@923
   352
qed "UN_I";
clasohm@923
   353
clasohm@923
   354
val major::prems = goalw Set.thy [UNION_def]
clasohm@923
   355
    "[| b : (UN x:A. B(x));  !!x.[| x:A;  b: B(x) |] ==> R |] ==> R";
clasohm@923
   356
by (rtac (major RS CollectD RS bexE) 1);
clasohm@923
   357
by (REPEAT (ares_tac prems 1));
clasohm@923
   358
qed "UN_E";
clasohm@923
   359
clasohm@923
   360
val prems = goal Set.thy
clasohm@923
   361
    "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
clasohm@923
   362
\    (UN x:A. C(x)) = (UN x:B. D(x))";
clasohm@923
   363
by (REPEAT (etac UN_E 1
clasohm@923
   364
     ORELSE ares_tac ([UN_I,equalityI,subsetI] @ 
clasohm@1465
   365
                      (prems RL [equalityD1,equalityD2] RL [subsetD])) 1));
clasohm@923
   366
qed "UN_cong";
clasohm@923
   367
clasohm@923
   368
nipkow@1548
   369
section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
clasohm@923
   370
clasohm@923
   371
val prems = goalw Set.thy [INTER_def]
clasohm@923
   372
    "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
clasohm@923
   373
by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
clasohm@923
   374
qed "INT_I";
clasohm@923
   375
clasohm@923
   376
val major::prems = goalw Set.thy [INTER_def]
clasohm@923
   377
    "[| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
clasohm@923
   378
by (rtac (major RS CollectD RS bspec) 1);
clasohm@923
   379
by (resolve_tac prems 1);
clasohm@923
   380
qed "INT_D";
clasohm@923
   381
clasohm@923
   382
(*"Classical" elimination -- by the Excluded Middle on a:A *)
clasohm@923
   383
val major::prems = goalw Set.thy [INTER_def]
clasohm@923
   384
    "[| b : (INT x:A. B(x));  b: B(a) ==> R;  a~:A ==> R |] ==> R";
clasohm@923
   385
by (rtac (major RS CollectD RS ballE) 1);
clasohm@923
   386
by (REPEAT (eresolve_tac prems 1));
clasohm@923
   387
qed "INT_E";
clasohm@923
   388
clasohm@923
   389
val prems = goal Set.thy
clasohm@923
   390
    "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
clasohm@923
   391
\    (INT x:A. C(x)) = (INT x:B. D(x))";
clasohm@923
   392
by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI]));
clasohm@923
   393
by (REPEAT (dtac INT_D 1
clasohm@923
   394
     ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1));
clasohm@923
   395
qed "INT_cong";
clasohm@923
   396
clasohm@923
   397
nipkow@1548
   398
section "Unions over a type; UNION1(B) = Union(range(B))";
clasohm@923
   399
clasohm@923
   400
(*The order of the premises presupposes that A is rigid; b may be flexible*)
clasohm@923
   401
val prems = goalw Set.thy [UNION1_def]
clasohm@923
   402
    "b: B(x) ==> b: (UN x. B(x))";
clasohm@923
   403
by (REPEAT (resolve_tac (prems @ [TrueI, CollectI RS UN_I]) 1));
clasohm@923
   404
qed "UN1_I";
clasohm@923
   405
clasohm@923
   406
val major::prems = goalw Set.thy [UNION1_def]
clasohm@923
   407
    "[| b : (UN x. B(x));  !!x. b: B(x) ==> R |] ==> R";
clasohm@923
   408
by (rtac (major RS UN_E) 1);
clasohm@923
   409
by (REPEAT (ares_tac prems 1));
clasohm@923
   410
qed "UN1_E";
clasohm@923
   411
clasohm@923
   412
nipkow@1548
   413
section "Intersections over a type; INTER1(B) = Inter(range(B))";
clasohm@923
   414
clasohm@923
   415
val prems = goalw Set.thy [INTER1_def]
clasohm@923
   416
    "(!!x. b: B(x)) ==> b : (INT x. B(x))";
clasohm@923
   417
by (REPEAT (ares_tac (INT_I::prems) 1));
clasohm@923
   418
qed "INT1_I";
clasohm@923
   419
clasohm@923
   420
val [major] = goalw Set.thy [INTER1_def]
clasohm@923
   421
    "b : (INT x. B(x)) ==> b: B(a)";
clasohm@923
   422
by (rtac (TrueI RS (CollectI RS (major RS INT_D))) 1);
clasohm@923
   423
qed "INT1_D";
clasohm@923
   424
nipkow@1548
   425
section "Union";
clasohm@923
   426
clasohm@923
   427
(*The order of the premises presupposes that C is rigid; A may be flexible*)
clasohm@923
   428
val prems = goalw Set.thy [Union_def]
clasohm@923
   429
    "[| X:C;  A:X |] ==> A : Union(C)";
clasohm@923
   430
by (REPEAT (resolve_tac (prems @ [UN_I]) 1));
clasohm@923
   431
qed "UnionI";
clasohm@923
   432
clasohm@923
   433
val major::prems = goalw Set.thy [Union_def]
clasohm@923
   434
    "[| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R";
clasohm@923
   435
by (rtac (major RS UN_E) 1);
clasohm@923
   436
by (REPEAT (ares_tac prems 1));
clasohm@923
   437
qed "UnionE";
clasohm@923
   438
nipkow@1548
   439
section "Inter";
clasohm@923
   440
clasohm@923
   441
val prems = goalw Set.thy [Inter_def]
clasohm@923
   442
    "[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
clasohm@923
   443
by (REPEAT (ares_tac ([INT_I] @ prems) 1));
clasohm@923
   444
qed "InterI";
clasohm@923
   445
clasohm@923
   446
(*A "destruct" rule -- every X in C contains A as an element, but
clasohm@923
   447
  A:X can hold when X:C does not!  This rule is analogous to "spec". *)
clasohm@923
   448
val major::prems = goalw Set.thy [Inter_def]
clasohm@923
   449
    "[| A : Inter(C);  X:C |] ==> A:X";
clasohm@923
   450
by (rtac (major RS INT_D) 1);
clasohm@923
   451
by (resolve_tac prems 1);
clasohm@923
   452
qed "InterD";
clasohm@923
   453
clasohm@923
   454
(*"Classical" elimination rule -- does not require proving X:C *)
clasohm@923
   455
val major::prems = goalw Set.thy [Inter_def]
clasohm@923
   456
    "[| A : Inter(C);  A:X ==> R;  X~:C ==> R |] ==> R";
clasohm@923
   457
by (rtac (major RS INT_E) 1);
clasohm@923
   458
by (REPEAT (eresolve_tac prems 1));
clasohm@923
   459
qed "InterE";
clasohm@923
   460
nipkow@1548
   461
section "The Powerset operator -- Pow";
clasohm@923
   462
clasohm@923
   463
qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)"
clasohm@923
   464
 (fn _ => [ (etac CollectI 1) ]);
clasohm@923
   465
clasohm@923
   466
qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B)  ==>  A<=B"
clasohm@923
   467
 (fn _=> [ (etac CollectD 1) ]);
clasohm@923
   468
clasohm@923
   469
val Pow_bottom = empty_subsetI RS PowI;        (* {}: Pow(B) *)
clasohm@923
   470
val Pow_top = subset_refl RS PowI;             (* A : Pow(A) *)
oheimb@1776
   471
oheimb@1776
   472
oheimb@1776
   473
oheimb@1776
   474
(*** Set reasoning tools ***)
oheimb@1776
   475
oheimb@1776
   476
oheimb@1776
   477
val mem_simps = [ Un_iff, Int_iff, Compl_iff, Diff_iff, singleton_iff,
oheimb@1776
   478
		  mem_Collect_eq];
oheimb@1776
   479
oheimb@1776
   480
val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
oheimb@1776
   481
oheimb@1776
   482
simpset := !simpset addsimps mem_simps
oheimb@1776
   483
                    addcongs [ball_cong,bex_cong]
oheimb@1776
   484
                    setmksimps (mksimps mksimps_pairs);