# HG changeset patch
# User paulson
# Date 864306683 -7200
# Node ID 4f5ffefa77992abf6d5f74d699e1cc44ac50d97e
# Parent  8adf24153732d4f09eae0e5223e220bcf70c7cb8
New example of recdef and permutative rewriting

diff -r 8adf24153732 -r 4f5ffefa7799 src/HOL/ex/Fib.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Fib.ML	Thu May 22 15:11:23 1997 +0200
@@ -0,0 +1,66 @@
+(*  Title:      HOL/ex/Fib
+    ID:         $Id$
+    Author:     Lawrence C Paulson
+    Copyright   1997  University of Cambridge
+
+Fibonacci numbers: proofs of laws taken from
+
+  R. L. Graham, D. E. Knuth, O. Patashnik.
+  Concrete Mathematics.
+  (Addison-Wesley, 1989)
+*)
+
+
+(** The difficulty in these proofs is to ensure that the induction hypotheses
+    are applied before the definition of "fib".  Towards this end, the 
+    "fib" equations are not added to the simpset and are applied very 
+    selectively at first.
+**)
+
+bind_thm ("fib_Suc_Suc", hd(rev fib.rules));
+
+
+(*Concrete Mathematics, page 280*)
+goal thy "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
+by (res_inst_tac [("u","n")] fib.induct 1);
+(*Simplify the LHS just enough to apply the induction hypotheses*)
+by (asm_full_simp_tac
+    (!simpset addsimps [read_instantiate[("x", "Suc(?m+?n)")] fib_Suc_Suc]) 3);
+by (ALLGOALS 
+    (asm_simp_tac (!simpset addsimps 
+		   (fib.rules @ add_ac @ mult_ac @
+		    [add_mult_distrib, add_mult_distrib2]))));
+qed "fib_add";
+
+
+goal thy "fib (Suc n) ~= 0";
+by (res_inst_tac [("u","n")] fib.induct 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps fib.rules)));
+qed "fib_Suc_neq_0";
+Addsimps [fib_Suc_neq_0];
+
+
+
+(*Concrete Mathematics, page 278: Cassini's identity*)
+goal thy "fib (Suc (Suc n)) * fib n = \
+\              (if n mod 2 = 0 then pred(fib(Suc n) * fib(Suc n)) \
+\                              else Suc (fib(Suc n) * fib(Suc n)))";
+by (res_inst_tac [("u","n")] fib.induct 1);
+by (res_inst_tac [("P", "%z. ?ff(x) * z = ?kk(x)")] (fib_Suc_Suc RS ssubst) 3);
+by (stac (read_instantiate [("x", "Suc(Suc ?n)")] fib_Suc_Suc) 3);
+by (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2]) 3);
+by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3);
+by (ALLGOALS  (*using fib.rules here results in a longer proof!*)
+    (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2, 
+				      mod_less, mod_Suc]
+                            setloop split_tac[expand_if])));
+by (step_tac (!claset addSDs [mod2_neq_0]) 1);
+by (ALLGOALS
+    (asm_full_simp_tac
+     (!simpset addsimps (fib.rules @ add_ac @ mult_ac @
+			 [add_mult_distrib, add_mult_distrib2, 
+			  mod_less, mod_Suc]))));
+qed "fib_Cassini";
+
+
+(** exercise: prove gcd(fib m, fib n) = fib(gcd(m,n)) **)
diff -r 8adf24153732 -r 4f5ffefa7799 src/HOL/ex/Fib.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Fib.thy	Thu May 22 15:11:23 1997 +0200
@@ -0,0 +1,18 @@
+(*  Title:      ex/Fib
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Fibonacci numbers and other simple examples of recursive definitions
+	(the TFL package)
+*)
+
+Fib = WF_Rel +
+
+consts fib  :: "nat => nat"
+recdef fib "less_than"
+    "fib 0 = 0"
+    "fib 1 = 1"
+    "fib (Suc(Suc x)) = (fib x + fib (Suc x))"
+
+end