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