--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Jan 04 22:57:39 2017 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Jan 04 21:28:28 2017 +0100
@@ -1,133 +1,17 @@
-(* Author: Manuel Eberl *)
+(* Title: HOL/Number_Theory/Euclidean_Algorithm.thy
+ Author: Manuel Eberl, TU Muenchen
+*)
-section \<open>Abstract euclidean algorithm\<close>
+section \<open>Abstract euclidean algorithm in euclidean (semi)rings\<close>
theory Euclidean_Algorithm
-imports "~~/src/HOL/GCD" Factorial_Ring
-begin
-
-text \<open>
- A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
- implemented. It must provide:
- \begin{itemize}
- \item division with remainder
- \item a size function such that @{term "size (a mod b) < size b"}
- for any @{term "b \<noteq> 0"}
- \end{itemize}
- The existence of these functions makes it possible to derive gcd and lcm functions
- for any Euclidean semiring.
-\<close>
-class euclidean_semiring = semidom_modulo + normalization_semidom +
- fixes euclidean_size :: "'a \<Rightarrow> nat"
- assumes size_0 [simp]: "euclidean_size 0 = 0"
- assumes mod_size_less:
- "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
- assumes size_mult_mono:
- "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
+ imports "~~/src/HOL/GCD"
+ "~~/src/HOL/Number_Theory/Factorial_Ring"
+ "~~/src/HOL/Number_Theory/Euclidean_Division"
begin
-lemma euclidean_size_normalize [simp]:
- "euclidean_size (normalize a) = euclidean_size a"
-proof (cases "a = 0")
- case True
- then show ?thesis
- by simp
-next
- case [simp]: False
- have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
- by (rule size_mult_mono) simp
- moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
- by (rule size_mult_mono) simp
- ultimately show ?thesis
- by simp
-qed
-
-lemma euclidean_division:
- fixes a :: 'a and b :: 'a
- assumes "b \<noteq> 0"
- obtains s and t where "a = s * b + t"
- and "euclidean_size t < euclidean_size b"
-proof -
- from div_mult_mod_eq [of a b]
- have "a = a div b * b + a mod b" by simp
- with that and assms show ?thesis by (auto simp add: mod_size_less)
-qed
-
-lemma dvd_euclidean_size_eq_imp_dvd:
- assumes "a \<noteq> 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b"
- shows "a dvd b"
-proof (rule ccontr)
- assume "\<not> a dvd b"
- hence "b mod a \<noteq> 0" using mod_0_imp_dvd[of b a] by blast
- then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
- from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff)
- from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast
- with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
- with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
- using size_mult_mono by force
- moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
- have "euclidean_size (b mod a) < euclidean_size a"
- using mod_size_less by blast
- ultimately show False using size_eq by simp
-qed
-
-lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
- by (subst mult.commute) (rule size_mult_mono)
-
-lemma euclidean_size_times_unit:
- assumes "is_unit a"
- shows "euclidean_size (a * b) = euclidean_size b"
-proof (rule antisym)
- from assms have [simp]: "a \<noteq> 0" by auto
- thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
- from assms have "is_unit (1 div a)" by simp
- hence "1 div a \<noteq> 0" by (intro notI) simp_all
- hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
- by (rule size_mult_mono')
- also from assms have "(1 div a) * (a * b) = b"
- by (simp add: algebra_simps unit_div_mult_swap)
- finally show "euclidean_size (a * b) \<le> euclidean_size b" .
-qed
-
-lemma euclidean_size_unit: "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
- using euclidean_size_times_unit[of a 1] by simp
-
-lemma unit_iff_euclidean_size:
- "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
-proof safe
- assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
- show "is_unit a" by (rule dvd_euclidean_size_eq_imp_dvd[OF A _ B]) simp_all
-qed (auto intro: euclidean_size_unit)
-
-lemma euclidean_size_times_nonunit:
- assumes "a \<noteq> 0" "b \<noteq> 0" "\<not>is_unit a"
- shows "euclidean_size b < euclidean_size (a * b)"
-proof (rule ccontr)
- assume "\<not>euclidean_size b < euclidean_size (a * b)"
- with size_mult_mono'[OF assms(1), of b]
- have eq: "euclidean_size (a * b) = euclidean_size b" by simp
- have "a * b dvd b"
- by (rule dvd_euclidean_size_eq_imp_dvd[OF _ _ eq]) (insert assms, simp_all)
- hence "a * b dvd 1 * b" by simp
- with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
- with assms(3) show False by contradiction
-qed
-
-lemma dvd_imp_size_le:
- assumes "a dvd b" "b \<noteq> 0"
- shows "euclidean_size a \<le> euclidean_size b"
- using assms by (auto elim!: dvdE simp: size_mult_mono)
-
-lemma dvd_proper_imp_size_less:
- assumes "a dvd b" "\<not>b dvd a" "b \<noteq> 0"
- shows "euclidean_size a < euclidean_size b"
-proof -
- from assms(1) obtain c where "b = a * c" by (erule dvdE)
- hence z: "b = c * a" by (simp add: mult.commute)
- from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
- with z assms show ?thesis
- by (auto intro!: euclidean_size_times_nonunit simp: )
-qed
+context euclidean_semiring
+begin
function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
where
@@ -432,7 +316,7 @@
end
-class euclidean_ring = euclidean_semiring + idom
+context euclidean_ring
begin
function euclid_ext_aux :: "'a \<Rightarrow> _" where
@@ -680,27 +564,6 @@
subsection \<open>Typical instances\<close>
-instantiation nat :: euclidean_semiring
-begin
-
-definition [simp]:
- "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
-
-instance by standard simp_all
-
-end
-
-
-instantiation int :: euclidean_ring
-begin
-
-definition [simp]:
- "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
-
-instance by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split)
-
-end
-
instance nat :: euclidean_semiring_gcd
proof
show [simp]: "gcd = (gcd_eucl :: nat \<Rightarrow> _)" "Lcm = (Lcm_eucl :: nat set \<Rightarrow> _)"