src/HOL/ex/Fib.ML
author paulson
Thu, 22 May 1997 15:11:23 +0200
changeset 3300 4f5ffefa7799
child 3724 f33e301a89f5
permissions -rw-r--r--
New example of recdef and permutative rewriting
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
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    28
    (!simpset addsimps [read_instantiate[("x", "Suc(?m+?n)")] fib_Suc_Suc]) 3);
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    29
by (ALLGOALS 
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    30
    (asm_simp_tac (!simpset addsimps 
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);
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    38
by (ALLGOALS (asm_simp_tac (!simpset addsimps fib.rules)));
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
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    42
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    43
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    44
(*Concrete Mathematics, page 278: Cassini's identity*)
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    45
goal thy "fib (Suc (Suc n)) * fib n = \
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    46
\              (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
    47
\                              else Suc (fib(Suc n) * fib(Suc n)))";
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    48
by (res_inst_tac [("u","n")] fib.induct 1);
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    49
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
    50
by (stac (read_instantiate [("x", "Suc(Suc ?n)")] fib_Suc_Suc) 3);
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    51
by (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2]) 3);
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    52
by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3);
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    53
by (ALLGOALS  (*using fib.rules here results in a longer proof!*)
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    54
    (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2, 
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    55
				      mod_less, mod_Suc]
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    56
                            setloop split_tac[expand_if])));
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    57
by (step_tac (!claset addSDs [mod2_neq_0]) 1);
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    58
by (ALLGOALS
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    59
    (asm_full_simp_tac
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    60
     (!simpset addsimps (fib.rules @ add_ac @ mult_ac @
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    61
			 [add_mult_distrib, add_mult_distrib2, 
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    62
			  mod_less, mod_Suc]))));
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    63
qed "fib_Cassini";
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    64
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    65
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    66
(** exercise: prove gcd(fib m, fib n) = fib(gcd(m,n)) **)