pairScript.sml
1(* ===================================================================== *)
2(* FILE : pairScript.sml *)
3(* DESCRIPTION : The theory of pairs. This is a mix of the original *)
4(* non-definitional theory of pairs from hol88 *)
5(* and John Harrison's definitional theory of pairs from *)
6(* GTT, plus some subsequent simplifications from *)
7(* Konrad Slind. *)
8(* *)
9(* AUTHORS : (c) Mike Gordon, John Harrison, Konrad Slind *)
10(* Jim Grundy *)
11(* University of Cambridge *)
12(* DATE : August 7, 1997 *)
13(* ===================================================================== *)
14
15Theory pair[bare]
16Ancestors
17 relation
18Libs
19 HolKernel Parse boolLib mesonLib metisLib
20 quotientLib simpLib boolSimps BasicProvers
21 computeLib[qualified] OpenTheoryMap[qualified]
22
23fun simp ths = simpLib.asm_simp_tac (srw_ss()) ths (* don't eta-reduce *)
24
25(*---------------------------------------------------------------------------*)
26(* Define the type of pairs and tell the grammar about it. *)
27(*---------------------------------------------------------------------------*)
28
29val pairfn = Term `\a b. (a=x) /\ (b=y)`;
30
31Theorem PAIR_EXISTS[local]:
32 ?p:'a -> 'b -> bool. (\p. ?x y. p = ^pairfn) p
33Proof
34 BETA_TAC
35 THEN Ho_Rewrite.ONCE_REWRITE_TAC [SWAP_EXISTS_THM] THEN Q.EXISTS_TAC `x`
36 THEN Ho_Rewrite.ONCE_REWRITE_TAC [SWAP_EXISTS_THM] THEN Q.EXISTS_TAC `y`
37 THEN EXISTS_TAC pairfn
38 THEN REFL_TAC
39QED
40
41val ABS_REP_prod =
42 let val tydef = new_type_definition("prod", PAIR_EXISTS)
43 in
44 define_new_type_bijections
45 {ABS="ABS_prod", REP="REP_prod",
46 name="ABS_REP_prod", tyax=tydef}
47 end;
48
49val _ = add_infix_type
50 {Prec = 70,
51 ParseName = SOME "#", Name = "prod",
52 Assoc = HOLgrammars.RIGHT};
53val _ = TeX_notation { hol = "#", TeX = ("\\HOLTokenProd{}", 1)}
54local
55 val ns = ["Data","Pair"]
56in
57 val _ = OpenTheoryMap.OpenTheory_tyop_name
58 {tyop={Thy="pair",Tyop="prod"},name=(ns,"*")}
59 fun ot0 x y =
60 OpenTheoryMap.OpenTheory_const_name{const={Thy="pair",Name=x},name=(ns,y)}
61 fun ot x = ot0 x x
62end
63
64Theorem REP_ABS_PAIR[local]:
65 !x y. REP_prod (ABS_prod ^pairfn) = ^pairfn
66Proof
67 REPEAT GEN_TAC
68 THEN REWRITE_TAC [SYM (SPEC pairfn (CONJUNCT2 ABS_REP_prod))]
69 THEN BETA_TAC
70 THEN MAP_EVERY Q.EXISTS_TAC [`x`, `y`]
71 THEN REFL_TAC
72QED
73
74
75(*---------------------------------------------------------------------------*)
76(* Define the constructor for pairs, and install grammar rule for it. *)
77(*---------------------------------------------------------------------------*)
78
79val COMMA_DEF =
80 Q.new_definition
81 ("COMMA_DEF[notuserdef]",
82 `$, x y = ABS_prod ^pairfn`);
83val _ = ot","
84
85val _ = add_rule {term_name = ",", fixity = Infixr 50,
86 pp_elements = [TOK ",", BreakSpace(0,0)],
87 paren_style = ParoundName,
88 block_style = (AroundSameName, (PP.INCONSISTENT, 0))};
89
90
91(*---------------------------------------------------------------------------
92 The constructor for pairs is one-to-one.
93 ---------------------------------------------------------------------------*)
94
95Theorem PAIR_EQ:
96 ((x,y) = (a,b)) <=> (x=a) /\ (y=b)
97Proof
98 EQ_TAC THENL
99 [REWRITE_TAC[COMMA_DEF]
100 THEN DISCH_THEN(MP_TAC o Q.AP_TERM `REP_prod`)
101 THEN REWRITE_TAC [REP_ABS_PAIR]
102 THEN Ho_Rewrite.REWRITE_TAC [FUN_EQ_THM]
103 THEN DISCH_THEN (MP_TAC o Q.SPECL [`x`, `y`])
104 THEN REWRITE_TAC[],
105 STRIP_TAC THEN ASM_REWRITE_TAC[]]
106QED
107
108Theorem CLOSED_PAIR_EQ[simp,compute] =
109 itlist Q.GEN [`x`, `y`, `a`, `b`] PAIR_EQ;
110
111
112(*---------------------------------------------------------------------------
113 Case analysis for pairs.
114 ---------------------------------------------------------------------------*)
115
116Theorem ABS_PAIR_THM:
117 !x. ?q r. x = (q,r)
118Proof
119 GEN_TAC THEN REWRITE_TAC[COMMA_DEF]
120 THEN MP_TAC(Q.SPEC `REP_prod x` (CONJUNCT2 ABS_REP_prod))
121 THEN REWRITE_TAC[CONJUNCT1 ABS_REP_prod] THEN BETA_TAC
122 THEN DISCH_THEN(Q.X_CHOOSE_THEN `a` (Q.X_CHOOSE_THEN `b` MP_TAC))
123 THEN DISCH_THEN(MP_TAC o Q.AP_TERM `ABS_prod`)
124 THEN REWRITE_TAC[CONJUNCT1 ABS_REP_prod]
125 THEN DISCH_THEN SUBST1_TAC
126 THEN MAP_EVERY Q.EXISTS_TAC [`a`, `b`]
127 THEN REFL_TAC
128QED
129
130Theorem pair_CASES = ABS_PAIR_THM
131
132
133(*---------------------------------------------------------------------------*
134 * Surjective pairing and definition of projection functions. *
135 * *
136 * PAIR = |- !x. (FST x,SND x) = x *
137 * FST = |- !x y. FST (x,y) = x *
138 * SND = |- !x y. SND (x,y) = y *
139 *---------------------------------------------------------------------------*)
140
141val PAIR =
142 boolLib.new_specification
143 ("PAIR[simp]", ["FST","SND"],
144 Ho_Rewrite.REWRITE_RULE[SKOLEM_THM] (GSYM ABS_PAIR_THM));
145
146local val th1 = REWRITE_RULE [PAIR_EQ] (SPEC (Term`(x,y):'a#'b`) PAIR)
147 val (th2,th3) = (CONJUNCT1 th1, CONJUNCT2 th1)
148in
149Theorem FST[simp,compute] = itlist Q.GEN [`x`,`y`] th2;
150Theorem SND[simp,compute] = itlist Q.GEN [`x`,`y`] th3;
151end;
152val _ = ot0 "FST" "fst"
153val _ = ot0 "SND" "snd"
154
155Theorem PAIR_FST_SND_EQ:
156 !(p:'a # 'b) q. (p = q) <=> (FST p = FST q) /\ (SND p = SND q)
157Proof
158 REPEAT GEN_TAC THEN
159 X_CHOOSE_THEN ``p1:'a`` (X_CHOOSE_THEN ``p2:'b`` SUBST_ALL_TAC)
160 (SPEC ``p:'a # 'b`` ABS_PAIR_THM) THEN
161 X_CHOOSE_THEN ``q1:'a`` (X_CHOOSE_THEN ``q2:'b`` SUBST_ALL_TAC)
162 (SPEC ``q:'a # 'b`` ABS_PAIR_THM) THEN
163 REWRITE_TAC [PAIR_EQ, FST, SND]
164QED
165
166val SWAP_def = new_definition ("SWAP_def", ``SWAP a = (SND a, FST a)``)
167
168(* Theorem the SWAP inverts itself *)
169Theorem SWAP_SWAP[simp]:
170 !x. SWAP (SWAP x) = x
171Proof
172 simp[SWAP_def]
173QED
174
175Theorem SWAP_o_SWAP[simp]:
176 SWAP o SWAP = I /\
177 SWAP o SWAP o f = f
178Proof
179 simp[FUN_EQ_THM]
180QED
181
182Theorem FST_SWAP[simp]:
183 !x. (FST (SWAP x)) = SND x
184Proof
185 simp[SWAP_def]
186QED
187
188Theorem SND_SWAP[simp]:
189 !x. (SND (SWAP x)) = FST x
190Proof
191 simp[SWAP_def]
192QED
193
194Theorem FST_o_SWAP[simp]:
195 FST o SWAP = SND /\
196 FST o SWAP o f = SND o f
197Proof
198 simp[FUN_EQ_THM]
199QED
200
201Theorem SND_o_SWAP[simp]:
202 SND o SWAP = FST /\
203 SND o SWAP o f = FST o f
204Proof
205 simp[FUN_EQ_THM]
206QED
207
208(*---------------------------------------------------------------------------*)
209(* CURRY and UNCURRY. UNCURRY is needed for terms of the form `\(x,y).t` *)
210(*---------------------------------------------------------------------------*)
211
212val CURRY_DEF = new_definition(
213 "CURRY_DEF[simp]",
214 “CURRY f (x:'a) (y:'b) :'c = f (x,y)”
215);
216
217val UNCURRY = Q.new_definition
218 ("UNCURRY",
219 `UNCURRY f (v:'a#'b) = f (FST v) (SND v)`);
220val _ = ot0 "UNCURRY" "uncurry"
221
222Theorem UNCURRY_VAR = UNCURRY; (* compatibility *)
223
224Theorem ELIM_UNCURRY:
225 !f:'a -> 'b -> 'c. UNCURRY f = \x. f (FST x) (SND x)
226Proof
227 GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN
228 REWRITE_TAC [UNCURRY] THEN CONV_TAC (RAND_CONV BETA_CONV) THEN
229 REFL_TAC
230QED
231
232Theorem UNCURRY_DEF[simp,compute]:
233 !f x y. UNCURRY f (x,y) :'c = f x y
234Proof
235 REWRITE_TAC [UNCURRY,FST,SND]
236QED
237
238Theorem UNCURRY_CONST[simp]:
239 (UNCURRY (\x1 x2. y) x) = y
240Proof
241 REWRITE_TAC[UNCURRY]
242QED
243
244Theorem UNCURRY_SWAP[simp]:
245 UNCURRY f (SWAP x) = UNCURRY (flip f) x
246Proof
247 simp[UNCURRY]
248QED
249
250Theorem IN_UNCURRY_R[simp]:
251 (x,y) IN UNCURRY R <=> R x y
252Proof
253 simp[IN_DEF]
254QED
255
256(* ------------------------------------------------------------------------- *)
257(* CURRY_UNCURRY_THM = |- !f. CURRY(UNCURRY f) = f *)
258(* ------------------------------------------------------------------------- *)
259
260val CURRY_UNCURRY_THM =
261 let val th1 = prove
262 (“CURRY (UNCURRY (f:'a->'b->'c)) x y = f x y”,
263 REWRITE_TAC [UNCURRY_DEF, CURRY_DEF])
264 val th2 = GEN “y:'b” th1
265 val th3 = EXT th2
266 val th4 = GEN “x:'a” th3
267 val th4 = EXT th4
268 in
269 GEN “f:'a->'b->'c” th4
270 end;
271Theorem CURRY_UNCURRY_THM[simp] = CURRY_UNCURRY_THM
272
273(* ------------------------------------------------------------------------- *)
274(* UNCURRY_CURRY_THM = |- !f. UNCURRY(CURRY f) = f *)
275(* ------------------------------------------------------------------------- *)
276
277val UNCURRY_CURRY_THM =
278 let val th1 = prove
279 (“UNCURRY (CURRY (f:('a#'b)->'c)) (x,y) = f(x,y)”,
280 REWRITE_TAC [CURRY_DEF, UNCURRY_DEF])
281 val th2 = Q.INST [`x:'a` |-> `FST (z:'a#'b)`,
282 `y:'b` |-> `SND (z:'a#'b)`] th1
283 val th3 = CONV_RULE (RAND_CONV
284 (RAND_CONV (K (ISPEC “z:'a#'b” PAIR)))) th2
285 val th4 = CONV_RULE(RATOR_CONV (RAND_CONV
286 (RAND_CONV (K (ISPEC “z:'a#'b” PAIR)))))th3
287 val th5 = GEN “z:'a#'b” th4
288 val th6 = EXT th5
289 in
290 GEN “f:('a#'b)->'c” th6
291 end;
292
293Theorem UNCURRY_CURRY_THM[simp] = UNCURRY_CURRY_THM;
294
295(* ------------------------------------------------------------------------- *)
296(* CURRY_ONE_ONE_THM = |- (CURRY f = CURRY g) = (f = g) *)
297(* ------------------------------------------------------------------------- *)
298
299val CURRY_ONE_ONE_THM =
300 let val th1 = ASSUME “(f:('a#'b)->'c) = g”
301 val th2 = AP_TERM “CURRY:(('a#'b)->'c)->('a->'b->'c)” th1
302 val th3 = DISCH_ALL th2
303 val thA = ASSUME “(CURRY (f:('a#'b)->'c)) = (CURRY g)”
304 val thB = AP_TERM “UNCURRY:('a->'b->'c)->(('a#'b)->'c)” thA
305 val thC = PURE_REWRITE_RULE [UNCURRY_CURRY_THM] thB
306 val thD = DISCH_ALL thC
307 in
308 IMP_ANTISYM_RULE thD th3
309 end;
310
311Theorem CURRY_ONE_ONE_THM[simp] = CURRY_ONE_ONE_THM;
312
313(* ------------------------------------------------------------------------- *)
314(* UNCURRY_ONE_ONE_THM = |- (UNCURRY f = UNCURRY g) = (f = g) *)
315(* ------------------------------------------------------------------------- *)
316
317val UNCURRY_ONE_ONE_THM =
318 let val th1 = ASSUME “(f:'a->'b->'c) = g”
319 val th2 = AP_TERM “UNCURRY:('a->'b->'c)->(('a#'b)->'c)” th1
320 val th3 = DISCH_ALL th2
321 val thA = ASSUME “(UNCURRY (f:'a->'b->'c)) = (UNCURRY g)”
322 val thB = AP_TERM “CURRY:(('a#'b)->'c)->('a->'b->'c)” thA
323 val thC = PURE_REWRITE_RULE [CURRY_UNCURRY_THM] thB
324 val thD = DISCH_ALL thC
325 in
326 IMP_ANTISYM_RULE thD th3
327 end;
328
329Theorem UNCURRY_ONE_ONE_THM[simp] = UNCURRY_ONE_ONE_THM;
330
331(* ----------------------------------------------------------------------
332 UNCURRY_EQ = |- UNCURRY f x = y <=> ?a b. x = (a,b) /\ f a b = y
333
334 (given that UNCURRY = flip pair_CASE, this is the "case equality"
335 theorem recast)
336 ---------------------------------------------------------------------- *)
337
338Theorem UNCURRY_EQ:
339 UNCURRY f x = y <=> ?a b. x = (a,b) /\ f a b = y
340Proof
341 Q.SPEC_THEN ‘x’ STRIP_ASSUME_TAC pair_CASES >>
342 ASM_SIMP_TAC bool_ss [UNCURRY_DEF, PAIR_EQ]
343QED
344
345(* ------------------------------------------------------------------------- *)
346(* pair_Axiom = |- !f. ?fn. !x y. fn (x,y) = f x y *)
347(* ------------------------------------------------------------------------- *)
348
349Theorem pair_Axiom:
350 !f:'a->'b->'c. ?fn. !x y. fn (x,y) = f x y
351Proof
352 GEN_TAC THEN Q.EXISTS_TAC`UNCURRY f` THEN REWRITE_TAC[UNCURRY_DEF]
353QED
354
355(* -------------------------------------------------------------------------*)
356(* UNCURRY_CONG = *)
357(* |- !f' f M' M. *)
358(* (M = M') /\ *)
359(* (!x y. (M' = (x,y)) ==> (f x y = f' x y)) *)
360(* ==> *)
361(* (UNCURRY f M = UNCURRY f' M') *)
362(* -------------------------------------------------------------------------*)
363
364Theorem UNCURRY_CONG:
365 !f' f M' M.
366 (M = M') /\ (!x y. (M' = (x,y)) ==> (f x y = f' x y)) ==>
367 (UNCURRY f M = UNCURRY f' M')
368Proof
369 REPEAT STRIP_TAC THEN
370 Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC pair_CASES THEN
371 Q.SPEC_THEN `M'` FULL_STRUCT_CASES_TAC pair_CASES THEN
372 FULL_SIMP_TAC bool_ss [PAIR_EQ, UNCURRY_DEF]
373QED
374
375(*---------------------------------------------------------------------------
376 LAMBDA_PROD = |- !P. (\p. P p) = (\(p1,p2). P (p1,p2))
377 ---------------------------------------------------------------------------*)
378
379Theorem LAMBDA_PROD:
380 !P:'a#'b->'c. (\p. P p) = \(p1,p2). P(p1,p2)
381Proof
382 GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC
383 THEN STRUCT_CASES_TAC (Q.SPEC `p` ABS_PAIR_THM)
384 THEN REWRITE_TAC [UNCURRY,FST,SND]
385 THEN BETA_TAC THEN REFL_TAC
386QED
387
388(*---------------------------------------------------------------------------
389 EXISTS_PROD = |- (?p. P p) = ?p_1 p_2. P (p_1,p_2)
390 ---------------------------------------------------------------------------*)
391
392Theorem EXISTS_PROD:
393 (?p. P p) = ?p_1 p_2. P (p_1,p_2)
394Proof
395 EQ_TAC THEN STRIP_TAC
396 THENL [MAP_EVERY Q.EXISTS_TAC [`FST p`, `SND p`], Q.EXISTS_TAC `p_1, p_2`]
397 THEN ASM_REWRITE_TAC[PAIR]
398QED
399
400(*---------------------------------------------------------------------------
401 FORALL_PROD = |- (!p. P p) = !p_1 p_2. P (p_1,p_2)
402 ---------------------------------------------------------------------------*)
403
404Theorem FORALL_PROD:
405 (!p. P p) = !p_1 p_2. P (p_1,p_2)
406Proof
407 EQ_TAC THENL
408 [DISCH_THEN(fn th => REPEAT GEN_TAC THEN ASSUME_TAC (Q.SPEC `p_1, p_2` th)),
409 REPEAT STRIP_TAC
410 THEN REPEAT_TCL CHOOSE_THEN SUBST_ALL_TAC (Q.SPEC `p` ABS_PAIR_THM)
411 ]
412 THEN ASM_REWRITE_TAC[]
413QED
414
415
416Theorem pair_induction = #2(EQ_IMP_RULE FORALL_PROD) |> GEN_ALL
417
418(* ----------------------------------------------------------------------
419 PROD_ALL
420 ---------------------------------------------------------------------- *)
421
422val PROD_ALL_def = new_definition(
423 "PROD_ALL_def",
424 ``PROD_ALL (P:'a -> bool) (Q : 'b -> bool) p <=> P (FST p) /\ Q (SND p)``);
425
426Theorem PROD_ALL_THM[simp,compute]:
427 PROD_ALL P Q (x:'a,y:'b) <=> P x /\ Q y
428Proof REWRITE_TAC [PROD_ALL_def, FST, SND]
429QED
430
431Theorem PROD_ALL_MONO:
432 (!x:'a. P x ==> P' x) /\ (!y:'b. Q y ==> Q' y) ==>
433 PROD_ALL P Q p ==> PROD_ALL P' Q' p
434Proof
435 Q.SPEC_THEN `p` STRUCT_CASES_TAC ABS_PAIR_THM THEN
436 REWRITE_TAC [PROD_ALL_THM] THEN REPEAT STRIP_TAC THEN RES_TAC
437QED
438val _ = IndDefLib.export_mono "PROD_ALL_MONO"
439
440Theorem PROD_ALL_CONG:
441 !p p' P P' Q Q'.
442 (p = p') /\ (!x:'a y:'b. (p' = (x,y)) ==> (P x <=> P' x)) /\
443 (!x:'a y:'b. (p' = (x,y)) ==> (Q y <=> Q' y)) ==>
444 (PROD_ALL P Q p <=> PROD_ALL P' Q' p')
445Proof
446 SIMP_TAC (BasicProvers.srw_ss()) [FORALL_PROD, PAIR_EQ]
447QED
448
449(* ------------------------------------------------------------------------- *)
450(* ELIM_PEXISTS = |- !P. (?p. P (FST p) (SND p)) = ?p1 p2. P p1 p2 *)
451(* ------------------------------------------------------------------------- *)
452
453Theorem ELIM_PEXISTS:
454 (?p. P (FST p) (SND p)) = ?p1 p2. P p1 p2
455Proof
456 EQ_TAC THEN STRIP_TAC THENL
457 [MAP_EVERY Q.EXISTS_TAC [`FST p`, `SND p`] THEN ASM_REWRITE_TAC [],
458 Q.EXISTS_TAC `(p1,p2)` THEN ASM_REWRITE_TAC [FST,SND]]
459QED
460
461(* ------------------------------------------------------------------------- *)
462(* ELIM_PFORALL = |- !P. (!p. P (FST p) (SND p)) = !p1 p2. P p1 p2 *)
463(* ------------------------------------------------------------------------- *)
464
465Theorem ELIM_PFORALL:
466 (!p. P (FST p) (SND p)) = !p1 p2. P p1 p2
467Proof
468 EQ_TAC THEN REPEAT STRIP_TAC THENL
469 [POP_ASSUM (MP_TAC o Q.SPEC `(p1,p2)`) THEN REWRITE_TAC [FST,SND],
470 ASM_REWRITE_TAC []]
471QED
472
473(* ------------------------------------------------------------------------- *)
474(* PFORALL_THM = |- !P. (!x y. P x y) = (!(x,y). P x y) *)
475(* ------------------------------------------------------------------------- *)
476
477Theorem PFORALL_THM:
478 !P:'a -> 'b -> bool. (!x y. P x y) = !(x,y). P x y
479Proof
480 REWRITE_TAC [ELIM_UNCURRY] THEN BETA_TAC THEN
481 MATCH_ACCEPT_TAC (GSYM ELIM_PFORALL)
482QED
483
484(* ------------------------------------------------------------------------- *)
485(* PEXISTS_THM = |- !P. (?x y. P x y) = (?(x,y). P x y) *)
486(* ------------------------------------------------------------------------- *)
487
488Theorem PEXISTS_THM:
489 !P:'a -> 'b -> bool. (?x y. P x y) = ?(x,y). P x y
490Proof
491 REWRITE_TAC [ELIM_UNCURRY] THEN BETA_TAC THEN
492 MATCH_ACCEPT_TAC (GSYM ELIM_PEXISTS)
493QED
494
495
496(* ------------------------------------------------------------------------- *)
497(* Rewrite versions of ELIM_PEXISTS and ELIM_PFORALL *)
498(* ------------------------------------------------------------------------- *)
499
500Theorem ELIM_PEXISTS_EVAL:
501 $? (UNCURRY (\x. P x)) = ?x. $? (P x)
502Proof
503 Q.SUBGOAL_THEN `!x. P x = \y. P x y` (fn th => ONCE_REWRITE_TAC [th]) THEN
504 REWRITE_TAC [ETA_THM, PEXISTS_THM]
505QED
506
507Theorem ELIM_PFORALL_EVAL:
508 $! (UNCURRY (\x. P x)) = !x. $! (P x)
509Proof
510 Q.SUBGOAL_THEN `!x. P x = \y. P x y` (fn th => ONCE_REWRITE_TAC [th]) THEN
511 REWRITE_TAC [ETA_THM, PFORALL_THM]
512QED
513
514(*---------------------------------------------------------------------------
515 Map for pairs
516 ---------------------------------------------------------------------------*)
517
518val PAIR_MAP = Q.new_infixr_definition
519 ("PAIR_MAP",
520 `$## (f:'a->'c) (g:'b->'d) p = (f (FST p), g (SND p))`, 490);
521
522Theorem PAIR_MAP_THM[simp,compute]:
523 !f g x y. (f##g) (x,y) = (f x, g y)
524Proof REWRITE_TAC [PAIR_MAP,FST,SND]
525QED
526
527Theorem pair_map_eq[simp]:
528 (f ## g) p = (w,v) <=> (?x y. (p = (x,y)) /\ (w = f x) /\ (v = g y))
529Proof
530 Q.SPEC_THEN ‘p’ STRIP_ASSUME_TAC pair_CASES >>
531 simp [] >> EQ_TAC >> simp[]
532QED
533
534Theorem FST_PAIR_MAP[simp]:
535 !p f g. FST ((f ## g) p) = f (FST p)
536Proof REWRITE_TAC [PAIR_MAP, FST]
537QED
538
539Theorem SND_PAIR_MAP[simp]:
540 !p f g. SND ((f ## g) p) = g (SND p)
541Proof REWRITE_TAC [PAIR_MAP, SND]
542QED
543
544Theorem FST_o_PAIR_MAP[simp]:
545 FST o (g ## f) = g o FST /\
546 FST o (g ## f) o f' = g o FST o f'
547Proof simp [FUN_EQ_THM]
548QED
549
550Theorem SND_o_PAIR_MAP[simp]:
551 SND o (g ## f) = (f o SND) /\
552 SND o (g ## f) o f' = f o SND o f'
553Proof simp [FUN_EQ_THM]
554QED
555
556Theorem PAIR_MAP_I[simp,quotient_simp]:
557 (I ## I) = (I : 'a # 'b -> 'a # 'b)
558Proof
559 simp[FUN_EQ_THM, FORALL_PROD]
560QED
561
562
563(*---------------------------------------------------------------------------
564 Distribution laws for paired lets. Only will work for the
565 exact form given. See also boolTheory.
566 ---------------------------------------------------------------------------*)
567
568Theorem LET2_RAND:
569 !(P:'c->'d) (M:'a#'b) N.
570 P (let (x,y) = M in N x y) = (let (x,y) = M in P (N x y))
571Proof
572REWRITE_TAC[boolTheory.LET_DEF] THEN REPEAT GEN_TAC THEN BETA_TAC
573 THEN REPEAT_TCL CHOOSE_THEN SUBST_ALL_TAC
574 (SPEC (Term `M:'a#'b`) ABS_PAIR_THM)
575 THEN REWRITE_TAC[UNCURRY_DEF] THEN BETA_TAC THEN REFL_TAC
576QED
577
578Theorem LET2_RATOR:
579 !(M:'a1#'a2) (N:'a1->'a2->'b->'c) (b:'b).
580 (let (x,y) = M in N x y) b = let (x,y) = M in N x y b
581Proof
582REWRITE_TAC [boolTheory.LET_DEF] THEN BETA_TAC
583 THEN REWRITE_TAC [UNCURRY_VAR] THEN BETA_TAC
584 THEN REWRITE_TAC[]
585QED
586
587Theorem UNCURRY_RAND:
588 !f'. f' (UNCURRY f x) = UNCURRY ((o) f' o f) x
589Proof
590 REWRITE_TAC [UNCURRY_VAR,combinTheory.o_DEF] THEN BETA_TAC
591 THEN REWRITE_TAC[]
592QED
593
594Theorem UNCURRY_RATOR:
595 !M . UNCURRY M f0 x = UNCURRY (flip (flip o M) x) f0
596Proof
597 REWRITE_TAC [UNCURRY_VAR,combinTheory.C_DEF,combinTheory.o_DEF]
598 THEN BETA_TAC THEN BETA_TAC
599 THEN REWRITE_TAC[]
600QED
601
602Theorem o_UNCURRY_R:
603 f o UNCURRY g = UNCURRY ((o) f o g)
604Proof
605 SRW_TAC [][FUN_EQ_THM, UNCURRY]
606QED
607
608Theorem C_UNCURRY_L:
609 combin$C (UNCURRY f) x = UNCURRY (combin$C (combin$C o f) x)
610Proof
611 SRW_TAC [][FUN_EQ_THM, UNCURRY]
612QED
613
614Theorem S_UNCURRY_R:
615 S f (UNCURRY g) = UNCURRY (S (S o ((o) f) o (,)) g)
616Proof
617 SRW_TAC [][FUN_EQ_THM, UNCURRY, PAIR]
618QED
619
620Theorem UNCURRY'[local]:
621 UNCURRY f = \p. f (FST p) (SND p)
622Proof
623 SRW_TAC [][FUN_EQ_THM, UNCURRY]
624QED
625
626Theorem FORALL_UNCURRY:
627 (!) (UNCURRY f) = (!) ((!) o f)
628Proof
629 SRW_TAC [][UNCURRY', combinTheory.o_DEF] THEN
630 Q.SUBGOAL_THEN `!x. f x = \y. f x y` (fn th => ONCE_REWRITE_TAC [th]) THENL [
631 REWRITE_TAC [FUN_EQ_THM] THEN BETA_TAC THEN REWRITE_TAC [],
632 ALL_TAC
633 ] THEN
634 SRW_TAC [][FORALL_PROD, FST, SND]
635QED
636
637(* --------------------------------------------------------------------- *)
638(* A nice theorem from Tom Melham, lifted from examples/lambda/ncScript *)
639(* States ability to express a function: *)
640(* *)
641(* h : A -> B x C *)
642(* *)
643(* as the combination h = <f,g> of two component functions *)
644(* *)
645(* f : A -> B and g : A -> C *)
646(* *)
647(* --------------------------------------------------------------------- *)
648
649Theorem PAIR_FUN_THM:
650 !P. (?!f:'a->('b#'c). P f) =
651 (?!p:('a->'b)#('a->'c). P(\a.(FST p a, SND p a)))
652Proof
653RW_TAC bool_ss [EXISTS_UNIQUE_THM]
654 THEN EQ_TAC THEN RW_TAC bool_ss []
655 THENL
656 [Q.EXISTS_TAC `FST o f, SND o f`
657 THEN RW_TAC bool_ss [FST,SND,combinTheory.o_THM,PAIR,ETA_THM],
658 STRIP_ASSUME_TAC (Q.ISPEC `p:('a -> 'b) # ('a -> 'c)` ABS_PAIR_THM) THEN
659 STRIP_ASSUME_TAC (Q.ISPEC `p':('a -> 'b) # ('a -> 'c)` ABS_PAIR_THM)
660 THEN RW_TAC bool_ss []
661 THEN RULE_ASSUM_TAC (REWRITE_RULE [FST,SND])
662 THEN ``(\a:'a. (q a:'b,r a:'c)) = (\a:'a. (q' a:'b,r' a:'c))`` via RES_TAC
663 THEN simpLib.FULL_SIMP_TAC bool_ss [FUN_EQ_THM,PAIR_EQ],
664 PROVE_TAC[],
665 Q.PAT_ASSUM `$! M`
666 (MP_TAC o Q.SPECL [`(FST o f, SND o f)`, `(FST o y, SND o y)`])
667 THEN RW_TAC bool_ss [FST,SND,combinTheory.o_THM,
668 PAIR,PAIR_EQ,FUN_EQ_THM,ETA_THM]
669 THEN PROVE_TAC [PAIR_EQ,PAIR]]
670QED
671
672
673(*---------------------------------------------------------------------------
674 TFL support.
675 ---------------------------------------------------------------------------*)
676
677val pair_CASE_def =
678 new_definition("pair_CASE_def",
679 “pair_CASE (p:('a#'b)) f = f (FST p) (SND p)”)
680val _ = ot0 "pair_case" "case"
681
682Theorem pair_case_thm =
683 pair_CASE_def |> Q.SPEC ‘(x,y)’ |> REWRITE_RULE [FST, SND] |> SPEC_ALL
684
685(* and, to be consistent with what would be generated if we could use
686 Datatype to generate the pair type: *)
687Theorem pair_case_def = pair_case_thm
688Overload case = “pair_CASE”
689
690
691Theorem pair_CASE_UNCURRY:
692 pair_CASE = flip UNCURRY
693Proof
694 SIMP_TAC bool_ss [FUN_EQ_THM, pair_CASE_def, combinTheory.C_DEF, UNCURRY]
695QED
696
697Theorem UNCURRY_pair_CASE:
698 UNCURRY = flip pair_CASE
699Proof
700 SIMP_TAC bool_ss [FUN_EQ_THM, pair_CASE_def, combinTheory.C_DEF, UNCURRY]
701QED
702
703
704Theorem pair_case_cong =
705 Prim_rec.case_cong_thm pair_CASES pair_case_thm;
706val pair_rws = [PAIR, FST, SND];
707
708Theorem pair_case_eq:
709 (pair_CASE p f = v) <=> ?x y. (p = (x,y)) /\ (f x y = v)
710Proof
711 SIMP_TAC bool_ss [pair_CASE_UNCURRY, UNCURRY_EQ, combinTheory.C_DEF]
712QED
713
714Theorem pair_CASE_SWAP[simp]:
715 pair_CASE (SWAP v) f = pair_CASE v (flip f)
716Proof
717 simp[pair_CASE_UNCURRY]
718QED
719
720Theorem pair_case_ho_elim:
721 !f'. f'(pair_CASE p f) = (?x y. p = (x,y) /\ f'(f x y))
722Proof
723 strip_tac THEN
724 Q.ISPEC_THEN ‘p’ STRUCT_CASES_TAC pair_CASES THEN
725 SRW_TAC[][pair_CASE_def, FST, SND, PAIR_EQ]
726QED
727
728val _ = TypeBase.export [
729 TypeBasePure.mk_datatype_info_no_simpls {
730 ax=TypeBasePure.ORIG pair_Axiom,
731 case_def=pair_case_thm,
732 case_cong=pair_case_cong,
733 case_eq = pair_case_eq,
734 case_elim = pair_case_ho_elim,
735 induction=TypeBasePure.ORIG pair_induction,
736 nchotomy=ABS_PAIR_THM,
737 size=NONE,
738 encode=NONE,
739 fields=[],
740 accessors=[],
741 updates=[],
742 destructors=[FST,SND],
743 recognizers=[],
744 lift=SOME(mk_var("pairSyntax.lift_prod",
745 “:'type -> ('a -> 'term) -> ('b -> 'term) -> 'a # 'b ->
746 'term”)),
747 one_one=SOME CLOSED_PAIR_EQ,
748 distinct=NONE
749 }
750 ];
751
752(*---------------------------------------------------------------------------
753 Generate some ML that gets evaluated at theory load time.
754
755 The TFL definition package uses "pair_case" as a case construct,
756 rather than UNCURRY. This (apparently) solves a deeply buried
757 problem in termination condition extraction involving paired
758 beta-reduction.
759
760 ---------------------------------------------------------------------------*)
761
762Theorem datatype_pair:
763 DATATYPE (pair ((,) : 'a -> 'b -> 'a # 'b))
764Proof
765 REWRITE_TAC [DATATYPE_TAG_THM]
766QED
767
768
769(*---------------------------------------------------------------------------
770 Wellfoundedness and pairs.
771 ---------------------------------------------------------------------------*)
772
773
774(*---------------------------------------------------------------------------
775 * The lexicographic combination of two wellfounded orderings is wellfounded.
776 * The minimal element of this relation is found by
777 *
778 * 1. Finding the set of first elements of the pairs in B
779 * 2. That set is non-empty, so it has an R-minimal element, call it min
780 * 3. Find the set of second elements of those pairs in B whose first
781 * element is min.
782 * 4. This set is non-empty, so it has a Q-minimal element, call it min'.
783 * 5. A minimal element is (min,min').
784 *---------------------------------------------------------------------------*)
785
786val LEX_DEF =
787Q.new_infixr_definition
788("LEX_DEF",
789 `$LEX (R1:'a->'a->bool) (R2:'b->'b->bool)
790 =
791 \(s,t) (u,v). R1 s u \/ (s=u) /\ R2 t v`, 490);
792
793Theorem LEX_DEF_THM:
794 (R1 LEX R2) (a,b) (c,d) <=> R1 a c \/ (a = c) /\ R2 b d
795Proof
796 REWRITE_TAC [LEX_DEF,UNCURRY_DEF] THEN BETA_TAC THEN
797 REWRITE_TAC [UNCURRY_DEF] THEN BETA_TAC THEN REFL_TAC
798QED
799
800Theorem LEX_MONO:
801 (!x y. R1 x y ==> R2 x y) /\
802 (!x y. R3 x y ==> R4 x y)
803 ==>
804 (R1 LEX R3) x y ==> (R2 LEX R4) x y
805Proof
806 STRIP_TAC THEN
807 Q.SPEC_THEN`x`FULL_STRUCT_CASES_TAC pair_CASES THEN
808 Q.SPEC_THEN`y`FULL_STRUCT_CASES_TAC pair_CASES THEN
809 SRW_TAC[][LEX_DEF_THM] THEN
810 PROVE_TAC[]
811QED
812val () = IndDefLib.export_mono"LEX_MONO";
813
814Theorem WF_LEX:
815 !(R:'a->'a->bool) (Q:'b->'b->bool). WF R /\ WF Q ==> WF (R LEX Q)
816Proof
817REWRITE_TAC [LEX_DEF, relationTheory.WF_DEF]
818 THEN CONV_TAC (DEPTH_CONV LEFT_IMP_EXISTS_CONV)
819 THEN REPEAT STRIP_TAC
820 THEN Q.SUBGOAL_THEN `?w1. (\v. ?y. B (v,y)) w1` STRIP_ASSUME_TAC THENL
821 [BETA_TAC THEN MAP_EVERY Q.EXISTS_TAC [`FST w`, `SND w`]
822 THEN ASM_REWRITE_TAC pair_rws,
823 Q.SUBGOAL_THEN
824 `?min. (\v. ?y. B (v,y)) min
825 /\ !b. R b min ==>
826 ~(\v. ?y. B (v,y)) b` STRIP_ASSUME_TAC THENL
827 [RES_TAC THEN ASM_MESON_TAC[],
828 Q.SUBGOAL_THEN
829 `?w2:'b. (\z. B (min:'a,z)) w2` STRIP_ASSUME_TAC THENL
830 [BETA_TAC THEN RULE_ASSUM_TAC BETA_RULE THEN ASM_REWRITE_TAC[],
831 Q.SUBGOAL_THEN
832 `?min':'b. (\z. B (min,z)) min'
833 /\ !b. Q b min' ==>
834 ~((\z. B (min,z)) b)` STRIP_ASSUME_TAC THENL
835 [RES_TAC THEN ASM_MESON_TAC[],
836 RULE_ASSUM_TAC BETA_RULE
837 THEN EXISTS_TAC (Term`(min:'a, (min':'b))`)
838 THEN ASM_REWRITE_TAC[]
839 THEN GEN_TAC THEN SUBST_TAC [GSYM(Q.SPEC`b:'a#'b` PAIR)]
840 THEN REWRITE_TAC [UNCURRY_DEF] THEN BETA_TAC
841 THEN REWRITE_TAC [UNCURRY_DEF] THEN BETA_TAC
842 THEN ASM_MESON_TAC pair_rws]]]]
843QED
844
845(*---------------------------------------------------------------------------
846 * The relational product of two wellfounded relations is wellfounded. This
847 * is a consequence of WF_LEX.
848 *---------------------------------------------------------------------------*)
849
850val RPROD_DEF =
851Q.new_definition
852("RPROD_DEF",
853 `RPROD (R1:'a->'b->bool)
854 (R2:'c->'d->bool) = \(s,t) (u,v). R1 s u /\ R2 t v`);
855
856
857Theorem WF_RPROD:
858 !(R:'a->'a->bool) (Q:'b->'b->bool). WF R /\ WF Q ==> WF(RPROD R Q)
859Proof
860REPEAT STRIP_TAC THEN MATCH_MP_TAC relationTheory.WF_SUBSET
861 THEN Q.EXISTS_TAC`R LEX Q`
862 THEN CONJ_TAC
863 THENL [MATCH_MP_TAC WF_LEX THEN ASM_REWRITE_TAC[],
864 REWRITE_TAC[LEX_DEF,RPROD_DEF]
865 THEN GEN_TAC THEN SUBST_TAC [GSYM(Q.SPEC`x:'a#'b` PAIR)]
866 THEN GEN_TAC THEN SUBST_TAC [GSYM(Q.SPEC`y:'a#'b` PAIR)]
867 THEN REWRITE_TAC [UNCURRY_DEF] THEN BETA_TAC
868 THEN REWRITE_TAC [UNCURRY_DEF] THEN BETA_TAC
869 THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]]
870QED
871
872(* more relational properties of LEX *)
873Theorem total_LEX[simp]:
874 total R1 /\ total R2 ==> total (R1 LEX R2)
875Proof
876 ASM_SIMP_TAC (srw_ss()) [total_def, FORALL_PROD, LEX_DEF, UNCURRY_DEF] THEN
877 METIS_TAC[]
878QED
879
880Theorem transitive_LEX[simp]:
881 transitive R1 /\ transitive R2 ==> transitive (R1 LEX R2)
882Proof
883 SIMP_TAC (srw_ss()) [transitive_def, FORALL_PROD, LEX_DEF, UNCURRY_DEF] THEN
884 METIS_TAC[]
885QED
886
887Theorem reflexive_LEX[simp]:
888 reflexive (R1 LEX R2) <=> reflexive R1 \/ reflexive R2
889Proof
890 SIMP_TAC (srw_ss()) [reflexive_def, LEX_DEF, FORALL_PROD, UNCURRY_DEF] THEN
891 METIS_TAC[]
892QED
893
894Theorem symmetric_LEX[simp]:
895 symmetric R1 /\ symmetric R2 ==> symmetric (R1 LEX R2)
896Proof
897 SIMP_TAC (srw_ss()) [symmetric_def, LEX_DEF, FORALL_PROD, UNCURRY_DEF] THEN
898 METIS_TAC[]
899QED
900
901Theorem LEX_CONG:
902 !R1 R2 v1 v2 R1' R2' v1' v2'.
903 (v1 = v1') /\ (v2 = v2') /\
904 (!a b c d. (v1' = (a,b)) /\ (v2' = (c,d)) ==> (R1 a c = R1' a c)) /\
905 (!a b c d. (v1' = (a,b)) /\ (v2' = (c,d)) /\ (a=c) ==> (R2 b d = R2' b d))
906 ==>
907 ($LEX R1 R2 v1 v2 = $LEX R1' R2' v1' v2')
908Proof
909 Ho_Rewrite.REWRITE_TAC [LEX_DEF,FORALL_PROD,PAIR_EQ]
910 THEN NTAC 2 (REWRITE_TAC [UNCURRY_VAR,FST,SND] THEN BETA_TAC)
911 THEN METIS_TAC[]
912QED
913
914(* ----------------------------------------------------------------------
915 PAIR_REL : ('a -> 'c -> bool) -> ('b -> 'd -> bool) ->
916 ('a # 'b -> 'c # 'd -> bool)
917 ---------------------------------------------------------------------- *)
918
919Overload PAIR_REL = “RPROD”
920val _ = set_mapped_fixity{fixity = Infixr 490, term_name = "PAIR_REL",
921 tok = "###"}
922
923Theorem PAIR_REL = RPROD_DEF
924Theorem PAIR_REL_THM[simp,compute]:
925 (R1 ### R2) (a,b) (c,d) <=> R1 a c /\ R2 b d
926Proof
927 SIMP_TAC (srw_ss()) [PAIR_REL]
928QED
929
930Theorem PAIR_REL_EQ[simp,quotient_simp]:
931 ($= ### $=) = $=
932Proof
933 SIMP_TAC (srw_ss()) [FUN_EQ_THM, FORALL_PROD]
934QED
935
936Theorem PAIR_REL_REFL:
937 (!x:'a. R1 x x) /\ (!y:'b. R2 y y) ==>
938 !xy. (R1 ### R2) xy xy
939Proof
940 SIMP_TAC (srw_ss()) [FORALL_PROD]
941QED
942
943Theorem PAIR_REL_SYM:
944 (!x y:'a. R1 x y <=> R1 y x) /\ (!a b:'b. R2 a b <=> R2 b a) ==>
945 !xy ab. (R1 ### R2) xy ab <=> (R1 ### R2) ab xy
946Proof
947 SIMP_TAC (srw_ss()) [FORALL_PROD]
948QED
949
950Theorem PAIR_REL_TRANS:
951 (!x y z:'a. R1 x y /\ R1 y z ==> R1 x z) /\
952 (!a b c:'b. R2 a b /\ R2 b c ==> R2 a c) ==>
953 !xy ab uv. (R1 ### R2) xy ab /\ (R1 ### R2) ab uv ==>
954 (R1 ### R2) xy uv
955Proof
956 SIMP_TAC (srw_ss()) [FORALL_PROD] >> METIS_TAC[]
957QED
958
959Theorem PAIR_EQUIV[quotient_equiv]:
960 !(R1:'a -> 'a -> bool) (R2 : 'b -> 'b -> bool).
961 EQUIV R1 ==> EQUIV R2 ==> EQUIV (R1 ### R2)
962Proof
963 rpt gen_tac >> simp[EQUIV_def, EQUIV_REFL_SYM_TRANS, PAIR_REL_REFL] >>
964 rpt strip_tac
965 >- (irule $ iffLR PAIR_REL_SYM >> simp[EQ_IMP_THM]) >>
966 irule PAIR_REL_TRANS >> METIS_TAC[]
967QED
968
969(* ----------------------------------------------------------------------
970 "set" functions
971
972 setFST : ('a # 'b) -> 'a set
973 setSND : ('a # 'b) -> 'b set
974 ---------------------------------------------------------------------- *)
975
976val setFST_def = new_definition(
977 "setFST_def[compute]",
978 “setFST p = λx. x = FST p”);
979
980val setSND_def = new_definition(
981 "setSND_def[compute]",
982 “setSND p = λx. x = SND p”);
983
984Theorem setFST_thm[simp]:
985 setFST (a,b) = λx. x = a
986Proof
987 simp[setFST_def]
988QED
989
990Theorem setSND_thm[simp]:
991 setSND (a,b) = λx. x = b
992Proof
993 simp[setSND_def]
994QED
995
996Theorem PAIR_MAP_CONG:
997 (!a:'a. a IN setFST ab ==> f1 a = f2 a :'c) /\
998 (!b:'b. b IN setSND ab ==> g1 b = g2 b :'d) ==>
999 (f1 ## g1) ab = (f2 ## g2) ab
1000Proof
1001 Q.ID_SPEC_TAC ‘ab’ >> SIMP_TAC (srw_ss()) [FORALL_PROD, IN_DEF]
1002QED
1003
1004Theorem PAIR_MAP_SET:
1005 (setFST ((f ## g) ab) = λc. ?a:'a. c:'c = f a /\ a IN setFST ab) /\
1006 (setSND ((f ## g) ab) = λd. ?b:'b. d:'d = g b /\ b IN setSND ab)
1007Proof
1008 Q.ID_SPEC_TAC ‘ab’ >> SIMP_TAC (srw_ss()) [FORALL_PROD, IN_DEF]
1009QED
1010
1011(* ----------------------------------------------------------------------
1012 Theorems to support the quotient package
1013 ---------------------------------------------------------------------- *)
1014
1015Theorem PAIR_QUOTIENT[quotient]:
1016 !R1 (abs1:'a -> 'c) rep1.
1017 QUOTIENT R1 abs1 rep1 ==>
1018 !R2 (abs2:'b -> 'd) rep2.
1019 QUOTIENT R2 abs2 rep2 ==>
1020 QUOTIENT (R1 ### R2) (abs1 ## abs2) (rep1 ## rep2)
1021Proof
1022 REPEAT STRIP_TAC
1023 THEN REWRITE_TAC[QUOTIENT_def]
1024 THEN REPEAT CONJ_TAC
1025 THENL
1026 [ rpt (dxrule_then assume_tac QUOTIENT_ABS_REP) >>
1027 simp[FORALL_PROD],
1028
1029 rpt (dxrule_then assume_tac QUOTIENT_REP_REFL) >>
1030 simp[FORALL_PROD],
1031
1032 simp[FORALL_PROD] >>
1033 rpt (dxrule_then (fn th => simp[Once th, SimpLHS]) QUOTIENT_REL) >>
1034 simp[AC CONJ_ASSOC CONJ_COMM]
1035 ]
1036QED
1037
1038
1039
1040(* Here are some definitional and well-formedness theorems
1041 for some standard polymorphic operators. Could almost certainly be
1042 generated and proved automatically.
1043*)
1044
1045(* FST, SND, COMMA, CURRY, UNCURRY, ## *)
1046
1047Theorem FST_PRS[quotient_prs]:
1048 !R1 (abs1:'a -> 'c) rep1.
1049 QUOTIENT R1 abs1 rep1 ==>
1050 !R2 (abs2:'b -> 'd) rep2.
1051 QUOTIENT R2 abs2 rep2 ==>
1052 !p. FST p = abs1 (FST ((rep1 ## rep2) p))
1053Proof
1054 REPEAT (rpt GEN_TAC THEN DISCH_TAC) >>
1055 rpt (dxrule_then assume_tac QUOTIENT_ABS_REP) >>
1056 simp[FORALL_PROD]
1057QED
1058
1059Theorem FST_RSP[quotient_rsp]:
1060 !R1 (abs1:'a -> 'c) rep1.
1061 QUOTIENT R1 abs1 rep1 ==>
1062 !R2 (abs2:'b -> 'd) rep2.
1063 QUOTIENT R2 abs2 rep2 ==>
1064 !p1 p2. (R1 ### R2) p1 p2 ==> R1 (FST p1) (FST p2)
1065Proof
1066 simp[FORALL_PROD]
1067QED
1068
1069Theorem SND_PRS[quotient_prs]:
1070 !R1 (abs1:'a -> 'c) rep1.
1071 QUOTIENT R1 abs1 rep1 ==>
1072 !R2 (abs2:'b -> 'd) rep2.
1073 QUOTIENT R2 abs2 rep2 ==>
1074 !p. SND p = abs2 (SND ((rep1 ## rep2) p))
1075Proof
1076 REPEAT GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN DISCH_TAC >>
1077 rpt (dxrule_then assume_tac QUOTIENT_ABS_REP) >>
1078 simp[FORALL_PROD]
1079QED
1080
1081Theorem SND_RSP[quotient_rsp]:
1082 !R1 (abs1:'a -> 'c) rep1.
1083 QUOTIENT R1 abs1 rep1 ==>
1084 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1085 !p1 p2.
1086 (R1 ### R2) p1 p2 ==> R2 (SND p1) (SND p2)
1087Proof
1088 simp[FORALL_PROD]
1089QED
1090
1091Theorem COMMA_PRS[quotient_prs]:
1092 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1093 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1094 !a b. (a,b) = (abs1 ## abs2) (rep1 a, rep2 b)
1095Proof
1096 REPEAT GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN DISCH_TAC >>
1097 rpt (dxrule_then assume_tac QUOTIENT_ABS_REP) >>
1098 simp[]
1099QED
1100
1101Theorem COMMA_RSP[quotient_rsp]:
1102 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1103 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1104 !a1 a2 b1 b2.
1105 R1 a1 b1 /\ R2 a2 b2 ==>
1106 (R1 ### R2) (a1,a2) (b1,b2)
1107Proof
1108 simp[]
1109QED
1110
1111Theorem CURRY_PRS[quotient_prs]:
1112 !R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
1113 !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
1114 !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
1115 !f a b. CURRY f a b =
1116 abs3 (CURRY (((abs1 ## abs2) --> rep3) f)
1117 (rep1 a) (rep2 b))
1118Proof
1119 ntac 3 (REPEAT GEN_TAC THEN DISCH_TAC) >>
1120 rpt (dxrule_then assume_tac QUOTIENT_ABS_REP) >>
1121 simp[FUN_MAP_THM]
1122QED
1123
1124Theorem CURRY_RSP[quotient_rsp]:
1125 !R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
1126 !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
1127 !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
1128 !f1 f2.
1129 ((R1 ### R2) ===> R3) f1 f2 ==>
1130 (R1 ===> R2 ===> R3) (CURRY f1) (CURRY f2)
1131Proof
1132 simp[FUN_REL]
1133QED
1134
1135Theorem UNCURRY_PRS[quotient_prs]:
1136 !R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
1137 !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
1138 !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
1139 !f p. UNCURRY f p =
1140 abs3 (UNCURRY ((abs1 --> abs2 --> rep3) f)
1141 ((rep1 ## rep2) p))
1142Proof
1143 REPEAT (REPEAT GEN_TAC THEN DISCH_TAC) >>
1144 rpt (dxrule_then assume_tac QUOTIENT_ABS_REP) >>
1145 simp[FUN_MAP_THM, FORALL_PROD]
1146QED
1147
1148Theorem UNCURRY_RSP[quotient_rsp]:
1149 !R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
1150 !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
1151 !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
1152 !f1 f2.
1153 (R1 ===> R2 ===> R3) f1 f2 ==>
1154 ((R1 ### R2) ===> R3) (UNCURRY f1) (UNCURRY f2)
1155Proof
1156 simp[FUN_REL, FORALL_PROD]
1157QED
1158
1159Theorem PAIR_MAP_PRS[quotient_prs]:
1160 !R1 (abs1:'a -> 'e) rep1. QUOTIENT R1 abs1 rep1 ==>
1161 !R2 (abs2:'b -> 'f) rep2. QUOTIENT R2 abs2 rep2 ==>
1162 !R3 (abs3:'c -> 'g) rep3. QUOTIENT R3 abs3 rep3 ==>
1163 !R4 (abs4:'d -> 'h) rep4. QUOTIENT R4 abs4 rep4 ==>
1164 !f g. (f ## g) =
1165 ((rep1 ## rep3) --> (abs2 ## abs4))
1166 (((abs1 --> rep2) f) ## ((abs3 --> rep4) g))
1167Proof
1168 REPEAT (REPEAT GEN_TAC THEN DISCH_TAC) >>
1169 rpt (dxrule_then assume_tac QUOTIENT_ABS_REP) >>
1170 simp[FUN_EQ_THM, FORALL_PROD, FUN_MAP_THM]
1171QED
1172
1173Theorem PAIR_MAP_RSP[quotient_rsp]:
1174 !R1 (abs1:'a -> 'e) rep1. QUOTIENT R1 abs1 rep1 ==>
1175 !R2 (abs2:'b -> 'f) rep2. QUOTIENT R2 abs2 rep2 ==>
1176 !R3 (abs3:'c -> 'g) rep3. QUOTIENT R3 abs3 rep3 ==>
1177 !R4 (abs4:'d -> 'h) rep4. QUOTIENT R4 abs4 rep4 ==>
1178 !f1 f2 g1 g2.
1179 (R1 ===> R2) f1 f2 /\ (R3 ===> R4) g1 g2 ==>
1180 ((R1 ### R3) ===> (R2 ### R4)) (f1 ## g1) (f2 ## g2)
1181Proof
1182 simp[FUN_REL, FORALL_PROD]
1183QED
1184
1185
1186(*---------------------------------------------------------------------------
1187 Generate some ML that gets evaluated at theory load time.
1188 It adds relevant rewrites into the global compset.
1189 ---------------------------------------------------------------------------*)
1190
1191fun stA s =
1192 let
1193 val nm = s ^ "_lazyfied"
1194 val th = save_thm(nm, computeLib.lazyfy_thm $ DB.fetch "-" s)
1195 in
1196 ThmAttribute.store_at_attribute {
1197 name = nm, attrname = "compute", args = [], thm = th
1198 }
1199 end
1200
1201(* not super apparent to me why these need to be lazyfied, with possible
1202 exception of pair_case_thm, which gives us some evaluation order control
1203*)
1204val _ = app stA ["pair_case_thm", "SWAP_def", "CURRY_DEF"]
1205
1206Theorem FST_EQ_EQUIV:
1207 (FST p = x) <=> ?y. p = (x,y)
1208Proof
1209 Q.ISPEC_THEN `p` STRUCT_CASES_TAC pair_CASES >> simp_tac(srw_ss())[]
1210QED
1211
1212Theorem SND_EQ_EQUIV:
1213 (SND p = y) <=> ?x. p = (x,y)
1214Proof
1215 Q.ISPEC_THEN `p` STRUCT_CASES_TAC pair_CASES >> simp_tac(srw_ss())[]
1216QED
1217
1218val _ = export_theory_as_docfiles "pair-help/thms"