1 (* Title: HOL/Product_Type.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Ordered Pairs, the Cartesian product type, the unit type |
|
7 *) |
|
8 |
|
9 (** unit **) |
|
10 |
|
11 Goalw [Unity_def] |
|
12 "u = ()"; |
|
13 by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1); |
|
14 by (rtac (Rep_unit_inverse RS sym) 1); |
|
15 qed "unit_eq"; |
|
16 |
|
17 (*simplification procedure for unit_eq. |
|
18 Cannot use this rule directly -- it loops!*) |
|
19 local |
|
20 val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT)); |
|
21 val unit_meta_eq = standard (mk_meta_eq unit_eq); |
|
22 fun proc _ _ t = |
|
23 if HOLogic.is_unit t then None |
|
24 else Some unit_meta_eq; |
|
25 in |
|
26 val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc; |
|
27 end; |
|
28 |
|
29 Addsimprocs [unit_eq_proc]; |
|
30 |
|
31 Goal "(!!x::unit. PROP P x) == PROP P ()"; |
|
32 by (Simp_tac 1); |
|
33 qed "unit_all_eq1"; |
|
34 |
|
35 Goal "(!!x::unit. PROP P) == PROP P"; |
|
36 by (rtac triv_forall_equality 1); |
|
37 qed "unit_all_eq2"; |
|
38 |
|
39 Goal "P () ==> P x"; |
|
40 by (Simp_tac 1); |
|
41 qed "unit_induct"; |
|
42 |
|
43 (*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u), |
|
44 replacing it by f rather than by %u.f(). *) |
|
45 Goal "(%u::unit. f()) = f"; |
|
46 by (rtac ext 1); |
|
47 by (Simp_tac 1); |
|
48 qed "unit_abs_eta_conv"; |
|
49 Addsimps [unit_abs_eta_conv]; |
|
50 |
|
51 |
|
52 (** prod **) |
|
53 |
|
54 Goalw [Prod_def] "Pair_Rep a b : Prod"; |
|
55 by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]); |
|
56 qed "ProdI"; |
|
57 |
|
58 Goalw [Pair_Rep_def] "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'"; |
|
59 by (dtac (fun_cong RS fun_cong) 1); |
|
60 by (Blast_tac 1); |
|
61 qed "Pair_Rep_inject"; |
|
62 |
|
63 Goal "inj_on Abs_Prod Prod"; |
|
64 by (rtac inj_on_inverseI 1); |
|
65 by (etac Abs_Prod_inverse 1); |
|
66 qed "inj_on_Abs_Prod"; |
|
67 |
|
68 val prems = Goalw [Pair_def] |
|
69 "[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R"; |
|
70 by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1); |
|
71 by (REPEAT (ares_tac (prems@[ProdI]) 1)); |
|
72 qed "Pair_inject"; |
|
73 |
|
74 Goal "((a,b) = (a',b')) = (a=a' & b=b')"; |
|
75 by (blast_tac (claset() addSEs [Pair_inject]) 1); |
|
76 qed "Pair_eq"; |
|
77 AddIffs [Pair_eq]; |
|
78 |
|
79 Goalw [fst_def] "fst (a,b) = a"; |
|
80 by (Blast_tac 1); |
|
81 qed "fst_conv"; |
|
82 Goalw [snd_def] "snd (a,b) = b"; |
|
83 by (Blast_tac 1); |
|
84 qed "snd_conv"; |
|
85 Addsimps [fst_conv, snd_conv]; |
|
86 |
|
87 Goal "fst (x, y) = a ==> x = a"; |
|
88 by (Asm_full_simp_tac 1); |
|
89 qed "fst_eqD"; |
|
90 Goal "snd (x, y) = a ==> y = a"; |
|
91 by (Asm_full_simp_tac 1); |
|
92 qed "snd_eqD"; |
|
93 |
|
94 Goalw [Pair_def] "? x y. p = (x,y)"; |
|
95 by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1); |
|
96 by (EVERY1[etac exE, etac exE, rtac exI, rtac exI, |
|
97 rtac (Rep_Prod_inverse RS sym RS trans), etac arg_cong]); |
|
98 qed "PairE_lemma"; |
|
99 |
|
100 val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q"; |
|
101 by (rtac (PairE_lemma RS exE) 1); |
|
102 by (REPEAT (eresolve_tac [prem,exE] 1)); |
|
103 qed "PairE"; |
|
104 |
|
105 fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac, |
|
106 K prune_params_tac]; |
|
107 |
|
108 (* Do not add as rewrite rule: invalidates some proofs in IMP *) |
|
109 Goal "p = (fst(p),snd(p))"; |
|
110 by (pair_tac "p" 1); |
|
111 by (Asm_simp_tac 1); |
|
112 qed "surjective_pairing"; |
|
113 Addsimps [surjective_pairing RS sym]; |
|
114 |
|
115 Goal "? x y. z = (x, y)"; |
|
116 by (rtac exI 1); |
|
117 by (rtac exI 1); |
|
118 by (rtac surjective_pairing 1); |
|
119 qed "surj_pair"; |
|
120 Addsimps [surj_pair]; |
|
121 |
|
122 |
|
123 bind_thm ("split_paired_all", |
|
124 SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection))); |
|
125 bind_thms ("split_tupled_all", [split_paired_all, unit_all_eq2]); |
|
126 |
|
127 (* |
|
128 Addsimps [split_paired_all] does not work with simplifier |
|
129 because it also affects premises in congrence rules, |
|
130 where is can lead to premises of the form !!a b. ... = ?P(a,b) |
|
131 which cannot be solved by reflexivity. |
|
132 *) |
|
133 |
|
134 (* replace parameters of product type by individual component parameters *) |
|
135 local |
|
136 fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) = |
|
137 can HOLogic.dest_prodT T orelse exists_paired_all t |
|
138 | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u |
|
139 | exists_paired_all (Abs (_, _, t)) = exists_paired_all t |
|
140 | exists_paired_all _ = false; |
|
141 val ss = HOL_basic_ss |
|
142 addsimps [split_paired_all, unit_all_eq2, unit_abs_eta_conv] |
|
143 addsimprocs [unit_eq_proc]; |
|
144 in |
|
145 val split_all_tac = SUBGOAL (fn (t, i) => |
|
146 if exists_paired_all t then full_simp_tac ss i else no_tac); |
|
147 fun split_all th = |
|
148 if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th; |
|
149 end; |
|
150 |
|
151 claset_ref() := claset() |
|
152 addSWrapper ("split_all_tac", fn tac2 => split_all_tac ORELSE' tac2); |
|
153 |
|
154 Goal "(!x. P x) = (!a b. P(a,b))"; |
|
155 by (Fast_tac 1); |
|
156 qed "split_paired_All"; |
|
157 Addsimps [split_paired_All]; |
|
158 (* AddIffs is not a good idea because it makes Blast_tac loop *) |
|
159 |
|
160 bind_thm ("prod_induct", |
|
161 allI RS (allI RS (split_paired_All RS iffD2)) RS spec); |
|
162 |
|
163 Goal "(? x. P x) = (? a b. P(a,b))"; |
|
164 by (Fast_tac 1); |
|
165 qed "split_paired_Ex"; |
|
166 Addsimps [split_paired_Ex]; |
|
167 |
|
168 Goalw [split_def] "split c (a,b) = c a b"; |
|
169 by (Simp_tac 1); |
|
170 qed "split_conv"; |
|
171 Addsimps [split_conv]; |
|
172 (*bind_thm ("split", split_conv); (*for compatibility*)*) |
|
173 |
|
174 (*Subsumes the old split_Pair when f is the identity function*) |
|
175 Goal "split (%x y. f(x,y)) = f"; |
|
176 by (rtac ext 1); |
|
177 by (pair_tac "x" 1); |
|
178 by (Simp_tac 1); |
|
179 qed "split_Pair_apply"; |
|
180 |
|
181 (*Can't be added to simpset: loops!*) |
|
182 Goal "(SOME x. P x) = (SOME (a,b). P(a,b))"; |
|
183 by (simp_tac (simpset() addsimps [split_Pair_apply]) 1); |
|
184 qed "split_paired_Eps"; |
|
185 |
|
186 Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; |
|
187 by (split_all_tac 1); |
|
188 by (Asm_simp_tac 1); |
|
189 qed "Pair_fst_snd_eq"; |
|
190 |
|
191 Goal "fst p = fst q ==> snd p = snd q ==> p = q"; |
|
192 by (asm_simp_tac (simpset() addsimps [Pair_fst_snd_eq]) 1); |
|
193 qed "prod_eqI"; |
|
194 AddXIs [prod_eqI]; |
|
195 |
|
196 (*Prevents simplification of c: much faster*) |
|
197 Goal "p=q ==> split c p = split c q"; |
|
198 by (etac arg_cong 1); |
|
199 qed "split_weak_cong"; |
|
200 |
|
201 Goal "(%(x,y). f(x,y)) = f"; |
|
202 by (rtac ext 1); |
|
203 by (split_all_tac 1); |
|
204 by (rtac split_conv 1); |
|
205 qed "split_eta"; |
|
206 |
|
207 val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g"; |
|
208 by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1); |
|
209 qed "cond_split_eta"; |
|
210 |
|
211 (*simplification procedure for cond_split_eta. |
|
212 using split_eta a rewrite rule is not general enough, and using |
|
213 cond_split_eta directly would render some existing proofs very inefficient. |
|
214 similarly for split_beta. *) |
|
215 local |
|
216 fun Pair_pat k 0 (Bound m) = (m = k) |
|
217 | Pair_pat k i (Const ("Pair", _) $ Bound m $ t) = i > 0 andalso |
|
218 m = k+i andalso Pair_pat k (i-1) t |
|
219 | Pair_pat _ _ _ = false; |
|
220 fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t |
|
221 | no_args k i (t $ u) = no_args k i t andalso no_args k i u |
|
222 | no_args k i (Bound m) = m < k orelse m > k+i |
|
223 | no_args _ _ _ = true; |
|
224 fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then Some (i,t) else None |
|
225 | split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t |
|
226 | split_pat tp i _ = None; |
|
227 fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm [] |
|
228 (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))) |
|
229 (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1])); |
|
230 val sign = sign_of (the_context ()); |
|
231 fun simproc name patstr = Simplifier.mk_simproc name |
|
232 [Thm.read_cterm sign (patstr, HOLogic.termT)]; |
|
233 |
|
234 val beta_patstr = "split f z"; |
|
235 val eta_patstr = "split f"; |
|
236 fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t |
|
237 | beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse |
|
238 (beta_term_pat k i t andalso beta_term_pat k i u) |
|
239 | beta_term_pat k i t = no_args k i t; |
|
240 fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg |
|
241 | eta_term_pat _ _ _ = false; |
|
242 fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t) |
|
243 | subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg |
|
244 else (subst arg k i t $ subst arg k i u) |
|
245 | subst arg k i t = t; |
|
246 fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) = |
|
247 (case split_pat beta_term_pat 1 t of |
|
248 Some (i,f) => Some (metaeq sg s (subst arg 0 i f)) |
|
249 | None => None) |
|
250 | beta_proc _ _ _ = None; |
|
251 fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) = |
|
252 (case split_pat eta_term_pat 1 t of |
|
253 Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end)) |
|
254 | None => None) |
|
255 | eta_proc _ _ _ = None; |
|
256 in |
|
257 val split_beta_proc = simproc "split_beta" beta_patstr beta_proc; |
|
258 val split_eta_proc = simproc "split_eta" eta_patstr eta_proc; |
|
259 end; |
|
260 |
|
261 Addsimprocs [split_beta_proc,split_eta_proc]; |
|
262 |
|
263 Goal "(%(x,y). P x y) z = P (fst z) (snd z)"; |
|
264 by (stac surjective_pairing 1 THEN rtac split_conv 1); |
|
265 qed "split_beta"; |
|
266 |
|
267 (*For use with split_tac and the simplifier*) |
|
268 Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))"; |
|
269 by (stac surjective_pairing 1); |
|
270 by (stac split_conv 1); |
|
271 by (Blast_tac 1); |
|
272 qed "split_split"; |
|
273 |
|
274 (* could be done after split_tac has been speeded up significantly: |
|
275 simpset_ref() := simpset() addsplits [split_split]; |
|
276 precompute the constants involved and don't do anything unless |
|
277 the current goal contains one of those constants |
|
278 *) |
|
279 |
|
280 Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))"; |
|
281 by (stac split_split 1); |
|
282 by (Simp_tac 1); |
|
283 qed "split_split_asm"; |
|
284 |
|
285 (** split used as a logical connective or set former **) |
|
286 |
|
287 (*These rules are for use with blast_tac. |
|
288 Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*) |
|
289 |
|
290 Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p"; |
|
291 by (split_all_tac 1); |
|
292 by (Asm_simp_tac 1); |
|
293 qed "splitI2"; |
|
294 |
|
295 Goal "!!p. [| !!a b. (a,b)=p ==> c a b x |] ==> split c p x"; |
|
296 by (split_all_tac 1); |
|
297 by (Asm_simp_tac 1); |
|
298 qed "splitI2'"; |
|
299 |
|
300 Goal "c a b ==> split c (a,b)"; |
|
301 by (Asm_simp_tac 1); |
|
302 qed "splitI"; |
|
303 |
|
304 val prems = Goalw [split_def] |
|
305 "[| split c p; !!x y. [| p = (x,y); c x y |] ==> Q |] ==> Q"; |
|
306 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
|
307 qed "splitE"; |
|
308 |
|
309 val prems = Goalw [split_def] |
|
310 "[| split c p z; !!x y. [| p = (x,y); c x y z |] ==> Q |] ==> Q"; |
|
311 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
|
312 qed "splitE'"; |
|
313 |
|
314 val major::prems = Goal |
|
315 "[| Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R \ |
|
316 \ |] ==> R"; |
|
317 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
|
318 by (rtac (split_beta RS subst) 1 THEN rtac major 1); |
|
319 qed "splitE2"; |
|
320 |
|
321 Goal "split R (a,b) ==> R a b"; |
|
322 by (etac (split_conv RS iffD1) 1); |
|
323 qed "splitD"; |
|
324 |
|
325 Goal "z: c a b ==> z: split c (a,b)"; |
|
326 by (Asm_simp_tac 1); |
|
327 qed "mem_splitI"; |
|
328 |
|
329 Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p"; |
|
330 by (split_all_tac 1); |
|
331 by (Asm_simp_tac 1); |
|
332 qed "mem_splitI2"; |
|
333 |
|
334 val prems = Goalw [split_def] |
|
335 "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"; |
|
336 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
|
337 qed "mem_splitE"; |
|
338 |
|
339 AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2]; |
|
340 AddSEs [splitE, splitE', mem_splitE]; |
|
341 |
|
342 Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P"; |
|
343 by (rtac ext 1); |
|
344 by (Fast_tac 1); |
|
345 qed "split_eta_SetCompr"; |
|
346 Addsimps [split_eta_SetCompr]; |
|
347 |
|
348 Goal "(%u. ? x y. u = (x, y) & P x y) = split P"; |
|
349 br ext 1; |
|
350 by (Fast_tac 1); |
|
351 qed "split_eta_SetCompr2"; |
|
352 Addsimps [split_eta_SetCompr2]; |
|
353 |
|
354 (* allows simplifications of nested splits in case of independent predicates *) |
|
355 Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"; |
|
356 by (rtac ext 1); |
|
357 by (Blast_tac 1); |
|
358 qed "split_part"; |
|
359 Addsimps [split_part]; |
|
360 |
|
361 Goal "(@(x',y'). x = x' & y = y') = (x,y)"; |
|
362 by (Blast_tac 1); |
|
363 qed "Eps_split_eq"; |
|
364 Addsimps [Eps_split_eq]; |
|
365 (* |
|
366 the following would be slightly more general, |
|
367 but cannot be used as rewrite rule: |
|
368 ### Cannot add premise as rewrite rule because it contains (type) unknowns: |
|
369 ### ?y = .x |
|
370 Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)"; |
|
371 by (rtac some_equality 1); |
|
372 by ( Simp_tac 1); |
|
373 by (split_all_tac 1); |
|
374 by (Asm_full_simp_tac 1); |
|
375 qed "Eps_split_eq"; |
|
376 *) |
|
377 |
|
378 (*** prod_fun -- action of the product functor upon functions ***) |
|
379 |
|
380 Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))"; |
|
381 by (rtac split_conv 1); |
|
382 qed "prod_fun"; |
|
383 Addsimps [prod_fun]; |
|
384 |
|
385 Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))"; |
|
386 by (rtac ext 1); |
|
387 by (pair_tac "x" 1); |
|
388 by (Asm_simp_tac 1); |
|
389 qed "prod_fun_compose"; |
|
390 |
|
391 Goal "prod_fun (%x. x) (%y. y) = (%z. z)"; |
|
392 by (rtac ext 1); |
|
393 by (pair_tac "z" 1); |
|
394 by (Asm_simp_tac 1); |
|
395 qed "prod_fun_ident"; |
|
396 Addsimps [prod_fun_ident]; |
|
397 |
|
398 Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)`r"; |
|
399 by (rtac image_eqI 1); |
|
400 by (rtac (prod_fun RS sym) 1); |
|
401 by (assume_tac 1); |
|
402 qed "prod_fun_imageI"; |
|
403 |
|
404 val major::prems = Goal |
|
405 "[| c: (prod_fun f g)`r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \ |
|
406 \ |] ==> P"; |
|
407 by (rtac (major RS imageE) 1); |
|
408 by (res_inst_tac [("p","x")] PairE 1); |
|
409 by (resolve_tac prems 1); |
|
410 by (Blast_tac 2); |
|
411 by (blast_tac (claset() addIs [prod_fun]) 1); |
|
412 qed "prod_fun_imageE"; |
|
413 |
|
414 AddIs [prod_fun_imageI]; |
|
415 AddSEs [prod_fun_imageE]; |
|
416 |
|
417 |
|
418 (*** Disjoint union of a family of sets - Sigma ***) |
|
419 |
|
420 Goalw [Sigma_def] "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B"; |
|
421 by (REPEAT (ares_tac [singletonI,UN_I] 1)); |
|
422 qed "SigmaI"; |
|
423 |
|
424 AddSIs [SigmaI]; |
|
425 |
|
426 (*The general elimination rule*) |
|
427 val major::prems = Goalw [Sigma_def] |
|
428 "[| c: Sigma A B; \ |
|
429 \ !!x y.[| x:A; y:B(x); c=(x,y) |] ==> P \ |
|
430 \ |] ==> P"; |
|
431 by (cut_facts_tac [major] 1); |
|
432 by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ; |
|
433 qed "SigmaE"; |
|
434 |
|
435 (** Elimination of (a,b):A*B -- introduces no eigenvariables **) |
|
436 |
|
437 Goal "(a,b) : Sigma A B ==> a : A"; |
|
438 by (etac SigmaE 1); |
|
439 by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ; |
|
440 qed "SigmaD1"; |
|
441 |
|
442 Goal "(a,b) : Sigma A B ==> b : B(a)"; |
|
443 by (etac SigmaE 1); |
|
444 by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ; |
|
445 qed "SigmaD2"; |
|
446 |
|
447 val [major,minor]= Goal |
|
448 "[| (a,b) : Sigma A B; \ |
|
449 \ [| a:A; b:B(a) |] ==> P \ |
|
450 \ |] ==> P"; |
|
451 by (rtac minor 1); |
|
452 by (rtac (major RS SigmaD1) 1); |
|
453 by (rtac (major RS SigmaD2) 1) ; |
|
454 qed "SigmaE2"; |
|
455 |
|
456 AddSEs [SigmaE2, SigmaE]; |
|
457 |
|
458 val prems = Goal |
|
459 "[| A<=C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"; |
|
460 by (cut_facts_tac prems 1); |
|
461 by (blast_tac (claset() addIs (prems RL [subsetD])) 1); |
|
462 qed "Sigma_mono"; |
|
463 |
|
464 Goal "Sigma {} B = {}"; |
|
465 by (Blast_tac 1) ; |
|
466 qed "Sigma_empty1"; |
|
467 |
|
468 Goal "A <*> {} = {}"; |
|
469 by (Blast_tac 1) ; |
|
470 qed "Sigma_empty2"; |
|
471 |
|
472 Addsimps [Sigma_empty1,Sigma_empty2]; |
|
473 |
|
474 Goal "UNIV <*> UNIV = UNIV"; |
|
475 by Auto_tac; |
|
476 qed "UNIV_Times_UNIV"; |
|
477 Addsimps [UNIV_Times_UNIV]; |
|
478 |
|
479 Goal "- (UNIV <*> A) = UNIV <*> (-A)"; |
|
480 by Auto_tac; |
|
481 qed "Compl_Times_UNIV1"; |
|
482 |
|
483 Goal "- (A <*> UNIV) = (-A) <*> UNIV"; |
|
484 by Auto_tac; |
|
485 qed "Compl_Times_UNIV2"; |
|
486 |
|
487 Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; |
|
488 |
|
489 Goal "((a,b): Sigma A B) = (a:A & b:B(a))"; |
|
490 by (Blast_tac 1); |
|
491 qed "mem_Sigma_iff"; |
|
492 AddIffs [mem_Sigma_iff]; |
|
493 |
|
494 Goal "x:C ==> (A <*> C <= B <*> C) = (A <= B)"; |
|
495 by (Blast_tac 1); |
|
496 qed "Times_subset_cancel2"; |
|
497 |
|
498 Goal "x:C ==> (A <*> C = B <*> C) = (A = B)"; |
|
499 by (blast_tac (claset() addEs [equalityE]) 1); |
|
500 qed "Times_eq_cancel2"; |
|
501 |
|
502 Goal "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"; |
|
503 by (Fast_tac 1); |
|
504 qed "SetCompr_Sigma_eq"; |
|
505 |
|
506 (*** Complex rules for Sigma ***) |
|
507 |
|
508 Goal "{(a,b). P a & Q b} = Collect P <*> Collect Q"; |
|
509 by (Blast_tac 1); |
|
510 qed "Collect_split"; |
|
511 |
|
512 Addsimps [Collect_split]; |
|
513 |
|
514 (*Suggested by Pierre Chartier*) |
|
515 Goal "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)"; |
|
516 by (Blast_tac 1); |
|
517 qed "UN_Times_distrib"; |
|
518 |
|
519 Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"; |
|
520 by (Fast_tac 1); |
|
521 qed "split_paired_Ball_Sigma"; |
|
522 Addsimps [split_paired_Ball_Sigma]; |
|
523 |
|
524 Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"; |
|
525 by (Fast_tac 1); |
|
526 qed "split_paired_Bex_Sigma"; |
|
527 Addsimps [split_paired_Bex_Sigma]; |
|
528 |
|
529 Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))"; |
|
530 by (Blast_tac 1); |
|
531 qed "Sigma_Un_distrib1"; |
|
532 |
|
533 Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))"; |
|
534 by (Blast_tac 1); |
|
535 qed "Sigma_Un_distrib2"; |
|
536 |
|
537 Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))"; |
|
538 by (Blast_tac 1); |
|
539 qed "Sigma_Int_distrib1"; |
|
540 |
|
541 Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))"; |
|
542 by (Blast_tac 1); |
|
543 qed "Sigma_Int_distrib2"; |
|
544 |
|
545 Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))"; |
|
546 by (Blast_tac 1); |
|
547 qed "Sigma_Diff_distrib1"; |
|
548 |
|
549 Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))"; |
|
550 by (Blast_tac 1); |
|
551 qed "Sigma_Diff_distrib2"; |
|
552 |
|
553 Goal "Sigma (Union X) B = (UN A:X. Sigma A B)"; |
|
554 by (Blast_tac 1); |
|
555 qed "Sigma_Union"; |
|
556 |
|
557 (*Non-dependent versions are needed to avoid the need for higher-order |
|
558 matching, especially when the rules are re-oriented*) |
|
559 Goal "(A Un B) <*> C = (A <*> C) Un (B <*> C)"; |
|
560 by (Blast_tac 1); |
|
561 qed "Times_Un_distrib1"; |
|
562 |
|
563 Goal "(A Int B) <*> C = (A <*> C) Int (B <*> C)"; |
|
564 by (Blast_tac 1); |
|
565 qed "Times_Int_distrib1"; |
|
566 |
|
567 Goal "(A - B) <*> C = (A <*> C) - (B <*> C)"; |
|
568 by (Blast_tac 1); |
|
569 qed "Times_Diff_distrib1"; |
|
570 |
|
571 |
|
572 (*Attempts to remove occurrences of split, and pair-valued parameters*) |
|
573 val remove_split = rewrite_rule [split_conv RS eq_reflection] o split_all; |
|
574 |
|
575 local |
|
576 |
|
577 (*In ap_split S T u, term u expects separate arguments for the factors of S, |
|
578 with result type T. The call creates a new term expecting one argument |
|
579 of type S.*) |
|
580 fun ap_split (Type ("*", [T1, T2])) T3 u = |
|
581 HOLogic.split_const (T1, T2, T3) $ |
|
582 Abs("v", T1, |
|
583 ap_split T2 T3 |
|
584 ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ |
|
585 Bound 0)) |
|
586 | ap_split T T3 u = u; |
|
587 |
|
588 (*Curries any Var of function type in the rule*) |
|
589 fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) = |
|
590 let val T' = HOLogic.prodT_factors T1 ---> T2 |
|
591 val newt = ap_split T1 T2 (Var (v, T')) |
|
592 val cterm = Thm.cterm_of (#sign (rep_thm rl)) |
|
593 in |
|
594 instantiate ([], [(cterm t, cterm newt)]) rl |
|
595 end |
|
596 | split_rule_var' (t, rl) = rl; |
|
597 |
|
598 (*** Complete splitting of partially splitted rules ***) |
|
599 |
|
600 fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U |
|
601 (ap_split T (flat (map HOLogic.prodT_factors Ts) ---> U) |
|
602 (incr_boundvars 1 u) $ Bound 0)) |
|
603 | ap_split' _ _ u = u; |
|
604 |
|
605 fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) = |
|
606 let |
|
607 val cterm = Thm.cterm_of (#sign (rep_thm rl)) |
|
608 val (Us', U') = strip_type T; |
|
609 val Us = take (length ts, Us'); |
|
610 val U = drop (length ts, Us') ---> U'; |
|
611 val T' = flat (map HOLogic.prodT_factors Us) ---> U; |
|
612 fun mk_tuple ((xs, insts), v as Var ((a, _), T)) = |
|
613 let |
|
614 val Ts = HOLogic.prodT_factors T; |
|
615 val ys = variantlist (replicate (length Ts) a, xs); |
|
616 in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T |
|
617 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts) |
|
618 end |
|
619 | mk_tuple (x, _) = x; |
|
620 val newt = ap_split' Us U (Var (v, T')); |
|
621 val cterm = Thm.cterm_of (#sign (rep_thm rl)); |
|
622 val (vs', insts) = foldl mk_tuple ((vs, []), ts); |
|
623 in |
|
624 (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs') |
|
625 end |
|
626 | complete_split_rule_var (_, x) = x; |
|
627 |
|
628 fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t) |
|
629 | collect_vars (vs, t) = (case strip_comb t of |
|
630 (v as Var _, ts) => (v, ts)::vs |
|
631 | (t, ts) => foldl collect_vars (vs, ts)); |
|
632 |
|
633 in |
|
634 |
|
635 val split_rule_var = standard o remove_split o split_rule_var'; |
|
636 |
|
637 (*Curries ALL function variables occurring in a rule's conclusion*) |
|
638 fun split_rule rl = standard (remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl))); |
|
639 |
|
640 fun complete_split_rule rl = |
|
641 standard (remove_split (fst (foldr complete_split_rule_var |
|
642 (collect_vars ([], concl_of rl), |
|
643 (rl, map (fst o fst o dest_Var) (term_vars (#prop (rep_thm rl)))))))); |
|
644 |
|
645 end; |
|