# HG changeset patch # User haftmann # Date 1417013986 -3600 # Node ID 67771d267ff2163c39d929bf3d0d72789920ff86 # Parent 5f060de2dfd651fd06290f1e2b1da0be448afc81 prefer abbrev for is_unit diff -r 5f060de2dfd6 -r 67771d267ff2 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Nov 26 15:46:19 2014 +0100 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Nov 26 15:59:46 2014 +0100 @@ -9,29 +9,29 @@ context semiring_div begin -definition ring_inv :: "'a \ 'a" +abbreviation is_unit :: "'a \ bool" where - "ring_inv x = 1 div x" - -definition is_unit :: "'a \ bool" -where - "is_unit x \ x dvd 1" + "is_unit x \ x dvd 1" definition associated :: "'a \ 'a \ bool" where "associated x y \ x dvd y \ y dvd x" +definition ring_inv :: "'a \ 'a" +where + "ring_inv x = 1 div x" + lemma unit_prod [intro]: "is_unit x \ is_unit y \ is_unit (x * y)" - unfolding is_unit_def by (subst mult_1_left [of 1, symmetric], rule mult_dvd_mono) + by (subst mult_1_left [of 1, symmetric], rule mult_dvd_mono) lemma unit_ring_inv: "is_unit y \ x div y = x * ring_inv y" - by (simp add: div_mult_swap ring_inv_def is_unit_def) + by (simp add: div_mult_swap ring_inv_def) lemma unit_ring_inv_ring_inv [simp]: "is_unit x \ ring_inv (ring_inv x) = x" - unfolding is_unit_def ring_inv_def + unfolding ring_inv_def by (metis div_mult_mult1_if div_mult_self1_is_id dvd_mult_div_cancel mult_1_right) lemma inv_imp_eq_ring_inv: @@ -40,7 +40,7 @@ lemma ring_inv_is_inv1 [simp]: "is_unit a \ a * ring_inv a = 1" - unfolding is_unit_def ring_inv_def by simp + unfolding ring_inv_def by simp lemma ring_inv_is_inv2 [simp]: "is_unit a \ ring_inv a * a = 1" @@ -51,7 +51,7 @@ shows "is_unit (ring_inv x)" proof - from assms have "1 = ring_inv x * x" by simp - then show "is_unit (ring_inv x)" unfolding is_unit_def by (rule dvdI) + then show "is_unit (ring_inv x)" by (rule dvdI) qed lemma mult_unit_dvd_iff: @@ -104,11 +104,11 @@ lemma unit_imp_dvd [dest]: "is_unit y \ y dvd x" - by (rule dvd_trans [of _ 1]) (simp_all add: is_unit_def) + by (rule dvd_trans [of _ 1]) simp_all lemma dvd_unit_imp_unit: "is_unit y \ x dvd y \ is_unit x" - by (unfold is_unit_def) (rule dvd_trans) + by (rule dvd_trans) lemma ring_inv_0 [simp]: "ring_inv 0 = 0" @@ -138,15 +138,15 @@ lemma associated_unit: "is_unit x \ associated x y \ is_unit y" - unfolding associated_def by (fast dest: dvd_unit_imp_unit) + unfolding associated_def using dvd_unit_imp_unit by auto lemma is_unit_1 [simp]: "is_unit 1" - unfolding is_unit_def by simp + by simp lemma not_is_unit_0 [simp]: "\ is_unit 0" - unfolding is_unit_def by auto + by auto lemma unit_mult_left_cancel: assumes "is_unit x" @@ -193,7 +193,7 @@ unfolding associated_def by simp_all hence "1 = x div y * (y div x)" by (simp add: div_mult_swap) - hence "is_unit (x div y)" unfolding is_unit_def by (rule dvdI) + hence "is_unit (x div y)" .. moreover have "x = (x div y) * y" by simp ultimately show ?thesis by blast qed @@ -218,21 +218,21 @@ lemma is_unit_neg [simp]: "is_unit (- x) \ is_unit x" - unfolding is_unit_def by simp + by simp lemma is_unit_neg_1 [simp]: "is_unit (-1)" - unfolding is_unit_def by simp + by simp end lemma is_unit_nat [simp]: "is_unit (x::nat) \ x = 1" - unfolding is_unit_def by simp + by simp lemma is_unit_int: "is_unit (x::int) \ x = 1 \ x = -1" - unfolding is_unit_def by auto + by auto text {* A Euclidean semiring is a semiring upon which the Euclidean algorithm can be @@ -741,7 +741,7 @@ by (rule sym, rule gcdI, simp_all) lemma coprime: "gcd a b = 1 \ (\d. d dvd a \ d dvd b \ is_unit d)" - by (auto simp: is_unit_def intro: coprimeI gcd_greatest dvd_gcd_D1 dvd_gcd_D2) + by (auto intro: coprimeI gcd_greatest dvd_gcd_D1 dvd_gcd_D2) lemma div_gcd_coprime: assumes nz: "a \ 0 \ b \ 0" @@ -858,7 +858,7 @@ lemma coprime_common_divisor: "gcd a b = 1 \ x dvd a \ x dvd b \ is_unit x" apply (subgoal_tac "x dvd gcd a b") - apply (simp add: is_unit_def) + apply simp apply (erule (1) gcd_greatest) done @@ -1144,14 +1144,15 @@ "lcm a b = 1 \ is_unit a \ is_unit b" proof assume "lcm a b = 1" - then show "is_unit a \ is_unit b" unfolding is_unit_def by auto + then show "is_unit a \ is_unit b" by auto next assume "is_unit a \ is_unit b" - hence "a dvd 1" and "b dvd 1" unfolding is_unit_def by simp_all - hence "is_unit (lcm a b)" unfolding is_unit_def by (rule lcm_least) + hence "a dvd 1" and "b dvd 1" by simp_all + hence "is_unit (lcm a b)" by (rule lcm_least) hence "lcm a b = normalisation_factor (lcm a b)" by (subst normalisation_factor_unit, simp_all) - also have "\ = 1" using `is_unit a \ is_unit b` by (auto simp add: is_unit_def) + also have "\ = 1" using `is_unit a \ is_unit b` + by auto finally show "lcm a b = 1" . qed @@ -1389,7 +1390,7 @@ "Lcm A = 1 \ (\x\A. is_unit x)" proof assume "Lcm A = 1" - then show "\x\A. is_unit x" unfolding is_unit_def by auto + then show "\x\A. is_unit x" by auto qed (rule LcmI [symmetric], auto) lemma Lcm_no_units: @@ -1733,7 +1734,7 @@ "normalisation_factor_nat (n::nat) = (if n = 0 then 0 else 1 :: nat)" instance proof -qed (simp_all add: is_unit_def) +qed simp_all end @@ -1749,11 +1750,11 @@ instance proof case goal2 then show ?case by (auto simp add: abs_mult nat_mult_distrib) next - case goal3 then show ?case by (simp add: zsgn_def is_unit_def) + case goal3 then show ?case by (simp add: zsgn_def) next - case goal5 then show ?case by (auto simp: zsgn_def is_unit_def) + case goal5 then show ?case by (auto simp: zsgn_def) next - case goal6 then show ?case by (auto split: abs_split simp: zsgn_def is_unit_def) + case goal6 then show ?case by (auto split: abs_split simp: zsgn_def) qed (auto simp: sgn_times split: abs_split) end