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