src/HOL/Library/Polynomial.thy
 changeset 60352 d46de31a50c4 parent 60040 1fa1023b13b9 child 60429 d3d1e185cd63
```     1.1 --- a/src/HOL/Library/Polynomial.thy	Mon Jun 01 18:59:21 2015 +0200
1.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Jun 01 18:59:21 2015 +0200
1.3 @@ -1360,14 +1360,14 @@
1.4  instantiation poly :: (field) ring_div
1.5  begin
1.6
1.7 -definition div_poly where
1.8 -  "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
1.9 +definition divide_poly where
1.10 +  div_poly_def: "divide x y = (THE q. \<exists>r. pdivmod_rel x y q r)"
1.11
1.12  definition mod_poly where
1.13    "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
1.14
1.15  lemma div_poly_eq:
1.16 -  "pdivmod_rel x y q r \<Longrightarrow> x div y = q"
1.17 +  "pdivmod_rel x y q r \<Longrightarrow> divide x y = q"
1.18  unfolding div_poly_def
1.19  by (fast elim: pdivmod_rel_unique_div)
1.20
1.21 @@ -1377,7 +1377,7 @@
1.22  by (fast elim: pdivmod_rel_unique_mod)
1.23
1.24  lemma pdivmod_rel:
1.25 -  "pdivmod_rel x y (x div y) (x mod y)"
1.26 +  "pdivmod_rel x y (divide x y) (x mod y)"
1.27  proof -
1.28    from pdivmod_rel_exists
1.29      obtain q r where "pdivmod_rel x y q r" by fast
1.30 @@ -1387,41 +1387,41 @@
1.31
1.32  instance proof
1.33    fix x y :: "'a poly"
1.34 -  show "x div y * y + x mod y = x"
1.35 +  show "divide x y * y + x mod y = x"
1.36      using pdivmod_rel [of x y]
1.38  next
1.39    fix x :: "'a poly"
1.40    have "pdivmod_rel x 0 0 x"
1.41      by (rule pdivmod_rel_by_0)
1.42 -  thus "x div 0 = 0"
1.43 +  thus "divide x 0 = 0"
1.44      by (rule div_poly_eq)
1.45  next
1.46    fix y :: "'a poly"
1.47    have "pdivmod_rel 0 y 0 0"
1.48      by (rule pdivmod_rel_0)
1.49 -  thus "0 div y = 0"
1.50 +  thus "divide 0 y = 0"
1.51      by (rule div_poly_eq)
1.52  next
1.53    fix x y z :: "'a poly"
1.54    assume "y \<noteq> 0"
1.55 -  hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
1.56 +  hence "pdivmod_rel (x + z * y) y (z + divide x y) (x mod y)"
1.57      using pdivmod_rel [of x y]
1.58      by (simp add: pdivmod_rel_def distrib_right)
1.59 -  thus "(x + z * y) div y = z + x div y"
1.60 +  thus "divide (x + z * y) y = z + divide x y"
1.61      by (rule div_poly_eq)
1.62  next
1.63    fix x y z :: "'a poly"
1.64    assume "x \<noteq> 0"
1.65 -  show "(x * y) div (x * z) = y div z"
1.66 +  show "divide (x * y) (x * z) = divide y z"
1.67    proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
1.68      have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
1.69        by (rule pdivmod_rel_by_0)
1.70 -    then have [simp]: "\<And>x::'a poly. x div 0 = 0"
1.71 +    then have [simp]: "\<And>x::'a poly. divide x 0 = 0"
1.72        by (rule div_poly_eq)
1.73      have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
1.74        by (rule pdivmod_rel_0)
1.75 -    then have [simp]: "\<And>x::'a poly. 0 div x = 0"
1.76 +    then have [simp]: "\<And>x::'a poly. divide 0 x = 0"
1.77        by (rule div_poly_eq)
1.78      case False then show ?thesis by auto
1.79    next
1.80 @@ -1430,8 +1430,8 @@
1.81      have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
1.82        by (auto simp add: pdivmod_rel_def algebra_simps)
1.83          (rule classical, simp add: degree_mult_eq)
1.84 -    moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
1.85 -    ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
1.86 +    moreover from pdivmod_rel have "pdivmod_rel y z (divide y z) (y mod z)" .
1.87 +    ultimately have "pdivmod_rel (x * y) (x * z) (divide y z) (x * (y mod z))" .
1.88      then show ?thesis by (simp add: div_poly_eq)
1.89    qed
1.90  qed
```