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
6 Ordered pairs in Zermelo-Fraenkel Set Theory
7 *)
9 (** Lemmas for showing that <a,b> uniquely determines a and b **)
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) ]);
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) ]);
21 val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);
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) ]);
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) ]);
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) ]);
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) ]);
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) ]);
49 (*** Sigma: Disjoint union of a family of sets
50      Generalizes Cartesian product ***)
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)) ]);
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)) ]);
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)) ]);
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)) ]);
76 (*Also provable via
77   rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
78 		  THEN prune_params_tac)
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) ]);
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) ]);
94 val Sigma_empty1 = prove_goal ZF.thy "Sigma(0,B) = 0"
95  (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
97 val Sigma_empty2 = prove_goal ZF.thy "A*0 = 0"
98  (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
101 (*** Eliminator - split ***)
103 val split = prove_goalw ZF.thy [split_def]
104     "split(%x y.c(x,y), <a,b>) = c(a,b)"
105  (fn _ =>
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)) ]);
117 (*** conversions for fst and snd ***)
119 val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"
120  (fn _=> [ (rtac split 1) ]);
122 val snd_conv = prove_goalw ZF.thy [snd_def] "snd(<a,b>) = b"
123  (fn _=> [ (rtac split 1) ]);
126 (*** split for predicates: result type o ***)
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();
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();
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();
142 val pair_cs = upair_cs