diff options
author | 2000-08-14 21:06:06 +0000 | |
---|---|---|
committer | 2000-08-14 21:06:06 +0000 | |
commit | a0466897230202bff4724a9c91b037ea0862d817 (patch) | |
tree | c985394d68e8f2c5be36a175c32dd2c0f6d5d121 /etc | |
parent | 2bd0d2a681d79f027919aec58661f06a2d184426 (diff) |
Files for testing theorem dependency features.
Diffstat (limited to 'etc')
-rw-r--r-- | etc/isa/depends/Fib.ML | 106 | ||||
-rw-r--r-- | etc/isa/depends/Fib.thy | 17 | ||||
-rw-r--r-- | etc/isa/depends/Primes.ML | 197 | ||||
-rw-r--r-- | etc/isa/depends/Primes.thy | 33 | ||||
-rw-r--r-- | etc/isa/depends/Usedepends.ML | 3 | ||||
-rw-r--r-- | etc/isa/depends/Usedepends.thy | 5 |
6 files changed, 361 insertions, 0 deletions
diff --git a/etc/isa/depends/Fib.ML b/etc/isa/depends/Fib.ML new file mode 100644 index 00000000..eba2f0e0 --- /dev/null +++ b/etc/isa/depends/Fib.ML @@ -0,0 +1,106 @@ +(* 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. +**) + +Delsimps fib.Suc_Suc; + +val [fib_Suc_Suc] = fib.Suc_Suc; +val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc; + +(*Concrete Mathematics, page 280*) +Goal "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 [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3); +by (ALLGOALS + (asm_simp_tac (simpset() addsimps + ([fib_Suc_Suc, add_mult_distrib, add_mult_distrib2])))); +qed "fib_add"; + + +Goal "fib (Suc n) ~= 0"; +by (res_inst_tac [("u","n")] fib.induct 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc]))); +qed "fib_Suc_neq_0"; + +(* Also add 0 < fib (Suc n) *) +Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1]; + +Goal "0<n ==> 0 < fib n"; +by (rtac (not0_implies_Suc RS exE) 1); +by Auto_tac; +qed "fib_gr_0"; + +(*Concrete Mathematics, page 278: Cassini's identity. + It is much easier to prove using integers!*) +Goal "int (fib (Suc (Suc n)) * fib n) = \ +\ (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \ +\ else int (fib(Suc n) * fib(Suc n)) + #1)"; +by (res_inst_tac [("u","n")] fib.induct 1); +by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2); +by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1); +by (asm_full_simp_tac + (simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, + mod_Suc, zmult_int RS sym] @ zmult_ac) 1); +qed "fib_Cassini"; + + + +(** Towards Law 6.111 of Concrete Mathematics **) + +Goal "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 "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 "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)"; +by (rtac (gcd_fib_add RS sym RS trans) 1); +by (Asm_simp_tac 1); +qed "gcd_fib_diff"; + +Goal "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_geq, + not_less_iff_le, diff_less]) 1); +qed "gcd_fib_mod"; + +(*Law 6.111*) +Goal "fib(gcd(m,n)) = gcd(fib m, fib n)"; +by (res_inst_tac [("m","m"),("n","n")] gcd_induct 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 --git a/etc/isa/depends/Fib.thy b/etc/isa/depends/Fib.thy new file mode 100644 index 00000000..9272ed8c --- /dev/null +++ b/etc/isa/depends/Fib.thy @@ -0,0 +1,17 @@ +(* Title: ex/Fib + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1997 University of Cambridge + +The Fibonacci function. Demonstrates the use of recdef. +*) + +Fib = Usedepends + Divides + Primes + + +consts fib :: "nat => nat" +recdef fib "less_than" + zero "fib 0 = 0" + one "fib 1 = 1" + Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)" + +end diff --git a/etc/isa/depends/Primes.ML b/etc/isa/depends/Primes.ML new file mode 100644 index 00000000..102419da --- /dev/null +++ b/etc/isa/depends/Primes.ML @@ -0,0 +1,197 @@ +(* Title: HOL/ex/Primes.ML + ID: $Id$ + Author: Christophe Tabacznyj and Lawrence C Paulson + Copyright 1996 University of Cambridge + +The "divides" relation, the greatest common divisor and Euclid's algorithm + +See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992) +*) + +eta_contract:=false; + +(************************************************) +(** Greatest Common Divisor **) +(************************************************) + +(*** Euclid's Algorithm ***) + + +val [gcd_eq] = gcd.simps; + + +val prems = goal thy + "[| !!m. P m 0; \ +\ !!m n. [| 0<n; P n (m mod n) |] ==> P m n \ +\ |] ==> P (m::nat) (n::nat)"; +by (res_inst_tac [("u","m"),("v","n")] gcd.induct 1); +by (case_tac "n=0" 1); +by (asm_simp_tac (simpset() addsimps prems) 1); +by Safe_tac; +by (asm_simp_tac (simpset() addsimps prems) 1); +qed "gcd_induct"; + + +Goal "gcd(m,0) = m"; +by (Simp_tac 1); +qed "gcd_0"; +Addsimps [gcd_0]; + +Goal "0<n ==> gcd(m,n) = gcd (n, m mod n)"; +by (Asm_simp_tac 1); +qed "gcd_non_0"; + +Delsimps gcd.simps; + +Goal "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 "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"; +by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [gcd_non_0]))); +by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1); +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 "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"; +by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod]))); +qed_spec_mp "gcd_greatest"; + +(*Function gcd yields the Greatest Common Divisor*) +Goalw [is_gcd_def] "is_gcd (gcd(m,n)) m n"; +by (asm_simp_tac (simpset() addsimps [gcd_greatest, gcd_dvd_both]) 1); +qed "is_gcd"; + +(*uniqueness of GCDs*) +Goalw [is_gcd_def] "[| 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 [is_gcd_def] + "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"; +by (Blast_tac 1); +qed "is_gcd_dvd"; + +(** Commutativity **) + +Goalw [is_gcd_def] "is_gcd k m n = is_gcd k n m"; +by (Blast_tac 1); +qed "is_gcd_commute"; + +Goal "gcd(m,n) = gcd(n,m)"; +by (rtac is_gcd_unique 1); +by (rtac is_gcd 2); +by (asm_simp_tac (simpset() addsimps [is_gcd, is_gcd_commute]) 1); +qed "gcd_commute"; + +Goal "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"; +by (rtac is_gcd_unique 1); +by (rtac is_gcd 2); +by (rewtac is_gcd_def); +by (blast_tac (claset() addSIs [gcd_dvd1, gcd_dvd2] + addIs [gcd_greatest, dvd_trans]) 1); +qed "gcd_assoc"; + +Goal "gcd(0,m) = m"; +by (stac gcd_commute 1); +by (rtac gcd_0 1); +qed "gcd_0_left"; + +Goal "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 "k * gcd(m,n) = gcd(k*m, k*n)"; +by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); +by (Asm_full_simp_tac 1); +by (case_tac "k=0" 1); + by (Asm_full_simp_tac 1); +by (asm_full_simp_tac + (simpset() addsimps [mod_geq, gcd_non_0, mod_mult_distrib2]) 1); +qed "gcd_mult_distrib2"; + +Goal "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 "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 "[| 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 [prime_def] "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1"; +by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1); +by Auto_tac; +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.*) +Goal "[| 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 "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); +by Auto_tac; +by (asm_simp_tac (simpset() addsimps [mod_add_self1]) 1); +by (stac gcd_commute 1); +by (stac gcd_non_0 1); +by Safe_tac; +qed "gcd_add"; + +Goal "gcd(m, n+m) = gcd(m,n)"; +by (asm_simp_tac (simpset() addsimps [add_commute, gcd_add]) 1); +qed "gcd_add2"; + +Goal "gcd(m, k*m+n) = gcd(m,n)"; +by (induct_tac "k" 1); +by (asm_simp_tac (simpset() addsimps [gcd_add, add_assoc]) 2); +by (Simp_tac 1); +qed "gcd_add_mult"; + + +(** More multiplication laws **) + +Goal "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 "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"; +by (rtac dvd_anti_sym 1); +by (rtac gcd_dvd_gcd_mult 2); +by (rtac ([relprime_dvd_mult, gcd_dvd2] MRS gcd_greatest) 1); +by (stac mult_commute 2); +by (rtac gcd_dvd1 2); +by (stac gcd_commute 1); +by (asm_simp_tac (simpset() addsimps [gcd_assoc RS sym]) 1); +qed "gcd_mult_cancel"; diff --git a/etc/isa/depends/Primes.thy b/etc/isa/depends/Primes.thy new file mode 100644 index 00000000..fac39463 --- /dev/null +++ b/etc/isa/depends/Primes.thy @@ -0,0 +1,33 @@ +(* Title: HOL/ex/Primes.thy + ID: $Id$ + Author: Christophe Tabacznyj and Lawrence C Paulson + Copyright 1996 University of Cambridge + +The Greatest Common Divisor and Euclid's algorithm + +The "simpset" clause in the recdef declaration used to be necessary when the +two lemmas where not part of the default simpset. +*) + +Primes = Main + + + +consts + is_gcd :: [nat,nat,nat]=>bool (*gcd as a relation*) + gcd :: "nat*nat=>nat" (*Euclid's algorithm *) + coprime :: [nat,nat]=>bool + prime :: nat set + +recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)" +(* simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" *) + "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" + +defs + is_gcd_def "is_gcd p m n == p dvd m & p dvd n & + (ALL d. d dvd m & d dvd n --> d dvd p)" + + coprime_def "coprime m n == gcd(m,n) = 1" + + prime_def "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}" + +end diff --git a/etc/isa/depends/Usedepends.ML b/etc/isa/depends/Usedepends.ML new file mode 100644 index 00000000..7557d6e8 --- /dev/null +++ b/etc/isa/depends/Usedepends.ML @@ -0,0 +1,3 @@ +use "~/ProofGeneral/isa/depends.ML"; + + diff --git a/etc/isa/depends/Usedepends.thy b/etc/isa/depends/Usedepends.thy new file mode 100644 index 00000000..4f8eb516 --- /dev/null +++ b/etc/isa/depends/Usedepends.thy @@ -0,0 +1,5 @@ +(* dummy theory to load depends.ML *) +theory Usedepends = Main: +end + + |