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.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"
```