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