slight preference for American English
authorhaftmann
Fri Jun 12 21:53:05 2015 +0200 (2015-06-12)
changeset 60438e1c345094813
parent 60437 63edc650cf67
child 60439 b765e08f8bc0
slight preference for American English
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     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.246        by (simp add: unit_eq_div2)
   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.503        by (simp add: unit_eq_div2)
   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.578        apply (simp add: l\<^sub>0_props)
   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.612      by (simp add: lcm_coprime)
   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.640      by (simp add: Gcd_Lcm)
   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.656    by (simp add: gcd_0)
   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)