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)