pairToolsContextScript.sml

1Theory pairToolsContext[bare]
2Ancestors
3  pair
4Libs
5  HolKernel Parse boolLib
6
7(* ------------------------------------------------------------------------- *)
8(* Lemmas pairTools.sml formerly proved as it loaded.                        *)
9(* ------------------------------------------------------------------------- *)
10
11Theorem ELIM_PEXISTS2:
12  (?p:('a#'b). P (FST p) (SND p) p) <=> ?p1 p2. P p1 p2 (p1, p2)
13Proof
14  CONV_TAC (LHS_CONV (HO_REWR_CONV pairTheory.EXISTS_PROD)) THEN
15  REWRITE_TAC [pairTheory.FST, pairTheory.SND]
16QED
17
18Theorem ELIM_PFORALL2:
19  (!p:('a#'b). P (FST p) (SND p) p) <=> !p1 p2. P p1 p2 (p1, p2)
20Proof
21  CONV_TAC (LHS_CONV (HO_REWR_CONV pairTheory.FORALL_PROD)) THEN
22  REWRITE_TAC [pairTheory.FST, pairTheory.SND]
23QED
24
25Theorem PFORALL_THM2:
26  !P:'a->'b->bool. (!x. $! (P x)) <=> $! (UNCURRY P)
27Proof
28  GEN_TAC THEN
29  Q.SUBGOAL_THEN `P = (\x y. P x y)`
30     (fn thm => ONCE_ASM_REWRITE_TAC [thm])
31  THEN1 (REWRITE_TAC [FUN_EQ_THM] THEN BETA_TAC THEN REWRITE_TAC []) THEN
32  BETA_TAC THEN REWRITE_TAC [pairTheory.PFORALL_THM]
33QED
34
35Theorem PEXISTS_THM2:
36  !P:'a->'b->bool. (?x. $? (P x)) <=> $? (UNCURRY P)
37Proof
38  GEN_TAC THEN
39  Q.SUBGOAL_THEN `P = (\x y. P x y)`
40     (fn thm => ONCE_ASM_REWRITE_TAC [thm])
41  THEN1 (REWRITE_TAC [FUN_EQ_THM] THEN BETA_TAC THEN REWRITE_TAC []) THEN
42  BETA_TAC THEN REWRITE_TAC [pairTheory.PEXISTS_THM]
43QED