6 Ordered pairs in Zermelo-Fraenkel Set Theory |
6 Ordered pairs in Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
9 (** Lemmas for showing that <a,b> uniquely determines a and b **) |
9 (** Lemmas for showing that <a,b> uniquely determines a and b **) |
10 |
10 |
11 qed_goal "singleton_eq_iff" thy |
11 Goal "{a} = {b} <-> a=b"; |
12 "{a} = {b} <-> a=b" |
12 by (resolve_tac [extension RS iff_trans] 1); |
13 (fn _=> [ (resolve_tac [extension RS iff_trans] 1), |
13 by (Blast_tac 1) ; |
14 (Blast_tac 1) ]); |
14 qed "singleton_eq_iff"; |
15 |
15 |
16 qed_goal "doubleton_eq_iff" thy |
16 Goal "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"; |
17 "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)" |
17 by (resolve_tac [extension RS iff_trans] 1); |
18 (fn _=> [ (resolve_tac [extension RS iff_trans] 1), |
18 by (Blast_tac 1) ; |
19 (Blast_tac 1) ]); |
19 qed "doubleton_eq_iff"; |
20 |
20 |
21 qed_goalw "Pair_iff" thy [Pair_def] |
21 qed_goalw "Pair_iff" thy [Pair_def] |
22 "<a,b> = <c,d> <-> a=c & b=d" |
22 "<a,b> = <c,d> <-> a=c & b=d" |
23 (fn _=> [ (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1), |
23 (fn _=> [ (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1), |
24 (Blast_tac 1) ]); |
24 (Blast_tac 1) ]); |
58 qed_goalw "Sigma_iff" thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)" |
58 qed_goalw "Sigma_iff" thy [Sigma_def] "<a,b>: Sigma(A,B) <-> a:A & b:B(a)" |
59 (fn _ => [ Blast_tac 1 ]); |
59 (fn _ => [ Blast_tac 1 ]); |
60 |
60 |
61 Addsimps [Sigma_iff]; |
61 Addsimps [Sigma_iff]; |
62 |
62 |
63 qed_goal "SigmaI" thy |
63 Goal "[| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)"; |
64 "!!a b. [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)" |
64 by (Asm_simp_tac 1); |
65 (fn _ => [ Asm_simp_tac 1 ]); |
65 qed "SigmaI"; |
|
66 |
66 AddTCs [SigmaI]; |
67 AddTCs [SigmaI]; |
67 |
68 |
68 bind_thm ("SigmaD1", Sigma_iff RS iffD1 RS conjunct1); |
69 bind_thm ("SigmaD1", Sigma_iff RS iffD1 RS conjunct1); |
69 bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2); |
70 bind_thm ("SigmaD2", Sigma_iff RS iffD1 RS conjunct2); |
70 |
71 |
75 \ |] ==> P" |
76 \ |] ==> P" |
76 (fn major::prems=> |
77 (fn major::prems=> |
77 [ (cut_facts_tac [major] 1), |
78 [ (cut_facts_tac [major] 1), |
78 (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]); |
79 (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]); |
79 |
80 |
80 qed_goal "SigmaE2" thy |
81 val [major,minor]= Goal |
81 "[| <a,b> : Sigma(A,B); \ |
82 "[| <a,b> : Sigma(A,B); \ |
82 \ [| a:A; b:B(a) |] ==> P \ |
83 \ [| a:A; b:B(a) |] ==> P \ |
83 \ |] ==> P" |
84 \ |] ==> P"; |
84 (fn [major,minor]=> |
85 by (rtac minor 1); |
85 [ (rtac minor 1), |
86 by (rtac (major RS SigmaD1) 1); |
86 (rtac (major RS SigmaD1) 1), |
87 by (rtac (major RS SigmaD2) 1) ; |
87 (rtac (major RS SigmaD2) 1) ]); |
88 qed "SigmaE2"; |
88 |
89 |
89 qed_goalw "Sigma_cong" thy [Sigma_def] |
90 qed_goalw "Sigma_cong" thy [Sigma_def] |
90 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
91 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
91 \ Sigma(A,B) = Sigma(A',B')" |
92 \ Sigma(A,B) = Sigma(A',B')" |
92 (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]); |
93 (fn prems=> [ (simp_tac (simpset() addsimps prems) 1) ]); |
97 Sigmas and Pis are abbreviated as * or -> *) |
98 Sigmas and Pis are abbreviated as * or -> *) |
98 |
99 |
99 AddSIs [SigmaI]; |
100 AddSIs [SigmaI]; |
100 AddSEs [SigmaE2, SigmaE]; |
101 AddSEs [SigmaE2, SigmaE]; |
101 |
102 |
102 qed_goal "Sigma_empty1" thy "Sigma(0,B) = 0" |
103 Goal "Sigma(0,B) = 0"; |
103 (fn _ => [ (Blast_tac 1) ]); |
104 by (Blast_tac 1) ; |
|
105 qed "Sigma_empty1"; |
104 |
106 |
105 qed_goal "Sigma_empty2" thy "A*0 = 0" |
107 Goal "A*0 = 0"; |
106 (fn _ => [ (Blast_tac 1) ]); |
108 by (Blast_tac 1) ; |
|
109 qed "Sigma_empty2"; |
107 |
110 |
108 Addsimps [Sigma_empty1, Sigma_empty2]; |
111 Addsimps [Sigma_empty1, Sigma_empty2]; |
109 |
112 |
110 Goal "A*B=0 <-> A=0 | B=0"; |
113 Goal "A*B=0 <-> A=0 | B=0"; |
111 by (Blast_tac 1); |
114 by (Blast_tac 1); |
120 qed_goalw "snd_conv" thy [snd_def] "snd(<a,b>) = b" |
123 qed_goalw "snd_conv" thy [snd_def] "snd(<a,b>) = b" |
121 (fn _=> [ (Blast_tac 1) ]); |
124 (fn _=> [ (Blast_tac 1) ]); |
122 |
125 |
123 Addsimps [fst_conv,snd_conv]; |
126 Addsimps [fst_conv,snd_conv]; |
124 |
127 |
125 qed_goal "fst_type" thy "!!p. p:Sigma(A,B) ==> fst(p) : A" |
128 Goal "p:Sigma(A,B) ==> fst(p) : A"; |
126 (fn _=> [ Auto_tac ]); |
129 by (Auto_tac) ; |
|
130 qed "fst_type"; |
127 |
131 |
128 qed_goal "snd_type" thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))" |
132 Goal "p:Sigma(A,B) ==> snd(p) : B(fst(p))"; |
129 (fn _=> [ Auto_tac ]); |
133 by (Auto_tac) ; |
|
134 qed "snd_type"; |
130 |
135 |
131 qed_goal "Pair_fst_snd_eq" thy |
136 Goal "a: Sigma(A,B) ==> <fst(a),snd(a)> = a"; |
132 "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a" |
137 by (Auto_tac) ; |
133 (fn _=> [ Auto_tac ]); |
138 qed "Pair_fst_snd_eq"; |
134 |
139 |
135 |
140 |
136 (*** Eliminator - split ***) |
141 (*** Eliminator - split ***) |
137 |
142 |
138 (*A META-equality, so that it applies to higher types as well...*) |
143 (*A META-equality, so that it applies to higher types as well...*) |
139 Goalw [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"; |
144 Goalw [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"; |
140 by (Simp_tac 1); |
145 by (Simp_tac 1); |
141 qed "split"; |
146 qed "split"; |
142 Addsimps [split]; |
147 Addsimps [split]; |
143 |
148 |
144 qed_goal "split_type" thy |
149 val major::prems= Goal |
145 "[| p:Sigma(A,B); \ |
150 "[| p:Sigma(A,B); \ |
146 \ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \ |
151 \ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \ |
147 \ |] ==> split(%x y. c(x,y), p) : C(p)" |
152 \ |] ==> split(%x y. c(x,y), p) : C(p)"; |
148 (fn major::prems=> |
153 by (rtac (major RS SigmaE) 1); |
149 [ (rtac (major RS SigmaE) 1), |
154 by (asm_simp_tac (simpset() addsimps prems) 1); |
150 (asm_simp_tac (simpset() addsimps prems) 1) ]); |
155 qed "split_type"; |
151 AddTCs [split_type]; |
156 AddTCs [split_type]; |
152 |
157 |
153 Goalw [split_def] |
158 Goalw [split_def] |
154 "u: A*B ==> \ |
159 "u: A*B ==> \ |
155 \ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"; |
160 \ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"; |