diff options
Diffstat (limited to 'etc/isa/depends/Primes.ML')
| -rw-r--r-- | etc/isa/depends/Primes.ML | 197 |
1 files changed, 0 insertions, 197 deletions
diff --git a/etc/isa/depends/Primes.ML b/etc/isa/depends/Primes.ML deleted file mode 100644 index 102419da..00000000 --- a/etc/isa/depends/Primes.ML +++ /dev/null @@ -1,197 +0,0 @@ -(* 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"; |