moved normalization and unit_factor into Main HOL corpus
authorhaftmann
Wed Jul 08 14:01:34 2015 +0200 (2015-07-08)
changeset 60685cb21b7022b00
parent 60684 53a71c9203b2
child 60686 ea5bc46c11e6
moved normalization and unit_factor into Main HOL corpus
CONTRIBUTORS
src/HOL/Divides.thy
src/HOL/Library/Polynomial.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Number_Theory/Normalization_Semidom.thy
src/HOL/Power.thy
src/HOL/Rings.thy
     1.1 --- a/CONTRIBUTORS	Wed Jul 08 00:04:15 2015 +0200
     1.2 +++ b/CONTRIBUTORS	Wed Jul 08 14:01:34 2015 +0200
     1.3 @@ -15,7 +15,8 @@
     1.4  
     1.5  * Summer 2015: Manuel Eberl and Florian Haftmann, TUM
     1.6    Type class hierarchy with common algebraic notions of integral
     1.7 -  (semi)domains like units and associated elements.
     1.8 +  (semi)domains like units, associated elements and normalization
     1.9 +  wrt. units.
    1.10  
    1.11  
    1.12  Contributions to Isabelle2015
     2.1 --- a/src/HOL/Divides.thy	Wed Jul 08 00:04:15 2015 +0200
     2.2 +++ b/src/HOL/Divides.thy	Wed Jul 08 14:01:34 2015 +0200
     2.3 @@ -1034,6 +1034,25 @@
     2.4  
     2.5  end
     2.6  
     2.7 +instantiation nat :: normalization_semidom
     2.8 +begin
     2.9 +
    2.10 +definition normalize_nat
    2.11 +  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
    2.12 +
    2.13 +definition unit_factor_nat
    2.14 +  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
    2.15 +
    2.16 +lemma unit_factor_simps [simp]:
    2.17 +  "unit_factor 0 = (0::nat)"
    2.18 +  "unit_factor (Suc n) = 1"
    2.19 +  by (simp_all add: unit_factor_nat_def)
    2.20 +
    2.21 +instance
    2.22 +  by standard (simp_all add: unit_factor_nat_def)
    2.23 +  
    2.24 +end
    2.25 +
    2.26  lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
    2.27    let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
    2.28    by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
    2.29 @@ -1890,6 +1909,27 @@
    2.30    "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
    2.31    by auto
    2.32  
    2.33 +instantiation int :: normalization_semidom
    2.34 +begin
    2.35 +
    2.36 +definition normalize_int
    2.37 +  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
    2.38 +
    2.39 +definition unit_factor_int
    2.40 +  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
    2.41 +
    2.42 +instance
    2.43 +proof
    2.44 +  fix k :: int
    2.45 +  assume "k \<noteq> 0"
    2.46 +  then have "\<bar>sgn k\<bar> = 1"
    2.47 +    by (cases "0::int" k rule: linorder_cases) simp_all
    2.48 +  then show "is_unit (unit_factor k)"
    2.49 +    by simp
    2.50 +qed (simp_all add: sgn_times mult_sgn_abs)
    2.51 +  
    2.52 +end
    2.53 +  
    2.54  text{*Basic laws about division and remainder*}
    2.55  
    2.56  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
     3.1 --- a/src/HOL/Library/Polynomial.thy	Wed Jul 08 00:04:15 2015 +0200
     3.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Jul 08 14:01:34 2015 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  section \<open>Polynomials as type over a ring structure\<close>
     3.5  
     3.6  theory Polynomial
     3.7 -imports Main GCD "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Infinite_Set"
     3.8 +imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Infinite_Set"
     3.9  begin
    3.10  
    3.11  subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
    3.12 @@ -1495,6 +1495,63 @@
    3.13    shows "monom (coeff p (degree p)) 0 = p"
    3.14    using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
    3.15  
    3.16 +lemma is_unit_polyE:
    3.17 +  assumes "is_unit p"
    3.18 +  obtains a where "p = monom a 0" and "a \<noteq> 0"
    3.19 +proof -
    3.20 +  obtain a q where "p = pCons a q" by (cases p)
    3.21 +  with assms have "p = [:a:]" and "a \<noteq> 0"
    3.22 +    by (simp_all add: is_unit_pCons_iff)
    3.23 +  with that show thesis by (simp add: monom_0)
    3.24 +qed
    3.25 +
    3.26 +instantiation poly :: (field) normalization_semidom
    3.27 +begin
    3.28 +
    3.29 +definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
    3.30 +  where "normalize_poly p = smult (1 / coeff p (degree p)) p"
    3.31 +
    3.32 +definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
    3.33 +  where "unit_factor_poly p = monom (coeff p (degree p)) 0"
    3.34 +
    3.35 +instance
    3.36 +proof
    3.37 +  fix p :: "'a poly"
    3.38 +  show "unit_factor p * normalize p = p"
    3.39 +    by (simp add: normalize_poly_def unit_factor_poly_def)
    3.40 +      (simp only: mult_smult_left [symmetric] smult_monom, simp)
    3.41 +next
    3.42 +  show "normalize 0 = (0::'a poly)"
    3.43 +    by (simp add: normalize_poly_def)
    3.44 +next
    3.45 +  show "unit_factor 0 = (0::'a poly)"
    3.46 +    by (simp add: unit_factor_poly_def)
    3.47 +next
    3.48 +  fix p :: "'a poly"
    3.49 +  assume "is_unit p"
    3.50 +  then obtain a where "p = monom a 0" and "a \<noteq> 0"
    3.51 +    by (rule is_unit_polyE)
    3.52 +  then show "normalize p = 1"
    3.53 +    by (auto simp add: normalize_poly_def smult_monom degree_monom_eq)
    3.54 +next
    3.55 +  fix p q :: "'a poly"
    3.56 +  assume "q \<noteq> 0"
    3.57 +  from \<open>q \<noteq> 0\<close> have "is_unit (monom (coeff q (degree q)) 0)"
    3.58 +    by (auto intro: is_unit_monom_0)
    3.59 +  then show "is_unit (unit_factor q)"
    3.60 +    by (simp add: unit_factor_poly_def)
    3.61 +next
    3.62 +  fix p q :: "'a poly"
    3.63 +  have "monom (coeff (p * q) (degree (p * q))) 0 =
    3.64 +    monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
    3.65 +    by (simp add: monom_0 coeff_degree_mult)
    3.66 +  then show "unit_factor (p * q) =
    3.67 +    unit_factor p * unit_factor q"
    3.68 +    by (simp add: unit_factor_poly_def)
    3.69 +qed
    3.70 +
    3.71 +end
    3.72 +
    3.73  lemma degree_mod_less:
    3.74    "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
    3.75    using pdivmod_rel [of x y]
     4.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 00:04:15 2015 +0200
     4.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:34 2015 +0200
     4.3 @@ -3,66 +3,9 @@
     4.4  section \<open>Abstract euclidean algorithm\<close>
     4.5  
     4.6  theory Euclidean_Algorithm
     4.7 -imports Complex_Main "~~/src/HOL/Library/Polynomial" "~~/src/HOL/Number_Theory/Normalization_Semidom"
     4.8 +imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial"
     4.9  begin
    4.10  
    4.11 -lemma is_unit_polyE:
    4.12 -  assumes "is_unit p"
    4.13 -  obtains a where "p = monom a 0" and "a \<noteq> 0"
    4.14 -proof -
    4.15 -  obtain a q where "p = pCons a q" by (cases p)
    4.16 -  with assms have "p = [:a:]" and "a \<noteq> 0"
    4.17 -    by (simp_all add: is_unit_pCons_iff)
    4.18 -  with that show thesis by (simp add: monom_0)
    4.19 -qed
    4.20 -
    4.21 -instantiation poly :: (field) normalization_semidom
    4.22 -begin
    4.23 -
    4.24 -definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
    4.25 -  where "normalize_poly p = smult (1 / coeff p (degree p)) p"
    4.26 -
    4.27 -definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
    4.28 -  where "unit_factor_poly p = monom (coeff p (degree p)) 0"
    4.29 -
    4.30 -instance
    4.31 -proof
    4.32 -  fix p :: "'a poly"
    4.33 -  show "unit_factor p * normalize p = p"
    4.34 -    by (simp add: normalize_poly_def unit_factor_poly_def)
    4.35 -      (simp only: mult_smult_left [symmetric] smult_monom, simp)
    4.36 -next
    4.37 -  show "normalize 0 = (0::'a poly)"
    4.38 -    by (simp add: normalize_poly_def)
    4.39 -next
    4.40 -  show "unit_factor 0 = (0::'a poly)"
    4.41 -    by (simp add: unit_factor_poly_def)
    4.42 -next
    4.43 -  fix p :: "'a poly"
    4.44 -  assume "is_unit p"
    4.45 -  then obtain a where "p = monom a 0" and "a \<noteq> 0"
    4.46 -    by (rule is_unit_polyE)
    4.47 -  then show "normalize p = 1"
    4.48 -    by (auto simp add: normalize_poly_def smult_monom degree_monom_eq)
    4.49 -next
    4.50 -  fix p q :: "'a poly"
    4.51 -  assume "q \<noteq> 0"
    4.52 -  from \<open>q \<noteq> 0\<close> have "is_unit (monom (coeff q (degree q)) 0)"
    4.53 -    by (auto intro: is_unit_monom_0)
    4.54 -  then show "is_unit (unit_factor q)"
    4.55 -    by (simp add: unit_factor_poly_def)
    4.56 -next
    4.57 -  fix p q :: "'a poly"
    4.58 -  have "monom (coeff (p * q) (degree (p * q))) 0 =
    4.59 -    monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
    4.60 -    by (simp add: monom_0 coeff_degree_mult)
    4.61 -  then show "unit_factor (p * q) =
    4.62 -    unit_factor p * unit_factor q"
    4.63 -    by (simp add: unit_factor_poly_def)
    4.64 -qed
    4.65 -
    4.66 -end
    4.67 -
    4.68  text \<open>
    4.69    A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
    4.70    implemented. It must provide:
    4.71 @@ -912,7 +855,8 @@
    4.72    assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d"
    4.73      and "unit_factor c = (if c = 0 then 0 else 1)"
    4.74    shows "c = lcm a b"
    4.75 -  by (rule associated_eqI) (auto simp: assms associated_def intro: lcm_least)
    4.76 +  by (rule associated_eqI)
    4.77 +    (auto simp: assms associated_def intro: lcm_least, simp_all add: lcm_gcd)
    4.78  
    4.79  sublocale lcm!: abel_semigroup lcm
    4.80  proof
     5.1 --- a/src/HOL/Number_Theory/Normalization_Semidom.thy	Wed Jul 08 00:04:15 2015 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,336 +0,0 @@
     5.4 -theory Normalization_Semidom
     5.5 -imports Main
     5.6 -begin
     5.7 -
     5.8 -context algebraic_semidom
     5.9 -begin
    5.10 -
    5.11 -lemma is_unit_divide_mult_cancel_left:
    5.12 -  assumes "a \<noteq> 0" and "is_unit b"
    5.13 -  shows "a div (a * b) = 1 div b"
    5.14 -proof -
    5.15 -  from assms have "a div (a * b) = a div a div b"
    5.16 -    by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
    5.17 -  with assms show ?thesis by simp
    5.18 -qed
    5.19 -
    5.20 -lemma is_unit_divide_mult_cancel_right:
    5.21 -  assumes "a \<noteq> 0" and "is_unit b"
    5.22 -  shows "a div (b * a) = 1 div b"
    5.23 -  using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)
    5.24 -
    5.25 -end
    5.26 -
    5.27 -class normalization_semidom = algebraic_semidom +
    5.28 -  fixes normalize :: "'a \<Rightarrow> 'a"
    5.29 -    and unit_factor :: "'a \<Rightarrow> 'a"
    5.30 -  assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
    5.31 -  assumes normalize_0 [simp]: "normalize 0 = 0"
    5.32 -    and unit_factor_0 [simp]: "unit_factor 0 = 0"
    5.33 -  assumes is_unit_normalize:
    5.34 -    "is_unit a  \<Longrightarrow> normalize a = 1"
    5.35 -  assumes unit_factor_is_unit [iff]: 
    5.36 -    "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
    5.37 -  assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
    5.38 -begin
    5.39 -
    5.40 -lemma unit_factor_dvd [simp]:
    5.41 -  "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
    5.42 -  by (rule unit_imp_dvd) simp
    5.43 -
    5.44 -lemma unit_factor_self [simp]:
    5.45 -  "unit_factor a dvd a"
    5.46 -  by (cases "a = 0") simp_all 
    5.47 -  
    5.48 -lemma normalize_mult_unit_factor [simp]:
    5.49 -  "normalize a * unit_factor a = a"
    5.50 -  using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
    5.51 -
    5.52 -lemma normalize_eq_0_iff [simp]:
    5.53 -  "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
    5.54 -proof
    5.55 -  assume ?P
    5.56 -  moreover have "unit_factor a * normalize a = a" by simp
    5.57 -  ultimately show ?Q by simp 
    5.58 -next
    5.59 -  assume ?Q then show ?P by simp
    5.60 -qed
    5.61 -
    5.62 -lemma unit_factor_eq_0_iff [simp]:
    5.63 -  "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
    5.64 -proof
    5.65 -  assume ?P
    5.66 -  moreover have "unit_factor a * normalize a = a" by simp
    5.67 -  ultimately show ?Q by simp 
    5.68 -next
    5.69 -  assume ?Q then show ?P by simp
    5.70 -qed
    5.71 -
    5.72 -lemma is_unit_unit_factor:
    5.73 -  assumes "is_unit a" shows "unit_factor a = a"
    5.74 -proof - 
    5.75 -  from assms have "normalize a = 1" by (rule is_unit_normalize)
    5.76 -  moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
    5.77 -  ultimately show ?thesis by simp
    5.78 -qed
    5.79 -
    5.80 -lemma unit_factor_1 [simp]:
    5.81 -  "unit_factor 1 = 1"
    5.82 -  by (rule is_unit_unit_factor) simp
    5.83 -
    5.84 -lemma normalize_1 [simp]:
    5.85 -  "normalize 1 = 1"
    5.86 -  by (rule is_unit_normalize) simp
    5.87 -
    5.88 -lemma normalize_1_iff:
    5.89 -  "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
    5.90 -proof
    5.91 -  assume ?Q then show ?P by (rule is_unit_normalize)
    5.92 -next
    5.93 -  assume ?P
    5.94 -  then have "a \<noteq> 0" by auto
    5.95 -  from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1"
    5.96 -    by simp
    5.97 -  then have "unit_factor a = a"
    5.98 -    by simp
    5.99 -  moreover have "is_unit (unit_factor a)"
   5.100 -    using \<open>a \<noteq> 0\<close> by simp
   5.101 -  ultimately show ?Q by simp
   5.102 -qed
   5.103 -  
   5.104 -lemma div_normalize [simp]:
   5.105 -  "a div normalize a = unit_factor a"
   5.106 -proof (cases "a = 0")
   5.107 -  case True then show ?thesis by simp
   5.108 -next
   5.109 -  case False then have "normalize a \<noteq> 0" by simp 
   5.110 -  with nonzero_mult_divide_cancel_right
   5.111 -  have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
   5.112 -  then show ?thesis by simp
   5.113 -qed
   5.114 -
   5.115 -lemma div_unit_factor [simp]:
   5.116 -  "a div unit_factor a = normalize a"
   5.117 -proof (cases "a = 0")
   5.118 -  case True then show ?thesis by simp
   5.119 -next
   5.120 -  case False then have "unit_factor a \<noteq> 0" by simp 
   5.121 -  with nonzero_mult_divide_cancel_left
   5.122 -  have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
   5.123 -  then show ?thesis by simp
   5.124 -qed
   5.125 -
   5.126 -lemma normalize_div [simp]:
   5.127 -  "normalize a div a = 1 div unit_factor a"
   5.128 -proof (cases "a = 0")
   5.129 -  case True then show ?thesis by simp
   5.130 -next
   5.131 -  case False
   5.132 -  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
   5.133 -    by simp
   5.134 -  also have "\<dots> = 1 div unit_factor a"
   5.135 -    using False by (subst is_unit_divide_mult_cancel_right) simp_all
   5.136 -  finally show ?thesis .
   5.137 -qed
   5.138 -
   5.139 -lemma mult_one_div_unit_factor [simp]:
   5.140 -  "a * (1 div unit_factor b) = a div unit_factor b"
   5.141 -  by (cases "b = 0") simp_all
   5.142 -
   5.143 -lemma normalize_mult:
   5.144 -  "normalize (a * b) = normalize a * normalize b"
   5.145 -proof (cases "a = 0 \<or> b = 0")
   5.146 -  case True then show ?thesis by auto
   5.147 -next
   5.148 -  case False
   5.149 -  from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" .
   5.150 -  then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp
   5.151 -  also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps)
   5.152 -  also have "\<dots> = a * b div unit_factor b div unit_factor a"
   5.153 -    using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
   5.154 -  also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
   5.155 -    using False by (subst unit_div_mult_swap) simp_all
   5.156 -  also have "\<dots> = normalize a * normalize b"
   5.157 -    using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
   5.158 -  finally show ?thesis .
   5.159 -qed
   5.160 - 
   5.161 -lemma unit_factor_idem [simp]:
   5.162 -  "unit_factor (unit_factor a) = unit_factor a"
   5.163 -  by (cases "a = 0") (auto intro: is_unit_unit_factor)
   5.164 -
   5.165 -lemma normalize_unit_factor [simp]:
   5.166 -  "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
   5.167 -  by (rule is_unit_normalize) simp
   5.168 -  
   5.169 -lemma normalize_idem [simp]:
   5.170 -  "normalize (normalize a) = normalize a"
   5.171 -proof (cases "a = 0")
   5.172 -  case True then show ?thesis by simp
   5.173 -next
   5.174 -  case False
   5.175 -  have "normalize a = normalize (unit_factor a * normalize a)" by simp
   5.176 -  also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
   5.177 -    by (simp only: normalize_mult)
   5.178 -  finally show ?thesis using False by simp_all
   5.179 -qed
   5.180 -
   5.181 -lemma unit_factor_normalize [simp]:
   5.182 -  assumes "a \<noteq> 0"
   5.183 -  shows "unit_factor (normalize a) = 1"
   5.184 -proof -
   5.185 -  from assms have "normalize a \<noteq> 0" by simp
   5.186 -  have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
   5.187 -    by (simp only: unit_factor_mult_normalize)
   5.188 -  then have "unit_factor (normalize a) * normalize a = normalize a"
   5.189 -    by simp
   5.190 -  with \<open>normalize a \<noteq> 0\<close>
   5.191 -  have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
   5.192 -    by simp
   5.193 -  with \<open>normalize a \<noteq> 0\<close>
   5.194 -  show ?thesis by simp
   5.195 -qed
   5.196 -
   5.197 -lemma dvd_unit_factor_div:
   5.198 -  assumes "b dvd a"
   5.199 -  shows "unit_factor (a div b) = unit_factor a div unit_factor b"
   5.200 -proof -
   5.201 -  from assms have "a = a div b * b"
   5.202 -    by simp
   5.203 -  then have "unit_factor a = unit_factor (a div b * b)"
   5.204 -    by simp
   5.205 -  then show ?thesis
   5.206 -    by (cases "b = 0") (simp_all add: unit_factor_mult)
   5.207 -qed
   5.208 -
   5.209 -lemma dvd_normalize_div:
   5.210 -  assumes "b dvd a"
   5.211 -  shows "normalize (a div b) = normalize a div normalize b"
   5.212 -proof -
   5.213 -  from assms have "a = a div b * b"
   5.214 -    by simp
   5.215 -  then have "normalize a = normalize (a div b * b)"
   5.216 -    by simp
   5.217 -  then show ?thesis
   5.218 -    by (cases "b = 0") (simp_all add: normalize_mult)
   5.219 -qed
   5.220 -
   5.221 -lemma normalize_dvd_iff [simp]:
   5.222 -  "normalize a dvd b \<longleftrightarrow> a dvd b"
   5.223 -proof -
   5.224 -  have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
   5.225 -    using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
   5.226 -      by (cases "a = 0") simp_all
   5.227 -  then show ?thesis by simp
   5.228 -qed
   5.229 -
   5.230 -lemma dvd_normalize_iff [simp]:
   5.231 -  "a dvd normalize b \<longleftrightarrow> a dvd b"
   5.232 -proof -
   5.233 -  have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
   5.234 -    using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
   5.235 -      by (cases "b = 0") simp_all
   5.236 -  then show ?thesis by simp
   5.237 -qed
   5.238 -
   5.239 -lemma associated_normalize_left [simp]:
   5.240 -  "associated (normalize a) b \<longleftrightarrow> associated a b"
   5.241 -  by (auto simp add: associated_def)
   5.242 -
   5.243 -lemma associated_normalize_right [simp]:
   5.244 -  "associated a (normalize b) \<longleftrightarrow> associated a b"
   5.245 -  by (auto simp add: associated_def)
   5.246 -
   5.247 -lemma associated_iff_normalize:
   5.248 -  "associated a b \<longleftrightarrow> normalize a = normalize b" (is "?P \<longleftrightarrow> ?Q")
   5.249 -proof (cases "a = 0 \<or> b = 0")
   5.250 -  case True then show ?thesis by auto
   5.251 -next
   5.252 -  case False
   5.253 -  show ?thesis
   5.254 -  proof
   5.255 -    assume ?P then show ?Q
   5.256 -      by (rule associated_is_unitE) (simp add: normalize_mult is_unit_normalize)
   5.257 -  next
   5.258 -    from False have *: "is_unit (unit_factor a div unit_factor b)"
   5.259 -      by auto
   5.260 -    assume ?Q then have "unit_factor a * normalize a = unit_factor a * normalize b"
   5.261 -      by simp
   5.262 -    then have "a = unit_factor a * (b div unit_factor b)"
   5.263 -      by simp
   5.264 -    with False have "a = (unit_factor a div unit_factor b) * b"
   5.265 -      by (simp add: unit_div_commute unit_div_mult_swap [symmetric])
   5.266 -    with * show ?P 
   5.267 -      by (rule is_unit_associatedI)
   5.268 -  qed
   5.269 -qed
   5.270 -
   5.271 -lemma normalize_power:
   5.272 -  "normalize (a ^ n) = normalize a ^ n"
   5.273 -  by (induct n) (simp_all add: normalize_mult)
   5.274 -
   5.275 -lemma unit_factor_power:
   5.276 -  "unit_factor (a ^ n) = unit_factor a ^ n"
   5.277 -  by (induct n) (simp_all add: unit_factor_mult)
   5.278 -
   5.279 -lemma associated_eqI:
   5.280 -  assumes "associated a b"
   5.281 -  assumes "unit_factor a \<in> {0, 1}" and "unit_factor b \<in> {0, 1}"
   5.282 -  shows "a = b"
   5.283 -proof (cases "a = 0")
   5.284 -  case True with assms show ?thesis by simp
   5.285 -next
   5.286 -  case False with assms have "b \<noteq> 0" by auto
   5.287 -  with False assms have "unit_factor a = unit_factor b"
   5.288 -    by simp
   5.289 -  moreover from assms have "normalize a = normalize b"
   5.290 -    by (simp add: associated_iff_normalize)
   5.291 -  ultimately have "unit_factor a * normalize a = unit_factor b * normalize b"
   5.292 -    by simp
   5.293 -  then show ?thesis
   5.294 -    by simp
   5.295 -qed
   5.296 -
   5.297 -end
   5.298 -
   5.299 -instantiation nat :: normalization_semidom
   5.300 -begin
   5.301 -
   5.302 -definition normalize_nat
   5.303 -  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
   5.304 -
   5.305 -definition unit_factor_nat
   5.306 -  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
   5.307 -
   5.308 -lemma unit_factor_simps [simp]:
   5.309 -  "unit_factor 0 = (0::nat)"
   5.310 -  "unit_factor (Suc n) = 1"
   5.311 -  by (simp_all add: unit_factor_nat_def)
   5.312 -
   5.313 -instance
   5.314 -  by default (simp_all add: unit_factor_nat_def)
   5.315 -  
   5.316 -end
   5.317 -
   5.318 -instantiation int :: normalization_semidom
   5.319 -begin
   5.320 -
   5.321 -definition normalize_int
   5.322 -  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
   5.323 -
   5.324 -definition unit_factor_int
   5.325 -  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
   5.326 -
   5.327 -instance
   5.328 -proof
   5.329 -  fix k :: int
   5.330 -  assume "k \<noteq> 0"
   5.331 -  then have "\<bar>sgn k\<bar> = 1"
   5.332 -    by (cases "0::int" k rule: linorder_cases) simp_all
   5.333 -  then show "is_unit (unit_factor k)"
   5.334 -    by simp
   5.335 -qed (simp_all add: sgn_times mult_sgn_abs)
   5.336 -  
   5.337 -end
   5.338 -
   5.339 -end
     6.1 --- a/src/HOL/Power.thy	Wed Jul 08 00:04:15 2015 +0200
     6.2 +++ b/src/HOL/Power.thy	Wed Jul 08 14:01:34 2015 +0200
     6.3 @@ -306,6 +306,19 @@
     6.4  
     6.5  end
     6.6  
     6.7 +context normalization_semidom
     6.8 +begin
     6.9 +
    6.10 +lemma normalize_power:
    6.11 +  "normalize (a ^ n) = normalize a ^ n"
    6.12 +  by (induct n) (simp_all add: normalize_mult)
    6.13 +
    6.14 +lemma unit_factor_power:
    6.15 +  "unit_factor (a ^ n) = unit_factor a ^ n"
    6.16 +  by (induct n) (simp_all add: unit_factor_mult)
    6.17 +
    6.18 +end
    6.19 +
    6.20  context division_ring
    6.21  begin
    6.22  
     7.1 --- a/src/HOL/Rings.thy	Wed Jul 08 00:04:15 2015 +0200
     7.2 +++ b/src/HOL/Rings.thy	Wed Jul 08 14:01:34 2015 +0200
     7.3 @@ -909,6 +909,289 @@
     7.4  
     7.5  end
     7.6  
     7.7 +context algebraic_semidom
     7.8 +begin
     7.9 +
    7.10 +lemma is_unit_divide_mult_cancel_left:
    7.11 +  assumes "a \<noteq> 0" and "is_unit b"
    7.12 +  shows "a div (a * b) = 1 div b"
    7.13 +proof -
    7.14 +  from assms have "a div (a * b) = a div a div b"
    7.15 +    by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
    7.16 +  with assms show ?thesis by simp
    7.17 +qed
    7.18 +
    7.19 +lemma is_unit_divide_mult_cancel_right:
    7.20 +  assumes "a \<noteq> 0" and "is_unit b"
    7.21 +  shows "a div (b * a) = 1 div b"
    7.22 +  using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)
    7.23 +
    7.24 +end
    7.25 +
    7.26 +class normalization_semidom = algebraic_semidom +
    7.27 +  fixes normalize :: "'a \<Rightarrow> 'a"
    7.28 +    and unit_factor :: "'a \<Rightarrow> 'a"
    7.29 +  assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
    7.30 +  assumes normalize_0 [simp]: "normalize 0 = 0"
    7.31 +    and unit_factor_0 [simp]: "unit_factor 0 = 0"
    7.32 +  assumes is_unit_normalize:
    7.33 +    "is_unit a  \<Longrightarrow> normalize a = 1"
    7.34 +  assumes unit_factor_is_unit [iff]: 
    7.35 +    "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
    7.36 +  assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
    7.37 +begin
    7.38 +
    7.39 +lemma unit_factor_dvd [simp]:
    7.40 +  "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
    7.41 +  by (rule unit_imp_dvd) simp
    7.42 +
    7.43 +lemma unit_factor_self [simp]:
    7.44 +  "unit_factor a dvd a"
    7.45 +  by (cases "a = 0") simp_all 
    7.46 +  
    7.47 +lemma normalize_mult_unit_factor [simp]:
    7.48 +  "normalize a * unit_factor a = a"
    7.49 +  using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
    7.50 +
    7.51 +lemma normalize_eq_0_iff [simp]:
    7.52 +  "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
    7.53 +proof
    7.54 +  assume ?P
    7.55 +  moreover have "unit_factor a * normalize a = a" by simp
    7.56 +  ultimately show ?Q by simp 
    7.57 +next
    7.58 +  assume ?Q then show ?P by simp
    7.59 +qed
    7.60 +
    7.61 +lemma unit_factor_eq_0_iff [simp]:
    7.62 +  "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
    7.63 +proof
    7.64 +  assume ?P
    7.65 +  moreover have "unit_factor a * normalize a = a" by simp
    7.66 +  ultimately show ?Q by simp 
    7.67 +next
    7.68 +  assume ?Q then show ?P by simp
    7.69 +qed
    7.70 +
    7.71 +lemma is_unit_unit_factor:
    7.72 +  assumes "is_unit a" shows "unit_factor a = a"
    7.73 +proof - 
    7.74 +  from assms have "normalize a = 1" by (rule is_unit_normalize)
    7.75 +  moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
    7.76 +  ultimately show ?thesis by simp
    7.77 +qed
    7.78 +
    7.79 +lemma unit_factor_1 [simp]:
    7.80 +  "unit_factor 1 = 1"
    7.81 +  by (rule is_unit_unit_factor) simp
    7.82 +
    7.83 +lemma normalize_1 [simp]:
    7.84 +  "normalize 1 = 1"
    7.85 +  by (rule is_unit_normalize) simp
    7.86 +
    7.87 +lemma normalize_1_iff:
    7.88 +  "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
    7.89 +proof
    7.90 +  assume ?Q then show ?P by (rule is_unit_normalize)
    7.91 +next
    7.92 +  assume ?P
    7.93 +  then have "a \<noteq> 0" by auto
    7.94 +  from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1"
    7.95 +    by simp
    7.96 +  then have "unit_factor a = a"
    7.97 +    by simp
    7.98 +  moreover have "is_unit (unit_factor a)"
    7.99 +    using \<open>a \<noteq> 0\<close> by simp
   7.100 +  ultimately show ?Q by simp
   7.101 +qed
   7.102 +  
   7.103 +lemma div_normalize [simp]:
   7.104 +  "a div normalize a = unit_factor a"
   7.105 +proof (cases "a = 0")
   7.106 +  case True then show ?thesis by simp
   7.107 +next
   7.108 +  case False then have "normalize a \<noteq> 0" by simp 
   7.109 +  with nonzero_mult_divide_cancel_right
   7.110 +  have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
   7.111 +  then show ?thesis by simp
   7.112 +qed
   7.113 +
   7.114 +lemma div_unit_factor [simp]:
   7.115 +  "a div unit_factor a = normalize a"
   7.116 +proof (cases "a = 0")
   7.117 +  case True then show ?thesis by simp
   7.118 +next
   7.119 +  case False then have "unit_factor a \<noteq> 0" by simp 
   7.120 +  with nonzero_mult_divide_cancel_left
   7.121 +  have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
   7.122 +  then show ?thesis by simp
   7.123 +qed
   7.124 +
   7.125 +lemma normalize_div [simp]:
   7.126 +  "normalize a div a = 1 div unit_factor a"
   7.127 +proof (cases "a = 0")
   7.128 +  case True then show ?thesis by simp
   7.129 +next
   7.130 +  case False
   7.131 +  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
   7.132 +    by simp
   7.133 +  also have "\<dots> = 1 div unit_factor a"
   7.134 +    using False by (subst is_unit_divide_mult_cancel_right) simp_all
   7.135 +  finally show ?thesis .
   7.136 +qed
   7.137 +
   7.138 +lemma mult_one_div_unit_factor [simp]:
   7.139 +  "a * (1 div unit_factor b) = a div unit_factor b"
   7.140 +  by (cases "b = 0") simp_all
   7.141 +
   7.142 +lemma normalize_mult:
   7.143 +  "normalize (a * b) = normalize a * normalize b"
   7.144 +proof (cases "a = 0 \<or> b = 0")
   7.145 +  case True then show ?thesis by auto
   7.146 +next
   7.147 +  case False
   7.148 +  from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" .
   7.149 +  then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp
   7.150 +  also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps)
   7.151 +  also have "\<dots> = a * b div unit_factor b div unit_factor a"
   7.152 +    using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
   7.153 +  also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
   7.154 +    using False by (subst unit_div_mult_swap) simp_all
   7.155 +  also have "\<dots> = normalize a * normalize b"
   7.156 +    using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
   7.157 +  finally show ?thesis .
   7.158 +qed
   7.159 + 
   7.160 +lemma unit_factor_idem [simp]:
   7.161 +  "unit_factor (unit_factor a) = unit_factor a"
   7.162 +  by (cases "a = 0") (auto intro: is_unit_unit_factor)
   7.163 +
   7.164 +lemma normalize_unit_factor [simp]:
   7.165 +  "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
   7.166 +  by (rule is_unit_normalize) simp
   7.167 +  
   7.168 +lemma normalize_idem [simp]:
   7.169 +  "normalize (normalize a) = normalize a"
   7.170 +proof (cases "a = 0")
   7.171 +  case True then show ?thesis by simp
   7.172 +next
   7.173 +  case False
   7.174 +  have "normalize a = normalize (unit_factor a * normalize a)" by simp
   7.175 +  also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
   7.176 +    by (simp only: normalize_mult)
   7.177 +  finally show ?thesis using False by simp_all
   7.178 +qed
   7.179 +
   7.180 +lemma unit_factor_normalize [simp]:
   7.181 +  assumes "a \<noteq> 0"
   7.182 +  shows "unit_factor (normalize a) = 1"
   7.183 +proof -
   7.184 +  from assms have "normalize a \<noteq> 0" by simp
   7.185 +  have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
   7.186 +    by (simp only: unit_factor_mult_normalize)
   7.187 +  then have "unit_factor (normalize a) * normalize a = normalize a"
   7.188 +    by simp
   7.189 +  with \<open>normalize a \<noteq> 0\<close>
   7.190 +  have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
   7.191 +    by simp
   7.192 +  with \<open>normalize a \<noteq> 0\<close>
   7.193 +  show ?thesis by simp
   7.194 +qed
   7.195 +
   7.196 +lemma dvd_unit_factor_div:
   7.197 +  assumes "b dvd a"
   7.198 +  shows "unit_factor (a div b) = unit_factor a div unit_factor b"
   7.199 +proof -
   7.200 +  from assms have "a = a div b * b"
   7.201 +    by simp
   7.202 +  then have "unit_factor a = unit_factor (a div b * b)"
   7.203 +    by simp
   7.204 +  then show ?thesis
   7.205 +    by (cases "b = 0") (simp_all add: unit_factor_mult)
   7.206 +qed
   7.207 +
   7.208 +lemma dvd_normalize_div:
   7.209 +  assumes "b dvd a"
   7.210 +  shows "normalize (a div b) = normalize a div normalize b"
   7.211 +proof -
   7.212 +  from assms have "a = a div b * b"
   7.213 +    by simp
   7.214 +  then have "normalize a = normalize (a div b * b)"
   7.215 +    by simp
   7.216 +  then show ?thesis
   7.217 +    by (cases "b = 0") (simp_all add: normalize_mult)
   7.218 +qed
   7.219 +
   7.220 +lemma normalize_dvd_iff [simp]:
   7.221 +  "normalize a dvd b \<longleftrightarrow> a dvd b"
   7.222 +proof -
   7.223 +  have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
   7.224 +    using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
   7.225 +      by (cases "a = 0") simp_all
   7.226 +  then show ?thesis by simp
   7.227 +qed
   7.228 +
   7.229 +lemma dvd_normalize_iff [simp]:
   7.230 +  "a dvd normalize b \<longleftrightarrow> a dvd b"
   7.231 +proof -
   7.232 +  have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
   7.233 +    using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
   7.234 +      by (cases "b = 0") simp_all
   7.235 +  then show ?thesis by simp
   7.236 +qed
   7.237 +
   7.238 +lemma associated_normalize_left [simp]:
   7.239 +  "associated (normalize a) b \<longleftrightarrow> associated a b"
   7.240 +  by (auto simp add: associated_def)
   7.241 +
   7.242 +lemma associated_normalize_right [simp]:
   7.243 +  "associated a (normalize b) \<longleftrightarrow> associated a b"
   7.244 +  by (auto simp add: associated_def)
   7.245 +
   7.246 +lemma associated_iff_normalize:
   7.247 +  "associated a b \<longleftrightarrow> normalize a = normalize b" (is "?P \<longleftrightarrow> ?Q")
   7.248 +proof (cases "a = 0 \<or> b = 0")
   7.249 +  case True then show ?thesis by auto
   7.250 +next
   7.251 +  case False
   7.252 +  show ?thesis
   7.253 +  proof
   7.254 +    assume ?P then show ?Q
   7.255 +      by (rule associated_is_unitE) (simp add: normalize_mult is_unit_normalize)
   7.256 +  next
   7.257 +    from False have *: "is_unit (unit_factor a div unit_factor b)"
   7.258 +      by auto
   7.259 +    assume ?Q then have "unit_factor a * normalize a = unit_factor a * normalize b"
   7.260 +      by simp
   7.261 +    then have "a = unit_factor a * (b div unit_factor b)"
   7.262 +      by simp
   7.263 +    with False have "a = (unit_factor a div unit_factor b) * b"
   7.264 +      by (simp add: unit_div_commute unit_div_mult_swap [symmetric])
   7.265 +    with * show ?P 
   7.266 +      by (rule is_unit_associatedI)
   7.267 +  qed
   7.268 +qed
   7.269 +
   7.270 +lemma associated_eqI:
   7.271 +  assumes "associated a b"
   7.272 +  assumes "a \<noteq> 0 \<Longrightarrow> unit_factor a = 1" and "b \<noteq> 0 \<Longrightarrow> unit_factor b = 1"
   7.273 +  shows "a = b"
   7.274 +proof (cases "a = 0")
   7.275 +  case True with assms show ?thesis by simp
   7.276 +next
   7.277 +  case False with assms have "b \<noteq> 0" by auto
   7.278 +  with False assms have "unit_factor a = unit_factor b"
   7.279 +    by simp
   7.280 +  moreover from assms have "normalize a = normalize b"
   7.281 +    by (simp add: associated_iff_normalize)
   7.282 +  ultimately have "unit_factor a * normalize a = unit_factor b * normalize b"
   7.283 +    by simp
   7.284 +  then show ?thesis
   7.285 +    by simp
   7.286 +qed
   7.287 +
   7.288 +end
   7.289 +
   7.290  class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
   7.291    assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   7.292    assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"