# HG changeset patch # User haftmann # Date 1246994768 -7200 # Node ID 3fc19d2f0ac9e3d731c0cee149ba8d08997fd9c5 # Parent 2133f596c520d15a0fff7f8ee6b0a97f67937207# Parent 56c134c6c5d898ba06d35bcf39a1641337e141a1 merged diff -r 2133f596c520 -r 3fc19d2f0ac9 src/HOL/Algebra/Exponent.thy --- a/src/HOL/Algebra/Exponent.thy Tue Jul 07 17:50:03 2009 +0200 +++ b/src/HOL/Algebra/Exponent.thy Tue Jul 07 21:26:08 2009 +0200 @@ -217,7 +217,7 @@ prefer 2 apply (blast intro: dvd_mult2) apply (drule dvd_diffD1) apply assumption - prefer 2 apply (blast intro: nat_dvd_diff) + prefer 2 apply (blast intro: dvd_diff_nat) apply (drule gr0_implies_Suc, auto) done @@ -233,7 +233,7 @@ prefer 2 apply (blast intro: dvd_mult2) apply (drule dvd_diffD1) apply assumption - prefer 2 apply (blast intro: nat_dvd_diff) + prefer 2 apply (blast intro: dvd_diff_nat) apply (drule less_imp_Suc_add, auto) done diff -r 2133f596c520 -r 3fc19d2f0ac9 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Tue Jul 07 17:50:03 2009 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Tue Jul 07 21:26:08 2009 +0200 @@ -1042,7 +1042,7 @@ consts plusinf:: "fm \ fm" (* Virtual substitution of +\*) minusinf:: "fm \ fm" (* Virtual substitution of -\*) - \ :: "fm \ int" (* Compute lcm {d| N\<^isup>?\<^isup> Dvd c*x+t \ p}*) + \ :: "fm \ int" (* Compute lcm {d| N\<^isup>? Dvd c*x+t \ p}*) d\ :: "fm \ int \ bool" (* checks if a given l divides all the ds above*) recdef minusinf "measure size" @@ -1104,7 +1104,7 @@ proof (induct p rule: iszlfm.induct) case (1 p q) let ?d = "\ (And p q)" - from prems int_lcm_pos have dp: "?d >0" by simp + from prems lcm_pos_int have dp: "?d >0" by simp have d1: "\ p dvd \ (And p q)" using prems by simp hence th: "d\ p ?d" using delta_mono prems(3-4) by(simp only: iszlfm.simps) have "\ q dvd \ (And p q)" using prems by simp @@ -1113,7 +1113,7 @@ next case (2 p q) let ?d = "\ (And p q)" - from prems int_lcm_pos have dp: "?d >0" by simp + from prems lcm_pos_int have dp: "?d >0" by simp have "\ p dvd \ (And p q)" using prems by simp hence th: "d\ p ?d" using delta_mono prems by(simp only: iszlfm.simps) have "\ q dvd \ (And p q)" using prems by simp @@ -1410,15 +1410,15 @@ from prems have dl2: "\ q dvd lcm (\ p) (\ q)" by simp from prems d\_mono[where p = "p" and l="\ p" and l'="lcm (\ p) (\ q)"] d\_mono[where p = "q" and l="\ q" and l'="lcm (\ p) (\ q)"] - dl1 dl2 show ?case by (auto simp add: int_lcm_pos) + dl1 dl2 show ?case by (auto simp add: lcm_pos_int) next case (2 p q) from prems have dl1: "\ p dvd lcm (\ p) (\ q)" by simp from prems have dl2: "\ q dvd lcm (\ p) (\ q)" by simp from prems d\_mono[where p = "p" and l="\ p" and l'="lcm (\ p) (\ q)"] d\_mono[where p = "q" and l="\ q" and l'="lcm (\ p) (\ q)"] - dl1 dl2 show ?case by (auto simp add: int_lcm_pos) -qed (auto simp add: int_lcm_pos) + dl1 dl2 show ?case by (auto simp add: lcm_pos_int) +qed (auto simp add: lcm_pos_int) lemma a\: assumes linp: "iszlfm p" and d: "d\ p l" and lp: "l > 0" shows "iszlfm (a\ p l) \ d\ (a\ p l) 1 \ (Ifm bbs (l*x #bs) (a\ p l) = Ifm bbs (x#bs) p)" diff -r 2133f596c520 -r 3fc19d2f0ac9 src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Tue Jul 07 17:50:03 2009 +0200 +++ b/src/HOL/Decision_Procs/Ferrack.thy Tue Jul 07 21:26:08 2009 +0200 @@ -746,7 +746,7 @@ moreover {assume g1:"?g>1" hence g0: "?g > 0" by simp from g1 nnz have gp0: "?g' \ 0" by simp - hence g'p: "?g' > 0" using int_gcd_ge_0[where x="n" and y="numgcd ?t'"] by arith + hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith hence "?g'= 1 \ ?g' > 1" by arith moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)} moreover {assume g'1:"?g'>1" @@ -782,7 +782,7 @@ moreover {assume g1:"?g>1" hence g0: "?g > 0" by simp from g1 nnz have gp0: "?g' \ 0" by simp - hence g'p: "?g' > 0" using int_gcd_ge_0[where x="n" and y="numgcd ?t'"] by arith + hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith hence "?g'= 1 \ ?g' > 1" by arith moreover {assume "?g'=1" hence ?thesis using prems by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)} diff -r 2133f596c520 -r 3fc19d2f0ac9 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Tue Jul 07 17:50:03 2009 +0200 +++ b/src/HOL/Decision_Procs/MIR.thy Tue Jul 07 21:26:08 2009 +0200 @@ -1060,7 +1060,7 @@ moreover {assume g1:"?g>1" hence g0: "?g > 0" by simp from g1 nnz have gp0: "?g' \ 0" by simp - hence g'p: "?g' > 0" using int_gcd_ge_0[where x="n" and y="numgcd ?t'"] by arith + hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith hence "?g'= 1 \ ?g' > 1" by arith moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def)} moreover {assume g'1:"?g'>1" @@ -1096,7 +1096,7 @@ moreover {assume g1:"?g>1" hence g0: "?g > 0" by simp from g1 nnz have gp0: "?g' \ 0" by simp - hence g'p: "?g' > 0" using int_gcd_ge_0[where x="n" and y="numgcd ?t'"] by arith + hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith hence "?g'= 1 \ ?g' > 1" by arith moreover {assume "?g'=1" hence ?thesis using prems by (auto simp add: Let_def simp_num_pair_def)} @@ -1233,7 +1233,7 @@ moreover {assume g1:"?g>1" hence g0: "?g > 0" by simp from g1 dnz have gp0: "?g' \ 0" by simp - hence g'p: "?g' > 0" using int_gcd_ge_0[where x="d" and y="numgcd t"] by arith + hence g'p: "?g' > 0" using gcd_ge_0_int[where x="d" and y="numgcd t"] by arith hence "?g'= 1 \ ?g' > 1" by arith moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simpdvd_def)} moreover {assume g'1:"?g'>1" @@ -2126,7 +2126,7 @@ proof (induct p rule: iszlfm.induct) case (1 p q) let ?d = "\ (And p q)" - from prems int_lcm_pos have dp: "?d >0" by simp + from prems lcm_pos_int have dp: "?d >0" by simp have d1: "\ p dvd \ (And p q)" using prems by simp hence th: "d\ p ?d" using delta_mono prems by(simp only: iszlfm.simps) blast @@ -2136,7 +2136,7 @@ next case (2 p q) let ?d = "\ (And p q)" - from prems int_lcm_pos have dp: "?d >0" by simp + from prems lcm_pos_int have dp: "?d >0" by simp have "\ p dvd \ (And p q)" using prems by simp hence th: "d\ p ?d" using delta_mono prems by(simp only: iszlfm.simps) blast have "\ q dvd \ (And p q)" using prems by simp hence th': "d\ q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast @@ -2514,15 +2514,15 @@ from prems have dl2: "\ q dvd lcm (\ p) (\ q)" by simp from prems d\_mono[where p = "p" and l="\ p" and l'="lcm (\ p) (\ q)"] d\_mono[where p = "q" and l="\ q" and l'="lcm (\ p) (\ q)"] - dl1 dl2 show ?case by (auto simp add: int_lcm_pos) + dl1 dl2 show ?case by (auto simp add: lcm_pos_int) next case (2 p q) from prems have dl1: "\ p dvd lcm (\ p) (\ q)" by simp from prems have dl2: "\ q dvd lcm (\ p) (\ q)" by simp from prems d\_mono[where p = "p" and l="\ p" and l'="lcm (\ p) (\ q)"] d\_mono[where p = "q" and l="\ q" and l'="lcm (\ p) (\ q)"] - dl1 dl2 show ?case by (auto simp add: int_lcm_pos) -qed (auto simp add: int_lcm_pos) + dl1 dl2 show ?case by (auto simp add: lcm_pos_int) +qed (auto simp add: lcm_pos_int) lemma a\: assumes linp: "iszlfm p (a #bs)" and d: "d\ p l" and lp: "l > 0" shows "iszlfm (a\ p l) (a #bs) \ d\ (a\ p l) 1 \ (Ifm (real (l * x) #bs) (a\ p l) = Ifm ((real x)#bs) p)" @@ -4175,7 +4175,7 @@ by (induct p rule: isrlfm.induct, auto) lemma zgcd_le1: assumes ip: "(0::int) < i" shows "gcd i j \ i" proof- - from int_gcd_dvd1 have th: "gcd i j dvd i" by blast + from gcd_dvd1_int have th: "gcd i j dvd i" by blast from zdvd_imp_le[OF th ip] show ?thesis . qed diff -r 2133f596c520 -r 3fc19d2f0ac9 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Jul 07 17:50:03 2009 +0200 +++ b/src/HOL/Divides.thy Tue Jul 07 21:26:08 2009 +0200 @@ -887,7 +887,7 @@ interpretation dvd: order "op dvd" "\n m \ nat. n dvd m \ \ m dvd n" proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym) -lemma nat_dvd_diff[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)" +lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)" unfolding dvd_def by (blast intro: diff_mult_distrib2 [symmetric]) @@ -897,7 +897,7 @@ done lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\m |] ==> k dvd (n::nat)" -by (drule_tac m = m in nat_dvd_diff, auto) +by (drule_tac m = m in dvd_diff_nat, auto) lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))" apply (rule iffI) @@ -906,7 +906,7 @@ apply (subgoal_tac "n = (n+k) -k") prefer 2 apply simp apply (erule ssubst) - apply (erule nat_dvd_diff) + apply (erule dvd_diff_nat) apply (rule dvd_refl) done diff -r 2133f596c520 -r 3fc19d2f0ac9 src/HOL/Extraction/Euclid.thy --- a/src/HOL/Extraction/Euclid.thy Tue Jul 07 17:50:03 2009 +0200 +++ b/src/HOL/Extraction/Euclid.thy Tue Jul 07 21:26:08 2009 +0200 @@ -189,7 +189,7 @@ assume pn: "p \ n" from `prime p` have "0 < p" by (rule prime_g_zero) then have "p dvd n!" using pn by (rule dvd_factorial) - with dvd have "p dvd ?k - n!" by (rule nat_dvd_diff) + with dvd have "p dvd ?k - n!" by (rule dvd_diff_nat) then have "p dvd 1" by simp with prime show False using prime_nd_one by auto qed diff -r 2133f596c520 -r 3fc19d2f0ac9 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Tue Jul 07 17:50:03 2009 +0200 +++ b/src/HOL/GCD.thy Tue Jul 07 21:26:08 2009 +0200 @@ -163,7 +163,7 @@ subsection {* GCD *} (* was gcd_induct *) -lemma nat_gcd_induct: +lemma gcd_nat_induct: fixes m n :: nat assumes "\m. P m 0" and "\m n. 0 < n \ P n (m mod n) \ P m n" @@ -175,43 +175,43 @@ (* specific to int *) -lemma int_gcd_neg1 [simp]: "gcd (-x::int) y = gcd x y" +lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y" by (simp add: gcd_int_def) -lemma int_gcd_neg2 [simp]: "gcd (x::int) (-y) = gcd x y" +lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y" by (simp add: gcd_int_def) lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y" by(simp add: gcd_int_def) -lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)" +lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)" by (simp add: gcd_int_def) lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y" -by (metis abs_idempotent int_gcd_abs) +by (metis abs_idempotent gcd_abs_int) lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y" -by (metis abs_idempotent int_gcd_abs) +by (metis abs_idempotent gcd_abs_int) -lemma int_gcd_cases: +lemma gcd_cases_int: fixes x :: int and y assumes "x >= 0 \ y >= 0 \ P (gcd x y)" and "x >= 0 \ y <= 0 \ P (gcd x (-y))" and "x <= 0 \ y >= 0 \ P (gcd (-x) y)" and "x <= 0 \ y <= 0 \ P (gcd (-x) (-y))" shows "P (gcd x y)" -by (insert prems, auto simp add: int_gcd_neg1 int_gcd_neg2, arith) +by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith) -lemma int_gcd_ge_0 [simp]: "gcd (x::int) y >= 0" +lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0" by (simp add: gcd_int_def) -lemma int_lcm_neg1: "lcm (-x::int) y = lcm x y" +lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y" by (simp add: lcm_int_def) -lemma int_lcm_neg2: "lcm (x::int) (-y) = lcm x y" +lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y" by (simp add: lcm_int_def) -lemma int_lcm_abs: "lcm (x::int) y = lcm (abs x) (abs y)" +lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)" by (simp add: lcm_int_def) lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j" @@ -223,53 +223,53 @@ lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y" by (metis abs_idempotent lcm_int_def) -lemma int_lcm_cases: +lemma lcm_cases_int: fixes x :: int and y assumes "x >= 0 \ y >= 0 \ P (lcm x y)" and "x >= 0 \ y <= 0 \ P (lcm x (-y))" and "x <= 0 \ y >= 0 \ P (lcm (-x) y)" and "x <= 0 \ y <= 0 \ P (lcm (-x) (-y))" shows "P (lcm x y)" -by (insert prems, auto simp add: int_lcm_neg1 int_lcm_neg2, arith) +by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith) -lemma int_lcm_ge_0 [simp]: "lcm (x::int) y >= 0" +lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0" by (simp add: lcm_int_def) (* was gcd_0, etc. *) -lemma nat_gcd_0 [simp]: "gcd (x::nat) 0 = x" +lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x" by simp (* was igcd_0, etc. *) -lemma int_gcd_0 [simp]: "gcd (x::int) 0 = abs x" +lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x" by (unfold gcd_int_def, auto) -lemma nat_gcd_0_left [simp]: "gcd 0 (x::nat) = x" +lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x" by simp -lemma int_gcd_0_left [simp]: "gcd 0 (x::int) = abs x" +lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x" by (unfold gcd_int_def, auto) -lemma nat_gcd_red: "gcd (x::nat) y = gcd y (x mod y)" +lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)" by (case_tac "y = 0", auto) (* weaker, but useful for the simplifier *) -lemma nat_gcd_non_0: "y ~= (0::nat) \ gcd (x::nat) y = gcd y (x mod y)" +lemma gcd_non_0_nat: "y ~= (0::nat) \ gcd (x::nat) y = gcd y (x mod y)" by simp -lemma nat_gcd_1 [simp]: "gcd (m::nat) 1 = 1" +lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1" by simp -lemma nat_gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" +lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0" by (simp add: One_nat_def) -lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1" +lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1" by (simp add: gcd_int_def) -lemma nat_gcd_idem: "gcd (x::nat) x = x" +lemma gcd_idem_nat: "gcd (x::nat) x = x" by simp -lemma int_gcd_idem: "gcd (x::int) x = abs x" +lemma gcd_idem_int: "gcd (x::int) x = abs x" by (auto simp add: gcd_int_def) declare gcd_nat.simps [simp del] @@ -279,260 +279,260 @@ conjunctions don't seem provable separately. *} -lemma nat_gcd_dvd1 [iff]: "(gcd (m::nat)) n dvd m" - and nat_gcd_dvd2 [iff]: "(gcd m n) dvd n" - apply (induct m n rule: nat_gcd_induct) - apply (simp_all add: nat_gcd_non_0) +lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m" + and gcd_dvd2_nat [iff]: "(gcd m n) dvd n" + apply (induct m n rule: gcd_nat_induct) + apply (simp_all add: gcd_non_0_nat) apply (blast dest: dvd_mod_imp_dvd) done -lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x" -by (metis gcd_int_def int_dvd_iff nat_gcd_dvd1) +lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x" +by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat) -lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y" -by (metis gcd_int_def int_dvd_iff nat_gcd_dvd2) +lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y" +by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat) lemma dvd_gcd_D1_nat: "k dvd gcd m n \ (k::nat) dvd m" -by(metis nat_gcd_dvd1 dvd_trans) +by(metis gcd_dvd1_nat dvd_trans) lemma dvd_gcd_D2_nat: "k dvd gcd m n \ (k::nat) dvd n" -by(metis nat_gcd_dvd2 dvd_trans) +by(metis gcd_dvd2_nat dvd_trans) lemma dvd_gcd_D1_int: "i dvd gcd m n \ (i::int) dvd m" -by(metis int_gcd_dvd1 dvd_trans) +by(metis gcd_dvd1_int dvd_trans) lemma dvd_gcd_D2_int: "i dvd gcd m n \ (i::int) dvd n" -by(metis int_gcd_dvd2 dvd_trans) +by(metis gcd_dvd2_int dvd_trans) -lemma nat_gcd_le1 [simp]: "a \ 0 \ gcd (a::nat) b \ a" +lemma gcd_le1_nat [simp]: "a \ 0 \ gcd (a::nat) b \ a" by (rule dvd_imp_le, auto) -lemma nat_gcd_le2 [simp]: "b \ 0 \ gcd (a::nat) b \ b" +lemma gcd_le2_nat [simp]: "b \ 0 \ gcd (a::nat) b \ b" by (rule dvd_imp_le, auto) -lemma int_gcd_le1 [simp]: "a > 0 \ gcd (a::int) b \ a" +lemma gcd_le1_int [simp]: "a > 0 \ gcd (a::int) b \ a" by (rule zdvd_imp_le, auto) -lemma int_gcd_le2 [simp]: "b > 0 \ gcd (a::int) b \ b" +lemma gcd_le2_int [simp]: "b > 0 \ gcd (a::int) b \ b" by (rule zdvd_imp_le, auto) -lemma nat_gcd_greatest: "(k::nat) dvd m \ k dvd n \ k dvd gcd m n" -by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod) +lemma gcd_greatest_nat: "(k::nat) dvd m \ k dvd n \ k dvd gcd m n" +by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod) -lemma int_gcd_greatest: +lemma gcd_greatest_int: "(k::int) dvd m \ k dvd n \ k dvd gcd m n" - apply (subst int_gcd_abs) + apply (subst gcd_abs_int) apply (subst abs_dvd_iff [symmetric]) - apply (rule nat_gcd_greatest [transferred]) + apply (rule gcd_greatest_nat [transferred]) apply auto done -lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) = +lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) = (k dvd m & k dvd n)" - by (blast intro!: nat_gcd_greatest intro: dvd_trans) + by (blast intro!: gcd_greatest_nat intro: dvd_trans) -lemma int_gcd_greatest_iff: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)" - by (blast intro!: int_gcd_greatest intro: dvd_trans) +lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)" + by (blast intro!: gcd_greatest_int intro: dvd_trans) -lemma nat_gcd_zero [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)" - by (simp only: dvd_0_left_iff [symmetric] nat_gcd_greatest_iff) +lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)" + by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat) -lemma int_gcd_zero [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)" +lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)" by (auto simp add: gcd_int_def) -lemma nat_gcd_pos [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)" - by (insert nat_gcd_zero [of m n], arith) +lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)" + by (insert gcd_zero_nat [of m n], arith) -lemma int_gcd_pos [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)" - by (insert int_gcd_zero [of m n], insert int_gcd_ge_0 [of m n], arith) +lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)" + by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith) -lemma nat_gcd_commute: "gcd (m::nat) n = gcd n m" +lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m" by (rule dvd_anti_sym, auto) -lemma int_gcd_commute: "gcd (m::int) n = gcd n m" - by (auto simp add: gcd_int_def nat_gcd_commute) +lemma gcd_commute_int: "gcd (m::int) n = gcd n m" + by (auto simp add: gcd_int_def gcd_commute_nat) -lemma nat_gcd_assoc: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)" +lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)" apply (rule dvd_anti_sym) apply (blast intro: dvd_trans)+ done -lemma int_gcd_assoc: "gcd (gcd (k::int) m) n = gcd k (gcd m n)" - by (auto simp add: gcd_int_def nat_gcd_assoc) +lemma gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)" + by (auto simp add: gcd_int_def gcd_assoc_nat) -lemmas nat_gcd_left_commute = - mk_left_commute[of gcd, OF nat_gcd_assoc nat_gcd_commute] +lemmas gcd_left_commute_nat = + mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat] -lemmas int_gcd_left_commute = - mk_left_commute[of gcd, OF int_gcd_assoc int_gcd_commute] +lemmas gcd_left_commute_int = + mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int] -lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute +lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat -- {* gcd is an AC-operator *} -lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute +lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int -lemma nat_gcd_unique: "(d::nat) dvd a \ d dvd b \ +lemma gcd_unique_nat: "(d::nat) dvd a \ d dvd b \ (\e. e dvd a \ e dvd b \ e dvd d) \ d = gcd a b" apply auto apply (rule dvd_anti_sym) - apply (erule (1) nat_gcd_greatest) + apply (erule (1) gcd_greatest_nat) apply auto done -lemma int_gcd_unique: "d >= 0 & (d::int) dvd a \ d dvd b \ +lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \ d dvd b \ (\e. e dvd a \ e dvd b \ e dvd d) \ d = gcd a b" apply (case_tac "d = 0") apply force apply (rule iffI) apply (rule zdvd_anti_sym) apply arith - apply (subst int_gcd_pos) + apply (subst gcd_pos_int) apply clarsimp apply (drule_tac x = "d + 1" in spec) apply (frule zdvd_imp_le) - apply (auto intro: int_gcd_greatest) + apply (auto intro: gcd_greatest_int) done lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \ gcd x y = x" -by (metis dvd.eq_iff nat_gcd_unique) +by (metis dvd.eq_iff gcd_unique_nat) lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \ gcd x y = y" -by (metis dvd.eq_iff nat_gcd_unique) +by (metis dvd.eq_iff gcd_unique_nat) lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \ gcd (x::int) y = abs x" -by (metis abs_dvd_iff abs_eq_0 int_gcd_0_left int_gcd_abs int_gcd_unique) +by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int) lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \ gcd (x::int) y = abs y" -by (metis gcd_proj1_if_dvd_int int_gcd_commute) +by (metis gcd_proj1_if_dvd_int gcd_commute_int) text {* \medskip Multiplication laws *} -lemma nat_gcd_mult_distrib: "(k::nat) * gcd m n = gcd (k * m) (k * n)" +lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)" -- {* \cite[page 27]{davenport92} *} - apply (induct m n rule: nat_gcd_induct) + apply (induct m n rule: gcd_nat_induct) apply simp apply (case_tac "k = 0") - apply (simp_all add: mod_geq nat_gcd_non_0 mod_mult_distrib2) + apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2) done -lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)" - apply (subst (1 2) int_gcd_abs) +lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)" + apply (subst (1 2) gcd_abs_int) apply (subst (1 2) abs_mult) - apply (rule nat_gcd_mult_distrib [transferred]) + apply (rule gcd_mult_distrib_nat [transferred]) apply auto done -lemma nat_coprime_dvd_mult: "coprime (k::nat) n \ k dvd m * n \ k dvd m" - apply (insert nat_gcd_mult_distrib [of m k n]) +lemma coprime_dvd_mult_nat: "coprime (k::nat) n \ k dvd m * n \ k dvd m" + apply (insert gcd_mult_distrib_nat [of m k n]) apply simp apply (erule_tac t = m in ssubst) apply simp done -lemma int_coprime_dvd_mult: +lemma coprime_dvd_mult_int: "coprime (k::int) n \ k dvd m * n \ k dvd m" apply (subst abs_dvd_iff [symmetric]) apply (subst dvd_abs_iff [symmetric]) -apply (subst (asm) int_gcd_abs) -apply (rule nat_coprime_dvd_mult [transferred]) +apply (subst (asm) gcd_abs_int) +apply (rule coprime_dvd_mult_nat [transferred]) prefer 4 apply assumption apply auto apply (subst abs_mult [symmetric], auto) done -lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \ +lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \ (k dvd m * n) = (k dvd m)" - by (auto intro: nat_coprime_dvd_mult) + by (auto intro: coprime_dvd_mult_nat) -lemma int_coprime_dvd_mult_iff: "coprime (k::int) n \ +lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \ (k dvd m * n) = (k dvd m)" - by (auto intro: int_coprime_dvd_mult) + by (auto intro: coprime_dvd_mult_int) -lemma nat_gcd_mult_cancel: "coprime k n \ gcd ((k::nat) * m) n = gcd m n" +lemma gcd_mult_cancel_nat: "coprime k n \ gcd ((k::nat) * m) n = gcd m n" apply (rule dvd_anti_sym) - apply (rule nat_gcd_greatest) - apply (rule_tac n = k in nat_coprime_dvd_mult) - apply (simp add: nat_gcd_assoc) - apply (simp add: nat_gcd_commute) + apply (rule gcd_greatest_nat) + apply (rule_tac n = k in coprime_dvd_mult_nat) + apply (simp add: gcd_assoc_nat) + apply (simp add: gcd_commute_nat) apply (simp_all add: mult_commute) done -lemma int_gcd_mult_cancel: +lemma gcd_mult_cancel_int: "coprime (k::int) n \ gcd (k * m) n = gcd m n" -apply (subst (1 2) int_gcd_abs) +apply (subst (1 2) gcd_abs_int) apply (subst abs_mult) -apply (rule nat_gcd_mult_cancel [transferred], auto) +apply (rule gcd_mult_cancel_nat [transferred], auto) done text {* \medskip Addition laws *} -lemma nat_gcd_add1 [simp]: "gcd ((m::nat) + n) n = gcd m n" +lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n" apply (case_tac "n = 0") - apply (simp_all add: nat_gcd_non_0) + apply (simp_all add: gcd_non_0_nat) done -lemma nat_gcd_add2 [simp]: "gcd (m::nat) (m + n) = gcd m n" - apply (subst (1 2) nat_gcd_commute) +lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n" + apply (subst (1 2) gcd_commute_nat) apply (subst add_commute) apply simp done (* to do: add the other variations? *) -lemma nat_gcd_diff1: "(m::nat) >= n \ gcd (m - n) n = gcd m n" - by (subst nat_gcd_add1 [symmetric], auto) +lemma gcd_diff1_nat: "(m::nat) >= n \ gcd (m - n) n = gcd m n" + by (subst gcd_add1_nat [symmetric], auto) -lemma nat_gcd_diff2: "(n::nat) >= m \ gcd (n - m) n = gcd m n" - apply (subst nat_gcd_commute) - apply (subst nat_gcd_diff1 [symmetric]) +lemma gcd_diff2_nat: "(n::nat) >= m \ gcd (n - m) n = gcd m n" + apply (subst gcd_commute_nat) + apply (subst gcd_diff1_nat [symmetric]) apply auto - apply (subst nat_gcd_commute) - apply (subst nat_gcd_diff1) + apply (subst gcd_commute_nat) + apply (subst gcd_diff1_nat) apply assumption - apply (rule nat_gcd_commute) + apply (rule gcd_commute_nat) done -lemma int_gcd_non_0: "(y::int) > 0 \ gcd x y = gcd y (x mod y)" +lemma gcd_non_0_int: "(y::int) > 0 \ gcd x y = gcd y (x mod y)" apply (frule_tac b = y and a = x in pos_mod_sign) apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib) - apply (auto simp add: nat_gcd_non_0 nat_mod_distrib [symmetric] + apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] zmod_zminus1_eq_if) apply (frule_tac a = x in pos_mod_bound) - apply (subst (1 2) nat_gcd_commute) - apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2 + apply (subst (1 2) gcd_commute_nat) + apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle) done -lemma int_gcd_red: "gcd (x::int) y = gcd y (x mod y)" +lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)" apply (case_tac "y = 0") apply force apply (case_tac "y > 0") - apply (subst int_gcd_non_0, auto) - apply (insert int_gcd_non_0 [of "-y" "-x"]) - apply (auto simp add: int_gcd_neg1 int_gcd_neg2) + apply (subst gcd_non_0_int, auto) + apply (insert gcd_non_0_int [of "-y" "-x"]) + apply (auto simp add: gcd_neg1_int gcd_neg2_int) done -lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n" -by (metis int_gcd_red mod_add_self1 zadd_commute) +lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n" +by (metis gcd_red_int mod_add_self1 zadd_commute) -lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n" -by (metis int_gcd_add1 int_gcd_commute zadd_commute) +lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n" +by (metis gcd_add1_int gcd_commute_int zadd_commute) -lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n" -by (metis mod_mult_self3 nat_gcd_commute nat_gcd_red) +lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n" +by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat) -lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n" -by (metis int_gcd_commute int_gcd_red mod_mult_self1 zadd_commute) +lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n" +by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute) (* to do: differences, and all variations of addition rules as simplification rules for nat and int *) (* FIXME remove iff *) -lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n" +lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n" using mult_dvd_mono [of 1] by auto (* to do: add the three variations of these, and for ints? *) @@ -559,7 +559,7 @@ apply(rule Max_eqI[THEN sym]) apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat) apply simp - apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le nat_gcd_greatest_iff nat_gcd_pos) + apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat) apply simp done @@ -568,14 +568,14 @@ apply(rule Max_eqI[THEN sym]) apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int) apply simp - apply (metis int_gcd_greatest_iff int_gcd_pos zdvd_imp_le) + apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le) apply simp done subsection {* Coprimality *} -lemma nat_div_gcd_coprime: +lemma div_gcd_coprime_nat: assumes nz: "(a::nat) \ 0 \ b \ 0" shows "coprime (a div gcd a b) (b div gcd a b)" proof - @@ -593,34 +593,34 @@ then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def) - have "?g \ 0" using nz by (simp add: nat_gcd_zero) + have "?g \ 0" using nz by (simp add: gcd_zero_nat) then have gp: "?g > 0" by arith - from nat_gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . + from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" . with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp qed -lemma int_div_gcd_coprime: +lemma div_gcd_coprime_int: assumes nz: "(a::int) \ 0 \ b \ 0" shows "coprime (a div gcd a b) (b div gcd a b)" -apply (subst (1 2 3) int_gcd_abs) +apply (subst (1 2 3) gcd_abs_int) apply (subst (1 2) abs_div) apply simp apply simp apply(subst (1 2) abs_gcd_int) -apply (rule nat_div_gcd_coprime [transferred]) -using nz apply (auto simp add: int_gcd_abs [symmetric]) +apply (rule div_gcd_coprime_nat [transferred]) +using nz apply (auto simp add: gcd_abs_int [symmetric]) done -lemma nat_coprime: "coprime (a::nat) b \ (\d. d dvd a \ d dvd b \ d = 1)" - using nat_gcd_unique[of 1 a b, simplified] by auto +lemma coprime_nat: "coprime (a::nat) b \ (\d. d dvd a \ d dvd b \ d = 1)" + using gcd_unique_nat[of 1 a b, simplified] by auto -lemma nat_coprime_Suc_0: +lemma coprime_Suc_0_nat: "coprime (a::nat) b \ (\d. d dvd a \ d dvd b \ d = Suc 0)" - using nat_coprime by (simp add: One_nat_def) + using coprime_nat by (simp add: One_nat_def) -lemma int_coprime: "coprime (a::int) b \ +lemma coprime_int: "coprime (a::int) b \ (\d. d >= 0 \ d dvd a \ d dvd b \ d = 1)" - using int_gcd_unique [of 1 a b] + using gcd_unique_int [of 1 a b] apply clarsimp apply (erule subst) apply (rule iffI) @@ -631,7 +631,7 @@ apply force done -lemma nat_gcd_coprime: +lemma gcd_coprime_nat: assumes z: "gcd (a::nat) b \ 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b" shows "coprime a' b'" @@ -640,7 +640,7 @@ apply (erule ssubst) apply (subgoal_tac "b' = b div gcd a b") apply (erule ssubst) - apply (rule nat_div_gcd_coprime) + apply (rule div_gcd_coprime_nat) using prems apply force apply (subst (1) b) @@ -649,7 +649,7 @@ using z apply force done -lemma int_gcd_coprime: +lemma gcd_coprime_int: assumes z: "gcd (a::int) b \ 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b" shows "coprime a' b'" @@ -658,7 +658,7 @@ apply (erule ssubst) apply (subgoal_tac "b' = b div gcd a b") apply (erule ssubst) - apply (rule int_div_gcd_coprime) + apply (rule div_gcd_coprime_int) using prems apply force apply (subst (1) b) @@ -667,117 +667,117 @@ using z apply force done -lemma nat_coprime_mult: assumes da: "coprime (d::nat) a" and db: "coprime d b" +lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b" shows "coprime d (a * b)" - apply (subst nat_gcd_commute) - using da apply (subst nat_gcd_mult_cancel) - apply (subst nat_gcd_commute, assumption) - apply (subst nat_gcd_commute, rule db) + apply (subst gcd_commute_nat) + using da apply (subst gcd_mult_cancel_nat) + apply (subst gcd_commute_nat, assumption) + apply (subst gcd_commute_nat, rule db) done -lemma int_coprime_mult: assumes da: "coprime (d::int) a" and db: "coprime d b" +lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b" shows "coprime d (a * b)" - apply (subst int_gcd_commute) - using da apply (subst int_gcd_mult_cancel) - apply (subst int_gcd_commute, assumption) - apply (subst int_gcd_commute, rule db) + apply (subst gcd_commute_int) + using da apply (subst gcd_mult_cancel_int) + apply (subst gcd_commute_int, assumption) + apply (subst gcd_commute_int, rule db) done -lemma nat_coprime_lmult: +lemma coprime_lmult_nat: assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" proof - have "gcd d a dvd gcd d (a * b)" - by (rule nat_gcd_greatest, auto) + by (rule gcd_greatest_nat, auto) with dab show ?thesis by auto qed -lemma int_coprime_lmult: +lemma coprime_lmult_int: assumes "coprime (d::int) (a * b)" shows "coprime d a" proof - have "gcd d a dvd gcd d (a * b)" - by (rule int_gcd_greatest, auto) + by (rule gcd_greatest_int, auto) with assms show ?thesis by auto qed -lemma nat_coprime_rmult: +lemma coprime_rmult_nat: assumes "coprime (d::nat) (a * b)" shows "coprime d b" proof - have "gcd d b dvd gcd d (a * b)" - by (rule nat_gcd_greatest, auto intro: dvd_mult) + by (rule gcd_greatest_nat, auto intro: dvd_mult) with assms show ?thesis by auto qed -lemma int_coprime_rmult: +lemma coprime_rmult_int: assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" proof - have "gcd d b dvd gcd d (a * b)" - by (rule int_gcd_greatest, auto intro: dvd_mult) + by (rule gcd_greatest_int, auto intro: dvd_mult) with dab show ?thesis by auto qed -lemma nat_coprime_mul_eq: "coprime (d::nat) (a * b) \ +lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \ coprime d a \ coprime d b" - using nat_coprime_rmult[of d a b] nat_coprime_lmult[of d a b] - nat_coprime_mult[of d a b] + using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b] + coprime_mult_nat[of d a b] by blast -lemma int_coprime_mul_eq: "coprime (d::int) (a * b) \ +lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \ coprime d a \ coprime d b" - using int_coprime_rmult[of d a b] int_coprime_lmult[of d a b] - int_coprime_mult[of d a b] + using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b] + coprime_mult_int[of d a b] by blast -lemma nat_gcd_coprime_exists: +lemma gcd_coprime_exists_nat: assumes nz: "gcd (a::nat) b \ 0" shows "\a' b'. a = a' * gcd a b \ b = b' * gcd a b \ coprime a' b'" apply (rule_tac x = "a div gcd a b" in exI) apply (rule_tac x = "b div gcd a b" in exI) - using nz apply (auto simp add: nat_div_gcd_coprime dvd_div_mult) + using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult) done -lemma int_gcd_coprime_exists: +lemma gcd_coprime_exists_int: assumes nz: "gcd (a::int) b \ 0" shows "\a' b'. a = a' * gcd a b \ b = b' * gcd a b \ coprime a' b'" apply (rule_tac x = "a div gcd a b" in exI) apply (rule_tac x = "b div gcd a b" in exI) - using nz apply (auto simp add: int_div_gcd_coprime dvd_div_mult_self) + using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self) done -lemma nat_coprime_exp: "coprime (d::nat) a \ coprime d (a^n)" - by (induct n, simp_all add: nat_coprime_mult) +lemma coprime_exp_nat: "coprime (d::nat) a \ coprime d (a^n)" + by (induct n, simp_all add: coprime_mult_nat) -lemma int_coprime_exp: "coprime (d::int) a \ coprime d (a^n)" - by (induct n, simp_all add: int_coprime_mult) +lemma coprime_exp_int: "coprime (d::int) a \ coprime d (a^n)" + by (induct n, simp_all add: coprime_mult_int) -lemma nat_coprime_exp2 [intro]: "coprime (a::nat) b \ coprime (a^n) (b^m)" - apply (rule nat_coprime_exp) - apply (subst nat_gcd_commute) - apply (rule nat_coprime_exp) - apply (subst nat_gcd_commute, assumption) +lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \ coprime (a^n) (b^m)" + apply (rule coprime_exp_nat) + apply (subst gcd_commute_nat) + apply (rule coprime_exp_nat) + apply (subst gcd_commute_nat, assumption) done -lemma int_coprime_exp2 [intro]: "coprime (a::int) b \ coprime (a^n) (b^m)" - apply (rule int_coprime_exp) - apply (subst int_gcd_commute) - apply (rule int_coprime_exp) - apply (subst int_gcd_commute, assumption) +lemma coprime_exp2_int [intro]: "coprime (a::int) b \ coprime (a^n) (b^m)" + apply (rule coprime_exp_int) + apply (subst gcd_commute_int) + apply (rule coprime_exp_int) + apply (subst gcd_commute_int, assumption) done -lemma nat_gcd_exp: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n" +lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n" proof (cases) assume "a = 0 & b = 0" thus ?thesis by simp next assume "~(a = 0 & b = 0)" hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)" - by (auto simp:nat_div_gcd_coprime) + by (auto simp:div_gcd_coprime_nat) hence "gcd ((a div gcd a b)^n * (gcd a b)^n) ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" apply (subst (1 2) mult_commute) - apply (subst nat_gcd_mult_distrib [symmetric]) + apply (subst gcd_mult_distrib_nat [symmetric]) apply simp done also have "(a div gcd a b)^n * (gcd a b)^n = a^n" @@ -797,29 +797,29 @@ finally show ?thesis . qed -lemma int_gcd_exp: "gcd ((a::int)^n) (b^n) = (gcd a b)^n" - apply (subst (1 2) int_gcd_abs) +lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n" + apply (subst (1 2) gcd_abs_int) apply (subst (1 2) power_abs) - apply (rule nat_gcd_exp [where n = n, transferred]) + apply (rule gcd_exp_nat [where n = n, transferred]) apply auto done -lemma nat_coprime_divprod: "(d::nat) dvd a * b \ coprime d a \ d dvd b" - using nat_coprime_dvd_mult_iff[of d a b] +lemma coprime_divprod_nat: "(d::nat) dvd a * b \ coprime d a \ d dvd b" + using coprime_dvd_mult_iff_nat[of d a b] by (auto simp add: mult_commute) -lemma int_coprime_divprod: "(d::int) dvd a * b \ coprime d a \ d dvd b" - using int_coprime_dvd_mult_iff[of d a b] +lemma coprime_divprod_int: "(d::int) dvd a * b \ coprime d a \ d dvd b" + using coprime_dvd_mult_iff_int[of d a b] by (auto simp add: mult_commute) -lemma nat_division_decomp: assumes dc: "(a::nat) dvd b * c" +lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c" shows "\b' c'. a = b' * c' \ b' dvd b \ c' dvd c" proof- let ?g = "gcd a b" {assume "?g = 0" with dc have ?thesis by auto} moreover {assume z: "?g \ 0" - from nat_gcd_coprime_exists[OF z] + from gcd_coprime_exists_nat[OF z] obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" by blast have thb: "?g dvd b" by auto @@ -828,21 +828,21 @@ from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc) with z have th_1: "a' dvd b' * c" by auto - from nat_coprime_dvd_mult[OF ab'(3)] th_1 + from coprime_dvd_mult_nat[OF ab'(3)] th_1 have thc: "a' dvd c" by (subst (asm) mult_commute, blast) from ab' have "a = ?g*a'" by algebra with thb thc have ?thesis by blast } ultimately show ?thesis by blast qed -lemma int_division_decomp: assumes dc: "(a::int) dvd b * c" +lemma division_decomp_int: assumes dc: "(a::int) dvd b * c" shows "\b' c'. a = b' * c' \ b' dvd b \ c' dvd c" proof- let ?g = "gcd a b" {assume "?g = 0" with dc have ?thesis by auto} moreover {assume z: "?g \ 0" - from int_gcd_coprime_exists[OF z] + from gcd_coprime_exists_int[OF z] obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" by blast have thb: "?g dvd b" by auto @@ -852,14 +852,14 @@ from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc) with z have th_1: "a' dvd b' * c" by auto - from int_coprime_dvd_mult[OF ab'(3)] th_1 + from coprime_dvd_mult_int[OF ab'(3)] th_1 have thc: "a' dvd c" by (subst (asm) mult_commute, blast) from ab' have "a = ?g*a'" by algebra with thb thc have ?thesis by blast } ultimately show ?thesis by blast qed -lemma nat_pow_divides_pow: +lemma pow_divides_pow_nat: assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \ 0" shows "a dvd b" proof- @@ -869,7 +869,7 @@ moreover {assume z: "?g \ 0" hence zn: "?g ^ n \ 0" using n by (simp add: neq0_conv) - from nat_gcd_coprime_exists[OF z] + from gcd_coprime_exists_nat[OF z] obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" by blast from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" @@ -880,14 +880,14 @@ have "a' dvd a'^n" by (simp add: m) with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute) - from nat_coprime_dvd_mult[OF nat_coprime_exp [OF ab'(3), of m]] th1 + from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1 have "a' dvd b'" by (subst (asm) mult_commute, blast) hence "a'*?g dvd b'*?g" by simp with ab'(1,2) have ?thesis by simp } ultimately show ?thesis by blast qed -lemma int_pow_divides_pow: +lemma pow_divides_pow_int: assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \ 0" shows "a dvd b" proof- @@ -897,7 +897,7 @@ moreover {assume z: "?g \ 0" hence zn: "?g ^ n \ 0" using n by (simp add: neq0_conv) - from int_gcd_coprime_exists[OF z] + from gcd_coprime_exists_int[OF z] obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" by blast from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" @@ -909,7 +909,7 @@ with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute) - from int_coprime_dvd_mult[OF int_coprime_exp [OF ab'(3), of m]] th1 + from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1 have "a' dvd b'" by (subst (asm) mult_commute, blast) hence "a'*?g dvd b'*?g" by simp with ab'(1,2) have ?thesis by simp } @@ -917,76 +917,76 @@ qed (* FIXME move to Divides(?) *) -lemma nat_pow_divides_eq [simp]: "n ~= 0 \ ((a::nat)^n dvd b^n) = (a dvd b)" - by (auto intro: nat_pow_divides_pow dvd_power_same) +lemma pow_divides_eq_nat [simp]: "n ~= 0 \ ((a::nat)^n dvd b^n) = (a dvd b)" + by (auto intro: pow_divides_pow_nat dvd_power_same) -lemma int_pow_divides_eq [simp]: "n ~= 0 \ ((a::int)^n dvd b^n) = (a dvd b)" - by (auto intro: int_pow_divides_pow dvd_power_same) +lemma pow_divides_eq_int [simp]: "n ~= 0 \ ((a::int)^n dvd b^n) = (a dvd b)" + by (auto intro: pow_divides_pow_int dvd_power_same) -lemma nat_divides_mult: +lemma divides_mult_nat: assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n" shows "m * n dvd r" proof- from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'" unfolding dvd_def by blast from mr n' have "m dvd n'*n" by (simp add: mult_commute) - hence "m dvd n'" using nat_coprime_dvd_mult_iff[OF mn] by simp + hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp then obtain k where k: "n' = m*k" unfolding dvd_def by blast from n' k show ?thesis unfolding dvd_def by auto qed -lemma int_divides_mult: +lemma divides_mult_int: assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n" shows "m * n dvd r" proof- from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'" unfolding dvd_def by blast from mr n' have "m dvd n'*n" by (simp add: mult_commute) - hence "m dvd n'" using int_coprime_dvd_mult_iff[OF mn] by simp + hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp then obtain k where k: "n' = m*k" unfolding dvd_def by blast from n' k show ?thesis unfolding dvd_def by auto qed -lemma nat_coprime_plus_one [simp]: "coprime ((n::nat) + 1) n" +lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n" apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)") apply force - apply (rule nat_dvd_diff) + apply (rule dvd_diff_nat) apply auto done -lemma nat_coprime_Suc [simp]: "coprime (Suc n) n" - using nat_coprime_plus_one by (simp add: One_nat_def) +lemma coprime_Suc_nat [simp]: "coprime (Suc n) n" + using coprime_plus_one_nat by (simp add: One_nat_def) -lemma int_coprime_plus_one [simp]: "coprime ((n::int) + 1) n" +lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n" apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)") apply force apply (rule dvd_diff) apply auto done -lemma nat_coprime_minus_one: "(n::nat) \ 0 \ coprime (n - 1) n" - using nat_coprime_plus_one [of "n - 1"] - nat_gcd_commute [of "n - 1" n] by auto +lemma coprime_minus_one_nat: "(n::nat) \ 0 \ coprime (n - 1) n" + using coprime_plus_one_nat [of "n - 1"] + gcd_commute_nat [of "n - 1" n] by auto -lemma int_coprime_minus_one: "coprime ((n::int) - 1) n" - using int_coprime_plus_one [of "n - 1"] - int_gcd_commute [of "n - 1" n] by auto +lemma coprime_minus_one_int: "coprime ((n::int) - 1) n" + using coprime_plus_one_int [of "n - 1"] + gcd_commute_int [of "n - 1" n] by auto -lemma nat_setprod_coprime [rule_format]: +lemma setprod_coprime_nat [rule_format]: "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x" apply (case_tac "finite A") apply (induct set: finite) - apply (auto simp add: nat_gcd_mult_cancel) + apply (auto simp add: gcd_mult_cancel_nat) done -lemma int_setprod_coprime [rule_format]: +lemma setprod_coprime_int [rule_format]: "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x" apply (case_tac "finite A") apply (induct set: finite) - apply (auto simp add: int_gcd_mult_cancel) + apply (auto simp add: gcd_mult_cancel_int) done -lemma nat_prime_odd: "prime (p::nat) \ p > 2 \ odd p" +lemma prime_odd_nat: "prime (p::nat) \ p > 2 \ odd p" unfolding prime_nat_def apply (subst even_mult_two_ex) apply clarify @@ -994,41 +994,41 @@ apply auto done -lemma int_prime_odd: "prime (p::int) \ p > 2 \ odd p" +lemma prime_odd_int: "prime (p::int) \ p > 2 \ odd p" unfolding prime_int_def - apply (frule nat_prime_odd) + apply (frule prime_odd_nat) apply (auto simp add: even_nat_def) done -lemma nat_coprime_common_divisor: "coprime (a::nat) b \ x dvd a \ +lemma coprime_common_divisor_nat: "coprime (a::nat) b \ x dvd a \ x dvd b \ x = 1" apply (subgoal_tac "x dvd gcd a b") apply simp - apply (erule (1) nat_gcd_greatest) + apply (erule (1) gcd_greatest_nat) done -lemma int_coprime_common_divisor: "coprime (a::int) b \ x dvd a \ +lemma coprime_common_divisor_int: "coprime (a::int) b \ x dvd a \ x dvd b \ abs x = 1" apply (subgoal_tac "x dvd gcd a b") apply simp - apply (erule (1) int_gcd_greatest) + apply (erule (1) gcd_greatest_int) done -lemma nat_coprime_divisors: "(d::int) dvd a \ e dvd b \ coprime a b \ +lemma coprime_divisors_nat: "(d::int) dvd a \ e dvd b \ coprime a b \ coprime d e" apply (auto simp add: dvd_def) - apply (frule int_coprime_lmult) - apply (subst int_gcd_commute) - apply (subst (asm) (2) int_gcd_commute) - apply (erule int_coprime_lmult) + apply (frule coprime_lmult_int) + apply (subst gcd_commute_int) + apply (subst (asm) (2) gcd_commute_int) + apply (erule coprime_lmult_int) done -lemma nat_invertible_coprime: "(x::nat) * y mod m = 1 \ coprime x m" -apply (metis nat_coprime_lmult nat_gcd_1 nat_gcd_commute nat_gcd_red) +lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \ coprime x m" +apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat) done -lemma int_invertible_coprime: "(x::int) * y mod m = 1 \ coprime x m" -apply (metis int_coprime_lmult int_gcd_1 int_gcd_commute int_gcd_red) +lemma invertible_coprime_int: "(x::int) * y mod m = 1 \ coprime x m" +apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int) done @@ -1054,7 +1054,7 @@ lemma bezw_aux [rule_format]: "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)" -proof (induct x y rule: nat_gcd_induct) +proof (induct x y rule: gcd_nat_induct) fix m :: nat show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)" by auto @@ -1064,7 +1064,7 @@ snd (bezw n (m mod n)) * int (m mod n) = int (gcd n (m mod n))" thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)" - apply (simp add: bezw_non_0 nat_gcd_non_0) + apply (simp add: bezw_non_0 gcd_non_0_nat) apply (erule subst) apply (simp add: ring_simps) apply (subst mod_div_equality [of m n, symmetric]) @@ -1075,7 +1075,7 @@ done qed -lemma int_bezout: +lemma bezout_int: fixes x y shows "EX u v. u * (x::int) + v * y = gcd x y" proof - @@ -1098,7 +1098,7 @@ apply auto apply (rule_tac x = u in exI) apply (rule_tac x = "-v" in exI) - apply (subst int_gcd_neg2 [symmetric]) + apply (subst gcd_neg2_int [symmetric]) apply auto done moreover have "x <= 0 \ y >= 0 \ ?thesis" @@ -1106,7 +1106,7 @@ apply auto apply (rule_tac x = "-u" in exI) apply (rule_tac x = v in exI) - apply (subst int_gcd_neg1 [symmetric]) + apply (subst gcd_neg1_int [symmetric]) apply auto done moreover have "x <= 0 \ y <= 0 \ ?thesis" @@ -1114,8 +1114,8 @@ apply auto apply (rule_tac x = "-u" in exI) apply (rule_tac x = "-v" in exI) - apply (subst int_gcd_neg1 [symmetric]) - apply (subst int_gcd_neg2 [symmetric]) + apply (subst gcd_neg1_int [symmetric]) + apply (subst gcd_neg2_int [symmetric]) apply auto done ultimately show ?thesis by blast @@ -1160,7 +1160,7 @@ ultimately show "P a b" by blast qed -lemma nat_bezout_lemma: +lemma bezout_lemma_nat: assumes ex: "\(d::nat) x y. d dvd a \ d dvd b \ (a * x = b * y + d \ b * x = a * y + d)" shows "\d x y. d dvd a \ d dvd a + b \ @@ -1177,7 +1177,7 @@ apply algebra done -lemma nat_bezout_add: "\(d::nat) x y. d dvd a \ d dvd b \ +lemma bezout_add_nat: "\(d::nat) x y. d dvd a \ d dvd b \ (a * x = b * y + d \ b * x = a * y + d)" apply(induct a b rule: ind_euclid) apply blast @@ -1194,9 +1194,9 @@ apply algebra done -lemma nat_bezout1: "\(d::nat) x y. d dvd a \ d dvd b \ +lemma bezout1_nat: "\(d::nat) x y. d dvd a \ d dvd b \ (a * x - b * y = d \ b * x - a * y = d)" - using nat_bezout_add[of a b] + using bezout_add_nat[of a b] apply clarsimp apply (rule_tac x="d" in exI, simp) apply (rule_tac x="x" in exI) @@ -1204,11 +1204,11 @@ apply auto done -lemma nat_bezout_add_strong: assumes nz: "a \ (0::nat)" +lemma bezout_add_strong_nat: assumes nz: "a \ (0::nat)" shows "\d x y. d dvd a \ d dvd b \ a * x = b * y + d" proof- from nz have ap: "a > 0" by simp - from nat_bezout_add[of a b] + from bezout_add_nat[of a b] have "(\d x y. d dvd a \ d dvd b \ a * x = b * y + d) \ (\d x y. d dvd a \ d dvd b \ b * x = a * y + d)" by blast moreover @@ -1258,11 +1258,11 @@ ultimately show ?thesis by blast qed -lemma nat_bezout: assumes a: "(a::nat) \ 0" +lemma bezout_nat: assumes a: "(a::nat) \ 0" shows "\x y. a * x = b * y + gcd a b" proof- let ?g = "gcd a b" - from nat_bezout_add_strong[OF a, of b] + from bezout_add_strong_nat[OF a, of b] obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast from d(1,2) have "d dvd ?g" by simp then obtain k where k: "?g = d*k" unfolding dvd_def by blast @@ -1274,99 +1274,99 @@ subsection {* LCM *} -lemma int_lcm_altdef: "lcm (a::int) b = (abs a) * (abs b) div gcd a b" +lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b" by (simp add: lcm_int_def lcm_nat_def zdiv_int zmult_int [symmetric] gcd_int_def) -lemma nat_prod_gcd_lcm: "(m::nat) * n = gcd m n * lcm m n" +lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n" unfolding lcm_nat_def - by (simp add: dvd_mult_div_cancel [OF nat_gcd_dvd_prod]) + by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat]) -lemma int_prod_gcd_lcm: "abs(m::int) * abs n = gcd m n * lcm m n" +lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n" unfolding lcm_int_def gcd_int_def apply (subst int_mult [symmetric]) - apply (subst nat_prod_gcd_lcm [symmetric]) + apply (subst prod_gcd_lcm_nat [symmetric]) apply (subst nat_abs_mult_distrib [symmetric]) apply (simp, simp add: abs_mult) done -lemma nat_lcm_0 [simp]: "lcm (m::nat) 0 = 0" +lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0" unfolding lcm_nat_def by simp -lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0" +lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0" unfolding lcm_int_def by simp -lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0" +lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0" unfolding lcm_nat_def by simp -lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0" +lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0" unfolding lcm_int_def by simp -lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m" - unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps) +lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m" + unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps) -lemma int_lcm_commute: "lcm (m::int) n = lcm n m" - unfolding lcm_int_def by (subst nat_lcm_commute, rule refl) +lemma lcm_commute_int: "lcm (m::int) n = lcm n m" + unfolding lcm_int_def by (subst lcm_commute_nat, rule refl) -lemma nat_lcm_pos: +lemma lcm_pos_nat: "(m::nat) > 0 \ n>0 \ lcm m n > 0" -by (metis gr0I mult_is_0 nat_prod_gcd_lcm) +by (metis gr0I mult_is_0 prod_gcd_lcm_nat) -lemma int_lcm_pos: +lemma lcm_pos_int: "(m::int) ~= 0 \ n ~= 0 \ lcm m n > 0" - apply (subst int_lcm_abs) - apply (rule nat_lcm_pos [transferred]) + apply (subst lcm_abs_int) + apply (rule lcm_pos_nat [transferred]) apply auto done -lemma nat_dvd_pos: +lemma dvd_pos_nat: fixes n m :: nat assumes "n > 0" and "m dvd n" shows "m > 0" using assms by (cases m) auto -lemma nat_lcm_least: +lemma lcm_least_nat: assumes "(m::nat) dvd k" and "n dvd k" shows "lcm m n dvd k" proof (cases k) case 0 then show ?thesis by auto next case (Suc _) then have pos_k: "k > 0" by auto - from assms nat_dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto - with nat_gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp + from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto + with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp from assms obtain p where k_m: "k = m * p" using dvd_def by blast from assms obtain q where k_n: "k = n * q" using dvd_def by blast from pos_k k_m have pos_p: "p > 0" by auto from pos_k k_n have pos_q: "q > 0" by auto have "k * k * gcd q p = k * gcd (k * q) (k * p)" - by (simp add: mult_ac nat_gcd_mult_distrib) + by (simp add: mult_ac gcd_mult_distrib_nat) also have "\ = k * gcd (m * p * q) (n * q * p)" by (simp add: k_m [symmetric] k_n [symmetric]) also have "\ = k * p * q * gcd m n" - by (simp add: mult_ac nat_gcd_mult_distrib) + by (simp add: mult_ac gcd_mult_distrib_nat) finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n" by (simp only: k_m [symmetric] k_n [symmetric]) then have "p * q * m * n * gcd q p = p * q * k * gcd m n" by (simp add: mult_ac) with pos_p pos_q have "m * n * gcd q p = k * gcd m n" by simp - with nat_prod_gcd_lcm [of m n] + with prod_gcd_lcm_nat [of m n] have "lcm m n * gcd q p * gcd m n = k * gcd m n" by (simp add: mult_ac) with pos_gcd have "lcm m n * gcd q p = k" by auto then show ?thesis using dvd_def by auto qed -lemma int_lcm_least: +lemma lcm_least_int: "(m::int) dvd k \ n dvd k \ lcm m n dvd k" -apply (subst int_lcm_abs) +apply (subst lcm_abs_int) apply (rule dvd_trans) -apply (rule nat_lcm_least [transferred, of _ "abs k" _]) +apply (rule lcm_least_nat [transferred, of _ "abs k" _]) apply auto done -lemma nat_lcm_dvd1: "(m::nat) dvd lcm m n" +lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n" proof (cases m) case 0 then show ?thesis by simp next @@ -1382,82 +1382,82 @@ then obtain k where "n = gcd m n * k" using dvd_def by auto then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n" by (simp add: mult_ac) - also have "\ = m * k" using mpos npos nat_gcd_zero by simp + also have "\ = m * k" using mpos npos gcd_zero_nat by simp finally show ?thesis by (simp add: lcm_nat_def) qed qed -lemma int_lcm_dvd1: "(m::int) dvd lcm m n" - apply (subst int_lcm_abs) +lemma lcm_dvd1_int: "(m::int) dvd lcm m n" + apply (subst lcm_abs_int) apply (rule dvd_trans) prefer 2 - apply (rule nat_lcm_dvd1 [transferred]) + apply (rule lcm_dvd1_nat [transferred]) apply auto done -lemma nat_lcm_dvd2: "(n::nat) dvd lcm m n" - by (subst nat_lcm_commute, rule nat_lcm_dvd1) +lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n" + by (subst lcm_commute_nat, rule lcm_dvd1_nat) -lemma int_lcm_dvd2: "(n::int) dvd lcm m n" - by (subst int_lcm_commute, rule int_lcm_dvd1) +lemma lcm_dvd2_int: "(n::int) dvd lcm m n" + by (subst lcm_commute_int, rule lcm_dvd1_int) lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \ k dvd lcm m n" -by(metis nat_lcm_dvd1 dvd_trans) +by(metis lcm_dvd1_nat dvd_trans) lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \ k dvd lcm m n" -by(metis nat_lcm_dvd2 dvd_trans) +by(metis lcm_dvd2_nat dvd_trans) lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \ i dvd lcm m n" -by(metis int_lcm_dvd1 dvd_trans) +by(metis lcm_dvd1_int dvd_trans) lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \ i dvd lcm m n" -by(metis int_lcm_dvd2 dvd_trans) +by(metis lcm_dvd2_int dvd_trans) -lemma nat_lcm_unique: "(a::nat) dvd d \ b dvd d \ +lemma lcm_unique_nat: "(a::nat) dvd d \ b dvd d \ (\e. a dvd e \ b dvd e \ d dvd e) \ d = lcm a b" - by (auto intro: dvd_anti_sym nat_lcm_least nat_lcm_dvd1 nat_lcm_dvd2) + by (auto intro: dvd_anti_sym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat) -lemma int_lcm_unique: "d >= 0 \ (a::int) dvd d \ b dvd d \ +lemma lcm_unique_int: "d >= 0 \ (a::int) dvd d \ b dvd d \ (\e. a dvd e \ b dvd e \ d dvd e) \ d = lcm a b" - by (auto intro: dvd_anti_sym [transferred] int_lcm_least) + by (auto intro: dvd_anti_sym [transferred] lcm_least_int) lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \ lcm x y = y" apply (rule sym) - apply (subst nat_lcm_unique [symmetric]) + apply (subst lcm_unique_nat [symmetric]) apply auto done lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \ lcm x y = abs y" apply (rule sym) - apply (subst int_lcm_unique [symmetric]) + apply (subst lcm_unique_int [symmetric]) apply auto done lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \ lcm y x = y" -by (subst nat_lcm_commute, erule lcm_proj2_if_dvd_nat) +by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat) lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \ lcm y x = abs y" -by (subst int_lcm_commute, erule lcm_proj2_if_dvd_int) +by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int) lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)" -apply(rule nat_lcm_unique[THEN iffD1]) -apply (metis dvd.order_trans nat_lcm_unique) +apply(rule lcm_unique_nat[THEN iffD1]) +apply (metis dvd.order_trans lcm_unique_nat) done lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)" -apply(rule int_lcm_unique[THEN iffD1]) -apply (metis dvd_trans int_lcm_unique) +apply(rule lcm_unique_int[THEN iffD1]) +apply (metis dvd_trans lcm_unique_int) done lemmas lcm_left_commute_nat = - mk_left_commute[of lcm, OF lcm_assoc_nat nat_lcm_commute] + mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat] lemmas lcm_left_commute_int = - mk_left_commute[of lcm, OF lcm_assoc_int int_lcm_commute] + mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int] -lemmas lcm_ac_nat = lcm_assoc_nat nat_lcm_commute lcm_left_commute_nat -lemmas lcm_ac_int = lcm_assoc_int int_lcm_commute lcm_left_commute_int +lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat +lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int subsection {* Primes *} @@ -1465,40 +1465,40 @@ (* Is there a better way to handle these, rather than making them elim rules? *) -lemma nat_prime_ge_0 [elim]: "prime (p::nat) \ p >= 0" +lemma prime_ge_0_nat [elim]: "prime (p::nat) \ p >= 0" by (unfold prime_nat_def, auto) -lemma nat_prime_gt_0 [elim]: "prime (p::nat) \ p > 0" +lemma prime_gt_0_nat [elim]: "prime (p::nat) \ p > 0" by (unfold prime_nat_def, auto) -lemma nat_prime_ge_1 [elim]: "prime (p::nat) \ p >= 1" +lemma prime_ge_1_nat [elim]: "prime (p::nat) \ p >= 1" by (unfold prime_nat_def, auto) -lemma nat_prime_gt_1 [elim]: "prime (p::nat) \