985 |
985 |
986 lemma isnpolyh_zero_iff: |
986 lemma isnpolyh_zero_iff: |
987 assumes nq: "isnpolyh p n0" and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{ring_char_0,power,division_by_zero,field})" |
987 assumes nq: "isnpolyh p n0" and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{ring_char_0,power,division_by_zero,field})" |
988 shows "p = 0\<^sub>p" |
988 shows "p = 0\<^sub>p" |
989 using nq eq |
989 using nq eq |
990 proof (induct n\<equiv>"maxindex p" arbitrary: p n0 rule: nat_less_induct) |
990 proof (induct "maxindex p" arbitrary: p n0 rule: less_induct) |
991 fix n p n0 |
991 case less |
992 assume H: "\<forall>m<n. \<forall>p n0. isnpolyh p n0 \<longrightarrow> |
992 note np = `isnpolyh p n0` and zp = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)` |
993 (\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)) \<longrightarrow> m = maxindex p \<longrightarrow> p = 0\<^sub>p" |
993 {assume nz: "maxindex p = 0" |
994 and np: "isnpolyh p n0" and zp: "\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" and n: "n = maxindex p" |
994 then obtain c where "p = C c" using np by (cases p, auto) |
995 {assume nz: "n = 0" |
|
996 then obtain c where "p = C c" using n np by (cases p, auto) |
|
997 with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp} |
995 with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp} |
998 moreover |
996 moreover |
999 {assume nz: "n \<noteq> 0" |
997 {assume nz: "maxindex p \<noteq> 0" |
1000 let ?h = "head p" |
998 let ?h = "head p" |
1001 let ?hd = "decrpoly ?h" |
999 let ?hd = "decrpoly ?h" |
1002 let ?ihd = "maxindex ?hd" |
1000 let ?ihd = "maxindex ?hd" |
1003 from head_isnpolyh[OF np] head_polybound0[OF np] have h:"isnpolyh ?h n0" "polybound0 ?h" |
1001 from head_isnpolyh[OF np] head_polybound0[OF np] have h:"isnpolyh ?h n0" "polybound0 ?h" |
1004 by simp_all |
1002 by simp_all |
1005 hence nhd: "isnpolyh ?hd (n0 - 1)" using decrpoly_normh by blast |
1003 hence nhd: "isnpolyh ?hd (n0 - 1)" using decrpoly_normh by blast |
1006 |
1004 |
1007 from maxindex_coefficients[of p] coefficients_head[of p, symmetric] |
1005 from maxindex_coefficients[of p] coefficients_head[of p, symmetric] |
1008 have mihn: "maxindex ?h \<le> n" unfolding n by auto |
1006 have mihn: "maxindex ?h \<le> maxindex p" by auto |
1009 with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < n" by auto |
1007 with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < maxindex p" by auto |
1010 {fix bs:: "'a list" assume bs: "wf_bs bs ?hd" |
1008 {fix bs:: "'a list" assume bs: "wf_bs bs ?hd" |
1011 let ?ts = "take ?ihd bs" |
1009 let ?ts = "take ?ihd bs" |
1012 let ?rs = "drop ?ihd bs" |
1010 let ?rs = "drop ?ihd bs" |
1013 have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp |
1011 have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp |
1014 have bs_ts_eq: "?ts@ ?rs = bs" by simp |
1012 have bs_ts_eq: "?ts@ ?rs = bs" by simp |
1015 from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x#?ts) ?h" by simp |
1013 from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x#?ts) ?h" by simp |
1016 from ihd_lt_n have "ALL x. length (x#?ts) \<le> n" by simp |
1014 from ihd_lt_n have "ALL x. length (x#?ts) \<le> maxindex p" by simp |
1017 with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = n" by blast |
1015 with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = maxindex p" by blast |
1018 hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" using n unfolding wf_bs_def by simp |
1016 hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" unfolding wf_bs_def by simp |
1019 with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast |
1017 with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast |
1020 hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp |
1018 hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp |
1021 with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a] |
1019 with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a] |
1022 have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x" by simp |
1020 have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x" by simp |
1023 hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) |
1021 hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) |
1024 hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0" |
1022 hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0" |
1025 thm poly_zero |
|
1026 using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff) |
1023 using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff) |
1027 with coefficients_head[of p, symmetric] |
1024 with coefficients_head[of p, symmetric] |
1028 have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp |
1025 have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp |
1029 from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp |
1026 from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp |
1030 with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" by simp |
1027 with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" by simp |
1031 with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp } |
1028 with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp } |
1032 then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast |
1029 then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast |
1033 |
1030 |
1034 from H[rule_format, OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast |
1031 from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast |
1035 hence "?h = 0\<^sub>p" by simp |
1032 hence "?h = 0\<^sub>p" by simp |
1036 with head_nz[OF np] have "p = 0\<^sub>p" by simp} |
1033 with head_nz[OF np] have "p = 0\<^sub>p" by simp} |
1037 ultimately show "p = 0\<^sub>p" by blast |
1034 ultimately show "p = 0\<^sub>p" by blast |
1038 qed |
1035 qed |
1039 |
1036 |
1355 and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p" |
1352 and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p" |
1356 shows "polydivide_aux_dom (a,n,p,k,s) \<and> |
1353 shows "polydivide_aux_dom (a,n,p,k,s) \<and> |
1357 (polydivide_aux (a,n,p,k,s) = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p) |
1354 (polydivide_aux (a,n,p,k,s) = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p) |
1358 \<and> (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))" |
1355 \<and> (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))" |
1359 using ns |
1356 using ns |
1360 proof(induct d\<equiv>"degree s" arbitrary: s k k' r n1 rule: nat_less_induct) |
1357 proof(induct "degree s" arbitrary: s k k' r n1 rule: less_induct) |
1361 fix d s k k' r n1 |
1358 case less |
1362 let ?D = "polydivide_aux_dom" |
1359 let ?D = "polydivide_aux_dom" |
1363 let ?dths = "?D (a, n, p, k, s)" |
1360 let ?dths = "?D (a, n, p, k, s)" |
1364 let ?qths = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" |
1361 let ?qths = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" |
1365 let ?qrths = "polydivide_aux (a, n, p, k, s) = (k', r) \<longrightarrow> k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) |
1362 let ?qrths = "polydivide_aux (a, n, p, k, s) = (k', r) \<longrightarrow> k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) |
1366 \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths" |
1363 \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths" |
1367 let ?ths = "?dths \<and> ?qrths" |
1364 let ?ths = "?dths \<and> ?qrths" |
1368 let ?b = "head s" |
1365 let ?b = "head s" |
1369 let ?p' = "funpow (d - n) shift1 p" |
1366 let ?p' = "funpow (degree s - n) shift1 p" |
1370 let ?xdn = "funpow (d - n) shift1 1\<^sub>p" |
1367 let ?xdn = "funpow (degree s - n) shift1 1\<^sub>p" |
1371 let ?akk' = "a ^\<^sub>p (k' - k)" |
1368 let ?akk' = "a ^\<^sub>p (k' - k)" |
1372 assume H: "\<forall>m<d. \<forall>x xa xb xc xd. |
1369 note ns = `isnpolyh s n1` |
1373 isnpolyh x xd \<longrightarrow> |
|
1374 m = degree x \<longrightarrow> ?D (a, n, p, xa, x) \<and> |
|
1375 (polydivide_aux (a, n, p, xa, x) = (xb, xc) \<longrightarrow> |
|
1376 xa \<le> xb \<and> (degree xc = 0 \<or> degree xc < degree p) \<and> |
|
1377 (\<exists> nr. isnpolyh xc nr) \<and> |
|
1378 (\<exists>q n1. isnpolyh q n1 \<and> a ^\<^sub>p xb - xa *\<^sub>p x = p *\<^sub>p q +\<^sub>p xc))" |
|
1379 and ns: "isnpolyh s n1" and ds: "d = degree s" |
|
1380 from np have np0: "isnpolyh p 0" |
1370 from np have np0: "isnpolyh p 0" |
1381 using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by simp |
1371 using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by simp |
1382 have np': "isnpolyh ?p' 0" using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="d -n"] isnpoly_def by simp |
1372 have np': "isnpolyh ?p' 0" using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="degree s - n"] isnpoly_def by simp |
1383 have headp': "head ?p' = head p" using funpow_shift1_head[OF np pnz] by simp |
1373 have headp': "head ?p' = head p" using funpow_shift1_head[OF np pnz] by simp |
1384 from funpow_shift1_isnpoly[where p="1\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def) |
1374 from funpow_shift1_isnpoly[where p="1\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def) |
1385 from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap |
1375 from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap |
1386 have nakk':"isnpolyh ?akk' 0" by blast |
1376 have nakk':"isnpolyh ?akk' 0" by blast |
1387 {assume sz: "s = 0\<^sub>p" |
1377 {assume sz: "s = 0\<^sub>p" |
1389 from polydivide_aux.psimps[OF dom] sz |
1379 from polydivide_aux.psimps[OF dom] sz |
1390 have ?qrths using np apply clarsimp by (rule exI[where x="0\<^sub>p"], simp) |
1380 have ?qrths using np apply clarsimp by (rule exI[where x="0\<^sub>p"], simp) |
1391 hence ?ths using dom by blast} |
1381 hence ?ths using dom by blast} |
1392 moreover |
1382 moreover |
1393 {assume sz: "s \<noteq> 0\<^sub>p" |
1383 {assume sz: "s \<noteq> 0\<^sub>p" |
1394 {assume dn: "d < n" |
1384 {assume dn: "degree s < n" |
1395 with sz ds have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all) |
1385 with sz have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all) |
1396 from polydivide_aux.psimps[OF dom] sz dn ds |
1386 from polydivide_aux.psimps[OF dom] sz dn |
1397 have "?qrths" using ns ndp np by auto (rule exI[where x="0\<^sub>p"],simp) |
1387 have "?qrths" using ns ndp np by auto (rule exI[where x="0\<^sub>p"],simp) |
1398 with dom have ?ths by blast} |
1388 with dom have ?ths by blast} |
1399 moreover |
1389 moreover |
1400 {assume dn': "\<not> d < n" hence dn: "d \<ge> n" by arith |
1390 {assume dn': "\<not> degree s < n" hence dn: "degree s \<ge> n" by arith |
1401 have degsp': "degree s = degree ?p'" |
1391 have degsp': "degree s = degree ?p'" |
1402 using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp |
1392 using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] by simp |
1403 {assume ba: "?b = a" |
1393 {assume ba: "?b = a" |
1404 hence headsp': "head s = head ?p'" using ap headp' by simp |
1394 hence headsp': "head s = head ?p'" using ap headp' by simp |
1405 have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp |
1395 have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp |
1406 from ds degree_polysub_samehead[OF ns np' headsp' degsp'] |
1396 from degree_polysub_samehead[OF ns np' headsp' degsp'] |
1407 have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp |
1397 have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp |
1408 moreover |
1398 moreover |
1409 {assume deglt:"degree (s -\<^sub>p ?p') < d" |
1399 {assume deglt:"degree (s -\<^sub>p ?p') < degree s" |
1410 from H[rule_format, OF deglt nr,simplified] |
1400 from less(1)[OF deglt nr] |
1411 have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast |
1401 have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast |
1412 have dom: ?dths apply (rule polydivide_aux_real_domintros) |
1402 have dom: ?dths apply (rule polydivide_aux_real_domintros) |
1413 using ba ds dn' domsp by simp_all |
1403 using ba dn' domsp by simp_all |
1414 from polydivide_aux.psimps[OF dom] sz dn' ba ds |
1404 from polydivide_aux.psimps[OF dom] sz dn' ba |
1415 have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')" |
1405 have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')" |
1416 by (simp add: Let_def) |
1406 by (simp add: Let_def) |
1417 {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)" |
1407 {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)" |
1418 from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified] |
1408 from less(1)[OF deglt nr, of k k' r] |
1419 trans[OF eq[symmetric] h1] |
1409 trans[OF eq[symmetric] h1] |
1420 have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p" |
1410 have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p" |
1421 and q1:"\<exists>q nq. isnpolyh q nq \<and> (a ^\<^sub>p k' - k *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r)" by auto |
1411 and q1:"\<exists>q nq. isnpolyh q nq \<and> (a ^\<^sub>p k' - k *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r)" by auto |
1422 from q1 obtain q n1 where nq: "isnpolyh q n1" |
1412 from q1 obtain q n1 where nq: "isnpolyh q n1" |
1423 and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r" by blast |
1413 and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r" by blast |
1432 Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp |
1422 Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp |
1433 hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = |
1423 hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = |
1434 Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" |
1424 Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" |
1435 by (simp add: ring_simps) |
1425 by (simp add: ring_simps) |
1436 hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = |
1426 hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = |
1437 Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p) |
1427 Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p) |
1438 + Ipoly bs p * Ipoly bs q + Ipoly bs r" |
1428 + Ipoly bs p * Ipoly bs q + Ipoly bs r" |
1439 by (auto simp only: funpow_shift1_1) |
1429 by (auto simp only: funpow_shift1_1) |
1440 hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = |
1430 hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = |
1441 Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p) |
1431 Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p) |
1442 + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps) |
1432 + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps) |
1443 hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = |
1433 hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = |
1444 Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp |
1434 Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp |
1445 with isnpolyh_unique[OF nakks' nqr'] |
1435 with isnpolyh_unique[OF nakks' nqr'] |
1446 have "a ^\<^sub>p (k' - k) *\<^sub>p s = |
1436 have "a ^\<^sub>p (k' - k) *\<^sub>p s = |
1447 p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast |
1437 p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast |
1448 hence ?qths using nq' |
1438 hence ?qths using nq' |
1449 apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI) |
1439 apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q" in exI) |
1450 apply (rule_tac x="0" in exI) by simp |
1440 apply (rule_tac x="0" in exI) by simp |
1451 with kk' nr dr have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths" |
1441 with kk' nr dr have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths" |
1452 by blast } hence ?qrths by blast |
1442 by blast } hence ?qrths by blast |
1453 with dom have ?ths by blast} |
1443 with dom have ?ths by blast} |
1454 moreover |
1444 moreover |
1455 {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p" |
1445 {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p" |
1456 hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" |
1446 hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" |
1457 apply (simp) by (rule polydivide_aux_real_domintros, simp_all) |
1447 apply (simp) by (rule polydivide_aux_real_domintros, simp_all) |
1458 have dom: ?dths apply (rule polydivide_aux_real_domintros) |
1448 have dom: ?dths apply (rule polydivide_aux_real_domintros) |
1459 using ba ds dn' domsp by simp_all |
1449 using ba dn' domsp by simp_all |
1460 from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{ring_char_0,division_by_zero,field}"] |
1450 from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{ring_char_0,division_by_zero,field}"] |
1461 have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp |
1451 have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp |
1462 hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp |
1452 hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp |
1463 by (simp only: funpow_shift1_1) simp |
1453 by (simp only: funpow_shift1_1) simp |
1464 hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast |
1454 hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast |
1465 {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)" |
1455 {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)" |
1466 from polydivide_aux.psimps[OF dom] sz dn' ba ds |
1456 from polydivide_aux.psimps[OF dom] sz dn' ba |
1467 have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')" |
1457 have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')" |
1468 by (simp add: Let_def) |
1458 by (simp add: Let_def) |
1469 also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp |
1459 also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp |
1470 finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp |
1460 finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp |
1471 with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]] |
1461 with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]] |
1472 polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths |
1462 polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths |
1473 apply auto |
1463 apply auto |
1474 apply (rule exI[where x="?xdn"]) |
1464 apply (rule exI[where x="?xdn"]) |
1475 apply auto |
1465 apply (auto simp add: polymul_commute[of p]) |
1476 apply (rule polymul_commute) |
|
1477 apply simp_all |
|
1478 done} |
1466 done} |
1479 with dom have ?ths by blast} |
1467 with dom have ?ths by blast} |
1480 ultimately have ?ths by blast } |
1468 ultimately have ?ths by blast } |
1481 moreover |
1469 moreover |
1482 {assume ba: "?b \<noteq> a" |
1470 {assume ba: "?b \<noteq> a" |
1486 have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p" |
1474 have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p" |
1487 using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] |
1475 using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] |
1488 polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns] |
1476 polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns] |
1489 funpow_shift1_nz[OF pnz] by simp_all |
1477 funpow_shift1_nz[OF pnz] by simp_all |
1490 from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz |
1478 from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz |
1491 polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"] |
1479 polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="degree s - n"] |
1492 have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" |
1480 have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" |
1493 using head_head[OF ns] funpow_shift1_head[OF np pnz] |
1481 using head_head[OF ns] funpow_shift1_head[OF np pnz] |
1494 polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]] |
1482 polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]] |
1495 by (simp add: ap) |
1483 by (simp add: ap) |
1496 from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] |
1484 from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] |
1497 head_nz[OF np] pnz sz ap[symmetric] |
1485 head_nz[OF np] pnz sz ap[symmetric] |
1498 funpow_shift1_nz[OF pnz, where n="d - n"] |
1486 funpow_shift1_nz[OF pnz, where n="degree s - n"] |
1499 polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"] head_nz[OF ns] |
1487 polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"] head_nz[OF ns] |
1500 ndp ds[symmetric] dn |
1488 ndp dn |
1501 have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') " |
1489 have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') " |
1502 by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree) |
1490 by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree) |
1503 {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d" |
1491 {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s" |
1504 have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))" |
1492 have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))" |
1505 using H[rule_format, OF dth nth, simplified] by blast |
1493 using less(1)[OF dth nth] by blast |
1506 have dom: ?dths |
1494 have dom: ?dths using ba dn' th |
1507 using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros) |
1495 by - (rule polydivide_aux_real_domintros, simp_all) |
1508 using ba ds dn' by simp_all |
|
1509 from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']] |
1496 from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']] |
1510 ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp |
1497 ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp |
1511 {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)" |
1498 {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)" |
1512 from h1 polydivide_aux.psimps[OF dom] sz dn' ba ds |
1499 from h1 polydivide_aux.psimps[OF dom] sz dn' ba |
1513 have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)" |
1500 have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)" |
1514 by (simp add: Let_def) |
1501 by (simp add: Let_def) |
1515 with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"] |
1502 with less(1)[OF dth nasbp', of "Suc k" k' r] |
1516 obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" |
1503 obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" |
1517 and dr: "degree r = 0 \<or> degree r < degree p" |
1504 and dr: "degree r = 0 \<or> degree r < degree p" |
1518 and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto |
1505 and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto |
1519 from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith |
1506 from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith |
1520 {fix bs:: "'a::{ring_char_0,division_by_zero,field} list" |
1507 {fix bs:: "'a::{ring_char_0,division_by_zero,field} list" |
1522 from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric] |
1509 from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric] |
1523 have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp |
1510 have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp |
1524 hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r" |
1511 hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r" |
1525 by (simp add: ring_simps power_Suc) |
1512 by (simp add: ring_simps power_Suc) |
1526 hence "Ipoly bs a ^ (k' - k) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r" |
1513 hence "Ipoly bs a ^ (k' - k) * Ipoly bs s = Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r" |
1527 by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"]) |
1514 by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"]) |
1528 hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r" |
1515 hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r" |
1529 by (simp add: ring_simps)} |
1516 by (simp add: ring_simps)} |
1530 hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = |
1517 hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = |
1531 Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" by auto |
1518 Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" by auto |
1532 let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)" |
1519 let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)" |
1544 with dom have ?ths by blast} |
1531 with dom have ?ths by blast} |
1545 moreover |
1532 moreover |
1546 {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p" |
1533 {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p" |
1547 hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))" |
1534 hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))" |
1548 apply (simp) by (rule polydivide_aux_real_domintros, simp_all) |
1535 apply (simp) by (rule polydivide_aux_real_domintros, simp_all) |
1549 have dom: ?dths using sz ba dn' ds domsp |
1536 have dom: ?dths using sz ba dn' domsp |
1550 by - (rule polydivide_aux_real_domintros, simp_all) |
1537 by - (rule polydivide_aux_real_domintros, simp_all) |
1551 {fix bs :: "'a::{ring_char_0,division_by_zero,field} list" |
1538 {fix bs :: "'a::{ring_char_0,division_by_zero,field} list" |
1552 from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz |
1539 from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz |
1553 have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp |
1540 have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp |
1554 hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" |
1541 hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" |
1555 by (simp add: funpow_shift1_1[where n="d - n" and p="p"]) |
1542 by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"]) |
1556 hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp |
1543 hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp |
1557 } |
1544 } |
1558 hence hth: "\<forall> (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" .. |
1545 hence hth: "\<forall> (bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" .. |
1559 from hth |
1546 from hth |
1560 have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" |
1547 have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" |
1561 using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns] |
1548 using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns] |
1562 polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]], |
1549 polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]], |
1563 simplified ap] by simp |
1550 simplified ap] by simp |
1564 {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)" |
1551 {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)" |
1565 from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] |
1552 from h1 sz ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] |
1566 have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def) |
1553 have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def) |
1567 with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn] |
1554 with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn] |
1568 polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq |
1555 polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq |
1569 have ?qrths apply (clarsimp simp add: Let_def) |
1556 have ?qrths apply (clarsimp simp add: Let_def) |
1570 apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp |
1557 apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp |
1571 apply (rule exI[where x="0"], simp) |
1558 apply (rule exI[where x="0"], simp) |
1572 done} |
1559 done} |
1573 hence ?qrths by blast |
1560 hence ?qrths by blast |
1574 with dom have ?ths by blast} |
1561 with dom have ?ths by blast} |
1575 ultimately have ?ths using degree_polysub_samehead[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_normh[OF head_isnpolyh[OF ns] np'] hdth degth] polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] |
1562 ultimately have ?ths using degree_polysub_samehead[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_normh[OF head_isnpolyh[OF ns] np'] hdth degth] polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] |
1576 head_nz[OF np] pnz sz ap[symmetric] ds[symmetric] |
1563 head_nz[OF np] pnz sz ap[symmetric] |
1577 by (simp add: degree_eq_degreen0[symmetric]) blast } |
1564 by (simp add: degree_eq_degreen0[symmetric]) blast } |
1578 ultimately have ?ths by blast |
1565 ultimately have ?ths by blast |
1579 } |
1566 } |
1580 ultimately have ?ths by blast} |
1567 ultimately have ?ths by blast} |
1581 ultimately show ?ths by blast |
1568 ultimately show ?ths by blast |