src/ZF/upair.ML
author lcp
Mon, 31 Oct 1994 18:09:32 +0100
changeset 673 023cef668158
parent 572 13c30ac40f8f
child 686 be908d8d41ef
permissions -rw-r--r--
ZF/upair/mem_asym,succ_inject: tidied
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/upair
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
UNORDERED pairs in Zermelo-Fraenkel Set Theory 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
Observe the order of dependence:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
    Upair is defined in terms of Replace
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
    Un is defined in terms of Upair and Union (similarly for Int)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
    cons is defined in terms of Upair and Un
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
    Ordered pairs and descriptions are defined using cons ("set notation")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
(*** Lemmas about power sets  ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
val Pow_bottom = empty_subsetI RS PowI;		(* 0 : Pow(B) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
val Pow_top = subset_refl RS PowI;		(* A : Pow(A) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
val Pow_neq_0 = Pow_top RSN (2,equals0D);	(* Pow(a)=0 ==> P *) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
(*** Unordered pairs - Upair ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
val pairing = prove_goalw ZF.thy [Upair_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
    "c : Upair(a,b) <-> (c=a | c=b)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
 (fn _ => [ (fast_tac (lemmas_cs addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
val UpairI1 = prove_goal ZF.thy "a : Upair(a,b)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
 (fn _ => [ (rtac (refl RS disjI1 RS (pairing RS iffD2)) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
val UpairI2 = prove_goal ZF.thy "b : Upair(a,b)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
 (fn _ => [ (rtac (refl RS disjI2 RS (pairing RS iffD2)) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val UpairE = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
    "[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  [ (rtac (major RS (pairing RS iffD1 RS disjE)) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
    (REPEAT (eresolve_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
(*** Rules for binary union -- Un -- defined via Upair ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
val UnI1 = prove_goalw ZF.thy [Un_def] "c : A ==> c : A Un B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
 (fn [prem]=> [ (rtac (prem RS (UpairI1 RS UnionI)) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
val UnI2 = prove_goalw ZF.thy [Un_def] "c : B ==> c : A Un B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
 (fn [prem]=> [ (rtac (prem RS (UpairI2 RS UnionI)) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
val UnE = prove_goalw ZF.thy [Un_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
    "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
  [ (rtac (major RS UnionE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
    (etac UpairE 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
    (REPEAT (EVERY1 [resolve_tac prems, etac subst, assume_tac])) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
572
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    55
(*Stronger version of the rule above*)
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    56
val UnE' = prove_goal ZF.thy
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    57
    "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P"
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    58
 (fn major::prems =>
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    59
  [(rtac (major RS UnE) 1),
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    60
   (eresolve_tac prems 1),
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    61
   (rtac classical 1),
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    62
   (eresolve_tac prems 1),
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    63
   (swap_res_tac prems 1),
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    64
   (etac notnotD 1)]);
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
    65
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
val Un_iff = prove_goal ZF.thy "c : A Un B <-> (c:A | c:B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
 (fn _ => [ (fast_tac (lemmas_cs addIs [UnI1,UnI2] addSEs [UnE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
(*Classical introduction rule: no commitment to A vs B*)
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
    70
val UnCI = prove_goal ZF.thy "(c ~: B ==> c : A) ==> c : A Un B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
  [ (rtac (disjCI RS (Un_iff RS iffD2)) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
    (etac prem 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
(*** Rules for small intersection -- Int -- defined via Upair ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
val IntI = prove_goalw ZF.thy [Int_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
    "[| c : A;  c : B |] ==> c : A Int B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
  [ (REPEAT (resolve_tac (prems @ [UpairI1,InterI]) 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
     ORELSE eresolve_tac [UpairE, ssubst] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
val IntD1 = prove_goalw ZF.thy [Int_def] "c : A Int B ==> c : A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
  [ (rtac (UpairI1 RS (major RS InterD)) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
val IntD2 = prove_goalw ZF.thy [Int_def] "c : A Int B ==> c : B"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
  [ (rtac (UpairI2 RS (major RS InterD)) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
val IntE = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
    "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
  [ (resolve_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
    (REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
val Int_iff = prove_goal ZF.thy "c : A Int B <-> (c:A & c:B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
 (fn _ => [ (fast_tac (lemmas_cs addSIs [IntI] addSEs [IntE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
(*** Rules for set difference -- defined via Upair ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
val DiffI = prove_goalw ZF.thy [Diff_def]
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
   105
    "[| c : A;  c ~: B |] ==> c : A - B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
 (fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
val DiffD1 = prove_goalw ZF.thy [Diff_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
    "c : A - B ==> c : A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
 (fn [major]=> [ (rtac (major RS CollectD1) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
val DiffD2 = prove_goalw ZF.thy [Diff_def]
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   113
    "c : A - B ==> c ~: B"
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   114
 (fn [major]=> [ (rtac (major RS CollectD2) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
val DiffE = prove_goal ZF.thy
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
   117
    "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
  [ (resolve_tac prems 1),
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   120
    (REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
   122
val Diff_iff = prove_goal ZF.thy "c : A-B <-> (c:A & c~:B)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
 (fn _ => [ (fast_tac (lemmas_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
(*** Rules for cons -- defined via Un and Upair ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
val consI1 = prove_goalw ZF.thy [cons_def] "a : cons(a,B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
 (fn _ => [ (rtac (UpairI1 RS UnI1) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
val consI2 = prove_goalw ZF.thy [cons_def] "a : B ==> a : cons(b,B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
 (fn [prem]=> [ (rtac (prem RS UnI2) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
val consE = prove_goalw ZF.thy [cons_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
    "[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
  [ (rtac (major RS UnE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
    (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
572
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   139
(*Stronger version of the rule above*)
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   140
val consE' = prove_goal ZF.thy
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   141
    "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P"
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   142
 (fn major::prems =>
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   143
  [(rtac (major RS consE) 1),
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   144
   (eresolve_tac prems 1),
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   145
   (rtac classical 1),
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   146
   (eresolve_tac prems 1),
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   147
   (swap_res_tac prems 1),
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   148
   (etac notnotD 1)]);
13c30ac40f8f ZF/upair/consE', UnE': new
lcp
parents: 485
diff changeset
   149
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
val cons_iff = prove_goal ZF.thy "a : cons(b,A) <-> (a=b | a:A)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
 (fn _ => [ (fast_tac (lemmas_cs addIs [consI1,consI2] addSEs [consE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
(*Classical introduction rule*)
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
   154
val consCI = prove_goal ZF.thy "(a~:B ==> a=b) ==> a: cons(b,B)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
 (fn [prem]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
  [ (rtac (disjCI RS (cons_iff RS iffD2)) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
    (etac prem 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
(*** Singletons - using cons ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
val singletonI = prove_goal ZF.thy "a : {a}"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
 (fn _=> [ (rtac consI1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
val singletonE = prove_goal ZF.thy "[| a: {b};  a=b ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
  [ (rtac (major RS consE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
    (REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
(*** Rules for Descriptions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
val the_equality = prove_goalw ZF.thy [the_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
    "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
  [ (fast_tac (lemmas_cs addIs ([equalityI,singletonI]@prems) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
	                 addEs (prems RL [subst])) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
(* Only use this if you already know EX!x. P(x) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
val the_equality2 = prove_goal ZF.thy
673
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   180
    "!!P. [| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   181
 (fn _ =>
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   182
  [ (deepen_tac (lemmas_cs addSIs [the_equality]) 1 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
val theI = prove_goal ZF.thy "EX! x. P(x) ==> P(THE x. P(x))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
  [ (rtac (major RS ex1E) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
    (resolve_tac [major RS the_equality2 RS ssubst] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
    (REPEAT (assume_tac 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   190
(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   191
  (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   192
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   193
(*If it's "undefined", it's zero!*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   194
val the_0 = prove_goalw ZF.thy [the_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   195
    "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   196
 (fn _ =>
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   197
  [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [ReplaceE]) 1) ]);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   198
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
(*** if -- a conditional expression for formulae ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
goalw ZF.thy [if_def] "if(True,a,b) = a";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
by (fast_tac (lemmas_cs addIs [the_equality]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
val if_true = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
goalw ZF.thy [if_def] "if(False,a,b) = b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
by (fast_tac (lemmas_cs addIs [the_equality]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
val if_false = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   210
(*Never use with case splitting, or if P is known to be true or false*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
val prems = goalw ZF.thy [if_def]
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   212
    "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |] ==> if(P,a,b) = if(Q,c,d)";
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   213
by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
val if_cong = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
(*Not needed for rewriting, since P would rewrite to True anyway*)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   217
goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
val if_P = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
(*Not needed for rewriting, since P would rewrite to False anyway*)
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   222
goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
val if_not_P = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   226
val if_ss = FOL_ss addsimps  [if_true,if_false];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
val expand_if = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
    "P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   230
 (fn _=> [ (excluded_middle_tac "Q" 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   231
	   (asm_simp_tac if_ss 1),
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   232
	   (asm_simp_tac if_ss 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
    "[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   236
by (excluded_middle_tac "P" 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   237
by (ALLGOALS (asm_simp_tac (if_ss addsimps prems)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
val if_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
(*** Foundation lemmas ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   243
(*was called mem_anti_sym*)
673
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   244
val mem_asym = prove_goal ZF.thy "!!P. [| a:b;  b:a |] ==> P"
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   245
 (fn _=>
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   246
  [ (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
    (etac equals0D 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
    (rtac consI1 1),
673
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   249
    (fast_tac (lemmas_cs addIs [consI1,consI2]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
		         addSEs [consE,equalityE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   252
(*was called mem_anti_refl*)
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   253
val mem_irrefl = prove_goal ZF.thy "a:a ==> P"
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   254
 (fn [major]=> [ (rtac (major RS (major RS mem_asym)) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   256
val mem_not_refl = prove_goal ZF.thy "a ~: a"
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   257
 (K [ (rtac notI 1), (etac mem_irrefl 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   259
(*Good for proving inequalities by rewriting*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   260
val mem_imp_not_eq = prove_goal ZF.thy "!!a A. a:A ==> a ~= A"
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   261
 (fn _=> [ fast_tac (lemmas_cs addSEs [mem_irrefl]) 1 ]);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   262
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
(*** Rules for succ ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
val succI1 = prove_goalw ZF.thy [succ_def] "i : succ(i)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
 (fn _=> [ (rtac consI1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
val succI2 = prove_goalw ZF.thy [succ_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
    "i : j ==> i : succ(j)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
 (fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
val succE = prove_goalw ZF.thy [succ_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
    "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
  [ (rtac (major RS consE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
    (REPEAT (eresolve_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   278
val succ_iff = prove_goal ZF.thy "i : succ(j) <-> i=j | i:j"
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   279
 (fn _ => [ (fast_tac (lemmas_cs addIs [succI1,succI2] addSEs [succE]) 1) ]);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   280
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   281
(*Classical introduction rule*)
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
   282
val succCI = prove_goal ZF.thy "(i~:j ==> i=j) ==> i: succ(j)"
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   283
 (fn [prem]=>
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   284
  [ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   285
    (etac prem 1) ]);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   286
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
val succ_neq_0 = prove_goal ZF.thy "succ(n)=0 ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
  [ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
    (rtac succI1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
(*Useful for rewriting*)
37
cebe01deba80 added ~: for "not in"
lcp
parents: 14
diff changeset
   293
val succ_not_0 = prove_goal ZF.thy "succ(n) ~= 0"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
 (fn _=> [ (rtac notI 1), (etac succ_neq_0 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
(* succ(c) <= B ==> c : B *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
val succ_subsetD = succI1 RSN (2,subsetD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
673
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   299
val succ_inject = prove_goal ZF.thy "!!m n. succ(m) = succ(n) ==> m=n"
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   300
 (fn _ =>
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   301
  [ (fast_tac (lemmas_cs addSEs [succE, equalityE, make_elim succ_subsetD] 
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   302
                         addEs [mem_asym]) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
val succ_inject_iff = prove_goal ZF.thy "succ(m) = succ(n) <-> m=n"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
 (fn _=> [ (fast_tac (FOL_cs addSEs [succ_inject]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   307
(*UpairI1/2 should become UpairCI;  mem_irrefl as a hazE? *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
val upair_cs = lemmas_cs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
  addSIs [singletonI, DiffI, IntI, UnCI, consCI, succCI, UpairI1,UpairI2]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
  addSEs [singletonE, DiffE, IntE, UnE, consE, succE, UpairE];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311