numScript.sml
1Theory num[bare]
2Ancestors
3 bool
4Libs
5 HolKernel Parse boolLib
6
7infix THEN THENL;
8
9val _ = if !Globals.interactive then () else Feedback.emit_WARNING := false;
10
11(*---------------------------------------------------------------------------
12 * Define successor `SUC_REP:ind->ind` on ind.
13 *---------------------------------------------------------------------------*)
14
15val SUC_REP_DEF = new_specification
16 ("SUC_REP_DEF",["SUC_REP"], boolTheory.INFINITY_AX);
17
18
19Theorem ZERO_REP_EXISTS[local]:
20 ?z. !y. ~(z = SUC_REP y)
21Proof
22 Q.X_CHOOSE_THEN `zrep` ASSUME_TAC ((CONV_RULE NOT_FORALL_CONV o
23 REWRITE_RULE [ONTO_THM] o
24 CONJUNCT2) SUC_REP_DEF) THEN
25 POP_ASSUM (ASSUME_TAC o CONV_RULE NOT_EXISTS_CONV) THEN
26 Q.EXISTS_TAC `zrep` THEN POP_ASSUM ACCEPT_TAC
27QED
28
29(*---------------------------------------------------------------------------
30 * `ZERO_REP:ind` represents `0:num`
31 *---------------------------------------------------------------------------*)
32
33val ZERO_REP_DEF = new_specification
34 ("ZERO_REP_DEF",["ZERO_REP"], ZERO_REP_EXISTS);
35
36
37(*---------------------------------------------------------------------------*)
38(* `IS_NUM:ind->bool` defines the subset of `:ind` used to represent *)
39(* numbers. It is the smallest subset containing `ZERO_REP` and closed *)
40(* under `SUC_REP`. *)
41(*---------------------------------------------------------------------------*)
42
43val IS_NUM_REP = new_definition("IS_NUM_REP",
44 “IS_NUM_REP m =
45 !P:ind->bool. (P ZERO_REP /\ (!n. P n ==> P(SUC_REP n))) ==> P m”);
46
47(*---------------------------------------------------------------------------
48 * Prove that there is a representation in :ind of at least one number.
49 *---------------------------------------------------------------------------*)
50
51val EXISTS_NUM_REP = TAC_PROOF(([],“?n. IS_NUM_REP n”),
52 PURE_REWRITE_TAC [IS_NUM_REP] THEN
53 EXISTS_TAC (“ZERO_REP”) THEN
54 REPEAT STRIP_TAC);
55
56(*---------------------------------------------------------------------------
57 * Make the type definition.
58 *---------------------------------------------------------------------------*)
59
60val num_TY_DEF = new_type_definition ("num", EXISTS_NUM_REP);
61
62val num_ISO_DEF = define_new_type_bijections
63 {name = "num_ISO_DEF",
64 ABS = "ABS_num",
65 REP = "REP_num",
66 tyax = num_TY_DEF};
67
68val R_11 = prove_rep_fn_one_one num_ISO_DEF
69and R_ONTO = prove_rep_fn_onto num_ISO_DEF
70and A_11 = prove_abs_fn_one_one num_ISO_DEF
71and A_ONTO = prove_abs_fn_onto num_ISO_DEF;
72
73(*---------------------------------------------------------------------------
74 * Define ZERO.
75 *---------------------------------------------------------------------------*)
76
77val zero = mk_var("0", mk_thy_type{Tyop="num",Thy="num",Args=[]});
78
79val ZERO_DEF = new_definition("ZERO_DEF", “^zero = ABS_num ZERO_REP”);
80
81
82(*---------------------------------------------------------------------------
83 * Define the successor function on num.
84 *---------------------------------------------------------------------------*)
85
86val SUC_DEF = new_definition("SUC_DEF",
87 “SUC m = ABS_num(SUC_REP(REP_num m))”);
88
89local open OpenTheoryMap in
90val ns = ["Number","Natural"]
91val _ = OpenTheory_tyop_name{tyop={Thy="num",Tyop="num"},name=(ns,"natural")}
92val _ = OpenTheory_const_name{const={Thy="num",Name="0"},name=(ns,"zero")}
93val _ = OpenTheory_const_name{const={Thy="num",Name="SUC"},name=(ns,"suc")}
94end
95
96(*---------------------------------------------------------------------------
97 * Prove that IS_NUM_REP ZERO_REP.
98 *---------------------------------------------------------------------------*)
99
100val IS_NUM_REP_ZERO =
101 TAC_PROOF
102 (([], “IS_NUM_REP ZERO_REP”),
103 REWRITE_TAC [IS_NUM_REP] THEN REPEAT STRIP_TAC);
104
105(*---------------------------------------------------------------------------
106 * Prove that IS_NUM_REP (SUC_REP x).
107 *---------------------------------------------------------------------------*)
108
109val IS_NUM_SUC_REP =
110 TAC_PROOF
111 (([], “!i. IS_NUM_REP i ==> IS_NUM_REP (SUC_REP i)”),
112 REWRITE_TAC [IS_NUM_REP] THEN
113 REPEAT STRIP_TAC THEN RES_TAC THEN RES_TAC);
114
115val IS_NUM_REP_SUC_REP =
116 TAC_PROOF
117 (([], “!n. IS_NUM_REP(SUC_REP(REP_num n))”),
118 GEN_TAC THEN MATCH_MP_TAC IS_NUM_SUC_REP THEN
119 REWRITE_TAC [R_ONTO] THEN
120 EXISTS_TAC (“n:num”) THEN REFL_TAC);
121
122(*---------------------------------------------------------------------------
123 * |- !x1 x2. (SUC_REP x1 = SUC_REP x2) ==> (x1 = x2)
124 *---------------------------------------------------------------------------*)
125
126val SUC_REP_11 = CONJUNCT1 (REWRITE_RULE [ONE_ONE_THM] SUC_REP_DEF);
127
128(*---------------------------------------------------------------------------
129 * |- !x. ~(SUC_REP x = ZERO_REP)
130 *---------------------------------------------------------------------------*)
131
132val NOT_SUC_ZERO = GSYM ZERO_REP_DEF;
133
134(*----------------------------------------------------------------------*)
135(* Proof of NOT_SUC : |- !n. ~(SUC n = ZERO) *)
136(* ---------------------------------------------------------------------*)
137
138Theorem NOT_SUC:
139 !n. ~(SUC n = 0)
140Proof
141 PURE_REWRITE_TAC [SUC_DEF,ZERO_DEF] THEN GEN_TAC THEN
142 MP_TAC (SPECL [“SUC_REP(REP_num n)”,“ZERO_REP”] A_11) THEN
143 REWRITE_TAC [IS_NUM_REP_ZERO,IS_NUM_REP_SUC_REP] THEN
144 DISCH_THEN SUBST1_TAC THEN
145 MATCH_ACCEPT_TAC NOT_SUC_ZERO
146QED
147
148(* ---------------------------------------------------------------------*)
149(* Prove that |- !m n. (SUC m = SUC n) ==> (m = n) *)
150(* ---------------------------------------------------------------------*)
151
152Theorem INV_SUC:
153 !m n. (SUC m = SUC n) ==> (m = n)
154Proof
155 REPEAT GEN_TAC THEN REWRITE_TAC [SUC_DEF] THEN
156 MP_TAC (SPECL [“SUC_REP(REP_num m)”,
157 “SUC_REP(REP_num n)”] A_11) THEN
158 REWRITE_TAC [IS_NUM_REP_SUC_REP] THEN DISCH_THEN SUBST1_TAC THEN
159 DISCH_THEN (MP_TAC o MATCH_MP SUC_REP_11) THEN
160 REWRITE_TAC [R_11]
161QED
162
163(* ---------------------------------------------------------------------*)
164(* Prove induction theorem. *)
165(* ---------------------------------------------------------------------*)
166
167val ind_lemma1 =
168 TAC_PROOF
169 (([], “!P. P ZERO_REP /\ (!i. P i ==> P(SUC_REP i))
170 ==>
171 !i. IS_NUM_REP i ==> P i”),
172 PURE_ONCE_REWRITE_TAC [IS_NUM_REP] THEN
173 REPEAT STRIP_TAC THEN RES_TAC);
174
175val lemma =
176 TAC_PROOF(([], “(A ==> (A /\ B)) = (A ==> B)”),
177 ASM_CASES_TAC (“A:bool”) THEN ASM_REWRITE_TAC []);
178
179val ind_lemma2 = TAC_PROOF(([],
180 “!P. P ZERO_REP /\ (!i. IS_NUM_REP i /\ P i ==> P(SUC_REP i))
181 ==>
182 !i. IS_NUM_REP i ==> P i”),
183 GEN_TAC THEN STRIP_TAC THEN
184 MP_TAC (SPEC “\i. IS_NUM_REP i /\ P i” ind_lemma1) THEN
185 CONV_TAC(DEPTH_CONV BETA_CONV) THEN
186 REWRITE_TAC [lemma] THEN DISCH_THEN MATCH_MP_TAC THEN
187 ASM_REWRITE_TAC [IS_NUM_REP_ZERO] THEN
188 REPEAT STRIP_TAC THEN IMP_RES_TAC IS_NUM_SUC_REP THEN
189 RES_TAC);
190
191val lemma1 =
192 TAC_PROOF
193 (([], “(!i. IS_NUM_REP i ==> P(ABS_num i)) = (!n. P n)”),
194 EQ_TAC THEN REPEAT STRIP_TAC THENL
195 [STRIP_ASSUME_TAC (SPEC (“n:num”) A_ONTO) THEN
196 RES_TAC THEN ASM_REWRITE_TAC [],
197 POP_ASSUM MP_TAC THEN REWRITE_TAC [R_ONTO] THEN
198 STRIP_GOAL_THEN (STRIP_THM_THEN SUBST1_TAC) THEN
199 ASM_REWRITE_TAC []]);
200
201Theorem INDUCTION:
202 !P. P 0 /\ (!n. P n ==> P(SUC n)) ==> !n. P n
203Proof
204 GEN_TAC THEN STRIP_TAC THEN
205 MP_TAC (SPEC “\i. ((P(ABS_num i)):bool)” ind_lemma2) THEN
206 CONV_TAC(DEPTH_CONV BETA_CONV) THEN
207 REWRITE_TAC [SYM ZERO_DEF,lemma1] THEN
208 DISCH_THEN MATCH_MP_TAC THEN CONJ_TAC THENL
209 [FIRST_ASSUM ACCEPT_TAC,
210 REWRITE_TAC [R_ONTO] THEN
211 GEN_TAC THEN CONV_TAC ANTE_CONJ_CONV THEN
212 DISCH_THEN (STRIP_THM_THEN SUBST1_TAC) THEN
213 ASM_REWRITE_TAC [num_ISO_DEF,SYM (SPEC_ALL SUC_DEF)]]
214QED
215