src/HOL/ex/Fib.ML
author paulson
Wed, 15 Jul 1998 10:15:13 +0200
changeset 5143 b94cd208f073
parent 5069 3ea049f7979d
child 5537 c2bd39a2c0ee
permissions -rw-r--r--
Removal of leading "\!\!..." from most Goal commands
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
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    20
val [fib_0, fib_1, fib_Suc_Suc] = fib.rules;
3300
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    21
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    22
Addsimps [fib_0, fib_1];
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    23
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    24
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    25
val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc;
3300
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    26
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    27
(*Concrete Mathematics, page 280*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4812
diff changeset
    28
Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
3300
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    29
by (res_inst_tac [("u","n")] fib.induct 1);
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    30
(*Simplify the LHS just enough to apply the induction hypotheses*)
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    31
by (asm_full_simp_tac
4385
f6d019eefa1e Got rid of mod2_neq_0
paulson
parents: 4379
diff changeset
    32
    (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
    33
by (ALLGOALS 
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    34
    (asm_simp_tac (simpset() addsimps 
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    35
		   ([] @ add_ac @ mult_ac @
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    36
		    [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2]))));
3300
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    37
qed "fib_add";
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    38
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    39
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4812
diff changeset
    40
Goal "fib (Suc n) ~= 0";
3300
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    41
by (res_inst_tac [("u","n")] fib.induct 1);
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    42
by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc])));
3300
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    43
qed "fib_Suc_neq_0";
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    44
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    45
(* Also add  0 < fib (Suc n) *)
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    46
Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1];
4379
7049ca8f912e Replaced Fib(Suc n)~=0 by 0<Fib(Suc(n)).
nipkow
parents: 4089
diff changeset
    47
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    48
Goal "0<n ==> 0 < fib n";
4812
d65372e425e5 expandshort; new gcd_induct with inbuilt case analysis
paulson
parents: 4809
diff changeset
    49
by (rtac (not0_implies_Suc RS exE) 1);
d65372e425e5 expandshort; new gcd_induct with inbuilt case analysis
paulson
parents: 4809
diff changeset
    50
by Auto_tac;
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    51
qed "fib_gr_0";
3300
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    52
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    53
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    54
(*Concrete Mathematics, page 278: Cassini's identity*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4812
diff changeset
    55
Goal "fib (Suc (Suc n)) * fib n = \
4710
05e57f1879ee eliminated pred function;
wenzelm
parents: 4686
diff changeset
    56
\              (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n)) - 1 \
3300
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    57
\                              else Suc (fib(Suc n) * fib(Suc n)))";
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    58
by (res_inst_tac [("u","n")] fib.induct 1);
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    59
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
    60
by (stac (read_instantiate [("x", "Suc(Suc ?n)")] fib_Suc_Suc) 3);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    61
by (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2]) 3);
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    62
by (stac fib_Suc3 3);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    63
by (ALLGOALS  (*using [fib_Suc_Suc] here results in a longer proof!*)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    64
    (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2, 
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4385
diff changeset
    65
				       mod_less, mod_Suc])));
3300
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    66
by (ALLGOALS
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    67
    (asm_full_simp_tac
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    68
     (simpset() addsimps ([] @ add_ac @ mult_ac @
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    69
			 [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 
3300
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    70
			  mod_less, mod_Suc]))));
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    71
qed "fib_Cassini";
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    72
4f5ffefa7799 New example of recdef and permutative rewriting
paulson
parents:
diff changeset
    73
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    74
(** Towards Law 6.111 of Concrete Mathematics **)
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    75
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4812
diff changeset
    76
Goal "gcd(fib n, fib (Suc n)) = 1";
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    77
by (res_inst_tac [("u","n")] fib.induct 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    78
by (asm_simp_tac (simpset() addsimps [fib_Suc3, gcd_commute, gcd_add2]) 3);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    79
by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc])));
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    80
qed "gcd_fib_Suc_eq_1"; 
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    81
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    82
val gcd_fib_commute = 
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    83
    read_instantiate_sg (sign_of thy) [("m", "fib m")] gcd_commute;
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    84
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4812
diff changeset
    85
Goal "gcd(fib m, fib (n+m)) = gcd(fib m, fib n)";
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    86
by (simp_tac (simpset() addsimps [gcd_fib_commute]) 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    87
by (case_tac "m=0" 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    88
by (Asm_simp_tac 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    89
by (clarify_tac (claset() addSDs [not0_implies_Suc]) 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    90
by (simp_tac (simpset() addsimps [fib_add]) 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    91
by (asm_simp_tac (simpset() addsimps [add_commute, gcd_non_0]) 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    92
by (asm_simp_tac (simpset() addsimps [gcd_non_0 RS sym]) 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    93
by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    94
qed "gcd_fib_add";
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    95
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    96
Goal "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)";
4812
d65372e425e5 expandshort; new gcd_induct with inbuilt case analysis
paulson
parents: 4809
diff changeset
    97
by (rtac (gcd_fib_add RS sym RS trans) 1);
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    98
by (Asm_simp_tac 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
    99
qed "gcd_fib_diff";
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   100
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   101
Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   102
by (res_inst_tac [("n","n")] less_induct 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   103
by (stac mod_if 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   104
by (Asm_simp_tac 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   105
by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_less, mod_geq, 
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   106
				      not_less_iff_le, diff_less]) 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   107
qed "gcd_fib_mod";
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   108
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   109
(*Law 6.111*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4812
diff changeset
   110
Goal "fib(gcd(m,n)) = gcd(fib m, fib n)";
4812
d65372e425e5 expandshort; new gcd_induct with inbuilt case analysis
paulson
parents: 4809
diff changeset
   111
by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
4809
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   112
by (Asm_simp_tac 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   113
by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   114
by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1);
595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n)
paulson
parents: 4710
diff changeset
   115
qed "fib_gcd";