author | Manuel Eberl <eberlm@in.tum.de> |
Sun, 28 Feb 2016 21:19:58 +0100 | |
changeset 62457 | a3c7bd201da7 |
parent 62442 | 26e4be6a680f |
child 63040 | eb4ddd18d635 |
permissions | -rw-r--r-- |
58023 | 1 |
(* Author: Manuel Eberl *) |
2 |
||
60526 | 3 |
section \<open>Abstract euclidean algorithm\<close> |
58023 | 4 |
|
5 |
theory Euclidean_Algorithm |
|
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62428
diff
changeset
|
6 |
imports "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial" |
58023 | 7 |
begin |
60634 | 8 |
|
60526 | 9 |
text \<open> |
58023 | 10 |
A Euclidean semiring is a semiring upon which the Euclidean algorithm can be |
11 |
implemented. It must provide: |
|
12 |
\begin{itemize} |
|
13 |
\item division with remainder |
|
14 |
\item a size function such that @{term "size (a mod b) < size b"} |
|
15 |
for any @{term "b \<noteq> 0"} |
|
16 |
\end{itemize} |
|
17 |
The existence of these functions makes it possible to derive gcd and lcm functions |
|
18 |
for any Euclidean semiring. |
|
60526 | 19 |
\<close> |
60634 | 20 |
class euclidean_semiring = semiring_div + normalization_semidom + |
58023 | 21 |
fixes euclidean_size :: "'a \<Rightarrow> nat" |
62422 | 22 |
assumes size_0 [simp]: "euclidean_size 0 = 0" |
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
23 |
assumes mod_size_less: |
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
24 |
"b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b" |
58023 | 25 |
assumes size_mult_mono: |
60634 | 26 |
"b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)" |
58023 | 27 |
begin |
28 |
||
29 |
lemma euclidean_division: |
|
30 |
fixes a :: 'a and b :: 'a |
|
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
31 |
assumes "b \<noteq> 0" |
58023 | 32 |
obtains s and t where "a = s * b + t" |
33 |
and "euclidean_size t < euclidean_size b" |
|
34 |
proof - |
|
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
35 |
from div_mod_equality [of a b 0] |
58023 | 36 |
have "a = a div b * b + a mod b" by simp |
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
37 |
with that and assms show ?thesis by (auto simp add: mod_size_less) |
58023 | 38 |
qed |
39 |
||
40 |
lemma dvd_euclidean_size_eq_imp_dvd: |
|
41 |
assumes "a \<noteq> 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b" |
|
42 |
shows "a dvd b" |
|
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
43 |
proof (rule ccontr) |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
44 |
assume "\<not> a dvd b" |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
45 |
then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd) |
58023 | 46 |
from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff) |
47 |
from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast |
|
60526 | 48 |
with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto |
49 |
with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b" |
|
58023 | 50 |
using size_mult_mono by force |
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
51 |
moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close> |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
52 |
have "euclidean_size (b mod a) < euclidean_size a" |
58023 | 53 |
using mod_size_less by blast |
54 |
ultimately show False using size_eq by simp |
|
55 |
qed |
|
56 |
||
57 |
function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
58 |
where |
|
60634 | 59 |
"gcd_eucl a b = (if b = 0 then normalize a else gcd_eucl b (a mod b))" |
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
60 |
by pat_completeness simp |
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
61 |
termination |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
62 |
by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less) |
58023 | 63 |
|
64 |
declare gcd_eucl.simps [simp del] |
|
65 |
||
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
66 |
lemma gcd_eucl_induct [case_names zero mod]: |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
67 |
assumes H1: "\<And>b. P b 0" |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
68 |
and H2: "\<And>a b. b \<noteq> 0 \<Longrightarrow> P b (a mod b) \<Longrightarrow> P a b" |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
69 |
shows "P a b" |
58023 | 70 |
proof (induct a b rule: gcd_eucl.induct) |
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
71 |
case ("1" a b) |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
72 |
show ?case |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
73 |
proof (cases "b = 0") |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
74 |
case True then show "P a b" by simp (rule H1) |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
75 |
next |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
76 |
case False |
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
77 |
then have "P b (a mod b)" |
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
78 |
by (rule "1.hyps") |
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
79 |
with \<open>b \<noteq> 0\<close> show "P a b" |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
80 |
by (blast intro: H2) |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
81 |
qed |
58023 | 82 |
qed |
83 |
||
84 |
definition lcm_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
85 |
where |
|
60634 | 86 |
"lcm_eucl a b = normalize (a * b) div gcd_eucl a b" |
58023 | 87 |
|
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
88 |
definition Lcm_eucl :: "'a set \<Rightarrow> 'a" -- \<open> |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
89 |
Somewhat complicated definition of Lcm that has the advantage of working |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
90 |
for infinite sets as well\<close> |
58023 | 91 |
where |
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset
|
92 |
"Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then |
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset
|
93 |
let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = |
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset
|
94 |
(LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n) |
60634 | 95 |
in normalize l |
58023 | 96 |
else 0)" |
97 |
||
98 |
definition Gcd_eucl :: "'a set \<Rightarrow> 'a" |
|
99 |
where |
|
100 |
"Gcd_eucl A = Lcm_eucl {d. \<forall>a\<in>A. d dvd a}" |
|
101 |
||
62428
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
102 |
declare Lcm_eucl_def Gcd_eucl_def [code del] |
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
103 |
|
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
104 |
lemma gcd_eucl_0: |
60634 | 105 |
"gcd_eucl a 0 = normalize a" |
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
106 |
by (simp add: gcd_eucl.simps [of a 0]) |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
107 |
|
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
108 |
lemma gcd_eucl_0_left: |
60634 | 109 |
"gcd_eucl 0 a = normalize a" |
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
110 |
by (simp_all add: gcd_eucl_0 gcd_eucl.simps [of 0 a]) |
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
111 |
|
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
112 |
lemma gcd_eucl_non_0: |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
113 |
"b \<noteq> 0 \<Longrightarrow> gcd_eucl a b = gcd_eucl b (a mod b)" |
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
114 |
by (simp add: gcd_eucl.simps [of a b] gcd_eucl.simps [of b 0]) |
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
115 |
|
62422 | 116 |
lemma gcd_eucl_dvd1 [iff]: "gcd_eucl a b dvd a" |
117 |
and gcd_eucl_dvd2 [iff]: "gcd_eucl a b dvd b" |
|
118 |
by (induct a b rule: gcd_eucl_induct) |
|
119 |
(simp_all add: gcd_eucl_0 gcd_eucl_non_0 dvd_mod_iff) |
|
120 |
||
121 |
lemma normalize_gcd_eucl [simp]: |
|
122 |
"normalize (gcd_eucl a b) = gcd_eucl a b" |
|
123 |
by (induct a b rule: gcd_eucl_induct) (simp_all add: gcd_eucl_0 gcd_eucl_non_0) |
|
124 |
||
125 |
lemma gcd_eucl_greatest: |
|
126 |
fixes k a b :: 'a |
|
127 |
shows "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd_eucl a b" |
|
128 |
proof (induct a b rule: gcd_eucl_induct) |
|
129 |
case (zero a) from zero(1) show ?case by (rule dvd_trans) (simp add: gcd_eucl_0) |
|
130 |
next |
|
131 |
case (mod a b) |
|
132 |
then show ?case |
|
133 |
by (simp add: gcd_eucl_non_0 dvd_mod_iff) |
|
134 |
qed |
|
135 |
||
136 |
lemma eq_gcd_euclI: |
|
137 |
fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
138 |
assumes "\<And>a b. gcd a b dvd a" "\<And>a b. gcd a b dvd b" "\<And>a b. normalize (gcd a b) = gcd a b" |
|
139 |
"\<And>a b k. k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd a b" |
|
140 |
shows "gcd = gcd_eucl" |
|
141 |
by (intro ext, rule associated_eqI) (simp_all add: gcd_eucl_greatest assms) |
|
142 |
||
143 |
lemma gcd_eucl_zero [simp]: |
|
144 |
"gcd_eucl a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" |
|
145 |
by (metis dvd_0_left dvd_refl gcd_eucl_dvd1 gcd_eucl_dvd2 gcd_eucl_greatest)+ |
|
146 |
||
147 |
||
148 |
lemma dvd_Lcm_eucl [simp]: "a \<in> A \<Longrightarrow> a dvd Lcm_eucl A" |
|
149 |
and Lcm_eucl_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm_eucl A dvd b" |
|
150 |
and unit_factor_Lcm_eucl [simp]: |
|
151 |
"unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" |
|
152 |
proof - |
|
153 |
have "(\<forall>a\<in>A. a dvd Lcm_eucl A) \<and> (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> Lcm_eucl A dvd l') \<and> |
|
154 |
unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" (is ?thesis) |
|
155 |
proof (cases "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)") |
|
156 |
case False |
|
157 |
hence "Lcm_eucl A = 0" by (auto simp: Lcm_eucl_def) |
|
158 |
with False show ?thesis by auto |
|
159 |
next |
|
160 |
case True |
|
161 |
then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast |
|
162 |
def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" |
|
163 |
def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" |
|
164 |
have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" |
|
165 |
apply (subst n_def) |
|
166 |
apply (rule LeastI[of _ "euclidean_size l\<^sub>0"]) |
|
167 |
apply (rule exI[of _ l\<^sub>0]) |
|
168 |
apply (simp add: l\<^sub>0_props) |
|
169 |
done |
|
170 |
from someI_ex[OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l" and "euclidean_size l = n" |
|
171 |
unfolding l_def by simp_all |
|
172 |
{ |
|
173 |
fix l' assume "\<forall>a\<in>A. a dvd l'" |
|
174 |
with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd_eucl l l'" by (auto intro: gcd_eucl_greatest) |
|
175 |
moreover from \<open>l \<noteq> 0\<close> have "gcd_eucl l l' \<noteq> 0" by simp |
|
176 |
ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> |
|
177 |
euclidean_size b = euclidean_size (gcd_eucl l l')" |
|
178 |
by (intro exI[of _ "gcd_eucl l l'"], auto) |
|
179 |
hence "euclidean_size (gcd_eucl l l') \<ge> n" by (subst n_def) (rule Least_le) |
|
180 |
moreover have "euclidean_size (gcd_eucl l l') \<le> n" |
|
181 |
proof - |
|
182 |
have "gcd_eucl l l' dvd l" by simp |
|
183 |
then obtain a where "l = gcd_eucl l l' * a" unfolding dvd_def by blast |
|
184 |
with \<open>l \<noteq> 0\<close> have "a \<noteq> 0" by auto |
|
185 |
hence "euclidean_size (gcd_eucl l l') \<le> euclidean_size (gcd_eucl l l' * a)" |
|
186 |
by (rule size_mult_mono) |
|
187 |
also have "gcd_eucl l l' * a = l" using \<open>l = gcd_eucl l l' * a\<close> .. |
|
188 |
also note \<open>euclidean_size l = n\<close> |
|
189 |
finally show "euclidean_size (gcd_eucl l l') \<le> n" . |
|
190 |
qed |
|
191 |
ultimately have *: "euclidean_size l = euclidean_size (gcd_eucl l l')" |
|
192 |
by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>) |
|
193 |
from \<open>l \<noteq> 0\<close> have "l dvd gcd_eucl l l'" |
|
194 |
by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *) |
|
195 |
hence "l dvd l'" by (rule dvd_trans[OF _ gcd_eucl_dvd2]) |
|
196 |
} |
|
197 |
||
198 |
with \<open>(\<forall>a\<in>A. a dvd l)\<close> and unit_factor_is_unit[OF \<open>l \<noteq> 0\<close>] and \<open>l \<noteq> 0\<close> |
|
199 |
have "(\<forall>a\<in>A. a dvd normalize l) \<and> |
|
200 |
(\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l') \<and> |
|
201 |
unit_factor (normalize l) = |
|
202 |
(if normalize l = 0 then 0 else 1)" |
|
203 |
by (auto simp: unit_simps) |
|
204 |
also from True have "normalize l = Lcm_eucl A" |
|
205 |
by (simp add: Lcm_eucl_def Let_def n_def l_def) |
|
206 |
finally show ?thesis . |
|
207 |
qed |
|
208 |
note A = this |
|
209 |
||
210 |
{fix a assume "a \<in> A" then show "a dvd Lcm_eucl A" using A by blast} |
|
211 |
{fix b assume "\<And>a. a \<in> A \<Longrightarrow> a dvd b" then show "Lcm_eucl A dvd b" using A by blast} |
|
212 |
from A show "unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" by blast |
|
213 |
qed |
|
214 |
||
215 |
lemma normalize_Lcm_eucl [simp]: |
|
216 |
"normalize (Lcm_eucl A) = Lcm_eucl A" |
|
217 |
proof (cases "Lcm_eucl A = 0") |
|
218 |
case True then show ?thesis by simp |
|
219 |
next |
|
220 |
case False |
|
221 |
have "unit_factor (Lcm_eucl A) * normalize (Lcm_eucl A) = Lcm_eucl A" |
|
222 |
by (fact unit_factor_mult_normalize) |
|
223 |
with False show ?thesis by simp |
|
224 |
qed |
|
225 |
||
226 |
lemma eq_Lcm_euclI: |
|
227 |
fixes lcm :: "'a set \<Rightarrow> 'a" |
|
228 |
assumes "\<And>A a. a \<in> A \<Longrightarrow> a dvd lcm A" and "\<And>A c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> lcm A dvd c" |
|
229 |
"\<And>A. normalize (lcm A) = lcm A" shows "lcm = Lcm_eucl" |
|
230 |
by (intro ext, rule associated_eqI) (auto simp: assms intro: Lcm_eucl_least) |
|
231 |
||
58023 | 232 |
end |
233 |
||
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
234 |
class euclidean_ring = euclidean_semiring + idom |
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
235 |
begin |
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
236 |
|
62457
a3c7bd201da7
Minor adjustments to euclidean rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62442
diff
changeset
|
237 |
subclass ring_div .. |
a3c7bd201da7
Minor adjustments to euclidean rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62442
diff
changeset
|
238 |
|
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
239 |
function euclid_ext_aux :: "'a \<Rightarrow> _" where |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
240 |
"euclid_ext_aux r' r s' s t' t = ( |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
241 |
if r = 0 then let c = 1 div unit_factor r' in (s' * c, t' * c, normalize r') |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
242 |
else let q = r' div r |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
243 |
in euclid_ext_aux r (r' mod r) s (s' - q * s) t (t' - q * t))" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
244 |
by auto |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
245 |
termination by (relation "measure (\<lambda>(_,b,_,_,_,_). euclidean_size b)") (simp_all add: mod_size_less) |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
246 |
|
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
247 |
declare euclid_ext_aux.simps [simp del] |
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
248 |
|
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
249 |
lemma euclid_ext_aux_correct: |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
250 |
assumes "gcd_eucl r' r = gcd_eucl x y" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
251 |
assumes "s' * x + t' * y = r'" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
252 |
assumes "s * x + t * y = r" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
253 |
shows "case euclid_ext_aux r' r s' s t' t of (a,b,c) \<Rightarrow> |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
254 |
a * x + b * y = c \<and> c = gcd_eucl x y" (is "?P (euclid_ext_aux r' r s' s t' t)") |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
255 |
using assms |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
256 |
proof (induction r' r s' s t' t rule: euclid_ext_aux.induct) |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
257 |
case (1 r' r s' s t' t) |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
258 |
show ?case |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
259 |
proof (cases "r = 0") |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
260 |
case True |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
261 |
hence "euclid_ext_aux r' r s' s t' t = |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
262 |
(s' div unit_factor r', t' div unit_factor r', normalize r')" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
263 |
by (subst euclid_ext_aux.simps) (simp add: Let_def) |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
264 |
also have "?P \<dots>" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
265 |
proof safe |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
266 |
have "s' div unit_factor r' * x + t' div unit_factor r' * y = |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
267 |
(s' * x + t' * y) div unit_factor r'" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
268 |
by (cases "r' = 0") (simp_all add: unit_div_commute) |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
269 |
also have "s' * x + t' * y = r'" by fact |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
270 |
also have "\<dots> div unit_factor r' = normalize r'" by simp |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
271 |
finally show "s' div unit_factor r' * x + t' div unit_factor r' * y = normalize r'" . |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
272 |
next |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
273 |
from "1.prems" True show "normalize r' = gcd_eucl x y" by (simp add: gcd_eucl_0) |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
274 |
qed |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
275 |
finally show ?thesis . |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
276 |
next |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
277 |
case False |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
278 |
hence "euclid_ext_aux r' r s' s t' t = |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
279 |
euclid_ext_aux r (r' mod r) s (s' - r' div r * s) t (t' - r' div r * t)" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
280 |
by (subst euclid_ext_aux.simps) (simp add: Let_def) |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
281 |
also from "1.prems" False have "?P \<dots>" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
282 |
proof (intro "1.IH") |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
283 |
have "(s' - r' div r * s) * x + (t' - r' div r * t) * y = |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
284 |
(s' * x + t' * y) - r' div r * (s * x + t * y)" by (simp add: algebra_simps) |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
285 |
also have "s' * x + t' * y = r'" by fact |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
286 |
also have "s * x + t * y = r" by fact |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
287 |
also have "r' - r' div r * r = r' mod r" using mod_div_equality[of r' r] |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
288 |
by (simp add: algebra_simps) |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
289 |
finally show "(s' - r' div r * s) * x + (t' - r' div r * t) * y = r' mod r" . |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
290 |
qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality') |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
291 |
finally show ?thesis . |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
292 |
qed |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
293 |
qed |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
294 |
|
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
295 |
definition euclid_ext where |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
296 |
"euclid_ext a b = euclid_ext_aux a b 1 0 0 1" |
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
297 |
|
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
298 |
lemma euclid_ext_0: |
60634 | 299 |
"euclid_ext a 0 = (1 div unit_factor a, 0, normalize a)" |
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
300 |
by (simp add: euclid_ext_def euclid_ext_aux.simps) |
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
301 |
|
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
302 |
lemma euclid_ext_left_0: |
60634 | 303 |
"euclid_ext 0 a = (0, 1 div unit_factor a, normalize a)" |
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
304 |
by (simp add: euclid_ext_def euclid_ext_aux.simps) |
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
305 |
|
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
306 |
lemma euclid_ext_correct': |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
307 |
"case euclid_ext x y of (a,b,c) \<Rightarrow> a * x + b * y = c \<and> c = gcd_eucl x y" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
308 |
unfolding euclid_ext_def by (rule euclid_ext_aux_correct) simp_all |
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
309 |
|
62457
a3c7bd201da7
Minor adjustments to euclidean rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62442
diff
changeset
|
310 |
lemma euclid_ext_gcd_eucl: |
a3c7bd201da7
Minor adjustments to euclidean rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62442
diff
changeset
|
311 |
"(case euclid_ext x y of (a,b,c) \<Rightarrow> c) = gcd_eucl x y" |
a3c7bd201da7
Minor adjustments to euclidean rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62442
diff
changeset
|
312 |
using euclid_ext_correct'[of x y] by (simp add: case_prod_unfold) |
a3c7bd201da7
Minor adjustments to euclidean rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62442
diff
changeset
|
313 |
|
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
314 |
definition euclid_ext' where |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
315 |
"euclid_ext' x y = (case euclid_ext x y of (a, b, _) \<Rightarrow> (a, b))" |
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
316 |
|
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
317 |
lemma euclid_ext'_correct': |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
318 |
"case euclid_ext' x y of (a,b) \<Rightarrow> a * x + b * y = gcd_eucl x y" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
319 |
using euclid_ext_correct'[of x y] by (simp add: case_prod_unfold euclid_ext'_def) |
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
320 |
|
60634 | 321 |
lemma euclid_ext'_0: "euclid_ext' a 0 = (1 div unit_factor a, 0)" |
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
322 |
by (simp add: euclid_ext'_def euclid_ext_0) |
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
323 |
|
60634 | 324 |
lemma euclid_ext'_left_0: "euclid_ext' 0 a = (0, 1 div unit_factor a)" |
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
325 |
by (simp add: euclid_ext'_def euclid_ext_left_0) |
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
326 |
|
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
327 |
end |
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
328 |
|
58023 | 329 |
class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd + |
330 |
assumes gcd_gcd_eucl: "gcd = gcd_eucl" and lcm_lcm_eucl: "lcm = lcm_eucl" |
|
331 |
assumes Gcd_Gcd_eucl: "Gcd = Gcd_eucl" and Lcm_Lcm_eucl: "Lcm = Lcm_eucl" |
|
332 |
begin |
|
333 |
||
62422 | 334 |
subclass semiring_gcd |
335 |
by standard (simp_all add: gcd_gcd_eucl gcd_eucl_greatest lcm_lcm_eucl lcm_eucl_def) |
|
58023 | 336 |
|
62422 | 337 |
subclass semiring_Gcd |
338 |
by standard (auto simp: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def intro: Lcm_eucl_least) |
|
339 |
||
58023 | 340 |
lemma gcd_non_0: |
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset
|
341 |
"b \<noteq> 0 \<Longrightarrow> gcd a b = gcd b (a mod b)" |
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
342 |
unfolding gcd_gcd_eucl by (fact gcd_eucl_non_0) |
58023 | 343 |
|
62422 | 344 |
lemmas gcd_0 = gcd_0_right |
345 |
lemmas dvd_gcd_iff = gcd_greatest_iff |
|
58023 | 346 |
lemmas gcd_greatest_iff = dvd_gcd_iff |
347 |
||
348 |
lemma gcd_mod1 [simp]: |
|
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset
|
349 |
"gcd (a mod b) b = gcd a b" |
58023 | 350 |
by (rule gcdI, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff) |
351 |
||
352 |
lemma gcd_mod2 [simp]: |
|
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset
|
353 |
"gcd a (b mod a) = gcd a b" |
58023 | 354 |
by (rule gcdI, simp, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff) |
355 |
||
356 |
lemma euclidean_size_gcd_le1 [simp]: |
|
357 |
assumes "a \<noteq> 0" |
|
358 |
shows "euclidean_size (gcd a b) \<le> euclidean_size a" |
|
359 |
proof - |
|
360 |
have "gcd a b dvd a" by (rule gcd_dvd1) |
|
361 |
then obtain c where A: "a = gcd a b * c" unfolding dvd_def by blast |
|
60526 | 362 |
with \<open>a \<noteq> 0\<close> show ?thesis by (subst (2) A, intro size_mult_mono) auto |
58023 | 363 |
qed |
364 |
||
365 |
lemma euclidean_size_gcd_le2 [simp]: |
|
366 |
"b \<noteq> 0 \<Longrightarrow> euclidean_size (gcd a b) \<le> euclidean_size b" |
|
367 |
by (subst gcd.commute, rule euclidean_size_gcd_le1) |
|
368 |
||
369 |
lemma euclidean_size_gcd_less1: |
|
370 |
assumes "a \<noteq> 0" and "\<not>a dvd b" |
|
371 |
shows "euclidean_size (gcd a b) < euclidean_size a" |
|
372 |
proof (rule ccontr) |
|
373 |
assume "\<not>euclidean_size (gcd a b) < euclidean_size a" |
|
62422 | 374 |
with \<open>a \<noteq> 0\<close> have A: "euclidean_size (gcd a b) = euclidean_size a" |
58023 | 375 |
by (intro le_antisym, simp_all) |
62422 | 376 |
have "a dvd gcd a b" |
377 |
by (rule dvd_euclidean_size_eq_imp_dvd) (simp_all add: assms A) |
|
378 |
hence "a dvd b" using dvd_gcdD2 by blast |
|
60526 | 379 |
with \<open>\<not>a dvd b\<close> show False by contradiction |
58023 | 380 |
qed |
381 |
||
382 |
lemma euclidean_size_gcd_less2: |
|
383 |
assumes "b \<noteq> 0" and "\<not>b dvd a" |
|
384 |
shows "euclidean_size (gcd a b) < euclidean_size b" |
|
385 |
using assms by (subst gcd.commute, rule euclidean_size_gcd_less1) |
|
386 |
||
387 |
lemma euclidean_size_lcm_le1: |
|
388 |
assumes "a \<noteq> 0" and "b \<noteq> 0" |
|
389 |
shows "euclidean_size a \<le> euclidean_size (lcm a b)" |
|
390 |
proof - |
|
60690 | 391 |
have "a dvd lcm a b" by (rule dvd_lcm1) |
392 |
then obtain c where A: "lcm a b = a * c" .. |
|
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62428
diff
changeset
|
393 |
with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_eq_0_iff) |
58023 | 394 |
then show ?thesis by (subst A, intro size_mult_mono) |
395 |
qed |
|
396 |
||
397 |
lemma euclidean_size_lcm_le2: |
|
398 |
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> euclidean_size b \<le> euclidean_size (lcm a b)" |
|
399 |
using euclidean_size_lcm_le1 [of b a] by (simp add: ac_simps) |
|
400 |
||
401 |
lemma euclidean_size_lcm_less1: |
|
402 |
assumes "b \<noteq> 0" and "\<not>b dvd a" |
|
403 |
shows "euclidean_size a < euclidean_size (lcm a b)" |
|
404 |
proof (rule ccontr) |
|
405 |
from assms have "a \<noteq> 0" by auto |
|
406 |
assume "\<not>euclidean_size a < euclidean_size (lcm a b)" |
|
60526 | 407 |
with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "euclidean_size (lcm a b) = euclidean_size a" |
58023 | 408 |
by (intro le_antisym, simp, intro euclidean_size_lcm_le1) |
409 |
with assms have "lcm a b dvd a" |
|
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62428
diff
changeset
|
410 |
by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_eq_0_iff) |
62422 | 411 |
hence "b dvd a" by (rule lcm_dvdD2) |
60526 | 412 |
with \<open>\<not>b dvd a\<close> show False by contradiction |
58023 | 413 |
qed |
414 |
||
415 |
lemma euclidean_size_lcm_less2: |
|
416 |
assumes "a \<noteq> 0" and "\<not>a dvd b" |
|
417 |
shows "euclidean_size b < euclidean_size (lcm a b)" |
|
418 |
using assms euclidean_size_lcm_less1 [of a b] by (simp add: ac_simps) |
|
419 |
||
62428
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
420 |
lemma Lcm_eucl_set [code]: |
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
421 |
"Lcm_eucl (set xs) = foldl lcm_eucl 1 xs" |
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
422 |
by (simp add: Lcm_Lcm_eucl [symmetric] lcm_lcm_eucl Lcm_set) |
58023 | 423 |
|
62428
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
424 |
lemma Gcd_eucl_set [code]: |
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
425 |
"Gcd_eucl (set xs) = foldl gcd_eucl 0 xs" |
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
426 |
by (simp add: Gcd_Gcd_eucl [symmetric] gcd_gcd_eucl Gcd_set) |
58023 | 427 |
|
428 |
end |
|
429 |
||
60526 | 430 |
text \<open> |
58023 | 431 |
A Euclidean ring is a Euclidean semiring with additive inverses. It provides a |
432 |
few more lemmas; in particular, Bezout's lemma holds for any Euclidean ring. |
|
60526 | 433 |
\<close> |
58023 | 434 |
|
435 |
class euclidean_ring_gcd = euclidean_semiring_gcd + idom |
|
436 |
begin |
|
437 |
||
438 |
subclass euclidean_ring .. |
|
60439
b765e08f8bc0
proper subclass instances for existing gcd (semi)rings
haftmann
parents:
60438
diff
changeset
|
439 |
subclass ring_gcd .. |
b765e08f8bc0
proper subclass instances for existing gcd (semi)rings
haftmann
parents:
60438
diff
changeset
|
440 |
|
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
441 |
lemma euclid_ext_gcd [simp]: |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
442 |
"(case euclid_ext a b of (_, _ , t) \<Rightarrow> t) = gcd a b" |
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
443 |
using euclid_ext_correct'[of a b] by (simp add: case_prod_unfold Let_def gcd_gcd_eucl) |
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
444 |
|
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
445 |
lemma euclid_ext_gcd' [simp]: |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
446 |
"euclid_ext a b = (r, s, t) \<Longrightarrow> t = gcd a b" |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
447 |
by (insert euclid_ext_gcd[of a b], drule (1) subst, simp) |
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
448 |
|
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
449 |
lemma euclid_ext_correct: |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
450 |
"case euclid_ext x y of (a,b,c) \<Rightarrow> a * x + b * y = c \<and> c = gcd x y" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
451 |
using euclid_ext_correct'[of x y] |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
452 |
by (simp add: gcd_gcd_eucl case_prod_unfold) |
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
453 |
|
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
454 |
lemma euclid_ext'_correct: |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
455 |
"fst (euclid_ext' a b) * a + snd (euclid_ext' a b) * b = gcd a b" |
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
456 |
using euclid_ext_correct'[of a b] |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
457 |
by (simp add: gcd_gcd_eucl case_prod_unfold euclid_ext'_def) |
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
458 |
|
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
459 |
lemma bezout: "\<exists>s t. s * a + t * b = gcd a b" |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
460 |
using euclid_ext'_correct by blast |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
461 |
|
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
462 |
end |
58023 | 463 |
|
464 |
||
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
465 |
subsection \<open>Typical instances\<close> |
58023 | 466 |
|
467 |
instantiation nat :: euclidean_semiring |
|
468 |
begin |
|
469 |
||
470 |
definition [simp]: |
|
471 |
"euclidean_size_nat = (id :: nat \<Rightarrow> nat)" |
|
472 |
||
473 |
instance proof |
|
59061 | 474 |
qed simp_all |
58023 | 475 |
|
476 |
end |
|
477 |
||
62422 | 478 |
|
58023 | 479 |
instantiation int :: euclidean_ring |
480 |
begin |
|
481 |
||
482 |
definition [simp]: |
|
483 |
"euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)" |
|
484 |
||
60580 | 485 |
instance |
60686 | 486 |
by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split) |
58023 | 487 |
|
488 |
end |
|
489 |
||
62422 | 490 |
|
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
491 |
instantiation poly :: (field) euclidean_ring |
60571 | 492 |
begin |
493 |
||
494 |
definition euclidean_size_poly :: "'a poly \<Rightarrow> nat" |
|
62422 | 495 |
where "euclidean_size p = (if p = 0 then 0 else 2 ^ degree p)" |
60571 | 496 |
|
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
497 |
lemma euclidean_size_poly_0 [simp]: |
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
498 |
"euclidean_size (0::'a poly) = 0" |
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
499 |
by (simp add: euclidean_size_poly_def) |
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
500 |
|
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
501 |
lemma euclidean_size_poly_not_0 [simp]: |
62422 | 502 |
"p \<noteq> 0 \<Longrightarrow> euclidean_size p = 2 ^ degree p" |
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
503 |
by (simp add: euclidean_size_poly_def) |
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
504 |
|
60571 | 505 |
instance |
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
506 |
proof |
60571 | 507 |
fix p q :: "'a poly" |
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
508 |
assume "q \<noteq> 0" |
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
509 |
then have "p mod q = 0 \<or> degree (p mod q) < degree q" |
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
510 |
by (rule degree_mod_less [of q p]) |
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
511 |
with \<open>q \<noteq> 0\<close> show "euclidean_size (p mod q) < euclidean_size q" |
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
512 |
by (cases "p mod q = 0") simp_all |
60571 | 513 |
next |
514 |
fix p q :: "'a poly" |
|
515 |
assume "q \<noteq> 0" |
|
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
516 |
from \<open>q \<noteq> 0\<close> have "degree p \<le> degree (p * q)" |
60571 | 517 |
by (rule degree_mult_right_le) |
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
518 |
with \<open>q \<noteq> 0\<close> show "euclidean_size p \<le> euclidean_size (p * q)" |
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
519 |
by (cases "p = 0") simp_all |
62422 | 520 |
qed simp |
60571 | 521 |
|
58023 | 522 |
end |
60571 | 523 |
|
62422 | 524 |
|
525 |
instance nat :: euclidean_semiring_gcd |
|
526 |
proof |
|
527 |
show [simp]: "gcd = (gcd_eucl :: nat \<Rightarrow> _)" "Lcm = (Lcm_eucl :: nat set \<Rightarrow> _)" |
|
528 |
by (simp_all add: eq_gcd_euclI eq_Lcm_euclI) |
|
529 |
show "lcm = (lcm_eucl :: nat \<Rightarrow> _)" "Gcd = (Gcd_eucl :: nat set \<Rightarrow> _)" |
|
530 |
by (intro ext, simp add: lcm_eucl_def lcm_nat_def Gcd_nat_def Gcd_eucl_def)+ |
|
531 |
qed |
|
532 |
||
533 |
instance int :: euclidean_ring_gcd |
|
534 |
proof |
|
535 |
show [simp]: "gcd = (gcd_eucl :: int \<Rightarrow> _)" "Lcm = (Lcm_eucl :: int set \<Rightarrow> _)" |
|
536 |
by (simp_all add: eq_gcd_euclI eq_Lcm_euclI) |
|
537 |
show "lcm = (lcm_eucl :: int \<Rightarrow> _)" "Gcd = (Gcd_eucl :: int set \<Rightarrow> _)" |
|
538 |
by (intro ext, simp add: lcm_eucl_def lcm_altdef_int |
|
539 |
semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+ |
|
540 |
qed |
|
541 |
||
542 |
||
543 |
instantiation poly :: (field) euclidean_ring_gcd |
|
544 |
begin |
|
545 |
||
546 |
definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where |
|
547 |
"gcd_poly = gcd_eucl" |
|
548 |
||
549 |
definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where |
|
550 |
"lcm_poly = lcm_eucl" |
|
551 |
||
552 |
definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where |
|
553 |
"Gcd_poly = Gcd_eucl" |
|
554 |
||
555 |
definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where |
|
556 |
"Lcm_poly = Lcm_eucl" |
|
557 |
||
558 |
instance by standard (simp_all only: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def) |
|
559 |
end |
|
60687 | 560 |
|
62425 | 561 |
lemma poly_gcd_monic: |
562 |
"lead_coeff (gcd x y) = (if x = 0 \<and> y = 0 then 0 else 1)" |
|
563 |
using unit_factor_gcd[of x y] |
|
564 |
by (simp add: unit_factor_poly_def monom_0 one_poly_def lead_coeff_def split: if_split_asm) |
|
565 |
||
566 |
lemma poly_dvd_antisym: |
|
567 |
fixes p q :: "'a::idom poly" |
|
568 |
assumes coeff: "coeff p (degree p) = coeff q (degree q)" |
|
569 |
assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q" |
|
570 |
proof (cases "p = 0") |
|
571 |
case True with coeff show "p = q" by simp |
|
572 |
next |
|
573 |
case False with coeff have "q \<noteq> 0" by auto |
|
574 |
have degree: "degree p = degree q" |
|
575 |
using \<open>p dvd q\<close> \<open>q dvd p\<close> \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> |
|
576 |
by (intro order_antisym dvd_imp_degree_le) |
|
577 |
||
578 |
from \<open>p dvd q\<close> obtain a where a: "q = p * a" .. |
|
579 |
with \<open>q \<noteq> 0\<close> have "a \<noteq> 0" by auto |
|
580 |
with degree a \<open>p \<noteq> 0\<close> have "degree a = 0" |
|
581 |
by (simp add: degree_mult_eq) |
|
582 |
with coeff a show "p = q" |
|
583 |
by (cases a, auto split: if_splits) |
|
584 |
qed |
|
585 |
||
586 |
lemma poly_gcd_unique: |
|
587 |
fixes d x y :: "_ poly" |
|
588 |
assumes dvd1: "d dvd x" and dvd2: "d dvd y" |
|
589 |
and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d" |
|
590 |
and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)" |
|
591 |
shows "d = gcd x y" |
|
592 |
using assms by (intro gcdI) (auto simp: normalize_poly_def split: if_split_asm) |
|
593 |
||
594 |
lemma poly_gcd_code [code]: |
|
595 |
"gcd x y = (if y = 0 then normalize x else gcd y (x mod (y :: _ poly)))" |
|
596 |
by (simp add: gcd_0 gcd_non_0) |
|
597 |
||
60571 | 598 |
end |