# 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 \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
+  pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
 where
   [code del]:
-  "divmod_poly_rel x y q r \<longleftrightarrow>
+  "pdivmod_rel x y q r \<longleftrightarrow>
     x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> 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 \<le> 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 \<noteq> 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 \<or> 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 \<noteq> 0` by simp
 qed
 
-lemma divmod_poly_rel_exists: "\<exists>q r. divmod_poly_rel x y q r"
+lemma pdivmod_rel_exists: "\<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 \<and> 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 \<noteq> 0"
   from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> 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 \<or> 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 \<or> 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. \<exists>r. divmod_poly_rel x y q r)"
+  [code del]: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
 
 definition mod_poly where
-  [code del]: "x mod y = (THE r. \<exists>q. divmod_poly_rel x y q r)"
+  [code del]: "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
 
 lemma div_poly_eq:
-  "divmod_poly_rel x y q r \<Longrightarrow> x div y = q"
+  "pdivmod_rel x y q r \<Longrightarrow> 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 \<Longrightarrow> x mod y = r"
+  "pdivmod_rel x y q r \<Longrightarrow> 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 \<noteq> 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 \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
+  pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> '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