(* Title: ZF/ex/Primes.thy ID: $Id: Primes.thy,v 1.10 2005/06/17 14:15:11 haftmann Exp $ Author: Christophe Tabacznyj and Lawrence C Paulson Copyright 1996 University of Cambridge *) header{*The Divides Relation and Euclid's algorithm for the GCD*} theory Primes imports Main begin constdefs divides :: "[i,i]=>o" (infixl "dvd" 50) "m dvd n == m ∈ nat & n ∈ nat & (∃k ∈ nat. n = m#*k)" is_gcd :: "[i,i,i]=>o" --{*definition of great common divisor*} "is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) & (∀d∈nat. (d dvd m) & (d dvd n) --> d dvd p)" gcd :: "[i,i]=>i" --{*Euclid's algorithm for the gcd*} "gcd(m,n) == transrec(natify(n), %n f. λm ∈ nat. if n=0 then m else f`(m mod n)`n) ` natify(m)" coprime :: "[i,i]=>o" --{*the coprime relation*} "coprime(m,n) == gcd(m,n) = 1" prime :: i --{*the set of prime numbers*} "prime == {p ∈ nat. 1<p & (∀m ∈ nat. m dvd p --> m=1 | m=p)}" subsection{*The Divides Relation*} lemma dvdD: "m dvd n ==> m ∈ nat & n ∈ nat & (∃k ∈ nat. n = m#*k)" by (unfold divides_def, assumption) lemma dvdE: "[|m dvd n; !!k. [|m ∈ nat; n ∈ nat; k ∈ nat; n = m#*k|] ==> P|] ==> P" by (blast dest!: dvdD) lemmas dvd_imp_nat1 = dvdD [THEN conjunct1, standard] lemmas dvd_imp_nat2 = dvdD [THEN conjunct2, THEN conjunct1, standard] lemma dvd_0_right [simp]: "m ∈ nat ==> m dvd 0" apply (simp add: divides_def) apply (fast intro: nat_0I mult_0_right [symmetric]) done lemma dvd_0_left: "0 dvd m ==> m = 0" by (simp add: divides_def) lemma dvd_refl [simp]: "m ∈ nat ==> m dvd m" apply (simp add: divides_def) apply (fast intro: nat_1I mult_1_right [symmetric]) done lemma dvd_trans: "[| m dvd n; n dvd p |] ==> m dvd p" by (auto simp add: divides_def intro: mult_assoc mult_type) lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m=n" apply (simp add: divides_def) apply (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff) done lemma dvd_mult_left: "[|(i#*j) dvd k; i ∈ nat|] ==> i dvd k" by (auto simp add: divides_def mult_assoc) lemma dvd_mult_right: "[|(i#*j) dvd k; j ∈ nat|] ==> j dvd k" apply (simp add: divides_def, clarify) apply (rule_tac x = "i#*k" in bexI) apply (simp add: mult_ac) apply (rule mult_type) done subsection{*Euclid's Algorithm for the GCD*} lemma gcd_0 [simp]: "gcd(m,0) = natify(m)" apply (simp add: gcd_def) apply (subst transrec, simp) done lemma gcd_natify1 [simp]: "gcd(natify(m),n) = gcd(m,n)" by (simp add: gcd_def) lemma gcd_natify2 [simp]: "gcd(m, natify(n)) = gcd(m,n)" by (simp add: gcd_def) lemma gcd_non_0_raw: "[| 0<n; n ∈ nat |] ==> gcd(m,n) = gcd(n, m mod n)" apply (simp add: gcd_def) apply (rule_tac P = "%z. ?left (z) = ?right" in transrec [THEN ssubst]) apply (simp add: ltD [THEN mem_imp_not_eq, THEN not_sym] mod_less_divisor [THEN ltD]) done lemma gcd_non_0: "0 < natify(n) ==> gcd(m,n) = gcd(n, m mod n)" apply (cut_tac m = m and n = "natify (n) " in gcd_non_0_raw) apply auto done lemma gcd_1 [simp]: "gcd(m,1) = 1" by (simp (no_asm_simp) add: gcd_non_0) lemma dvd_add: "[| k dvd a; k dvd b |] ==> k dvd (a #+ b)" apply (simp add: divides_def) apply (fast intro: add_mult_distrib_left [symmetric] add_type) done lemma dvd_mult: "k dvd n ==> k dvd (m #* n)" apply (simp add: divides_def) apply (fast intro: mult_left_commute mult_type) done lemma dvd_mult2: "k dvd m ==> k dvd (m #* n)" apply (subst mult_commute) apply (blast intro: dvd_mult) done (* k dvd (m*k) *) lemmas dvdI1 [simp] = dvd_refl [THEN dvd_mult, standard] lemmas dvdI2 [simp] = dvd_refl [THEN dvd_mult2, standard] lemma dvd_mod_imp_dvd_raw: "[| a ∈ nat; b ∈ nat; k dvd b; k dvd (a mod b) |] ==> k dvd a" apply (case_tac "b=0") apply (simp add: DIVISION_BY_ZERO_MOD) apply (blast intro: mod_div_equality [THEN subst] elim: dvdE intro!: dvd_add dvd_mult mult_type mod_type div_type) done lemma dvd_mod_imp_dvd: "[| k dvd (a mod b); k dvd b; a ∈ nat |] ==> k dvd a" apply (cut_tac b = "natify (b)" in dvd_mod_imp_dvd_raw) apply auto apply (simp add: divides_def) done (*Imitating TFL*) lemma gcd_induct_lemma [rule_format (no_asm)]: "[| n ∈ nat; ∀m ∈ nat. P(m,0); ∀m ∈ nat. ∀n ∈ nat. 0<n --> P(n, m mod n) --> P(m,n) |] ==> ∀m ∈ nat. P (m,n)" apply (erule_tac i = n in complete_induct) apply (case_tac "x=0") apply (simp (no_asm_simp)) apply clarify apply (drule_tac x1 = m and x = x in bspec [THEN bspec]) apply (simp_all add: Ord_0_lt_iff) apply (blast intro: mod_less_divisor [THEN ltD]) done lemma gcd_induct: "!!P. [| m ∈ nat; n ∈ nat; !!m. m ∈ nat ==> P(m,0); !!m n. [|m ∈ nat; n ∈ nat; 0<n; P(n, m mod n)|] ==> P(m,n) |] ==> P (m,n)" by (blast intro: gcd_induct_lemma) subsection{*Basic Properties of @{term gcd}*} text{*type of gcd*} lemma gcd_type [simp,TC]: "gcd(m, n) ∈ nat" apply (subgoal_tac "gcd (natify (m), natify (n)) ∈ nat") apply simp apply (rule_tac m = "natify (m)" and n = "natify (n)" in gcd_induct) apply auto apply (simp add: gcd_non_0) done text{* Property 1: gcd(a,b) divides a and b *} lemma gcd_dvd_both: "[| m ∈ nat; n ∈ nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n" apply (rule_tac m = m and n = n in gcd_induct) apply (simp_all add: gcd_non_0) apply (blast intro: dvd_mod_imp_dvd_raw nat_into_Ord [THEN Ord_0_lt]) done lemma gcd_dvd1 [simp]: "m ∈ nat ==> gcd(m,n) dvd m" apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both) apply auto done lemma gcd_dvd2 [simp]: "n ∈ nat ==> gcd(m,n) dvd n" apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both) apply auto done text{* if f divides a and b then f divides gcd(a,b) *} lemma dvd_mod: "[| f dvd a; f dvd b |] ==> f dvd (a mod b)" apply (simp add: divides_def) apply (case_tac "b=0") apply (simp add: DIVISION_BY_ZERO_MOD, auto) apply (blast intro: mod_mult_distrib2 [symmetric]) done text{* Property 2: for all a,b,f naturals, if f divides a and f divides b then f divides gcd(a,b)*} lemma gcd_greatest_raw [rule_format]: "[| m ∈ nat; n ∈ nat; f ∈ nat |] ==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)" apply (rule_tac m = m and n = n in gcd_induct) apply (simp_all add: gcd_non_0 dvd_mod) done lemma gcd_greatest: "[| f dvd m; f dvd n; f ∈ nat |] ==> f dvd gcd(m,n)" apply (rule gcd_greatest_raw) apply (auto simp add: divides_def) done lemma gcd_greatest_iff [simp]: "[| k ∈ nat; m ∈ nat; n ∈ nat |] ==> (k dvd gcd (m, n)) <-> (k dvd m & k dvd n)" by (blast intro!: gcd_greatest gcd_dvd1 gcd_dvd2 intro: dvd_trans) subsection{*The Greatest Common Divisor*} text{*The GCD exists and function gcd computes it.*} lemma is_gcd: "[| m ∈ nat; n ∈ nat |] ==> is_gcd(gcd(m,n), m, n)" by (simp add: is_gcd_def) text{*The GCD is unique*} lemma is_gcd_unique: "[|is_gcd(m,a,b); is_gcd(n,a,b); m∈nat; n∈nat|] ==> m=n" apply (simp add: is_gcd_def) apply (blast intro: dvd_anti_sym) done lemma is_gcd_commute: "is_gcd(k,m,n) <-> is_gcd(k,n,m)" by (simp add: is_gcd_def, blast) lemma gcd_commute_raw: "[| m ∈ nat; n ∈ nat |] ==> gcd(m,n) = gcd(n,m)" apply (rule is_gcd_unique) apply (rule is_gcd) apply (rule_tac [3] is_gcd_commute [THEN iffD1]) apply (rule_tac [3] is_gcd, auto) done lemma gcd_commute: "gcd(m,n) = gcd(n,m)" apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_commute_raw) apply auto done lemma gcd_assoc_raw: "[| k ∈ nat; m ∈ nat; n ∈ nat |] ==> gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" apply (rule is_gcd_unique) apply (rule is_gcd) apply (simp_all add: is_gcd_def) apply (blast intro: gcd_dvd1 gcd_dvd2 gcd_type intro: dvd_trans) done lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) " in gcd_assoc_raw) apply auto done lemma gcd_0_left [simp]: "gcd (0, m) = natify(m)" by (simp add: gcd_commute [of 0]) lemma gcd_1_left [simp]: "gcd (1, m) = 1" by (simp add: gcd_commute [of 1]) subsection{*Addition laws*} lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)" apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))") apply simp apply (case_tac "natify (n) = 0") apply (auto simp add: Ord_0_lt_iff 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, simp) apply (rule gcd_commute) done lemma gcd_add2' [simp]: "gcd (m, n #+ m) = gcd (m, n)" by (subst add_commute, rule gcd_add2) lemma gcd_add_mult_raw: "k ∈ nat ==> gcd (m, k #* m #+ n) = gcd (m, n)" apply (erule nat_induct) apply (auto simp add: gcd_add2 add_assoc) done lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)" apply (cut_tac k = "natify (k)" in gcd_add_mult_raw) apply auto done subsection{* Multiplication Laws*} lemma gcd_mult_distrib2_raw: "[| k ∈ nat; m ∈ nat; n ∈ nat |] ==> k #* gcd (m, n) = gcd (k #* m, k #* n)" apply (erule_tac m = m and n = n in gcd_induct, assumption) apply simp apply (case_tac "k = 0", simp) apply (simp add: mod_geq gcd_non_0 mod_mult_distrib2 Ord_0_lt_iff) done lemma gcd_mult_distrib2: "k #* gcd (m, n) = gcd (k #* m, k #* n)" apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) " in gcd_mult_distrib2_raw) apply auto done lemma gcd_mult [simp]: "gcd (k, k #* n) = natify(k)" by (cut_tac k = k and m = 1 and n = n in gcd_mult_distrib2, auto) lemma gcd_self [simp]: "gcd (k, k) = natify(k)" by (cut_tac k = k and n = 1 in gcd_mult, auto) lemma relprime_dvd_mult: "[| gcd (k,n) = 1; k dvd (m #* n); m ∈ nat |] ==> k dvd m" apply (cut_tac k = m and m = k and n = n in gcd_mult_distrib2, auto) apply (erule_tac b = m in ssubst) apply (simp add: dvd_imp_nat1) done lemma relprime_dvd_mult_iff: "[| gcd (k,n) = 1; m ∈ nat |] ==> k dvd (m #* n) <-> k dvd m" by (blast intro: dvdI2 relprime_dvd_mult dvd_trans) lemma prime_imp_relprime: "[| p ∈ prime; ~ (p dvd n); n ∈ nat |] ==> gcd (p, n) = 1" apply (simp add: prime_def, clarify) apply (drule_tac x = "gcd (p,n)" in bspec) apply auto apply (cut_tac m = p and n = n in gcd_dvd2, auto) done lemma prime_into_nat: "p ∈ prime ==> p ∈ nat" by (simp add: prime_def) lemma prime_nonzero: "p ∈ prime ==> p≠0" by (auto simp add: prime_def) text{*This theorem leads immediately to a proof of the uniqueness of factorization. If @{term p} divides a product of primes then it is one of those primes.*} lemma prime_dvd_mult: "[|p dvd m #* n; p ∈ prime; m ∈ nat; n ∈ nat |] ==> p dvd m ∨ p dvd n" by (blast intro: relprime_dvd_mult prime_imp_relprime prime_into_nat) lemma gcd_mult_cancel_raw: "[|gcd (k,n) = 1; m ∈ nat; n ∈ nat|] ==> gcd (k #* m, n) = gcd (m, n)" apply (rule dvd_anti_sym) apply (rule gcd_greatest) apply (rule relprime_dvd_mult [of _ k]) apply (simp add: gcd_assoc) apply (simp add: gcd_commute) apply (simp_all add: mult_commute) apply (blast intro: dvdI1 gcd_dvd1 dvd_trans) done lemma gcd_mult_cancel: "gcd (k,n) = 1 ==> gcd (k #* m, n) = gcd (m, n)" apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_mult_cancel_raw) apply auto done subsection{*The Square Root of a Prime is Irrational: Key Lemma*} lemma prime_dvd_other_side: "[|n#*n = p#*(k#*k); p ∈ prime; n ∈ nat|] ==> p dvd n" apply (subgoal_tac "p dvd n#*n") apply (blast dest: prime_dvd_mult) apply (rule_tac j = "k#*k" in dvd_mult_left) apply (auto simp add: prime_def) done lemma reduction: "[|k#*k = p#*(j#*j); p ∈ prime; 0 < k; j ∈ nat; k ∈ nat|] ==> k < p#*j & 0 < j" apply (rule ccontr) apply (simp add: not_lt_iff_le prime_into_nat) apply (erule disjE) apply (frule mult_le_mono, assumption+) apply (simp add: mult_ac) apply (auto dest!: natify_eqE simp add: not_lt_iff_le prime_into_nat mult_le_cancel_le1) apply (simp add: prime_def) apply (blast dest: lt_trans1) done lemma rearrange: "j #* (p#*j) = k#*k ==> k#*k = p#*(j#*j)" by (simp add: mult_ac) lemma prime_not_square: "[|m ∈ nat; p ∈ prime|] ==> ∀k ∈ nat. 0<k --> m#*m ≠ p#*(k#*k)" apply (erule complete_induct, clarify) apply (frule prime_dvd_other_side, assumption) apply assumption apply (erule dvdE) apply (simp add: mult_assoc mult_cancel1 prime_nonzero prime_into_nat) apply (blast dest: rearrange reduction ltD) done end
lemma dvdD:
m dvd n ==> m ∈ nat ∧ n ∈ nat ∧ (∃k∈nat. n = m #× k)
lemma dvdE:
[| m dvd n; !!k. [| m ∈ nat; n ∈ nat; k ∈ nat; n = m #× k |] ==> P |] ==> P
lemmas dvd_imp_nat1:
m dvd n ==> m ∈ nat
lemmas dvd_imp_nat1:
m dvd n ==> m ∈ nat
lemmas dvd_imp_nat2:
m dvd n ==> n ∈ nat
lemmas dvd_imp_nat2:
m dvd n ==> n ∈ nat
lemma dvd_0_right:
m ∈ nat ==> m dvd 0
lemma dvd_0_left:
0 dvd m ==> m = 0
lemma dvd_refl:
m ∈ nat ==> m dvd m
lemma dvd_trans:
[| m dvd n; n dvd p |] ==> m dvd p
lemma dvd_anti_sym:
[| m dvd n; n dvd m |] ==> m = n
lemma dvd_mult_left:
[| i #× j dvd k; i ∈ nat |] ==> i dvd k
lemma dvd_mult_right:
[| i #× j dvd k; j ∈ nat |] ==> j dvd k
lemma gcd_0:
gcd(m, 0) = natify(m)
lemma gcd_natify1:
gcd(natify(m), n) = gcd(m, n)
lemma gcd_natify2:
gcd(m, natify(n)) = gcd(m, n)
lemma gcd_non_0_raw:
[| 0 < n; n ∈ nat |] ==> gcd(m, n) = gcd(n, m mod n)
lemma gcd_non_0:
0 < natify(n) ==> gcd(m, n) = gcd(n, m mod n)
lemma gcd_1:
gcd(m, 1) = 1
lemma dvd_add:
[| k dvd a; k dvd b |] ==> k dvd a #+ b
lemma dvd_mult:
k dvd n ==> k dvd m #× n
lemma dvd_mult2:
k dvd m ==> k dvd m #× n
lemmas dvdI1:
k ∈ nat ==> k dvd m #× k
lemmas dvdI1:
k ∈ nat ==> k dvd m #× k
lemmas dvdI2:
k ∈ nat ==> k dvd k #× n
lemmas dvdI2:
k ∈ nat ==> k dvd k #× n
lemma dvd_mod_imp_dvd_raw:
[| a ∈ nat; b ∈ nat; k dvd b; k dvd a mod b |] ==> k dvd a
lemma dvd_mod_imp_dvd:
[| k dvd a mod b; k dvd b; a ∈ nat |] ==> k dvd a
lemma gcd_induct_lemma:
[| n ∈ nat; ∀m∈nat. P(m, 0); ∀m∈nat. ∀n∈nat. 0 < n --> P(n, m mod n) --> P(m, n); m ∈ nat |] ==> P(m, n)
lemma gcd_induct:
[| m ∈ nat; n ∈ nat; !!m. m ∈ nat ==> P(m, 0); !!m n. [| m ∈ nat; n ∈ nat; 0 < n; P(n, m mod n) |] ==> P(m, n) |] ==> P(m, n)
lemma gcd_type:
gcd(m, n) ∈ nat
lemma gcd_dvd_both:
[| m ∈ nat; n ∈ nat |] ==> gcd(m, n) dvd m ∧ gcd(m, n) dvd n
lemma gcd_dvd1:
m ∈ nat ==> gcd(m, n) dvd m
lemma gcd_dvd2:
n ∈ nat ==> gcd(m, n) dvd n
lemma dvd_mod:
[| f dvd a; f dvd b |] ==> f dvd a mod b
lemma gcd_greatest_raw:
[| m ∈ nat; n ∈ nat; f ∈ nat; f dvd m; f dvd n |] ==> f dvd gcd(m, n)
lemma gcd_greatest:
[| f dvd m; f dvd n; f ∈ nat |] ==> f dvd gcd(m, n)
lemma gcd_greatest_iff:
[| k ∈ nat; m ∈ nat; n ∈ nat |] ==> k dvd gcd(m, n) <-> k dvd m ∧ k dvd n
lemma is_gcd:
[| m ∈ nat; n ∈ nat |] ==> is_gcd(gcd(m, n), m, n)
lemma is_gcd_unique:
[| is_gcd(m, a, b); is_gcd(n, a, b); m ∈ nat; n ∈ nat |] ==> m = n
lemma is_gcd_commute:
is_gcd(k, m, n) <-> is_gcd(k, n, m)
lemma gcd_commute_raw:
[| m ∈ nat; n ∈ nat |] ==> gcd(m, n) = gcd(n, m)
lemma gcd_commute:
gcd(m, n) = gcd(n, m)
lemma gcd_assoc_raw:
[| k ∈ nat; m ∈ nat; n ∈ nat |] ==> gcd(gcd(k, m), n) = gcd(k, gcd(m, n))
lemma gcd_assoc:
gcd(gcd(k, m), n) = gcd(k, gcd(m, n))
lemma gcd_0_left:
gcd(0, m) = natify(m)
lemma gcd_1_left:
gcd(1, m) = 1
lemma gcd_add1:
gcd(m #+ n, n) = gcd(m, n)
lemma gcd_add2:
gcd(m, m #+ n) = gcd(m, n)
lemma gcd_add2':
gcd(m, n #+ m) = gcd(m, n)
lemma gcd_add_mult_raw:
k ∈ nat ==> gcd(m, k #× m #+ n) = gcd(m, n)
lemma gcd_add_mult:
gcd(m, k #× m #+ n) = gcd(m, n)
lemma gcd_mult_distrib2_raw:
[| k ∈ nat; m ∈ nat; n ∈ nat |] ==> k #× gcd(m, n) = gcd(k #× m, k #× n)
lemma gcd_mult_distrib2:
k #× gcd(m, n) = gcd(k #× m, k #× n)
lemma gcd_mult:
gcd(k, k #× n) = natify(k)
lemma gcd_self:
gcd(k, k) = natify(k)
lemma relprime_dvd_mult:
[| gcd(k, n) = 1; k dvd m #× n; m ∈ nat |] ==> k dvd m
lemma relprime_dvd_mult_iff:
[| gcd(k, n) = 1; m ∈ nat |] ==> k dvd m #× n <-> k dvd m
lemma prime_imp_relprime:
[| p ∈ prime; ¬ p dvd n; n ∈ nat |] ==> gcd(p, n) = 1
lemma prime_into_nat:
p ∈ prime ==> p ∈ nat
lemma prime_nonzero:
p ∈ prime ==> p ≠ 0
lemma prime_dvd_mult:
[| p dvd m #× n; p ∈ prime; m ∈ nat; n ∈ nat |] ==> p dvd m ∨ p dvd n
lemma gcd_mult_cancel_raw:
[| gcd(k, n) = 1; m ∈ nat; n ∈ nat |] ==> gcd(k #× m, n) = gcd(m, n)
lemma gcd_mult_cancel:
gcd(k, n) = 1 ==> gcd(k #× m, n) = gcd(m, n)
lemma prime_dvd_other_side:
[| n #× n = p #× k #× k; p ∈ prime; n ∈ nat |] ==> p dvd n
lemma reduction:
[| k #× k = p #× j #× j; p ∈ prime; 0 < k; j ∈ nat; k ∈ nat |] ==> k < p #× j ∧ 0 < j
lemma rearrange:
j #× p #× j = k #× k ==> k #× k = p #× j #× j
lemma prime_not_square:
[| m ∈ nat; p ∈ prime |] ==> ∀k∈nat. 0 < k --> m #× m ≠ p #× k #× k