src/HOL/Old_Number_Theory/Primes.thy
 changeset 61382 efac889fccbc parent 61076 bdc1e2f0a86a child 62348 9a5f43dac883
```     1.1 --- a/src/HOL/Old_Number_Theory/Primes.thy	Sat Oct 10 16:21:34 2015 +0200
1.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy	Sat Oct 10 16:26:23 2015 +0200
1.3 @@ -3,7 +3,7 @@
1.4      Copyright   1996  University of Cambridge
1.5  *)
1.6
1.7 -section {* Primality on nat *}
1.8 +section \<open>Primality on nat\<close>
1.9
1.10  theory Primes
1.11  imports Complex_Main Legacy_GCD
1.12 @@ -27,11 +27,11 @@
1.13    apply (metis gcd_dvd1 gcd_dvd2)
1.14    done
1.15
1.16 -text {*
1.17 +text \<open>
1.18    This theorem leads immediately to a proof of the uniqueness of
1.19    factorization.  If @{term p} divides a product of primes then it is
1.20    one of those primes.
1.21 -*}
1.22 +\<close>
1.23
1.24  lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \<or> p dvd n"
1.25    by (blast intro: relprime_dvd_mult prime_imp_relprime)
1.26 @@ -92,7 +92,7 @@
1.27    ultimately show ?thesis by blast
1.28  qed
1.29
1.30 -text {* Elementary theory of divisibility *}
1.31 +text \<open>Elementary theory of divisibility\<close>
1.32  lemma divides_ge: "(a::nat) dvd b \<Longrightarrow> b = 0 \<or> a \<le> b" unfolding dvd_def by auto
1.33  lemma divides_antisym: "(x::nat) dvd y \<and> y dvd x \<longleftrightarrow> x = y"
1.34    using dvd_antisym[of x y] by auto
1.35 @@ -176,7 +176,7 @@
1.36  lemma divides_rexp:
1.37    "x dvd y \<Longrightarrow> (x::nat) dvd (y^(Suc n))" by (simp add: dvd_mult2[of x y])
1.38
1.39 -text {* Coprimality *}
1.40 +text \<open>Coprimality\<close>
1.41
1.42  lemma coprime: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
1.43  using gcd_unique[of 1 a b, simplified] by (auto simp add: coprime_def)
1.44 @@ -379,7 +379,7 @@
1.45  qed
1.46
1.47
1.48 -text {* A binary form of the Chinese Remainder Theorem. *}
1.49 +text \<open>A binary form of the Chinese Remainder Theorem.\<close>
1.50
1.51  lemma chinese_remainder: assumes ab: "coprime a b" and a:"a \<noteq> 0" and b:"b \<noteq> 0"
1.52    shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
1.53 @@ -397,9 +397,9 @@
1.54    thus ?thesis by blast
1.55  qed
1.56
1.57 -text {* Primality *}
1.58 +text \<open>Primality\<close>
1.59
1.60 -text {* A few useful theorems about primes *}
1.61 +text \<open>A few useful theorems about primes\<close>
1.62
1.63  lemma prime_0[simp]: "~prime 0" by (simp add: prime_def)
1.64  lemma prime_1[simp]: "~ prime 1"  by (simp add: prime_def)
1.65 @@ -591,7 +591,7 @@
1.66  lemma prime_odd: "prime p \<Longrightarrow> p = 2 \<or> odd p" unfolding prime_def by auto
1.67
1.68
1.69 -text {* One property of coprimality is easier to prove via prime factors. *}
1.70 +text \<open>One property of coprimality is easier to prove via prime factors.\<close>
1.71
1.72  lemma prime_divprod_pow:
1.73    assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
1.74 @@ -714,7 +714,7 @@
1.75  ultimately show ?ths by blast
1.76  qed
1.77
1.78 -text {* More useful lemmas. *}
1.79 +text \<open>More useful lemmas.\<close>
1.80  lemma prime_product:
1.81    assumes "prime (p * q)"
1.82    shows "p = 1 \<or> q = 1"
1.83 @@ -722,7 +722,7 @@
1.84    from assms have
1.85      "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
1.86      unfolding prime_def by auto
1.87 -  from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
1.88 +  from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
1.89    then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
1.90    have "p dvd p * q" by simp
1.91    then have "p = 1 \<or> p = p * q" by (rule P)
```