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