--- a/NEWS Tue Aug 09 19:44:28 2016 +0200
+++ b/NEWS Tue Aug 09 19:45:01 2016 +0200
@@ -197,10 +197,12 @@
clashes.
INCOMPATIBILITY.
-* Number_Theory: algebraic foundation for primes: Introduction of
-predicates "is_prime", "irreducible", a "prime_factorization"
-function, the "factorial_ring" typeclass with instance proofs for
-nat, int, poly.
+* Number_Theory: algebraic foundation for primes: Generalisation of
+predicate "prime" and introduction of predicates "prime_elem",
+"irreducible", a "prime_factorization" function, and the "factorial_ring"
+typeclass with instance proofs for nat, int, poly. Some theorems now have
+different names, most notably "prime_def" is now "prime_nat_iff".
+INCOMPATIBILITY.
* Probability: Code generation and QuickCheck for Probability Mass
Functions.
--- a/src/FOL/simpdata.ML Tue Aug 09 19:44:28 2016 +0200
+++ b/src/FOL/simpdata.ML Tue Aug 09 19:45:01 2016 +0200
@@ -97,6 +97,7 @@
val contrapos = @{thm contrapos}
val contrapos2 = @{thm contrapos2}
val notnotD = @{thm notnotD}
+ val safe_tac = Cla.safe_tac
);
val split_tac = Splitter.split_tac;
--- a/src/HOL/Algebra/Divisibility.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Tue Aug 09 19:45:01 2016 +0200
@@ -2250,7 +2250,7 @@
subsection \<open>Irreducible Elements are Prime\<close>
-lemma (in factorial_monoid) irreducible_is_prime:
+lemma (in factorial_monoid) irreducible_prime:
assumes pirr: "irreducible G p"
and pcarr: "p \<in> carrier G"
shows "prime G p"
@@ -2340,7 +2340,7 @@
\<comment>"A version using @{const factors}, more complicated"
-lemma (in factorial_monoid) factors_irreducible_is_prime:
+lemma (in factorial_monoid) factors_irreducible_prime:
assumes pirr: "irreducible G p"
and pcarr: "p \<in> carrier G"
shows "prime G p"
@@ -3638,7 +3638,7 @@
done
sublocale factorial_monoid \<subseteq> primeness_condition_monoid
- by standard (rule irreducible_is_prime)
+ by standard (rule irreducible_prime)
lemma (in factorial_monoid) primeness_condition:
--- a/src/HOL/Algebra/Exponent.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Algebra/Exponent.thy Tue Aug 09 19:45:01 2016 +0200
@@ -15,8 +15,8 @@
text\<open>needed in this form to prove Sylow's theorem\<close>
corollary (in algebraic_semidom) div_combine:
- "\<lbrakk>is_prime_elem p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
- by (metis add_Suc_right mult.commute prime_power_dvd_cases)
+ "\<lbrakk>prime_elem p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
+ by (metis add_Suc_right mult.commute prime_elem_power_dvd_cases)
lemma exponent_p_a_m_k_equation:
fixes p :: nat
@@ -61,16 +61,16 @@
case (Suc k)
then have *: "(Suc (j+k) choose Suc k) > 0" by simp
then have "multiplicity p ((Suc (j+k) choose Suc k) * Suc k) = multiplicity p (Suc k)"
- by (subst Suc_times_binomial_eq [symmetric], subst prime_multiplicity_mult_distrib)
+ by (subst Suc_times_binomial_eq [symmetric], subst prime_elem_multiplicity_mult_distrib)
(insert p Suc.prems, simp_all add: eeq [symmetric] Suc.IH)
with p * show ?case
- by (subst (asm) prime_multiplicity_mult_distrib) simp_all
+ by (subst (asm) prime_elem_multiplicity_mult_distrib) simp_all
qed
text\<open>The lemma above, with two changes of variables\<close>
lemma p_not_div_choose:
assumes "k < K" and "k \<le> n"
- and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> multiplicity p (n - k + (K - j)) = multiplicity p (K - j)" "is_prime p"
+ and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> multiplicity p (n - k + (K - j)) = multiplicity p (K - j)" "prime p"
shows "multiplicity p (n choose k) = 0"
apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1])
apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff)
@@ -78,7 +78,7 @@
done
proposition const_p_fac:
- assumes "m>0" and prime: "is_prime p"
+ assumes "m>0" and prime: "prime p"
shows "multiplicity p (p^a * m choose p^a) = multiplicity p m"
proof-
from assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m"
@@ -93,13 +93,13 @@
by (subst times_binomial_minus1_eq [symmetric]) (auto simp: prime_gt_0_nat)
also from p have "p ^ a - Suc 0 \<le> p ^ a * m - Suc 0" by linarith
with prime * p have "multiplicity p ?rhs = multiplicity p (p ^ a * m)"
- by (subst prime_multiplicity_mult_distrib) auto
+ by (subst prime_elem_multiplicity_mult_distrib) auto
also have "\<dots> = a + multiplicity p m"
- using prime p by (subst prime_multiplicity_mult_distrib) simp_all
+ using prime p by (subst prime_elem_multiplicity_mult_distrib) simp_all
finally show ?thesis .
qed
then show ?thesis
- using prime p by (subst (asm) prime_multiplicity_mult_distrib) simp_all
+ using prime p by (subst (asm) prime_elem_multiplicity_mult_distrib) simp_all
qed
end
--- a/src/HOL/Algebra/Ideal.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Algebra/Ideal.thy Tue Aug 09 19:45:01 2016 +0200
@@ -99,7 +99,7 @@
assumes I_notcarr: "carrier R \<noteq> I"
and I_prime: "\<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I"
-lemma (in primeideal) is_primeideal: "primeideal I R"
+lemma (in primeideal) primeideal: "primeideal I R"
by (rule primeideal_axioms)
lemma primeidealI:
@@ -769,7 +769,7 @@
qed
text \<open>In a cring every maximal ideal is prime\<close>
-lemma (in cring) maximalideal_is_prime:
+lemma (in cring) maximalideal_prime:
assumes "maximalideal I R"
shows "primeideal I R"
proof -
--- a/src/HOL/Algebra/IntRing.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Algebra/IntRing.thy Tue Aug 09 19:45:01 2016 +0200
@@ -251,7 +251,7 @@
then obtain x where "1 = x * p" by best
then have "\<bar>p * x\<bar> = 1" by (simp add: mult.commute)
then show False using prime
- by (auto dest!: abs_zmult_eq_1 simp: is_prime_def)
+ by (auto dest!: abs_zmult_eq_1 simp: prime_def)
qed
--- a/src/HOL/Data_Structures/AA_Set.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Data_Structures/AA_Set.thy Tue Aug 09 19:45:01 2016 +0200
@@ -329,7 +329,7 @@
from lDown_tDouble and r obtain rrlv rrr rra rrl where
rr :"rr = Node rrlv rrr rra rrl" by (cases rr) auto
from lDown_tDouble show ?thesis unfolding adjust_def r rr
- apply (cases rl) apply (auto simp add: invar.simps(2))
+ apply (cases rl) apply (auto simp add: invar.simps(2) split!: if_split)
using lDown_tDouble by (auto simp: split_case lvl_0_iff elim:lvl.elims split: tree.split)
qed (auto simp: split_case invar.simps(2) adjust_def split: tree.splits)
--- a/src/HOL/Data_Structures/Tree234_Map.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Data_Structures/Tree234_Map.thy Tue Aug 09 19:45:01 2016 +0200
@@ -127,12 +127,11 @@
"sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
by(simp add: update_def inorder_upd)
-
lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
by(induction t rule: del.induct)
- ((auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)[1])+
-(* 200 secs (2015) *)
+ (auto simp: del_list_simps inorder_nodes del_minD split!: if_splits prod.splits)
+(* 30 secs (2016) *)
lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
inorder(delete x t) = del_list x (inorder t)"
@@ -142,21 +141,18 @@
subsection \<open>Balancedness\<close>
lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
-by (induct t) (auto, auto split: up\<^sub>i.split) (* 20 secs (2015) *)
+by (induct t) (auto, auto split!: if_split up\<^sub>i.split) (* 20 secs (2015) *)
lemma bal_update: "bal t \<Longrightarrow> bal (update x y t)"
by (simp add: update_def bal_upd)
-
lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
by(induction x t rule: del.induct)
- (auto simp add: heights height_del_min split: prod.split)
-(* 20 secs (2015) *)
+ (auto simp add: heights height_del_min split!: if_split prod.split)
lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
by(induction x t rule: del.induct)
- (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
-(* 100 secs (2015) *)
+ (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split)
corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
by(simp add: delete_def bal_tree\<^sub>d_del)
--- a/src/HOL/Data_Structures/Tree234_Set.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Data_Structures/Tree234_Set.thy Tue Aug 09 19:45:01 2016 +0200
@@ -206,14 +206,14 @@
by (induction t) (auto simp: elems_simps1 ball_Un)
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps2)
+by (induction t) (auto simp: elems_simps2 split!: if_splits)
subsubsection \<open>Functional correctness of insert:\<close>
lemma inorder_ins:
"sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
-by(induction t) (auto, auto simp: ins_list_simps split: up\<^sub>i.splits)
+by(induction t) (auto, auto simp: ins_list_simps split!: if_splits up\<^sub>i.splits)
lemma inorder_insert:
"sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
@@ -271,8 +271,8 @@
lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
by(induction t rule: del.induct)
- (auto simp: inorder_nodes del_list_simps del_minD split: prod.splits)
- (* 150 secs (2015) *)
+ (auto simp: inorder_nodes del_list_simps del_minD split!: if_split prod.splits)
+ (* 30 secs (2016) *)
lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
inorder(delete x t) = del_list x (inorder t)"
@@ -297,7 +297,7 @@
end
lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
-by (induct t) (auto, auto split: up\<^sub>i.split) (* 20 secs (2015) *)
+by (induct t) (auto split!: if_split up\<^sub>i.split)
text{* Now an alternative proof (by Brian Huffman) that runs faster because
@@ -486,7 +486,7 @@
lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
by(induction x t rule: del.induct)
- (auto simp add: heights height_del_min split: prod.split)
+ (auto simp add: heights height_del_min split!: if_split prod.split)
lemma bal_del_min:
"\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
@@ -495,8 +495,7 @@
lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
by(induction x t rule: del.induct)
- (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
-(* 60 secs (2015) *)
+ (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split)
corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
by(simp add: delete_def bal_tree\<^sub>d_del)
--- a/src/HOL/Data_Structures/Tree23_Map.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Data_Structures/Tree23_Map.thy Tue Aug 09 19:45:01 2016 +0200
@@ -89,7 +89,7 @@
lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
by(induction t rule: del.induct)
- (auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)
+ (auto simp: del_list_simps inorder_nodes del_minD split!: if_split prod.splits)
corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
inorder(delete x t) = del_list x (inorder t)"
@@ -99,7 +99,7 @@
subsection \<open>Balancedness\<close>
lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
-by (induct t) (auto split: up\<^sub>i.split)(* 16 secs in 2015 *)
+by (induct t) (auto split!: if_split up\<^sub>i.split)(* 16 secs in 2015 *)
corollary bal_update: "bal t \<Longrightarrow> bal (update x y t)"
by (simp add: update_def bal_upd)
--- a/src/HOL/Data_Structures/Tree23_Set.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Tue Aug 09 19:45:01 2016 +0200
@@ -191,7 +191,7 @@
lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
by(induction t rule: del.induct)
- (auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)
+ (auto simp: del_list_simps inorder_nodes del_minD split!: if_split prod.splits)
lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
inorder(delete x t) = del_list x (inorder t)"
@@ -217,7 +217,7 @@
end
lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
-by (induct t) (auto split: up\<^sub>i.split) (* 15 secs in 2015 *)
+by (induct t) (auto split!: if_split up\<^sub>i.split) (* 15 secs in 2015 *)
text{* Now an alternative proof (by Brian Huffman) that runs faster because
two properties (balance and height) are combined in one predicate. *}
--- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Tue Aug 09 19:45:01 2016 +0200
@@ -67,7 +67,7 @@
(* Goldblatt: Exercise 5.11(3a) - p 57 *)
lemma starprime:
"starprime = {p. 1 < p & (\<forall>m. m dvd p --> m = 1 | m = p)}"
-by (transfer, auto simp add: is_prime_nat_iff)
+by (transfer, auto simp add: prime_nat_iff)
(* Goldblatt Exercise 5.11(3b) - p 57 *)
lemma hyperprime_factor_exists [rule_format]:
@@ -277,7 +277,7 @@
apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}")
apply (force simp add: starprime_def)
apply (metis Compl_iff add.commute dvd_add_left_iff empty_iff hdvd_one_eq_one hypnat_one_not_prime
- imageE insert_iff mem_Collect_eq not_is_prime_0)
+ imageE insert_iff mem_Collect_eq not_prime_0)
done
end
--- a/src/HOL/Number_Theory/Eratosthenes.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy Tue Aug 09 19:45:01 2016 +0200
@@ -295,8 +295,8 @@
from 2 show ?thesis
apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
dest: prime_gt_Suc_0_nat)
- apply (metis One_nat_def Suc_le_eq less_not_refl is_prime_nat_iff)
- apply (metis One_nat_def Suc_le_eq aux is_prime_nat_iff)
+ apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_iff)
+ apply (metis One_nat_def Suc_le_eq aux prime_nat_iff)
done
qed
qed
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Tue Aug 09 19:45:01 2016 +0200
@@ -411,7 +411,7 @@
interpret semiring_gcd 1 0 "op *" gcd_eucl lcm_eucl "op div" "op +" "op -" normalize unit_factor
by standard (rule lcm_gcd_eucl_facts; assumption)+
fix p assume p: "irreducible p"
- thus "is_prime_elem p" by (rule irreducible_imp_prime_gcd)
+ thus "prime_elem p" by (rule irreducible_imp_prime_elem_gcd)
qed
lemma gcd_eucl_eq_gcd_factorial: "gcd_eucl = gcd_factorial"
--- a/src/HOL/Number_Theory/Factorial_Ring.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy Tue Aug 09 19:45:01 2016 +0200
@@ -54,51 +54,51 @@
lemma irreducibleD: "irreducible p \<Longrightarrow> p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1"
by (simp add: irreducible_def)
-definition is_prime_elem :: "'a \<Rightarrow> bool" where
- "is_prime_elem p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p dvd (a * b) \<longrightarrow> p dvd a \<or> p dvd b)"
+definition prime_elem :: "'a \<Rightarrow> bool" where
+ "prime_elem p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p dvd (a * b) \<longrightarrow> p dvd a \<or> p dvd b)"
-lemma not_is_prime_elem_zero [simp]: "\<not>is_prime_elem 0"
- by (simp add: is_prime_elem_def)
+lemma not_prime_elem_zero [simp]: "\<not>prime_elem 0"
+ by (simp add: prime_elem_def)
-lemma is_prime_elem_not_unit: "is_prime_elem p \<Longrightarrow> \<not>p dvd 1"
- by (simp add: is_prime_elem_def)
+lemma prime_elem_not_unit: "prime_elem p \<Longrightarrow> \<not>p dvd 1"
+ by (simp add: prime_elem_def)
-lemma is_prime_elemI:
- "p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b) \<Longrightarrow> is_prime_elem p"
- by (simp add: is_prime_elem_def)
+lemma prime_elemI:
+ "p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b) \<Longrightarrow> prime_elem p"
+ by (simp add: prime_elem_def)
-lemma prime_divides_productD:
- "is_prime_elem p \<Longrightarrow> p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b"
- by (simp add: is_prime_elem_def)
+lemma prime_elem_dvd_multD:
+ "prime_elem p \<Longrightarrow> p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b"
+ by (simp add: prime_elem_def)
-lemma prime_dvd_mult_iff:
- "is_prime_elem p \<Longrightarrow> p dvd (a * b) \<longleftrightarrow> p dvd a \<or> p dvd b"
- by (auto simp: is_prime_elem_def)
+lemma prime_elem_dvd_mult_iff:
+ "prime_elem p \<Longrightarrow> p dvd (a * b) \<longleftrightarrow> p dvd a \<or> p dvd b"
+ by (auto simp: prime_elem_def)
-lemma not_is_prime_elem_one [simp]:
- "\<not> is_prime_elem 1"
- by (auto dest: is_prime_elem_not_unit)
+lemma not_prime_elem_one [simp]:
+ "\<not> prime_elem 1"
+ by (auto dest: prime_elem_not_unit)
-lemma is_prime_elem_not_zeroI:
- assumes "is_prime_elem p"
+lemma prime_elem_not_zeroI:
+ assumes "prime_elem p"
shows "p \<noteq> 0"
using assms by (auto intro: ccontr)
-lemma is_prime_elem_dvd_power:
- "is_prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
- by (induction n) (auto dest: prime_divides_productD intro: dvd_trans[of _ 1])
+lemma prime_elem_dvd_power:
+ "prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
+ by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1])
-lemma is_prime_elem_dvd_power_iff:
- "is_prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
- by (auto dest: is_prime_elem_dvd_power intro: dvd_trans)
+lemma prime_elem_dvd_power_iff:
+ "prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
+ by (auto dest: prime_elem_dvd_power intro: dvd_trans)
-lemma is_prime_elem_imp_nonzero [simp]:
- "ASSUMPTION (is_prime_elem x) \<Longrightarrow> x \<noteq> 0"
- unfolding ASSUMPTION_def by (rule is_prime_elem_not_zeroI)
+lemma prime_elem_imp_nonzero [simp]:
+ "ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 0"
+ unfolding ASSUMPTION_def by (rule prime_elem_not_zeroI)
-lemma is_prime_elem_imp_not_one [simp]:
- "ASSUMPTION (is_prime_elem x) \<Longrightarrow> x \<noteq> 1"
+lemma prime_elem_imp_not_one [simp]:
+ "ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 1"
unfolding ASSUMPTION_def by auto
end
@@ -110,42 +110,42 @@
lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
by (subst mult.commute) (rule mult_unit_dvd_iff)
-lemma prime_imp_irreducible:
- assumes "is_prime_elem p"
+lemma prime_elem_imp_irreducible:
+ assumes "prime_elem p"
shows "irreducible p"
proof (rule irreducibleI)
fix a b
assume p_eq: "p = a * b"
with assms have nz: "a \<noteq> 0" "b \<noteq> 0" by auto
from p_eq have "p dvd a * b" by simp
- with \<open>is_prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_divides_productD)
+ with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD)
with \<open>p = a * b\<close> have "a * b dvd 1 * b \<or> a * b dvd a * 1" by auto
thus "a dvd 1 \<or> b dvd 1"
by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)])
-qed (insert assms, simp_all add: is_prime_elem_def)
+qed (insert assms, simp_all add: prime_elem_def)
-lemma is_prime_elem_mono:
- assumes "is_prime_elem p" "\<not>q dvd 1" "q dvd p"
- shows "is_prime_elem q"
+lemma prime_elem_mono:
+ assumes "prime_elem p" "\<not>q dvd 1" "q dvd p"
+ shows "prime_elem q"
proof -
from \<open>q dvd p\<close> obtain r where r: "p = q * r" by (elim dvdE)
hence "p dvd q * r" by simp
- with \<open>is_prime_elem p\<close> have "p dvd q \<or> p dvd r" by (rule prime_divides_productD)
+ with \<open>prime_elem p\<close> have "p dvd q \<or> p dvd r" by (rule prime_elem_dvd_multD)
hence "p dvd q"
proof
assume "p dvd r"
then obtain s where s: "r = p * s" by (elim dvdE)
from r have "p * 1 = p * (q * s)" by (subst (asm) s) (simp add: mult_ac)
- with \<open>is_prime_elem p\<close> have "q dvd 1"
+ with \<open>prime_elem p\<close> have "q dvd 1"
by (subst (asm) mult_cancel_left) auto
with \<open>\<not>q dvd 1\<close> show ?thesis by contradiction
qed
show ?thesis
- proof (rule is_prime_elemI)
+ proof (rule prime_elemI)
fix a b assume "q dvd (a * b)"
with \<open>p dvd q\<close> have "p dvd (a * b)" by (rule dvd_trans)
- with \<open>is_prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_divides_productD)
+ with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD)
with \<open>q dvd p\<close> show "q dvd a \<or> q dvd b" by (blast intro: dvd_trans)
qed (insert assms, auto)
qed
@@ -178,12 +178,12 @@
"irreducible x \<longleftrightarrow> x \<noteq> 0 \<and> \<not>is_unit x \<and> (\<forall>b. b dvd x \<longrightarrow> x dvd b \<or> is_unit b)"
using irreducibleI'[of x] irreducibleD'[of x] irreducible_not_unit[of x] by auto
-lemma is_prime_elem_multD:
- assumes "is_prime_elem (a * b)"
+lemma prime_elem_multD:
+ assumes "prime_elem (a * b)"
shows "is_unit a \<or> is_unit b"
proof -
- from assms have "a \<noteq> 0" "b \<noteq> 0" by (auto dest!: is_prime_elem_not_zeroI)
- moreover from assms prime_divides_productD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
+ from assms have "a \<noteq> 0" "b \<noteq> 0" by (auto dest!: prime_elem_not_zeroI)
+ moreover from assms prime_elem_dvd_multD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
by auto
ultimately show ?thesis
using dvd_times_left_cancel_iff [of a b 1]
@@ -191,36 +191,62 @@
by auto
qed
-lemma is_prime_elemD2:
- assumes "is_prime_elem p" and "a dvd p" and "\<not> is_unit a"
+lemma prime_elemD2:
+ assumes "prime_elem p" and "a dvd p" and "\<not> is_unit a"
shows "p dvd a"
proof -
from \<open>a dvd p\<close> obtain b where "p = a * b" ..
- with \<open>is_prime_elem p\<close> is_prime_elem_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
+ with \<open>prime_elem p\<close> prime_elem_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
with \<open>p = a * b\<close> show ?thesis
by (auto simp add: mult_unit_dvd_iff)
qed
+lemma prime_elem_dvd_msetprodE:
+ assumes "prime_elem p"
+ assumes dvd: "p dvd msetprod A"
+ obtains a where "a \<in># A" and "p dvd a"
+proof -
+ from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
+ proof (induct A)
+ case empty then show ?case
+ using \<open>prime_elem p\<close> by (simp add: prime_elem_not_unit)
+ next
+ case (add A a)
+ then have "p dvd msetprod A * a" by simp
+ with \<open>prime_elem p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
+ by (blast dest: prime_elem_dvd_multD)
+ then show ?case proof cases
+ case B then show ?thesis by auto
+ next
+ case A
+ with add.hyps obtain b where "b \<in># A" "p dvd b"
+ by auto
+ then show ?thesis by auto
+ qed
+ qed
+ with that show thesis by blast
+qed
+
context
begin
-private lemma is_prime_elem_powerD:
- assumes "is_prime_elem (p ^ n)"
- shows "is_prime_elem p \<and> n = 1"
+private lemma prime_elem_powerD:
+ assumes "prime_elem (p ^ n)"
+ shows "prime_elem p \<and> n = 1"
proof (cases n)
case (Suc m)
note assms
also from Suc have "p ^ n = p * p^m" by simp
- finally have "is_unit p \<or> is_unit (p^m)" by (rule is_prime_elem_multD)
- moreover from assms have "\<not>is_unit p" by (simp add: is_prime_elem_def is_unit_power_iff)
+ finally have "is_unit p \<or> is_unit (p^m)" by (rule prime_elem_multD)
+ moreover from assms have "\<not>is_unit p" by (simp add: prime_elem_def is_unit_power_iff)
ultimately have "is_unit (p ^ m)" by simp
with \<open>\<not>is_unit p\<close> have "m = 0" by (simp add: is_unit_power_iff)
with Suc assms show ?thesis by simp
qed (insert assms, simp_all)
-lemma is_prime_elem_power_iff:
- "is_prime_elem (p ^ n) \<longleftrightarrow> is_prime_elem p \<and> n = 1"
- by (auto dest: is_prime_elem_powerD)
+lemma prime_elem_power_iff:
+ "prime_elem (p ^ n) \<longleftrightarrow> prime_elem p \<and> n = 1"
+ by (auto dest: prime_elem_powerD)
end
@@ -229,17 +255,17 @@
by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff
mult_unit_dvd_iff dvd_mult_unit_iff)
-lemma is_prime_elem_mult_unit_left:
- "is_unit a \<Longrightarrow> is_prime_elem (a * p) \<longleftrightarrow> is_prime_elem p"
- by (auto simp: is_prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff)
+lemma prime_elem_mult_unit_left:
+ "is_unit a \<Longrightarrow> prime_elem (a * p) \<longleftrightarrow> prime_elem p"
+ by (auto simp: prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff)
-lemma prime_dvd_cases:
- assumes pk: "p*k dvd m*n" and p: "is_prime_elem p"
+lemma prime_elem_dvd_cases:
+ assumes pk: "p*k dvd m*n" and p: "prime_elem p"
shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)"
proof -
have "p dvd m*n" using dvd_mult_left pk by blast
then consider "p dvd m" | "p dvd n"
- using p prime_dvd_mult_iff by blast
+ using p prime_elem_dvd_mult_iff by blast
then show ?thesis
proof cases
case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel)
@@ -254,8 +280,8 @@
qed
qed
-lemma prime_power_dvd_prod:
- assumes pc: "p^c dvd m*n" and p: "is_prime_elem p"
+lemma prime_elem_power_dvd_prod:
+ assumes pc: "p^c dvd m*n" and p: "prime_elem p"
shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n"
using pc
proof (induct c arbitrary: m n)
@@ -263,7 +289,7 @@
next
case (Suc c)
consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y"
- using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
+ using prime_elem_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
then show ?case
proof cases
case (1 x)
@@ -284,217 +310,40 @@
lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y"
by arith
-lemma prime_power_dvd_cases:
- "\<lbrakk>p^c dvd m * n; a + b = Suc c; is_prime_elem p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
- using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem)
-
-end
-
-context normalization_semidom
-begin
-
-lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x"
- using irreducible_mult_unit_left[of "1 div unit_factor x" x]
- by (cases "x = 0") (simp_all add: unit_div_commute)
-
-lemma is_prime_elem_normalize_iff [simp]: "is_prime_elem (normalize x) = is_prime_elem x"
- using is_prime_elem_mult_unit_left[of "1 div unit_factor x" x]
- by (cases "x = 0") (simp_all add: unit_div_commute)
-
-definition is_prime :: "'a \<Rightarrow> bool" where
- "is_prime p \<longleftrightarrow> is_prime_elem p \<and> normalize p = p"
-
-lemma not_is_prime_0 [simp]: "\<not>is_prime 0" by (simp add: is_prime_def)
-
-lemma not_is_prime_unit: "is_unit x \<Longrightarrow> \<not>is_prime x"
- using is_prime_elem_not_unit[of x] by (auto simp add: is_prime_def)
-
-lemma not_is_prime_1 [simp]: "\<not>is_prime 1" by (simp add: not_is_prime_unit)
-
-lemma is_primeI: "is_prime_elem x \<Longrightarrow> normalize x = x \<Longrightarrow> is_prime x"
- by (simp add: is_prime_def)
-
-lemma prime_imp_prime_elem [dest]: "is_prime p \<Longrightarrow> is_prime_elem p"
- by (simp add: is_prime_def)
-
-lemma normalize_is_prime: "is_prime p \<Longrightarrow> normalize p = p"
- by (simp add: is_prime_def)
-
-lemma is_prime_normalize_iff [simp]: "is_prime (normalize p) \<longleftrightarrow> is_prime_elem p"
- by (auto simp add: is_prime_def)
-
-lemma is_prime_power_iff:
- "is_prime (p ^ n) \<longleftrightarrow> is_prime p \<and> n = 1"
- by (auto simp: is_prime_def is_prime_elem_power_iff)
-
-lemma is_prime_elem_not_unit' [simp]:
- "ASSUMPTION (is_prime_elem x) \<Longrightarrow> \<not>is_unit x"
- unfolding ASSUMPTION_def by (rule is_prime_elem_not_unit)
-
-lemma is_prime_imp_nonzero [simp]:
- "ASSUMPTION (is_prime x) \<Longrightarrow> x \<noteq> 0"
- unfolding ASSUMPTION_def is_prime_def by auto
-
-lemma is_prime_imp_not_one [simp]:
- "ASSUMPTION (is_prime x) \<Longrightarrow> x \<noteq> 1"
- unfolding ASSUMPTION_def by auto
-
-lemma is_prime_not_unit' [simp]:
- "ASSUMPTION (is_prime x) \<Longrightarrow> \<not>is_unit x"
- unfolding ASSUMPTION_def is_prime_def by auto
-
-lemma is_prime_normalize' [simp]: "ASSUMPTION (is_prime x) \<Longrightarrow> normalize x = x"
- unfolding ASSUMPTION_def is_prime_def by simp
-
-lemma unit_factor_is_prime: "is_prime x \<Longrightarrow> unit_factor x = 1"
- using unit_factor_normalize[of x] unfolding is_prime_def by auto
-
-lemma unit_factor_is_prime' [simp]: "ASSUMPTION (is_prime x) \<Longrightarrow> unit_factor x = 1"
- unfolding ASSUMPTION_def by (rule unit_factor_is_prime)
-
-lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (is_prime x) \<Longrightarrow> is_prime_elem x"
- by (simp add: is_prime_def ASSUMPTION_def)
-
- lemma is_prime_elem_associated:
- assumes "is_prime_elem p" and "is_prime_elem q" and "q dvd p"
- shows "normalize q = normalize p"
-using \<open>q dvd p\<close> proof (rule associatedI)
- from \<open>is_prime_elem q\<close> have "\<not> is_unit q"
- by (simp add: is_prime_elem_not_unit)
- with \<open>is_prime_elem p\<close> \<open>q dvd p\<close> show "p dvd q"
- by (blast intro: is_prime_elemD2)
-qed
-
-lemma is_prime_dvd_multD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
- by (intro prime_divides_productD) simp_all
-
-lemma is_prime_dvd_mult_iff [simp]: "is_prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
- by (auto dest: is_prime_dvd_multD)
-
-lemma is_prime_dvd_power:
- "is_prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
- by (auto dest!: is_prime_elem_dvd_power simp: is_prime_def)
-
-lemma is_prime_dvd_power_iff:
- "is_prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
- by (intro is_prime_elem_dvd_power_iff) simp_all
+lemma prime_elem_power_dvd_cases:
+ "\<lbrakk>p^c dvd m * n; a + b = Suc c; prime_elem p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
+ using power_le_dvd by (blast dest: prime_elem_power_dvd_prod add_eq_Suc_lem)
-lemma prime_dvd_msetprodE:
- assumes "is_prime_elem p"
- assumes dvd: "p dvd msetprod A"
- obtains a where "a \<in># A" and "p dvd a"
-proof -
- from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
- proof (induct A)
- case empty then show ?case
- using \<open>is_prime_elem p\<close> by (simp add: is_prime_elem_not_unit)
- next
- case (add A a)
- then have "p dvd msetprod A * a" by simp
- with \<open>is_prime_elem p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
- by (blast dest: prime_divides_productD)
- then show ?case proof cases
- case B then show ?thesis by auto
- next
- case A
- with add.hyps obtain b where "b \<in># A" "p dvd b"
- by auto
- then show ?thesis by auto
- qed
- qed
- with that show thesis by blast
-qed
-
-lemma msetprod_subset_imp_dvd:
- assumes "A \<subseteq># B"
- shows "msetprod A dvd msetprod B"
-proof -
- from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
- also have "msetprod \<dots> = msetprod (B - A) * msetprod A" by simp
- also have "msetprod A dvd \<dots>" by simp
- finally show ?thesis .
-qed
-
-lemma prime_dvd_msetprod_iff: "is_prime p \<Longrightarrow> p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
- by (induction A) (simp_all add: prime_dvd_mult_iff prime_imp_prime_elem, blast+)
+lemma prime_elem_not_unit' [simp]:
+ "ASSUMPTION (prime_elem x) \<Longrightarrow> \<not>is_unit x"
+ unfolding ASSUMPTION_def by (rule prime_elem_not_unit)
-lemma primes_dvd_imp_eq:
- assumes "is_prime p" "is_prime q" "p dvd q"
- shows "p = q"
-proof -
- from assms have "irreducible q" by (simp add: prime_imp_irreducible is_prime_def)
- from irreducibleD'[OF this \<open>p dvd q\<close>] assms have "q dvd p" by simp
- with \<open>p dvd q\<close> have "normalize p = normalize q" by (rule associatedI)
- with assms show "p = q" by simp
-qed
-
-lemma prime_dvd_msetprod_primes_iff:
- assumes "is_prime p" "\<And>q. q \<in># A \<Longrightarrow> is_prime q"
- shows "p dvd msetprod A \<longleftrightarrow> p \<in># A"
-proof -
- from assms(1) have "p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_msetprod_iff)
- also from assms have "\<dots> \<longleftrightarrow> p \<in># A" by (auto dest: primes_dvd_imp_eq)
- finally show ?thesis .
-qed
-
-lemma msetprod_primes_dvd_imp_subset:
- assumes "msetprod A dvd msetprod B" "\<And>p. p \<in># A \<Longrightarrow> is_prime p" "\<And>p. p \<in># B \<Longrightarrow> is_prime p"
- shows "A \<subseteq># B"
-using assms
-proof (induction A arbitrary: B)
- case empty
- thus ?case by simp
-next
- case (add A p B)
- hence p: "is_prime p" by simp
- define B' where "B' = B - {#p#}"
- from add.prems have "p dvd msetprod B" by (simp add: dvd_mult_right)
- with add.prems have "p \<in># B"
- by (subst (asm) (2) prime_dvd_msetprod_primes_iff) simp_all
- hence B: "B = B' + {#p#}" by (simp add: B'_def)
- from add.prems p have "A \<subseteq># B'" by (intro add.IH) (simp_all add: B)
- thus ?case by (simp add: B)
-qed
-
-lemma normalize_msetprod_primes:
- "(\<And>p. p \<in># A \<Longrightarrow> is_prime p) \<Longrightarrow> normalize (msetprod A) = msetprod A"
-proof (induction A)
- case (add A p)
- hence "is_prime p" by simp
- hence "normalize p = p" by simp
- with add show ?case by (simp add: normalize_mult)
-qed simp_all
-
-lemma msetprod_dvd_msetprod_primes_iff:
- assumes "\<And>x. x \<in># A \<Longrightarrow> is_prime x" "\<And>x. x \<in># B \<Longrightarrow> is_prime x"
- shows "msetprod A dvd msetprod B \<longleftrightarrow> A \<subseteq># B"
- using assms by (auto intro: msetprod_subset_imp_dvd msetprod_primes_dvd_imp_subset)
-
-lemma prime_dvd_power_iff:
- assumes "is_prime_elem p"
+lemma prime_elem_dvd_power_iff:
+ assumes "prime_elem p"
shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
- using assms by (induct n) (auto dest: is_prime_elem_not_unit prime_divides_productD)
+ using assms by (induct n) (auto dest: prime_elem_not_unit prime_elem_dvd_multD)
lemma prime_power_dvd_multD:
- assumes "is_prime_elem p"
+ assumes "prime_elem p"
assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a"
shows "p ^ n dvd b"
-using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> proof (induct n arbitrary: b)
+ using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close>
+proof (induct n arbitrary: b)
case 0 then show ?case by simp
next
case (Suc n) show ?case
proof (cases "n = 0")
- case True with Suc \<open>is_prime_elem p\<close> \<open>\<not> p dvd a\<close> show ?thesis
- by (simp add: prime_dvd_mult_iff)
+ case True with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> show ?thesis
+ by (simp add: prime_elem_dvd_mult_iff)
next
case False then have "n > 0" by simp
- from \<open>is_prime_elem p\<close> have "p \<noteq> 0" by auto
+ from \<open>prime_elem p\<close> have "p \<noteq> 0" by auto
from Suc.prems have *: "p * p ^ n dvd a * b"
by simp
then have "p dvd a * b"
by (rule dvd_mult_left)
- with Suc \<open>is_prime_elem p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
- by (simp add: prime_dvd_mult_iff)
+ with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
+ by (simp add: prime_elem_dvd_mult_iff)
moreover define c where "c = b div p"
ultimately have b: "b = p * c" by simp
with * have "p * p ^ n dvd p * (a * c)"
@@ -508,6 +357,158 @@
qed
qed
+end
+
+context normalization_semidom
+begin
+
+lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x"
+ using irreducible_mult_unit_left[of "1 div unit_factor x" x]
+ by (cases "x = 0") (simp_all add: unit_div_commute)
+
+lemma prime_elem_normalize_iff [simp]: "prime_elem (normalize x) = prime_elem x"
+ using prime_elem_mult_unit_left[of "1 div unit_factor x" x]
+ by (cases "x = 0") (simp_all add: unit_div_commute)
+
+lemma prime_elem_associated:
+ assumes "prime_elem p" and "prime_elem q" and "q dvd p"
+ shows "normalize q = normalize p"
+using \<open>q dvd p\<close> proof (rule associatedI)
+ from \<open>prime_elem q\<close> have "\<not> is_unit q"
+ by (auto simp add: prime_elem_not_unit)
+ with \<open>prime_elem p\<close> \<open>q dvd p\<close> show "p dvd q"
+ by (blast intro: prime_elemD2)
+qed
+
+definition prime :: "'a \<Rightarrow> bool" where
+ "prime p \<longleftrightarrow> prime_elem p \<and> normalize p = p"
+
+lemma not_prime_0 [simp]: "\<not>prime 0" by (simp add: prime_def)
+
+lemma not_prime_unit: "is_unit x \<Longrightarrow> \<not>prime x"
+ using prime_elem_not_unit[of x] by (auto simp add: prime_def)
+
+lemma not_prime_1 [simp]: "\<not>prime 1" by (simp add: not_prime_unit)
+
+lemma primeI: "prime_elem x \<Longrightarrow> normalize x = x \<Longrightarrow> prime x"
+ by (simp add: prime_def)
+
+lemma prime_imp_prime_elem [dest]: "prime p \<Longrightarrow> prime_elem p"
+ by (simp add: prime_def)
+
+lemma normalize_prime: "prime p \<Longrightarrow> normalize p = p"
+ by (simp add: prime_def)
+
+lemma prime_normalize_iff [simp]: "prime (normalize p) \<longleftrightarrow> prime_elem p"
+ by (auto simp add: prime_def)
+
+lemma prime_power_iff:
+ "prime (p ^ n) \<longleftrightarrow> prime p \<and> n = 1"
+ by (auto simp: prime_def prime_elem_power_iff)
+
+lemma prime_imp_nonzero [simp]:
+ "ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 0"
+ unfolding ASSUMPTION_def prime_def by auto
+
+lemma prime_imp_not_one [simp]:
+ "ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 1"
+ unfolding ASSUMPTION_def by auto
+
+lemma prime_not_unit' [simp]:
+ "ASSUMPTION (prime x) \<Longrightarrow> \<not>is_unit x"
+ unfolding ASSUMPTION_def prime_def by auto
+
+lemma prime_normalize' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> normalize x = x"
+ unfolding ASSUMPTION_def prime_def by simp
+
+lemma unit_factor_prime: "prime x \<Longrightarrow> unit_factor x = 1"
+ using unit_factor_normalize[of x] unfolding prime_def by auto
+
+lemma unit_factor_prime' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> unit_factor x = 1"
+ unfolding ASSUMPTION_def by (rule unit_factor_prime)
+
+lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> prime_elem x"
+ by (simp add: prime_def ASSUMPTION_def)
+
+lemma prime_dvd_multD: "prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
+ by (intro prime_elem_dvd_multD) simp_all
+
+lemma prime_dvd_mult_iff [simp]: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
+ by (auto dest: prime_dvd_multD)
+
+lemma prime_dvd_power:
+ "prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
+ by (auto dest!: prime_elem_dvd_power simp: prime_def)
+
+lemma prime_dvd_power_iff:
+ "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
+ by (subst prime_elem_dvd_power_iff) simp_all
+
+lemma msetprod_subset_imp_dvd:
+ assumes "A \<subseteq># B"
+ shows "msetprod A dvd msetprod B"
+proof -
+ from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
+ also have "msetprod \<dots> = msetprod (B - A) * msetprod A" by simp
+ also have "msetprod A dvd \<dots>" by simp
+ finally show ?thesis .
+qed
+
+lemma prime_dvd_msetprod_iff: "prime p \<Longrightarrow> p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
+ by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+)
+
+lemma primes_dvd_imp_eq:
+ assumes "prime p" "prime q" "p dvd q"
+ shows "p = q"
+proof -
+ from assms have "irreducible q" by (simp add: prime_elem_imp_irreducible prime_def)
+ from irreducibleD'[OF this \<open>p dvd q\<close>] assms have "q dvd p" by simp
+ with \<open>p dvd q\<close> have "normalize p = normalize q" by (rule associatedI)
+ with assms show "p = q" by simp
+qed
+
+lemma prime_dvd_msetprod_primes_iff:
+ assumes "prime p" "\<And>q. q \<in># A \<Longrightarrow> prime q"
+ shows "p dvd msetprod A \<longleftrightarrow> p \<in># A"
+proof -
+ from assms(1) have "p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_msetprod_iff)
+ also from assms have "\<dots> \<longleftrightarrow> p \<in># A" by (auto dest: primes_dvd_imp_eq)
+ finally show ?thesis .
+qed
+
+lemma msetprod_primes_dvd_imp_subset:
+ assumes "msetprod A dvd msetprod B" "\<And>p. p \<in># A \<Longrightarrow> prime p" "\<And>p. p \<in># B \<Longrightarrow> prime p"
+ shows "A \<subseteq># B"
+using assms
+proof (induction A arbitrary: B)
+ case empty
+ thus ?case by simp
+next
+ case (add A p B)
+ hence p: "prime p" by simp
+ define B' where "B' = B - {#p#}"
+ from add.prems have "p dvd msetprod B" by (simp add: dvd_mult_right)
+ with add.prems have "p \<in># B"
+ by (subst (asm) (2) prime_dvd_msetprod_primes_iff) simp_all
+ hence B: "B = B' + {#p#}" by (simp add: B'_def)
+ from add.prems p have "A \<subseteq># B'" by (intro add.IH) (simp_all add: B)
+ thus ?case by (simp add: B)
+qed
+
+lemma normalize_msetprod_primes:
+ "(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (msetprod A) = msetprod A"
+proof (induction A)
+ case (add A p)
+ hence "prime p" by simp
+ hence "normalize p = p" by simp
+ with add show ?case by (simp add: normalize_mult)
+qed simp_all
+
+lemma msetprod_dvd_msetprod_primes_iff:
+ assumes "\<And>x. x \<in># A \<Longrightarrow> prime x" "\<And>x. x \<in># B \<Longrightarrow> prime x"
+ shows "msetprod A dvd msetprod B \<longleftrightarrow> A \<subseteq># B"
+ using assms by (auto intro: msetprod_subset_imp_dvd msetprod_primes_dvd_imp_subset)
+
lemma is_unit_msetprod_iff:
"is_unit (msetprod A) \<longleftrightarrow> (\<forall>x. x \<in># A \<longrightarrow> is_unit x)"
by (induction A) (auto simp: is_unit_mult_iff)
@@ -516,7 +517,7 @@
by (intro multiset_eqI) (simp_all add: count_eq_zero_iff)
lemma is_unit_msetprod_primes_iff:
- assumes "\<And>x. x \<in># A \<Longrightarrow> is_prime x"
+ assumes "\<And>x. x \<in># A \<Longrightarrow> prime x"
shows "is_unit (msetprod A) \<longleftrightarrow> A = {#}"
proof
assume unit: "is_unit (msetprod A)"
@@ -524,16 +525,16 @@
proof (intro multiset_emptyI notI)
fix x assume "x \<in># A"
with unit have "is_unit x" by (subst (asm) is_unit_msetprod_iff) blast
- moreover from \<open>x \<in># A\<close> have "is_prime x" by (rule assms)
+ moreover from \<open>x \<in># A\<close> have "prime x" by (rule assms)
ultimately show False by simp
qed
qed simp_all
lemma msetprod_primes_irreducible_imp_prime:
assumes irred: "irreducible (msetprod A)"
- assumes A: "\<And>x. x \<in># A \<Longrightarrow> is_prime x"
- assumes B: "\<And>x. x \<in># B \<Longrightarrow> is_prime x"
- assumes C: "\<And>x. x \<in># C \<Longrightarrow> is_prime x"
+ assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
+ assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
+ assumes C: "\<And>x. x \<in># C \<Longrightarrow> prime x"
assumes dvd: "msetprod A dvd msetprod B * msetprod C"
shows "msetprod A dvd msetprod B \<or> msetprod A dvd msetprod C"
proof -
@@ -564,8 +565,8 @@
qed
lemma msetprod_primes_finite_divisor_powers:
- assumes A: "\<And>x. x \<in># A \<Longrightarrow> is_prime x"
- assumes B: "\<And>x. x \<in># B \<Longrightarrow> is_prime x"
+ assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
+ assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
assumes "A \<noteq> {#}"
shows "finite {n. msetprod A ^ n dvd msetprod B}"
proof -
@@ -594,10 +595,10 @@
context semiring_gcd
begin
-lemma irreducible_imp_prime_gcd:
+lemma irreducible_imp_prime_elem_gcd:
assumes "irreducible x"
- shows "is_prime_elem x"
-proof (rule is_prime_elemI)
+ shows "prime_elem x"
+proof (rule prime_elemI)
fix a b assume "x dvd a * b"
from dvd_productE[OF this] obtain y z where yz: "x = y * z" "y dvd a" "z dvd b" .
from \<open>irreducible x\<close> and \<open>x = y * z\<close> have "is_unit y \<or> is_unit z" by (rule irreducibleD)
@@ -605,77 +606,77 @@
by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff')
qed (insert assms, auto simp: irreducible_not_unit)
-lemma is_prime_elem_imp_coprime:
- assumes "is_prime_elem p" "\<not>p dvd n"
+lemma prime_elem_imp_coprime:
+ assumes "prime_elem p" "\<not>p dvd n"
shows "coprime p n"
proof (rule coprimeI)
fix d assume "d dvd p" "d dvd n"
show "is_unit d"
proof (rule ccontr)
assume "\<not>is_unit d"
- from \<open>is_prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d"
- by (rule is_prime_elemD2)
+ from \<open>prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d"
+ by (rule prime_elemD2)
from this and \<open>d dvd n\<close> have "p dvd n" by (rule dvd_trans)
with \<open>\<not>p dvd n\<close> show False by contradiction
qed
qed
-lemma is_prime_imp_coprime:
- assumes "is_prime p" "\<not>p dvd n"
+lemma prime_imp_coprime:
+ assumes "prime p" "\<not>p dvd n"
shows "coprime p n"
- using assms by (simp add: is_prime_elem_imp_coprime)
+ using assms by (simp add: prime_elem_imp_coprime)
-lemma is_prime_elem_imp_power_coprime:
- "is_prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
- by (auto intro!: coprime_exp dest: is_prime_elem_imp_coprime simp: gcd.commute)
+lemma prime_elem_imp_power_coprime:
+ "prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
+ by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute)
-lemma is_prime_imp_power_coprime:
- "is_prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
- by (simp add: is_prime_elem_imp_power_coprime)
+lemma prime_imp_power_coprime:
+ "prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
+ by (simp add: prime_elem_imp_power_coprime)
-lemma prime_divprod_pow:
- assumes p: "is_prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
+lemma prime_elem_divprod_pow:
+ assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
shows "p^n dvd a \<or> p^n dvd b"
using assms
proof -
from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
- by (auto simp: coprime is_prime_elem_def)
+ by (auto simp: coprime prime_elem_def)
with p have "coprime (p^n) a \<or> coprime (p^n) b"
- by (auto intro: is_prime_elem_imp_coprime coprime_exp_left)
+ by (auto intro: prime_elem_imp_coprime coprime_exp_left)
with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
qed
lemma primes_coprime:
- "is_prime p \<Longrightarrow> is_prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
- using is_prime_imp_coprime primes_dvd_imp_eq by blast
+ "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
+ using prime_imp_coprime primes_dvd_imp_eq by blast
end
class factorial_semiring = normalization_semidom +
assumes prime_factorization_exists:
- "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize x"
+ "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize x"
begin
lemma prime_factorization_exists':
assumes "x \<noteq> 0"
- obtains A where "\<And>x. x \<in># A \<Longrightarrow> is_prime x" "msetprod A = normalize x"
+ obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "msetprod A = normalize x"
proof -
from prime_factorization_exists[OF assms] obtain A
- where A: "\<And>x. x \<in># A \<Longrightarrow> is_prime_elem x" "msetprod A = normalize x" by blast
+ where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "msetprod A = normalize x" by blast
define A' where "A' = image_mset normalize A"
have "msetprod A' = normalize (msetprod A)"
by (simp add: A'_def normalize_msetprod)
also note A(2)
finally have "msetprod A' = normalize x" by simp
- moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> is_prime x" by (auto simp: is_prime_def A'_def)
+ moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> prime x" by (auto simp: prime_def A'_def)
ultimately show ?thesis by (intro that[of A']) blast
qed
-lemma irreducible_imp_prime:
+lemma irreducible_imp_prime_elem:
assumes "irreducible x"
- shows "is_prime_elem x"
-proof (rule is_prime_elemI)
+ shows "prime_elem x"
+proof (rule prime_elemI)
fix a b assume dvd: "x dvd a * b"
from assms have "x \<noteq> 0" by auto
show "x dvd a \<or> x dvd b"
@@ -708,12 +709,12 @@
lemma finite_prime_divisors:
assumes "x \<noteq> 0"
- shows "finite {p. is_prime p \<and> p dvd x}"
+ shows "finite {p. prime p \<and> p dvd x}"
proof -
from prime_factorization_exists'[OF assms] guess A . note A = this
- have "{p. is_prime p \<and> p dvd x} \<subseteq> set_mset A"
+ have "{p. prime p \<and> p dvd x} \<subseteq> set_mset A"
proof safe
- fix p assume p: "is_prime p" and dvd: "p dvd x"
+ fix p assume p: "prime p" and dvd: "p dvd x"
from dvd have "p dvd normalize x" by simp
also from A have "normalize x = msetprod A" by simp
finally show "p \<in># A" using p A by (subst (asm) prime_dvd_msetprod_primes_iff)
@@ -722,23 +723,23 @@
ultimately show ?thesis by (rule finite_subset)
qed
-lemma prime_iff_irreducible: "is_prime_elem x \<longleftrightarrow> irreducible x"
- by (blast intro: irreducible_imp_prime prime_imp_irreducible)
+lemma prime_elem_iff_irreducible: "prime_elem x \<longleftrightarrow> irreducible x"
+ by (blast intro: irreducible_imp_prime_elem prime_elem_imp_irreducible)
lemma prime_divisor_exists:
assumes "a \<noteq> 0" "\<not>is_unit a"
- shows "\<exists>b. b dvd a \<and> is_prime b"
+ shows "\<exists>b. b dvd a \<and> prime b"
proof -
from prime_factorization_exists'[OF assms(1)] guess A . note A = this
moreover from A and assms have "A \<noteq> {#}" by auto
then obtain x where "x \<in># A" by blast
- with A(1) have *: "x dvd msetprod A" "is_prime x" by (auto simp: dvd_msetprod)
+ with A(1) have *: "x dvd msetprod A" "prime x" by (auto simp: dvd_msetprod)
with A have "x dvd a" by simp
with * show ?thesis by blast
qed
lemma prime_divisors_induct [case_names zero unit factor]:
- assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. is_prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)"
+ assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)"
shows "P x"
proof (cases "x = 0")
case False
@@ -746,7 +747,7 @@
from A(1) have "P (unit_factor x * msetprod A)"
proof (induction A)
case (add A p)
- from add.prems have "is_prime p" by simp
+ from add.prems have "prime p" by simp
moreover from add.prems have "P (unit_factor x * msetprod A)" by (intro add.IH) simp_all
ultimately have "P (p * (unit_factor x * msetprod A))" by (rule assms(3))
thus ?case by (simp add: mult_ac)
@@ -755,18 +756,18 @@
qed (simp_all add: assms(1))
lemma no_prime_divisors_imp_unit:
- assumes "a \<noteq> 0" "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> is_prime_elem b"
+ assumes "a \<noteq> 0" "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> prime_elem b"
shows "is_unit a"
proof (rule ccontr)
assume "\<not>is_unit a"
from prime_divisor_exists[OF assms(1) this] guess b by (elim exE conjE)
- with assms(2)[of b] show False by (simp add: is_prime_def)
+ with assms(2)[of b] show False by (simp add: prime_def)
qed
lemma prime_divisorE:
assumes "a \<noteq> 0" and "\<not> is_unit a"
- obtains p where "is_prime p" and "p dvd a"
- using assms no_prime_divisors_imp_unit unfolding is_prime_def by blast
+ obtains p where "prime p" and "p dvd a"
+ using assms no_prime_divisors_imp_unit unfolding prime_def by blast
definition multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
"multiplicity p x = (if finite {n. p ^ n dvd x} then Max {n. p ^ n dvd x} else 0)"
@@ -864,17 +865,17 @@
lemma multiplicity_zero [simp]: "multiplicity p 0 = 0"
by (simp add: multiplicity_def)
-lemma prime_multiplicity_eq_zero_iff:
- "is_prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
+lemma prime_elem_multiplicity_eq_zero_iff:
+ "prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
by (rule multiplicity_eq_zero_iff) simp_all
lemma prime_multiplicity_other:
- assumes "is_prime p" "is_prime q" "p \<noteq> q"
+ assumes "prime p" "prime q" "p \<noteq> q"
shows "multiplicity p q = 0"
- using assms by (subst prime_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)
+ using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)
lemma prime_multiplicity_gt_zero_iff:
- "is_prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
+ "prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
by (rule multiplicity_gt_zero_iff) simp_all
lemma multiplicity_unit_left: "is_unit p \<Longrightarrow> multiplicity p x = 0"
@@ -943,8 +944,8 @@
"p \<noteq> 0 \<Longrightarrow> \<not>is_unit p \<Longrightarrow> multiplicity p (p ^ n) = n"
by (simp add: multiplicity_same_power')
-lemma multiplicity_prime_times_other:
- assumes "is_prime_elem p" "\<not>p dvd q"
+lemma multiplicity_prime_elem_times_other:
+ assumes "prime_elem p" "\<not>p dvd q"
shows "multiplicity p (q * x) = multiplicity p x"
proof (cases "x = 0")
case False
@@ -959,38 +960,38 @@
from multiplicity_decompose'[OF False this] guess y . note y = this [folded n_def]
from y have "p ^ Suc n dvd q * x \<longleftrightarrow> p ^ n * p dvd p ^ n * (q * y)" by (simp add: mult_ac)
also from assms have "\<dots> \<longleftrightarrow> p dvd q * y" by simp
- also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_dvd_mult_iff) fact+
+ also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_elem_dvd_mult_iff) fact+
also from assms y have "\<dots> \<longleftrightarrow> False" by simp
finally show "\<not>(p ^ Suc n dvd q * x)" by blast
qed
qed simp_all
lift_definition prime_factorization :: "'a \<Rightarrow> 'a multiset" is
- "\<lambda>x p. if is_prime p then multiplicity p x else 0"
+ "\<lambda>x p. if prime p then multiplicity p x else 0"
unfolding multiset_def
proof clarify
fix x :: 'a
- show "finite {p. 0 < (if is_prime p then multiplicity p x else 0)}" (is "finite ?A")
+ show "finite {p. 0 < (if prime p then multiplicity p x else 0)}" (is "finite ?A")
proof (cases "x = 0")
case False
- from False have "?A \<subseteq> {p. is_prime p \<and> p dvd x}"
+ from False have "?A \<subseteq> {p. prime p \<and> p dvd x}"
by (auto simp: multiplicity_gt_zero_iff)
- moreover from False have "finite {p. is_prime p \<and> p dvd x}"
+ moreover from False have "finite {p. prime p \<and> p dvd x}"
by (rule finite_prime_divisors)
ultimately show ?thesis by (rule finite_subset)
qed simp_all
qed
lemma count_prime_factorization_nonprime:
- "\<not>is_prime p \<Longrightarrow> count (prime_factorization x) p = 0"
+ "\<not>prime p \<Longrightarrow> count (prime_factorization x) p = 0"
by transfer simp
lemma count_prime_factorization_prime:
- "is_prime p \<Longrightarrow> count (prime_factorization x) p = multiplicity p x"
+ "prime p \<Longrightarrow> count (prime_factorization x) p = multiplicity p x"
by transfer simp
lemma count_prime_factorization:
- "count (prime_factorization x) p = (if is_prime p then multiplicity p x else 0)"
+ "count (prime_factorization x) p = (if prime p then multiplicity p x else 0)"
by transfer simp
lemma unit_imp_no_irreducible_divisors:
@@ -999,9 +1000,9 @@
using assms dvd_unit_imp_unit irreducible_not_unit by blast
lemma unit_imp_no_prime_divisors:
- assumes "is_unit x" "is_prime_elem p"
+ assumes "is_unit x" "prime_elem p"
shows "\<not>p dvd x"
- using unit_imp_no_irreducible_divisors[OF assms(1) prime_imp_irreducible[OF assms(2)]] .
+ using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] .
lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}"
by (simp add: multiset_eq_iff count_prime_factorization)
@@ -1013,7 +1014,7 @@
{
assume x: "x \<noteq> 0" "\<not>is_unit x"
{
- fix p assume p: "is_prime p"
+ fix p assume p: "prime p"
have "count (prime_factorization x) p = 0" by (simp add: *)
also from p have "count (prime_factorization x) p = multiplicity p x"
by (rule count_prime_factorization_prime)
@@ -1029,7 +1030,7 @@
proof
assume x: "is_unit x"
{
- fix p assume p: "is_prime p"
+ fix p assume p: "prime p"
from p x have "multiplicity p x = 0"
by (subst multiplicity_eq_zero_iff)
(auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors)
@@ -1044,7 +1045,7 @@
proof (rule multiset_eqI)
fix p :: 'a
show "count (prime_factorization x) p = count {#} p"
- proof (cases "is_prime p")
+ proof (cases "prime p")
case True
with assms have "multiplicity p x = 0"
by (subst multiplicity_eq_zero_iff)
@@ -1057,17 +1058,17 @@
by (simp add: prime_factorization_unit)
lemma prime_factorization_times_prime:
- assumes "x \<noteq> 0" "is_prime p"
+ assumes "x \<noteq> 0" "prime p"
shows "prime_factorization (p * x) = {#p#} + prime_factorization x"
proof (rule multiset_eqI)
fix q :: 'a
- consider "\<not>is_prime q" | "p = q" | "is_prime q" "p \<noteq> q" by blast
+ consider "\<not>prime q" | "p = q" | "prime q" "p \<noteq> q" by blast
thus "count (prime_factorization (p * x)) q = count ({#p#} + prime_factorization x) q"
proof cases
- assume q: "is_prime q" "p \<noteq> q"
+ assume q: "prime q" "p \<noteq> q"
with assms primes_dvd_imp_eq[of q p] have "\<not>q dvd p" by auto
with q assms show ?thesis
- by (simp add: multiplicity_prime_times_other count_prime_factorization)
+ by (simp add: multiplicity_prime_elem_times_other count_prime_factorization)
qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same)
qed
@@ -1080,17 +1081,17 @@
is_unit_normalize normalize_mult)
lemma in_prime_factorization_iff:
- "p \<in># prime_factorization x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> is_prime p"
+ "p \<in># prime_factorization x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
proof -
have "p \<in># prime_factorization x \<longleftrightarrow> count (prime_factorization x) p > 0" by simp
- also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> is_prime p"
+ also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
by (subst count_prime_factorization, cases "x = 0")
(auto simp: multiplicity_eq_zero_iff multiplicity_gt_zero_iff)
finally show ?thesis .
qed
lemma in_prime_factorization_imp_prime:
- "p \<in># prime_factorization x \<Longrightarrow> is_prime p"
+ "p \<in># prime_factorization x \<Longrightarrow> prime p"
by (simp add: in_prime_factorization_iff)
lemma in_prime_factorization_imp_dvd:
@@ -1111,18 +1112,18 @@
qed
lemma prime_factorization_prime:
- assumes "is_prime p"
+ assumes "prime p"
shows "prime_factorization p = {#p#}"
proof (rule multiset_eqI)
fix q :: 'a
- consider "\<not>is_prime q" | "q = p" | "is_prime q" "q \<noteq> p" by blast
+ consider "\<not>prime q" | "q = p" | "prime q" "q \<noteq> p" by blast
thus "count (prime_factorization p) q = count {#p#} q"
by cases (insert assms, auto dest: primes_dvd_imp_eq
simp: count_prime_factorization multiplicity_self multiplicity_eq_zero_iff)
qed
lemma prime_factorization_msetprod_primes:
- assumes "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
+ assumes "\<And>p. p \<in># A \<Longrightarrow> prime p"
shows "prime_factorization (msetprod A) = A"
using assms
proof (induction A)
@@ -1204,7 +1205,7 @@
qed
lemma prime_factorization_prime_power:
- "is_prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p"
+ "prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p"
by (induction n)
(simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute)
@@ -1242,8 +1243,8 @@
by (auto dest: in_prime_factorization_imp_prime)
-lemma prime_multiplicity_mult_distrib:
- assumes "is_prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
+lemma prime_elem_multiplicity_mult_distrib:
+ assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
shows "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
proof -
have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
@@ -1259,23 +1260,23 @@
finally show ?thesis .
qed
-lemma prime_multiplicity_power_distrib:
- assumes "is_prime_elem p" "x \<noteq> 0"
+lemma prime_elem_multiplicity_power_distrib:
+ assumes "prime_elem p" "x \<noteq> 0"
shows "multiplicity p (x ^ n) = n * multiplicity p x"
- by (induction n) (simp_all add: assms prime_multiplicity_mult_distrib)
+ by (induction n) (simp_all add: assms prime_elem_multiplicity_mult_distrib)
-lemma prime_multiplicity_msetprod_distrib:
- assumes "is_prime_elem p" "0 \<notin># A"
+lemma prime_elem_multiplicity_msetprod_distrib:
+ assumes "prime_elem p" "0 \<notin># A"
shows "multiplicity p (msetprod A) = msetsum (image_mset (multiplicity p) A)"
- using assms by (induction A) (auto simp: prime_multiplicity_mult_distrib)
+ using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib)
-lemma prime_multiplicity_setprod_distrib:
- assumes "is_prime_elem p" "0 \<notin> f ` A" "finite A"
+lemma prime_elem_multiplicity_setprod_distrib:
+ assumes "prime_elem p" "0 \<notin> f ` A" "finite A"
shows "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
proof -
have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
using assms by (subst setprod_unfold_msetprod)
- (simp_all add: prime_multiplicity_msetprod_distrib setsum_unfold_msetsum
+ (simp_all add: prime_elem_multiplicity_msetprod_distrib setsum_unfold_msetsum
multiset.map_comp o_def)
also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
by (induction A rule: finite_induct) simp_all
@@ -1292,10 +1293,10 @@
by (simp add: prime_factors_def)
lemma prime_factorsI:
- "x \<noteq> 0 \<Longrightarrow> is_prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
+ "x \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
by (auto simp: prime_factors_def in_prime_factorization_iff)
-lemma prime_factors_prime [intro]: "p \<in> prime_factors x \<Longrightarrow> is_prime p"
+lemma prime_factors_prime [intro]: "p \<in> prime_factors x \<Longrightarrow> prime p"
by (auto simp: prime_factors_def dest: in_prime_factorization_imp_prime)
lemma prime_factors_dvd [dest]: "p \<in> prime_factors x \<Longrightarrow> p dvd x"
@@ -1306,7 +1307,7 @@
unfolding prime_factors_def by simp
lemma prime_factors_altdef_multiplicity:
- "prime_factors n = {p. is_prime p \<and> multiplicity p n > 0}"
+ "prime_factors n = {p. prime p \<and> multiplicity p n > 0}"
by (cases "n = 0")
(auto simp: prime_factors_def prime_multiplicity_gt_zero_iff
prime_imp_prime_elem in_prime_factorization_iff)
@@ -1335,8 +1336,8 @@
lemma prime_factorization_unique'':
assumes S_eq: "S = {p. 0 < f p}"
and "finite S"
- and S: "\<forall>p\<in>S. is_prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
- shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
+ and S: "\<forall>p\<in>S. prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
+ shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
proof
define A where "A = Abs_multiset f"
from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
@@ -1357,15 +1358,15 @@
by (intro prime_factorization_msetprod_primes) (auto dest: in_prime_factorization_imp_prime)
finally show "S = prime_factors n" by (simp add: prime_factors_def set_mset_A [symmetric])
- show "(\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
+ show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
proof safe
- fix p :: 'a assume p: "is_prime p"
+ fix p :: 'a assume p: "prime p"
have "multiplicity p n = multiplicity p (normalize n)" by simp
also have "normalize n = msetprod A"
by (simp add: msetprod_multiplicity S_eq set_mset_A count_A S)
also from p set_mset_A S(1)
have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
- by (intro prime_multiplicity_msetprod_distrib) auto
+ by (intro prime_elem_multiplicity_msetprod_distrib) auto
also from S(1) p
have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
@@ -1374,10 +1375,10 @@
qed
qed
-lemma multiplicity_prime [simp]: "is_prime_elem p \<Longrightarrow> multiplicity p p = 1"
+lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1"
by (rule multiplicity_self) auto
-lemma multiplicity_prime_power [simp]: "is_prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
+lemma multiplicity_prime_power [simp]: "prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
by (subst multiplicity_same_power') auto
lemma prime_factors_product:
@@ -1385,8 +1386,8 @@
by (simp add: prime_factors_def prime_factorization_mult)
lemma multiplicity_distinct_prime_power:
- "is_prime p \<Longrightarrow> is_prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
- by (subst prime_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
+ "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
+ by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
lemma dvd_imp_multiplicity_le:
assumes "a dvd b" "b \<noteq> 0"
@@ -1404,7 +1405,7 @@
(* RENAMED multiplicity_dvd *)
lemma multiplicity_le_imp_dvd:
- assumes "x \<noteq> 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
+ assumes "x \<noteq> 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
shows "x dvd y"
proof (cases "y = 0")
case False
@@ -1417,17 +1418,17 @@
"x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd)
-lemma prime_factors_altdef: "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. is_prime p \<and> p dvd x}"
+lemma prime_factors_altdef: "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. prime p \<and> p dvd x}"
by (auto intro: prime_factorsI)
lemma multiplicity_eq_imp_eq:
assumes "x \<noteq> 0" "y \<noteq> 0"
- assumes "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+ assumes "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
shows "normalize x = normalize y"
using assms by (intro associatedI multiplicity_le_imp_dvd) simp_all
lemma prime_factorization_unique':
- assumes "\<forall>p \<in># M. is_prime p" "\<forall>p \<in># N. is_prime p" "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
+ assumes "\<forall>p \<in># M. prime p" "\<forall>p \<in># N. prime p" "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
shows "M = N"
proof -
have "prime_factorization (\<Prod>i \<in># M. i) = prime_factorization (\<Prod>i \<in># N. i)"
@@ -1504,7 +1505,7 @@
hence "\<forall>y. y \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> y \<in># prime_factorization x"
by (auto dest: mset_subset_eqD)
with in_prime_factorization_imp_prime[of _ x]
- have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> is_prime p" by blast
+ have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> prime p" by blast
with assms show ?thesis
by (simp add: Gcd_factorial_def prime_factorization_msetprod_primes)
qed
@@ -1519,7 +1520,7 @@
finally show ?thesis by (simp add: Lcm_factorial_def)
next
case False
- have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> is_prime y"
+ have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> prime y"
by (auto simp: in_Sup_multiset_iff assms in_prime_factorization_imp_prime)
with assms False show ?thesis
by (simp add: Lcm_factorial_def prime_factorization_msetprod_primes)
@@ -1586,7 +1587,7 @@
then obtain x where "x \<in> A" "x \<noteq> 0" by blast
hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
by (intro subset_mset.cInf_lower) auto
- hence "is_prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
+ hence "prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
using that by (auto dest: mset_subset_eqD intro: in_prime_factorization_imp_prime)
with False show ?thesis
by (auto simp add: Gcd_factorial_def normalize_msetprod_primes)
@@ -1692,9 +1693,9 @@
lemma (in normalization_semidom) factorial_semiring_altI_aux:
assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
- assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> is_prime_elem x"
+ assumes irreducible_imp_prime_elem: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
assumes "(x::'a) \<noteq> 0"
- shows "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize x"
+ shows "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize x"
using \<open>x \<noteq> 0\<close>
proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct)
case (less a)
@@ -1709,7 +1710,7 @@
proof (cases "\<exists>b. b dvd a \<and> \<not>is_unit b \<and> \<not>a dvd b")
case False
with \<open>\<not>is_unit a\<close> less.prems have "irreducible a" by (auto simp: irreducible_altdef)
- hence "is_prime_elem a" by (rule irreducible_imp_prime)
+ hence "prime_elem a" by (rule irreducible_imp_prime_elem)
thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
next
case True
@@ -1722,7 +1723,7 @@
with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)"
by (rule psubset_card_mono)
moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
- ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize b"
+ ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize b"
by (intro less) auto
then guess A .. note A = this
@@ -1741,7 +1742,7 @@
ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)"
by (rule psubset_card_mono)
- with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize c"
+ with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize c"
by (intro less) auto
then guess B .. note B = this
@@ -1752,7 +1753,7 @@
lemma factorial_semiring_altI:
assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
- assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> is_prime_elem x"
+ assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
shows "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
by intro_classes (rule factorial_semiring_altI_aux[OF assms])
@@ -1816,7 +1817,7 @@
qed
lemma
- assumes "x \<noteq> 0" "y \<noteq> 0" "is_prime p"
+ assumes "x \<noteq> 0" "y \<noteq> 0" "prime p"
shows multiplicity_gcd: "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
and multiplicity_lcm: "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
proof -
--- a/src/HOL/Number_Theory/Gauss.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy Tue Aug 09 19:45:01 2016 +0200
@@ -112,7 +112,7 @@
from p_a_relprime have "\<not>p dvd a"
by (simp add: cong_altdef_int)
with p_prime have "coprime a (int p)"
- by (subst gcd.commute, intro is_prime_imp_coprime) auto
+ by (subst gcd.commute, intro prime_imp_coprime) auto
with a cong_mult_rcancel_int [of a "int p" x y]
have "[x = y] (mod p)" by simp
with cong_less_imp_eq_int [of x y p] p_minus_one_l
@@ -144,7 +144,7 @@
from p_a_relprime have "\<not>p dvd a"
by (simp add: cong_altdef_int)
with p_prime have "coprime a (int p)"
- by (subst gcd.commute, intro is_prime_imp_coprime) auto
+ by (subst gcd.commute, intro prime_imp_coprime) auto
with a' cong_mult_rcancel_int [of a "int p" x y]
have "[x = y] (mod p)" by simp
with cong_less_imp_eq_int [of x y p] p_minus_one_l
@@ -207,7 +207,7 @@
lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
using p_prime A_ncong_p [OF assms]
- by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: is_prime_imp_coprime)
+ by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: prime_imp_coprime)
lemma A_prod_relprime: "gcd (setprod id A) p = 1"
by (metis id_def all_A_relprime setprod_coprime)
--- a/src/HOL/Number_Theory/Pocklington.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy Tue Aug 09 19:45:01 2016 +0200
@@ -12,7 +12,7 @@
lemma prime:
"prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
- unfolding is_prime_nat_iff
+ unfolding prime_nat_iff
proof safe
fix m assume p: "p > 0" "p \<noteq> 1" and m: "m dvd p" "m \<noteq> p"
and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
@@ -20,8 +20,8 @@
moreover from p m have "m < p" by (auto dest: dvd_imp_le)
ultimately have "coprime p m" using * by blast
with m show "m = 1" by simp
-qed (auto simp: is_prime_nat_iff simp del: One_nat_def
- intro!: is_prime_imp_coprime dest: dvd_imp_le)
+qed (auto simp: prime_nat_iff simp del: One_nat_def
+ intro!: prime_imp_coprime dest: dvd_imp_le)
lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
proof-
@@ -85,7 +85,7 @@
with y(2) have th: "p dvd a"
by (auto dest: cong_dvd_eq_nat)
have False
- by (metis gcd_nat.absorb1 not_is_prime_1 p pa th)}
+ by (metis gcd_nat.absorb1 not_prime_1 p pa th)}
with y show ?thesis unfolding Ex1_def using neq0_conv by blast
qed
@@ -428,18 +428,18 @@
proof (cases "n=0 \<or> n=1")
case True
then show ?thesis
- by (metis bigger_prime dvd_0_right not_is_prime_1 not_is_prime_0)
+ by (metis bigger_prime dvd_0_right not_prime_1 not_prime_0)
next
case False
show ?thesis
proof
assume "prime n"
then show ?rhs
- by (metis not_is_prime_1 is_prime_nat_iff)
+ by (metis not_prime_1 prime_nat_iff)
next
assume ?rhs
with False show "prime n"
- by (auto simp: is_prime_nat_iff) (metis One_nat_def prime_factor_nat is_prime_nat_iff)
+ by (auto simp: prime_nat_iff) (metis One_nat_def prime_factor_nat prime_nat_iff)
qed
qed
@@ -475,7 +475,7 @@
with H[rule_format, of e] h have "e=1" by simp
with e have "d = n" by simp}
ultimately have "d=1 \<or> d=n" by blast}
- ultimately have ?thesis unfolding is_prime_nat_iff using np n(2) by blast}
+ ultimately have ?thesis unfolding prime_nat_iff using np n(2) by blast}
ultimately show ?thesis by auto
qed
@@ -485,7 +485,7 @@
proof-
{assume "n=0 \<or> n=1"
hence ?thesis
- by (metis not_is_prime_0 not_is_prime_1)}
+ by (metis not_prime_0 not_prime_1)}
moreover
{assume n: "n\<noteq>0" "n\<noteq>1"
{assume H: ?lhs
@@ -539,7 +539,7 @@
from aq P(1) Pq have caP:"coprime (a^ ((n - 1) div P) - 1) n" by blast
from Pq obtain s where s: "q = P*s" unfolding dvd_def by blast
have P0: "P \<noteq> 0" using P(1)
- by (metis not_is_prime_0)
+ by (metis not_prime_0)
from P(2) obtain t where t: "d = P*t" unfolding dvd_def by blast
from d s t P0 have s': "ord p (a^r) * t = s"
by (metis mult.commute mult_cancel1 mult.assoc)
@@ -559,7 +559,7 @@
hence o: "ord p (a^r) = q" using d by simp
from pp phi_prime[of p] have phip: "phi p = p - 1" by simp
{fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
- from pp[unfolded is_prime_nat_iff] d have dp: "d = p" by blast
+ from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast
from n have "n \<noteq> 0" by simp
then have False using d dp pn
by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)}
@@ -675,7 +675,7 @@
from Cons.prems[unfolded primefact_def]
have q: "prime q" "q * foldr op * qs 1 = n" "\<forall>p \<in>set qs. prime p" and p: "prime p" "p dvd q * foldr op * qs 1" by simp_all
{assume "p dvd q"
- with p(1) q(1) have "p = q" unfolding is_prime_nat_iff by auto
+ with p(1) q(1) have "p = q" unfolding prime_nat_iff by auto
hence ?case by simp}
moreover
{ assume h: "p dvd foldr op * qs 1"
@@ -730,7 +730,7 @@
from psp primefact_contains[OF pfpsq p]
have p': "coprime (a ^ (r * (q div p)) mod n - 1) n"
by (simp add: list_all_iff)
- from p is_prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)"
+ from p prime_nat_iff have p01: "p \<noteq> 0" "p \<noteq> 1" "p =Suc(p - 1)"
by auto
from div_mult1_eq[of r q p] p(2)
have eq1: "r* (q div p) = (n - 1) div p"
--- a/src/HOL/Number_Theory/Polynomial_Factorial.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Number_Theory/Polynomial_Factorial.thy Tue Aug 09 19:45:01 2016 +0200
@@ -812,9 +812,9 @@
subsection \<open>More properties of content and primitive part\<close>
lemma lift_prime_elem_poly:
- assumes "is_prime_elem (c :: 'a :: semidom)"
- shows "is_prime_elem [:c:]"
-proof (rule is_prime_elemI)
+ assumes "prime_elem (c :: 'a :: semidom)"
+ shows "prime_elem [:c:]"
+proof (rule prime_elemI)
fix a b assume *: "[:c:] dvd a * b"
from * have dvd: "c dvd coeff (a * b) n" for n
by (subst (asm) const_poly_dvd_iff) blast
@@ -862,25 +862,25 @@
ultimately have "c dvd coeff a i * coeff b m"
by (simp add: dvd_add_left_iff)
with assms coeff_m show "c dvd coeff a i"
- by (simp add: prime_dvd_mult_iff)
+ by (simp add: prime_elem_dvd_mult_iff)
qed
hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
}
thus "[:c:] dvd a \<or> [:c:] dvd b" by blast
-qed (insert assms, simp_all add: is_prime_elem_def one_poly_def)
+qed (insert assms, simp_all add: prime_elem_def one_poly_def)
lemma prime_elem_const_poly_iff:
fixes c :: "'a :: semidom"
- shows "is_prime_elem [:c:] \<longleftrightarrow> is_prime_elem c"
+ shows "prime_elem [:c:] \<longleftrightarrow> prime_elem c"
proof
- assume A: "is_prime_elem [:c:]"
- show "is_prime_elem c"
- proof (rule is_prime_elemI)
+ assume A: "prime_elem [:c:]"
+ show "prime_elem c"
+ proof (rule prime_elemI)
fix a b assume "c dvd a * b"
hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac)
- from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_divides_productD)
+ from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_elem_dvd_multD)
thus "c dvd a \<or> c dvd b" by simp
- qed (insert A, auto simp: is_prime_elem_def is_unit_poly_iff)
+ qed (insert A, auto simp: prime_elem_def is_unit_poly_iff)
qed (auto intro: lift_prime_elem_poly)
context
@@ -897,16 +897,16 @@
hence "f * g \<noteq> 0" by auto
{
assume "\<not>is_unit (content (f * g))"
- with False have "\<exists>p. p dvd content (f * g) \<and> is_prime p"
+ with False have "\<exists>p. p dvd content (f * g) \<and> prime p"
by (intro prime_divisor_exists) simp_all
- then obtain p where "p dvd content (f * g)" "is_prime p" by blast
+ then obtain p where "p dvd content (f * g)" "prime p" by blast
from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g"
by (simp add: const_poly_dvd_iff_dvd_content)
- moreover from \<open>is_prime p\<close> have "is_prime_elem [:p:]" by (simp add: lift_prime_elem_poly)
+ moreover from \<open>prime p\<close> have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly)
ultimately have "[:p:] dvd f \<or> [:p:] dvd g"
- by (simp add: prime_dvd_mult_iff)
+ by (simp add: prime_elem_dvd_mult_iff)
with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content)
- with \<open>is_prime p\<close> have False by simp
+ with \<open>prime p\<close> have False by simp
}
hence "is_unit (content (f * g))" by blast
hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content)
@@ -1033,12 +1033,12 @@
private lemma field_poly_irreducible_imp_prime:
assumes "irreducible (p :: 'a :: field poly)"
- shows "is_prime_elem p"
+ shows "prime_elem p"
proof -
have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
- from field_poly.irreducible_imp_prime[of p] assms
- show ?thesis unfolding irreducible_def is_prime_elem_def dvd_field_poly
- comm_semiring_1.irreducible_def[OF A] comm_semiring_1.is_prime_elem_def[OF A] by blast
+ from field_poly.irreducible_imp_prime_elem[of p] assms
+ show ?thesis unfolding irreducible_def prime_elem_def dvd_field_poly
+ comm_semiring_1.irreducible_def[OF A] comm_semiring_1.prime_elem_def[OF A] by blast
qed
private lemma field_poly_msetprod_prime_factorization:
@@ -1053,14 +1053,14 @@
private lemma field_poly_in_prime_factorization_imp_prime:
assumes "(p :: 'a :: field poly) \<in># field_poly.prime_factorization x"
- shows "is_prime_elem p"
+ shows "prime_elem p"
proof -
have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1
normalize_field_poly unit_factor_field_poly" ..
from field_poly.in_prime_factorization_imp_prime[of p x] assms
- show ?thesis unfolding is_prime_elem_def dvd_field_poly
- comm_semiring_1.is_prime_elem_def[OF A] normalization_semidom.is_prime_def[OF B] by blast
+ show ?thesis unfolding prime_elem_def dvd_field_poly
+ comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast
qed
@@ -1144,24 +1144,24 @@
private lemma irreducible_imp_prime_poly:
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
assumes "irreducible p"
- shows "is_prime_elem p"
+ shows "prime_elem p"
proof (cases "degree p = 0")
case True
with assms show ?thesis
by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff
- intro!: irreducible_imp_prime elim!: degree_eq_zeroE)
+ intro!: irreducible_imp_prime_elem elim!: degree_eq_zeroE)
next
case False
from assms False have irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
by (simp_all add: nonconst_poly_irreducible_iff)
- from irred have prime: "is_prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime)
+ from irred have prime: "prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime)
show ?thesis
- proof (rule is_prime_elemI)
+ proof (rule prime_elemI)
fix q r assume "p dvd q * r"
hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd)
hence "fract_poly p dvd fract_poly q * fract_poly r" by simp
from prime and this have "fract_poly p dvd fract_poly q \<or> fract_poly p dvd fract_poly r"
- by (rule prime_divides_productD)
+ by (rule prime_elem_dvd_multD)
with primitive show "p dvd q \<or> p dvd r" by (auto dest: fract_poly_dvdD)
qed (insert assms, auto simp: irreducible_def)
qed
@@ -1196,9 +1196,9 @@
by (simp add: nonconst_poly_irreducible_iff)
qed
-lemma is_prime_elem_primitive_part_fract:
+lemma prime_elem_primitive_part_fract:
fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
- shows "irreducible p \<Longrightarrow> is_prime_elem (primitive_part_fract p)"
+ shows "irreducible p \<Longrightarrow> prime_elem (primitive_part_fract p)"
by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract)
lemma irreducible_linear_field_poly:
@@ -1214,8 +1214,8 @@
by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE)
qed (insert assms, auto simp: is_unit_poly_iff)
-lemma is_prime_elem_linear_field_poly:
- "(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> is_prime_elem [:a,b:]"
+lemma prime_elem_linear_field_poly:
+ "(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> prime_elem [:a,b:]"
by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly)
lemma irreducible_linear_poly:
@@ -1224,9 +1224,9 @@
by (auto intro!: irreducible_linear_field_poly
simp: nonconst_poly_irreducible_iff content_def map_poly_pCons)
-lemma is_prime_elem_linear_poly:
+lemma prime_elem_linear_poly:
fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
- shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> is_prime_elem [:a,b:]"
+ shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]"
by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
@@ -1235,7 +1235,7 @@
private lemma poly_prime_factorization_exists_content_1:
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
assumes "p \<noteq> 0" "content p = 1"
- shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize p"
+ shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize p"
proof -
let ?P = "field_poly.prime_factorization (fract_poly p)"
define c where "c = msetprod (image_mset fract_content ?P)"
@@ -1282,8 +1282,8 @@
by (simp add: multiset.map_comp e_def A_def normalize_msetprod)
finally have "msetprod A = normalize p" ..
- have "is_prime_elem p" if "p \<in># A" for p
- using that by (auto simp: A_def is_prime_elem_primitive_part_fract prime_imp_irreducible
+ have "prime_elem p" if "p \<in># A" for p
+ using that by (auto simp: A_def prime_elem_primitive_part_fract prime_elem_imp_irreducible
dest!: field_poly_in_prime_factorization_imp_prime )
from this and \<open>msetprod A = normalize p\<close> show ?thesis
by (intro exI[of _ A]) blast
@@ -1292,15 +1292,15 @@
lemma poly_prime_factorization_exists:
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
assumes "p \<noteq> 0"
- shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize p"
+ shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize p"
proof -
define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
- have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize (primitive_part p)"
+ have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize (primitive_part p)"
by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
then guess A by (elim exE conjE) note A = this
moreover from assms have "msetprod B = [:content p:]"
by (simp add: B_def msetprod_const_poly msetprod_prime_factorization)
- moreover have "\<forall>p. p \<in># B \<longrightarrow> is_prime_elem p"
+ moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p"
by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime)
ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
qed
--- a/src/HOL/Number_Theory/Primes.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Number_Theory/Primes.thy Tue Aug 09 19:45:01 2016 +0200
@@ -55,57 +55,55 @@
declare [[coercion int]]
declare [[coercion_enabled]]
-abbreviation (input) "prime \<equiv> is_prime"
-
-lemma is_prime_elem_nat_iff:
- "is_prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
+lemma prime_elem_nat_iff:
+ "prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
proof safe
- assume *: "is_prime_elem n"
+ assume *: "prime_elem n"
from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
thus "n > 1" by (cases n) simp_all
fix m assume m: "m dvd n" "m \<noteq> n"
from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
- by (intro irreducibleD' prime_imp_irreducible)
+ by (intro irreducibleD' prime_elem_imp_irreducible)
with m show "m = 1" by (auto dest: dvd_antisym)
next
assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
- thus "is_prime_elem n"
- by (auto simp: prime_iff_irreducible irreducible_altdef)
+ thus "prime_elem n"
+ by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
qed
-lemma is_prime_nat_iff_is_prime_elem: "is_prime (n :: nat) \<longleftrightarrow> is_prime_elem n"
- by (simp add: is_prime_def)
+lemma prime_nat_iff_prime_elem: "prime (n :: nat) \<longleftrightarrow> prime_elem n"
+ by (simp add: prime_def)
-lemma is_prime_nat_iff:
- "is_prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
- by (simp add: is_prime_nat_iff_is_prime_elem is_prime_elem_nat_iff)
+lemma prime_nat_iff:
+ "prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
+ by (simp add: prime_nat_iff_prime_elem prime_elem_nat_iff)
-lemma is_prime_elem_int_nat_transfer: "is_prime_elem (n::int) \<longleftrightarrow> is_prime_elem (nat (abs n))"
+lemma prime_elem_int_nat_transfer: "prime_elem (n::int) \<longleftrightarrow> prime_elem (nat (abs n))"
proof
- assume "is_prime_elem n"
- thus "is_prime_elem (nat (abs n))" by (auto simp: is_prime_elem_def nat_dvd_iff)
+ assume "prime_elem n"
+ thus "prime_elem (nat (abs n))" by (auto simp: prime_elem_def nat_dvd_iff)
next
- assume "is_prime_elem (nat (abs n))"
- thus "is_prime_elem n"
- by (auto simp: dvd_int_unfold_dvd_nat is_prime_elem_def abs_mult nat_mult_distrib)
+ assume "prime_elem (nat (abs n))"
+ thus "prime_elem n"
+ by (auto simp: dvd_int_unfold_dvd_nat prime_elem_def abs_mult nat_mult_distrib)
qed
-lemma is_prime_elem_nat_int_transfer [simp]: "is_prime_elem (int n) \<longleftrightarrow> is_prime_elem n"
- by (auto simp: is_prime_elem_int_nat_transfer)
+lemma prime_elem_nat_int_transfer [simp]: "prime_elem (int n) \<longleftrightarrow> prime_elem n"
+ by (auto simp: prime_elem_int_nat_transfer)
-lemma is_prime_nat_int_transfer [simp]: "is_prime (int n) \<longleftrightarrow> is_prime n"
- by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
+lemma prime_nat_int_transfer [simp]: "prime (int n) \<longleftrightarrow> prime n"
+ by (auto simp: prime_elem_int_nat_transfer prime_def)
-lemma is_prime_int_nat_transfer: "is_prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> is_prime (nat n)"
- by (auto simp: is_prime_elem_int_nat_transfer is_prime_def)
+lemma prime_int_nat_transfer: "prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> prime (nat n)"
+ by (auto simp: prime_elem_int_nat_transfer prime_def)
-lemma is_prime_int_iff:
- "is_prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
+lemma prime_int_iff:
+ "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
proof (intro iffI conjI allI impI; (elim conjE)?)
- assume *: "is_prime n"
- hence irred: "irreducible n" by (simp add: prime_imp_irreducible)
+ assume *: "prime n"
+ hence irred: "irreducible n" by (simp add: prime_elem_imp_irreducible)
from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1"
- by (auto simp: is_prime_def zabs_def not_less split: if_splits)
+ by (auto simp: prime_def zabs_def not_less split: if_splits)
thus "n > 1" by presburger
fix m assume "m dvd n" \<open>m \<ge> 0\<close>
with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
@@ -121,8 +119,8 @@
with n(2) have "int m = 1 \<or> int m = n" by auto
thus "m = 1 \<or> m = nat n" by auto
qed
- ultimately show "is_prime n"
- unfolding is_prime_int_nat_transfer is_prime_nat_iff by auto
+ ultimately show "prime n"
+ unfolding prime_int_nat_transfer prime_nat_iff by auto
qed
@@ -131,7 +129,7 @@
shows "\<not>n dvd p"
proof
assume "n dvd p"
- from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
+ from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
by (cases "n = 0") (auto dest!: dvd_imp_le)
qed
@@ -141,7 +139,7 @@
shows "\<not>n dvd p"
proof
assume "n dvd p"
- from assms(1) have "irreducible p" by (simp add: prime_imp_irreducible)
+ from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
by (auto dest!: zdvd_imp_le)
qed
@@ -153,60 +151,60 @@
by (intro prime_int_not_dvd) auto
lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
- unfolding is_prime_int_iff by auto
+ unfolding prime_int_iff by auto
lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
- unfolding is_prime_nat_iff by auto
+ unfolding prime_nat_iff by auto
lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
- unfolding is_prime_int_iff by auto
+ unfolding prime_int_iff by auto
lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
- unfolding is_prime_nat_iff by auto
+ unfolding prime_nat_iff by auto
lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
- unfolding is_prime_nat_iff by auto
+ unfolding prime_nat_iff by auto
lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
- unfolding is_prime_int_iff by auto
+ unfolding prime_int_iff by auto
lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
- unfolding is_prime_nat_iff by auto
+ unfolding prime_nat_iff by auto
lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
- unfolding is_prime_nat_iff by auto
+ unfolding prime_nat_iff by auto
lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
- unfolding is_prime_int_iff by auto
+ unfolding prime_int_iff by auto
lemma prime_ge_2_nat: "prime p \<Longrightarrow> p \<ge> (2::nat)"
- unfolding is_prime_nat_iff by auto
+ unfolding prime_nat_iff by auto
lemma prime_ge_2_int: "prime p \<Longrightarrow> p \<ge> (2::int)"
- unfolding is_prime_int_iff by auto
+ unfolding prime_int_iff by auto
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))"
- unfolding is_prime_int_iff by blast
+ unfolding prime_int_iff by blast
lemma not_prime_eq_prod_nat:
assumes "m > 1" "\<not>prime (m::nat)"
shows "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
using assms irreducible_altdef[of m]
- by (auto simp: prime_iff_irreducible is_prime_def irreducible_altdef)
+ by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
subsubsection \<open>Make prime naively executable\<close>
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
- unfolding One_nat_def [symmetric] by (rule not_is_prime_1)
+ unfolding One_nat_def [symmetric] by (rule not_prime_1)
-lemma is_prime_nat_iff':
+lemma prime_nat_iff':
"prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
proof safe
assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p"
- show "is_prime p" unfolding is_prime_nat_iff
+ show "prime p" unfolding prime_nat_iff
proof (intro conjI allI impI)
fix m assume "m dvd p"
with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
@@ -215,25 +213,25 @@
with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le)
ultimately show "m = 1 \<or> m = p" by simp
qed fact+
-qed (auto simp: is_prime_nat_iff)
+qed (auto simp: prime_nat_iff)
lemma prime_nat_code [code_unfold]:
"(prime :: nat \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))"
- by (rule ext, rule is_prime_nat_iff')
+ by (rule ext, rule prime_nat_iff')
-lemma is_prime_int_iff':
+lemma prime_int_iff':
"prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs = ?rhs")
proof
assume "?lhs"
- thus "?rhs" by (auto simp: is_prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
+ thus "?rhs" by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
next
assume "?rhs"
- thus "?lhs" by (auto simp: is_prime_int_nat_transfer zdvd_int prime_nat_code)
+ thus "?lhs" by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_code)
qed
lemma prime_int_code [code_unfold]:
"(prime :: int \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))"
- by (rule ext, rule is_prime_int_iff')
+ by (rule ext, rule prime_int_iff')
lemma prime_nat_simp:
"prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
@@ -248,7 +246,7 @@
lemma two_is_prime_nat [simp]: "prime (2::nat)"
by simp
-declare is_prime_int_nat_transfer[of "numeral m" for m, simp]
+declare prime_int_nat_transfer[of "numeral m" for m, simp]
text\<open>A bit of regression testing:\<close>
@@ -282,7 +280,7 @@
then have "p dvd 1" by simp
then have "p <= 1" by auto
moreover from \<open>prime p\<close> have "p > 1"
- using is_prime_nat_iff by blast
+ using prime_nat_iff by blast
ultimately have False by auto}
then have "n < p" by presburger
with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
@@ -313,7 +311,7 @@
proof -
from assms have
"1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
- unfolding is_prime_nat_iff by auto
+ unfolding prime_nat_iff by auto
from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
have "p dvd p * q" by simp
@@ -332,7 +330,7 @@
next
case (Suc k x y)
from Suc.prems have pxy: "p dvd x*y" by auto
- from is_prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
+ from prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
{assume px: "p dvd x"
then obtain d where d: "x = p*d" unfolding dvd_def by blast
@@ -446,7 +444,7 @@
shows "\<exists>x y. a*x = Suc (p*y)"
proof -
have ap: "coprime a p"
- by (metis gcd.commute p pa is_prime_imp_coprime)
+ by (metis gcd.commute p pa prime_imp_coprime)
moreover from p have "p \<noteq> 1" by auto
ultimately have "\<exists>x y. a * x = p * y + 1"
by (rule coprime_bezout_strong)
@@ -470,7 +468,7 @@
fixes n :: int
shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
unfolding prime_factors_def
- by (auto split: if_splits simp: is_prime_def dest!: in_prime_factorization_imp_prime)
+ by (auto split: if_splits simp: prime_def dest!: in_prime_factorization_imp_prime)
lemma msetprod_prime_factorization_int:
fixes n :: int
@@ -480,7 +478,7 @@
lemma prime_factorization_exists_nat:
"n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
- using prime_factorization_exists[of n] by (auto simp: is_prime_def)
+ using prime_factorization_exists[of n] by (auto simp: prime_def)
lemma msetprod_prime_factorization_nat [simp]:
"(n::nat) > 0 \<Longrightarrow> msetprod (prime_factorization n) = n"
@@ -499,7 +497,7 @@
assumes S_eq: "S = {p. 0 < f p}"
and "finite S"
and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
- shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
+ shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
using assms by (intro prime_factorization_unique'') auto
lemma prime_factorization_unique_int:
@@ -507,7 +505,7 @@
assumes S_eq: "S = {p. 0 < f p}"
and "finite S"
and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
- shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
+ shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
using assms by (intro prime_factorization_unique'') auto
lemma prime_factors_characterization_nat:
@@ -536,23 +534,23 @@
by (rule prime_factors_characterization_int) (auto simp: abs_setprod prime_ge_0_int)
lemma multiplicity_characterization_nat:
- "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> is_prime p \<Longrightarrow>
+ "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow>
n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
- (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> is_prime p \<longrightarrow>
+ (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> prime p \<longrightarrow>
multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
by (intro impI, rule multiplicity_characterization_nat) auto
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
- finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> is_prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
+ finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric])
(auto simp: abs_setprod power_abs prime_ge_0_int intro!: setprod.cong)
lemma multiplicity_characterization'_int [rule_format]:
"finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
- (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> is_prime p \<Longrightarrow>
+ (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> prime p \<Longrightarrow>
multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
@@ -561,18 +559,18 @@
lemma multiplicity_eq_nat:
fixes x and y::nat
- assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+ assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
shows "x = y"
using multiplicity_eq_imp_eq[of x y] assms by simp
lemma multiplicity_eq_int:
fixes x y :: int
- assumes "x > 0" "y > 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+ assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
shows "x = y"
using multiplicity_eq_imp_eq[of x y] assms by simp
lemma multiplicity_prod_prime_powers:
- assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> is_prime x" "is_prime p"
+ assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> prime x" "prime p"
shows "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
proof -
define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
@@ -592,7 +590,7 @@
also have "\<dots> = msetprod A"
by (auto simp: msetprod_multiplicity count_A set_mset_A intro!: setprod.cong)
also from assms have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
- by (subst prime_multiplicity_msetprod_distrib) (auto dest: prime)
+ by (subst prime_elem_multiplicity_msetprod_distrib) (auto dest: prime)
also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
also have "msetsum \<dots> = (if p \<in> S then f p else 0)" by (simp add: msetsum_delta count_A g_def)
@@ -600,21 +598,21 @@
qed
(* TODO Legacy names *)
-lemmas prime_imp_coprime_nat = is_prime_imp_coprime[where ?'a = nat]
-lemmas prime_imp_coprime_int = is_prime_imp_coprime[where ?'a = int]
-lemmas prime_dvd_mult_nat = is_prime_dvd_mult_iff[where ?'a = nat]
-lemmas prime_dvd_mult_int = is_prime_dvd_mult_iff[where ?'a = int]
-lemmas prime_dvd_mult_eq_nat = is_prime_dvd_mult_iff[where ?'a = nat]
-lemmas prime_dvd_mult_eq_int = is_prime_dvd_mult_iff[where ?'a = int]
-lemmas prime_dvd_power_nat = is_prime_dvd_power[where ?'a = nat]
-lemmas prime_dvd_power_int = is_prime_dvd_power[where ?'a = int]
-lemmas prime_dvd_power_nat_iff = is_prime_dvd_power_iff[where ?'a = nat]
-lemmas prime_dvd_power_int_iff = is_prime_dvd_power_iff[where ?'a = int]
-lemmas prime_imp_power_coprime_nat = is_prime_imp_power_coprime[where ?'a = nat]
-lemmas prime_imp_power_coprime_int = is_prime_imp_power_coprime[where ?'a = int]
+lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
+lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
+lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat]
+lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int]
+lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat]
+lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int]
+lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat]
+lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int]
+lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat]
+lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int]
+lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat]
+lemmas prime_imp_power_coprime_int = prime_imp_power_coprime[where ?'a = int]
lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
-lemmas prime_divprod_pow_nat = prime_divprod_pow[where ?'a = nat]
-lemmas prime_exp = is_prime_elem_power_iff[where ?'a = nat]
+lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
+lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
-end
\ No newline at end of file
+end
--- a/src/HOL/Number_Theory/Residues.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Number_Theory/Residues.thy Tue Aug 09 19:45:01 2016 +0200
@@ -280,7 +280,7 @@
qed
then show ?thesis
using \<open>2 \<le> p\<close>
- by (simp add: is_prime_nat_iff)
+ by (simp add: prime_nat_iff)
(metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
not_numeral_le_zero one_dvd)
qed
--- a/src/HOL/Proofs/Extraction/Euclid.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy Tue Aug 09 19:45:01 2016 +0200
@@ -28,7 +28,7 @@
by (induct m) auto
lemma prime_eq: "prime (p::nat) \<longleftrightarrow> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p)"
- apply (simp add: is_prime_nat_iff)
+ apply (simp add: prime_nat_iff)
apply (rule iffI)
apply blast
apply (erule conjE)
--- a/src/HOL/Tools/simpdata.ML Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/Tools/simpdata.ML Tue Aug 09 19:45:01 2016 +0200
@@ -152,6 +152,7 @@
val contrapos = @{thm contrapos_nn}
val contrapos2 = @{thm contrapos_pp}
val notnotD = @{thm notnotD}
+ val safe_tac = Classical.safe_tac
);
val split_tac = Splitter.split_tac;
--- a/src/HOL/ex/Sqrt.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/ex/Sqrt.thy Tue Aug 09 19:45:01 2016 +0200
@@ -14,7 +14,7 @@
assumes "prime (p::nat)"
shows "sqrt p \<notin> \<rat>"
proof
- from \<open>prime p\<close> have p: "1 < p" by (simp add: is_prime_nat_iff)
+ from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_iff)
assume "sqrt p \<in> \<rat>"
then obtain m n :: nat where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
@@ -59,7 +59,7 @@
assumes "prime (p::nat)"
shows "sqrt p \<notin> \<rat>"
proof
- from \<open>prime p\<close> have p: "1 < p" by (simp add: is_prime_nat_iff)
+ from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_iff)
assume "sqrt p \<in> \<rat>"
then obtain m n :: nat where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
--- a/src/HOL/ex/Sqrt_Script.thy Tue Aug 09 19:44:28 2016 +0200
+++ b/src/HOL/ex/Sqrt_Script.thy Tue Aug 09 19:45:01 2016 +0200
@@ -17,7 +17,7 @@
subsection \<open>Preliminaries\<close>
lemma prime_nonzero: "prime (p::nat) \<Longrightarrow> p \<noteq> 0"
- by (force simp add: is_prime_nat_iff)
+ by (force simp add: prime_nat_iff)
lemma prime_dvd_other_side:
"(n::nat) * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
@@ -32,7 +32,7 @@
apply (erule disjE)
apply (frule mult_le_mono, assumption)
apply auto
- apply (force simp add: is_prime_nat_iff)
+ apply (force simp add: prime_nat_iff)
done
lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"
--- a/src/Provers/splitter.ML Tue Aug 09 19:44:28 2016 +0200
+++ b/src/Provers/splitter.ML Tue Aug 09 19:45:01 2016 +0200
@@ -19,6 +19,7 @@
val contrapos : thm (* "[| ~ Q; P ==> Q |] ==> ~ P" *)
val contrapos2 : thm (* "[| Q; ~ P ==> ~ Q |] ==> P" *)
val notnotD : thm (* "~ ~ P ==> P" *)
+ val safe_tac : Proof.context -> tactic
end
signature SPLITTER =
@@ -33,9 +34,8 @@
val split_inside_tac: Proof.context -> thm list -> int -> tactic
val split_asm_tac : Proof.context -> thm list -> int -> tactic
val add_split: thm -> Proof.context -> Proof.context
+ val add_split_bang: thm -> Proof.context -> Proof.context
val del_split: thm -> Proof.context -> Proof.context
- val split_add: attribute
- val split_del: attribute
val split_modifiers : Method.modifier parser list
end;
@@ -435,12 +435,20 @@
fun split_name (name, T) asm = "split " ^
(if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;
-fun add_split split ctxt =
+fun gen_add_split bang split ctxt =
let
val (name, asm) = split_thm_info split
- fun tac ctxt' = (if asm then split_asm_tac else split_tac) ctxt' [split]
+ fun tac ctxt' =
+ (if asm then split_asm_tac ctxt' [split]
+ else if bang
+ then split_tac ctxt' [split] THEN_ALL_NEW
+ TRY o (SELECT_GOAL (Data.safe_tac ctxt'))
+ else split_tac ctxt' [split])
in Simplifier.addloop (ctxt, (split_name name asm, tac)) end;
+val add_split = gen_add_split false;
+val add_split_bang = gen_add_split true;
+
fun del_split split ctxt =
let val (name, asm) = split_thm_info split
in Simplifier.delloop (ctxt, split_name name asm) end;
@@ -450,20 +458,26 @@
val splitN = "split";
-val split_add = Simplifier.attrib add_split;
+fun split_add bang = Simplifier.attrib (gen_add_split bang);
val split_del = Simplifier.attrib del_split;
-val _ =
- Theory.setup
- (Attrib.setup @{binding split}
- (Attrib.add_del split_add split_del) "declare case split rule");
+val opt_bang = Scan.optional (Args.bang >> K true) false;
+
+val add_del =
+ Scan.lift (Args.add |-- opt_bang >> split_add
+ || Args.del >> K split_del || opt_bang >> split_add);
+
+val _ = Theory.setup
+ (Attrib.setup @{binding split} add_del "declare case split rule");
(* methods *)
val split_modifiers =
- [Args.$$$ splitN -- Args.colon >> K (Method.modifier split_add @{here}),
- Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier split_add @{here}),
+ [Args.$$$ splitN -- Args.colon >> K (Method.modifier (split_add false) @{here}),
+ Args.$$$ splitN -- Args.bang_colon >> K (Method.modifier (split_add true) @{here}),
+ Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier (split_add false) @{here}),
+ Args.$$$ splitN -- Args.add -- Args.bang_colon >> K (Method.modifier (split_add true) @{here}),
Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del @{here})];
val _ =