--- a/src/HOL/IsaMakefile Tue Sep 12 22:13:23 2000 +0200
+++ b/src/HOL/IsaMakefile Wed Sep 13 18:45:10 2000 +0200
@@ -173,6 +173,8 @@
HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
$(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \
+ NumberTheory/Fib.ML NumberTheory/Fib.thy NumberTheory/Primes.thy \
+ NumberTheory/Factorization.ML NumberTheory/Factorization.thy \
NumberTheory/BijectionRel.ML NumberTheory/BijectionRel.thy \
NumberTheory/Chinese.ML NumberTheory/Chinese.thy \
NumberTheory/EulerFermat.ML NumberTheory/EulerFermat.thy \
@@ -430,8 +432,6 @@
$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.ML ex/AVL.thy ex/BT.ML ex/BT.thy \
ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML ex/NatSum.thy \
- ex/Fib.ML ex/Fib.thy ex/Primes.thy \
- ex/Factorization.ML ex/Factorization.thy \
ex/Primrec.ML ex/Primrec.thy \
ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \
ex/ROOT.ML ex/Recdefs.ML ex/Recdefs.thy ex/cla.ML \
--- a/src/HOL/Isar_examples/ROOT.ML Tue Sep 12 22:13:23 2000 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML Wed Sep 13 18:45:10 2000 +0200
@@ -13,8 +13,8 @@
time_use_thy "Summation";
time_use_thy "KnasterTarski";
time_use_thy "MutilatedCheckerboard";
-with_path "../Induct" time_use_thy "MultisetOrder";
-with_path "../W0" time_use_thy "W_correct";
-with_path "../ex" time_use_thy "Fibonacci";
+with_path "../Induct" time_use_thy "MultisetOrder";
+with_path "../W0" time_use_thy "W_correct";
+with_path "../NumberTheory" time_use_thy "Fibonacci";
time_use_thy "Puzzle";
time_use_thy "NestedDatatype";
--- a/src/HOL/ex/Factorization.ML Tue Sep 12 22:13:23 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,312 +0,0 @@
-(* Title: HOL/ex/Factorization.thy
- ID: $Id$
- Author: Thomas Marthedal Rasmussen
- Copyright 2000 University of Cambridge
-
-Fundamental Theorem of Arithmetic (unique factorization into primes)
-*)
-
-val prime_def = thm "prime_def";
-val prime_dvd_mult = thm "prime_dvd_mult";
-
-
-(* --- Arithmetic --- *)
-
-Goal "!!m::nat. [| m ~= m*k; m ~= 1 |] ==> 1<m";
-by (case_tac "m" 1);
-by Auto_tac;
-qed "one_less_m";
-
-Goal "!!m::nat. [| m ~= m*k; 1<m*k |] ==> 1<k";
-by (case_tac "k" 1);
-by Auto_tac;
-qed "one_less_k";
-
-Goal "!!m::nat. [| 0<k; k*n=k*m |] ==> n=m";
-by Auto_tac;
-qed "mult_left_cancel";
-
-Goal "!!m::nat. [| 0<m; m*n = m |] ==> n=1";
-by (case_tac "n" 1);
-by Auto_tac;
-qed "mn_eq_m_one";
-
-Goal "!!m::nat. [| 0<n; 0<k |] ==> 1<m --> m*n = k --> n<k";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed_spec_mp "prod_mn_less_k";
-
-
-(* --- Prime List & Product --- *)
-
-Goal "prod (xs @ ys) = prod xs * prod ys";
-by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [mult_assoc])));
-qed "prod_append";
-
-Goal "prod (x#xs) = prod (y#ys) ==> x*prod xs = y*prod ys";
-by Auto_tac;
-qed "prod_xy_prod";
-
-Goalw [primel_def] "primel (xs @ ys) = (primel xs & primel ys)";
-by Auto_tac;
-qed "primel_append";
-
-Goalw [primel_def] "n:prime ==> primel [n] & prod [n] = n";
-by Auto_tac;
-qed "prime_primel";
-
-Goalw [prime_def,dvd_def] "p:prime ==> ~(p dvd 1)";
-by Auto_tac;
-by (case_tac "k" 1);
-by Auto_tac;
-qed "prime_nd_one";
-
-Goalw [dvd_def] "[| prod (x#xs) = prod ys |] ==> x dvd (prod ys)";
-by (rtac exI 1);
-by (rtac sym 1);
-by (Asm_full_simp_tac 1);
-qed "hd_dvd_prod";
-
-Goalw [primel_def] "primel (x#xs) ==> primel xs";
-by Auto_tac;
-qed "primel_tl";
-
-Goalw [primel_def] "(primel (x#xs)) = (x:prime & primel xs)";
-by Auto_tac;
-qed "primel_hd_tl";
-
-Goalw [prime_def] "[| p:prime; q:prime; p dvd q |] ==> p=q";
-by Auto_tac;
-qed "primes_eq";
-
-Goalw [primel_def,prime_def] "[| primel xs; prod xs = 1 |] ==> xs = []";
-by (case_tac "xs" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "primel_one_empty";
-
-Goalw [prime_def] "p:prime ==> 1<p";
-by Auto_tac;
-qed "prime_g_one";
-
-Goalw [prime_def] "p:prime ==> 0<p";
-by Auto_tac;
-qed "prime_g_zero";
-
-Goalw [primel_def,prime_def] "primel xs --> xs ~= [] --> 1 < prod xs";
-by (induct_tac "xs" 1);
-by (auto_tac (claset() addEs [one_less_mult], simpset()));
-qed_spec_mp "primel_nempty_g_one";
-
-Goalw [primel_def,prime_def] "primel xs --> 0 < prod xs";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed_spec_mp "primel_prod_gz";
-
-
-(* --- Sorting --- *)
-
-Goal "nondec xs --> nondec (oinsert x xs)";
-by (induct_tac "xs" 1);
-by (case_tac "list" 2);
-by (ALLGOALS(asm_full_simp_tac (simpset()delcongs[thm"list.weak_case_cong"])));
-qed_spec_mp "nondec_oinsert";
-
-Goal "nondec (sort xs)";
-by (induct_tac "xs" 1);
-by (ALLGOALS (Asm_full_simp_tac));
-by (etac nondec_oinsert 1);
-qed "nondec_sort";
-
-Goal "[| x<=y; l=y#ys |] ==> x#l = oinsert x l";
-by (ALLGOALS Asm_full_simp_tac);
-qed "x_less_y_oinsert";
-
-Goal "nondec xs --> xs = sort xs";
-by (induct_tac "xs" 1);
-by Safe_tac;
-by (ALLGOALS Asm_full_simp_tac);
-by (case_tac "list" 1);
-by (ALLGOALS Asm_full_simp_tac);
-by (case_tac "list" 1);
-by (Asm_full_simp_tac 1);
-by (res_inst_tac [("y","aa"),("ys","lista")] x_less_y_oinsert 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed_spec_mp "nondec_sort_eq";
-
-Goal "oinsert x (oinsert y l) = oinsert y (oinsert x l)";
-by (induct_tac "l" 1);
-by Auto_tac;
-qed "oinsert_x_y";
-
-
-(* --- Permutation --- *)
-
-Goalw [primel_def] "xs <~~> ys ==> primel xs --> primel ys";
-by (etac perm.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed_spec_mp "perm_primel";
-
-Goal "xs <~~> ys ==> prod xs = prod ys";
-by (etac perm.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));
-qed_spec_mp "perm_prod";
-
-Goal "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys";
-by (etac perm.induct 1);
-by Auto_tac;
-qed "perm_subst_oinsert";
-
-Goal "x#xs <~~> oinsert x xs";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "perm_oinsert";
-
-Goal "xs <~~> sort xs";
-by (induct_tac "xs" 1);
-by (auto_tac (claset() addIs [perm_oinsert]
- addEs [perm_subst_oinsert],
- simpset()));
-qed "perm_sort";
-
-Goal "xs <~~> ys ==> sort xs = sort ys";
-by (etac perm.induct 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [oinsert_x_y])));
-qed "perm_sort_eq";
-
-
-(* --- Existence --- *)
-
-Goal "primel xs ==> EX ys. primel ys & nondec ys & prod ys = prod xs";
-by (blast_tac (claset() addIs [nondec_sort, perm_prod,perm_primel,perm_sort,
- perm_sym]) 1);
-qed "ex_nondec_lemma";
-
-Goalw [prime_def,dvd_def]
- "1<n & n~:prime --> (EX m k.1<m & 1<k & m<n & k<n & n=m*k)";
-by (auto_tac (claset() addIs [n_less_m_mult_n, n_less_n_mult_m,
- one_less_m, one_less_k],
- simpset()));
-qed_spec_mp "not_prime_ex_mk";
-
-Goal "[| primel xs; primel ys |] \
-\ ==> EX l. primel l & prod l = prod xs * prod ys";
-by (rtac exI 1);
-by Safe_tac;
-by (rtac prod_append 2);
-by (asm_simp_tac (simpset() addsimps [primel_append]) 1);
-qed "split_primel";
-
-Goal "1<n --> (EX l. primel l & prod l = n)";
-by (induct_thm_tac nat_less_induct "n" 1);
-by (rtac impI 1);
-by (case_tac "n:prime" 1);
-by (rtac exI 1);
-by (etac prime_primel 1);
-by (cut_inst_tac [("n","n")] not_prime_ex_mk 1);
-by (auto_tac (claset() addSIs [split_primel], simpset()));
-qed_spec_mp "factor_exists";
-
-Goal "1<n ==> (EX l. primel l & nondec l & prod l = n)";
-by (etac (factor_exists RS exE) 1);
-by (blast_tac (claset() addSIs [ex_nondec_lemma]) 1);
-qed "nondec_factor_exists";
-
-
-(* --- Uniqueness --- *)
-
-Goal "p:prime ==> p dvd (prod xs) --> (EX m. m:set xs & p dvd m)";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_full_simp_tac);
-by (etac prime_nd_one 1);
-by (rtac impI 1);
-by (dtac prime_dvd_mult 1);
-by Auto_tac;
-qed_spec_mp "prime_dvd_mult_list";
-
-Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
-\ ==> EX m. m :set ys & x dvd m";
-by (rtac prime_dvd_mult_list 1);
-by (etac hd_dvd_prod 2);
-by (asm_full_simp_tac (simpset() addsimps [primel_hd_tl]) 1);
-qed "hd_xs_dvd_prod";
-
-Goal "[| primel (x#xs); primel ys; m:set ys; x dvd m |] ==> x=m";
-by (rtac primes_eq 1);
-by (auto_tac (claset(), simpset() addsimps [primel_def,primel_hd_tl]));
-qed "prime_dvd_eq";
-
-Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] ==> x:set ys";
-by (ftac hd_xs_dvd_prod 1);
-by Auto_tac;
-by (dtac prime_dvd_eq 1);
-by Auto_tac;
-qed "hd_xs_eq_prod";
-
-Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
-\ ==> EX l. ys <~~> (x#l)";
-by (rtac exI 1);
-by (rtac perm_remove 1);
-by (etac hd_xs_eq_prod 1);
-by (ALLGOALS assume_tac);
-qed "perm_primel_ex";
-
-Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \
-\ ==> prod xs < prod ys";
-by (auto_tac (claset() addIs [prod_mn_less_k,prime_g_one,primel_prod_gz],
- simpset() addsimps [primel_hd_tl]));
-qed "primel_prod_less";
-
-Goal "[| primel xs; p*prod xs = p; p:prime |] ==> xs=[]";
-by (auto_tac (claset() addIs [primel_one_empty,mn_eq_m_one,prime_g_zero],
- simpset()));
-qed "prod_one_empty";
-
-Goal "[| ALL m. m < prod ys --> (ALL xs ys. primel xs & primel ys & \
-\ prod xs = prod ys & prod xs = m --> xs <~~> ys); primel list; \
-\ primel x; prod list = prod x; prod x < prod ys |] ==> x <~~> list";
-by (Asm_full_simp_tac 1);
-qed "uniq_ex_lemma";
-
-Goal "ALL xs ys. (primel xs & primel ys & prod xs = prod ys & prod xs = n \
-\ --> xs <~~> ys)";
-by (induct_thm_tac nat_less_induct "n" 1);
-by Safe_tac;
-by (case_tac "xs" 1);
-by (force_tac (claset() addIs [primel_one_empty], simpset()) 1);
-by (rtac (perm_primel_ex RS exE) 1);
-by (ALLGOALS Asm_full_simp_tac);
-by (rtac (perm.trans RS perm_sym) 1);
-by (assume_tac 1);
-by (rtac perm.Cons 1);
-by (case_tac "x=[]" 1);
-by (asm_full_simp_tac (simpset() addsimps [perm_sing_eq,primel_hd_tl]) 1);
-by (res_inst_tac [("p","a")] prod_one_empty 1);
-by (ALLGOALS Asm_full_simp_tac);
-by (etac uniq_ex_lemma 1);
-by (auto_tac (claset() addIs [primel_tl,perm_primel],
- simpset() addsimps [primel_hd_tl]));
-by (res_inst_tac [("k","a"),("n","prod list"),("m","prod x")] mult_left_cancel 1);
-by (res_inst_tac [("x","a")] primel_prod_less 3);
-by (rtac prod_xy_prod 2);
-by (res_inst_tac [("s","prod ys")] trans 2);
-by (etac perm_prod 3);
-by (etac (perm_prod RS sym) 5);
-by (auto_tac (claset() addIs [perm_primel,prime_g_zero], simpset()));
-qed_spec_mp "factor_unique";
-
-Goal "[| xs <~~> ys; nondec xs; nondec ys |] ==> xs = ys";
-by (rtac trans 1);
-by (rtac trans 1);
-by (etac nondec_sort_eq 1);
-by (etac perm_sort_eq 1);
-by (etac (nondec_sort_eq RS sym) 1);
-qed "perm_nondec_unique";
-
-Goal "ALL n. 1<n --> (EX! l. primel l & nondec l & prod l = n)";
-by Safe_tac;
-by (etac nondec_factor_exists 1);
-by (rtac perm_nondec_unique 1);
-by (rtac factor_unique 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed_spec_mp "unique_prime_factorization";
--- a/src/HOL/ex/Factorization.thy Tue Sep 12 22:13:23 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(* Title: HOL/ex/Factorization.thy
- ID: $Id$
- Author: Thomas Marthedal Rasmussen
- Copyright 2000 University of Cambridge
-
-Fundamental Theorem of Arithmetic (unique factorization into primes)
-*)
-
-
-Factorization = Primes + Perm +
-
-consts
- primel :: nat list => bool
- nondec :: nat list => bool
- prod :: nat list => nat
- oinsert :: [nat, nat list] => nat list
- sort :: nat list => nat list
-
-defs
- primel_def "primel xs == set xs <= prime"
-
-primrec
- "nondec [] = True"
- "nondec (x#xs) = (case xs of [] => True | y#ys => x<=y & nondec xs)"
-
-primrec
- "prod [] = 1"
- "prod (x#xs) = x * prod xs"
-
-primrec
- "oinsert x [] = [x]"
- "oinsert x (y#ys) = (if x<=y then x#y#ys else y#oinsert x ys)"
-
-primrec
- "sort [] = []"
- "sort (x#xs) = oinsert x (sort xs)"
-
-end
\ No newline at end of file
--- a/src/HOL/ex/Fib.ML Tue Sep 12 22:13:23 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,113 +0,0 @@
-(* 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 (induct_thm_tac fib.induct "n" 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 (induct_thm_tac fib.induct "n" 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 (induct_thm_tac fib.induct "n" 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 **)
-
-val gcd_induct = thm "gcd_induct";
-val gcd_commute = thm "gcd_commute";
-val gcd_add2 = thm "gcd_add2";
-val gcd_non_0 = thm "gcd_non_0";
-val gcd_mult_cancel = thm "gcd_mult_cancel";
-
-
-Goal "gcd(fib n, fib (Suc n)) = 1";
-by (induct_thm_tac fib.induct "n" 1);
-by (asm_simp_tac (simpset() addsimps [gcd_commute, fib_Suc3]) 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 (induct_thm_tac nat_less_induct "n" 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 (induct_thm_tac gcd_induct "m n" 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 Tue Sep 12 22:13:23 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(* 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 = 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
--- a/src/HOL/ex/Primes.thy Tue Sep 12 22:13:23 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,208 +0,0 @@
-(* 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
-
-See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992)
-*)
-
-theory Primes = Main:
-consts
- gcd :: "nat*nat=>nat" (*Euclid's algorithm *)
-
-recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
- "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
-
-constdefs
- is_gcd :: "[nat,nat,nat]=>bool" (*gcd as a relation*)
- "is_gcd p m n == p dvd m & p dvd n &
- (ALL d. d dvd m & d dvd n --> d dvd p)"
-
- coprime :: "[nat,nat]=>bool"
- "coprime m n == gcd(m,n) = 1"
-
- prime :: "nat set"
- "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
-
-
-(************************************************)
-(** Greatest Common Divisor **)
-(************************************************)
-
-(*** Euclid's Algorithm ***)
-
-
-lemma gcd_induct:
- "[| !!m. P m 0;
- !!m n. [| 0<n; P n (m mod n) |] ==> P m n
- |] ==> P (m::nat) (n::nat)"
- apply (induct_tac m n rule: gcd.induct)
- apply (case_tac "n=0")
- apply (simp_all)
- done
-
-
-lemma gcd_0 [simp]: "gcd(m,0) = m"
- apply (simp);
- done
-
-lemma gcd_non_0: "0<n ==> gcd(m,n) = gcd (n, m mod n)"
- apply (simp)
- done;
-
-declare gcd.simps [simp del];
-
-lemma gcd_1 [simp]: "gcd(m,1) = 1"
- apply (simp add: gcd_non_0)
- done
-
-(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*)
-lemma gcd_dvd_both: "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"
- apply (induct_tac m n rule: gcd_induct)
- apply (simp_all add: gcd_non_0)
- apply (blast dest: dvd_mod_imp_dvd)
- done
-
-lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1]
-lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2];
-
-
-(*Maximality: for all m,n,k naturals,
- if k divides m and k divides n then k divides gcd(m,n)*)
-lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
- apply (induct_tac m n rule: gcd_induct)
- apply (simp_all add: gcd_non_0 dvd_mod);
- done;
-
-lemma gcd_greatest_iff [iff]: "k dvd gcd(m,n) = (k dvd m & k dvd n)"
- apply (blast intro!: gcd_greatest intro: dvd_trans);
- done;
-
-(*Function gcd yields the Greatest Common Divisor*)
-lemma is_gcd: "is_gcd (gcd(m,n)) m n"
- apply (simp add: is_gcd_def gcd_greatest)
- done
-
-(*uniqueness of GCDs*)
-lemma is_gcd_unique: "[| is_gcd m a b; is_gcd n a b |] ==> m=n"
- apply (simp add: is_gcd_def);
- apply (blast intro: dvd_anti_sym)
- done
-
-lemma is_gcd_dvd: "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"
- apply (auto simp add: is_gcd_def);
- done
-
-(** Commutativity **)
-
-lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
- apply (auto simp add: is_gcd_def);
- done
-
-lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
- apply (rule is_gcd_unique)
- apply (rule is_gcd)
- apply (subst is_gcd_commute)
- apply (simp add: is_gcd)
- done
-
-lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"
- apply (rule is_gcd_unique)
- apply (rule is_gcd)
- apply (simp add: is_gcd_def);
- apply (blast intro: dvd_trans);
- done
-
-lemma gcd_0_left [simp]: "gcd(0,m) = m"
- apply (simp add: gcd_commute [of 0])
- done
-
-lemma gcd_1_left [simp]: "gcd(1,m) = 1"
- apply (simp add: gcd_commute [of 1])
- done
-
-
-(** Multiplication laws **)
-
-(*Davenport, page 27*)
-lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)"
- apply (induct_tac m n rule: gcd_induct)
- apply (simp)
- apply (case_tac "k=0")
- apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
- done
-
-lemma gcd_self [simp]: "gcd(m,m) = m"
- apply (rule gcd_mult_distrib2 [of m 1 1, simplified, THEN sym])
- done
-
-lemma gcd_mult [simp]: "gcd(k, k*n) = k"
- apply (rule gcd_mult_distrib2 [of k 1 n, simplified, THEN sym])
- done
-
-lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
- apply (subgoal_tac "gcd(m*k, m*n) = m")
- apply (erule_tac t="m" in subst);
- apply (simp)
- apply (simp add: gcd_mult_distrib2 [THEN sym]);
- done
-
-lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> k dvd (m*n) = k dvd m";
- apply (blast intro: relprime_dvd_mult dvd_trans)
- done
-
-lemma prime_imp_relprime: "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1"
- apply (auto simp add: prime_def)
- apply (drule_tac x="gcd(p,n)" in spec)
- apply auto
- apply (insert gcd_dvd2 [of p n])
- apply (simp)
- done
-
-(*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.*)
-lemma prime_dvd_mult: "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"
- apply (blast intro: relprime_dvd_mult prime_imp_relprime)
- done
-
-
-(** Addition laws **)
-
-lemma gcd_add1 [simp]: "gcd(m+n, n) = gcd(m,n)"
- apply (case_tac "n=0")
- apply (simp_all add: gcd_non_0)
- done
-
-lemma gcd_add2 [simp]: "gcd(m, m+n) = gcd(m,n)"
- apply (rule gcd_commute [THEN trans])
- apply (subst add_commute)
- apply (simp add: gcd_add1)
- apply (rule gcd_commute)
- done
-
-lemma gcd_add2' [simp]: "gcd(m, n+m) = gcd(m,n)"
- apply (subst add_commute)
- apply (rule gcd_add2)
- done
-
-lemma gcd_add_mult: "gcd(m, k*m+n) = gcd(m,n)"
- apply (induct_tac "k")
- apply (simp_all add: gcd_add2 add_assoc)
- done
-
-
-(** More multiplication laws **)
-
-lemma gcd_mult_cancel: "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"
- apply (rule dvd_anti_sym)
- apply (rule gcd_greatest)
- apply (rule_tac n="k" in relprime_dvd_mult)
- apply (simp add: gcd_assoc)
- apply (simp add: gcd_commute)
- apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
- apply (blast intro: gcd_dvd1 dvd_trans);
- done
-
-end
--- a/src/HOL/ex/ROOT.ML Tue Sep 12 22:13:23 2000 +0200
+++ b/src/HOL/ex/ROOT.ML Wed Sep 13 18:45:10 2000 +0200
@@ -6,9 +6,6 @@
(*some examples of recursive function definitions: the TFL package*)
time_use_thy "Recdefs";
-time_use_thy "Primes";
-time_use_thy "Fib";
-with_path "../Induct" time_use_thy "Factorization";
time_use_thy "Primrec";
time_use_thy "NatSum";