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