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.98 +text \<open>\medskip Addition laws\<close>
    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.160        simp add: unit_factor_Gcd uf)
   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