src/ZF/pair.ML
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/pair.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,153 @@
     1.4 +(*  Title: 	ZF/pair
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +Ordered pairs in Zermelo-Fraenkel Set Theory 
    1.10 +*)
    1.11 +
    1.12 +(** Lemmas for showing that <a,b> uniquely determines a and b **)
    1.13 +
    1.14 +val doubleton_iff = prove_goal ZF.thy
    1.15 +    "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
    1.16 + (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
    1.17 +           (fast_tac upair_cs 1) ]);
    1.18 +
    1.19 +val Pair_iff = prove_goalw ZF.thy [Pair_def]
    1.20 +    "<a,b> = <c,d> <-> a=c & b=d"
    1.21 + (fn _=> [ (SIMP_TAC (FOL_ss addrews [doubleton_iff]) 1),
    1.22 +           (fast_tac FOL_cs 1) ]);
    1.23 +
    1.24 +val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);
    1.25 +
    1.26 +val Pair_inject1 = prove_goal ZF.thy "<a,b> = <c,d> ==> a=c"
    1.27 + (fn [major]=>
    1.28 +  [ (rtac (major RS Pair_inject) 1), (assume_tac 1) ]);
    1.29 +
    1.30 +val Pair_inject2 = prove_goal ZF.thy "<a,b> = <c,d> ==> b=d"
    1.31 + (fn [major]=>
    1.32 +  [ (rtac (major RS Pair_inject) 1), (assume_tac 1) ]);
    1.33 +
    1.34 +val Pair_neq_0 = prove_goalw ZF.thy [Pair_def] "<a,b>=0 ==> P"
    1.35 + (fn [major]=>
    1.36 +  [ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),
    1.37 +    (rtac consI1 1) ]);
    1.38 +
    1.39 +val Pair_neq_fst = prove_goalw ZF.thy [Pair_def] "<a,b>=a ==> P"
    1.40 + (fn [major]=>
    1.41 +  [ (rtac (consI1 RS mem_anti_sym RS FalseE) 1),
    1.42 +    (rtac (major RS subst) 1),
    1.43 +    (rtac consI1 1) ]);
    1.44 +
    1.45 +val Pair_neq_snd = prove_goalw ZF.thy [Pair_def] "<a,b>=b ==> P"
    1.46 + (fn [major]=>
    1.47 +  [ (rtac (consI1 RS consI2 RS mem_anti_sym RS FalseE) 1),
    1.48 +    (rtac (major RS subst) 1),
    1.49 +    (rtac (consI1 RS consI2) 1) ]);
    1.50 +
    1.51 +
    1.52 +(*** Sigma: Disjoint union of a family of sets
    1.53 +     Generalizes Cartesian product ***)
    1.54 +
    1.55 +val SigmaI = prove_goalw ZF.thy [Sigma_def]
    1.56 +    "[| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)"
    1.57 + (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
    1.58 +
    1.59 +(*The general elimination rule*)
    1.60 +val SigmaE = prove_goalw ZF.thy [Sigma_def]
    1.61 +    "[| c: Sigma(A,B);  \
    1.62 +\       !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P \
    1.63 +\    |] ==> P"
    1.64 + (fn major::prems=>
    1.65 +  [ (cut_facts_tac [major] 1),
    1.66 +    (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
    1.67 +
    1.68 +(** Elimination of <a,b>:A*B -- introduces no eigenvariables **)
    1.69 +val SigmaD1 = prove_goal ZF.thy "<a,b> : Sigma(A,B) ==> a : A"
    1.70 + (fn [major]=>
    1.71 +  [ (rtac (major RS SigmaE) 1),
    1.72 +    (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
    1.73 +
    1.74 +val SigmaD2 = prove_goal ZF.thy "<a,b> : Sigma(A,B) ==> b : B(a)"
    1.75 + (fn [major]=>
    1.76 +  [ (rtac (major RS SigmaE) 1),
    1.77 +    (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
    1.78 +
    1.79 +(*Also provable via 
    1.80 +  rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
    1.81 +		  THEN prune_params_tac)
    1.82 +      (read_instantiate [("c","<a,b>")] SigmaE);  *)
    1.83 +val SigmaE2 = prove_goal ZF.thy
    1.84 +    "[| <a,b> : Sigma(A,B);    \
    1.85 +\       [| a:A;  b:B(a) |] ==> P   \
    1.86 +\    |] ==> P"
    1.87 + (fn [major,minor]=>
    1.88 +  [ (rtac minor 1),
    1.89 +    (rtac (major RS SigmaD1) 1),
    1.90 +    (rtac (major RS SigmaD2) 1) ]);
    1.91 +
    1.92 +val Sigma_cong = prove_goalw ZF.thy [Sigma_def]
    1.93 +    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
    1.94 +\    Sigma(A,B) = Sigma(A',B')"
    1.95 + (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
    1.96 +
    1.97 +val Sigma_empty1 = prove_goal ZF.thy "Sigma(0,B) = 0"
    1.98 + (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
    1.99 +
   1.100 +val Sigma_empty2 = prove_goal ZF.thy "A*0 = 0"
   1.101 + (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
   1.102 +
   1.103 +
   1.104 +(*** Eliminator - split ***)
   1.105 +
   1.106 +val split = prove_goalw ZF.thy [split_def]
   1.107 +    "split(%x y.c(x,y), <a,b>) = c(a,b)"
   1.108 + (fn _ =>
   1.109 +  [ (fast_tac (upair_cs addIs [the_equality] addEs [Pair_inject]) 1) ]);
   1.110 +
   1.111 +val split_type = prove_goal ZF.thy
   1.112 +    "[|  p:Sigma(A,B);   \
   1.113 +\        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \
   1.114 +\    |] ==> split(%x y.c(x,y), p) : C(p)"
   1.115 + (fn major::prems=>
   1.116 +  [ (rtac (major RS SigmaE) 1),
   1.117 +    (etac ssubst 1),
   1.118 +    (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
   1.119 +
   1.120 +(*This congruence rule uses NO typing information...*)
   1.121 +val split_cong = prove_goalw ZF.thy [split_def] 
   1.122 +    "[| p=p';  !!x y.c(x,y) = c'(x,y) |] ==> \
   1.123 +\    split(%x y.c(x,y), p) = split(%x y.c'(x,y), p')"
   1.124 + (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
   1.125 +
   1.126 +
   1.127 +(*** conversions for fst and snd ***)
   1.128 +
   1.129 +val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"
   1.130 + (fn _=> [ (rtac split 1) ]);
   1.131 +
   1.132 +val snd_conv = prove_goalw ZF.thy [snd_def] "snd(<a,b>) = b"
   1.133 + (fn _=> [ (rtac split 1) ]);
   1.134 +
   1.135 +
   1.136 +(*** split for predicates: result type o ***)
   1.137 +
   1.138 +goalw ZF.thy [fsplit_def] "!!R a b. R(a,b) ==> fsplit(R, <a,b>)";
   1.139 +by (REPEAT (ares_tac [refl,exI,conjI] 1));
   1.140 +val fsplitI = result();
   1.141 +
   1.142 +val major::prems = goalw ZF.thy [fsplit_def]
   1.143 +    "[| fsplit(R,z);  !!x y. [| z = <x,y>;  R(x,y) |] ==> P |] ==> P";
   1.144 +by (cut_facts_tac [major] 1);
   1.145 +by (REPEAT (eresolve_tac (prems@[asm_rl,exE,conjE]) 1));
   1.146 +val fsplitE = result();
   1.147 +
   1.148 +goal ZF.thy "!!R a b. fsplit(R,<a,b>) ==> R(a,b)";
   1.149 +by (REPEAT (eresolve_tac [asm_rl,fsplitE,Pair_inject,ssubst] 1));
   1.150 +val fsplitD = result();
   1.151 +
   1.152 +val pair_cs = upair_cs 
   1.153 +    addSIs [SigmaI]
   1.154 +    addSEs [SigmaE2, SigmaE, Pair_inject, make_elim succ_inject,
   1.155 +	    Pair_neq_0, sym RS Pair_neq_0, succ_neq_0, sym RS succ_neq_0];
   1.156 +