--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Primes.ML Thu Jun 13 14:25:45 1996 +0200
@@ -0,0 +1,175 @@
+(* Title: ZF/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
+*)
+
+eta_contract:=false;
+
+open Primes;
+
+(************************************************)
+(** Divides Relation **)
+(************************************************)
+
+goalw thy [dvd_def] "!!m. m dvd n ==> m:nat & n:nat & (EX k:nat. n = m#*k)";
+ba 1;
+qed "dvdD";
+
+bind_thm ("dvd_imp_nat1", dvdD RS conjunct1);
+bind_thm ("dvd_imp_nat2", dvdD RS conjunct2 RS conjunct1);
+
+
+goalw thy [dvd_def] "!!m. m:nat ==> m dvd 0";
+by (fast_tac (ZF_cs addIs [nat_0I, mult_0_right RS sym]) 1);
+qed "dvd_0_right";
+
+goalw thy [dvd_def] "!!m. 0 dvd m ==> m = 0";
+by (fast_tac (ZF_cs addss arith_ss) 1);
+qed "dvd_0_left";
+
+goalw thy [dvd_def] "!!m. m:nat ==> m dvd m";
+by (fast_tac (ZF_cs addIs [nat_1I, mult_1_right RS sym]) 1);
+qed "dvd_refl";
+
+goalw thy [dvd_def] "!!m n p. [| m dvd n; n dvd p |] ==> m dvd p";
+by (fast_tac (ZF_cs addIs [mult_assoc, mult_type] ) 1);
+qed "dvd_trans";
+
+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);
+qed "dvd_anti_sym";
+
+
+(************************************************)
+(** Greatest Common Divisor **)
+(************************************************)
+
+(* GCD by Euclid's Algorithm *)
+
+goalw thy [egcd_def] "!!m. m:nat ==> egcd(m,0) = m";
+by (rtac (transrec RS ssubst) 1);
+by (asm_simp_tac ZF_ss 1);
+qed "egcd_0";
+
+goalw thy [egcd_def]
+ "!!m. [| 0<n; m:nat; n:nat |] ==> egcd(m,n) = egcd(n, m mod n)";
+by (res_inst_tac [("P", "%z. ?left(z) = ?right")] (transrec RS ssubst) 1);
+by (asm_simp_tac (arith_ss addsimps [ltD RS mem_imp_not_eq RS not_sym,
+ mod_less_divisor RS ltD]) 1);
+qed "egcd_lt_0";
+
+goal thy "!!m. m:nat ==> egcd(m,0) dvd m";
+by (asm_simp_tac (arith_ss addsimps [egcd_0,dvd_refl]) 1);
+qed "egcd_0_dvd_m";
+
+goal thy "!!m. m:nat ==> egcd(m,0) dvd 0";
+by (asm_simp_tac (arith_ss addsimps [egcd_0,dvd_0_right]) 1);
+qed "egcd_0_dvd_0";
+
+goalw thy [dvd_def] "!!k. [| k dvd a; k dvd b |] ==> k dvd (a #+ b)";
+by (fast_tac (ZF_cs addIs [add_mult_distrib_left RS sym, add_type]) 1);
+qed "dvd_add";
+
+goalw thy [dvd_def] "!!k. [| k dvd a; q:nat |] ==> k dvd (q #* a)";
+by (fast_tac (ZF_cs addIs [mult_left_commute, mult_type]) 1);
+qed "dvd_mult";
+
+goal thy "!!k. [| k dvd b; k dvd (a mod b); 0 < b; a:nat |] ==> k dvd a";
+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);
+qed "gcd_ind";
+
+
+(* egcd type *)
+
+goal thy "!!b. b:nat ==> ALL a:nat. egcd(a,b):nat";
+by (etac complete_induct 1);
+by (resolve_tac [ballI] 1);
+by (excluded_middle_tac "x=0" 1);
+(* case x = 0 *)
+by (asm_simp_tac (arith_ss addsimps [egcd_0]) 2);
+(* case x > 0 *)
+by (asm_simp_tac (arith_ss addsimps [egcd_lt_0, nat_into_Ord RS Ord_0_lt]) 1);
+by (eres_inst_tac [("x","a mod x")] ballE 1);
+by (asm_simp_tac ZF_ss 1);
+by (asm_full_simp_tac (arith_ss addsimps [mod_less_divisor RS ltD,
+ nat_into_Ord RS Ord_0_lt]) 1);
+qed "egcd_type";
+
+
+(* Property 1: egcd(a,b) divides a and b *)
+
+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 (excluded_middle_tac "x=0" 1);
+(* case x = 0 *)
+by (asm_simp_tac (arith_ss addsimps [egcd_0,dvd_refl,dvd_0_right]) 2);
+(* case x > 0 *)
+by (asm_simp_tac (arith_ss addsimps [egcd_lt_0, nat_into_Ord RS Ord_0_lt]) 1);
+by (eres_inst_tac [("x","a mod x")] ballE 1);
+by (asm_simp_tac ZF_ss 1);
+by (asm_full_simp_tac (arith_ss addsimps [mod_less_divisor RS ltD,
+ nat_into_Ord RS Ord_0_lt]) 2);
+by (best_tac (ZF_cs addIs [gcd_ind, nat_into_Ord RS Ord_0_lt]) 1);
+qed "egcd_prop1";
+
+
+(* if f divides a and b then f divides egcd(a,b) *)
+
+goalw thy [dvd_def] "!!a. [| f dvd a; f dvd b; 0<b |] ==> f dvd (a mod b)";
+by (safe_tac (ZF_cs addSIs [mult_type, mod_type]));
+ren "m n" 1;
+by (rtac (zero_lt_mult_iff RS iffD1 RS conjE) 1);
+by (REPEAT_SOME assume_tac);
+by (res_inst_tac
+ [("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);
+by (asm_simp_tac arith_ss 1);
+qed "dvd_mod";
+
+
+(* Property 2: for all a,b,f naturals,
+ if f divides a and f divides b then f divides egcd(a,b)*)
+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 (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);
+(* 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);
+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);
+by (fast_tac (ZF_cs addSIs [dvd_mod, nat_into_Ord RS Ord_0_lt]) 1);
+qed "egcd_prop2";
+
+(* GCD PROOF : GCD exists and egcd fits the definition *)
+
+goalw thy [gcd_def] "!!b. [| a: nat; b:nat |] ==> gcd(egcd(a,b), a, b)";
+by (asm_simp_tac (arith_ss addsimps [egcd_prop1]) 1);
+by (fast_tac (ZF_cs addIs [egcd_prop2 RS spec RS mp, dvd_imp_nat1]) 1);
+qed "gcd";
+
+(* GCD is unique *)
+
+goalw thy [gcd_def] "!!a. gcd(m,a,b) & gcd(n,a,b) --> m=n";
+by (fast_tac (ZF_cs addIs [dvd_anti_sym]) 1);
+qed "gcd_unique";
+