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.117 +text \<open>\medskip Addition laws\<close>
   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>
   1.193      by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
   1.194    thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
   1.195  qed
   1.196 @@ -736,7 +736,7 @@
   1.197  lemma dvd_imp_dvd_zlcm2:
   1.198    assumes "k dvd j" shows "k dvd (zlcm i j)"
   1.199  proof -
   1.200 -  have "nat(abs k) dvd nat(abs j)" using `k dvd j`
   1.201 +  have "nat(abs k) dvd nat(abs j)" using \<open>k dvd j\<close>
   1.202      by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
   1.203    thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
   1.204  qed