# HG changeset patch # User huffman # Date 1232039835 28800 # Node ID 50345a0f9df8d7266c715323e7bb54f0ebe5767c # Parent 2de73447d47ca05a80747b9370f223777bf856cf rename divmod_poly to pdivmod diff -r 2de73447d47c -r 50345a0f9df8 src/HOL/Polynomial.thy --- a/src/HOL/Polynomial.thy Thu Jan 15 09:10:42 2009 -0800 +++ b/src/HOL/Polynomial.thy Thu Jan 15 09:17:15 2009 -0800 @@ -647,19 +647,19 @@ subsection {* Long division of polynomials *} definition - divmod_poly_rel :: "'a::field poly \ 'a poly \ 'a poly \ 'a poly \ bool" + pdivmod_rel :: "'a::field poly \ 'a poly \ 'a poly \ 'a poly \ bool" where [code del]: - "divmod_poly_rel x y q r \ + "pdivmod_rel x y q r \ x = q * y + r \ (if y = 0 then q = 0 else r = 0 \ degree r < degree y)" -lemma divmod_poly_rel_0: - "divmod_poly_rel 0 y 0 0" - unfolding divmod_poly_rel_def by simp +lemma pdivmod_rel_0: + "pdivmod_rel 0 y 0 0" + unfolding pdivmod_rel_def by simp -lemma divmod_poly_rel_by_0: - "divmod_poly_rel x 0 0 x" - unfolding divmod_poly_rel_def by simp +lemma pdivmod_rel_by_0: + "pdivmod_rel x 0 0 x" + unfolding pdivmod_rel_def by simp lemma eq_zero_or_degree_less: assumes "degree p \ n" and "coeff p n = 0" @@ -685,15 +685,15 @@ then show ?thesis .. qed -lemma divmod_poly_rel_pCons: - assumes rel: "divmod_poly_rel x y q r" +lemma pdivmod_rel_pCons: + assumes rel: "pdivmod_rel x y q r" assumes y: "y \ 0" assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)" - shows "divmod_poly_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)" - (is "divmod_poly_rel ?x y ?q ?r") + shows "pdivmod_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)" + (is "pdivmod_rel ?x y ?q ?r") proof - have x: "x = q * y + r" and r: "r = 0 \ degree r < degree y" - using assms unfolding divmod_poly_rel_def by simp_all + using assms unfolding pdivmod_rel_def by simp_all have 1: "?x = ?q * y + ?r" using b x by simp @@ -716,31 +716,31 @@ qed from 1 2 show ?thesis - unfolding divmod_poly_rel_def + unfolding pdivmod_rel_def using `y \ 0` by simp qed -lemma divmod_poly_rel_exists: "\q r. divmod_poly_rel x y q r" +lemma pdivmod_rel_exists: "\q r. pdivmod_rel x y q r" apply (cases "y = 0") -apply (fast intro!: divmod_poly_rel_by_0) +apply (fast intro!: pdivmod_rel_by_0) apply (induct x) -apply (fast intro!: divmod_poly_rel_0) -apply (fast intro!: divmod_poly_rel_pCons) +apply (fast intro!: pdivmod_rel_0) +apply (fast intro!: pdivmod_rel_pCons) done -lemma divmod_poly_rel_unique: - assumes 1: "divmod_poly_rel x y q1 r1" - assumes 2: "divmod_poly_rel x y q2 r2" +lemma pdivmod_rel_unique: + assumes 1: "pdivmod_rel x y q1 r1" + assumes 2: "pdivmod_rel x y q2 r2" shows "q1 = q2 \ r1 = r2" proof (cases "y = 0") assume "y = 0" with assms show ?thesis - by (simp add: divmod_poly_rel_def) + by (simp add: pdivmod_rel_def) next assume [simp]: "y \ 0" from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \ degree r1 < degree y" - unfolding divmod_poly_rel_def by simp_all + unfolding pdivmod_rel_def by simp_all from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \ degree r2 < degree y" - unfolding divmod_poly_rel_def by simp_all + unfolding pdivmod_rel_def by simp_all from q1 q2 have q3: "(q1 - q2) * y = r2 - r1" by (simp add: ring_simps) from r1 r2 have r3: "(r2 - r1) = 0 \ degree (r2 - r1) < degree y" @@ -761,36 +761,36 @@ qed qed -lemmas divmod_poly_rel_unique_div = - divmod_poly_rel_unique [THEN conjunct1, standard] +lemmas pdivmod_rel_unique_div = + pdivmod_rel_unique [THEN conjunct1, standard] -lemmas divmod_poly_rel_unique_mod = - divmod_poly_rel_unique [THEN conjunct2, standard] +lemmas pdivmod_rel_unique_mod = + pdivmod_rel_unique [THEN conjunct2, standard] instantiation poly :: (field) ring_div begin definition div_poly where - [code del]: "x div y = (THE q. \r. divmod_poly_rel x y q r)" + [code del]: "x div y = (THE q. \r. pdivmod_rel x y q r)" definition mod_poly where - [code del]: "x mod y = (THE r. \q. divmod_poly_rel x y q r)" + [code del]: "x mod y = (THE r. \q. pdivmod_rel x y q r)" lemma div_poly_eq: - "divmod_poly_rel x y q r \ x div y = q" + "pdivmod_rel x y q r \ x div y = q" unfolding div_poly_def -by (fast elim: divmod_poly_rel_unique_div) +by (fast elim: pdivmod_rel_unique_div) lemma mod_poly_eq: - "divmod_poly_rel x y q r \ x mod y = r" + "pdivmod_rel x y q r \ x mod y = r" unfolding mod_poly_def -by (fast elim: divmod_poly_rel_unique_mod) +by (fast elim: pdivmod_rel_unique_mod) -lemma divmod_poly_rel: - "divmod_poly_rel x y (x div y) (x mod y)" +lemma pdivmod_rel: + "pdivmod_rel x y (x div y) (x mod y)" proof - - from divmod_poly_rel_exists - obtain q r where "divmod_poly_rel x y q r" by fast + from pdivmod_rel_exists + obtain q r where "pdivmod_rel x y q r" by fast thus ?thesis by (simp add: div_poly_eq mod_poly_eq) qed @@ -798,26 +798,26 @@ instance proof fix x y :: "'a poly" show "x div y * y + x mod y = x" - using divmod_poly_rel [of x y] - by (simp add: divmod_poly_rel_def) + using pdivmod_rel [of x y] + by (simp add: pdivmod_rel_def) next fix x :: "'a poly" - have "divmod_poly_rel x 0 0 x" - by (rule divmod_poly_rel_by_0) + have "pdivmod_rel x 0 0 x" + by (rule pdivmod_rel_by_0) thus "x div 0 = 0" by (rule div_poly_eq) next fix y :: "'a poly" - have "divmod_poly_rel 0 y 0 0" - by (rule divmod_poly_rel_0) + have "pdivmod_rel 0 y 0 0" + by (rule pdivmod_rel_0) thus "0 div y = 0" by (rule div_poly_eq) next fix x y z :: "'a poly" assume "y \ 0" - hence "divmod_poly_rel (x + z * y) y (z + x div y) (x mod y)" - using divmod_poly_rel [of x y] - by (simp add: divmod_poly_rel_def left_distrib) + hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)" + using pdivmod_rel [of x y] + by (simp add: pdivmod_rel_def left_distrib) thus "(x + z * y) div y = z + x div y" by (rule div_poly_eq) qed @@ -826,22 +826,22 @@ lemma degree_mod_less: "y \ 0 \ x mod y = 0 \ degree (x mod y) < degree y" - using divmod_poly_rel [of x y] - unfolding divmod_poly_rel_def by simp + using pdivmod_rel [of x y] + unfolding pdivmod_rel_def by simp lemma div_poly_less: "degree x < degree y \ x div y = 0" proof - assume "degree x < degree y" - hence "divmod_poly_rel x y 0 x" - by (simp add: divmod_poly_rel_def) + hence "pdivmod_rel x y 0 x" + by (simp add: pdivmod_rel_def) thus "x div y = 0" by (rule div_poly_eq) qed lemma mod_poly_less: "degree x < degree y \ x mod y = x" proof - assume "degree x < degree y" - hence "divmod_poly_rel x y 0 x" - by (simp add: divmod_poly_rel_def) + hence "pdivmod_rel x y 0 x" + by (simp add: pdivmod_rel_def) thus "x mod y = x" by (rule mod_poly_eq) qed @@ -852,7 +852,7 @@ shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)" unfolding b apply (rule mod_poly_eq) -apply (rule divmod_poly_rel_pCons [OF divmod_poly_rel y refl]) +apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl]) done @@ -1087,30 +1087,30 @@ text {* code generator setup for div and mod *} definition - divmod_poly :: "'a::field poly \ 'a poly \ 'a poly \ 'a poly" + pdivmod :: "'a::field poly \ 'a poly \ 'a poly \ 'a poly" where - [code del]: "divmod_poly x y = (x div y, x mod y)" + [code del]: "pdivmod x y = (x div y, x mod y)" -lemma div_poly_code [code]: "x div y = fst (divmod_poly x y)" - unfolding divmod_poly_def by simp +lemma div_poly_code [code]: "x div y = fst (pdivmod x y)" + unfolding pdivmod_def by simp -lemma mod_poly_code [code]: "x mod y = snd (divmod_poly x y)" - unfolding divmod_poly_def by simp +lemma mod_poly_code [code]: "x mod y = snd (pdivmod x y)" + unfolding pdivmod_def by simp -lemma divmod_poly_0 [code]: "divmod_poly 0 y = (0, 0)" - unfolding divmod_poly_def by simp +lemma pdivmod_0 [code]: "pdivmod 0 y = (0, 0)" + unfolding pdivmod_def by simp -lemma divmod_poly_pCons [code]: - "divmod_poly (pCons a x) y = +lemma pdivmod_pCons [code]: + "pdivmod (pCons a x) y = (if y = 0 then (0, pCons a x) else - (let (q, r) = divmod_poly x y; + (let (q, r) = pdivmod x y; b = coeff (pCons a r) (degree y) / coeff y (degree y) in (pCons b q, pCons a r - smult b y)))" -apply (simp add: divmod_poly_def Let_def, safe) +apply (simp add: pdivmod_def Let_def, safe) apply (rule div_poly_eq) -apply (erule divmod_poly_rel_pCons [OF divmod_poly_rel _ refl]) +apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl]) apply (rule mod_poly_eq) -apply (erule divmod_poly_rel_pCons [OF divmod_poly_rel _ refl]) +apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl]) done end