Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
--- a/src/HOL/Algebra/Divisibility.thy Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Sun Feb 02 19:15:25 2014 +0000
@@ -2831,9 +2831,7 @@
proof -
interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
- apply (simp add: somegcd_meet[OF carr])
- apply (rule meet_closed[simplified], fact+)
- done
+ by (metis carr(1) carr(2) gcd_closed)
qed
lemma (in gcd_condition_monoid) gcd_divides_l:
@@ -2842,9 +2840,7 @@
proof -
interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
- apply (simp add: somegcd_meet[OF carr])
- apply (rule meet_left[simplified], fact+)
- done
+ by (metis carr(1) carr(2) gcd_isgcd isgcd_def)
qed
lemma (in gcd_condition_monoid) gcd_divides_r:
@@ -2853,9 +2849,7 @@
proof -
interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
- apply (simp add: somegcd_meet[OF carr])
- apply (rule meet_right[simplified], fact+)
- done
+ by (metis carr gcd_isgcd isgcd_def)
qed
lemma (in gcd_condition_monoid) gcd_divides:
@@ -2865,9 +2859,7 @@
proof -
interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
- apply (simp add: somegcd_meet L)
- apply (rule meet_le[simplified], fact+)
- done
+ by (metis gcd_isgcd isgcd_def assms)
qed
lemma (in gcd_condition_monoid) gcd_cong_l:
@@ -3409,13 +3401,7 @@
from aa2carr carr aa1fs aa2fs
have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
- apply (intro wfactors_mult_single)
- apply (rule wfactorsE[OF afs'], fast intro: nth_mem[OF len])
- apply (fast intro: nth_mem[OF len])
- apply fast
- apply fast
- apply assumption
- done
+ by (metis irrasi wfactors_mult_single)
with len carr aa1carr aa2carr aa1fs
have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
apply (intro wfactors_mult)
@@ -3429,23 +3415,15 @@
with carr
have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
by simp
-
with v2 afs' carr aa1carr aa2carr nth_mem[OF len]
have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
- apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'" "as'"])
- apply fast+
- apply (simp, fast)
- done
+ by (metis as' ee_wfactorsD m_closed)
then
have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
- apply (simp add: m_assoc[symmetric])
- apply (simp add: m_comm)
- done
+ by (metis aa1carr aa2carr asicarr m_lcomm)
from carr asiah
have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
- apply (intro mult_cong_l)
- apply (fast intro: associated_sym, simp+)
- done
+ by (metis associated_sym m_closed mult_cong_l)
also note t1
finally
have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
@@ -3530,7 +3508,6 @@
where ascarr[simp]: "set as \<subseteq> carrier G"
and afs: "wfactors G as a"
by (auto simp del: carr)
-
have "ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'"
by (metis afs ascarr assms ee_length wfactors_unique)
thus "EX c. ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" ..
@@ -3549,8 +3526,7 @@
apply (simp add: factorcount_def)
apply (rule theI2)
apply (rule alen)
- apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)
- apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)
+ apply (metis afs alen ascarr)+
done
from ascarr afs have "ac = length as" by (iprover intro: alen[rule_format])
--- a/src/HOL/Algebra/IntRing.thy Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Algebra/IntRing.thy Sun Feb 02 19:15:25 2014 +0000
@@ -239,14 +239,10 @@
lemma multiples_principalideal:
"principalideal {x * a | x. True } \<Z>"
-apply (subst int_Idl[symmetric], rule principalidealI)
- apply (rule int.genideal_ideal, simp)
-apply fast
-done
-
+by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)
lemma prime_primeideal:
- assumes prime: "prime (nat p)"
+ assumes prime: "prime p"
shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
apply (rule primeidealI)
apply (rule int.genideal_ideal, simp)
@@ -257,48 +253,18 @@
apply (elim exE)
proof -
fix a b x
- have ppos: "0 <= p"
- by (metis prime linear nat_0_iff zero_not_prime_nat)
- have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
- proof -
- fix x
- assume "nat p dvd nat (abs x)"
- hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
- thus "p dvd x" by (simp add: ppos)
- qed
- assume "a * b = x * p"
+ assume "a * b = x * int p"
hence "p dvd a * b" by simp
- hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff)
- hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
- hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)"
- by (metis prime prime_dvd_mult_eq_nat)
- hence "p dvd a | p dvd b" by (fast intro: unnat)
- thus "(EX x. a = x * p) | (EX x. b = x * p)"
- proof
- assume "p dvd a"
- hence "EX x. a = p * x" by (simp add: dvd_def)
- then obtain x
- where "a = p * x" by fast
- hence "a = x * p" by simp
- hence "EX x. a = x * p" by simp
- thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
- next
- assume "p dvd b"
- hence "EX x. b = p * x" by (simp add: dvd_def)
- then obtain x
- where "b = p * x" by fast
- hence "b = x * p" by simp
- hence "EX x. b = x * p" by simp
- thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
- qed
+ hence "p dvd a | p dvd b"
+ by (metis prime prime_dvd_mult_eq_int)
+ thus "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)"
+ by (metis dvd_def mult_commute)
next
- assume "UNIV = {uu. EX x. uu = x * p}"
- then obtain x where "1 = x * p" by best
- then have "p * x = 1" by (metis mult_commute)
- hence "\<bar>p * x\<bar> = 1" by simp
- hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
- then show "False"
- by (metis prime abs_of_pos one_not_prime_int prime_gt_0_int prime_int_def)
+ assume "UNIV = {uu. EX x. uu = x * int p}"
+ then obtain x where "1 = x * int p" by best
+ hence "\<bar>int p * x\<bar> = 1" by (simp add: mult_commute)
+ then show False
+ by (metis abs_of_nat int_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime)
qed
@@ -454,7 +420,7 @@
done
lemma ZFact_prime_is_domain:
- assumes pprime: "prime (nat p)"
+ assumes pprime: "prime p"
shows "domain (ZFact p)"
apply (unfold ZFact_def)
apply (rule primeideal.quotient_is_domain)
--- a/src/HOL/Number_Theory/Cong.thy Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Number_Theory/Cong.thy Sun Feb 02 19:15:25 2014 +0000
@@ -261,7 +261,8 @@
by (simp add: cong_altdef_int)
lemma cong_square_int:
- "\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk>
+ fixes a::int
+ shows "\<lbrakk> prime p; 0 < a; [a * a = 1] (mod p) \<rbrakk>
\<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
apply (simp only: cong_altdef_int)
apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
--- a/src/HOL/Number_Theory/Primes.thy Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Number_Theory/Primes.thy Sun Feb 02 19:15:25 2014 +0000
@@ -32,129 +32,76 @@
begin
declare One_nat_def [simp]
-
-class prime = one +
- fixes prime :: "'a \<Rightarrow> bool"
-
-instantiation nat :: prime
-begin
-
-definition prime_nat :: "nat \<Rightarrow> bool"
- where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
-
-instance ..
-
-end
-
-instantiation int :: prime
-begin
-
-definition prime_int :: "int \<Rightarrow> bool"
- where "prime_int p = prime (nat p)"
+declare [[coercion int]]
+declare [[coercion_enabled]]
-instance ..
-
-end
-
-
-subsection {* Set up Transfer *}
+definition prime :: "nat \<Rightarrow> bool"
+ where "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
-lemma transfer_nat_int_prime:
- "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
- unfolding gcd_int_def lcm_int_def prime_int_def by auto
-
-declare transfer_morphism_nat_int[transfer add return:
- transfer_nat_int_prime]
-
-lemma transfer_int_nat_prime: "prime (int x) = prime x"
- unfolding gcd_int_def lcm_int_def prime_int_def by auto
-
-declare transfer_morphism_int_nat[transfer add return:
- transfer_int_nat_prime]
+lemmas prime_nat_def = prime_def
subsection {* Primes *}
-lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
+lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
apply (metis dvd_eq_mod_eq_0 even_Suc even_def mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
done
-lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
- unfolding prime_int_def
- apply (frule prime_odd_nat)
- apply (auto simp add: even_nat_def)
- done
-
(* FIXME Is there a better way to handle these, rather than making them elim rules? *)
-lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
- unfolding prime_nat_def by auto
-
-lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
- unfolding prime_nat_def by auto
-
-lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
+lemma prime_gt_0_nat [elim]: "prime p \<Longrightarrow> p > 0"
unfolding prime_nat_def by auto
-lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
+lemma prime_ge_1_nat [elim]: "prime p \<Longrightarrow> p >= 1"
unfolding prime_nat_def by auto
-lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
- unfolding prime_nat_def by auto
-
-lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
- unfolding prime_nat_def by auto
-
-lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
+lemma prime_gt_1_nat [elim]: "prime p \<Longrightarrow> p > 1"
unfolding prime_nat_def by auto
-lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
- unfolding prime_int_def prime_nat_def by auto
-
-lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
- unfolding prime_int_def prime_nat_def by auto
-
-lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
- unfolding prime_int_def prime_nat_def by auto
-
-lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
- unfolding prime_int_def prime_nat_def by auto
+lemma prime_ge_Suc_0_nat [elim]: "prime p \<Longrightarrow> p >= Suc 0"
+ unfolding prime_nat_def by auto
-lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
- unfolding prime_int_def prime_nat_def by auto
-
+lemma prime_gt_Suc_0_nat [elim]: "prime p \<Longrightarrow> p > Suc 0"
+ unfolding prime_nat_def by auto
-lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
- m = 1 \<or> m = p))"
- using prime_nat_def [transferred]
- apply (cases "p >= 0")
- apply blast
- apply (auto simp add: prime_ge_0_int)
- done
+lemma prime_ge_2_nat [elim]: "prime p \<Longrightarrow> p >= 2"
+ unfolding prime_nat_def by auto
-lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
+lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
apply (unfold prime_nat_def)
apply (metis gcd_dvd1_nat gcd_dvd2_nat)
done
-lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
+lemma prime_int_altdef:
+ "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
+ m = 1 \<or> m = p))"
+ apply (simp add: prime_def)
+ apply (auto simp add: )
+ apply (metis One_nat_def int_1 nat_0_le nat_dvd_iff)
+ apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
+ done
+
+lemma prime_imp_coprime_int:
+ fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
apply (unfold prime_int_altdef)
apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
done
-lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
+lemma prime_dvd_mult_nat: "prime p \<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 prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
+lemma prime_dvd_mult_int:
+ fixes n::int shows "prime p \<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 prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
+lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
p dvd m * n = (p dvd m \<or> p dvd n)"
by (rule iffI, rule prime_dvd_mult_nat, auto)
-lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
- p dvd m * n = (p dvd m \<or> p dvd n)"
+lemma prime_dvd_mult_eq_int [simp]:
+ fixes n::int
+ shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
by (rule iffI, rule prime_dvd_mult_int, auto)
lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
@@ -163,25 +110,20 @@
by (metis mult_commute linorder_neq_iff linorder_not_le mult_1
n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
-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
- by (metis div_mult_self1_is_id div_mult_self2_is_id
- int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
-
-lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
+lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
by (induct n) auto
-lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
- by (induct n) (auto simp: prime_ge_0_int)
+lemma prime_dvd_power_int:
+ fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
+ by (induct n) auto
-lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
+lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow>
p dvd x^n \<longleftrightarrow> p dvd x"
by (cases n) (auto elim: prime_dvd_power_nat)
-lemma prime_dvd_power_int_iff: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow>
- p dvd x^n \<longleftrightarrow> p dvd x"
+lemma prime_dvd_power_int_iff:
+ fixes x::int
+ shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
by (cases n) (auto elim: prime_dvd_power_int)
@@ -190,80 +132,47 @@
lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
by (simp add: prime_nat_def)
-lemma zero_not_prime_int [simp]: "~prime (0::int)"
- by (simp add: prime_int_def)
-
lemma one_not_prime_nat [simp]: "~prime (1::nat)"
by (simp add: prime_nat_def)
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
by (simp add: prime_nat_def)
-lemma one_not_prime_int [simp]: "~prime (1::int)"
- by (simp add: prime_int_def)
-
lemma prime_nat_code [code]:
- "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
+ "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
apply (simp add: Ball_def)
apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
done
lemma prime_nat_simp:
- "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
+ "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
by (auto simp add: prime_nat_code)
lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
-lemma prime_int_code [code]:
- "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
-proof
- assume "?L"
- then show "?R"
- by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
-next
- assume "?R"
- then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int)
-qed
-
-lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
- by (auto simp add: prime_int_code)
-
-lemmas prime_int_simp_numeral [simp] = prime_int_simp [of "numeral m"] for m
-
lemma two_is_prime_nat [simp]: "prime (2::nat)"
by simp
-lemma two_is_prime_int [simp]: "prime (2::int)"
- by simp
-
text{* A bit of regression testing: *}
lemma "prime(97::nat)" by simp
-lemma "prime(97::int)" by simp
lemma "prime(997::nat)" by eval
-lemma "prime(997::int)" by eval
-lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
+lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
-lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
+lemma prime_imp_power_coprime_int:
+ fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
-lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
+lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
-lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
- by (metis leD linear prime_gt_0_int prime_imp_coprime_int prime_int_altdef)
-
lemma primes_imp_powers_coprime_nat:
- "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
+ "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
by (rule coprime_exp2_nat, rule primes_coprime_nat)
-lemma primes_imp_powers_coprime_int:
- "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
- by (rule coprime_exp2_int, rule primes_coprime_int)
-
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")
@@ -276,7 +185,7 @@
text {* One property of coprimality is easier to prove via prime factors. *}
lemma prime_divprod_pow_nat:
- assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
+ assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
shows "p^n dvd a \<or> p^n dvd b"
proof-
{ assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
@@ -316,7 +225,7 @@
subsection {* Infinitely many primes *}
-lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
+lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
proof-
have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
from prime_factor_nat [OF f1]
--- a/src/HOL/Number_Theory/Residues.thy Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Number_Theory/Residues.thy Sun Feb 02 19:15:25 2014 +0000
@@ -14,7 +14,6 @@
MiscAlgebra
begin
-
(*
A locale for residue rings
@@ -235,13 +234,14 @@
(* prime residues *)
locale residues_prime =
- fixes p :: int and R (structure)
+ fixes p and R (structure)
assumes p_prime [intro]: "prime p"
defines "R == residue_ring p"
sublocale residues_prime < residues p
apply (unfold R_def residues_def)
using p_prime apply auto
+ apply (metis (full_types) int_1 of_nat_less_iff prime_gt_1_nat)
done
context residues_prime
@@ -357,26 +357,26 @@
done
lemma fermat_theorem:
+ fixes a::int
assumes "prime p" and "~ (p dvd a)"
- shows "[a^(nat p - 1) = 1] (mod p)"
+ shows "[a^(p - 1) = 1] (mod p)"
proof -
from assms have "[a^phi p = 1] (mod p)"
apply (intro euler_theorem)
- (* auto should get this next part. matching across
- substitutions is needed. *)
- apply (frule prime_gt_1_int, arith)
- apply (subst gcd_commute_int, erule prime_imp_coprime_int, assumption)
+ apply (metis of_nat_0_le_iff)
+ apply (metis gcd_int.commute prime_imp_coprime_int)
done
also have "phi p = nat p - 1"
by (rule phi_prime, rule assms)
- finally show ?thesis .
+ finally show ?thesis
+ by (metis nat_int)
qed
lemma fermat_theorem_nat:
assumes "prime p" and "~ (p dvd a)"
shows "[a^(p - 1) = 1] (mod p)"
using fermat_theorem [of p a] assms
-by (metis int_1 nat_int of_nat_power prime_int_def transfer_int_nat_cong zdvd_int)
+by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int)
subsection {* Wilson's theorem *}
@@ -445,18 +445,20 @@
apply auto
done
also have "\<dots> = fact (p - 1) mod p"
- apply (subst fact_altdef_int)
- apply (insert assms, force)
- apply (subst res_prime_units_eq, rule refl)
+ apply (subst fact_altdef_nat)
+ apply (insert assms)
+ apply (subst res_prime_units_eq)
+ apply (simp add: int_setprod zmod_int setprod_int_eq)
done
finally have "fact (p - 1) mod p = \<ominus> \<one>".
- then show ?thesis by (simp add: res_to_cong_simps)
+ then show ?thesis
+ by (metis Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
qed
-lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
- apply (frule prime_gt_1_int)
+lemma wilson_theorem: "prime p \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
+ apply (frule prime_gt_1_nat)
apply (case_tac "p = 2")
- apply (subst fact_altdef_int, simp)
+ apply (subst fact_altdef_nat, simp)
apply (subst cong_int_def)
apply simp
apply (rule residues_prime.wilson_theorem1)
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Sun Feb 02 19:15:25 2014 +0000
@@ -242,7 +242,7 @@
lemma prime_factors_prime_int [intro]:
assumes "n >= 0" and "p : prime_factors (n::int)"
shows "prime p"
- apply (rule prime_factors_prime_nat [transferred, of n p])
+ apply (rule prime_factors_prime_nat [transferred, of n p, simplified])
using assms apply auto
done
@@ -252,8 +252,7 @@
done
lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow>
- p > (0::int)"
- apply (frule (1) prime_factors_prime_int)
+ int p > (0::int)"
apply auto
done
@@ -307,7 +306,7 @@
apply force
apply force
using assms
- apply (simp add: Abs_multiset_inverse set_of_def msetprod_multiplicity)
+ apply (simp add: set_of_def msetprod_multiplicity)
done
with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
by (simp add: Abs_multiset_inverse)
@@ -354,14 +353,15 @@
done
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>
+ finite S \<Longrightarrow> (ALL p:S. prime (nat 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 primes_characterization'_int)
apply auto
- apply (auto simp add: prime_ge_0_int)
+ apply (metis nat_int)
+ apply (metis le_cases nat_le_0 zero_not_prime_nat)
done
lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
@@ -390,14 +390,15 @@
done
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>
+ finite S \<Longrightarrow> (ALL p:S. prime (nat 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 multiplicity_characterization'_int)
apply auto
- apply (auto simp add: prime_ge_0_int)
+ apply (metis nat_int)
+ apply (metis le_cases nat_le_0 zero_not_prime_nat)
done
lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
@@ -415,25 +416,20 @@
lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0"
by (metis multiplicity_int_def multiplicity_one_nat' transfer_nat_int_numerals(2))
-lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
+lemma multiplicity_prime_nat [simp]: "prime p \<Longrightarrow> multiplicity p p = 1"
apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then 1 else 0)"])
apply auto
by (metis (full_types) less_not_refl)
-lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
- unfolding prime_int_def multiplicity_int_def by auto
-
-lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p (p^n) = n"
+lemma multiplicity_prime_power_nat [simp]: "prime p \<Longrightarrow> multiplicity p (p^n) = n"
apply (cases "n = 0")
apply auto
apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then n else 0)"])
apply auto
by (metis (full_types) less_not_refl)
-lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p (p^n) = n"
- apply (frule prime_ge_0_int)
- apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
- done
+lemma multiplicity_prime_power_int [simp]: "prime p \<Longrightarrow> multiplicity p ( (int p)^n) = n"
+ by (metis multiplicity_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> multiplicity p n = 0"
apply (cases "n = 0")
@@ -442,9 +438,6 @@
apply (auto simp add: set_of_def multiplicity_nat_def)
done
-lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
- unfolding multiplicity_int_def prime_int_def by auto
-
lemma multiplicity_not_factor_nat [simp]:
"p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
apply (subst (asm) prime_factors_altdef_nat)
@@ -584,18 +577,17 @@
(* Here the issue with transfer is the implicit quantifier over S *)
lemma multiplicity_prod_prime_powers_int:
- "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
+ "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p:S. prime (nat 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 multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)"
and S = "nat ` S", transferred])
apply auto
- apply (metis prime_int_def)
- apply (metis prime_ge_0_int)
- apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
+ apply (metis linear nat_0_iff zero_not_prime_nat)
+ apply (metis (full_types) image_iff int_nat_eq less_le less_linear nat_0_iff zero_not_prime_nat)
done
-lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
+lemma multiplicity_distinct_prime_power_nat: "prime p \<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)
@@ -603,14 +595,10 @@
apply auto
done
-lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
- p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
- 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 multiplicity_distinct_prime_power_int: "prime p \<Longrightarrow> prime q \<Longrightarrow>
+ p ~= q \<Longrightarrow> multiplicity p (int q ^ n) = 0"
+ by (metis multiplicity_distinct_prime_power_nat of_nat_power transfer_int_nat_multiplicity)
+
lemma dvd_multiplicity_nat:
"(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
@@ -670,11 +658,12 @@
by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
multiplicity_nonprime_nat neq0_conv)
-lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
+lemma multiplicity_dvd'_int:
+ fixes x::int and y::int
+ shows "0 < x \<Longrightarrow> 0 <= y \<Longrightarrow>
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
- by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv
- multiplicity_dvd_int multiplicity_nonprime_int nat_int transfer_nat_int_relations(4)
- less_le)
+by (metis GCD.dvd_int_iff abs_int_eq multiplicity_dvd'_nat multiplicity_int_def nat_int
+ zero_le_imp_eq_int zero_less_imp_eq_int)
lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
(x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
@@ -700,11 +689,7 @@
lemma prime_factors_altdef2_int:
assumes "(n::int) > 0"
shows "(p : prime_factors n) = (prime p & p dvd n)"
- apply (cases "p >= 0")
- apply (rule prime_factors_altdef2_nat [transferred])
- using assms apply auto
- apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
- done
+using assms by (simp add: prime_factors_altdef2_nat [transferred])
lemma multiplicity_eq_nat:
fixes x and y::nat
--- a/src/HOL/Set_Interval.thy Sat Feb 01 22:02:20 2014 +0100
+++ b/src/HOL/Set_Interval.thy Sun Feb 02 19:15:25 2014 +0000
@@ -1635,4 +1635,18 @@
transfer_int_nat_set_function_closures
]
+lemma setprod_int_plus_eq: "setprod int {i..i+j} = \<Prod>{int i..int (i+j)}"
+ by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)
+
+lemma setprod_int_eq: "setprod int {i..j} = \<Prod>{int i..int j}"
+proof (cases "i \<le> j")
+ case True
+ then show ?thesis
+ by (metis Nat.le_iff_add setprod_int_plus_eq)
+next
+ case False
+ then show ?thesis
+ by auto
+qed
+
end