--- a/src/HOL/GCD.thy Sat Jul 18 21:44:18 2015 +0200
+++ b/src/HOL/GCD.thy Sat Jul 18 22:58:50 2015 +0200
@@ -25,13 +25,13 @@
*)
-section {* Greatest common divisor and least common multiple *}
+section \<open>Greatest common divisor and least common multiple\<close>
theory GCD
imports Main
begin
-subsection {* GCD and LCM definitions *}
+subsection \<open>GCD and LCM definitions\<close>
class gcd = zero + one + dvd +
fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
@@ -592,7 +592,7 @@
end
-subsection {* Transfer setup *}
+subsection \<open>Transfer setup\<close>
lemma transfer_nat_int_gcd:
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
@@ -622,7 +622,7 @@
transfer_int_nat_gcd transfer_int_nat_gcd_closures]
-subsection {* GCD properties *}
+subsection \<open>GCD properties\<close>
(* was gcd_induct *)
lemma gcd_nat_induct:
@@ -744,10 +744,10 @@
declare gcd_nat.simps [simp del]
-text {*
+text \<open>
\medskip @{term "gcd m n"} divides @{text m} and @{text n}. The
conjunctions don't seem provable separately.
-*}
+\<close>
instance nat :: semiring_gcd
proof
@@ -868,12 +868,12 @@
lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
by (metis gcd_proj1_if_dvd_int gcd_commute_int)
-text {*
+text \<open>
\medskip Multiplication laws
-*}
+\<close>
lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
- -- {* @{cite \<open>page 27\<close> davenport92} *}
+ -- \<open>@{cite \<open>page 27\<close> davenport92}\<close>
apply (induct m n rule: gcd_nat_induct)
apply simp
apply (case_tac "k = 0")
@@ -944,16 +944,16 @@
assume ?rhs then show ?lhs by simp
next
assume ?lhs
- from `?lhs` have "a dvd b * d" by (auto intro: dvdI dest: sym)
- with `coprime a d` have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat)
- from `?lhs` have "b dvd a * c" by (auto intro: dvdI dest: sym)
- with `coprime b c` have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat)
- from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult.commute)
- with `coprime b c` have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
- from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult.commute)
- with `coprime a d` have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
- from `a dvd b` `b dvd a` have "a = b" by (rule Nat.dvd.antisym)
- moreover from `c dvd d` `d dvd c` have "c = d" by (rule Nat.dvd.antisym)
+ from \<open>?lhs\<close> have "a dvd b * d" by (auto intro: dvdI dest: sym)
+ with \<open>coprime a d\<close> have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat)
+ from \<open>?lhs\<close> have "b dvd a * c" by (auto intro: dvdI dest: sym)
+ with \<open>coprime b c\<close> have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat)
+ from \<open>?lhs\<close> have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult.commute)
+ with \<open>coprime b c\<close> have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
+ from \<open>?lhs\<close> have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult.commute)
+ with \<open>coprime a d\<close> have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
+ from \<open>a dvd b\<close> \<open>b dvd a\<close> have "a = b" by (rule Nat.dvd.antisym)
+ moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "c = d" by (rule Nat.dvd.antisym)
ultimately show ?rhs ..
qed
@@ -963,7 +963,7 @@
shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"
using assms by (intro coprime_crossproduct_nat [transferred]) auto
-text {* \medskip Addition laws *}
+text \<open>\medskip Addition laws\<close>
lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
apply (case_tac "n = 0")
@@ -1085,7 +1085,7 @@
by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
-subsection {* Coprimality *}
+subsection \<open>Coprimality\<close>
context semiring_gcd
begin
@@ -1504,7 +1504,7 @@
by (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
-subsection {* Bezout's theorem *}
+subsection \<open>Bezout's theorem\<close>
(* Function bezw returns a pair of witnesses to Bezout's theorem --
see the theorems that follow the definition. *)
@@ -1592,7 +1592,7 @@
ultimately show ?thesis by blast
qed
-text {* versions of Bezout for nat, by Amine Chaieb *}
+text \<open>versions of Bezout for nat, by Amine Chaieb\<close>
lemma ind_euclid:
assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
@@ -1744,7 +1744,7 @@
qed
-subsection {* LCM properties *}
+subsection \<open>LCM properties\<close>
lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
by (simp add: lcm_int_def lcm_nat_def zdiv_int
@@ -1906,7 +1906,7 @@
by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
-subsection {* The complete divisibility lattice *}
+subsection \<open>The complete divisibility lattice\<close>
interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
by standard simp_all
@@ -1916,9 +1916,9 @@
interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
-text{* Lifting gcd and lcm to sets (Gcd/Lcm).
+text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
-*}
+\<close>
instantiation nat :: Gcd
begin
@@ -2034,7 +2034,7 @@
simp add: unit_factor_Gcd uf)
qed
-text{* Alternative characterizations of Gcd: *}
+text\<open>Alternative characterizations of Gcd:\<close>
lemma Gcd_eq_Max: "finite(M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> Gcd M = Max(\<Inter>m\<in>M. {d. d dvd m})"
apply(rule antisym)
@@ -2097,7 +2097,7 @@
dvd.neq_le_trans dvd_triv_right mult.commute)
done
-text{* Nitpick: *}
+text\<open>Nitpick:\<close>
lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
by (induct x y rule: nat_gcd.induct)
@@ -2107,7 +2107,7 @@
by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
-subsubsection {* Setwise gcd and lcm for integers *}
+subsubsection \<open>Setwise gcd and lcm for integers\<close>
instantiation int :: Gcd
begin