prim_recScript.sml
1(* ===================================================================== *)
2(* FILE : mk_prim_rec.sml *)
3(* DESCRIPTION : The primitive recursion theorem from Peano's axioms. *)
4(* Translated from hol88. *)
5(* *)
6(* AUTHORS : (c) Mike Gordon and *)
7(* Tom Melham, University of Cambridge *)
8(* TRANSLATOR : Konrad Slind, University of Calgary *)
9(* DATE : September 15, 1991 *)
10(* ===================================================================== *)
11
12
13(*---------------------------------------------------------------------------
14 * In this file, we prove the primitive recursion theorem directly
15 * from Peano's axioms (which are actually theorems in HOL).
16 * These `axioms' define the type ":num" and two
17 * constants "0:num" and "SUC:num->num", they are:
18 *
19 * NOT_SUC |- !n. ~(SUC n = 0)
20 *
21 * INV_SUC |- !m n. (SUC m = SUC n) ==> (m = n)
22 *
23 * INDUCTION |- !P. (P 0 /\ (!n. P n ==> P(SUC n))) ==> !n. P n
24 *
25 * Using INDUCTION one can define an induction rule and tactic.
26 * The rule is an ML function:
27 *
28 * INDUCT: (thm # thm) -> thm
29 *
30 * A1 |- t[0] A2 |- !n. t[n] ==> t[SUC n]
31 * -----------------------------------------------
32 * A1 u A2 |- !n. t[n]
33 *
34 * The tactic is:
35 *
36 * [A] !n.t[n]
37 * ================================
38 * [A] t[0] , [A,t[n]] t[SUC x]
39 *
40 * From now on we only make (non-recursive) definitions and prove theorems.
41 *
42 * The following definition of < is from Hodges's article in "The Handbook of
43 * Philosophical Logic" (page 111):
44 *
45 * m < n = ?P. (!n. P(SUC n) ==> P n) /\ P m /\ ~(P n)
46 *
47 *
48 * The following consequence of INV_SUC will be useful for rewriting:
49 *
50 * |- !m n. (SUC m = SUC n) = (m = n)
51 *
52 * It is used in SUC_ID and PRIM_REC_EXISTS below. We establish it by
53 * forward proof.
54 *
55 * After proving this we prove some standard properties of <.
56 *---------------------------------------------------------------------------*)
57Theory prim_rec[bare]
58Libs
59 HolKernel boolLib Prim_rec Parse simpLib boolSimps
60 BasicProvers[qualified] (* enable [simp] tag *)
61
62
63type thm = Thm.thm
64
65val _ = if !Globals.interactive then () else Feedback.emit_WARNING := false;
66
67(* Added TFM 88.04.02 *)
68
69val NOT_SUC = numTheory.NOT_SUC
70and INV_SUC = numTheory.INV_SUC
71and INDUCTION = numTheory.INDUCTION;
72
73fun INDUCT_TAC g = INDUCT_THEN INDUCTION ASSUME_TAC g;
74
75val LESS_DEF = new_definition (
76 "LESS_DEF",
77 “$< m n = ?P. (!n. P(SUC n) ==> P n) /\ P m /\ ~(P n)”)
78val _ = set_fixity "<" (Infix(NONASSOC, 450))
79val _ = TeX_notation {hol = "<", TeX = ("\\HOLTokenLt{}", 1)}
80val _ = OpenTheoryMap.OpenTheory_const_name{
81 const={Thy="prim_rec",Name="<"},
82 name=(["Number","Natural"],"<")
83 }
84
85Theorem INV_SUC_EQ =
86 GENL [“m:num”, “n:num”]
87 (IMP_ANTISYM_RULE
88 (SPEC_ALL INV_SUC)
89 (DISCH (“m:num = n”)
90 (AP_TERM (“SUC”)
91 (ASSUME (“m:num = n”)))));
92
93(*---------------------------------------------------------------------------
94 * First we define a partial inverse to SUC called PRE such that:
95 *
96 * (PRE 0 = 0) /\ (!m. PRE(SUC m) = m)
97 *---------------------------------------------------------------------------*)
98val PRE_DEF = new_definition("PRE_DEF",
99 “PRE m = (if (m=0) then 0 else @n. m = SUC n)”);
100val _ = OpenTheoryMap.OpenTheory_const_name{
101 const={Thy="prim_rec",Name="PRE"},
102 name=(["Number","Natural"],"pre")
103 }
104
105Theorem PRE:
106 (PRE 0 = 0) /\ (!m. PRE(SUC m) = m)
107Proof
108 REPEAT STRIP_TAC
109 THEN REWRITE_TAC[PRE_DEF, INV_SUC_EQ, NOT_SUC, SELECT_REFL_2]
110QED
111
112Theorem LESS_REFL: !n. ~(n < n)
113Proof
114 GEN_TAC THEN
115 REWRITE_TAC[LESS_DEF, NOT_AND]
116QED
117
118
119Theorem SUC_LESS:
120 !m n. (SUC m < n) ==> m < n
121Proof
122 REWRITE_TAC[LESS_DEF]
123 THEN REPEAT STRIP_TAC
124 THEN EXISTS_TAC (“P:num->bool”)
125 THEN RES_TAC
126 THEN ASM_REWRITE_TAC[]
127QED
128
129Theorem NOT_LESS_0:
130 !n. ~(n < 0)
131Proof
132 INDUCT_TAC
133 THEN REWRITE_TAC[LESS_REFL]
134 THEN IMP_RES_TAC(CONTRAPOS
135 (SPECL[“n:num”, “0”] SUC_LESS))
136 THEN ASM_REWRITE_TAC[]
137QED
138
139Theorem LESS_0:
140 !n. 0 < (SUC n)
141Proof
142 GEN_TAC
143 THEN REWRITE_TAC[LESS_DEF]
144 THEN EXISTS_TAC (“\x.x = 0”)
145 THEN CONV_TAC(DEPTH_CONV BETA_CONV)
146 THEN REWRITE_TAC[NOT_SUC]
147QED
148
149Theorem LESS_0_0:
150 0 < SUC 0
151Proof
152 REWRITE_TAC[LESS_0]
153QED
154
155Theorem LESS_MONO:
156 !m n. (m < n) ==> (SUC m < SUC n)
157Proof
158 REWRITE_TAC[LESS_DEF]
159 THEN REPEAT STRIP_TAC
160 THEN EXISTS_TAC ``\n : num. P (PRE n) : bool``
161 THEN CONV_TAC(DEPTH_CONV BETA_CONV)
162 THEN ASM_REWRITE_TAC [PRE]
163 THEN INDUCT_TAC (* don't have num_CASES yet *)
164 THEN ASM_REWRITE_TAC [PRE]
165QED
166
167Theorem LESS_MONO_REV:
168 !m n. (SUC m < SUC n) ==> (m < n)
169Proof
170 REWRITE_TAC[LESS_DEF]
171 THEN REPEAT STRIP_TAC
172 THEN EXISTS_TAC ``\n : num. P (SUC n) : bool``
173 THEN CONV_TAC(DEPTH_CONV BETA_CONV)
174 THEN ASM_REWRITE_TAC []
175QED
176
177Theorem LESS_MONO_EQ:
178 !m n. (SUC m < SUC n) = (m < n)
179Proof
180 REPEAT GEN_TAC THEN EQ_TAC
181 THEN REWRITE_TAC [LESS_MONO, LESS_MONO_REV]
182QED
183
184(* now show that < is the transitive closure of the successor relation *)
185
186Theorem TC_LESS_0[local]:
187 !n. TC (\x y. y = SUC x) 0 (SUC n)
188Proof
189 INDUCT_TAC
190 THENL [ irule relationTheory.TC_SUBSET THEN BETA_TAC THEN REFL_TAC,
191 ONCE_REWRITE_TAC [relationTheory.TC_CASES2] THEN DISJ2_TAC
192 THEN EXISTS_TAC ``SUC n`` THEN BETA_TAC THEN ASM_REWRITE_TAC [] ]
193QED
194
195Theorem TC_NOT_LESS_0[local]:
196 !n. ~(TC (\x y. y = SUC x) n 0)
197Proof
198 ONCE_REWRITE_TAC [relationTheory.TC_CASES2]
199 THEN BETA_TAC THEN REWRITE_TAC [GSYM NOT_SUC]
200QED
201
202Theorem TC_IM_RTC_SUC:
203 !m n. TC (\x y. y = SUC x) m (SUC n) = RTC (\x y. y = SUC x) m n
204Proof
205 ONCE_REWRITE_TAC [relationTheory.TC_CASES2] THEN BETA_TAC
206 THEN REWRITE_TAC [relationTheory.RTC_CASES_TC, INV_SUC_EQ]
207 THEN REPEAT (STRIP_TAC ORELSE EQ_TAC)
208 THEN ASM_REWRITE_TAC []
209 THEN DISJ2_TAC THEN EXISTS_TAC ``n : num``
210 THEN ASM_REWRITE_TAC []
211QED
212
213Theorem RTC_IM_TC:
214 !m n. RTC (\x y. y = f x) (f m) n = TC (\x y. y = f x) m n
215Proof
216 REWRITE_TAC [relationTheory.EXTEND_RTC_TC_EQN]
217 THEN BETA_TAC THEN REPEAT (STRIP_TAC ORELSE EQ_TAC)
218 THENL [Q.EXISTS_TAC `f m`,
219 FIRST_X_ASSUM (ASSUME_TAC o SYM)]
220 THEN ASM_REWRITE_TAC []
221QED
222
223Theorem TC_LESS_MONO_EQ[local]:
224 !m n. TC (\x y. y = SUC x) (SUC m) (SUC n) = TC (\x y. y = SUC x) m n
225Proof
226 REWRITE_TAC [TC_IM_RTC_SUC, RTC_IM_TC]
227QED
228
229Theorem LESS_ALT:
230 $< = TC (\x y. y = SUC x)
231Proof
232 REWRITE_TAC [FUN_EQ_THM] THEN
233 INDUCT_TAC THEN INDUCT_TAC THEN
234 REWRITE_TAC [NOT_LESS_0, TC_NOT_LESS_0, LESS_0, TC_LESS_0,
235 TC_LESS_MONO_EQ, LESS_MONO_EQ]
236 THEN FIRST_ASSUM MATCH_ACCEPT_TAC
237QED
238
239Theorem LESS_SUC_REFL:
240 !n. n < SUC n
241Proof
242 INDUCT_TAC
243 THEN REWRITE_TAC[LESS_0_0]
244 THEN IMP_RES_TAC LESS_MONO
245 THEN ASM_REWRITE_TAC[]
246QED
247
248Theorem LESS_SUC:
249 !m n. (m < n) ==> (m < SUC n)
250Proof
251 REWRITE_TAC [LESS_DEF]
252 THEN REPEAT STRIP_TAC
253 THEN EXISTS_TAC (“P:num->bool”)
254 THEN IMP_RES_TAC
255 (CONTRAPOS(SPEC (“(n:num)”)
256 (ASSUME (“ !n'. P(SUC n') ==> P n' ”))))
257 THEN ASM_REWRITE_TAC[]
258QED
259
260Theorem LESS_LEMMA1:
261 !m n. (m < SUC n) ==> (m = n) \/ (m < n)
262Proof
263 REWRITE_TAC [LESS_ALT, TC_IM_RTC_SUC, relationTheory.RTC_CASES_TC]
264QED
265
266Theorem LESS_LEMMA2:
267 !m n. ((m = n) \/ (m < n)) ==> (m < SUC n)
268Proof
269 REPEAT STRIP_TAC
270 THEN (IMP_RES_TAC LESS_SUC)
271 THEN ASM_REWRITE_TAC[LESS_SUC_REFL]
272QED
273
274(* |- !m n. m < (SUC n) = (m = n) \/ m < n *)
275Theorem LESS_THM =
276 GENL [“m:num”, “n:num”]
277 (IMP_ANTISYM_RULE(SPEC_ALL LESS_LEMMA1)
278 (SPEC_ALL LESS_LEMMA2));
279
280Theorem LESS_SUC_IMP:
281 !m n. (m < SUC n) ==> ~(m = n) ==> (m < n)
282Proof
283 REWRITE_TAC[LESS_THM]
284 THEN REPEAT STRIP_TAC
285 THEN RES_TAC
286 THEN ASM_REWRITE_TAC[]
287QED
288
289Theorem EQ_LESS:
290 !n. (SUC m = n) ==> (m < n)
291Proof
292 INDUCT_TAC
293 THEN REWRITE_TAC[NOT_SUC, LESS_THM]
294 THEN DISCH_TAC
295 THEN IMP_RES_TAC INV_SUC
296 THEN ASM_REWRITE_TAC[]
297QED
298
299Theorem SUC_ID:
300 !n. ~(SUC n = n)
301Proof
302 INDUCT_TAC
303 THEN ASM_REWRITE_TAC[NOT_SUC, INV_SUC_EQ]
304QED
305
306Theorem NOT_LESS_EQ:
307 !m n. (m = n) ==> ~(m < n)
308Proof
309 REPEAT GEN_TAC
310 THEN DISCH_TAC
311 THEN ASM_REWRITE_TAC[LESS_REFL]
312QED
313
314Theorem LESS_NOT_EQ:
315 !m n. (m < n) ==> ~(m = n)
316Proof
317 REPEAT STRIP_TAC
318 THEN IMP_RES_TAC
319 (DISCH_ALL(SUBS[ASSUME (“(m:num) = n”)]
320 (ASSUME (“m < n”))))
321 THEN IMP_RES_TAC LESS_REFL
322 THEN RES_TAC
323 THEN ASM_REWRITE_TAC[]
324QED
325
326(*---------------------------------------------------------------------------
327 * Now we will prove that:
328 *
329 * |- !x f. ?fun.
330 * (fun 0 = x) /\
331 * (!m. fun(SUC m) = f(fun m)m)
332 *
333 * We start by defining a (higher order) function SIMP_REC and
334 * proving that:
335 *
336 * |- !m x f.
337 * (SIMP_REC x f 0 = x) /\
338 * (SIMP_REC x f (SUC m) = f(SIMP_REC x f m))
339 *
340 * We then define a function PRIM_REC in terms of SIMP_REC and prove that:
341 *
342 * |- !m x f.
343 * (PRIM_REC x f 0 = x) /\
344 * (PRIM_REC x f (SUC m) = f (PRIM_REC x f m) m)
345 *
346 * This is sufficient to justify any primitive recursive definition
347 * because a definition:
348 *
349 * fun 0 x1 ... xn = f1(x1, ... ,xn)
350 *
351 * fun (SUC m) x1 ... xn = f2(fun m x1 ... xn, m, x1, ... ,xn)
352 *
353 * is equivalent to:
354 *
355 * fun 0 = \x1 ... xn. f1(x1, ... ,xn)
356 *
357 * fun (SUC m) = \x1 ... xn. f2(fun m x1 ... xn, m, x1, ... ,xn)
358 * = (\f m x1 ... xn. f2(f x1 ... xn, m, x1, ... ,xn))(fun m)m
359 *
360 * which defines fun to be:
361 *
362 * PRIM_REC
363 * (\x1 ... xn. f1(x1, ... ,xn))
364 * (\f m x1 ... xn. f2(f x1 ... xn, m, x1, ... ,xn))
365 *---------------------------------------------------------------------------*)
366
367val SIMP_REC_REL =
368 new_definition
369 ("SIMP_REC_REL",
370 “!(fun:num->'a) (x:'a) (f:'a->'a) (n:num).
371 SIMP_REC_REL fun x f n <=>
372 (fun 0 = x) /\
373 !m. (m < n) ==> (fun(SUC m) = f(fun m))”);
374
375Theorem SIMP_REC_EXISTS:
376 !x f n. ?fun:num->'a. SIMP_REC_REL fun x f n
377Proof
378 GEN_TAC THEN GEN_TAC THEN INDUCT_THEN INDUCTION STRIP_ASSUME_TAC THEN
379 PURE_REWRITE_TAC[SIMP_REC_REL] THENL [
380 EXISTS_TAC (“\p:num. (x:'a)”) THEN REWRITE_TAC[NOT_LESS_0],
381 Q.EXISTS_TAC `\p. if p = SUC n then f (fun n) else fun p` THEN
382 BETA_TAC THEN REWRITE_TAC [INV_SUC_EQ, GSYM NOT_SUC] THEN
383 POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE [SIMP_REC_REL]) THEN
384 ASM_REWRITE_TAC [] THEN REPEAT STRIP_TAC THEN
385 Q.ASM_CASES_TAC `m = SUC n` THENL [
386 POP_ASSUM SUBST_ALL_TAC THEN IMP_RES_TAC LESS_REFL,
387 ALL_TAC
388 ] THEN ASM_REWRITE_TAC [] THEN COND_CASES_TAC THEN
389 ASM_REWRITE_TAC [] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
390 IMP_RES_TAC LESS_SUC_IMP
391 ]
392QED
393
394Theorem SIMP_REC_REL_UNIQUE:
395 !x f g1 g2 m1 m2.
396 SIMP_REC_REL g1 x f m1 /\ SIMP_REC_REL g2 x f m2 ==>
397 !n. n < m1 /\ n < m2 ==> (g1 n = g2 n)
398Proof
399 REWRITE_TAC [SIMP_REC_REL] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
400 INDUCT_THEN INDUCTION STRIP_ASSUME_TAC THEN ASM_REWRITE_TAC [] THEN
401 DISCH_THEN (CONJUNCTS_THEN (ASSUME_TAC o MATCH_MP SUC_LESS)) THEN
402 RES_TAC THEN ASM_REWRITE_TAC []
403QED
404
405Theorem SIMP_REC_REL_UNIQUE_RESULT:
406 !x f n.
407 ?!y. ?g. SIMP_REC_REL g x f (SUC n) /\ (y = g n)
408Proof
409 REPEAT GEN_TAC THEN
410 SIMP_TAC bool_ss [EXISTS_UNIQUE_THM, SIMP_REC_EXISTS] THEN
411 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN
412 ASSUME_TAC (Q.SPEC `n` LESS_SUC_REFL) THEN
413 IMP_RES_TAC SIMP_REC_REL_UNIQUE
414QED
415
416val SIMP_REC = new_specification
417 ("SIMP_REC",["SIMP_REC"],
418 ((CONJUNCT1 o
419 SIMP_RULE bool_ss [EXISTS_UNIQUE_THM] o
420 SIMP_RULE bool_ss [UNIQUE_SKOLEM_THM])
421 SIMP_REC_REL_UNIQUE_RESULT));
422
423Theorem LESS_SUC_SUC:
424 !m. (m < SUC m) /\ (m < SUC(SUC m))
425Proof
426 INDUCT_TAC
427 THEN ASM_REWRITE_TAC[LESS_THM]
428QED
429
430Theorem SIMP_REC_THM:
431 !(x:'a) f.
432 (SIMP_REC x f 0 = x) /\
433 (!m. SIMP_REC x f (SUC m) = f(SIMP_REC x f m))
434Proof
435 REPEAT GEN_TAC THEN
436 ASSUME_TAC (SPECL [Term`x:'a`, Term`f:'a -> 'a`] SIMP_REC) THEN
437 CONJ_TAC THENL [
438 POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE [SIMP_REC_REL] o
439 Q.SPEC `0`) THEN ASM_REWRITE_TAC [],
440 GEN_TAC THEN
441 FIRST_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `SUC m`) THEN
442 FIRST_X_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `m`) THEN
443 ASM_REWRITE_TAC [] THEN
444 Q.SUBGOAL_THEN `g (SUC m) = f (g m)` SUBST1_TAC THENL [
445 FULL_SIMP_TAC bool_ss [SIMP_REC_REL, LESS_SUC_SUC],
446 ALL_TAC
447 ] THEN AP_TERM_TAC THEN STRIP_ASSUME_TAC (Q.SPEC `m` LESS_SUC_SUC) THEN
448 IMP_RES_TAC SIMP_REC_REL_UNIQUE
449 ]
450QED
451
452(*---------------------------------------------------------------------------
453 * We now use simple recursion to prove that:
454 *
455 * |- !x f. ?fun.
456 * (fun ZERO = x) /\
457 * (!m. fun(SUC m) = f(fun m)m)
458 *
459 * We proceed by defining a function PRIM_REC and proving that:
460 *
461 * |- !m x f.
462 * (PRIM_REC x f 0 = x) /\
463 * (PRIM_REC x f (SUC m) = f(PRIM_REC x f m)m)
464 *---------------------------------------------------------------------------*)
465
466
467val PRIM_REC_FUN =
468 new_definition
469 ("PRIM_REC_FUN",
470 “PRIM_REC_FUN (x:'a) (f:'a->num->'a) =
471 SIMP_REC (\n:num. x) (\fun n. f(fun(PRE n))n)”);
472
473Theorem PRIM_REC_EQN:
474 !(x:'a) f.
475 (!n. PRIM_REC_FUN x f 0 n = x) /\
476 (!m n. PRIM_REC_FUN x f (SUC m) n = f (PRIM_REC_FUN x f m (PRE n)) n)
477Proof
478 REPEAT STRIP_TAC
479 THEN REWRITE_TAC [PRIM_REC_FUN, SIMP_REC_THM]
480 THEN CONV_TAC(DEPTH_CONV BETA_CONV)
481 THEN REWRITE_TAC[]
482QED
483
484val PRIM_REC =
485 new_definition
486 ("PRIM_REC",
487 “PRIM_REC (x:'a) f m = PRIM_REC_FUN x f m (PRE m)”);
488
489Theorem PRIM_REC_THM:
490 !x f.
491 (PRIM_REC (x:'a) f 0 = x) /\
492 (!m. PRIM_REC x f (SUC m) = f (PRIM_REC x f m) m)
493Proof
494 REPEAT STRIP_TAC
495 THEN REWRITE_TAC[PRIM_REC, PRIM_REC_FUN, SIMP_REC_THM]
496 THEN CONV_TAC(DEPTH_CONV BETA_CONV)
497 THEN REWRITE_TAC[PRE]
498QED
499
500
501(*---------------------------------------------------------------------------*
502 * The axiom of dependent choice (DC). *
503 *---------------------------------------------------------------------------*)
504
505local
506 val DCkey = BETA_RULE (SPEC
507 (Term`\y. P y /\ R (SIMP_REC a (\x. @y. P y /\ R x y) n) y`)
508 SELECT_AX)
509 val totalDClem = prove
510 (Term`!P R a. P a /\ (!x. P x ==> ?y. P y /\ R x y)
511 ==>
512 !n. P (SIMP_REC a (\x. @y. P y /\ R x y) n)`,
513 REPEAT GEN_TAC THEN STRIP_TAC
514 THEN INDUCT_THEN numTheory.INDUCTION ASSUME_TAC
515 THEN ASM_REWRITE_TAC [SIMP_REC_THM]
516 THEN BETA_TAC THEN RES_TAC THEN IMP_RES_TAC DCkey)
517in
518Theorem DC: !P R a.
519 P a /\ (!x. P x ==> ?y. P y /\ R x y)
520 ==>
521 ?f. (f 0 = a) /\ (!n. P (f n) /\ R (f n) (f (SUC n)))
522Proof
523REPEAT STRIP_TAC
524 THEN EXISTS_TAC (Term`SIMP_REC a (\x. @y. P y /\ R x y)`)
525 THEN REWRITE_TAC [SIMP_REC_THM] THEN BETA_TAC THEN GEN_TAC
526 THEN SUBGOAL_THEN
527 (Term`P (SIMP_REC a (\x. @y. P y /\ R x y) n)`) ASSUME_TAC THENL
528 [MATCH_MP_TAC totalDClem THEN ASM_REWRITE_TAC[],
529 ASM_REWRITE_TAC[] THEN RES_THEN MP_TAC THEN DISCH_THEN (K ALL_TAC)
530 THEN DISCH_THEN (CHOOSE_THEN (ACCEPT_TAC o CONJUNCT2 o MATCH_MP DCkey))]
531QED
532end;
533
534
535(*----------------------------------------------------------------------*)
536(* Unique existence theorem for prim rec definitions on num. *)
537(* *)
538(* ADDED TFM 88.04.02 *)
539(*----------------------------------------------------------------------*)
540
541Theorem num_Axiom_old:
542 !e:'a. !f. ?! fn1. (fn1 0 = e) /\
543 (!n. fn1 (SUC n) = f (fn1 n) n)
544Proof
545 REPEAT GEN_TAC THEN
546 CONV_TAC EXISTS_UNIQUE_CONV THEN CONJ_TAC THENL
547 [EXISTS_TAC “PRIM_REC (e:'a) (f:'a->num->'a)” THEN
548 REWRITE_TAC [PRIM_REC_THM],
549 CONV_TAC (DEPTH_CONV BETA_CONV) THEN
550 REPEAT STRIP_TAC THEN
551 CONV_TAC FUN_EQ_CONV THEN
552 INDUCT_TAC THEN ASM_REWRITE_TAC []]
553QED
554
555Theorem num_Axiom:
556 !(e:'a) f. ?fn. (fn 0 = e) /\ !n. fn (SUC n) = f n (fn n)
557Proof
558 REPEAT GEN_TAC THEN
559 STRIP_ASSUME_TAC
560 (CONV_RULE EXISTS_UNIQUE_CONV
561 (SPECL [Term`e:'a`, Term`\a:'a n:num. f n a:'a`] num_Axiom_old)) THEN
562 EXISTS_TAC (Term`fn1 : num -> 'a`) THEN
563 RULE_ASSUM_TAC BETA_RULE THEN ASM_REWRITE_TAC []
564QED
565
566val [num_case_def] = Prim_rec.define_case_constant num_Axiom
567Overload case = “num_CASE”
568
569val _ = TypeBase.export $ TypeBasePure.gen_datatype_info
570 {ax=num_Axiom, case_defs=[num_case_def], ind=INDUCTION}
571
572
573(*---------------------------------------------------------------------------*
574 * Wellfoundedness taken as no infinite descending chains in 'a. This defn *
575 * is conceptually simpler (to some) than the original definition of *
576 * wellfoundedness, which is solely in terms of sets (and therefore *
577 * logically simpler). *
578 *---------------------------------------------------------------------------*)
579
580val wellfounded_def =
581Q.new_definition
582 ("wellfounded_def",
583 `wellfounded (R:'a->'a->bool) = ~?f. !n. R (f (SUC n)) (f n)`);
584
585Overload Wellfounded = ``wellfounded``
586
587(*---------------------------------------------------------------------------
588 * First half of showing that the two definitions of wellfoundedness agree.
589 *---------------------------------------------------------------------------*)
590
591Theorem WF_IMP_WELLFOUNDED[local]:
592 !R. WF R ==> wellfounded R
593Proof
594 GEN_TAC THEN CONV_TAC CONTRAPOS_CONV
595 THEN REWRITE_TAC[wellfounded_def,relationTheory.WF_DEF]
596 THEN STRIP_TAC
597 THEN Ho_Rewrite.REWRITE_TAC
598 [NOT_FORALL_THM,NOT_EXISTS_THM,boolTheory.NOT_IMP,DE_MORGAN_THM]
599 THEN Q.EXISTS_TAC`\p:'a. ?n:num. p = f n`
600 THEN BETA_TAC THEN CONJ_TAC THENL
601 [MAP_EVERY Q.EXISTS_TAC [`(f:num->'a) n`, `n`] THEN REFL_TAC,
602 REWRITE_TAC[GSYM IMP_DISJ_THM]
603 THEN GEN_TAC THEN DISCH_THEN (CHOOSE_THEN SUBST1_TAC)
604 THEN Q.EXISTS_TAC`f(SUC n)` THEN ASM_REWRITE_TAC[]
605 THEN Q.EXISTS_TAC`SUC n` THEN REFL_TAC]
606QED
607
608(*---------------------------------------------------------------------------
609 * Second half.
610 *---------------------------------------------------------------------------*)
611
612Theorem WELLFOUNDED_IMP_WF[local]:
613 !R. wellfounded R ==> WF R
614Proof
615 REWRITE_TAC[wellfounded_def,relationTheory.WF_DEF]
616 THEN GEN_TAC THEN CONV_TAC CONTRAPOS_CONV
617 THEN Ho_Rewrite.REWRITE_TAC
618 [NOT_FORALL_THM,NOT_EXISTS_THM,NOT_IMP,DE_MORGAN_THM]
619 THEN REWRITE_TAC [GSYM IMP_DISJ_THM]
620 THEN REPEAT STRIP_TAC
621 THEN Q.EXISTS_TAC`SIMP_REC w (\x. @q. R q x /\ B q)` THEN GEN_TAC
622 THEN Q.SUBGOAL_THEN `!n. B(SIMP_REC w (\x. @q. R q x /\ B q) n)`
623 (ASSUME_TAC o SPEC_ALL)
624 THENL [INDUCT_TAC,ALL_TAC]
625 THEN ASM_REWRITE_TAC[SIMP_REC_THM] THEN BETA_TAC
626 THEN RES_TAC
627 THEN IMP_RES_TAC(BETA_RULE
628 (Q.SPEC `\q. R q (SIMP_REC w (\x. @q. R q x /\ B q) n) /\ B q`
629 boolTheory.SELECT_AX))
630QED
631
632
633Theorem WF_IFF_WELLFOUNDED:
634 !R. WF R = wellfounded R
635Proof
636GEN_TAC THEN EQ_TAC THEN STRIP_TAC
637 THENL [IMP_RES_TAC WF_IMP_WELLFOUNDED,
638 IMP_RES_TAC WELLFOUNDED_IMP_WF]
639QED
640
641
642Theorem WF_PRED:
643 WF \x y. y = SUC x
644Proof
645 REWRITE_TAC[relationTheory.WF_DEF] THEN BETA_TAC THEN GEN_TAC
646 THEN CONV_TAC CONTRAPOS_CONV
647 THEN Ho_Rewrite.REWRITE_TAC
648 [NOT_FORALL_THM,NOT_EXISTS_THM,NOT_IMP,DE_MORGAN_THM]
649 THEN REWRITE_TAC [GSYM IMP_DISJ_THM]
650 THEN DISCH_TAC
651 THEN INDUCT_TAC THEN CCONTR_TAC THEN RULE_ASSUM_TAC (REWRITE_RULE[])
652 THEN RES_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[INV_SUC_EQ, GSYM NOT_SUC])
653 THENL (map FIRST_ASSUM [ACCEPT_TAC, MATCH_MP_TAC])
654 THEN FILTER_ASM_REWRITE_TAC is_eq [] THEN ASM_REWRITE_TAC[]
655QED
656
657
658(*----------------------------------------------------------------------------
659 * This theorem is now a lot nicer as < can be defined as the transitive
660 * closure of predecessor.
661 *---------------------------------------------------------------------------*)
662
663Theorem WF_LESS[simp]: WF $<
664Proof
665 REWRITE_TAC[LESS_ALT, relationTheory.WF_TC_EQN, WF_PRED]
666QED
667
668
669
670(*---------------------------------------------------------------------------
671 * Measure functions are definable as inverse image into (<). Every relation
672 * arising from a measure function is wellfounded, which is really great!
673 *---------------------------------------------------------------------------*)
674
675val measure_def = Q.new_definition ("measure_def", `measure = inv_image $<`);
676val _ = OpenTheoryMap.OpenTheory_const_name{
677 const={Thy="prim_rec",Name="measure"},
678 name=(["Relation"],"measure")
679 }
680
681Theorem WF_measure[simp]: !m. WF (measure m)
682Proof
683REWRITE_TAC[measure_def]
684 THEN MATCH_MP_TAC relationTheory.WF_inv_image
685 THEN ACCEPT_TAC WF_LESS
686QED
687
688Theorem measure_thm[simp]:
689 !f x y. measure f x y <=> f x < f y
690Proof
691 REWRITE_TAC [measure_def,relationTheory.inv_image_def] THEN BETA_TAC THEN
692 REWRITE_TAC []
693QED