author | clasohm |
Fri, 02 Feb 1996 12:05:24 +0100 | |
changeset 1472 | a89803e3d1bd |
parent 1465 | 5d7a7e439cec |
child 1485 | 240cc98b94a7 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/prod |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
923 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
For prod.thy. Ordered Pairs, the Cartesian product type, the unit type |
|
7 |
*) |
|
8 |
||
9 |
open Prod; |
|
10 |
||
11 |
(*This counts as a non-emptiness result for admitting 'a * 'b as a type*) |
|
12 |
goalw Prod.thy [Prod_def] "Pair_Rep a b : Prod"; |
|
13 |
by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]); |
|
14 |
qed "ProdI"; |
|
15 |
||
16 |
val [major] = goalw Prod.thy [Pair_Rep_def] |
|
17 |
"Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'"; |
|
18 |
by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), |
|
1465 | 19 |
rtac conjI, rtac refl, rtac refl]); |
923 | 20 |
qed "Pair_Rep_inject"; |
21 |
||
22 |
goal Prod.thy "inj_onto Abs_Prod Prod"; |
|
23 |
by (rtac inj_onto_inverseI 1); |
|
24 |
by (etac Abs_Prod_inverse 1); |
|
25 |
qed "inj_onto_Abs_Prod"; |
|
26 |
||
27 |
val prems = goalw Prod.thy [Pair_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
28 |
"[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R"; |
923 | 29 |
by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1); |
30 |
by (REPEAT (ares_tac (prems@[ProdI]) 1)); |
|
31 |
qed "Pair_inject"; |
|
32 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
33 |
goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')"; |
923 | 34 |
by (fast_tac (set_cs addIs [Pair_inject]) 1); |
35 |
qed "Pair_eq"; |
|
36 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
37 |
goalw Prod.thy [fst_def] "fst((a,b)) = a"; |
923 | 38 |
by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1); |
39 |
qed "fst_conv"; |
|
40 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
41 |
goalw Prod.thy [snd_def] "snd((a,b)) = b"; |
923 | 42 |
by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1); |
43 |
qed "snd_conv"; |
|
44 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
45 |
goalw Prod.thy [Pair_def] "? x y. p = (x,y)"; |
923 | 46 |
by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1); |
47 |
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI, |
|
1465 | 48 |
rtac (Rep_Prod_inverse RS sym RS trans), etac arg_cong]); |
923 | 49 |
qed "PairE_lemma"; |
50 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
51 |
val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q"; |
923 | 52 |
by (rtac (PairE_lemma RS exE) 1); |
53 |
by (REPEAT (eresolve_tac [prem,exE] 1)); |
|
54 |
qed "PairE"; |
|
55 |
||
1301 | 56 |
(* replace parameters of product type by individual component parameters *) |
57 |
local |
|
58 |
fun is_pair (_,Type("*",_)) = true |
|
59 |
| is_pair _ = false; |
|
60 |
||
61 |
fun find_pair_param t = |
|
62 |
let val params = Logic.strip_params t |
|
63 |
in if exists is_pair params |
|
64 |
then let val params = rev(rename_wrt_term t params) |
|
65 |
(*as they are printed*) |
|
66 |
in apsome fst (find_first is_pair params) end |
|
67 |
else None |
|
68 |
end; |
|
69 |
||
70 |
in |
|
71 |
||
72 |
val split_all_tac = REPEAT o SUBGOAL (fn (t,_) => |
|
73 |
case find_pair_param t of |
|
74 |
None => no_tac |
|
75 |
| Some x => EVERY[res_inst_tac[("p",x)] PairE 1, |
|
76 |
REPEAT(hyp_subst_tac 1), prune_params_tac]); |
|
77 |
||
78 |
end; |
|
79 |
||
80 |
goal Prod.thy "(!x. P x) = (!a b. P(a,b))"; |
|
81 |
by(fast_tac (HOL_cs addbefore split_all_tac 1) 1); |
|
82 |
qed "split_paired_All"; |
|
83 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
84 |
goalw Prod.thy [split_def] "split c (a,b) = c a b"; |
923 | 85 |
by (sstac [fst_conv, snd_conv] 1); |
86 |
by (rtac refl 1); |
|
87 |
qed "split"; |
|
88 |
||
1301 | 89 |
Addsimps [fst_conv, snd_conv, split_paired_All, split, Pair_eq]; |
923 | 90 |
|
91 |
goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; |
|
92 |
by (res_inst_tac[("p","s")] PairE 1); |
|
93 |
by (res_inst_tac[("p","t")] PairE 1); |
|
1264 | 94 |
by (Asm_simp_tac 1); |
923 | 95 |
qed "Pair_fst_snd_eq"; |
96 |
||
97 |
(*Prevents simplification of c: much faster*) |
|
98 |
qed_goal "split_weak_cong" Prod.thy |
|
99 |
"p=q ==> split c p = split c q" |
|
100 |
(fn [prem] => [rtac (prem RS arg_cong) 1]); |
|
101 |
||
102 |
(* Do not add as rewrite rule: invalidates some proofs in IMP *) |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
103 |
goal Prod.thy "p = (fst(p),snd(p))"; |
923 | 104 |
by (res_inst_tac [("p","p")] PairE 1); |
1264 | 105 |
by (Asm_simp_tac 1); |
923 | 106 |
qed "surjective_pairing"; |
107 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
108 |
goal Prod.thy "p = split (%x y.(x,y)) p"; |
923 | 109 |
by (res_inst_tac [("p","p")] PairE 1); |
1264 | 110 |
by (Asm_simp_tac 1); |
923 | 111 |
qed "surjective_pairing2"; |
112 |
||
113 |
(*For use with split_tac and the simplifier*) |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
114 |
goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))"; |
923 | 115 |
by (stac surjective_pairing 1); |
116 |
by (stac split 1); |
|
117 |
by (fast_tac (HOL_cs addSEs [Pair_inject]) 1); |
|
118 |
qed "expand_split"; |
|
119 |
||
120 |
(** split used as a logical connective or set former **) |
|
121 |
||
122 |
(*These rules are for use with fast_tac. |
|
123 |
Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*) |
|
124 |
||
1454
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
125 |
goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p"; |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
126 |
by(split_all_tac 1); |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
127 |
by (Asm_simp_tac 1); |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
128 |
qed "splitI2"; |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
129 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
130 |
goal Prod.thy "!!a b c. c a b ==> split c (a,b)"; |
1264 | 131 |
by (Asm_simp_tac 1); |
923 | 132 |
qed "splitI"; |
133 |
||
134 |
val prems = goalw Prod.thy [split_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
135 |
"[| split c p; !!x y. [| p = (x,y); c x y |] ==> Q |] ==> Q"; |
923 | 136 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
137 |
qed "splitE"; |
|
138 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
139 |
goal Prod.thy "!!R a b. split R (a,b) ==> R a b"; |
923 | 140 |
by (etac (split RS iffD1) 1); |
141 |
qed "splitD"; |
|
142 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
143 |
goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)"; |
1264 | 144 |
by (Asm_simp_tac 1); |
923 | 145 |
qed "mem_splitI"; |
146 |
||
1454
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
147 |
goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p"; |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
148 |
by(split_all_tac 1); |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
149 |
by (Asm_simp_tac 1); |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
150 |
qed "mem_splitI2"; |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
151 |
|
923 | 152 |
val prems = goalw Prod.thy [split_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
153 |
"[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"; |
923 | 154 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
155 |
qed "mem_splitE"; |
|
156 |
||
157 |
(*** prod_fun -- action of the product functor upon functions ***) |
|
158 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
159 |
goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))"; |
923 | 160 |
by (rtac split 1); |
161 |
qed "prod_fun"; |
|
162 |
||
163 |
goal Prod.thy |
|
164 |
"prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))"; |
|
165 |
by (rtac ext 1); |
|
166 |
by (res_inst_tac [("p","x")] PairE 1); |
|
1264 | 167 |
by (asm_simp_tac (!simpset addsimps [prod_fun,o_def]) 1); |
923 | 168 |
qed "prod_fun_compose"; |
169 |
||
170 |
goal Prod.thy "prod_fun (%x.x) (%y.y) = (%z.z)"; |
|
171 |
by (rtac ext 1); |
|
172 |
by (res_inst_tac [("p","z")] PairE 1); |
|
1264 | 173 |
by (asm_simp_tac (!simpset addsimps [prod_fun]) 1); |
923 | 174 |
qed "prod_fun_ident"; |
175 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
176 |
val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r"; |
923 | 177 |
by (rtac image_eqI 1); |
178 |
by (rtac (prod_fun RS sym) 1); |
|
179 |
by (resolve_tac prems 1); |
|
180 |
qed "prod_fun_imageI"; |
|
181 |
||
182 |
val major::prems = goal Prod.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
183 |
"[| c: (prod_fun f g)``r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \ |
923 | 184 |
\ |] ==> P"; |
185 |
by (rtac (major RS imageE) 1); |
|
186 |
by (res_inst_tac [("p","x")] PairE 1); |
|
187 |
by (resolve_tac prems 1); |
|
188 |
by (fast_tac HOL_cs 2); |
|
189 |
by (fast_tac (HOL_cs addIs [prod_fun]) 1); |
|
190 |
qed "prod_fun_imageE"; |
|
191 |
||
192 |
(*** Disjoint union of a family of sets - Sigma ***) |
|
193 |
||
194 |
qed_goalw "SigmaI" Prod.thy [Sigma_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
195 |
"[| a:A; b:B(a) |] ==> (a,b) : Sigma A B" |
923 | 196 |
(fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]); |
197 |
||
198 |
(*The general elimination rule*) |
|
199 |
qed_goalw "SigmaE" Prod.thy [Sigma_def] |
|
200 |
"[| c: Sigma A B; \ |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
201 |
\ !!x y.[| x:A; y:B(x); c=(x,y) |] ==> P \ |
923 | 202 |
\ |] ==> P" |
203 |
(fn major::prems=> |
|
204 |
[ (cut_facts_tac [major] 1), |
|
205 |
(REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]); |
|
206 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
207 |
(** Elimination of (a,b):A*B -- introduces no eigenvariables **) |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
208 |
qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A" |
923 | 209 |
(fn [major]=> |
210 |
[ (rtac (major RS SigmaE) 1), |
|
211 |
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); |
|
212 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
213 |
qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)" |
923 | 214 |
(fn [major]=> |
215 |
[ (rtac (major RS SigmaE) 1), |
|
216 |
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); |
|
217 |
||
218 |
qed_goal "SigmaE2" Prod.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
219 |
"[| (a,b) : Sigma A B; \ |
923 | 220 |
\ [| a:A; b:B(a) |] ==> P \ |
221 |
\ |] ==> P" |
|
222 |
(fn [major,minor]=> |
|
223 |
[ (rtac minor 1), |
|
224 |
(rtac (major RS SigmaD1) 1), |
|
225 |
(rtac (major RS SigmaD2) 1) ]); |
|
226 |
||
227 |
(*** Domain of a relation ***) |
|
228 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
229 |
val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r"; |
923 | 230 |
by (rtac CollectI 1); |
231 |
by (rtac bexI 1); |
|
232 |
by (rtac (fst_conv RS sym) 1); |
|
233 |
by (resolve_tac prems 1); |
|
234 |
qed "fst_imageI"; |
|
235 |
||
236 |
val major::prems = goal Prod.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
237 |
"[| a : fst``r; !!y.[| (a,y) : r |] ==> P |] ==> P"; |
923 | 238 |
by (rtac (major RS imageE) 1); |
239 |
by (resolve_tac prems 1); |
|
240 |
by (etac ssubst 1); |
|
241 |
by (rtac (surjective_pairing RS subst) 1); |
|
242 |
by (assume_tac 1); |
|
243 |
qed "fst_imageE"; |
|
244 |
||
245 |
(*** Range of a relation ***) |
|
246 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
247 |
val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r"; |
923 | 248 |
by (rtac CollectI 1); |
249 |
by (rtac bexI 1); |
|
250 |
by (rtac (snd_conv RS sym) 1); |
|
251 |
by (resolve_tac prems 1); |
|
252 |
qed "snd_imageI"; |
|
253 |
||
254 |
val major::prems = goal Prod.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
255 |
"[| a : snd``r; !!y.[| (y,a) : r |] ==> P |] ==> P"; |
923 | 256 |
by (rtac (major RS imageE) 1); |
257 |
by (resolve_tac prems 1); |
|
258 |
by (etac ssubst 1); |
|
259 |
by (rtac (surjective_pairing RS subst) 1); |
|
260 |
by (assume_tac 1); |
|
261 |
qed "snd_imageE"; |
|
262 |
||
263 |
(** Exhaustion rule for unit -- a degenerate form of induction **) |
|
264 |
||
265 |
goalw Prod.thy [Unity_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
266 |
"u = ()"; |
923 | 267 |
by (stac (rewrite_rule [Unit_def] Rep_Unit RS CollectD RS sym) 1); |
268 |
by (rtac (Rep_Unit_inverse RS sym) 1); |
|
269 |
qed "unit_eq"; |
|
270 |
||
1454
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
271 |
val prod_cs = set_cs addSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2] |
923 | 272 |
addIs [fst_imageI, snd_imageI, prod_fun_imageI] |
1454
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
273 |
addSEs [SigmaE2, SigmaE, splitE, mem_splitE, |
1465 | 274 |
fst_imageE, snd_imageE, prod_fun_imageE, |
275 |
Pair_inject]; |