src/ZF/pair.ML
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/pair
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   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Ordered pairs in 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
(** Lemmas for showing that <a,b> uniquely determines a and b **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val doubleton_iff = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
    "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
 (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
           (fast_tac upair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
val Pair_iff = prove_goalw ZF.thy [Pair_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
    "<a,b> = <c,d> <-> a=c & b=d"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
 (fn _=> [ (SIMP_TAC (FOL_ss addrews [doubleton_iff]) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
           (fast_tac FOL_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
val Pair_inject1 = prove_goal ZF.thy "<a,b> = <c,d> ==> a=c"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  [ (rtac (major RS Pair_inject) 1), (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val Pair_inject2 = prove_goal ZF.thy "<a,b> = <c,d> ==> b=d"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  [ (rtac (major RS Pair_inject) 1), (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
val Pair_neq_0 = prove_goalw ZF.thy [Pair_def] "<a,b>=0 ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  [ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
    (rtac consI1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
val Pair_neq_fst = prove_goalw ZF.thy [Pair_def] "<a,b>=a ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  [ (rtac (consI1 RS mem_anti_sym RS FalseE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
    (rtac (major RS subst) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
    (rtac consI1 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
val Pair_neq_snd = prove_goalw ZF.thy [Pair_def] "<a,b>=b ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
  [ (rtac (consI1 RS consI2 RS mem_anti_sym RS FalseE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
    (rtac (major RS subst) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
    (rtac (consI1 RS consI2) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
(*** Sigma: Disjoint union of a family of sets
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
     Generalizes Cartesian product ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
val SigmaI = prove_goalw ZF.thy [Sigma_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
    "[| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
 (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
(*The general elimination rule*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
val SigmaE = prove_goalw ZF.thy [Sigma_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
    "[| c: Sigma(A,B);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
\       !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
\    |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
  [ (cut_facts_tac [major] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
    (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
(** Elimination of <a,b>:A*B -- introduces no eigenvariables **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
val SigmaD1 = prove_goal ZF.thy "<a,b> : Sigma(A,B) ==> a : A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  [ (rtac (major RS SigmaE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
    (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
val SigmaD2 = prove_goal ZF.thy "<a,b> : Sigma(A,B) ==> b : B(a)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
  [ (rtac (major RS SigmaE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
    (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
(*Also provable via 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
  rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
		  THEN prune_params_tac)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
      (read_instantiate [("c","<a,b>")] SigmaE);  *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
val SigmaE2 = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
    "[| <a,b> : Sigma(A,B);    \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
\       [| a:A;  b:B(a) |] ==> P   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
\    |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
 (fn [major,minor]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
  [ (rtac minor 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
    (rtac (major RS SigmaD1) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
    (rtac (major RS SigmaD2) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
val Sigma_cong = prove_goalw ZF.thy [Sigma_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
\    Sigma(A,B) = Sigma(A',B')"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
 (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
val Sigma_empty1 = prove_goal ZF.thy "Sigma(0,B) = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
 (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
val Sigma_empty2 = prove_goal ZF.thy "A*0 = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
 (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
(*** Eliminator - split ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
val split = prove_goalw ZF.thy [split_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
    "split(%x y.c(x,y), <a,b>) = c(a,b)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
 (fn _ =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
  [ (fast_tac (upair_cs addIs [the_equality] addEs [Pair_inject]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
val split_type = prove_goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
    "[|  p:Sigma(A,B);   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
\        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
\    |] ==> split(%x y.c(x,y), p) : C(p)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
  [ (rtac (major RS SigmaE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
    (etac ssubst 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
    (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
(*This congruence rule uses NO typing information...*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
val split_cong = prove_goalw ZF.thy [split_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
    "[| p=p';  !!x y.c(x,y) = c'(x,y) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
\    split(%x y.c(x,y), p) = split(%x y.c'(x,y), p')"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
 (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
(*** conversions for fst and snd ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
 (fn _=> [ (rtac split 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
val snd_conv = prove_goalw ZF.thy [snd_def] "snd(<a,b>) = b"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
 (fn _=> [ (rtac split 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
(*** split for predicates: result type o ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
goalw ZF.thy [fsplit_def] "!!R a b. R(a,b) ==> fsplit(R, <a,b>)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
by (REPEAT (ares_tac [refl,exI,conjI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
val fsplitI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
val major::prems = goalw ZF.thy [fsplit_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
    "[| fsplit(R,z);  !!x y. [| z = <x,y>;  R(x,y) |] ==> P |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
by (cut_facts_tac [major] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
by (REPEAT (eresolve_tac (prems@[asm_rl,exE,conjE]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
val fsplitE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
goal ZF.thy "!!R a b. fsplit(R,<a,b>) ==> R(a,b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
by (REPEAT (eresolve_tac [asm_rl,fsplitE,Pair_inject,ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
val fsplitD = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
val pair_cs = upair_cs 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
    addSIs [SigmaI]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
    addSEs [SigmaE2, SigmaE, Pair_inject, make_elim succ_inject,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
	    Pair_neq_0, sym RS Pair_neq_0, succ_neq_0, sym RS succ_neq_0];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153