--- 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<j; 0<k; j:nat; k:nat |] ==> 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 & 0<n";
-by (etac nat_induct 1);
-by (etac nat_induct 2);
-by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mult_0_right])));
+by (best_tac (ZF_cs addEs [natE] addss (arith_ss addsimps [mult_0_right])) 1);
qed "zero_lt_mult_iff";
+goal Arith.thy "!!k. [| m: nat; n: nat |] ==> 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<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n";
by (eres_inst_tac [("i","m")] complete_induct 1);
by (excluded_middle_tac "x<n" 1);
by (asm_simp_tac (arith_ss addsimps [div_less, zero_lt_mult_iff,
- mult_lt_mono2]) 2);
+ mult_lt_mono2]) 2);
by (asm_full_simp_tac
(arith_ss addsimps [not_lt_iff_le, nat_into_Ord,
zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq,
diff_mult_distrib2 RS sym,
- div_termination RS ltD]) 1);
+ div_termination RS ltD]) 1);
qed "div_cancel";
goal Arith.thy
@@ -548,18 +559,29 @@
by (eres_inst_tac [("i","m")] complete_induct 1);
by (excluded_middle_tac "x<n" 1);
by (asm_simp_tac (arith_ss addsimps [mod_less, zero_lt_mult_iff,
- mult_lt_mono2]) 2);
+ mult_lt_mono2]) 2);
by (asm_full_simp_tac
(arith_ss addsimps [not_lt_iff_le, nat_into_Ord,
zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq,
diff_mult_distrib2 RS sym,
- div_termination RS ltD]) 1);
+ div_termination RS ltD]) 1);
qed "mult_mod_distrib";
+(** Lemma for gcd **)
+val mono_lemma = (nat_into_Ord RS Ord_0_lt) RSN (2,mult_lt_mono2);
+
+goal Arith.thy "!!m n. [| m = m#*n; m: nat; n: nat |] ==> 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];
--- 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";
--- 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"
--- 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";