author | paulson <lp15@cam.ac.uk> |
Mon, 30 Nov 2020 22:00:23 +0000 | |
changeset 72797 | 402afc68f2f9 |
parent 71398 | e0237f2eb49d |
child 73103 | b69fd6e19662 |
permissions | -rw-r--r-- |
65435 | 1 |
(* Title: HOL/Computational_Algebra/Factorial_Ring.thy |
63924 | 2 |
Author: Manuel Eberl, TU Muenchen |
60804 | 3 |
Author: Florian Haftmann, TU Muenchen |
4 |
*) |
|
5 |
||
6 |
section \<open>Factorial (semi)rings\<close> |
|
7 |
||
8 |
theory Factorial_Ring |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
9 |
imports |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
10 |
Main |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66276
diff
changeset
|
11 |
"HOL-Library.Multiset" |
63498 | 12 |
begin |
13 |
||
63924 | 14 |
subsection \<open>Irreducible and prime elements\<close> |
63498 | 15 |
|
16 |
context comm_semiring_1 |
|
62499 | 17 |
begin |
18 |
||
63498 | 19 |
definition irreducible :: "'a \<Rightarrow> bool" where |
20 |
"irreducible p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p = a * b \<longrightarrow> a dvd 1 \<or> b dvd 1)" |
|
21 |
||
22 |
lemma not_irreducible_zero [simp]: "\<not>irreducible 0" |
|
23 |
by (simp add: irreducible_def) |
|
24 |
||
25 |
lemma irreducible_not_unit: "irreducible p \<Longrightarrow> \<not>p dvd 1" |
|
26 |
by (simp add: irreducible_def) |
|
27 |
||
28 |
lemma not_irreducible_one [simp]: "\<not>irreducible 1" |
|
29 |
by (simp add: irreducible_def) |
|
30 |
||
31 |
lemma irreducibleI: |
|
32 |
"p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1) \<Longrightarrow> irreducible p" |
|
33 |
by (simp add: irreducible_def) |
|
34 |
||
35 |
lemma irreducibleD: "irreducible p \<Longrightarrow> p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1" |
|
36 |
by (simp add: irreducible_def) |
|
37 |
||
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
38 |
lemma irreducible_mono: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
39 |
assumes irr: "irreducible b" and "a dvd b" "\<not>a dvd 1" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
40 |
shows "irreducible a" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
41 |
proof (rule irreducibleI) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
42 |
fix c d assume "a = c * d" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
43 |
from assms obtain k where [simp]: "b = a * k" by auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
44 |
from \<open>a = c * d\<close> have "b = c * d * k" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
45 |
by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
46 |
hence "c dvd 1 \<or> (d * k) dvd 1" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
47 |
using irreducibleD[OF irr, of c "d * k"] by (auto simp: mult.assoc) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
48 |
thus "c dvd 1 \<or> d dvd 1" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
49 |
by auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
50 |
qed (use assms in \<open>auto simp: irreducible_def\<close>) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
51 |
|
63633 | 52 |
definition prime_elem :: "'a \<Rightarrow> bool" where |
53 |
"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)" |
|
63498 | 54 |
|
63633 | 55 |
lemma not_prime_elem_zero [simp]: "\<not>prime_elem 0" |
56 |
by (simp add: prime_elem_def) |
|
63498 | 57 |
|
63633 | 58 |
lemma prime_elem_not_unit: "prime_elem p \<Longrightarrow> \<not>p dvd 1" |
59 |
by (simp add: prime_elem_def) |
|
63498 | 60 |
|
63633 | 61 |
lemma prime_elemI: |
62 |
"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" |
|
63 |
by (simp add: prime_elem_def) |
|
63498 | 64 |
|
63633 | 65 |
lemma prime_elem_dvd_multD: |
66 |
"prime_elem p \<Longrightarrow> p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b" |
|
67 |
by (simp add: prime_elem_def) |
|
63498 | 68 |
|
63633 | 69 |
lemma prime_elem_dvd_mult_iff: |
70 |
"prime_elem p \<Longrightarrow> p dvd (a * b) \<longleftrightarrow> p dvd a \<or> p dvd b" |
|
71 |
by (auto simp: prime_elem_def) |
|
63498 | 72 |
|
63633 | 73 |
lemma not_prime_elem_one [simp]: |
74 |
"\<not> prime_elem 1" |
|
75 |
by (auto dest: prime_elem_not_unit) |
|
63498 | 76 |
|
63633 | 77 |
lemma prime_elem_not_zeroI: |
78 |
assumes "prime_elem p" |
|
63498 | 79 |
shows "p \<noteq> 0" |
80 |
using assms by (auto intro: ccontr) |
|
81 |
||
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
82 |
lemma prime_elem_dvd_power: |
63633 | 83 |
"prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x" |
84 |
by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1]) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
85 |
|
63633 | 86 |
lemma prime_elem_dvd_power_iff: |
87 |
"prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x" |
|
88 |
by (auto dest: prime_elem_dvd_power intro: dvd_trans) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
89 |
|
63633 | 90 |
lemma prime_elem_imp_nonzero [simp]: |
91 |
"ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 0" |
|
92 |
unfolding ASSUMPTION_def by (rule prime_elem_not_zeroI) |
|
63498 | 93 |
|
63633 | 94 |
lemma prime_elem_imp_not_one [simp]: |
95 |
"ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 1" |
|
63498 | 96 |
unfolding ASSUMPTION_def by auto |
97 |
||
98 |
end |
|
99 |
||
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
100 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
101 |
lemma (in normalization_semidom) irreducible_cong: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
102 |
assumes "normalize a = normalize b" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
103 |
shows "irreducible a \<longleftrightarrow> irreducible b" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
104 |
proof (cases "a = 0 \<or> a dvd 1") |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
105 |
case True |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
106 |
hence "\<not>irreducible a" by (auto simp: irreducible_def) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
107 |
from True have "normalize a = 0 \<or> normalize a dvd 1" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
108 |
by auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
109 |
also note assms |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
110 |
finally have "b = 0 \<or> b dvd 1" by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
111 |
hence "\<not>irreducible b" by (auto simp: irreducible_def) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
112 |
with \<open>\<not>irreducible a\<close> show ?thesis by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
113 |
next |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
114 |
case False |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
115 |
hence b: "b \<noteq> 0" "\<not>is_unit b" using assms |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
116 |
by (auto simp: is_unit_normalize[of b]) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
117 |
show ?thesis |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
118 |
proof |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
119 |
assume "irreducible a" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
120 |
thus "irreducible b" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
121 |
by (rule irreducible_mono) (use assms False b in \<open>auto dest: associatedD2\<close>) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
122 |
next |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
123 |
assume "irreducible b" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
124 |
thus "irreducible a" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
125 |
by (rule irreducible_mono) (use assms False b in \<open>auto dest: associatedD1\<close>) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
126 |
qed |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
127 |
qed |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
128 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
129 |
lemma (in normalization_semidom) associatedE1: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
130 |
assumes "normalize a = normalize b" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
131 |
obtains u where "is_unit u" "a = u * b" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
132 |
proof (cases "a = 0") |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
133 |
case [simp]: False |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
134 |
from assms have [simp]: "b \<noteq> 0" by auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
135 |
show ?thesis |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
136 |
proof (rule that) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
137 |
show "is_unit (unit_factor a div unit_factor b)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
138 |
by auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
139 |
have "unit_factor a div unit_factor b * b = unit_factor a * (b div unit_factor b)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
140 |
using \<open>b \<noteq> 0\<close> unit_div_commute unit_div_mult_swap unit_factor_is_unit by metis |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
141 |
also have "b div unit_factor b = normalize b" by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
142 |
finally show "a = unit_factor a div unit_factor b * b" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
143 |
by (metis assms unit_factor_mult_normalize) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
144 |
qed |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
145 |
next |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
146 |
case [simp]: True |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
147 |
hence [simp]: "b = 0" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
148 |
using assms[symmetric] by auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
149 |
show ?thesis |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
150 |
by (intro that[of 1]) auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
151 |
qed |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
152 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
153 |
lemma (in normalization_semidom) associatedE2: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
154 |
assumes "normalize a = normalize b" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
155 |
obtains u where "is_unit u" "b = u * a" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
156 |
proof - |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
157 |
from assms have "normalize b = normalize a" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
158 |
by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
159 |
then obtain u where "is_unit u" "b = u * a" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
160 |
by (elim associatedE1) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
161 |
thus ?thesis using that by blast |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
162 |
qed |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
163 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
164 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
165 |
(* TODO Move *) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
166 |
lemma (in normalization_semidom) normalize_power_normalize: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
167 |
"normalize (normalize x ^ n) = normalize (x ^ n)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
168 |
proof (induction n) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
169 |
case (Suc n) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
170 |
have "normalize (normalize x ^ Suc n) = normalize (x * normalize (normalize x ^ n))" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
171 |
by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
172 |
also note Suc.IH |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
173 |
finally show ?case by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
174 |
qed auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
175 |
|
62499 | 176 |
context algebraic_semidom |
60804 | 177 |
begin |
178 |
||
63633 | 179 |
lemma prime_elem_imp_irreducible: |
180 |
assumes "prime_elem p" |
|
63498 | 181 |
shows "irreducible p" |
182 |
proof (rule irreducibleI) |
|
183 |
fix a b |
|
184 |
assume p_eq: "p = a * b" |
|
185 |
with assms have nz: "a \<noteq> 0" "b \<noteq> 0" by auto |
|
186 |
from p_eq have "p dvd a * b" by simp |
|
63633 | 187 |
with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD) |
63498 | 188 |
with \<open>p = a * b\<close> have "a * b dvd 1 * b \<or> a * b dvd a * 1" by auto |
189 |
thus "a dvd 1 \<or> b dvd 1" |
|
190 |
by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)]) |
|
63633 | 191 |
qed (insert assms, simp_all add: prime_elem_def) |
63498 | 192 |
|
63924 | 193 |
lemma (in algebraic_semidom) unit_imp_no_irreducible_divisors: |
194 |
assumes "is_unit x" "irreducible p" |
|
195 |
shows "\<not>p dvd x" |
|
196 |
proof (rule notI) |
|
197 |
assume "p dvd x" |
|
198 |
with \<open>is_unit x\<close> have "is_unit p" |
|
199 |
by (auto intro: dvd_trans) |
|
200 |
with \<open>irreducible p\<close> show False |
|
201 |
by (simp add: irreducible_not_unit) |
|
202 |
qed |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
203 |
|
63924 | 204 |
lemma unit_imp_no_prime_divisors: |
205 |
assumes "is_unit x" "prime_elem p" |
|
206 |
shows "\<not>p dvd x" |
|
207 |
using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] . |
|
208 |
||
63633 | 209 |
lemma prime_elem_mono: |
210 |
assumes "prime_elem p" "\<not>q dvd 1" "q dvd p" |
|
211 |
shows "prime_elem q" |
|
63498 | 212 |
proof - |
213 |
from \<open>q dvd p\<close> obtain r where r: "p = q * r" by (elim dvdE) |
|
214 |
hence "p dvd q * r" by simp |
|
63633 | 215 |
with \<open>prime_elem p\<close> have "p dvd q \<or> p dvd r" by (rule prime_elem_dvd_multD) |
63498 | 216 |
hence "p dvd q" |
217 |
proof |
|
218 |
assume "p dvd r" |
|
219 |
then obtain s where s: "r = p * s" by (elim dvdE) |
|
220 |
from r have "p * 1 = p * (q * s)" by (subst (asm) s) (simp add: mult_ac) |
|
63633 | 221 |
with \<open>prime_elem p\<close> have "q dvd 1" |
63498 | 222 |
by (subst (asm) mult_cancel_left) auto |
223 |
with \<open>\<not>q dvd 1\<close> show ?thesis by contradiction |
|
224 |
qed |
|
225 |
||
226 |
show ?thesis |
|
63633 | 227 |
proof (rule prime_elemI) |
63498 | 228 |
fix a b assume "q dvd (a * b)" |
229 |
with \<open>p dvd q\<close> have "p dvd (a * b)" by (rule dvd_trans) |
|
63633 | 230 |
with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD) |
63498 | 231 |
with \<open>q dvd p\<close> show "q dvd a \<or> q dvd b" by (blast intro: dvd_trans) |
232 |
qed (insert assms, auto) |
|
62499 | 233 |
qed |
234 |
||
63498 | 235 |
lemma irreducibleD': |
236 |
assumes "irreducible a" "b dvd a" |
|
237 |
shows "a dvd b \<or> is_unit b" |
|
238 |
proof - |
|
239 |
from assms obtain c where c: "a = b * c" by (elim dvdE) |
|
240 |
from irreducibleD[OF assms(1) this] have "is_unit b \<or> is_unit c" . |
|
241 |
thus ?thesis by (auto simp: c mult_unit_dvd_iff) |
|
242 |
qed |
|
60804 | 243 |
|
63498 | 244 |
lemma irreducibleI': |
245 |
assumes "a \<noteq> 0" "\<not>is_unit a" "\<And>b. b dvd a \<Longrightarrow> a dvd b \<or> is_unit b" |
|
246 |
shows "irreducible a" |
|
247 |
proof (rule irreducibleI) |
|
248 |
fix b c assume a_eq: "a = b * c" |
|
249 |
hence "a dvd b \<or> is_unit b" by (intro assms) simp_all |
|
250 |
thus "is_unit b \<or> is_unit c" |
|
251 |
proof |
|
252 |
assume "a dvd b" |
|
253 |
hence "b * c dvd b * 1" by (simp add: a_eq) |
|
254 |
moreover from \<open>a \<noteq> 0\<close> a_eq have "b \<noteq> 0" by auto |
|
255 |
ultimately show ?thesis by (subst (asm) dvd_times_left_cancel_iff) auto |
|
256 |
qed blast |
|
257 |
qed (simp_all add: assms(1,2)) |
|
60804 | 258 |
|
63498 | 259 |
lemma irreducible_altdef: |
260 |
"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)" |
|
261 |
using irreducibleI'[of x] irreducibleD'[of x] irreducible_not_unit[of x] by auto |
|
60804 | 262 |
|
63633 | 263 |
lemma prime_elem_multD: |
264 |
assumes "prime_elem (a * b)" |
|
60804 | 265 |
shows "is_unit a \<or> is_unit b" |
266 |
proof - |
|
63633 | 267 |
from assms have "a \<noteq> 0" "b \<noteq> 0" by (auto dest!: prime_elem_not_zeroI) |
268 |
moreover from assms prime_elem_dvd_multD [of "a * b"] have "a * b dvd a \<or> a * b dvd b" |
|
60804 | 269 |
by auto |
270 |
ultimately show ?thesis |
|
271 |
using dvd_times_left_cancel_iff [of a b 1] |
|
272 |
dvd_times_right_cancel_iff [of b a 1] |
|
273 |
by auto |
|
274 |
qed |
|
275 |
||
63633 | 276 |
lemma prime_elemD2: |
277 |
assumes "prime_elem p" and "a dvd p" and "\<not> is_unit a" |
|
60804 | 278 |
shows "p dvd a" |
279 |
proof - |
|
280 |
from \<open>a dvd p\<close> obtain b where "p = a * b" .. |
|
63633 | 281 |
with \<open>prime_elem p\<close> prime_elem_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto |
60804 | 282 |
with \<open>p = a * b\<close> show ?thesis |
283 |
by (auto simp add: mult_unit_dvd_iff) |
|
284 |
qed |
|
285 |
||
63830 | 286 |
lemma prime_elem_dvd_prod_msetE: |
63633 | 287 |
assumes "prime_elem p" |
63830 | 288 |
assumes dvd: "p dvd prod_mset A" |
63633 | 289 |
obtains a where "a \<in># A" and "p dvd a" |
290 |
proof - |
|
291 |
from dvd have "\<exists>a. a \<in># A \<and> p dvd a" |
|
292 |
proof (induct A) |
|
293 |
case empty then show ?case |
|
294 |
using \<open>prime_elem p\<close> by (simp add: prime_elem_not_unit) |
|
295 |
next |
|
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63633
diff
changeset
|
296 |
case (add a A) |
63830 | 297 |
then have "p dvd a * prod_mset A" by simp |
298 |
with \<open>prime_elem p\<close> consider (A) "p dvd prod_mset A" | (B) "p dvd a" |
|
63633 | 299 |
by (blast dest: prime_elem_dvd_multD) |
300 |
then show ?case proof cases |
|
301 |
case B then show ?thesis by auto |
|
302 |
next |
|
303 |
case A |
|
304 |
with add.hyps obtain b where "b \<in># A" "p dvd b" |
|
305 |
by auto |
|
306 |
then show ?thesis by auto |
|
307 |
qed |
|
308 |
qed |
|
309 |
with that show thesis by blast |
|
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
310 |
|
63633 | 311 |
qed |
312 |
||
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
313 |
context |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
314 |
begin |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
315 |
|
63633 | 316 |
private lemma prime_elem_powerD: |
317 |
assumes "prime_elem (p ^ n)" |
|
318 |
shows "prime_elem p \<and> n = 1" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
319 |
proof (cases n) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
320 |
case (Suc m) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
321 |
note assms |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
322 |
also from Suc have "p ^ n = p * p^m" by simp |
63633 | 323 |
finally have "is_unit p \<or> is_unit (p^m)" by (rule prime_elem_multD) |
324 |
moreover from assms have "\<not>is_unit p" by (simp add: prime_elem_def is_unit_power_iff) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
325 |
ultimately have "is_unit (p ^ m)" by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
326 |
with \<open>\<not>is_unit p\<close> have "m = 0" by (simp add: is_unit_power_iff) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
327 |
with Suc assms show ?thesis by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
328 |
qed (insert assms, simp_all) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
329 |
|
63633 | 330 |
lemma prime_elem_power_iff: |
331 |
"prime_elem (p ^ n) \<longleftrightarrow> prime_elem p \<and> n = 1" |
|
332 |
by (auto dest: prime_elem_powerD) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
333 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
334 |
end |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
335 |
|
63498 | 336 |
lemma irreducible_mult_unit_left: |
337 |
"is_unit a \<Longrightarrow> irreducible (a * p) \<longleftrightarrow> irreducible p" |
|
338 |
by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff |
|
339 |
mult_unit_dvd_iff dvd_mult_unit_iff) |
|
340 |
||
63633 | 341 |
lemma prime_elem_mult_unit_left: |
342 |
"is_unit a \<Longrightarrow> prime_elem (a * p) \<longleftrightarrow> prime_elem p" |
|
343 |
by (auto simp: prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff) |
|
63498 | 344 |
|
63633 | 345 |
lemma prime_elem_dvd_cases: |
346 |
assumes pk: "p*k dvd m*n" and p: "prime_elem p" |
|
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
347 |
shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
348 |
proof - |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
349 |
have "p dvd m*n" using dvd_mult_left pk by blast |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
350 |
then consider "p dvd m" | "p dvd n" |
63633 | 351 |
using p prime_elem_dvd_mult_iff by blast |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
352 |
then show ?thesis |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
353 |
proof cases |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
354 |
case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
355 |
then have "\<exists>x. k dvd x * n \<and> m = p * x" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
356 |
using p pk by (auto simp: mult.assoc) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
357 |
then show ?thesis .. |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
358 |
next |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
359 |
case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) |
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
360 |
with p pk have "\<exists>y. k dvd m*y \<and> n = p*y" |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
361 |
by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
362 |
then show ?thesis .. |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
363 |
qed |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
364 |
qed |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
365 |
|
63633 | 366 |
lemma prime_elem_power_dvd_prod: |
367 |
assumes pc: "p^c dvd m*n" and p: "prime_elem p" |
|
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
368 |
shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
369 |
using pc |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
370 |
proof (induct c arbitrary: m n) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
371 |
case 0 show ?case by simp |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
372 |
next |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
373 |
case (Suc c) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
374 |
consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y" |
63633 | 375 |
using prime_elem_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
376 |
then show ?case |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
377 |
proof cases |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
378 |
case (1 x) |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
379 |
with Suc.hyps[of x n] obtain a b where "a + b = c \<and> p ^ a dvd x \<and> p ^ b dvd n" by blast |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
380 |
with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
381 |
by (auto intro: mult_dvd_mono) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
382 |
thus ?thesis by blast |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
383 |
next |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
384 |
case (2 y) |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
385 |
with Suc.hyps[of m y] obtain a b where "a + b = c \<and> p ^ a dvd m \<and> p ^ b dvd y" by blast |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
386 |
with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
387 |
by (auto intro: mult_dvd_mono) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
388 |
with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n" |
68606
96a49db47c97
removal of smt and certain refinements
paulson <lp15@cam.ac.uk>
parents:
67051
diff
changeset
|
389 |
by blast |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
390 |
qed |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
391 |
qed |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
392 |
|
63633 | 393 |
lemma prime_elem_power_dvd_cases: |
63924 | 394 |
assumes "p ^ c dvd m * n" and "a + b = Suc c" and "prime_elem p" |
395 |
shows "p ^ a dvd m \<or> p ^ b dvd n" |
|
396 |
proof - |
|
397 |
from assms obtain r s |
|
398 |
where "r + s = c \<and> p ^ r dvd m \<and> p ^ s dvd n" |
|
399 |
by (blast dest: prime_elem_power_dvd_prod) |
|
400 |
moreover with assms have |
|
401 |
"a \<le> r \<or> b \<le> s" by arith |
|
402 |
ultimately show ?thesis by (auto intro: power_le_dvd) |
|
403 |
qed |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
404 |
|
63633 | 405 |
lemma prime_elem_not_unit' [simp]: |
406 |
"ASSUMPTION (prime_elem x) \<Longrightarrow> \<not>is_unit x" |
|
407 |
unfolding ASSUMPTION_def by (rule prime_elem_not_unit) |
|
63498 | 408 |
|
63633 | 409 |
lemma prime_elem_dvd_power_iff: |
410 |
assumes "prime_elem p" |
|
62499 | 411 |
shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0" |
63633 | 412 |
using assms by (induct n) (auto dest: prime_elem_not_unit prime_elem_dvd_multD) |
62499 | 413 |
|
414 |
lemma prime_power_dvd_multD: |
|
63633 | 415 |
assumes "prime_elem p" |
62499 | 416 |
assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a" |
417 |
shows "p ^ n dvd b" |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
418 |
using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> |
63633 | 419 |
proof (induct n arbitrary: b) |
62499 | 420 |
case 0 then show ?case by simp |
421 |
next |
|
422 |
case (Suc n) show ?case |
|
423 |
proof (cases "n = 0") |
|
63633 | 424 |
case True with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> show ?thesis |
425 |
by (simp add: prime_elem_dvd_mult_iff) |
|
62499 | 426 |
next |
427 |
case False then have "n > 0" by simp |
|
63633 | 428 |
from \<open>prime_elem p\<close> have "p \<noteq> 0" by auto |
62499 | 429 |
from Suc.prems have *: "p * p ^ n dvd a * b" |
430 |
by simp |
|
431 |
then have "p dvd a * b" |
|
432 |
by (rule dvd_mult_left) |
|
63633 | 433 |
with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> have "p dvd b" |
434 |
by (simp add: prime_elem_dvd_mult_iff) |
|
63040 | 435 |
moreover define c where "c = b div p" |
62499 | 436 |
ultimately have b: "b = p * c" by simp |
437 |
with * have "p * p ^ n dvd p * (a * c)" |
|
438 |
by (simp add: ac_simps) |
|
439 |
with \<open>p \<noteq> 0\<close> have "p ^ n dvd a * c" |
|
440 |
by simp |
|
441 |
with Suc.hyps \<open>n > 0\<close> have "p ^ n dvd c" |
|
442 |
by blast |
|
443 |
with \<open>p \<noteq> 0\<close> show ?thesis |
|
444 |
by (simp add: b) |
|
445 |
qed |
|
446 |
qed |
|
447 |
||
63633 | 448 |
end |
449 |
||
63924 | 450 |
|
451 |
subsection \<open>Generalized primes: normalized prime elements\<close> |
|
452 |
||
63633 | 453 |
context normalization_semidom |
454 |
begin |
|
455 |
||
63924 | 456 |
lemma irreducible_normalized_divisors: |
457 |
assumes "irreducible x" "y dvd x" "normalize y = y" |
|
458 |
shows "y = 1 \<or> y = normalize x" |
|
459 |
proof - |
|
460 |
from assms have "is_unit y \<or> x dvd y" by (auto simp: irreducible_altdef) |
|
461 |
thus ?thesis |
|
462 |
proof (elim disjE) |
|
463 |
assume "is_unit y" |
|
464 |
hence "normalize y = 1" by (simp add: is_unit_normalize) |
|
465 |
with assms show ?thesis by simp |
|
466 |
next |
|
467 |
assume "x dvd y" |
|
468 |
with \<open>y dvd x\<close> have "normalize y = normalize x" by (rule associatedI) |
|
469 |
with assms show ?thesis by simp |
|
470 |
qed |
|
471 |
qed |
|
472 |
||
63633 | 473 |
lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x" |
474 |
using irreducible_mult_unit_left[of "1 div unit_factor x" x] |
|
475 |
by (cases "x = 0") (simp_all add: unit_div_commute) |
|
476 |
||
477 |
lemma prime_elem_normalize_iff [simp]: "prime_elem (normalize x) = prime_elem x" |
|
478 |
using prime_elem_mult_unit_left[of "1 div unit_factor x" x] |
|
479 |
by (cases "x = 0") (simp_all add: unit_div_commute) |
|
480 |
||
481 |
lemma prime_elem_associated: |
|
482 |
assumes "prime_elem p" and "prime_elem q" and "q dvd p" |
|
483 |
shows "normalize q = normalize p" |
|
484 |
using \<open>q dvd p\<close> proof (rule associatedI) |
|
485 |
from \<open>prime_elem q\<close> have "\<not> is_unit q" |
|
486 |
by (auto simp add: prime_elem_not_unit) |
|
487 |
with \<open>prime_elem p\<close> \<open>q dvd p\<close> show "p dvd q" |
|
488 |
by (blast intro: prime_elemD2) |
|
489 |
qed |
|
490 |
||
491 |
definition prime :: "'a \<Rightarrow> bool" where |
|
492 |
"prime p \<longleftrightarrow> prime_elem p \<and> normalize p = p" |
|
493 |
||
494 |
lemma not_prime_0 [simp]: "\<not>prime 0" by (simp add: prime_def) |
|
495 |
||
496 |
lemma not_prime_unit: "is_unit x \<Longrightarrow> \<not>prime x" |
|
497 |
using prime_elem_not_unit[of x] by (auto simp add: prime_def) |
|
498 |
||
499 |
lemma not_prime_1 [simp]: "\<not>prime 1" by (simp add: not_prime_unit) |
|
500 |
||
501 |
lemma primeI: "prime_elem x \<Longrightarrow> normalize x = x \<Longrightarrow> prime x" |
|
502 |
by (simp add: prime_def) |
|
503 |
||
504 |
lemma prime_imp_prime_elem [dest]: "prime p \<Longrightarrow> prime_elem p" |
|
505 |
by (simp add: prime_def) |
|
506 |
||
507 |
lemma normalize_prime: "prime p \<Longrightarrow> normalize p = p" |
|
508 |
by (simp add: prime_def) |
|
509 |
||
510 |
lemma prime_normalize_iff [simp]: "prime (normalize p) \<longleftrightarrow> prime_elem p" |
|
511 |
by (auto simp add: prime_def) |
|
512 |
||
513 |
lemma prime_power_iff: |
|
514 |
"prime (p ^ n) \<longleftrightarrow> prime p \<and> n = 1" |
|
515 |
by (auto simp: prime_def prime_elem_power_iff) |
|
516 |
||
517 |
lemma prime_imp_nonzero [simp]: |
|
518 |
"ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 0" |
|
519 |
unfolding ASSUMPTION_def prime_def by auto |
|
520 |
||
521 |
lemma prime_imp_not_one [simp]: |
|
522 |
"ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 1" |
|
523 |
unfolding ASSUMPTION_def by auto |
|
524 |
||
525 |
lemma prime_not_unit' [simp]: |
|
526 |
"ASSUMPTION (prime x) \<Longrightarrow> \<not>is_unit x" |
|
527 |
unfolding ASSUMPTION_def prime_def by auto |
|
528 |
||
529 |
lemma prime_normalize' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> normalize x = x" |
|
530 |
unfolding ASSUMPTION_def prime_def by simp |
|
531 |
||
532 |
lemma unit_factor_prime: "prime x \<Longrightarrow> unit_factor x = 1" |
|
533 |
using unit_factor_normalize[of x] unfolding prime_def by auto |
|
534 |
||
535 |
lemma unit_factor_prime' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> unit_factor x = 1" |
|
536 |
unfolding ASSUMPTION_def by (rule unit_factor_prime) |
|
537 |
||
538 |
lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> prime_elem x" |
|
539 |
by (simp add: prime_def ASSUMPTION_def) |
|
540 |
||
541 |
lemma prime_dvd_multD: "prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b" |
|
542 |
by (intro prime_elem_dvd_multD) simp_all |
|
543 |
||
64631
7705926ee595
removed dangerous simp rule: prime computations can be excessively long
haftmann
parents:
64272
diff
changeset
|
544 |
lemma prime_dvd_mult_iff: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b" |
63633 | 545 |
by (auto dest: prime_dvd_multD) |
546 |
||
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
547 |
lemma prime_dvd_power: |
63633 | 548 |
"prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x" |
549 |
by (auto dest!: prime_elem_dvd_power simp: prime_def) |
|
550 |
||
551 |
lemma prime_dvd_power_iff: |
|
552 |
"prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x" |
|
553 |
by (subst prime_elem_dvd_power_iff) simp_all |
|
554 |
||
63830 | 555 |
lemma prime_dvd_prod_mset_iff: "prime p \<Longrightarrow> p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" |
63633 | 556 |
by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+) |
557 |
||
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
558 |
lemma prime_dvd_prod_iff: "finite A \<Longrightarrow> prime p \<Longrightarrow> p dvd prod f A \<longleftrightarrow> (\<exists>x\<in>A. p dvd f x)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
559 |
by (auto simp: prime_dvd_prod_mset_iff prod_unfold_prod_mset) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
560 |
|
63633 | 561 |
lemma primes_dvd_imp_eq: |
562 |
assumes "prime p" "prime q" "p dvd q" |
|
563 |
shows "p = q" |
|
564 |
proof - |
|
565 |
from assms have "irreducible q" by (simp add: prime_elem_imp_irreducible prime_def) |
|
566 |
from irreducibleD'[OF this \<open>p dvd q\<close>] assms have "q dvd p" by simp |
|
567 |
with \<open>p dvd q\<close> have "normalize p = normalize q" by (rule associatedI) |
|
568 |
with assms show "p = q" by simp |
|
569 |
qed |
|
570 |
||
63830 | 571 |
lemma prime_dvd_prod_mset_primes_iff: |
63633 | 572 |
assumes "prime p" "\<And>q. q \<in># A \<Longrightarrow> prime q" |
63830 | 573 |
shows "p dvd prod_mset A \<longleftrightarrow> p \<in># A" |
63633 | 574 |
proof - |
63830 | 575 |
from assms(1) have "p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_prod_mset_iff) |
63633 | 576 |
also from assms have "\<dots> \<longleftrightarrow> p \<in># A" by (auto dest: primes_dvd_imp_eq) |
577 |
finally show ?thesis . |
|
578 |
qed |
|
579 |
||
63830 | 580 |
lemma prod_mset_primes_dvd_imp_subset: |
581 |
assumes "prod_mset A dvd prod_mset B" "\<And>p. p \<in># A \<Longrightarrow> prime p" "\<And>p. p \<in># B \<Longrightarrow> prime p" |
|
63633 | 582 |
shows "A \<subseteq># B" |
583 |
using assms |
|
584 |
proof (induction A arbitrary: B) |
|
585 |
case empty |
|
586 |
thus ?case by simp |
|
587 |
next |
|
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63633
diff
changeset
|
588 |
case (add p A B) |
63633 | 589 |
hence p: "prime p" by simp |
590 |
define B' where "B' = B - {#p#}" |
|
63830 | 591 |
from add.prems have "p dvd prod_mset B" by (simp add: dvd_mult_left) |
63633 | 592 |
with add.prems have "p \<in># B" |
63830 | 593 |
by (subst (asm) (2) prime_dvd_prod_mset_primes_iff) simp_all |
63633 | 594 |
hence B: "B = B' + {#p#}" by (simp add: B'_def) |
595 |
from add.prems p have "A \<subseteq># B'" by (intro add.IH) (simp_all add: B) |
|
596 |
thus ?case by (simp add: B) |
|
597 |
qed |
|
598 |
||
63830 | 599 |
lemma prod_mset_dvd_prod_mset_primes_iff: |
63633 | 600 |
assumes "\<And>x. x \<in># A \<Longrightarrow> prime x" "\<And>x. x \<in># B \<Longrightarrow> prime x" |
63830 | 601 |
shows "prod_mset A dvd prod_mset B \<longleftrightarrow> A \<subseteq># B" |
602 |
using assms by (auto intro: prod_mset_subset_imp_dvd prod_mset_primes_dvd_imp_subset) |
|
63633 | 603 |
|
63830 | 604 |
lemma is_unit_prod_mset_primes_iff: |
63633 | 605 |
assumes "\<And>x. x \<in># A \<Longrightarrow> prime x" |
63830 | 606 |
shows "is_unit (prod_mset A) \<longleftrightarrow> A = {#}" |
63924 | 607 |
by (auto simp add: is_unit_prod_mset_iff) |
608 |
(meson all_not_in_conv assms not_prime_unit set_mset_eq_empty_iff) |
|
63498 | 609 |
|
63830 | 610 |
lemma prod_mset_primes_irreducible_imp_prime: |
611 |
assumes irred: "irreducible (prod_mset A)" |
|
63633 | 612 |
assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x" |
613 |
assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x" |
|
614 |
assumes C: "\<And>x. x \<in># C \<Longrightarrow> prime x" |
|
63830 | 615 |
assumes dvd: "prod_mset A dvd prod_mset B * prod_mset C" |
616 |
shows "prod_mset A dvd prod_mset B \<or> prod_mset A dvd prod_mset C" |
|
63498 | 617 |
proof - |
63830 | 618 |
from dvd have "prod_mset A dvd prod_mset (B + C)" |
63498 | 619 |
by simp |
620 |
with A B C have subset: "A \<subseteq># B + C" |
|
63830 | 621 |
by (subst (asm) prod_mset_dvd_prod_mset_primes_iff) auto |
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
622 |
define A1 and A2 where "A1 = A \<inter># B" and "A2 = A - A1" |
63498 | 623 |
have "A = A1 + A2" unfolding A1_def A2_def |
624 |
by (rule sym, intro subset_mset.add_diff_inverse) simp_all |
|
625 |
from subset have "A1 \<subseteq># B" "A2 \<subseteq># C" |
|
626 |
by (auto simp: A1_def A2_def Multiset.subset_eq_diff_conv Multiset.union_commute) |
|
63830 | 627 |
from \<open>A = A1 + A2\<close> have "prod_mset A = prod_mset A1 * prod_mset A2" by simp |
628 |
from irred and this have "is_unit (prod_mset A1) \<or> is_unit (prod_mset A2)" |
|
63498 | 629 |
by (rule irreducibleD) |
630 |
with A have "A1 = {#} \<or> A2 = {#}" unfolding A1_def A2_def |
|
63830 | 631 |
by (subst (asm) (1 2) is_unit_prod_mset_primes_iff) (auto dest: Multiset.in_diffD) |
63498 | 632 |
with dvd \<open>A = A1 + A2\<close> \<open>A1 \<subseteq># B\<close> \<open>A2 \<subseteq># C\<close> show ?thesis |
63830 | 633 |
by (auto intro: prod_mset_subset_imp_dvd) |
63498 | 634 |
qed |
635 |
||
63830 | 636 |
lemma prod_mset_primes_finite_divisor_powers: |
63633 | 637 |
assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x" |
638 |
assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x" |
|
63498 | 639 |
assumes "A \<noteq> {#}" |
63830 | 640 |
shows "finite {n. prod_mset A ^ n dvd prod_mset B}" |
63498 | 641 |
proof - |
642 |
from \<open>A \<noteq> {#}\<close> obtain x where x: "x \<in># A" by blast |
|
643 |
define m where "m = count B x" |
|
63830 | 644 |
have "{n. prod_mset A ^ n dvd prod_mset B} \<subseteq> {..m}" |
63498 | 645 |
proof safe |
63830 | 646 |
fix n assume dvd: "prod_mset A ^ n dvd prod_mset B" |
647 |
from x have "x ^ n dvd prod_mset A ^ n" by (intro dvd_power_same dvd_prod_mset) |
|
63498 | 648 |
also note dvd |
63830 | 649 |
also have "x ^ n = prod_mset (replicate_mset n x)" by simp |
63498 | 650 |
finally have "replicate_mset n x \<subseteq># B" |
63830 | 651 |
by (rule prod_mset_primes_dvd_imp_subset) (insert A B x, simp_all split: if_splits) |
63498 | 652 |
thus "n \<le> m" by (simp add: count_le_replicate_mset_subset_eq m_def) |
60804 | 653 |
qed |
63498 | 654 |
moreover have "finite {..m}" by simp |
655 |
ultimately show ?thesis by (rule finite_subset) |
|
656 |
qed |
|
657 |
||
63924 | 658 |
end |
63498 | 659 |
|
63924 | 660 |
|
67051 | 661 |
subsection \<open>In a semiring with GCD, each irreducible element is a prime element\<close> |
63498 | 662 |
|
663 |
context semiring_gcd |
|
664 |
begin |
|
665 |
||
63633 | 666 |
lemma irreducible_imp_prime_elem_gcd: |
63498 | 667 |
assumes "irreducible x" |
63633 | 668 |
shows "prime_elem x" |
669 |
proof (rule prime_elemI) |
|
63498 | 670 |
fix a b assume "x dvd a * b" |
671 |
from dvd_productE[OF this] obtain y z where yz: "x = y * z" "y dvd a" "z dvd b" . |
|
672 |
from \<open>irreducible x\<close> and \<open>x = y * z\<close> have "is_unit y \<or> is_unit z" by (rule irreducibleD) |
|
673 |
with yz show "x dvd a \<or> x dvd b" |
|
674 |
by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff') |
|
675 |
qed (insert assms, auto simp: irreducible_not_unit) |
|
676 |
||
63633 | 677 |
lemma prime_elem_imp_coprime: |
678 |
assumes "prime_elem p" "\<not>p dvd n" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
679 |
shows "coprime p n" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
680 |
proof (rule coprimeI) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
681 |
fix d assume "d dvd p" "d dvd n" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
682 |
show "is_unit d" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
683 |
proof (rule ccontr) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
684 |
assume "\<not>is_unit d" |
63633 | 685 |
from \<open>prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d" |
686 |
by (rule prime_elemD2) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
687 |
from this and \<open>d dvd n\<close> have "p dvd n" by (rule dvd_trans) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
688 |
with \<open>\<not>p dvd n\<close> show False by contradiction |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
689 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
690 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
691 |
|
63633 | 692 |
lemma prime_imp_coprime: |
693 |
assumes "prime p" "\<not>p dvd n" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
694 |
shows "coprime p n" |
63633 | 695 |
using assms by (simp add: prime_elem_imp_coprime) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
696 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
697 |
lemma prime_elem_imp_power_coprime: |
67051 | 698 |
"prime_elem p \<Longrightarrow> \<not> p dvd a \<Longrightarrow> coprime a (p ^ m)" |
699 |
by (cases "m > 0") (auto dest: prime_elem_imp_coprime simp add: ac_simps) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
700 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
701 |
lemma prime_imp_power_coprime: |
67051 | 702 |
"prime p \<Longrightarrow> \<not> p dvd a \<Longrightarrow> coprime a (p ^ m)" |
703 |
by (rule prime_elem_imp_power_coprime) simp_all |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
704 |
|
63633 | 705 |
lemma prime_elem_divprod_pow: |
706 |
assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
707 |
shows "p^n dvd a \<or> p^n dvd b" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
708 |
using assms |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
709 |
proof - |
67051 | 710 |
from p have "\<not> is_unit p" |
711 |
by simp |
|
712 |
with ab p have "\<not> p dvd a \<or> \<not> p dvd b" |
|
713 |
using not_coprimeI by blast |
|
714 |
with p have "coprime (p ^ n) a \<or> coprime (p ^ n) b" |
|
715 |
by (auto dest: prime_elem_imp_power_coprime simp add: ac_simps) |
|
716 |
with pab show ?thesis |
|
717 |
by (auto simp add: coprime_dvd_mult_left_iff coprime_dvd_mult_right_iff) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
718 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
719 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
720 |
lemma primes_coprime: |
63633 | 721 |
"prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q" |
722 |
using prime_imp_coprime primes_dvd_imp_eq by blast |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
723 |
|
63498 | 724 |
end |
725 |
||
726 |
||
63924 | 727 |
subsection \<open>Factorial semirings: algebraic structures with unique prime factorizations\<close> |
728 |
||
63498 | 729 |
class factorial_semiring = normalization_semidom + |
730 |
assumes prime_factorization_exists: |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
731 |
"x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize x" |
63924 | 732 |
|
733 |
text \<open>Alternative characterization\<close> |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
734 |
|
63924 | 735 |
lemma (in normalization_semidom) factorial_semiring_altI_aux: |
736 |
assumes finite_divisors: "\<And>x. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}" |
|
737 |
assumes irreducible_imp_prime_elem: "\<And>x. irreducible x \<Longrightarrow> prime_elem x" |
|
738 |
assumes "x \<noteq> 0" |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
739 |
shows "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize x" |
63924 | 740 |
using \<open>x \<noteq> 0\<close> |
741 |
proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct) |
|
742 |
case (less a) |
|
743 |
let ?fctrs = "\<lambda>a. {b. b dvd a \<and> normalize b = b}" |
|
744 |
show ?case |
|
745 |
proof (cases "is_unit a") |
|
746 |
case True |
|
747 |
thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize) |
|
748 |
next |
|
749 |
case False |
|
750 |
show ?thesis |
|
751 |
proof (cases "\<exists>b. b dvd a \<and> \<not>is_unit b \<and> \<not>a dvd b") |
|
752 |
case False |
|
753 |
with \<open>\<not>is_unit a\<close> less.prems have "irreducible a" by (auto simp: irreducible_altdef) |
|
754 |
hence "prime_elem a" by (rule irreducible_imp_prime_elem) |
|
755 |
thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto |
|
756 |
next |
|
757 |
case True |
|
758 |
then guess b by (elim exE conjE) note b = this |
|
759 |
||
760 |
from b have "?fctrs b \<subseteq> ?fctrs a" by (auto intro: dvd_trans) |
|
761 |
moreover from b have "normalize a \<notin> ?fctrs b" "normalize a \<in> ?fctrs a" by simp_all |
|
762 |
hence "?fctrs b \<noteq> ?fctrs a" by blast |
|
763 |
ultimately have "?fctrs b \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast |
|
764 |
with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)" |
|
765 |
by (rule psubset_card_mono) |
|
766 |
moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
767 |
ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize b" |
63924 | 768 |
by (intro less) auto |
769 |
then guess A .. note A = this |
|
770 |
||
771 |
define c where "c = a div b" |
|
772 |
from b have c: "a = b * c" by (simp add: c_def) |
|
773 |
from less.prems c have "c \<noteq> 0" by auto |
|
774 |
from b c have "?fctrs c \<subseteq> ?fctrs a" by (auto intro: dvd_trans) |
|
775 |
moreover have "normalize a \<notin> ?fctrs c" |
|
776 |
proof safe |
|
777 |
assume "normalize a dvd c" |
|
778 |
hence "b * c dvd 1 * c" by (simp add: c) |
|
779 |
hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+ |
|
780 |
with b show False by simp |
|
781 |
qed |
|
782 |
with \<open>normalize a \<in> ?fctrs a\<close> have "?fctrs a \<noteq> ?fctrs c" by blast |
|
783 |
ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast |
|
784 |
with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)" |
|
785 |
by (rule psubset_card_mono) |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
786 |
with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize c" |
63924 | 787 |
by (intro less) auto |
788 |
then guess B .. note B = this |
|
789 |
||
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
790 |
show ?thesis |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
791 |
proof (rule exI[of _ "A + B"]; safe) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
792 |
have "normalize (prod_mset (A + B)) = |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
793 |
normalize (normalize (prod_mset A) * normalize (prod_mset B))" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
794 |
by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
795 |
also have "\<dots> = normalize (b * c)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
796 |
by (simp only: A B) auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
797 |
also have "b * c = a" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
798 |
using c by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
799 |
finally show "normalize (prod_mset (A + B)) = normalize a" . |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
800 |
next |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
801 |
qed (use A B in auto) |
63924 | 802 |
qed |
803 |
qed |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
804 |
qed |
63924 | 805 |
|
806 |
lemma factorial_semiring_altI: |
|
807 |
assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}" |
|
808 |
assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x" |
|
809 |
shows "OFCLASS('a :: normalization_semidom, factorial_semiring_class)" |
|
810 |
by intro_classes (rule factorial_semiring_altI_aux[OF assms]) |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
811 |
|
63924 | 812 |
text \<open>Properties\<close> |
813 |
||
814 |
context factorial_semiring |
|
63498 | 815 |
begin |
816 |
||
817 |
lemma prime_factorization_exists': |
|
818 |
assumes "x \<noteq> 0" |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
819 |
obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "normalize (prod_mset A) = normalize x" |
63498 | 820 |
proof - |
821 |
from prime_factorization_exists[OF assms] obtain A |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
822 |
where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "normalize (prod_mset A) = normalize x" by blast |
63498 | 823 |
define A' where "A' = image_mset normalize A" |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
824 |
have "normalize (prod_mset A') = normalize (prod_mset A)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
825 |
by (simp add: A'_def normalize_prod_mset_normalize) |
63498 | 826 |
also note A(2) |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
827 |
finally have "normalize (prod_mset A') = normalize x" by simp |
63633 | 828 |
moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> prime x" by (auto simp: prime_def A'_def) |
63498 | 829 |
ultimately show ?thesis by (intro that[of A']) blast |
830 |
qed |
|
831 |
||
63633 | 832 |
lemma irreducible_imp_prime_elem: |
63498 | 833 |
assumes "irreducible x" |
63633 | 834 |
shows "prime_elem x" |
835 |
proof (rule prime_elemI) |
|
63498 | 836 |
fix a b assume dvd: "x dvd a * b" |
837 |
from assms have "x \<noteq> 0" by auto |
|
838 |
show "x dvd a \<or> x dvd b" |
|
839 |
proof (cases "a = 0 \<or> b = 0") |
|
840 |
case False |
|
841 |
hence "a \<noteq> 0" "b \<noteq> 0" by blast+ |
|
842 |
note nz = \<open>x \<noteq> 0\<close> this |
|
843 |
from nz[THEN prime_factorization_exists'] guess A B C . note ABC = this |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
844 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
845 |
have "irreducible (prod_mset A)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
846 |
by (subst irreducible_cong[OF ABC(2)]) fact |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
847 |
moreover have "normalize (prod_mset A) dvd |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
848 |
normalize (normalize (prod_mset B) * normalize (prod_mset C))" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
849 |
unfolding ABC using dvd by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
850 |
hence "prod_mset A dvd prod_mset B * prod_mset C" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
851 |
unfolding normalize_mult_normalize_left normalize_mult_normalize_right by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
852 |
ultimately have "prod_mset A dvd prod_mset B \<or> prod_mset A dvd prod_mset C" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
853 |
by (intro prod_mset_primes_irreducible_imp_prime) (use ABC in auto) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
854 |
hence "normalize (prod_mset A) dvd normalize (prod_mset B) \<or> |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
855 |
normalize (prod_mset A) dvd normalize (prod_mset C)" by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
856 |
thus ?thesis unfolding ABC by simp |
63498 | 857 |
qed auto |
858 |
qed (insert assms, simp_all add: irreducible_def) |
|
859 |
||
860 |
lemma finite_divisor_powers: |
|
861 |
assumes "y \<noteq> 0" "\<not>is_unit x" |
|
862 |
shows "finite {n. x ^ n dvd y}" |
|
863 |
proof (cases "x = 0") |
|
864 |
case True |
|
865 |
with assms have "{n. x ^ n dvd y} = {0}" by (auto simp: power_0_left) |
|
866 |
thus ?thesis by simp |
|
867 |
next |
|
868 |
case False |
|
869 |
note nz = this \<open>y \<noteq> 0\<close> |
|
870 |
from nz[THEN prime_factorization_exists'] guess A B . note AB = this |
|
871 |
from AB assms have "A \<noteq> {#}" by (auto simp: normalize_1_iff) |
|
63830 | 872 |
from AB(2,4) prod_mset_primes_finite_divisor_powers [of A B, OF AB(1,3) this] |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
873 |
have "finite {n. prod_mset A ^ n dvd prod_mset B}" by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
874 |
also have "{n. prod_mset A ^ n dvd prod_mset B} = |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
875 |
{n. normalize (normalize (prod_mset A) ^ n) dvd normalize (prod_mset B)}" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
876 |
unfolding normalize_power_normalize by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
877 |
also have "\<dots> = {n. x ^ n dvd y}" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
878 |
unfolding AB unfolding normalize_power_normalize by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
879 |
finally show ?thesis . |
63498 | 880 |
qed |
881 |
||
882 |
lemma finite_prime_divisors: |
|
883 |
assumes "x \<noteq> 0" |
|
63633 | 884 |
shows "finite {p. prime p \<and> p dvd x}" |
63498 | 885 |
proof - |
886 |
from prime_factorization_exists'[OF assms] guess A . note A = this |
|
63633 | 887 |
have "{p. prime p \<and> p dvd x} \<subseteq> set_mset A" |
63498 | 888 |
proof safe |
63633 | 889 |
fix p assume p: "prime p" and dvd: "p dvd x" |
63498 | 890 |
from dvd have "p dvd normalize x" by simp |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
891 |
also from A have "normalize x = normalize (prod_mset A)" by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
892 |
finally have "p dvd prod_mset A" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
893 |
by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
894 |
thus "p \<in># A" using p A |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
895 |
by (subst (asm) prime_dvd_prod_mset_primes_iff) |
63498 | 896 |
qed |
897 |
moreover have "finite (set_mset A)" by simp |
|
898 |
ultimately show ?thesis by (rule finite_subset) |
|
60804 | 899 |
qed |
900 |
||
63633 | 901 |
lemma prime_elem_iff_irreducible: "prime_elem x \<longleftrightarrow> irreducible x" |
902 |
by (blast intro: irreducible_imp_prime_elem prime_elem_imp_irreducible) |
|
62499 | 903 |
|
63498 | 904 |
lemma prime_divisor_exists: |
905 |
assumes "a \<noteq> 0" "\<not>is_unit a" |
|
63633 | 906 |
shows "\<exists>b. b dvd a \<and> prime b" |
63498 | 907 |
proof - |
908 |
from prime_factorization_exists'[OF assms(1)] guess A . note A = this |
|
909 |
moreover from A and assms have "A \<noteq> {#}" by auto |
|
910 |
then obtain x where "x \<in># A" by blast |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
911 |
with A(1) have *: "x dvd normalize (prod_mset A)" "prime x" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
912 |
by (auto simp: dvd_prod_mset) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
913 |
hence "x dvd a" unfolding A by simp |
63539 | 914 |
with * show ?thesis by blast |
63498 | 915 |
qed |
60804 | 916 |
|
63498 | 917 |
lemma prime_divisors_induct [case_names zero unit factor]: |
63633 | 918 |
assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)" |
63498 | 919 |
shows "P x" |
920 |
proof (cases "x = 0") |
|
921 |
case False |
|
922 |
from prime_factorization_exists'[OF this] guess A . note A = this |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
923 |
from A obtain u where u: "is_unit u" "x = u * prod_mset A" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
924 |
by (elim associatedE2) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
925 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
926 |
from A(1) have "P (u * prod_mset A)" |
63498 | 927 |
proof (induction A) |
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63633
diff
changeset
|
928 |
case (add p A) |
63633 | 929 |
from add.prems have "prime p" by simp |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
930 |
moreover from add.prems have "P (u * prod_mset A)" by (intro add.IH) simp_all |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
931 |
ultimately have "P (p * (u * prod_mset A))" by (rule assms(3)) |
63498 | 932 |
thus ?case by (simp add: mult_ac) |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
933 |
qed (simp_all add: assms False u) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
934 |
with A u show ?thesis by simp |
63498 | 935 |
qed (simp_all add: assms(1)) |
936 |
||
937 |
lemma no_prime_divisors_imp_unit: |
|
63633 | 938 |
assumes "a \<noteq> 0" "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> prime_elem b" |
63498 | 939 |
shows "is_unit a" |
940 |
proof (rule ccontr) |
|
941 |
assume "\<not>is_unit a" |
|
942 |
from prime_divisor_exists[OF assms(1) this] guess b by (elim exE conjE) |
|
63633 | 943 |
with assms(2)[of b] show False by (simp add: prime_def) |
60804 | 944 |
qed |
62499 | 945 |
|
63498 | 946 |
lemma prime_divisorE: |
947 |
assumes "a \<noteq> 0" and "\<not> is_unit a" |
|
63633 | 948 |
obtains p where "prime p" and "p dvd a" |
949 |
using assms no_prime_divisors_imp_unit unfolding prime_def by blast |
|
63498 | 950 |
|
951 |
definition multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where |
|
952 |
"multiplicity p x = (if finite {n. p ^ n dvd x} then Max {n. p ^ n dvd x} else 0)" |
|
953 |
||
954 |
lemma multiplicity_dvd: "p ^ multiplicity p x dvd x" |
|
955 |
proof (cases "finite {n. p ^ n dvd x}") |
|
956 |
case True |
|
957 |
hence "multiplicity p x = Max {n. p ^ n dvd x}" |
|
958 |
by (simp add: multiplicity_def) |
|
959 |
also have "\<dots> \<in> {n. p ^ n dvd x}" |
|
960 |
by (rule Max_in) (auto intro!: True exI[of _ "0::nat"]) |
|
961 |
finally show ?thesis by simp |
|
962 |
qed (simp add: multiplicity_def) |
|
963 |
||
964 |
lemma multiplicity_dvd': "n \<le> multiplicity p x \<Longrightarrow> p ^ n dvd x" |
|
965 |
by (rule dvd_trans[OF le_imp_power_dvd multiplicity_dvd]) |
|
966 |
||
967 |
context |
|
968 |
fixes x p :: 'a |
|
969 |
assumes xp: "x \<noteq> 0" "\<not>is_unit p" |
|
970 |
begin |
|
971 |
||
972 |
lemma multiplicity_eq_Max: "multiplicity p x = Max {n. p ^ n dvd x}" |
|
973 |
using finite_divisor_powers[OF xp] by (simp add: multiplicity_def) |
|
974 |
||
975 |
lemma multiplicity_geI: |
|
976 |
assumes "p ^ n dvd x" |
|
977 |
shows "multiplicity p x \<ge> n" |
|
978 |
proof - |
|
979 |
from assms have "n \<le> Max {n. p ^ n dvd x}" |
|
980 |
by (intro Max_ge finite_divisor_powers xp) simp_all |
|
981 |
thus ?thesis by (subst multiplicity_eq_Max) |
|
982 |
qed |
|
983 |
||
984 |
lemma multiplicity_lessI: |
|
985 |
assumes "\<not>p ^ n dvd x" |
|
986 |
shows "multiplicity p x < n" |
|
987 |
proof (rule ccontr) |
|
988 |
assume "\<not>(n > multiplicity p x)" |
|
989 |
hence "p ^ n dvd x" by (intro multiplicity_dvd') simp |
|
990 |
with assms show False by contradiction |
|
62499 | 991 |
qed |
992 |
||
63498 | 993 |
lemma power_dvd_iff_le_multiplicity: |
994 |
"p ^ n dvd x \<longleftrightarrow> n \<le> multiplicity p x" |
|
995 |
using multiplicity_geI[of n] multiplicity_lessI[of n] by (cases "p ^ n dvd x") auto |
|
996 |
||
997 |
lemma multiplicity_eq_zero_iff: |
|
998 |
shows "multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x" |
|
999 |
using power_dvd_iff_le_multiplicity[of 1] by auto |
|
1000 |
||
1001 |
lemma multiplicity_gt_zero_iff: |
|
1002 |
shows "multiplicity p x > 0 \<longleftrightarrow> p dvd x" |
|
1003 |
using power_dvd_iff_le_multiplicity[of 1] by auto |
|
1004 |
||
1005 |
lemma multiplicity_decompose: |
|
1006 |
"\<not>p dvd (x div p ^ multiplicity p x)" |
|
1007 |
proof |
|
1008 |
assume *: "p dvd x div p ^ multiplicity p x" |
|
1009 |
have "x = x div p ^ multiplicity p x * (p ^ multiplicity p x)" |
|
1010 |
using multiplicity_dvd[of p x] by simp |
|
1011 |
also from * have "x div p ^ multiplicity p x = (x div p ^ multiplicity p x div p) * p" by simp |
|
1012 |
also have "x div p ^ multiplicity p x div p * p * p ^ multiplicity p x = |
|
1013 |
x div p ^ multiplicity p x div p * p ^ Suc (multiplicity p x)" |
|
1014 |
by (simp add: mult_assoc) |
|
1015 |
also have "p ^ Suc (multiplicity p x) dvd \<dots>" by (rule dvd_triv_right) |
|
1016 |
finally show False by (subst (asm) power_dvd_iff_le_multiplicity) simp |
|
1017 |
qed |
|
1018 |
||
1019 |
lemma multiplicity_decompose': |
|
1020 |
obtains y where "x = p ^ multiplicity p x * y" "\<not>p dvd y" |
|
1021 |
using that[of "x div p ^ multiplicity p x"] |
|
1022 |
by (simp add: multiplicity_decompose multiplicity_dvd) |
|
1023 |
||
1024 |
end |
|
1025 |
||
1026 |
lemma multiplicity_zero [simp]: "multiplicity p 0 = 0" |
|
1027 |
by (simp add: multiplicity_def) |
|
1028 |
||
63633 | 1029 |
lemma prime_elem_multiplicity_eq_zero_iff: |
1030 |
"prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1031 |
by (rule multiplicity_eq_zero_iff) simp_all |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1032 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1033 |
lemma prime_multiplicity_other: |
63633 | 1034 |
assumes "prime p" "prime q" "p \<noteq> q" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1035 |
shows "multiplicity p q = 0" |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1036 |
using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1037 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1038 |
lemma prime_multiplicity_gt_zero_iff: |
63633 | 1039 |
"prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1040 |
by (rule multiplicity_gt_zero_iff) simp_all |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1041 |
|
63498 | 1042 |
lemma multiplicity_unit_left: "is_unit p \<Longrightarrow> multiplicity p x = 0" |
1043 |
by (simp add: multiplicity_def is_unit_power_iff unit_imp_dvd) |
|
62499 | 1044 |
|
63498 | 1045 |
lemma multiplicity_unit_right: |
1046 |
assumes "is_unit x" |
|
1047 |
shows "multiplicity p x = 0" |
|
1048 |
proof (cases "is_unit p \<or> x = 0") |
|
1049 |
case False |
|
1050 |
with multiplicity_lessI[of x p 1] this assms |
|
1051 |
show ?thesis by (auto dest: dvd_unit_imp_unit) |
|
1052 |
qed (auto simp: multiplicity_unit_left) |
|
1053 |
||
1054 |
lemma multiplicity_one [simp]: "multiplicity p 1 = 0" |
|
1055 |
by (rule multiplicity_unit_right) simp_all |
|
1056 |
||
1057 |
lemma multiplicity_eqI: |
|
1058 |
assumes "p ^ n dvd x" "\<not>p ^ Suc n dvd x" |
|
1059 |
shows "multiplicity p x = n" |
|
1060 |
proof - |
|
1061 |
consider "x = 0" | "is_unit p" | "x \<noteq> 0" "\<not>is_unit p" by blast |
|
1062 |
thus ?thesis |
|
1063 |
proof cases |
|
1064 |
assume xp: "x \<noteq> 0" "\<not>is_unit p" |
|
1065 |
from xp assms(1) have "multiplicity p x \<ge> n" by (intro multiplicity_geI) |
|
1066 |
moreover from assms(2) xp have "multiplicity p x < Suc n" by (intro multiplicity_lessI) |
|
1067 |
ultimately show ?thesis by simp |
|
1068 |
next |
|
1069 |
assume "is_unit p" |
|
1070 |
hence "is_unit (p ^ Suc n)" by (simp add: is_unit_power_iff del: power_Suc) |
|
1071 |
hence "p ^ Suc n dvd x" by (rule unit_imp_dvd) |
|
1072 |
with \<open>\<not>p ^ Suc n dvd x\<close> show ?thesis by contradiction |
|
1073 |
qed (insert assms, simp_all) |
|
1074 |
qed |
|
1075 |
||
1076 |
||
1077 |
context |
|
1078 |
fixes x p :: 'a |
|
1079 |
assumes xp: "x \<noteq> 0" "\<not>is_unit p" |
|
1080 |
begin |
|
1081 |
||
1082 |
lemma multiplicity_times_same: |
|
1083 |
assumes "p \<noteq> 0" |
|
1084 |
shows "multiplicity p (p * x) = Suc (multiplicity p x)" |
|
1085 |
proof (rule multiplicity_eqI) |
|
1086 |
show "p ^ Suc (multiplicity p x) dvd p * x" |
|
1087 |
by (auto intro!: mult_dvd_mono multiplicity_dvd) |
|
1088 |
from xp assms show "\<not> p ^ Suc (Suc (multiplicity p x)) dvd p * x" |
|
1089 |
using power_dvd_iff_le_multiplicity[OF xp, of "Suc (multiplicity p x)"] by simp |
|
62499 | 1090 |
qed |
1091 |
||
1092 |
end |
|
1093 |
||
63498 | 1094 |
lemma multiplicity_same_power': "multiplicity p (p ^ n) = (if p = 0 \<or> is_unit p then 0 else n)" |
1095 |
proof - |
|
1096 |
consider "p = 0" | "is_unit p" |"p \<noteq> 0" "\<not>is_unit p" by blast |
|
1097 |
thus ?thesis |
|
1098 |
proof cases |
|
1099 |
assume "p \<noteq> 0" "\<not>is_unit p" |
|
1100 |
thus ?thesis by (induction n) (simp_all add: multiplicity_times_same) |
|
1101 |
qed (simp_all add: power_0_left multiplicity_unit_left) |
|
1102 |
qed |
|
62499 | 1103 |
|
63498 | 1104 |
lemma multiplicity_same_power: |
1105 |
"p \<noteq> 0 \<Longrightarrow> \<not>is_unit p \<Longrightarrow> multiplicity p (p ^ n) = n" |
|
1106 |
by (simp add: multiplicity_same_power') |
|
1107 |
||
63633 | 1108 |
lemma multiplicity_prime_elem_times_other: |
1109 |
assumes "prime_elem p" "\<not>p dvd q" |
|
63498 | 1110 |
shows "multiplicity p (q * x) = multiplicity p x" |
1111 |
proof (cases "x = 0") |
|
1112 |
case False |
|
1113 |
show ?thesis |
|
1114 |
proof (rule multiplicity_eqI) |
|
1115 |
have "1 * p ^ multiplicity p x dvd q * x" |
|
1116 |
by (intro mult_dvd_mono multiplicity_dvd) simp_all |
|
1117 |
thus "p ^ multiplicity p x dvd q * x" by simp |
|
62499 | 1118 |
next |
63498 | 1119 |
define n where "n = multiplicity p x" |
1120 |
from assms have "\<not>is_unit p" by simp |
|
1121 |
from multiplicity_decompose'[OF False this] guess y . note y = this [folded n_def] |
|
1122 |
from y have "p ^ Suc n dvd q * x \<longleftrightarrow> p ^ n * p dvd p ^ n * (q * y)" by (simp add: mult_ac) |
|
1123 |
also from assms have "\<dots> \<longleftrightarrow> p dvd q * y" by simp |
|
63633 | 1124 |
also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_elem_dvd_mult_iff) fact+ |
63498 | 1125 |
also from assms y have "\<dots> \<longleftrightarrow> False" by simp |
1126 |
finally show "\<not>(p ^ Suc n dvd q * x)" by blast |
|
62499 | 1127 |
qed |
63498 | 1128 |
qed simp_all |
1129 |
||
63924 | 1130 |
lemma multiplicity_self: |
1131 |
assumes "p \<noteq> 0" "\<not>is_unit p" |
|
1132 |
shows "multiplicity p p = 1" |
|
1133 |
proof - |
|
1134 |
from assms have "multiplicity p p = Max {n. p ^ n dvd p}" |
|
1135 |
by (simp add: multiplicity_eq_Max) |
|
1136 |
also from assms have "p ^ n dvd p \<longleftrightarrow> n \<le> 1" for n |
|
1137 |
using dvd_power_iff[of p n 1] by auto |
|
1138 |
hence "{n. p ^ n dvd p} = {..1}" by auto |
|
1139 |
also have "\<dots> = {0,1}" by auto |
|
1140 |
finally show ?thesis by simp |
|
1141 |
qed |
|
1142 |
||
1143 |
lemma multiplicity_times_unit_left: |
|
1144 |
assumes "is_unit c" |
|
1145 |
shows "multiplicity (c * p) x = multiplicity p x" |
|
1146 |
proof - |
|
1147 |
from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}" |
|
1148 |
by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff) |
|
1149 |
thus ?thesis by (simp add: multiplicity_def) |
|
1150 |
qed |
|
1151 |
||
1152 |
lemma multiplicity_times_unit_right: |
|
1153 |
assumes "is_unit c" |
|
1154 |
shows "multiplicity p (c * x) = multiplicity p x" |
|
1155 |
proof - |
|
1156 |
from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}" |
|
1157 |
by (subst mult.commute) (simp add: dvd_mult_unit_iff) |
|
1158 |
thus ?thesis by (simp add: multiplicity_def) |
|
1159 |
qed |
|
1160 |
||
1161 |
lemma multiplicity_normalize_left [simp]: |
|
1162 |
"multiplicity (normalize p) x = multiplicity p x" |
|
1163 |
proof (cases "p = 0") |
|
1164 |
case [simp]: False |
|
1165 |
have "normalize p = (1 div unit_factor p) * p" |
|
1166 |
by (simp add: unit_div_commute is_unit_unit_factor) |
|
1167 |
also have "multiplicity \<dots> x = multiplicity p x" |
|
1168 |
by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor) |
|
1169 |
finally show ?thesis . |
|
1170 |
qed simp_all |
|
1171 |
||
1172 |
lemma multiplicity_normalize_right [simp]: |
|
1173 |
"multiplicity p (normalize x) = multiplicity p x" |
|
1174 |
proof (cases "x = 0") |
|
1175 |
case [simp]: False |
|
1176 |
have "normalize x = (1 div unit_factor x) * x" |
|
1177 |
by (simp add: unit_div_commute is_unit_unit_factor) |
|
1178 |
also have "multiplicity p \<dots> = multiplicity p x" |
|
1179 |
by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor) |
|
1180 |
finally show ?thesis . |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1181 |
qed simp_all |
63924 | 1182 |
|
1183 |
lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1" |
|
1184 |
by (rule multiplicity_self) auto |
|
1185 |
||
1186 |
lemma multiplicity_prime_power [simp]: "prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n" |
|
1187 |
by (subst multiplicity_same_power') auto |
|
1188 |
||
63498 | 1189 |
lift_definition prime_factorization :: "'a \<Rightarrow> 'a multiset" is |
63633 | 1190 |
"\<lambda>x p. if prime p then multiplicity p x else 0" |
63498 | 1191 |
unfolding multiset_def |
1192 |
proof clarify |
|
1193 |
fix x :: 'a |
|
63633 | 1194 |
show "finite {p. 0 < (if prime p then multiplicity p x else 0)}" (is "finite ?A") |
63498 | 1195 |
proof (cases "x = 0") |
1196 |
case False |
|
63633 | 1197 |
from False have "?A \<subseteq> {p. prime p \<and> p dvd x}" |
63498 | 1198 |
by (auto simp: multiplicity_gt_zero_iff) |
63633 | 1199 |
moreover from False have "finite {p. prime p \<and> p dvd x}" |
63498 | 1200 |
by (rule finite_prime_divisors) |
1201 |
ultimately show ?thesis by (rule finite_subset) |
|
1202 |
qed simp_all |
|
1203 |
qed |
|
1204 |
||
63905 | 1205 |
abbreviation prime_factors :: "'a \<Rightarrow> 'a set" where |
1206 |
"prime_factors a \<equiv> set_mset (prime_factorization a)" |
|
1207 |
||
63498 | 1208 |
lemma count_prime_factorization_nonprime: |
63633 | 1209 |
"\<not>prime p \<Longrightarrow> count (prime_factorization x) p = 0" |
63498 | 1210 |
by transfer simp |
1211 |
||
1212 |
lemma count_prime_factorization_prime: |
|
63633 | 1213 |
"prime p \<Longrightarrow> count (prime_factorization x) p = multiplicity p x" |
63498 | 1214 |
by transfer simp |
1215 |
||
1216 |
lemma count_prime_factorization: |
|
63633 | 1217 |
"count (prime_factorization x) p = (if prime p then multiplicity p x else 0)" |
63498 | 1218 |
by transfer simp |
1219 |
||
63924 | 1220 |
lemma dvd_imp_multiplicity_le: |
1221 |
assumes "a dvd b" "b \<noteq> 0" |
|
1222 |
shows "multiplicity p a \<le> multiplicity p b" |
|
1223 |
proof (cases "is_unit p") |
|
1224 |
case False |
|
1225 |
with assms show ?thesis |
|
1226 |
by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)]) |
|
1227 |
qed (insert assms, auto simp: multiplicity_unit_left) |
|
63498 | 1228 |
|
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1229 |
lemma prime_power_inj: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1230 |
assumes "prime a" "a ^ m = a ^ n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1231 |
shows "m = n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1232 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1233 |
have "multiplicity a (a ^ m) = multiplicity a (a ^ n)" by (simp only: assms) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1234 |
thus ?thesis using assms by (subst (asm) (1 2) multiplicity_prime_power) simp_all |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1235 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1236 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1237 |
lemma prime_power_inj': |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1238 |
assumes "prime p" "prime q" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1239 |
assumes "p ^ m = q ^ n" "m > 0" "n > 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1240 |
shows "p = q" "m = n" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1241 |
proof - |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1242 |
from assms have "p ^ 1 dvd p ^ m" by (intro le_imp_power_dvd) simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1243 |
also have "p ^ m = q ^ n" by fact |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1244 |
finally have "p dvd q ^ n" by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1245 |
with assms have "p dvd q" using prime_dvd_power[of p q] by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1246 |
with assms show "p = q" by (simp add: primes_dvd_imp_eq) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1247 |
with assms show "m = n" by (simp add: prime_power_inj) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1248 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1249 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1250 |
lemma prime_power_eq_one_iff [simp]: "prime p \<Longrightarrow> p ^ n = 1 \<longleftrightarrow> n = 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1251 |
using prime_power_inj[of p n 0] by auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1252 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1253 |
lemma one_eq_prime_power_iff [simp]: "prime p \<Longrightarrow> 1 = p ^ n \<longleftrightarrow> n = 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1254 |
using prime_power_inj[of p 0 n] by auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1255 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1256 |
lemma prime_power_inj'': |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1257 |
assumes "prime p" "prime q" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1258 |
shows "p ^ m = q ^ n \<longleftrightarrow> (m = 0 \<and> n = 0) \<or> (p = q \<and> m = n)" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1259 |
using assms |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1260 |
by (cases "m = 0"; cases "n = 0") |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1261 |
(auto dest: prime_power_inj'[OF assms]) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1262 |
|
63498 | 1263 |
lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}" |
1264 |
by (simp add: multiset_eq_iff count_prime_factorization) |
|
1265 |
||
1266 |
lemma prime_factorization_empty_iff: |
|
1267 |
"prime_factorization x = {#} \<longleftrightarrow> x = 0 \<or> is_unit x" |
|
1268 |
proof |
|
1269 |
assume *: "prime_factorization x = {#}" |
|
1270 |
{ |
|
1271 |
assume x: "x \<noteq> 0" "\<not>is_unit x" |
|
1272 |
{ |
|
63633 | 1273 |
fix p assume p: "prime p" |
63498 | 1274 |
have "count (prime_factorization x) p = 0" by (simp add: *) |
1275 |
also from p have "count (prime_factorization x) p = multiplicity p x" |
|
1276 |
by (rule count_prime_factorization_prime) |
|
1277 |
also from x p have "\<dots> = 0 \<longleftrightarrow> \<not>p dvd x" by (simp add: multiplicity_eq_zero_iff) |
|
1278 |
finally have "\<not>p dvd x" . |
|
1279 |
} |
|
1280 |
with prime_divisor_exists[OF x] have False by blast |
|
1281 |
} |
|
1282 |
thus "x = 0 \<or> is_unit x" by blast |
|
1283 |
next |
|
1284 |
assume "x = 0 \<or> is_unit x" |
|
1285 |
thus "prime_factorization x = {#}" |
|
1286 |
proof |
|
1287 |
assume x: "is_unit x" |
|
1288 |
{ |
|
63633 | 1289 |
fix p assume p: "prime p" |
63498 | 1290 |
from p x have "multiplicity p x = 0" |
1291 |
by (subst multiplicity_eq_zero_iff) |
|
1292 |
(auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors) |
|
1293 |
} |
|
1294 |
thus ?thesis by (simp add: multiset_eq_iff count_prime_factorization) |
|
1295 |
qed simp_all |
|
1296 |
qed |
|
1297 |
||
1298 |
lemma prime_factorization_unit: |
|
1299 |
assumes "is_unit x" |
|
1300 |
shows "prime_factorization x = {#}" |
|
1301 |
proof (rule multiset_eqI) |
|
1302 |
fix p :: 'a |
|
1303 |
show "count (prime_factorization x) p = count {#} p" |
|
63633 | 1304 |
proof (cases "prime p") |
63498 | 1305 |
case True |
1306 |
with assms have "multiplicity p x = 0" |
|
1307 |
by (subst multiplicity_eq_zero_iff) |
|
1308 |
(auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors) |
|
1309 |
with True show ?thesis by (simp add: count_prime_factorization_prime) |
|
1310 |
qed (simp_all add: count_prime_factorization_nonprime) |
|
1311 |
qed |
|
1312 |
||
1313 |
lemma prime_factorization_1 [simp]: "prime_factorization 1 = {#}" |
|
1314 |
by (simp add: prime_factorization_unit) |
|
1315 |
||
1316 |
lemma prime_factorization_times_prime: |
|
63633 | 1317 |
assumes "x \<noteq> 0" "prime p" |
63498 | 1318 |
shows "prime_factorization (p * x) = {#p#} + prime_factorization x" |
1319 |
proof (rule multiset_eqI) |
|
1320 |
fix q :: 'a |
|
63633 | 1321 |
consider "\<not>prime q" | "p = q" | "prime q" "p \<noteq> q" by blast |
63498 | 1322 |
thus "count (prime_factorization (p * x)) q = count ({#p#} + prime_factorization x) q" |
1323 |
proof cases |
|
63633 | 1324 |
assume q: "prime q" "p \<noteq> q" |
63498 | 1325 |
with assms primes_dvd_imp_eq[of q p] have "\<not>q dvd p" by auto |
1326 |
with q assms show ?thesis |
|
63633 | 1327 |
by (simp add: multiplicity_prime_elem_times_other count_prime_factorization) |
63498 | 1328 |
qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same) |
1329 |
qed |
|
1330 |
||
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1331 |
lemma prod_mset_prime_factorization_weak: |
63498 | 1332 |
assumes "x \<noteq> 0" |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1333 |
shows "normalize (prod_mset (prime_factorization x)) = normalize x" |
63498 | 1334 |
using assms |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1335 |
proof (induction x rule: prime_divisors_induct) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1336 |
case (factor p x) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1337 |
have "normalize (prod_mset (prime_factorization (p * x))) = |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1338 |
normalize (p * normalize (prod_mset (prime_factorization x)))" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1339 |
using factor.prems factor.hyps by (simp add: prime_factorization_times_prime) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1340 |
also have "normalize (prod_mset (prime_factorization x)) = normalize x" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1341 |
by (rule factor.IH) (use factor in auto) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1342 |
finally show ?case by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1343 |
qed (auto simp: prime_factorization_unit is_unit_normalize) |
63498 | 1344 |
|
63905 | 1345 |
lemma in_prime_factors_iff: |
1346 |
"p \<in> prime_factors x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p" |
|
63498 | 1347 |
proof - |
63905 | 1348 |
have "p \<in> prime_factors x \<longleftrightarrow> count (prime_factorization x) p > 0" by simp |
63633 | 1349 |
also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p" |
63498 | 1350 |
by (subst count_prime_factorization, cases "x = 0") |
1351 |
(auto simp: multiplicity_eq_zero_iff multiplicity_gt_zero_iff) |
|
1352 |
finally show ?thesis . |
|
1353 |
qed |
|
1354 |
||
63905 | 1355 |
lemma in_prime_factors_imp_prime [intro]: |
1356 |
"p \<in> prime_factors x \<Longrightarrow> prime p" |
|
1357 |
by (simp add: in_prime_factors_iff) |
|
63498 | 1358 |
|
63905 | 1359 |
lemma in_prime_factors_imp_dvd [dest]: |
1360 |
"p \<in> prime_factors x \<Longrightarrow> p dvd x" |
|
1361 |
by (simp add: in_prime_factors_iff) |
|
63498 | 1362 |
|
63924 | 1363 |
lemma prime_factorsI: |
1364 |
"x \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x" |
|
1365 |
by (auto simp: in_prime_factors_iff) |
|
1366 |
||
1367 |
lemma prime_factors_dvd: |
|
1368 |
"x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. prime p \<and> p dvd x}" |
|
1369 |
by (auto intro: prime_factorsI) |
|
1370 |
||
1371 |
lemma prime_factors_multiplicity: |
|
1372 |
"prime_factors n = {p. prime p \<and> multiplicity p n > 0}" |
|
1373 |
by (cases "n = 0") (auto simp add: prime_factors_dvd prime_multiplicity_gt_zero_iff) |
|
63498 | 1374 |
|
1375 |
lemma prime_factorization_prime: |
|
63633 | 1376 |
assumes "prime p" |
63498 | 1377 |
shows "prime_factorization p = {#p#}" |
1378 |
proof (rule multiset_eqI) |
|
1379 |
fix q :: 'a |
|
63633 | 1380 |
consider "\<not>prime q" | "q = p" | "prime q" "q \<noteq> p" by blast |
63498 | 1381 |
thus "count (prime_factorization p) q = count {#p#} q" |
1382 |
by cases (insert assms, auto dest: primes_dvd_imp_eq |
|
1383 |
simp: count_prime_factorization multiplicity_self multiplicity_eq_zero_iff) |
|
1384 |
qed |
|
1385 |
||
63830 | 1386 |
lemma prime_factorization_prod_mset_primes: |
63633 | 1387 |
assumes "\<And>p. p \<in># A \<Longrightarrow> prime p" |
63830 | 1388 |
shows "prime_factorization (prod_mset A) = A" |
63498 | 1389 |
using assms |
1390 |
proof (induction A) |
|
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63633
diff
changeset
|
1391 |
case (add p A) |
63498 | 1392 |
from add.prems[of 0] have "0 \<notin># A" by auto |
63830 | 1393 |
hence "prod_mset A \<noteq> 0" by auto |
63498 | 1394 |
with add show ?case |
1395 |
by (simp_all add: mult_ac prime_factorization_times_prime Multiset.union_commute) |
|
1396 |
qed simp_all |
|
1397 |
||
1398 |
lemma prime_factorization_cong: |
|
1399 |
"normalize x = normalize y \<Longrightarrow> prime_factorization x = prime_factorization y" |
|
1400 |
by (simp add: multiset_eq_iff count_prime_factorization |
|
1401 |
multiplicity_normalize_right [of _ x, symmetric] |
|
1402 |
multiplicity_normalize_right [of _ y, symmetric] |
|
1403 |
del: multiplicity_normalize_right) |
|
1404 |
||
1405 |
lemma prime_factorization_unique: |
|
1406 |
assumes "x \<noteq> 0" "y \<noteq> 0" |
|
1407 |
shows "prime_factorization x = prime_factorization y \<longleftrightarrow> normalize x = normalize y" |
|
1408 |
proof |
|
1409 |
assume "prime_factorization x = prime_factorization y" |
|
63830 | 1410 |
hence "prod_mset (prime_factorization x) = prod_mset (prime_factorization y)" by simp |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1411 |
hence "normalize (prod_mset (prime_factorization x)) = |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1412 |
normalize (prod_mset (prime_factorization y))" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1413 |
by (simp only: ) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1414 |
with assms show "normalize x = normalize y" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1415 |
by (simp add: prod_mset_prime_factorization_weak) |
63498 | 1416 |
qed (rule prime_factorization_cong) |
1417 |
||
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1418 |
lemma prime_factorization_normalize [simp]: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1419 |
"prime_factorization (normalize x) = prime_factorization x" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1420 |
by (cases "x = 0", simp, subst prime_factorization_unique) auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1421 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1422 |
lemma prime_factorization_eqI_strong: |
69785
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1423 |
assumes "\<And>p. p \<in># P \<Longrightarrow> prime p" "prod_mset P = n" |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1424 |
shows "prime_factorization n = P" |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1425 |
using prime_factorization_prod_mset_primes[of P] assms by simp |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1426 |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1427 |
lemma prime_factorization_eqI: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1428 |
assumes "\<And>p. p \<in># P \<Longrightarrow> prime p" "normalize (prod_mset P) = normalize n" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1429 |
shows "prime_factorization n = P" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1430 |
proof - |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1431 |
have "P = prime_factorization (normalize (prod_mset P))" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1432 |
using prime_factorization_prod_mset_primes[of P] assms(1) by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1433 |
with assms(2) show ?thesis by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1434 |
qed |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1435 |
|
63498 | 1436 |
lemma prime_factorization_mult: |
1437 |
assumes "x \<noteq> 0" "y \<noteq> 0" |
|
1438 |
shows "prime_factorization (x * y) = prime_factorization x + prime_factorization y" |
|
1439 |
proof - |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1440 |
have "normalize (prod_mset (prime_factorization x) * prod_mset (prime_factorization y)) = |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1441 |
normalize (normalize (prod_mset (prime_factorization x)) * |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1442 |
normalize (prod_mset (prime_factorization y)))" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1443 |
by (simp only: normalize_mult_normalize_left normalize_mult_normalize_right) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1444 |
also have "\<dots> = normalize (x * y)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1445 |
by (subst (1 2) prod_mset_prime_factorization_weak) (use assms in auto) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1446 |
finally show ?thesis |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1447 |
by (intro prime_factorization_eqI) auto |
62499 | 1448 |
qed |
1449 |
||
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1450 |
lemma prime_factorization_prod: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1451 |
assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1452 |
shows "prime_factorization (prod f A) = (\<Sum>n\<in>A. prime_factorization (f n))" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1453 |
using assms by (induction A rule: finite_induct) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1454 |
(auto simp: Sup_multiset_empty prime_factorization_mult) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1455 |
|
63924 | 1456 |
lemma prime_elem_multiplicity_mult_distrib: |
1457 |
assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0" |
|
1458 |
shows "multiplicity p (x * y) = multiplicity p x + multiplicity p y" |
|
1459 |
proof - |
|
1460 |
have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)" |
|
1461 |
by (subst count_prime_factorization_prime) (simp_all add: assms) |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1462 |
also from assms |
63924 | 1463 |
have "prime_factorization (x * y) = prime_factorization x + prime_factorization y" |
1464 |
by (intro prime_factorization_mult) |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1465 |
also have "count \<dots> (normalize p) = |
63924 | 1466 |
count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)" |
1467 |
by simp |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1468 |
also have "\<dots> = multiplicity p x + multiplicity p y" |
63924 | 1469 |
by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms) |
1470 |
finally show ?thesis . |
|
1471 |
qed |
|
1472 |
||
1473 |
lemma prime_elem_multiplicity_prod_mset_distrib: |
|
1474 |
assumes "prime_elem p" "0 \<notin># A" |
|
1475 |
shows "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)" |
|
1476 |
using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib) |
|
1477 |
||
1478 |
lemma prime_elem_multiplicity_power_distrib: |
|
1479 |
assumes "prime_elem p" "x \<noteq> 0" |
|
1480 |
shows "multiplicity p (x ^ n) = n * multiplicity p x" |
|
1481 |
using assms prime_elem_multiplicity_prod_mset_distrib [of p "replicate_mset n x"] |
|
1482 |
by simp |
|
1483 |
||
64272 | 1484 |
lemma prime_elem_multiplicity_prod_distrib: |
63924 | 1485 |
assumes "prime_elem p" "0 \<notin> f ` A" "finite A" |
64272 | 1486 |
shows "multiplicity p (prod f A) = (\<Sum>x\<in>A. multiplicity p (f x))" |
63924 | 1487 |
proof - |
64272 | 1488 |
have "multiplicity p (prod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))" |
1489 |
using assms by (subst prod_unfold_prod_mset) |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1490 |
(simp_all add: prime_elem_multiplicity_prod_mset_distrib sum_unfold_sum_mset |
63924 | 1491 |
multiset.map_comp o_def) |
1492 |
also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))" |
|
1493 |
by (induction A rule: finite_induct) simp_all |
|
1494 |
finally show ?thesis . |
|
1495 |
qed |
|
1496 |
||
1497 |
lemma multiplicity_distinct_prime_power: |
|
1498 |
"prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0" |
|
1499 |
by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other) |
|
1500 |
||
63498 | 1501 |
lemma prime_factorization_prime_power: |
63633 | 1502 |
"prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p" |
63498 | 1503 |
by (induction n) |
1504 |
(simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute) |
|
1505 |
||
1506 |
lemma prime_factorization_subset_iff_dvd: |
|
1507 |
assumes [simp]: "x \<noteq> 0" "y \<noteq> 0" |
|
1508 |
shows "prime_factorization x \<subseteq># prime_factorization y \<longleftrightarrow> x dvd y" |
|
1509 |
proof - |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1510 |
have "x dvd y \<longleftrightarrow> |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1511 |
normalize (prod_mset (prime_factorization x)) dvd normalize (prod_mset (prime_factorization y))" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1512 |
using assms by (subst (1 2) prod_mset_prime_factorization_weak) auto |
63498 | 1513 |
also have "\<dots> \<longleftrightarrow> prime_factorization x \<subseteq># prime_factorization y" |
63905 | 1514 |
by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd) |
63498 | 1515 |
finally show ?thesis .. |
1516 |
qed |
|
1517 |
||
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1518 |
lemma prime_factorization_subset_imp_dvd: |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1519 |
"x \<noteq> 0 \<Longrightarrow> (prime_factorization x \<subseteq># prime_factorization y) \<Longrightarrow> x dvd y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1520 |
by (cases "y = 0") (simp_all add: prime_factorization_subset_iff_dvd) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1521 |
|
63498 | 1522 |
lemma prime_factorization_divide: |
1523 |
assumes "b dvd a" |
|
1524 |
shows "prime_factorization (a div b) = prime_factorization a - prime_factorization b" |
|
1525 |
proof (cases "a = 0") |
|
1526 |
case [simp]: False |
|
1527 |
from assms have [simp]: "b \<noteq> 0" by auto |
|
1528 |
have "prime_factorization ((a div b) * b) = prime_factorization (a div b) + prime_factorization b" |
|
1529 |
by (intro prime_factorization_mult) (insert assms, auto elim!: dvdE) |
|
1530 |
with assms show ?thesis by simp |
|
1531 |
qed simp_all |
|
1532 |
||
63905 | 1533 |
lemma zero_not_in_prime_factors [simp]: "0 \<notin> prime_factors x" |
1534 |
by (auto dest: in_prime_factors_imp_prime) |
|
63498 | 1535 |
|
63904 | 1536 |
lemma prime_prime_factors: |
63905 | 1537 |
"prime p \<Longrightarrow> prime_factors p = {p}" |
1538 |
by (drule prime_factorization_prime) simp |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1539 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1540 |
lemma prime_factors_product: |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1541 |
"x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y" |
63905 | 1542 |
by (simp add: prime_factorization_mult) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1543 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1544 |
lemma dvd_prime_factors [intro]: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1545 |
"y \<noteq> 0 \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<subseteq> prime_factors y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1546 |
by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1547 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1548 |
(* RENAMED multiplicity_dvd *) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1549 |
lemma multiplicity_le_imp_dvd: |
63633 | 1550 |
assumes "x \<noteq> 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1551 |
shows "x dvd y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1552 |
proof (cases "y = 0") |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1553 |
case False |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1554 |
from assms this have "prime_factorization x \<subseteq># prime_factorization y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1555 |
by (intro mset_subset_eqI) (auto simp: count_prime_factorization) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1556 |
with assms False show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1557 |
qed auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1558 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1559 |
lemma dvd_multiplicity_eq: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1560 |
"x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1561 |
by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1562 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1563 |
lemma multiplicity_eq_imp_eq: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1564 |
assumes "x \<noteq> 0" "y \<noteq> 0" |
63633 | 1565 |
assumes "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1566 |
shows "normalize x = normalize y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1567 |
using assms by (intro associatedI multiplicity_le_imp_dvd) simp_all |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1568 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1569 |
lemma prime_factorization_unique': |
63633 | 1570 |
assumes "\<forall>p \<in># M. prime p" "\<forall>p \<in># N. prime p" "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1571 |
shows "M = N" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1572 |
proof - |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1573 |
have "prime_factorization (\<Prod>i \<in># M. i) = prime_factorization (\<Prod>i \<in># N. i)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1574 |
by (simp only: assms) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1575 |
also from assms have "prime_factorization (\<Prod>i \<in># M. i) = M" |
63830 | 1576 |
by (subst prime_factorization_prod_mset_primes) simp_all |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1577 |
also from assms have "prime_factorization (\<Prod>i \<in># N. i) = N" |
63830 | 1578 |
by (subst prime_factorization_prod_mset_primes) simp_all |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1579 |
finally show ?thesis . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1580 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1581 |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1582 |
lemma prime_factorization_unique'': |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1583 |
assumes "\<forall>p \<in># M. prime p" "\<forall>p \<in># N. prime p" "normalize (\<Prod>i \<in># M. i) = normalize (\<Prod>i \<in># N. i)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1584 |
shows "M = N" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1585 |
proof - |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1586 |
have "prime_factorization (normalize (\<Prod>i \<in># M. i)) = |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1587 |
prime_factorization (normalize (\<Prod>i \<in># N. i))" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1588 |
by (simp only: assms) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1589 |
also from assms have "prime_factorization (normalize (\<Prod>i \<in># M. i)) = M" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1590 |
by (subst prime_factorization_normalize, subst prime_factorization_prod_mset_primes) simp_all |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1591 |
also from assms have "prime_factorization (normalize (\<Prod>i \<in># N. i)) = N" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1592 |
by (subst prime_factorization_normalize, subst prime_factorization_prod_mset_primes) simp_all |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1593 |
finally show ?thesis . |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1594 |
qed |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1595 |
|
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1596 |
lemma multiplicity_cong: |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1597 |
"(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> multiplicity p a = multiplicity p b" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1598 |
by (simp add: multiplicity_def) |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1599 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1600 |
lemma not_dvd_imp_multiplicity_0: |
63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1601 |
assumes "\<not>p dvd x" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1602 |
shows "multiplicity p x = 0" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1603 |
proof - |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1604 |
from assms have "multiplicity p x < 1" |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1605 |
by (intro multiplicity_lessI) auto |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1606 |
thus ?thesis by simp |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1607 |
qed |
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset
|
1608 |
|
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1609 |
lemma inj_on_Prod_primes: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1610 |
assumes "\<And>P p. P \<in> A \<Longrightarrow> p \<in> P \<Longrightarrow> prime p" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1611 |
assumes "\<And>P. P \<in> A \<Longrightarrow> finite P" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1612 |
shows "inj_on Prod A" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1613 |
proof (rule inj_onI) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1614 |
fix P Q assume PQ: "P \<in> A" "Q \<in> A" "\<Prod>P = \<Prod>Q" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1615 |
with prime_factorization_unique'[of "mset_set P" "mset_set Q"] assms[of P] assms[of Q] |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1616 |
have "mset_set P = mset_set Q" by (auto simp: prod_unfold_prod_mset) |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1617 |
with assms[of P] assms[of Q] PQ show "P = Q" by simp |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1618 |
qed |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1619 |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1620 |
lemma divides_primepow_weak: |
67051 | 1621 |
assumes "prime p" and "a dvd p ^ n" |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1622 |
obtains m where "m \<le> n" and "normalize a = normalize (p ^ m)" |
67051 | 1623 |
proof - |
1624 |
from assms have "a \<noteq> 0" |
|
1625 |
by auto |
|
1626 |
with assms |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1627 |
have "normalize (prod_mset (prime_factorization a)) dvd |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1628 |
normalize (prod_mset (prime_factorization (p ^ n)))" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1629 |
by (subst (1 2) prod_mset_prime_factorization_weak) auto |
67051 | 1630 |
then have "prime_factorization a \<subseteq># prime_factorization (p ^ n)" |
1631 |
by (simp add: in_prime_factors_imp_prime prod_mset_dvd_prod_mset_primes_iff) |
|
1632 |
with assms have "prime_factorization a \<subseteq># replicate_mset n p" |
|
1633 |
by (simp add: prime_factorization_prime_power) |
|
1634 |
then obtain m where "m \<le> n" and "prime_factorization a = replicate_mset m p" |
|
1635 |
by (rule msubseteq_replicate_msetE) |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1636 |
then have *: "normalize (prod_mset (prime_factorization a)) = |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1637 |
normalize (prod_mset (replicate_mset m p))" by metis |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1638 |
also have "normalize (prod_mset (prime_factorization a)) = normalize a" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1639 |
using \<open>a \<noteq> 0\<close> by (simp add: prod_mset_prime_factorization_weak) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1640 |
also have "prod_mset (replicate_mset m p) = p ^ m" |
67051 | 1641 |
by simp |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1642 |
finally show ?thesis using \<open>m \<le> n\<close> |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1643 |
by (intro that[of m]) |
67051 | 1644 |
qed |
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1645 |
|
69785
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1646 |
lemma divide_out_primepow_ex: |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1647 |
assumes "n \<noteq> 0" "\<exists>p\<in>prime_factors n. P p" |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1648 |
obtains p k n' where "P p" "prime p" "p dvd n" "\<not>p dvd n'" "k > 0" "n = p ^ k * n'" |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1649 |
proof - |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1650 |
from assms obtain p where p: "P p" "prime p" "p dvd n" |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1651 |
by auto |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1652 |
define k where "k = multiplicity p n" |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1653 |
define n' where "n' = n div p ^ k" |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1654 |
have n': "n = p ^ k * n'" "\<not>p dvd n'" |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1655 |
using assms p multiplicity_decompose[of n p] |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1656 |
by (auto simp: n'_def k_def multiplicity_dvd) |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1657 |
from n' p have "k > 0" by (intro Nat.gr0I) auto |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1658 |
with n' p that[of p n' k] show ?thesis by auto |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1659 |
qed |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1660 |
|
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1661 |
lemma divide_out_primepow: |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1662 |
assumes "n \<noteq> 0" "\<not>is_unit n" |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1663 |
obtains p k n' where "prime p" "p dvd n" "\<not>p dvd n'" "k > 0" "n = p ^ k * n'" |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1664 |
using divide_out_primepow_ex[OF assms(1), of "\<lambda>_. True"] prime_divisor_exists[OF assms] assms |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1665 |
prime_factorsI by metis |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
68606
diff
changeset
|
1666 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1667 |
|
63924 | 1668 |
subsection \<open>GCD and LCM computation with unique factorizations\<close> |
1669 |
||
63498 | 1670 |
definition "gcd_factorial a b = (if a = 0 then normalize b |
1671 |
else if b = 0 then normalize a |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1672 |
else normalize (prod_mset (prime_factorization a \<inter># prime_factorization b)))" |
63498 | 1673 |
|
1674 |
definition "lcm_factorial a b = (if a = 0 \<or> b = 0 then 0 |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1675 |
else normalize (prod_mset (prime_factorization a \<union># prime_factorization b)))" |
63498 | 1676 |
|
1677 |
definition "Gcd_factorial A = |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1678 |
(if A \<subseteq> {0} then 0 else normalize (prod_mset (Inf (prime_factorization ` (A - {0})))))" |
63498 | 1679 |
|
1680 |
definition "Lcm_factorial A = |
|
1681 |
(if A = {} then 1 |
|
1682 |
else if 0 \<notin> A \<and> subset_mset.bdd_above (prime_factorization ` (A - {0})) then |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1683 |
normalize (prod_mset (Sup (prime_factorization ` A))) |
63498 | 1684 |
else |
1685 |
0)" |
|
1686 |
||
1687 |
lemma prime_factorization_gcd_factorial: |
|
1688 |
assumes [simp]: "a \<noteq> 0" "b \<noteq> 0" |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1689 |
shows "prime_factorization (gcd_factorial a b) = prime_factorization a \<inter># prime_factorization b" |
63498 | 1690 |
proof - |
1691 |
have "prime_factorization (gcd_factorial a b) = |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1692 |
prime_factorization (prod_mset (prime_factorization a \<inter># prime_factorization b))" |
63498 | 1693 |
by (simp add: gcd_factorial_def) |
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1694 |
also have "\<dots> = prime_factorization a \<inter># prime_factorization b" |
63905 | 1695 |
by (subst prime_factorization_prod_mset_primes) auto |
63498 | 1696 |
finally show ?thesis . |
1697 |
qed |
|
1698 |
||
1699 |
lemma prime_factorization_lcm_factorial: |
|
1700 |
assumes [simp]: "a \<noteq> 0" "b \<noteq> 0" |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1701 |
shows "prime_factorization (lcm_factorial a b) = prime_factorization a \<union># prime_factorization b" |
63498 | 1702 |
proof - |
1703 |
have "prime_factorization (lcm_factorial a b) = |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1704 |
prime_factorization (prod_mset (prime_factorization a \<union># prime_factorization b))" |
63498 | 1705 |
by (simp add: lcm_factorial_def) |
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1706 |
also have "\<dots> = prime_factorization a \<union># prime_factorization b" |
63905 | 1707 |
by (subst prime_factorization_prod_mset_primes) auto |
63498 | 1708 |
finally show ?thesis . |
1709 |
qed |
|
1710 |
||
1711 |
lemma prime_factorization_Gcd_factorial: |
|
1712 |
assumes "\<not>A \<subseteq> {0}" |
|
1713 |
shows "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))" |
|
1714 |
proof - |
|
1715 |
from assms obtain x where x: "x \<in> A - {0}" by auto |
|
1716 |
hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x" |
|
1717 |
by (intro subset_mset.cInf_lower) simp_all |
|
63905 | 1718 |
hence "\<forall>y. y \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> y \<in> prime_factors x" |
63498 | 1719 |
by (auto dest: mset_subset_eqD) |
63905 | 1720 |
with in_prime_factors_imp_prime[of _ x] |
63633 | 1721 |
have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> prime p" by blast |
63498 | 1722 |
with assms show ?thesis |
63830 | 1723 |
by (simp add: Gcd_factorial_def prime_factorization_prod_mset_primes) |
63498 | 1724 |
qed |
1725 |
||
1726 |
lemma prime_factorization_Lcm_factorial: |
|
1727 |
assumes "0 \<notin> A" "subset_mset.bdd_above (prime_factorization ` A)" |
|
1728 |
shows "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)" |
|
1729 |
proof (cases "A = {}") |
|
1730 |
case True |
|
1731 |
hence "prime_factorization ` A = {}" by auto |
|
1732 |
also have "Sup \<dots> = {#}" by (simp add: Sup_multiset_empty) |
|
1733 |
finally show ?thesis by (simp add: Lcm_factorial_def) |
|
1734 |
next |
|
1735 |
case False |
|
63633 | 1736 |
have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> prime y" |
63905 | 1737 |
by (auto simp: in_Sup_multiset_iff assms) |
63498 | 1738 |
with assms False show ?thesis |
63830 | 1739 |
by (simp add: Lcm_factorial_def prime_factorization_prod_mset_primes) |
63498 | 1740 |
qed |
1741 |
||
1742 |
lemma gcd_factorial_commute: "gcd_factorial a b = gcd_factorial b a" |
|
1743 |
by (simp add: gcd_factorial_def multiset_inter_commute) |
|
1744 |
||
1745 |
lemma gcd_factorial_dvd1: "gcd_factorial a b dvd a" |
|
1746 |
proof (cases "a = 0 \<or> b = 0") |
|
1747 |
case False |
|
1748 |
hence "gcd_factorial a b \<noteq> 0" by (auto simp: gcd_factorial_def) |
|
1749 |
with False show ?thesis |
|
1750 |
by (subst prime_factorization_subset_iff_dvd [symmetric]) |
|
1751 |
(auto simp: prime_factorization_gcd_factorial) |
|
1752 |
qed (auto simp: gcd_factorial_def) |
|
1753 |
||
1754 |
lemma gcd_factorial_dvd2: "gcd_factorial a b dvd b" |
|
1755 |
by (subst gcd_factorial_commute) (rule gcd_factorial_dvd1) |
|
1756 |
||
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1757 |
lemma normalize_gcd_factorial [simp]: "normalize (gcd_factorial a b) = gcd_factorial a b" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1758 |
by (simp add: gcd_factorial_def) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1759 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1760 |
lemma normalize_lcm_factorial [simp]: "normalize (lcm_factorial a b) = lcm_factorial a b" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1761 |
by (simp add: lcm_factorial_def) |
63498 | 1762 |
|
1763 |
lemma gcd_factorial_greatest: "c dvd gcd_factorial a b" if "c dvd a" "c dvd b" for a b c |
|
1764 |
proof (cases "a = 0 \<or> b = 0") |
|
1765 |
case False |
|
1766 |
with that have [simp]: "c \<noteq> 0" by auto |
|
1767 |
let ?p = "prime_factorization" |
|
1768 |
from that False have "?p c \<subseteq># ?p a" "?p c \<subseteq># ?p b" |
|
1769 |
by (simp_all add: prime_factorization_subset_iff_dvd) |
|
1770 |
hence "prime_factorization c \<subseteq># |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1771 |
prime_factorization (prod_mset (prime_factorization a \<inter># prime_factorization b))" |
63905 | 1772 |
using False by (subst prime_factorization_prod_mset_primes) auto |
63498 | 1773 |
with False show ?thesis |
1774 |
by (auto simp: gcd_factorial_def prime_factorization_subset_iff_dvd [symmetric]) |
|
1775 |
qed (auto simp: gcd_factorial_def that) |
|
1776 |
||
1777 |
lemma lcm_factorial_gcd_factorial: |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1778 |
"lcm_factorial a b = normalize (a * b div gcd_factorial a b)" for a b |
63498 | 1779 |
proof (cases "a = 0 \<or> b = 0") |
1780 |
case False |
|
1781 |
let ?p = "prime_factorization" |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1782 |
have 1: "normalize x * normalize y dvd z \<longleftrightarrow> x * y dvd z" for x y z :: 'a |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1783 |
proof - |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1784 |
have "normalize (normalize x * normalize y) dvd z \<longleftrightarrow> x * y dvd z" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1785 |
unfolding normalize_mult_normalize_left normalize_mult_normalize_right by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1786 |
thus ?thesis unfolding normalize_dvd_iff by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1787 |
qed |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1788 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1789 |
have "?p (a * b) = (?p a \<union># ?p b) + (?p a \<inter># ?p b)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1790 |
using False by (subst prime_factorization_mult) (auto intro!: multiset_eqI) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1791 |
hence "normalize (prod_mset (?p (a * b))) = |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1792 |
normalize (prod_mset ((?p a \<union># ?p b) + (?p a \<inter># ?p b)))" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1793 |
by (simp only:) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1794 |
hence *: "normalize (a * b) = normalize (lcm_factorial a b * gcd_factorial a b)" using False |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1795 |
by (subst (asm) prod_mset_prime_factorization_weak) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1796 |
(auto simp: lcm_factorial_def gcd_factorial_def) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1797 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1798 |
have [simp]: "gcd_factorial a b dvd a * b" "lcm_factorial a b dvd a * b" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1799 |
using associatedD2[OF *] by auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1800 |
from False have [simp]: "gcd_factorial a b \<noteq> 0" "lcm_factorial a b \<noteq> 0" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1801 |
by (auto simp: gcd_factorial_def lcm_factorial_def) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1802 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1803 |
show ?thesis |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1804 |
by (rule associated_eqI) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1805 |
(use * in \<open>auto simp: dvd_div_iff_mult div_dvd_iff_mult dest: associatedD1 associatedD2\<close>) |
63498 | 1806 |
qed (auto simp: lcm_factorial_def) |
1807 |
||
1808 |
lemma normalize_Gcd_factorial: |
|
1809 |
"normalize (Gcd_factorial A) = Gcd_factorial A" |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1810 |
by (simp add: Gcd_factorial_def) |
63498 | 1811 |
|
1812 |
lemma Gcd_factorial_eq_0_iff: |
|
1813 |
"Gcd_factorial A = 0 \<longleftrightarrow> A \<subseteq> {0}" |
|
1814 |
by (auto simp: Gcd_factorial_def in_Inf_multiset_iff split: if_splits) |
|
1815 |
||
1816 |
lemma Gcd_factorial_dvd: |
|
1817 |
assumes "x \<in> A" |
|
1818 |
shows "Gcd_factorial A dvd x" |
|
1819 |
proof (cases "x = 0") |
|
1820 |
case False |
|
1821 |
with assms have "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))" |
|
1822 |
by (intro prime_factorization_Gcd_factorial) auto |
|
1823 |
also from False assms have "\<dots> \<subseteq># prime_factorization x" |
|
1824 |
by (intro subset_mset.cInf_lower) auto |
|
1825 |
finally show ?thesis |
|
1826 |
by (subst (asm) prime_factorization_subset_iff_dvd) |
|
1827 |
(insert assms False, auto simp: Gcd_factorial_eq_0_iff) |
|
1828 |
qed simp_all |
|
1829 |
||
1830 |
lemma Gcd_factorial_greatest: |
|
1831 |
assumes "\<And>y. y \<in> A \<Longrightarrow> x dvd y" |
|
1832 |
shows "x dvd Gcd_factorial A" |
|
1833 |
proof (cases "A \<subseteq> {0}") |
|
1834 |
case False |
|
1835 |
from False obtain y where "y \<in> A" "y \<noteq> 0" by auto |
|
1836 |
with assms[of y] have nz: "x \<noteq> 0" by auto |
|
1837 |
from nz assms have "prime_factorization x \<subseteq># prime_factorization y" if "y \<in> A - {0}" for y |
|
1838 |
using that by (subst prime_factorization_subset_iff_dvd) auto |
|
1839 |
with False have "prime_factorization x \<subseteq># Inf (prime_factorization ` (A - {0}))" |
|
1840 |
by (intro subset_mset.cInf_greatest) auto |
|
1841 |
also from False have "\<dots> = prime_factorization (Gcd_factorial A)" |
|
1842 |
by (rule prime_factorization_Gcd_factorial [symmetric]) |
|
1843 |
finally show ?thesis |
|
1844 |
by (subst (asm) prime_factorization_subset_iff_dvd) |
|
1845 |
(insert nz False, auto simp: Gcd_factorial_eq_0_iff) |
|
1846 |
qed (simp_all add: Gcd_factorial_def) |
|
1847 |
||
1848 |
lemma normalize_Lcm_factorial: |
|
1849 |
"normalize (Lcm_factorial A) = Lcm_factorial A" |
|
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1850 |
by (simp add: Lcm_factorial_def) |
63498 | 1851 |
|
1852 |
lemma Lcm_factorial_eq_0_iff: |
|
1853 |
"Lcm_factorial A = 0 \<longleftrightarrow> 0 \<in> A \<or> \<not>subset_mset.bdd_above (prime_factorization ` A)" |
|
1854 |
by (auto simp: Lcm_factorial_def in_Sup_multiset_iff) |
|
1855 |
||
1856 |
lemma dvd_Lcm_factorial: |
|
1857 |
assumes "x \<in> A" |
|
1858 |
shows "x dvd Lcm_factorial A" |
|
1859 |
proof (cases "0 \<notin> A \<and> subset_mset.bdd_above (prime_factorization ` A)") |
|
1860 |
case True |
|
1861 |
with assms have [simp]: "0 \<notin> A" "x \<noteq> 0" "A \<noteq> {}" by auto |
|
1862 |
from assms True have "prime_factorization x \<subseteq># Sup (prime_factorization ` A)" |
|
1863 |
by (intro subset_mset.cSup_upper) auto |
|
1864 |
also have "\<dots> = prime_factorization (Lcm_factorial A)" |
|
1865 |
by (rule prime_factorization_Lcm_factorial [symmetric]) (insert True, simp_all) |
|
1866 |
finally show ?thesis |
|
1867 |
by (subst (asm) prime_factorization_subset_iff_dvd) |
|
1868 |
(insert True, auto simp: Lcm_factorial_eq_0_iff) |
|
1869 |
qed (insert assms, auto simp: Lcm_factorial_def) |
|
1870 |
||
1871 |
lemma Lcm_factorial_least: |
|
1872 |
assumes "\<And>y. y \<in> A \<Longrightarrow> y dvd x" |
|
1873 |
shows "Lcm_factorial A dvd x" |
|
1874 |
proof - |
|
1875 |
consider "A = {}" | "0 \<in> A" | "x = 0" | "A \<noteq> {}" "0 \<notin> A" "x \<noteq> 0" by blast |
|
1876 |
thus ?thesis |
|
1877 |
proof cases |
|
1878 |
assume *: "A \<noteq> {}" "0 \<notin> A" "x \<noteq> 0" |
|
1879 |
hence nz: "x \<noteq> 0" if "x \<in> A" for x using that by auto |
|
1880 |
from * have bdd: "subset_mset.bdd_above (prime_factorization ` A)" |
|
1881 |
by (intro subset_mset.bdd_aboveI[of _ "prime_factorization x"]) |
|
1882 |
(auto simp: prime_factorization_subset_iff_dvd nz dest: assms) |
|
1883 |
have "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)" |
|
1884 |
by (rule prime_factorization_Lcm_factorial) fact+ |
|
1885 |
also from * have "\<dots> \<subseteq># prime_factorization x" |
|
1886 |
by (intro subset_mset.cSup_least) |
|
1887 |
(auto simp: prime_factorization_subset_iff_dvd nz dest: assms) |
|
1888 |
finally show ?thesis |
|
1889 |
by (subst (asm) prime_factorization_subset_iff_dvd) |
|
1890 |
(insert * bdd, auto simp: Lcm_factorial_eq_0_iff) |
|
1891 |
qed (auto simp: Lcm_factorial_def dest: assms) |
|
1892 |
qed |
|
1893 |
||
1894 |
lemmas gcd_lcm_factorial = |
|
1895 |
gcd_factorial_dvd1 gcd_factorial_dvd2 gcd_factorial_greatest |
|
1896 |
normalize_gcd_factorial lcm_factorial_gcd_factorial |
|
1897 |
normalize_Gcd_factorial Gcd_factorial_dvd Gcd_factorial_greatest |
|
1898 |
normalize_Lcm_factorial dvd_Lcm_factorial Lcm_factorial_least |
|
1899 |
||
60804 | 1900 |
end |
1901 |
||
63498 | 1902 |
class factorial_semiring_gcd = factorial_semiring + gcd + Gcd + |
1903 |
assumes gcd_eq_gcd_factorial: "gcd a b = gcd_factorial a b" |
|
1904 |
and lcm_eq_lcm_factorial: "lcm a b = lcm_factorial a b" |
|
1905 |
and Gcd_eq_Gcd_factorial: "Gcd A = Gcd_factorial A" |
|
1906 |
and Lcm_eq_Lcm_factorial: "Lcm A = Lcm_factorial A" |
|
60804 | 1907 |
begin |
1908 |
||
63498 | 1909 |
lemma prime_factorization_gcd: |
1910 |
assumes [simp]: "a \<noteq> 0" "b \<noteq> 0" |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1911 |
shows "prime_factorization (gcd a b) = prime_factorization a \<inter># prime_factorization b" |
63498 | 1912 |
by (simp add: gcd_eq_gcd_factorial prime_factorization_gcd_factorial) |
60804 | 1913 |
|
63498 | 1914 |
lemma prime_factorization_lcm: |
1915 |
assumes [simp]: "a \<noteq> 0" "b \<noteq> 0" |
|
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63905
diff
changeset
|
1916 |
shows "prime_factorization (lcm a b) = prime_factorization a \<union># prime_factorization b" |
63498 | 1917 |
by (simp add: lcm_eq_lcm_factorial prime_factorization_lcm_factorial) |
60804 | 1918 |
|
63498 | 1919 |
lemma prime_factorization_Gcd: |
1920 |
assumes "Gcd A \<noteq> 0" |
|
1921 |
shows "prime_factorization (Gcd A) = Inf (prime_factorization ` (A - {0}))" |
|
1922 |
using assms |
|
1923 |
by (simp add: prime_factorization_Gcd_factorial Gcd_eq_Gcd_factorial Gcd_factorial_eq_0_iff) |
|
1924 |
||
1925 |
lemma prime_factorization_Lcm: |
|
1926 |
assumes "Lcm A \<noteq> 0" |
|
1927 |
shows "prime_factorization (Lcm A) = Sup (prime_factorization ` A)" |
|
1928 |
using assms |
|
1929 |
by (simp add: prime_factorization_Lcm_factorial Lcm_eq_Lcm_factorial Lcm_factorial_eq_0_iff) |
|
1930 |
||
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1931 |
lemma prime_factors_gcd [simp]: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1932 |
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> prime_factors (gcd a b) = |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1933 |
prime_factors a \<inter> prime_factors b" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1934 |
by (subst prime_factorization_gcd) auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1935 |
|
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1936 |
lemma prime_factors_lcm [simp]: |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1937 |
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> prime_factors (lcm a b) = |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1938 |
prime_factors a \<union> prime_factors b" |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1939 |
by (subst prime_factorization_lcm) auto |
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
65552
diff
changeset
|
1940 |
|
63498 | 1941 |
subclass semiring_gcd |
1942 |
by (standard, unfold gcd_eq_gcd_factorial lcm_eq_lcm_factorial) |
|
1943 |
(rule gcd_lcm_factorial; assumption)+ |
|
1944 |
||
1945 |
subclass semiring_Gcd |
|
1946 |
by (standard, unfold Gcd_eq_Gcd_factorial Lcm_eq_Lcm_factorial) |
|
1947 |
(rule gcd_lcm_factorial; assumption)+ |
|
60804 | 1948 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1949 |
lemma |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1950 |
assumes "x \<noteq> 0" "y \<noteq> 0" |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1951 |
shows gcd_eq_factorial': |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1952 |
"gcd x y = normalize (\<Prod>p \<in> prime_factors x \<inter> prime_factors y. |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1953 |
p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1") |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1954 |
and lcm_eq_factorial': |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1955 |
"lcm x y = normalize (\<Prod>p \<in> prime_factors x \<union> prime_factors y. |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1956 |
p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2") |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1957 |
proof - |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1958 |
have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1959 |
also have "\<dots> = ?rhs1" |
63905 | 1960 |
by (auto simp: gcd_factorial_def assms prod_mset_multiplicity |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1961 |
count_prime_factorization_prime |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1962 |
intro!: arg_cong[of _ _ normalize] dest: in_prime_factors_imp_prime intro!: prod.cong) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1963 |
finally show "gcd x y = ?rhs1" . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1964 |
have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1965 |
also have "\<dots> = ?rhs2" |
63905 | 1966 |
by (auto simp: lcm_factorial_def assms prod_mset_multiplicity |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1967 |
count_prime_factorization_prime intro!: arg_cong[of _ _ normalize] |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
1968 |
dest: in_prime_factors_imp_prime intro!: prod.cong) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1969 |
finally show "lcm x y = ?rhs2" . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1970 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1971 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1972 |
lemma |
63633 | 1973 |
assumes "x \<noteq> 0" "y \<noteq> 0" "prime p" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1974 |
shows multiplicity_gcd: "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1975 |
and multiplicity_lcm: "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1976 |
proof - |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1977 |
have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1978 |
also from assms have "multiplicity p \<dots> = min (multiplicity p x) (multiplicity p y)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1979 |
by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_gcd_factorial) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1980 |
finally show "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1981 |
have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1982 |
also from assms have "multiplicity p \<dots> = max (multiplicity p x) (multiplicity p y)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1983 |
by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_lcm_factorial) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1984 |
finally show "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1985 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1986 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1987 |
lemma gcd_lcm_distrib: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1988 |
"gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1989 |
proof (cases "x = 0 \<or> y = 0 \<or> z = 0") |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1990 |
case True |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1991 |
thus ?thesis |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1992 |
by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1993 |
next |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1994 |
case False |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1995 |
hence "normalize (gcd x (lcm y z)) = normalize (lcm (gcd x y) (gcd x z))" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1996 |
by (intro associatedI prime_factorization_subset_imp_dvd) |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
1997 |
(auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1998 |
subset_mset.inf_sup_distrib1) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
1999 |
thus ?thesis by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2000 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2001 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2002 |
lemma lcm_gcd_distrib: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2003 |
"lcm x (gcd y z) = gcd (lcm x y) (lcm x z)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2004 |
proof (cases "x = 0 \<or> y = 0 \<or> z = 0") |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2005 |
case True |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2006 |
thus ?thesis |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2007 |
by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2008 |
next |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2009 |
case False |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2010 |
hence "normalize (lcm x (gcd y z)) = normalize (gcd (lcm x y) (lcm x z))" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2011 |
by (intro associatedI prime_factorization_subset_imp_dvd) |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65435
diff
changeset
|
2012 |
(auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2013 |
subset_mset.sup_inf_distrib1) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2014 |
thus ?thesis by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2015 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63498
diff
changeset
|
2016 |
|
60804 | 2017 |
end |
2018 |
||
63498 | 2019 |
class factorial_ring_gcd = factorial_semiring_gcd + idom |
60804 | 2020 |
begin |
2021 |
||
63498 | 2022 |
subclass ring_gcd .. |
60804 | 2023 |
|
63498 | 2024 |
subclass idom_divide .. |
60804 | 2025 |
|
2026 |
end |
|
2027 |
||
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2028 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2029 |
class factorial_semiring_multiplicative = |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2030 |
factorial_semiring + normalization_semidom_multiplicative |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2031 |
begin |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2032 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2033 |
lemma normalize_prod_mset_primes: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2034 |
"(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (prod_mset A) = prod_mset A" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2035 |
proof (induction A) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2036 |
case (add p A) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2037 |
hence "prime p" by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2038 |
hence "normalize p = p" by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2039 |
with add show ?case by (simp add: normalize_mult) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2040 |
qed simp_all |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2041 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2042 |
lemma prod_mset_prime_factorization: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2043 |
assumes "x \<noteq> 0" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2044 |
shows "prod_mset (prime_factorization x) = normalize x" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2045 |
using assms |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2046 |
by (induction x rule: prime_divisors_induct) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2047 |
(simp_all add: prime_factorization_unit prime_factorization_times_prime |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2048 |
is_unit_normalize normalize_mult) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2049 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2050 |
lemma prime_decomposition: "unit_factor x * prod_mset (prime_factorization x) = x" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2051 |
by (cases "x = 0") (simp_all add: prod_mset_prime_factorization) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2052 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2053 |
lemma prod_prime_factors: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2054 |
assumes "x \<noteq> 0" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2055 |
shows "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2056 |
proof - |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2057 |
have "normalize x = prod_mset (prime_factorization x)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2058 |
by (simp add: prod_mset_prime_factorization assms) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2059 |
also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2060 |
by (subst prod_mset_multiplicity) simp_all |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2061 |
also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2062 |
by (intro prod.cong) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2063 |
(simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2064 |
finally show ?thesis .. |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2065 |
qed |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2066 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2067 |
lemma prime_factorization_unique'': |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2068 |
assumes S_eq: "S = {p. 0 < f p}" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2069 |
and "finite S" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2070 |
and S: "\<forall>p\<in>S. prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2071 |
shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2072 |
proof |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2073 |
define A where "A = Abs_multiset f" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2074 |
from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2075 |
with S(2) have nz: "n \<noteq> 0" by auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2076 |
from S_eq \<open>finite S\<close> have count_A: "count A = f" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2077 |
unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2078 |
from S_eq count_A have set_mset_A: "set_mset A = S" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2079 |
by (simp only: set_mset_def) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2080 |
from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" . |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2081 |
also have "\<dots> = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2082 |
also from nz have "normalize n = prod_mset (prime_factorization n)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2083 |
by (simp add: prod_mset_prime_factorization) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2084 |
finally have "prime_factorization (prod_mset A) = |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2085 |
prime_factorization (prod_mset (prime_factorization n))" by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2086 |
also from S(1) have "prime_factorization (prod_mset A) = A" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2087 |
by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2088 |
also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2089 |
by (intro prime_factorization_prod_mset_primes) auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2090 |
finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric]) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2091 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2092 |
show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2093 |
proof safe |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2094 |
fix p :: 'a assume p: "prime p" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2095 |
have "multiplicity p n = multiplicity p (normalize n)" by simp |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2096 |
also have "normalize n = prod_mset A" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2097 |
by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2098 |
also from p set_mset_A S(1) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2099 |
have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2100 |
by (intro prime_elem_multiplicity_prod_mset_distrib) auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2101 |
also from S(1) p |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2102 |
have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2103 |
by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2104 |
also have "sum_mset \<dots> = f p" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2105 |
by (simp add: semiring_1_class.sum_mset_delta' count_A) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2106 |
finally show "f p = multiplicity p n" .. |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2107 |
qed |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2108 |
qed |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2109 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2110 |
lemma divides_primepow: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2111 |
assumes "prime p" and "a dvd p ^ n" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2112 |
obtains m where "m \<le> n" and "normalize a = p ^ m" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2113 |
using divides_primepow_weak[OF assms] that assms |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2114 |
by (auto simp add: normalize_power) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2115 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2116 |
lemma Ex_other_prime_factor: |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2117 |
assumes "n \<noteq> 0" and "\<not>(\<exists>k. normalize n = p ^ k)" "prime p" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2118 |
shows "\<exists>q\<in>prime_factors n. q \<noteq> p" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2119 |
proof (rule ccontr) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2120 |
assume *: "\<not>(\<exists>q\<in>prime_factors n. q \<noteq> p)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2121 |
have "normalize n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2122 |
using assms(1) by (intro prod_prime_factors [symmetric]) auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2123 |
also from * have "\<dots> = (\<Prod>p\<in>{p}. p ^ multiplicity p n)" |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2124 |
using assms(3) by (intro prod.mono_neutral_left) (auto simp: prime_factors_multiplicity) |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2125 |
finally have "normalize n = p ^ multiplicity p n" by auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2126 |
with assms show False by auto |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2127 |
qed |
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2128 |
|
60804 | 2129 |
end |
71398
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2130 |
|
e0237f2eb49d
Removed multiplicativity assumption from normalization_semidom
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
2131 |
end |