author | haftmann |
Wed, 12 Oct 2016 20:38:47 +0200 | |
changeset 64164 | 38c407446400 |
parent 64163 | 62c9e5c05928 |
child 64177 | 006f303fb173 |
permissions | -rw-r--r-- |
58023 | 1 |
(* Author: Manuel Eberl *) |
2 |
||
60526 | 3 |
section \<open>Abstract euclidean algorithm\<close> |
58023 | 4 |
|
5 |
theory Euclidean_Algorithm |
|
63498 | 6 |
imports "~~/src/HOL/GCD" Factorial_Ring |
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> |
64164
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
20 |
class euclidean_semiring = semiring_modulo + 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 |
||
64164
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
29 |
lemma zero_mod_left [simp]: "0 mod a = 0" |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
30 |
using mod_div_equality [of 0 a] by simp |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
31 |
|
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
32 |
lemma dvd_mod_iff: |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
33 |
assumes "k dvd n" |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
34 |
shows "(k dvd m mod n) = (k dvd m)" |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
35 |
proof - |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
36 |
from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))" |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
37 |
by (simp add: dvd_add_right_iff) |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
38 |
also have "(m div n) * n + m mod n = m" |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
39 |
using mod_div_equality [of m n] by simp |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
40 |
finally show ?thesis . |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
41 |
qed |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
42 |
|
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
43 |
lemma mod_0_imp_dvd: |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
44 |
assumes "a mod b = 0" |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
45 |
shows "b dvd a" |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
46 |
proof - |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
47 |
have "b dvd ((a div b) * b)" by simp |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
48 |
also have "(a div b) * b = a" |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
49 |
using mod_div_equality [of a b] by (simp add: assms) |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
50 |
finally show ?thesis . |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
51 |
qed |
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
52 |
|
63947 | 53 |
lemma euclidean_size_normalize [simp]: |
54 |
"euclidean_size (normalize a) = euclidean_size a" |
|
55 |
proof (cases "a = 0") |
|
56 |
case True |
|
57 |
then show ?thesis |
|
58 |
by simp |
|
59 |
next |
|
60 |
case [simp]: False |
|
61 |
have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)" |
|
62 |
by (rule size_mult_mono) simp |
|
63 |
moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))" |
|
64 |
by (rule size_mult_mono) simp |
|
65 |
ultimately show ?thesis |
|
66 |
by simp |
|
67 |
qed |
|
68 |
||
58023 | 69 |
lemma euclidean_division: |
70 |
fixes a :: 'a and b :: 'a |
|
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
71 |
assumes "b \<noteq> 0" |
58023 | 72 |
obtains s and t where "a = s * b + t" |
73 |
and "euclidean_size t < euclidean_size b" |
|
74 |
proof - |
|
64164
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
75 |
from mod_div_equality [of a b] |
58023 | 76 |
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
|
77 |
with that and assms show ?thesis by (auto simp add: mod_size_less) |
58023 | 78 |
qed |
79 |
||
80 |
lemma dvd_euclidean_size_eq_imp_dvd: |
|
81 |
assumes "a \<noteq> 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b" |
|
82 |
shows "a dvd b" |
|
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
83 |
proof (rule ccontr) |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
84 |
assume "\<not> a dvd b" |
64163
62c9e5c05928
stripped dependency on pragmatic type class semiring_div
haftmann
parents:
63947
diff
changeset
|
85 |
hence "b mod a \<noteq> 0" using mod_0_imp_dvd[of b a] by blast |
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
86 |
then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd) |
64164
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
87 |
from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff) |
58023 | 88 |
from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast |
60526 | 89 |
with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto |
90 |
with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b" |
|
58023 | 91 |
using size_mult_mono by force |
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
92 |
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
|
93 |
have "euclidean_size (b mod a) < euclidean_size a" |
58023 | 94 |
using mod_size_less by blast |
95 |
ultimately show False using size_eq by simp |
|
96 |
qed |
|
97 |
||
63498 | 98 |
lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)" |
99 |
by (subst mult.commute) (rule size_mult_mono) |
|
100 |
||
101 |
lemma euclidean_size_times_unit: |
|
102 |
assumes "is_unit a" |
|
103 |
shows "euclidean_size (a * b) = euclidean_size b" |
|
104 |
proof (rule antisym) |
|
105 |
from assms have [simp]: "a \<noteq> 0" by auto |
|
106 |
thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono') |
|
107 |
from assms have "is_unit (1 div a)" by simp |
|
108 |
hence "1 div a \<noteq> 0" by (intro notI) simp_all |
|
109 |
hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))" |
|
110 |
by (rule size_mult_mono') |
|
111 |
also from assms have "(1 div a) * (a * b) = b" |
|
112 |
by (simp add: algebra_simps unit_div_mult_swap) |
|
113 |
finally show "euclidean_size (a * b) \<le> euclidean_size b" . |
|
114 |
qed |
|
115 |
||
116 |
lemma euclidean_size_unit: "is_unit x \<Longrightarrow> euclidean_size x = euclidean_size 1" |
|
117 |
using euclidean_size_times_unit[of x 1] by simp |
|
118 |
||
119 |
lemma unit_iff_euclidean_size: |
|
120 |
"is_unit x \<longleftrightarrow> euclidean_size x = euclidean_size 1 \<and> x \<noteq> 0" |
|
121 |
proof safe |
|
122 |
assume A: "x \<noteq> 0" and B: "euclidean_size x = euclidean_size 1" |
|
123 |
show "is_unit x" by (rule dvd_euclidean_size_eq_imp_dvd[OF A _ B]) simp_all |
|
124 |
qed (auto intro: euclidean_size_unit) |
|
125 |
||
126 |
lemma euclidean_size_times_nonunit: |
|
127 |
assumes "a \<noteq> 0" "b \<noteq> 0" "\<not>is_unit a" |
|
128 |
shows "euclidean_size b < euclidean_size (a * b)" |
|
129 |
proof (rule ccontr) |
|
130 |
assume "\<not>euclidean_size b < euclidean_size (a * b)" |
|
131 |
with size_mult_mono'[OF assms(1), of b] |
|
132 |
have eq: "euclidean_size (a * b) = euclidean_size b" by simp |
|
133 |
have "a * b dvd b" |
|
134 |
by (rule dvd_euclidean_size_eq_imp_dvd[OF _ _ eq]) (insert assms, simp_all) |
|
135 |
hence "a * b dvd 1 * b" by simp |
|
136 |
with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff) |
|
137 |
with assms(3) show False by contradiction |
|
138 |
qed |
|
139 |
||
140 |
lemma dvd_imp_size_le: |
|
141 |
assumes "x dvd y" "y \<noteq> 0" |
|
142 |
shows "euclidean_size x \<le> euclidean_size y" |
|
143 |
using assms by (auto elim!: dvdE simp: size_mult_mono) |
|
144 |
||
145 |
lemma dvd_proper_imp_size_less: |
|
146 |
assumes "x dvd y" "\<not>y dvd x" "y \<noteq> 0" |
|
147 |
shows "euclidean_size x < euclidean_size y" |
|
148 |
proof - |
|
149 |
from assms(1) obtain z where "y = x * z" by (erule dvdE) |
|
150 |
hence z: "y = z * x" by (simp add: mult.commute) |
|
151 |
from z assms have "\<not>is_unit z" by (auto simp: mult.commute mult_unit_dvd_iff) |
|
152 |
with z assms show ?thesis |
|
153 |
by (auto intro!: euclidean_size_times_nonunit simp: ) |
|
154 |
qed |
|
155 |
||
58023 | 156 |
function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
157 |
where |
|
60634 | 158 |
"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
|
159 |
by pat_completeness simp |
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
160 |
termination |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
161 |
by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less) |
58023 | 162 |
|
163 |
declare gcd_eucl.simps [simp del] |
|
164 |
||
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
165 |
lemma gcd_eucl_induct [case_names zero mod]: |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
166 |
assumes H1: "\<And>b. P b 0" |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
167 |
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
|
168 |
shows "P a b" |
58023 | 169 |
proof (induct a b rule: gcd_eucl.induct) |
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
170 |
case ("1" a b) |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
171 |
show ?case |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
172 |
proof (cases "b = 0") |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
173 |
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
|
174 |
next |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
175 |
case False |
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
176 |
then have "P b (a mod b)" |
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
177 |
by (rule "1.hyps") |
60569
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
178 |
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
|
179 |
by (blast intro: H2) |
f2f1f6860959
generalized to definition from literature, which covers also polynomials
haftmann
parents:
60526
diff
changeset
|
180 |
qed |
58023 | 181 |
qed |
182 |
||
183 |
definition lcm_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
184 |
where |
|
60634 | 185 |
"lcm_eucl a b = normalize (a * b) div gcd_eucl a b" |
58023 | 186 |
|
63167 | 187 |
definition Lcm_eucl :: "'a set \<Rightarrow> 'a" \<comment> \<open> |
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
188 |
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
|
189 |
for infinite sets as well\<close> |
58023 | 190 |
where |
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset
|
191 |
"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
|
192 |
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
|
193 |
(LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n) |
60634 | 194 |
in normalize l |
58023 | 195 |
else 0)" |
196 |
||
197 |
definition Gcd_eucl :: "'a set \<Rightarrow> 'a" |
|
198 |
where |
|
199 |
"Gcd_eucl A = Lcm_eucl {d. \<forall>a\<in>A. d dvd a}" |
|
200 |
||
62428
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
201 |
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
|
202 |
|
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
203 |
lemma gcd_eucl_0: |
60634 | 204 |
"gcd_eucl a 0 = normalize a" |
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
205 |
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
|
206 |
|
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
207 |
lemma gcd_eucl_0_left: |
60634 | 208 |
"gcd_eucl 0 a = normalize a" |
60600
87fbfea0bd0a
simplified termination criterion for euclidean algorithm (again)
haftmann
parents:
60599
diff
changeset
|
209 |
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
|
210 |
|
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
211 |
lemma gcd_eucl_non_0: |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
212 |
"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
|
213 |
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
|
214 |
|
62422 | 215 |
lemma gcd_eucl_dvd1 [iff]: "gcd_eucl a b dvd a" |
216 |
and gcd_eucl_dvd2 [iff]: "gcd_eucl a b dvd b" |
|
217 |
by (induct a b rule: gcd_eucl_induct) |
|
218 |
(simp_all add: gcd_eucl_0 gcd_eucl_non_0 dvd_mod_iff) |
|
219 |
||
220 |
lemma normalize_gcd_eucl [simp]: |
|
221 |
"normalize (gcd_eucl a b) = gcd_eucl a b" |
|
222 |
by (induct a b rule: gcd_eucl_induct) (simp_all add: gcd_eucl_0 gcd_eucl_non_0) |
|
223 |
||
224 |
lemma gcd_eucl_greatest: |
|
225 |
fixes k a b :: 'a |
|
226 |
shows "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd_eucl a b" |
|
227 |
proof (induct a b rule: gcd_eucl_induct) |
|
228 |
case (zero a) from zero(1) show ?case by (rule dvd_trans) (simp add: gcd_eucl_0) |
|
229 |
next |
|
230 |
case (mod a b) |
|
231 |
then show ?case |
|
232 |
by (simp add: gcd_eucl_non_0 dvd_mod_iff) |
|
233 |
qed |
|
234 |
||
63498 | 235 |
lemma gcd_euclI: |
236 |
fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
237 |
assumes "d dvd a" "d dvd b" "normalize d = d" |
|
238 |
"\<And>k. k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd d" |
|
239 |
shows "gcd_eucl a b = d" |
|
240 |
by (rule associated_eqI) (simp_all add: gcd_eucl_greatest assms) |
|
241 |
||
62422 | 242 |
lemma eq_gcd_euclI: |
243 |
fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
244 |
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" |
|
245 |
"\<And>a b k. k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd a b" |
|
246 |
shows "gcd = gcd_eucl" |
|
247 |
by (intro ext, rule associated_eqI) (simp_all add: gcd_eucl_greatest assms) |
|
248 |
||
249 |
lemma gcd_eucl_zero [simp]: |
|
250 |
"gcd_eucl a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" |
|
251 |
by (metis dvd_0_left dvd_refl gcd_eucl_dvd1 gcd_eucl_dvd2 gcd_eucl_greatest)+ |
|
252 |
||
253 |
||
254 |
lemma dvd_Lcm_eucl [simp]: "a \<in> A \<Longrightarrow> a dvd Lcm_eucl A" |
|
255 |
and Lcm_eucl_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm_eucl A dvd b" |
|
256 |
and unit_factor_Lcm_eucl [simp]: |
|
257 |
"unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" |
|
258 |
proof - |
|
259 |
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> |
|
260 |
unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" (is ?thesis) |
|
261 |
proof (cases "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)") |
|
262 |
case False |
|
263 |
hence "Lcm_eucl A = 0" by (auto simp: Lcm_eucl_def) |
|
264 |
with False show ?thesis by auto |
|
265 |
next |
|
266 |
case True |
|
267 |
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 |
|
63040 | 268 |
define n where "n = (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)" |
269 |
define l where "l = (SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)" |
|
62422 | 270 |
have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" |
271 |
apply (subst n_def) |
|
272 |
apply (rule LeastI[of _ "euclidean_size l\<^sub>0"]) |
|
273 |
apply (rule exI[of _ l\<^sub>0]) |
|
274 |
apply (simp add: l\<^sub>0_props) |
|
275 |
done |
|
276 |
from someI_ex[OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l" and "euclidean_size l = n" |
|
277 |
unfolding l_def by simp_all |
|
278 |
{ |
|
279 |
fix l' assume "\<forall>a\<in>A. a dvd l'" |
|
280 |
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) |
|
281 |
moreover from \<open>l \<noteq> 0\<close> have "gcd_eucl l l' \<noteq> 0" by simp |
|
282 |
ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> |
|
283 |
euclidean_size b = euclidean_size (gcd_eucl l l')" |
|
284 |
by (intro exI[of _ "gcd_eucl l l'"], auto) |
|
285 |
hence "euclidean_size (gcd_eucl l l') \<ge> n" by (subst n_def) (rule Least_le) |
|
286 |
moreover have "euclidean_size (gcd_eucl l l') \<le> n" |
|
287 |
proof - |
|
288 |
have "gcd_eucl l l' dvd l" by simp |
|
289 |
then obtain a where "l = gcd_eucl l l' * a" unfolding dvd_def by blast |
|
290 |
with \<open>l \<noteq> 0\<close> have "a \<noteq> 0" by auto |
|
291 |
hence "euclidean_size (gcd_eucl l l') \<le> euclidean_size (gcd_eucl l l' * a)" |
|
292 |
by (rule size_mult_mono) |
|
293 |
also have "gcd_eucl l l' * a = l" using \<open>l = gcd_eucl l l' * a\<close> .. |
|
294 |
also note \<open>euclidean_size l = n\<close> |
|
295 |
finally show "euclidean_size (gcd_eucl l l') \<le> n" . |
|
296 |
qed |
|
297 |
ultimately have *: "euclidean_size l = euclidean_size (gcd_eucl l l')" |
|
298 |
by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>) |
|
299 |
from \<open>l \<noteq> 0\<close> have "l dvd gcd_eucl l l'" |
|
300 |
by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *) |
|
301 |
hence "l dvd l'" by (rule dvd_trans[OF _ gcd_eucl_dvd2]) |
|
302 |
} |
|
303 |
||
304 |
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> |
|
305 |
have "(\<forall>a\<in>A. a dvd normalize l) \<and> |
|
306 |
(\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l') \<and> |
|
307 |
unit_factor (normalize l) = |
|
308 |
(if normalize l = 0 then 0 else 1)" |
|
309 |
by (auto simp: unit_simps) |
|
310 |
also from True have "normalize l = Lcm_eucl A" |
|
311 |
by (simp add: Lcm_eucl_def Let_def n_def l_def) |
|
312 |
finally show ?thesis . |
|
313 |
qed |
|
314 |
note A = this |
|
315 |
||
316 |
{fix a assume "a \<in> A" then show "a dvd Lcm_eucl A" using A by blast} |
|
317 |
{fix b assume "\<And>a. a \<in> A \<Longrightarrow> a dvd b" then show "Lcm_eucl A dvd b" using A by blast} |
|
318 |
from A show "unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" by blast |
|
319 |
qed |
|
63498 | 320 |
|
62422 | 321 |
lemma normalize_Lcm_eucl [simp]: |
322 |
"normalize (Lcm_eucl A) = Lcm_eucl A" |
|
323 |
proof (cases "Lcm_eucl A = 0") |
|
324 |
case True then show ?thesis by simp |
|
325 |
next |
|
326 |
case False |
|
327 |
have "unit_factor (Lcm_eucl A) * normalize (Lcm_eucl A) = Lcm_eucl A" |
|
328 |
by (fact unit_factor_mult_normalize) |
|
329 |
with False show ?thesis by simp |
|
330 |
qed |
|
331 |
||
332 |
lemma eq_Lcm_euclI: |
|
333 |
fixes lcm :: "'a set \<Rightarrow> 'a" |
|
334 |
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" |
|
335 |
"\<And>A. normalize (lcm A) = lcm A" shows "lcm = Lcm_eucl" |
|
336 |
by (intro ext, rule associated_eqI) (auto simp: assms intro: Lcm_eucl_least) |
|
337 |
||
63498 | 338 |
lemma Gcd_eucl_dvd: "x \<in> A \<Longrightarrow> Gcd_eucl A dvd x" |
339 |
unfolding Gcd_eucl_def by (auto intro: Lcm_eucl_least) |
|
340 |
||
341 |
lemma Gcd_eucl_greatest: "(\<And>x. x \<in> A \<Longrightarrow> d dvd x) \<Longrightarrow> d dvd Gcd_eucl A" |
|
342 |
unfolding Gcd_eucl_def by auto |
|
343 |
||
344 |
lemma normalize_Gcd_eucl [simp]: "normalize (Gcd_eucl A) = Gcd_eucl A" |
|
345 |
by (simp add: Gcd_eucl_def) |
|
346 |
||
347 |
lemma Lcm_euclI: |
|
348 |
assumes "\<And>x. x \<in> A \<Longrightarrow> x dvd d" "\<And>d'. (\<And>x. x \<in> A \<Longrightarrow> x dvd d') \<Longrightarrow> d dvd d'" "normalize d = d" |
|
349 |
shows "Lcm_eucl A = d" |
|
350 |
proof - |
|
351 |
have "normalize (Lcm_eucl A) = normalize d" |
|
352 |
by (intro associatedI) (auto intro: dvd_Lcm_eucl Lcm_eucl_least assms) |
|
353 |
thus ?thesis by (simp add: assms) |
|
354 |
qed |
|
355 |
||
356 |
lemma Gcd_euclI: |
|
357 |
assumes "\<And>x. x \<in> A \<Longrightarrow> d dvd x" "\<And>d'. (\<And>x. x \<in> A \<Longrightarrow> d' dvd x) \<Longrightarrow> d' dvd d" "normalize d = d" |
|
358 |
shows "Gcd_eucl A = d" |
|
359 |
proof - |
|
360 |
have "normalize (Gcd_eucl A) = normalize d" |
|
361 |
by (intro associatedI) (auto intro: Gcd_eucl_dvd Gcd_eucl_greatest assms) |
|
362 |
thus ?thesis by (simp add: assms) |
|
363 |
qed |
|
364 |
||
365 |
lemmas lcm_gcd_eucl_facts = |
|
366 |
gcd_eucl_dvd1 gcd_eucl_dvd2 gcd_eucl_greatest normalize_gcd_eucl lcm_eucl_def |
|
367 |
Gcd_eucl_def Gcd_eucl_dvd Gcd_eucl_greatest normalize_Gcd_eucl |
|
368 |
dvd_Lcm_eucl Lcm_eucl_least normalize_Lcm_eucl |
|
369 |
||
370 |
lemma normalized_factors_product: |
|
371 |
"{p. p dvd a * b \<and> normalize p = p} = |
|
372 |
(\<lambda>(x,y). x * y) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})" |
|
373 |
proof safe |
|
374 |
fix p assume p: "p dvd a * b" "normalize p = p" |
|
375 |
interpret semiring_gcd 1 0 "op *" gcd_eucl lcm_eucl "op div" "op +" "op -" normalize unit_factor |
|
376 |
by standard (rule lcm_gcd_eucl_facts; assumption)+ |
|
377 |
from dvd_productE[OF p(1)] guess x y . note xy = this |
|
378 |
define x' y' where "x' = normalize x" and "y' = normalize y" |
|
379 |
have "p = x' * y'" |
|
380 |
by (subst p(2) [symmetric]) (simp add: xy x'_def y'_def normalize_mult) |
|
381 |
moreover from xy have "normalize x' = x'" "normalize y' = y'" "x' dvd a" "y' dvd b" |
|
382 |
by (simp_all add: x'_def y'_def) |
|
383 |
ultimately show "p \<in> (\<lambda>(x, y). x * y) ` |
|
384 |
({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})" |
|
385 |
by blast |
|
386 |
qed (auto simp: normalize_mult mult_dvd_mono) |
|
387 |
||
388 |
||
389 |
subclass factorial_semiring |
|
390 |
proof (standard, rule factorial_semiring_altI_aux) |
|
391 |
fix x assume "x \<noteq> 0" |
|
392 |
thus "finite {p. p dvd x \<and> normalize p = p}" |
|
393 |
proof (induction "euclidean_size x" arbitrary: x rule: less_induct) |
|
394 |
case (less x) |
|
395 |
show ?case |
|
396 |
proof (cases "\<exists>y. y dvd x \<and> \<not>x dvd y \<and> \<not>is_unit y") |
|
397 |
case False |
|
398 |
have "{p. p dvd x \<and> normalize p = p} \<subseteq> {1, normalize x}" |
|
399 |
proof |
|
400 |
fix p assume p: "p \<in> {p. p dvd x \<and> normalize p = p}" |
|
401 |
with False have "is_unit p \<or> x dvd p" by blast |
|
402 |
thus "p \<in> {1, normalize x}" |
|
403 |
proof (elim disjE) |
|
404 |
assume "is_unit p" |
|
405 |
hence "normalize p = 1" by (simp add: is_unit_normalize) |
|
406 |
with p show ?thesis by simp |
|
407 |
next |
|
408 |
assume "x dvd p" |
|
409 |
with p have "normalize p = normalize x" by (intro associatedI) simp_all |
|
410 |
with p show ?thesis by simp |
|
411 |
qed |
|
412 |
qed |
|
413 |
moreover have "finite \<dots>" by simp |
|
414 |
ultimately show ?thesis by (rule finite_subset) |
|
415 |
||
416 |
next |
|
417 |
case True |
|
418 |
then obtain y where y: "y dvd x" "\<not>x dvd y" "\<not>is_unit y" by blast |
|
419 |
define z where "z = x div y" |
|
420 |
let ?fctrs = "\<lambda>x. {p. p dvd x \<and> normalize p = p}" |
|
421 |
from y have x: "x = y * z" by (simp add: z_def) |
|
422 |
with less.prems have "y \<noteq> 0" "z \<noteq> 0" by auto |
|
423 |
from x y have "\<not>is_unit z" by (auto simp: mult_unit_dvd_iff) |
|
424 |
have "?fctrs x = (\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z)" |
|
425 |
by (subst x) (rule normalized_factors_product) |
|
426 |
also have "\<not>y * z dvd y * 1" "\<not>y * z dvd 1 * z" |
|
427 |
by (subst dvd_times_left_cancel_iff dvd_times_right_cancel_iff; fact)+ |
|
428 |
hence "finite ((\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z))" |
|
429 |
by (intro finite_imageI finite_cartesian_product less dvd_proper_imp_size_less) |
|
430 |
(auto simp: x) |
|
431 |
finally show ?thesis . |
|
432 |
qed |
|
433 |
qed |
|
434 |
next |
|
435 |
interpret semiring_gcd 1 0 "op *" gcd_eucl lcm_eucl "op div" "op +" "op -" normalize unit_factor |
|
436 |
by standard (rule lcm_gcd_eucl_facts; assumption)+ |
|
437 |
fix p assume p: "irreducible p" |
|
63633 | 438 |
thus "prime_elem p" by (rule irreducible_imp_prime_elem_gcd) |
63498 | 439 |
qed |
440 |
||
441 |
lemma gcd_eucl_eq_gcd_factorial: "gcd_eucl = gcd_factorial" |
|
442 |
by (intro ext gcd_euclI gcd_lcm_factorial) |
|
443 |
||
444 |
lemma lcm_eucl_eq_lcm_factorial: "lcm_eucl = lcm_factorial" |
|
445 |
by (intro ext) (simp add: lcm_eucl_def lcm_factorial_gcd_factorial gcd_eucl_eq_gcd_factorial) |
|
446 |
||
447 |
lemma Gcd_eucl_eq_Gcd_factorial: "Gcd_eucl = Gcd_factorial" |
|
448 |
by (intro ext Gcd_euclI gcd_lcm_factorial) |
|
449 |
||
450 |
lemma Lcm_eucl_eq_Lcm_factorial: "Lcm_eucl = Lcm_factorial" |
|
451 |
by (intro ext Lcm_euclI gcd_lcm_factorial) |
|
452 |
||
453 |
lemmas eucl_eq_factorial = |
|
454 |
gcd_eucl_eq_gcd_factorial lcm_eucl_eq_lcm_factorial |
|
455 |
Gcd_eucl_eq_Gcd_factorial Lcm_eucl_eq_Lcm_factorial |
|
456 |
||
58023 | 457 |
end |
458 |
||
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
459 |
class euclidean_ring = euclidean_semiring + idom |
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
460 |
begin |
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
461 |
|
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
462 |
function euclid_ext_aux :: "'a \<Rightarrow> _" where |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
463 |
"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
|
464 |
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
|
465 |
else let q = r' div r |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
466 |
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
|
467 |
by auto |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
468 |
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
|
469 |
|
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
470 |
declare euclid_ext_aux.simps [simp del] |
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
471 |
|
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
472 |
lemma euclid_ext_aux_correct: |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
473 |
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
|
474 |
assumes "s' * x + t' * y = r'" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
475 |
assumes "s * x + t * y = r" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
476 |
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
|
477 |
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
|
478 |
using assms |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
479 |
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
|
480 |
case (1 r' r s' s t' t) |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
481 |
show ?case |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
482 |
proof (cases "r = 0") |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
483 |
case True |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
484 |
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
|
485 |
(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
|
486 |
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
|
487 |
also have "?P \<dots>" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
488 |
proof safe |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
489 |
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
|
490 |
(s' * x + t' * y) div unit_factor r'" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
491 |
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
|
492 |
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
|
493 |
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
|
494 |
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
|
495 |
next |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
496 |
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
|
497 |
qed |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
498 |
finally show ?thesis . |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
499 |
next |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
500 |
case False |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
501 |
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
|
502 |
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
|
503 |
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
|
504 |
also from "1.prems" False have "?P \<dots>" |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
505 |
proof (intro "1.IH") |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
506 |
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
|
507 |
(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
|
508 |
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
|
509 |
also have "s * x + t * y = r" by fact |
64164
38c407446400
separate type class for arbitrary quotient and remainder partitions
haftmann
parents:
64163
diff
changeset
|
510 |
also have "r' - r' div r * r = r' mod r" using mod_div_equality [of r' r] |
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
511 |
by (simp add: algebra_simps) |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
512 |
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
|
513 |
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
|
514 |
finally show ?thesis . |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
515 |
qed |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
516 |
qed |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
517 |
|
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
518 |
definition euclid_ext where |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
519 |
"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
|
520 |
|
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
521 |
lemma euclid_ext_0: |
60634 | 522 |
"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
|
523 |
by (simp add: euclid_ext_def euclid_ext_aux.simps) |
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
524 |
|
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
525 |
lemma euclid_ext_left_0: |
60634 | 526 |
"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
|
527 |
by (simp add: euclid_ext_def euclid_ext_aux.simps) |
60598
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
528 |
|
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
529 |
lemma euclid_ext_correct': |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
530 |
"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
|
531 |
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
|
532 |
|
62457
a3c7bd201da7
Minor adjustments to euclidean rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62442
diff
changeset
|
533 |
lemma euclid_ext_gcd_eucl: |
a3c7bd201da7
Minor adjustments to euclidean rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62442
diff
changeset
|
534 |
"(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
|
535 |
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
|
536 |
|
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
537 |
definition euclid_ext' where |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
538 |
"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
|
539 |
|
62442
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
540 |
lemma euclid_ext'_correct': |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
541 |
"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
|
542 |
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
|
543 |
|
60634 | 544 |
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
|
545 |
by (simp add: euclid_ext'_def euclid_ext_0) |
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
546 |
|
60634 | 547 |
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
|
548 |
by (simp add: euclid_ext'_def euclid_ext_left_0) |
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
549 |
|
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
550 |
end |
78ca5674c66a
rings follow immediately their corresponding semirings
haftmann
parents:
60582
diff
changeset
|
551 |
|
58023 | 552 |
class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd + |
553 |
assumes gcd_gcd_eucl: "gcd = gcd_eucl" and lcm_lcm_eucl: "lcm = lcm_eucl" |
|
554 |
assumes Gcd_Gcd_eucl: "Gcd = Gcd_eucl" and Lcm_Lcm_eucl: "Lcm = Lcm_eucl" |
|
555 |
begin |
|
556 |
||
62422 | 557 |
subclass semiring_gcd |
558 |
by standard (simp_all add: gcd_gcd_eucl gcd_eucl_greatest lcm_lcm_eucl lcm_eucl_def) |
|
58023 | 559 |
|
62422 | 560 |
subclass semiring_Gcd |
561 |
by standard (auto simp: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def intro: Lcm_eucl_least) |
|
63498 | 562 |
|
563 |
subclass factorial_semiring_gcd |
|
564 |
proof |
|
565 |
fix a b |
|
566 |
show "gcd a b = gcd_factorial a b" |
|
567 |
by (rule sym, rule gcdI) (rule gcd_lcm_factorial; assumption)+ |
|
568 |
thus "lcm a b = lcm_factorial a b" |
|
569 |
by (simp add: lcm_factorial_gcd_factorial lcm_gcd) |
|
570 |
next |
|
571 |
fix A |
|
572 |
show "Gcd A = Gcd_factorial A" |
|
573 |
by (rule sym, rule GcdI) (rule gcd_lcm_factorial; assumption)+ |
|
574 |
show "Lcm A = Lcm_factorial A" |
|
575 |
by (rule sym, rule LcmI) (rule gcd_lcm_factorial; assumption)+ |
|
576 |
qed |
|
577 |
||
58023 | 578 |
lemma gcd_non_0: |
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset
|
579 |
"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
|
580 |
unfolding gcd_gcd_eucl by (fact gcd_eucl_non_0) |
58023 | 581 |
|
62422 | 582 |
lemmas gcd_0 = gcd_0_right |
583 |
lemmas dvd_gcd_iff = gcd_greatest_iff |
|
58023 | 584 |
lemmas gcd_greatest_iff = dvd_gcd_iff |
585 |
||
586 |
lemma gcd_mod1 [simp]: |
|
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset
|
587 |
"gcd (a mod b) b = gcd a b" |
58023 | 588 |
by (rule gcdI, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff) |
589 |
||
590 |
lemma gcd_mod2 [simp]: |
|
60430
ce559c850a27
standardized algebraic conventions: prefer a, b, c over x, y, z
haftmann
parents:
59061
diff
changeset
|
591 |
"gcd a (b mod a) = gcd a b" |
58023 | 592 |
by (rule gcdI, simp, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff) |
593 |
||
594 |
lemma euclidean_size_gcd_le1 [simp]: |
|
595 |
assumes "a \<noteq> 0" |
|
596 |
shows "euclidean_size (gcd a b) \<le> euclidean_size a" |
|
597 |
proof - |
|
598 |
have "gcd a b dvd a" by (rule gcd_dvd1) |
|
599 |
then obtain c where A: "a = gcd a b * c" unfolding dvd_def by blast |
|
60526 | 600 |
with \<open>a \<noteq> 0\<close> show ?thesis by (subst (2) A, intro size_mult_mono) auto |
58023 | 601 |
qed |
602 |
||
603 |
lemma euclidean_size_gcd_le2 [simp]: |
|
604 |
"b \<noteq> 0 \<Longrightarrow> euclidean_size (gcd a b) \<le> euclidean_size b" |
|
605 |
by (subst gcd.commute, rule euclidean_size_gcd_le1) |
|
606 |
||
607 |
lemma euclidean_size_gcd_less1: |
|
608 |
assumes "a \<noteq> 0" and "\<not>a dvd b" |
|
609 |
shows "euclidean_size (gcd a b) < euclidean_size a" |
|
610 |
proof (rule ccontr) |
|
611 |
assume "\<not>euclidean_size (gcd a b) < euclidean_size a" |
|
62422 | 612 |
with \<open>a \<noteq> 0\<close> have A: "euclidean_size (gcd a b) = euclidean_size a" |
58023 | 613 |
by (intro le_antisym, simp_all) |
62422 | 614 |
have "a dvd gcd a b" |
615 |
by (rule dvd_euclidean_size_eq_imp_dvd) (simp_all add: assms A) |
|
616 |
hence "a dvd b" using dvd_gcdD2 by blast |
|
60526 | 617 |
with \<open>\<not>a dvd b\<close> show False by contradiction |
58023 | 618 |
qed |
619 |
||
620 |
lemma euclidean_size_gcd_less2: |
|
621 |
assumes "b \<noteq> 0" and "\<not>b dvd a" |
|
622 |
shows "euclidean_size (gcd a b) < euclidean_size b" |
|
623 |
using assms by (subst gcd.commute, rule euclidean_size_gcd_less1) |
|
624 |
||
625 |
lemma euclidean_size_lcm_le1: |
|
626 |
assumes "a \<noteq> 0" and "b \<noteq> 0" |
|
627 |
shows "euclidean_size a \<le> euclidean_size (lcm a b)" |
|
628 |
proof - |
|
60690 | 629 |
have "a dvd lcm a b" by (rule dvd_lcm1) |
630 |
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
|
631 |
with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_eq_0_iff) |
58023 | 632 |
then show ?thesis by (subst A, intro size_mult_mono) |
633 |
qed |
|
634 |
||
635 |
lemma euclidean_size_lcm_le2: |
|
636 |
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> euclidean_size b \<le> euclidean_size (lcm a b)" |
|
637 |
using euclidean_size_lcm_le1 [of b a] by (simp add: ac_simps) |
|
638 |
||
639 |
lemma euclidean_size_lcm_less1: |
|
640 |
assumes "b \<noteq> 0" and "\<not>b dvd a" |
|
641 |
shows "euclidean_size a < euclidean_size (lcm a b)" |
|
642 |
proof (rule ccontr) |
|
643 |
from assms have "a \<noteq> 0" by auto |
|
644 |
assume "\<not>euclidean_size a < euclidean_size (lcm a b)" |
|
60526 | 645 |
with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "euclidean_size (lcm a b) = euclidean_size a" |
58023 | 646 |
by (intro le_antisym, simp, intro euclidean_size_lcm_le1) |
647 |
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
|
648 |
by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_eq_0_iff) |
62422 | 649 |
hence "b dvd a" by (rule lcm_dvdD2) |
60526 | 650 |
with \<open>\<not>b dvd a\<close> show False by contradiction |
58023 | 651 |
qed |
652 |
||
653 |
lemma euclidean_size_lcm_less2: |
|
654 |
assumes "a \<noteq> 0" and "\<not>a dvd b" |
|
655 |
shows "euclidean_size b < euclidean_size (lcm a b)" |
|
656 |
using assms euclidean_size_lcm_less1 [of a b] by (simp add: ac_simps) |
|
657 |
||
62428
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
658 |
lemma Lcm_eucl_set [code]: |
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
659 |
"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
|
660 |
by (simp add: Lcm_Lcm_eucl [symmetric] lcm_lcm_eucl Lcm_set) |
58023 | 661 |
|
62428
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
662 |
lemma Gcd_eucl_set [code]: |
4d5fbec92bb1
Fixed code equations for Gcd/Lcm
Manuel Eberl <eberlm@in.tum.de>
parents:
62425
diff
changeset
|
663 |
"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
|
664 |
by (simp add: Gcd_Gcd_eucl [symmetric] gcd_gcd_eucl Gcd_set) |
58023 | 665 |
|
666 |
end |
|
667 |
||
63498 | 668 |
|
60526 | 669 |
text \<open> |
58023 | 670 |
A Euclidean ring is a Euclidean semiring with additive inverses. It provides a |
671 |
few more lemmas; in particular, Bezout's lemma holds for any Euclidean ring. |
|
60526 | 672 |
\<close> |
58023 | 673 |
|
674 |
class euclidean_ring_gcd = euclidean_semiring_gcd + idom |
|
675 |
begin |
|
676 |
||
677 |
subclass euclidean_ring .. |
|
60439
b765e08f8bc0
proper subclass instances for existing gcd (semi)rings
haftmann
parents:
60438
diff
changeset
|
678 |
subclass ring_gcd .. |
63498 | 679 |
subclass factorial_ring_gcd .. |
60439
b765e08f8bc0
proper subclass instances for existing gcd (semi)rings
haftmann
parents:
60438
diff
changeset
|
680 |
|
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
681 |
lemma euclid_ext_gcd [simp]: |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
682 |
"(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
|
683 |
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
|
684 |
|
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
685 |
lemma euclid_ext_gcd' [simp]: |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
686 |
"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
|
687 |
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
|
688 |
|
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
689 |
lemma euclid_ext_correct: |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
690 |
"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
|
691 |
using euclid_ext_correct'[of x y] |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
692 |
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
|
693 |
|
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
694 |
lemma euclid_ext'_correct: |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
695 |
"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
|
696 |
using euclid_ext_correct'[of a b] |
26e4be6a680f
More efficient Extended Euclidean Algorithm
Manuel Eberl <eberlm@in.tum.de>
parents:
62429
diff
changeset
|
697 |
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
|
698 |
|
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
699 |
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
|
700 |
using euclid_ext'_correct by blast |
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
701 |
|
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
702 |
end |
58023 | 703 |
|
704 |
||
60572
718b1ba06429
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
haftmann
parents:
60571
diff
changeset
|
705 |
subsection \<open>Typical instances\<close> |
58023 | 706 |
|
707 |
instantiation nat :: euclidean_semiring |
|
708 |
begin |
|
709 |
||
710 |
definition [simp]: |
|
711 |
"euclidean_size_nat = (id :: nat \<Rightarrow> nat)" |
|
712 |
||
63498 | 713 |
instance by standard simp_all |
58023 | 714 |
|
715 |
end |
|
716 |
||
62422 | 717 |
|
58023 | 718 |
instantiation int :: euclidean_ring |
719 |
begin |
|
720 |
||
721 |
definition [simp]: |
|
722 |
"euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)" |
|
723 |
||
63498 | 724 |
instance by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split) |
58023 | 725 |
|
726 |
end |
|
727 |
||
62422 | 728 |
instance nat :: euclidean_semiring_gcd |
729 |
proof |
|
730 |
show [simp]: "gcd = (gcd_eucl :: nat \<Rightarrow> _)" "Lcm = (Lcm_eucl :: nat set \<Rightarrow> _)" |
|
731 |
by (simp_all add: eq_gcd_euclI eq_Lcm_euclI) |
|
732 |
show "lcm = (lcm_eucl :: nat \<Rightarrow> _)" "Gcd = (Gcd_eucl :: nat set \<Rightarrow> _)" |
|
733 |
by (intro ext, simp add: lcm_eucl_def lcm_nat_def Gcd_nat_def Gcd_eucl_def)+ |
|
734 |
qed |
|
735 |
||
736 |
instance int :: euclidean_ring_gcd |
|
737 |
proof |
|
738 |
show [simp]: "gcd = (gcd_eucl :: int \<Rightarrow> _)" "Lcm = (Lcm_eucl :: int set \<Rightarrow> _)" |
|
739 |
by (simp_all add: eq_gcd_euclI eq_Lcm_euclI) |
|
740 |
show "lcm = (lcm_eucl :: int \<Rightarrow> _)" "Gcd = (Gcd_eucl :: int set \<Rightarrow> _)" |
|
741 |
by (intro ext, simp add: lcm_eucl_def lcm_altdef_int |
|
742 |
semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+ |
|
743 |
qed |
|
744 |
||
63924 | 745 |
end |