author haftmann Fri Jun 12 21:53:05 2015 +0200 (2015-06-12) changeset 60438 e1c345094813 parent 60437 63edc650cf67 child 60439 b765e08f8bc0
slight preference for American English
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 21:52:49 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 12 21:53:05 2015 +0200
1.3 @@ -311,78 +311,78 @@
1.4    \item division with remainder
1.5    \item a size function such that @{term "size (a mod b) < size b"}
1.6          for any @{term "b \<noteq> 0"}
1.7 -  \item a normalisation factor such that two associated numbers are equal iff
1.8 -        they are the same when divd by their normalisation factors.
1.9 +  \item a normalization factor such that two associated numbers are equal iff
1.10 +        they are the same when divd by their normalization factors.
1.11    \end{itemize}
1.12    The existence of these functions makes it possible to derive gcd and lcm functions
1.13    for any Euclidean semiring.
1.14  *}
1.15  class euclidean_semiring = semiring_div +
1.16    fixes euclidean_size :: "'a \<Rightarrow> nat"
1.17 -  fixes normalisation_factor :: "'a \<Rightarrow> 'a"
1.18 +  fixes normalization_factor :: "'a \<Rightarrow> 'a"
1.19    assumes mod_size_less [simp]:
1.20      "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
1.21    assumes size_mult_mono:
1.22      "b \<noteq> 0 \<Longrightarrow> euclidean_size (a * b) \<ge> euclidean_size a"
1.23 -  assumes normalisation_factor_is_unit [intro,simp]:
1.24 -    "a \<noteq> 0 \<Longrightarrow> is_unit (normalisation_factor a)"
1.25 -  assumes normalisation_factor_mult: "normalisation_factor (a * b) =
1.26 -    normalisation_factor a * normalisation_factor b"
1.27 -  assumes normalisation_factor_unit: "is_unit a \<Longrightarrow> normalisation_factor a = a"
1.28 -  assumes normalisation_factor_0 [simp]: "normalisation_factor 0 = 0"
1.29 +  assumes normalization_factor_is_unit [intro,simp]:
1.30 +    "a \<noteq> 0 \<Longrightarrow> is_unit (normalization_factor a)"
1.31 +  assumes normalization_factor_mult: "normalization_factor (a * b) =
1.32 +    normalization_factor a * normalization_factor b"
1.33 +  assumes normalization_factor_unit: "is_unit a \<Longrightarrow> normalization_factor a = a"
1.34 +  assumes normalization_factor_0 [simp]: "normalization_factor 0 = 0"
1.35  begin
1.36
1.37 -lemma normalisation_factor_dvd [simp]:
1.38 -  "a \<noteq> 0 \<Longrightarrow> normalisation_factor a dvd b"
1.39 +lemma normalization_factor_dvd [simp]:
1.40 +  "a \<noteq> 0 \<Longrightarrow> normalization_factor a dvd b"
1.41    by (rule unit_imp_dvd, simp)
1.42
1.43 -lemma normalisation_factor_1 [simp]:
1.44 -  "normalisation_factor 1 = 1"
1.45 -  by (simp add: normalisation_factor_unit)
1.46 +lemma normalization_factor_1 [simp]:
1.47 +  "normalization_factor 1 = 1"
1.48 +  by (simp add: normalization_factor_unit)
1.49
1.50 -lemma normalisation_factor_0_iff [simp]:
1.51 -  "normalisation_factor a = 0 \<longleftrightarrow> a = 0"
1.52 +lemma normalization_factor_0_iff [simp]:
1.53 +  "normalization_factor a = 0 \<longleftrightarrow> a = 0"
1.54  proof
1.55 -  assume "normalisation_factor a = 0"
1.56 -  hence "\<not> is_unit (normalisation_factor a)"
1.57 +  assume "normalization_factor a = 0"
1.58 +  hence "\<not> is_unit (normalization_factor a)"
1.59      by simp
1.60    then show "a = 0" by auto
1.61  qed simp
1.62
1.63 -lemma normalisation_factor_pow:
1.64 -  "normalisation_factor (a ^ n) = normalisation_factor a ^ n"
1.65 -  by (induct n) (simp_all add: normalisation_factor_mult power_Suc2)
1.66 +lemma normalization_factor_pow:
1.67 +  "normalization_factor (a ^ n) = normalization_factor a ^ n"
1.68 +  by (induct n) (simp_all add: normalization_factor_mult power_Suc2)
1.69
1.70 -lemma normalisation_correct [simp]:
1.71 -  "normalisation_factor (a div normalisation_factor a) = (if a = 0 then 0 else 1)"
1.72 +lemma normalization_correct [simp]:
1.73 +  "normalization_factor (a div normalization_factor a) = (if a = 0 then 0 else 1)"
1.74  proof (cases "a = 0", simp)
1.75    assume "a \<noteq> 0"
1.76 -  let ?nf = "normalisation_factor"
1.77 -  from normalisation_factor_is_unit[OF a \<noteq> 0] have "?nf a \<noteq> 0"
1.78 +  let ?nf = "normalization_factor"
1.79 +  from normalization_factor_is_unit[OF a \<noteq> 0] have "?nf a \<noteq> 0"
1.80      by auto
1.81    have "?nf (a div ?nf a) * ?nf (?nf a) = ?nf (a div ?nf a * ?nf a)"
1.82 -    by (simp add: normalisation_factor_mult)
1.83 +    by (simp add: normalization_factor_mult)
1.84    also have "a div ?nf a * ?nf a = a" using a \<noteq> 0
1.85      by simp
1.86    also have "?nf (?nf a) = ?nf a" using a \<noteq> 0
1.87 -    normalisation_factor_is_unit normalisation_factor_unit by simp
1.88 -  finally have "normalisation_factor (a div normalisation_factor a) = 1"
1.89 +    normalization_factor_is_unit normalization_factor_unit by simp
1.90 +  finally have "normalization_factor (a div normalization_factor a) = 1"
1.91      using ?nf a \<noteq> 0 by (metis div_mult_self2_is_id div_self)
1.92    with a \<noteq> 0 show ?thesis by simp
1.93  qed
1.94
1.95 -lemma normalisation_0_iff [simp]:
1.96 -  "a div normalisation_factor a = 0 \<longleftrightarrow> a = 0"
1.97 +lemma normalization_0_iff [simp]:
1.98 +  "a div normalization_factor a = 0 \<longleftrightarrow> a = 0"
1.99    by (cases "a = 0", simp, subst unit_eq_div1, blast, simp)
1.100
1.101 -lemma mult_div_normalisation [simp]:
1.102 -  "b * (1 div normalisation_factor a) = b div normalisation_factor a"
1.103 +lemma mult_div_normalization [simp]:
1.104 +  "b * (1 div normalization_factor a) = b div normalization_factor a"
1.105    by (cases "a = 0") simp_all
1.106
1.107  lemma associated_iff_normed_eq:
1.108 -  "associated a b \<longleftrightarrow> a div normalisation_factor a = b div normalisation_factor b"
1.109 -proof (cases "b = 0", simp, cases "a = 0", metis associated_0(1) normalisation_0_iff, rule iffI)
1.110 -  let ?nf = normalisation_factor
1.111 +  "associated a b \<longleftrightarrow> a div normalization_factor a = b div normalization_factor b"
1.112 +proof (cases "b = 0", simp, cases "a = 0", metis associated_0(1) normalization_0_iff, rule iffI)
1.113 +  let ?nf = normalization_factor
1.114    assume "a \<noteq> 0" "b \<noteq> 0" "a div ?nf a = b div ?nf b"
1.115    hence "a = b * (?nf a div ?nf b)"
1.116      apply (subst (asm) unit_eq_div1, blast, subst (asm) unit_div_commute, blast)
1.117 @@ -393,21 +393,21 @@
1.118    then obtain c where "is_unit c" and "a = c * b" by blast
1.119    then show "associated a b" by (rule is_unit_associatedI)
1.120  next
1.121 -  let ?nf = normalisation_factor
1.122 +  let ?nf = normalization_factor
1.123    assume "a \<noteq> 0" "b \<noteq> 0" "associated a b"
1.124    then obtain c where "is_unit c" and "a = c * b" by (blast elim: associated_is_unitE)
1.125    then show "a div ?nf a = b div ?nf b"
1.126 -    apply (simp only: a = c * b normalisation_factor_mult normalisation_factor_unit)
1.127 +    apply (simp only: a = c * b normalization_factor_mult normalization_factor_unit)
1.128      apply (rule div_mult_mult1, force)
1.129      done
1.130    qed
1.131
1.132  lemma normed_associated_imp_eq:
1.133 -  "associated a b \<Longrightarrow> normalisation_factor a \<in> {0, 1} \<Longrightarrow> normalisation_factor b \<in> {0, 1} \<Longrightarrow> a = b"
1.134 +  "associated a b \<Longrightarrow> normalization_factor a \<in> {0, 1} \<Longrightarrow> normalization_factor b \<in> {0, 1} \<Longrightarrow> a = b"
1.135    by (simp add: associated_iff_normed_eq, elim disjE, simp_all)
1.136
1.137 -lemmas normalisation_factor_dvd_iff [simp] =
1.138 -  unit_dvd_iff [OF normalisation_factor_is_unit]
1.139 +lemmas normalization_factor_dvd_iff [simp] =
1.140 +  unit_dvd_iff [OF normalization_factor_is_unit]
1.141
1.142  lemma euclidean_division:
1.143    fixes a :: 'a and b :: 'a
1.144 @@ -437,7 +437,7 @@
1.145
1.146  function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.147  where
1.148 -  "gcd_eucl a b = (if b = 0 then a div normalisation_factor a else gcd_eucl b (a mod b))"
1.149 +  "gcd_eucl a b = (if b = 0 then a div normalization_factor a else gcd_eucl b (a mod b))"
1.150    by (pat_completeness, simp)
1.151  termination by (relation "measure (euclidean_size \<circ> snd)", simp_all)
1.152
1.153 @@ -451,7 +451,7 @@
1.154
1.155  definition lcm_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.156  where
1.157 -  "lcm_eucl a b = a * b div (gcd_eucl a b * normalisation_factor (a * b))"
1.158 +  "lcm_eucl a b = a * b div (gcd_eucl a b * normalization_factor (a * b))"
1.159
1.160    (* Somewhat complicated definition of Lcm that has the advantage of working
1.161       for infinite sets as well *)
1.162 @@ -461,7 +461,7 @@
1.163    "Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then
1.164       let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l =
1.165         (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)
1.166 -       in l div normalisation_factor l
1.167 +       in l div normalization_factor l
1.168        else 0)"
1.169
1.170  definition Gcd_eucl :: "'a set \<Rightarrow> 'a"
1.171 @@ -484,11 +484,11 @@
1.172    by (rule gcd_red)
1.173
1.174  lemma gcd_0_left:
1.175 -  "gcd 0 a = a div normalisation_factor a"
1.176 +  "gcd 0 a = a div normalization_factor a"
1.177     by (simp only: gcd_gcd_eucl, subst gcd_eucl.simps, subst gcd_eucl.simps, simp add: Let_def)
1.178
1.179  lemma gcd_0:
1.180 -  "gcd a 0 = a div normalisation_factor a"
1.181 +  "gcd a 0 = a div normalization_factor a"
1.182    by (simp only: gcd_gcd_eucl, subst gcd_eucl.simps, simp add: Let_def)
1.183
1.184  lemma gcd_dvd1 [iff]: "gcd a b dvd a"
1.185 @@ -540,8 +540,8 @@
1.186    "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
1.187    by (metis dvd_0_left dvd_refl gcd_dvd1 gcd_dvd2 gcd_greatest)+
1.188
1.189 -lemma normalisation_factor_gcd [simp]:
1.190 -  "normalisation_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" (is "?f a b = ?g a b")
1.191 +lemma normalization_factor_gcd [simp]:
1.192 +  "normalization_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" (is "?f a b = ?g a b")
1.193  proof (induct a b rule: gcd_eucl.induct)
1.194    fix a b :: 'a
1.195    assume IH: "b \<noteq> 0 \<Longrightarrow> ?f b (a mod b) = ?g b (a mod b)"
1.196 @@ -550,7 +550,7 @@
1.197
1.198  lemma gcdI:
1.199    "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> (\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd k)
1.200 -    \<Longrightarrow> normalisation_factor k = (if k = 0 then 0 else 1) \<Longrightarrow> k = gcd a b"
1.201 +    \<Longrightarrow> normalization_factor k = (if k = 0 then 0 else 1) \<Longrightarrow> k = gcd a b"
1.202    by (intro normed_associated_imp_eq) (auto simp: associated_def intro: gcd_greatest)
1.203
1.204  sublocale gcd!: abel_semigroup gcd
1.205 @@ -565,7 +565,7 @@
1.206      moreover have "gcd (gcd a b) c dvd c" by simp
1.207      ultimately show "gcd (gcd a b) c dvd gcd b c"
1.208        by (rule gcd_greatest)
1.209 -    show "normalisation_factor (gcd (gcd a b) c) =  (if gcd (gcd a b) c = 0 then 0 else 1)"
1.210 +    show "normalization_factor (gcd (gcd a b) c) =  (if gcd (gcd a b) c = 0 then 0 else 1)"
1.211        by auto
1.212      fix l assume "l dvd a" and "l dvd gcd b c"
1.213      with dvd_trans[OF _ gcd_dvd1] and dvd_trans[OF _ gcd_dvd2]
1.214 @@ -580,7 +580,7 @@
1.215  qed
1.216
1.217  lemma gcd_unique: "d dvd a \<and> d dvd b \<and>
1.218 -    normalisation_factor d = (if d = 0 then 0 else 1) \<and>
1.219 +    normalization_factor d = (if d = 0 then 0 else 1) \<and>
1.220      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
1.221    by (rule, auto intro: gcdI simp: gcd_greatest)
1.222
1.223 @@ -594,29 +594,29 @@
1.224    by (rule sym, rule gcdI, simp_all)
1.225
1.226  lemma gcd_proj2_if_dvd:
1.227 -  "b dvd a \<Longrightarrow> gcd a b = b div normalisation_factor b"
1.228 +  "b dvd a \<Longrightarrow> gcd a b = b div normalization_factor b"
1.229    by (cases "b = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0 gcd_0)
1.230
1.231  lemma gcd_proj1_if_dvd:
1.232 -  "a dvd b \<Longrightarrow> gcd a b = a div normalisation_factor a"
1.233 +  "a dvd b \<Longrightarrow> gcd a b = a div normalization_factor a"
1.234    by (subst gcd.commute, simp add: gcd_proj2_if_dvd)
1.235
1.236 -lemma gcd_proj1_iff: "gcd m n = m div normalisation_factor m \<longleftrightarrow> m dvd n"
1.237 +lemma gcd_proj1_iff: "gcd m n = m div normalization_factor m \<longleftrightarrow> m dvd n"
1.238  proof
1.239 -  assume A: "gcd m n = m div normalisation_factor m"
1.240 +  assume A: "gcd m n = m div normalization_factor m"
1.241    show "m dvd n"
1.242    proof (cases "m = 0")
1.243      assume [simp]: "m \<noteq> 0"
1.244 -    from A have B: "m = gcd m n * normalisation_factor m"
1.245 +    from A have B: "m = gcd m n * normalization_factor m"
1.247      show ?thesis by (subst B, simp add: mult_unit_dvd_iff)
1.248    qed (insert A, simp)
1.249  next
1.250    assume "m dvd n"
1.251 -  then show "gcd m n = m div normalisation_factor m" by (rule gcd_proj1_if_dvd)
1.252 +  then show "gcd m n = m div normalization_factor m" by (rule gcd_proj1_if_dvd)
1.253  qed
1.254
1.255 -lemma gcd_proj2_iff: "gcd m n = n div normalisation_factor n \<longleftrightarrow> n dvd m"
1.256 +lemma gcd_proj2_iff: "gcd m n = n div normalization_factor n \<longleftrightarrow> n dvd m"
1.257    by (subst gcd.commute, simp add: gcd_proj1_iff)
1.258
1.259  lemma gcd_mod1 [simp]:
1.260 @@ -627,21 +627,21 @@
1.261    "gcd a (b mod a) = gcd a b"
1.262    by (rule gcdI, simp, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff)
1.263
1.264 -lemma normalisation_factor_dvd' [simp]:
1.265 -  "normalisation_factor a dvd a"
1.266 +lemma normalization_factor_dvd' [simp]:
1.267 +  "normalization_factor a dvd a"
1.268    by (cases "a = 0", simp_all)
1.269
1.270  lemma gcd_mult_distrib':
1.271 -  "k div normalisation_factor k * gcd a b = gcd (k*a) (k*b)"
1.272 +  "k div normalization_factor k * gcd a b = gcd (k*a) (k*b)"
1.273  proof (induct a b rule: gcd_eucl.induct)
1.274    case (1 a b)
1.275    show ?case
1.276    proof (cases "b = 0")
1.277      case True
1.278 -    then show ?thesis by (simp add: normalisation_factor_mult gcd_0 algebra_simps div_mult_div_if_dvd)
1.279 +    then show ?thesis by (simp add: normalization_factor_mult gcd_0 algebra_simps div_mult_div_if_dvd)
1.280    next
1.281      case False
1.282 -    hence "k div normalisation_factor k * gcd a b =  gcd (k * b) (k * (a mod b))"
1.283 +    hence "k div normalization_factor k * gcd a b =  gcd (k * b) (k * (a mod b))"
1.284        using 1 by (subst gcd_red, simp)
1.285      also have "... = gcd (k * a) (k * b)"
1.286        by (simp add: mult_mod_right gcd.commute)
1.287 @@ -650,13 +650,13 @@
1.288  qed
1.289
1.290  lemma gcd_mult_distrib:
1.291 -  "k * gcd a b = gcd (k*a) (k*b) * normalisation_factor k"
1.292 +  "k * gcd a b = gcd (k*a) (k*b) * normalization_factor k"
1.293  proof-
1.294 -  let ?nf = "normalisation_factor"
1.295 +  let ?nf = "normalization_factor"
1.296    from gcd_mult_distrib'
1.297      have "gcd (k*a) (k*b) = k div ?nf k * gcd a b" ..
1.298    also have "... = k * gcd a b div ?nf k"
1.299 -    by (metis dvd_div_mult dvd_eq_mod_eq_0 mod_0 normalisation_factor_dvd)
1.300 +    by (metis dvd_div_mult dvd_eq_mod_eq_0 mod_0 normalization_factor_dvd)
1.301    finally show ?thesis
1.302      by simp
1.303  qed
1.304 @@ -696,7 +696,7 @@
1.305    apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps)
1.306    apply (rule gcd_dvd2)
1.307    apply (rule gcd_greatest, simp add: unit_simps, assumption)
1.308 -  apply (subst normalisation_factor_gcd, simp add: gcd_0)
1.309 +  apply (subst normalization_factor_gcd, simp add: gcd_0)
1.310    done
1.311
1.312  lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
1.313 @@ -708,7 +708,7 @@
1.314  lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
1.315    by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
1.316
1.317 -lemma gcd_idem: "gcd a a = a div normalisation_factor a"
1.318 +lemma gcd_idem: "gcd a a = a div normalization_factor a"
1.319    by (cases "a = 0") (simp add: gcd_0_left, rule sym, rule gcdI, simp_all)
1.320
1.321  lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
1.322 @@ -740,7 +740,7 @@
1.323    assumes "gcd c b = 1" and "c dvd a * b"
1.324    shows "c dvd a"
1.325  proof -
1.326 -  let ?nf = "normalisation_factor"
1.327 +  let ?nf = "normalization_factor"
1.328    from assms gcd_mult_distrib [of a c b]
1.329      have A: "a = gcd (a * c) (a * b) * ?nf a" by simp
1.330    from c dvd a * b show ?thesis by (subst A, simp_all add: gcd_greatest)
1.331 @@ -758,7 +758,7 @@
1.332    with A show "gcd a b dvd c" by (rule dvd_trans)
1.333    have "gcd c d dvd d" by simp
1.334    with A show "gcd a b dvd d" by (rule dvd_trans)
1.335 -  show "normalisation_factor (gcd a b) = (if gcd a b = 0 then 0 else 1)"
1.336 +  show "normalization_factor (gcd a b) = (if gcd a b = 0 then 0 else 1)"
1.337      by simp
1.338    fix l assume "l dvd c" and "l dvd d"
1.339    hence "l dvd gcd c d" by (rule gcd_greatest)
1.340 @@ -919,8 +919,8 @@
1.341      using div_gcd_coprime by (subst sym, auto simp: div_gcd_coprime)
1.342    hence "(gcd a b) ^ n = (gcd a b) ^ n * ..." by simp
1.343    also note gcd_mult_distrib
1.344 -  also have "normalisation_factor ((gcd a b)^n) = 1"
1.345 -    by (simp add: normalisation_factor_pow A)
1.346 +  also have "normalization_factor ((gcd a b)^n) = 1"
1.347 +    by (simp add: normalization_factor_pow A)
1.348    also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
1.349      by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp)
1.350    also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
1.351 @@ -1042,13 +1042,13 @@
1.352  qed
1.353
1.354  lemma lcm_gcd:
1.355 -  "lcm a b = a * b div (gcd a b * normalisation_factor (a*b))"
1.356 +  "lcm a b = a * b div (gcd a b * normalization_factor (a*b))"
1.357    by (simp only: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def)
1.358
1.359  lemma lcm_gcd_prod:
1.360 -  "lcm a b * gcd a b = a * b div normalisation_factor (a*b)"
1.361 +  "lcm a b * gcd a b = a * b div normalization_factor (a*b)"
1.362  proof (cases "a * b = 0")
1.363 -  let ?nf = normalisation_factor
1.364 +  let ?nf = normalization_factor
1.365    assume "a * b \<noteq> 0"
1.366    hence "gcd a b \<noteq> 0" by simp
1.367    from lcm_gcd have "lcm a b * gcd a b = gcd a b * (a * b div (?nf (a*b) * gcd a b))"
1.368 @@ -1063,8 +1063,8 @@
1.369  proof (cases "a*b = 0")
1.370    assume "a * b \<noteq> 0"
1.371    hence "gcd a b \<noteq> 0" by simp
1.372 -  let ?c = "1 div normalisation_factor (a * b)"
1.373 -  from a * b \<noteq> 0 have [simp]: "is_unit (normalisation_factor (a * b))" by simp
1.374 +  let ?c = "1 div normalization_factor (a * b)"
1.375 +  from a * b \<noteq> 0 have [simp]: "is_unit (normalization_factor (a * b))" by simp
1.376    from lcm_gcd_prod[of a b] have "lcm a b * gcd a b = a * ?c * b"
1.377      by (simp add: div_mult_swap unit_div_commute)
1.378    hence "lcm a b * gcd a b div gcd a b = a * ?c * b div gcd a b" by simp
1.379 @@ -1078,7 +1078,7 @@
1.380  lemma lcm_least:
1.381    "\<lbrakk>a dvd k; b dvd k\<rbrakk> \<Longrightarrow> lcm a b dvd k"
1.382  proof (cases "k = 0")
1.383 -  let ?nf = normalisation_factor
1.384 +  let ?nf = normalization_factor
1.385    assume "k \<noteq> 0"
1.386    hence "is_unit (?nf k)" by simp
1.387    hence "?nf k \<noteq> 0" by (metis not_is_unit_0)
1.388 @@ -1120,7 +1120,7 @@
1.389  lemma lcm_zero:
1.390    "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
1.391  proof -
1.392 -  let ?nf = normalisation_factor
1.393 +  let ?nf = normalization_factor
1.394    {
1.395      assume "a \<noteq> 0" "b \<noteq> 0"
1.396      hence "a * b div ?nf (a * b) \<noteq> 0" by (simp add: no_zero_divisors)
1.397 @@ -1137,30 +1137,30 @@
1.398
1.399  lemma gcd_lcm:
1.400    assumes "lcm a b \<noteq> 0"
1.401 -  shows "gcd a b = a * b div (lcm a b * normalisation_factor (a * b))"
1.402 +  shows "gcd a b = a * b div (lcm a b * normalization_factor (a * b))"
1.403  proof-
1.404    from assms have "gcd a b \<noteq> 0" by (simp add: lcm_zero)
1.405 -  let ?c = "normalisation_factor (a * b)"
1.406 +  let ?c = "normalization_factor (a * b)"
1.407    from lcm a b \<noteq> 0 have "?c \<noteq> 0" by (intro notI, simp add: lcm_zero no_zero_divisors)
1.408    hence "is_unit ?c" by simp
1.409    from lcm_gcd_prod [of a b] have "gcd a b = a * b div ?c div lcm a b"
1.410      by (subst (2) div_mult_self2_is_id[OF lcm a b \<noteq> 0, symmetric], simp add: mult_ac)
1.411    also from is_unit ?c have "... = a * b div (lcm a b * ?c)"
1.412 -    by (metis ?c \<noteq> 0 div_mult_mult1 dvd_mult_div_cancel mult_commute normalisation_factor_dvd')
1.413 +    by (metis ?c \<noteq> 0 div_mult_mult1 dvd_mult_div_cancel mult_commute normalization_factor_dvd')
1.414    finally show ?thesis .
1.415  qed
1.416
1.417 -lemma normalisation_factor_lcm [simp]:
1.418 -  "normalisation_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
1.419 +lemma normalization_factor_lcm [simp]:
1.420 +  "normalization_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
1.421  proof (cases "a = 0 \<or> b = 0")
1.422    case True then show ?thesis
1.423      by (auto simp add: lcm_gcd)
1.424  next
1.425    case False
1.426 -  let ?nf = normalisation_factor
1.427 +  let ?nf = normalization_factor
1.428    from lcm_gcd_prod[of a b]
1.429      have "?nf (lcm a b) * ?nf (gcd a b) = ?nf (a*b) div ?nf (a*b)"
1.430 -    by (metis div_by_0 div_self normalisation_correct normalisation_factor_0 normalisation_factor_mult)
1.431 +    by (metis div_by_0 div_self normalization_correct normalization_factor_0 normalization_factor_mult)
1.432    also have "... = (if a*b = 0 then 0 else 1)"
1.433      by simp
1.434    finally show ?thesis using False by simp
1.435 @@ -1171,7 +1171,7 @@
1.436
1.437  lemma lcmI:
1.438    "\<lbrakk>a dvd k; b dvd k; \<And>l. a dvd l \<Longrightarrow> b dvd l \<Longrightarrow> k dvd l;
1.439 -    normalisation_factor k = (if k = 0 then 0 else 1)\<rbrakk> \<Longrightarrow> k = lcm a b"
1.440 +    normalization_factor k = (if k = 0 then 0 else 1)\<rbrakk> \<Longrightarrow> k = lcm a b"
1.441    by (intro normed_associated_imp_eq) (auto simp: associated_def intro: lcm_least)
1.442
1.443  sublocale lcm!: abel_semigroup lcm
1.444 @@ -1222,8 +1222,8 @@
1.445    assume "is_unit a \<and> is_unit b"
1.446    hence "a dvd 1" and "b dvd 1" by simp_all
1.447    hence "is_unit (lcm a b)" by (rule lcm_least)
1.448 -  hence "lcm a b = normalisation_factor (lcm a b)"
1.449 -    by (subst normalisation_factor_unit, simp_all)
1.450 +  hence "lcm a b = normalization_factor (lcm a b)"
1.451 +    by (subst normalization_factor_unit, simp_all)
1.452    also have "\<dots> = 1" using is_unit a \<and> is_unit b
1.453      by auto
1.454    finally show "lcm a b = 1" .
1.455 @@ -1239,7 +1239,7 @@
1.456
1.457  lemma lcm_unique:
1.458    "a dvd d \<and> b dvd d \<and>
1.459 -  normalisation_factor d = (if d = 0 then 0 else 1) \<and>
1.460 +  normalization_factor d = (if d = 0 then 0 else 1) \<and>
1.461    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
1.462    by (rule, auto intro: lcmI simp: lcm_least lcm_zero)
1.463
1.464 @@ -1252,43 +1252,43 @@
1.465    by (metis lcm_dvd2 dvd_trans)
1.466
1.467  lemma lcm_1_left [simp]:
1.468 -  "lcm 1 a = a div normalisation_factor a"
1.469 +  "lcm 1 a = a div normalization_factor a"
1.470    by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
1.471
1.472  lemma lcm_1_right [simp]:
1.473 -  "lcm a 1 = a div normalisation_factor a"
1.474 +  "lcm a 1 = a div normalization_factor a"
1.475    using lcm_1_left [of a] by (simp add: ac_simps)
1.476
1.477  lemma lcm_coprime:
1.478 -  "gcd a b = 1 \<Longrightarrow> lcm a b = a * b div normalisation_factor (a*b)"
1.479 +  "gcd a b = 1 \<Longrightarrow> lcm a b = a * b div normalization_factor (a*b)"
1.480    by (subst lcm_gcd) simp
1.481
1.482  lemma lcm_proj1_if_dvd:
1.483 -  "b dvd a \<Longrightarrow> lcm a b = a div normalisation_factor a"
1.484 +  "b dvd a \<Longrightarrow> lcm a b = a div normalization_factor a"
1.485    by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
1.486
1.487  lemma lcm_proj2_if_dvd:
1.488 -  "a dvd b \<Longrightarrow> lcm a b = b div normalisation_factor b"
1.489 +  "a dvd b \<Longrightarrow> lcm a b = b div normalization_factor b"
1.490    using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
1.491
1.492  lemma lcm_proj1_iff:
1.493 -  "lcm m n = m div normalisation_factor m \<longleftrightarrow> n dvd m"
1.494 +  "lcm m n = m div normalization_factor m \<longleftrightarrow> n dvd m"
1.495  proof
1.496 -  assume A: "lcm m n = m div normalisation_factor m"
1.497 +  assume A: "lcm m n = m div normalization_factor m"
1.498    show "n dvd m"
1.499    proof (cases "m = 0")
1.500      assume [simp]: "m \<noteq> 0"
1.501 -    from A have B: "m = lcm m n * normalisation_factor m"
1.502 +    from A have B: "m = lcm m n * normalization_factor m"
1.504      show ?thesis by (subst B, simp)
1.505    qed simp
1.506  next
1.507    assume "n dvd m"
1.508 -  then show "lcm m n = m div normalisation_factor m" by (rule lcm_proj1_if_dvd)
1.509 +  then show "lcm m n = m div normalization_factor m" by (rule lcm_proj1_if_dvd)
1.510  qed
1.511
1.512  lemma lcm_proj2_iff:
1.513 -  "lcm m n = n div normalisation_factor n \<longleftrightarrow> m dvd n"
1.514 +  "lcm m n = n div normalization_factor n \<longleftrightarrow> m dvd n"
1.515    using lcm_proj1_iff [of n m] by (simp add: ac_simps)
1.516
1.517  lemma euclidean_size_lcm_le1:
1.518 @@ -1330,7 +1330,7 @@
1.519    apply (rule dvd_trans[of _ "b * a"], simp, rule lcm_dvd1)
1.520    apply (rule lcm_dvd2)
1.521    apply (rule lcm_least, simp add: unit_simps, assumption)
1.522 -  apply (subst normalisation_factor_lcm, simp add: lcm_zero)
1.523 +  apply (subst normalization_factor_lcm, simp add: lcm_zero)
1.524    done
1.525
1.526  lemma lcm_mult_unit2:
1.527 @@ -1375,11 +1375,11 @@
1.528
1.529  lemma dvd_Lcm [simp]: "a \<in> A \<Longrightarrow> a dvd Lcm A"
1.530    and Lcm_dvd [simp]: "(\<forall>a\<in>A. a dvd l') \<Longrightarrow> Lcm A dvd l'"
1.531 -  and normalisation_factor_Lcm [simp]:
1.532 -          "normalisation_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
1.533 +  and normalization_factor_Lcm [simp]:
1.534 +          "normalization_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
1.535  proof -
1.536    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.537 -    normalisation_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" (is ?thesis)
1.538 +    normalization_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" (is ?thesis)
1.539    proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>a\<in>A. a dvd l)")
1.540      case False
1.541      hence "Lcm A = 0" by (auto simp: Lcm_Lcm_eucl Lcm_eucl_def)
1.542 @@ -1421,13 +1421,13 @@
1.543        hence "l dvd l'" by (blast dest: dvd_gcd_D2)
1.544      }
1.545
1.546 -    with (\<forall>a\<in>A. a dvd l) and normalisation_factor_is_unit[OF l \<noteq> 0] and l \<noteq> 0
1.547 -      have "(\<forall>a\<in>A. a dvd l div normalisation_factor l) \<and>
1.548 -        (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> l div normalisation_factor l dvd l') \<and>
1.549 -        normalisation_factor (l div normalisation_factor l) =
1.550 -        (if l div normalisation_factor l = 0 then 0 else 1)"
1.551 +    with (\<forall>a\<in>A. a dvd l) and normalization_factor_is_unit[OF l \<noteq> 0] and l \<noteq> 0
1.552 +      have "(\<forall>a\<in>A. a dvd l div normalization_factor l) \<and>
1.553 +        (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> l div normalization_factor l dvd l') \<and>
1.554 +        normalization_factor (l div normalization_factor l) =
1.555 +        (if l div normalization_factor l = 0 then 0 else 1)"
1.556        by (auto simp: unit_simps)
1.557 -    also from True have "l div normalisation_factor l = Lcm A"
1.558 +    also from True have "l div normalization_factor l = Lcm A"
1.559        by (simp add: Lcm_Lcm_eucl Lcm_eucl_def Let_def n_def l_def)
1.560      finally show ?thesis .
1.561    qed
1.562 @@ -1435,12 +1435,12 @@
1.563
1.564    {fix a assume "a \<in> A" then show "a dvd Lcm A" using A by blast}
1.565    {fix l' assume "\<forall>a\<in>A. a dvd l'" then show "Lcm A dvd l'" using A by blast}
1.566 -  from A show "normalisation_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" by blast
1.567 +  from A show "normalization_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" by blast
1.568  qed
1.569
1.570  lemma LcmI:
1.571    "(\<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.572 -      normalisation_factor l = (if l = 0 then 0 else 1) \<Longrightarrow> l = Lcm A"
1.573 +      normalization_factor l = (if l = 0 then 0 else 1) \<Longrightarrow> l = Lcm A"
1.574    by (intro normed_associated_imp_eq)
1.575      (auto intro: Lcm_dvd dvd_Lcm simp: associated_def)
1.576
1.577 @@ -1501,8 +1501,8 @@
1.579        done
1.580      from someI_ex[OF this] have "l \<noteq> 0" unfolding l_def by simp_all
1.581 -    hence "l div normalisation_factor l \<noteq> 0" by simp
1.582 -    also from ex have "l div normalisation_factor l = Lcm A"
1.583 +    hence "l div normalization_factor l \<noteq> 0" by simp
1.584 +    also from ex have "l div normalization_factor l = Lcm A"
1.585         by (simp only: Lcm_Lcm_eucl Lcm_eucl_def n_def l_def if_True Let_def)
1.586      finally show False using Lcm A = 0 by contradiction
1.587    qed
1.588 @@ -1556,7 +1556,7 @@
1.589    using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite by (simp add: ac_simps)
1.590
1.591  lemma Lcm_singleton [simp]:
1.592 -  "Lcm {a} = a div normalisation_factor a"
1.593 +  "Lcm {a} = a div normalization_factor a"
1.594    by simp
1.595
1.596  lemma Lcm_2 [simp]:
1.597 @@ -1567,21 +1567,21 @@
1.598  lemma Lcm_coprime:
1.599    assumes "finite A" and "A \<noteq> {}"
1.600    assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
1.601 -  shows "Lcm A = \<Prod>A div normalisation_factor (\<Prod>A)"
1.602 +  shows "Lcm A = \<Prod>A div normalization_factor (\<Prod>A)"
1.603  using assms proof (induct rule: finite_ne_induct)
1.604    case (insert a A)
1.605    have "Lcm (insert a A) = lcm a (Lcm A)" by simp
1.606 -  also from insert have "Lcm A = \<Prod>A div normalisation_factor (\<Prod>A)" by blast
1.607 +  also from insert have "Lcm A = \<Prod>A div normalization_factor (\<Prod>A)" by blast
1.608    also have "lcm a \<dots> = lcm a (\<Prod>A)" by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
1.609    also from insert have "gcd a (\<Prod>A) = 1" by (subst gcd.commute, intro setprod_coprime) auto
1.610 -  with insert have "lcm a (\<Prod>A) = \<Prod>(insert a A) div normalisation_factor (\<Prod>(insert a A))"
1.611 +  with insert have "lcm a (\<Prod>A) = \<Prod>(insert a A) div normalization_factor (\<Prod>(insert a A))"
1.613    finally show ?case .
1.614  qed simp
1.615
1.616  lemma Lcm_coprime':
1.617    "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.618 -    \<Longrightarrow> Lcm A = \<Prod>A div normalisation_factor (\<Prod>A)"
1.619 +    \<Longrightarrow> Lcm A = \<Prod>A div normalization_factor (\<Prod>A)"
1.620    by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
1.621
1.622  lemma Gcd_Lcm:
1.623 @@ -1590,8 +1590,8 @@
1.624
1.625  lemma Gcd_dvd [simp]: "a \<in> A \<Longrightarrow> Gcd A dvd a"
1.626    and dvd_Gcd [simp]: "(\<forall>a\<in>A. g' dvd a) \<Longrightarrow> g' dvd Gcd A"
1.627 -  and normalisation_factor_Gcd [simp]:
1.628 -    "normalisation_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
1.629 +  and normalization_factor_Gcd [simp]:
1.630 +    "normalization_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
1.631  proof -
1.632    fix a assume "a \<in> A"
1.633    hence "Lcm {d. \<forall>a\<in>A. d dvd a} dvd a" by (intro Lcm_dvd) blast
1.634 @@ -1601,13 +1601,13 @@
1.635    hence "g' dvd Lcm {d. \<forall>a\<in>A. d dvd a}" by (intro dvd_Lcm) blast
1.636    then show "g' dvd Gcd A" by (simp add: Gcd_Lcm)
1.637  next
1.638 -  show "normalisation_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
1.639 +  show "normalization_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
1.641  qed
1.642
1.643  lemma GcdI:
1.644    "(\<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.645 -    normalisation_factor l = (if l = 0 then 0 else 1) \<Longrightarrow> l = Gcd A"
1.646 +    normalization_factor l = (if l = 0 then 0 else 1) \<Longrightarrow> l = Gcd A"
1.647    by (intro normed_associated_imp_eq)
1.648      (auto intro: Gcd_dvd dvd_Gcd simp: associated_def)
1.649
1.650 @@ -1648,7 +1648,7 @@
1.651    "Gcd (set xs) = fold gcd xs 0"
1.652    using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite by (simp add: ac_simps)
1.653
1.654 -lemma Gcd_singleton [simp]: "Gcd {a} = a div normalisation_factor a"
1.655 +lemma Gcd_singleton [simp]: "Gcd {a} = a div normalization_factor a"
1.657
1.658  lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b"
1.659 @@ -1713,7 +1713,7 @@
1.660  function euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a \<times> 'a" where
1.661    "euclid_ext a b =
1.662       (if b = 0 then
1.663 -        let c = 1 div normalisation_factor a in (c, 0, a * c)
1.664 +        let c = 1 div normalization_factor a in (c, 0, a * c)
1.665        else
1.666          case euclid_ext b (a mod b) of
1.667              (s,t,c) \<Rightarrow> (t, s - t * (a div b), c))"
1.668 @@ -1723,7 +1723,7 @@
1.669  declare euclid_ext.simps [simp del]
1.670
1.671  lemma euclid_ext_0:
1.672 -  "euclid_ext a 0 = (1 div normalisation_factor a, 0, a div normalisation_factor a)"
1.673 +  "euclid_ext a 0 = (1 div normalization_factor a, 0, a div normalization_factor a)"
1.674    by (subst euclid_ext.simps) (simp add: Let_def)
1.675
1.676  lemma euclid_ext_non_0:
1.677 @@ -1787,7 +1787,7 @@
1.678  lemma bezout: "\<exists>s t. s * a + t * b = gcd a b"
1.679    using euclid_ext'_correct by blast
1.680
1.681 -lemma euclid_ext'_0 [simp]: "euclid_ext' a 0 = (1 div normalisation_factor a, 0)"
1.682 +lemma euclid_ext'_0 [simp]: "euclid_ext' a 0 = (1 div normalization_factor a, 0)"
1.683    by (simp add: bezw_def euclid_ext'_def euclid_ext_0)
1.684
1.685  lemma euclid_ext'_non_0: "b \<noteq> 0 \<Longrightarrow> euclid_ext' a b = (snd (euclid_ext' b (a mod b)),
1.686 @@ -1804,7 +1804,7 @@
1.687    "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
1.688
1.689  definition [simp]:
1.690 -  "normalisation_factor_nat (n::nat) = (if n = 0 then 0 else 1 :: nat)"
1.691 +  "normalization_factor_nat (n::nat) = (if n = 0 then 0 else 1 :: nat)"
1.692
1.693  instance proof
1.694  qed simp_all
1.695 @@ -1818,7 +1818,7 @@
1.696    "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
1.697
1.698  definition [simp]:
1.699 -  "normalisation_factor_int = (sgn :: int \<Rightarrow> int)"
1.700 +  "normalization_factor_int = (sgn :: int \<Rightarrow> int)"
1.701
1.702  instance proof
1.703    case goal2 then show ?case by (auto simp add: abs_mult nat_mult_distrib)