author eberlm Fri Feb 26 14:58:07 2016 +0100 (2016-02-26) changeset 62425 d0936b500bf5 parent 62424 8c47e7fcdb8d child 62426 bd650e3a210f
Tuned Euclidean Ring instance for polynomials
```     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.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
```