src/HOL/Number_Theory/Euclidean_Algorithm.thy
 changeset 64848 c50db2128048 parent 64786 340db65fd2c1 child 64850 fc9265882329
```     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Jan 09 15:54:48 2017 +0000
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Jan 09 18:53:06 2017 +0100
1.3 @@ -71,7 +71,7 @@
1.4
1.5  lemma semiring_gcd:
1.6    "class.semiring_gcd one zero times gcd lcm
1.7 -    divide plus minus normalize unit_factor"
1.8 +    divide plus minus unit_factor normalize"
1.9  proof
1.10    show "gcd a b dvd a"
1.11      and "gcd a b dvd b" for a b
1.12 @@ -97,12 +97,12 @@
1.13  qed
1.14
1.15  interpretation semiring_gcd one zero times gcd lcm
1.16 -  divide plus minus normalize unit_factor
1.17 +  divide plus minus unit_factor normalize
1.18    by (fact semiring_gcd)
1.19
1.20  lemma semiring_Gcd:
1.21    "class.semiring_Gcd one zero times gcd lcm Gcd Lcm
1.22 -    divide plus minus normalize unit_factor"
1.23 +    divide plus minus unit_factor normalize"
1.24  proof -
1.25    show ?thesis
1.26    proof
1.27 @@ -180,13 +180,13 @@
1.28  qed
1.29
1.30  interpretation semiring_Gcd one zero times gcd lcm Gcd Lcm
1.31 -    divide plus minus normalize unit_factor
1.32 +    divide plus minus unit_factor normalize
1.33    by (fact semiring_Gcd)
1.34
1.35  subclass factorial_semiring
1.36  proof -
1.37    show "class.factorial_semiring divide plus minus zero times one
1.38 -     normalize unit_factor"
1.39 +     unit_factor normalize"
1.40    proof (standard, rule factorial_semiring_altI_aux) -- \<open>FIXME rule\<close>
1.41      fix x assume "x \<noteq> 0"
1.42      thus "finite {p. p dvd x \<and> normalize p = p}"
1.43 @@ -406,7 +406,7 @@
1.44    interpret semiring_Gcd 1 0 times
1.45      Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
1.46      Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
1.47 -    divide plus minus normalize unit_factor
1.48 +    divide plus minus unit_factor normalize
1.49      rewrites "dvd.dvd op * = Rings.dvd"
1.50      by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
1.51    show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
1.52 @@ -558,7 +558,7 @@
1.53    interpret semiring_Gcd 1 0 times
1.54      "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
1.55      "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
1.56 -    divide plus minus normalize unit_factor
1.57 +    divide plus minus unit_factor normalize
1.58      rewrites "dvd.dvd op * = Rings.dvd"
1.59      by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
1.60    show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
1.61 @@ -590,7 +590,7 @@
1.62    interpret semiring_Gcd 1 0 times
1.63      "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
1.64      "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
1.65 -    divide plus minus normalize unit_factor
1.66 +    divide plus minus unit_factor normalize
1.67      rewrites "dvd.dvd op * = Rings.dvd"
1.68      by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
1.69    show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
```