1207 del: mult_pCons_left) |
1207 del: mult_pCons_left) |
1208 qed |
1208 qed |
1209 qed |
1209 qed |
1210 |
1210 |
1211 |
1211 |
|
1212 subsection {* Order of polynomial roots *} |
|
1213 |
|
1214 definition |
|
1215 order :: "'a::{idom,recpower} \<Rightarrow> 'a poly \<Rightarrow> nat" |
|
1216 where |
|
1217 [code del]: |
|
1218 "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)" |
|
1219 |
|
1220 lemma degree_power_le: "degree (p ^ n) \<le> degree p * n" |
|
1221 by (induct n, simp, auto intro: order_trans degree_mult_le) |
|
1222 |
|
1223 lemma coeff_linear_power: |
|
1224 fixes a :: "'a::{comm_semiring_1,recpower}" |
|
1225 shows "coeff ([:a, 1:] ^ n) n = 1" |
|
1226 apply (induct n, simp_all) |
|
1227 apply (subst coeff_eq_0) |
|
1228 apply (auto intro: le_less_trans degree_power_le) |
|
1229 done |
|
1230 |
|
1231 lemma degree_linear_power: |
|
1232 fixes a :: "'a::{comm_semiring_1,recpower}" |
|
1233 shows "degree ([:a, 1:] ^ n) = n" |
|
1234 apply (rule order_antisym) |
|
1235 apply (rule ord_le_eq_trans [OF degree_power_le], simp) |
|
1236 apply (rule le_degree, simp add: coeff_linear_power) |
|
1237 done |
|
1238 |
|
1239 lemma order_1: "[:-a, 1:] ^ order a p dvd p" |
|
1240 apply (cases "p = 0", simp) |
|
1241 apply (cases "order a p", simp) |
|
1242 apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)") |
|
1243 apply (drule not_less_Least, simp) |
|
1244 apply (fold order_def, simp) |
|
1245 done |
|
1246 |
|
1247 lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p" |
|
1248 unfolding order_def |
|
1249 apply (rule LeastI_ex) |
|
1250 apply (rule_tac x="degree p" in exI) |
|
1251 apply (rule notI) |
|
1252 apply (drule (1) dvd_imp_degree_le) |
|
1253 apply (simp only: degree_linear_power) |
|
1254 done |
|
1255 |
|
1256 lemma order: |
|
1257 "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p" |
|
1258 by (rule conjI [OF order_1 order_2]) |
|
1259 |
|
1260 lemma order_degree: |
|
1261 assumes p: "p \<noteq> 0" |
|
1262 shows "order a p \<le> degree p" |
|
1263 proof - |
|
1264 have "order a p = degree ([:-a, 1:] ^ order a p)" |
|
1265 by (simp only: degree_linear_power) |
|
1266 also have "\<dots> \<le> degree p" |
|
1267 using order_1 p by (rule dvd_imp_degree_le) |
|
1268 finally show ?thesis . |
|
1269 qed |
|
1270 |
|
1271 lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0" |
|
1272 apply (cases "p = 0", simp_all) |
|
1273 apply (rule iffI) |
|
1274 apply (rule ccontr, simp) |
|
1275 apply (frule order_2 [where a=a], simp) |
|
1276 apply (simp add: poly_eq_0_iff_dvd) |
|
1277 apply (simp add: poly_eq_0_iff_dvd) |
|
1278 apply (simp only: order_def) |
|
1279 apply (drule not_less_Least, simp) |
|
1280 done |
|
1281 |
|
1282 lemma poly_zero: |
|
1283 fixes p :: "'a::{idom,ring_char_0} poly" |
|
1284 shows "poly p = poly 0 \<longleftrightarrow> p = 0" |
|
1285 apply (cases "p = 0", simp_all) |
|
1286 apply (drule poly_roots_finite) |
|
1287 apply (auto simp add: infinite_UNIV_char_0) |
|
1288 done |
|
1289 |
|
1290 lemma poly_eq_iff: |
|
1291 fixes p q :: "'a::{idom,ring_char_0} poly" |
|
1292 shows "poly p = poly q \<longleftrightarrow> p = q" |
|
1293 using poly_zero [of "p - q"] |
|
1294 by (simp add: expand_fun_eq) |
|
1295 |
|
1296 |
1212 subsection {* Configuration of the code generator *} |
1297 subsection {* Configuration of the code generator *} |
1213 |
1298 |
1214 code_datatype "0::'a::zero poly" pCons |
1299 code_datatype "0::'a::zero poly" pCons |
1215 |
1300 |
1216 declare pCons_0_0 [code post] |
1301 declare pCons_0_0 [code post] |