src/ZF/ZF.ML
author wenzelm
Wed, 05 Dec 2001 03:07:44 +0100
changeset 12372 cd3a09c7dac9
parent 11770 b6bb7a853dd2
child 12836 5ef96e63fba6
permissions -rw-r--r--
tuned declarations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1016
diff changeset
     1
(*  Title:      ZF/ZF.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1016
diff changeset
     3
    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
     4
    Copyright   1994  University of Cambridge
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Basic introduction and elimination rules for Zermelo-Fraenkel Set Theory 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
825
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
     9
(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
    10
Goal "[| b:A;  a=b |] ==> a:A";
825
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
    11
by (etac ssubst 1);
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
    12
by (assume_tac 1);
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9211
diff changeset
    13
qed "subst_elem";
825
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
    14
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    15
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
(*** Bounded universal quantifier ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    18
val prems= Goalw [Ball_def] 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    19
    "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    20
by (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    21
qed "ballI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    23
Goalw [Ball_def] "[| ALL x:A. P(x);  x: A |] ==> P(x)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    24
by (etac (spec RS mp) 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    25
by (assume_tac 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    26
qed "bspec";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    28
val major::prems= Goalw [Ball_def] 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    29
    "[| ALL x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    30
by (rtac (major RS allE) 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    31
by (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    32
qed "ballE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
(*Used in the datatype package*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    35
Goal "[| x: A;  ALL x:A. P(x) |] ==> P(x)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    36
by (REPEAT (ares_tac [bspec] 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    37
qed "rev_bspec";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
(*Instantiates x first: better for automatic theorem proving?*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    40
val major::prems= Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    41
    "[| ALL x:A. P(x);  x~:A ==> Q;  P(x) ==> Q |] ==> Q";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    42
by (rtac (major RS ballE) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    43
by (REPEAT (eresolve_tac prems 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    44
qed "rev_ballE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    46
AddSIs [ballI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    47
AddEs  [rev_ballE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    48
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
val ball_tac = dtac bspec THEN' assume_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
(*Trival rewrite rule;   (ALL x:A.P)<->P holds only if A is nonempty!*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    53
Goal "(ALL x:A. P) <-> ((EX x. x:A) --> P)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    54
by (simp_tac (simpset() addsimps [Ball_def]) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    55
qed "ball_triv";
3425
fc4ca570d185 Better miniscoping for bounded quantifiers
paulson
parents: 2925
diff changeset
    56
Addsimps [ball_triv];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
(*Congruence rule for rewriting*)
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    59
val prems= Goalw [Ball_def] 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    60
    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    61
by (simp_tac (FOL_ss addsimps prems) 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    62
qed "ball_cong";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
(*** Bounded existential quantifier ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
6287
61904a3eafaa added rev_bexI
paulson
parents: 6111
diff changeset
    66
Goalw [Bex_def] "[| P(x);  x: A |] ==> EX x:A. P(x)";
61904a3eafaa added rev_bexI
paulson
parents: 6111
diff changeset
    67
by (Blast_tac 1);
61904a3eafaa added rev_bexI
paulson
parents: 6111
diff changeset
    68
qed "bexI";
61904a3eafaa added rev_bexI
paulson
parents: 6111
diff changeset
    69
61904a3eafaa added rev_bexI
paulson
parents: 6111
diff changeset
    70
(*The best argument order when there is only one x:A*)
61904a3eafaa added rev_bexI
paulson
parents: 6111
diff changeset
    71
Goalw [Bex_def] "[| x:A;  P(x) |] ==> EX x:A. P(x)";
61904a3eafaa added rev_bexI
paulson
parents: 6111
diff changeset
    72
by (Blast_tac 1);
61904a3eafaa added rev_bexI
paulson
parents: 6111
diff changeset
    73
qed "rev_bexI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
(*Not of the general form for such rules; ~EX has become ALL~ *)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    76
val prems= Goal "[| ALL x:A. ~P(x) ==> P(a);  a: A |] ==> EX x:A. P(x)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    77
by (rtac classical 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    78
by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    79
qed "bexCI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    81
val major::prems= Goalw [Bex_def] 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
    "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q \
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    83
\    |] ==> Q";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    84
by (rtac (major RS exE) 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    85
by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    86
qed "bexE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    88
AddIs  [bexI];  
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    89
AddSEs [bexE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
    90
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
(*We do not even have (EX x:A. True) <-> True unless A is nonempty!!*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    92
Goal "(EX x:A. P) <-> ((EX x. x:A) & P)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    93
by (simp_tac (simpset() addsimps [Bex_def]) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
    94
qed "bex_triv";
3425
fc4ca570d185 Better miniscoping for bounded quantifiers
paulson
parents: 2925
diff changeset
    95
Addsimps [bex_triv];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    97
val prems= Goalw [Bex_def] 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) \
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    99
\    |] ==> Bex(A,P) <-> Bex(A',P')";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   100
by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   101
qed "bex_cong";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   103
Addcongs [ball_cong, bex_cong];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   104
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   105
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
(*** Rules for subsets ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   108
val prems= Goalw [subset_def] 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   109
    "(!!x. x:A ==> x:B) ==> A <= B";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   110
by (REPEAT (ares_tac (prems @ [ballI]) 1)) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   111
qed "subsetI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
(*Rule in Modus Ponens style [was called subsetE] *)
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   114
Goalw [subset_def]  "[| A <= B;  c:A |] ==> c:B";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   115
by (etac bspec 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   116
by (assume_tac 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   117
qed "subsetD";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
(*Classical elimination rule*)
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   120
val major::prems= Goalw [subset_def] 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   121
    "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   122
by (rtac (major RS ballE) 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   123
by (REPEAT (eresolve_tac prems 1)) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   124
qed "subsetCE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   126
AddSIs [subsetI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   127
AddEs  [subsetCE, subsetD];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   128
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   129
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
(*Takes assumptions A<=B; c:A and creates the assumption c:B *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
val set_mp_tac = dtac subsetD THEN' assume_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
(*Sometimes useful with premises in this order*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   134
Goal "[| c:A; A<=B |] ==> c:B";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   135
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   136
qed "rev_subsetD";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
6111
5347c9a22897 better qed_spec_mp
paulson
parents: 5467
diff changeset
   138
(*Converts A<=B to x:A ==> x:B*)
5347c9a22897 better qed_spec_mp
paulson
parents: 5467
diff changeset
   139
fun impOfSubs th = th RSN (2, rev_subsetD);
5347c9a22897 better qed_spec_mp
paulson
parents: 5467
diff changeset
   140
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   141
Goal "[| A <= B; c ~: B |] ==> c ~: A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   142
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   143
qed "contra_subsetD";
1889
661603db8ee2 Addition of contra_subsetD and rev_contra_subsetD
paulson
parents: 1461
diff changeset
   144
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   145
Goal "[| c ~: B;  A <= B |] ==> c ~: A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   146
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   147
qed "rev_contra_subsetD";
1889
661603db8ee2 Addition of contra_subsetD and rev_contra_subsetD
paulson
parents: 1461
diff changeset
   148
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   149
Goal "A <= A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   150
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   151
qed "subset_refl";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   153
Addsimps [subset_refl];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   154
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   155
Goal "[| A<=B;  B<=C |] ==> A<=C";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   156
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   157
qed "subset_trans";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   159
(*Useful for proving A<=B by rewriting in some cases*)
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   160
Goalw [subset_def,Ball_def] 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   161
     "A<=B <-> (ALL x. x:A --> x:B)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   162
by (rtac iff_refl 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   163
qed "subset_iff";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   164
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
(*** Rules for equality ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
(*Anti-symmetry of the subset relation*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   169
Goal "[| A <= B;  B <= A |] ==> A = B";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   170
by (REPEAT (ares_tac [conjI, extension RS iffD2] 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   171
qed "equalityI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
2493
bdeb5024353a Removal of sum_cs and eq_cs
paulson
parents: 2469
diff changeset
   173
AddIs [equalityI];
bdeb5024353a Removal of sum_cs and eq_cs
paulson
parents: 2469
diff changeset
   174
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   175
val [prem] = Goal "(!!x. x:A <-> x:B) ==> A = B";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   176
by (rtac equalityI 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   177
by (REPEAT (ares_tac [subsetI, prem RS iffD1, prem RS iffD2] 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   178
qed "equality_iffI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   180
bind_thm ("equalityD1", extension RS iffD1 RS conjunct1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   181
bind_thm ("equalityD2", extension RS iffD1 RS conjunct2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   183
val prems = Goal "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   184
by (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   185
qed "equalityE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   187
val major::prems= Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   188
    "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   189
by (rtac (major RS equalityE) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   190
by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   191
qed "equalityCE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
(*Lemma for creating induction formulae -- for "pattern matching" on p
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
  To make the induction hypotheses usable, apply "spec" or "bspec" to
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
  put universal quantifiers over the free variables in p. 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
  Would it be better to do subgoal_tac "ALL z. p = f(z) --> R(z)" ??*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   197
val prems = Goal "[| p: A;  !!z. z: A ==> p=z --> R |] ==> R";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   198
by (rtac mp 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   199
by (REPEAT (resolve_tac (refl::prems) 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   200
qed "setup_induction";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
(*** Rules for Replace -- the derived form of replacement ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   205
Goalw [Replace_def] 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   206
    "b : {y. x:A, P(x,y)}  <->  (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   207
by (rtac (replacement RS iff_trans) 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   208
by (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   209
     ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   210
qed "Replace_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   213
val prems = Goal
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   214
    "[| P(x,b);  x: A;  !!y. P(x,y) ==> y=b |] ==> \
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   215
\    b : {y. x:A, P(x,y)}";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   216
by (rtac (Replace_iff RS iffD2) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   217
by (REPEAT (ares_tac (prems@[bexI,conjI,allI,impI]) 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   218
qed "ReplaceI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   221
val prems = Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
    "[| b : {y. x:A, P(x,y)};  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
\       !!x. [| x: A;  P(x,b);  ALL y. P(x,y)-->y=b |] ==> R \
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   224
\    |] ==> R";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   225
by (rtac (Replace_iff RS iffD1 RS bexE) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   226
by (etac conjE 2);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   227
by (REPEAT (ares_tac prems 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   228
qed "ReplaceE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   230
(*As above but without the (generally useless) 3rd assumption*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   231
val major::prems = Goal
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   232
    "[| b : {y. x:A, P(x,y)};  \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   233
\       !!x. [| x: A;  P(x,b) |] ==> R \
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   234
\    |] ==> R";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   235
by (rtac (major RS ReplaceE) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   236
by (REPEAT (ares_tac prems 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   237
qed "ReplaceE2";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   238
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   239
AddIs  [ReplaceI];  
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   240
AddSEs [ReplaceE2];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   241
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   242
val prems = Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
    "[| A=B;  !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   244
\    Replace(A,P) = Replace(B,Q)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   245
by (rtac equalityI 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   246
by (REPEAT
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   247
    (eresolve_tac ((prems RL [subst, ssubst])@[asm_rl, ReplaceE, spec RS mp]) 1     ORELSE resolve_tac [subsetI, ReplaceI] 1 
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   248
     ORELSE (resolve_tac (prems RL [iffD1,iffD2]) 1 THEN assume_tac 2)));
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   249
qed "Replace_cong";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   251
Addcongs [Replace_cong];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   252
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
(*** Rules for RepFun ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   255
Goalw [RepFun_def] "a : A ==> f(a) : {f(x). x:A}";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   256
by (REPEAT (ares_tac [ReplaceI,refl] 1)) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   257
qed "RepFunI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
120
09287f26bfb8 changed all co- and co_ to co
lcp
parents: 37
diff changeset
   259
(*Useful for coinduction proofs*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   260
Goal "[| b=f(a);  a : A |] ==> b : {f(x). x:A}";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   261
by (etac ssubst 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   262
by (etac RepFunI 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   263
qed "RepFun_eqI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   265
val major::prems= Goalw [RepFun_def] 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
    "[| b : {f(x). x:A};  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
\       !!x.[| x:A;  b=f(x) |] ==> P |] ==> \
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   268
\    P";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   269
by (rtac (major RS ReplaceE) 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   270
by (REPEAT (ares_tac prems 1)) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   271
qed "RepFunE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
2716
9e11a914156a Now uses RepFun_eqI instead of RepFunI;
paulson
parents: 2493
diff changeset
   273
AddIs  [RepFun_eqI];  
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   274
AddSEs [RepFunE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   275
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   276
val prems= Goalw [RepFun_def] 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   277
    "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   278
by (simp_tac (simpset() addsimps prems) 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   279
qed "RepFun_cong";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   280
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   281
Addcongs [RepFun_cong];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   283
Goalw [Bex_def] "b : {f(x). x:A} <-> (EX x:A. b=f(x))";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   284
by (Blast_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   285
qed "RepFun_iff";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   286
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
   287
Goal "{x. x:A} = A";
2877
6476784dba1c Converted to call blast_tac.
paulson
parents: 2815
diff changeset
   288
by (Blast_tac 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   289
qed "triv_RepFun";
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   290
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   291
Addsimps [RepFun_iff, triv_RepFun];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
(*** Rules for Collect -- forming a subset by separation ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
(*Separation is derivable from Replacement*)
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   296
Goalw [Collect_def] "a : {x:A. P(x)} <-> a:A & P(a)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   297
by (Blast_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   298
qed "separation";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   299
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   300
Addsimps [separation];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   302
Goal "[| a:A;  P(a) |] ==> a : {x:A. P(x)}";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   303
by (Asm_simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   304
qed "CollectI";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   305
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   306
val prems = Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   307
    "[| a : {x:A. P(x)};  [| a:A; P(a) |] ==> R |] ==> R";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   308
by (rtac (separation RS iffD1 RS conjE) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   309
by (REPEAT (ares_tac prems 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   310
qed "CollectE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   312
Goal "a : {x:A. P(x)} ==> a:A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   313
by (etac CollectE 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   314
by (assume_tac 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   315
qed "CollectD1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   317
Goal "a : {x:A. P(x)} ==> P(a)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   318
by (etac CollectE 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   319
by (assume_tac 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   320
qed "CollectD2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   322
val prems= Goalw [Collect_def]  
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   323
    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   324
by (simp_tac (simpset() addsimps prems) 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   325
qed "Collect_cong";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   326
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   327
AddSIs [CollectI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   328
AddSEs [CollectE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   329
Addcongs [Collect_cong];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
(*** Rules for Unions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   333
Addsimps [Union_iff];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   334
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
(*The order of the premises presupposes that C is rigid; A may be flexible*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   336
Goal "[| B: C;  A: B |] ==> A: Union(C)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   337
by (Simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   338
by (Blast_tac 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   339
qed "UnionI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   341
val prems = Goal "[| A : Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   342
by (resolve_tac [Union_iff RS iffD1 RS bexE] 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   343
by (REPEAT (ares_tac prems 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   344
qed "UnionE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
(*** Rules for Unions of families ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   347
(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   349
Goalw [Bex_def] "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   350
by (Simp_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   351
by (Blast_tac 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   352
qed "UN_iff";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   353
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   354
Addsimps [UN_iff];
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   355
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
(*The order of the premises presupposes that A is rigid; b may be flexible*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   357
Goal "[| a: A;  b: B(a) |] ==> b: (UN x:A. B(x))";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   358
by (Simp_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   359
by (Blast_tac 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   360
qed "UN_I";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   362
val major::prems= Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   363
    "[| b : (UN x:A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   364
by (rtac (major RS UnionE) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   365
by (REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   366
qed "UN_E";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   368
val prems = Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   369
    "[| A=B;  !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A. C(x)) = (UN x:B. D(x))";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   370
by (simp_tac (simpset() addsimps prems) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   371
qed "UN_cong";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   372
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   373
(*No "Addcongs [UN_cong]" because UN is a combination of constants*)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   374
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   375
(* UN_E appears before UnionE so that it is tried first, to avoid expensive
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   376
  calls to hyp_subst_tac.  Cannot include UN_I as it is unsafe: would enlarge
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   377
  the search space.*)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   378
AddIs  [UnionI];  
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   379
AddSEs [UN_E];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   380
AddSEs [UnionE];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   381
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   382
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   383
(*** Rules for Inter ***)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   384
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   385
(*Not obviously useful towards proving InterI, InterD, InterE*)
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   386
Goalw [Inter_def,Ball_def] 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   387
    "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   388
by (Simp_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   389
by (Blast_tac 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   390
qed "Inter_iff";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   391
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   392
(* Intersection is well-behaved only if the family is non-empty! *)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   393
val prems = Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   394
    "[| !!x. x: C ==> A: x;  EX c. c:C |] ==> A : Inter(C)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   395
by (simp_tac (simpset() addsimps [Inter_iff]) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   396
by (blast_tac (claset() addIs prems) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   397
qed "InterI";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   398
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   399
(*A "destruct" rule -- every B in C contains A as an element, but
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   400
  A:B can hold when B:C does not!  This rule is analogous to "spec". *)
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   401
Goalw [Inter_def] "[| A : Inter(C);  B : C |] ==> A : B";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   402
by (Blast_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   403
qed "InterD";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   404
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   405
(*"Classical" elimination rule -- does not require exhibiting B:C *)
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   406
val major::prems= Goalw [Inter_def] 
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   407
    "[| A : Inter(C);  B~:C ==> R;  A:B ==> R |] ==> R";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   408
by (rtac (major RS CollectD2 RS ballE) 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   409
by (REPEAT (eresolve_tac prems 1)) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   410
qed "InterE";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   411
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   412
AddSIs [InterI];
2716
9e11a914156a Now uses RepFun_eqI instead of RepFunI;
paulson
parents: 2493
diff changeset
   413
AddEs  [InterD, InterE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   414
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   415
(*** Rules for Intersections of families ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   416
(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   417
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   418
Goalw [Inter_def] "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   419
by (Simp_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   420
by (Best_tac 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   421
qed "INT_iff";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   422
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   423
val prems = Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   424
    "[| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   425
by (blast_tac (claset() addIs prems) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   426
qed "INT_I";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   427
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   428
Goal "[| b : (INT x:A. B(x));  a: A |] ==> b : B(a)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   429
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   430
qed "INT_E";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   431
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   432
val prems = Goal
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   433
    "[| A=B;  !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A. C(x)) = (INT x:B. D(x))";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   434
by (simp_tac (simpset() addsimps prems) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   435
qed "INT_cong";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   436
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   437
(*No "Addcongs [INT_cong]" because INT is a combination of constants*)
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   438
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   439
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   440
(*** Rules for Powersets ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   441
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   442
Goal "A <= B ==> A : Pow(B)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   443
by (etac (Pow_iff RS iffD2) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   444
qed "PowI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   445
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   446
Goal "A : Pow(B)  ==>  A<=B";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   447
by (etac (Pow_iff RS iffD1) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   448
qed "PowD";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   449
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   450
AddSIs [PowI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   451
AddSDs [PowD];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   452
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   453
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   454
(*** Rules for the empty set ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   455
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   456
(*The set {x:0.False} is empty; by foundation it equals 0 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   457
  See Suppes, page 21.*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   458
Goal "a ~: 0";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   459
by (cut_facts_tac [foundation] 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   460
by (best_tac (claset() addDs [equalityD2]) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   461
qed "not_mem_empty";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   462
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   463
bind_thm ("emptyE", not_mem_empty RS notE);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   464
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   465
Addsimps [not_mem_empty];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   466
AddSEs [emptyE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   467
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   468
Goal "0 <= A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   469
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   470
qed "empty_subsetI";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   471
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1902
diff changeset
   472
Addsimps [empty_subsetI];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   473
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   474
val prems = Goal "[| !!y. y:A ==> False |] ==> A=0";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   475
by (blast_tac (claset() addDs prems) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   476
qed "equals0I";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   477
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   478
Goal "A=0 ==> a ~: A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   479
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   480
qed "equals0D";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   481
5467
f864dbcda5f1 deleted the bogus equals0E, fixed equals0D
paulson
parents: 5265
diff changeset
   482
AddDs [equals0D, sym RS equals0D];
5265
9d1d4c43c76d Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents: 5242
diff changeset
   483
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   484
Goal "a:A ==> A ~= 0";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   485
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   486
qed "not_emptyI";
825
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
   487
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   488
val [major,minor]= Goal "[| A ~= 0;  !!x. x:A ==> R |] ==> R";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   489
by (rtac ([major, equals0I] MRS swap) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   490
by (swap_res_tac [minor] 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   491
by (assume_tac 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   492
qed "not_emptyE";
825
76d9575950f2 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp
parents: 775
diff changeset
   493
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   494
748
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   495
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   496
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   497
val cantor_cs = FOL_cs   (*precisely the rules needed for the proof*)
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   498
  addSIs [ballI, CollectI, PowI, subsetI] addIs [bexI]
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   499
  addSEs [CollectE, equalityCE];
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   500
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   501
(*The search is undirected; similar proof attempts may fail.
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   502
  b represents ANY map, such as (lam x:A.b(x)): A->Pow(A). *)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   503
Goal "EX S: Pow(A). ALL x:A. b(x) ~= S";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   504
by (best_tac cantor_cs 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   505
qed "cantor";
748
ba231bd734d2 moved Cantors theorem here from ZF/ex/misc
lcp
parents: 722
diff changeset
   506
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9211
diff changeset
   507
(*Lemma for the inductive definition in theory Zorn*)
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   508
Goal "Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   509
by (Blast_tac 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 7531
diff changeset
   510
qed "Union_in_Pow";
1902
e349b91cf197 Added function for storing default claset in theory.
berghofe
parents: 1889
diff changeset
   511
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9211
diff changeset
   512
Goal "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))";
11766
5200b3a8f6e3 improved atomize setup;
wenzelm
parents: 9907
diff changeset
   513
by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1);
5200b3a8f6e3 improved atomize setup;
wenzelm
parents: 9907
diff changeset
   514
qed "atomize_ball";