src/HOL/Old_Number_Theory/Legacy_GCD.thy
 changeset 61382 efac889fccbc parent 58889 5b7a9633cfa8 child 61762 d50b993b4fb9
```     1.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sat Oct 10 16:21:34 2015 +0200
1.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Sat Oct 10 16:26:23 2015 +0200
1.3 @@ -3,40 +3,40 @@
1.4      Copyright   1996  University of Cambridge
1.5  *)
1.6
1.7 -section {* The Greatest Common Divisor *}
1.8 +section \<open>The Greatest Common Divisor\<close>
1.9
1.10  theory Legacy_GCD
1.11  imports Main
1.12  begin
1.13
1.14 -text {*
1.15 +text \<open>
1.16    See @{cite davenport92}. \bigskip
1.17 -*}
1.18 +\<close>
1.19
1.20 -subsection {* Specification of GCD on nats *}
1.21 +subsection \<open>Specification of GCD on nats\<close>
1.22
1.23  definition
1.24 -  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
1.25 +  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- \<open>@{term gcd} as a relation\<close>
1.26    "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
1.27      (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
1.28
1.29 -text {* Uniqueness *}
1.30 +text \<open>Uniqueness\<close>
1.31
1.32  lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
1.33    by (simp add: is_gcd_def) (blast intro: dvd_antisym)
1.34
1.35 -text {* Connection to divides relation *}
1.36 +text \<open>Connection to divides relation\<close>
1.37
1.38  lemma is_gcd_dvd: "is_gcd a b m \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
1.39    by (auto simp add: is_gcd_def)
1.40
1.41 -text {* Commutativity *}
1.42 +text \<open>Commutativity\<close>
1.43
1.44  lemma is_gcd_commute: "is_gcd m n k = is_gcd n m k"
1.45    by (auto simp add: is_gcd_def)
1.46
1.47
1.48 -subsection {* GCD on nat by Euclid's algorithm *}
1.49 +subsection \<open>GCD on nat by Euclid's algorithm\<close>
1.50
1.51  fun gcd :: "nat => nat => nat"
1.52    where "gcd m n = (if n = 0 then m else gcd n (m mod n))"
1.53 @@ -68,10 +68,10 @@
1.54
1.55  declare gcd.simps [simp del]
1.56
1.57 -text {*
1.58 +text \<open>
1.59    \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
1.60    conjunctions don't seem provable separately.
1.61 -*}
1.62 +\<close>
1.63
1.64  lemma gcd_dvd1 [iff, algebra]: "gcd m n dvd m"
1.65    and gcd_dvd2 [iff, algebra]: "gcd m n dvd n"
1.66 @@ -80,24 +80,24 @@
1.67    apply (blast dest: dvd_mod_imp_dvd)
1.68    done
1.69
1.70 -text {*
1.71 +text \<open>
1.72    \medskip Maximality: for all @{term m}, @{term n}, @{term k}
1.73    naturals, if @{term k} divides @{term m} and @{term k} divides
1.74    @{term n} then @{term k} divides @{term "gcd m n"}.
1.75 -*}
1.76 +\<close>
1.77
1.78  lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
1.79    by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
1.80
1.81 -text {*
1.82 +text \<open>
1.83    \medskip Function gcd yields the Greatest Common Divisor.
1.84 -*}
1.85 +\<close>
1.86
1.87  lemma is_gcd: "is_gcd m n (gcd m n) "
1.88    by (simp add: is_gcd_def gcd_greatest)
1.89
1.90
1.91 -subsection {* Derived laws for GCD *}
1.92 +subsection \<open>Derived laws for GCD\<close>
1.93
1.94  lemma gcd_greatest_iff [iff, algebra]: "k dvd gcd m n \<longleftrightarrow> k dvd m \<and> k dvd n"
1.95    by (blast intro!: gcd_greatest intro: dvd_trans)
1.96 @@ -125,12 +125,12 @@
1.97  lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
1.98    unfolding One_nat_def by (rule gcd_1_left)
1.99
1.100 -text {*
1.101 +text \<open>
1.102    \medskip Multiplication laws
1.103 -*}
1.104 +\<close>
1.105
1.106  lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
1.107 -    -- {* @{cite \<open>page 27\<close> davenport92} *}
1.108 +    -- \<open>@{cite \<open>page 27\<close> davenport92}\<close>
1.109    apply (induct m n rule: gcd_induct)
1.110     apply simp
1.111    apply (case_tac "k = 0")
1.112 @@ -165,7 +165,7 @@
1.113    done
1.114
1.115
1.116 -text {* \medskip Addition laws *}
1.118
1.119  lemma gcd_add1 [simp, algebra]: "gcd (m + n) n = gcd m n"
1.120    by (cases "n = 0") (auto simp add: gcd_non_0)
1.121 @@ -190,9 +190,9 @@
1.122  lemma gcd_dvd_prod: "gcd m n dvd m * n"
1.123    using mult_dvd_mono [of 1] by auto
1.124
1.125 -text {*
1.126 +text \<open>
1.127    \medskip Division by gcd yields rrelatively primes.
1.128 -*}
1.129 +\<close>
1.130
1.131  lemma div_gcd_relprime:
1.132    assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
1.133 @@ -313,7 +313,7 @@
1.134  done
1.135
1.136
1.137 -text {* We can get a stronger version with a nonzeroness assumption. *}
1.138 +text \<open>We can get a stronger version with a nonzeroness assumption.\<close>
1.139  lemma divides_le: "m dvd n ==> m <= n \<or> n = (0::nat)" by (auto simp add: dvd_def)
1.140
1.141  lemma bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
1.142 @@ -449,7 +449,7 @@
1.143  qed
1.144
1.145
1.146 -subsection {* LCM defined by GCD *}
1.147 +subsection \<open>LCM defined by GCD\<close>
1.148
1.149
1.150  definition
1.151 @@ -562,7 +562,7 @@
1.152    done
1.153
1.154
1.155 -subsection {* GCD and LCM on integers *}
1.156 +subsection \<open>GCD and LCM on integers\<close>
1.157
1.158  definition
1.159    zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
1.160 @@ -595,7 +595,7 @@
1.161  proof -
1.162    assume "int (gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>)) = 1" "i dvd k * j"
1.163    then have g: "gcd (nat \<bar>i\<bar>) (nat \<bar>j\<bar>) = 1" by simp
1.164 -  from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
1.165 +  from \<open>i dvd k * j\<close> obtain h where h: "k*j = i*h" unfolding dvd_def by blast
1.166    have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
1.167      unfolding dvd_def
1.168      by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric])
1.169 @@ -620,7 +620,7 @@
1.170    let ?k' = "nat \<bar>k\<bar>"
1.171    let ?m' = "nat \<bar>m\<bar>"
1.172    let ?n' = "nat \<bar>n\<bar>"
1.173 -  from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
1.174 +  from \<open>k dvd m\<close> and \<open>k dvd n\<close> have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
1.175      unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
1.176    from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
1.177      unfolding zgcd_def by (simp only: zdvd_int)
1.178 @@ -696,7 +696,7 @@
1.179    done
1.180
1.181  lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
1.182 -  -- {* addition is an AC-operator *}
1.183 +  -- \<open>addition is an AC-operator\<close>
1.184
1.185  lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
1.186    by (simp del: minus_mult_right [symmetric]
1.187 @@ -728,7 +728,7 @@
1.188  lemma dvd_imp_dvd_zlcm1:
1.189    assumes "k dvd i" shows "k dvd (zlcm i j)"
1.190  proof -
1.191 -  have "nat(abs k) dvd nat(abs i)" using `k dvd i`
1.192 +  have "nat(abs k) dvd nat(abs i)" using \<open>k dvd i\<close>