rename divmod_poly to pdivmod
authorhuffman
Thu Jan 15 09:17:15 2009 -0800 (2009-01-15)
changeset 2953750345a0f9df8
parent 29536 2de73447d47c
child 29538 5cc98af1398d
rename divmod_poly to pdivmod
src/HOL/Polynomial.thy
     1.1 --- a/src/HOL/Polynomial.thy	Thu Jan 15 09:10:42 2009 -0800
     1.2 +++ b/src/HOL/Polynomial.thy	Thu Jan 15 09:17:15 2009 -0800
     1.3 @@ -647,19 +647,19 @@
     1.4  subsection {* Long division of polynomials *}
     1.5  
     1.6  definition
     1.7 -  divmod_poly_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
     1.8 +  pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
     1.9  where
    1.10    [code del]:
    1.11 -  "divmod_poly_rel x y q r \<longleftrightarrow>
    1.12 +  "pdivmod_rel x y q r \<longleftrightarrow>
    1.13      x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
    1.14  
    1.15 -lemma divmod_poly_rel_0:
    1.16 -  "divmod_poly_rel 0 y 0 0"
    1.17 -  unfolding divmod_poly_rel_def by simp
    1.18 +lemma pdivmod_rel_0:
    1.19 +  "pdivmod_rel 0 y 0 0"
    1.20 +  unfolding pdivmod_rel_def by simp
    1.21  
    1.22 -lemma divmod_poly_rel_by_0:
    1.23 -  "divmod_poly_rel x 0 0 x"
    1.24 -  unfolding divmod_poly_rel_def by simp
    1.25 +lemma pdivmod_rel_by_0:
    1.26 +  "pdivmod_rel x 0 0 x"
    1.27 +  unfolding pdivmod_rel_def by simp
    1.28  
    1.29  lemma eq_zero_or_degree_less:
    1.30    assumes "degree p \<le> n" and "coeff p n = 0"
    1.31 @@ -685,15 +685,15 @@
    1.32    then show ?thesis ..
    1.33  qed
    1.34  
    1.35 -lemma divmod_poly_rel_pCons:
    1.36 -  assumes rel: "divmod_poly_rel x y q r"
    1.37 +lemma pdivmod_rel_pCons:
    1.38 +  assumes rel: "pdivmod_rel x y q r"
    1.39    assumes y: "y \<noteq> 0"
    1.40    assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
    1.41 -  shows "divmod_poly_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)"
    1.42 -    (is "divmod_poly_rel ?x y ?q ?r")
    1.43 +  shows "pdivmod_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)"
    1.44 +    (is "pdivmod_rel ?x y ?q ?r")
    1.45  proof -
    1.46    have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
    1.47 -    using assms unfolding divmod_poly_rel_def by simp_all
    1.48 +    using assms unfolding pdivmod_rel_def by simp_all
    1.49  
    1.50    have 1: "?x = ?q * y + ?r"
    1.51      using b x by simp
    1.52 @@ -716,31 +716,31 @@
    1.53    qed
    1.54  
    1.55    from 1 2 show ?thesis
    1.56 -    unfolding divmod_poly_rel_def
    1.57 +    unfolding pdivmod_rel_def
    1.58      using `y \<noteq> 0` by simp
    1.59  qed
    1.60  
    1.61 -lemma divmod_poly_rel_exists: "\<exists>q r. divmod_poly_rel x y q r"
    1.62 +lemma pdivmod_rel_exists: "\<exists>q r. pdivmod_rel x y q r"
    1.63  apply (cases "y = 0")
    1.64 -apply (fast intro!: divmod_poly_rel_by_0)
    1.65 +apply (fast intro!: pdivmod_rel_by_0)
    1.66  apply (induct x)
    1.67 -apply (fast intro!: divmod_poly_rel_0)
    1.68 -apply (fast intro!: divmod_poly_rel_pCons)
    1.69 +apply (fast intro!: pdivmod_rel_0)
    1.70 +apply (fast intro!: pdivmod_rel_pCons)
    1.71  done
    1.72  
    1.73 -lemma divmod_poly_rel_unique:
    1.74 -  assumes 1: "divmod_poly_rel x y q1 r1"
    1.75 -  assumes 2: "divmod_poly_rel x y q2 r2"
    1.76 +lemma pdivmod_rel_unique:
    1.77 +  assumes 1: "pdivmod_rel x y q1 r1"
    1.78 +  assumes 2: "pdivmod_rel x y q2 r2"
    1.79    shows "q1 = q2 \<and> r1 = r2"
    1.80  proof (cases "y = 0")
    1.81    assume "y = 0" with assms show ?thesis
    1.82 -    by (simp add: divmod_poly_rel_def)
    1.83 +    by (simp add: pdivmod_rel_def)
    1.84  next
    1.85    assume [simp]: "y \<noteq> 0"
    1.86    from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
    1.87 -    unfolding divmod_poly_rel_def by simp_all
    1.88 +    unfolding pdivmod_rel_def by simp_all
    1.89    from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
    1.90 -    unfolding divmod_poly_rel_def by simp_all
    1.91 +    unfolding pdivmod_rel_def by simp_all
    1.92    from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
    1.93      by (simp add: ring_simps)
    1.94    from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
    1.95 @@ -761,36 +761,36 @@
    1.96    qed
    1.97  qed
    1.98  
    1.99 -lemmas divmod_poly_rel_unique_div =
   1.100 -  divmod_poly_rel_unique [THEN conjunct1, standard]
   1.101 +lemmas pdivmod_rel_unique_div =
   1.102 +  pdivmod_rel_unique [THEN conjunct1, standard]
   1.103  
   1.104 -lemmas divmod_poly_rel_unique_mod =
   1.105 -  divmod_poly_rel_unique [THEN conjunct2, standard]
   1.106 +lemmas pdivmod_rel_unique_mod =
   1.107 +  pdivmod_rel_unique [THEN conjunct2, standard]
   1.108  
   1.109  instantiation poly :: (field) ring_div
   1.110  begin
   1.111  
   1.112  definition div_poly where
   1.113 -  [code del]: "x div y = (THE q. \<exists>r. divmod_poly_rel x y q r)"
   1.114 +  [code del]: "x div y = (THE q. \<exists>r. pdivmod_rel x y q r)"
   1.115  
   1.116  definition mod_poly where
   1.117 -  [code del]: "x mod y = (THE r. \<exists>q. divmod_poly_rel x y q r)"
   1.118 +  [code del]: "x mod y = (THE r. \<exists>q. pdivmod_rel x y q r)"
   1.119  
   1.120  lemma div_poly_eq:
   1.121 -  "divmod_poly_rel x y q r \<Longrightarrow> x div y = q"
   1.122 +  "pdivmod_rel x y q r \<Longrightarrow> x div y = q"
   1.123  unfolding div_poly_def
   1.124 -by (fast elim: divmod_poly_rel_unique_div)
   1.125 +by (fast elim: pdivmod_rel_unique_div)
   1.126  
   1.127  lemma mod_poly_eq:
   1.128 -  "divmod_poly_rel x y q r \<Longrightarrow> x mod y = r"
   1.129 +  "pdivmod_rel x y q r \<Longrightarrow> x mod y = r"
   1.130  unfolding mod_poly_def
   1.131 -by (fast elim: divmod_poly_rel_unique_mod)
   1.132 +by (fast elim: pdivmod_rel_unique_mod)
   1.133  
   1.134 -lemma divmod_poly_rel:
   1.135 -  "divmod_poly_rel x y (x div y) (x mod y)"
   1.136 +lemma pdivmod_rel:
   1.137 +  "pdivmod_rel x y (x div y) (x mod y)"
   1.138  proof -
   1.139 -  from divmod_poly_rel_exists
   1.140 -    obtain q r where "divmod_poly_rel x y q r" by fast
   1.141 +  from pdivmod_rel_exists
   1.142 +    obtain q r where "pdivmod_rel x y q r" by fast
   1.143    thus ?thesis
   1.144      by (simp add: div_poly_eq mod_poly_eq)
   1.145  qed
   1.146 @@ -798,26 +798,26 @@
   1.147  instance proof
   1.148    fix x y :: "'a poly"
   1.149    show "x div y * y + x mod y = x"
   1.150 -    using divmod_poly_rel [of x y]
   1.151 -    by (simp add: divmod_poly_rel_def)
   1.152 +    using pdivmod_rel [of x y]
   1.153 +    by (simp add: pdivmod_rel_def)
   1.154  next
   1.155    fix x :: "'a poly"
   1.156 -  have "divmod_poly_rel x 0 0 x"
   1.157 -    by (rule divmod_poly_rel_by_0)
   1.158 +  have "pdivmod_rel x 0 0 x"
   1.159 +    by (rule pdivmod_rel_by_0)
   1.160    thus "x div 0 = 0"
   1.161      by (rule div_poly_eq)
   1.162  next
   1.163    fix y :: "'a poly"
   1.164 -  have "divmod_poly_rel 0 y 0 0"
   1.165 -    by (rule divmod_poly_rel_0)
   1.166 +  have "pdivmod_rel 0 y 0 0"
   1.167 +    by (rule pdivmod_rel_0)
   1.168    thus "0 div y = 0"
   1.169      by (rule div_poly_eq)
   1.170  next
   1.171    fix x y z :: "'a poly"
   1.172    assume "y \<noteq> 0"
   1.173 -  hence "divmod_poly_rel (x + z * y) y (z + x div y) (x mod y)"
   1.174 -    using divmod_poly_rel [of x y]
   1.175 -    by (simp add: divmod_poly_rel_def left_distrib)
   1.176 +  hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
   1.177 +    using pdivmod_rel [of x y]
   1.178 +    by (simp add: pdivmod_rel_def left_distrib)
   1.179    thus "(x + z * y) div y = z + x div y"
   1.180      by (rule div_poly_eq)
   1.181  qed
   1.182 @@ -826,22 +826,22 @@
   1.183  
   1.184  lemma degree_mod_less:
   1.185    "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
   1.186 -  using divmod_poly_rel [of x y]
   1.187 -  unfolding divmod_poly_rel_def by simp
   1.188 +  using pdivmod_rel [of x y]
   1.189 +  unfolding pdivmod_rel_def by simp
   1.190  
   1.191  lemma div_poly_less: "degree x < degree y \<Longrightarrow> x div y = 0"
   1.192  proof -
   1.193    assume "degree x < degree y"
   1.194 -  hence "divmod_poly_rel x y 0 x"
   1.195 -    by (simp add: divmod_poly_rel_def)
   1.196 +  hence "pdivmod_rel x y 0 x"
   1.197 +    by (simp add: pdivmod_rel_def)
   1.198    thus "x div y = 0" by (rule div_poly_eq)
   1.199  qed
   1.200  
   1.201  lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
   1.202  proof -
   1.203    assume "degree x < degree y"
   1.204 -  hence "divmod_poly_rel x y 0 x"
   1.205 -    by (simp add: divmod_poly_rel_def)
   1.206 +  hence "pdivmod_rel x y 0 x"
   1.207 +    by (simp add: pdivmod_rel_def)
   1.208    thus "x mod y = x" by (rule mod_poly_eq)
   1.209  qed
   1.210  
   1.211 @@ -852,7 +852,7 @@
   1.212    shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
   1.213  unfolding b
   1.214  apply (rule mod_poly_eq)
   1.215 -apply (rule divmod_poly_rel_pCons [OF divmod_poly_rel y refl])
   1.216 +apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl])
   1.217  done
   1.218  
   1.219  
   1.220 @@ -1087,30 +1087,30 @@
   1.221  text {* code generator setup for div and mod *}
   1.222  
   1.223  definition
   1.224 -  divmod_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
   1.225 +  pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
   1.226  where
   1.227 -  [code del]: "divmod_poly x y = (x div y, x mod y)"
   1.228 +  [code del]: "pdivmod x y = (x div y, x mod y)"
   1.229  
   1.230 -lemma div_poly_code [code]: "x div y = fst (divmod_poly x y)"
   1.231 -  unfolding divmod_poly_def by simp
   1.232 +lemma div_poly_code [code]: "x div y = fst (pdivmod x y)"
   1.233 +  unfolding pdivmod_def by simp
   1.234  
   1.235 -lemma mod_poly_code [code]: "x mod y = snd (divmod_poly x y)"
   1.236 -  unfolding divmod_poly_def by simp
   1.237 +lemma mod_poly_code [code]: "x mod y = snd (pdivmod x y)"
   1.238 +  unfolding pdivmod_def by simp
   1.239  
   1.240 -lemma divmod_poly_0 [code]: "divmod_poly 0 y = (0, 0)"
   1.241 -  unfolding divmod_poly_def by simp
   1.242 +lemma pdivmod_0 [code]: "pdivmod 0 y = (0, 0)"
   1.243 +  unfolding pdivmod_def by simp
   1.244  
   1.245 -lemma divmod_poly_pCons [code]:
   1.246 -  "divmod_poly (pCons a x) y =
   1.247 +lemma pdivmod_pCons [code]:
   1.248 +  "pdivmod (pCons a x) y =
   1.249      (if y = 0 then (0, pCons a x) else
   1.250 -      (let (q, r) = divmod_poly x y;
   1.251 +      (let (q, r) = pdivmod x y;
   1.252             b = coeff (pCons a r) (degree y) / coeff y (degree y)
   1.253          in (pCons b q, pCons a r - smult b y)))"
   1.254 -apply (simp add: divmod_poly_def Let_def, safe)
   1.255 +apply (simp add: pdivmod_def Let_def, safe)
   1.256  apply (rule div_poly_eq)
   1.257 -apply (erule divmod_poly_rel_pCons [OF divmod_poly_rel _ refl])
   1.258 +apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
   1.259  apply (rule mod_poly_eq)
   1.260 -apply (erule divmod_poly_rel_pCons [OF divmod_poly_rel _ refl])
   1.261 +apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
   1.262  done
   1.263  
   1.264  end