src/HOL/Library/Primes.thy

 imports Plain "~~/src/HOL/ATP_Linkup" GCD Parity
 begin
 
 definition
   coprime :: "nat => nat => bool" where
-  "coprime m n \<longleftrightarrow> (gcd (m, n) = 1)"
+  "coprime m n \<longleftrightarrow> (gcd m n = 1)"
 
 definition
   prime :: "nat \<Rightarrow> bool" where
   [code func del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
 

   apply (auto simp add: prime_def)
   apply (case_tac m)
    apply (auto dest!: dvd_imp_le)
   done
 
-lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd (p, n) = 1"
+lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd p n = 1"
   apply (auto simp add: prime_def)
   apply (metis One_nat_def gcd_dvd1 gcd_dvd2)
   done
 
 text {*

   ultimately have ?thesis by blast}
  ultimately show ?thesis by blast
 qed
 
 text {* Greatest common divisor. *}
-lemma gcd_unique: "d dvd a\<and>d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd(a,b)"
+lemma gcd_unique: "d dvd a\<and>d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
 proof(auto)
   assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
   from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b] 
-  have th: "gcd (a,b) dvd d" by blast
-  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd (a,b)" by blast 
+  have th: "gcd a b dvd d" by blast
+  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]] show "d =gcd a b" by blast 
 qed
 
 lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
-  shows "gcd (x,y) = gcd(u,v)"
-proof-
-  from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd (u,v)" by simp
-  with gcd_unique[of "gcd(u,v)" x y]  show ?thesis by auto
-qed
-
-lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd(a,b) \<or> b * x - a * y = gcd(a,b)"
-proof-
-  let ?g = "gcd (a,b)"
+  shows "gcd x y = gcd u v"
+proof-
+  from H have "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd gcd u v" by simp
+  with gcd_unique[of "gcd u v" x y]  show ?thesis by auto
+qed
+
+lemma bezout_gcd: "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
+proof-
+  let ?g = "gcd a b"
   from bezout[of a b] obtain d x y where d: "d dvd a" "d dvd b" "a * x - b * y = d \<or> b * x - a * y = d" by blast
   from d(1,2) have "d dvd ?g" by simp
   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
   from d(3) have "(a * x - b * y)*k = d*k \<or> (b * x - a * y)*k = d*k" by blast 
   hence "a * x * k - b * y*k = d*k \<or> b * x * k - a * y*k = d*k"

     by (simp add: k mult_assoc)
   thus ?thesis by blast
 qed
 
 lemma bezout_gcd_strong: assumes a: "a \<noteq> 0" 
-  shows "\<exists>x y. a * x = b * y + gcd(a,b)"
-proof-
-  let ?g = "gcd (a,b)"
+  shows "\<exists>x y. a * x = b * y + gcd a b"
+proof-
+  let ?g = "gcd a b"
   from bezout_add_strong[OF a, of b]
   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
   from d(1,2) have "d dvd ?g" by simp
   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
   from d(3) have "a * x * k = (b * y + d) *k " by auto 
   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
   thus ?thesis by blast
 qed
 
-lemma gcd_mult_distrib: "gcd(a * c, b * c) = c * gcd(a,b)"
+lemma gcd_mult_distrib: "gcd (a * c) (b * c) = c * gcd a b"
 by(simp add: gcd_mult_distrib2 mult_commute)
 
-lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd(a,b) dvd d"
+lemma gcd_bezout: "(\<exists>x y. a * x - b * y = d \<or> b * x - a * y = d) \<longleftrightarrow> gcd a b dvd d"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
-  let ?g = "gcd (a,b)"
+  let ?g = "gcd a b"
   {assume H: ?rhs then obtain k where k: "d = ?g*k" unfolding dvd_def by blast
     from bezout_gcd[of a b] obtain x y where xy: "a * x - b * y = ?g \<or> b * x - a * y = ?g"
       by blast
     hence "(a * x - b * y)*k = ?g*k \<or> (b * x - a * y)*k = ?g*k" by auto
     hence "a * x*k - b * y*k = ?g*k \<or> b * x * k - a * y*k = ?g*k" 

     from dvd_diff[OF dv(1,2)] dvd_diff[OF dv(3,4)] H
     have ?rhs by auto}
   ultimately show ?thesis by blast
 qed
 
-lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd(a,b) dvd d"
-proof-
-  let ?g = "gcd (a,b)"
+lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd a b dvd d"
+proof-
+  let ?g = "gcd a b"
     have dv: "?g dvd a*x" "?g dvd b * y" 
       using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
     from dvd_add[OF dv] H
     show ?thesis by auto
 qed
 
-lemma gcd_mult': "gcd(b,a * b) = b"
+lemma gcd_mult': "gcd b (a * b) = b"
 by (simp add: gcd_mult mult_commute[of a b]) 
 
-lemma gcd_add: "gcd(a + b,b) = gcd(a,b)" "gcd(b + a,b) = gcd(a,b)" "gcd(a,a + b) = gcd(a,b)" "gcd(a,b + a) = gcd(a,b)"
+lemma gcd_add: "gcd (a + b) b = gcd a b" "gcd (b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
 apply (simp_all add: gcd_add1)
 by (simp add: gcd_commute gcd_add1)
 
-lemma gcd_sub: "b <= a ==> gcd(a - b,b) = gcd(a,b)" "a <= b ==> gcd(a,b - a) = gcd(a,b)"
+lemma gcd_sub: "b <= a ==> gcd (a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
 proof-
   {fix a b assume H: "b \<le> (a::nat)"
     hence th: "a - b + b = a" by arith
-    from gcd_add(1)[of "a - b" b] th  have "gcd(a - b,b) = gcd(a,b)" by simp}
+    from gcd_add(1)[of "a - b" b] th  have "gcd (a - b) b = gcd a b" by simp}
   note th = this
 {
   assume ab: "b \<le> a"
-  from th[OF ab] show "gcd (a - b, b) = gcd (a, b)" by blast
+  from th[OF ab] show "gcd (a - b) b = gcd a b" by blast
 next
   assume ab: "a \<le> b"
-  from th[OF ab] show "gcd (a,b - a) = gcd (a, b)" 
+  from th[OF ab] show "gcd a (b - a) = gcd a b" 
     by (simp add: gcd_commute)}
 qed
 
 text {* Coprimality *}
 

 lemma coprime_1'[simp]: "coprime 1 a" by (simp add: coprime_def)
 lemma coprime_Suc0[simp]: "coprime a (Suc 0)" by (simp add: coprime_def)
 lemma coprime_Suc0'[simp]: "coprime (Suc 0) a" by (simp add: coprime_def)
 
 lemma gcd_coprime: 
-  assumes z: "gcd(a,b) \<noteq> 0" and a: "a = a' * gcd(a,b)" and b: "b = b' * gcd(a,b)" 
+  assumes z: "gcd a b \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b" 
   shows    "coprime a' b'"
 proof-
-  let ?g = "gcd(a,b)"
+  let ?g = "gcd a b"
   {assume bz: "a = 0" from b bz z a have ?thesis by (simp add: gcd_zero coprime_def)}
   moreover 
   {assume az: "a\<noteq> 0" 
     from z have z': "?g > 0" by simp
     from bezout_gcd_strong[OF az, of b] 

 qed
 lemma coprime_0: "coprime d 0 \<longleftrightarrow> d = 1" by (simp add: coprime_def)
 lemma coprime_mul: assumes da: "coprime d a" and db: "coprime d b"
   shows "coprime d (a * b)"
 proof-
-  from da have th: "gcd(a, d) = 1" by (simp add: coprime_def gcd_commute)
-  from gcd_mult_cancel[of a d b, OF th] db[unfolded coprime_def] have "gcd (d, a*b) = 1"
+  from da have th: "gcd a d = 1" by (simp add: coprime_def gcd_commute)
+  from gcd_mult_cancel[of a d b, OF th] db[unfolded coprime_def] have "gcd d (a * b) = 1"
     by (simp add: gcd_commute)
   thus ?thesis unfolding coprime_def .
 qed
 lemma coprime_lmul2: assumes dab: "coprime d (a * b)" shows "coprime d b"
 using prems unfolding coprime_bezout

 lemma coprime_mul_eq: "coprime d (a * b) \<longleftrightarrow> coprime d a \<and>  coprime d b"
   using coprime_rmul2[of d a b] coprime_lmul2[of d a b] coprime_mul[of d a b] 
   by blast
 
 lemma gcd_coprime_exists:
-  assumes nz: "gcd(a,b) \<noteq> 0" 
-  shows "\<exists>a' b'. a = a' * gcd(a,b) \<and> b = b' * gcd(a,b) \<and> coprime a' b'"
-proof-
-  let ?g = "gcd (a,b)"
+  assumes nz: "gcd a b \<noteq> 0" 
+  shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
+proof-
+  let ?g = "gcd a b"
   from gcd_dvd1[of a b] gcd_dvd2[of a b] 
   obtain a' b' where "a = ?g*a'"  "b = ?g*b'" unfolding dvd_def by blast
   hence ab': "a = a'*?g" "b = b'*?g" by algebra+
   from ab' gcd_coprime[OF nz ab'] show ?thesis by blast
 qed

   apply simp
   done
 lemma coprime_minus1: "n \<noteq> 0 ==> coprime (n - 1) n"
   using coprime_plus1[of "n - 1"] coprime_commute[of "n - 1" n] by auto
 
-lemma bezout_gcd_pow: "\<exists>x y. a ^n * x - b ^ n * y = gcd(a,b) ^ n \<or> b ^ n * x - a ^ n * y = gcd(a,b) ^ n"
-proof-
-  let ?g = "gcd (a,b)"
+lemma bezout_gcd_pow: "\<exists>x y. a ^n * x - b ^ n * y = gcd a b ^ n \<or> b ^ n * x - a ^ n * y = gcd a b ^ n"
+proof-
+  let ?g = "gcd a b"
   {assume z: "?g = 0" hence ?thesis 
       apply (cases n, simp)
       apply arith
       apply (simp only: z power_0_Suc)
       apply (rule exI[where x=0])

       using z ab'' by (simp only: power_mult_distrib[symmetric] 
 	diff_mult_distrib2 mult_assoc[symmetric])
     hence  ?thesis by blast }
   ultimately show ?thesis by blast
 qed
-lemma gcd_exp: "gcd (a^n, b^n) = gcd(a,b)^n"
-proof-
-  let ?g = "gcd(a^n,b^n)"
-  let ?gn = "gcd(a,b)^n"
+lemma gcd_exp: "gcd (a^n) (b^n) = gcd a b ^ n"
+proof-
+  let ?g = "gcd (a^n) (b^n)"
+  let ?gn = "gcd a b ^ n"
   {fix e assume H: "e dvd a^n" "e dvd b^n"
     from bezout_gcd_pow[of a n b] obtain x y 
       where xy: "a ^ n * x - b ^ n * y = ?gn \<or> b ^ n * x - a ^ n * y = ?gn" by blast
     from dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
       dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
-    have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd (a, b) ^ n", simp_all)}
+    have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd a b ^ n", simp_all)}
   hence th:  "\<forall>e. e dvd a^n \<and> e dvd b^n \<longrightarrow> e dvd ?gn" by blast
   from divides_exp[OF gcd_dvd1[of a b], of n] divides_exp[OF gcd_dvd2[of a b], of n] th
     gcd_unique have "?gn = ?g" by blast thus ?thesis by simp 
 qed
 

 by (simp only: coprime_def gcd_exp exp_eq_1) simp
 
 lemma division_decomp: assumes dc: "(a::nat) dvd b * c"
   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
 proof-
-  let ?g = "gcd (a,b)"
+  let ?g = "gcd a b"
   {assume "?g = 0" with dc have ?thesis apply (simp add: gcd_zero)
       apply (rule exI[where x="0"])
       by (rule exI[where x="c"], simp)}
   moreover
   {assume z: "?g \<noteq> 0"

 
 lemma nat_power_eq_0_iff: "(m::nat) ^ n = 0 \<longleftrightarrow> n \<noteq> 0 \<and> m = 0" by (induct n, auto)
 
 lemma divides_rev: assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0" shows "a dvd b"
 proof-
-  let ?g = "gcd (a,b)"
+  let ?g = "gcd a b"
   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   {assume "?g = 0" with ab n have ?thesis by (simp add: gcd_zero)}
   moreover
   {assume z: "?g \<noteq> 0"
     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)