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.35      by (simp add: pdivmod_rel_def)
    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