--- a/src/HOL/Number_Theory/Cong.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Cong.thy Fri Jun 19 21:41:33 2015 +0200
@@ -23,13 +23,13 @@
natural numbers and the integers, and added a number of new theorems.
*)
-section {* Congruence *}
+section \<open>Congruence\<close>
theory Cong
imports Primes
begin
-subsection {* Turn off @{text One_nat_def} *}
+subsection \<open>Turn off @{text One_nat_def}\<close>
lemma power_eq_one_eq_nat [simp]: "((x::nat)^m = 1) = (m = 0 | x = 1)"
by (induct m) auto
@@ -37,7 +37,7 @@
declare mod_pos_pos_trivial [simp]
-subsection {* Main definitions *}
+subsection \<open>Main definitions\<close>
class cong =
fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(()mod _'))")
@@ -74,7 +74,7 @@
end
-subsection {* Set up Transfer *}
+subsection \<open>Set up Transfer\<close>
lemma transfer_nat_int_cong:
@@ -97,7 +97,7 @@
transfer_int_nat_cong]
-subsection {* Congruence *}
+subsection \<open>Congruence\<close>
(* was zcong_0, etc. *)
lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
@@ -633,20 +633,20 @@
have "[?x = u1 * 1 + u2 * 0] (mod m1)"
apply (rule cong_add_nat)
apply (rule cong_scalar2_nat)
- apply (rule `[b1 = 1] (mod m1)`)
+ apply (rule \<open>[b1 = 1] (mod m1)\<close>)
apply (rule cong_scalar2_nat)
- apply (rule `[b2 = 0] (mod m1)`)
+ apply (rule \<open>[b2 = 0] (mod m1)\<close>)
done
then have "[?x = u1] (mod m1)" by simp
have "[?x = u1 * 0 + u2 * 1] (mod m2)"
apply (rule cong_add_nat)
apply (rule cong_scalar2_nat)
- apply (rule `[b1 = 0] (mod m2)`)
+ apply (rule \<open>[b1 = 0] (mod m2)\<close>)
apply (rule cong_scalar2_nat)
- apply (rule `[b2 = 1] (mod m2)`)
+ apply (rule \<open>[b2 = 1] (mod m2)\<close>)
done
then have "[?x = u2] (mod m2)" by simp
- with `[?x = u1] (mod m1)` show ?thesis by blast
+ with \<open>[?x = u1] (mod m1)\<close> show ?thesis by blast
qed
lemma binary_chinese_remainder_int:
@@ -661,20 +661,20 @@
have "[?x = u1 * 1 + u2 * 0] (mod m1)"
apply (rule cong_add_int)
apply (rule cong_scalar2_int)
- apply (rule `[b1 = 1] (mod m1)`)
+ apply (rule \<open>[b1 = 1] (mod m1)\<close>)
apply (rule cong_scalar2_int)
- apply (rule `[b2 = 0] (mod m1)`)
+ apply (rule \<open>[b2 = 0] (mod m1)\<close>)
done
then have "[?x = u1] (mod m1)" by simp
have "[?x = u1 * 0 + u2 * 1] (mod m2)"
apply (rule cong_add_int)
apply (rule cong_scalar2_int)
- apply (rule `[b1 = 0] (mod m2)`)
+ apply (rule \<open>[b1 = 0] (mod m2)\<close>)
apply (rule cong_scalar2_int)
- apply (rule `[b2 = 1] (mod m2)`)
+ apply (rule \<open>[b2 = 1] (mod m2)\<close>)
done
then have "[?x = u2] (mod m2)" by simp
- with `[?x = u1] (mod m1)` show ?thesis by blast
+ with \<open>[?x = u1] (mod m1)\<close> show ?thesis by blast
qed
lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
@@ -712,7 +712,7 @@
have one: "[?x = u1] (mod m1)"
apply (rule cong_trans_nat)
prefer 2
- apply (rule `[y = u1] (mod m1)`)
+ apply (rule \<open>[y = u1] (mod m1)\<close>)
apply (rule cong_modulus_mult_nat)
apply (rule cong_mod_nat)
using nz apply auto
@@ -720,7 +720,7 @@
have two: "[?x = u2] (mod m2)"
apply (rule cong_trans_nat)
prefer 2
- apply (rule `[y = u2] (mod m2)`)
+ apply (rule \<open>[y = u2] (mod m2)\<close>)
apply (subst mult.commute)
apply (rule cong_modulus_mult_nat)
apply (rule cong_mod_nat)
@@ -733,19 +733,19 @@
assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)"
have "[?x = z] (mod m1)"
apply (rule cong_trans_nat)
- apply (rule `[?x = u1] (mod m1)`)
+ apply (rule \<open>[?x = u1] (mod m1)\<close>)
apply (rule cong_sym_nat)
- apply (rule `[z = u1] (mod m1)`)
+ apply (rule \<open>[z = u1] (mod m1)\<close>)
done
moreover have "[?x = z] (mod m2)"
apply (rule cong_trans_nat)
- apply (rule `[?x = u2] (mod m2)`)
+ apply (rule \<open>[?x = u2] (mod m2)\<close>)
apply (rule cong_sym_nat)
- apply (rule `[z = u2] (mod m2)`)
+ apply (rule \<open>[z = u2] (mod m2)\<close>)
done
ultimately have "[?x = z] (mod m1 * m2)"
by (auto intro: coprime_cong_mult_nat a)
- with `z < m1 * m2` `?x < m1 * m2` show "z = ?x"
+ with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x"
apply (intro cong_less_modulus_unique_nat)
apply (auto, erule cong_sym_nat)
done
--- a/src/HOL/Number_Theory/Eratosthenes.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy Fri Jun 19 21:41:33 2015 +0200
@@ -2,14 +2,14 @@
Author: Florian Haftmann, TU Muenchen
*)
-section {* The sieve of Eratosthenes *}
+section \<open>The sieve of Eratosthenes\<close>
theory Eratosthenes
imports Main Primes
begin
-subsection {* Preliminary: strict divisibility *}
+subsection \<open>Preliminary: strict divisibility\<close>
context dvd
begin
@@ -20,9 +20,9 @@
end
-subsection {* Main corpus *}
+subsection \<open>Main corpus\<close>
-text {* The sieve is modelled as a list of booleans, where @{const False} means \emph{marked out}. *}
+text \<open>The sieve is modelled as a list of booleans, where @{const False} means \emph{marked out}.\<close>
type_synonym marks = "bool list"
@@ -58,7 +58,7 @@
intro!: sorted_filter distinct_filter inj_onI sorted_distinct_set_unique)
-text {* Marking out multiples in a sieve *}
+text \<open>Marking out multiples in a sieve\<close>
definition mark_out :: "nat \<Rightarrow> marks \<Rightarrow> marks"
where
@@ -78,7 +78,7 @@
nth_enumerate_eq less_eq_dvd_minus)
-text {* Auxiliary operation for efficient implementation *}
+text \<open>Auxiliary operation for efficient implementation\<close>
definition mark_out_aux :: "nat \<Rightarrow> nat \<Rightarrow> marks \<Rightarrow> marks"
where
@@ -104,15 +104,15 @@
assume "\<not> q > 0"
with q show False by simp
qed
- with `n > 0` have "Suc n * q \<ge> 2" by (auto simp add: gr0_conv_Suc)
+ with \<open>n > 0\<close> have "Suc n * q \<ge> 2" by (auto simp add: gr0_conv_Suc)
with q have a: "a = Suc n * q - 2" by simp
with B have "q + n * q < n + n + 2"
by auto
then have "m * q < m * 2" by (simp add: m_def)
- with `m > 0` have "q < 2" by simp
- with `q > 0` have "q = 1" by simp
+ with \<open>m > 0\<close> have "q < 2" by simp
+ with \<open>q > 0\<close> have "q = 1" by simp
with a have "a = n - 1" by simp
- with `n > 0` C show False by simp
+ with \<open>n > 0\<close> C show False by simp
qed
} note aux = this
show ?thesis
@@ -157,7 +157,7 @@
qed
-text {* Main entry point to sieve *}
+text \<open>Main entry point to sieve\<close>
fun sieve :: "nat \<Rightarrow> marks \<Rightarrow> marks"
where
@@ -165,7 +165,7 @@
| "sieve n (False # bs) = False # sieve (Suc n) bs"
| "sieve n (True # bs) = True # sieve (Suc n) (mark_out n bs)"
-text {*
+text \<open>
There are the following possible optimisations here:
\begin{itemize}
@@ -179,7 +179,7 @@
\end{itemize}
This is left as an constructive exercise to the reader.
-*}
+\<close>
lemma numbers_of_marks_sieve:
"numbers_of_marks (Suc n) (sieve n bs) =
@@ -199,15 +199,15 @@
assume "n > 0 \<and> n - 1 \<in> M"
then have "n > 0" and "n - 1 \<in> M" by auto
then have "Suc (n - 1) \<in> Suc ` M" by blast
- with `n > 0` show "n \<in> Suc ` M" by simp
+ with \<open>n > 0\<close> show "n \<in> Suc ` M" by simp
qed
{ fix m :: nat
assume "Suc (Suc n) \<le> m" and "m dvd Suc n"
- from `m dvd Suc n` obtain q where "Suc n = m * q" ..
- with `Suc (Suc n) \<le> m` have "Suc (m * q) \<le> m" by simp
+ from \<open>m dvd Suc n\<close> obtain q where "Suc n = m * q" ..
+ with \<open>Suc (Suc n) \<le> m\<close> have "Suc (m * q) \<le> m" by simp
then have "m * q < m" by arith
then have "q = 0" by simp
- with `Suc n = m * q` have False by simp
+ with \<open>Suc n = m * q\<close> have False by simp
} note aux1 = this
{ fix m q :: nat
assume "\<forall>q>0. 1 < q \<longrightarrow> Suc n < q \<longrightarrow> q \<le> Suc (n + length bs)
@@ -219,7 +219,7 @@
then have "\<not> Suc n dvd q" by (auto elim: dvdE)
moreover assume "Suc n < q" and "q \<le> Suc (n + length bs)"
and "bs ! (q - Suc (Suc n))"
- moreover note `q dvd m`
+ moreover note \<open>q dvd m\<close>
ultimately have "m dvd q" by (auto intro: *)
} note aux2 = this
from 3 show ?case
@@ -234,7 +234,7 @@
qed
-text {* Relation of the sieve algorithm to actual primes *}
+text \<open>Relation of the sieve algorithm to actual primes\<close>
definition primes_upto :: "nat \<Rightarrow> nat list"
where
@@ -267,11 +267,11 @@
assume *: "\<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m"
and "m dvd q" and "m \<noteq> 1"
have "m = q" proof (cases "m = 0")
- case True with `m dvd q` show ?thesis by simp
+ case True with \<open>m dvd q\<close> show ?thesis by simp
next
- case False with `m \<noteq> 1` have "Suc (Suc 0) \<le> m" by arith
- with `m < Suc n` * `m dvd q` have "q dvd m" by simp
- with `m dvd q` show ?thesis by (simp add: dvd.eq_iff)
+ case False with \<open>m \<noteq> 1\<close> have "Suc (Suc 0) \<le> m" by arith
+ with \<open>m < Suc n\<close> * \<open>m dvd q\<close> have "q dvd m" by simp
+ with \<open>m dvd q\<close> show ?thesis by (simp add: dvd.eq_iff)
qed
}
then have aux: "\<And>m q. Suc (Suc 0) \<le> q \<Longrightarrow>
@@ -303,7 +303,7 @@
by (simp add: set_primes_upto)
-subsection {* Application: smallest prime beyond a certain number *}
+subsection \<open>Application: smallest prime beyond a certain number\<close>
definition smallest_prime_beyond :: "nat \<Rightarrow> nat"
where
@@ -348,7 +348,7 @@
def A \<equiv> "{p. p \<le> n \<and> prime p \<and> m \<le> p}"
assume assms: "m \<le> p" "prime p" "p \<le> n"
then have "smallest_prime_beyond m \<le> p" by (auto intro: smallest_prime_beyond_smallest)
- from this `p \<le> n` have *: "smallest_prime_beyond m \<le> n" by (rule order_trans)
+ from this \<open>p \<le> n\<close> have *: "smallest_prime_beyond m \<le> n" by (rule order_trans)
from assms have ex: "\<exists>p\<le>n. prime p \<and> m \<le> p" by auto
then have "finite A" by (auto simp add: A_def)
with * have "Min A = smallest_prime_beyond m"
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Fri Jun 19 21:41:33 2015 +0200
@@ -1,12 +1,12 @@
(* Author: Manuel Eberl *)
-section {* Abstract euclidean algorithm *}
+section \<open>Abstract euclidean algorithm\<close>
theory Euclidean_Algorithm
imports Complex_Main
begin
-text {*
+text \<open>
A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
implemented. It must provide:
\begin{itemize}
@@ -18,7 +18,7 @@
\end{itemize}
The existence of these functions makes it possible to derive gcd and lcm functions
for any Euclidean semiring.
-*}
+\<close>
class euclidean_semiring = semiring_div +
fixes euclidean_size :: "'a \<Rightarrow> nat"
fixes normalization_factor :: "'a \<Rightarrow> 'a"
@@ -60,17 +60,17 @@
proof (cases "a = 0", simp)
assume "a \<noteq> 0"
let ?nf = "normalization_factor"
- from normalization_factor_is_unit[OF `a \<noteq> 0`] have "?nf a \<noteq> 0"
+ from normalization_factor_is_unit[OF \<open>a \<noteq> 0\<close>] have "?nf a \<noteq> 0"
by auto
have "?nf (a div ?nf a) * ?nf (?nf a) = ?nf (a div ?nf a * ?nf a)"
by (simp add: normalization_factor_mult)
- also have "a div ?nf a * ?nf a = a" using `a \<noteq> 0`
+ also have "a div ?nf a * ?nf a = a" using \<open>a \<noteq> 0\<close>
by simp
- also have "?nf (?nf a) = ?nf a" using `a \<noteq> 0`
+ also have "?nf (?nf a) = ?nf a" using \<open>a \<noteq> 0\<close>
normalization_factor_is_unit normalization_factor_unit by simp
finally have "normalization_factor (a div normalization_factor a) = 1"
- using `?nf a \<noteq> 0` by (metis div_mult_self2_is_id div_self)
- with `a \<noteq> 0` show ?thesis by simp
+ using \<open>?nf a \<noteq> 0\<close> by (metis div_mult_self2_is_id div_self)
+ with \<open>a \<noteq> 0\<close> show ?thesis by simp
qed
lemma normalization_0_iff [simp]:
@@ -90,7 +90,7 @@
apply (subst (asm) unit_eq_div1, blast, subst (asm) unit_div_commute, blast)
apply (subst div_mult_swap, simp, simp)
done
- with `a \<noteq> 0` `b \<noteq> 0` have "\<exists>c. is_unit c \<and> a = c * b"
+ with \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close> have "\<exists>c. is_unit c \<and> a = c * b"
by (intro exI[of _ "?nf a div ?nf b"], force simp: mult_ac)
then obtain c where "is_unit c" and "a = c * b" by blast
then show "associated a b" by (rule is_unit_associatedI)
@@ -99,7 +99,7 @@
assume "a \<noteq> 0" "b \<noteq> 0" "associated a b"
then obtain c where "is_unit c" and "a = c * b" by (blast elim: associated_is_unitE)
then show "a div ?nf a = b div ?nf b"
- apply (simp only: `a = c * b` normalization_factor_mult normalization_factor_unit)
+ apply (simp only: \<open>a = c * b\<close> normalization_factor_mult normalization_factor_unit)
apply (rule div_mult_mult1, force)
done
qed
@@ -129,10 +129,10 @@
assume "b mod a \<noteq> 0"
from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff)
from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast
- with `b mod a \<noteq> 0` have "c \<noteq> 0" by auto
- with `b mod a = b * c` have "euclidean_size (b mod a) \<ge> euclidean_size b"
+ with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
+ with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
using size_mult_mono by force
- moreover from `a \<noteq> 0` have "euclidean_size (b mod a) < euclidean_size a"
+ moreover from \<open>a \<noteq> 0\<close> have "euclidean_size (b mod a) < euclidean_size a"
using mod_size_less by blast
ultimately show False using size_eq by simp
qed
@@ -272,7 +272,7 @@
fix l assume "l dvd a" and "l dvd gcd b c"
with dvd_trans[OF _ gcd_dvd1] and dvd_trans[OF _ gcd_dvd2]
have "l dvd b" and "l dvd c" by blast+
- with `l dvd a` show "l dvd gcd (gcd a b) c"
+ with \<open>l dvd a\<close> show "l dvd gcd (gcd a b) c"
by (intro gcd_greatest)
qed
next
@@ -369,7 +369,7 @@
proof -
have "gcd a b dvd a" by (rule gcd_dvd1)
then obtain c where A: "a = gcd a b * c" unfolding dvd_def by blast
- with `a \<noteq> 0` show ?thesis by (subst (2) A, intro size_mult_mono) auto
+ with \<open>a \<noteq> 0\<close> show ?thesis by (subst (2) A, intro size_mult_mono) auto
qed
lemma euclidean_size_gcd_le2 [simp]:
@@ -381,11 +381,11 @@
shows "euclidean_size (gcd a b) < euclidean_size a"
proof (rule ccontr)
assume "\<not>euclidean_size (gcd a b) < euclidean_size a"
- with `a \<noteq> 0` have "euclidean_size (gcd a b) = euclidean_size a"
+ with \<open>a \<noteq> 0\<close> have "euclidean_size (gcd a b) = euclidean_size a"
by (intro le_antisym, simp_all)
with assms have "a dvd gcd a b" by (auto intro: dvd_euclidean_size_eq_imp_dvd)
hence "a dvd b" using dvd_gcd_D2 by blast
- with `\<not>a dvd b` show False by contradiction
+ with \<open>\<not>a dvd b\<close> show False by contradiction
qed
lemma euclidean_size_gcd_less2:
@@ -445,7 +445,7 @@
let ?nf = "normalization_factor"
from assms gcd_mult_distrib [of a c b]
have A: "a = gcd (a * c) (a * b) * ?nf a" by simp
- from `c dvd a * b` show ?thesis by (subst A, simp_all add: gcd_greatest)
+ from \<open>c dvd a * b\<close> show ?thesis by (subst A, simp_all add: gcd_greatest)
qed
lemma coprime_dvd_mult_iff:
@@ -472,7 +472,7 @@
shows "gcd (k * m) n = gcd m n"
proof (rule gcd_dvd_antisym)
have "gcd (gcd (k * m) n) k = gcd (gcd k n) (k * m)" by (simp add: ac_simps)
- also note `gcd k n = 1`
+ also note \<open>gcd k n = 1\<close>
finally have "gcd (gcd (k * m) n) k = 1" by simp
hence "gcd (k * m) n dvd m" by (rule coprime_dvd_mult, simp add: ac_simps)
moreover have "gcd (k * m) n dvd n" by simp
@@ -488,14 +488,14 @@
assume ?rhs then show ?lhs unfolding associated_def by (fast intro: mult_dvd_mono)
next
assume ?lhs
- from `?lhs` have "a dvd b * d" unfolding associated_def by (metis dvd_mult_left)
+ from \<open>?lhs\<close> have "a dvd b * d" unfolding associated_def by (metis dvd_mult_left)
hence "a dvd b" by (simp add: coprime_dvd_mult_iff)
- moreover from `?lhs` have "b dvd a * c" unfolding associated_def by (metis dvd_mult_left)
+ moreover from \<open>?lhs\<close> have "b dvd a * c" unfolding associated_def by (metis dvd_mult_left)
hence "b dvd a" by (simp add: coprime_dvd_mult_iff)
- moreover from `?lhs` have "c dvd d * b"
+ moreover from \<open>?lhs\<close> have "c dvd d * b"
unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
hence "c dvd d" by (simp add: coprime_dvd_mult_iff gcd.commute)
- moreover from `?lhs` have "d dvd c * a"
+ moreover from \<open>?lhs\<close> have "d dvd c * a"
unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
hence "d dvd c" by (simp add: coprime_dvd_mult_iff gcd.commute)
ultimately show ?rhs unfolding associated_def by simp
@@ -536,7 +536,7 @@
moreover from nz have "d \<noteq> 0" by simp
with div_mult_self1_is_id have "d * (l * u) div d = l * u" .
ultimately have "1 = l * u"
- using `d \<noteq> 0` by simp
+ using \<open>d \<noteq> 0\<close> by simp
then show "l dvd 1" ..
qed
@@ -555,7 +555,7 @@
proof (rule coprimeI)
fix l assume "l dvd d" and "l dvd a"
hence "l dvd a * b" by simp
- with `l dvd d` and dab show "l dvd 1" by (auto intro: gcd_greatest)
+ with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest)
qed
lemma coprime_rmult:
@@ -564,7 +564,7 @@
proof (rule coprimeI)
fix l assume "l dvd d" and "l dvd b"
hence "l dvd a * b" by simp
- with `l dvd d` and dab show "l dvd 1" by (auto intro: gcd_greatest)
+ with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest)
qed
lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
@@ -655,7 +655,7 @@
with dc have "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
from dc ab'(1,2) have "a'*?d dvd (b'*?d) * c" by simp
hence "?d * a' dvd ?d * (b' * c)" by (simp add: mult_ac)
- with `?d \<noteq> 0` have "a' dvd b' * c" by simp
+ with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c" by simp
with coprime_dvd_mult[OF ab'(3)]
have "a' dvd c" by (subst (asm) ac_simps, blast)
with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c" by (simp add: mult_ac)
@@ -672,8 +672,8 @@
let ?d = "gcd a b"
assume "?d \<noteq> 0"
from n obtain m where m: "n = Suc m" by (cases n, simp_all)
- from `?d \<noteq> 0` have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
- from gcd_coprime_exists[OF `?d \<noteq> 0`]
+ from \<open>?d \<noteq> 0\<close> have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
+ from gcd_coprime_exists[OF \<open>?d \<noteq> 0\<close>]
obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
by blast
from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
@@ -755,7 +755,7 @@
hence "gcd a b \<noteq> 0" by simp
from lcm_gcd have "lcm a b * gcd a b = gcd a b * (a * b div (?nf (a*b) * gcd a b))"
by (simp add: mult_ac)
- also from `a * b \<noteq> 0` have "... = a * b div ?nf (a*b)"
+ also from \<open>a * b \<noteq> 0\<close> have "... = a * b div ?nf (a*b)"
by (simp add: div_mult_swap mult.commute)
finally show ?thesis .
qed (auto simp add: lcm_gcd)
@@ -766,11 +766,11 @@
assume "a * b \<noteq> 0"
hence "gcd a b \<noteq> 0" by simp
let ?c = "1 div normalization_factor (a * b)"
- from `a * b \<noteq> 0` have [simp]: "is_unit (normalization_factor (a * b))" by simp
+ from \<open>a * b \<noteq> 0\<close> have [simp]: "is_unit (normalization_factor (a * b))" by simp
from lcm_gcd_prod[of a b] have "lcm a b * gcd a b = a * ?c * b"
by (simp add: div_mult_swap unit_div_commute)
hence "lcm a b * gcd a b div gcd a b = a * ?c * b div gcd a b" by simp
- with `gcd a b \<noteq> 0` have "lcm a b = a * ?c * b div gcd a b"
+ with \<open>gcd a b \<noteq> 0\<close> have "lcm a b = a * ?c * b div gcd a b"
by (subst (asm) div_mult_self2_is_id, simp_all)
also have "... = a * (?c * b div gcd a b)"
by (metis div_mult_swap gcd_dvd2 mult_assoc)
@@ -785,36 +785,36 @@
hence "is_unit (?nf k)" by simp
hence "?nf k \<noteq> 0" by (metis not_is_unit_0)
assume A: "a dvd k" "b dvd k"
- hence "gcd a b \<noteq> 0" using `k \<noteq> 0` by auto
+ hence "gcd a b \<noteq> 0" using \<open>k \<noteq> 0\<close> by auto
from A obtain r s where ar: "k = a * r" and bs: "k = b * s"
unfolding dvd_def by blast
- with `k \<noteq> 0` have "r * s \<noteq> 0"
+ with \<open>k \<noteq> 0\<close> have "r * s \<noteq> 0"
by auto (drule sym [of 0], simp)
hence "is_unit (?nf (r * s))" by simp
let ?c = "?nf k div ?nf (r*s)"
- from `is_unit (?nf k)` and `is_unit (?nf (r * s))` have "is_unit ?c" by (rule unit_div)
+ from \<open>is_unit (?nf k)\<close> and \<open>is_unit (?nf (r * s))\<close> have "is_unit ?c" by (rule unit_div)
hence "?c \<noteq> 0" using not_is_unit_0 by fast
from ar bs have "k * k * gcd s r = ?nf k * k * gcd (k * s) (k * r)"
by (subst mult_assoc, subst gcd_mult_distrib[of k s r], simp only: ac_simps)
also have "... = ?nf k * k * gcd ((r*s) * a) ((r*s) * b)"
- by (subst (3) `k = a * r`, subst (3) `k = b * s`, simp add: algebra_simps)
- also have "... = ?c * r*s * k * gcd a b" using `r * s \<noteq> 0`
+ by (subst (3) \<open>k = a * r\<close>, subst (3) \<open>k = b * s\<close>, simp add: algebra_simps)
+ also have "... = ?c * r*s * k * gcd a b" using \<open>r * s \<noteq> 0\<close>
by (subst gcd_mult_distrib'[symmetric], simp add: algebra_simps unit_simps)
finally have "(a*r) * (b*s) * gcd s r = ?c * k * r * s * gcd a b"
by (subst ar[symmetric], subst bs[symmetric], simp add: mult_ac)
hence "a * b * gcd s r * (r * s) = ?c * k * gcd a b * (r * s)"
by (simp add: algebra_simps)
- hence "?c * k * gcd a b = a * b * gcd s r" using `r * s \<noteq> 0`
+ hence "?c * k * gcd a b = a * b * gcd s r" using \<open>r * s \<noteq> 0\<close>
by (metis div_mult_self2_is_id)
also have "... = lcm a b * gcd a b * gcd s r * ?nf (a*b)"
by (subst lcm_gcd_prod[of a b], metis gcd_mult_distrib gcd_mult_distrib')
also have "... = lcm a b * gcd s r * ?nf (a*b) * gcd a b"
by (simp add: algebra_simps)
- finally have "k * ?c = lcm a b * gcd s r * ?nf (a*b)" using `gcd a b \<noteq> 0`
+ finally have "k * ?c = lcm a b * gcd s r * ?nf (a*b)" using \<open>gcd a b \<noteq> 0\<close>
by (metis mult.commute div_mult_self2_is_id)
- hence "k = lcm a b * (gcd s r * ?nf (a*b)) div ?c" using `?c \<noteq> 0`
+ hence "k = lcm a b * (gcd s r * ?nf (a*b)) div ?c" using \<open>?c \<noteq> 0\<close>
by (metis div_mult_self2_is_id mult_assoc)
- also have "... = lcm a b * (gcd s r * ?nf (a*b) div ?c)" using `is_unit ?c`
+ also have "... = lcm a b * (gcd s r * ?nf (a*b) div ?c)" using \<open>is_unit ?c\<close>
by (simp add: unit_simps)
finally show ?thesis by (rule dvdI)
qed simp
@@ -826,7 +826,7 @@
{
assume "a \<noteq> 0" "b \<noteq> 0"
hence "a * b div ?nf (a * b) \<noteq> 0" by (simp add: no_zero_divisors)
- moreover from `a \<noteq> 0` and `b \<noteq> 0` have "gcd a b \<noteq> 0" by simp
+ moreover from \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "gcd a b \<noteq> 0" by simp
ultimately have "lcm a b \<noteq> 0" using lcm_gcd_prod[of a b] by (intro notI, simp)
} moreover {
assume "a = 0 \<or> b = 0"
@@ -843,12 +843,12 @@
proof-
from assms have "gcd a b \<noteq> 0" by (simp add: lcm_zero)
let ?c = "normalization_factor (a * b)"
- from `lcm a b \<noteq> 0` have "?c \<noteq> 0" by (intro notI, simp add: lcm_zero no_zero_divisors)
+ from \<open>lcm a b \<noteq> 0\<close> have "?c \<noteq> 0" by (intro notI, simp add: lcm_zero no_zero_divisors)
hence "is_unit ?c" by simp
from lcm_gcd_prod [of a b] have "gcd a b = a * b div ?c div lcm a b"
- by (subst (2) div_mult_self2_is_id[OF `lcm a b \<noteq> 0`, symmetric], simp add: mult_ac)
- also from `is_unit ?c` have "... = a * b div (lcm a b * ?c)"
- by (metis `?c \<noteq> 0` div_mult_mult1 dvd_mult_div_cancel mult_commute normalization_factor_dvd')
+ by (subst (2) div_mult_self2_is_id[OF \<open>lcm a b \<noteq> 0\<close>, symmetric], simp add: mult_ac)
+ also from \<open>is_unit ?c\<close> have "... = a * b div (lcm a b * ?c)"
+ by (metis \<open>?c \<noteq> 0\<close> div_mult_mult1 dvd_mult_div_cancel mult_commute normalization_factor_dvd')
finally show ?thesis .
qed
@@ -891,11 +891,11 @@
fix l assume "a dvd l" and "lcm b c dvd l"
have "b dvd lcm b c" by simp
- from this and `lcm b c dvd l` have "b dvd l" by (rule dvd_trans)
+ from this and \<open>lcm b c dvd l\<close> have "b dvd l" by (rule dvd_trans)
have "c dvd lcm b c" by simp
- from this and `lcm b c dvd l` have "c dvd l" by (rule dvd_trans)
- from `a dvd l` and `b dvd l` have "lcm a b dvd l" by (rule lcm_least)
- from this and `c dvd l` show "lcm (lcm a b) c dvd l" by (rule lcm_least)
+ from this and \<open>lcm b c dvd l\<close> have "c dvd l" by (rule dvd_trans)
+ from \<open>a dvd l\<close> and \<open>b dvd l\<close> have "lcm a b dvd l" by (rule lcm_least)
+ from this and \<open>c dvd l\<close> show "lcm (lcm a b) c dvd l" by (rule lcm_least)
qed (simp add: lcm_zero)
next
fix a b
@@ -926,7 +926,7 @@
hence "is_unit (lcm a b)" by (rule lcm_least)
hence "lcm a b = normalization_factor (lcm a b)"
by (subst normalization_factor_unit, simp_all)
- also have "\<dots> = 1" using `is_unit a \<and> is_unit b`
+ also have "\<dots> = 1" using \<open>is_unit a \<and> is_unit b\<close>
by auto
finally show "lcm a b = 1" .
qed
@@ -999,7 +999,7 @@
proof -
have "a dvd lcm a b" by (rule lcm_dvd1)
then obtain c where A: "lcm a b = a * c" unfolding dvd_def by blast
- with `a \<noteq> 0` and `b \<noteq> 0` have "c \<noteq> 0" by (auto simp: lcm_zero)
+ with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_zero)
then show ?thesis by (subst A, intro size_mult_mono)
qed
@@ -1013,12 +1013,12 @@
proof (rule ccontr)
from assms have "a \<noteq> 0" by auto
assume "\<not>euclidean_size a < euclidean_size (lcm a b)"
- with `a \<noteq> 0` and `b \<noteq> 0` have "euclidean_size (lcm a b) = euclidean_size a"
+ with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "euclidean_size (lcm a b) = euclidean_size a"
by (intro le_antisym, simp, intro euclidean_size_lcm_le1)
with assms have "lcm a b dvd a"
by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_zero)
hence "b dvd a" by (rule dvd_lcm_D2)
- with `\<not>b dvd a` show False by contradiction
+ with \<open>\<not>b dvd a\<close> show False by contradiction
qed
lemma euclidean_size_lcm_less2:
@@ -1101,8 +1101,8 @@
unfolding l_def by simp_all
{
fix l' assume "\<forall>a\<in>A. a dvd l'"
- with `\<forall>a\<in>A. a dvd l` have "\<forall>a\<in>A. a dvd gcd l l'" by (auto intro: gcd_greatest)
- moreover from `l \<noteq> 0` have "gcd l l' \<noteq> 0" by simp
+ with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd l l'" by (auto intro: gcd_greatest)
+ moreover from \<open>l \<noteq> 0\<close> have "gcd l l' \<noteq> 0" by simp
ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> euclidean_size b = euclidean_size (gcd l l')"
by (intro exI[of _ "gcd l l'"], auto)
hence "euclidean_size (gcd l l') \<ge> n" by (subst n_def) (rule Least_le)
@@ -1110,20 +1110,20 @@
proof -
have "gcd l l' dvd l" by simp
then obtain a where "l = gcd l l' * a" unfolding dvd_def by blast
- with `l \<noteq> 0` have "a \<noteq> 0" by auto
+ with \<open>l \<noteq> 0\<close> have "a \<noteq> 0" by auto
hence "euclidean_size (gcd l l') \<le> euclidean_size (gcd l l' * a)"
by (rule size_mult_mono)
- also have "gcd l l' * a = l" using `l = gcd l l' * a` ..
- also note `euclidean_size l = n`
+ also have "gcd l l' * a = l" using \<open>l = gcd l l' * a\<close> ..
+ also note \<open>euclidean_size l = n\<close>
finally show "euclidean_size (gcd l l') \<le> n" .
qed
ultimately have "euclidean_size l = euclidean_size (gcd l l')"
- by (intro le_antisym, simp_all add: `euclidean_size l = n`)
- with `l \<noteq> 0` have "l dvd gcd l l'" by (blast intro: dvd_euclidean_size_eq_imp_dvd)
+ by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
+ with \<open>l \<noteq> 0\<close> have "l dvd gcd l l'" by (blast intro: dvd_euclidean_size_eq_imp_dvd)
hence "l dvd l'" by (blast dest: dvd_gcd_D2)
}
- with `(\<forall>a\<in>A. a dvd l)` and normalization_factor_is_unit[OF `l \<noteq> 0`] and `l \<noteq> 0`
+ with \<open>(\<forall>a\<in>A. a dvd l)\<close> and normalization_factor_is_unit[OF \<open>l \<noteq> 0\<close>] and \<open>l \<noteq> 0\<close>
have "(\<forall>a\<in>A. a dvd l div normalization_factor l) \<and>
(\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> l div normalization_factor l dvd l') \<and>
normalization_factor (l div normalization_factor l) =
@@ -1206,7 +1206,7 @@
hence "l div normalization_factor l \<noteq> 0" by simp
also from ex have "l div normalization_factor l = Lcm A"
by (simp only: Lcm_Lcm_eucl Lcm_eucl_def n_def l_def if_True Let_def)
- finally show False using `Lcm A = 0` by contradiction
+ finally show False using \<open>Lcm A = 0\<close> by contradiction
qed
qed (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
@@ -1218,13 +1218,13 @@
moreover {
assume "0 \<notin> A"
hence "\<Prod>A \<noteq> 0"
- apply (induct rule: finite_induct[OF `finite A`])
+ apply (induct rule: finite_induct[OF \<open>finite A\<close>])
apply simp
apply (subst setprod.insert, assumption, assumption)
apply (rule no_zero_divisors)
apply blast+
done
- moreover from `finite A` have "\<forall>a\<in>A. a dvd \<Prod>A" by blast
+ moreover from \<open>finite A\<close> have "\<forall>a\<in>A. a dvd \<Prod>A" by blast
ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)" by blast
with Lcm0_iff' have "Lcm A \<noteq> 0" by simp
}
@@ -1244,13 +1244,13 @@
proof (rule lcmI)
fix l assume "a dvd l" and "Lcm A dvd l"
hence "\<forall>a\<in>A. a dvd l" by (blast intro: dvd_trans dvd_Lcm)
- with `a dvd l` show "Lcm (insert a A) dvd l" by (force intro: Lcm_dvd)
+ with \<open>a dvd l\<close> show "Lcm (insert a A) dvd l" by (force intro: Lcm_dvd)
qed (auto intro: Lcm_dvd dvd_Lcm)
lemma Lcm_finite:
assumes "finite A"
shows "Lcm A = Finite_Set.fold lcm 1 A"
- by (induct rule: finite.induct[OF `finite A`])
+ by (induct rule: finite.induct[OF \<open>finite A\<close>])
(simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
lemma Lcm_set [code_unfold]:
@@ -1337,13 +1337,13 @@
proof (rule gcdI)
fix l assume "l dvd a" and "l dvd Gcd A"
hence "\<forall>a\<in>A. l dvd a" by (blast intro: dvd_trans Gcd_dvd)
- with `l dvd a` show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd)
+ with \<open>l dvd a\<close> show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd)
qed auto
lemma Gcd_finite:
assumes "finite A"
shows "Gcd A = Finite_Set.fold gcd 0 A"
- by (induct rule: finite.induct[OF `finite A`])
+ by (induct rule: finite.induct[OF \<open>finite A\<close>])
(simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
lemma Gcd_set [code_unfold]:
@@ -1361,10 +1361,10 @@
end
-text {*
+text \<open>
A Euclidean ring is a Euclidean semiring with additive inverses. It provides a
few more lemmas; in particular, Bezout's lemma holds for any Euclidean ring.
-*}
+\<close>
class euclidean_ring = euclidean_semiring + idom
--- a/src/HOL/Number_Theory/Fib.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Fib.thy Fri Jun 19 21:41:33 2015 +0200
@@ -8,14 +8,14 @@
Jeremy Avigad.
*)
-section {* Fib *}
+section \<open>Fib\<close>
theory Fib
imports Main "../GCD" "../Binomial"
begin
-subsection {* Fibonacci numbers *}
+subsection \<open>Fibonacci numbers\<close>
fun fib :: "nat \<Rightarrow> nat"
where
@@ -23,7 +23,7 @@
| fib1: "fib (Suc 0) = 1"
| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
-subsection {* Basic Properties *}
+subsection \<open>Basic Properties\<close>
lemma fib_1 [simp]: "fib (1::nat) = 1"
by (metis One_nat_def fib1)
@@ -41,12 +41,12 @@
lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
by (induct n rule: fib.induct) (auto simp add: )
-subsection {* A Few Elementary Results *}
+subsection \<open>A Few Elementary Results\<close>
-text {*
+text \<open>
\medskip Concrete Mathematics, page 278: Cassini's identity. The proof is
much easier using integers, not natural numbers!
-*}
+\<close>
lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
by (induction n rule: fib.induct) (auto simp add: field_simps power2_eq_square power_add)
@@ -57,7 +57,7 @@
using fib_Cassini_int [of n] by auto
-subsection {* Law 6.111 of Concrete Mathematics *}
+subsection \<open>Law 6.111 of Concrete Mathematics\<close>
lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
apply (induct n rule: fib.induct)
@@ -86,13 +86,13 @@
case True
then have "m \<le> n" by auto
with pos_m have pos_n: "0 < n" by auto
- with pos_m `m < n` have diff: "n - m < n" by auto
+ with pos_m \<open>m < n\<close> have diff: "n - m < n" by auto
have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
- by (simp add: mod_if [of n]) (insert `m < n`, auto)
+ by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto)
also have "\<dots> = gcd (fib m) (fib (n - m))"
by (simp add: less.hyps diff pos_m)
also have "\<dots> = gcd (fib m) (fib n)"
- by (simp add: gcd_fib_diff `m \<le> n`)
+ by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
next
case False
@@ -102,14 +102,14 @@
qed
lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
- -- {* Law 6.111 *}
+ -- \<open>Law 6.111\<close>
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod)
theorem fib_mult_eq_setsum_nat:
"fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
by (induct n rule: nat.induct) (auto simp add: field_simps)
-subsection {* Fibonacci and Binomial Coefficients *}
+subsection \<open>Fibonacci and Binomial Coefficients\<close>
lemma setsum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
by (induct n) auto
--- a/src/HOL/Number_Theory/Gauss.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy Fri Jun 19 21:41:33 2015 +0200
@@ -3,7 +3,7 @@
Ported by lcp but unfinished
*)
-section {* Gauss' Lemma *}
+section \<open>Gauss' Lemma\<close>
theory Gauss
imports Residues
@@ -38,7 +38,7 @@
definition "F = (\<lambda>x. (int p - x)) ` E"
-subsection {* Basic properties of p *}
+subsection \<open>Basic properties of p\<close>
lemma odd_p: "odd p"
by (metis p_prime p_ge_2 prime_odd_nat)
@@ -60,7 +60,7 @@
by (auto simp add: even_iff_mod_2_eq_zero) (metis p_eq2)
-subsection {* Basic Properties of the Gauss Sets *}
+subsection \<open>Basic Properties of the Gauss Sets\<close>
lemma finite_A: "finite (A)"
by (auto simp add: A_def)
@@ -208,7 +208,7 @@
by (metis id_def all_A_relprime setprod_coprime_int)
-subsection {* Relationships Between Gauss Sets *}
+subsection \<open>Relationships Between Gauss Sets\<close>
lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> (inj_on (\<lambda>b. b mod m) X)"
by (auto simp add: ResSet_def inj_on_def cong_int_def)
@@ -315,7 +315,7 @@
qed
-subsection {* Gauss' Lemma *}
+subsection \<open>Gauss' Lemma\<close>
lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Fri Jun 19 21:41:33 2015 +0200
@@ -291,7 +291,7 @@
proof -
have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
by (simp add: ring_simprules)
- also from `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
+ also from \<open>x \<otimes> x = \<one>\<close> have "\<dots> = \<zero>"
by (simp add: ring_simprules)
finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
--- a/src/HOL/Number_Theory/Number_Theory.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Number_Theory.thy Fri Jun 19 21:41:33 2015 +0200
@@ -1,5 +1,5 @@
-section {* Comprehensive number theory *}
+section \<open>Comprehensive number theory\<close>
theory Number_Theory
imports Fib Residues Eratosthenes
--- a/src/HOL/Number_Theory/Pocklington.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy Fri Jun 19 21:41:33 2015 +0200
@@ -2,13 +2,13 @@
Author: Amine Chaieb
*)
-section {* Pocklington's Theorem for Primes *}
+section \<open>Pocklington's Theorem for Primes\<close>
theory Pocklington
imports Residues
begin
-subsection{*Lemmas about previously defined terms*}
+subsection\<open>Lemmas about previously defined terms\<close>
lemma prime:
"prime p \<longleftrightarrow> p \<noteq> 0 \<and> p\<noteq>1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
@@ -52,7 +52,7 @@
qed
-subsection{*Some basic theorems about solving congruences*}
+subsection\<open>Some basic theorems about solving congruences\<close>
lemma cong_solve:
fixes n::nat assumes an: "coprime a n" shows "\<exists>x. [a * x = b] (mod n)"
@@ -135,7 +135,7 @@
qed
-subsection{*Lucas's theorem*}
+subsection\<open>Lucas's theorem\<close>
lemma phi_limit_strong: "phi(n) \<le> n - 1"
proof -
@@ -291,7 +291,7 @@
qed
-subsection{*Definition of the order of a number mod n (0 in non-coprime case)*}
+subsection\<open>Definition of the order of a number mod n (0 in non-coprime case)\<close>
definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)"
@@ -442,7 +442,7 @@
ultimately show ?thesis by blast
qed
-subsection{*Another trivial primality characterization*}
+subsection\<open>Another trivial primality characterization\<close>
lemma prime_prime_factor:
"prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"
@@ -530,7 +530,7 @@
qed
-subsection{*Pocklington theorem*}
+subsection\<open>Pocklington theorem\<close>
lemma pocklington_lemma:
assumes n: "n \<ge> 2" and nqr: "n - 1 = q*r" and an: "[a^ (n - 1) = 1] (mod n)"
@@ -666,7 +666,7 @@
qed
-subsection{*Prime factorizations*}
+subsection\<open>Prime factorizations\<close>
(* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
--- a/src/HOL/Number_Theory/Primes.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Primes.thy Fri Jun 19 21:41:33 2015 +0200
@@ -25,7 +25,7 @@
*)
-section {* Primes *}
+section \<open>Primes\<close>
theory Primes
imports "~~/src/HOL/GCD" "~~/src/HOL/Binomial"
@@ -40,7 +40,7 @@
lemmas prime_nat_def = prime_def
-subsection {* Primes *}
+subsection \<open>Primes\<close>
lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
@@ -126,7 +126,7 @@
by (cases n) (auto elim: prime_dvd_power_int)
-subsubsection {* Make prime naively executable *}
+subsubsection \<open>Make prime naively executable\<close>
lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
by (simp add: prime_nat_def)
@@ -152,7 +152,7 @@
lemma two_is_prime_nat [simp]: "prime (2::nat)"
by simp
-text{* A bit of regression testing: *}
+text\<open>A bit of regression testing:\<close>
lemma "prime(97::nat)" by simp
lemma "prime(997::nat)" by eval
@@ -181,7 +181,7 @@
nat_dvd_not_less neq0_conv prime_nat_def)
done
-text {* One property of coprimality is easier to prove via prime factors. *}
+text \<open>One property of coprimality is easier to prove via prime factors.\<close>
lemma prime_divprod_pow_nat:
assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
@@ -222,7 +222,7 @@
qed
-subsection {* Infinitely many primes *}
+subsection \<open>Infinitely many primes\<close>
lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
proof-
@@ -231,18 +231,18 @@
obtain p where "prime p" and "p dvd fact n + 1" by auto
then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
{ assume "p \<le> n"
- from `prime p` have "p \<ge> 1"
+ from \<open>prime p\<close> have "p \<ge> 1"
by (cases p, simp_all)
- with `p <= n` have "p dvd fact n"
+ with \<open>p <= n\<close> have "p dvd fact n"
by (intro dvd_fact)
- with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
+ with \<open>p dvd fact n + 1\<close> have "p dvd fact n + 1 - fact n"
by (rule dvd_diff_nat)
then have "p dvd 1" by simp
then have "p <= 1" by auto
- moreover from `prime p` have "p > 1" by auto
+ moreover from \<open>prime p\<close> have "p > 1" by auto
ultimately have False by auto}
then have "n < p" by presburger
- with `prime p` and `p <= fact n + 1` show ?thesis by auto
+ with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
qed
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
@@ -259,9 +259,9 @@
by auto
qed
-subsection{*Powers of Primes*}
+subsection\<open>Powers of Primes\<close>
-text{*Versions for type nat only*}
+text\<open>Versions for type nat only\<close>
lemma prime_product:
fixes p::nat
@@ -271,7 +271,7 @@
from assms have
"1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
unfolding prime_nat_def by auto
- from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
+ from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
have "p dvd p * q" by simp
then have "p = 1 \<or> p = p * q" by (rule P)
@@ -370,7 +370,7 @@
thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
qed
-subsection {*Chinese Remainder Theorem Variants*}
+subsection \<open>Chinese Remainder Theorem Variants\<close>
lemma bezout_gcd_nat:
fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
@@ -391,7 +391,7 @@
qed
-text {* A binary form of the Chinese Remainder Theorem. *}
+text \<open>A binary form of the Chinese Remainder Theorem.\<close>
lemma chinese_remainder:
fixes a::nat assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
@@ -411,7 +411,7 @@
thus ?thesis by blast
qed
-text {* Primality *}
+text \<open>Primality\<close>
lemma coprime_bezout_strong:
fixes a::nat assumes "coprime a b" "b \<noteq> 1"
--- a/src/HOL/Number_Theory/Residues.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/Residues.thy Fri Jun 19 21:41:33 2015 +0200
@@ -5,7 +5,7 @@
Euler's theorem and Wilson's theorem.
*)
-section {* Residue rings *}
+section \<open>Residue rings\<close>
theory Residues
imports UniqueFactorization MiscAlgebra
@@ -248,7 +248,7 @@
*)
-subsection{* Euler's theorem *}
+subsection\<open>Euler's theorem\<close>
(* the definition of the phi function *)
@@ -276,9 +276,9 @@
apply (rule cop)
using * apply auto
done
- with `x dvd p` `1 < x` have "False" by auto }
+ with \<open>x dvd p\<close> \<open>1 < x\<close> have "False" by auto }
then show ?thesis
- using `2 \<le> p`
+ using \<open>2 \<le> p\<close>
by (simp add: prime_def)
(metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
not_numeral_le_zero one_dvd)
@@ -374,7 +374,7 @@
by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
-subsection {* Wilson's theorem *}
+subsection \<open>Wilson's theorem\<close>
lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
{x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Fri Jun 19 21:33:03 2015 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Fri Jun 19 21:41:33 2015 +0200
@@ -8,7 +8,7 @@
that, by Jeremy Avigad and David Gray.
*)
-section {* UniqueFactorization *}
+section \<open>UniqueFactorization\<close>
theory UniqueFactorization
imports Cong "~~/src/HOL/Library/Multiset"
@@ -34,7 +34,7 @@
*)
-subsection {* unique factorization: multiset version *}
+subsection \<open>unique factorization: multiset version\<close>
lemma multiset_prime_factorization_exists [rule_format]: "n > 0 -->
(EX M. (ALL (p::nat) : set_mset M. prime p) & n = (PROD i :# M. i))"
@@ -154,7 +154,7 @@
done
-subsection {* Prime factors and multiplicity for nats and ints *}
+subsection \<open>Prime factors and multiplicity for nats and ints\<close>
class unique_factorization =
fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
@@ -191,7 +191,7 @@
end
-subsection {* Set up transfer *}
+subsection \<open>Set up transfer\<close>
lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n"
unfolding prime_factors_int_def
@@ -228,7 +228,7 @@
transfer_int_nat_multiplicity]
-subsection {* Properties of prime factors and multiplicity for nats and ints *}
+subsection \<open>Properties of prime factors and multiplicity for nats and ints\<close>
lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
unfolding prime_factors_int_def by auto
@@ -308,7 +308,7 @@
using assms
apply (simp add: set_mset_def msetprod_multiplicity)
done
- with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
+ with \<open>f \<in> multiset\<close> have "count (multiset_prime_factorization n) = f"
by simp
with S_eq show ?thesis
by (simp add: set_mset_def multiset_def prime_factors_nat_def multiplicity_nat_def)
@@ -710,7 +710,7 @@
done
-subsection {* An application *}
+subsection \<open>An application\<close>
lemma gcd_eq_nat:
assumes pos [arith]: "x > 0" "y > 0"