Tutorial/Recursive_definitions.ml

   1 let fib = define
   2  `fib n = if n = 0 \/ n = 1 then 1 else fib(n - 1) + fib(n - 2)`;;
   3
   4 let fib2 = define
   5  `(fib2 0 = 1) /\
   6   (fib2 1 = 1) /\
   7   (fib2 (n + 2) = fib2(n) + fib2(n + 1))`;;
   8
   9 let halve = define `halve (2 * n) = n`;;
  10
  11 let unknown = define `unknown n = unknown(n + 1)`;;
  12
  13 define
  14  `!n. collatz(n) = if n <= 1 then n
  15                    else if EVEN(n) then collatz(n DIV 2)
  16                    else collatz(3 * n + 1)`;;
  17
  18 let fusc_def = define
  19  `(fusc (2 * n) = if n = 0 then 0 else fusc(n)) /\
  20   (fusc (2 * n + 1) = if n = 0 then 1 else fusc(n) + fusc(n + 1))`;;
  21
  22 let fusc = prove
  23  (`fusc 0 = 0 /\
  24    fusc 1 = 1 /\
  25    fusc (2 * n) = fusc(n) /\
  26    fusc (2 * n + 1) = fusc(n) + fusc(n + 1)`,
  27   REWRITE_TAC[fusc_def] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
  28   MP_TAC(INST [`0`,`n:num`] fusc_def) THEN ARITH_TAC);;
  29
  30 let binom = define
  31  `(!n. binom(n,0) = 1) /\
  32   (!k. binom(0,SUC(k)) = 0) /\
  33   (!n k. binom(SUC(n),SUC(k)) = binom(n,SUC(k)) + binom(n,k))`;;
  34
  35 let BINOM_LT = prove
  36  (`!n k. n < k ==> (binom(n,k) = 0)`,
  37   INDUCT_TAC THEN INDUCT_TAC THEN REWRITE_TAC[binom; ARITH; LT_SUC; LT] THEN
  38   ASM_SIMP_TAC[ARITH_RULE `n < k ==> n < SUC(k)`; ARITH]);;
  39
  40 let BINOM_REFL = prove
  41  (`!n. binom(n,n) = 1`,
  42   INDUCT_TAC THEN ASM_SIMP_TAC[binom; BINOM_LT; LT; ARITH]);;
  43
  44 let BINOM_FACT = prove
  45  (`!n k. FACT n * FACT k * binom(n+k,k) = FACT(n + k)`,
  46   INDUCT_TAC THEN REWRITE_TAC[FACT; ADD_CLAUSES; MULT_CLAUSES; BINOM_REFL] THEN
  47   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; FACT; MULT_CLAUSES; binom] THEN
  48   FIRST_X_ASSUM(MP_TAC o SPEC `SUC k`) THEN POP_ASSUM MP_TAC THEN
  49   REWRITE_TAC[ADD_CLAUSES; FACT; binom] THEN CONV_TAC NUM_RING);;
  50
  51 let BINOMIAL_THEOREM = prove
  52  (`!n. (x + y) EXP n = nsum(0..n) (\k. binom(n,k) * x EXP k * y EXP (n - k))`,
  53   INDUCT_TAC THEN ASM_REWRITE_TAC[EXP] THEN
  54   REWRITE_TAC[NSUM_SING_NUMSEG; binom; SUB_REFL; EXP; MULT_CLAUSES] THEN
  55   SIMP_TAC[NSUM_CLAUSES_LEFT; ADD1; ARITH_RULE `0 <= n + 1`; NSUM_OFFSET] THEN
  56   ASM_REWRITE_TAC[EXP; binom; GSYM ADD1; GSYM NSUM_LMUL] THEN
  57   REWRITE_TAC[RIGHT_ADD_DISTRIB; NSUM_ADD_NUMSEG; MULT_CLAUSES; SUB_0] THEN
  58   MATCH_MP_TAC(ARITH_RULE `a = e /\ b = c + d ==> a + b = c + d + e`) THEN
  59   CONJ_TAC THENL [REWRITE_TAC[MULT_AC; SUB_SUC]; REWRITE_TAC[GSYM EXP]] THEN
  60   SIMP_TAC[ADD1; SYM(REWRITE_CONV[NSUM_OFFSET]`nsum(m+1..n+1) (\i. f i)`)] THEN
  61   REWRITE_TAC[NSUM_CLAUSES_NUMSEG; GSYM ADD1; LE_SUC; LE_0] THEN
  62   SIMP_TAC[NSUM_CLAUSES_LEFT; LE_0] THEN
  63   SIMP_TAC[BINOM_LT; LT; MULT_CLAUSES; ADD_CLAUSES; SUB_0; EXP; binom] THEN
  64   SIMP_TAC[ARITH; ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; EXP] THEN
  65   REWRITE_TAC[MULT_AC]);;