separate (semi)ring with normalization
authorhaftmann
Thu Jul 02 10:06:47 2015 +0200 (2015-07-02)
changeset 60634e3b6e516608b
parent 60633 f758c40e0a9a
child 60635 22830a64358f
separate (semi)ring with normalization
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Number_Theory/Normalization_Semidom.thy
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jul 02 14:10:42 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jul 02 10:06:47 2015 +0200
     1.3 @@ -3,9 +3,66 @@
     1.4  section \<open>Abstract euclidean algorithm\<close>
     1.5  
     1.6  theory Euclidean_Algorithm
     1.7 -imports Complex_Main "~~/src/HOL/Library/Polynomial"
     1.8 +imports Complex_Main "~~/src/HOL/Library/Polynomial" "~~/src/HOL/Number_Theory/Normalization_Semidom"
     1.9 +begin
    1.10 +
    1.11 +lemma is_unit_polyE:
    1.12 +  assumes "is_unit p"
    1.13 +  obtains a where "p = monom a 0" and "a \<noteq> 0"
    1.14 +proof -
    1.15 +  obtain a q where "p = pCons a q" by (cases p)
    1.16 +  with assms have "p = [:a:]" and "a \<noteq> 0"
    1.17 +    by (simp_all add: is_unit_pCons_iff)
    1.18 +  with that show thesis by (simp add: monom_0)
    1.19 +qed
    1.20 +
    1.21 +instantiation poly :: (field) normalization_semidom
    1.22  begin
    1.23 -  
    1.24 +
    1.25 +definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
    1.26 +  where "normalize_poly p = smult (1 / coeff p (degree p)) p"
    1.27 +
    1.28 +definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
    1.29 +  where "unit_factor_poly p = monom (coeff p (degree p)) 0"
    1.30 +
    1.31 +instance
    1.32 +proof
    1.33 +  fix p :: "'a poly"
    1.34 +  show "unit_factor p * normalize p = p"
    1.35 +    by (simp add: normalize_poly_def unit_factor_poly_def)
    1.36 +      (simp only: mult_smult_left [symmetric] smult_monom, simp)
    1.37 +next
    1.38 +  show "normalize 0 = (0::'a poly)"
    1.39 +    by (simp add: normalize_poly_def)
    1.40 +next
    1.41 +  show "unit_factor 0 = (0::'a poly)"
    1.42 +    by (simp add: unit_factor_poly_def)
    1.43 +next
    1.44 +  fix p :: "'a poly"
    1.45 +  assume "is_unit p"
    1.46 +  then obtain a where "p = monom a 0" and "a \<noteq> 0"
    1.47 +    by (rule is_unit_polyE)
    1.48 +  then show "normalize p = 1"
    1.49 +    by (auto simp add: normalize_poly_def smult_monom degree_monom_eq)
    1.50 +next
    1.51 +  fix p q :: "'a poly"
    1.52 +  assume "q \<noteq> 0"
    1.53 +  from \<open>q \<noteq> 0\<close> have "is_unit (monom (coeff q (degree q)) 0)"
    1.54 +    by (auto intro: is_unit_monom_0)
    1.55 +  then show "is_unit (unit_factor q)"
    1.56 +    by (simp add: unit_factor_poly_def)
    1.57 +next
    1.58 +  fix p q :: "'a poly"
    1.59 +  have "monom (coeff (p * q) (degree (p * q))) 0 =
    1.60 +    monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
    1.61 +    by (simp add: monom_0 coeff_degree_mult)
    1.62 +  then show "unit_factor (p * q) =
    1.63 +    unit_factor p * unit_factor q"
    1.64 +    by (simp add: unit_factor_poly_def)
    1.65 +qed
    1.66 +
    1.67 +end
    1.68 +
    1.69  text \<open>
    1.70    A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
    1.71    implemented. It must provide:
    1.72 @@ -13,136 +70,18 @@
    1.73    \item division with remainder
    1.74    \item a size function such that @{term "size (a mod b) < size b"} 
    1.75          for any @{term "b \<noteq> 0"}
    1.76 -  \item a normalization factor such that two associated numbers are equal iff 
    1.77 -        they are the same when divd by their normalization factors.
    1.78    \end{itemize}
    1.79    The existence of these functions makes it possible to derive gcd and lcm functions 
    1.80    for any Euclidean semiring.
    1.81  \<close> 
    1.82 -class euclidean_semiring = semiring_div + 
    1.83 +class euclidean_semiring = semiring_div + normalization_semidom + 
    1.84    fixes euclidean_size :: "'a \<Rightarrow> nat"
    1.85 -  fixes normalization_factor :: "'a \<Rightarrow> 'a"
    1.86    assumes mod_size_less: 
    1.87      "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
    1.88    assumes size_mult_mono:
    1.89 -    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a * b) \<ge> euclidean_size a"
    1.90 -  assumes normalization_factor_is_unit [intro,simp]: 
    1.91 -    "a \<noteq> 0 \<Longrightarrow> is_unit (normalization_factor a)"
    1.92 -  assumes normalization_factor_mult: "normalization_factor (a * b) = 
    1.93 -    normalization_factor a * normalization_factor b"
    1.94 -  assumes normalization_factor_unit: "is_unit a \<Longrightarrow> normalization_factor a = a"
    1.95 -  assumes normalization_factor_0 [simp]: "normalization_factor 0 = 0"
    1.96 +    "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
    1.97  begin
    1.98  
    1.99 -lemma normalization_factor_dvd [simp]:
   1.100 -  "a \<noteq> 0 \<Longrightarrow> normalization_factor a dvd b"
   1.101 -  by (rule unit_imp_dvd, simp)
   1.102 -    
   1.103 -lemma normalization_factor_1 [simp]:
   1.104 -  "normalization_factor 1 = 1"
   1.105 -  by (simp add: normalization_factor_unit)
   1.106 -
   1.107 -lemma normalization_factor_0_iff [simp]:
   1.108 -  "normalization_factor a = 0 \<longleftrightarrow> a = 0"
   1.109 -proof
   1.110 -  assume "normalization_factor a = 0"
   1.111 -  hence "\<not> is_unit (normalization_factor a)"
   1.112 -    by simp
   1.113 -  then show "a = 0" by auto
   1.114 -qed simp
   1.115 -
   1.116 -lemma normalization_factor_pow:
   1.117 -  "normalization_factor (a ^ n) = normalization_factor a ^ n"
   1.118 -  by (induct n) (simp_all add: normalization_factor_mult power_Suc2)
   1.119 -
   1.120 -lemma normalization_correct [simp]:
   1.121 -  "normalization_factor (a div normalization_factor a) = (if a = 0 then 0 else 1)"
   1.122 -proof (cases "a = 0", simp)
   1.123 -  assume "a \<noteq> 0"
   1.124 -  let ?nf = "normalization_factor"
   1.125 -  from normalization_factor_is_unit[OF \<open>a \<noteq> 0\<close>] have "?nf a \<noteq> 0"
   1.126 -    by auto
   1.127 -  have "?nf (a div ?nf a) * ?nf (?nf a) = ?nf (a div ?nf a * ?nf a)" 
   1.128 -    by (simp add: normalization_factor_mult)
   1.129 -  also have "a div ?nf a * ?nf a = a" using \<open>a \<noteq> 0\<close>
   1.130 -    by simp
   1.131 -  also have "?nf (?nf a) = ?nf a" using \<open>a \<noteq> 0\<close> 
   1.132 -    normalization_factor_is_unit normalization_factor_unit by simp
   1.133 -  finally have "normalization_factor (a div normalization_factor a) = 1"  
   1.134 -    using \<open>?nf a \<noteq> 0\<close> by (metis div_mult_self2_is_id div_self)
   1.135 -  with \<open>a \<noteq> 0\<close> show ?thesis by simp
   1.136 -qed
   1.137 -
   1.138 -lemma normalization_0_iff [simp]:
   1.139 -  "a div normalization_factor a = 0 \<longleftrightarrow> a = 0"
   1.140 -  by (cases "a = 0", simp, subst unit_eq_div1, blast, simp)
   1.141 -
   1.142 -lemma mult_div_normalization [simp]:
   1.143 -  "b * (1 div normalization_factor a) = b div normalization_factor a"
   1.144 -  by (cases "a = 0") simp_all
   1.145 -
   1.146 -lemma associated_iff_normed_eq:
   1.147 -  "associated a b \<longleftrightarrow> a div normalization_factor a = b div normalization_factor b" (is "?P \<longleftrightarrow> ?Q")
   1.148 -proof (cases "a = 0 \<or> b = 0")
   1.149 -  case True then show ?thesis by (auto dest: sym)
   1.150 -next
   1.151 -  case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
   1.152 -  show ?thesis
   1.153 -  proof
   1.154 -    assume ?Q
   1.155 -    from \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close>
   1.156 -    have "is_unit (normalization_factor a div normalization_factor b)"
   1.157 -      by auto
   1.158 -    moreover from \<open>?Q\<close> \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close>
   1.159 -    have "a = (normalization_factor a div normalization_factor b) * b"
   1.160 -      by (simp add: ac_simps div_mult_swap unit_eq_div1)
   1.161 -    ultimately show "associated a b" by (rule is_unit_associatedI) 
   1.162 -  next
   1.163 -    assume ?P
   1.164 -    then obtain c where "is_unit c" and "a = c * b"
   1.165 -      by (blast elim: associated_is_unitE)
   1.166 -    then show ?Q
   1.167 -      by (auto simp add: normalization_factor_mult normalization_factor_unit)
   1.168 -  qed
   1.169 -qed
   1.170 -
   1.171 -lemma normed_associated_imp_eq:
   1.172 -  "associated a b \<Longrightarrow> normalization_factor a \<in> {0, 1} \<Longrightarrow> normalization_factor b \<in> {0, 1} \<Longrightarrow> a = b"
   1.173 -  by (simp add: associated_iff_normed_eq, elim disjE, simp_all)
   1.174 -
   1.175 -lemma normed_dvd [iff]:
   1.176 -  "a div normalization_factor a dvd a"
   1.177 -proof (cases "a = 0")
   1.178 -  case True then show ?thesis by simp
   1.179 -next
   1.180 -  case False
   1.181 -  then have "a = a div normalization_factor a * normalization_factor a"
   1.182 -    by (auto intro: unit_div_mult_self)
   1.183 -  then show ?thesis ..
   1.184 -qed
   1.185 -
   1.186 -lemma dvd_normed [iff]:
   1.187 -  "a dvd a div normalization_factor a"
   1.188 -proof (cases "a = 0")
   1.189 -  case True then show ?thesis by simp
   1.190 -next
   1.191 -  case False
   1.192 -  then have "a div normalization_factor a = a * (1 div normalization_factor a)"
   1.193 -    by (auto intro: unit_mult_div_div)
   1.194 -  then show ?thesis ..
   1.195 -qed
   1.196 -
   1.197 -lemma associated_normed:
   1.198 -  "associated (a div normalization_factor a) a"
   1.199 -  by (rule associatedI) simp_all
   1.200 -
   1.201 -lemma normalization_factor_dvd' [simp]:
   1.202 -  "normalization_factor a dvd a"
   1.203 -  by (cases "a = 0", simp_all)
   1.204 -
   1.205 -lemmas normalization_factor_dvd_iff [simp] =
   1.206 -  unit_dvd_iff [OF normalization_factor_is_unit]
   1.207 -
   1.208  lemma euclidean_division:
   1.209    fixes a :: 'a and b :: 'a
   1.210    assumes "b \<noteq> 0"
   1.211 @@ -173,8 +112,7 @@
   1.212  
   1.213  function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.214  where
   1.215 -  "gcd_eucl a b = (if b = 0 then a div normalization_factor a
   1.216 -    else gcd_eucl b (a mod b))"
   1.217 +  "gcd_eucl a b = (if b = 0 then normalize a else gcd_eucl b (a mod b))"
   1.218    by pat_completeness simp
   1.219  termination
   1.220    by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less)
   1.221 @@ -201,7 +139,7 @@
   1.222  
   1.223  definition lcm_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.224  where
   1.225 -  "lcm_eucl a b = a * b div (gcd_eucl a b * normalization_factor (a * b))"
   1.226 +  "lcm_eucl a b = normalize (a * b) div gcd_eucl a b"
   1.227  
   1.228  definition Lcm_eucl :: "'a set \<Rightarrow> 'a" -- \<open>
   1.229    Somewhat complicated definition of Lcm that has the advantage of working
   1.230 @@ -210,7 +148,7 @@
   1.231    "Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then
   1.232       let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l =
   1.233         (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)
   1.234 -       in l div normalization_factor l
   1.235 +       in normalize l 
   1.236        else 0)"
   1.237  
   1.238  definition Gcd_eucl :: "'a set \<Rightarrow> 'a"
   1.239 @@ -218,11 +156,11 @@
   1.240    "Gcd_eucl A = Lcm_eucl {d. \<forall>a\<in>A. d dvd a}"
   1.241  
   1.242  lemma gcd_eucl_0:
   1.243 -  "gcd_eucl a 0 = a div normalization_factor a"
   1.244 +  "gcd_eucl a 0 = normalize a"
   1.245    by (simp add: gcd_eucl.simps [of a 0])
   1.246  
   1.247  lemma gcd_eucl_0_left:
   1.248 -  "gcd_eucl 0 a = a div normalization_factor a"
   1.249 +  "gcd_eucl 0 a = normalize a"
   1.250    by (simp_all add: gcd_eucl_0 gcd_eucl.simps [of 0 a])
   1.251  
   1.252  lemma gcd_eucl_non_0:
   1.253 @@ -237,7 +175,7 @@
   1.254  function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> 'a" where
   1.255    "euclid_ext a b = 
   1.256       (if b = 0 then 
   1.257 -        let c = 1 div normalization_factor a in (c, 0, a * c)
   1.258 +        (1 div unit_factor a, 0, normalize a)
   1.259        else
   1.260          case euclid_ext b (a mod b) of
   1.261              (s, t, c) \<Rightarrow> (t, s - t * (a div b), c))"
   1.262 @@ -248,11 +186,11 @@
   1.263  declare euclid_ext.simps [simp del]
   1.264  
   1.265  lemma euclid_ext_0: 
   1.266 -  "euclid_ext a 0 = (1 div normalization_factor a, 0, a div normalization_factor a)"
   1.267 +  "euclid_ext a 0 = (1 div unit_factor a, 0, normalize a)"
   1.268    by (simp add: euclid_ext.simps [of a 0])
   1.269  
   1.270  lemma euclid_ext_left_0: 
   1.271 -  "euclid_ext 0 a = (0, 1 div normalization_factor a, a div normalization_factor a)"
   1.272 +  "euclid_ext 0 a = (0, 1 div unit_factor a, normalize a)"
   1.273    by (simp add: euclid_ext_0 euclid_ext.simps [of 0 a])
   1.274  
   1.275  lemma euclid_ext_non_0: 
   1.276 @@ -261,7 +199,7 @@
   1.277    by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
   1.278  
   1.279  lemma euclid_ext_code [code]:
   1.280 -  "euclid_ext a b = (if b = 0 then (1 div normalization_factor a, 0, a div normalization_factor a)
   1.281 +  "euclid_ext a b = (if b = 0 then (1 div unit_factor a, 0, normalize a)
   1.282      else let (s, t, c) = euclid_ext b (a mod b) in  (t, s - t * (a div b), c))"
   1.283    by (simp add: euclid_ext.simps [of a b] euclid_ext.simps [of b 0])
   1.284  
   1.285 @@ -286,10 +224,10 @@
   1.286  where
   1.287    "euclid_ext' a b = (case euclid_ext a b of (s, t, _) \<Rightarrow> (s, t))"
   1.288  
   1.289 -lemma euclid_ext'_0: "euclid_ext' a 0 = (1 div normalization_factor a, 0)" 
   1.290 +lemma euclid_ext'_0: "euclid_ext' a 0 = (1 div unit_factor a, 0)" 
   1.291    by (simp add: euclid_ext'_def euclid_ext_0)
   1.292  
   1.293 -lemma euclid_ext'_left_0: "euclid_ext' 0 a = (0, 1 div normalization_factor a)" 
   1.294 +lemma euclid_ext'_left_0: "euclid_ext' 0 a = (0, 1 div unit_factor a)" 
   1.295    by (simp add: euclid_ext'_def euclid_ext_left_0)
   1.296    
   1.297  lemma euclid_ext'_non_0: "b \<noteq> 0 \<Longrightarrow> euclid_ext' a b = (snd (euclid_ext' b (a mod b)),
   1.298 @@ -304,11 +242,11 @@
   1.299  begin
   1.300  
   1.301  lemma gcd_0_left:
   1.302 -  "gcd 0 a = a div normalization_factor a"
   1.303 +  "gcd 0 a = normalize a"
   1.304    unfolding gcd_gcd_eucl by (fact gcd_eucl_0_left)
   1.305  
   1.306  lemma gcd_0:
   1.307 -  "gcd a 0 = a div normalization_factor a"
   1.308 +  "gcd a 0 = normalize a"
   1.309    unfolding gcd_gcd_eucl by (fact gcd_eucl_0)
   1.310  
   1.311  lemma gcd_non_0:
   1.312 @@ -347,15 +285,16 @@
   1.313    "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
   1.314    by (metis dvd_0_left dvd_refl gcd_dvd1 gcd_dvd2 gcd_greatest)+
   1.315  
   1.316 -lemma normalization_factor_gcd [simp]:
   1.317 -  "normalization_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" (is "?f a b = ?g a b")
   1.318 +lemma unit_factor_gcd [simp]:
   1.319 +  "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" (is "?f a b = ?g a b")
   1.320    by (induct a b rule: gcd_eucl_induct)
   1.321      (auto simp add: gcd_0 gcd_non_0)
   1.322  
   1.323  lemma gcdI:
   1.324 -  "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> (\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd k)
   1.325 -    \<Longrightarrow> normalization_factor k = (if k = 0 then 0 else 1) \<Longrightarrow> k = gcd a b"
   1.326 -  by (intro normed_associated_imp_eq) (auto simp: associated_def intro: gcd_greatest)
   1.327 +  assumes "c dvd a" and "c dvd b" and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
   1.328 +    and "unit_factor c = (if c = 0 then 0 else 1)"
   1.329 +  shows "c = gcd a b"
   1.330 +  by (rule associated_eqI) (auto simp: assms associated_def intro: gcd_greatest)
   1.331  
   1.332  sublocale gcd!: abel_semigroup gcd
   1.333  proof
   1.334 @@ -369,7 +308,7 @@
   1.335      moreover have "gcd (gcd a b) c dvd c" by simp
   1.336      ultimately show "gcd (gcd a b) c dvd gcd b c"
   1.337        by (rule gcd_greatest)
   1.338 -    show "normalization_factor (gcd (gcd a b) c) =  (if gcd (gcd a b) c = 0 then 0 else 1)"
   1.339 +    show "unit_factor (gcd (gcd a b) c) =  (if gcd (gcd a b) c = 0 then 0 else 1)"
   1.340        by auto
   1.341      fix l assume "l dvd a" and "l dvd gcd b c"
   1.342      with dvd_trans[OF _ gcd_dvd1] and dvd_trans[OF _ gcd_dvd2]
   1.343 @@ -384,7 +323,7 @@
   1.344  qed
   1.345  
   1.346  lemma gcd_unique: "d dvd a \<and> d dvd b \<and> 
   1.347 -    normalization_factor d = (if d = 0 then 0 else 1) \<and>
   1.348 +    unit_factor d = (if d = 0 then 0 else 1) \<and>
   1.349      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   1.350    by (rule, auto intro: gcdI simp: gcd_greatest)
   1.351  
   1.352 @@ -398,30 +337,30 @@
   1.353    by (rule sym, rule gcdI, simp_all)
   1.354  
   1.355  lemma gcd_proj2_if_dvd: 
   1.356 -  "b dvd a \<Longrightarrow> gcd a b = b div normalization_factor b"
   1.357 +  "b dvd a \<Longrightarrow> gcd a b = normalize b"
   1.358    by (cases "b = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0 gcd_0)
   1.359  
   1.360  lemma gcd_proj1_if_dvd: 
   1.361 -  "a dvd b \<Longrightarrow> gcd a b = a div normalization_factor a"
   1.362 +  "a dvd b \<Longrightarrow> gcd a b = normalize a"
   1.363    by (subst gcd.commute, simp add: gcd_proj2_if_dvd)
   1.364  
   1.365 -lemma gcd_proj1_iff: "gcd m n = m div normalization_factor m \<longleftrightarrow> m dvd n"
   1.366 +lemma gcd_proj1_iff: "gcd m n = normalize m \<longleftrightarrow> m dvd n"
   1.367  proof
   1.368 -  assume A: "gcd m n = m div normalization_factor m"
   1.369 +  assume A: "gcd m n = normalize m"
   1.370    show "m dvd n"
   1.371    proof (cases "m = 0")
   1.372      assume [simp]: "m \<noteq> 0"
   1.373 -    from A have B: "m = gcd m n * normalization_factor m"
   1.374 +    from A have B: "m = gcd m n * unit_factor m"
   1.375        by (simp add: unit_eq_div2)
   1.376      show ?thesis by (subst B, simp add: mult_unit_dvd_iff)
   1.377    qed (insert A, simp)
   1.378  next
   1.379    assume "m dvd n"
   1.380 -  then show "gcd m n = m div normalization_factor m" by (rule gcd_proj1_if_dvd)
   1.381 +  then show "gcd m n = normalize m" by (rule gcd_proj1_if_dvd)
   1.382  qed
   1.383    
   1.384 -lemma gcd_proj2_iff: "gcd m n = n div normalization_factor n \<longleftrightarrow> n dvd m"
   1.385 -  by (subst gcd.commute, simp add: gcd_proj1_iff)
   1.386 +lemma gcd_proj2_iff: "gcd m n = normalize n \<longleftrightarrow> n dvd m"
   1.387 +  using gcd_proj1_iff [of n m] by (simp add: ac_simps)
   1.388  
   1.389  lemma gcd_mod1 [simp]:
   1.390    "gcd (a mod b) b = gcd a b"
   1.391 @@ -432,20 +371,19 @@
   1.392    by (rule gcdI, simp, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff)
   1.393           
   1.394  lemma gcd_mult_distrib': 
   1.395 -  "c div normalization_factor c * gcd a b = gcd (c * a) (c * b)"
   1.396 +  "normalize c * gcd a b = gcd (c * a) (c * b)"
   1.397  proof (cases "c = 0")
   1.398    case True then show ?thesis by (simp_all add: gcd_0)
   1.399  next
   1.400 -  case False then have [simp]: "is_unit (normalization_factor c)" by simp
   1.401 +  case False then have [simp]: "is_unit (unit_factor c)" by simp
   1.402    show ?thesis
   1.403    proof (induct a b rule: gcd_eucl_induct)
   1.404      case (zero a) show ?case
   1.405      proof (cases "a = 0")
   1.406        case True then show ?thesis by (simp add: gcd_0)
   1.407      next
   1.408 -      case False then have "is_unit (normalization_factor a)" by simp
   1.409 -      then show ?thesis
   1.410 -        by (simp add: gcd_0 unit_div_commute unit_div_mult_swap normalization_factor_mult is_unit_div_mult2_eq)
   1.411 +      case False
   1.412 +      then show ?thesis by (simp add: gcd_0 normalize_mult)
   1.413      qed
   1.414      case (mod a b)
   1.415      then show ?case by (simp add: mult_mod_right gcd.commute)
   1.416 @@ -453,14 +391,15 @@
   1.417  qed
   1.418  
   1.419  lemma gcd_mult_distrib:
   1.420 -  "k * gcd a b = gcd (k*a) (k*b) * normalization_factor k"
   1.421 +  "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
   1.422  proof-
   1.423 -  let ?nf = "normalization_factor"
   1.424 -  from gcd_mult_distrib' 
   1.425 -    have "gcd (k*a) (k*b) = k div ?nf k * gcd a b" ..
   1.426 -  also have "... = k * gcd a b div ?nf k"
   1.427 -    by (metis dvd_div_mult dvd_eq_mod_eq_0 mod_0 normalization_factor_dvd)
   1.428 -  finally show ?thesis
   1.429 +  have "normalize k * gcd a b = gcd (k * a) (k * b)"
   1.430 +    by (simp add: gcd_mult_distrib')
   1.431 +  then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k"
   1.432 +    by simp
   1.433 +  then have "normalize k * unit_factor k * gcd a b  = gcd (k * a) (k * b) * unit_factor k"
   1.434 +    by (simp only: ac_simps)
   1.435 +  then show ?thesis
   1.436      by simp
   1.437  qed
   1.438  
   1.439 @@ -499,7 +438,7 @@
   1.440    apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps)
   1.441    apply (rule gcd_dvd2)
   1.442    apply (rule gcd_greatest, simp add: unit_simps, assumption)
   1.443 -  apply (subst normalization_factor_gcd, simp add: gcd_0)
   1.444 +  apply (subst unit_factor_gcd, simp add: gcd_0)
   1.445    done
   1.446  
   1.447  lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
   1.448 @@ -511,7 +450,25 @@
   1.449  lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
   1.450    by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
   1.451  
   1.452 -lemma gcd_idem: "gcd a a = a div normalization_factor a"
   1.453 +lemma normalize_gcd_left [simp]:
   1.454 +  "gcd (normalize a) b = gcd a b"
   1.455 +proof (cases "a = 0")
   1.456 +  case True then show ?thesis
   1.457 +    by simp
   1.458 +next
   1.459 +  case False then have "is_unit (unit_factor a)"
   1.460 +    by simp
   1.461 +  moreover have "normalize a = a div unit_factor a"
   1.462 +    by simp
   1.463 +  ultimately show ?thesis
   1.464 +    by (simp only: gcd_div_unit1)
   1.465 +qed
   1.466 +
   1.467 +lemma normalize_gcd_right [simp]:
   1.468 +  "gcd a (normalize b) = gcd a b"
   1.469 +  using normalize_gcd_left [of b a] by (simp add: ac_simps)
   1.470 +
   1.471 +lemma gcd_idem: "gcd a a = normalize a"
   1.472    by (cases "a = 0") (simp add: gcd_0_left, rule sym, rule gcdI, simp_all)
   1.473  
   1.474  lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
   1.475 @@ -543,7 +500,7 @@
   1.476    assumes "gcd c b = 1" and "c dvd a * b"
   1.477    shows "c dvd a"
   1.478  proof -
   1.479 -  let ?nf = "normalization_factor"
   1.480 +  let ?nf = "unit_factor"
   1.481    from assms gcd_mult_distrib [of a c b] 
   1.482      have A: "a = gcd (a * c) (a * b) * ?nf a" by simp
   1.483    from \<open>c dvd a * b\<close> show ?thesis by (subst A, simp_all add: gcd_greatest)
   1.484 @@ -561,7 +518,7 @@
   1.485    with A show "gcd a b dvd c" by (rule dvd_trans)
   1.486    have "gcd c d dvd d" by simp
   1.487    with A show "gcd a b dvd d" by (rule dvd_trans)
   1.488 -  show "normalization_factor (gcd a b) = (if gcd a b = 0 then 0 else 1)"
   1.489 +  show "unit_factor (gcd a b) = (if gcd a b = 0 then 0 else 1)"
   1.490      by simp
   1.491    fix l assume "l dvd c" and "l dvd d"
   1.492    hence "l dvd gcd c d" by (rule gcd_greatest)
   1.493 @@ -727,8 +684,8 @@
   1.494      using div_gcd_coprime by (subst sym, auto simp: div_gcd_coprime)
   1.495    hence "(gcd a b) ^ n = (gcd a b) ^ n * ..." by simp
   1.496    also note gcd_mult_distrib
   1.497 -  also have "normalization_factor ((gcd a b)^n) = 1"
   1.498 -    by (simp add: normalization_factor_pow A)
   1.499 +  also have "unit_factor ((gcd a b)^n) = 1"
   1.500 +    by (simp add: unit_factor_power A)
   1.501    also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
   1.502      by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp)
   1.503    also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
   1.504 @@ -850,29 +807,20 @@
   1.505  qed
   1.506  
   1.507  lemma lcm_gcd:
   1.508 -  "lcm a b = a * b div (gcd a b * normalization_factor (a*b))"
   1.509 -  by (simp only: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def)
   1.510 +  "lcm a b = normalize (a * b) div gcd a b"
   1.511 +  by (simp add: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def)
   1.512  
   1.513  lemma lcm_gcd_prod:
   1.514 -  "lcm a b * gcd a b = a * b div normalization_factor (a*b)"
   1.515 -proof (cases "a * b = 0")
   1.516 -  let ?nf = normalization_factor
   1.517 -  assume "a * b \<noteq> 0"
   1.518 -  hence "gcd a b \<noteq> 0" by simp
   1.519 -  from lcm_gcd have "lcm a b * gcd a b = gcd a b * (a * b div (?nf (a*b) * gcd a b))" 
   1.520 -    by (simp add: mult_ac)
   1.521 -  also from \<open>a * b \<noteq> 0\<close> have "... = a * b div ?nf (a*b)"
   1.522 -    by (simp add: div_mult_swap mult.commute)
   1.523 -  finally show ?thesis .
   1.524 -qed (auto simp add: lcm_gcd)
   1.525 +  "lcm a b * gcd a b = normalize (a * b)"
   1.526 +  by (simp add: lcm_gcd)
   1.527  
   1.528  lemma lcm_dvd1 [iff]:
   1.529    "a dvd lcm a b"
   1.530  proof (cases "a*b = 0")
   1.531    assume "a * b \<noteq> 0"
   1.532    hence "gcd a b \<noteq> 0" by simp
   1.533 -  let ?c = "1 div normalization_factor (a * b)"
   1.534 -  from \<open>a * b \<noteq> 0\<close> have [simp]: "is_unit (normalization_factor (a * b))" by simp
   1.535 +  let ?c = "1 div unit_factor (a * b)"
   1.536 +  from \<open>a * b \<noteq> 0\<close> have [simp]: "is_unit (unit_factor (a * b))" by simp
   1.537    from lcm_gcd_prod[of a b] have "lcm a b * gcd a b = a * ?c * b"
   1.538      by (simp add: div_mult_swap unit_div_commute)
   1.539    hence "lcm a b * gcd a b div gcd a b = a * ?c * b div gcd a b" by simp
   1.540 @@ -886,7 +834,7 @@
   1.541  lemma lcm_least:
   1.542    "\<lbrakk>a dvd k; b dvd k\<rbrakk> \<Longrightarrow> lcm a b dvd k"
   1.543  proof (cases "k = 0")
   1.544 -  let ?nf = normalization_factor
   1.545 +  let ?nf = unit_factor
   1.546    assume "k \<noteq> 0"
   1.547    hence "is_unit (?nf k)" by simp
   1.548    hence "?nf k \<noteq> 0" by (metis not_is_unit_0)
   1.549 @@ -928,7 +876,7 @@
   1.550  lemma lcm_zero:
   1.551    "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
   1.552  proof -
   1.553 -  let ?nf = normalization_factor
   1.554 +  let ?nf = unit_factor
   1.555    {
   1.556      assume "a \<noteq> 0" "b \<noteq> 0"
   1.557      hence "a * b div ?nf (a * b) \<noteq> 0" by (simp add: no_zero_divisors)
   1.558 @@ -945,42 +893,26 @@
   1.559  
   1.560  lemma gcd_lcm: 
   1.561    assumes "lcm a b \<noteq> 0"
   1.562 -  shows "gcd a b = a * b div (lcm a b * normalization_factor (a * b))"
   1.563 -proof-
   1.564 -  from assms have "gcd a b \<noteq> 0" by (simp add: lcm_zero)
   1.565 -  let ?c = "normalization_factor (a * b)"
   1.566 -  from \<open>lcm a b \<noteq> 0\<close> have "?c \<noteq> 0" by (intro notI, simp add: lcm_zero no_zero_divisors)
   1.567 -  hence "is_unit ?c" by simp
   1.568 -  from lcm_gcd_prod [of a b] have "gcd a b = a * b div ?c div lcm a b"
   1.569 -    by (subst (2) div_mult_self2_is_id[OF \<open>lcm a b \<noteq> 0\<close>, symmetric], simp add: mult_ac)
   1.570 -  also from \<open>is_unit ?c\<close> have "... = a * b div (lcm a b * ?c)"
   1.571 -    by (metis \<open>?c \<noteq> 0\<close> div_mult_mult1 dvd_mult_div_cancel mult_commute normalization_factor_dvd')
   1.572 -  finally show ?thesis .
   1.573 +  shows "gcd a b = normalize (a * b) div lcm a b"
   1.574 +proof -
   1.575 +  have "lcm a b * gcd a b = normalize (a * b)"
   1.576 +    by (fact lcm_gcd_prod)
   1.577 +  with assms show ?thesis
   1.578 +    by (metis nonzero_mult_divide_cancel_left)
   1.579  qed
   1.580  
   1.581 -lemma normalization_factor_lcm [simp]:
   1.582 -  "normalization_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
   1.583 -proof (cases "a = 0 \<or> b = 0")
   1.584 -  case True then show ?thesis
   1.585 -    by (auto simp add: lcm_gcd) 
   1.586 -next
   1.587 -  case False
   1.588 -  let ?nf = normalization_factor
   1.589 -  from lcm_gcd_prod[of a b] 
   1.590 -    have "?nf (lcm a b) * ?nf (gcd a b) = ?nf (a*b) div ?nf (a*b)"
   1.591 -    by (metis div_by_0 div_self normalization_correct normalization_factor_0 normalization_factor_mult)
   1.592 -  also have "... = (if a*b = 0 then 0 else 1)"
   1.593 -    by simp
   1.594 -  finally show ?thesis using False by simp
   1.595 -qed
   1.596 +lemma unit_factor_lcm [simp]:
   1.597 +  "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
   1.598 +  by (simp add: dvd_unit_factor_div lcm_gcd)
   1.599  
   1.600  lemma lcm_dvd2 [iff]: "b dvd lcm a b"
   1.601    using lcm_dvd1 [of b a] by (simp add: lcm_gcd ac_simps)
   1.602  
   1.603  lemma lcmI:
   1.604 -  "\<lbrakk>a dvd k; b dvd k; \<And>l. a dvd l \<Longrightarrow> b dvd l \<Longrightarrow> k dvd l;
   1.605 -    normalization_factor k = (if k = 0 then 0 else 1)\<rbrakk> \<Longrightarrow> k = lcm a b"
   1.606 -  by (intro normed_associated_imp_eq) (auto simp: associated_def intro: lcm_least)
   1.607 +  assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d"
   1.608 +    and "unit_factor c = (if c = 0 then 0 else 1)"
   1.609 +  shows "c = lcm a b"
   1.610 +  by (rule associated_eqI) (auto simp: assms associated_def intro: lcm_least)
   1.611  
   1.612  sublocale lcm!: abel_semigroup lcm
   1.613  proof
   1.614 @@ -1030,8 +962,8 @@
   1.615    assume "is_unit a \<and> is_unit b"
   1.616    hence "a dvd 1" and "b dvd 1" by simp_all
   1.617    hence "is_unit (lcm a b)" by (rule lcm_least)
   1.618 -  hence "lcm a b = normalization_factor (lcm a b)"
   1.619 -    by (subst normalization_factor_unit, simp_all)
   1.620 +  hence "lcm a b = unit_factor (lcm a b)"
   1.621 +    by (blast intro: sym is_unit_unit_factor)
   1.622    also have "\<dots> = 1" using \<open>is_unit a \<and> is_unit b\<close>
   1.623      by auto
   1.624    finally show "lcm a b = 1" .
   1.625 @@ -1047,7 +979,7 @@
   1.626  
   1.627  lemma lcm_unique:
   1.628    "a dvd d \<and> b dvd d \<and> 
   1.629 -  normalization_factor d = (if d = 0 then 0 else 1) \<and>
   1.630 +  unit_factor d = (if d = 0 then 0 else 1) \<and>
   1.631    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   1.632    by (rule, auto intro: lcmI simp: lcm_least lcm_zero)
   1.633  
   1.634 @@ -1060,43 +992,43 @@
   1.635    by (metis lcm_dvd2 dvd_trans)
   1.636  
   1.637  lemma lcm_1_left [simp]:
   1.638 -  "lcm 1 a = a div normalization_factor a"
   1.639 +  "lcm 1 a = normalize a"
   1.640    by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
   1.641  
   1.642  lemma lcm_1_right [simp]:
   1.643 -  "lcm a 1 = a div normalization_factor a"
   1.644 +  "lcm a 1 = normalize a"
   1.645    using lcm_1_left [of a] by (simp add: ac_simps)
   1.646  
   1.647  lemma lcm_coprime:
   1.648 -  "gcd a b = 1 \<Longrightarrow> lcm a b = a * b div normalization_factor (a*b)"
   1.649 +  "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
   1.650    by (subst lcm_gcd) simp
   1.651  
   1.652  lemma lcm_proj1_if_dvd: 
   1.653 -  "b dvd a \<Longrightarrow> lcm a b = a div normalization_factor a"
   1.654 +  "b dvd a \<Longrightarrow> lcm a b = normalize a"
   1.655    by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
   1.656  
   1.657  lemma lcm_proj2_if_dvd: 
   1.658 -  "a dvd b \<Longrightarrow> lcm a b = b div normalization_factor b"
   1.659 +  "a dvd b \<Longrightarrow> lcm a b = normalize b"
   1.660    using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
   1.661  
   1.662  lemma lcm_proj1_iff:
   1.663 -  "lcm m n = m div normalization_factor m \<longleftrightarrow> n dvd m"
   1.664 +  "lcm m n = normalize m \<longleftrightarrow> n dvd m"
   1.665  proof
   1.666 -  assume A: "lcm m n = m div normalization_factor m"
   1.667 +  assume A: "lcm m n = normalize m"
   1.668    show "n dvd m"
   1.669    proof (cases "m = 0")
   1.670      assume [simp]: "m \<noteq> 0"
   1.671 -    from A have B: "m = lcm m n * normalization_factor m"
   1.672 +    from A have B: "m = lcm m n * unit_factor m"
   1.673        by (simp add: unit_eq_div2)
   1.674      show ?thesis by (subst B, simp)
   1.675    qed simp
   1.676  next
   1.677    assume "n dvd m"
   1.678 -  then show "lcm m n = m div normalization_factor m" by (rule lcm_proj1_if_dvd)
   1.679 +  then show "lcm m n = normalize m" by (rule lcm_proj1_if_dvd)
   1.680  qed
   1.681  
   1.682  lemma lcm_proj2_iff:
   1.683 -  "lcm m n = n div normalization_factor n \<longleftrightarrow> m dvd n"
   1.684 +  "lcm m n = normalize n \<longleftrightarrow> m dvd n"
   1.685    using lcm_proj1_iff [of n m] by (simp add: ac_simps)
   1.686  
   1.687  lemma euclidean_size_lcm_le1: 
   1.688 @@ -1138,7 +1070,7 @@
   1.689    apply (rule dvd_trans[of _ "b * a"], simp, rule lcm_dvd1)
   1.690    apply (rule lcm_dvd2)
   1.691    apply (rule lcm_least, simp add: unit_simps, assumption)
   1.692 -  apply (subst normalization_factor_lcm, simp add: lcm_zero)
   1.693 +  apply (subst unit_factor_lcm, simp add: lcm_zero)
   1.694    done
   1.695  
   1.696  lemma lcm_mult_unit2:
   1.697 @@ -1153,6 +1085,24 @@
   1.698    "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
   1.699    by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
   1.700  
   1.701 +lemma normalize_lcm_left [simp]:
   1.702 +  "lcm (normalize a) b = lcm a b"
   1.703 +proof (cases "a = 0")
   1.704 +  case True then show ?thesis
   1.705 +    by simp
   1.706 +next
   1.707 +  case False then have "is_unit (unit_factor a)"
   1.708 +    by simp
   1.709 +  moreover have "normalize a = a div unit_factor a"
   1.710 +    by simp
   1.711 +  ultimately show ?thesis
   1.712 +    by (simp only: lcm_div_unit1)
   1.713 +qed
   1.714 +
   1.715 +lemma normalize_lcm_right [simp]:
   1.716 +  "lcm a (normalize b) = lcm a b"
   1.717 +  using normalize_lcm_left [of b a] by (simp add: ac_simps)
   1.718 +
   1.719  lemma lcm_left_idem:
   1.720    "lcm a (lcm a b) = lcm a b"
   1.721    apply (rule lcmI)
   1.722 @@ -1182,12 +1132,12 @@
   1.723  qed
   1.724  
   1.725  lemma dvd_Lcm [simp]: "a \<in> A \<Longrightarrow> a dvd Lcm A"
   1.726 -  and Lcm_dvd [simp]: "(\<forall>a\<in>A. a dvd l') \<Longrightarrow> Lcm A dvd l'"
   1.727 -  and normalization_factor_Lcm [simp]: 
   1.728 -          "normalization_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
   1.729 +  and Lcm_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm A dvd b"
   1.730 +  and unit_factor_Lcm [simp]: 
   1.731 +          "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
   1.732  proof -
   1.733    have "(\<forall>a\<in>A. a dvd Lcm A) \<and> (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> Lcm A dvd l') \<and>
   1.734 -    normalization_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" (is ?thesis)
   1.735 +    unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" (is ?thesis)
   1.736    proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>a\<in>A. a dvd l)")
   1.737      case False
   1.738      hence "Lcm A = 0" by (auto simp: Lcm_Lcm_eucl Lcm_eucl_def)
   1.739 @@ -1229,39 +1179,42 @@
   1.740        hence "l dvd l'" by (blast dest: dvd_gcd_D2)
   1.741      }
   1.742  
   1.743 -    with \<open>(\<forall>a\<in>A. a dvd l)\<close> and normalization_factor_is_unit[OF \<open>l \<noteq> 0\<close>] and \<open>l \<noteq> 0\<close>
   1.744 -      have "(\<forall>a\<in>A. a dvd l div normalization_factor l) \<and> 
   1.745 -        (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> l div normalization_factor l dvd l') \<and>
   1.746 -        normalization_factor (l div normalization_factor l) = 
   1.747 -        (if l div normalization_factor l = 0 then 0 else 1)"
   1.748 +    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>
   1.749 +      have "(\<forall>a\<in>A. a dvd normalize l) \<and> 
   1.750 +        (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l') \<and>
   1.751 +        unit_factor (normalize l) = 
   1.752 +        (if normalize l = 0 then 0 else 1)"
   1.753        by (auto simp: unit_simps)
   1.754 -    also from True have "l div normalization_factor l = Lcm A"
   1.755 +    also from True have "normalize l = Lcm A"
   1.756        by (simp add: Lcm_Lcm_eucl Lcm_eucl_def Let_def n_def l_def)
   1.757      finally show ?thesis .
   1.758    qed
   1.759    note A = this
   1.760  
   1.761    {fix a assume "a \<in> A" then show "a dvd Lcm A" using A by blast}
   1.762 -  {fix l' assume "\<forall>a\<in>A. a dvd l'" then show "Lcm A dvd l'" using A by blast}
   1.763 -  from A show "normalization_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" by blast
   1.764 +  {fix b assume "\<And>a. a \<in> A \<Longrightarrow> a dvd b" then show "Lcm A dvd b" using A by blast}
   1.765 +  from A show "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" by blast
   1.766  qed
   1.767 -    
   1.768 +
   1.769 +lemma normalize_Lcm [simp]:
   1.770 +  "normalize (Lcm A) = Lcm A"
   1.771 +  by (cases "Lcm A = 0") (auto intro: associated_eqI)
   1.772 +
   1.773  lemma LcmI:
   1.774 -  "(\<And>a. a\<in>A \<Longrightarrow> a dvd l) \<Longrightarrow> (\<And>l'. (\<forall>a\<in>A. a dvd l') \<Longrightarrow> l dvd l') \<Longrightarrow>
   1.775 -      normalization_factor l = (if l = 0 then 0 else 1) \<Longrightarrow> l = Lcm A"
   1.776 -  by (intro normed_associated_imp_eq)
   1.777 -    (auto intro: Lcm_dvd dvd_Lcm simp: associated_def)
   1.778 +  assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c"
   1.779 +    and "unit_factor b = (if b = 0 then 0 else 1)" shows "b = Lcm A"
   1.780 +  by (rule associated_eqI) (auto simp: assms associated_def intro: Lcm_least)
   1.781  
   1.782  lemma Lcm_subset:
   1.783    "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
   1.784 -  by (blast intro: Lcm_dvd dvd_Lcm)
   1.785 +  by (blast intro: Lcm_least dvd_Lcm)
   1.786  
   1.787  lemma Lcm_Un:
   1.788    "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
   1.789    apply (rule lcmI)
   1.790    apply (blast intro: Lcm_subset)
   1.791    apply (blast intro: Lcm_subset)
   1.792 -  apply (intro Lcm_dvd ballI, elim UnE)
   1.793 +  apply (intro Lcm_least ballI, elim UnE)
   1.794    apply (rule dvd_trans, erule dvd_Lcm, assumption)
   1.795    apply (rule dvd_trans, erule dvd_Lcm, assumption)
   1.796    apply simp
   1.797 @@ -1279,7 +1232,7 @@
   1.798  proof -
   1.799    have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A" by blast
   1.800    hence "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
   1.801 -    by (simp add: Lcm_Un[symmetric])
   1.802 +    by (simp add: Lcm_Un [symmetric])
   1.803    also have "Lcm {a\<in>A. is_unit a} = 1" by (simp add: Lcm_1_iff)
   1.804    finally show ?thesis by simp
   1.805  qed
   1.806 @@ -1309,8 +1262,8 @@
   1.807        apply (simp add: l\<^sub>0_props)
   1.808        done
   1.809      from someI_ex[OF this] have "l \<noteq> 0" unfolding l_def by simp_all
   1.810 -    hence "l div normalization_factor l \<noteq> 0" by simp
   1.811 -    also from ex have "l div normalization_factor l = Lcm A"
   1.812 +    hence "normalize l \<noteq> 0" by simp
   1.813 +    also from ex have "normalize l = Lcm A"
   1.814         by (simp only: Lcm_Lcm_eucl Lcm_eucl_def n_def l_def if_True Let_def)
   1.815      finally show False using \<open>Lcm A = 0\<close> by contradiction
   1.816    qed
   1.817 @@ -1350,8 +1303,8 @@
   1.818  proof (rule lcmI)
   1.819    fix l assume "a dvd l" and "Lcm A dvd l"
   1.820    hence "\<forall>a\<in>A. a dvd l" by (blast intro: dvd_trans dvd_Lcm)
   1.821 -  with \<open>a dvd l\<close> show "Lcm (insert a A) dvd l" by (force intro: Lcm_dvd)
   1.822 -qed (auto intro: Lcm_dvd dvd_Lcm)
   1.823 +  with \<open>a dvd l\<close> show "Lcm (insert a A) dvd l" by (force intro: Lcm_least)
   1.824 +qed (auto intro: Lcm_least dvd_Lcm)
   1.825   
   1.826  lemma Lcm_finite:
   1.827    assumes "finite A"
   1.828 @@ -1364,32 +1317,31 @@
   1.829    using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite by (simp add: ac_simps)
   1.830  
   1.831  lemma Lcm_singleton [simp]:
   1.832 -  "Lcm {a} = a div normalization_factor a"
   1.833 +  "Lcm {a} = normalize a"
   1.834    by simp
   1.835  
   1.836  lemma Lcm_2 [simp]:
   1.837    "Lcm {a,b} = lcm a b"
   1.838 -  by (simp only: Lcm_insert Lcm_empty lcm_1_right)
   1.839 -    (cases "b = 0", simp, rule lcm_div_unit2, simp)
   1.840 +  by simp
   1.841  
   1.842  lemma Lcm_coprime:
   1.843    assumes "finite A" and "A \<noteq> {}" 
   1.844    assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
   1.845 -  shows "Lcm A = \<Prod>A div normalization_factor (\<Prod>A)"
   1.846 +  shows "Lcm A = normalize (\<Prod>A)"
   1.847  using assms proof (induct rule: finite_ne_induct)
   1.848    case (insert a A)
   1.849    have "Lcm (insert a A) = lcm a (Lcm A)" by simp
   1.850 -  also from insert have "Lcm A = \<Prod>A div normalization_factor (\<Prod>A)" by blast
   1.851 +  also from insert have "Lcm A = normalize (\<Prod>A)" by blast
   1.852    also have "lcm a \<dots> = lcm a (\<Prod>A)" by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
   1.853    also from insert have "gcd a (\<Prod>A) = 1" by (subst gcd.commute, intro setprod_coprime) auto
   1.854 -  with insert have "lcm a (\<Prod>A) = \<Prod>(insert a A) div normalization_factor (\<Prod>(insert a A))"
   1.855 +  with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
   1.856      by (simp add: lcm_coprime)
   1.857    finally show ?case .
   1.858  qed simp
   1.859        
   1.860  lemma Lcm_coprime':
   1.861    "card A \<noteq> 0 \<Longrightarrow> (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1)
   1.862 -    \<Longrightarrow> Lcm A = \<Prod>A div normalization_factor (\<Prod>A)"
   1.863 +    \<Longrightarrow> Lcm A = normalize (\<Prod>A)"
   1.864    by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
   1.865  
   1.866  lemma Gcd_Lcm:
   1.867 @@ -1397,31 +1349,35 @@
   1.868    by (simp add: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def)
   1.869  
   1.870  lemma Gcd_dvd [simp]: "a \<in> A \<Longrightarrow> Gcd A dvd a"
   1.871 -  and dvd_Gcd [simp]: "(\<forall>a\<in>A. g' dvd a) \<Longrightarrow> g' dvd Gcd A"
   1.872 -  and normalization_factor_Gcd [simp]: 
   1.873 -    "normalization_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
   1.874 +  and Gcd_greatest: "(\<And>a. a \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> b dvd Gcd A"
   1.875 +  and unit_factor_Gcd [simp]: 
   1.876 +    "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
   1.877  proof -
   1.878    fix a assume "a \<in> A"
   1.879 -  hence "Lcm {d. \<forall>a\<in>A. d dvd a} dvd a" by (intro Lcm_dvd) blast
   1.880 +  hence "Lcm {d. \<forall>a\<in>A. d dvd a} dvd a" by (intro Lcm_least) blast
   1.881    then show "Gcd A dvd a" by (simp add: Gcd_Lcm)
   1.882  next
   1.883 -  fix g' assume "\<forall>a\<in>A. g' dvd a"
   1.884 +  fix g' assume "\<And>a. a \<in> A \<Longrightarrow> g' dvd a"
   1.885    hence "g' dvd Lcm {d. \<forall>a\<in>A. d dvd a}" by (intro dvd_Lcm) blast
   1.886    then show "g' dvd Gcd A" by (simp add: Gcd_Lcm)
   1.887  next
   1.888 -  show "normalization_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
   1.889 +  show "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
   1.890      by (simp add: Gcd_Lcm)
   1.891  qed
   1.892  
   1.893 +lemma normalize_Gcd [simp]:
   1.894 +  "normalize (Gcd A) = Gcd A"
   1.895 +  by (cases "Gcd A = 0") (auto intro: associated_eqI)
   1.896 +
   1.897  lemma GcdI:
   1.898 -  "(\<And>a. a\<in>A \<Longrightarrow> l dvd a) \<Longrightarrow> (\<And>l'. (\<forall>a\<in>A. l' dvd a) \<Longrightarrow> l' dvd l) \<Longrightarrow>
   1.899 -    normalization_factor l = (if l = 0 then 0 else 1) \<Longrightarrow> l = Gcd A"
   1.900 -  by (intro normed_associated_imp_eq)
   1.901 -    (auto intro: Gcd_dvd dvd_Gcd simp: associated_def)
   1.902 +  assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
   1.903 +    and "unit_factor b = (if b = 0 then 0 else 1)"
   1.904 +  shows "b = Gcd A"
   1.905 +  by (rule associated_eqI) (auto simp: assms associated_def intro: Gcd_greatest)
   1.906  
   1.907  lemma Lcm_Gcd:
   1.908    "Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
   1.909 -  by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_dvd)
   1.910 +  by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_greatest)
   1.911  
   1.912  lemma Gcd_0_iff:
   1.913    "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}"
   1.914 @@ -1443,8 +1399,8 @@
   1.915  proof (rule gcdI)
   1.916    fix l assume "l dvd a" and "l dvd Gcd A"
   1.917    hence "\<forall>a\<in>A. l dvd a" by (blast intro: dvd_trans Gcd_dvd)
   1.918 -  with \<open>l dvd a\<close> show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd)
   1.919 -qed auto
   1.920 +  with \<open>l dvd a\<close> show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd Gcd_greatest)
   1.921 +qed (auto intro: Gcd_greatest)
   1.922  
   1.923  lemma Gcd_finite:
   1.924    assumes "finite A"
   1.925 @@ -1456,11 +1412,11 @@
   1.926    "Gcd (set xs) = fold gcd xs 0"
   1.927    using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite by (simp add: ac_simps)
   1.928  
   1.929 -lemma Gcd_singleton [simp]: "Gcd {a} = a div normalization_factor a"
   1.930 +lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
   1.931    by (simp add: gcd_0)
   1.932  
   1.933  lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b"
   1.934 -  by (simp only: Gcd_insert Gcd_empty gcd_0) (cases "b = 0", simp, rule gcd_div_unit2, simp)
   1.935 +  by (simp add: gcd_0)
   1.936  
   1.937  subclass semiring_gcd
   1.938    by unfold_locales (simp_all add: gcd_greatest_iff)
   1.939 @@ -1554,7 +1510,7 @@
   1.940    "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
   1.941  
   1.942  definition [simp]:
   1.943 -  "normalization_factor_nat (n::nat) = (if n = 0 then 0 else 1 :: nat)"
   1.944 +  "unit_factor_nat (n::nat) = (if n = 0 then 0 else 1 :: nat)"
   1.945  
   1.946  instance proof
   1.947  qed simp_all
   1.948 @@ -1568,22 +1524,10 @@
   1.949    "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   1.950  
   1.951  definition [simp]:
   1.952 -  "normalization_factor_int = (sgn :: int \<Rightarrow> int)"
   1.953 +  "unit_factor_int = (sgn :: int \<Rightarrow> int)"
   1.954  
   1.955  instance
   1.956 -proof (default, goals)
   1.957 -  case 2
   1.958 -  then show ?case by (auto simp add: abs_mult nat_mult_distrib)
   1.959 -next
   1.960 -  case 3
   1.961 -  then show ?case by (simp add: zsgn_def)
   1.962 -next
   1.963 -  case 5
   1.964 -  then show ?case by (auto simp: zsgn_def)
   1.965 -next
   1.966 -  case 6
   1.967 -  then show ?case by (auto split: abs_split simp: zsgn_def)
   1.968 -qed (auto simp: sgn_times split: abs_split)
   1.969 +by standard (auto simp add: abs_mult nat_mult_distrib sgn_times split: abs_split)
   1.970  
   1.971  end
   1.972  
   1.973 @@ -1593,8 +1537,9 @@
   1.974  definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
   1.975    where "euclidean_size p = (if p = 0 then 0 else Suc (degree p))"
   1.976  
   1.977 -definition normalization_factor_poly :: "'a poly \<Rightarrow> 'a poly"
   1.978 -  where "normalization_factor p = monom (coeff p (degree p)) 0"
   1.979 +lemma euclidenan_size_poly_minus_one_degree [simp]:
   1.980 +  "euclidean_size p - 1 = degree p"
   1.981 +  by (simp add: euclidean_size_poly_def)
   1.982  
   1.983  lemma euclidean_size_poly_0 [simp]:
   1.984    "euclidean_size (0::'a poly) = 0"
   1.985 @@ -1619,30 +1564,6 @@
   1.986      by (rule degree_mult_right_le)
   1.987    with \<open>q \<noteq> 0\<close> show "euclidean_size p \<le> euclidean_size (p * q)"
   1.988      by (cases "p = 0") simp_all
   1.989 -  from \<open>q \<noteq> 0\<close> have "is_unit (monom (coeff q (degree q)) 0)"
   1.990 -    by (auto intro: is_unit_monom_0)
   1.991 -  then show "is_unit (normalization_factor q)"
   1.992 -    by (simp add: normalization_factor_poly_def)
   1.993 -next
   1.994 -  fix p :: "'a poly"
   1.995 -  assume "is_unit p"
   1.996 -  then have "monom (coeff p (degree p)) 0 = p"
   1.997 -    by (fact is_unit_monom_trival)
   1.998 -  then show "normalization_factor p = p"
   1.999 -    by (simp add: normalization_factor_poly_def)
  1.1000 -next
  1.1001 -  fix p q :: "'a poly"
  1.1002 -  have "monom (coeff (p * q) (degree (p * q))) 0 =
  1.1003 -    monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
  1.1004 -    by (simp add: monom_0 coeff_degree_mult)
  1.1005 -  then show "normalization_factor (p * q) =
  1.1006 -    normalization_factor p * normalization_factor q"
  1.1007 -    by (simp add: normalization_factor_poly_def)
  1.1008 -next
  1.1009 -  have "monom (coeff 0 (degree 0)) 0 = 0"
  1.1010 -    by simp
  1.1011 -  then show "normalization_factor 0 = (0::'a poly)"
  1.1012 -    by (simp add: normalization_factor_poly_def)
  1.1013  qed
  1.1014  
  1.1015  end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Number_Theory/Normalization_Semidom.thy	Thu Jul 02 10:06:47 2015 +0200
     2.3 @@ -0,0 +1,336 @@
     2.4 +theory Normalization_Semidom
     2.5 +imports Main
     2.6 +begin
     2.7 +
     2.8 +context algebraic_semidom
     2.9 +begin
    2.10 +
    2.11 +lemma is_unit_divide_mult_cancel_left:
    2.12 +  assumes "a \<noteq> 0" and "is_unit b"
    2.13 +  shows "a div (a * b) = 1 div b"
    2.14 +proof -
    2.15 +  from assms have "a div (a * b) = a div a div b"
    2.16 +    by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
    2.17 +  with assms show ?thesis by simp
    2.18 +qed
    2.19 +
    2.20 +lemma is_unit_divide_mult_cancel_right:
    2.21 +  assumes "a \<noteq> 0" and "is_unit b"
    2.22 +  shows "a div (b * a) = 1 div b"
    2.23 +  using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)
    2.24 +
    2.25 +end
    2.26 +
    2.27 +class normalization_semidom = algebraic_semidom +
    2.28 +  fixes normalize :: "'a \<Rightarrow> 'a"
    2.29 +    and unit_factor :: "'a \<Rightarrow> 'a"
    2.30 +  assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
    2.31 +  assumes normalize_0 [simp]: "normalize 0 = 0"
    2.32 +    and unit_factor_0 [simp]: "unit_factor 0 = 0"
    2.33 +  assumes is_unit_normalize:
    2.34 +    "is_unit a  \<Longrightarrow> normalize a = 1"
    2.35 +  assumes unit_factor_is_unit [iff]: 
    2.36 +    "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
    2.37 +  assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
    2.38 +begin
    2.39 +
    2.40 +lemma unit_factor_dvd [simp]:
    2.41 +  "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
    2.42 +  by (rule unit_imp_dvd) simp
    2.43 +
    2.44 +lemma unit_factor_self [simp]:
    2.45 +  "unit_factor a dvd a"
    2.46 +  by (cases "a = 0") simp_all 
    2.47 +  
    2.48 +lemma normalize_mult_unit_factor [simp]:
    2.49 +  "normalize a * unit_factor a = a"
    2.50 +  using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
    2.51 +
    2.52 +lemma normalize_eq_0_iff [simp]:
    2.53 +  "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
    2.54 +proof
    2.55 +  assume ?P
    2.56 +  moreover have "unit_factor a * normalize a = a" by simp
    2.57 +  ultimately show ?Q by simp 
    2.58 +next
    2.59 +  assume ?Q then show ?P by simp
    2.60 +qed
    2.61 +
    2.62 +lemma unit_factor_eq_0_iff [simp]:
    2.63 +  "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
    2.64 +proof
    2.65 +  assume ?P
    2.66 +  moreover have "unit_factor a * normalize a = a" by simp
    2.67 +  ultimately show ?Q by simp 
    2.68 +next
    2.69 +  assume ?Q then show ?P by simp
    2.70 +qed
    2.71 +
    2.72 +lemma is_unit_unit_factor:
    2.73 +  assumes "is_unit a" shows "unit_factor a = a"
    2.74 +proof - 
    2.75 +  from assms have "normalize a = 1" by (rule is_unit_normalize)
    2.76 +  moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
    2.77 +  ultimately show ?thesis by simp
    2.78 +qed
    2.79 +
    2.80 +lemma unit_factor_1 [simp]:
    2.81 +  "unit_factor 1 = 1"
    2.82 +  by (rule is_unit_unit_factor) simp
    2.83 +
    2.84 +lemma normalize_1 [simp]:
    2.85 +  "normalize 1 = 1"
    2.86 +  by (rule is_unit_normalize) simp
    2.87 +
    2.88 +lemma normalize_1_iff:
    2.89 +  "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
    2.90 +proof
    2.91 +  assume ?Q then show ?P by (rule is_unit_normalize)
    2.92 +next
    2.93 +  assume ?P
    2.94 +  then have "a \<noteq> 0" by auto
    2.95 +  from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1"
    2.96 +    by simp
    2.97 +  then have "unit_factor a = a"
    2.98 +    by simp
    2.99 +  moreover have "is_unit (unit_factor a)"
   2.100 +    using \<open>a \<noteq> 0\<close> by simp
   2.101 +  ultimately show ?Q by simp
   2.102 +qed
   2.103 +  
   2.104 +lemma div_normalize [simp]:
   2.105 +  "a div normalize a = unit_factor a"
   2.106 +proof (cases "a = 0")
   2.107 +  case True then show ?thesis by simp
   2.108 +next
   2.109 +  case False then have "normalize a \<noteq> 0" by simp 
   2.110 +  with nonzero_mult_divide_cancel_right
   2.111 +  have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
   2.112 +  then show ?thesis by simp
   2.113 +qed
   2.114 +
   2.115 +lemma div_unit_factor [simp]:
   2.116 +  "a div unit_factor a = normalize a"
   2.117 +proof (cases "a = 0")
   2.118 +  case True then show ?thesis by simp
   2.119 +next
   2.120 +  case False then have "unit_factor a \<noteq> 0" by simp 
   2.121 +  with nonzero_mult_divide_cancel_left
   2.122 +  have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
   2.123 +  then show ?thesis by simp
   2.124 +qed
   2.125 +
   2.126 +lemma normalize_div [simp]:
   2.127 +  "normalize a div a = 1 div unit_factor a"
   2.128 +proof (cases "a = 0")
   2.129 +  case True then show ?thesis by simp
   2.130 +next
   2.131 +  case False
   2.132 +  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
   2.133 +    by simp
   2.134 +  also have "\<dots> = 1 div unit_factor a"
   2.135 +    using False by (subst is_unit_divide_mult_cancel_right) simp_all
   2.136 +  finally show ?thesis .
   2.137 +qed
   2.138 +
   2.139 +lemma mult_one_div_unit_factor [simp]:
   2.140 +  "a * (1 div unit_factor b) = a div unit_factor b"
   2.141 +  by (cases "b = 0") simp_all
   2.142 +
   2.143 +lemma normalize_mult:
   2.144 +  "normalize (a * b) = normalize a * normalize b"
   2.145 +proof (cases "a = 0 \<or> b = 0")
   2.146 +  case True then show ?thesis by auto
   2.147 +next
   2.148 +  case False
   2.149 +  from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" .
   2.150 +  then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp
   2.151 +  also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps)
   2.152 +  also have "\<dots> = a * b div unit_factor b div unit_factor a"
   2.153 +    using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
   2.154 +  also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
   2.155 +    using False by (subst unit_div_mult_swap) simp_all
   2.156 +  also have "\<dots> = normalize a * normalize b"
   2.157 +    using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
   2.158 +  finally show ?thesis .
   2.159 +qed
   2.160 + 
   2.161 +lemma unit_factor_idem [simp]:
   2.162 +  "unit_factor (unit_factor a) = unit_factor a"
   2.163 +  by (cases "a = 0") (auto intro: is_unit_unit_factor)
   2.164 +
   2.165 +lemma normalize_unit_factor [simp]:
   2.166 +  "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
   2.167 +  by (rule is_unit_normalize) simp
   2.168 +  
   2.169 +lemma normalize_idem [simp]:
   2.170 +  "normalize (normalize a) = normalize a"
   2.171 +proof (cases "a = 0")
   2.172 +  case True then show ?thesis by simp
   2.173 +next
   2.174 +  case False
   2.175 +  have "normalize a = normalize (unit_factor a * normalize a)" by simp
   2.176 +  also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
   2.177 +    by (simp only: normalize_mult)
   2.178 +  finally show ?thesis using False by simp_all
   2.179 +qed
   2.180 +
   2.181 +lemma unit_factor_normalize [simp]:
   2.182 +  assumes "a \<noteq> 0"
   2.183 +  shows "unit_factor (normalize a) = 1"
   2.184 +proof -
   2.185 +  from assms have "normalize a \<noteq> 0" by simp
   2.186 +  have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
   2.187 +    by (simp only: unit_factor_mult_normalize)
   2.188 +  then have "unit_factor (normalize a) * normalize a = normalize a"
   2.189 +    by simp
   2.190 +  with \<open>normalize a \<noteq> 0\<close>
   2.191 +  have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
   2.192 +    by simp
   2.193 +  with \<open>normalize a \<noteq> 0\<close>
   2.194 +  show ?thesis by simp
   2.195 +qed
   2.196 +
   2.197 +lemma dvd_unit_factor_div:
   2.198 +  assumes "b dvd a"
   2.199 +  shows "unit_factor (a div b) = unit_factor a div unit_factor b"
   2.200 +proof -
   2.201 +  from assms have "a = a div b * b"
   2.202 +    by simp
   2.203 +  then have "unit_factor a = unit_factor (a div b * b)"
   2.204 +    by simp
   2.205 +  then show ?thesis
   2.206 +    by (cases "b = 0") (simp_all add: unit_factor_mult)
   2.207 +qed
   2.208 +
   2.209 +lemma dvd_normalize_div:
   2.210 +  assumes "b dvd a"
   2.211 +  shows "normalize (a div b) = normalize a div normalize b"
   2.212 +proof -
   2.213 +  from assms have "a = a div b * b"
   2.214 +    by simp
   2.215 +  then have "normalize a = normalize (a div b * b)"
   2.216 +    by simp
   2.217 +  then show ?thesis
   2.218 +    by (cases "b = 0") (simp_all add: normalize_mult)
   2.219 +qed
   2.220 +
   2.221 +lemma normalize_dvd_iff [simp]:
   2.222 +  "normalize a dvd b \<longleftrightarrow> a dvd b"
   2.223 +proof -
   2.224 +  have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
   2.225 +    using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
   2.226 +      by (cases "a = 0") simp_all
   2.227 +  then show ?thesis by simp
   2.228 +qed
   2.229 +
   2.230 +lemma dvd_normalize_iff [simp]:
   2.231 +  "a dvd normalize b \<longleftrightarrow> a dvd b"
   2.232 +proof -
   2.233 +  have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
   2.234 +    using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
   2.235 +      by (cases "b = 0") simp_all
   2.236 +  then show ?thesis by simp
   2.237 +qed
   2.238 +
   2.239 +lemma associated_normalize_left [simp]:
   2.240 +  "associated (normalize a) b \<longleftrightarrow> associated a b"
   2.241 +  by (auto simp add: associated_def)
   2.242 +
   2.243 +lemma associated_normalize_right [simp]:
   2.244 +  "associated a (normalize b) \<longleftrightarrow> associated a b"
   2.245 +  by (auto simp add: associated_def)
   2.246 +
   2.247 +lemma associated_iff_normalize:
   2.248 +  "associated a b \<longleftrightarrow> normalize a = normalize b" (is "?P \<longleftrightarrow> ?Q")
   2.249 +proof (cases "a = 0 \<or> b = 0")
   2.250 +  case True then show ?thesis by auto
   2.251 +next
   2.252 +  case False
   2.253 +  show ?thesis
   2.254 +  proof
   2.255 +    assume ?P then show ?Q
   2.256 +      by (rule associated_is_unitE) (simp add: normalize_mult is_unit_normalize)
   2.257 +  next
   2.258 +    from False have *: "is_unit (unit_factor a div unit_factor b)"
   2.259 +      by auto
   2.260 +    assume ?Q then have "unit_factor a * normalize a = unit_factor a * normalize b"
   2.261 +      by simp
   2.262 +    then have "a = unit_factor a * (b div unit_factor b)"
   2.263 +      by simp
   2.264 +    with False have "a = (unit_factor a div unit_factor b) * b"
   2.265 +      by (simp add: unit_div_commute unit_div_mult_swap [symmetric])
   2.266 +    with * show ?P 
   2.267 +      by (rule is_unit_associatedI)
   2.268 +  qed
   2.269 +qed
   2.270 +
   2.271 +lemma normalize_power:
   2.272 +  "normalize (a ^ n) = normalize a ^ n"
   2.273 +  by (induct n) (simp_all add: normalize_mult)
   2.274 +
   2.275 +lemma unit_factor_power:
   2.276 +  "unit_factor (a ^ n) = unit_factor a ^ n"
   2.277 +  by (induct n) (simp_all add: unit_factor_mult)
   2.278 +
   2.279 +lemma associated_eqI:
   2.280 +  assumes "associated a b"
   2.281 +  assumes "unit_factor a \<in> {0, 1}" and "unit_factor b \<in> {0, 1}"
   2.282 +  shows "a = b"
   2.283 +proof (cases "a = 0")
   2.284 +  case True with assms show ?thesis by simp
   2.285 +next
   2.286 +  case False with assms have "b \<noteq> 0" by auto
   2.287 +  with False assms have "unit_factor a = unit_factor b"
   2.288 +    by simp
   2.289 +  moreover from assms have "normalize a = normalize b"
   2.290 +    by (simp add: associated_iff_normalize)
   2.291 +  ultimately have "unit_factor a * normalize a = unit_factor b * normalize b"
   2.292 +    by simp
   2.293 +  then show ?thesis
   2.294 +    by simp
   2.295 +qed
   2.296 +
   2.297 +end
   2.298 +
   2.299 +instantiation nat :: normalization_semidom
   2.300 +begin
   2.301 +
   2.302 +definition normalize_nat
   2.303 +  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
   2.304 +
   2.305 +definition unit_factor_nat
   2.306 +  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
   2.307 +
   2.308 +lemma unit_factor_simps [simp]:
   2.309 +  "unit_factor 0 = (0::nat)"
   2.310 +  "unit_factor (Suc n) = 1"
   2.311 +  by (simp_all add: unit_factor_nat_def)
   2.312 +
   2.313 +instance
   2.314 +  by default (simp_all add: unit_factor_nat_def)
   2.315 +  
   2.316 +end
   2.317 +
   2.318 +instantiation int :: normalization_semidom
   2.319 +begin
   2.320 +
   2.321 +definition normalize_int
   2.322 +  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
   2.323 +
   2.324 +definition unit_factor_int
   2.325 +  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
   2.326 +
   2.327 +instance
   2.328 +proof
   2.329 +  fix k :: int
   2.330 +  assume "k \<noteq> 0"
   2.331 +  then have "\<bar>sgn k\<bar> = 1"
   2.332 +    by (cases "0::int" k rule: linorder_cases) simp_all
   2.333 +  then show "is_unit (unit_factor k)"
   2.334 +    by simp
   2.335 +qed (simp_all add: sgn_times mult_sgn_abs)
   2.336 +  
   2.337 +end
   2.338 +
   2.339 +end