# HG changeset patch # User paulson # Date 893061420 -7200 # Node ID 595f905cc34891efec082d0229246b36fbd4ea0c # Parent 995bc5bd8319c62edee7ed40d8db2b9c9087c3c7 proving fib(gcd(m,n)) = gcd(fib m, fib n) diff -r 995bc5bd8319 -r 595f905cc348 src/HOL/ex/Fib.ML --- 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 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 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"; diff -r 995bc5bd8319 -r 595f905cc348 src/HOL/ex/Fib.thy --- 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" diff -r 995bc5bd8319 -r 595f905cc348 src/HOL/ex/Primes.ML --- 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 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"; diff -r 995bc5bd8319 -r 595f905cc348 src/HOL/ex/ROOT.ML --- 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";