1open HolKernel Parse boolLib bossLib; 2 3open numpairTheory primrecfnsTheory nlistTheory arithmeticTheory listTheory 4 recursivefnsTheory 5 6val _ = new_theory "unary_recfns"; 7 8val _ = monadsyntax.enable_monadsyntax() 9val _ = monadsyntax.enable_monad "option" 10 11Definition pr1_pr_def: 12 pr1_pr b s n = 13 if nfst n = 0 then b (nsnd n) 14 else 15 s ((nfst n - 1) ��� pr1_pr b s ((nfst n - 1) ��� nsnd n) ��� nsnd n) 16Termination 17 WF_REL_TAC ���measure (��(b,s,n). nfst n)��� >> simp[] 18End 19 20Theorem pr1_pr_thm[simp]: 21 pr1_pr b s (0 ��� v) = b v ��� 22 pr1_pr b s (SUC n ��� v) = s (n ��� pr1_pr b s (n ��� v) ��� v) ��� 23 pr1_pr b s ((n + 1) ��� v) = s (n ��� pr1_pr b s (n ��� v) ��� v) 24Proof 25 csimp[GSYM ADD1] >> conj_tac >> 26 simp[Once pr1_pr_def, SimpLHS] 27QED 28 29 30Inductive primrec1: 31 primrec1 (K 0) ��� 32 primrec1 SUC ��� 33 primrec1 nfst ��� 34 primrec1 nsnd ��� 35 (���f g. primrec1 f ��� primrec1 g ��� primrec1 (��n. f n ��� g n)) ��� 36 (���f g. primrec1 f ��� primrec1 g ��� primrec1 (f o g)) ��� 37 (���b s. primrec1 b ��� primrec1 s ��� primrec1 (pr1_pr b s)) 38End 39 40Theorem primrec1_I[simp]: 41 primrec1 I ��� primrec1 (��x. x) 42Proof 43 ���I = (��x:num. x)��� by simp[FUN_EQ_THM] >> simp[] >> 44 ���primrec1 (��n. nfst n ��� nsnd n)��� by metis_tac[primrec1_rules] >> 45 fs[] 46QED 47 48Theorem primrec1_add: 49 primrec1 (��n. nfst n + nsnd n) 50Proof 51 ���primrec1 (SUC o nfst o nfst)��� by metis_tac[primrec1_rules] >> 52 qabbrev_tac ���ADD = pr1_pr I (SUC o nfst o nsnd)��� >> 53 ���primrec1 ADD��� by metis_tac[primrec1_rules, primrec1_I] >> 54 ���ADD = (��n. nfst n + nsnd n)��� suffices_by (rw[] >> fs[]) >> 55 simp[FUN_EQ_THM, Abbr���ADD���] >> gen_tac >> 56 ������x y. n = x ��� y��� by metis_tac[npair_cases] >> rw[] >> Induct_on ���x��� >> 57 simp[] 58QED 59 60Theorem primrec_Cn = List.nth (CONJUNCTS primrec_rules, 3) 61 62Theorem primrec1_primrec: 63 ���f. primrec1 f ��� ���g. primrec g 1 ��� ���n. g [n] = f n 64Proof 65 Induct_on ���primrec1��� >> rw[] 66 >- (qexists_tac ���zerof��� >> simp[]) 67 >- (qexists_tac ���succ��� >> simp[primrec_rules]) 68 >- (qexists_tac ���pr1 nfst��� >> simp[primrec_nfst]) 69 >- (qexists_tac ���pr1 nsnd��� >> simp[primrec_nsnd]) 70 >- (rename [���f1 _ ��� f2 _���, ���g1 [_] = f1 _���, ���g2 [_] = f2 _���] >> 71 qexists_tac ���Cn (pr2 npair) [g1; g2]��� >> simp[primrec_rules]) 72 >- (rename [���f1 (f2 _)���, ���g1 [_] = f1 _���, ���g2 [_] = f2 _���] >> 73 qexists_tac ���Cn g1 [g2]���>> simp[primrec_rules]) >> 74 rename [���pr1_pr b1 s1���, ���b [_] = b1 _���, ���s [_] = s1 _���] >> 75 qexists_tac 76 ���Cn (Pr b (Cn s [Cn (pr2 npair) [proj 0; Cn (pr2 npair) [proj 1; proj 2]]])) 77 [pr1 nfst; pr1 nsnd]��� >> 78 conj_tac 79 >- (irule primrec_Cn >> simp[] >> irule alt_Pr_rule >> simp[primrec_rules]) >> 80 gen_tac >> 81 ������x y. n = x ��� y��� by metis_tac[npair_cases] >> rw[] >> Induct_on ���x��� >> 82 simp[] 83QED 84 85Definition unfold_def[simp]: 86 unfold 0 m = [] ��� 87 unfold (SUC n) m = if n = 0 then [m] 88 else nfst m :: unfold n (nsnd m) 89End 90 91Theorem unfold1[simp]: 92 unfold 1 n = [n] 93Proof 94 simp_tac bool_ss [ONE, unfold_def] 95QED 96 97Theorem unfold_LENGTH[simp]: 98 ���m n. LENGTH (unfold m n) = m 99Proof 100 Induct_on ���m��� >> rw[] 101QED 102 103Theorem unfold_EQ_NIL[simp]: 104 unfold a n = [] ��� a = 0 105Proof 106 Cases_on ���a��� >> rw[] 107QED 108 109Definition fold_def[simp]: 110 fold [] = 0 ��� 111 fold [x] = x ��� 112 fold (x::xs) = x ��� fold xs 113End 114 115Theorem fold_unfold[simp]: 116 ���a n. 0 < a ��� fold (unfold a n) = n 117Proof 118 Induct >> rw[] >> 119 Cases_on ���unfold a (nsnd n)��� >> fs[] >> 120 pop_assum (assume_tac o SYM) >> simp[] 121QED 122 123Theorem unfold_fold[simp]: 124 ���l. unfold (LENGTH l) (fold l) = l 125Proof 126 Induct_on ���l��� >> simp[] >> rw[] >> Cases_on ���l��� >> fs[] 127QED 128 129Theorem unfold_fold_alt: 130 n = LENGTH l ��� unfold n (fold l) = l 131Proof 132 simp[] 133QED 134 135Triviality FUNPOW_o: 136 FUNPOW f 0 = I ��� 137 FUNPOW f (SUC n) = f o FUNPOW f n 138Proof 139 simp[FUN_EQ_THM, FUNPOW_SUC] 140QED 141 142Definition foldfs_def[simp]: 143 foldfs [f] n = f n ��� 144 foldfs (f::fs) n = f n ��� foldfs fs n 145End 146 147Theorem foldfs_as_function: 148 foldfs [f] = f ��� 149 foldfs (f::g::fs) = ��n. f n ��� foldfs (g::fs) n 150Proof 151 simp[FUN_EQ_THM] 152QED 153 154Theorem primrec1_foldfs: 155 fs ��� [] ��� (���f. MEM f fs ��� primrec1 f) ��� primrec1 (foldfs fs) 156Proof 157 Induct_on ���fs��� >> simp[DISJ_IMP_THM, FORALL_AND_THM] >> qx_gen_tac ���f��� >> 158 Cases_on ���fs��� >> fs[foldfs_as_function, DISJ_IMP_THM, FORALL_AND_THM] >> 159 metis_tac[primrec1_rules] 160QED 161 162Theorem unfold_foldfs: 163 ���a fs n. 0 < a ��� LENGTH fs = a ��� unfold a (foldfs fs n) = MAP (��f. f n) fs 164Proof 165 Induct_on ���fs��� >> simp[] >> fs[] >> rw[] 166 >- (Cases_on ���fs��� >> fs[]) >> 167 Cases_on ���fs��� >> fs[] 168QED 169 170Theorem MAP_CONG' = REWRITE_RULE [GSYM AND_IMP_INTRO] MAP_CONG 171 172Theorem primrec_primrec1: 173 ���f a. primrec f a ��� ���g. primrec1 g ��� ���n. g n = f (unfold a n) 174Proof 175 Induct_on ���primrec��� >> rw[] 176 >- (qexists_tac ���K 0��� >> simp[primrec1_rules]) 177 >- (qexists_tac ���SUC��� >> simp[primrec1_rules]) 178 >- (rename [���proj i (unfold a _)���] >> 179 qexists_tac ���(if i + 1 = a then I else nfst) o FUNPOW nsnd i��� >> conj_tac 180 >- (pop_assum (K ALL_TAC) >> 181 ���primrec1 (FUNPOW nsnd i)��� 182 suffices_by metis_tac[primrec1_rules, primrec1_I] >> 183 Induct_on ���i��� >> simp[FUNPOW_o, primrec1_rules]) >> 184 pop_assum mp_tac >> qid_spec_tac ���a��� >> 185 ONCE_REWRITE_TAC [EQ_SYM_EQ] >> 186 Induct_on ���i��� >> simp[] 187 >- (rw[] >> simp[] >> Cases_on ���a��� >> simp[]) >> 188 rw[] 189 >- (simp_tac bool_ss [GSYM ADD1, Once unfold_def] >> 190 simp[Excl "unfold_def"] >> simp[FUNPOW]) >> 191 ������a0. a = SUC a0��� by (Cases_on ���a��� >> fs[]) >> fs[FUNPOW]) 192 >- (fs[listTheory.EVERY_MEM, PULL_EXISTS, GSYM RIGHT_EXISTS_IMP_THM] >> 193 fs[SKOLEM_THM] >> rename [���primrec1 (mk1 _)���] >> 194 rename [���f1 _ = f (unfold (LENGTH gs) _)���] >> 195 qexists_tac ���f1 o foldfs (MAP mk1 gs)��� >> 196 ���gs ��� []��� by (strip_tac >> fs[] >> drule primrec_nzero >> simp[]) >> 197 conj_tac 198 >- simp[primrec1_foldfs, primrec1_rules, MEM_MAP, PULL_EXISTS] >> 199 ���0 < LENGTH gs��� by (CCONTR_TAC >> fs[]) >> 200 simp[Cn_def, unfold_foldfs, MAP_MAP_o, combinTheory.o_ABS_L, 201 Cong MAP_CONG']) >> 202 rename [���b1 _ = b (unfold a _)���, ���s1 _ = s (unfold (a + 2) _)���] >> 203 ���0 < a��� by metis_tac[primrec_nzero] >> 204 qexists_tac ���pr1_pr b1 s1��� >> simp[primrec1_rules] >> 205 simp[GSYM ADD1] >> 206 qx_gen_tac ���N��� >> 207 ������x y. N = x ��� y��� by metis_tac[npair_cases] >> rw[] >> 208 Induct_on ���x��� >> simp[] >> ������n. n + 2 = SUC (SUC n)��� by simp[] >> simp[] 209QED 210 211Theorem primrec_primrec1_fold: 212 ���f a. primrec f a ��� ���g. primrec1 g ��� ���l. LENGTH l = a ��� f l = g (fold l) 213Proof 214 rw[] >> drule_then (qx_choose_then ���G��� strip_assume_tac) primrec_primrec1 >> 215 qexists_tac ���G��� >> rw[] >> rw[unfold_fold] 216QED 217 218Definition recpair_def: 219 recpair f g (n:num) = do i <- f n; j <- g n; return (i ��� j); od 220End 221 222Definition recCn1_def: 223 recCn1 (f:num->num option) g (n:num) = do x <- g n ; f x; od 224End 225 226Definition recPr1_def: 227 recPr1 b s n = if nfst n = 0 then b (nsnd n) 228 else do 229 r <- recPr1 b s ((nfst n - 1) ��� nsnd n) ; 230 s ((nfst n - 1) ��� r ��� nsnd n) 231 od 232Termination 233 WF_REL_TAC ���measure (��(b,s,n). nfst n)��� >> simp[] 234End 235 236Theorem recPr1_thm[simp]: 237 recPr1 b s (0 ��� m) = b m ��� 238 recPr1 b s (SUC n ��� m) = do r <- recPr1 b s (n ��� m) ; 239 s (n ��� r ��� m) ; 240 od 241Proof 242 conj_tac >> simp[Once recPr1_def, SimpLHS] 243QED 244 245Definition recMin1_def: 246 recMin1 f m = 247 OLEAST n. f (n ��� m) = SOME 0 ��� ���i. i < n ��� ���r. f (i ��� m) = SOME r 248End 249 250Inductive recfn1: 251 recfn1 (SOME o K 0) ��� 252 recfn1 (SOME o SUC) ��� 253 recfn1 (SOME o nfst) ��� 254 recfn1 (SOME o nsnd) ��� 255 (���f g. recfn1 f ��� recfn1 g ��� recfn1 (recpair f g)) ��� 256 (���f g. recfn1 f ��� recfn1 g ��� recfn1 (recCn1 f g)) ��� 257 (���b s. recfn1 b ��� recfn1 s ��� recfn1 (recPr1 b s)) ��� 258 (���f. recfn1 f ��� recfn1 (recMin1 f)) 259End 260 261Theorem primrec1_recfn1: 262 ���f. primrec1 f ��� recfn1 (SOME o f) 263Proof 264 Induct_on ���primrec1��� >> rw[recfn1_rules] 265 >- (rename [���f1 _ ��� f2 _���] >> 266 ���recfn1 (recpair (SOME o f1)(SOME o f2))��� by simp[recfn1_rules] >> 267 pop_assum mp_tac >> 268 qmatch_abbrev_tac ���recfn1 F1 ��� recfn1 F2��� >> 269 ���F1 = F2��� suffices_by simp[] >> 270 simp[recpair_def, Abbr���F1���, Abbr���F2���, FUN_EQ_THM]) 271 >- (rename [���SOME o f o g���] >> 272 ���recCn1 (SOME o f) (SOME o g) = SOME o f o g��� 273 suffices_by metis_tac[recfn1_rules] >> 274 simp[FUN_EQ_THM, recCn1_def]) 275 >- (rename [���SOME o pr1_pr b s���] >> 276 ���recPr1 (SOME o b) (SOME o s) = SOME o pr1_pr b s��� 277 suffices_by metis_tac[recfn1_rules] >> 278 simp[FUN_EQ_THM] >> qx_gen_tac ���N��� >> 279 ������x y. N = x ��� y��� by metis_tac[npair_cases] >> rw[] >> 280 Induct_on ���x��� >> simp[]) 281QED 282 283Theorem recfn1_recfn: 284 ���f. recfn1 f ��� recfn (rec1 f) 1 285Proof 286 Induct_on ���recfn1��� >> rw[] >> irule recfn_rec1 287 >- (qexists_tac ���K (SOME 0)��� >> simp[]) 288 >- (qexists_tac ���SOME o succ��� >> simp[recfn_rules]) 289 >- (qexists_tac ���SOME o pr1 nfst��� >> simp[] >> 290 irule primrec_recfn >> simp[]) 291 >- (qexists_tac ���SOME o pr1 nsnd��� >> simp[] >> 292 irule primrec_recfn >> simp[]) 293 >- (rename [���recpair f1 f2���] >> 294 qexists_tac ���recCn (SOME o pr2 npair) [rec1 f1; rec1 f2]��� >> 295 simp[recCn_def, recpair_def, rec1_def] >> conj_tac 296 >- (irule recfnCn >> simp[] >> irule primrec_recfn >> simp[]) >> 297 qx_gen_tac ���N��� >> Cases_on ���f1 N��� >> simp[] >> Cases_on ���f2 N��� >> simp[]) 298 >- (rename [���recCn1 f g _���] >> 299 qexists_tac ���recCn (rec1 f) [rec1 g]��� >> simp[recfn_rules] >> 300 simp[recCn_def, recCn1_def, rec1_def] >> qx_gen_tac ���N��� >> 301 Cases_on ���g N��� >> simp[]) 302 >- (rename [���recPr1 b s _���] >> 303 qexists_tac 304 ���recCn (recPr (rec1 b) 305 (recCn (rec1 s) [ 306 SOME o Cn (pr2 npair) [ 307 proj 0; 308 Cn (pr2 npair) [proj 1; proj 2] 309 ] 310 ])) 311 [SOME o pr1 nfst; SOME o pr1 nsnd]��� >> 312 conj_tac 313 >- (irule recfnCn >> simp[primrec_recfn] >> 314 irule recfnPr >> simp[] >> irule recfnCn >> simp[] >> 315 irule primrec_recfn >> irule primrec_Cn >> 316 simp[primrec_rules]) >> 317 qx_gen_tac ���N��� >> ������x y. N = x ��� y��� by metis_tac[npair_cases] >> 318 rw[recCn_def] >> Induct_on ���x��� >> simp[Once recPr_def, rec1_def] >> 319 Cases_on ���recPr1 b s (x ��� y)��� >> simp[recCn_def, rec1_def]) >> 320 rename [���recMin1 f���] >> 321 qexists_tac 322 ���minimise (recCn (rec1 f) [SOME o Cn (pr2 $*,) [proj 0; proj 1]])��� >> 323 conj_tac 324 >- (irule (last (CONJUNCTS recfn_rules)) >> simp[] >> irule recfnCn >> 325 simp[] >> irule primrec_recfn >> simp[primrec_rules]) >> 326 simp[minimise_def, recMin1_def, recCn_def, rec1_def] >> qx_gen_tac ���N��� >> 327 rw[] 328 >- (simp[whileTheory.OLEAST_EQ_SOME] >> SELECT_ELIM_TAC >> conj_tac 329 >- metis_tac[] >> 330 simp[] >> rw[] >- metis_tac[] >> 331 first_x_assum drule >> simp[PULL_EXISTS]) >> 332 fs[] >> rename [���f (A ��� B) = SOME 0���] >> 333 Cases_on ���f (A ��� B) = SOME 0��� >> simp[] >> 334 qspec_then �����n. f (n ��� B) = SOME 0��� mp_tac WOP >> simp[] >> impl_tac 335 >- metis_tac[] >> 336 disch_then (qx_choose_then ���A0��� strip_assume_tac) >> 337 ���A0 ��� A��� by metis_tac[DECIDE �����(x < y) ��� y ��� x���] >> 338 ������i0. i0 < A0 ��� ���m. f (i0 ��� B) = SOME m ��� m = 0��� by metis_tac[] >> 339 metis_tac[DECIDE ���x < y ��� y ��� z ��� x < z���] 340QED 341 342(* basically, expanding def'n of rec1 *) 343Theorem recfn1_recfn_alt: 344 recfn1 f ��� ���g. recfn g 1 ��� ���n. g [n] = f n 345Proof 346 strip_tac >> drule_then strip_assume_tac recfn1_recfn >> 347 qexists_tac ���rec1 f��� >> simp[rec1_def] 348QED 349 350Definition ofoldfs_def: 351 ofoldfs [f] (n:num) = f n ��� 352 ofoldfs (f::fs) n = do r1 <- f n ; 353 rs <- ofoldfs fs n ; 354 return (r1 ��� rs) ; 355 od 356End 357 358Theorem ofoldfs_thm[simp]: 359 ofoldfs [f] = f ��� 360 ofoldfs (f1::f2::fs) = recpair f1 (ofoldfs (f2::fs)) 361Proof 362 simp[FUN_EQ_THM, recpair_def, ofoldfs_def] 363QED 364 365Theorem ofoldfs_EQ_NONE[simp]: 366 fs ��� [] ��� 367 (ofoldfs fs n = NONE ��� ���f. MEM f fs ��� f n = NONE) 368Proof 369 Induct_on ���fs��� >> simp[] >> Cases_on ���fs��� >> 370 simp[recpair_def, PULL_EXISTS] >> 371 metis_tac[TypeBase.distinct_of ���:�� option���, TypeBase.nchotomy_of ���:�� option���] 372QED 373 374 375Theorem recfn1_ofoldfs: 376 fs ��� [] ��� (���f. MEM f fs ��� recfn1 f) ��� recfn1 (ofoldfs fs) 377Proof 378 Induct_on ���fs��� >> fs[DISJ_IMP_THM, FORALL_AND_THM] >> 379 qx_gen_tac ���f��� >> Cases_on���fs��� >> 380 fs[DISJ_IMP_THM, FORALL_AND_THM, recfn1_rules] 381QED 382 383Theorem ofoldfs_EQ_SOME: 384 fs ��� [] ��� 385 ���l. ofoldfs fs n = SOME l ��� l = fold (MAP (��f. THE (f n)) fs) 386Proof 387 Induct_on ���fs��� >> simp[] >> Cases_on ���fs��� >> fs[] >> 388 simp[recpair_def, PULL_EXISTS] 389QED 390 391Theorem recfn_recfn1: 392 ���f a. recfn f a ��� ���g. recfn1 g ��� ���n. g n = f (unfold a n) 393Proof 394 Induct_on ���recfn��� >> rw[] 395 >- (qexists_tac ���SOME o K 0��� >> simp[recfn1_rules]) 396 >- (qexists_tac ���SOME o SUC��� >> simp[recfn1_rules]) 397 >- (���primrec (proj i) a��� by simp[primrec_rules] >> 398 drule_then (qx_choose_then ���G��� strip_assume_tac) primrec_primrec1 >> 399 qexists_tac ���SOME o G��� >> simp[] >> simp[primrec1_recfn1]) 400 >- (fs[EVERY_MEM, GSYM RIGHT_EXISTS_IMP_THM, PULL_EXISTS, SKOLEM_THM] >> 401 rename [���mk1 _ _ = _ (unfold _ _)���] >> 402 rename [���f1 _ = f (unfold (LENGTH gs) _)���] >> 403 qexists_tac ���recCn1 f1 (ofoldfs (MAP mk1 gs))��� >> 404 ���gs ��� []��� by (strip_tac >> fs[] >> drule recfn_nzero >> simp[]) >> 405 conj_tac 406 >- simp[recfn1_ofoldfs, recfn1_rules, MEM_MAP, PULL_EXISTS] >> 407 ���0 < LENGTH gs��� by (CCONTR_TAC >> fs[]) >> 408 simp[recCn_def, MAP_MAP_o, recCn1_def, EVERY_MEM, MEM_MAP, 409 combinTheory.o_ABS_R] >> qx_gen_tac ���N��� >> 410 Cases_on���ofoldfs (MAP mk1 gs) N��� >> simp[] 411 >- (rfs[MEM_MAP] >> rw[] >> qpat_x_assum ���mk1 _ N = NONE��� mp_tac >> 412 simp[] >> metis_tac[]) >> 413 ������g. NONE ��� g (unfold a N) ��� ��MEM g gs��� 414 by (CCONTR_TAC >> fs[] >> rename [���MEM G gs���] >> 415 ���NONE = mk1 G N��� by metis_tac[] >> 416 metis_tac[MEM_MAP, ofoldfs_EQ_NONE, MAP_EQ_NIL, 417 TypeBase.distinct_of ���:�� option���]) >> 418 simp[] >> 419 ���MAP mk1 gs ��� []��� by simp[] >> 420 drule_all ofoldfs_EQ_SOME >> 421 rw[MAP_MAP_o, combinTheory.o_ABS_L, unfold_fold_alt] >> 422 simp[Cong MAP_CONG'] >> fs[] >> metis_tac[]) 423 >- (rename [���b1 _ = b (unfold (a-1) _)���, ���s1 _ = s (unfold (a + 1) _)���] >> 424 ���0 < a-1��� by metis_tac[recfn_nzero] >> 425 qexists_tac ���recPr1 b1 s1��� >> simp[recfn1_rules] >> 426 qx_gen_tac ���N��� >> 427 ������x y. N = x ��� y��� by metis_tac[npair_cases] >> rw[] >> 428 Induct_on ���x��� >> simp[] 429 >- (������a0. a = SUC a0��� by (Cases_on ���a��� >> fs[]) >> 430 simp[unfold_def, Once recPr_def]) >> 431 ������a0. a = SUC a0��� by (Cases_on ���a��� >> fs[]) >> simp[unfold_def] >> 432 simp[SimpRHS, Once recPr_def] >> simp[GSYM ADD1] >> 433 Cases_on���recPr b s (x::unfold a0 y)��� >> simp[]) 434 >- (rename [���f1 _ = f (unfold _ _)���] >> 435 qexists_tac ���recMin1 f1��� >> simp[recfn1_rules] >> 436 simp[recMin1_def, minimise_def, GSYM ADD1] >> qx_gen_tac ���N��� >> 437 rw[] >> fs[] 438 >- (simp[whileTheory.OLEAST_EQ_SOME] >> SELECT_ELIM_TAC >> 439 conj_tac >- metis_tac[] >> 440 rw[] >- metis_tac[] >> 441 first_x_assum (drule_then strip_assume_tac) >> simp[]) >> 442 rename [���f (n::unfold a N) = SOME 0���] >> 443 Cases_on ���f (n::unfold a N) = SOME 0��� >> simp[] >> 444 qspec_then �����i. f (i::unfold a N) = SOME 0��� mp_tac WOP >> 445 impl_tac >- metis_tac[] >> simp[] >> 446 disch_then (qx_choose_then ���n0��� strip_assume_tac) >> 447 ���n0 ��� n��� by metis_tac[DECIDE �����(x < y) ��� y ��� x���] >> 448 ������i. i < n0 ��� ���m. f (i :: unfold a N) = SOME m ��� m = 0��� by metis_tac[] >> 449 qexists_tac ���i��� >> simp[] >> metis_tac[]) 450QED 451 452Theorem recfn_recfn1_alt: 453 recfn f a ��� ���g. recfn1 g ��� ���l. LENGTH l = a ��� f l = g (fold l) 454Proof 455 metis_tac[unfold_fold, recfn_recfn1] 456QED 457 458val _ = export_theory(); 459