1open HolKernel Parse boolLib bossLib 2 3open numpairTheory 4open arithmeticTheory 5 6fun Store_thm (trip as (n,t,tac)) = store_thm trip before export_rewrites [n] 7fun Save_thm (tup as (n,th)) = save_thm tup before export_rewrites [n] 8 9val _ = new_theory "primrecfns" 10 11val nB_def = Define`(nB T = 1) ��� (nB F = 0)` 12val _ = export_rewrites ["nB_def"] 13 14val nB_11 = Store_thm( 15 "nB_11", 16 ``(nB b1 = nB b2) <=> (b1 <=> b2)``, 17 Cases_on `b1` THEN Cases_on `b2` THEN SRW_TAC [][]); 18 19val mult_nB = Store_thm( 20 "mult_nB", 21 ``nB p * nB q = nB (p ��� q)``, 22 Cases_on `p` THEN SRW_TAC [][]); 23 24val nB_eq0 = Store_thm( 25 "nB_eq0", 26 ``(nB p = 0) ��� ��p``, 27 Cases_on `p` THEN SRW_TAC [][]) 28 29val nB_eq1 = Store_thm( 30 "nB_eq1", 31 ``(nB p = 1) ��� p``, 32 Cases_on `p` THEN SRW_TAC [][]); 33 34val nB_sub1 = Store_thm( 35 "nB_sub1", 36 ``1 - nB p = nB (��p)``, 37 Cases_on `p` THEN SRW_TAC [][]); 38 39val proj_def = Define` 40 proj n l = if LENGTH l <= n then 0 else EL n l 41`; 42 43val proj_thm = Store_thm( 44 "proj_thm", 45 ``(proj n [] = 0) ��� 46 (proj n (h::t) = if n = 0 then h else proj (n - 1) t)``, 47 SRW_TAC [ARITH_ss][proj_def] THEN 48 Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) []); 49 50val succ_def = Define`(succ [] = 1) ��� (succ (h::t) = SUC h)` 51val _ = export_rewrites ["succ_def"] 52 53val Cn_def = Define` 54 Cn (f:num list -> num) (gs:(num list -> num) list) (l:num list) = 55 f (MAP (��g. g l) gs) 56` 57 58val Cn0123 = Store_thm( 59 "Cn0123", 60 ``(Cn f [g] l = f [g l]) ��� 61 (Cn f [g1; g2] l = f [g1 l; g2 l]) ��� 62 (Cn f [g1; g2; g3] l = f [g1 l; g2 l; g3 l])``, 63 SRW_TAC [][Cn_def]); 64 65val Pr_def = Define ` 66 Pr b r l = case l of 67 [] => b [] 68 | (0::t) => b t 69 | (SUC n :: t) => r (n :: Pr b r (n :: t) :: t)` 70 71val Pr_thm = Store_thm( 72 "Pr_thm", 73 ``(Pr b r (0 :: t) = b t) ��� 74 (Pr b r (SUC m :: t) = r (m :: Pr b r (m :: t) :: t)) ��� 75 (Pr b r ((m + 1) :: t) = r (m :: Pr b r (m :: t) :: t)) ��� 76 (Pr b r ((1 + m) :: t) = r (m :: Pr b r (m :: t) :: t))``, 77 REPEAT CONJ_TAC THEN 78 SIMP_TAC bool_ss [Once Pr_def, SimpLHS, ONE, ADD_CLAUSES] THEN 79 SRW_TAC [][]); 80 81val _ = overload_on ("zerof", ``K 0 : num list -> num``) 82 83val (primrec_rules, primrec_ind, primrec_cases) = Hol_reln` 84 primrec zerof 1 ��� 85 primrec succ 1 ��� 86 (���i n. i < n ��� primrec (proj i) n) ��� 87 (���f gs m. primrec f (LENGTH gs) ��� EVERY (��g. primrec g m) gs ��� 88 primrec (Cn f gs) m) ��� 89 (���b r n. primrec b n ��� primrec r (n + 2) ��� primrec (Pr b r) (n + 1)) 90`; 91val primrec_cn = List.nth(CONJUNCTS primrec_rules, 3) 92 93val strong_primrec_ind = save_thm( 94 "strong_primrec_ind", 95 IndDefLib.derive_strong_induction(primrec_rules, primrec_ind)) 96 97 98val primrec_nzero = store_thm( 99 "primrec_nzero", 100 ``���f k. primrec f k ��� 0 < k``, 101 HO_MATCH_MP_TAC primrec_ind THEN SRW_TAC [ARITH_ss][] THEN 102 FULL_SIMP_TAC (srw_ss()) []); 103 104val EL_TAKE = store_thm( 105 "EL_TAKE", 106 ``���i n l. i < n ��� n ��� LENGTH l ��� (EL i l = EL i (TAKE n l))``, 107 Induct THEN Cases_on `l` THEN SRW_TAC [ARITH_ss][]); 108 109val MAP_EQ = store_thm( 110 "MAP_EQ", 111 ``���f g l. (MAP f l = MAP g l) ��� ���e. MEM e l ��� (f e = g e)``, 112 Induct_on `l` THEN SRW_TAC [][] THEN METIS_TAC []); 113 114val TAKE_ID = prove( 115 ``���l n. (LENGTH l = n) ��� (TAKE n l = l)``, 116 Induct THEN SRW_TAC [ARITH_ss][]); 117 118val primrec_arg_too_long = store_thm( 119 "primrec_arg_too_long", 120 ``���f n. primrec f n ��� 121 ���l. n ��� LENGTH l ��� (f l = f (TAKE n l))``, 122 HO_MATCH_MP_TAC primrec_ind THEN SRW_TAC [][] THENL [ 123 Cases_on `l` THEN FULL_SIMP_TAC (srw_ss()) [], 124 SRW_TAC [ARITH_ss][proj_def, EL_TAKE], 125 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN 126 SRW_TAC [][Cn_def, TAKE_ID] THEN AP_TERM_TAC THEN 127 SRW_TAC [][MAP_EQ] THEN 128 FULL_SIMP_TAC (srw_ss()) [listTheory.EVERY_MEM], 129 130 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN 131 `���h t. l = h::t` 132 by (Cases_on `l` THEN FULL_SIMP_TAC (srw_ss()) []) THEN 133 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [ADD1] THEN 134 Induct_on `h` THEN SRW_TAC [][] THEN 135 FIRST_X_ASSUM (Q.SPEC_THEN `h::Pr f f' (h::TAKE n t)::t` 136 MP_TAC) THEN 137 ASM_SIMP_TAC bool_ss [TWO, ONE, listTheory.TAKE_def, 138 listTheory.LENGTH, ADD_CLAUSES] THEN 139 SRW_TAC [][] 140 ]); 141 142open rich_listTheory 143 144val GENLIST1 = prove(``GENLIST f 1 = [f 0]``, 145 SIMP_TAC bool_ss [ONE, GENLIST, SNOC]); 146val GENLIST_CONS = prove( 147 ``GENLIST f (SUC n) = f 0 :: (GENLIST (f o SUC) n)``, 148 Induct_on `n` THEN SRW_TAC [][GENLIST, SNOC]); 149 150val primrec_nil = store_thm( 151 "primrec_nil", 152 ``���f n. primrec f n ��� (f [] = f (GENLIST (K 0) n))``, 153 HO_MATCH_MP_TAC primrec_ind THEN SIMP_TAC (srw_ss()) [GENLIST1] THEN 154 REPEAT CONJ_TAC THENL [ 155 SIMP_TAC bool_ss [Once EQ_SYM_EQ] THEN 156 Induct_on `n` THEN SRW_TAC [][GENLIST_CONS] THEN 157 FIRST_X_ASSUM MATCH_MP_TAC THEN DECIDE_TAC, 158 159 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN SRW_TAC [][Cn_def] THEN 160 AP_TERM_TAC THEN Q.PAT_X_ASSUM `f X = f []` (K ALL_TAC) THEN 161 Induct_on `gs` THEN SRW_TAC [][], 162 163 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN SRW_TAC [][] THEN 164 SRW_TAC [][Once Pr_def, SimpRHS] THEN 165 Cases_on `n` THEN SRW_TAC [][GENLIST1, ADD_CLAUSES, GENLIST_CONS] THEN 166 SRW_TAC [][GSYM ADD1] 167 ]); 168 169val primrec_short = store_thm( 170 "primrec_short", 171 ``���f n. primrec f n ��� 172 ���l. LENGTH l < n ��� (f l = f (l ++ GENLIST (K 0) (n - LENGTH l)))``, 173 HO_MATCH_MP_TAC strong_primrec_ind THEN SIMP_TAC (srw_ss()) [GENLIST1] THEN 174 REPEAT CONJ_TAC THENL [ 175 SRW_TAC [][] THEN 176 `LENGTH l = 0` by DECIDE_TAC THEN 177 FULL_SIMP_TAC (srw_ss()) [LENGTH_NIL, GENLIST1], 178 179 SRW_TAC [][proj_def] THEN 180 SRW_TAC [ARITH_ss][EL_GENLIST, EL_APPEND1, EL_APPEND2], 181 182 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN SRW_TAC [][Cn_def] THEN 183 AP_TERM_TAC THEN 184 Q.PAT_X_ASSUM `���l. LENGTH l < N ��� (f X = f Y)` (K ALL_TAC) THEN 185 Q.PAT_X_ASSUM `primrec f N` (K ALL_TAC) THEN 186 Induct_on `gs` THEN SRW_TAC [][], 187 188 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN SRW_TAC [ARITH_ss][] THEN 189 `(l = []) ��� ���m ms. l = m :: ms` by (Cases_on `l` THEN SRW_TAC [][]) THEN1 190 (SRW_TAC [][] THEN METIS_TAC [primrec_nil, primrec_rules]) THEN 191 SRW_TAC [][] THEN 192 FULL_SIMP_TAC (srw_ss()) [DECIDE ``SUC x < y + 1 <=> x < y``] THEN 193 SRW_TAC [ARITH_ss][ADD1] THEN 194 Induct_on `m` THEN SRW_TAC [][] THEN 195 FIRST_X_ASSUM (Q.SPEC_THEN `m::Pr f f' (m::ms)::ms` MP_TAC) THEN 196 SRW_TAC [ARITH_ss][ADD1] 197 ]); 198 199val alt_Pr_rule = Store_thm( 200 "alt_Pr_rule", 201 ``���b r m. primrec b (m - 1) ��� primrec r (m + 1) ��� primrec (Pr b r) m``, 202 SRW_TAC [][] THEN 203 Cases_on `m` THEN1 (IMP_RES_TAC primrec_nzero THEN 204 FULL_SIMP_TAC (srw_ss()) []) THEN 205 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [ADD1, primrec_rules]); 206 207val primrec_K = Store_thm( 208 "primrec_K", 209 ``���n m. 0 < m ��� primrec (K n) m``, 210 Induct THEN SRW_TAC [][primrec_rules] THENL [ 211 Q_TAC SUFF_TAC `zerof = Cn zerof [proj 0]` THEN1 212 (DISCH_THEN SUBST1_TAC THEN SRW_TAC [][primrec_rules]) THEN 213 SRW_TAC [][FUN_EQ_THM], 214 Q_TAC SUFF_TAC `K (SUC n) = Cn succ [K n]` 215 THEN1 SRW_TAC [][primrec_rules] THEN 216 SRW_TAC [][FUN_EQ_THM] 217 ]); 218 219val Pr1_def = Define` 220 Pr1 n f = Cn (Pr (K n) (Cn f [proj 0; proj 1])) 221 [proj 0; K 0] 222`; 223 224val Pr1_correct = Store_thm( 225 "Pr1_correct", 226 ``(Pr1 n f [0] = n) ��� 227 (Pr1 n f [SUC m] = f [m; Pr1 n f [m]])``, 228 SRW_TAC [][Pr1_def]); 229 230val primrec_Pr1 = Store_thm( 231 "primrec_Pr1", 232 ``primrec f 2 ��� primrec (Pr1 n f) 1``, 233 SRW_TAC [][Pr1_def, primrec_rules, alt_Pr_rule]); 234 235val pr1_def = Define` 236 (pr1 f [] = f 0: num) ��� 237 (pr1 f (x::t) = f x) 238`; 239val _ = export_rewrites ["pr1_def"] 240 241val unary_primrec_eq = store_thm( 242 "unary_primrec_eq", 243 ``primrec f 1 ��� (���n. f [n] = g n) ��� (f = pr1 g)``, 244 SRW_TAC [][] THEN SIMP_TAC (srw_ss()) [FUN_EQ_THM] THEN 245 Q.X_GEN_TAC `l` THEN 246 `(l = []) ��� ���n ns. l = n :: ns` by (Cases_on `l` THEN SRW_TAC [][]) THEN 247 SRW_TAC [][] THENL [ 248 IMP_RES_THEN MP_TAC primrec_nil THEN SRW_TAC [][GENLIST1], 249 IMP_RES_THEN (Q.SPEC_THEN `n::ns` MP_TAC) primrec_arg_too_long THEN 250 SRW_TAC [ARITH_ss][] 251 ]); 252val primrec_pr1 = store_thm( 253 "primrec_pr1", 254 ``(���g. primrec g 1 ��� (���n. g [n] = f n)) ��� primrec (pr1 f) 1``, 255 METIS_TAC [unary_primrec_eq]); 256 257val pr2_def = Define` 258 (pr2 f [] = f 0 0 : num) ��� 259 (pr2 f [x] = f x 0) ��� 260 (pr2 f (x::y::t) = f x y) 261`; 262val _ = export_rewrites ["pr2_def"] 263 264val GENLIST2 = prove( 265 ``GENLIST f 2 = [f 0; f 1]``, 266 SIMP_TAC bool_ss [TWO, ONE, GENLIST, SNOC]); 267val binary_primrec_eq = store_thm( 268 "binary_primrec_eq", 269 ``primrec f 2 ��� (���n m. f [n; m] = g n m) ��� (f = pr2 g)``, 270 SRW_TAC [][] THEN SIMP_TAC (srw_ss()) [FUN_EQ_THM] THEN 271 Q.X_GEN_TAC `l` THEN 272 `(l = []) ��� ���n ns. l = n :: ns` by (Cases_on `l` THEN SRW_TAC [][]) THENL [ 273 SRW_TAC [][] THEN 274 `f [] = f (GENLIST (K 0) 2)` by METIS_TAC [primrec_nil] THEN 275 SRW_TAC [][GENLIST2], 276 277 `(ns = []) ��� ���m ms. ns = m::ms` by (Cases_on `ns` THEN SRW_TAC [][]) THEN 278 SRW_TAC [][] THENL [ 279 IMP_RES_THEN (Q.SPEC_THEN `[n]` MP_TAC) primrec_short THEN 280 SRW_TAC [][GENLIST1], 281 282 IMP_RES_THEN (Q.SPEC_THEN `n::m::ms` MP_TAC) primrec_arg_too_long THEN 283 SRW_TAC [ARITH_ss][] 284 ] 285 ]) 286 287val primrec_pr2 = store_thm( 288 "primrec_pr2", 289 ``(���g. primrec g 2 ��� (���m n. g [m; n] = f m n)) ��� primrec (pr2 f) 2``, 290 METIS_TAC [binary_primrec_eq]); 291 292val primrec_pr_add = Store_thm( 293 "primrec_pr_add", 294 ``primrec (pr2 (+)) 2``, 295 MATCH_MP_TAC primrec_pr2 THEN 296 Q.EXISTS_TAC `Pr (proj 0) (Cn succ [proj 1])` THEN 297 SRW_TAC [][primrec_rules, alt_Pr_rule] THEN 298 Induct_on `m` THEN SRW_TAC [][ADD_CLAUSES]); 299val _ = temp_set_fixity "+." (Infixl 500) 300val _ = temp_overload_on ("+.", ``��n m. Cn (pr2 (+)) [n; m]``) 301 302val primrec_pr_mult = Store_thm( 303 "primrec_pr_mult", 304 ``primrec (pr2 $*) 2``, 305 MATCH_MP_TAC primrec_pr2 THEN 306 Q.EXISTS_TAC `Pr zerof (proj 1 +. proj 2)` THEN 307 SRW_TAC [][primrec_rules, alt_Pr_rule] THEN 308 Induct_on `m` THEN SRW_TAC [][MULT_CLAUSES]); 309val _ = temp_set_fixity "*." (Infixl 600) 310val _ = temp_overload_on ("*.", ``��n m. Cn (pr2 $*) [n; m]``) 311 312val primrec_pr_pred = Store_thm( 313 "primrec_pr_pred", 314 ``primrec (pr1 PRE) 1``, 315 MATCH_MP_TAC primrec_pr1 THEN Q.EXISTS_TAC `Pr1 0 (proj 0)` THEN 316 SRW_TAC [][primrec_rules] THEN 317 Cases_on `n` THEN SRW_TAC [][]); 318 319val _ = overload_on ("pr_iszero", ``pr1 (��n. nB (n = 0))``) 320 321val primrec_pr_iszero = Store_thm( 322 "primrec_pr_iszero", 323 ``primrec pr_iszero 1``, 324 MATCH_MP_TAC primrec_pr1 THEN Q.EXISTS_TAC `Pr1 1 (K 0)` THEN 325 SRW_TAC [][primrec_rules] THEN 326 Cases_on `n` THEN SRW_TAC [][]); 327 328val cflip_def = Define` 329 cflip f = Cn f [proj 1; proj 0] 330`; 331 332val cflip_thm = Store_thm( 333 "cflip_thm", 334 ``cflip f [n; m] = f [m; n]``, 335 SRW_TAC [][cflip_def]); 336val primrec_cflip = Store_thm( 337 "primrec_cflip", 338 ``primrec f 2 ��� primrec (cflip f) 2``, 339 SRW_TAC [][primrec_rules, cflip_def]); 340 341val primrec_pr_sub = Store_thm( 342 "primrec_pr_sub", 343 ``primrec (pr2 $-) 2``, 344 MATCH_MP_TAC primrec_pr2 THEN 345 Q.EXISTS_TAC `cflip (Pr (proj 0) (Cn (pr1 PRE) [proj 1]))` THEN 346 SRW_TAC [][primrec_rules] THEN Induct_on `n` THEN SRW_TAC [ARITH_ss][]) 347val _ = temp_set_fixity "-." (Infixl 500); 348val _ = temp_overload_on ("-.", ``��n m. Cn (pr2 $-) [n; m]``) 349 350val _ = overload_on ("pr_le", ``pr2 (��x y. nB (x ��� y))``) 351val _ = temp_set_fixity "<=." (Infix(NONASSOC, 450)) 352val _ = temp_overload_on ("<=.", ``��n m. Cn pr_le [n; m]``) 353 354val primrec_pr_le = Store_thm( 355 "primrec_pr_le", 356 ``primrec pr_le 2``, 357 MATCH_MP_TAC primrec_pr2 THEN 358 Q.EXISTS_TAC `Cn pr_iszero [pr2 $-]` THEN 359 SRW_TAC [][primrec_rules]); 360 361val pr_eq_def = Define` 362 pr_eq = Cn (pr2 $*) [pr_le; cflip pr_le] 363`; 364 365val pr_eq_thm = Store_thm( 366 "pr_eq_thm", 367 ``pr_eq [n; m] = nB (n = m)``, 368 SRW_TAC [ARITH_ss][pr_eq_def]); 369 370val primrec_pr_eq = Store_thm( 371 "primrec_pr_eq", 372 ``primrec pr_eq 2``, 373 SRW_TAC [][pr_eq_def, primrec_rules]); 374 375val _ = temp_set_fixity "=." (Infix(NONASSOC, 450)) 376val _ = temp_overload_on ("=.", ``��n m. Cn pr_eq [n; m]``) 377 378val pr_cond_def = Define` 379 pr_cond P f g = 380 Cn (proj 0 *. proj 1 +. (K 1 -. proj 0) *. proj 2) [P;f;g] 381`; 382 383val pr_predicate_def = Define` 384 pr_predicate P = ���n. (P n = 0) ��� (P n = 1) 385`; 386 387val Cn_pr_eq_predicate = Store_thm( 388 "Cn_pr_eq_predicate", 389 ``pr_predicate (Cn pr_eq [f; g])``, 390 SRW_TAC [][pr_predicate_def, pr_eq_thm]); 391 392val Cn_pr_le_predicate = Store_thm( 393 "Cn_pr_le_predicate", 394 ``pr_predicate (Cn pr_le [f;g])``, 395 SRW_TAC [][pr_predicate_def]); 396 397val pr_cond_thm = Store_thm( 398 "pr_cond_thm", 399 ``pr_predicate P ��� 400 (pr_cond P f g n = if P n = 1 then f n else g n)``, 401 SRW_TAC [][pr_cond_def, pr_predicate_def] THEN 402 `P n = 0` by METIS_TAC [] THEN 403 SRW_TAC [][]); 404 405val primrec_pr_cond = Store_thm( 406 "primrec_pr_cond", 407 ``primrec P n ��� primrec f n ��� primrec g n ��� primrec (pr_cond P f g) n``, 408 SRW_TAC [][pr_cond_def] THEN 409 MATCH_MP_TAC primrec_cn THEN SRW_TAC [][] THEN 410 MATCH_MP_TAC primrec_cn THEN SRW_TAC [][] THEN 411 MATCH_MP_TAC primrec_cn THEN SRW_TAC [][] THEN 412 SRW_TAC [][primrec_rules]); 413 414(* 0 div m = 0 /\ 415 (n + 1) div m = let r = n div m 416 in 417 if n + 1 - r * m = m then r + 1 else r 418 419 In recursive case, h is called with (n, r, m) 420 421*) 422val pr_div_def = Define` 423 pr_div = 424 Pr (K 0) 425 (pr_cond (proj 0 +. K 1 -. (proj 1 *. proj 2) =. proj 2) 426 (Cn succ [proj 1]) 427 (proj 1)) 428`; 429 430val primrec_pr_div = Store_thm( 431 "primrec_pr_div", 432 ``primrec pr_div 2``, 433 SRW_TAC [][pr_div_def] THEN 434 MATCH_MP_TAC alt_Pr_rule THEN SRW_TAC [][] THEN 435 MATCH_MP_TAC primrec_pr_cond THEN SRW_TAC [][primrec_rules]); 436 437val pr_div_recursion = store_thm( 438 "pr_div_recursion", 439 ``(pr_div [0; m] = 0) ��� 440 (pr_div [n + 1; m] = let r = pr_div [n; m] 441 in 442 if n + 1 - r * m = m then r + 1 else r)``, 443 SIMP_TAC (srw_ss()) [pr_div_def, LET_THM, ADD1]); 444 445val pr_div_thm = Store_thm( 446 "pr_div_thm", 447 ``0 < m ��� (pr_div [n; m] = n DIV m)``, 448 STRIP_TAC THEN Induct_on `n` THEN1 449 SRW_TAC [][pr_div_recursion, ZERO_DIV] THEN 450 SRW_TAC [][pr_div_recursion, ADD1, LET_THM] THENL [ 451 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN MATCH_MP_TAC DIV_UNIQUE THEN 452 Q.EXISTS_TAC `0` THEN SRW_TAC [ARITH_ss][RIGHT_ADD_DISTRIB], 453 454 Q.SPEC_THEN `m` (IMP_RES_THEN MP_TAC) DIVISION THEN 455 NTAC 2 (DISCH_THEN (Q.SPEC_THEN `n` ASSUME_TAC)) THEN 456 Q.ABBREV_TAC `q = n DIV m` THEN 457 Q.ABBREV_TAC `r = n MOD m` THEN 458 markerLib.RM_ALL_ABBREVS_TAC THEN 459 Q.PAT_X_ASSUM `pr_div X = Y` (K ALL_TAC) THEN 460 SRW_TAC [][] THEN 461 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN MATCH_MP_TAC DIV_UNIQUE THEN 462 Q.EXISTS_TAC `r + 1` THEN DECIDE_TAC 463 ]); 464 465val pr_mod_def = Define`pr_mod = proj 0 -. (pr_div *. proj 1)` 466 467val pr_mod_eqn = store_thm( 468 "pr_mod_eqn", 469 ``pr_mod [n; m] = n - pr_div [n; m] * m``, 470 SRW_TAC [][pr_mod_def]); 471 472val pr_mod_thm = Store_thm( 473 "pr_mod_thm", 474 ``0 < m ��� (pr_mod [n; m] = n MOD m)``, 475 SRW_TAC [][pr_mod_eqn] THEN 476 Q.SPEC_THEN `m` (IMP_RES_THEN MP_TAC) DIVISION THEN 477 NTAC 2 (DISCH_THEN (Q.SPEC_THEN `n` ASSUME_TAC)) THEN 478 DECIDE_TAC); 479 480val primrec_pr_mod = Store_thm( 481 "primrec_pr_mod", 482 ``primrec pr_mod 2``, 483 SRW_TAC [][pr_mod_def, primrec_rules]); 484 485(* ---------------------------------------------------------------------- 486 number pairing 487 ---------------------------------------------------------------------- *) 488 489(* triangular number calculation *) 490val _ = temp_overload_on ("tri.", ``��n. Cn (pr1 tri) [n]``); 491 492val primrec_tri = Store_thm( 493 "primrec_tri", 494 ``primrec (pr1 tri) 1``, 495 MATCH_MP_TAC primrec_pr1 THEN 496 Q.EXISTS_TAC `Pr1 0 (proj 0 +. K 1 +. proj 1)` THEN 497 SRW_TAC [][primrec_rules] THEN 498 Induct_on `n` THEN SRW_TAC [][tri_def, ADD1]); 499 500(* inverse triangular - start at the input value n, and try successively smaller 501 values until an m <= n comes up such that tri (m) <= the original n *) 502val _ = temp_overload_on ("invtri.", ``��n. Cn (pr1 tri�����) [n]``) 503 504val Pr_eval = prove( 505 ``0 < m ==> (Pr b r (m :: t) = r (m - 1 :: Pr b r (m - 1 :: t) :: t))``, 506 STRIP_TAC THEN SIMP_TAC (srw_ss()) [Once Pr_def, SimpLHS] THEN 507 Cases_on `m` THEN SRW_TAC [ARITH_ss][]); 508 509val tri_eval = CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV tri_def 510 511val tri_bounds_lemma = prove( 512 ``���n. n + 3 ��� tri (n + 2)``, 513 Induct THEN SRW_TAC [ARITH_ss][ADD_CLAUSES, tri_eval, tri_def]); 514 515val primrec_invtri = Store_thm( 516 "primrec_invtri", 517 ``primrec (pr1 tri�����) 1``, 518 MATCH_MP_TAC primrec_pr1 THEN 519 Q.EXISTS_TAC ` 520 Cn (Pr zerof (pr_cond (tri. (proj 0 +. K 1) <=. proj 2) 521 (proj 0 +. K 1) 522 (proj 1))) 523 [proj 0; proj 0] 524 ` THEN 525 CONJ_TAC THENL [ 526 MATCH_MP_TAC primrec_cn THEN 527 SRW_TAC [][primrec_rules] THEN 528 MATCH_MP_TAC alt_Pr_rule THEN 529 SRW_TAC [][primrec_rules] THEN 530 MATCH_MP_TAC primrec_pr_cond THEN 531 SRW_TAC [][primrec_rules], 532 533 Q.X_GEN_TAC `n` THEN 534 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN 535 MATCH_MP_TAC invtri_unique THEN SRW_TAC [][] THENL [ 536 Q.MATCH_ABBREV_TAC `tri (Pr zerof recn [n;n]) ��� n` THEN 537 Q_TAC SUFF_TAC `���n m. tri (Pr zerof recn [n;m]) ��� m` 538 THEN1 METIS_TAC [] THEN 539 Induct THEN SRW_TAC [][tri_def] THEN 540 markerLib.UNABBREV_ALL_TAC THEN 541 SRW_TAC [][pr_cond_thm], 542 543 Q.MATCH_ABBREV_TAC `n < tri (Pr zerof recn [n;n] + 1)` THEN 544 Q_TAC SUFF_TAC 545 `���n m. (���p. n < p /\ p ��� m ��� m < tri p) ��� 546 m < tri (Pr zerof recn [n;m] + 1)` 547 THEN1 (DISCH_THEN (Q.SPECL_THEN [`n`,`n`] STRIP_ASSUME_TAC) THEN 548 FIRST_X_ASSUM MATCH_MP_TAC THEN DECIDE_TAC) THEN 549 Induct THEN SRW_TAC [][] THENL [ 550 Cases_on `m = 0` THEN1 551 (ASM_SIMP_TAC bool_ss [ONE, tri_def] THEN DECIDE_TAC) THEN 552 `1 ��� m ��� 0 < 1` by DECIDE_TAC THEN METIS_TAC [], 553 554 SRW_TAC [][] THEN markerLib.UNABBREV_ALL_TAC THEN 555 SRW_TAC [][] THENL [ 556 Cases_on `n = 0` THENL [ 557 SRW_TAC [][tri_def] THEN 558 Cases_on `m = 1` THEN1 SRW_TAC [][tri_eval] THEN 559 FIRST_X_ASSUM MATCH_MP_TAC THEN 560 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [tri_eval], 561 562 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [ARITH_ss][] THEN 563 MATCH_MP_TAC LESS_EQ_TRANS THEN 564 Q.EXISTS_TAC `tri (n + 1)` THEN 565 SRW_TAC [][] THEN 566 Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 567 SRW_TAC [ARITH_ss][ADD_CLAUSES, ADD1, tri_bounds_lemma] 568 ], 569 570 Q.PAT_X_ASSUM `���m. (���p:num. P p) ��� Q m` MATCH_MP_TAC THEN 571 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [NOT_LESS_EQUAL] THEN 572 Cases_on `p = n + 1` THEN1 SRW_TAC [][] THEN 573 FIRST_X_ASSUM MATCH_MP_TAC THEN DECIDE_TAC 574 ] 575 ] 576 ] 577 ]); 578 579(* --- npair *) 580val primrec_npair = Store_thm( 581 "primrec_npair", 582 ``primrec (pr2 npair) 2``, 583 MATCH_MP_TAC primrec_pr2 THEN 584 Q.EXISTS_TAC `tri. (proj 0 +. proj 1) +. proj 1` THEN 585 SRW_TAC [][primrec_rules, npair_def]); 586 587(* --- nfst *) 588val primrec_nfst = Store_thm( 589 "primrec_nfst", 590 ``primrec (pr1 nfst) 1``, 591 MATCH_MP_TAC primrec_pr1 THEN 592 Q.EXISTS_TAC `tri. (invtri. (proj 0)) +. invtri. (proj 0) -. proj 0` THEN 593 SRW_TAC [][primrec_rules, nfst_def] THEN 594 MATCH_MP_TAC primrec_cn THEN SRW_TAC [][primrec_rules]); 595 596(* --- nsnd *) 597val primrec_nsnd = Store_thm( 598 "primrec_nsnd", 599 ``primrec (pr1 nsnd) 1``, 600 MATCH_MP_TAC primrec_pr1 THEN 601 Q.EXISTS_TAC `proj 0 -. tri. (invtri. (proj 0))` THEN 602 SRW_TAC [][primrec_rules, nsnd_def]); 603 604(* ---------------------------------------------------------------------- 605 Proof that Ackermann function is not primitive recursive. 606 607 Taken from the Isabelle/HOL example by Larry Paulson, and also 608 referring to his original source: 609 610 @inproceedings{Szasz:Ackermann:1993, 611 author = {Nora Szasz}, 612 title = {A Machine Checked Proof that {Ackermann}'s Function is not 613 Primitive Recursive}, 614 booktitle = {Papers Presented at the Second Annual Workshop on 615 Logical Environments}, 616 year = {1993}, 617 isbn = {0-521-43312-6}, 618 location = {Edinburgh, Scotland}, 619 pages = {317--338}, 620 url = {http://portal.acm.org/citation.cfm?id=185881.185934}, 621 publisher = {Cambridge University Press}, 622 address = {New York, NY, USA}, 623 } 624 625 ---------------------------------------------------------------------- *) 626 627val Ackermann_def = Define` 628 (Ackermann 0 m = m + 1) ��� 629 (Ackermann (SUC n) 0 = Ackermann n 1) ��� 630 (Ackermann (SUC n) (SUC m) = Ackermann n (Ackermann (SUC n) m)) 631`; 632val H_ind = theorem "Ackermann_ind" 633val H_thm = CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV Ackermann_def 634val H_def = Ackermann_def 635val _ = augment_srw_ss [rewrites [H_def]] 636 637val _ = temp_overload_on ("H", ``Ackermann``); 638 639val Alemma1 = prove( 640 ``(H 1 n = n + 2) ��� (H 2 n = 2 * n + 3)``, 641 `���n. H 1 n = n + 2` 642 by (Induct_on `n` THEN SRW_TAC [][H_thm] THEN 643 ONCE_REWRITE_TAC [ONE] THEN 644 SRW_TAC [][Ackermann_def] THEN DECIDE_TAC) THEN 645 SRW_TAC [][] THEN 646 Induct_on `n` THEN SRW_TAC [][H_thm] THEN 647 SIMP_TAC bool_ss [SimpLHS, TWO] THEN 648 SRW_TAC [][Ackermann_def] THEN DECIDE_TAC); 649val _ = augment_srw_ss [rewrites [Alemma1]] 650 651val A4 = prove( 652 ``���m n. n < H m n``, 653 HO_MATCH_MP_TAC H_ind THEN SRW_TAC [ARITH_ss][]) 654val _ = augment_srw_ss [rewrites [A4]] 655 656val A5_0 = prove( 657 ``���n m. H n m < H n (m + 1)``, 658 SIMP_TAC (srw_ss()) [GSYM ADD1] THEN 659 HO_MATCH_MP_TAC H_ind THEN SRW_TAC [][]); 660 661val A5 = prove( 662 ``j < k ==> H i j < H i k``, 663 MATCH_MP_TAC STRICTLY_INCREASING_TC THEN SRW_TAC [][A5_0, ADD1]); 664 665val A5' = prove( 666 ``j ��� k ==> H i j ��� H i k``, 667 METIS_TAC [LESS_OR_EQ, A5]); 668 669val A6 = prove( 670 ``���m n. H m (n + 1) ��� H (m + 1) n``, 671 REWRITE_TAC [GSYM ADD1] THEN 672 Induct_on `n` THEN SRW_TAC [ARITH_ss][] THEN 673 METIS_TAC [LESS_EQ_TRANS, A5', LESS_OR, A4]); 674 675val A7_0 = prove( 676 ``H i j < H (SUC i) j``, 677 METIS_TAC [A6, ADD1, LESS_LESS_EQ_TRANS, A5, prim_recTheory.LESS_SUC_REFL]); 678 679val A7 = prove( 680 ``i < j ==> H i k < H j k``, 681 Q_TAC SUFF_TAC `i < j ==> (��n. H n k) i < (��n. H n k) j` 682 THEN1 SRW_TAC [][] THEN 683 MATCH_MP_TAC STRICTLY_INCREASING_TC THEN SRW_TAC [][A7_0]) 684 685val A7' = prove( 686 ``i ��� j ==> H i k ��� H j k``, 687 METIS_TAC [LESS_OR_EQ, A7]); 688 689val A10 = prove( 690 ``H i��� (H i��� j) < H (i��� + i��� + 2) j``, 691 SIMP_TAC bool_ss [TWO, ADD_CLAUSES, ONE] THEN 692 `H i��� (H i��� j) < H (i��� + i���) (H (i��� + i��� + 1) j)` 693 by METIS_TAC [A7', LESS_LESS_EQ_TRANS, DECIDE ``x <= x + y``, A5, A7, 694 DECIDE ``y < x + y + 1``] THEN 695 `H (SUC (i��� + i���)) (SUC j) = H (i��� + i���) (H (i��� + i��� + 1) j)` 696 by SRW_TAC [][ADD1] THEN 697 POP_ASSUM (SUBST_ALL_TAC o SYM) THEN 698 METIS_TAC [A6, ADD1, LESS_LESS_EQ_TRANS]); 699 700val A11 = prove( 701 ``H i��� j + H i��� j < H (i��� + i��� + 4) j``, 702 MATCH_MP_TAC LESS_TRANS THEN Q.EXISTS_TAC `H 2 (H (i��� + i���) j)` THEN 703 Tactical.REVERSE CONJ_TAC THEN1 704 (A10 |> Q.INST [`i���` |-> `i��� + i���`, `i���` |-> `2`] 705 |> CONV_RULE (DEPTH_CONV numSimps.ADDL_CANON_CONV) 706 |> ACCEPT_TAC) THEN 707 SRW_TAC [][] THEN 708 MATCH_MP_TAC LESS_EQ_LESS_TRANS THEN 709 Q.EXISTS_TAC `2 * H (i��� + i���) j` THEN SRW_TAC [][] THEN 710 `H i��� j ��� H (i��� + i���) j` by SRW_TAC [][A7'] THEN 711 `H i��� j ��� H (i��� + i���) j` by SRW_TAC [][A7'] THEN 712 DECIDE_TAC) 713 714val A12 = prove( 715 ``i < H k j ==> i + j < H (k + 4) j``, 716 STRIP_TAC THEN MATCH_MP_TAC LESS_TRANS THEN 717 Q.EXISTS_TAC `H k j + H 0 j` THEN CONJ_TAC THEN1 SRW_TAC [ARITH_ss][] THEN 718 METIS_TAC [DECIDE ``k + 0 + 4 = k + 4``, A11]); 719 720val EL_SUM = store_thm( 721 "EL_SUM", 722 ``���i l. i < LENGTH l ��� (EL i l ��� SUM l)``, 723 Induct_on `l` THEN SRW_TAC [][] THEN 724 Cases_on `i` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 725 RES_TAC THEN DECIDE_TAC); 726 727val Cn_case_aux = prove( 728 ``EVERY (��g. primrec g k ��� ���J. ���l. (LENGTH l = k) ==> g l < H J (SUM l)) gs 729 ==> 730 ���J. ���l. (LENGTH l = k) ==> SUM (MAP (��g. g l) gs) < H J (SUM l)``, 731 Induct_on `gs` THEN SRW_TAC [][] THEN1 732 (Q.EXISTS_TAC `0` THEN SRW_TAC [ARITH_ss][]) THEN 733 FULL_SIMP_TAC (srw_ss()) [] THEN 734 Q.EXISTS_TAC `J + J' + 4` THEN REPEAT STRIP_TAC THEN RES_TAC THEN 735 (A11 |> Q.INST [`i���` |-> `J`, `i���` |-> `J'`, `j` |-> `SUM l`] 736 |> ASSUME_TAC) THEN 737 DECIDE_TAC) 738 739val Cn_case = prove( 740 ``EVERY (��g. primrec g k ��� ���J. ���l. (LENGTH l = k) ==> g l < H J (SUM l)) gs ��� 741 (���l. (LENGTH l = LENGTH gs) ==> f l < H J (SUM l)) ==> 742 ���J. ���l. (LENGTH l = k) ==> Cn f gs l < H J (SUM l)``, 743 SRW_TAC [][Cn_def] THEN 744 METIS_TAC [LESS_TRANS, A5, A10, LENGTH_MAP, Cn_case_aux]); 745 746val Pr_case_aux = prove( 747 ``(���l. (LENGTH l = k) ==> f l + SUM l < H kf (SUM l)) ��� 748 (���l. (LENGTH l = k + 2) ==> g l + SUM l < H kg (SUM l)) ��� 749 (LENGTH l = k + 1) ==> 750 Pr f g l + SUM l < H (SUC (kf + kg)) (SUM l)``, 751 Cases_on `l` THEN1 (SRW_TAC [][Once Pr_def]) THEN 752 SRW_TAC [][] THEN 753 FULL_SIMP_TAC (srw_ss()) [ADD1] THEN SRW_TAC [][] THEN 754 Induct_on `h` THEN1 755 (SRW_TAC [][] THEN 756 METIS_TAC [LESS_TRANS, DECIDE ``x < x + y + 1``, A7]) THEN 757 Q.MATCH_ABBREV_TAC 758 `Prt + (SUC h + SUM t) < H (kf + kg + 1) (SUC h + SUM t)` THEN 759 Q.ABBREV_TAC `reclist = h::Pr f g (h::t)::t` THEN 760 `LENGTH reclist = LENGTH t + 2` by SRW_TAC [ARITH_ss][Abbr`reclist`] THEN 761 `Prt + (SUC h + SUM t) ��� H kg (SUM reclist)` 762 by (`Prt = g reclist` by SRW_TAC [][Abbr`Prt`, Abbr`reclist`] THEN 763 `Prt + (SUC h + SUM t) ��� Prt + SUM reclist + 1` 764 by SRW_TAC [ARITH_ss][Abbr`reclist`] THEN 765 `Prt + SUM reclist < H kg (SUM reclist)` by METIS_TAC [] THEN 766 DECIDE_TAC) THEN 767 `SUM reclist = Pr f g (h::t) + (h + SUM t)` 768 by SRW_TAC [ARITH_ss][Abbr`reclist`] THEN 769 `SUM reclist < H (kf + kg + 1) (h + SUM t)` by METIS_TAC [] THEN 770 `Prt + (SUC h + SUM t) < H kg (H (kf + kg + 1) (h + SUM t))` 771 by METIS_TAC [A5, LESS_EQ_LESS_TRANS] THEN 772 `H kg (H (kf + kg + 1) (h + SUM t)) ��� 773 H (kf + kg) (H (kf + kg + 1) (h + SUM t))` 774 by METIS_TAC [A7', DECIDE ``x ��� y + x``] THEN 775 POP_ASSUM (fn th2 => POP_ASSUM (fn th1 => 776 MATCH_MP LESS_LESS_EQ_TRANS (CONJ th1 th2) |> ASSUME_TAC)) THEN 777 FULL_SIMP_TAC bool_ss [GSYM ADD1, GSYM H_def, ADD_CLAUSES]) 778 779val Pr_case = prove( 780 ``(���l. (LENGTH l = k) ==> f l < H kf (SUM l)) ��� 781 (���l. (LENGTH l = k + 2) ==> g l < H kg (SUM l)) ==> 782 ���J. ���l. (LENGTH l = k + 1) ==> Pr f g l < H J (SUM l)``, 783 SRW_TAC [][] THEN Q.EXISTS_TAC `SUC ((kf + 4) + (kg + 4))` THEN 784 SRW_TAC [][] THEN 785 MATCH_MP_TAC LESS_EQ_LESS_TRANS THEN 786 Q.EXISTS_TAC `Pr f g l + SUM l` THEN SRW_TAC [][] THEN 787 METIS_TAC [A12, Pr_case_aux]); 788 789val Ackermann_grows_too_fast = store_thm( 790 "Ackermann_grows_too_fast", 791 ``���f k. primrec f k ��� ���J. ���l. (LENGTH l = k) ��� f l < H J (SUM l)``, 792 HO_MATCH_MP_TAC strong_primrec_ind THEN REPEAT STRIP_TAC THENL [ 793 Q.EXISTS_TAC `0` THEN SRW_TAC [ARITH_ss][], 794 795 Q.EXISTS_TAC `1` THEN SRW_TAC [ARITH_ss][] THEN 796 Cases_on `l` THEN FULL_SIMP_TAC (srw_ss()) [] THEN DECIDE_TAC, 797 798 Q.EXISTS_TAC `0` THEN SRW_TAC [ARITH_ss][] THEN 799 MATCH_MP_TAC (DECIDE ``p ��� x ��� p < x + 1``) THEN 800 SRW_TAC [ARITH_ss][proj_def, EL_SUM], 801 802 METIS_TAC [Cn_case], 803 METIS_TAC [Pr_case] 804 ]); 805 806val Ackermann_not_primrec = store_thm( 807 "Ackermann_not_primrec", 808 ``�����f. primrec f 2 ��� ���n m. f [n; m] = H n m``, 809 STRIP_TAC THEN 810 Q.ABBREV_TAC `g = Cn f [proj 0; proj 0]` THEN 811 `���n. g [n] = H n n` by SRW_TAC [][Abbr`g`] THEN 812 `primrec g 1` by SRW_TAC [][Abbr`g`, primrec_rules] THEN 813 `���J. ���n. g [n] < H J n` 814 by (IMP_RES_TAC Ackermann_grows_too_fast THEN 815 Q.PAT_X_ASSUM `���l. (LENGTH l = 1) ��� g l < H X Y` 816 (Q.SPEC_THEN `[n]` (MP_TAC o Q.GEN `n`)) THEN 817 DISCH_THEN (ASSUME_TAC o SIMP_RULE (srw_ss()) []) THEN 818 METIS_TAC []) THEN 819 POP_ASSUM (Q.SPEC_THEN `J` MP_TAC) THEN SRW_TAC [][]); 820 821val _ = export_theory() 822