--- 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
--- 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 \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
- \<delta> :: "fm \<Rightarrow> int" (* Compute lcm {d| N\<^isup>?\<^isup> Dvd c*x+t \<in> p}*)
+ \<delta> :: "fm \<Rightarrow> int" (* Compute lcm {d| N\<^isup>? Dvd c*x+t \<in> p}*)
d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> 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 = "\<delta> (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: "\<delta> p dvd \<delta> (And p q)" using prems by simp
hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp only: iszlfm.simps)
have "\<delta> q dvd \<delta> (And p q)" using prems by simp
@@ -1113,7 +1113,7 @@
next
case (2 p q)
let ?d = "\<delta> (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 "\<delta> p dvd \<delta> (And p q)" using prems by simp
hence th: "d\<delta> p ?d" using delta_mono prems by(simp only: iszlfm.simps)
have "\<delta> q dvd \<delta> (And p q)" using prems by simp
@@ -1410,15 +1410,15 @@
from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> 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: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> 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\<beta>: assumes linp: "iszlfm p" and d: "d\<beta> p l" and lp: "l > 0"
shows "iszlfm (a\<beta> p l) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a\<beta> p l) = Ifm bbs (x#bs) p)"
--- 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' \<noteq> 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 \<or> ?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' \<noteq> 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 \<or> ?g' > 1" by arith
moreover {assume "?g'=1" hence ?thesis using prems
by (auto simp add: Let_def simp_num_pair_def simpnum_numbound0)}
--- 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' \<noteq> 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 \<or> ?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' \<noteq> 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 \<or> ?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' \<noteq> 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 \<or> ?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 = "\<delta> (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: "\<delta> p dvd \<delta> (And p q)" using prems by simp
hence th: "d\<delta> p ?d"
using delta_mono prems by(simp only: iszlfm.simps) blast
@@ -2136,7 +2136,7 @@
next
case (2 p q)
let ?d = "\<delta> (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 "\<delta> p dvd \<delta> (And p q)" using prems by simp hence th: "d\<delta> p ?d" using delta_mono prems
by(simp only: iszlfm.simps) blast
have "\<delta> q dvd \<delta> (And p q)" using prems by simp hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast
@@ -2514,15 +2514,15 @@
from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> 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: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> 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\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d\<beta> p l" and lp: "l > 0"
shows "iszlfm (a\<beta> p l) (a #bs) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm (real (l * x) #bs) (a\<beta> 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 \<le> 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
--- 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" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> 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\<le>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
--- 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 \<le> 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
--- 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 "\<And>m. P m 0"
and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> 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 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> 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 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> 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) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
+lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> 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 \<Longrightarrow> (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 \<Longrightarrow> (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 \<Longrightarrow> (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 \<Longrightarrow> (i::int) dvd n"
-by(metis int_gcd_dvd2 dvd_trans)
+by(metis gcd_dvd2_int dvd_trans)
-lemma nat_gcd_le1 [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
+lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
by (rule dvd_imp_le, auto)
-lemma nat_gcd_le2 [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
+lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
by (rule dvd_imp_le, auto)
-lemma int_gcd_le1 [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
+lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
by (rule zdvd_imp_le, auto)
-lemma int_gcd_le2 [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
+lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
by (rule zdvd_imp_le, auto)
-lemma nat_gcd_greatest: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> 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 \<Longrightarrow> k dvd n \<Longrightarrow> 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 \<Longrightarrow> k dvd n \<Longrightarrow> 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 \<and> d dvd b \<and>
+lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> 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 \<and> d dvd b \<and>
+lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
- apply (insert nat_gcd_mult_distrib [of m k n])
+lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> 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 \<Longrightarrow> k dvd m * n \<Longrightarrow> 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 \<Longrightarrow>
+lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
(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 \<Longrightarrow>
+lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
(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 \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
+lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> gcd (m - n) n = gcd m n"
- by (subst nat_gcd_add1 [symmetric], auto)
+lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
+ by (subst gcd_add1_nat [symmetric], auto)
-lemma nat_gcd_diff2: "(n::nat) >= m \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> gcd x y = gcd y (x mod y)"
+lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> 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) \<noteq> 0 \<or> b \<noteq> 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 \<noteq> 0" using nz by (simp add: nat_gcd_zero)
+ have "?g \<noteq> 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) \<noteq> 0 \<or> b \<noteq> 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 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
- using nat_gcd_unique[of 1 a b, simplified] by auto
+lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> 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 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> 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 \<longleftrightarrow>
+lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
(\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> 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 \<noteq> 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 \<noteq> 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) \<longleftrightarrow>
+lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
coprime d a \<and> 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) \<longleftrightarrow>
+lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
coprime d a \<and> 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 \<noteq> 0"
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> 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 \<noteq> 0"
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> 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 \<Longrightarrow> coprime d (a^n)"
- by (induct n, simp_all add: nat_coprime_mult)
+lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
+ by (induct n, simp_all add: coprime_mult_nat)
-lemma int_coprime_exp: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
- by (induct n, simp_all add: int_coprime_mult)
+lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
+ by (induct n, simp_all add: coprime_mult_int)
-lemma nat_coprime_exp2 [intro]: "coprime (a::nat) b \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
- using nat_coprime_dvd_mult_iff[of d a b]
+lemma coprime_divprod_nat: "(d::nat) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> 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 \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
- using int_coprime_dvd_mult_iff[of d a b]
+lemma coprime_divprod_int: "(d::int) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> 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 "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
proof-
let ?g = "gcd a b"
{assume "?g = 0" with dc have ?thesis by auto}
moreover
{assume z: "?g \<noteq> 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 "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
proof-
let ?g = "gcd a b"
{assume "?g = 0" with dc have ?thesis by auto}
moreover
{assume z: "?g \<noteq> 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 \<noteq> 0"
shows "a dvd b"
proof-
@@ -869,7 +869,7 @@
moreover
{assume z: "?g \<noteq> 0"
hence zn: "?g ^ n \<noteq> 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 \<noteq> 0"
shows "a dvd b"
proof-
@@ -897,7 +897,7 @@
moreover
{assume z: "?g \<noteq> 0"
hence zn: "?g ^ n \<noteq> 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 \<Longrightarrow> ((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 \<Longrightarrow> ((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 \<Longrightarrow> ((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 \<Longrightarrow> ((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) \<noteq> 0 \<Longrightarrow> 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) \<noteq> 0 \<Longrightarrow> 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) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
+lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> 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) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
+lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> 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 \<Longrightarrow> x dvd a \<Longrightarrow>
+lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
x dvd b \<Longrightarrow> 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 \<Longrightarrow> x dvd a \<Longrightarrow>
+lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
x dvd b \<Longrightarrow> 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 \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
+lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> y >= 0 \<Longrightarrow> ?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 \<Longrightarrow> y <= 0 \<Longrightarrow> ?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: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
(a * x = b * y + d \<or> b * x = a * y + d)"
shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
@@ -1177,7 +1177,7 @@
apply algebra
done
-lemma nat_bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
+lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
(a * x = b * y + d \<or> b * x = a * y + d)"
apply(induct a b rule: ind_euclid)
apply blast
@@ -1194,9 +1194,9 @@
apply algebra
done
-lemma nat_bezout1: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
+lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
(a * x - b * y = d \<or> 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 \<noteq> (0::nat)"
+lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> 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 "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
(\<exists>d x y. d dvd a \<and> d dvd b \<and> 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) \<noteq> 0"
+lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
shows "\<exists>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 \<Longrightarrow> n>0 \<Longrightarrow> 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 \<Longrightarrow> n ~= 0 \<Longrightarrow> 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 "\<dots> = k * gcd (m * p * q) (n * q * p)"
by (simp add: k_m [symmetric] k_n [symmetric])
also have "\<dots> = 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 \<Longrightarrow> n dvd k \<Longrightarrow> 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 "\<dots> = m * k" using mpos npos nat_gcd_zero by simp
+ also have "\<dots> = 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<and> b dvd d \<and>
+lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> 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 \<and> (a::int) dvd d \<and> b dvd d \<and>
+lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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) \<Longrightarrow> p >= 0"
+lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
by (unfold prime_nat_def, auto)
-lemma nat_prime_gt_0 [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
+lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
by (unfold prime_nat_def, auto)
-lemma nat_prime_ge_1 [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
+lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
by (unfold prime_nat_def, auto)
-lemma nat_prime_gt_1 [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
+lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
by (unfold prime_nat_def, auto)
-lemma nat_prime_ge_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
+lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
by (unfold prime_nat_def, auto)
-lemma nat_prime_gt_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
+lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
by (unfold prime_nat_def, auto)
-lemma nat_prime_ge_2 [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
+lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
by (unfold prime_nat_def, auto)
-lemma int_prime_ge_0 [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
+lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
by (unfold prime_int_def prime_nat_def, auto)
-lemma int_prime_gt_0 [elim]: "prime (p::int) \<Longrightarrow> p > 0"
+lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
by (unfold prime_int_def prime_nat_def, auto)
-lemma int_prime_ge_1 [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
+lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
by (unfold prime_int_def prime_nat_def, auto)
-lemma int_prime_gt_1 [elim]: "prime (p::int) \<Longrightarrow> p > 1"
+lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
by (unfold prime_int_def prime_nat_def, auto)
-lemma int_prime_ge_2 [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
+lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
by (unfold prime_int_def prime_nat_def, auto)
thm prime_nat_def;
@@ -1508,59 +1508,59 @@
m = 1 \<or> m = p))"
using prime_nat_def [transferred]
apply (case_tac "p >= 0")
- by (blast, auto simp add: int_prime_ge_0)
+ by (blast, auto simp add: prime_ge_0_int)
(* To do: determine primality of any numeral *)
-lemma nat_zero_not_prime [simp]: "~prime (0::nat)"
+lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
by (simp add: prime_nat_def)
-lemma int_zero_not_prime [simp]: "~prime (0::int)"
+lemma zero_not_prime_int [simp]: "~prime (0::int)"
by (simp add: prime_int_def)
-lemma nat_one_not_prime [simp]: "~prime (1::nat)"
+lemma one_not_prime_nat [simp]: "~prime (1::nat)"
by (simp add: prime_nat_def)
-lemma nat_Suc_0_not_prime [simp]: "~prime (Suc 0)"
+lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
by (simp add: prime_nat_def One_nat_def)
-lemma int_one_not_prime [simp]: "~prime (1::int)"
+lemma one_not_prime_int [simp]: "~prime (1::int)"
by (simp add: prime_int_def)
-lemma nat_two_is_prime [simp]: "prime (2::nat)"
+lemma two_is_prime_nat [simp]: "prime (2::nat)"
apply (auto simp add: prime_nat_def)
apply (case_tac m)
apply (auto dest!: dvd_imp_le)
done
-lemma int_two_is_prime [simp]: "prime (2::int)"
- by (rule nat_two_is_prime [transferred direction: nat "op <= (0::int)"])
+lemma two_is_prime_int [simp]: "prime (2::int)"
+ by (rule two_is_prime_nat [transferred direction: nat "op <= (0::int)"])
-lemma nat_prime_imp_coprime: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
+lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
apply (unfold prime_nat_def)
- apply (metis nat_gcd_dvd1 nat_gcd_dvd2)
+ apply (metis gcd_dvd1_nat gcd_dvd2_nat)
done
-lemma int_prime_imp_coprime: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
+lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
apply (unfold prime_int_altdef)
- apply (metis int_gcd_dvd1 int_gcd_dvd2 int_gcd_ge_0)
+ apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
done
-lemma nat_prime_dvd_mult: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
- by (blast intro: nat_coprime_dvd_mult nat_prime_imp_coprime)
+lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
+ by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
-lemma int_prime_dvd_mult: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
- by (blast intro: int_coprime_dvd_mult int_prime_imp_coprime)
+lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
+ by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
-lemma nat_prime_dvd_mult_eq [simp]: "prime (p::nat) \<Longrightarrow>
+lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
p dvd m * n = (p dvd m \<or> p dvd n)"
- by (rule iffI, rule nat_prime_dvd_mult, auto)
+ by (rule iffI, rule prime_dvd_mult_nat, auto)
-lemma int_prime_dvd_mult_eq [simp]: "prime (p::int) \<Longrightarrow>
+lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
p dvd m * n = (p dvd m \<or> p dvd n)"
- by (rule iffI, rule int_prime_dvd_mult, auto)
+ by (rule iffI, rule prime_dvd_mult_int, auto)
-lemma nat_not_prime_eq_prod: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
+lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
unfolding prime_nat_def dvd_def apply auto
apply (subgoal_tac "k > 1")
@@ -1573,7 +1573,7 @@
(* there's a lot of messing around with signs of products here --
could this be made more automatic? *)
-lemma int_not_prime_eq_prod: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
+lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
unfolding prime_int_altdef dvd_def
apply auto
@@ -1593,72 +1593,72 @@
apply auto
done
-lemma nat_prime_dvd_power [rule_format]: "prime (p::nat) -->
+lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
n > 0 --> (p dvd x^n --> p dvd x)"
by (induct n rule: nat_induct, auto)
-lemma int_prime_dvd_power [rule_format]: "prime (p::int) -->
+lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
n > 0 --> (p dvd x^n --> p dvd x)"
apply (induct n rule: nat_induct, auto)
- apply (frule int_prime_ge_0)
+ apply (frule prime_ge_0_int)
apply auto
done
-lemma nat_prime_imp_power_coprime: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
+lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
coprime a (p^m)"
- apply (rule nat_coprime_exp)
- apply (subst nat_gcd_commute)
- apply (erule (1) nat_prime_imp_coprime)
+ apply (rule coprime_exp_nat)
+ apply (subst gcd_commute_nat)
+ apply (erule (1) prime_imp_coprime_nat)
done
-lemma int_prime_imp_power_coprime: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
+lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
coprime a (p^m)"
- apply (rule int_coprime_exp)
- apply (subst int_gcd_commute)
- apply (erule (1) int_prime_imp_coprime)
+ apply (rule coprime_exp_int)
+ apply (subst gcd_commute_int)
+ apply (erule (1) prime_imp_coprime_int)
done
-lemma nat_primes_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
- apply (rule nat_prime_imp_coprime, assumption)
+lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
+ apply (rule prime_imp_coprime_nat, assumption)
apply (unfold prime_nat_def, auto)
done
-lemma int_primes_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
- apply (rule int_prime_imp_coprime, assumption)
+lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
+ apply (rule prime_imp_coprime_int, assumption)
apply (unfold prime_int_altdef, clarify)
apply (drule_tac x = q in spec)
apply (drule_tac x = p in spec)
apply auto
done
-lemma nat_primes_imp_powers_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
+lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
coprime (p^m) (q^n)"
- by (rule nat_coprime_exp2, rule nat_primes_coprime)
+ by (rule coprime_exp2_nat, rule primes_coprime_nat)
-lemma int_primes_imp_powers_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
+lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
coprime (p^m) (q^n)"
- by (rule int_coprime_exp2, rule int_primes_coprime)
+ by (rule coprime_exp2_int, rule primes_coprime_int)
-lemma nat_prime_factor: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
+lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
apply (induct n rule: nat_less_induct)
apply (case_tac "n = 0")
- using nat_two_is_prime apply blast
+ using two_is_prime_nat apply blast
apply (case_tac "prime n")
apply blast
apply (subgoal_tac "n > 1")
- apply (frule (1) nat_not_prime_eq_prod)
+ apply (frule (1) not_prime_eq_prod_nat)
apply (auto intro: dvd_mult dvd_mult2)
done
(* An Isar version:
-lemma nat_prime_factor_b:
+lemma prime_factor_b_nat:
fixes n :: nat
assumes "n \<noteq> 1"
shows "\<exists>p. prime p \<and> p dvd n"
using `n ~= 1`
-proof (induct n rule: nat_less_induct)
+proof (induct n rule: less_induct_nat)
fix n :: nat
assume "n ~= 1" and
ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
@@ -1666,9 +1666,9 @@
proof -
{
assume "n = 0"
- moreover note nat_two_is_prime
+ moreover note two_is_prime_nat
ultimately have ?thesis
- by (auto simp del: nat_two_is_prime)
+ by (auto simp del: two_is_prime_nat)
}
moreover
{
@@ -1679,7 +1679,7 @@
{
assume "n ~= 0" and "~ prime n"
with `n ~= 1` have "n > 1" by auto
- with `~ prime n` and nat_not_prime_eq_prod obtain m k where
+ with `~ prime n` and not_prime_eq_prod_nat obtain m k where
"n = m * k" and "1 < m" and "m < n" by blast
with ih obtain p where "prime p" and "p dvd m" by blast
with `n = m * k` have ?thesis by auto
@@ -1692,7 +1692,7 @@
text {* One property of coprimality is easier to prove via prime factors. *}
-lemma nat_prime_divprod_pow:
+lemma prime_divprod_pow_nat:
assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
shows "p^n dvd a \<or> p^n dvd b"
proof-
@@ -1705,27 +1705,27 @@
from n have "p dvd p^n" by (intro dvd_power, auto)
also note pab
finally have pab': "p dvd a * b".
- from nat_prime_dvd_mult[OF p pab']
+ from prime_dvd_mult_nat[OF p pab']
have "p dvd a \<or> p dvd b" .
moreover
{assume pa: "p dvd a"
have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
- from nat_coprime_common_divisor [OF ab, OF pa] p have "\<not> p dvd b" by auto
+ from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
with p have "coprime b p"
- by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
+ by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
hence pnb: "coprime (p^n) b"
- by (subst nat_gcd_commute, rule nat_coprime_exp)
- from nat_coprime_divprod[OF pnba pnb] have ?thesis by blast }
+ by (subst gcd_commute_nat, rule coprime_exp_nat)
+ from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
moreover
{assume pb: "p dvd b"
have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
- from nat_coprime_common_divisor [OF ab, of p] pb p have "\<not> p dvd a"
+ from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
by auto
with p have "coprime a p"
- by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
+ by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
hence pna: "coprime (p^n) a"
- by (subst nat_gcd_commute, rule nat_coprime_exp)
- from nat_coprime_divprod[OF pab pna] have ?thesis by blast }
+ by (subst gcd_commute_nat, rule coprime_exp_nat)
+ from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
ultimately have ?thesis by blast}
ultimately show ?thesis by blast
qed
--- a/src/HOL/Library/Abstract_Rat.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy Tue Jul 07 21:26:08 2009 +0200
@@ -30,8 +30,8 @@
(let g = gcd a b
in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
-declare int_gcd_dvd1[presburger]
-declare int_gcd_dvd2[presburger]
+declare gcd_dvd1_int[presburger]
+declare gcd_dvd2_int[presburger]
lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
proof -
have " \<exists> a b. x = (a,b)" by auto
@@ -43,7 +43,7 @@
let ?a' = "a div ?g"
let ?b' = "b div ?g"
let ?g' = "gcd ?a' ?b'"
- from anz bnz have "?g \<noteq> 0" by simp with int_gcd_ge_0[of a b]
+ from anz bnz have "?g \<noteq> 0" by simp with gcd_ge_0_int[of a b]
have gpos: "?g > 0" by arith
have gdvd: "?g dvd a" "?g dvd b" by arith+
from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
@@ -51,7 +51,7 @@
have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
by - (rule notI, simp)+
from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
- from int_div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
+ from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
from bnz have "b < 0 \<or> b > 0" by arith
moreover
{assume b: "b > 0"
@@ -137,7 +137,7 @@
lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
by (simp add: Ninv_def isnormNum_def split_def)
- (cases "fst x = 0", auto simp add: int_gcd_commute)
+ (cases "fst x = 0", auto simp add: gcd_commute_int)
lemma isnormNum_int[simp]:
"isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
@@ -203,7 +203,7 @@
from prems have eq:"a * b' = a'*b"
by (simp add: INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
from prems have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
- by (simp_all add: isnormNum_def add: int_gcd_commute)
+ by (simp_all add: isnormNum_def add: gcd_commute_int)
from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
apply -
apply algebra
@@ -211,8 +211,8 @@
apply simp
apply algebra
done
- from zdvd_dvd_eq[OF bz int_coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
- int_coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
+ from zdvd_dvd_eq[OF bz coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
+ coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
have eq1: "b = b'" using pos by arith
with eq have "a = a'" using pos by simp
with eq1 have ?rhs by simp}
@@ -297,8 +297,8 @@
let ?g = "gcd (a * b' + b * a') (b*b')"
have gz: "?g \<noteq> 0" using z by simp
have ?thesis using aa' bb' z gz
- of_int_div[where ?'a = 'a, OF gz int_gcd_dvd1[where x="a * b' + b * a'" and y="b*b'"]] of_int_div[where ?'a = 'a,
- OF gz int_gcd_dvd2[where x="a * b' + b * a'" and y="b*b'"]]
+ of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]] of_int_div[where ?'a = 'a,
+ OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
ultimately have ?thesis using aa' bb'
by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
@@ -319,8 +319,8 @@
{assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
let ?g="gcd (a*a') (b*b')"
have gz: "?g \<noteq> 0" using z by simp
- from z of_int_div[where ?'a = 'a, OF gz int_gcd_dvd1[where x="a*a'" and y="b*b'"]]
- of_int_div[where ?'a = 'a , OF gz int_gcd_dvd2[where x="a*a'" and y="b*b'"]]
+ from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]]
+ of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]]
have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
ultimately show ?thesis by blast
qed
@@ -478,7 +478,7 @@
qed
lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
- by (simp add: Nmul_def split_def Let_def int_gcd_commute mult_commute)
+ by (simp add: Nmul_def split_def Let_def gcd_commute_int mult_commute)
lemma Nmul_assoc:
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
--- a/src/HOL/Library/Legacy_GCD.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/Library/Legacy_GCD.thy Tue Jul 07 21:26:08 2009 +0200
@@ -409,7 +409,7 @@
{fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y"
using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
- from nat_dvd_diff[OF dv(1,2)] nat_dvd_diff[OF dv(3,4)] H
+ from dvd_diff_nat[OF dv(1,2)] dvd_diff_nat[OF dv(3,4)] H
have ?rhs by auto}
ultimately show ?thesis by blast
qed
--- a/src/HOL/Library/Pocklington.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/Library/Pocklington.thy Tue Jul 07 21:26:08 2009 +0200
@@ -846,7 +846,7 @@
from lh[unfolded nat_mod]
obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2" by blast
hence "a ^ d + n * q1 - n * q2 = 1" by simp
- with nat_dvd_diff [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp
+ with dvd_diff_nat [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp
with p(3) have False by simp
hence ?rhs ..}
ultimately have ?rhs by blast}
--- a/src/HOL/Library/Primes.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/Library/Primes.thy Tue Jul 07 21:26:08 2009 +0200
@@ -311,8 +311,8 @@
{fix e assume H: "e dvd a^n" "e dvd b^n"
from bezout_gcd_pow[of a n b] obtain x y
where xy: "a ^ n * x - b ^ n * y = ?gn \<or> b ^ n * x - a ^ n * y = ?gn" by blast
- from nat_dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
- nat_dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
+ from dvd_diff_nat [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
+ dvd_diff_nat [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd a b ^ n", simp_all)}
hence th: "\<forall>e. e dvd a^n \<and> e dvd b^n \<longrightarrow> e dvd ?gn" by blast
from divides_exp[OF gcd_dvd1[of a b], of n] divides_exp[OF gcd_dvd2[of a b], of n] th
--- a/src/HOL/NewNumberTheory/Binomial.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/NewNumberTheory/Binomial.thy Tue Jul 07 21:26:08 2009 +0200
@@ -109,68 +109,68 @@
subsection {* Factorial *}
-lemma nat_fact_zero [simp]: "fact (0::nat) = 1"
+lemma fact_zero_nat [simp]: "fact (0::nat) = 1"
by simp
-lemma int_fact_zero [simp]: "fact (0::int) = 1"
+lemma fact_zero_int [simp]: "fact (0::int) = 1"
by (simp add: fact_int_def)
-lemma nat_fact_one [simp]: "fact (1::nat) = 1"
+lemma fact_one_nat [simp]: "fact (1::nat) = 1"
by simp
-lemma nat_fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
+lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
by (simp add: One_nat_def)
-lemma int_fact_one [simp]: "fact (1::int) = 1"
+lemma fact_one_int [simp]: "fact (1::int) = 1"
by (simp add: fact_int_def)
-lemma nat_fact_plus_one: "fact ((n::nat) + 1) = (n + 1) * fact n"
+lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
by simp
-lemma nat_fact_Suc: "fact (Suc n) = (Suc n) * fact n"
+lemma fact_Suc_nat: "fact (Suc n) = (Suc n) * fact n"
by (simp add: One_nat_def)
-lemma int_fact_plus_one:
+lemma fact_plus_one_int:
assumes "n >= 0"
shows "fact ((n::int) + 1) = (n + 1) * fact n"
- using prems by (rule nat_fact_plus_one [transferred])
+ using prems by (rule fact_plus_one_nat [transferred])
-lemma nat_fact_reduce: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
+lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
by simp
-lemma int_fact_reduce:
+lemma fact_reduce_int:
assumes "(n::int) > 0"
shows "fact n = n * fact (n - 1)"
using prems apply (subst tsub_eq [symmetric], auto)
- apply (rule nat_fact_reduce [transferred])
+ apply (rule fact_reduce_nat [transferred])
using prems apply auto
done
declare fact_nat.simps [simp del]
-lemma nat_fact_nonzero [simp]: "fact (n::nat) \<noteq> 0"
- apply (induct n rule: nat_induct')
- apply (auto simp add: nat_fact_plus_one)
+lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
+ apply (induct n rule: induct'_nat)
+ apply (auto simp add: fact_plus_one_nat)
done
-lemma int_fact_nonzero [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
+lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
by (simp add: fact_int_def)
-lemma nat_fact_gt_zero [simp]: "fact (n :: nat) > 0"
- by (insert nat_fact_nonzero [of n], arith)
+lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
+ by (insert fact_nonzero_nat [of n], arith)
-lemma int_fact_gt_zero [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
+lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
by (auto simp add: fact_int_def)
-lemma nat_fact_ge_one [simp]: "fact (n :: nat) >= 1"
- by (insert nat_fact_nonzero [of n], arith)
+lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
+ by (insert fact_nonzero_nat [of n], arith)
-lemma nat_fact_ge_Suc_0 [simp]: "fact (n :: nat) >= Suc 0"
- by (insert nat_fact_nonzero [of n], arith)
+lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
+ by (insert fact_nonzero_nat [of n], arith)
-lemma int_fact_ge_one [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
+lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
apply (auto simp add: fact_int_def)
apply (subgoal_tac "1 = int 1")
apply (erule ssubst)
@@ -178,41 +178,41 @@
apply auto
done
-lemma nat_dvd_fact [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
- apply (induct n rule: nat_induct')
- apply (auto simp add: nat_fact_plus_one)
+lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
+ apply (induct n rule: induct'_nat)
+ apply (auto simp add: fact_plus_one_nat)
apply (subgoal_tac "m = n + 1")
apply auto
done
-lemma int_dvd_fact [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
+lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
apply (case_tac "1 <= n")
apply (induct n rule: int_ge_induct)
- apply (auto simp add: int_fact_plus_one)
+ apply (auto simp add: fact_plus_one_int)
apply (subgoal_tac "m = i + 1")
apply auto
done
-lemma nat_interval_plus_one: "(i::nat) <= j + 1 \<Longrightarrow>
+lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
{i..j+1} = {i..j} Un {j+1}"
by auto
-lemma int_interval_plus_one: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
+lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
by auto
-lemma nat_fact_altdef: "fact (n::nat) = (PROD i:{1..n}. i)"
- apply (induct n rule: nat_induct')
+lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
+ apply (induct n rule: induct'_nat)
apply force
- apply (subst nat_fact_plus_one)
- apply (subst nat_interval_plus_one)
+ apply (subst fact_plus_one_nat)
+ apply (subst interval_plus_one_nat)
apply auto
done
-lemma int_fact_altdef: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
+lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
apply (induct n rule: int_ge_induct)
apply force
- apply (subst int_fact_plus_one, assumption)
- apply (subst int_interval_plus_one)
+ apply (subst fact_plus_one_int, assumption)
+ apply (subst interval_plus_one_int)
apply auto
done
@@ -220,8 +220,8 @@
lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
proof-
- have f1: "fact n + 1 \<noteq> 1" using nat_fact_ge_one [of n] by arith
- from nat_prime_factor [OF f1]
+ have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
+ from prime_factor_nat [OF f1]
obtain p where "prime p" and "p dvd fact n + 1" by auto
hence "p \<le> fact n + 1"
by (intro dvd_imp_le, auto)
@@ -229,9 +229,9 @@
from `prime p` have "p \<ge> 1"
by (cases p, simp_all)
with `p <= n` have "p dvd fact n"
- by (intro nat_dvd_fact)
+ by (intro dvd_fact_nat)
with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
- by (rule nat_dvd_diff)
+ by (rule dvd_diff_nat)
hence "p dvd 1" by simp
hence "p <= 1" by auto
moreover from `prime p` have "p > 1" by auto
@@ -256,95 +256,94 @@
subsection {* Binomial coefficients *}
-lemma nat_choose_zero [simp]: "(n::nat) choose 0 = 1"
+lemma choose_zero_nat [simp]: "(n::nat) choose 0 = 1"
by simp
-lemma int_choose_zero [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 0 = 1"
+lemma choose_zero_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 0 = 1"
by (simp add: binomial_int_def)
-lemma nat_zero_choose [rule_format,simp]: "ALL (k::nat) > n. n choose k = 0"
- by (induct n rule: nat_induct', auto)
+lemma zero_choose_nat [rule_format,simp]: "ALL (k::nat) > n. n choose k = 0"
+ by (induct n rule: induct'_nat, auto)
-lemma int_zero_choose [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
+lemma zero_choose_int [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
unfolding binomial_int_def apply (case_tac "n < 0")
apply force
apply (simp del: binomial_nat.simps)
done
-lemma nat_choose_reduce: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
+lemma choose_reduce_nat: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
(n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
by simp
-lemma int_choose_reduce: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
+lemma choose_reduce_int: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
(n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
- unfolding binomial_int_def apply (subst nat_choose_reduce)
+ unfolding binomial_int_def apply (subst choose_reduce_nat)
apply (auto simp del: binomial_nat.simps
simp add: nat_diff_distrib)
done
-lemma nat_choose_plus_one: "((n::nat) + 1) choose (k + 1) =
+lemma choose_plus_one_nat: "((n::nat) + 1) choose (k + 1) =
(n choose (k + 1)) + (n choose k)"
- by (simp add: nat_choose_reduce)
+ by (simp add: choose_reduce_nat)
-lemma nat_choose_Suc: "(Suc n) choose (Suc k) =
+lemma choose_Suc_nat: "(Suc n) choose (Suc k) =
(n choose (Suc k)) + (n choose k)"
- by (simp add: nat_choose_reduce One_nat_def)
+ by (simp add: choose_reduce_nat One_nat_def)
-lemma int_choose_plus_one: "n \<ge> 0 \<Longrightarrow> k \<ge> 0 \<Longrightarrow> ((n::int) + 1) choose (k + 1) =
+lemma choose_plus_one_int: "n \<ge> 0 \<Longrightarrow> k \<ge> 0 \<Longrightarrow> ((n::int) + 1) choose (k + 1) =
(n choose (k + 1)) + (n choose k)"
- by (simp add: binomial_int_def nat_choose_plus_one nat_add_distrib
- del: binomial_nat.simps)
+ by (simp add: binomial_int_def choose_plus_one_nat nat_add_distrib del: binomial_nat.simps)
declare binomial_nat.simps [simp del]
-lemma nat_choose_self [simp]: "((n::nat) choose n) = 1"
- by (induct n rule: nat_induct', auto simp add: nat_choose_plus_one)
+lemma choose_self_nat [simp]: "((n::nat) choose n) = 1"
+ by (induct n rule: induct'_nat, auto simp add: choose_plus_one_nat)
-lemma int_choose_self [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"
+lemma choose_self_int [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"
by (auto simp add: binomial_int_def)
-lemma nat_choose_one [simp]: "(n::nat) choose 1 = n"
- by (induct n rule: nat_induct', auto simp add: nat_choose_reduce)
+lemma choose_one_nat [simp]: "(n::nat) choose 1 = n"
+ by (induct n rule: induct'_nat, auto simp add: choose_reduce_nat)
-lemma int_choose_one [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"
+lemma choose_one_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"
by (auto simp add: binomial_int_def)
-lemma nat_plus_one_choose_self [simp]: "(n::nat) + 1 choose n = n + 1"
- apply (induct n rule: nat_induct', force)
+lemma plus_one_choose_self_nat [simp]: "(n::nat) + 1 choose n = n + 1"
+ apply (induct n rule: induct'_nat, force)
apply (case_tac "n = 0")
apply auto
- apply (subst nat_choose_reduce)
+ apply (subst choose_reduce_nat)
apply (auto simp add: One_nat_def)
(* natdiff_cancel_numerals introduces Suc *)
done
-lemma nat_Suc_choose_self [simp]: "(Suc n) choose n = Suc n"
- using nat_plus_one_choose_self by (simp add: One_nat_def)
+lemma Suc_choose_self_nat [simp]: "(Suc n) choose n = Suc n"
+ using plus_one_choose_self_nat by (simp add: One_nat_def)
-lemma int_plus_one_choose_self [rule_format, simp]:
+lemma plus_one_choose_self_int [rule_format, simp]:
"(n::int) \<ge> 0 \<longrightarrow> n + 1 choose n = n + 1"
by (auto simp add: binomial_int_def nat_add_distrib)
(* bounded quantification doesn't work with the unicode characters? *)
-lemma nat_choose_pos [rule_format]: "ALL k <= (n::nat).
+lemma choose_pos_nat [rule_format]: "ALL k <= (n::nat).
((n::nat) choose k) > 0"
- apply (induct n rule: nat_induct')
+ apply (induct n rule: induct'_nat)
apply force
apply clarify
apply (case_tac "k = 0")
apply force
- apply (subst nat_choose_reduce)
+ apply (subst choose_reduce_nat)
apply auto
done
-lemma int_choose_pos: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
+lemma choose_pos_int: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
((n::int) choose k) > 0"
- by (auto simp add: binomial_int_def nat_choose_pos)
+ by (auto simp add: binomial_int_def choose_pos_nat)
lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow>
(ALL n. P (n + 1) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (k + 1) \<longrightarrow>
P (n + 1) (k + 1))) \<longrightarrow> (ALL k <= n. P n k)"
- apply (induct n rule: nat_induct')
+ apply (induct n rule: induct'_nat)
apply auto
apply (case_tac "k = 0")
apply auto
@@ -355,7 +354,7 @@
apply auto
done
-lemma nat_choose_altdef_aux: "(k::nat) \<le> n \<Longrightarrow>
+lemma choose_altdef_aux_nat: "(k::nat) \<le> n \<Longrightarrow>
fact k * fact (n - k) * (n choose k) = fact n"
apply (rule binomial_induct [of _ k n])
apply auto
@@ -364,22 +363,22 @@
assume less: "k < n"
assume ih1: "fact k * fact (n - k) * (n choose k) = fact n"
hence one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
- by (subst nat_fact_plus_one, auto)
+ by (subst fact_plus_one_nat, auto)
assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) =
fact n"
with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) *
(n choose (k + 1)) = (n - k) * fact n"
- by (subst (2) nat_fact_plus_one, auto)
+ by (subst (2) fact_plus_one_nat, auto)
with less have two: "fact (k + 1) * fact (n - k) * (n choose (k + 1)) =
(n - k) * fact n" by simp
have "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
fact (k + 1) * fact (n - k) * (n choose (k + 1)) +
fact (k + 1) * fact (n - k) * (n choose k)"
- by (subst nat_choose_reduce, auto simp add: ring_simps)
+ by (subst choose_reduce_nat, auto simp add: ring_simps)
also note one
also note two
also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)"
- apply (subst nat_fact_plus_one)
+ apply (subst fact_plus_one_nat)
apply (subst left_distrib [symmetric])
apply simp
done
@@ -387,43 +386,43 @@
fact (n + 1)" .
qed
-lemma nat_choose_altdef: "(k::nat) \<le> n \<Longrightarrow>
+lemma choose_altdef_nat: "(k::nat) \<le> n \<Longrightarrow>
n choose k = fact n div (fact k * fact (n - k))"
- apply (frule nat_choose_altdef_aux)
+ apply (frule choose_altdef_aux_nat)
apply (erule subst)
apply (simp add: mult_ac)
done
-lemma int_choose_altdef:
+lemma choose_altdef_int:
assumes "(0::int) <= k" and "k <= n"
shows "n choose k = fact n div (fact k * fact (n - k))"
apply (subst tsub_eq [symmetric], rule prems)
- apply (rule nat_choose_altdef [transferred])
+ apply (rule choose_altdef_nat [transferred])
using prems apply auto
done
-lemma nat_choose_dvd: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
- unfolding dvd_def apply (frule nat_choose_altdef_aux)
+lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
+ unfolding dvd_def apply (frule choose_altdef_aux_nat)
(* why don't blast and auto get this??? *)
apply (rule exI)
apply (erule sym)
done
-lemma int_choose_dvd:
+lemma choose_dvd_int:
assumes "(0::int) <= k" and "k <= n"
shows "fact k * fact (n - k) dvd fact n"
apply (subst tsub_eq [symmetric], rule prems)
- apply (rule nat_choose_dvd [transferred])
+ apply (rule choose_dvd_nat [transferred])
using prems apply auto
done
(* generalizes Tobias Nipkow's proof to any commutative semiring *)
theorem binomial: "(a+b::'a::{comm_ring_1,power})^n =
(SUM k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")
-proof (induct n rule: nat_induct')
+proof (induct n rule: induct'_nat)
show "?P 0" by simp
next
fix n
@@ -455,7 +454,7 @@
"... = a^(n+1) + b^(n+1) +
(SUM k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"
by (auto simp add: ring_simps setsum_addf [symmetric]
- nat_choose_reduce)
+ choose_reduce_nat)
also have "... = (SUM k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"
using decomp by (simp add: ring_simps)
finally show "?P (n + 1)" by simp
@@ -464,7 +463,7 @@
lemma set_explicit: "{S. S = T \<and> P S} = (if P T then {T} else {})"
by auto
-lemma nat_card_subsets [rule_format]:
+lemma card_subsets_nat [rule_format]:
fixes S :: "'a set"
assumes "finite S"
shows "ALL k. card {T. T \<le> S \<and> card T = k} = card S choose k"
@@ -480,7 +479,7 @@
fix k
show "card {T. T \<subseteq> (insert x F) \<and> card T = k} =
card (insert x F) choose k" (is "?Q k")
- proof (induct k rule: nat_induct')
+ proof (induct k rule: induct'_nat)
from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
apply auto
apply (subst (asm) card_0_eq)
@@ -530,7 +529,7 @@
by auto
finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) =
card F choose (k + 1) + (card F choose k)".
- with iassms nat_choose_plus_one show ?thesis
+ with iassms choose_plus_one_nat show ?thesis
by auto
qed
qed
--- a/src/HOL/NewNumberTheory/Cong.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/NewNumberTheory/Cong.thy Tue Jul 07 21:26:08 2009 +0200
@@ -35,18 +35,18 @@
subsection {* Turn off One_nat_def *}
-lemma nat_induct' [case_names zero plus1, induct type: nat]:
+lemma induct'_nat [case_names zero plus1, induct type: nat]:
"\<lbrakk> P (0::nat); !!n. P n \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow> P n"
by (erule nat_induct) (simp add:One_nat_def)
-lemma nat_cases [case_names zero plus1, cases type: nat]:
+lemma cases_nat [case_names zero plus1, cases type: nat]:
"P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n"
-by(metis nat_induct')
+by(metis induct'_nat)
lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n"
by (simp add: One_nat_def)
-lemma nat_power_eq_one_eq [simp]:
+lemma power_eq_one_eq_nat [simp]:
"((x::nat)^m = 1) = (m = 0 | x = 1)"
by (induct m, auto)
@@ -147,55 +147,55 @@
subsection {* Congruence *}
(* was zcong_0, etc. *)
-lemma nat_cong_0 [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
+lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
by (unfold cong_nat_def, auto)
-lemma int_cong_0 [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
+lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
by (unfold cong_int_def, auto)
-lemma nat_cong_1 [simp, presburger]: "[(a::nat) = b] (mod 1)"
+lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)"
by (unfold cong_nat_def, auto)
-lemma nat_cong_Suc_0 [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
+lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
by (unfold cong_nat_def, auto simp add: One_nat_def)
-lemma int_cong_1 [simp, presburger]: "[(a::int) = b] (mod 1)"
+lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)"
by (unfold cong_int_def, auto)
-lemma nat_cong_refl [simp]: "[(k::nat) = k] (mod m)"
+lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)"
by (unfold cong_nat_def, auto)
-lemma int_cong_refl [simp]: "[(k::int) = k] (mod m)"
+lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)"
by (unfold cong_int_def, auto)
-lemma nat_cong_sym: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
+lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
by (unfold cong_nat_def, auto)
-lemma int_cong_sym: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
+lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
by (unfold cong_int_def, auto)
-lemma nat_cong_sym_eq: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
+lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
by (unfold cong_nat_def, auto)
-lemma int_cong_sym_eq: "[(a::int) = b] (mod m) = [b = a] (mod m)"
+lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)"
by (unfold cong_int_def, auto)
-lemma nat_cong_trans [trans]:
+lemma cong_trans_nat [trans]:
"[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
by (unfold cong_nat_def, auto)
-lemma int_cong_trans [trans]:
+lemma cong_trans_int [trans]:
"[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
by (unfold cong_int_def, auto)
-lemma nat_cong_add:
+lemma cong_add_nat:
"[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
apply (unfold cong_nat_def)
apply (subst (1 2) mod_add_eq)
apply simp
done
-lemma int_cong_add:
+lemma cong_add_int:
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
apply (unfold cong_int_def)
apply (subst (1 2) mod_add_left_eq)
@@ -203,35 +203,35 @@
apply simp
done
-lemma int_cong_diff:
+lemma cong_diff_int:
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
apply (unfold cong_int_def)
apply (subst (1 2) mod_diff_eq)
apply simp
done
-lemma int_cong_diff_aux:
+lemma cong_diff_aux_int:
"(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow>
[c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
apply (subst (1 2) tsub_eq)
- apply (auto intro: int_cong_diff)
+ apply (auto intro: cong_diff_int)
done;
-lemma nat_cong_diff:
+lemma cong_diff_nat:
assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
"[c = d] (mod m)"
shows "[a - c = b - d] (mod m)"
- using prems by (rule int_cong_diff_aux [transferred]);
+ using prems by (rule cong_diff_aux_int [transferred]);
-lemma nat_cong_mult:
+lemma cong_mult_nat:
"[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
apply (unfold cong_nat_def)
apply (subst (1 2) mod_mult_eq)
apply simp
done
-lemma int_cong_mult:
+lemma cong_mult_int:
"[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
apply (unfold cong_int_def)
apply (subst (1 2) zmod_zmult1_eq)
@@ -240,197 +240,197 @@
apply simp
done
-lemma nat_cong_exp: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
+lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
apply (induct k)
- apply (auto simp add: nat_cong_refl nat_cong_mult)
+ apply (auto simp add: cong_refl_nat cong_mult_nat)
done
-lemma int_cong_exp: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
+lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
apply (induct k)
- apply (auto simp add: int_cong_refl int_cong_mult)
+ apply (auto simp add: cong_refl_int cong_mult_int)
done
-lemma nat_cong_setsum [rule_format]:
+lemma cong_setsum_nat [rule_format]:
"(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
[(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
apply (case_tac "finite A")
apply (induct set: finite)
- apply (auto intro: nat_cong_add)
+ apply (auto intro: cong_add_nat)
done
-lemma int_cong_setsum [rule_format]:
+lemma cong_setsum_int [rule_format]:
"(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
[(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
apply (case_tac "finite A")
apply (induct set: finite)
- apply (auto intro: int_cong_add)
+ apply (auto intro: cong_add_int)
done
-lemma nat_cong_setprod [rule_format]:
+lemma cong_setprod_nat [rule_format]:
"(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
[(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
apply (case_tac "finite A")
apply (induct set: finite)
- apply (auto intro: nat_cong_mult)
+ apply (auto intro: cong_mult_nat)
done
-lemma int_cong_setprod [rule_format]:
+lemma cong_setprod_int [rule_format]:
"(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
[(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
apply (case_tac "finite A")
apply (induct set: finite)
- apply (auto intro: int_cong_mult)
+ apply (auto intro: cong_mult_int)
done
-lemma nat_cong_scalar: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
- by (rule nat_cong_mult, simp_all)
+lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
+ by (rule cong_mult_nat, simp_all)
-lemma int_cong_scalar: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
- by (rule int_cong_mult, simp_all)
+lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
+ by (rule cong_mult_int, simp_all)
-lemma nat_cong_scalar2: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
- by (rule nat_cong_mult, simp_all)
+lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
+ by (rule cong_mult_nat, simp_all)
-lemma int_cong_scalar2: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
- by (rule int_cong_mult, simp_all)
+lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
+ by (rule cong_mult_int, simp_all)
-lemma nat_cong_mult_self: "[(a::nat) * m = 0] (mod m)"
+lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)"
by (unfold cong_nat_def, auto)
-lemma int_cong_mult_self: "[(a::int) * m = 0] (mod m)"
+lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)"
by (unfold cong_int_def, auto)
-lemma int_cong_eq_diff_cong_0: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
+lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
apply (rule iffI)
- apply (erule int_cong_diff [of a b m b b, simplified])
- apply (erule int_cong_add [of "a - b" 0 m b b, simplified])
+ apply (erule cong_diff_int [of a b m b b, simplified])
+ apply (erule cong_add_int [of "a - b" 0 m b b, simplified])
done
-lemma int_cong_eq_diff_cong_0_aux: "a >= b \<Longrightarrow>
+lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow>
[(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
- by (subst tsub_eq, assumption, rule int_cong_eq_diff_cong_0)
+ by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int)
-lemma nat_cong_eq_diff_cong_0:
+lemma cong_eq_diff_cong_0_nat:
assumes "(a::nat) >= b"
shows "[a = b] (mod m) = [a - b = 0] (mod m)"
- using prems by (rule int_cong_eq_diff_cong_0_aux [transferred])
+ using prems by (rule cong_eq_diff_cong_0_aux_int [transferred])
-lemma nat_cong_diff_cong_0':
+lemma cong_diff_cong_0'_nat:
"[(x::nat) = y] (mod n) \<longleftrightarrow>
(if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
apply (case_tac "y <= x")
- apply (frule nat_cong_eq_diff_cong_0 [where m = n])
+ apply (frule cong_eq_diff_cong_0_nat [where m = n])
apply auto [1]
apply (subgoal_tac "x <= y")
- apply (frule nat_cong_eq_diff_cong_0 [where m = n])
- apply (subst nat_cong_sym_eq)
+ apply (frule cong_eq_diff_cong_0_nat [where m = n])
+ apply (subst cong_sym_eq_nat)
apply auto
done
-lemma nat_cong_altdef: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
- apply (subst nat_cong_eq_diff_cong_0, assumption)
+lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
+ apply (subst cong_eq_diff_cong_0_nat, assumption)
apply (unfold cong_nat_def)
apply (simp add: dvd_eq_mod_eq_0 [symmetric])
done
-lemma int_cong_altdef: "[(a::int) = b] (mod m) = (m dvd (a - b))"
- apply (subst int_cong_eq_diff_cong_0)
+lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
+ apply (subst cong_eq_diff_cong_0_int)
apply (unfold cong_int_def)
apply (simp add: dvd_eq_mod_eq_0 [symmetric])
done
-lemma int_cong_abs: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
- by (simp add: int_cong_altdef)
+lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
+ by (simp add: cong_altdef_int)
-lemma int_cong_square:
+lemma cong_square_int:
"\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk>
\<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
- apply (simp only: int_cong_altdef)
- apply (subst int_prime_dvd_mult_eq [symmetric], assumption)
+ apply (simp only: cong_altdef_int)
+ apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
(* any way around this? *)
apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
apply (auto simp add: ring_simps)
done
-lemma int_cong_mult_rcancel:
+lemma cong_mult_rcancel_int:
"coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
- apply (subst (1 2) int_cong_altdef)
+ apply (subst (1 2) cong_altdef_int)
apply (subst left_diff_distrib [symmetric])
- apply (rule int_coprime_dvd_mult_iff)
- apply (subst int_gcd_commute, assumption)
+ apply (rule coprime_dvd_mult_iff_int)
+ apply (subst gcd_commute_int, assumption)
done
-lemma nat_cong_mult_rcancel:
+lemma cong_mult_rcancel_nat:
assumes "coprime k (m::nat)"
shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
- apply (rule int_cong_mult_rcancel [transferred])
+ apply (rule cong_mult_rcancel_int [transferred])
using prems apply auto
done
-lemma nat_cong_mult_lcancel:
+lemma cong_mult_lcancel_nat:
"coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
- by (simp add: mult_commute nat_cong_mult_rcancel)
+ by (simp add: mult_commute cong_mult_rcancel_nat)
-lemma int_cong_mult_lcancel:
+lemma cong_mult_lcancel_int:
"coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
- by (simp add: mult_commute int_cong_mult_rcancel)
+ by (simp add: mult_commute cong_mult_rcancel_int)
(* was zcong_zgcd_zmult_zmod *)
-lemma int_coprime_cong_mult:
+lemma coprime_cong_mult_int:
"[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
\<Longrightarrow> [a = b] (mod m * n)"
- apply (simp only: int_cong_altdef)
- apply (erule (2) int_divides_mult)
+ apply (simp only: cong_altdef_int)
+ apply (erule (2) divides_mult_int)
done
-lemma nat_coprime_cong_mult:
+lemma coprime_cong_mult_nat:
assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
shows "[a = b] (mod m * n)"
- apply (rule int_coprime_cong_mult [transferred])
+ apply (rule coprime_cong_mult_int [transferred])
using prems apply auto
done
-lemma nat_cong_less_imp_eq: "0 \<le> (a::nat) \<Longrightarrow>
+lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow>
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
by (auto simp add: cong_nat_def mod_pos_pos_trivial)
-lemma int_cong_less_imp_eq: "0 \<le> (a::int) \<Longrightarrow>
+lemma cong_less_imp_eq_int: "0 \<le> (a::int) \<Longrightarrow>
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
by (auto simp add: cong_int_def mod_pos_pos_trivial)
-lemma nat_cong_less_unique:
+lemma cong_less_unique_nat:
"0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
apply auto
apply (rule_tac x = "a mod m" in exI)
apply (unfold cong_nat_def, auto)
done
-lemma int_cong_less_unique:
+lemma cong_less_unique_int:
"0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
apply auto
apply (rule_tac x = "a mod m" in exI)
apply (unfold cong_int_def, auto simp add: mod_pos_pos_trivial)
done
-lemma int_cong_iff_lin: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
- apply (auto simp add: int_cong_altdef dvd_def ring_simps)
+lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
+ apply (auto simp add: cong_altdef_int dvd_def ring_simps)
apply (rule_tac [!] x = "-k" in exI, auto)
done
-lemma nat_cong_iff_lin: "([(a::nat) = b] (mod m)) =
+lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
(\<exists>k1 k2. b + k1 * m = a + k2 * m)"
apply (rule iffI)
apply (case_tac "b <= a")
- apply (subst (asm) nat_cong_altdef, assumption)
+ apply (subst (asm) cong_altdef_nat, assumption)
apply (unfold dvd_def, auto)
apply (rule_tac x = k in exI)
apply (rule_tac x = 0 in exI)
apply (auto simp add: ring_simps)
- apply (subst (asm) nat_cong_sym_eq)
- apply (subst (asm) nat_cong_altdef)
+ apply (subst (asm) cong_sym_eq_nat)
+ apply (subst (asm) cong_altdef_nat)
apply force
apply (unfold dvd_def, auto)
apply (rule_tac x = 0 in exI)
@@ -443,50 +443,50 @@
apply auto
done
-lemma int_cong_gcd_eq: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
- apply (subst (asm) int_cong_iff_lin, auto)
+lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
+ apply (subst (asm) cong_iff_lin_int, auto)
apply (subst add_commute)
- apply (subst (2) int_gcd_commute)
+ apply (subst (2) gcd_commute_int)
apply (subst mult_commute)
- apply (subst int_gcd_add_mult)
- apply (rule int_gcd_commute)
+ apply (subst gcd_add_mult_int)
+ apply (rule gcd_commute_int)
done
-lemma nat_cong_gcd_eq:
+lemma cong_gcd_eq_nat:
assumes "[(a::nat) = b] (mod m)"
shows "gcd a m = gcd b m"
- apply (rule int_cong_gcd_eq [transferred])
+ apply (rule cong_gcd_eq_int [transferred])
using prems apply auto
done
-lemma nat_cong_imp_coprime: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
+lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
coprime b m"
- by (auto simp add: nat_cong_gcd_eq)
+ by (auto simp add: cong_gcd_eq_nat)
-lemma int_cong_imp_coprime: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
+lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
coprime b m"
- by (auto simp add: int_cong_gcd_eq)
+ by (auto simp add: cong_gcd_eq_int)
-lemma nat_cong_cong_mod: "[(a::nat) = b] (mod m) =
+lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) =
[a mod m = b mod m] (mod m)"
by (auto simp add: cong_nat_def)
-lemma int_cong_cong_mod: "[(a::int) = b] (mod m) =
+lemma cong_cong_mod_int: "[(a::int) = b] (mod m) =
[a mod m = b mod m] (mod m)"
by (auto simp add: cong_int_def)
-lemma int_cong_minus [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
- by (subst (1 2) int_cong_altdef, auto)
+lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
+ by (subst (1 2) cong_altdef_int, auto)
-lemma nat_cong_zero [iff]: "[(a::nat) = b] (mod 0) = (a = b)"
+lemma cong_zero_nat [iff]: "[(a::nat) = b] (mod 0) = (a = b)"
by (auto simp add: cong_nat_def)
-lemma int_cong_zero [iff]: "[(a::int) = b] (mod 0) = (a = b)"
+lemma cong_zero_int [iff]: "[(a::int) = b] (mod 0) = (a = b)"
by (auto simp add: cong_int_def)
(*
-lemma int_mod_dvd_mod:
+lemma mod_dvd_mod_int:
"0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)"
apply (unfold dvd_def, auto)
apply (rule mod_mod_cancel)
@@ -497,79 +497,79 @@
assumes "0 < (m::nat)" and "m dvd b"
shows "(a mod b mod m) = (a mod m)"
- apply (rule int_mod_dvd_mod [transferred])
+ apply (rule mod_dvd_mod_int [transferred])
using prems apply auto
done
*)
-lemma nat_cong_add_lcancel:
+lemma cong_add_lcancel_nat:
"[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
- by (simp add: nat_cong_iff_lin)
+ by (simp add: cong_iff_lin_nat)
-lemma int_cong_add_lcancel:
+lemma cong_add_lcancel_int:
"[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
- by (simp add: int_cong_iff_lin)
+ by (simp add: cong_iff_lin_int)
-lemma nat_cong_add_rcancel: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
- by (simp add: nat_cong_iff_lin)
+lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+ by (simp add: cong_iff_lin_nat)
-lemma int_cong_add_rcancel: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
- by (simp add: int_cong_iff_lin)
+lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+ by (simp add: cong_iff_lin_int)
-lemma nat_cong_add_lcancel_0: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
- by (simp add: nat_cong_iff_lin)
+lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+ by (simp add: cong_iff_lin_nat)
-lemma int_cong_add_lcancel_0: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
- by (simp add: int_cong_iff_lin)
+lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+ by (simp add: cong_iff_lin_int)
-lemma nat_cong_add_rcancel_0: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
- by (simp add: nat_cong_iff_lin)
+lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+ by (simp add: cong_iff_lin_nat)
-lemma int_cong_add_rcancel_0: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
- by (simp add: int_cong_iff_lin)
+lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+ by (simp add: cong_iff_lin_int)
-lemma nat_cong_dvd_modulus: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
+lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
[x = y] (mod n)"
- apply (auto simp add: nat_cong_iff_lin dvd_def)
+ apply (auto simp add: cong_iff_lin_nat dvd_def)
apply (rule_tac x="k1 * k" in exI)
apply (rule_tac x="k2 * k" in exI)
apply (simp add: ring_simps)
done
-lemma int_cong_dvd_modulus: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
+lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
[x = y] (mod n)"
- by (auto simp add: int_cong_altdef dvd_def)
+ by (auto simp add: cong_altdef_int dvd_def)
-lemma nat_cong_dvd_eq: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
+lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0)
-lemma int_cong_dvd_eq: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
+lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0)
-lemma nat_cong_mod: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
+lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
by (simp add: cong_nat_def)
-lemma int_cong_mod: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
+lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
by (simp add: cong_int_def)
-lemma nat_mod_mult_cong: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
+lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
by (simp add: cong_nat_def mod_mult2_eq mod_add_left_eq)
-lemma int_neg_cong: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
- apply (simp add: int_cong_altdef)
+lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
+ apply (simp add: cong_altdef_int)
apply (subst dvd_minus_iff [symmetric])
apply (simp add: ring_simps)
done
-lemma int_cong_modulus_neg: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
- by (auto simp add: int_cong_altdef)
+lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
+ by (auto simp add: cong_altdef_int)
-lemma int_mod_mult_cong: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
+lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
\<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
apply (case_tac "b > 0")
apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
- apply (subst (1 2) int_cong_modulus_neg)
+ apply (subst (1 2) cong_modulus_neg_int)
apply (unfold cong_int_def)
apply (subgoal_tac "a * b = (-a * -b)")
apply (erule ssubst)
@@ -577,89 +577,89 @@
apply (auto simp add: mod_add_left_eq)
done
-lemma nat_cong_to_1: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
+lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
apply (case_tac "a = 0")
apply force
- apply (subst (asm) nat_cong_altdef)
+ apply (subst (asm) cong_altdef_nat)
apply auto
done
-lemma nat_0_cong_1: "[(0::nat) = 1] (mod n) = (n = 1)"
+lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)"
by (unfold cong_nat_def, auto)
-lemma int_0_cong_1: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
+lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
-lemma nat_cong_to_1': "[(a::nat) = 1] (mod n) \<longleftrightarrow>
+lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
apply (case_tac "n = 1")
apply auto [1]
apply (drule_tac x = "a - 1" in spec)
apply force
apply (case_tac "a = 0")
- apply (auto simp add: nat_0_cong_1) [1]
+ apply (auto simp add: cong_0_1_nat) [1]
apply (rule iffI)
- apply (drule nat_cong_to_1)
+ apply (drule cong_to_1_nat)
apply (unfold dvd_def)
apply auto [1]
apply (rule_tac x = k in exI)
apply (auto simp add: ring_simps) [1]
- apply (subst nat_cong_altdef)
+ apply (subst cong_altdef_nat)
apply (auto simp add: dvd_def)
done
-lemma nat_cong_le: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
- apply (subst nat_cong_altdef)
+lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
+ apply (subst cong_altdef_nat)
apply assumption
apply (unfold dvd_def, auto simp add: ring_simps)
apply (rule_tac x = k in exI)
apply auto
done
-lemma nat_cong_solve: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
+lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
apply (case_tac "n = 0")
apply force
- apply (frule nat_bezout [of a n], auto)
+ apply (frule bezout_nat [of a n], auto)
apply (rule exI, erule ssubst)
- apply (rule nat_cong_trans)
- apply (rule nat_cong_add)
+ apply (rule cong_trans_nat)
+ apply (rule cong_add_nat)
apply (subst mult_commute)
- apply (rule nat_cong_mult_self)
+ apply (rule cong_mult_self_nat)
prefer 2
apply simp
- apply (rule nat_cong_refl)
- apply (rule nat_cong_refl)
+ apply (rule cong_refl_nat)
+ apply (rule cong_refl_nat)
done
-lemma int_cong_solve: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
+lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
apply (case_tac "n = 0")
apply (case_tac "a \<ge> 0")
apply auto
apply (rule_tac x = "-1" in exI)
apply auto
- apply (insert int_bezout [of a n], auto)
+ apply (insert bezout_int [of a n], auto)
apply (rule exI)
apply (erule subst)
- apply (rule int_cong_trans)
+ apply (rule cong_trans_int)
prefer 2
- apply (rule int_cong_add)
- apply (rule int_cong_refl)
- apply (rule int_cong_sym)
- apply (rule int_cong_mult_self)
+ apply (rule cong_add_int)
+ apply (rule cong_refl_int)
+ apply (rule cong_sym_int)
+ apply (rule cong_mult_self_int)
apply simp
apply (subst mult_commute)
- apply (rule int_cong_refl)
+ apply (rule cong_refl_int)
done
-lemma nat_cong_solve_dvd:
+lemma cong_solve_dvd_nat:
assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
shows "EX x. [a * x = d] (mod n)"
proof -
- from nat_cong_solve [OF a] obtain x where
+ from cong_solve_nat [OF a] obtain x where
"[a * x = gcd a n](mod n)"
by auto
hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
- by (elim nat_cong_scalar2)
+ by (elim cong_scalar2_nat)
also from b have "(d div gcd a n) * gcd a n = d"
by (rule dvd_div_mult_self)
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
@@ -668,15 +668,15 @@
by auto
qed
-lemma int_cong_solve_dvd:
+lemma cong_solve_dvd_int:
assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
shows "EX x. [a * x = d] (mod n)"
proof -
- from int_cong_solve [OF a] obtain x where
+ from cong_solve_int [OF a] obtain x where
"[a * x = gcd a n](mod n)"
by auto
hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
- by (elim int_cong_scalar2)
+ by (elim cong_scalar2_int)
also from b have "(d div gcd a n) * gcd a n = d"
by (rule dvd_div_mult_self)
also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
@@ -685,41 +685,41 @@
by auto
qed
-lemma nat_cong_solve_coprime: "coprime (a::nat) n \<Longrightarrow>
+lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow>
EX x. [a * x = 1] (mod n)"
apply (case_tac "a = 0")
apply force
- apply (frule nat_cong_solve [of a n])
+ apply (frule cong_solve_nat [of a n])
apply auto
done
-lemma int_cong_solve_coprime: "coprime (a::int) n \<Longrightarrow>
+lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow>
EX x. [a * x = 1] (mod n)"
apply (case_tac "a = 0")
apply auto
apply (case_tac "n \<ge> 0")
apply auto
apply (subst cong_int_def, auto)
- apply (frule int_cong_solve [of a n])
+ apply (frule cong_solve_int [of a n])
apply auto
done
-lemma nat_coprime_iff_invertible: "m > (1::nat) \<Longrightarrow> coprime a m =
+lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m =
(EX x. [a * x = 1] (mod m))"
- apply (auto intro: nat_cong_solve_coprime)
- apply (unfold cong_nat_def, auto intro: nat_invertible_coprime)
+ apply (auto intro: cong_solve_coprime_nat)
+ apply (unfold cong_nat_def, auto intro: invertible_coprime_nat)
done
-lemma int_coprime_iff_invertible: "m > (1::int) \<Longrightarrow> coprime a m =
+lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m =
(EX x. [a * x = 1] (mod m))"
- apply (auto intro: int_cong_solve_coprime)
+ apply (auto intro: cong_solve_coprime_int)
apply (unfold cong_int_def)
- apply (auto intro: int_invertible_coprime)
+ apply (auto intro: invertible_coprime_int)
done
-lemma int_coprime_iff_invertible': "m > (1::int) \<Longrightarrow> coprime a m =
+lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m =
(EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
- apply (subst int_coprime_iff_invertible)
+ apply (subst coprime_iff_invertible_int)
apply auto
apply (auto simp add: cong_int_def)
apply (rule_tac x = "x mod m" in exI)
@@ -727,200 +727,200 @@
done
-lemma nat_cong_cong_lcm: "[(x::nat) = y] (mod a) \<Longrightarrow>
+lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
apply (case_tac "y \<le> x")
- apply (auto simp add: nat_cong_altdef nat_lcm_least) [1]
- apply (rule nat_cong_sym)
- apply (subst (asm) (1 2) nat_cong_sym_eq)
- apply (auto simp add: nat_cong_altdef nat_lcm_least)
+ apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
+ apply (rule cong_sym_nat)
+ apply (subst (asm) (1 2) cong_sym_eq_nat)
+ apply (auto simp add: cong_altdef_nat lcm_least_nat)
done
-lemma int_cong_cong_lcm: "[(x::int) = y] (mod a) \<Longrightarrow>
+lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
[x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
- by (auto simp add: int_cong_altdef int_lcm_least) [1]
+ by (auto simp add: cong_altdef_int lcm_least_int) [1]
-lemma nat_cong_cong_coprime: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
+lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
[x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
- apply (frule (1) nat_cong_cong_lcm)back
+ apply (frule (1) cong_cong_lcm_nat)back
apply (simp add: lcm_nat_def)
done
-lemma int_cong_cong_coprime: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
+lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
[x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
- apply (frule (1) int_cong_cong_lcm)back
- apply (simp add: int_lcm_altdef int_cong_abs abs_mult [symmetric])
+ apply (frule (1) cong_cong_lcm_int)back
+ apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
done
-lemma nat_cong_cong_setprod_coprime [rule_format]: "finite A \<Longrightarrow>
+lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
(ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
[x = y] (mod (PROD i:A. m i))"
apply (induct set: finite)
apply auto
- apply (rule nat_cong_cong_coprime)
- apply (subst nat_gcd_commute)
- apply (rule nat_setprod_coprime)
+ apply (rule cong_cong_coprime_nat)
+ apply (subst gcd_commute_nat)
+ apply (rule setprod_coprime_nat)
apply auto
done
-lemma int_cong_cong_setprod_coprime [rule_format]: "finite A \<Longrightarrow>
+lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
(ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
(ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow>
[x = y] (mod (PROD i:A. m i))"
apply (induct set: finite)
apply auto
- apply (rule int_cong_cong_coprime)
- apply (subst int_gcd_commute)
- apply (rule int_setprod_coprime)
+ apply (rule cong_cong_coprime_int)
+ apply (subst gcd_commute_int)
+ apply (rule setprod_coprime_int)
apply auto
done
-lemma nat_binary_chinese_remainder_aux:
+lemma binary_chinese_remainder_aux_nat:
assumes a: "coprime (m1::nat) m2"
shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
[b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
proof -
- from nat_cong_solve_coprime [OF a]
+ from cong_solve_coprime_nat [OF a]
obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
by auto
from a have b: "coprime m2 m1"
- by (subst nat_gcd_commute)
- from nat_cong_solve_coprime [OF b]
+ by (subst gcd_commute_nat)
+ from cong_solve_coprime_nat [OF b]
obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
by auto
have "[m1 * x1 = 0] (mod m1)"
- by (subst mult_commute, rule nat_cong_mult_self)
+ by (subst mult_commute, rule cong_mult_self_nat)
moreover have "[m2 * x2 = 0] (mod m2)"
- by (subst mult_commute, rule nat_cong_mult_self)
+ by (subst mult_commute, rule cong_mult_self_nat)
moreover note one two
ultimately show ?thesis by blast
qed
-lemma int_binary_chinese_remainder_aux:
+lemma binary_chinese_remainder_aux_int:
assumes a: "coprime (m1::int) m2"
shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
[b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
proof -
- from int_cong_solve_coprime [OF a]
+ from cong_solve_coprime_int [OF a]
obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
by auto
from a have b: "coprime m2 m1"
- by (subst int_gcd_commute)
- from int_cong_solve_coprime [OF b]
+ by (subst gcd_commute_int)
+ from cong_solve_coprime_int [OF b]
obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
by auto
have "[m1 * x1 = 0] (mod m1)"
- by (subst mult_commute, rule int_cong_mult_self)
+ by (subst mult_commute, rule cong_mult_self_int)
moreover have "[m2 * x2 = 0] (mod m2)"
- by (subst mult_commute, rule int_cong_mult_self)
+ by (subst mult_commute, rule cong_mult_self_int)
moreover note one two
ultimately show ?thesis by blast
qed
-lemma nat_binary_chinese_remainder:
+lemma binary_chinese_remainder_nat:
assumes a: "coprime (m1::nat) m2"
shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
proof -
- from nat_binary_chinese_remainder_aux [OF a] obtain b1 b2
+ from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
"[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
by blast
let ?x = "u1 * b1 + u2 * b2"
have "[?x = u1 * 1 + u2 * 0] (mod m1)"
- apply (rule nat_cong_add)
- apply (rule nat_cong_scalar2)
+ apply (rule cong_add_nat)
+ apply (rule cong_scalar2_nat)
apply (rule `[b1 = 1] (mod m1)`)
- apply (rule nat_cong_scalar2)
+ apply (rule cong_scalar2_nat)
apply (rule `[b2 = 0] (mod m1)`)
done
hence "[?x = u1] (mod m1)" by simp
have "[?x = u1 * 0 + u2 * 1] (mod m2)"
- apply (rule nat_cong_add)
- apply (rule nat_cong_scalar2)
+ apply (rule cong_add_nat)
+ apply (rule cong_scalar2_nat)
apply (rule `[b1 = 0] (mod m2)`)
- apply (rule nat_cong_scalar2)
+ apply (rule cong_scalar2_nat)
apply (rule `[b2 = 1] (mod m2)`)
done
hence "[?x = u2] (mod m2)" by simp
with `[?x = u1] (mod m1)` show ?thesis by blast
qed
-lemma int_binary_chinese_remainder:
+lemma binary_chinese_remainder_int:
assumes a: "coprime (m1::int) m2"
shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
proof -
- from int_binary_chinese_remainder_aux [OF a] obtain b1 b2
+ from binary_chinese_remainder_aux_int [OF a] obtain b1 b2
where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
"[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
by blast
let ?x = "u1 * b1 + u2 * b2"
have "[?x = u1 * 1 + u2 * 0] (mod m1)"
- apply (rule int_cong_add)
- apply (rule int_cong_scalar2)
+ apply (rule cong_add_int)
+ apply (rule cong_scalar2_int)
apply (rule `[b1 = 1] (mod m1)`)
- apply (rule int_cong_scalar2)
+ apply (rule cong_scalar2_int)
apply (rule `[b2 = 0] (mod m1)`)
done
hence "[?x = u1] (mod m1)" by simp
have "[?x = u1 * 0 + u2 * 1] (mod m2)"
- apply (rule int_cong_add)
- apply (rule int_cong_scalar2)
+ apply (rule cong_add_int)
+ apply (rule cong_scalar2_int)
apply (rule `[b1 = 0] (mod m2)`)
- apply (rule int_cong_scalar2)
+ apply (rule cong_scalar2_int)
apply (rule `[b2 = 1] (mod m2)`)
done
hence "[?x = u2] (mod m2)" by simp
with `[?x = u1] (mod m1)` show ?thesis by blast
qed
-lemma nat_cong_modulus_mult: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
+lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
[x = y] (mod m)"
apply (case_tac "y \<le> x")
- apply (simp add: nat_cong_altdef)
+ apply (simp add: cong_altdef_nat)
apply (erule dvd_mult_left)
- apply (rule nat_cong_sym)
- apply (subst (asm) nat_cong_sym_eq)
- apply (simp add: nat_cong_altdef)
+ apply (rule cong_sym_nat)
+ apply (subst (asm) cong_sym_eq_nat)
+ apply (simp add: cong_altdef_nat)
apply (erule dvd_mult_left)
done
-lemma int_cong_modulus_mult: "[(x::int) = y] (mod m * n) \<Longrightarrow>
+lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
[x = y] (mod m)"
- apply (simp add: int_cong_altdef)
+ apply (simp add: cong_altdef_int)
apply (erule dvd_mult_left)
done
-lemma nat_cong_less_modulus_unique:
+lemma cong_less_modulus_unique_nat:
"[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
by (simp add: cong_nat_def)
-lemma nat_binary_chinese_remainder_unique:
+lemma binary_chinese_remainder_unique_nat:
assumes a: "coprime (m1::nat) m2" and
nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
proof -
- from nat_binary_chinese_remainder [OF a] obtain y where
+ from binary_chinese_remainder_nat [OF a] obtain y where
"[y = u1] (mod m1)" and "[y = u2] (mod m2)"
by blast
let ?x = "y mod (m1 * m2)"
from nz have less: "?x < m1 * m2"
by auto
have one: "[?x = u1] (mod m1)"
- apply (rule nat_cong_trans)
+ apply (rule cong_trans_nat)
prefer 2
apply (rule `[y = u1] (mod m1)`)
- apply (rule nat_cong_modulus_mult)
- apply (rule nat_cong_mod)
+ apply (rule cong_modulus_mult_nat)
+ apply (rule cong_mod_nat)
using nz apply auto
done
have two: "[?x = u2] (mod m2)"
- apply (rule nat_cong_trans)
+ apply (rule cong_trans_nat)
prefer 2
apply (rule `[y = u2] (mod m2)`)
apply (subst mult_commute)
- apply (rule nat_cong_modulus_mult)
- apply (rule nat_cong_mod)
+ apply (rule cong_modulus_mult_nat)
+ apply (rule cong_mod_nat)
using nz apply auto
done
have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow>
@@ -930,29 +930,29 @@
assume "z < m1 * m2"
assume "[z = u1] (mod m1)" and "[z = u2] (mod m2)"
have "[?x = z] (mod m1)"
- apply (rule nat_cong_trans)
+ apply (rule cong_trans_nat)
apply (rule `[?x = u1] (mod m1)`)
- apply (rule nat_cong_sym)
+ apply (rule cong_sym_nat)
apply (rule `[z = u1] (mod m1)`)
done
moreover have "[?x = z] (mod m2)"
- apply (rule nat_cong_trans)
+ apply (rule cong_trans_nat)
apply (rule `[?x = u2] (mod m2)`)
- apply (rule nat_cong_sym)
+ apply (rule cong_sym_nat)
apply (rule `[z = u2] (mod m2)`)
done
ultimately have "[?x = z] (mod m1 * m2)"
- by (auto intro: nat_coprime_cong_mult a)
+ by (auto intro: coprime_cong_mult_nat a)
with `z < m1 * m2` `?x < m1 * m2` show "z = ?x"
- apply (intro nat_cong_less_modulus_unique)
- apply (auto, erule nat_cong_sym)
+ apply (intro cong_less_modulus_unique_nat)
+ apply (auto, erule cong_sym_nat)
done
qed
with less one two show ?thesis
by auto
qed
-lemma nat_chinese_remainder_aux:
+lemma chinese_remainder_aux_nat:
fixes A :: "'a set" and
m :: "'a \<Rightarrow> nat"
assumes fin: "finite A" and
@@ -963,20 +963,20 @@
fix i
assume "i : A"
with cop have "coprime (PROD j : A - {i}. m j) (m i)"
- by (intro nat_setprod_coprime, auto)
+ by (intro setprod_coprime_nat, auto)
hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
- by (elim nat_cong_solve_coprime)
+ by (elim cong_solve_coprime_nat)
then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
by auto
moreover have "[(PROD j : A - {i}. m j) * x = 0]
(mod (PROD j : A - {i}. m j))"
- by (subst mult_commute, rule nat_cong_mult_self)
+ by (subst mult_commute, rule cong_mult_self_nat)
ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
(mod setprod m (A - {i}))"
by blast
qed
-lemma nat_chinese_remainder:
+lemma chinese_remainder_nat:
fixes A :: "'a set" and
m :: "'a \<Rightarrow> nat" and
u :: "'a \<Rightarrow> nat"
@@ -985,7 +985,7 @@
cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
shows "EX x. (ALL i:A. [x = u i] (mod m i))"
proof -
- from nat_chinese_remainder_aux [OF fin cop] obtain b where
+ from chinese_remainder_aux_nat [OF fin cop] obtain b where
bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
[b i = 0] (mod (PROD j : A - {i}. m j))"
by blast
@@ -1003,13 +1003,13 @@
by auto
also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
- apply (rule nat_cong_add)
- apply (rule nat_cong_scalar2)
+ apply (rule cong_add_nat)
+ apply (rule cong_scalar2_nat)
using bprop a apply blast
- apply (rule nat_cong_setsum)
- apply (rule nat_cong_scalar2)
+ apply (rule cong_setsum_nat)
+ apply (rule cong_scalar2_nat)
using bprop apply auto
- apply (rule nat_cong_dvd_modulus)
+ apply (rule cong_dvd_modulus_nat)
apply (drule (1) bspec)
apply (erule conjE)
apply assumption
@@ -1022,19 +1022,19 @@
qed
qed
-lemma nat_coprime_cong_prod [rule_format]: "finite A \<Longrightarrow>
+lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
(ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
(ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
[x = y] (mod (PROD i:A. m i))"
apply (induct set: finite)
apply auto
- apply (erule (1) nat_coprime_cong_mult)
- apply (subst nat_gcd_commute)
- apply (rule nat_setprod_coprime)
+ apply (erule (1) coprime_cong_mult_nat)
+ apply (subst gcd_commute_nat)
+ apply (rule setprod_coprime_nat)
apply auto
done
-lemma nat_chinese_remainder_unique:
+lemma chinese_remainder_unique_nat:
fixes A :: "'a set" and
m :: "'a \<Rightarrow> nat" and
u :: "'a \<Rightarrow> nat"
@@ -1044,7 +1044,7 @@
cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
proof -
- from nat_chinese_remainder [OF fin cop] obtain y where
+ from chinese_remainder_nat [OF fin cop] obtain y where
one: "(ALL i:A. [y = u i] (mod m i))"
by blast
let ?x = "y mod (PROD i:A. m i)"
@@ -1054,11 +1054,11 @@
by auto
have cong: "ALL i:A. [?x = u i] (mod m i)"
apply auto
- apply (rule nat_cong_trans)
+ apply (rule cong_trans_nat)
prefer 2
using one apply auto
- apply (rule nat_cong_dvd_modulus)
- apply (rule nat_cong_mod)
+ apply (rule cong_dvd_modulus_nat)
+ apply (rule cong_mod_nat)
using prodnz apply auto
apply (rule dvd_setprod)
apply (rule fin)
@@ -1072,16 +1072,16 @@
assume zcong: "(ALL i:A. [z = u i] (mod m i))"
have "ALL i:A. [?x = z] (mod m i)"
apply clarify
- apply (rule nat_cong_trans)
+ apply (rule cong_trans_nat)
using cong apply (erule bspec)
- apply (rule nat_cong_sym)
+ apply (rule cong_sym_nat)
using zcong apply auto
done
with fin cop have "[?x = z] (mod (PROD i:A. m i))"
- by (intro nat_coprime_cong_prod, auto)
+ by (intro coprime_cong_prod_nat, auto)
with zless less show "z = ?x"
- apply (intro nat_cong_less_modulus_unique)
- apply (auto, erule nat_cong_sym)
+ apply (intro cong_less_modulus_unique_nat)
+ apply (auto, erule cong_sym_nat)
done
qed
from less cong unique show ?thesis
--- a/src/HOL/NewNumberTheory/Fib.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/NewNumberTheory/Fib.thy Tue Jul 07 21:26:08 2009 +0200
@@ -86,45 +86,45 @@
subsection {* Fibonacci numbers *}
-lemma nat_fib_0 [simp]: "fib (0::nat) = 0"
+lemma fib_0_nat [simp]: "fib (0::nat) = 0"
by simp
-lemma int_fib_0 [simp]: "fib (0::int) = 0"
+lemma fib_0_int [simp]: "fib (0::int) = 0"
unfolding fib_int_def by simp
-lemma nat_fib_1 [simp]: "fib (1::nat) = 1"
+lemma fib_1_nat [simp]: "fib (1::nat) = 1"
by simp
-lemma nat_fib_Suc_0 [simp]: "fib (Suc 0) = Suc 0"
+lemma fib_Suc_0_nat [simp]: "fib (Suc 0) = Suc 0"
by simp
-lemma int_fib_1 [simp]: "fib (1::int) = 1"
+lemma fib_1_int [simp]: "fib (1::int) = 1"
unfolding fib_int_def by simp
-lemma nat_fib_reduce: "(n::nat) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
+lemma fib_reduce_nat: "(n::nat) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
by simp
declare fib_nat.simps [simp del]
-lemma int_fib_reduce: "(n::int) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
+lemma fib_reduce_int: "(n::int) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
unfolding fib_int_def
- by (auto simp add: nat_fib_reduce nat_diff_distrib)
+ by (auto simp add: fib_reduce_nat nat_diff_distrib)
-lemma int_fib_neg [simp]: "(n::int) < 0 \<Longrightarrow> fib n = 0"
+lemma fib_neg_int [simp]: "(n::int) < 0 \<Longrightarrow> fib n = 0"
unfolding fib_int_def by auto
-lemma nat_fib_2 [simp]: "fib (2::nat) = 1"
- by (subst nat_fib_reduce, auto)
+lemma fib_2_nat [simp]: "fib (2::nat) = 1"
+ by (subst fib_reduce_nat, auto)
-lemma int_fib_2 [simp]: "fib (2::int) = 1"
- by (subst int_fib_reduce, auto)
+lemma fib_2_int [simp]: "fib (2::int) = 1"
+ by (subst fib_reduce_int, auto)
-lemma nat_fib_plus_2: "fib ((n::nat) + 2) = fib (n + 1) + fib n"
- by (subst nat_fib_reduce, auto simp add: One_nat_def)
+lemma fib_plus_2_nat: "fib ((n::nat) + 2) = fib (n + 1) + fib n"
+ by (subst fib_reduce_nat, auto simp add: One_nat_def)
(* the need for One_nat_def is due to the natdiff_cancel_numerals
procedure *)
-lemma nat_fib_induct: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
+lemma fib_induct_nat: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow>
(!!n. P n \<Longrightarrow> P (n + 1) \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
apply (atomize, induct n rule: nat_less_induct)
apply auto
@@ -138,13 +138,13 @@
apply (auto simp add: One_nat_def) (* again, natdiff_cancel *)
done
-lemma nat_fib_add: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
+lemma fib_add_nat: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) +
fib k * fib n"
- apply (induct n rule: nat_fib_induct)
+ apply (induct n rule: fib_induct_nat)
apply auto
- apply (subst nat_fib_reduce)
+ apply (subst fib_reduce_nat)
apply (auto simp add: ring_simps)
- apply (subst (1 3 5) nat_fib_reduce)
+ apply (subst (1 3 5) fib_reduce_nat)
apply (auto simp add: ring_simps Suc_eq_plus1)
(* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
@@ -153,112 +153,112 @@
apply auto
done
-lemma nat_fib_add': "fib (n + Suc k) = fib (Suc k) * fib (Suc n) +
+lemma fib_add'_nat: "fib (n + Suc k) = fib (Suc k) * fib (Suc n) +
fib k * fib n"
- using nat_fib_add by (auto simp add: One_nat_def)
+ using fib_add_nat by (auto simp add: One_nat_def)
(* transfer from nats to ints *)
-lemma int_fib_add [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
+lemma fib_add_int [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
fib (n + k + 1) = fib (k + 1) * fib (n + 1) +
fib k * fib n "
- by (rule nat_fib_add [transferred])
+ by (rule fib_add_nat [transferred])
-lemma nat_fib_neq_0: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
- apply (induct n rule: nat_fib_induct)
- apply (auto simp add: nat_fib_plus_2)
+lemma fib_neq_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
+ apply (induct n rule: fib_induct_nat)
+ apply (auto simp add: fib_plus_2_nat)
done
-lemma nat_fib_gr_0: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
- by (frule nat_fib_neq_0, simp)
+lemma fib_gr_0_nat: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
+ by (frule fib_neq_0_nat, simp)
-lemma int_fib_gr_0: "(n::int) > 0 \<Longrightarrow> fib n > 0"
- unfolding fib_int_def by (simp add: nat_fib_gr_0)
+lemma fib_gr_0_int: "(n::int) > 0 \<Longrightarrow> fib n > 0"
+ unfolding fib_int_def by (simp add: fib_gr_0_nat)
text {*
\medskip Concrete Mathematics, page 278: Cassini's identity. The proof is
much easier using integers, not natural numbers!
*}
-lemma int_fib_Cassini_aux: "fib (int n + 2) * fib (int n) -
+lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
(fib (int n + 1))^2 = (-1)^(n + 1)"
apply (induct n)
- apply (auto simp add: ring_simps power2_eq_square int_fib_reduce
+ apply (auto simp add: ring_simps power2_eq_square fib_reduce_int
power_add)
done
-lemma int_fib_Cassini: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
+lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
(fib (n + 1))^2 = (-1)^(nat n + 1)"
- by (insert int_fib_Cassini_aux [of "nat n"], auto)
+ by (insert fib_Cassini_aux_int [of "nat n"], auto)
(*
-lemma int_fib_Cassini': "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
+lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
(fib (n + 1))^2 + (-1)^(nat n + 1)"
- by (frule int_fib_Cassini, simp)
+ by (frule fib_Cassini_int, simp)
*)
-lemma int_fib_Cassini': "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
+lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
(if even n then tsub ((fib (n + 1))^2) 1
else (fib (n + 1))^2 + 1)"
- apply (frule int_fib_Cassini, auto simp add: pos_int_even_equiv_nat_even)
+ apply (frule fib_Cassini_int, auto simp add: pos_int_even_equiv_nat_even)
apply (subst tsub_eq)
- apply (insert int_fib_gr_0 [of "n + 1"], force)
+ apply (insert fib_gr_0_int [of "n + 1"], force)
apply auto
done
-lemma nat_fib_Cassini: "fib ((n::nat) + 2) * fib n =
+lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
(if even n then (fib (n + 1))^2 - 1
else (fib (n + 1))^2 + 1)"
- by (rule int_fib_Cassini' [transferred, of n], auto)
+ by (rule fib_Cassini'_int [transferred, of n], auto)
text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
-lemma nat_coprime_fib_plus_1: "coprime (fib (n::nat)) (fib (n + 1))"
- apply (induct n rule: nat_fib_induct)
+lemma coprime_fib_plus_1_nat: "coprime (fib (n::nat)) (fib (n + 1))"
+ apply (induct n rule: fib_induct_nat)
apply auto
- apply (subst (2) nat_fib_reduce)
+ apply (subst (2) fib_reduce_nat)
apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
apply (subst add_commute, auto)
- apply (subst nat_gcd_commute, auto simp add: ring_simps)
+ apply (subst gcd_commute_nat, auto simp add: ring_simps)
done
-lemma nat_coprime_fib_Suc: "coprime (fib n) (fib (Suc n))"
- using nat_coprime_fib_plus_1 by (simp add: One_nat_def)
+lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
+ using coprime_fib_plus_1_nat by (simp add: One_nat_def)
-lemma int_coprime_fib_plus_1:
+lemma coprime_fib_plus_1_int:
"n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
- by (erule nat_coprime_fib_plus_1 [transferred])
+ by (erule coprime_fib_plus_1_nat [transferred])
-lemma nat_gcd_fib_add: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
- apply (simp add: nat_gcd_commute [of "fib m"])
- apply (rule nat_cases [of _ m])
+lemma gcd_fib_add_nat: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
+ apply (simp add: gcd_commute_nat [of "fib m"])
+ apply (rule cases_nat [of _ m])
apply simp
apply (subst add_assoc [symmetric])
- apply (simp add: nat_fib_add)
- apply (subst nat_gcd_commute)
+ apply (simp add: fib_add_nat)
+ apply (subst gcd_commute_nat)
apply (subst mult_commute)
- apply (subst nat_gcd_add_mult)
- apply (subst nat_gcd_commute)
- apply (rule nat_gcd_mult_cancel)
- apply (rule nat_coprime_fib_plus_1)
+ apply (subst gcd_add_mult_nat)
+ apply (subst gcd_commute_nat)
+ apply (rule gcd_mult_cancel_nat)
+ apply (rule coprime_fib_plus_1_nat)
done
-lemma int_gcd_fib_add [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
+lemma gcd_fib_add_int [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)"
- by (erule nat_gcd_fib_add [transferred])
+ by (erule gcd_fib_add_nat [transferred])
-lemma nat_gcd_fib_diff: "(m::nat) \<le> n \<Longrightarrow>
+lemma gcd_fib_diff_nat: "(m::nat) \<le> n \<Longrightarrow>
gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
- by (simp add: nat_gcd_fib_add [symmetric, of _ "n-m"])
+ by (simp add: gcd_fib_add_nat [symmetric, of _ "n-m"])
-lemma int_gcd_fib_diff: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
+lemma gcd_fib_diff_int: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow>
gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
- by (simp add: int_gcd_fib_add [symmetric, of _ "n-m"])
+ by (simp add: gcd_fib_add_int [symmetric, of _ "n-m"])
-lemma nat_gcd_fib_mod: "0 < (m::nat) \<Longrightarrow>
+lemma gcd_fib_mod_nat: "0 < (m::nat) \<Longrightarrow>
gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
proof (induct n rule: less_induct)
case (less n)
@@ -273,7 +273,7 @@
by (simp add: mod_if [of n]) (insert m_n, auto)
also have "\<dots> = gcd (fib m) (fib (n - m))"
by (simp add: less.hyps diff pos_m)
- also have "\<dots> = gcd (fib m) (fib n)" by (simp add: nat_gcd_fib_diff m_n')
+ also have "\<dots> = gcd (fib m) (fib n)" by (simp add: gcd_fib_diff_nat m_n')
finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
next
case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
@@ -281,39 +281,39 @@
qed
qed
-lemma int_gcd_fib_mod:
+lemma gcd_fib_mod_int:
assumes "0 < (m::int)" and "0 <= n"
shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
- apply (rule nat_gcd_fib_mod [transferred])
+ apply (rule gcd_fib_mod_nat [transferred])
using prems apply auto
done
-lemma nat_fib_gcd: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
+lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
-- {* Law 6.111 *}
- apply (induct m n rule: nat_gcd_induct)
- apply (simp_all add: nat_gcd_non_0 nat_gcd_commute nat_gcd_fib_mod)
+ apply (induct m n rule: gcd_nat_induct)
+ apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)
done
-lemma int_fib_gcd: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
+lemma fib_gcd_int: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
fib (gcd (m::int) n) = gcd (fib m) (fib n)"
- by (erule nat_fib_gcd [transferred])
+ by (erule fib_gcd_nat [transferred])
-lemma nat_atMost_plus_one: "{..(k::nat) + 1} = insert (k + 1) {..k}"
+lemma atMost_plus_one_nat: "{..(k::nat) + 1} = insert (k + 1) {..k}"
by auto
-theorem nat_fib_mult_eq_setsum:
+theorem fib_mult_eq_setsum_nat:
"fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
apply (induct n)
- apply (auto simp add: nat_atMost_plus_one nat_fib_plus_2 ring_simps)
+ apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat ring_simps)
done
-theorem nat_fib_mult_eq_setsum':
+theorem fib_mult_eq_setsum'_nat:
"fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
- using nat_fib_mult_eq_setsum by (simp add: One_nat_def)
+ using fib_mult_eq_setsum_nat by (simp add: One_nat_def)
-theorem int_fib_mult_eq_setsum [rule_format]:
+theorem fib_mult_eq_setsum_int [rule_format]:
"n >= 0 \<Longrightarrow> fib ((n::int) + 1) * fib n = (\<Sum>k \<in> {0..n}. fib k * fib k)"
- by (erule nat_fib_mult_eq_setsum [transferred])
+ by (erule fib_mult_eq_setsum_nat [transferred])
end
--- a/src/HOL/NewNumberTheory/MiscAlgebra.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/NewNumberTheory/MiscAlgebra.thy Tue Jul 07 21:26:08 2009 +0200
@@ -12,7 +12,7 @@
(* finiteness stuff *)
-lemma int_bounded_set1 [intro]: "finite {(x::int). a < x & x < b & P x}"
+lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}"
apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..<b}")
apply (erule finite_subset)
apply auto
--- a/src/HOL/NewNumberTheory/Residues.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/NewNumberTheory/Residues.thy Tue Jul 07 21:26:08 2009 +0200
@@ -105,10 +105,10 @@
apply auto
apply (subgoal_tac "x ~= 0")
apply auto
- apply (rule int_invertible_coprime)
+ apply (rule invertible_coprime_int)
apply (subgoal_tac "x ~= 0")
apply auto
- apply (subst (asm) int_coprime_iff_invertible')
+ apply (subst (asm) coprime_iff_invertible'_int)
apply (rule m_gt_one)
apply (auto simp add: cong_int_def mult_commute)
done
@@ -202,8 +202,8 @@
apply (subgoal_tac "a mod m ~= 0")
apply arith
apply auto
- apply (subst (asm) int_gcd_red)
- apply (subst int_gcd_commute, assumption)
+ apply (subst (asm) gcd_red_int)
+ apply (subst gcd_commute_int, assumption)
done
lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
@@ -254,8 +254,8 @@
res_units_eq)
apply (rule classical)
apply (erule notE)
- apply (subst int_gcd_commute)
- apply (rule int_prime_imp_coprime)
+ apply (subst gcd_commute_int)
+ apply (rule prime_imp_coprime_int)
apply (rule p_prime)
apply (rule notI)
apply (frule zdvd_imp_le)
@@ -265,8 +265,8 @@
lemma res_prime_units_eq: "Units R = {1..p - 1}"
apply (subst res_units_eq)
apply auto
- apply (subst int_gcd_commute)
- apply (rule int_prime_imp_coprime)
+ apply (subst gcd_commute_int)
+ apply (rule prime_imp_coprime_int)
apply (rule p_prime)
apply (rule zdvd_not_zless)
apply auto
@@ -367,8 +367,8 @@
apply (intro euler_theorem)
(* auto should get this next part. matching across
substitutions is needed. *)
- apply (frule int_prime_gt_1, arith)
- apply (subst int_gcd_commute, erule int_prime_imp_coprime, assumption)
+ apply (frule prime_gt_1_int, arith)
+ apply (subst gcd_commute_int, erule prime_imp_coprime_int, assumption)
done
also have "phi p = nat p - 1"
by (rule phi_prime, rule prems)
@@ -442,7 +442,7 @@
apply auto
done
also have "\<dots> = fact (p - 1) mod p"
- apply (subst int_fact_altdef)
+ apply (subst fact_altdef_int)
apply (insert prems, force)
apply (subst res_prime_units_eq, rule refl)
done
@@ -452,9 +452,9 @@
qed
lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
- apply (frule int_prime_gt_1)
+ apply (frule prime_gt_1_int)
apply (case_tac "p = 2")
- apply (subst int_fact_altdef, simp)
+ apply (subst fact_altdef_int, simp)
apply (subst cong_int_def)
apply simp
apply (rule residues_prime.wilson_theorem1)
--- a/src/HOL/NewNumberTheory/UniqueFactorization.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/NewNumberTheory/UniqueFactorization.thy Tue Jul 07 21:26:08 2009 +0200
@@ -134,7 +134,7 @@
moreover
{
assume "n > 1" and "~ prime n"
- from prems nat_not_prime_eq_prod
+ from prems not_prime_eq_prod_nat
obtain m k where "n = m * k & 1 < m & m < n & 1 < k & k < n"
by blast
with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
@@ -182,13 +182,13 @@
a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
moreover have "coprime (a ^ count M a)
(PROD i : (set_of N - {a}). i ^ (count N i))"
- apply (subst nat_gcd_commute)
- apply (rule nat_setprod_coprime)
- apply (rule nat_primes_imp_powers_coprime)
+ apply (subst gcd_commute_nat)
+ apply (rule setprod_coprime_nat)
+ apply (rule primes_imp_powers_coprime_nat)
apply (insert prems, auto)
done
ultimately have "a ^ count M a dvd a^(count N a)"
- by (elim nat_coprime_dvd_mult)
+ by (elim coprime_dvd_mult_nat)
with a show ?thesis
by (intro power_dvd_imp_le, auto)
next
@@ -322,66 +322,66 @@
subsection {* Properties of prime factors and multiplicity for nats and ints *}
-lemma int_prime_factors_ge_0 [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
+lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
by (unfold prime_factors_int_def, auto)
-lemma nat_prime_factors_prime [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
+lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
apply (case_tac "n = 0")
apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
done
-lemma int_prime_factors_prime [intro]:
+lemma prime_factors_prime_int [intro]:
assumes "n >= 0" and "p : prime_factors (n::int)"
shows "prime p"
- apply (rule nat_prime_factors_prime [transferred, of n p])
+ apply (rule prime_factors_prime_nat [transferred, of n p])
using prems apply auto
done
-lemma nat_prime_factors_gt_0 [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
- by (frule nat_prime_factors_prime, auto)
+lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
+ by (frule prime_factors_prime_nat, auto)
-lemma int_prime_factors_gt_0 [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow>
+lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow>
p > (0::int)"
- by (frule (1) int_prime_factors_prime, auto)
+ by (frule (1) prime_factors_prime_int, auto)
-lemma nat_prime_factors_finite [iff]: "finite (prime_factors (n::nat))"
+lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))"
by (unfold prime_factors_nat_def, auto)
-lemma int_prime_factors_finite [iff]: "finite (prime_factors (n::int))"
+lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))"
by (unfold prime_factors_int_def, auto)
-lemma nat_prime_factors_altdef: "prime_factors (n::nat) =
+lemma prime_factors_altdef_nat: "prime_factors (n::nat) =
{p. multiplicity p n > 0}"
by (force simp add: prime_factors_nat_def multiplicity_nat_def)
-lemma int_prime_factors_altdef: "prime_factors (n::int) =
+lemma prime_factors_altdef_int: "prime_factors (n::int) =
{p. p >= 0 & multiplicity p n > 0}"
apply (unfold prime_factors_int_def multiplicity_int_def)
- apply (subst nat_prime_factors_altdef)
+ apply (subst prime_factors_altdef_nat)
apply (auto simp add: image_def)
done
-lemma nat_prime_factorization: "(n::nat) > 0 \<Longrightarrow>
+lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow>
n = (PROD p : prime_factors n. p^(multiplicity p n))"
by (frule multiset_prime_factorization,
simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
-thm nat_prime_factorization [transferred]
+thm prime_factorization_nat [transferred]
-lemma int_prime_factorization:
+lemma prime_factorization_int:
assumes "(n::int) > 0"
shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
- apply (rule nat_prime_factorization [transferred, of n])
+ apply (rule prime_factorization_nat [transferred, of n])
using prems apply auto
done
-lemma nat_neq_zero_eq_gt_zero: "((x::nat) ~= 0) = (x > 0)"
+lemma neq_zero_eq_gt_zero_nat: "((x::nat) ~= 0) = (x > 0)"
by auto
-lemma nat_prime_factorization_unique:
+lemma prime_factorization_unique_nat:
"S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
n = (PROD p : S. p^(f p)) \<Longrightarrow>
S = prime_factors n & (ALL p. f p = multiplicity p n)"
@@ -407,23 +407,23 @@
unfolding multiset_def apply force
done
-lemma nat_prime_factors_characterization: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
+lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
prime_factors n = S"
- by (rule nat_prime_factorization_unique [THEN conjunct1, symmetric],
+ by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric],
assumption+)
-lemma nat_prime_factors_characterization':
+lemma prime_factors_characterization'_nat:
"finite {p. 0 < f (p::nat)} \<Longrightarrow>
(ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
- apply (rule nat_prime_factors_characterization)
+ apply (rule prime_factors_characterization_nat)
apply auto
done
(* A minor glitch:*)
-thm nat_prime_factors_characterization'
+thm prime_factors_characterization'_nat
[where f = "%x. f (int (x::nat))",
transferred direction: nat "op <= (0::int)", rule_format]
@@ -432,106 +432,106 @@
remain a comparison between nats. But the transfer still works.
*)
-lemma int_primes_characterization' [rule_format]:
+lemma primes_characterization'_int [rule_format]:
"finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
(ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
prime_factors (PROD p | p >=0 & 0 < f p . p ^ f p) =
{p. p >= 0 & 0 < f p}"
- apply (insert nat_prime_factors_characterization'
+ apply (insert prime_factors_characterization'_nat
[where f = "%x. f (int (x::nat))",
transferred direction: nat "op <= (0::int)"])
apply auto
done
-lemma int_prime_factors_characterization: "S = {p. 0 < f (p::int)} \<Longrightarrow>
+lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
prime_factors n = S"
apply simp
apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
apply (simp only:)
- apply (subst int_primes_characterization')
+ apply (subst primes_characterization'_int)
apply auto
- apply (auto simp add: int_prime_ge_0)
+ apply (auto simp add: prime_ge_0_int)
done
-lemma nat_multiplicity_characterization: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
+lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
multiplicity p n = f p"
- by (frule nat_prime_factorization_unique [THEN conjunct2, rule_format,
+ by (frule prime_factorization_unique_nat [THEN conjunct2, rule_format,
symmetric], auto)
-lemma nat_multiplicity_characterization': "finite {p. 0 < f (p::nat)} \<longrightarrow>
+lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
(ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
multiplicity p (PROD p | 0 < f p . p ^ f p) = f p"
apply (rule impI)+
- apply (rule nat_multiplicity_characterization)
+ apply (rule multiplicity_characterization_nat)
apply auto
done
-lemma int_multiplicity_characterization' [rule_format]:
+lemma multiplicity_characterization'_int [rule_format]:
"finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
(ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow>
multiplicity p (PROD p | p >= 0 & 0 < f p . p ^ f p) = f p"
- apply (insert nat_multiplicity_characterization'
+ apply (insert multiplicity_characterization'_nat
[where f = "%x. f (int (x::nat))",
transferred direction: nat "op <= (0::int)", rule_format])
apply auto
done
-lemma int_multiplicity_characterization: "S = {p. 0 < f (p::int)} \<Longrightarrow>
+lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
p >= 0 \<Longrightarrow> multiplicity p n = f p"
apply simp
apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
apply (simp only:)
- apply (subst int_multiplicity_characterization')
+ apply (subst multiplicity_characterization'_int)
apply auto
- apply (auto simp add: int_prime_ge_0)
+ apply (auto simp add: prime_ge_0_int)
done
-lemma nat_multiplicity_zero [simp]: "multiplicity (p::nat) 0 = 0"
+lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
-lemma int_multiplicity_zero [simp]: "multiplicity (p::int) 0 = 0"
+lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0"
by (simp add: multiplicity_int_def)
-lemma nat_multiplicity_one [simp]: "multiplicity p (1::nat) = 0"
- by (subst nat_multiplicity_characterization [where f = "%x. 0"], auto)
+lemma multiplicity_one_nat [simp]: "multiplicity p (1::nat) = 0"
+ by (subst multiplicity_characterization_nat [where f = "%x. 0"], auto)
-lemma int_multiplicity_one [simp]: "multiplicity p (1::int) = 0"
+lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0"
by (simp add: multiplicity_int_def)
-lemma nat_multiplicity_prime [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
- apply (subst nat_multiplicity_characterization
+lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
+ apply (subst multiplicity_characterization_nat
[where f = "(%q. if q = p then 1 else 0)"])
apply auto
apply (case_tac "x = p")
apply auto
done
-lemma int_multiplicity_prime [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
+lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
unfolding prime_int_def multiplicity_int_def by auto
-lemma nat_multiplicity_prime_power [simp]: "prime (p::nat) \<Longrightarrow>
+lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow>
multiplicity p (p^n) = n"
apply (case_tac "n = 0")
apply auto
- apply (subst nat_multiplicity_characterization
+ apply (subst multiplicity_characterization_nat
[where f = "(%q. if q = p then n else 0)"])
apply auto
apply (case_tac "x = p")
apply auto
done
-lemma int_multiplicity_prime_power [simp]: "prime (p::int) \<Longrightarrow>
+lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow>
multiplicity p (p^n) = n"
- apply (frule int_prime_ge_0)
+ apply (frule prime_ge_0_int)
apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
done
-lemma nat_multiplicity_nonprime [simp]: "~ prime (p::nat) \<Longrightarrow>
+lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow>
multiplicity p n = 0"
apply (case_tac "n = 0")
apply auto
@@ -539,22 +539,22 @@
apply (auto simp add: set_of_def multiplicity_nat_def)
done
-lemma int_multiplicity_nonprime [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
+lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
by (unfold multiplicity_int_def prime_int_def, auto)
-lemma nat_multiplicity_not_factor [simp]:
+lemma multiplicity_not_factor_nat [simp]:
"p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
- by (subst (asm) nat_prime_factors_altdef, auto)
+ by (subst (asm) prime_factors_altdef_nat, auto)
-lemma int_multiplicity_not_factor [simp]:
+lemma multiplicity_not_factor_int [simp]:
"p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0"
- by (subst (asm) int_prime_factors_altdef, auto)
+ by (subst (asm) prime_factors_altdef_int, auto)
-lemma nat_multiplicity_product_aux: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
+lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
(ALL p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
- apply (rule nat_prime_factorization_unique)
- apply (simp only: nat_prime_factors_altdef)
+ apply (rule prime_factorization_unique_nat)
+ apply (simp only: prime_factors_altdef_nat)
apply auto
apply (subst power_add)
apply (subst setprod_timesf)
@@ -568,7 +568,7 @@
(\<Prod>p\<in>prime_factors l - prime_factors k. 1)")
apply (erule ssubst)
apply (simp add: setprod_1)
- apply (erule nat_prime_factorization)
+ apply (erule prime_factorization_nat)
apply (rule setprod_cong, auto)
apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un
(prime_factors k - prime_factors l)")
@@ -579,47 +579,47 @@
(\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
apply (erule ssubst)
apply (simp add: setprod_1)
- apply (erule nat_prime_factorization)
+ apply (erule prime_factorization_nat)
apply (rule setprod_cong, auto)
done
(* transfer doesn't have the same problem here with the right
choice of rules. *)
-lemma int_multiplicity_product_aux:
+lemma multiplicity_product_aux_int:
assumes "(k::int) > 0" and "l > 0"
shows
"(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
(ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
- apply (rule nat_multiplicity_product_aux [transferred, of l k])
+ apply (rule multiplicity_product_aux_nat [transferred, of l k])
using prems apply auto
done
-lemma nat_prime_factors_product: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
+lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
prime_factors k Un prime_factors l"
- by (rule nat_multiplicity_product_aux [THEN conjunct1, symmetric])
+ by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric])
-lemma int_prime_factors_product: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
+lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
prime_factors k Un prime_factors l"
- by (rule int_multiplicity_product_aux [THEN conjunct1, symmetric])
+ by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric])
-lemma nat_multiplicity_product: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) =
+lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) =
multiplicity p k + multiplicity p l"
- by (rule nat_multiplicity_product_aux [THEN conjunct2, rule_format,
+ by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format,
symmetric])
-lemma int_multiplicity_product: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow>
+lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow>
multiplicity p (k * l) = multiplicity p k + multiplicity p l"
- by (rule int_multiplicity_product_aux [THEN conjunct2, rule_format,
+ by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format,
symmetric])
-lemma nat_multiplicity_setprod: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow>
+lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow>
multiplicity (p::nat) (PROD x : S. f x) =
(SUM x : S. multiplicity p (f x))"
apply (induct set: finite)
apply auto
- apply (subst nat_multiplicity_product)
+ apply (subst multiplicity_product_nat)
apply auto
done
@@ -643,12 +643,12 @@
add return: transfer_nat_int_sum_prod_closure3
del: transfer_nat_int_sum_prod2 (1)]
-lemma int_multiplicity_setprod: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow>
+lemma multiplicity_setprod_int: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow>
(ALL x : S. f x > 0) \<Longrightarrow>
multiplicity (p::int) (PROD x : S. f x) =
(SUM x : S. multiplicity p (f x))"
- apply (frule nat_multiplicity_setprod
+ apply (frule multiplicity_setprod_nat
[where f = "%x. nat(int(nat(f x)))",
transferred direction: nat "op <= (0::int)"])
apply auto
@@ -663,13 +663,13 @@
declare TransferMorphism_nat_int[transfer
add return: transfer_nat_int_sum_prod2 (1)]
-lemma nat_multiplicity_prod_prime_powers:
+lemma multiplicity_prod_prime_powers_nat:
"finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow>
multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
apply (subgoal_tac "(PROD p : S. p ^ f p) =
(PROD p : S. p ^ (%x. if x : S then f x else 0) p)")
apply (erule ssubst)
- apply (subst nat_multiplicity_characterization)
+ apply (subst multiplicity_characterization_nat)
prefer 5 apply (rule refl)
apply (rule refl)
apply auto
@@ -683,85 +683,85 @@
(* Here the issue with transfer is the implicit quantifier over S *)
-lemma int_multiplicity_prod_prime_powers:
+lemma multiplicity_prod_prime_powers_int:
"(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
apply (subgoal_tac "int ` nat ` S = S")
- apply (frule nat_multiplicity_prod_prime_powers [where f = "%x. f(int x)"
+ apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)"
and S = "nat ` S", transferred])
apply auto
apply (subst prime_int_def [symmetric])
apply auto
apply (subgoal_tac "xb >= 0")
apply force
- apply (rule int_prime_ge_0)
+ apply (rule prime_ge_0_int)
apply force
apply (subst transfer_nat_int_set_return_embed)
apply (unfold nat_set_def, auto)
done
-lemma nat_multiplicity_distinct_prime_power: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
+lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
apply (erule ssubst)
- apply (subst nat_multiplicity_prod_prime_powers)
+ apply (subst multiplicity_prod_prime_powers_nat)
apply auto
done
-lemma int_multiplicity_distinct_prime_power: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
+lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
- apply (frule int_prime_ge_0 [of q])
- apply (frule nat_multiplicity_distinct_prime_power [transferred leaving: n])
+ apply (frule prime_ge_0_int [of q])
+ apply (frule multiplicity_distinct_prime_power_nat [transferred leaving: n])
prefer 4
apply assumption
apply auto
done
-lemma nat_dvd_multiplicity:
+lemma dvd_multiplicity_nat:
"(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
apply (case_tac "x = 0")
- apply (auto simp add: dvd_def nat_multiplicity_product)
+ apply (auto simp add: dvd_def multiplicity_product_nat)
done
-lemma int_dvd_multiplicity:
+lemma dvd_multiplicity_int:
"(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow>
multiplicity p x <= multiplicity p y"
apply (case_tac "x = 0")
apply (auto simp add: dvd_def)
apply (subgoal_tac "0 < k")
- apply (auto simp add: int_multiplicity_product)
+ apply (auto simp add: multiplicity_product_int)
apply (erule zero_less_mult_pos)
apply arith
done
-lemma nat_dvd_prime_factors [intro]:
+lemma dvd_prime_factors_nat [intro]:
"0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
- apply (simp only: nat_prime_factors_altdef)
+ apply (simp only: prime_factors_altdef_nat)
apply auto
- apply (frule nat_dvd_multiplicity)
+ apply (frule dvd_multiplicity_nat)
apply auto
(* It is a shame that auto and arith don't get this. *)
apply (erule order_less_le_trans)back
apply assumption
done
-lemma int_dvd_prime_factors [intro]:
+lemma dvd_prime_factors_int [intro]:
"0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
- apply (auto simp add: int_prime_factors_altdef)
+ apply (auto simp add: prime_factors_altdef_int)
apply (erule order_less_le_trans)
- apply (rule int_dvd_multiplicity)
+ apply (rule dvd_multiplicity_int)
apply auto
done
-lemma nat_multiplicity_dvd: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
+lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow>
x dvd y"
- apply (subst nat_prime_factorization [of x], assumption)
- apply (subst nat_prime_factorization [of y], assumption)
+ apply (subst prime_factorization_nat [of x], assumption)
+ apply (subst prime_factorization_nat [of y], assumption)
apply (rule setprod_dvd_setprod_subset2)
apply force
- apply (subst nat_prime_factors_altdef)+
+ apply (subst prime_factors_altdef_nat)+
apply auto
(* Again, a shame that auto and arith don't get this. *)
apply (drule_tac x = xa in spec, auto)
@@ -769,14 +769,14 @@
apply blast
done
-lemma int_multiplicity_dvd: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
+lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow>
x dvd y"
- apply (subst int_prime_factorization [of x], assumption)
- apply (subst int_prime_factorization [of y], assumption)
+ apply (subst prime_factorization_int [of x], assumption)
+ apply (subst prime_factorization_int [of y], assumption)
apply (rule setprod_dvd_setprod_subset2)
apply force
- apply (subst int_prime_factors_altdef)+
+ apply (subst prime_factors_altdef_int)+
apply auto
apply (rule dvd_power_le)
apply auto
@@ -785,83 +785,83 @@
apply auto
done
-lemma nat_multiplicity_dvd': "(0::nat) < x \<Longrightarrow>
+lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow>
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
apply (cases "y = 0")
apply auto
- apply (rule nat_multiplicity_dvd, auto)
+ apply (rule multiplicity_dvd_nat, auto)
apply (case_tac "prime p")
apply auto
done
-lemma int_multiplicity_dvd': "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
+lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
apply (cases "y = 0")
apply auto
- apply (rule int_multiplicity_dvd, auto)
+ apply (rule multiplicity_dvd_int, auto)
apply (case_tac "prime p")
apply auto
done
-lemma nat_dvd_multiplicity_eq: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
+lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
(x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
- by (auto intro: nat_dvd_multiplicity nat_multiplicity_dvd)
+ by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat)
-lemma int_dvd_multiplicity_eq: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
+lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
(x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)"
- by (auto intro: int_dvd_multiplicity int_multiplicity_dvd)
+ by (auto intro: dvd_multiplicity_int multiplicity_dvd_int)
-lemma nat_prime_factors_altdef2: "(n::nat) > 0 \<Longrightarrow>
+lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow>
(p : prime_factors n) = (prime p & p dvd n)"
apply (case_tac "prime p")
apply auto
- apply (subst nat_prime_factorization [where n = n], assumption)
+ apply (subst prime_factorization_nat [where n = n], assumption)
apply (rule dvd_trans)
apply (rule dvd_power [where x = p and n = "multiplicity p n"])
- apply (subst (asm) nat_prime_factors_altdef, force)
+ apply (subst (asm) prime_factors_altdef_nat, force)
apply (rule dvd_setprod)
apply auto
- apply (subst nat_prime_factors_altdef)
- apply (subst (asm) nat_dvd_multiplicity_eq)
+ apply (subst prime_factors_altdef_nat)
+ apply (subst (asm) dvd_multiplicity_eq_nat)
apply auto
apply (drule spec [where x = p])
apply auto
done
-lemma int_prime_factors_altdef2:
+lemma prime_factors_altdef2_int:
assumes "(n::int) > 0"
shows "(p : prime_factors n) = (prime p & p dvd n)"
apply (case_tac "p >= 0")
- apply (rule nat_prime_factors_altdef2 [transferred])
+ apply (rule prime_factors_altdef2_nat [transferred])
using prems apply auto
- apply (auto simp add: int_prime_ge_0 int_prime_factors_ge_0)
+ apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
done
-lemma nat_multiplicity_eq:
+lemma multiplicity_eq_nat:
fixes x and y::nat
assumes [arith]: "x > 0" "y > 0" and
mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
shows "x = y"
apply (rule dvd_anti_sym)
- apply (auto intro: nat_multiplicity_dvd')
+ apply (auto intro: multiplicity_dvd'_nat)
done
-lemma int_multiplicity_eq:
+lemma multiplicity_eq_int:
fixes x and y::int
assumes [arith]: "x > 0" "y > 0" and
mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
shows "x = y"
apply (rule dvd_anti_sym [transferred])
- apply (auto intro: int_multiplicity_dvd')
+ apply (auto intro: multiplicity_dvd'_int)
done
subsection {* An application *}
-lemma nat_gcd_eq:
+lemma gcd_eq_nat:
assumes pos [arith]: "x > 0" "y > 0"
shows "gcd (x::nat) y =
(PROD p: prime_factors x Un prime_factors y.
@@ -874,26 +874,26 @@
have aux: "!!p. prime p \<Longrightarrow> multiplicity p z =
min (multiplicity p x) (multiplicity p y)"
unfolding z_def
- apply (subst nat_multiplicity_prod_prime_powers)
- apply (auto simp add: nat_multiplicity_not_factor)
+ apply (subst multiplicity_prod_prime_powers_nat)
+ apply (auto simp add: multiplicity_not_factor_nat)
done
have "z dvd x"
- by (intro nat_multiplicity_dvd', auto simp add: aux)
+ by (intro multiplicity_dvd'_nat, auto simp add: aux)
moreover have "z dvd y"
- by (intro nat_multiplicity_dvd', auto simp add: aux)
+ by (intro multiplicity_dvd'_nat, auto simp add: aux)
moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z"
apply auto
apply (case_tac "w = 0", auto)
- apply (erule nat_multiplicity_dvd')
- apply (auto intro: nat_dvd_multiplicity simp add: aux)
+ apply (erule multiplicity_dvd'_nat)
+ apply (auto intro: dvd_multiplicity_nat simp add: aux)
done
ultimately have "z = gcd x y"
- by (subst nat_gcd_unique [symmetric], blast)
+ by (subst gcd_unique_nat [symmetric], blast)
thus ?thesis
unfolding z_def by auto
qed
-lemma nat_lcm_eq:
+lemma lcm_eq_nat:
assumes pos [arith]: "x > 0" "y > 0"
shows "lcm (x::nat) y =
(PROD p: prime_factors x Un prime_factors y.
@@ -906,61 +906,61 @@
have aux: "!!p. prime p \<Longrightarrow> multiplicity p z =
max (multiplicity p x) (multiplicity p y)"
unfolding z_def
- apply (subst nat_multiplicity_prod_prime_powers)
- apply (auto simp add: nat_multiplicity_not_factor)
+ apply (subst multiplicity_prod_prime_powers_nat)
+ apply (auto simp add: multiplicity_not_factor_nat)
done
have "x dvd z"
- by (intro nat_multiplicity_dvd', auto simp add: aux)
+ by (intro multiplicity_dvd'_nat, auto simp add: aux)
moreover have "y dvd z"
- by (intro nat_multiplicity_dvd', auto simp add: aux)
+ by (intro multiplicity_dvd'_nat, auto simp add: aux)
moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w"
apply auto
apply (case_tac "w = 0", auto)
- apply (rule nat_multiplicity_dvd')
- apply (auto intro: nat_dvd_multiplicity simp add: aux)
+ apply (rule multiplicity_dvd'_nat)
+ apply (auto intro: dvd_multiplicity_nat simp add: aux)
done
ultimately have "z = lcm x y"
- by (subst nat_lcm_unique [symmetric], blast)
+ by (subst lcm_unique_nat [symmetric], blast)
thus ?thesis
unfolding z_def by auto
qed
-lemma nat_multiplicity_gcd:
+lemma multiplicity_gcd_nat:
assumes [arith]: "x > 0" "y > 0"
shows "multiplicity (p::nat) (gcd x y) =
min (multiplicity p x) (multiplicity p y)"
- apply (subst nat_gcd_eq)
+ apply (subst gcd_eq_nat)
apply auto
- apply (subst nat_multiplicity_prod_prime_powers)
+ apply (subst multiplicity_prod_prime_powers_nat)
apply auto
done
-lemma nat_multiplicity_lcm:
+lemma multiplicity_lcm_nat:
assumes [arith]: "x > 0" "y > 0"
shows "multiplicity (p::nat) (lcm x y) =
max (multiplicity p x) (multiplicity p y)"
- apply (subst nat_lcm_eq)
+ apply (subst lcm_eq_nat)
apply auto
- apply (subst nat_multiplicity_prod_prime_powers)
+ apply (subst multiplicity_prod_prime_powers_nat)
apply auto
done
-lemma nat_gcd_lcm_distrib: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
+lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
apply (case_tac "x = 0 | y = 0 | z = 0")
apply auto
- apply (rule nat_multiplicity_eq)
- apply (auto simp add: nat_multiplicity_gcd nat_multiplicity_lcm
- nat_lcm_pos)
+ apply (rule multiplicity_eq_nat)
+ apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat
+ lcm_pos_nat)
done
-lemma int_gcd_lcm_distrib: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
- apply (subst (1 2 3) int_gcd_abs)
- apply (subst int_lcm_abs)
+lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
+ apply (subst (1 2 3) gcd_abs_int)
+ apply (subst lcm_abs_int)
apply (subst (2) abs_of_nonneg)
apply force
- apply (rule nat_gcd_lcm_distrib [transferred])
+ apply (rule gcd_lcm_distrib_nat [transferred])
apply auto
done
--- a/src/HOL/RealDef.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/RealDef.thy Tue Jul 07 21:26:08 2009 +0200
@@ -925,7 +925,7 @@
have "?gcd' = 1"
proof -
have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
- by (rule nat_gcd_mult_distrib)
+ by (rule gcd_mult_distrib_nat)
with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
with gcd show ?thesis by auto
qed
--- a/src/HOL/ex/LocaleTest2.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/ex/LocaleTest2.thy Tue Jul 07 21:26:08 2009 +0200
@@ -599,7 +599,7 @@
apply (rule_tac x = "gcd x y" in exI)
apply auto [1]
apply (rule_tac x = "lcm x y" in exI)
- apply (auto intro: nat_lcm_dvd1 nat_lcm_dvd2 nat_lcm_least)
+ apply (auto intro: lcm_dvd1_nat lcm_dvd2_nat lcm_least_nat)
done
then interpret nat_dvd: dlat "op dvd :: [nat, nat] => bool" .
txt {* Interpretation to ease use of definitions, which are
@@ -613,7 +613,7 @@
apply (unfold nat_dvd.join_def)
apply (rule the_equality)
apply (unfold nat_dvd.is_sup_def)
- by (auto intro: nat_lcm_dvd1 nat_lcm_dvd2 nat_lcm_least)
+ by (auto intro: lcm_dvd1_nat lcm_dvd2_nat lcm_least_nat)
qed
text {* Interpreted theorems from the locales, involving defined terms. *}
--- a/src/HOL/ex/Sqrt.thy Tue Jul 07 17:50:03 2009 +0200
+++ b/src/HOL/ex/Sqrt.thy Tue Jul 07 21:26:08 2009 +0200
@@ -34,12 +34,12 @@
have "p dvd m \<and> p dvd n"
proof
from eq have "p dvd m\<twosuperior>" ..
- with `prime p` pos2 show "p dvd m" by (rule nat_prime_dvd_power)
+ with `prime p` pos2 show "p dvd m" by (rule prime_dvd_power_nat)
then obtain k where "m = p * k" ..
with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
then have "p dvd n\<twosuperior>" ..
- with `prime p` pos2 show "p dvd n" by (rule nat_prime_dvd_power)
+ with `prime p` pos2 show "p dvd n" by (rule prime_dvd_power_nat)
qed
then have "p dvd gcd m n" ..
with gcd have "p dvd 1" by simp
@@ -48,7 +48,7 @@
qed
corollary "sqrt (real (2::nat)) \<notin> \<rat>"
- by (rule sqrt_prime_irrational) (rule nat_two_is_prime)
+ by (rule sqrt_prime_irrational) (rule two_is_prime_nat)
subsection {* Variations *}
@@ -75,13 +75,13 @@
also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
then have "p dvd m\<twosuperior>" ..
- with `prime p` pos2 have dvd_m: "p dvd m" by (rule nat_prime_dvd_power)
+ with `prime p` pos2 have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
then obtain k where "m = p * k" ..
with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power2_eq_square mult_ac)
with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power2_eq_square)
then have "p dvd n\<twosuperior>" ..
- with `prime p` pos2 have "p dvd n" by (rule nat_prime_dvd_power)
- with dvd_m have "p dvd gcd m n" by (rule nat_gcd_greatest)
+ with `prime p` pos2 have "p dvd n" by (rule prime_dvd_power_nat)
+ with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)
with gcd have "p dvd 1" by simp
then have "p \<le> 1" by (simp add: dvd_imp_le)
with p show False by simp