# HG changeset patch # User paulson # Date 834675757 -7200 # Node ID 09fff2f0d727de96715d1b411ba1aa75879eaf6a # Parent 75c54074cd8c5096ea23de6dc94d29317eea138d New example of GCDs and divides relation diff -r 75c54074cd8c -r 09fff2f0d727 src/ZF/Arith.ML --- a/src/ZF/Arith.ML Thu Jun 13 14:25:45 1996 +0200 +++ b/src/ZF/Arith.ML Thu Jun 13 16:22:37 1996 +0200 @@ -1,4 +1,4 @@ -(* Title: ZF/arith.ML +(* Title: ZF/Arith.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge @@ -197,6 +197,15 @@ [ (nat_ind_tac "m" [] 1), (ALLGOALS (asm_simp_tac (arith_ss addsimps add_ac))) ]); +goal Arith.thy "!!n. n:nat ==> 1 #* n = n"; +by (asm_simp_tac (arith_ss addsimps [add_0_right]) 1); +qed "mult_1"; + +goal Arith.thy "!!n. n:nat ==> n #* 1 = n"; +by (asm_simp_tac (arith_ss addsimps [mult_0_right, add_0_right, + mult_succ_right]) 1); +qed "mult_1_right"; + (*Commutative law for multiplication*) qed_goal "mult_commute" Arith.thy "[| m:nat; n:nat |] ==> m #* n = n #* m" @@ -308,7 +317,7 @@ "!!m. [| m:nat; n: nat; k:nat |] ==> k #* (m #- n) = (k #* m) #- (k #* n)"; val mult_commute_k = read_instantiate [("m","k")] mult_commute; by (asm_simp_tac (arith_ss addsimps - [mult_commute_k, diff_mult_distrib]) 1); + [mult_commute_k, diff_mult_distrib]) 1); qed "diff_mult_distrib2" ; (*** Remainder ***) @@ -499,7 +508,7 @@ by (forward_tac [lt_nat_in_nat] 1); by (nat_ind_tac "k" [] 2); by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mult_0_right, mult_succ_right, - add_le_mono]))); + add_le_mono]))); qed "mult_le_mono1"; (* le monotonicity, BOTH arguments*) @@ -515,7 +524,7 @@ (*strict, in 1st argument; proof is by induction on k>0*) goal Arith.thy "!!i j k. [| i k#*i < k#*j"; -be zero_lt_natE 1; +by (etac zero_lt_natE 1); by (forward_tac [lt_nat_in_nat] 2); by (ALLGOALS (asm_simp_tac arith_ss)); by (nat_ind_tac "x" [] 1); @@ -523,23 +532,25 @@ qed "mult_lt_mono2"; goal Arith.thy "!!k. [| m: nat; n: nat |] ==> 0 < m#*n <-> 0 m#*n = 1 <-> m=1 & n=1"; +by (best_tac (ZF_cs addEs [natE] addss (arith_ss addsimps [mult_0_right])) 1); +qed "mult_eq_1_iff"; + (*Cancellation law for division*) goal Arith.thy "!!k. [| 0 (k#*m) div (k#*n) = m div n"; by (eres_inst_tac [("i","m")] complete_induct 1); by (excluded_middle_tac "x n=1 | m=0"; +by (rtac disjCI 1); +by (dtac sym 1); +by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I])); +by (fast_tac (lt_cs addss (arith_ss addsimps [mult_0_right])) 1); +by (fast_tac (lt_cs addDs [mono_lemma] + addss (arith_ss addsimps [mult_1_right])) 1); +qed "mult_eq_self_implies_10"; val arith_ss0 = arith_ss and arith_ss = arith_ss addsimps [add_0_right, add_succ_right, mult_0_right, mult_succ_right, - mod_type, div_type, + mod_type, div_type, mod_less, mod_geq, div_less, div_geq]; diff -r 75c54074cd8c -r 09fff2f0d727 src/ZF/ex/Primes.ML --- a/src/ZF/ex/Primes.ML Thu Jun 13 14:25:45 1996 +0200 +++ b/src/ZF/ex/Primes.ML Thu Jun 13 16:22:37 1996 +0200 @@ -11,11 +11,11 @@ open Primes; (************************************************) -(** Divides Relation **) +(** Divides Relation **) (************************************************) goalw thy [dvd_def] "!!m. m dvd n ==> m:nat & n:nat & (EX k:nat. n = m#*k)"; -ba 1; +by (assume_tac 1); qed "dvdD"; bind_thm ("dvd_imp_nat1", dvdD RS conjunct1); @@ -40,7 +40,7 @@ goalw thy [dvd_def] "!!m n. [| m dvd n; n dvd m |] ==> m=n"; by (fast_tac (ZF_cs addDs [mult_eq_self_implies_10] - addss (arith_ss addsimps [mult_assoc, mult_eq_1_iff])) 1); + addss (arith_ss addsimps [mult_assoc, mult_eq_1_iff])) 1); qed "dvd_anti_sym"; @@ -82,7 +82,7 @@ by (deepen_tac (ZF_cs addIs [mod_div_equality RS subst] addDs [dvdD] - addSIs [dvd_add, dvd_mult, mult_type,mod_type,div_type]) 0 1); + addSIs [dvd_add, dvd_mult, mult_type,mod_type,div_type]) 0 1); qed "gcd_ind"; @@ -90,7 +90,7 @@ goal thy "!!b. b:nat ==> ALL a:nat. egcd(a,b):nat"; by (etac complete_induct 1); -by (resolve_tac [ballI] 1); +by (rtac ballI 1); by (excluded_middle_tac "x=0" 1); (* case x = 0 *) by (asm_simp_tac (arith_ss addsimps [egcd_0]) 2); @@ -108,7 +108,7 @@ goal thy "!!b. b:nat ==> ALL a: nat. (egcd(a,b) dvd a) & (egcd(a,b) dvd b)"; by (res_inst_tac [("i","b")] complete_induct 1); by (assume_tac 1); -by (resolve_tac [ballI] 1); +by (rtac ballI 1); by (excluded_middle_tac "x=0" 1); (* case x = 0 *) by (asm_simp_tac (arith_ss addsimps [egcd_0,dvd_refl,dvd_0_right]) 2); @@ -133,8 +133,8 @@ [("x", "(((m div n)#*n #+ m mod n) #- ((f#*m) div (f#*n)) #* n)")] bexI 1); by (asm_simp_tac (arith_ss addsimps [diff_mult_distrib2, div_cancel, - mult_mod_distrib, add_mult_distrib_left, - diff_add_inverse]) 1); + mult_mod_distrib, add_mult_distrib_left, + diff_add_inverse]) 1); by (asm_simp_tac arith_ss 1); qed "dvd_mod"; @@ -144,19 +144,19 @@ goal thy "!!b. [| b:nat; f:nat |] ==> \ \ ALL a. (f dvd a) & (f dvd b) --> f dvd egcd(a,b)"; by (etac complete_induct 1); -by (resolve_tac [allI] 1); +by (rtac allI 1); by (excluded_middle_tac "x=0" 1); (* case x = 0 *) by (asm_simp_tac (arith_ss addsimps [egcd_0,dvd_refl,dvd_0_right, - dvd_imp_nat2]) 2); + dvd_imp_nat2]) 2); (* case x > 0 *) by (safe_tac ZF_cs); by (asm_simp_tac (arith_ss addsimps [egcd_lt_0, nat_into_Ord RS Ord_0_lt, - dvd_imp_nat2]) 1); + dvd_imp_nat2]) 1); by (eres_inst_tac [("x","a mod x")] ballE 1); by (asm_full_simp_tac (arith_ss addsimps [mod_less_divisor RS ltD, dvd_imp_nat2, - nat_into_Ord RS Ord_0_lt, egcd_lt_0]) 2); + nat_into_Ord RS Ord_0_lt, egcd_lt_0]) 2); by (fast_tac (ZF_cs addSIs [dvd_mod, nat_into_Ord RS Ord_0_lt]) 1); qed "egcd_prop2"; diff -r 75c54074cd8c -r 09fff2f0d727 src/ZF/ex/Primes.thy --- a/src/ZF/ex/Primes.thy Thu Jun 13 14:25:45 1996 +0200 +++ b/src/ZF/ex/Primes.thy Thu Jun 13 16:22:37 1996 +0200 @@ -8,20 +8,20 @@ Primes = Arith + consts - dvd :: [i,i]=>o (infixl 70) - gcd :: [i,i,i]=>o (* great common divisor *) - egcd :: [i,i]=>i (* gcd by Euclid's algorithm *) - coprime :: [i,i]=>o (* coprime definition *) - prime :: [i]=>o (* prime definition *) + dvd :: [i,i]=>o (infixl 70) + gcd :: [i,i,i]=>o (* great common divisor *) + egcd :: [i,i]=>i (* gcd by Euclid's algorithm *) + coprime :: [i,i]=>o (* coprime definition *) + prime :: i=>o (* prime definition *) defs dvd_def "m dvd n == m:nat & n:nat & (EX k:nat. n = m#*k)" - gcd_def "gcd(p,m,n) == ((p dvd m) & (p dvd n)) \ -\ & (ALL d. (d dvd m) & (d dvd n) --> d dvd p)" + gcd_def "gcd(p,m,n) == ((p dvd m) & (p dvd n)) & + (ALL d. (d dvd m) & (d dvd n) --> d dvd p)" - egcd_def "egcd(m,n) == \ -\ transrec(n, %n f. lam m:nat. if(n=0, m, f`(m mod n)`n)) ` m" + egcd_def "egcd(m,n) == + transrec(n, %n f. lam m:nat. if(n=0, m, f`(m mod n)`n)) ` m" coprime_def "coprime(m,n) == egcd(m,n) = 1" diff -r 75c54074cd8c -r 09fff2f0d727 src/ZF/ex/ROOT.ML --- a/src/ZF/ex/ROOT.ML Thu Jun 13 14:25:45 1996 +0200 +++ b/src/ZF/ex/ROOT.ML Thu Jun 13 16:22:37 1996 +0200 @@ -12,8 +12,9 @@ proof_timing := true; time_use "misc.ML"; -time_use_thy "Ramsey"; -time_use_thy "Limit"; +time_use_thy "Primes"; (*GCD theory*) +time_use_thy "Ramsey"; (*Simple form of Ramsey's theorem*) +time_use_thy "Limit"; (*Inverse limit construction of domains*) (*Integers & Binary integer arithmetic*) time_use_thy "Bin";