src/HOL/ex/Fib.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4379 7049ca8f912e
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (*  Title:      HOL/ex/Fib
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   1997  University of Cambridge
     5 
     6 Fibonacci numbers: proofs of laws taken from
     7 
     8   R. L. Graham, D. E. Knuth, O. Patashnik.
     9   Concrete Mathematics.
    10   (Addison-Wesley, 1989)
    11 *)
    12 
    13 
    14 (** The difficulty in these proofs is to ensure that the induction hypotheses
    15     are applied before the definition of "fib".  Towards this end, the 
    16     "fib" equations are not added to the simpset and are applied very 
    17     selectively at first.
    18 **)
    19 
    20 bind_thm ("fib_Suc_Suc", hd(rev fib.rules));
    21 
    22 
    23 (*Concrete Mathematics, page 280*)
    24 goal thy "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
    25 by (res_inst_tac [("u","n")] fib.induct 1);
    26 (*Simplify the LHS just enough to apply the induction hypotheses*)
    27 by (asm_full_simp_tac
    28     (simpset() addsimps [read_instantiate[("x", "Suc(?m+?n)")] fib_Suc_Suc]) 3);
    29 by (ALLGOALS 
    30     (asm_simp_tac (simpset() addsimps 
    31 		   (fib.rules @ add_ac @ mult_ac @
    32 		    [add_mult_distrib, add_mult_distrib2]))));
    33 qed "fib_add";
    34 
    35 
    36 goal thy "fib (Suc n) ~= 0";
    37 by (res_inst_tac [("u","n")] fib.induct 1);
    38 by (ALLGOALS (asm_simp_tac (simpset() addsimps fib.rules)));
    39 qed "fib_Suc_neq_0";
    40 Addsimps [fib_Suc_neq_0];
    41 
    42 
    43 
    44 (*Concrete Mathematics, page 278: Cassini's identity*)
    45 goal thy "fib (Suc (Suc n)) * fib n = \
    46 \              (if n mod 2 = 0 then pred(fib(Suc n) * fib(Suc n)) \
    47 \                              else Suc (fib(Suc n) * fib(Suc n)))";
    48 by (res_inst_tac [("u","n")] fib.induct 1);
    49 by (res_inst_tac [("P", "%z. ?ff(x) * z = ?kk(x)")] (fib_Suc_Suc RS ssubst) 3);
    50 by (stac (read_instantiate [("x", "Suc(Suc ?n)")] fib_Suc_Suc) 3);
    51 by (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2]) 3);
    52 by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3);
    53 by (ALLGOALS  (*using fib.rules here results in a longer proof!*)
    54     (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2, 
    55 				      mod_less, mod_Suc]
    56                             addsplits [expand_if])));
    57 by (safe_tac (claset() addSDs [mod2_neq_0]));
    58 by (ALLGOALS
    59     (asm_full_simp_tac
    60      (simpset() addsimps (fib.rules @ add_ac @ mult_ac @
    61 			 [add_mult_distrib, add_mult_distrib2, 
    62 			  mod_less, mod_Suc]))));
    63 qed "fib_Cassini";
    64 
    65 
    66 (** exercise: prove gcd(fib m, fib n) = fib(gcd(m,n)) **)