author huffman Thu Jan 15 09:17:15 2009 -0800 (2009-01-15) changeset 29537 50345a0f9df8 parent 29536 2de73447d47c child 29538 5cc98af1398d
rename divmod_poly to pdivmod
 src/HOL/Polynomial.thy file | annotate | diff | revisions
```     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.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
```