src/ZF/upair.ML
author clasohm
Wed, 07 Dec 1994 13:12:04 +0100
changeset 760 f0200e91b272
parent 738 3054a10ed5b5
child 834 ad1d0eb0ee82
permissions -rw-r--r--
added qed and qed_goal[w]
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    24
qed_goalw "pairing" ZF.thy [Upair_def]
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    28
qed_goal "UpairI1" ZF.thy "a : Upair(a,b)"
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    31
qed_goal "UpairI2" ZF.thy "b : Upair(a,b)"
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    34
qed_goal "UpairE" ZF.thy
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    42
qed_goalw "UnI1" ZF.thy [Un_def] "c : A ==> c : A Un B"
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    45
qed_goalw "UnI2" ZF.thy [Un_def] "c : B ==> c : A Un B"
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    48
qed_goalw "UnE" ZF.thy [Un_def] 
0
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*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    56
qed_goal "UnE'" ZF.thy
572
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    66
qed_goal "Un_iff" ZF.thy "c : A Un B <-> (c:A | c:B)"
0
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*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    70
qed_goal "UnCI" 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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    78
qed_goalw "IntI" ZF.thy [Int_def]
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    84
qed_goalw "IntD1" ZF.thy [Int_def] "c : A Int B ==> c : A"
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    88
qed_goalw "IntD2" ZF.thy [Int_def] "c : A Int B ==> c : B"
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    92
qed_goal "IntE" ZF.thy
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
    98
qed_goal "Int_iff" ZF.thy "c : A Int B <-> (c:A & c:B)"
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   104
qed_goalw "DiffI" 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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   108
qed_goalw "DiffD1" ZF.thy [Diff_def]
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   112
qed_goalw "DiffD2" 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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   116
qed_goal "DiffE" 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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   122
qed_goal "Diff_iff" 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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   127
qed_goalw "consI1" ZF.thy [cons_def] "a : cons(a,B)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
 (fn _ => [ (rtac (UpairI1 RS UnI1) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   130
qed_goalw "consI2" ZF.thy [cons_def] "a : B ==> a : cons(b,B)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
 (fn [prem]=> [ (rtac (prem RS UnI2) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   133
qed_goalw "consE" ZF.thy [cons_def]
0
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*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   140
qed_goal "consE'" ZF.thy
572
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   150
qed_goal "cons_iff" ZF.thy "a : cons(b,A) <-> (a=b | a:A)"
0
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*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   154
qed_goal "consCI" 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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   161
qed_goal "singletonI" ZF.thy "a : {a}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
 (fn _=> [ (rtac consI1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   164
qed_goal "singletonE" ZF.thy "[| a: {b};  a=b ==> P |] ==> P"
0
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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   172
qed_goalw "the_equality" ZF.thy [the_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
    "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
738
3054a10ed5b5 the_equality: more careful use of addSIs and addIs
lcp
parents: 686
diff changeset
   174
 (fn [pa,eq] =>
3054a10ed5b5 the_equality: more careful use of addSIs and addIs
lcp
parents: 686
diff changeset
   175
  [ (fast_tac (lemmas_cs addSIs [singletonI,pa] addIs [equalityI]
3054a10ed5b5 the_equality: more careful use of addSIs and addIs
lcp
parents: 686
diff changeset
   176
	                 addEs [eq RS subst]) 1) ]);
0
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) *)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   179
qed_goal "the_equality2" 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
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   184
qed_goal "theI" ZF.thy "EX! x. P(x) ==> P(THE x. P(x))"
0
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
686
be908d8d41ef ZF/upair/theI2: new
lcp
parents: 673
diff changeset
   190
(*Easier to apply than theI: conclusion has only one occurrence of P*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   191
qed_goal "theI2" ZF.thy
686
be908d8d41ef ZF/upair/theI2: new
lcp
parents: 673
diff changeset
   192
    "[| EX! x. P(x);  !!x. P(x) ==> Q(x) |] ==> Q(THE x.P(x))"
be908d8d41ef ZF/upair/theI2: new
lcp
parents: 673
diff changeset
   193
 (fn prems => [ resolve_tac prems 1, 
be908d8d41ef ZF/upair/theI2: new
lcp
parents: 673
diff changeset
   194
	        rtac theI 1, 
be908d8d41ef ZF/upair/theI2: new
lcp
parents: 673
diff changeset
   195
		resolve_tac prems 1 ]);
be908d8d41ef ZF/upair/theI2: new
lcp
parents: 673
diff changeset
   196
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   197
(*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
   198
  (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   199
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   200
(*If it's "undefined", it's zero!*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   201
qed_goalw "the_0" ZF.thy [the_def]
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   202
    "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   203
 (fn _ =>
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents: 437
diff changeset
   204
  [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [ReplaceE]) 1) ]);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   205
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
(*** if -- a conditional expression for formulae ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
goalw ZF.thy [if_def] "if(True,a,b) = a";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
by (fast_tac (lemmas_cs addIs [the_equality]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   211
qed "if_true";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
goalw ZF.thy [if_def] "if(False,a,b) = b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
by (fast_tac (lemmas_cs addIs [the_equality]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   215
qed "if_false";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   217
(*Never use with case splitting, or if P is known to be true or false*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
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
   219
    "[| 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
   220
by (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   221
qed "if_cong";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
(*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
   224
goalw ZF.thy [if_def] "!!P. P ==> if(P,a,b) = a";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   226
qed "if_P";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
(*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
   229
goalw ZF.thy [if_def] "!!P. ~P ==> if(P,a,b) = b";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   231
qed "if_not_P";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   233
val if_ss = FOL_ss addsimps  [if_true,if_false];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   235
qed_goal "expand_if" ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
    "P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   237
 (fn _=> [ (excluded_middle_tac "Q" 1),
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   238
	   (asm_simp_tac if_ss 1),
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   239
	   (asm_simp_tac if_ss 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
val prems = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
    "[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A";
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   243
by (excluded_middle_tac "P" 1);
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   244
by (ALLGOALS (asm_simp_tac (if_ss addsimps prems)));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   245
qed "if_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
(*** Foundation lemmas ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   250
(*was called mem_anti_sym*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   251
qed_goal "mem_asym" ZF.thy "!!P. [| a:b;  b:a |] ==> P"
673
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   252
 (fn _=>
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   253
  [ (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
    (etac equals0D 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
    (rtac consI1 1),
673
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   256
    (fast_tac (lemmas_cs addIs [consI1,consI2]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
		         addSEs [consE,equalityE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   259
(*was called mem_anti_refl*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   260
qed_goal "mem_irrefl" ZF.thy "a:a ==> P"
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   261
 (fn [major]=> [ (rtac (major RS (major RS mem_asym)) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   263
qed_goal "mem_not_refl" ZF.thy "a ~: a"
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   264
 (K [ (rtac notI 1), (etac mem_irrefl 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   266
(*Good for proving inequalities by rewriting*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   267
qed_goal "mem_imp_not_eq" ZF.thy "!!a A. a:A ==> a ~= A"
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   268
 (fn _=> [ fast_tac (lemmas_cs addSEs [mem_irrefl]) 1 ]);
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents: 37
diff changeset
   269
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
(*** Rules for succ ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   272
qed_goalw "succI1" ZF.thy [succ_def] "i : succ(i)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
 (fn _=> [ (rtac consI1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   275
qed_goalw "succI2" ZF.thy [succ_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
    "i : j ==> i : succ(j)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
 (fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   279
qed_goalw "succE" ZF.thy [succ_def]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
    "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
  [ (rtac (major RS consE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
    (REPEAT (eresolve_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   285
qed_goal "succ_iff" ZF.thy "i : succ(j) <-> i=j | i:j"
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   286
 (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
   287
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   288
(*Classical introduction rule*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   289
qed_goal "succCI" 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
   290
 (fn [prem]=>
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   291
  [ (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
   292
    (etac prem 1) ]);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
   293
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   294
qed_goal "succ_neq_0" ZF.thy "succ(n)=0 ==> P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
  [ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
    (rtac succI1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
(*Useful for rewriting*)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   300
qed_goal "succ_not_0" ZF.thy "succ(n) ~= 0"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
 (fn _=> [ (rtac notI 1), (etac succ_neq_0 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
(* succ(c) <= B ==> c : B *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
val succ_subsetD = succI1 RSN (2,subsetD);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   306
qed_goal "succ_inject" ZF.thy "!!m n. succ(m) = succ(n) ==> m=n"
673
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   307
 (fn _ =>
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   308
  [ (fast_tac (lemmas_cs addSEs [succE, equalityE, make_elim succ_subsetD] 
023cef668158 ZF/upair/mem_asym,succ_inject: tidied
lcp
parents: 572
diff changeset
   309
                         addEs [mem_asym]) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 738
diff changeset
   311
qed_goal "succ_inject_iff" ZF.thy "succ(m) = succ(n) <-> m=n"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
 (fn _=> [ (fast_tac (FOL_cs addSEs [succ_inject]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents: 435
diff changeset
   314
(*UpairI1/2 should become UpairCI;  mem_irrefl as a hazE? *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
val upair_cs = lemmas_cs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
  addSIs [singletonI, DiffI, IntI, UnCI, consCI, succCI, UpairI1,UpairI2]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
  addSEs [singletonE, DiffE, IntE, UnE, consE, succE, UpairE];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318