(* 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 [dvd_def] "m dvd n ==> m:nat & n:nat & (EX k:nat. n = m#*k)";
by (assume_tac 1);
qed "dvdD";
bind_thm ("dvd_imp_nat1", dvdD RS conjunct1);
bind_thm ("dvd_imp_nat2", dvdD RS conjunct2 RS conjunct1);
Goalw [dvd_def] "m:nat ==> m dvd 0";
by (fast_tac (claset() addIs [nat_0I, mult_0_right RS sym]) 1);
qed "dvd_0_right";
Goalw [dvd_def] "0 dvd m ==> m = 0";
by (fast_tac (claset() addss (simpset())) 1);
qed "dvd_0_left";
Goalw [dvd_def] "m:nat ==> m dvd m";
by (fast_tac (claset() addIs [nat_1I, mult_1_right RS sym]) 1);
qed "dvd_refl";
Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
by (fast_tac (claset() addIs [mult_assoc, mult_type] ) 1);
qed "dvd_trans";
Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m=n";
by (fast_tac (claset() addDs [mult_eq_self_implies_10]
addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
qed "dvd_anti_sym";
(************************************************)
(** Greatest Common Divisor **)
(************************************************)
(* GCD by Euclid's Algorithm *)
Goalw [egcd_def] "m:nat ==> egcd(m,0) = m";
by (stac transrec 1);
by (Asm_simp_tac 1);
qed "egcd_0";
Goalw [egcd_def]
"[| 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 (simpset() addsimps [ltD RS mem_imp_not_eq RS not_sym,
mod_less_divisor RS ltD]) 1);
qed "egcd_lt_0";
Goal "m:nat ==> egcd(m,0) dvd m";
by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_refl]) 1);
qed "egcd_0_dvd_m";
Goal "m:nat ==> egcd(m,0) dvd 0";
by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_0_right]) 1);
qed "egcd_0_dvd_0";
Goalw [dvd_def] "[| k dvd a; k dvd b |] ==> k dvd (a #+ b)";
by (fast_tac (claset() addIs [add_mult_distrib_left RS sym, add_type]) 1);
qed "dvd_add";
Goalw [dvd_def] "[| k dvd a; q:nat |] ==> k dvd (q #* a)";
by (fast_tac (claset() addIs [mult_left_commute, mult_type]) 1);
qed "dvd_mult";
Goal "[| k dvd b; k dvd (a mod b); 0 < b; a:nat |] ==> k dvd a";
by (deepen_tac
(claset() 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 "b:nat ==> ALL a:nat. egcd(a,b):nat";
by (etac complete_induct 1);
by (rtac ballI 1);
by (excluded_middle_tac "x=0" 1);
(* case x = 0 *)
by (asm_simp_tac (simpset() addsimps [egcd_0]) 2);
(* case x > 0 *)
by (asm_simp_tac (simpset() 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 1);
by (asm_full_simp_tac (simpset() 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 "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 (rtac ballI 1);
by (excluded_middle_tac "x=0" 1);
(* case x = 0 *)
by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_refl,dvd_0_right]) 2);
(* case x > 0 *)
by (asm_simp_tac (simpset() 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 1);
by (asm_full_simp_tac (simpset() addsimps [mod_less_divisor RS ltD,
nat_into_Ord RS Ord_0_lt]) 2);
by (best_tac (claset() 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 [dvd_def] "[| f dvd a; f dvd b; 0<b |] ==> f dvd (a mod b)";
by (safe_tac (claset() 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 (simpset() addsimps [diff_mult_distrib2, div_cancel,
mult_mod_distrib, add_mult_distrib_left,
diff_add_inverse]) 1);
by (Asm_simp_tac 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 "[| b:nat; f:nat |] ==> \
\ ALL a. (f dvd a) & (f dvd b) --> f dvd egcd(a,b)";
by (etac complete_induct 1);
by (rtac allI 1);
by (excluded_middle_tac "x=0" 1);
(* case x = 0 *)
by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_refl,dvd_0_right,
dvd_imp_nat2]) 2);
(* case x > 0 *)
by Safe_tac;
by (asm_simp_tac (simpset() 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
(simpset() addsimps [mod_less_divisor RS ltD, dvd_imp_nat2,
nat_into_Ord RS Ord_0_lt, egcd_lt_0]) 2);
by (fast_tac (claset() addSIs [dvd_mod, nat_into_Ord RS Ord_0_lt]) 1);
qed "egcd_prop2";
(* GCD PROOF : GCD exists and egcd fits the definition *)
Goalw [gcd_def] "[| a: nat; b:nat |] ==> gcd(egcd(a,b), a, b)";
by (asm_simp_tac (simpset() addsimps [egcd_prop1]) 1);
by (fast_tac (claset() addIs [egcd_prop2 RS spec RS mp, dvd_imp_nat1]) 1);
qed "gcd";
(* GCD is unique *)
Goalw [gcd_def] "gcd(m,a,b) & gcd(n,a,b) --> m=n";
by (fast_tac (claset() addIs [dvd_anti_sym]) 1);
qed "gcd_unique";