src/ZF/upair.ML
author paulson
Fri Jan 29 17:08:20 1999 +0100 (1999-01-29)
changeset 6163 be8234f37e48
parent 6153 bff90585cce5
child 8127 68c6159440f1
permissions -rw-r--r--
expandshort
clasohm@1461
     1
(*  Title:      ZF/upair
clasohm@0
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@0
     6
UNORDERED pairs in Zermelo-Fraenkel Set Theory 
clasohm@0
     7
clasohm@0
     8
Observe the order of dependence:
clasohm@0
     9
    Upair is defined in terms of Replace
clasohm@0
    10
    Un is defined in terms of Upair and Union (similarly for Int)
clasohm@0
    11
    cons is defined in terms of Upair and Un
clasohm@0
    12
    Ordered pairs and descriptions are defined using cons ("set notation")
clasohm@0
    13
*)
clasohm@0
    14
clasohm@0
    15
(*** Lemmas about power sets  ***)
clasohm@0
    16
clasohm@1461
    17
val Pow_bottom = empty_subsetI RS PowI;         (* 0 : Pow(B) *)
clasohm@1461
    18
val Pow_top = subset_refl RS PowI;              (* A : Pow(A) *)
clasohm@0
    19
clasohm@0
    20
clasohm@0
    21
(*** Unordered pairs - Upair ***)
clasohm@0
    22
paulson@5325
    23
qed_goalw "Upair_iff" thy [Upair_def]
clasohm@0
    24
    "c : Upair(a,b) <-> (c=a | c=b)"
paulson@5468
    25
 (fn _ => [ (Blast_tac 1) ]);
paulson@2469
    26
paulson@2469
    27
Addsimps [Upair_iff];
clasohm@0
    28
paulson@5325
    29
qed_goal "UpairI1" thy "a : Upair(a,b)"
paulson@2469
    30
 (fn _ => [ Simp_tac 1 ]);
clasohm@0
    31
paulson@5325
    32
qed_goal "UpairI2" thy "b : Upair(a,b)"
paulson@2469
    33
 (fn _ => [ Simp_tac 1 ]);
clasohm@0
    34
paulson@5325
    35
qed_goal "UpairE" thy
clasohm@0
    36
    "[| a : Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
clasohm@0
    37
 (fn major::prems=>
paulson@2469
    38
  [ (rtac (major RS (Upair_iff RS iffD1 RS disjE)) 1),
clasohm@0
    39
    (REPEAT (eresolve_tac prems 1)) ]);
clasohm@0
    40
paulson@2469
    41
AddSIs [UpairI1,UpairI2];
paulson@2469
    42
AddSEs [UpairE];
paulson@2469
    43
clasohm@0
    44
(*** Rules for binary union -- Un -- defined via Upair ***)
clasohm@0
    45
paulson@5325
    46
qed_goalw "Un_iff" thy [Un_def] "c : A Un B <-> (c:A | c:B)"
paulson@2877
    47
 (fn _ => [ Blast_tac 1 ]);
paulson@2469
    48
paulson@2469
    49
Addsimps [Un_iff];
clasohm@0
    50
paulson@5325
    51
qed_goal "UnI1" thy "!!c. c : A ==> c : A Un B"
paulson@2469
    52
 (fn _ => [ Asm_simp_tac 1 ]);
clasohm@0
    53
paulson@5325
    54
qed_goal "UnI2" thy "!!c. c : B ==> c : A Un B"
paulson@2469
    55
 (fn _ => [ Asm_simp_tac 1 ]);
paulson@2469
    56
paulson@5325
    57
qed_goal "UnE" thy 
clasohm@0
    58
    "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P"
clasohm@0
    59
 (fn major::prems=>
paulson@2469
    60
  [ (rtac (major RS (Un_iff RS iffD1 RS disjE)) 1),
paulson@2469
    61
    (REPEAT (eresolve_tac prems 1)) ]);
clasohm@0
    62
lcp@572
    63
(*Stronger version of the rule above*)
paulson@5325
    64
qed_goal "UnE'" thy
lcp@572
    65
    "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P"
lcp@572
    66
 (fn major::prems =>
lcp@572
    67
  [(rtac (major RS UnE) 1),
lcp@572
    68
   (eresolve_tac prems 1),
lcp@572
    69
   (rtac classical 1),
lcp@572
    70
   (eresolve_tac prems 1),
lcp@572
    71
   (swap_res_tac prems 1),
lcp@572
    72
   (etac notnotD 1)]);
lcp@572
    73
paulson@2469
    74
(*Classical introduction rule: no commitment to A vs B*)
paulson@5325
    75
qed_goal "UnCI" thy "(c ~: B ==> c : A) ==> c : A Un B"
paulson@2469
    76
 (fn prems=>
wenzelm@4091
    77
  [ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]);
clasohm@0
    78
paulson@2469
    79
AddSIs [UnCI];
paulson@2469
    80
AddSEs [UnE];
clasohm@0
    81
clasohm@0
    82
clasohm@0
    83
(*** Rules for small intersection -- Int -- defined via Upair ***)
clasohm@0
    84
paulson@5325
    85
qed_goalw "Int_iff" thy [Int_def] "c : A Int B <-> (c:A & c:B)"
paulson@2877
    86
 (fn _ => [ Blast_tac 1 ]);
paulson@2469
    87
paulson@2469
    88
Addsimps [Int_iff];
paulson@2469
    89
paulson@5325
    90
qed_goal "IntI" thy "!!c. [| c : A;  c : B |] ==> c : A Int B"
paulson@2469
    91
 (fn _ => [ Asm_simp_tac 1 ]);
clasohm@0
    92
paulson@5325
    93
qed_goal "IntD1" thy "!!c. c : A Int B ==> c : A"
paulson@2469
    94
 (fn _ => [ Asm_full_simp_tac 1 ]);
clasohm@0
    95
paulson@5325
    96
qed_goal "IntD2" thy "!!c. c : A Int B ==> c : B"
paulson@2469
    97
 (fn _ => [ Asm_full_simp_tac 1 ]);
clasohm@0
    98
paulson@5325
    99
qed_goal "IntE" thy
clasohm@0
   100
    "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P"
clasohm@0
   101
 (fn prems=>
clasohm@0
   102
  [ (resolve_tac prems 1),
clasohm@0
   103
    (REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ]);
clasohm@0
   104
paulson@2469
   105
AddSIs [IntI];
paulson@2469
   106
AddSEs [IntE];
clasohm@0
   107
clasohm@0
   108
(*** Rules for set difference -- defined via Upair ***)
clasohm@0
   109
paulson@5325
   110
qed_goalw "Diff_iff" thy [Diff_def] "c : A-B <-> (c:A & c~:B)"
paulson@2877
   111
 (fn _ => [ Blast_tac 1 ]);
paulson@2469
   112
paulson@2469
   113
Addsimps [Diff_iff];
paulson@2469
   114
paulson@5325
   115
qed_goal "DiffI" thy "!!c. [| c : A;  c ~: B |] ==> c : A - B"
paulson@2469
   116
 (fn _ => [ Asm_simp_tac 1 ]);
clasohm@0
   117
paulson@5325
   118
qed_goal "DiffD1" thy "!!c. c : A - B ==> c : A"
paulson@2469
   119
 (fn _ => [ Asm_full_simp_tac 1 ]);
clasohm@0
   120
paulson@5325
   121
qed_goal "DiffD2" thy "!!c. c : A - B ==> c ~: B"
paulson@2469
   122
 (fn _ => [ Asm_full_simp_tac 1 ]);
clasohm@0
   123
paulson@5325
   124
qed_goal "DiffE" thy
lcp@37
   125
    "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
clasohm@0
   126
 (fn prems=>
clasohm@0
   127
  [ (resolve_tac prems 1),
lcp@485
   128
    (REPEAT (ares_tac (prems RL [DiffD1, DiffD2]) 1)) ]);
clasohm@0
   129
paulson@2469
   130
AddSIs [DiffI];
paulson@2469
   131
AddSEs [DiffE];
clasohm@0
   132
clasohm@0
   133
(*** Rules for cons -- defined via Un and Upair ***)
clasohm@0
   134
paulson@5325
   135
qed_goalw "cons_iff" thy [cons_def] "a : cons(b,A) <-> (a=b | a:A)"
paulson@2877
   136
 (fn _ => [ Blast_tac 1 ]);
paulson@2469
   137
paulson@2469
   138
Addsimps [cons_iff];
clasohm@0
   139
paulson@5325
   140
qed_goal "consI1" thy "a : cons(a,B)"
paulson@2469
   141
 (fn _ => [ Simp_tac 1 ]);
paulson@2469
   142
paulson@2469
   143
Addsimps [consI1];
paulson@6153
   144
AddTCs   [consI1];   (*risky as a typechecking rule, but solves otherwise
paulson@6153
   145
		       unconstrained goals of the form  x : ?A*)
clasohm@0
   146
paulson@5325
   147
qed_goal "consI2" thy "!!B. a : B ==> a : cons(b,B)"
paulson@2469
   148
 (fn _ => [ Asm_simp_tac 1 ]);
paulson@2469
   149
paulson@5325
   150
qed_goal "consE" thy
clasohm@0
   151
    "[| a : cons(b,A);  a=b ==> P;  a:A ==> P |] ==> P"
clasohm@0
   152
 (fn major::prems=>
paulson@2469
   153
  [ (rtac (major RS (cons_iff RS iffD1 RS disjE)) 1),
clasohm@0
   154
    (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);
clasohm@0
   155
lcp@572
   156
(*Stronger version of the rule above*)
paulson@5325
   157
qed_goal "consE'" thy
lcp@572
   158
    "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P"
lcp@572
   159
 (fn major::prems =>
lcp@572
   160
  [(rtac (major RS consE) 1),
lcp@572
   161
   (eresolve_tac prems 1),
lcp@572
   162
   (rtac classical 1),
lcp@572
   163
   (eresolve_tac prems 1),
lcp@572
   164
   (swap_res_tac prems 1),
lcp@572
   165
   (etac notnotD 1)]);
lcp@572
   166
paulson@2469
   167
(*Classical introduction rule*)
paulson@5325
   168
qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)"
paulson@2469
   169
 (fn prems=>
wenzelm@4091
   170
  [ Simp_tac 1, blast_tac (claset() addSIs prems) 1 ]);
clasohm@0
   171
paulson@2469
   172
AddSIs [consCI];
paulson@2469
   173
AddSEs [consE];
clasohm@0
   174
paulson@5325
   175
qed_goal "cons_not_0" thy "cons(a,B) ~= 0"
wenzelm@4091
   176
 (fn _ => [ (blast_tac (claset() addEs [equalityE]) 1) ]);
paulson@1609
   177
paulson@2469
   178
bind_thm ("cons_neq_0", cons_not_0 RS notE);
paulson@2469
   179
paulson@2469
   180
Addsimps [cons_not_0, cons_not_0 RS not_sym];
paulson@2469
   181
paulson@1609
   182
clasohm@0
   183
(*** Singletons - using cons ***)
clasohm@0
   184
paulson@5325
   185
qed_goal "singleton_iff" thy "a : {b} <-> a=b"
paulson@2469
   186
 (fn _ => [ Simp_tac 1 ]);
paulson@2469
   187
paulson@5325
   188
qed_goal "singletonI" thy "a : {a}"
clasohm@0
   189
 (fn _=> [ (rtac consI1 1) ]);
clasohm@0
   190
paulson@2469
   191
bind_thm ("singletonE", make_elim (singleton_iff RS iffD1));
clasohm@0
   192
paulson@2469
   193
AddSIs [singletonI];
paulson@2469
   194
AddSEs [singletonE];
clasohm@0
   195
clasohm@0
   196
(*** Rules for Descriptions ***)
clasohm@0
   197
paulson@5325
   198
qed_goalw "the_equality" thy [the_def]
clasohm@0
   199
    "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
lcp@738
   200
 (fn [pa,eq] =>
wenzelm@4091
   201
  [ (fast_tac (claset() addSIs [pa] addEs [eq RS subst]) 1) ]);
clasohm@0
   202
paulson@5506
   203
AddIs [the_equality];
paulson@5506
   204
clasohm@0
   205
(* Only use this if you already know EX!x. P(x) *)
paulson@5325
   206
qed_goal "the_equality2" thy
lcp@673
   207
    "!!P. [| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
paulson@5506
   208
 (fn _ => [ (Blast_tac 1) ]);
clasohm@0
   209
paulson@5325
   210
qed_goal "theI" thy "EX! x. P(x) ==> P(THE x. P(x))"
clasohm@0
   211
 (fn [major]=>
clasohm@0
   212
  [ (rtac (major RS ex1E) 1),
clasohm@0
   213
    (resolve_tac [major RS the_equality2 RS ssubst] 1),
clasohm@0
   214
    (REPEAT (assume_tac 1)) ]);
clasohm@0
   215
lcp@435
   216
(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then 
lcp@435
   217
  (THE x.P(x))  rewrites to  (THE x. Q(x))  *)
lcp@435
   218
lcp@435
   219
(*If it's "undefined", it's zero!*)
paulson@5325
   220
qed_goalw "the_0" thy [the_def]
lcp@435
   221
    "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
paulson@5488
   222
 (fn _ => [ (blast_tac (claset() addSEs [ReplaceE]) 1) ]);
lcp@435
   223
clasohm@0
   224
paulson@5506
   225
(*Easier to apply than theI: conclusion has only one occurrence of P*)
paulson@5506
   226
val prems = 
paulson@5506
   227
Goal "[| ~ Q(0) ==> EX! x. P(x);  !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))";
paulson@5506
   228
by (rtac classical 1);
paulson@5506
   229
by (resolve_tac prems 1);
paulson@5506
   230
by (rtac theI 1);
paulson@5506
   231
by (rtac classical 1);
paulson@5506
   232
by (resolve_tac prems 1);
paulson@6163
   233
by (etac (the_0 RS subst) 1);
paulson@6163
   234
by (assume_tac 1);
paulson@5506
   235
qed "theI2";
paulson@5506
   236
clasohm@0
   237
(*** if -- a conditional expression for formulae ***)
clasohm@0
   238
paulson@6068
   239
Goalw [if_def] "(if True then a else b) = a";
paulson@5506
   240
by (Blast_tac 1);
clasohm@760
   241
qed "if_true";
clasohm@0
   242
paulson@6068
   243
Goalw [if_def] "(if False then a else b) = b";
paulson@5506
   244
by (Blast_tac 1);
clasohm@760
   245
qed "if_false";
clasohm@0
   246
lcp@6
   247
(*Never use with case splitting, or if P is known to be true or false*)
paulson@5325
   248
val prems = Goalw [if_def]
paulson@6068
   249
    "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |] \
paulson@6068
   250
\    ==> (if P then a else b) = (if Q then c else d)";
wenzelm@4091
   251
by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1);
clasohm@760
   252
qed "if_cong";
clasohm@0
   253
clasohm@0
   254
(*Not needed for rewriting, since P would rewrite to True anyway*)
paulson@6068
   255
Goalw [if_def] "P ==> (if P then a else b) = a";
paulson@5506
   256
by (Blast_tac 1);
clasohm@760
   257
qed "if_P";
clasohm@0
   258
clasohm@0
   259
(*Not needed for rewriting, since P would rewrite to False anyway*)
paulson@6068
   260
Goalw [if_def] "~P ==> (if P then a else b) = b";
paulson@5506
   261
by (Blast_tac 1);
clasohm@760
   262
qed "if_not_P";
clasohm@0
   263
paulson@2469
   264
Addsimps [if_true, if_false];
clasohm@0
   265
paulson@5325
   266
qed_goal "split_if" thy
paulson@6068
   267
    "P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
paulson@5325
   268
 (fn _=> [ (case_tac "Q" 1),
paulson@2469
   269
           (Asm_simp_tac 1),
paulson@2469
   270
           (Asm_simp_tac 1) ]);
clasohm@0
   271
paulson@3914
   272
(** Rewrite rules for boolean case-splitting: faster than 
paulson@5116
   273
	addsplits[split_if]
paulson@3914
   274
**)
paulson@3914
   275
paulson@5116
   276
bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if);
paulson@5116
   277
bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if);
paulson@3914
   278
paulson@5116
   279
bind_thm ("split_if_mem1", read_instantiate [("P", "%x. x : ?b")] split_if);
paulson@5116
   280
bind_thm ("split_if_mem2", read_instantiate [("P", "%x. ?a : x")] split_if);
paulson@3914
   281
paulson@5116
   282
val split_ifs = [split_if_eq1, split_if_eq2,
paulson@5116
   283
		 split_if_mem1, split_if_mem2];
paulson@3914
   284
paulson@5116
   285
(*Logically equivalent to split_if_mem2*)
paulson@6068
   286
qed_goal "if_iff" thy "a: (if P then x else y) <-> P & a:x | ~P & a:y"
paulson@5116
   287
 (fn _=> [ (simp_tac (simpset() addsplits [split_if]) 1) ]);
lcp@1017
   288
paulson@5325
   289
qed_goal "if_type" thy
paulson@6068
   290
    "[| P ==> a: A;  ~P ==> b: A |] ==> (if P then a else b): A"
lcp@1017
   291
 (fn prems=> [ (simp_tac 
paulson@5116
   292
                (simpset() addsimps prems addsplits [split_if]) 1) ]);
paulson@6153
   293
AddTCs [if_type];
clasohm@0
   294
clasohm@0
   295
(*** Foundation lemmas ***)
clasohm@0
   296
lcp@437
   297
(*was called mem_anti_sym*)
paulson@5325
   298
qed_goal "mem_asym" thy "[| a:b;  ~P ==> b:a |] ==> P"
paulson@2877
   299
 (fn prems=>
paulson@2877
   300
  [ (rtac classical 1),
paulson@2877
   301
    (res_inst_tac [("A1","{a,b}")] (foundation RS disjE) 1),
wenzelm@4091
   302
    REPEAT (blast_tac (claset() addIs prems addSEs [equalityE]) 1) ]);
clasohm@0
   303
lcp@437
   304
(*was called mem_anti_refl*)
paulson@5325
   305
qed_goal "mem_irrefl" thy "a:a ==> P"
paulson@2469
   306
 (fn [major]=> [ (rtac ([major,major] MRS mem_asym) 1) ]);
clasohm@0
   307
paulson@2469
   308
(*mem_irrefl should NOT be added to default databases:
paulson@2469
   309
      it would be tried on most goals, making proofs slower!*)
paulson@2469
   310
paulson@5325
   311
qed_goal "mem_not_refl" thy "a ~: a"
lcp@437
   312
 (K [ (rtac notI 1), (etac mem_irrefl 1) ]);
clasohm@0
   313
lcp@435
   314
(*Good for proving inequalities by rewriting*)
paulson@5325
   315
qed_goal "mem_imp_not_eq" thy "!!a A. a:A ==> a ~= A"
wenzelm@4091
   316
 (fn _=> [ blast_tac (claset() addSEs [mem_irrefl]) 1 ]);
lcp@435
   317
clasohm@0
   318
(*** Rules for succ ***)
clasohm@0
   319
paulson@5325
   320
qed_goalw "succ_iff" thy [succ_def] "i : succ(j) <-> i=j | i:j"
paulson@2877
   321
 (fn _ => [ Blast_tac 1 ]);
paulson@2469
   322
paulson@5325
   323
qed_goalw "succI1" thy [succ_def] "i : succ(i)"
clasohm@0
   324
 (fn _=> [ (rtac consI1 1) ]);
clasohm@0
   325
paulson@2469
   326
Addsimps [succI1];
paulson@2469
   327
paulson@5325
   328
qed_goalw "succI2" thy [succ_def]
clasohm@0
   329
    "i : j ==> i : succ(j)"
clasohm@0
   330
 (fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
clasohm@0
   331
paulson@5325
   332
qed_goalw "succE" thy [succ_def]
clasohm@0
   333
    "[| i : succ(j);  i=j ==> P;  i:j ==> P |] ==> P"
clasohm@0
   334
 (fn major::prems=>
clasohm@0
   335
  [ (rtac (major RS consE) 1),
clasohm@0
   336
    (REPEAT (eresolve_tac prems 1)) ]);
clasohm@0
   337
lcp@14
   338
(*Classical introduction rule*)
paulson@5325
   339
qed_goal "succCI" thy "(i~:j ==> i=j) ==> i: succ(j)"
lcp@14
   340
 (fn [prem]=>
lcp@14
   341
  [ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
lcp@14
   342
    (etac prem 1) ]);
lcp@14
   343
paulson@2469
   344
AddSIs [succCI];
paulson@2469
   345
AddSEs [succE];
paulson@2469
   346
paulson@5325
   347
qed_goal "succ_not_0" thy "succ(n) ~= 0"
wenzelm@4091
   348
 (fn _=> [ (blast_tac (claset() addSEs [equalityE]) 1) ]);
clasohm@0
   349
paulson@2469
   350
bind_thm ("succ_neq_0", succ_not_0 RS notE);
paulson@2469
   351
paulson@2469
   352
Addsimps [succ_not_0, succ_not_0 RS not_sym];
paulson@2469
   353
AddSEs [succ_neq_0, sym RS succ_neq_0];
paulson@2469
   354
clasohm@0
   355
clasohm@0
   356
(* succ(c) <= B ==> c : B *)
clasohm@0
   357
val succ_subsetD = succI1 RSN (2,subsetD);
clasohm@0
   358
paulson@1609
   359
(* succ(b) ~= b *)
paulson@1609
   360
bind_thm ("succ_neq_self", succI1 RS mem_imp_not_eq RS not_sym);
paulson@1609
   361
paulson@1609
   362
paulson@5325
   363
qed_goal "succ_inject_iff" thy "succ(m) = succ(n) <-> m=n"
wenzelm@4091
   364
 (fn _=> [ (blast_tac (claset() addEs [mem_asym] addSEs [equalityE]) 1) ]);
clasohm@0
   365
paulson@2469
   366
bind_thm ("succ_inject", succ_inject_iff RS iffD1);
clasohm@0
   367
paulson@2469
   368
Addsimps [succ_inject_iff];
paulson@2469
   369
AddSDs [succ_inject];
clasohm@0
   370
paulson@2877
   371
(*Not needed now that cons is available.  Deletion reduces the search space.*)
paulson@2877
   372
Delrules [UpairI1,UpairI2,UpairE];
paulson@2469
   373
paulson@2469
   374
use"simpdata.ML";