src/ZF/ZF.ML
author lcp
Tue, 26 Jul 1994 13:44:42 +0200
changeset 485 5e00a676a211
parent 435 ca5356bd315a
child 516 1957113f0d7d
permissions -rw-r--r--
Axiom of choice, cardinality results, etc.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/zf.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open ZF;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
signature ZF_LEMMAS = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  sig
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    13
  val ballE	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    14
  val ballI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    15
  val ball_cong	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    16
  val ball_simp	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    17
  val ball_tac	: int -> tactic
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    18
  val bexCI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    19
  val bexE	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    20
  val bexI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    21
  val bex_cong	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    22
  val bspec	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    23
  val CollectD1	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    24
  val CollectD2	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    25
  val CollectE	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    26
  val CollectI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    27
  val Collect_cong	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    28
  val emptyE	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    29
  val empty_subsetI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    30
  val equalityCE	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    31
  val equalityD1	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    32
  val equalityD2	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    33
  val equalityE	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    34
  val equalityI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    35
  val equality_iffI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    36
  val equals0D	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    37
  val equals0I	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    38
  val ex1_functional	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    39
  val InterD	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    40
  val InterE	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    41
  val InterI	: thm
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
    42
  val Inter_iff : thm
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    43
  val INT_E	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    44
  val INT_I	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    45
  val INT_cong	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    46
  val lemmas_cs	: claset
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    47
  val PowD	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    48
  val PowI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    49
  val RepFunE	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    50
  val RepFunI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    51
  val RepFun_eqI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    52
  val RepFun_cong	: thm
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
    53
  val RepFun_iff	: thm
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    54
  val ReplaceE	: thm
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
    55
  val ReplaceE2	: thm
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    56
  val ReplaceI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    57
  val Replace_iff	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    58
  val Replace_cong	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    59
  val rev_ballE	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    60
  val rev_bspec	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    61
  val rev_subsetD	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    62
  val separation	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    63
  val setup_induction	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    64
  val set_mp_tac	: int -> tactic
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    65
  val subsetCE	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    66
  val subsetD	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    67
  val subsetI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    68
  val subset_iff	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    69
  val subset_refl	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    70
  val subset_trans	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    71
  val UnionE	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    72
  val UnionI	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    73
  val UN_E	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    74
  val UN_I	: thm
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
    75
  val UN_cong	: thm
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
structure ZF_Lemmas : ZF_LEMMAS = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
(*** Bounded universal quantifier ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
val ballI = prove_goalw ZF.thy [Ball_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
    "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
 (fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
val bspec = prove_goalw ZF.thy [Ball_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
    "[| ALL x:A. P(x);  x: A |] ==> P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
  [ (rtac (major RS spec RS mp) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
    (resolve_tac prems 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
val ballE = prove_goalw ZF.thy [Ball_def]
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
    95
    "[| ALL x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
  [ (rtac (major RS allE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
    (REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
(*Used in the datatype package*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
val rev_bspec = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
    "!!x A P. [| x: A;  ALL x:A. P(x) |] ==> P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
  [ REPEAT (ares_tac [bspec] 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
(*Instantiates x first: better for automatic theorem proving?*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
val rev_ballE = prove_goal ZF.thy
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
   108
    "[| ALL x:A. P(x);  x~:A ==> Q;  P(x) ==> Q |] ==> Q"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
  [ (rtac (major RS ballE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
    (REPEAT (eresolve_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
val ball_tac = dtac bspec THEN' assume_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
(*Trival rewrite rule;   (ALL x:A.P)<->P holds only if A is nonempty!*)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   117
val ball_simp = prove_goal ZF.thy "(ALL x:A. True) <-> True"
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   118
 (fn _=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
(*Congruence rule for rewriting*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
val ball_cong = prove_goalw ZF.thy [Ball_def]
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   122
    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   123
 (fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
(*** Bounded existential quantifier ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
val bexI = prove_goalw ZF.thy [Bex_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
    "[| P(x);  x: A |] ==> EX x:A. P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
 (fn prems=> [ (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
(*Not of the general form for such rules; ~EX has become ALL~ *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
val bexCI = prove_goal ZF.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
   "[| ALL x:A. ~P(x) ==> P(a);  a: A |] ==> EX x:A.P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
  [ (rtac classical 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
    (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
val bexE = prove_goalw ZF.thy [Bex_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
    "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
\    |] ==> Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
  [ (rtac (major RS exE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
    (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
(*We do not even have (EX x:A. True) <-> True unless A is nonempty!!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
val bex_cong = prove_goalw ZF.thy [Bex_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
    "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) \
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   149
\    |] ==> Bex(A,P) <-> Bex(A',P')"
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   150
 (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
(*** Rules for subsets ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
val subsetI = prove_goalw ZF.thy [subset_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
    "(!!x.x:A ==> x:B) ==> A <= B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
 (fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
(*Rule in Modus Ponens style [was called subsetE] *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
val subsetD = prove_goalw ZF.thy [subset_def] "[| A <= B;  c:A |] ==> c:B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
  [ (rtac (major RS bspec) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
    (resolve_tac prems 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
(*Classical elimination rule*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
val subsetCE = prove_goalw ZF.thy [subset_def]
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
   166
    "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
  [ (rtac (major RS ballE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
    (REPEAT (eresolve_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
(*Takes assumptions A<=B; c:A and creates the assumption c:B *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
val set_mp_tac = dtac subsetD THEN' assume_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
(*Sometimes useful with premises in this order*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
val rev_subsetD = prove_goal ZF.thy "!!A B c. [| c:A; A<=B |] ==> c:B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
 (fn _=> [REPEAT (ares_tac [subsetD] 1)]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
val subset_refl = prove_goal ZF.thy "A <= A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
 (fn _=> [ (rtac subsetI 1), atac 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
val subset_trans = prove_goal ZF.thy "[| A<=B;  B<=C |] ==> A<=C"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
 (fn prems=> [ (REPEAT (ares_tac ([subsetI]@(prems RL [subsetD])) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   184
(*Useful for proving A<=B by rewriting in some cases*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   185
val subset_iff = prove_goalw ZF.thy [subset_def,Ball_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   186
     "A<=B <-> (ALL x. x:A --> x:B)"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   187
 (fn _=> [ (rtac iff_refl 1) ]);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   188
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
(*** Rules for equality ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
(*Anti-symmetry of the subset relation*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
val equalityI = prove_goal ZF.thy "[| A <= B;  B <= A |] ==> A = B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
 (fn prems=> [ (REPEAT (resolve_tac (prems@[conjI, extension RS iffD2]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
val equality_iffI = prove_goal ZF.thy "(!!x. x:A <-> x:B) ==> A = B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
 (fn [prem] =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
  [ (rtac equalityI 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
    (REPEAT (ares_tac [subsetI, prem RS iffD1, prem RS iffD2] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
val equalityD1 = prove_goal ZF.thy "A = B ==> A<=B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
  [ (rtac (extension RS iffD1 RS conjunct1) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
    (resolve_tac prems 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
val equalityD2 = prove_goal ZF.thy "A = B ==> B<=A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
  [ (rtac (extension RS iffD1 RS conjunct2) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
    (resolve_tac prems 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
val equalityE = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
    "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
  [ (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
val equalityCE = prove_goal ZF.thy
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
   217
    "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
  [ (rtac (major RS equalityE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
    (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
(*Lemma for creating induction formulae -- for "pattern matching" on p
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
  To make the induction hypotheses usable, apply "spec" or "bspec" to
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
  put universal quantifiers over the free variables in p. 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
  Would it be better to do subgoal_tac "ALL z. p = f(z) --> R(z)" ??*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
val setup_induction = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
    "[| p: A;  !!z. z: A ==> p=z --> R |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
  [ (rtac mp 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
    (REPEAT (resolve_tac (refl::prems) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
(*** Rules for Replace -- the derived form of replacement ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
val ex1_functional = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
    "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
  [ (cut_facts_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
    (best_tac FOL_dup_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
val Replace_iff = prove_goalw ZF.thy [Replace_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
    "b : {y. x:A, P(x,y)}  <->  (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
 (fn _=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
  [ (rtac (replacement RS iff_trans) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
    (REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
        ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
val ReplaceI = prove_goal ZF.thy
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   250
    "[| P(x,b);  x: A;  !!y. P(x,y) ==> y=b |] ==> \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
\    b : {y. x:A, P(x,y)}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
  [ (rtac (Replace_iff RS iffD2) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
    (REPEAT (ares_tac (prems@[bexI,conjI,allI,impI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
val ReplaceE = prove_goal ZF.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
    "[| b : {y. x:A, P(x,y)};  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
\       !!x. [| x: A;  P(x,b);  ALL y. P(x,y)-->y=b |] ==> R \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
\    |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
  [ (rtac (Replace_iff RS iffD1 RS bexE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
    (etac conjE 2),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   266
(*As above but without the (generally useless) 3rd assumption*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   267
val ReplaceE2 = prove_goal ZF.thy 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   268
    "[| b : {y. x:A, P(x,y)};  \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   269
\       !!x. [| x: A;  P(x,b) |] ==> R \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   270
\    |] ==> R"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   271
 (fn major::prems=>
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   272
  [ (rtac (major RS ReplaceE) 1),
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   273
    (REPEAT (ares_tac prems 1)) ]);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   274
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
val Replace_cong = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
    "[| A=B;  !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   277
\    Replace(A,P) = Replace(B,Q)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
   let val substprems = prems RL [subst, ssubst]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
       and iffprems = prems RL [iffD1,iffD2]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
   in [ (rtac equalityI 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
	(REPEAT (eresolve_tac (substprems@[asm_rl, ReplaceE, spec RS mp]) 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
	 ORELSE resolve_tac [subsetI, ReplaceI] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
	 ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
   end);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
(*** Rules for RepFun ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
val RepFunI = prove_goalw ZF.thy [RepFun_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
    "!!a A. a : A ==> f(a) : {f(x). x:A}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
 (fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
120
09287f26bfb8 changed all co- and co_ to co
lcp
parents: 37
diff changeset
   293
(*Useful for coinduction proofs*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
val RepFun_eqI = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
    "!!b a f. [| b=f(a);  a : A |] ==> b : {f(x). x:A}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
 (fn _ => [ etac ssubst 1, etac RepFunI 1 ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
val RepFunE = prove_goalw ZF.thy [RepFun_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
    "[| b : {f(x). x:A};  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
\       !!x.[| x:A;  b=f(x) |] ==> P |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
\    P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
  [ (rtac (major RS ReplaceE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
val RepFun_cong = prove_goalw ZF.thy [RepFun_def]
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   307
    "[| A=B;  !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   308
 (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   310
val RepFun_iff = prove_goalw ZF.thy [Bex_def]
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   311
    "b : {f(x). x:A} <-> (EX x:A. b=f(x))"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   312
 (fn _ => [ (fast_tac (FOL_cs addIs [RepFunI] addSEs [RepFunE]) 1) ]);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   313
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
(*** Rules for Collect -- forming a subset by separation ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
(*Separation is derivable from Replacement*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
val separation = prove_goalw ZF.thy [Collect_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
    "a : {x:A. P(x)} <-> a:A & P(a)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
 (fn _=> [ (fast_tac (FOL_cs addIs  [bexI,ReplaceI] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
		             addSEs [bexE,ReplaceE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
val CollectI = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
    "[| a:A;  P(a) |] ==> a : {x:A. P(x)}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
  [ (rtac (separation RS iffD2) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
    (REPEAT (resolve_tac (prems@[conjI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
val CollectE = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
    "[| a : {x:A. P(x)};  [| a:A; P(a) |] ==> R |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
  [ (rtac (separation RS iffD1 RS conjE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
val CollectD1 = prove_goal ZF.thy "a : {x:A. P(x)} ==> a:A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
  [ (rtac (major RS CollectE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
    (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
val CollectD2 = prove_goal ZF.thy "a : {x:A. P(x)} ==> P(a)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
  [ (rtac (major RS CollectE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
    (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
val Collect_cong = prove_goalw ZF.thy [Collect_def] 
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   346
    "[| A=B;  !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   347
 (fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
(*** Rules for Unions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
(*The order of the premises presupposes that C is rigid; A may be flexible*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
val UnionI = prove_goal ZF.thy "[| B: C;  A: B |] ==> A: Union(C)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
 (fn prems=>
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   354
  [ (resolve_tac [Union_iff RS iffD2] 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
    (REPEAT (resolve_tac (prems @ [bexI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
val UnionE = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
    "[| A : Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
 (fn prems=>
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   360
  [ (resolve_tac [Union_iff RS iffD1 RS bexE] 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
    (REPEAT (ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
(*** Rules for Inter ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
(*Not obviously useful towards proving InterI, InterD, InterE*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
val Inter_iff = prove_goalw ZF.thy [Inter_def,Ball_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
    "A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
 (fn _=> [ (rtac (separation RS iff_trans) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
	   (fast_tac (FOL_cs addIs [UnionI] addSEs [UnionE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
(* Intersection is well-behaved only if the family is non-empty! *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
val InterI = prove_goalw ZF.thy [Inter_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
    "[| !!x. x: C ==> A: x;  c:C |] ==> A : Inter(C)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   375
  [ (DEPTH_SOLVE (ares_tac ([CollectI,UnionI,ballI] @ prems) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
(*A "destruct" rule -- every B in C contains A as an element, but
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
  A:B can hold when B:C does not!  This rule is analogous to "spec". *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
val InterD = prove_goalw ZF.thy [Inter_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   380
    "[| A : Inter(C);  B : C |] ==> A : B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
 (fn [major,minor]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   382
  [ (rtac (major RS CollectD2 RS bspec) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
    (rtac minor 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
(*"Classical" elimination rule -- does not require exhibiting B:C *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
val InterE = prove_goalw ZF.thy [Inter_def]
37
cebe01deba80 added ~: for "not in"
lcp
parents: 6
diff changeset
   387
    "[| A : Inter(C);  A:B ==> R;  B~:C ==> R |] ==> R"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   389
  [ (rtac (major RS CollectD2 RS ballE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   390
    (REPEAT (eresolve_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   391
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   392
(*** Rules for Unions of families ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   393
(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   394
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   395
val UN_iff = prove_goalw ZF.thy [Bex_def]
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   396
    "b : (UN x:A. B(x)) <-> (EX x:A. b : B(x))"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   397
 (fn _=> [ (fast_tac (FOL_cs addIs [UnionI, RepFunI] 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   398
                             addSEs [UnionE, RepFunE]) 1) ]);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   399
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   400
(*The order of the premises presupposes that A is rigid; b may be flexible*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   401
val UN_I = prove_goal ZF.thy "[| a: A;  b: B(a) |] ==> b: (UN x:A. B(x))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   402
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   403
  [ (REPEAT (resolve_tac (prems@[UnionI,RepFunI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   404
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   405
val UN_E = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   406
    "[| b : (UN x:A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   407
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   408
  [ (rtac (major RS UnionE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   409
    (REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   410
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   411
val UN_cong = prove_goal ZF.thy
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   412
    "[| A=B;  !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A.C(x)) = (UN x:B.D(x))"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   413
 (fn prems=> [ (simp_tac (FOL_ss addcongs [RepFun_cong] addsimps prems) 1) ]);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   414
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   415
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   416
(*** Rules for Intersections of families ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   417
(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   418
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   419
val INT_iff = prove_goal ZF.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   420
    "b : (INT x:A. B(x)) <-> (ALL x:A. b : B(x)) & (EX x. x:A)"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   421
 (fn _=> [ (simp_tac (FOL_ss addsimps [Inter_def, Ball_def, Bex_def, 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   422
				       separation, Union_iff, RepFun_iff]) 1),
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   423
	   (fast_tac FOL_cs 1) ]);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   424
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   425
val INT_I = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   426
    "[| !!x. x: A ==> b: B(x);  a: A |] ==> b: (INT x:A. B(x))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   427
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   428
  [ (REPEAT (ares_tac (prems@[InterI,RepFunI]) 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   429
     ORELSE eresolve_tac [RepFunE,ssubst] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   430
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   431
val INT_E = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   432
    "[| b : (INT x:A. B(x));  a: A |] ==> b : B(a)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   433
 (fn [major,minor]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   434
  [ (rtac (major RS InterD) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   435
    (rtac (minor RS RepFunI) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   436
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   437
val INT_cong = prove_goal ZF.thy
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   438
    "[| A=B;  !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A.C(x)) = (INT x:B.D(x))"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   439
 (fn prems=> [ (simp_tac (FOL_ss addcongs [RepFun_cong] addsimps prems) 1) ]);
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 120
diff changeset
   440
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   441
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   442
(*** Rules for Powersets ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   443
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   444
val PowI = prove_goal ZF.thy "A <= B ==> A : Pow(B)"
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   445
 (fn [prem]=> [ (rtac (prem RS (Pow_iff RS iffD2)) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   446
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   447
val PowD = prove_goal ZF.thy "A : Pow(B)  ==>  A<=B"
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   448
 (fn [major]=> [ (rtac (major RS (Pow_iff RS iffD1)) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   449
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   450
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   451
(*** Rules for the empty set ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   452
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   453
(*The set {x:0.False} is empty; by foundation it equals 0 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   454
  See Suppes, page 21.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   455
val emptyE = prove_goal ZF.thy "a:0 ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   456
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   457
  [ (rtac (foundation RS disjE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   458
    (etac (equalityD2 RS subsetD RS CollectD2 RS FalseE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   459
    (rtac major 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   460
    (etac bexE 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   461
    (etac (CollectD2 RS FalseE) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   462
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   463
val empty_subsetI = prove_goal ZF.thy "0 <= A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   464
 (fn _ => [ (REPEAT (ares_tac [equalityI,subsetI,emptyE] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   465
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   466
val equals0I = prove_goal ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   467
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   468
  [ (REPEAT (ares_tac (prems@[empty_subsetI,subsetI,equalityI]) 1 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   469
      ORELSE eresolve_tac (prems RL [FalseE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   470
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   471
val equals0D = prove_goal ZF.thy "[| A=0;  a:A |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   472
 (fn [major,minor]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   473
  [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   474
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   475
val lemmas_cs = FOL_cs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   476
  addSIs [ballI, InterI, CollectI, PowI, subsetI]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   477
  addIs [bexI, UnionI, ReplaceI, RepFunI]
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 435
diff changeset
   478
  addSEs [bexE, make_elim PowD, UnionE, ReplaceE2, RepFunE,
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   479
	  CollectE, emptyE]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   480
  addEs [rev_ballE, InterD, make_elim InterD, subsetD, subsetCE];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   481
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   482
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   483
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   484
open ZF_Lemmas;