1 (* ========================================================================= *)
2 (* The axiom of infinity; construction of the natural numbers. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
12 (* ------------------------------------------------------------------------- *)
13 (* Declare a new type "ind" of individuals. *)
14 (* ------------------------------------------------------------------------- *)
18 (* ------------------------------------------------------------------------- *)
19 (* We assert the axiom of infinity as in HOL88, but then we can forget it! *)
20 (* ------------------------------------------------------------------------- *)
22 let ONE_ONE = new_definition
23 `ONE_ONE(f:A->B) = !x1 x2. (f x1 = f x2) ==> (x1 = x2)`;;
25 let ONTO = new_definition
26 `ONTO(f:A->B) = !y. ?x. y = f x`;;
28 let INFINITY_AX = new_axiom
29 `?f:ind->ind. ONE_ONE f /\ ~(ONTO f)`;;
31 (* ------------------------------------------------------------------------- *)
32 (* Actually introduce constants. *)
33 (* ------------------------------------------------------------------------- *)
35 let IND_SUC_0_EXISTS = prove
36 (`?(f:ind->ind) z. (!x1 x2. (f x1 = f x2) = (x1 = x2)) /\ (!x. ~(f x = z))`,
37 X_CHOOSE_TAC `f:ind->ind` INFINITY_AX THEN EXISTS_TAC `f:ind->ind` THEN
38 POP_ASSUM MP_TAC THEN REWRITE_TAC[ONE_ONE; ONTO] THEN MESON_TAC[]);;
41 let th1 = new_definition
42 `IND_SUC = @f:ind->ind. ?z. (!x1 x2. (f x1 = f x2) = (x1 = x2)) /\
44 let th2 = REWRITE_RULE[GSYM th1] (SELECT_RULE IND_SUC_0_EXISTS) in
45 let th3 = new_definition
46 `IND_0 = @z:ind. (!x1 x2. IND_SUC x1 = IND_SUC x2 <=> x1 = x2) /\
47 (!x. ~(IND_SUC x = z))` in
48 REWRITE_RULE[GSYM th3] (SELECT_RULE th2);;
50 let IND_SUC_INJ,IND_SUC_0 = CONJ_PAIR IND_SUC_SPEC;;
52 (* ------------------------------------------------------------------------- *)
53 (* Carve out the natural numbers inductively. *)
54 (* ------------------------------------------------------------------------- *)
56 let NUM_REP_RULES,NUM_REP_INDUCT,NUM_REP_CASES =
57 new_inductive_definition
59 (!i. NUM_REP i ==> NUM_REP (IND_SUC i))`;;
61 let num_tydef = new_basic_type_definition
62 "num" ("mk_num","dest_num")
63 (CONJUNCT1 NUM_REP_RULES);;
65 let ZERO_DEF = new_definition
68 let SUC_DEF = new_definition
69 `SUC n = mk_num(IND_SUC(dest_num n))`;;
71 (* ------------------------------------------------------------------------- *)
72 (* Distinctness and injectivity of constructors. *)
73 (* ------------------------------------------------------------------------- *)
77 REWRITE_TAC[SUC_DEF; ZERO_DEF] THEN
78 MESON_TAC[NUM_REP_RULES; fst num_tydef; snd num_tydef; IND_SUC_0]);;
81 (`!m n. SUC m = SUC n <=> m = n`,
82 REPEAT GEN_TAC THEN REWRITE_TAC[SUC_DEF] THEN
83 EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
84 POP_ASSUM(MP_TAC o AP_TERM `dest_num`) THEN
85 SUBGOAL_THEN `!p. NUM_REP (IND_SUC (dest_num p))` MP_TAC THENL
86 [GEN_TAC THEN MATCH_MP_TAC (CONJUNCT2 NUM_REP_RULES); ALL_TAC] THEN
87 REWRITE_TAC[fst num_tydef; snd num_tydef] THEN
88 DISCH_TAC THEN ASM_REWRITE_TAC[IND_SUC_INJ] THEN
89 DISCH_THEN(MP_TAC o AP_TERM `mk_num`) THEN
90 REWRITE_TAC[fst num_tydef]);;
92 (* ------------------------------------------------------------------------- *)
94 (* ------------------------------------------------------------------------- *)
96 let num_INDUCTION = prove
97 (`!P. P(_0) /\ (!n. P(n) ==> P(SUC n)) ==> !n. P n`,
99 MP_TAC(SPEC `\i. NUM_REP i /\ P(mk_num i):bool` NUM_REP_INDUCT) THEN
100 ASM_REWRITE_TAC[GSYM ZERO_DEF; NUM_REP_RULES] THEN
101 W(C SUBGOAL_THEN (fun t -> REWRITE_TAC[t]) o funpow 2 lhand o snd) THENL
102 [REPEAT STRIP_TAC THENL
103 [MATCH_MP_TAC(CONJUNCT2 NUM_REP_RULES) THEN ASM_REWRITE_TAC[];
104 SUBGOAL_THEN `mk_num(IND_SUC i) = SUC(mk_num i)` SUBST1_TAC THENL
105 [REWRITE_TAC[SUC_DEF] THEN REPEAT AP_TERM_TAC THEN
106 CONV_TAC SYM_CONV THEN REWRITE_TAC[GSYM(snd num_tydef)] THEN
107 FIRST_ASSUM MATCH_ACCEPT_TAC;
108 FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC]];
109 DISCH_THEN(MP_TAC o SPEC `dest_num n`) THEN
110 REWRITE_TAC[fst num_tydef; snd num_tydef]]);;
112 (* ------------------------------------------------------------------------- *)
114 (* ------------------------------------------------------------------------- *)
116 let num_Axiom = prove
117 (`!(e:A) f. ?!fn. (fn _0 = e) /\
118 (!n. fn (SUC n) = f (fn n) n)`,
119 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[EXISTS_UNIQUE_THM] THEN CONJ_TAC THENL
120 [(MP_TAC o prove_inductive_relations_exist)
121 `PRG _0 e /\ (!b:A n:num. PRG n b ==> PRG (SUC n) (f b n))` THEN
122 DISCH_THEN(CHOOSE_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
123 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (ASSUME_TAC o GSYM)) THEN
124 SUBGOAL_THEN `!n:num. ?!y:A. PRG n y` MP_TAC THENL
125 [MATCH_MP_TAC num_INDUCTION THEN REPEAT STRIP_TAC THEN
126 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC BINDER_CONV [GSYM th]) THEN
127 REWRITE_TAC[GSYM NOT_SUC; NOT_SUC; SUC_INJ; EXISTS_UNIQUE_REFL] THEN
128 REWRITE_TAC[UNWIND_THM1] THEN
129 UNDISCH_TAC `?!y. PRG (n:num) (y:A)` THEN
130 REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
131 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `y:A`) ASSUME_TAC) THEN
132 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
133 [MAP_EVERY EXISTS_TAC [`(f:A->num->A) y n`; `y:A`];
134 AP_THM_TAC THEN AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC] THEN
136 REWRITE_TAC[UNIQUE_SKOLEM_ALT] THEN
137 DISCH_THEN(X_CHOOSE_THEN `fn:num->A` (ASSUME_TAC o GSYM)) THEN
138 EXISTS_TAC `fn:num->A` THEN ASM_REWRITE_TAC[] THEN
139 GEN_TAC THEN FIRST_ASSUM(MATCH_MP_TAC o CONJUNCT2) THEN
140 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC I [GSYM th]) THEN REFL_TAC];
141 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
142 MATCH_MP_TAC num_INDUCTION THEN ASM_REWRITE_TAC[] THEN
143 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]]);;
145 (* ------------------------------------------------------------------------- *)
146 (* The basic numeral tag; rewrite existing instances of "_0". *)
147 (* ------------------------------------------------------------------------- *)
149 let NUMERAL = new_definition
150 `NUMERAL (n:num) = n`;;
152 let [NOT_SUC; num_INDUCTION; num_Axiom] =
153 let th = prove(`_0 = 0`,REWRITE_TAC[NUMERAL]) in
154 map (GEN_REWRITE_RULE DEPTH_CONV [th])
155 [NOT_SUC; num_INDUCTION; num_Axiom];;
157 (* ------------------------------------------------------------------------- *)
158 (* Induction tactic. *)
159 (* ------------------------------------------------------------------------- *)
161 let (INDUCT_TAC:tactic) =
162 MATCH_MP_TAC num_INDUCTION THEN
163 CONJ_TAC THENL [ALL_TAC; GEN_TAC THEN DISCH_TAC];;
166 let avs = fst(strip_forall(concl num_Axiom)) in
167 GENL avs (EXISTENCE (SPECL avs num_Axiom));;
169 (* ------------------------------------------------------------------------- *)
171 (* ------------------------------------------------------------------------- *)
173 let num_CASES = prove
174 (`!m. (m = 0) \/ (?n. m = SUC n)`,
175 INDUCT_TAC THEN MESON_TAC[]);;
177 (* ------------------------------------------------------------------------- *)
178 (* Augmenting inductive type store. *)
179 (* ------------------------------------------------------------------------- *)
181 let num_RECURSION_STD = prove
182 (`!e:Z f. ?fn. (fn 0 = e) /\ (!n. fn (SUC n) = f n (fn n))`,
184 MP_TAC(ISPECL [`e:Z`; `(\z n. (f:num->Z->Z) n z)`] num_RECURSION) THEN
187 inductive_type_store :=
188 ("num",(2,num_INDUCTION,num_RECURSION_STD))::(!inductive_type_store);;
190 (* ------------------------------------------------------------------------- *)
191 (* "Bitwise" binary representation of numerals. *)
192 (* ------------------------------------------------------------------------- *)
195 let def = new_definition
196 `BIT0 = @fn. fn 0 = 0 /\ (!n. fn (SUC n) = SUC (SUC(fn n)))`
197 and th = BETA_RULE(ISPECL [`0`; `\m n:num. SUC(SUC m)`] num_RECURSION) in
198 REWRITE_RULE[GSYM def] (SELECT_RULE th);;
200 let BIT1_DEF = new_definition
201 `BIT1 n = SUC (BIT0 n)`;;
203 (* ------------------------------------------------------------------------- *)
204 (* Syntax operations on numerals. *)
205 (* ------------------------------------------------------------------------- *)
208 let pow24 = pow2 24 and num_0 = Int 0
209 and zero_tm = mk_const("_0",[])
210 and BIT0_tm = mk_const("BIT0",[])
211 and BIT1_tm = mk_const("BIT1",[])
212 and NUMERAL_tm = mk_const("NUMERAL",[]) in
213 let rec stripzeros l = match l with false::t -> stripzeros t | _ -> l in
214 let rec raw_list_of_num l n =
215 if n =/ num_0 then stripzeros l else
216 let h = Num.int_of_num(mod_num n pow24) in
218 ((h land 8388608 <> 0)::(h land 4194304 <> 0)::(h land 2097152 <> 0)::
219 (h land 1048576 <> 0)::(h land 524288 <> 0)::(h land 262144 <> 0)::
220 (h land 131072 <> 0)::(h land 65536 <> 0)::(h land 32768 <> 0)::
221 (h land 16384 <> 0)::(h land 8192 <> 0)::(h land 4096 <> 0)::
222 (h land 2048 <> 0)::(h land 1024 <> 0)::(h land 512 <> 0)::
223 (h land 256 <> 0)::(h land 128 <> 0)::(h land 64 <> 0)::
224 (h land 32 <> 0)::(h land 16 <> 0)::(h land 8 <> 0)::(h land 4 <> 0)::
225 (h land 2 <> 0)::(h land 1 <> 0)::l) (quo_num n pow24) in
226 let rec numeral_of_list t l =
229 | b::r -> numeral_of_list(mk_comb((if b then BIT1_tm else BIT0_tm),t)) r in
230 let mk_raw_numeral n = numeral_of_list zero_tm (raw_list_of_num [] n) in
231 fun n -> if n </ num_0 then failwith "mk_numeral: negative argument" else
232 mk_comb(NUMERAL_tm,mk_raw_numeral n);;
234 let mk_small_numeral n = mk_numeral(Int n);;
236 let dest_small_numeral t = Num.int_of_num(dest_numeral t);;
238 let is_numeral = can dest_numeral;;
240 (* ------------------------------------------------------------------------- *)
241 (* Derived principles of definition based on existence. *)
243 (* This is put here because we use numerals as tags to force different *)
244 (* constants specified with equivalent theorems to have different underlying *)
245 (* definitions, ensuring that there are no provable equalities between them *)
246 (* and so in some sense the constants are "underspecified" as the user might *)
247 (* want for some applications. *)
248 (* ------------------------------------------------------------------------- *)
250 let the_specifications = ref [];;
252 let new_specification =
253 let code c = mk_small_numeral (Char.code (c.[0])) in
255 end_itlist (curry mk_pair) (map code (explode name)) in
256 let check_distinct l =
257 try itlist (fun t res -> if mem t res then fail() else t::res) l []; true
258 with Failure _ -> false in
259 let specify name th =
260 let ntm = mk_code name in
261 let gv = genvar(type_of ntm) in
262 let th0 = CONV_RULE(REWR_CONV SKOLEM_THM) (GEN gv th) in
263 let th1 = CONV_RULE(RATOR_CONV (REWR_CONV EXISTS_THM) THENC
265 let l,r = dest_comb(concl th1) in
266 let rn = mk_comb(r,ntm) in
267 let ty = type_of rn in
268 let th2 = new_definition(mk_eq(mk_var(name,ty),rn)) in
269 GEN_REWRITE_RULE ONCE_DEPTH_CONV [GSYM th2]
270 (SPEC ntm (CONV_RULE BETA_CONV th1)) in
271 let rec specifies names th =
274 | name::onames -> let th' = specify name th in
275 specifies onames th' in
277 let asl,c = dest_thm th in
278 if not (asl = []) then
279 failwith "new_specification: Assumptions not allowed in theorem" else
280 if not (frees c = []) then
281 failwith "new_specification: Free variables in predicate" else
282 let avs = fst(strip_exists c) in
283 if length names = 0 or length names > length avs then
284 failwith "new_specification: Unsuitable number of constant names" else
285 if not (check_distinct names) then
286 failwith "new_specification: Constant names not distinct"
288 try let sth = snd(find (fun ((names',th'),sth') ->
289 names' = names & aconv (concl th') (concl th))
290 (!the_specifications)) in
291 warn true ("Benign respecification"); sth
293 let sth = specifies names th in
294 the_specifications := ((names,th),sth)::(!the_specifications);