Tuned Euclidean Ring instance for polynomials
authoreberlm
Fri Feb 26 14:58:07 2016 +0100 (2016-02-26)
changeset 62425d0936b500bf5
parent 62424 8c47e7fcdb8d
child 62426 bd650e3a210f
Tuned Euclidean Ring instance for polynomials
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Fri Feb 26 11:57:36 2016 +0100
     1.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Fri Feb 26 14:58:07 2016 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4    Complex_Main
     1.5    "~~/src/HOL/Library/Library"
     1.6    "~~/src/HOL/Library/Sublist_Order"
     1.7 -  "~~/src/HOL/Library/Polynomial_GCD_euclidean"
     1.8 +  "~~/src/HOL/Number_Theory/Euclidean_Algorithm"
     1.9    "~~/src/HOL/Data_Structures/Tree_Map"
    1.10    "~~/src/HOL/Data_Structures/Tree_Set"
    1.11    "~~/src/HOL/Number_Theory/Eratosthenes"
     2.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Feb 26 11:57:36 2016 +0100
     2.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Feb 26 14:58:07 2016 +0100
     2.3 @@ -1213,4 +1213,41 @@
     2.4  instance by standard (simp_all only: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def)
     2.5  end
     2.6  
     2.7 +lemma poly_gcd_monic:
     2.8 +  "lead_coeff (gcd x y) = (if x = 0 \<and> y = 0 then 0 else 1)"
     2.9 +  using unit_factor_gcd[of x y]
    2.10 +  by (simp add: unit_factor_poly_def monom_0 one_poly_def lead_coeff_def split: if_split_asm)
    2.11 +
    2.12 +lemma poly_dvd_antisym:
    2.13 +  fixes p q :: "'a::idom poly"
    2.14 +  assumes coeff: "coeff p (degree p) = coeff q (degree q)"
    2.15 +  assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
    2.16 +proof (cases "p = 0")
    2.17 +  case True with coeff show "p = q" by simp
    2.18 +next
    2.19 +  case False with coeff have "q \<noteq> 0" by auto
    2.20 +  have degree: "degree p = degree q"
    2.21 +    using \<open>p dvd q\<close> \<open>q dvd p\<close> \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close>
    2.22 +    by (intro order_antisym dvd_imp_degree_le)
    2.23 +
    2.24 +  from \<open>p dvd q\<close> obtain a where a: "q = p * a" ..
    2.25 +  with \<open>q \<noteq> 0\<close> have "a \<noteq> 0" by auto
    2.26 +  with degree a \<open>p \<noteq> 0\<close> have "degree a = 0"
    2.27 +    by (simp add: degree_mult_eq)
    2.28 +  with coeff a show "p = q"
    2.29 +    by (cases a, auto split: if_splits)
    2.30 +qed
    2.31 +
    2.32 +lemma poly_gcd_unique:
    2.33 +  fixes d x y :: "_ poly"
    2.34 +  assumes dvd1: "d dvd x" and dvd2: "d dvd y"
    2.35 +    and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d"
    2.36 +    and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)"
    2.37 +  shows "d = gcd x y"
    2.38 +  using assms by (intro gcdI) (auto simp: normalize_poly_def split: if_split_asm)
    2.39 +
    2.40 +lemma poly_gcd_code [code]:
    2.41 +  "gcd x y = (if y = 0 then normalize x else gcd y (x mod (y :: _ poly)))"
    2.42 +  by (simp add: gcd_0 gcd_non_0)
    2.43 +
    2.44  end