# HG changeset patch # User haftmann # Date 1436356894 -7200 # Node ID cb21b7022b00d60ea4792e3a4a86fc36d1e1cc61 # Parent 53a71c9203b21c107da2561aff93fa216139f026 moved normalization and unit_factor into Main HOL corpus diff -r 53a71c9203b2 -r cb21b7022b00 CONTRIBUTORS --- a/CONTRIBUTORS Wed Jul 08 00:04:15 2015 +0200 +++ b/CONTRIBUTORS Wed Jul 08 14:01:34 2015 +0200 @@ -15,7 +15,8 @@ * Summer 2015: Manuel Eberl and Florian Haftmann, TUM Type class hierarchy with common algebraic notions of integral - (semi)domains like units and associated elements. + (semi)domains like units, associated elements and normalization + wrt. units. Contributions to Isabelle2015 diff -r 53a71c9203b2 -r cb21b7022b00 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Wed Jul 08 00:04:15 2015 +0200 +++ b/src/HOL/Divides.thy Wed Jul 08 14:01:34 2015 +0200 @@ -1034,6 +1034,25 @@ end +instantiation nat :: normalization_semidom +begin + +definition normalize_nat + where [simp]: "normalize = (id :: nat \ nat)" + +definition unit_factor_nat + where "unit_factor n = (if n = 0 then 0 else 1 :: nat)" + +lemma unit_factor_simps [simp]: + "unit_factor 0 = (0::nat)" + "unit_factor (Suc n) = 1" + by (simp_all add: unit_factor_nat_def) + +instance + by standard (simp_all add: unit_factor_nat_def) + +end + lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \ m < n then (0, m) else let (q, r) = divmod_nat (m - n) n in (Suc q, r))" by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq) @@ -1890,6 +1909,27 @@ "is_unit (k::int) \ k = 1 \ k = - 1" by auto +instantiation int :: normalization_semidom +begin + +definition normalize_int + where [simp]: "normalize = (abs :: int \ int)" + +definition unit_factor_int + where [simp]: "unit_factor = (sgn :: int \ int)" + +instance +proof + fix k :: int + assume "k \ 0" + then have "\sgn k\ = 1" + by (cases "0::int" k rule: linorder_cases) simp_all + then show "is_unit (unit_factor k)" + by simp +qed (simp_all add: sgn_times mult_sgn_abs) + +end + text{*Basic laws about division and remainder*} lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" diff -r 53a71c9203b2 -r cb21b7022b00 src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Wed Jul 08 00:04:15 2015 +0200 +++ b/src/HOL/Library/Polynomial.thy Wed Jul 08 14:01:34 2015 +0200 @@ -7,7 +7,7 @@ section \Polynomials as type over a ring structure\ theory Polynomial -imports Main GCD "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Infinite_Set" +imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Infinite_Set" begin subsection \Auxiliary: operations for lists (later) representing coefficients\ @@ -1495,6 +1495,63 @@ shows "monom (coeff p (degree p)) 0 = p" using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff) +lemma is_unit_polyE: + assumes "is_unit p" + obtains a where "p = monom a 0" and "a \ 0" +proof - + obtain a q where "p = pCons a q" by (cases p) + with assms have "p = [:a:]" and "a \ 0" + by (simp_all add: is_unit_pCons_iff) + with that show thesis by (simp add: monom_0) +qed + +instantiation poly :: (field) normalization_semidom +begin + +definition normalize_poly :: "'a poly \ 'a poly" + where "normalize_poly p = smult (1 / coeff p (degree p)) p" + +definition unit_factor_poly :: "'a poly \ 'a poly" + where "unit_factor_poly p = monom (coeff p (degree p)) 0" + +instance +proof + fix p :: "'a poly" + show "unit_factor p * normalize p = p" + by (simp add: normalize_poly_def unit_factor_poly_def) + (simp only: mult_smult_left [symmetric] smult_monom, simp) +next + show "normalize 0 = (0::'a poly)" + by (simp add: normalize_poly_def) +next + show "unit_factor 0 = (0::'a poly)" + by (simp add: unit_factor_poly_def) +next + fix p :: "'a poly" + assume "is_unit p" + then obtain a where "p = monom a 0" and "a \ 0" + by (rule is_unit_polyE) + then show "normalize p = 1" + by (auto simp add: normalize_poly_def smult_monom degree_monom_eq) +next + fix p q :: "'a poly" + assume "q \ 0" + from \q \ 0\ have "is_unit (monom (coeff q (degree q)) 0)" + by (auto intro: is_unit_monom_0) + then show "is_unit (unit_factor q)" + by (simp add: unit_factor_poly_def) +next + fix p q :: "'a poly" + have "monom (coeff (p * q) (degree (p * q))) 0 = + monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0" + by (simp add: monom_0 coeff_degree_mult) + then show "unit_factor (p * q) = + unit_factor p * unit_factor q" + by (simp add: unit_factor_poly_def) +qed + +end + lemma degree_mod_less: "y \ 0 \ x mod y = 0 \ degree (x mod y) < degree y" using pdivmod_rel [of x y] diff -r 53a71c9203b2 -r cb21b7022b00 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Jul 08 00:04:15 2015 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Jul 08 14:01:34 2015 +0200 @@ -3,66 +3,9 @@ section \Abstract euclidean algorithm\ theory Euclidean_Algorithm -imports Complex_Main "~~/src/HOL/Library/Polynomial" "~~/src/HOL/Number_Theory/Normalization_Semidom" -begin - -lemma is_unit_polyE: - assumes "is_unit p" - obtains a where "p = monom a 0" and "a \ 0" -proof - - obtain a q where "p = pCons a q" by (cases p) - with assms have "p = [:a:]" and "a \ 0" - by (simp_all add: is_unit_pCons_iff) - with that show thesis by (simp add: monom_0) -qed - -instantiation poly :: (field) normalization_semidom +imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial" begin -definition normalize_poly :: "'a poly \ 'a poly" - where "normalize_poly p = smult (1 / coeff p (degree p)) p" - -definition unit_factor_poly :: "'a poly \ 'a poly" - where "unit_factor_poly p = monom (coeff p (degree p)) 0" - -instance -proof - fix p :: "'a poly" - show "unit_factor p * normalize p = p" - by (simp add: normalize_poly_def unit_factor_poly_def) - (simp only: mult_smult_left [symmetric] smult_monom, simp) -next - show "normalize 0 = (0::'a poly)" - by (simp add: normalize_poly_def) -next - show "unit_factor 0 = (0::'a poly)" - by (simp add: unit_factor_poly_def) -next - fix p :: "'a poly" - assume "is_unit p" - then obtain a where "p = monom a 0" and "a \ 0" - by (rule is_unit_polyE) - then show "normalize p = 1" - by (auto simp add: normalize_poly_def smult_monom degree_monom_eq) -next - fix p q :: "'a poly" - assume "q \ 0" - from \q \ 0\ have "is_unit (monom (coeff q (degree q)) 0)" - by (auto intro: is_unit_monom_0) - then show "is_unit (unit_factor q)" - by (simp add: unit_factor_poly_def) -next - fix p q :: "'a poly" - have "monom (coeff (p * q) (degree (p * q))) 0 = - monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0" - by (simp add: monom_0 coeff_degree_mult) - then show "unit_factor (p * q) = - unit_factor p * unit_factor q" - by (simp add: unit_factor_poly_def) -qed - -end - text \ A Euclidean semiring is a semiring upon which the Euclidean algorithm can be implemented. It must provide: @@ -912,7 +855,8 @@ assumes "a dvd c" and "b dvd c" and "\d. a dvd d \ b dvd d \ c dvd d" and "unit_factor c = (if c = 0 then 0 else 1)" shows "c = lcm a b" - by (rule associated_eqI) (auto simp: assms associated_def intro: lcm_least) + by (rule associated_eqI) + (auto simp: assms associated_def intro: lcm_least, simp_all add: lcm_gcd) sublocale lcm!: abel_semigroup lcm proof diff -r 53a71c9203b2 -r cb21b7022b00 src/HOL/Number_Theory/Normalization_Semidom.thy --- a/src/HOL/Number_Theory/Normalization_Semidom.thy Wed Jul 08 00:04:15 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,336 +0,0 @@ -theory Normalization_Semidom -imports Main -begin - -context algebraic_semidom -begin - -lemma is_unit_divide_mult_cancel_left: - assumes "a \ 0" and "is_unit b" - shows "a div (a * b) = 1 div b" -proof - - from assms have "a div (a * b) = a div a div b" - by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq) - with assms show ?thesis by simp -qed - -lemma is_unit_divide_mult_cancel_right: - assumes "a \ 0" and "is_unit b" - shows "a div (b * a) = 1 div b" - using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps) - -end - -class normalization_semidom = algebraic_semidom + - fixes normalize :: "'a \ 'a" - and unit_factor :: "'a \ 'a" - assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a" - assumes normalize_0 [simp]: "normalize 0 = 0" - and unit_factor_0 [simp]: "unit_factor 0 = 0" - assumes is_unit_normalize: - "is_unit a \ normalize a = 1" - assumes unit_factor_is_unit [iff]: - "a \ 0 \ is_unit (unit_factor a)" - assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b" -begin - -lemma unit_factor_dvd [simp]: - "a \ 0 \ unit_factor a dvd b" - by (rule unit_imp_dvd) simp - -lemma unit_factor_self [simp]: - "unit_factor a dvd a" - by (cases "a = 0") simp_all - -lemma normalize_mult_unit_factor [simp]: - "normalize a * unit_factor a = a" - using unit_factor_mult_normalize [of a] by (simp add: ac_simps) - -lemma normalize_eq_0_iff [simp]: - "normalize a = 0 \ a = 0" (is "?P \ ?Q") -proof - assume ?P - moreover have "unit_factor a * normalize a = a" by simp - ultimately show ?Q by simp -next - assume ?Q then show ?P by simp -qed - -lemma unit_factor_eq_0_iff [simp]: - "unit_factor a = 0 \ a = 0" (is "?P \ ?Q") -proof - assume ?P - moreover have "unit_factor a * normalize a = a" by simp - ultimately show ?Q by simp -next - assume ?Q then show ?P by simp -qed - -lemma is_unit_unit_factor: - assumes "is_unit a" shows "unit_factor a = a" -proof - - from assms have "normalize a = 1" by (rule is_unit_normalize) - moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" . - ultimately show ?thesis by simp -qed - -lemma unit_factor_1 [simp]: - "unit_factor 1 = 1" - by (rule is_unit_unit_factor) simp - -lemma normalize_1 [simp]: - "normalize 1 = 1" - by (rule is_unit_normalize) simp - -lemma normalize_1_iff: - "normalize a = 1 \ is_unit a" (is "?P \ ?Q") -proof - assume ?Q then show ?P by (rule is_unit_normalize) -next - assume ?P - then have "a \ 0" by auto - from \?P\ have "unit_factor a * normalize a = unit_factor a * 1" - by simp - then have "unit_factor a = a" - by simp - moreover have "is_unit (unit_factor a)" - using \a \ 0\ by simp - ultimately show ?Q by simp -qed - -lemma div_normalize [simp]: - "a div normalize a = unit_factor a" -proof (cases "a = 0") - case True then show ?thesis by simp -next - case False then have "normalize a \ 0" by simp - with nonzero_mult_divide_cancel_right - have "unit_factor a * normalize a div normalize a = unit_factor a" by blast - then show ?thesis by simp -qed - -lemma div_unit_factor [simp]: - "a div unit_factor a = normalize a" -proof (cases "a = 0") - case True then show ?thesis by simp -next - case False then have "unit_factor a \ 0" by simp - with nonzero_mult_divide_cancel_left - have "unit_factor a * normalize a div unit_factor a = normalize a" by blast - then show ?thesis by simp -qed - -lemma normalize_div [simp]: - "normalize a div a = 1 div unit_factor a" -proof (cases "a = 0") - case True then show ?thesis by simp -next - case False - have "normalize a div a = normalize a div (unit_factor a * normalize a)" - by simp - also have "\ = 1 div unit_factor a" - using False by (subst is_unit_divide_mult_cancel_right) simp_all - finally show ?thesis . -qed - -lemma mult_one_div_unit_factor [simp]: - "a * (1 div unit_factor b) = a div unit_factor b" - by (cases "b = 0") simp_all - -lemma normalize_mult: - "normalize (a * b) = normalize a * normalize b" -proof (cases "a = 0 \ b = 0") - case True then show ?thesis by auto -next - case False - from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" . - then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp - also have "\ = a * b div unit_factor (b * a)" by (simp add: ac_simps) - also have "\ = a * b div unit_factor b div unit_factor a" - using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric]) - also have "\ = a * (b div unit_factor b) div unit_factor a" - using False by (subst unit_div_mult_swap) simp_all - also have "\ = normalize a * normalize b" - using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric]) - finally show ?thesis . -qed - -lemma unit_factor_idem [simp]: - "unit_factor (unit_factor a) = unit_factor a" - by (cases "a = 0") (auto intro: is_unit_unit_factor) - -lemma normalize_unit_factor [simp]: - "a \ 0 \ normalize (unit_factor a) = 1" - by (rule is_unit_normalize) simp - -lemma normalize_idem [simp]: - "normalize (normalize a) = normalize a" -proof (cases "a = 0") - case True then show ?thesis by simp -next - case False - have "normalize a = normalize (unit_factor a * normalize a)" by simp - also have "\ = normalize (unit_factor a) * normalize (normalize a)" - by (simp only: normalize_mult) - finally show ?thesis using False by simp_all -qed - -lemma unit_factor_normalize [simp]: - assumes "a \ 0" - shows "unit_factor (normalize a) = 1" -proof - - from assms have "normalize a \ 0" by simp - have "unit_factor (normalize a) * normalize (normalize a) = normalize a" - by (simp only: unit_factor_mult_normalize) - then have "unit_factor (normalize a) * normalize a = normalize a" - by simp - with \normalize a \ 0\ - have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a" - by simp - with \normalize a \ 0\ - show ?thesis by simp -qed - -lemma dvd_unit_factor_div: - assumes "b dvd a" - shows "unit_factor (a div b) = unit_factor a div unit_factor b" -proof - - from assms have "a = a div b * b" - by simp - then have "unit_factor a = unit_factor (a div b * b)" - by simp - then show ?thesis - by (cases "b = 0") (simp_all add: unit_factor_mult) -qed - -lemma dvd_normalize_div: - assumes "b dvd a" - shows "normalize (a div b) = normalize a div normalize b" -proof - - from assms have "a = a div b * b" - by simp - then have "normalize a = normalize (a div b * b)" - by simp - then show ?thesis - by (cases "b = 0") (simp_all add: normalize_mult) -qed - -lemma normalize_dvd_iff [simp]: - "normalize a dvd b \ a dvd b" -proof - - have "normalize a dvd b \ unit_factor a * normalize a dvd b" - using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b] - by (cases "a = 0") simp_all - then show ?thesis by simp -qed - -lemma dvd_normalize_iff [simp]: - "a dvd normalize b \ a dvd b" -proof - - have "a dvd normalize b \ a dvd normalize b * unit_factor b" - using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"] - by (cases "b = 0") simp_all - then show ?thesis by simp -qed - -lemma associated_normalize_left [simp]: - "associated (normalize a) b \ associated a b" - by (auto simp add: associated_def) - -lemma associated_normalize_right [simp]: - "associated a (normalize b) \ associated a b" - by (auto simp add: associated_def) - -lemma associated_iff_normalize: - "associated a b \ normalize a = normalize b" (is "?P \ ?Q") -proof (cases "a = 0 \ b = 0") - case True then show ?thesis by auto -next - case False - show ?thesis - proof - assume ?P then show ?Q - by (rule associated_is_unitE) (simp add: normalize_mult is_unit_normalize) - next - from False have *: "is_unit (unit_factor a div unit_factor b)" - by auto - assume ?Q then have "unit_factor a * normalize a = unit_factor a * normalize b" - by simp - then have "a = unit_factor a * (b div unit_factor b)" - by simp - with False have "a = (unit_factor a div unit_factor b) * b" - by (simp add: unit_div_commute unit_div_mult_swap [symmetric]) - with * show ?P - by (rule is_unit_associatedI) - qed -qed - -lemma normalize_power: - "normalize (a ^ n) = normalize a ^ n" - by (induct n) (simp_all add: normalize_mult) - -lemma unit_factor_power: - "unit_factor (a ^ n) = unit_factor a ^ n" - by (induct n) (simp_all add: unit_factor_mult) - -lemma associated_eqI: - assumes "associated a b" - assumes "unit_factor a \ {0, 1}" and "unit_factor b \ {0, 1}" - shows "a = b" -proof (cases "a = 0") - case True with assms show ?thesis by simp -next - case False with assms have "b \ 0" by auto - with False assms have "unit_factor a = unit_factor b" - by simp - moreover from assms have "normalize a = normalize b" - by (simp add: associated_iff_normalize) - ultimately have "unit_factor a * normalize a = unit_factor b * normalize b" - by simp - then show ?thesis - by simp -qed - -end - -instantiation nat :: normalization_semidom -begin - -definition normalize_nat - where [simp]: "normalize = (id :: nat \ nat)" - -definition unit_factor_nat - where "unit_factor n = (if n = 0 then 0 else 1 :: nat)" - -lemma unit_factor_simps [simp]: - "unit_factor 0 = (0::nat)" - "unit_factor (Suc n) = 1" - by (simp_all add: unit_factor_nat_def) - -instance - by default (simp_all add: unit_factor_nat_def) - -end - -instantiation int :: normalization_semidom -begin - -definition normalize_int - where [simp]: "normalize = (abs :: int \ int)" - -definition unit_factor_int - where [simp]: "unit_factor = (sgn :: int \ int)" - -instance -proof - fix k :: int - assume "k \ 0" - then have "\sgn k\ = 1" - by (cases "0::int" k rule: linorder_cases) simp_all - then show "is_unit (unit_factor k)" - by simp -qed (simp_all add: sgn_times mult_sgn_abs) - -end - -end diff -r 53a71c9203b2 -r cb21b7022b00 src/HOL/Power.thy --- a/src/HOL/Power.thy Wed Jul 08 00:04:15 2015 +0200 +++ b/src/HOL/Power.thy Wed Jul 08 14:01:34 2015 +0200 @@ -306,6 +306,19 @@ end +context normalization_semidom +begin + +lemma normalize_power: + "normalize (a ^ n) = normalize a ^ n" + by (induct n) (simp_all add: normalize_mult) + +lemma unit_factor_power: + "unit_factor (a ^ n) = unit_factor a ^ n" + by (induct n) (simp_all add: unit_factor_mult) + +end + context division_ring begin diff -r 53a71c9203b2 -r cb21b7022b00 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Wed Jul 08 00:04:15 2015 +0200 +++ b/src/HOL/Rings.thy Wed Jul 08 14:01:34 2015 +0200 @@ -909,6 +909,289 @@ end +context algebraic_semidom +begin + +lemma is_unit_divide_mult_cancel_left: + assumes "a \ 0" and "is_unit b" + shows "a div (a * b) = 1 div b" +proof - + from assms have "a div (a * b) = a div a div b" + by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq) + with assms show ?thesis by simp +qed + +lemma is_unit_divide_mult_cancel_right: + assumes "a \ 0" and "is_unit b" + shows "a div (b * a) = 1 div b" + using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps) + +end + +class normalization_semidom = algebraic_semidom + + fixes normalize :: "'a \ 'a" + and unit_factor :: "'a \ 'a" + assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a" + assumes normalize_0 [simp]: "normalize 0 = 0" + and unit_factor_0 [simp]: "unit_factor 0 = 0" + assumes is_unit_normalize: + "is_unit a \ normalize a = 1" + assumes unit_factor_is_unit [iff]: + "a \ 0 \ is_unit (unit_factor a)" + assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b" +begin + +lemma unit_factor_dvd [simp]: + "a \ 0 \ unit_factor a dvd b" + by (rule unit_imp_dvd) simp + +lemma unit_factor_self [simp]: + "unit_factor a dvd a" + by (cases "a = 0") simp_all + +lemma normalize_mult_unit_factor [simp]: + "normalize a * unit_factor a = a" + using unit_factor_mult_normalize [of a] by (simp add: ac_simps) + +lemma normalize_eq_0_iff [simp]: + "normalize a = 0 \ a = 0" (is "?P \ ?Q") +proof + assume ?P + moreover have "unit_factor a * normalize a = a" by simp + ultimately show ?Q by simp +next + assume ?Q then show ?P by simp +qed + +lemma unit_factor_eq_0_iff [simp]: + "unit_factor a = 0 \ a = 0" (is "?P \ ?Q") +proof + assume ?P + moreover have "unit_factor a * normalize a = a" by simp + ultimately show ?Q by simp +next + assume ?Q then show ?P by simp +qed + +lemma is_unit_unit_factor: + assumes "is_unit a" shows "unit_factor a = a" +proof - + from assms have "normalize a = 1" by (rule is_unit_normalize) + moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" . + ultimately show ?thesis by simp +qed + +lemma unit_factor_1 [simp]: + "unit_factor 1 = 1" + by (rule is_unit_unit_factor) simp + +lemma normalize_1 [simp]: + "normalize 1 = 1" + by (rule is_unit_normalize) simp + +lemma normalize_1_iff: + "normalize a = 1 \ is_unit a" (is "?P \ ?Q") +proof + assume ?Q then show ?P by (rule is_unit_normalize) +next + assume ?P + then have "a \ 0" by auto + from \?P\ have "unit_factor a * normalize a = unit_factor a * 1" + by simp + then have "unit_factor a = a" + by simp + moreover have "is_unit (unit_factor a)" + using \a \ 0\ by simp + ultimately show ?Q by simp +qed + +lemma div_normalize [simp]: + "a div normalize a = unit_factor a" +proof (cases "a = 0") + case True then show ?thesis by simp +next + case False then have "normalize a \ 0" by simp + with nonzero_mult_divide_cancel_right + have "unit_factor a * normalize a div normalize a = unit_factor a" by blast + then show ?thesis by simp +qed + +lemma div_unit_factor [simp]: + "a div unit_factor a = normalize a" +proof (cases "a = 0") + case True then show ?thesis by simp +next + case False then have "unit_factor a \ 0" by simp + with nonzero_mult_divide_cancel_left + have "unit_factor a * normalize a div unit_factor a = normalize a" by blast + then show ?thesis by simp +qed + +lemma normalize_div [simp]: + "normalize a div a = 1 div unit_factor a" +proof (cases "a = 0") + case True then show ?thesis by simp +next + case False + have "normalize a div a = normalize a div (unit_factor a * normalize a)" + by simp + also have "\ = 1 div unit_factor a" + using False by (subst is_unit_divide_mult_cancel_right) simp_all + finally show ?thesis . +qed + +lemma mult_one_div_unit_factor [simp]: + "a * (1 div unit_factor b) = a div unit_factor b" + by (cases "b = 0") simp_all + +lemma normalize_mult: + "normalize (a * b) = normalize a * normalize b" +proof (cases "a = 0 \ b = 0") + case True then show ?thesis by auto +next + case False + from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" . + then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp + also have "\ = a * b div unit_factor (b * a)" by (simp add: ac_simps) + also have "\ = a * b div unit_factor b div unit_factor a" + using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric]) + also have "\ = a * (b div unit_factor b) div unit_factor a" + using False by (subst unit_div_mult_swap) simp_all + also have "\ = normalize a * normalize b" + using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric]) + finally show ?thesis . +qed + +lemma unit_factor_idem [simp]: + "unit_factor (unit_factor a) = unit_factor a" + by (cases "a = 0") (auto intro: is_unit_unit_factor) + +lemma normalize_unit_factor [simp]: + "a \ 0 \ normalize (unit_factor a) = 1" + by (rule is_unit_normalize) simp + +lemma normalize_idem [simp]: + "normalize (normalize a) = normalize a" +proof (cases "a = 0") + case True then show ?thesis by simp +next + case False + have "normalize a = normalize (unit_factor a * normalize a)" by simp + also have "\ = normalize (unit_factor a) * normalize (normalize a)" + by (simp only: normalize_mult) + finally show ?thesis using False by simp_all +qed + +lemma unit_factor_normalize [simp]: + assumes "a \ 0" + shows "unit_factor (normalize a) = 1" +proof - + from assms have "normalize a \ 0" by simp + have "unit_factor (normalize a) * normalize (normalize a) = normalize a" + by (simp only: unit_factor_mult_normalize) + then have "unit_factor (normalize a) * normalize a = normalize a" + by simp + with \normalize a \ 0\ + have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a" + by simp + with \normalize a \ 0\ + show ?thesis by simp +qed + +lemma dvd_unit_factor_div: + assumes "b dvd a" + shows "unit_factor (a div b) = unit_factor a div unit_factor b" +proof - + from assms have "a = a div b * b" + by simp + then have "unit_factor a = unit_factor (a div b * b)" + by simp + then show ?thesis + by (cases "b = 0") (simp_all add: unit_factor_mult) +qed + +lemma dvd_normalize_div: + assumes "b dvd a" + shows "normalize (a div b) = normalize a div normalize b" +proof - + from assms have "a = a div b * b" + by simp + then have "normalize a = normalize (a div b * b)" + by simp + then show ?thesis + by (cases "b = 0") (simp_all add: normalize_mult) +qed + +lemma normalize_dvd_iff [simp]: + "normalize a dvd b \ a dvd b" +proof - + have "normalize a dvd b \ unit_factor a * normalize a dvd b" + using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b] + by (cases "a = 0") simp_all + then show ?thesis by simp +qed + +lemma dvd_normalize_iff [simp]: + "a dvd normalize b \ a dvd b" +proof - + have "a dvd normalize b \ a dvd normalize b * unit_factor b" + using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"] + by (cases "b = 0") simp_all + then show ?thesis by simp +qed + +lemma associated_normalize_left [simp]: + "associated (normalize a) b \ associated a b" + by (auto simp add: associated_def) + +lemma associated_normalize_right [simp]: + "associated a (normalize b) \ associated a b" + by (auto simp add: associated_def) + +lemma associated_iff_normalize: + "associated a b \ normalize a = normalize b" (is "?P \ ?Q") +proof (cases "a = 0 \ b = 0") + case True then show ?thesis by auto +next + case False + show ?thesis + proof + assume ?P then show ?Q + by (rule associated_is_unitE) (simp add: normalize_mult is_unit_normalize) + next + from False have *: "is_unit (unit_factor a div unit_factor b)" + by auto + assume ?Q then have "unit_factor a * normalize a = unit_factor a * normalize b" + by simp + then have "a = unit_factor a * (b div unit_factor b)" + by simp + with False have "a = (unit_factor a div unit_factor b) * b" + by (simp add: unit_div_commute unit_div_mult_swap [symmetric]) + with * show ?P + by (rule is_unit_associatedI) + qed +qed + +lemma associated_eqI: + assumes "associated a b" + assumes "a \ 0 \ unit_factor a = 1" and "b \ 0 \ unit_factor b = 1" + shows "a = b" +proof (cases "a = 0") + case True with assms show ?thesis by simp +next + case False with assms have "b \ 0" by auto + with False assms have "unit_factor a = unit_factor b" + by simp + moreover from assms have "normalize a = normalize b" + by (simp add: associated_iff_normalize) + ultimately have "unit_factor a * normalize a = unit_factor b * normalize b" + by simp + then show ?thesis + by simp +qed + +end + class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add + assumes mult_left_mono: "a \ b \ 0 \ c \ c * a \ c * b" assumes mult_right_mono: "a \ b \ 0 \ c \ a * c \ b * c"