src/HOL/GCD.thy
 changeset 60758 d8d85a8172b5 parent 60690 a9e45c9588c3 child 61169 4de9ff3ea29a
```     1.1 --- a/src/HOL/GCD.thy	Sat Jul 18 21:44:18 2015 +0200
1.2 +++ b/src/HOL/GCD.thy	Sat Jul 18 22:58:50 2015 +0200
1.3 @@ -25,13 +25,13 @@
1.4  *)
1.5
1.6
1.7 -section {* Greatest common divisor and least common multiple *}
1.8 +section \<open>Greatest common divisor and least common multiple\<close>
1.9
1.10  theory GCD
1.11  imports Main
1.12  begin
1.13
1.14 -subsection {* GCD and LCM definitions *}
1.15 +subsection \<open>GCD and LCM definitions\<close>
1.16
1.17  class gcd = zero + one + dvd +
1.18    fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.19 @@ -592,7 +592,7 @@
1.20  end
1.21
1.22
1.23 -subsection {* Transfer setup *}
1.24 +subsection \<open>Transfer setup\<close>
1.25
1.26  lemma transfer_nat_int_gcd:
1.27    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
1.28 @@ -622,7 +622,7 @@
1.29      transfer_int_nat_gcd transfer_int_nat_gcd_closures]
1.30
1.31
1.32 -subsection {* GCD properties *}
1.33 +subsection \<open>GCD properties\<close>
1.34
1.35  (* was gcd_induct *)
1.36  lemma gcd_nat_induct:
1.37 @@ -744,10 +744,10 @@
1.38
1.39  declare gcd_nat.simps [simp del]
1.40
1.41 -text {*
1.42 +text \<open>
1.43    \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
1.44    conjunctions don't seem provable separately.
1.45 -*}
1.46 +\<close>
1.47
1.48  instance nat :: semiring_gcd
1.49  proof
1.50 @@ -868,12 +868,12 @@
1.51  lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
1.52    by (metis gcd_proj1_if_dvd_int gcd_commute_int)
1.53
1.54 -text {*
1.55 +text \<open>
1.56    \medskip Multiplication laws
1.57 -*}
1.58 +\<close>
1.59
1.60  lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
1.61 -    -- {* @{cite \<open>page 27\<close> davenport92} *}
1.62 +    -- \<open>@{cite \<open>page 27\<close> davenport92}\<close>
1.63    apply (induct m n rule: gcd_nat_induct)
1.64    apply simp
1.65    apply (case_tac "k = 0")
1.66 @@ -944,16 +944,16 @@
1.67    assume ?rhs then show ?lhs by simp
1.68  next
1.69    assume ?lhs
1.70 -  from `?lhs` have "a dvd b * d" by (auto intro: dvdI dest: sym)
1.71 -  with `coprime a d` have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat)
1.72 -  from `?lhs` have "b dvd a * c" by (auto intro: dvdI dest: sym)
1.73 -  with `coprime b c` have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat)
1.74 -  from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult.commute)
1.75 -  with `coprime b c` have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
1.76 -  from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult.commute)
1.77 -  with `coprime a d` have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
1.78 -  from `a dvd b` `b dvd a` have "a = b" by (rule Nat.dvd.antisym)
1.79 -  moreover from `c dvd d` `d dvd c` have "c = d" by (rule Nat.dvd.antisym)
1.80 +  from \<open>?lhs\<close> have "a dvd b * d" by (auto intro: dvdI dest: sym)
1.81 +  with \<open>coprime a d\<close> have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat)
1.82 +  from \<open>?lhs\<close> have "b dvd a * c" by (auto intro: dvdI dest: sym)
1.83 +  with \<open>coprime b c\<close> have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat)
1.84 +  from \<open>?lhs\<close> have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult.commute)
1.85 +  with \<open>coprime b c\<close> have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
1.86 +  from \<open>?lhs\<close> have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult.commute)
1.87 +  with \<open>coprime a d\<close> have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
1.88 +  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "a = b" by (rule Nat.dvd.antisym)
1.89 +  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "c = d" by (rule Nat.dvd.antisym)
1.90    ultimately show ?rhs ..
1.91  qed
1.92
1.93 @@ -963,7 +963,7 @@
1.94    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>"
1.95    using assms by (intro coprime_crossproduct_nat [transferred]) auto
1.96
1.97 -text {* \medskip Addition laws *}
1.99
1.100  lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
1.101    apply (case_tac "n = 0")
1.102 @@ -1085,7 +1085,7 @@
1.103    by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
1.104
1.105
1.106 -subsection {* Coprimality *}
1.107 +subsection \<open>Coprimality\<close>
1.108
1.109  context semiring_gcd
1.110  begin
1.111 @@ -1504,7 +1504,7 @@
1.112  by (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
1.113
1.114
1.115 -subsection {* Bezout's theorem *}
1.116 +subsection \<open>Bezout's theorem\<close>
1.117
1.118  (* Function bezw returns a pair of witnesses to Bezout's theorem --
1.119     see the theorems that follow the definition. *)
1.120 @@ -1592,7 +1592,7 @@
1.121    ultimately show ?thesis by blast
1.122  qed
1.123
1.124 -text {* versions of Bezout for nat, by Amine Chaieb *}
1.125 +text \<open>versions of Bezout for nat, by Amine Chaieb\<close>
1.126
1.127  lemma ind_euclid:
1.128    assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
1.129 @@ -1744,7 +1744,7 @@
1.130  qed
1.131
1.132
1.133 -subsection {* LCM properties *}
1.134 +subsection \<open>LCM properties\<close>
1.135
1.136  lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
1.137    by (simp add: lcm_int_def lcm_nat_def zdiv_int
1.138 @@ -1906,7 +1906,7 @@
1.139  by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
1.140
1.141
1.142 -subsection {* The complete divisibility lattice *}
1.143 +subsection \<open>The complete divisibility lattice\<close>
1.144
1.145  interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
1.146    by standard simp_all
1.147 @@ -1916,9 +1916,9 @@
1.148
1.149  interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
1.150
1.151 -text{* Lifting gcd and lcm to sets (Gcd/Lcm).
1.152 +text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
1.153  Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
1.154 -*}
1.155 +\<close>
1.156
1.157  instantiation nat :: Gcd
1.158  begin
1.159 @@ -2034,7 +2034,7 @@
1.161  qed
1.162
1.163 -text{* Alternative characterizations of Gcd: *}
1.164 +text\<open>Alternative characterizations of Gcd:\<close>
1.165
1.166  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})"
1.167  apply(rule antisym)
1.168 @@ -2097,7 +2097,7 @@
1.169               dvd.neq_le_trans dvd_triv_right mult.commute)
1.170  done
1.171
1.172 -text{* Nitpick: *}
1.173 +text\<open>Nitpick:\<close>
1.174
1.175  lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
1.176  by (induct x y rule: nat_gcd.induct)
1.177 @@ -2107,7 +2107,7 @@
1.178  by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
1.179
1.180
1.181 -subsubsection {* Setwise gcd and lcm for integers *}
1.182 +subsubsection \<open>Setwise gcd and lcm for integers\<close>
1.183
1.184  instantiation int :: Gcd
1.185  begin
```