canonContextScript.sml

1Theory canonContext[bare]
2Ancestors
3  combin
4Libs
5  HolKernel Parse boolLib tautLib
6
7(* ------------------------------------------------------------------------- *)
8(* Lemmas Canon.sml formerly proved as it loaded.  Doing it in a proper      *)
9(* theory removes the load-order sensitivity flagged by TAC_PROOF's          *)
10(* current-theory check.                                                     *)
11(* ------------------------------------------------------------------------- *)
12
13(* ONEWAY_SKOLEM_CONV support *)
14
15Theorem pth1: (?x:'a. P) <=> P
16Proof
17  REWRITE_TAC[EXISTS_SIMP]
18QED
19
20Theorem pth2:  (z:'a = $@ P) ==> ($? P <=> P z)
21Proof
22  DISCH_THEN SUBST1_TAC THEN
23  CONV_TAC (LAND_CONV (RATOR_CONV (REWR_CONV boolTheory.EXISTS_DEF) THENC
24                       BETA_CONV)) THEN
25  REFL_TAC
26QED
27
28(* NNF_CONV / NNF_SKOLEM_CONV support *)
29
30Theorem pth_pimp:  (p ==> q) <=> q \/ ~p
31Proof TAUT_TAC
32QED
33
34Theorem pth_peq1:  (p = q) <=> (p \/ ~q) /\ (~p \/ q)
35Proof TAUT_TAC
36QED
37
38Theorem pth_peq2:  (p = q) <=> (p /\ q) \/ (~p /\ ~q)
39Proof TAUT_TAC
40QED
41
42Theorem pth_pcond1: (if p then q else q') <=> (p \/ q') /\ (~p \/ q)
43Proof TAUT_TAC
44QED
45
46Theorem pth_pcond2: (if p then q else q') <=> (p /\ q) \/ (~p /\ q')
47Proof TAUT_TAC
48QED
49
50Theorem pth_nnot:  ~~p:bool <=> p
51Proof TAUT_TAC
52QED
53
54Theorem pth_nand:  ~(p /\ q) <=> ~p \/ ~q
55Proof TAUT_TAC
56QED
57
58Theorem pth_nor:   ~(p \/ q) <=> ~p /\ ~q
59Proof TAUT_TAC
60QED
61
62Theorem pth_nimp:  ~(p ==> q) <=> ~q /\ p
63Proof TAUT_TAC
64QED
65
66Theorem pth_neq1:  ~(p = q) <=> (p \/ q) /\ (~p \/ ~q)
67Proof TAUT_TAC
68QED
69
70Theorem pth_neq2:  ~(p = q) <=> (p /\ ~q) \/ (~p /\ q)
71Proof TAUT_TAC
72QED
73
74Theorem pth_ncond1: ~(if p then q else q') <=> (p \/ ~q') /\ (~p \/ ~q)
75Proof TAUT_TAC
76QED
77
78Theorem pth_ncond2: ~(if p then q else q') <=> (p /\ ~q) \/ (~p /\ ~q')
79Proof TAUT_TAC
80QED
81
82Theorem EXISTS_UNIQUE_THM2:
83  !P. (?!x:'a. P x) <=> (?x. P x /\ !y. P y ==> (y = x))
84Proof
85  REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
86  GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
87    Q.EXISTS_TAC `x` THEN ASM_REWRITE_TAC[] THEN
88    REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
89    ASM_REWRITE_TAC[],
90    CONJ_TAC THEN1 (Q.EXISTS_TAC `x` THEN ASM_REWRITE_TAC[]) THEN
91    REPEAT STRIP_TAC THEN
92    MATCH_MP_TAC EQ_TRANS THEN Q.EXISTS_TAC `x` THEN
93    CONJ_TAC THENL [
94      FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[],
95      CONV_TAC SYM_CONV THEN FIRST_ASSUM MATCH_MP_TAC THEN
96      ASM_REWRITE_TAC[]
97    ]
98  ]
99QED
100
101Theorem LOCAL_COND_ELIM_THM1:
102  !P:'a->bool. P(if a then b else c) <=> (~a \/ P(b)) /\ (a \/ P(c))
103Proof
104  GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]
105QED
106
107Theorem LOCAL_COND_ELIM_THM2:
108  !P:'a->bool. P(if a then b else c) <=> a /\ P(b) \/ ~a /\ P(c)
109Proof
110  GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]
111QED
112
113(* PROP_CNF_CONV support *)
114
115Theorem cnf_th1:  a \/ (b /\ c) <=> (a \/ b) /\ (a \/ c)
116Proof TAUT_TAC
117QED
118
119Theorem cnf_th2:  (a /\ b) \/ c <=> (a \/ c) /\ (b \/ c)
120Proof TAUT_TAC
121QED
122
123(* PROP_DNF_CONV support *)
124
125Theorem dnf_th1:  a /\ (b \/ c) <=> (a /\ b) \/ (a /\ c)
126Proof TAUT_TAC
127QED
128
129Theorem dnf_th2:  (a \/ b) /\ c <=> (a /\ c) \/ (b /\ c)
130Proof TAUT_TAC
131QED
132
133(* REFUTE support *)
134
135Theorem refute_pth:    (~p ==> F) ==> p
136Proof TAUT_TAC
137QED
138
139Theorem refute_pth_d:  (a \/ b) /\ c <=> (a /\ c) \/ (b /\ c)
140Proof TAUT_TAC
141QED
142
143(* EQ_ABS_CONV support *)
144
145Theorem eq_abs_pth:  (f:'a->'b = \x. t x) <=> (!x. f x = t x)
146Proof
147  REWRITE_TAC[FUN_EQ_THM, BETA_THM]
148QED
149
150(* UNLAMB_CONV support *)
151
152Theorem unlamb_pth:  P (t:'a) <=> (!x. (x = t) ==> P x)
153Proof
154  EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
155  FIRST_ASSUM MATCH_MP_TAC THEN REFL_TAC
156QED
157
158(* FOL_CONV / APP_CONV support *)
159
160Theorem app_conv_th:  !(f:'a->'b) x. f x = combin$I f x
161Proof
162  REWRITE_TAC[combinTheory.I_THM]
163QED
164
165(* DISJ_ACI_RULE support *)
166
167Theorem disj_aci_left:   ~(a \/ b) ==> ~a
168Proof TAUT_TAC
169QED
170
171Theorem disj_aci_right:  ~(a \/ b) ==> ~b
172Proof TAUT_TAC
173QED
174
175Theorem disj_aci_pth:    ~a ==> ~b ==> ~(a \/ b)
176Proof TAUT_TAC
177QED
178
179Theorem disj_aci_neg:    (~a <=> ~b) ==> (a <=> b)
180Proof TAUT_TAC
181QED