1open HolKernel Parse boolLib bossLib 2 3open listTheory rich_listTheory 4open primrecfnsTheory 5 6open lcsymtacs 7 8val _ = new_theory "recursivefns" 9 10val minimise_def = Define` 11 minimise f l = 12 if (���n. (f (n::l) = SOME 0) ��� ���i. i < n ��� ���m. 0 < m ��� (f (i::l) = SOME m)) 13 then 14 SOME (@n. (f (n :: l) = SOME 0) ��� 15 ���i. i < n ��� ���m. 0 < m ��� (f (i::l) = SOME m)) 16 else NONE 17`; 18 19val recCn_def = Define` 20 recCn (f:num list -> num option) gs l = 21 let results = MAP (��g : num list -> num option. g l) gs 22 in 23 if EVERY (��r. r ��� NONE) results then f (MAP THE results) 24 else NONE 25`; 26 27val recPr_def = Define` 28 recPr zf sf l = 29 case l of 30 [] => zf [] 31 | 0::t => zf t 32 | SUC n::t => case recPr zf sf (n :: t) of 33 NONE => NONE 34 | SOME r => sf (n::r::t) 35`; 36 37val (recfn_rules, recfn_ind, recfn_cases) = Hol_reln` 38 recfn (SOME o K 0) 1 ��� 39 recfn (SOME o succ) 1 ��� 40 (���i n. i < n ��� recfn (SOME o proj i) n) ��� 41 (���f gs m. recfn f (LENGTH gs) ��� EVERY (��g. recfn g m) gs ��� 42 recfn (recCn f gs) m) ��� 43 (���zf sf n. recfn zf (n - 1) ��� recfn sf (n + 1) ��� recfn (recPr zf sf) n) ��� 44 (���f n. 0 < n ��� recfn f (n + 1) ��� recfn (minimise f) n) 45`; 46 47val recfn_rulesl = CONJUNCTS recfn_rules 48val recfnCn = save_thm("recfnCn", List.nth(recfn_rulesl, 3)) 49val recfnPr = save_thm("recfnPr", List.nth(recfn_rulesl, 4)) 50 51val primrec_recfn = store_thm( 52 "primrec_recfn", 53 ``���f n. primrec f n ��� recfn (SOME o f) n``, 54 Induct_on ���primrec��� >> SRW_TAC [][recfn_rules] THENL [ 55 `SOME o Cn f gs = recCn (SOME o f) (MAP (��g. SOME o g) gs)` 56 by SRW_TAC [][FUN_EQ_THM, recCn_def, LET_THM, MAP_MAP_o, 57 combinTheory.o_ABS_R, EVERY_MAP, Cn_def] THEN 58 SRW_TAC [][] THEN MATCH_MP_TAC recfnCn THEN 59 SRW_TAC [][EVERY_MAP] THEN FULL_SIMP_TAC (srw_ss()) [EVERY_MEM], 60 61 `SOME o Pr f f' = recPr (SOME o f) (SOME o f')` 62 by (SIMP_TAC (srw_ss()) [FUN_EQ_THM] THEN Q.X_GEN_TAC `list` THEN 63 `(list = []) ��� ���m ms. list = m :: ms` 64 by (Cases_on `list` THEN SRW_TAC [][]) 65 THEN1 SRW_TAC [][Once recPr_def, Once Pr_def] THEN 66 SRW_TAC [][] THEN 67 Induct_on `m` THEN SRW_TAC [][Once recPr_def] THEN 68 POP_ASSUM (SUBST1_TAC o SYM) THEN SRW_TAC [][]) THEN 69 SRW_TAC [][] THEN MATCH_MP_TAC recfnPr THEN SRW_TAC [ARITH_ss][] 70 ]); 71 72val minimise_thm = Q.store_thm( 73 "minimise_thm", 74 `minimise f l = 75 some n. (f (n::l) = SOME 0) ��� (���i. i<n ��� ���m. 0<m ��� (f (i::l) = SOME m))`, 76 simp[minimise_def] >> DEEP_INTRO_TAC optionTheory.some_intro >> rw[] 77 >- metis_tac[] >> 78 SELECT_ELIM_TAC >> rw[] >> 79 metis_tac[arithmeticTheory.LESS_LESS_CASES, prim_recTheory.LESS_REFL, 80 optionTheory.SOME_11]); 81 82val totalrec_def = Define` 83 totalrec f n = recfn f n ��� ���l. (LENGTH l = n) ��� ���m. f l = SOME m 84`; 85 86val rec1_def = Define` 87 (rec1 f [] = f 0 : num option) ��� 88 (rec1 f (x::t) = f x) 89`; 90 91val rec2_def = Define` 92 (rec2 f [] = f 0 0 : num option) ��� 93 (rec2 f [x] = f x 0) ��� 94 (rec2 f (x::y::t) = f x y) 95`; 96val _ = export_rewrites ["rec2_def"] 97 98val recfn_K = store_thm( 99 "recfn_K[simp]", 100 ``recfn (K (SOME i)) 1``, 101 `recfn (SOME o K i) 1` by simp[primrec_recfn] >> fs[]); 102 103val MAP_CONG' = REWRITE_RULE [GSYM AND_IMP_INTRO] MAP_CONG 104 105val recfn_short_extended = Q.store_thm( 106 "recfn_short_extended", 107 `���f n. recfn f n ��� 108 ���xs. LENGTH xs ��� n ��� 109 (f (xs ++ GENLIST (K 0) (n - LENGTH xs)) = f xs)`, 110 Induct_on `recfn` >> simp[] >> rpt strip_tac 111 >- (Cases_on `xs` >> simp[succ_def]) 112 >- (qid_spec_tac`xs` >> Induct_on `n` >> simp[proj_def] >> rw[] >> 113 simp[EL_APPEND_EQN]) 114 >- (simp[recCn_def] >> fs[EVERY_MEM] >> COND_CASES_TAC >> fs[MEM_MAP] 115 >- (COND_CASES_TAC >- simp[Cong MAP_CONG'] >> fs[] >> metis_tac[]) 116 >- metis_tac[]) 117 >- (Cases_on `xs` >> simp_tac (srw_ss ())[] 118 >- (ONCE_REWRITE_TAC[recPr_def] >> Cases_on `n` >> simp[GENLIST_CONS] >> 119 last_x_assum (qspec_then `[]` mp_tac) >> simp[]) 120 >- (fs[] >> Induct_on`h` >> simp[] 121 >- (ONCE_REWRITE_TAC[recPr_def] >> 122 last_x_assum (qspec_then `t` mp_tac) >> 123 simp[arithmeticTheory.ADD1]) >> 124 ONCE_REWRITE_TAC[recPr_def] >> simp[] >> 125 rename [���option_CASE (recPr f g (h::t))���] >> 126 Cases_on`recPr f g (h::t)` >> simp[] >> 127 rename [���g (h1::h2::(t ++ GENLIST _ _))���] >> 128 first_x_assum(qspec_then `h1::h2::t`mp_tac) >> 129 simp[arithmeticTheory.ADD1])) 130 >- (simp[minimise_thm] >> rename [���_ (xs ++ GENLIST (K 0) _)���] >> 131 first_x_assum(qspec_then`j::xs` (mp_tac o Q.GEN`j`)) >> 132 simp[arithmeticTheory.ADD1])) 133 134val recfn_nonzero = Q.store_thm( 135 "recfn_nonzero", 136 ������f n. recfn f n ��� n ��� 0���, 137 Induct_on ���recfn��� >> rw[] >> rename [���gs ��� []���] >> 138 Cases_on ���gs��� >> fs[]); 139 140val recfn_long_truncated = Q.store_thm( 141 "recfn_long_truncated", 142 `���f n. recfn f n ��� ���l. n ��� LENGTH l ��� (f (TAKE n l) = f l)`, 143 Induct_on`recfn` >> simp[] >> rpt strip_tac 144 >- (Cases_on `l` >> fs[succ_def]) 145 >- (simp[proj_def,EL_TAKE]) 146 >- (simp[recCn_def] >> fs[EVERY_MEM] >> COND_CASES_TAC >> fs[MEM_MAP] 147 >- (COND_CASES_TAC >-(simp[Cong MAP_CONG']) >> fs[] >> metis_tac[]) 148 >- metis_tac[]) 149 >- (rename [���recfn f (n - 1)���, ���recfn g (n + 1)���, ���TAKE n l���] >> 150 ���n - 1 ��� 0��� by metis_tac[recfn_nonzero] >> ���2 ��� n��� by simp[] >> 151 ������h t. l = h::t��� by (Cases_on ���l��� >> fs[]) >> rw[] >> fs[] >> 152 Induct_on ���h��� >> ONCE_REWRITE_TAC [recPr_def] >> simp[] >> 153 Cases_on ���recPr f g (h::t)��� >> simp[] >> 154 first_x_assum 155 (qspec_then ���h1::h2::t��� 156 (irule o 157 SIMP_RULE (srw_ss() ++ ARITH_ss) 158 [listTheory.TAKE_def, ASSUME ���2 ��� n���] o 159 Q.GENL [���h1���, ���h2���])) >> simp[]) 160 >- (simp[minimise_thm] >> rename [���f (TAKE (n + 1) _)���, ���n ��� LENGTH xs���] >> 161 first_x_assum(qspec_then`j::xs` (mp_tac o Q.GEN`j`)) >> 162 simp[arithmeticTheory.ADD1])); 163 164val unary_recfn_eq = Q.store_thm( 165 "unary_recfn_eq", 166 `recfn f 1 ��� (���n. f [n] = g n) ��� (f = rec1 g)`, 167 strip_tac >> simp[FUN_EQ_THM] >> Cases >> simp[rec1_def] 168 >- (drule_then (qspec_then `[]` mp_tac) recfn_short_extended >> simp[]) 169 >- (drule_then (qspec_then ���h::t��� mp_tac) recfn_long_truncated >> simp[])) 170 171val recfn_rec1 = Q.store_thm( 172 "recfn_rec1", 173 `(���g. recfn g 1 ��� ���n. g [n] = f n) ��� recfn (rec1 f) 1`, 174 metis_tac[unary_recfn_eq]); 175 176val _ = export_theory() 177