author haftmann Thu Jul 02 10:06:47 2015 +0200 (2015-07-02) changeset 60634 e3b6e516608b parent 60633 f758c40e0a9a child 60635 22830a64358f
separate (semi)ring with normalization
     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.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.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.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.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.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.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