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