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 640Theorem measure_thm[simp]: 641 !f x y. measure f x y <=> f x < f y 642Proof 643 REWRITE_TAC [measure_def,relationTheory.inv_image_def] THEN BETA_TAC THEN 644 REWRITE_TAC [] 645QED 646 647val _ = export_theory() ; 648