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"