src/HOL/NumberTheory/Fib.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9944 2a705d1af4dc
child 10965 cd89ce2795ab
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9944
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     1
(*  Title:      HOL/ex/Fib
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     2
    ID:         $Id$
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     5
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     6
Fibonacci numbers: proofs of laws taken from
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     7
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     8
  R. L. Graham, D. E. Knuth, O. Patashnik.
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     9
  Concrete Mathematics.
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    10
  (Addison-Wesley, 1989)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    11
*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    12
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    13
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    14
(** The difficulty in these proofs is to ensure that the induction hypotheses
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    15
    are applied before the definition of "fib".  Towards this end, the 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    16
    "fib" equations are not added to the simpset and are applied very 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    17
    selectively at first.
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    18
**)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    19
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    20
Delsimps fib.Suc_Suc;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    21
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    22
val [fib_Suc_Suc] = fib.Suc_Suc;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    23
val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    24
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    25
(*Concrete Mathematics, page 280*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    26
Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    27
by (induct_thm_tac fib.induct "n" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    28
(*Simplify the LHS just enough to apply the induction hypotheses*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    29
by (asm_full_simp_tac
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    30
    (simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    31
by (ALLGOALS 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    32
    (asm_simp_tac (simpset() addsimps 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    33
		   ([fib_Suc_Suc, add_mult_distrib, add_mult_distrib2]))));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    34
qed "fib_add";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    35
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    36
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    37
Goal "fib (Suc n) ~= 0";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    38
by (induct_thm_tac fib.induct "n" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    39
by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc])));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    40
qed "fib_Suc_neq_0";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    41
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    42
(* Also add  0 < fib (Suc n) *)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    43
Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1];
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    44
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    45
Goal "0<n ==> 0 < fib n";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    46
by (rtac (not0_implies_Suc RS exE) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    47
by Auto_tac;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    48
qed "fib_gr_0";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    49
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    50
(*Concrete Mathematics, page 278: Cassini's identity.
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    51
  It is much easier to prove using integers!*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    52
Goal "int (fib (Suc (Suc n)) * fib n) = \
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    53
\     (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    54
\                     else int (fib(Suc n) * fib(Suc n)) + #1)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    55
by (induct_thm_tac fib.induct "n" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    56
by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    57
by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    58
by (asm_full_simp_tac
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    59
     (simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    60
			  mod_Suc, zmult_int RS sym] @ zmult_ac) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    61
qed "fib_Cassini";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    62
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    63
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    64
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    65
(** Towards Law 6.111 of Concrete Mathematics **)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    66
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    67
val gcd_induct = thm "gcd_induct";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    68
val gcd_commute = thm "gcd_commute";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    69
val gcd_add2 = thm "gcd_add2";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    70
val gcd_non_0 = thm "gcd_non_0";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    71
val gcd_mult_cancel = thm "gcd_mult_cancel";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    72
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    73
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    74
Goal "gcd(fib n, fib (Suc n)) = 1";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    75
by (induct_thm_tac fib.induct "n" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    76
by (asm_simp_tac (simpset() addsimps [gcd_commute, fib_Suc3]) 3);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    77
by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc])));
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    78
qed "gcd_fib_Suc_eq_1"; 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    79
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    80
val gcd_fib_commute = 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    81
    read_instantiate_sg (sign_of thy) [("m", "fib m")] gcd_commute;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    82
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    83
Goal "gcd(fib m, fib (n+m)) = gcd(fib m, fib n)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    84
by (simp_tac (simpset() addsimps [gcd_fib_commute]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    85
by (case_tac "m=0" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    86
by (Asm_simp_tac 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    87
by (clarify_tac (claset() addSDs [not0_implies_Suc]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    88
by (simp_tac (simpset() addsimps [fib_add]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    89
by (asm_simp_tac (simpset() addsimps [add_commute, gcd_non_0]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    90
by (asm_simp_tac (simpset() addsimps [gcd_non_0 RS sym]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    91
by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    92
qed "gcd_fib_add";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    93
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    94
Goal "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    95
by (rtac (gcd_fib_add RS sym RS trans) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    96
by (Asm_simp_tac 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    97
qed "gcd_fib_diff";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    98
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    99
Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   100
by (induct_thm_tac nat_less_induct "n" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   101
by (stac mod_if 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   102
by (Asm_simp_tac 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   103
by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_geq, 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   104
				      not_less_iff_le, diff_less]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   105
qed "gcd_fib_mod";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   106
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   107
(*Law 6.111*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   108
Goal "fib(gcd(m,n)) = gcd(fib m, fib n)";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   109
by (induct_thm_tac gcd_induct "m n" 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   110
by (Asm_simp_tac 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   111
by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   112
by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   113
qed "fib_gcd";