src/HOL/Number_Theory/Primes.thy
changeset 60526 fad653acf58f
parent 59730 b7c394c7a619
child 60688 01488b559910
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Fri Jun 19 21:33:03 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Jun 19 21:41:33 2015 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -section {* Primes *}
     1.8 +section \<open>Primes\<close>
     1.9  
    1.10  theory Primes
    1.11  imports "~~/src/HOL/GCD" "~~/src/HOL/Binomial"
    1.12 @@ -40,7 +40,7 @@
    1.13  lemmas prime_nat_def = prime_def
    1.14  
    1.15  
    1.16 -subsection {* Primes *}
    1.17 +subsection \<open>Primes\<close>
    1.18  
    1.19  lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    1.20    apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
    1.21 @@ -126,7 +126,7 @@
    1.22    by (cases n) (auto elim: prime_dvd_power_int)
    1.23  
    1.24  
    1.25 -subsubsection {* Make prime naively executable *}
    1.26 +subsubsection \<open>Make prime naively executable\<close>
    1.27  
    1.28  lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
    1.29    by (simp add: prime_nat_def)
    1.30 @@ -152,7 +152,7 @@
    1.31  lemma two_is_prime_nat [simp]: "prime (2::nat)"
    1.32    by simp
    1.33  
    1.34 -text{* A bit of regression testing: *}
    1.35 +text\<open>A bit of regression testing:\<close>
    1.36  
    1.37  lemma "prime(97::nat)" by simp
    1.38  lemma "prime(997::nat)" by eval
    1.39 @@ -181,7 +181,7 @@
    1.40      nat_dvd_not_less neq0_conv prime_nat_def)
    1.41    done
    1.42  
    1.43 -text {* One property of coprimality is easier to prove via prime factors. *}
    1.44 +text \<open>One property of coprimality is easier to prove via prime factors.\<close>
    1.45  
    1.46  lemma prime_divprod_pow_nat:
    1.47    assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
    1.48 @@ -222,7 +222,7 @@
    1.49  qed
    1.50  
    1.51  
    1.52 -subsection {* Infinitely many primes *}
    1.53 +subsection \<open>Infinitely many primes\<close>
    1.54  
    1.55  lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
    1.56  proof-
    1.57 @@ -231,18 +231,18 @@
    1.58    obtain p where "prime p" and "p dvd fact n + 1" by auto
    1.59    then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
    1.60    { assume "p \<le> n"
    1.61 -    from `prime p` have "p \<ge> 1"
    1.62 +    from \<open>prime p\<close> have "p \<ge> 1"
    1.63        by (cases p, simp_all)
    1.64 -    with `p <= n` have "p dvd fact n"
    1.65 +    with \<open>p <= n\<close> have "p dvd fact n"
    1.66        by (intro dvd_fact)
    1.67 -    with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
    1.68 +    with \<open>p dvd fact n + 1\<close> have "p dvd fact n + 1 - fact n"
    1.69        by (rule dvd_diff_nat)
    1.70      then have "p dvd 1" by simp
    1.71      then have "p <= 1" by auto
    1.72 -    moreover from `prime p` have "p > 1" by auto
    1.73 +    moreover from \<open>prime p\<close> have "p > 1" by auto
    1.74      ultimately have False by auto}
    1.75    then have "n < p" by presburger
    1.76 -  with `prime p` and `p <= fact n + 1` show ?thesis by auto
    1.77 +  with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
    1.78  qed
    1.79  
    1.80  lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
    1.81 @@ -259,9 +259,9 @@
    1.82      by auto
    1.83  qed
    1.84  
    1.85 -subsection{*Powers of Primes*}
    1.86 +subsection\<open>Powers of Primes\<close>
    1.87  
    1.88 -text{*Versions for type nat only*}
    1.89 +text\<open>Versions for type nat only\<close>
    1.90  
    1.91  lemma prime_product:
    1.92    fixes p::nat
    1.93 @@ -271,7 +271,7 @@
    1.94    from assms have
    1.95      "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
    1.96      unfolding prime_nat_def by auto
    1.97 -  from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
    1.98 +  from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
    1.99    then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
   1.100    have "p dvd p * q" by simp
   1.101    then have "p = 1 \<or> p = p * q" by (rule P)
   1.102 @@ -370,7 +370,7 @@
   1.103    thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
   1.104  qed
   1.105  
   1.106 -subsection {*Chinese Remainder Theorem Variants*}
   1.107 +subsection \<open>Chinese Remainder Theorem Variants\<close>
   1.108  
   1.109  lemma bezout_gcd_nat:
   1.110    fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
   1.111 @@ -391,7 +391,7 @@
   1.112  qed
   1.113  
   1.114  
   1.115 -text {* A binary form of the Chinese Remainder Theorem. *}
   1.116 +text \<open>A binary form of the Chinese Remainder Theorem.\<close>
   1.117  
   1.118  lemma chinese_remainder:
   1.119    fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
   1.120 @@ -411,7 +411,7 @@
   1.121    thus ?thesis by blast
   1.122  qed
   1.123  
   1.124 -text {* Primality *}
   1.125 +text \<open>Primality\<close>
   1.126  
   1.127  lemma coprime_bezout_strong:
   1.128    fixes a::nat assumes "coprime a b"  "b \<noteq> 1"