src/HOL/GCD.thy
changeset 31952 40501bb2d57c
parent 31814 7c122634da81
child 31992 f8aed98faae7
child 32036 8a9228872fbd
     1.1 --- a/src/HOL/GCD.thy	Tue Jul 07 07:56:24 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Tue Jul 07 17:39:51 2009 +0200
     1.3 @@ -163,7 +163,7 @@
     1.4  subsection {* GCD *}
     1.5  
     1.6  (* was gcd_induct *)
     1.7 -lemma nat_gcd_induct:
     1.8 +lemma gcd_nat_induct:
     1.9    fixes m n :: nat
    1.10    assumes "\<And>m. P m 0"
    1.11      and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
    1.12 @@ -175,43 +175,43 @@
    1.13  
    1.14  (* specific to int *)
    1.15  
    1.16 -lemma int_gcd_neg1 [simp]: "gcd (-x::int) y = gcd x y"
    1.17 +lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
    1.18    by (simp add: gcd_int_def)
    1.19  
    1.20 -lemma int_gcd_neg2 [simp]: "gcd (x::int) (-y) = gcd x y"
    1.21 +lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
    1.22    by (simp add: gcd_int_def)
    1.23  
    1.24  lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
    1.25  by(simp add: gcd_int_def)
    1.26  
    1.27 -lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)"
    1.28 +lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)"
    1.29  by (simp add: gcd_int_def)
    1.30  
    1.31  lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
    1.32 -by (metis abs_idempotent int_gcd_abs)
    1.33 +by (metis abs_idempotent gcd_abs_int)
    1.34  
    1.35  lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
    1.36 -by (metis abs_idempotent int_gcd_abs)
    1.37 +by (metis abs_idempotent gcd_abs_int)
    1.38  
    1.39 -lemma int_gcd_cases:
    1.40 +lemma gcd_cases_int:
    1.41    fixes x :: int and y
    1.42    assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
    1.43        and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
    1.44        and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
    1.45        and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
    1.46    shows "P (gcd x y)"
    1.47 -by (insert prems, auto simp add: int_gcd_neg1 int_gcd_neg2, arith)
    1.48 +by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith)
    1.49  
    1.50 -lemma int_gcd_ge_0 [simp]: "gcd (x::int) y >= 0"
    1.51 +lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
    1.52    by (simp add: gcd_int_def)
    1.53  
    1.54 -lemma int_lcm_neg1: "lcm (-x::int) y = lcm x y"
    1.55 +lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
    1.56    by (simp add: lcm_int_def)
    1.57  
    1.58 -lemma int_lcm_neg2: "lcm (x::int) (-y) = lcm x y"
    1.59 +lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
    1.60    by (simp add: lcm_int_def)
    1.61  
    1.62 -lemma int_lcm_abs: "lcm (x::int) y = lcm (abs x) (abs y)"
    1.63 +lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)"
    1.64    by (simp add: lcm_int_def)
    1.65  
    1.66  lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
    1.67 @@ -223,53 +223,53 @@
    1.68  lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
    1.69  by (metis abs_idempotent lcm_int_def)
    1.70  
    1.71 -lemma int_lcm_cases:
    1.72 +lemma lcm_cases_int:
    1.73    fixes x :: int and y
    1.74    assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
    1.75        and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
    1.76        and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
    1.77        and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
    1.78    shows "P (lcm x y)"
    1.79 -by (insert prems, auto simp add: int_lcm_neg1 int_lcm_neg2, arith)
    1.80 +by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith)
    1.81  
    1.82 -lemma int_lcm_ge_0 [simp]: "lcm (x::int) y >= 0"
    1.83 +lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
    1.84    by (simp add: lcm_int_def)
    1.85  
    1.86  (* was gcd_0, etc. *)
    1.87 -lemma nat_gcd_0 [simp]: "gcd (x::nat) 0 = x"
    1.88 +lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"
    1.89    by simp
    1.90  
    1.91  (* was igcd_0, etc. *)
    1.92 -lemma int_gcd_0 [simp]: "gcd (x::int) 0 = abs x"
    1.93 +lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
    1.94    by (unfold gcd_int_def, auto)
    1.95  
    1.96 -lemma nat_gcd_0_left [simp]: "gcd 0 (x::nat) = x"
    1.97 +lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"
    1.98    by simp
    1.99  
   1.100 -lemma int_gcd_0_left [simp]: "gcd 0 (x::int) = abs x"
   1.101 +lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
   1.102    by (unfold gcd_int_def, auto)
   1.103  
   1.104 -lemma nat_gcd_red: "gcd (x::nat) y = gcd y (x mod y)"
   1.105 +lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
   1.106    by (case_tac "y = 0", auto)
   1.107  
   1.108  (* weaker, but useful for the simplifier *)
   1.109  
   1.110 -lemma nat_gcd_non_0: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   1.111 +lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   1.112    by simp
   1.113  
   1.114 -lemma nat_gcd_1 [simp]: "gcd (m::nat) 1 = 1"
   1.115 +lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
   1.116    by simp
   1.117  
   1.118 -lemma nat_gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   1.119 +lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   1.120    by (simp add: One_nat_def)
   1.121  
   1.122 -lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1"
   1.123 +lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
   1.124    by (simp add: gcd_int_def)
   1.125  
   1.126 -lemma nat_gcd_idem: "gcd (x::nat) x = x"
   1.127 +lemma gcd_idem_nat: "gcd (x::nat) x = x"
   1.128  by simp
   1.129  
   1.130 -lemma int_gcd_idem: "gcd (x::int) x = abs x"
   1.131 +lemma gcd_idem_int: "gcd (x::int) x = abs x"
   1.132  by (auto simp add: gcd_int_def)
   1.133  
   1.134  declare gcd_nat.simps [simp del]
   1.135 @@ -279,260 +279,260 @@
   1.136    conjunctions don't seem provable separately.
   1.137  *}
   1.138  
   1.139 -lemma nat_gcd_dvd1 [iff]: "(gcd (m::nat)) n dvd m"
   1.140 -  and nat_gcd_dvd2 [iff]: "(gcd m n) dvd n"
   1.141 -  apply (induct m n rule: nat_gcd_induct)
   1.142 -  apply (simp_all add: nat_gcd_non_0)
   1.143 +lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
   1.144 +  and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
   1.145 +  apply (induct m n rule: gcd_nat_induct)
   1.146 +  apply (simp_all add: gcd_non_0_nat)
   1.147    apply (blast dest: dvd_mod_imp_dvd)
   1.148  done
   1.149  
   1.150 -lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x"
   1.151 -by (metis gcd_int_def int_dvd_iff nat_gcd_dvd1)
   1.152 +lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x"
   1.153 +by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat)
   1.154  
   1.155 -lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y"
   1.156 -by (metis gcd_int_def int_dvd_iff nat_gcd_dvd2)
   1.157 +lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y"
   1.158 +by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat)
   1.159  
   1.160  lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   1.161 -by(metis nat_gcd_dvd1 dvd_trans)
   1.162 +by(metis gcd_dvd1_nat dvd_trans)
   1.163  
   1.164  lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   1.165 -by(metis nat_gcd_dvd2 dvd_trans)
   1.166 +by(metis gcd_dvd2_nat dvd_trans)
   1.167  
   1.168  lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   1.169 -by(metis int_gcd_dvd1 dvd_trans)
   1.170 +by(metis gcd_dvd1_int dvd_trans)
   1.171  
   1.172  lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   1.173 -by(metis int_gcd_dvd2 dvd_trans)
   1.174 +by(metis gcd_dvd2_int dvd_trans)
   1.175  
   1.176 -lemma nat_gcd_le1 [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   1.177 +lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   1.178    by (rule dvd_imp_le, auto)
   1.179  
   1.180 -lemma nat_gcd_le2 [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   1.181 +lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   1.182    by (rule dvd_imp_le, auto)
   1.183  
   1.184 -lemma int_gcd_le1 [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   1.185 +lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   1.186    by (rule zdvd_imp_le, auto)
   1.187  
   1.188 -lemma int_gcd_le2 [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   1.189 +lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   1.190    by (rule zdvd_imp_le, auto)
   1.191  
   1.192 -lemma nat_gcd_greatest: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   1.193 -by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
   1.194 +lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   1.195 +by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)
   1.196  
   1.197 -lemma int_gcd_greatest:
   1.198 +lemma gcd_greatest_int:
   1.199    "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   1.200 -  apply (subst int_gcd_abs)
   1.201 +  apply (subst gcd_abs_int)
   1.202    apply (subst abs_dvd_iff [symmetric])
   1.203 -  apply (rule nat_gcd_greatest [transferred])
   1.204 +  apply (rule gcd_greatest_nat [transferred])
   1.205    apply auto
   1.206  done
   1.207  
   1.208 -lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) =
   1.209 +lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =
   1.210      (k dvd m & k dvd n)"
   1.211 -  by (blast intro!: nat_gcd_greatest intro: dvd_trans)
   1.212 +  by (blast intro!: gcd_greatest_nat intro: dvd_trans)
   1.213  
   1.214 -lemma int_gcd_greatest_iff: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   1.215 -  by (blast intro!: int_gcd_greatest intro: dvd_trans)
   1.216 +lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   1.217 +  by (blast intro!: gcd_greatest_int intro: dvd_trans)
   1.218  
   1.219 -lemma nat_gcd_zero [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   1.220 -  by (simp only: dvd_0_left_iff [symmetric] nat_gcd_greatest_iff)
   1.221 +lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   1.222 +  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)
   1.223  
   1.224 -lemma int_gcd_zero [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   1.225 +lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   1.226    by (auto simp add: gcd_int_def)
   1.227  
   1.228 -lemma nat_gcd_pos [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   1.229 -  by (insert nat_gcd_zero [of m n], arith)
   1.230 +lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   1.231 +  by (insert gcd_zero_nat [of m n], arith)
   1.232  
   1.233 -lemma int_gcd_pos [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   1.234 -  by (insert int_gcd_zero [of m n], insert int_gcd_ge_0 [of m n], arith)
   1.235 +lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   1.236 +  by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
   1.237  
   1.238 -lemma nat_gcd_commute: "gcd (m::nat) n = gcd n m"
   1.239 +lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
   1.240    by (rule dvd_anti_sym, auto)
   1.241  
   1.242 -lemma int_gcd_commute: "gcd (m::int) n = gcd n m"
   1.243 -  by (auto simp add: gcd_int_def nat_gcd_commute)
   1.244 +lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
   1.245 +  by (auto simp add: gcd_int_def gcd_commute_nat)
   1.246  
   1.247 -lemma nat_gcd_assoc: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
   1.248 +lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
   1.249    apply (rule dvd_anti_sym)
   1.250    apply (blast intro: dvd_trans)+
   1.251  done
   1.252  
   1.253 -lemma int_gcd_assoc: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
   1.254 -  by (auto simp add: gcd_int_def nat_gcd_assoc)
   1.255 +lemma gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
   1.256 +  by (auto simp add: gcd_int_def gcd_assoc_nat)
   1.257  
   1.258 -lemmas nat_gcd_left_commute =
   1.259 -  mk_left_commute[of gcd, OF nat_gcd_assoc nat_gcd_commute]
   1.260 +lemmas gcd_left_commute_nat =
   1.261 +  mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat]
   1.262  
   1.263 -lemmas int_gcd_left_commute =
   1.264 -  mk_left_commute[of gcd, OF int_gcd_assoc int_gcd_commute]
   1.265 +lemmas gcd_left_commute_int =
   1.266 +  mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int]
   1.267  
   1.268 -lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute
   1.269 +lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
   1.270    -- {* gcd is an AC-operator *}
   1.271  
   1.272 -lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute
   1.273 +lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
   1.274  
   1.275 -lemma nat_gcd_unique: "(d::nat) dvd a \<and> d dvd b \<and>
   1.276 +lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
   1.277      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   1.278    apply auto
   1.279    apply (rule dvd_anti_sym)
   1.280 -  apply (erule (1) nat_gcd_greatest)
   1.281 +  apply (erule (1) gcd_greatest_nat)
   1.282    apply auto
   1.283  done
   1.284  
   1.285 -lemma int_gcd_unique: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   1.286 +lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   1.287      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   1.288    apply (case_tac "d = 0")
   1.289    apply force
   1.290    apply (rule iffI)
   1.291    apply (rule zdvd_anti_sym)
   1.292    apply arith
   1.293 -  apply (subst int_gcd_pos)
   1.294 +  apply (subst gcd_pos_int)
   1.295    apply clarsimp
   1.296    apply (drule_tac x = "d + 1" in spec)
   1.297    apply (frule zdvd_imp_le)
   1.298 -  apply (auto intro: int_gcd_greatest)
   1.299 +  apply (auto intro: gcd_greatest_int)
   1.300  done
   1.301  
   1.302  lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
   1.303 -by (metis dvd.eq_iff nat_gcd_unique)
   1.304 +by (metis dvd.eq_iff gcd_unique_nat)
   1.305  
   1.306  lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   1.307 -by (metis dvd.eq_iff nat_gcd_unique)
   1.308 +by (metis dvd.eq_iff gcd_unique_nat)
   1.309  
   1.310  lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
   1.311 -by (metis abs_dvd_iff abs_eq_0 int_gcd_0_left int_gcd_abs int_gcd_unique)
   1.312 +by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int)
   1.313  
   1.314  lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
   1.315 -by (metis gcd_proj1_if_dvd_int int_gcd_commute)
   1.316 +by (metis gcd_proj1_if_dvd_int gcd_commute_int)
   1.317  
   1.318  
   1.319  text {*
   1.320    \medskip Multiplication laws
   1.321  *}
   1.322  
   1.323 -lemma nat_gcd_mult_distrib: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   1.324 +lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   1.325      -- {* \cite[page 27]{davenport92} *}
   1.326 -  apply (induct m n rule: nat_gcd_induct)
   1.327 +  apply (induct m n rule: gcd_nat_induct)
   1.328    apply simp
   1.329    apply (case_tac "k = 0")
   1.330 -  apply (simp_all add: mod_geq nat_gcd_non_0 mod_mult_distrib2)
   1.331 +  apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2)
   1.332  done
   1.333  
   1.334 -lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   1.335 -  apply (subst (1 2) int_gcd_abs)
   1.336 +lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   1.337 +  apply (subst (1 2) gcd_abs_int)
   1.338    apply (subst (1 2) abs_mult)
   1.339 -  apply (rule nat_gcd_mult_distrib [transferred])
   1.340 +  apply (rule gcd_mult_distrib_nat [transferred])
   1.341    apply auto
   1.342  done
   1.343  
   1.344 -lemma nat_coprime_dvd_mult: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   1.345 -  apply (insert nat_gcd_mult_distrib [of m k n])
   1.346 +lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   1.347 +  apply (insert gcd_mult_distrib_nat [of m k n])
   1.348    apply simp
   1.349    apply (erule_tac t = m in ssubst)
   1.350    apply simp
   1.351    done
   1.352  
   1.353 -lemma int_coprime_dvd_mult:
   1.354 +lemma coprime_dvd_mult_int:
   1.355    "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
   1.356  apply (subst abs_dvd_iff [symmetric])
   1.357  apply (subst dvd_abs_iff [symmetric])
   1.358 -apply (subst (asm) int_gcd_abs)
   1.359 -apply (rule nat_coprime_dvd_mult [transferred])
   1.360 +apply (subst (asm) gcd_abs_int)
   1.361 +apply (rule coprime_dvd_mult_nat [transferred])
   1.362      prefer 4 apply assumption
   1.363     apply auto
   1.364  apply (subst abs_mult [symmetric], auto)
   1.365  done
   1.366  
   1.367 -lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \<Longrightarrow>
   1.368 +lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   1.369      (k dvd m * n) = (k dvd m)"
   1.370 -  by (auto intro: nat_coprime_dvd_mult)
   1.371 +  by (auto intro: coprime_dvd_mult_nat)
   1.372  
   1.373 -lemma int_coprime_dvd_mult_iff: "coprime (k::int) n \<Longrightarrow>
   1.374 +lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
   1.375      (k dvd m * n) = (k dvd m)"
   1.376 -  by (auto intro: int_coprime_dvd_mult)
   1.377 +  by (auto intro: coprime_dvd_mult_int)
   1.378  
   1.379 -lemma nat_gcd_mult_cancel: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   1.380 +lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
   1.381    apply (rule dvd_anti_sym)
   1.382 -  apply (rule nat_gcd_greatest)
   1.383 -  apply (rule_tac n = k in nat_coprime_dvd_mult)
   1.384 -  apply (simp add: nat_gcd_assoc)
   1.385 -  apply (simp add: nat_gcd_commute)
   1.386 +  apply (rule gcd_greatest_nat)
   1.387 +  apply (rule_tac n = k in coprime_dvd_mult_nat)
   1.388 +  apply (simp add: gcd_assoc_nat)
   1.389 +  apply (simp add: gcd_commute_nat)
   1.390    apply (simp_all add: mult_commute)
   1.391  done
   1.392  
   1.393 -lemma int_gcd_mult_cancel:
   1.394 +lemma gcd_mult_cancel_int:
   1.395    "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
   1.396 -apply (subst (1 2) int_gcd_abs)
   1.397 +apply (subst (1 2) gcd_abs_int)
   1.398  apply (subst abs_mult)
   1.399 -apply (rule nat_gcd_mult_cancel [transferred], auto)
   1.400 +apply (rule gcd_mult_cancel_nat [transferred], auto)
   1.401  done
   1.402  
   1.403  text {* \medskip Addition laws *}
   1.404  
   1.405 -lemma nat_gcd_add1 [simp]: "gcd ((m::nat) + n) n = gcd m n"
   1.406 +lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   1.407    apply (case_tac "n = 0")
   1.408 -  apply (simp_all add: nat_gcd_non_0)
   1.409 +  apply (simp_all add: gcd_non_0_nat)
   1.410  done
   1.411  
   1.412 -lemma nat_gcd_add2 [simp]: "gcd (m::nat) (m + n) = gcd m n"
   1.413 -  apply (subst (1 2) nat_gcd_commute)
   1.414 +lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   1.415 +  apply (subst (1 2) gcd_commute_nat)
   1.416    apply (subst add_commute)
   1.417    apply simp
   1.418  done
   1.419  
   1.420  (* to do: add the other variations? *)
   1.421  
   1.422 -lemma nat_gcd_diff1: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   1.423 -  by (subst nat_gcd_add1 [symmetric], auto)
   1.424 +lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   1.425 +  by (subst gcd_add1_nat [symmetric], auto)
   1.426  
   1.427 -lemma nat_gcd_diff2: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   1.428 -  apply (subst nat_gcd_commute)
   1.429 -  apply (subst nat_gcd_diff1 [symmetric])
   1.430 +lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   1.431 +  apply (subst gcd_commute_nat)
   1.432 +  apply (subst gcd_diff1_nat [symmetric])
   1.433    apply auto
   1.434 -  apply (subst nat_gcd_commute)
   1.435 -  apply (subst nat_gcd_diff1)
   1.436 +  apply (subst gcd_commute_nat)
   1.437 +  apply (subst gcd_diff1_nat)
   1.438    apply assumption
   1.439 -  apply (rule nat_gcd_commute)
   1.440 +  apply (rule gcd_commute_nat)
   1.441  done
   1.442  
   1.443 -lemma int_gcd_non_0: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   1.444 +lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   1.445    apply (frule_tac b = y and a = x in pos_mod_sign)
   1.446    apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
   1.447 -  apply (auto simp add: nat_gcd_non_0 nat_mod_distrib [symmetric]
   1.448 +  apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
   1.449      zmod_zminus1_eq_if)
   1.450    apply (frule_tac a = x in pos_mod_bound)
   1.451 -  apply (subst (1 2) nat_gcd_commute)
   1.452 -  apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2
   1.453 +  apply (subst (1 2) gcd_commute_nat)
   1.454 +  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
   1.455      nat_le_eq_zle)
   1.456  done
   1.457  
   1.458 -lemma int_gcd_red: "gcd (x::int) y = gcd y (x mod y)"
   1.459 +lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
   1.460    apply (case_tac "y = 0")
   1.461    apply force
   1.462    apply (case_tac "y > 0")
   1.463 -  apply (subst int_gcd_non_0, auto)
   1.464 -  apply (insert int_gcd_non_0 [of "-y" "-x"])
   1.465 -  apply (auto simp add: int_gcd_neg1 int_gcd_neg2)
   1.466 +  apply (subst gcd_non_0_int, auto)
   1.467 +  apply (insert gcd_non_0_int [of "-y" "-x"])
   1.468 +  apply (auto simp add: gcd_neg1_int gcd_neg2_int)
   1.469  done
   1.470  
   1.471 -lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n"
   1.472 -by (metis int_gcd_red mod_add_self1 zadd_commute)
   1.473 +lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
   1.474 +by (metis gcd_red_int mod_add_self1 zadd_commute)
   1.475  
   1.476 -lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n"
   1.477 -by (metis int_gcd_add1 int_gcd_commute zadd_commute)
   1.478 +lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
   1.479 +by (metis gcd_add1_int gcd_commute_int zadd_commute)
   1.480  
   1.481 -lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n"
   1.482 -by (metis mod_mult_self3 nat_gcd_commute nat_gcd_red)
   1.483 +lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
   1.484 +by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
   1.485  
   1.486 -lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n"
   1.487 -by (metis int_gcd_commute int_gcd_red mod_mult_self1 zadd_commute)
   1.488 +lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
   1.489 +by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute)
   1.490  
   1.491  
   1.492  (* to do: differences, and all variations of addition rules
   1.493      as simplification rules for nat and int *)
   1.494  
   1.495  (* FIXME remove iff *)
   1.496 -lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n"
   1.497 +lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n"
   1.498    using mult_dvd_mono [of 1] by auto
   1.499  
   1.500  (* to do: add the three variations of these, and for ints? *)
   1.501 @@ -559,7 +559,7 @@
   1.502  apply(rule Max_eqI[THEN sym])
   1.503    apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat)
   1.504   apply simp
   1.505 - apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le nat_gcd_greatest_iff nat_gcd_pos)
   1.506 + apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
   1.507  apply simp
   1.508  done
   1.509  
   1.510 @@ -568,14 +568,14 @@
   1.511  apply(rule Max_eqI[THEN sym])
   1.512    apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int)
   1.513   apply simp
   1.514 - apply (metis int_gcd_greatest_iff int_gcd_pos zdvd_imp_le)
   1.515 + apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
   1.516  apply simp
   1.517  done
   1.518  
   1.519  
   1.520  subsection {* Coprimality *}
   1.521  
   1.522 -lemma nat_div_gcd_coprime:
   1.523 +lemma div_gcd_coprime_nat:
   1.524    assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   1.525    shows "coprime (a div gcd a b) (b div gcd a b)"
   1.526  proof -
   1.527 @@ -593,34 +593,34 @@
   1.528    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   1.529      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   1.530        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   1.531 -  have "?g \<noteq> 0" using nz by (simp add: nat_gcd_zero)
   1.532 +  have "?g \<noteq> 0" using nz by (simp add: gcd_zero_nat)
   1.533    then have gp: "?g > 0" by arith
   1.534 -  from nat_gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.535 +  from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.536    with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   1.537  qed
   1.538  
   1.539 -lemma int_div_gcd_coprime:
   1.540 +lemma div_gcd_coprime_int:
   1.541    assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   1.542    shows "coprime (a div gcd a b) (b div gcd a b)"
   1.543 -apply (subst (1 2 3) int_gcd_abs)
   1.544 +apply (subst (1 2 3) gcd_abs_int)
   1.545  apply (subst (1 2) abs_div)
   1.546    apply simp
   1.547   apply simp
   1.548  apply(subst (1 2) abs_gcd_int)
   1.549 -apply (rule nat_div_gcd_coprime [transferred])
   1.550 -using nz apply (auto simp add: int_gcd_abs [symmetric])
   1.551 +apply (rule div_gcd_coprime_nat [transferred])
   1.552 +using nz apply (auto simp add: gcd_abs_int [symmetric])
   1.553  done
   1.554  
   1.555 -lemma nat_coprime: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   1.556 -  using nat_gcd_unique[of 1 a b, simplified] by auto
   1.557 +lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   1.558 +  using gcd_unique_nat[of 1 a b, simplified] by auto
   1.559  
   1.560 -lemma nat_coprime_Suc_0:
   1.561 +lemma coprime_Suc_0_nat:
   1.562      "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   1.563 -  using nat_coprime by (simp add: One_nat_def)
   1.564 +  using coprime_nat by (simp add: One_nat_def)
   1.565  
   1.566 -lemma int_coprime: "coprime (a::int) b \<longleftrightarrow>
   1.567 +lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
   1.568      (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   1.569 -  using int_gcd_unique [of 1 a b]
   1.570 +  using gcd_unique_int [of 1 a b]
   1.571    apply clarsimp
   1.572    apply (erule subst)
   1.573    apply (rule iffI)
   1.574 @@ -631,7 +631,7 @@
   1.575    apply force
   1.576  done
   1.577  
   1.578 -lemma nat_gcd_coprime:
   1.579 +lemma gcd_coprime_nat:
   1.580    assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
   1.581      b: "b = b' * gcd a b"
   1.582    shows    "coprime a' b'"
   1.583 @@ -640,7 +640,7 @@
   1.584    apply (erule ssubst)
   1.585    apply (subgoal_tac "b' = b div gcd a b")
   1.586    apply (erule ssubst)
   1.587 -  apply (rule nat_div_gcd_coprime)
   1.588 +  apply (rule div_gcd_coprime_nat)
   1.589    using prems
   1.590    apply force
   1.591    apply (subst (1) b)
   1.592 @@ -649,7 +649,7 @@
   1.593    using z apply force
   1.594  done
   1.595  
   1.596 -lemma int_gcd_coprime:
   1.597 +lemma gcd_coprime_int:
   1.598    assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
   1.599      b: "b = b' * gcd a b"
   1.600    shows    "coprime a' b'"
   1.601 @@ -658,7 +658,7 @@
   1.602    apply (erule ssubst)
   1.603    apply (subgoal_tac "b' = b div gcd a b")
   1.604    apply (erule ssubst)
   1.605 -  apply (rule int_div_gcd_coprime)
   1.606 +  apply (rule div_gcd_coprime_int)
   1.607    using prems
   1.608    apply force
   1.609    apply (subst (1) b)
   1.610 @@ -667,117 +667,117 @@
   1.611    using z apply force
   1.612  done
   1.613  
   1.614 -lemma nat_coprime_mult: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   1.615 +lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
   1.616      shows "coprime d (a * b)"
   1.617 -  apply (subst nat_gcd_commute)
   1.618 -  using da apply (subst nat_gcd_mult_cancel)
   1.619 -  apply (subst nat_gcd_commute, assumption)
   1.620 -  apply (subst nat_gcd_commute, rule db)
   1.621 +  apply (subst gcd_commute_nat)
   1.622 +  using da apply (subst gcd_mult_cancel_nat)
   1.623 +  apply (subst gcd_commute_nat, assumption)
   1.624 +  apply (subst gcd_commute_nat, rule db)
   1.625  done
   1.626  
   1.627 -lemma int_coprime_mult: assumes da: "coprime (d::int) a" and db: "coprime d b"
   1.628 +lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
   1.629      shows "coprime d (a * b)"
   1.630 -  apply (subst int_gcd_commute)
   1.631 -  using da apply (subst int_gcd_mult_cancel)
   1.632 -  apply (subst int_gcd_commute, assumption)
   1.633 -  apply (subst int_gcd_commute, rule db)
   1.634 +  apply (subst gcd_commute_int)
   1.635 +  using da apply (subst gcd_mult_cancel_int)
   1.636 +  apply (subst gcd_commute_int, assumption)
   1.637 +  apply (subst gcd_commute_int, rule db)
   1.638  done
   1.639  
   1.640 -lemma nat_coprime_lmult:
   1.641 +lemma coprime_lmult_nat:
   1.642    assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   1.643  proof -
   1.644    have "gcd d a dvd gcd d (a * b)"
   1.645 -    by (rule nat_gcd_greatest, auto)
   1.646 +    by (rule gcd_greatest_nat, auto)
   1.647    with dab show ?thesis
   1.648      by auto
   1.649  qed
   1.650  
   1.651 -lemma int_coprime_lmult:
   1.652 +lemma coprime_lmult_int:
   1.653    assumes "coprime (d::int) (a * b)" shows "coprime d a"
   1.654  proof -
   1.655    have "gcd d a dvd gcd d (a * b)"
   1.656 -    by (rule int_gcd_greatest, auto)
   1.657 +    by (rule gcd_greatest_int, auto)
   1.658    with assms show ?thesis
   1.659      by auto
   1.660  qed
   1.661  
   1.662 -lemma nat_coprime_rmult:
   1.663 +lemma coprime_rmult_nat:
   1.664    assumes "coprime (d::nat) (a * b)" shows "coprime d b"
   1.665  proof -
   1.666    have "gcd d b dvd gcd d (a * b)"
   1.667 -    by (rule nat_gcd_greatest, auto intro: dvd_mult)
   1.668 +    by (rule gcd_greatest_nat, auto intro: dvd_mult)
   1.669    with assms show ?thesis
   1.670      by auto
   1.671  qed
   1.672  
   1.673 -lemma int_coprime_rmult:
   1.674 +lemma coprime_rmult_int:
   1.675    assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   1.676  proof -
   1.677    have "gcd d b dvd gcd d (a * b)"
   1.678 -    by (rule int_gcd_greatest, auto intro: dvd_mult)
   1.679 +    by (rule gcd_greatest_int, auto intro: dvd_mult)
   1.680    with dab show ?thesis
   1.681      by auto
   1.682  qed
   1.683  
   1.684 -lemma nat_coprime_mul_eq: "coprime (d::nat) (a * b) \<longleftrightarrow>
   1.685 +lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
   1.686      coprime d a \<and>  coprime d b"
   1.687 -  using nat_coprime_rmult[of d a b] nat_coprime_lmult[of d a b]
   1.688 -    nat_coprime_mult[of d a b]
   1.689 +  using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
   1.690 +    coprime_mult_nat[of d a b]
   1.691    by blast
   1.692  
   1.693 -lemma int_coprime_mul_eq: "coprime (d::int) (a * b) \<longleftrightarrow>
   1.694 +lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
   1.695      coprime d a \<and>  coprime d b"
   1.696 -  using int_coprime_rmult[of d a b] int_coprime_lmult[of d a b]
   1.697 -    int_coprime_mult[of d a b]
   1.698 +  using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
   1.699 +    coprime_mult_int[of d a b]
   1.700    by blast
   1.701  
   1.702 -lemma nat_gcd_coprime_exists:
   1.703 +lemma gcd_coprime_exists_nat:
   1.704      assumes nz: "gcd (a::nat) b \<noteq> 0"
   1.705      shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   1.706    apply (rule_tac x = "a div gcd a b" in exI)
   1.707    apply (rule_tac x = "b div gcd a b" in exI)
   1.708 -  using nz apply (auto simp add: nat_div_gcd_coprime dvd_div_mult)
   1.709 +  using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult)
   1.710  done
   1.711  
   1.712 -lemma int_gcd_coprime_exists:
   1.713 +lemma gcd_coprime_exists_int:
   1.714      assumes nz: "gcd (a::int) b \<noteq> 0"
   1.715      shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   1.716    apply (rule_tac x = "a div gcd a b" in exI)
   1.717    apply (rule_tac x = "b div gcd a b" in exI)
   1.718 -  using nz apply (auto simp add: int_div_gcd_coprime dvd_div_mult_self)
   1.719 +  using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self)
   1.720  done
   1.721  
   1.722 -lemma nat_coprime_exp: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   1.723 -  by (induct n, simp_all add: nat_coprime_mult)
   1.724 +lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   1.725 +  by (induct n, simp_all add: coprime_mult_nat)
   1.726  
   1.727 -lemma int_coprime_exp: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   1.728 -  by (induct n, simp_all add: int_coprime_mult)
   1.729 +lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   1.730 +  by (induct n, simp_all add: coprime_mult_int)
   1.731  
   1.732 -lemma nat_coprime_exp2 [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   1.733 -  apply (rule nat_coprime_exp)
   1.734 -  apply (subst nat_gcd_commute)
   1.735 -  apply (rule nat_coprime_exp)
   1.736 -  apply (subst nat_gcd_commute, assumption)
   1.737 +lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   1.738 +  apply (rule coprime_exp_nat)
   1.739 +  apply (subst gcd_commute_nat)
   1.740 +  apply (rule coprime_exp_nat)
   1.741 +  apply (subst gcd_commute_nat, assumption)
   1.742  done
   1.743  
   1.744 -lemma int_coprime_exp2 [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   1.745 -  apply (rule int_coprime_exp)
   1.746 -  apply (subst int_gcd_commute)
   1.747 -  apply (rule int_coprime_exp)
   1.748 -  apply (subst int_gcd_commute, assumption)
   1.749 +lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   1.750 +  apply (rule coprime_exp_int)
   1.751 +  apply (subst gcd_commute_int)
   1.752 +  apply (rule coprime_exp_int)
   1.753 +  apply (subst gcd_commute_int, assumption)
   1.754  done
   1.755  
   1.756 -lemma nat_gcd_exp: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   1.757 +lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
   1.758  proof (cases)
   1.759    assume "a = 0 & b = 0"
   1.760    thus ?thesis by simp
   1.761    next assume "~(a = 0 & b = 0)"
   1.762    hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   1.763 -    by (auto simp:nat_div_gcd_coprime)
   1.764 +    by (auto simp:div_gcd_coprime_nat)
   1.765    hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   1.766        ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   1.767      apply (subst (1 2) mult_commute)
   1.768 -    apply (subst nat_gcd_mult_distrib [symmetric])
   1.769 +    apply (subst gcd_mult_distrib_nat [symmetric])
   1.770      apply simp
   1.771      done
   1.772    also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
   1.773 @@ -797,29 +797,29 @@
   1.774    finally show ?thesis .
   1.775  qed
   1.776  
   1.777 -lemma int_gcd_exp: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   1.778 -  apply (subst (1 2) int_gcd_abs)
   1.779 +lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
   1.780 +  apply (subst (1 2) gcd_abs_int)
   1.781    apply (subst (1 2) power_abs)
   1.782 -  apply (rule nat_gcd_exp [where n = n, transferred])
   1.783 +  apply (rule gcd_exp_nat [where n = n, transferred])
   1.784    apply auto
   1.785  done
   1.786  
   1.787 -lemma nat_coprime_divprod: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   1.788 -  using nat_coprime_dvd_mult_iff[of d a b]
   1.789 +lemma coprime_divprod_nat: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   1.790 +  using coprime_dvd_mult_iff_nat[of d a b]
   1.791    by (auto simp add: mult_commute)
   1.792  
   1.793 -lemma int_coprime_divprod: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   1.794 -  using int_coprime_dvd_mult_iff[of d a b]
   1.795 +lemma coprime_divprod_int: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
   1.796 +  using coprime_dvd_mult_iff_int[of d a b]
   1.797    by (auto simp add: mult_commute)
   1.798  
   1.799 -lemma nat_division_decomp: assumes dc: "(a::nat) dvd b * c"
   1.800 +lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
   1.801    shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   1.802  proof-
   1.803    let ?g = "gcd a b"
   1.804    {assume "?g = 0" with dc have ?thesis by auto}
   1.805    moreover
   1.806    {assume z: "?g \<noteq> 0"
   1.807 -    from nat_gcd_coprime_exists[OF z]
   1.808 +    from gcd_coprime_exists_nat[OF z]
   1.809      obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   1.810        by blast
   1.811      have thb: "?g dvd b" by auto
   1.812 @@ -828,21 +828,21 @@
   1.813      from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   1.814      hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   1.815      with z have th_1: "a' dvd b' * c" by auto
   1.816 -    from nat_coprime_dvd_mult[OF ab'(3)] th_1
   1.817 +    from coprime_dvd_mult_nat[OF ab'(3)] th_1
   1.818      have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   1.819      from ab' have "a = ?g*a'" by algebra
   1.820      with thb thc have ?thesis by blast }
   1.821    ultimately show ?thesis by blast
   1.822  qed
   1.823  
   1.824 -lemma int_division_decomp: assumes dc: "(a::int) dvd b * c"
   1.825 +lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"
   1.826    shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   1.827  proof-
   1.828    let ?g = "gcd a b"
   1.829    {assume "?g = 0" with dc have ?thesis by auto}
   1.830    moreover
   1.831    {assume z: "?g \<noteq> 0"
   1.832 -    from int_gcd_coprime_exists[OF z]
   1.833 +    from gcd_coprime_exists_int[OF z]
   1.834      obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   1.835        by blast
   1.836      have thb: "?g dvd b" by auto
   1.837 @@ -852,14 +852,14 @@
   1.838      from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   1.839      hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
   1.840      with z have th_1: "a' dvd b' * c" by auto
   1.841 -    from int_coprime_dvd_mult[OF ab'(3)] th_1
   1.842 +    from coprime_dvd_mult_int[OF ab'(3)] th_1
   1.843      have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
   1.844      from ab' have "a = ?g*a'" by algebra
   1.845      with thb thc have ?thesis by blast }
   1.846    ultimately show ?thesis by blast
   1.847  qed
   1.848  
   1.849 -lemma nat_pow_divides_pow:
   1.850 +lemma pow_divides_pow_nat:
   1.851    assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
   1.852    shows "a dvd b"
   1.853  proof-
   1.854 @@ -869,7 +869,7 @@
   1.855    moreover
   1.856    {assume z: "?g \<noteq> 0"
   1.857      hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   1.858 -    from nat_gcd_coprime_exists[OF z]
   1.859 +    from gcd_coprime_exists_nat[OF z]
   1.860      obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   1.861        by blast
   1.862      from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   1.863 @@ -880,14 +880,14 @@
   1.864      have "a' dvd a'^n" by (simp add: m)
   1.865      with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   1.866      hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   1.867 -    from nat_coprime_dvd_mult[OF nat_coprime_exp [OF ab'(3), of m]] th1
   1.868 +    from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
   1.869      have "a' dvd b'" by (subst (asm) mult_commute, blast)
   1.870      hence "a'*?g dvd b'*?g" by simp
   1.871      with ab'(1,2)  have ?thesis by simp }
   1.872    ultimately show ?thesis by blast
   1.873  qed
   1.874  
   1.875 -lemma int_pow_divides_pow:
   1.876 +lemma pow_divides_pow_int:
   1.877    assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
   1.878    shows "a dvd b"
   1.879  proof-
   1.880 @@ -897,7 +897,7 @@
   1.881    moreover
   1.882    {assume z: "?g \<noteq> 0"
   1.883      hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
   1.884 -    from int_gcd_coprime_exists[OF z]
   1.885 +    from gcd_coprime_exists_int[OF z]
   1.886      obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
   1.887        by blast
   1.888      from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   1.889 @@ -909,7 +909,7 @@
   1.890      with th0 have "a' dvd b'^n"
   1.891        using dvd_trans[of a' "a'^n" "b'^n"] by simp
   1.892      hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   1.893 -    from int_coprime_dvd_mult[OF int_coprime_exp [OF ab'(3), of m]] th1
   1.894 +    from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
   1.895      have "a' dvd b'" by (subst (asm) mult_commute, blast)
   1.896      hence "a'*?g dvd b'*?g" by simp
   1.897      with ab'(1,2)  have ?thesis by simp }
   1.898 @@ -917,76 +917,76 @@
   1.899  qed
   1.900  
   1.901  (* FIXME move to Divides(?) *)
   1.902 -lemma nat_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   1.903 -  by (auto intro: nat_pow_divides_pow dvd_power_same)
   1.904 +lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   1.905 +  by (auto intro: pow_divides_pow_nat dvd_power_same)
   1.906  
   1.907 -lemma int_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   1.908 -  by (auto intro: int_pow_divides_pow dvd_power_same)
   1.909 +lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   1.910 +  by (auto intro: pow_divides_pow_int dvd_power_same)
   1.911  
   1.912 -lemma nat_divides_mult:
   1.913 +lemma divides_mult_nat:
   1.914    assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   1.915    shows "m * n dvd r"
   1.916  proof-
   1.917    from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   1.918      unfolding dvd_def by blast
   1.919    from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   1.920 -  hence "m dvd n'" using nat_coprime_dvd_mult_iff[OF mn] by simp
   1.921 +  hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp
   1.922    then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   1.923    from n' k show ?thesis unfolding dvd_def by auto
   1.924  qed
   1.925  
   1.926 -lemma int_divides_mult:
   1.927 +lemma divides_mult_int:
   1.928    assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   1.929    shows "m * n dvd r"
   1.930  proof-
   1.931    from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   1.932      unfolding dvd_def by blast
   1.933    from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   1.934 -  hence "m dvd n'" using int_coprime_dvd_mult_iff[OF mn] by simp
   1.935 +  hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp
   1.936    then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   1.937    from n' k show ?thesis unfolding dvd_def by auto
   1.938  qed
   1.939  
   1.940 -lemma nat_coprime_plus_one [simp]: "coprime ((n::nat) + 1) n"
   1.941 +lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
   1.942    apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   1.943    apply force
   1.944 -  apply (rule nat_dvd_diff)
   1.945 +  apply (rule dvd_diff_nat)
   1.946    apply auto
   1.947  done
   1.948  
   1.949 -lemma nat_coprime_Suc [simp]: "coprime (Suc n) n"
   1.950 -  using nat_coprime_plus_one by (simp add: One_nat_def)
   1.951 +lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
   1.952 +  using coprime_plus_one_nat by (simp add: One_nat_def)
   1.953  
   1.954 -lemma int_coprime_plus_one [simp]: "coprime ((n::int) + 1) n"
   1.955 +lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
   1.956    apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
   1.957    apply force
   1.958    apply (rule dvd_diff)
   1.959    apply auto
   1.960  done
   1.961  
   1.962 -lemma nat_coprime_minus_one: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   1.963 -  using nat_coprime_plus_one [of "n - 1"]
   1.964 -    nat_gcd_commute [of "n - 1" n] by auto
   1.965 +lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   1.966 +  using coprime_plus_one_nat [of "n - 1"]
   1.967 +    gcd_commute_nat [of "n - 1" n] by auto
   1.968  
   1.969 -lemma int_coprime_minus_one: "coprime ((n::int) - 1) n"
   1.970 -  using int_coprime_plus_one [of "n - 1"]
   1.971 -    int_gcd_commute [of "n - 1" n] by auto
   1.972 +lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
   1.973 +  using coprime_plus_one_int [of "n - 1"]
   1.974 +    gcd_commute_int [of "n - 1" n] by auto
   1.975  
   1.976 -lemma nat_setprod_coprime [rule_format]:
   1.977 +lemma setprod_coprime_nat [rule_format]:
   1.978      "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
   1.979    apply (case_tac "finite A")
   1.980    apply (induct set: finite)
   1.981 -  apply (auto simp add: nat_gcd_mult_cancel)
   1.982 +  apply (auto simp add: gcd_mult_cancel_nat)
   1.983  done
   1.984  
   1.985 -lemma int_setprod_coprime [rule_format]:
   1.986 +lemma setprod_coprime_int [rule_format]:
   1.987      "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
   1.988    apply (case_tac "finite A")
   1.989    apply (induct set: finite)
   1.990 -  apply (auto simp add: int_gcd_mult_cancel)
   1.991 +  apply (auto simp add: gcd_mult_cancel_int)
   1.992  done
   1.993  
   1.994 -lemma nat_prime_odd: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   1.995 +lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   1.996    unfolding prime_nat_def
   1.997    apply (subst even_mult_two_ex)
   1.998    apply clarify
   1.999 @@ -994,41 +994,41 @@
  1.1000    apply auto
  1.1001  done
  1.1002  
  1.1003 -lemma int_prime_odd: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
  1.1004 +lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
  1.1005    unfolding prime_int_def
  1.1006 -  apply (frule nat_prime_odd)
  1.1007 +  apply (frule prime_odd_nat)
  1.1008    apply (auto simp add: even_nat_def)
  1.1009  done
  1.1010  
  1.1011 -lemma nat_coprime_common_divisor: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1.1012 +lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1.1013      x dvd b \<Longrightarrow> x = 1"
  1.1014    apply (subgoal_tac "x dvd gcd a b")
  1.1015    apply simp
  1.1016 -  apply (erule (1) nat_gcd_greatest)
  1.1017 +  apply (erule (1) gcd_greatest_nat)
  1.1018  done
  1.1019  
  1.1020 -lemma int_coprime_common_divisor: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1.1021 +lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
  1.1022      x dvd b \<Longrightarrow> abs x = 1"
  1.1023    apply (subgoal_tac "x dvd gcd a b")
  1.1024    apply simp
  1.1025 -  apply (erule (1) int_gcd_greatest)
  1.1026 +  apply (erule (1) gcd_greatest_int)
  1.1027  done
  1.1028  
  1.1029 -lemma nat_coprime_divisors: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
  1.1030 +lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
  1.1031      coprime d e"
  1.1032    apply (auto simp add: dvd_def)
  1.1033 -  apply (frule int_coprime_lmult)
  1.1034 -  apply (subst int_gcd_commute)
  1.1035 -  apply (subst (asm) (2) int_gcd_commute)
  1.1036 -  apply (erule int_coprime_lmult)
  1.1037 +  apply (frule coprime_lmult_int)
  1.1038 +  apply (subst gcd_commute_int)
  1.1039 +  apply (subst (asm) (2) gcd_commute_int)
  1.1040 +  apply (erule coprime_lmult_int)
  1.1041  done
  1.1042  
  1.1043 -lemma nat_invertible_coprime: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1.1044 -apply (metis nat_coprime_lmult nat_gcd_1 nat_gcd_commute nat_gcd_red)
  1.1045 +lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1.1046 +apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
  1.1047  done
  1.1048  
  1.1049 -lemma int_invertible_coprime: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1.1050 -apply (metis int_coprime_lmult int_gcd_1 int_gcd_commute int_gcd_red)
  1.1051 +lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1.1052 +apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
  1.1053  done
  1.1054  
  1.1055  
  1.1056 @@ -1054,7 +1054,7 @@
  1.1057  
  1.1058  lemma bezw_aux [rule_format]:
  1.1059      "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1.1060 -proof (induct x y rule: nat_gcd_induct)
  1.1061 +proof (induct x y rule: gcd_nat_induct)
  1.1062    fix m :: nat
  1.1063    show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1.1064      by auto
  1.1065 @@ -1064,7 +1064,7 @@
  1.1066          snd (bezw n (m mod n)) * int (m mod n) =
  1.1067          int (gcd n (m mod n))"
  1.1068      thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1.1069 -      apply (simp add: bezw_non_0 nat_gcd_non_0)
  1.1070 +      apply (simp add: bezw_non_0 gcd_non_0_nat)
  1.1071        apply (erule subst)
  1.1072        apply (simp add: ring_simps)
  1.1073        apply (subst mod_div_equality [of m n, symmetric])
  1.1074 @@ -1075,7 +1075,7 @@
  1.1075        done
  1.1076  qed
  1.1077  
  1.1078 -lemma int_bezout:
  1.1079 +lemma bezout_int:
  1.1080    fixes x y
  1.1081    shows "EX u v. u * (x::int) + v * y = gcd x y"
  1.1082  proof -
  1.1083 @@ -1098,7 +1098,7 @@
  1.1084      apply auto
  1.1085      apply (rule_tac x = u in exI)
  1.1086      apply (rule_tac x = "-v" in exI)
  1.1087 -    apply (subst int_gcd_neg2 [symmetric])
  1.1088 +    apply (subst gcd_neg2_int [symmetric])
  1.1089      apply auto
  1.1090      done
  1.1091    moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1.1092 @@ -1106,7 +1106,7 @@
  1.1093      apply auto
  1.1094      apply (rule_tac x = "-u" in exI)
  1.1095      apply (rule_tac x = v in exI)
  1.1096 -    apply (subst int_gcd_neg1 [symmetric])
  1.1097 +    apply (subst gcd_neg1_int [symmetric])
  1.1098      apply auto
  1.1099      done
  1.1100    moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1.1101 @@ -1114,8 +1114,8 @@
  1.1102      apply auto
  1.1103      apply (rule_tac x = "-u" in exI)
  1.1104      apply (rule_tac x = "-v" in exI)
  1.1105 -    apply (subst int_gcd_neg1 [symmetric])
  1.1106 -    apply (subst int_gcd_neg2 [symmetric])
  1.1107 +    apply (subst gcd_neg1_int [symmetric])
  1.1108 +    apply (subst gcd_neg2_int [symmetric])
  1.1109      apply auto
  1.1110      done
  1.1111    ultimately show ?thesis by blast
  1.1112 @@ -1160,7 +1160,7 @@
  1.1113  ultimately  show "P a b" by blast
  1.1114  qed
  1.1115  
  1.1116 -lemma nat_bezout_lemma:
  1.1117 +lemma bezout_lemma_nat:
  1.1118    assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1.1119      (a * x = b * y + d \<or> b * x = a * y + d)"
  1.1120    shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1.1121 @@ -1177,7 +1177,7 @@
  1.1122    apply algebra
  1.1123  done
  1.1124  
  1.1125 -lemma nat_bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1.1126 +lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1.1127      (a * x = b * y + d \<or> b * x = a * y + d)"
  1.1128    apply(induct a b rule: ind_euclid)
  1.1129    apply blast
  1.1130 @@ -1194,9 +1194,9 @@
  1.1131    apply algebra
  1.1132  done
  1.1133  
  1.1134 -lemma nat_bezout1: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1.1135 +lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1.1136      (a * x - b * y = d \<or> b * x - a * y = d)"
  1.1137 -  using nat_bezout_add[of a b]
  1.1138 +  using bezout_add_nat[of a b]
  1.1139    apply clarsimp
  1.1140    apply (rule_tac x="d" in exI, simp)
  1.1141    apply (rule_tac x="x" in exI)
  1.1142 @@ -1204,11 +1204,11 @@
  1.1143    apply auto
  1.1144  done
  1.1145  
  1.1146 -lemma nat_bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
  1.1147 +lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1.1148    shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1.1149  proof-
  1.1150   from nz have ap: "a > 0" by simp
  1.1151 - from nat_bezout_add[of a b]
  1.1152 + from bezout_add_nat[of a b]
  1.1153   have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1.1154     (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1.1155   moreover
  1.1156 @@ -1258,11 +1258,11 @@
  1.1157   ultimately show ?thesis by blast
  1.1158  qed
  1.1159  
  1.1160 -lemma nat_bezout: assumes a: "(a::nat) \<noteq> 0"
  1.1161 +lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1.1162    shows "\<exists>x y. a * x = b * y + gcd a b"
  1.1163  proof-
  1.1164    let ?g = "gcd a b"
  1.1165 -  from nat_bezout_add_strong[OF a, of b]
  1.1166 +  from bezout_add_strong_nat[OF a, of b]
  1.1167    obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1.1168    from d(1,2) have "d dvd ?g" by simp
  1.1169    then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1.1170 @@ -1274,99 +1274,99 @@
  1.1171  
  1.1172  subsection {* LCM *}
  1.1173  
  1.1174 -lemma int_lcm_altdef: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1.1175 +lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
  1.1176    by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1.1177      zmult_int [symmetric] gcd_int_def)
  1.1178  
  1.1179 -lemma nat_prod_gcd_lcm: "(m::nat) * n = gcd m n * lcm m n"
  1.1180 +lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1.1181    unfolding lcm_nat_def
  1.1182 -  by (simp add: dvd_mult_div_cancel [OF nat_gcd_dvd_prod])
  1.1183 +  by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1.1184  
  1.1185 -lemma int_prod_gcd_lcm: "abs(m::int) * abs n = gcd m n * lcm m n"
  1.1186 +lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
  1.1187    unfolding lcm_int_def gcd_int_def
  1.1188    apply (subst int_mult [symmetric])
  1.1189 -  apply (subst nat_prod_gcd_lcm [symmetric])
  1.1190 +  apply (subst prod_gcd_lcm_nat [symmetric])
  1.1191    apply (subst nat_abs_mult_distrib [symmetric])
  1.1192    apply (simp, simp add: abs_mult)
  1.1193  done
  1.1194  
  1.1195 -lemma nat_lcm_0 [simp]: "lcm (m::nat) 0 = 0"
  1.1196 +lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1.1197    unfolding lcm_nat_def by simp
  1.1198  
  1.1199 -lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0"
  1.1200 +lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1.1201    unfolding lcm_int_def by simp
  1.1202  
  1.1203 -lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0"
  1.1204 +lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1.1205    unfolding lcm_nat_def by simp
  1.1206  
  1.1207 -lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0"
  1.1208 +lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1.1209    unfolding lcm_int_def by simp
  1.1210  
  1.1211 -lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m"
  1.1212 -  unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps)
  1.1213 +lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m"
  1.1214 +  unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps)
  1.1215  
  1.1216 -lemma int_lcm_commute: "lcm (m::int) n = lcm n m"
  1.1217 -  unfolding lcm_int_def by (subst nat_lcm_commute, rule refl)
  1.1218 +lemma lcm_commute_int: "lcm (m::int) n = lcm n m"
  1.1219 +  unfolding lcm_int_def by (subst lcm_commute_nat, rule refl)
  1.1220  
  1.1221  
  1.1222 -lemma nat_lcm_pos:
  1.1223 +lemma lcm_pos_nat:
  1.1224    "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1.1225 -by (metis gr0I mult_is_0 nat_prod_gcd_lcm)
  1.1226 +by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1.1227  
  1.1228 -lemma int_lcm_pos:
  1.1229 +lemma lcm_pos_int:
  1.1230    "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1.1231 -  apply (subst int_lcm_abs)
  1.1232 -  apply (rule nat_lcm_pos [transferred])
  1.1233 +  apply (subst lcm_abs_int)
  1.1234 +  apply (rule lcm_pos_nat [transferred])
  1.1235    apply auto
  1.1236  done
  1.1237  
  1.1238 -lemma nat_dvd_pos:
  1.1239 +lemma dvd_pos_nat:
  1.1240    fixes n m :: nat
  1.1241    assumes "n > 0" and "m dvd n"
  1.1242    shows "m > 0"
  1.1243  using assms by (cases m) auto
  1.1244  
  1.1245 -lemma nat_lcm_least:
  1.1246 +lemma lcm_least_nat:
  1.1247    assumes "(m::nat) dvd k" and "n dvd k"
  1.1248    shows "lcm m n dvd k"
  1.1249  proof (cases k)
  1.1250    case 0 then show ?thesis by auto
  1.1251  next
  1.1252    case (Suc _) then have pos_k: "k > 0" by auto
  1.1253 -  from assms nat_dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1.1254 -  with nat_gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
  1.1255 +  from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
  1.1256 +  with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp
  1.1257    from assms obtain p where k_m: "k = m * p" using dvd_def by blast
  1.1258    from assms obtain q where k_n: "k = n * q" using dvd_def by blast
  1.1259    from pos_k k_m have pos_p: "p > 0" by auto
  1.1260    from pos_k k_n have pos_q: "q > 0" by auto
  1.1261    have "k * k * gcd q p = k * gcd (k * q) (k * p)"
  1.1262 -    by (simp add: mult_ac nat_gcd_mult_distrib)
  1.1263 +    by (simp add: mult_ac gcd_mult_distrib_nat)
  1.1264    also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
  1.1265      by (simp add: k_m [symmetric] k_n [symmetric])
  1.1266    also have "\<dots> = k * p * q * gcd m n"
  1.1267 -    by (simp add: mult_ac nat_gcd_mult_distrib)
  1.1268 +    by (simp add: mult_ac gcd_mult_distrib_nat)
  1.1269    finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
  1.1270      by (simp only: k_m [symmetric] k_n [symmetric])
  1.1271    then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
  1.1272      by (simp add: mult_ac)
  1.1273    with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
  1.1274      by simp
  1.1275 -  with nat_prod_gcd_lcm [of m n]
  1.1276 +  with prod_gcd_lcm_nat [of m n]
  1.1277    have "lcm m n * gcd q p * gcd m n = k * gcd m n"
  1.1278      by (simp add: mult_ac)
  1.1279    with pos_gcd have "lcm m n * gcd q p = k" by auto
  1.1280    then show ?thesis using dvd_def by auto
  1.1281  qed
  1.1282  
  1.1283 -lemma int_lcm_least:
  1.1284 +lemma lcm_least_int:
  1.1285    "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1.1286 -apply (subst int_lcm_abs)
  1.1287 +apply (subst lcm_abs_int)
  1.1288  apply (rule dvd_trans)
  1.1289 -apply (rule nat_lcm_least [transferred, of _ "abs k" _])
  1.1290 +apply (rule lcm_least_nat [transferred, of _ "abs k" _])
  1.1291  apply auto
  1.1292  done
  1.1293  
  1.1294 -lemma nat_lcm_dvd1: "(m::nat) dvd lcm m n"
  1.1295 +lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
  1.1296  proof (cases m)
  1.1297    case 0 then show ?thesis by simp
  1.1298  next
  1.1299 @@ -1382,82 +1382,82 @@
  1.1300      then obtain k where "n = gcd m n * k" using dvd_def by auto
  1.1301      then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
  1.1302        by (simp add: mult_ac)
  1.1303 -    also have "\<dots> = m * k" using mpos npos nat_gcd_zero by simp
  1.1304 +    also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
  1.1305      finally show ?thesis by (simp add: lcm_nat_def)
  1.1306    qed
  1.1307  qed
  1.1308  
  1.1309 -lemma int_lcm_dvd1: "(m::int) dvd lcm m n"
  1.1310 -  apply (subst int_lcm_abs)
  1.1311 +lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
  1.1312 +  apply (subst lcm_abs_int)
  1.1313    apply (rule dvd_trans)
  1.1314    prefer 2
  1.1315 -  apply (rule nat_lcm_dvd1 [transferred])
  1.1316 +  apply (rule lcm_dvd1_nat [transferred])
  1.1317    apply auto
  1.1318  done
  1.1319  
  1.1320 -lemma nat_lcm_dvd2: "(n::nat) dvd lcm m n"
  1.1321 -  by (subst nat_lcm_commute, rule nat_lcm_dvd1)
  1.1322 +lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
  1.1323 +  by (subst lcm_commute_nat, rule lcm_dvd1_nat)
  1.1324  
  1.1325 -lemma int_lcm_dvd2: "(n::int) dvd lcm m n"
  1.1326 -  by (subst int_lcm_commute, rule int_lcm_dvd1)
  1.1327 +lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
  1.1328 +  by (subst lcm_commute_int, rule lcm_dvd1_int)
  1.1329  
  1.1330  lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1.1331 -by(metis nat_lcm_dvd1 dvd_trans)
  1.1332 +by(metis lcm_dvd1_nat dvd_trans)
  1.1333  
  1.1334  lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1.1335 -by(metis nat_lcm_dvd2 dvd_trans)
  1.1336 +by(metis lcm_dvd2_nat dvd_trans)
  1.1337  
  1.1338  lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1.1339 -by(metis int_lcm_dvd1 dvd_trans)
  1.1340 +by(metis lcm_dvd1_int dvd_trans)
  1.1341  
  1.1342  lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1.1343 -by(metis int_lcm_dvd2 dvd_trans)
  1.1344 +by(metis lcm_dvd2_int dvd_trans)
  1.1345  
  1.1346 -lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and>
  1.1347 +lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1.1348      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1.1349 -  by (auto intro: dvd_anti_sym nat_lcm_least nat_lcm_dvd1 nat_lcm_dvd2)
  1.1350 +  by (auto intro: dvd_anti_sym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
  1.1351  
  1.1352 -lemma int_lcm_unique: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1.1353 +lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1.1354      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1.1355 -  by (auto intro: dvd_anti_sym [transferred] int_lcm_least)
  1.1356 +  by (auto intro: dvd_anti_sym [transferred] lcm_least_int)
  1.1357  
  1.1358  lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1.1359    apply (rule sym)
  1.1360 -  apply (subst nat_lcm_unique [symmetric])
  1.1361 +  apply (subst lcm_unique_nat [symmetric])
  1.1362    apply auto
  1.1363  done
  1.1364  
  1.1365  lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
  1.1366    apply (rule sym)
  1.1367 -  apply (subst int_lcm_unique [symmetric])
  1.1368 +  apply (subst lcm_unique_int [symmetric])
  1.1369    apply auto
  1.1370  done
  1.1371  
  1.1372  lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1.1373 -by (subst nat_lcm_commute, erule lcm_proj2_if_dvd_nat)
  1.1374 +by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
  1.1375  
  1.1376  lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
  1.1377 -by (subst int_lcm_commute, erule lcm_proj2_if_dvd_int)
  1.1378 +by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
  1.1379  
  1.1380  
  1.1381  lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
  1.1382 -apply(rule nat_lcm_unique[THEN iffD1])
  1.1383 -apply (metis dvd.order_trans nat_lcm_unique)
  1.1384 +apply(rule lcm_unique_nat[THEN iffD1])
  1.1385 +apply (metis dvd.order_trans lcm_unique_nat)
  1.1386  done
  1.1387  
  1.1388  lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
  1.1389 -apply(rule int_lcm_unique[THEN iffD1])
  1.1390 -apply (metis dvd_trans int_lcm_unique)
  1.1391 +apply(rule lcm_unique_int[THEN iffD1])
  1.1392 +apply (metis dvd_trans lcm_unique_int)
  1.1393  done
  1.1394  
  1.1395  lemmas lcm_left_commute_nat =
  1.1396 -  mk_left_commute[of lcm, OF lcm_assoc_nat nat_lcm_commute]
  1.1397 +  mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
  1.1398  
  1.1399  lemmas lcm_left_commute_int =
  1.1400 -  mk_left_commute[of lcm, OF lcm_assoc_int int_lcm_commute]
  1.1401 +  mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
  1.1402  
  1.1403 -lemmas lcm_ac_nat = lcm_assoc_nat nat_lcm_commute lcm_left_commute_nat
  1.1404 -lemmas lcm_ac_int = lcm_assoc_int int_lcm_commute lcm_left_commute_int
  1.1405 +lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  1.1406 +lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  1.1407  
  1.1408  
  1.1409  subsection {* Primes *}
  1.1410 @@ -1465,40 +1465,40 @@
  1.1411  (* Is there a better way to handle these, rather than making them
  1.1412     elim rules? *)
  1.1413  
  1.1414 -lemma nat_prime_ge_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
  1.1415 +lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
  1.1416    by (unfold prime_nat_def, auto)
  1.1417  
  1.1418 -lemma nat_prime_gt_0 [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
  1.1419 +lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
  1.1420    by (unfold prime_nat_def, auto)
  1.1421  
  1.1422 -lemma nat_prime_ge_1 [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
  1.1423 +lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
  1.1424    by (unfold prime_nat_def, auto)
  1.1425  
  1.1426 -lemma nat_prime_gt_1 [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
  1.1427 +lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
  1.1428    by (unfold prime_nat_def, auto)
  1.1429  
  1.1430 -lemma nat_prime_ge_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
  1.1431 +lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
  1.1432    by (unfold prime_nat_def, auto)
  1.1433  
  1.1434 -lemma nat_prime_gt_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
  1.1435 +lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
  1.1436    by (unfold prime_nat_def, auto)
  1.1437  
  1.1438 -lemma nat_prime_ge_2 [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
  1.1439 +lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
  1.1440    by (unfold prime_nat_def, auto)
  1.1441  
  1.1442 -lemma int_prime_ge_0 [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
  1.1443 +lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
  1.1444    by (unfold prime_int_def prime_nat_def, auto)
  1.1445  
  1.1446 -lemma int_prime_gt_0 [elim]: "prime (p::int) \<Longrightarrow> p > 0"
  1.1447 +lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
  1.1448    by (unfold prime_int_def prime_nat_def, auto)
  1.1449  
  1.1450 -lemma int_prime_ge_1 [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
  1.1451 +lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
  1.1452    by (unfold prime_int_def prime_nat_def, auto)
  1.1453  
  1.1454 -lemma int_prime_gt_1 [elim]: "prime (p::int) \<Longrightarrow> p > 1"
  1.1455 +lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
  1.1456    by (unfold prime_int_def prime_nat_def, auto)
  1.1457  
  1.1458 -lemma int_prime_ge_2 [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
  1.1459 +lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
  1.1460    by (unfold prime_int_def prime_nat_def, auto)
  1.1461  
  1.1462  thm prime_nat_def;
  1.1463 @@ -1508,59 +1508,59 @@
  1.1464      m = 1 \<or> m = p))"
  1.1465    using prime_nat_def [transferred]
  1.1466      apply (case_tac "p >= 0")
  1.1467 -    by (blast, auto simp add: int_prime_ge_0)
  1.1468 +    by (blast, auto simp add: prime_ge_0_int)
  1.1469  
  1.1470  (* To do: determine primality of any numeral *)
  1.1471  
  1.1472 -lemma nat_zero_not_prime [simp]: "~prime (0::nat)"
  1.1473 +lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
  1.1474    by (simp add: prime_nat_def)
  1.1475  
  1.1476 -lemma int_zero_not_prime [simp]: "~prime (0::int)"
  1.1477 +lemma zero_not_prime_int [simp]: "~prime (0::int)"
  1.1478    by (simp add: prime_int_def)
  1.1479  
  1.1480 -lemma nat_one_not_prime [simp]: "~prime (1::nat)"
  1.1481 +lemma one_not_prime_nat [simp]: "~prime (1::nat)"
  1.1482    by (simp add: prime_nat_def)
  1.1483  
  1.1484 -lemma nat_Suc_0_not_prime [simp]: "~prime (Suc 0)"
  1.1485 +lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
  1.1486    by (simp add: prime_nat_def One_nat_def)
  1.1487  
  1.1488 -lemma int_one_not_prime [simp]: "~prime (1::int)"
  1.1489 +lemma one_not_prime_int [simp]: "~prime (1::int)"
  1.1490    by (simp add: prime_int_def)
  1.1491  
  1.1492 -lemma nat_two_is_prime [simp]: "prime (2::nat)"
  1.1493 +lemma two_is_prime_nat [simp]: "prime (2::nat)"
  1.1494    apply (auto simp add: prime_nat_def)
  1.1495    apply (case_tac m)
  1.1496    apply (auto dest!: dvd_imp_le)
  1.1497    done
  1.1498  
  1.1499 -lemma int_two_is_prime [simp]: "prime (2::int)"
  1.1500 -  by (rule nat_two_is_prime [transferred direction: nat "op <= (0::int)"])
  1.1501 +lemma two_is_prime_int [simp]: "prime (2::int)"
  1.1502 +  by (rule two_is_prime_nat [transferred direction: nat "op <= (0::int)"])
  1.1503  
  1.1504 -lemma nat_prime_imp_coprime: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1.1505 +lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1.1506    apply (unfold prime_nat_def)
  1.1507 -  apply (metis nat_gcd_dvd1 nat_gcd_dvd2)
  1.1508 +  apply (metis gcd_dvd1_nat gcd_dvd2_nat)
  1.1509    done
  1.1510  
  1.1511 -lemma int_prime_imp_coprime: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1.1512 +lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
  1.1513    apply (unfold prime_int_altdef)
  1.1514 -  apply (metis int_gcd_dvd1 int_gcd_dvd2 int_gcd_ge_0)
  1.1515 +  apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
  1.1516    done
  1.1517  
  1.1518 -lemma nat_prime_dvd_mult: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1.1519 -  by (blast intro: nat_coprime_dvd_mult nat_prime_imp_coprime)
  1.1520 +lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1.1521 +  by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
  1.1522  
  1.1523 -lemma int_prime_dvd_mult: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1.1524 -  by (blast intro: int_coprime_dvd_mult int_prime_imp_coprime)
  1.1525 +lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
  1.1526 +  by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
  1.1527  
  1.1528 -lemma nat_prime_dvd_mult_eq [simp]: "prime (p::nat) \<Longrightarrow>
  1.1529 +lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
  1.1530      p dvd m * n = (p dvd m \<or> p dvd n)"
  1.1531 -  by (rule iffI, rule nat_prime_dvd_mult, auto)
  1.1532 +  by (rule iffI, rule prime_dvd_mult_nat, auto)
  1.1533  
  1.1534 -lemma int_prime_dvd_mult_eq [simp]: "prime (p::int) \<Longrightarrow>
  1.1535 +lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
  1.1536      p dvd m * n = (p dvd m \<or> p dvd n)"
  1.1537 -  by (rule iffI, rule int_prime_dvd_mult, auto)
  1.1538 +  by (rule iffI, rule prime_dvd_mult_int, auto)
  1.1539  
  1.1540 -lemma nat_not_prime_eq_prod: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1.1541 +lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1.1542      EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1.1543    unfolding prime_nat_def dvd_def apply auto
  1.1544    apply (subgoal_tac "k > 1")
  1.1545 @@ -1573,7 +1573,7 @@
  1.1546  
  1.1547  (* there's a lot of messing around with signs of products here --
  1.1548     could this be made more automatic? *)
  1.1549 -lemma int_not_prime_eq_prod: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1.1550 +lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
  1.1551      EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
  1.1552    unfolding prime_int_altdef dvd_def
  1.1553    apply auto
  1.1554 @@ -1593,72 +1593,72 @@
  1.1555    apply auto
  1.1556  done
  1.1557  
  1.1558 -lemma nat_prime_dvd_power [rule_format]: "prime (p::nat) -->
  1.1559 +lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
  1.1560      n > 0 --> (p dvd x^n --> p dvd x)"
  1.1561    by (induct n rule: nat_induct, auto)
  1.1562  
  1.1563 -lemma int_prime_dvd_power [rule_format]: "prime (p::int) -->
  1.1564 +lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
  1.1565      n > 0 --> (p dvd x^n --> p dvd x)"
  1.1566    apply (induct n rule: nat_induct, auto)
  1.1567 -  apply (frule int_prime_ge_0)
  1.1568 +  apply (frule prime_ge_0_int)
  1.1569    apply auto
  1.1570  done
  1.1571  
  1.1572 -lemma nat_prime_imp_power_coprime: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1.1573 +lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1.1574      coprime a (p^m)"
  1.1575 -  apply (rule nat_coprime_exp)
  1.1576 -  apply (subst nat_gcd_commute)
  1.1577 -  apply (erule (1) nat_prime_imp_coprime)
  1.1578 +  apply (rule coprime_exp_nat)
  1.1579 +  apply (subst gcd_commute_nat)
  1.1580 +  apply (erule (1) prime_imp_coprime_nat)
  1.1581  done
  1.1582  
  1.1583 -lemma int_prime_imp_power_coprime: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1.1584 +lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
  1.1585      coprime a (p^m)"
  1.1586 -  apply (rule int_coprime_exp)
  1.1587 -  apply (subst int_gcd_commute)
  1.1588 -  apply (erule (1) int_prime_imp_coprime)
  1.1589 +  apply (rule coprime_exp_int)
  1.1590 +  apply (subst gcd_commute_int)
  1.1591 +  apply (erule (1) prime_imp_coprime_int)
  1.1592  done
  1.1593  
  1.1594 -lemma nat_primes_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1.1595 -  apply (rule nat_prime_imp_coprime, assumption)
  1.1596 +lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1.1597 +  apply (rule prime_imp_coprime_nat, assumption)
  1.1598    apply (unfold prime_nat_def, auto)
  1.1599  done
  1.1600  
  1.1601 -lemma int_primes_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1.1602 -  apply (rule int_prime_imp_coprime, assumption)
  1.1603 +lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
  1.1604 +  apply (rule prime_imp_coprime_int, assumption)
  1.1605    apply (unfold prime_int_altdef, clarify)
  1.1606    apply (drule_tac x = q in spec)
  1.1607    apply (drule_tac x = p in spec)
  1.1608    apply auto
  1.1609  done
  1.1610  
  1.1611 -lemma nat_primes_imp_powers_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1.1612 +lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1.1613      coprime (p^m) (q^n)"
  1.1614 -  by (rule nat_coprime_exp2, rule nat_primes_coprime)
  1.1615 +  by (rule coprime_exp2_nat, rule primes_coprime_nat)
  1.1616  
  1.1617 -lemma int_primes_imp_powers_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1.1618 +lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
  1.1619      coprime (p^m) (q^n)"
  1.1620 -  by (rule int_coprime_exp2, rule int_primes_coprime)
  1.1621 +  by (rule coprime_exp2_int, rule primes_coprime_int)
  1.1622  
  1.1623 -lemma nat_prime_factor: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
  1.1624 +lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
  1.1625    apply (induct n rule: nat_less_induct)
  1.1626    apply (case_tac "n = 0")
  1.1627 -  using nat_two_is_prime apply blast
  1.1628 +  using two_is_prime_nat apply blast
  1.1629    apply (case_tac "prime n")
  1.1630    apply blast
  1.1631    apply (subgoal_tac "n > 1")
  1.1632 -  apply (frule (1) nat_not_prime_eq_prod)
  1.1633 +  apply (frule (1) not_prime_eq_prod_nat)
  1.1634    apply (auto intro: dvd_mult dvd_mult2)
  1.1635  done
  1.1636  
  1.1637  (* An Isar version:
  1.1638  
  1.1639 -lemma nat_prime_factor_b:
  1.1640 +lemma prime_factor_b_nat:
  1.1641    fixes n :: nat
  1.1642    assumes "n \<noteq> 1"
  1.1643    shows "\<exists>p. prime p \<and> p dvd n"
  1.1644  
  1.1645  using `n ~= 1`
  1.1646 -proof (induct n rule: nat_less_induct)
  1.1647 +proof (induct n rule: less_induct_nat)
  1.1648    fix n :: nat
  1.1649    assume "n ~= 1" and
  1.1650      ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
  1.1651 @@ -1666,9 +1666,9 @@
  1.1652    proof -
  1.1653    {
  1.1654      assume "n = 0"
  1.1655 -    moreover note nat_two_is_prime
  1.1656 +    moreover note two_is_prime_nat
  1.1657      ultimately have ?thesis
  1.1658 -      by (auto simp del: nat_two_is_prime)
  1.1659 +      by (auto simp del: two_is_prime_nat)
  1.1660    }
  1.1661    moreover
  1.1662    {
  1.1663 @@ -1679,7 +1679,7 @@
  1.1664    {
  1.1665      assume "n ~= 0" and "~ prime n"
  1.1666      with `n ~= 1` have "n > 1" by auto
  1.1667 -    with `~ prime n` and nat_not_prime_eq_prod obtain m k where
  1.1668 +    with `~ prime n` and not_prime_eq_prod_nat obtain m k where
  1.1669        "n = m * k" and "1 < m" and "m < n" by blast
  1.1670      with ih obtain p where "prime p" and "p dvd m" by blast
  1.1671      with `n = m * k` have ?thesis by auto
  1.1672 @@ -1692,7 +1692,7 @@
  1.1673  
  1.1674  text {* One property of coprimality is easier to prove via prime factors. *}
  1.1675  
  1.1676 -lemma nat_prime_divprod_pow:
  1.1677 +lemma prime_divprod_pow_nat:
  1.1678    assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
  1.1679    shows "p^n dvd a \<or> p^n dvd b"
  1.1680  proof-
  1.1681 @@ -1705,27 +1705,27 @@
  1.1682      from n have "p dvd p^n" by (intro dvd_power, auto)
  1.1683      also note pab
  1.1684      finally have pab': "p dvd a * b".
  1.1685 -    from nat_prime_dvd_mult[OF p pab']
  1.1686 +    from prime_dvd_mult_nat[OF p pab']
  1.1687      have "p dvd a \<or> p dvd b" .
  1.1688      moreover
  1.1689      {assume pa: "p dvd a"
  1.1690        have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1.1691 -      from nat_coprime_common_divisor [OF ab, OF pa] p have "\<not> p dvd b" by auto
  1.1692 +      from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
  1.1693        with p have "coprime b p"
  1.1694 -        by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
  1.1695 +        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
  1.1696        hence pnb: "coprime (p^n) b"
  1.1697 -        by (subst nat_gcd_commute, rule nat_coprime_exp)
  1.1698 -      from nat_coprime_divprod[OF pnba pnb] have ?thesis by blast }
  1.1699 +        by (subst gcd_commute_nat, rule coprime_exp_nat)
  1.1700 +      from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
  1.1701      moreover
  1.1702      {assume pb: "p dvd b"
  1.1703        have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
  1.1704 -      from nat_coprime_common_divisor [OF ab, of p] pb p have "\<not> p dvd a"
  1.1705 +      from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
  1.1706          by auto
  1.1707        with p have "coprime a p"
  1.1708 -        by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
  1.1709 +        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
  1.1710        hence pna: "coprime (p^n) a"
  1.1711 -        by (subst nat_gcd_commute, rule nat_coprime_exp)
  1.1712 -      from nat_coprime_divprod[OF pab pna] have ?thesis by blast }
  1.1713 +        by (subst gcd_commute_nat, rule coprime_exp_nat)
  1.1714 +      from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
  1.1715      ultimately have ?thesis by blast}
  1.1716    ultimately show ?thesis by blast
  1.1717  qed