Canon_Port_ContextScript.sml

1Theory Canon_Port_Context[bare]
2Ancestors
3  combin
4Libs
5  HolKernel Parse boolLib tautLib
6
7(* ------------------------------------------------------------------------- *)
8(* Lemmas Canon_Port.sml formerly proved as it loaded.                       *)
9(* ------------------------------------------------------------------------- *)
10
11Theorem APP_EQ_I:  !(f:'a->'b) x. f x = I f x
12Proof REWRITE_TAC[combinTheory.I_THM]
13QED
14
15Theorem NOT_EXISTS_UNIQUE_THM:
16  ~(?!x:'a. P x) <=> (!x. ~P x) \/ ?x x'. P x /\ P x' /\ ~(x = x')
17Proof
18  REWRITE_TAC [EXISTS_UNIQUE_THM, DE_MORGAN_THM, NOT_EXISTS_THM] THEN
19  CONV_TAC (REDEPTH_CONV NOT_FORALL_CONV) THEN
20  REWRITE_TAC [NOT_IMP, CONJ_ASSOC]
21QED
22
23Theorem cp_not_not:   ~~p:bool <=> p
24Proof tautLib.TAUT_TAC
25QED
26
27Theorem cp_not_and:   ~(p /\ q) <=> ~p \/ ~q
28Proof tautLib.TAUT_TAC
29QED
30
31Theorem cp_not_or:    ~(p \/ q) <=> ~p /\ ~q
32Proof tautLib.TAUT_TAC
33QED
34
35Theorem cp_not_imp:   ~(p ==> q) <=> p /\ ~q
36Proof tautLib.TAUT_TAC
37QED
38
39Theorem cp_imp:       p ==> q <=> ~p \/ q
40Proof tautLib.TAUT_TAC
41QED
42
43Theorem cp_not_eq_dnf: ~(p = q) <=> (p /\ ~q) \/ (~p /\ q)
44Proof tautLib.TAUT_TAC
45QED
46
47Theorem cp_eq_dnf:     (p = q) <=> (p /\ q) \/ (~p /\ ~q)
48Proof tautLib.TAUT_TAC
49QED
50
51Theorem cp_not_eq_cnf: ~(p = q) <=> (p \/ q) /\ (~p \/ ~q)
52Proof tautLib.TAUT_TAC
53QED
54
55Theorem cp_eq_cnf:     (p = q) <=> (p \/ ~q) /\ (~p \/ q)
56Proof tautLib.TAUT_TAC
57QED
58
59Theorem DELAMB_PTH:
60  (((\x. s x) = t) <=> (!x:'a. s x:'b = t x)) /\
61   ((s = \x. t x) <=> (!x. s x = t x))
62Proof
63  CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN BETA_TAC THEN REWRITE_TAC []
64QED
65
66Theorem cp_cnf_l:  a \/ (b /\ c) <=> (a \/ b) /\ (a \/ c)
67Proof tautLib.TAUT_TAC
68QED
69
70Theorem cp_cnf_r:  (a /\ b) \/ c <=> (a \/ c) /\ (b \/ c)
71Proof tautLib.TAUT_TAC
72QED
73
74Theorem cp_refute:  p <=> ~p ==> F
75Proof tautLib.TAUT_TAC
76QED