proving fib(gcd(m,n)) = gcd(fib m, fib n)

--- a/src/HOL/ex/Fib.ML	Sun Apr 19 17:01:04 1998 +0200
+++ b/src/HOL/ex/Fib.ML	Mon Apr 20 10:37:00 1998 +0200
@@ -17,8 +17,12 @@
     selectively at first.
 **)
 
-bind_thm ("fib_Suc_Suc", hd(rev fib.rules));
+val [fib_0, fib_1, fib_Suc_Suc] = fib.rules;
 
+Addsimps [fib_0, fib_1];
+
+
+val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc;
 
 (*Concrete Mathematics, page 280*)
 goal thy "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
@@ -28,23 +32,23 @@
     (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]))));
+		   ([] @ add_ac @ mult_ac @
+		    [fib_Suc_Suc, 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)));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc])));
 qed "fib_Suc_neq_0";
-Addsimps [fib_Suc_neq_0];
 
-goal thy "0 < fib (Suc n)";
-by (res_inst_tac [("u","n")] fib.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps fib.rules)));
-qed "fib_Suc_gr_0";
-Addsimps [fib_Suc_gr_0];
+(* Also add  0 < fib (Suc n) *)
+Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1];
 
+goal thy "!!n. 0<n ==> 0 < fib n";
+br (not0_implies_Suc RS exE) 1;
+auto();
+qed "fib_gr_0";
 
 
 (*Concrete Mathematics, page 278: Cassini's identity*)
@@ -55,16 +59,58 @@
 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!*)
+by (stac fib_Suc3 3);
+by (ALLGOALS  (*using [fib_Suc_Suc] here results in a longer proof!*)
     (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2, 
 				       mod_less, mod_Suc])));
 by (ALLGOALS
     (asm_full_simp_tac
-     (simpset() addsimps (fib.rules @ add_ac @ mult_ac @
-			 [add_mult_distrib, add_mult_distrib2, 
+     (simpset() addsimps ([] @ add_ac @ mult_ac @
+			 [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 
 			  mod_less, mod_Suc]))));
 qed "fib_Cassini";
 
 
-(** exercise: prove gcd(fib m, fib n) = fib(gcd(m,n)) **)
+(** Towards Law 6.111 of Concrete Mathematics **)
+
+goal thy "gcd(fib n, fib (Suc n)) = 1";
+by (res_inst_tac [("u","n")] fib.induct 1);
+by (asm_simp_tac (simpset() addsimps [fib_Suc3, gcd_commute, gcd_add2]) 3);
+by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc])));
+qed "gcd_fib_Suc_eq_1"; 
+
+val gcd_fib_commute = 
+    read_instantiate_sg (sign_of thy) [("m", "fib m")] gcd_commute;
+
+goal thy "gcd(fib m, fib (n+m)) = gcd(fib m, fib n)";
+by (simp_tac (simpset() addsimps [gcd_fib_commute]) 1);
+by (case_tac "m=0" 1);
+by (Asm_simp_tac 1);
+by (clarify_tac (claset() addSDs [not0_implies_Suc]) 1);
+by (simp_tac (simpset() addsimps [fib_add]) 1);
+by (asm_simp_tac (simpset() addsimps [add_commute, gcd_non_0]) 1);
+by (asm_simp_tac (simpset() addsimps [gcd_non_0 RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1);
+qed "gcd_fib_add";
+
+goal thy "!!m. m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)";
+br (gcd_fib_add RS sym RS trans) 1;
+by (Asm_simp_tac 1);
+qed "gcd_fib_diff";
+
+goal thy "!!m. 0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
+by (res_inst_tac [("n","n")] less_induct 1);
+by (stac mod_if 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_less, mod_geq, 
+				      not_less_iff_le, diff_less]) 1);
+qed "gcd_fib_mod";
+
+(*Law 6.111*)
+goal thy "fib(gcd(m,n)) = gcd(fib m, fib n)";
+by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
+by (case_tac "n=0" 1);
+by (Asm_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1);
+by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1);
+qed "fib_gcd";

--- a/src/HOL/ex/Fib.thy	Sun Apr 19 17:01:04 1998 +0200
+++ b/src/HOL/ex/Fib.thy	Mon Apr 20 10:37:00 1998 +0200
@@ -6,7 +6,7 @@
 The Fibonacci function.  Demonstrates the use of recdef.
 *)
 
-Fib = WF_Rel + Divides +
+Fib = WF_Rel + Divides + Primes +
 
 consts fib  :: "nat => nat"
 recdef fib "less_than"

--- a/src/HOL/ex/Primes.ML	Sun Apr 19 17:01:04 1998 +0200
+++ b/src/HOL/ex/Primes.ML	Mon Apr 20 10:37:00 1998 +0200
@@ -33,48 +33,92 @@
 by (rtac (gcd_eq RS trans) 1);
 by (Simp_tac 1);
 qed "gcd_0";
+Addsimps [gcd_0];
 
 goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
 by (rtac (gcd_eq RS trans) 1);
 by (Asm_simp_tac 1);
 by (Blast_tac 1);
-qed "gcd_less_0";
-Addsimps [gcd_0, gcd_less_0];
+qed "gcd_non_0";
 
-goal thy "gcd(m,0) dvd m";
-by (Simp_tac 1);
-qed "gcd_0_dvd_m";
-
-goal thy "gcd(m,0) dvd 0";
-by (Simp_tac 1);
-qed "gcd_0_dvd_0";
+goal thy "gcd(m,1) = 1";
+by (simp_tac (simpset() addsimps [gcd_non_0]) 1);
+qed "gcd_1";
+Addsimps [gcd_1];
 
 (*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
 goal thy "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)";
 by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
 by (case_tac "n=0" 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mod_less_divisor])));
+by (ALLGOALS 
+    (asm_full_simp_tac (simpset() addsimps [gcd_non_0, mod_less_divisor])));
 by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1);
-qed "gcd_divides_both";
+qed "gcd_dvd_both";
+
+bind_thm ("gcd_dvd1", gcd_dvd_both RS conjunct1);
+bind_thm ("gcd_dvd2", gcd_dvd_both RS conjunct2);
+
 
 (*Maximality: for all m,n,f naturals, 
                 if f divides m and f divides n then f divides gcd(m,n)*)
 goal thy "!!k. (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
 by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
 by (case_tac "n=0" 1);
-by (ALLGOALS(asm_full_simp_tac(simpset() addsimps[dvd_mod,mod_less_divisor])));
+by (ALLGOALS
+    (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod,
+					   mod_less_divisor])));
 qed_spec_mp "gcd_greatest";
 
 (*Function gcd yields the Greatest Common Divisor*)
 goalw thy [is_gcd_def] "is_gcd (gcd(m,n)) m n";
-by (asm_simp_tac (simpset() addsimps [gcd_greatest, gcd_divides_both]) 1);
+by (asm_simp_tac (simpset() addsimps [gcd_greatest, gcd_dvd_both]) 1);
 qed "is_gcd";
 
 (*uniqueness of GCDs*)
-goalw thy [is_gcd_def] "is_gcd m a b & is_gcd n a b --> m=n";
+goalw thy [is_gcd_def] "!!m n. [| is_gcd m a b; is_gcd n a b |] ==> m=n";
 by (blast_tac (claset() addIs [dvd_anti_sym]) 1);
 qed "is_gcd_unique";
 
+(*USED??*)
+goalw thy [is_gcd_def]
+    "!!m n. [| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m";
+by (Blast_tac 1);
+qed "is_gcd_dvd";
+
+(** Commutativity **)
+
+goalw thy [is_gcd_def] "is_gcd k m n = is_gcd k n m";
+by (Blast_tac 1);
+qed "is_gcd_commute";
+
+goal thy "gcd(m,n) = gcd(n,m)";
+br is_gcd_unique 1;
+br is_gcd 2;
+by (asm_simp_tac (simpset() addsimps [is_gcd, is_gcd_commute]) 1);
+qed "gcd_commute";
+
+goal thy "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))";
+br is_gcd_unique 1;
+br is_gcd 2;
+bw is_gcd_def;
+by (blast_tac (claset() addSIs [gcd_dvd1, gcd_dvd2]
+   	                addIs  [gcd_greatest, dvd_trans]) 1);
+qed "gcd_assoc";
+
+goal thy "gcd(0,m) = m";
+by (stac gcd_commute 1);
+by (rtac gcd_0 1);
+qed "gcd_0_left";
+
+goal thy "gcd(1,m) = 1";
+by (stac gcd_commute 1);
+by (rtac gcd_1 1);
+qed "gcd_1_left";
+Addsimps [gcd_0_left, gcd_1_left];
+
+
+(** Multiplication laws **)
+
 (*Davenport, page 27*)
 goal thy "k * gcd(m,n) = gcd(k*m, k*n)";
 by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
@@ -82,18 +126,70 @@
  by(Asm_full_simp_tac 1);
 by (case_tac "n=0" 1);
  by(Asm_full_simp_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [mod_geq, mod_mult_distrib2]) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [mod_geq, gcd_non_0, mod_mult_distrib2]) 1);
 qed "gcd_mult_distrib2";
 
+goal thy "gcd(m,m) = m";
+by (cut_inst_tac [("k","m"),("m","1"),("n","1")] gcd_mult_distrib2 1);
+by (Asm_full_simp_tac 1);
+qed "gcd_self";
+Addsimps [gcd_self];
+
+goal thy "gcd(k, k*n) = k";
+by (cut_inst_tac [("k","k"),("m","1"),("n","n")] gcd_mult_distrib2 1);
+by (Asm_full_simp_tac 1);
+qed "gcd_mult";
+Addsimps [gcd_mult];
+
+goal thy "!!k. [| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
+by (subgoal_tac "m = gcd(m*k, m*n)" 1);
+by (etac ssubst 1 THEN rtac gcd_greatest 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym])));
+qed "relprime_dvd_mult";
+
+goalw thy [prime_def] "!!p. [| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1";
+by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1);
+by (fast_tac (claset() addSss (simpset())) 1);
+qed "prime_imp_relprime";
+
 (*This theorem leads immediately to a proof of the uniqueness of factorization.
   If p divides a product of primes then it is one of those primes.*)
-goalw thy [prime_def] "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
-by (Clarify_tac 1);
-by (subgoal_tac "m = gcd(m*p, m*n)" 1);
-by (etac ssubst 1);
-by (rtac gcd_greatest 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym])));
-(*Now deduce  gcd(p,n)=1  to finish the proof*)
-by (cut_inst_tac [("m","p"),("n","n")] gcd_divides_both 1);
-by (fast_tac (claset() addSss (simpset())) 1);
+goal thy "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
+by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime]) 1);
 qed "prime_dvd_mult";
+
+
+(** Addition laws **)
+
+goal thy "gcd(m, m+n) = gcd(m,n)";
+by (res_inst_tac [("n1", "m+n")] (gcd_commute RS ssubst) 1);
+by (rtac (gcd_eq RS trans) 1);
+auto();
+by (asm_simp_tac (simpset() addsimps [mod_add_cancel1]) 1);
+by (stac gcd_commute 1);
+by (stac gcd_non_0 1);
+by Safe_tac;
+qed "gcd_add";
+
+goal thy "gcd(m, n+m) = gcd(m,n)";
+by (asm_simp_tac (simpset() addsimps [add_commute, gcd_add]) 1);
+qed "gcd_add2";
+
+
+(** More multiplication laws **)
+
+goal thy "gcd(m,n) dvd gcd(k*m, n)";
+by (blast_tac (claset() addIs [gcd_greatest, dvd_trans, 
+                               gcd_dvd1, gcd_dvd2]) 1);
+qed "gcd_dvd_gcd_mult";
+
+goal thy "!!n. gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)";
+br dvd_anti_sym 1;
+br gcd_dvd_gcd_mult 2;
+br ([relprime_dvd_mult, gcd_dvd2] MRS gcd_greatest) 1;
+by (stac mult_commute 2);
+br gcd_dvd1 2;
+by (stac gcd_commute 1);
+by (asm_simp_tac (simpset() addsimps [gcd_assoc RS sym]) 1);
+qed "gcd_mult_cancel";

--- a/src/HOL/ex/ROOT.ML	Sun Apr 19 17:01:04 1998 +0200
+++ b/src/HOL/ex/ROOT.ML	Mon Apr 20 10:37:00 1998 +0200
@@ -13,8 +13,8 @@
 
 (**Some examples of recursive function definitions: the TFL package**)
 time_use_thy "Recdef";
+time_use_thy "Primes";
 time_use_thy "Fib";
-time_use_thy "Primes";
 time_use_thy "Primrec";
 
 time_use_thy "NatSum";