summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 09 Mar 2014 18:43:38 +0100 | |

changeset 56009 | dda076a32aea |

parent 56008 | 2897b2a4f7fd |

child 56010 | abf4879d39f1 |

tuned proofs;

src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sun Mar 09 17:43:40 2014 +0100 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sun Mar 09 18:43:38 2014 +0100 @@ -188,7 +188,7 @@ | "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)" | "poly_cmul y p = C y *\<^sub>p p" -definition monic :: "poly \<Rightarrow> (poly \<times> bool)" +definition monic :: "poly \<Rightarrow> poly \<times> bool" where "monic p = (let h = headconst p @@ -200,7 +200,7 @@ definition shift1 :: "poly \<Rightarrow> poly" where "shift1 p = CN 0\<^sub>p 0 p" -abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" +abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where "funpow \<equiv> compow" partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<times> poly" @@ -250,7 +250,7 @@ ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>") where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p" -lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" +lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i" by (simp add: INum_def) lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j" @@ -278,56 +278,98 @@ lemma polyadd_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)" proof (induct p q arbitrary: n0 n1 rule: polyadd.induct) case (2 ab c' n' p' n0 n1) - from 2 have th1: "isnpolyh (C ab) (Suc n')" by simp - from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all - with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp - with 2(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^sub>p c') (Suc n')" by simp - from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp - thus ?case using 2 th3 by simp + from 2 have th1: "isnpolyh (C ab) (Suc n')" + by simp + from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" + by simp_all + with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" + by simp + with 2(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^sub>p c') (Suc n')" + by simp + from nplen1 have n01len1: "min n0 n1 \<le> n'" + by simp + then show ?case using 2 th3 + by simp next case (3 c' n' p' ab n1 n0) - from 3 have th1: "isnpolyh (C ab) (Suc n')" by simp - from 3(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all - with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp - with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (Suc n')" by simp - from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp - thus ?case using 3 th3 by simp + from 3 have th1: "isnpolyh (C ab) (Suc n')" + by simp + from 3(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" + by simp_all + with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" + by simp + with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (Suc n')" + by simp + from nplen1 have n01len1: "min n0 n1 \<le> n'" + by simp + then show ?case using 3 th3 + by simp next case (4 c n p c' n' p' n0 n1) - hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all - from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all - from 4 have ngen0: "n \<ge> n0" by simp - from 4 have n'gen1: "n' \<ge> n1" by simp - have "n < n' \<or> n' < n \<or> n = n'" by auto - moreover { + then have nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" + by simp_all + from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" + by simp_all + from 4 have ngen0: "n \<ge> n0" + by simp + from 4 have n'gen1: "n' \<ge> n1" + by simp + have "n < n' \<or> n' < n \<or> n = n'" + by auto + moreover + { assume eq: "n = n'" with "4.hyps"(3)[OF nc nc'] - have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto - hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)" - using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto - from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp - have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp - from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' have ?case by (simp add: Let_def) } - moreover { + have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" + by auto + then have ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)" + using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 + by auto + from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" + by simp + have minle: "min n0 n1 \<le> n'" + using ngen0 n'gen1 eq by simp + from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' have ?case + by (simp add: Let_def) + } + moreover + { assume lt: "n < n'" - have "min n0 n1 \<le> n0" by simp - with 4 lt have th1:"min n0 n1 \<le> n" by auto - from 4 have th21: "isnpolyh c (Suc n)" by simp - from 4 have th22: "isnpolyh (CN c' n' p') n'" by simp - from lt have th23: "min (Suc n) n' = Suc n" by arith - from "4.hyps"(1)[OF th21 th22] - have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)" using th23 by simp - with 4 lt th1 have ?case by simp } - moreover { - assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp - have "min n0 n1 \<le> n1" by simp - with 4 gt have th1:"min n0 n1 \<le> n'" by auto - from 4 have th21: "isnpolyh c' (Suc n')" by simp_all - from 4 have th22: "isnpolyh (CN c n p) n" by simp - from gt have th23: "min n (Suc n') = Suc n'" by arith - from "4.hyps"(2)[OF th22 th21] - have "isnpolyh (polyadd (CN c n p) c') (Suc n')" using th23 by simp - with 4 gt th1 have ?case by simp } + have "min n0 n1 \<le> n0" + by simp + with 4 lt have th1:"min n0 n1 \<le> n" + by auto + from 4 have th21: "isnpolyh c (Suc n)" + by simp + from 4 have th22: "isnpolyh (CN c' n' p') n'" + by simp + from lt have th23: "min (Suc n) n' = Suc n" + by arith + from "4.hyps"(1)[OF th21 th22] have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)" + using th23 by simp + with 4 lt th1 have ?case + by simp + } + moreover + { + assume gt: "n' < n" + then have gt': "n' < n \<and> \<not> n < n'" + by simp + have "min n0 n1 \<le> n1" + by simp + with 4 gt have th1: "min n0 n1 \<le> n'" + by auto + from 4 have th21: "isnpolyh c' (Suc n')" + by simp_all + from 4 have th22: "isnpolyh (CN c n p) n" + by simp + from gt have th23: "min n (Suc n') = Suc n'" + by arith + from "4.hyps"(2)[OF th22 th21] have "isnpolyh (polyadd (CN c n p) c') (Suc n')" + using th23 by simp + with 4 gt th1 have ?case + by simp + } ultimately show ?case by blast qed auto @@ -335,18 +377,22 @@ by (induct p q rule: polyadd.induct) (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left) -lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd p q)" +lemma polyadd_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polyadd p q)" using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp text{* The degree of addition and other general lemmas needed for the normal form of polymul *} lemma polyadd_different_degreen: - "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> - degreen (polyadd p q) m = max (degreen p m) (degreen q m)" + assumes "isnpolyh p n0" + and "isnpolyh q n1" + and "degreen p m \<noteq> degreen q m" + and "m \<le> min n0 n1" + shows "degreen (polyadd p q) m = max (degreen p m) (degreen q m)" + using assms proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct) case (4 c n p c' n' p' m n0 n1) have "n' = n \<or> n < n' \<or> n' < n" by arith - thus ?case + then show ?case proof (elim disjE) assume [simp]: "n' = n" from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7) @@ -360,10 +406,12 @@ qed qed auto -lemma headnz[simp]: "\<lbrakk>isnpolyh p n ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> headn p m \<noteq> 0\<^sub>p" +lemma headnz[simp]: "isnpolyh p n \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> headn p m \<noteq> 0\<^sub>p" by (induct p arbitrary: n rule: headn.induct) auto + lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> degree p = 0" by (induct p arbitrary: n rule: degree.induct) auto + lemma degreen_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> degreen p m = 0" by (induct p arbitrary: n rule: degreen.induct) auto @@ -372,24 +420,29 @@ lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degree c = 0" using degree_isnpolyh_Suc by auto + lemma degreen_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degreen c n = 0" using degreen_0 by auto lemma degreen_polyadd: - assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> max n0 n1" + assumes np: "isnpolyh p n0" + and nq: "isnpolyh q n1" + and m: "m \<le> max n0 n1" shows "degreen (p +\<^sub>p q) m \<le> max (degreen p m) (degreen q m)" using np nq m proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct) case (2 c c' n' p' n0 n1) - thus ?case by (cases n') simp_all + then show ?case + by (cases n') simp_all next case (3 c n p c' n0 n1) - thus ?case by (cases n) auto + then show ?case + by (cases n) auto next case (4 c n p c' n' p' n0 n1 m) have "n' = n \<or> n < n' \<or> n' < n" by arith - thus ?case + then show ?case proof (elim disjE) assume [simp]: "n' = n" from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7) @@ -397,21 +450,34 @@ qed simp_all qed auto -lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\<rbrakk> - \<Longrightarrow> degreen p m = degreen q m" +lemma polyadd_eq_const_degreen: + assumes "isnpolyh p n0" + and "isnpolyh q n1" + and "polyadd p q = C c" + shows "degreen p m = degreen q m" + using assms proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct) case (4 c n p c' n' p' m n0 n1 x) - { assume nn': "n' < n" hence ?case using 4 by simp } + { + assume nn': "n' < n" + then have ?case using 4 by simp + } moreover - { assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith + { + assume nn': "\<not> n' < n" + then have "n < n' \<or> n = n'" by arith moreover { assume "n < n'" with 4 have ?case by simp } - moreover { assume eq: "n = n'" hence ?case using 4 + moreover + { + assume eq: "n = n'" + then have ?case using 4 apply (cases "p +\<^sub>p p' = 0\<^sub>p") apply (auto simp add: Let_def) apply blast done } - ultimately have ?case by blast } + ultimately have ?case by blast + } ultimately show ?case by blast qed simp_all @@ -421,165 +487,201 @@ and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1" shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" - and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)" - and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0 else degreen p m + degreen q m)" + and "p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> q = 0\<^sub>p" + and "degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \<or> q = 0\<^sub>p then 0 else degreen p m + degreen q m)" using np nq m proof (induct p q arbitrary: n0 n1 m rule: polymul.induct) case (2 c c' n' p') - { case (1 n0 n1) - with "2.hyps"(4-6)[of n' n' n'] - and "2.hyps"(1-3)[of "Suc n'" "Suc n'" n'] + { + case (1 n0 n1) + with "2.hyps"(4-6)[of n' n' n'] and "2.hyps"(1-3)[of "Suc n'" "Suc n'" n'] show ?case by (auto simp add: min_def) next - case (2 n0 n1) thus ?case by auto + case (2 n0 n1) + then show ?case by auto next - case (3 n0 n1) thus ?case using "2.hyps" by auto } + case (3 n0 n1) + then show ?case using "2.hyps" by auto + } next case (3 c n p c') - { case (1 n0 n1) - with "3.hyps"(4-6)[of n n n] - "3.hyps"(1-3)[of "Suc n" "Suc n" n] + { + case (1 n0 n1) + with "3.hyps"(4-6)[of n n n] and "3.hyps"(1-3)[of "Suc n" "Suc n" n] show ?case by (auto simp add: min_def) next - case (2 n0 n1) thus ?case by auto + case (2 n0 n1) + then show ?case by auto next - case (3 n0 n1) thus ?case using "3.hyps" by auto } + case (3 n0 n1) + then show ?case using "3.hyps" by auto + } next case (4 c n p c' n' p') let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'" + { + case (1 n0 n1) + then have cnp: "isnpolyh ?cnp n" + and cnp': "isnpolyh ?cnp' n'" + and np: "isnpolyh p n" + and nc: "isnpolyh c (Suc n)" + and np': "isnpolyh p' n'" + and nc': "isnpolyh c' (Suc n')" + and nn0: "n \<ge> n0" + and nn1: "n' \<ge> n1" + by simp_all { - case (1 n0 n1) - hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'" - and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)" - and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')" - and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1" - by simp_all - { assume "n < n'" - with "4.hyps"(4-5)[OF np cnp', of n] - "4.hyps"(1)[OF nc cnp', of n] nn0 cnp - have ?case by (simp add: min_def) - } moreover { - assume "n' < n" - with "4.hyps"(16-17)[OF cnp np', of "n'"] - "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp' - have ?case - by (cases "Suc n' = n") (simp_all add: min_def) - } moreover { - assume "n' = n" - with "4.hyps"(16-17)[OF cnp np', of n] - "4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0 - have ?case - apply (auto intro!: polyadd_normh) - apply (simp_all add: min_def isnpolyh_mono[OF nn0]) - done + assume "n < n'" + with "4.hyps"(4-5)[OF np cnp', of n] and "4.hyps"(1)[OF nc cnp', of n] nn0 cnp + have ?case by (simp add: min_def) + } moreover { + assume "n' < n" + with "4.hyps"(16-17)[OF cnp np', of "n'"] and "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp' + have ?case by (cases "Suc n' = n") (simp_all add: min_def) + } moreover { + assume "n' = n" + with "4.hyps"(16-17)[OF cnp np', of n] and "4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0 + have ?case + apply (auto intro!: polyadd_normh) + apply (simp_all add: min_def isnpolyh_mono[OF nn0]) + done + } + ultimately show ?case by arith + next + fix n0 n1 m + assume np: "isnpolyh ?cnp n0" + assume np':"isnpolyh ?cnp' n1" + assume m: "m \<le> min n0 n1" + let ?d = "degreen (?cnp *\<^sub>p ?cnp') m" + let ?d1 = "degreen ?cnp m" + let ?d2 = "degreen ?cnp' m" + let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)" + have "n'<n \<or> n < n' \<or> n' = n" by auto + moreover + { + assume "n' < n \<or> n < n'" + with "4.hyps"(3,6,18) np np' m have ?eq + by auto + } + moreover + { + assume nn': "n' = n" + then have nn: "\<not> n' < n \<and> \<not> n < n'" by arith + from "4.hyps"(16,18)[of n n' n] + "4.hyps"(13,14)[of n "Suc n'" n] + np np' nn' + have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n" + "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" + "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" + "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def) + { + assume mn: "m = n" + from "4.hyps"(17,18)[OF norm(1,4), of n] + "4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn + have degs: + "degreen (?cnp *\<^sub>p c') n = (if c' = 0\<^sub>p then 0 else ?d1 + degreen c' n)" + "degreen (?cnp *\<^sub>p p') n = ?d1 + degreen p' n" + by (simp_all add: min_def) + from degs norm have th1: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" + by simp + then have neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" + by simp + have nmin: "n \<le> min n n" + by (simp add: min_def) + from polyadd_different_degreen[OF norm(3,6) neq nmin] th1 + have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n = + degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" + by simp + from "4.hyps"(16-18)[OF norm(1,4), of n] + "4.hyps"(13-15)[OF norm(1,2), of n] + mn norm m nn' deg + have ?eq by simp } - ultimately show ?case by arith - next - fix n0 n1 m - assume np: "isnpolyh ?cnp n0" and np':"isnpolyh ?cnp' n1" - and m: "m \<le> min n0 n1" - let ?d = "degreen (?cnp *\<^sub>p ?cnp') m" - let ?d1 = "degreen ?cnp m" - let ?d2 = "degreen ?cnp' m" - let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)" - have "n'<n \<or> n < n' \<or> n' = n" by auto - moreover - {assume "n' < n \<or> n < n'" - with "4.hyps"(3,6,18) np np' m - have ?eq by auto } moreover - { assume nn': "n' = n" - hence nn: "\<not> n' < n \<and> \<not> n < n'" by arith - from "4.hyps"(16,18)[of n n' n] - "4.hyps"(13,14)[of n "Suc n'" n] - np np' nn' - have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n" - "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" - "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" - "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def) - { assume mn: "m = n" - from "4.hyps"(17,18)[OF norm(1,4), of n] - "4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn - have degs: "degreen (?cnp *\<^sub>p c') n = - (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)" - "degreen (?cnp *\<^sub>p p') n = ?d1 + degreen p' n" by (simp_all add: min_def) - from degs norm - have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp - hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" - by simp - have nmin: "n \<le> min n n" by (simp add: min_def) - from polyadd_different_degreen[OF norm(3,6) neq nmin] th1 - have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n = degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp - from "4.hyps"(16-18)[OF norm(1,4), of n] - "4.hyps"(13-15)[OF norm(1,2), of n] - mn norm m nn' deg - have ?eq by simp } - moreover - { assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto - from nn' m np have max1: "m \<le> max n n" by simp - hence min1: "m \<le> min n n" by simp - hence min2: "m \<le> min n (Suc n)" by simp - from "4.hyps"(16-18)[OF norm(1,4) min1] - "4.hyps"(13-15)[OF norm(1,2) min2] - degreen_polyadd[OF norm(3,6) max1] - - have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m - \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)" - using mn nn' np np' by simp - with "4.hyps"(16-18)[OF norm(1,4) min1] - "4.hyps"(13-15)[OF norm(1,2) min2] - degreen_0[OF norm(3) mn'] - have ?eq using nn' mn np np' by clarsimp } - ultimately have ?eq by blast } - ultimately show ?eq by blast } - { case (2 n0 n1) - hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1" - and m: "m \<le> min n0 n1" by simp_all - hence mn: "m \<le> n" by simp - let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')" - {assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n" - hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp - from "4.hyps"(16-18) [of n n n] - "4.hyps"(13-15)[of n "Suc n" n] - np np' C(2) mn - have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n" - "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" - "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" - "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" - "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)" - "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n" - by (simp_all add: min_def) - - from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp - have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" - using norm by simp - from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq - have "False" by simp } - thus ?case using "4.hyps" by clarsimp } + { + assume mn: "m \<noteq> n" + then have mn': "m < n" + using m np by auto + from nn' m np have max1: "m \<le> max n n" + by simp + then have min1: "m \<le> min n n" + by simp + then have min2: "m \<le> min n (Suc n)" + by simp + from "4.hyps"(16-18)[OF norm(1,4) min1] + "4.hyps"(13-15)[OF norm(1,2) min2] + degreen_polyadd[OF norm(3,6) max1] + have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m \<le> + max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)" + using mn nn' np np' by simp + with "4.hyps"(16-18)[OF norm(1,4) min1] + "4.hyps"(13-15)[OF norm(1,2) min2] + degreen_0[OF norm(3) mn'] + have ?eq using nn' mn np np' by clarsimp + } + ultimately have ?eq by blast + } + ultimately show ?eq by blast + } + { + case (2 n0 n1) + then have np: "isnpolyh ?cnp n0" + and np': "isnpolyh ?cnp' n1" + and m: "m \<le> min n0 n1" by simp_all + then have mn: "m \<le> n" by simp + let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')" + { + assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n" + then have nn: "\<not> n' < n \<and> \<not> n < n'" + by simp + from "4.hyps"(16-18) [of n n n] + "4.hyps"(13-15)[of n "Suc n" n] + np np' C(2) mn + have norm: + "isnpolyh ?cnp n" + "isnpolyh c' (Suc n)" + "isnpolyh (?cnp *\<^sub>p c') n" + "isnpolyh p' n" + "isnpolyh (?cnp *\<^sub>p p') n" + "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" + "?cnp *\<^sub>p c' = 0\<^sub>p \<longleftrightarrow> c' = 0\<^sub>p" + "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" + "degreen (?cnp *\<^sub>p c') n = (if c' = 0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)" + "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n" + by (simp_all add: min_def) + from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" + by simp + have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" + using norm by simp + from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq + have False by simp + } + then show ?case using "4.hyps" by clarsimp + } qed auto -lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)" +lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = Ipoly bs p * Ipoly bs q" by (induct p q rule: polymul.induct) (auto simp add: field_simps) lemma polymul_normh: assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" - shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)" + shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)" using polymul_properties(1) by blast lemma polymul_eq0_iff: assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" - shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p) " + shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> q = 0\<^sub>p" using polymul_properties(2) by blast lemma polymul_degreen: (* FIXME duplicate? *) assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" - shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> - degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0 else degreen p m + degreen q m)" + shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<Longrightarrow> + degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \<or> q = 0\<^sub>p then 0 else degreen p m + degreen q m)" using polymul_properties(3) by blast lemma polymul_norm: assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" - shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul p q)" + shows "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polymul p q)" using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp lemma headconst_zero: "isnpolyh p n0 \<Longrightarrow> headconst p = 0\<^sub>N \<longleftrightarrow> p = 0\<^sub>p" @@ -601,7 +703,7 @@ from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" by simp_all from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" by simp with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast} - thus "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast + then show "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast qed @@ -610,12 +712,14 @@ lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p" by (induct p rule: polyneg.induct) auto -lemma polyneg0: "isnpolyh p n \<Longrightarrow> ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)" +lemma polyneg0: "isnpolyh p n \<Longrightarrow> (~\<^sub>p p) = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p" by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: Nneg_def) + lemma polyneg_polyneg: "isnpolyh p n0 \<Longrightarrow> ~\<^sub>p (~\<^sub>p p) = p" by (induct p arbitrary: n0 rule: polyneg.induct) auto -lemma polyneg_normh: "\<And>n. isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n " - by (induct p rule: polyneg.induct) (auto simp add: polyneg0) + +lemma polyneg_normh: "isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n" + by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: polyneg0) lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)" using isnpoly_def polyneg_normh by simp @@ -623,14 +727,15 @@ text{* polysub is a substraction and preserves normal forms *} -lemma polysub[simp]: "Ipoly bs (polysub p q) = (Ipoly bs p) - (Ipoly bs q)" +lemma polysub[simp]: "Ipoly bs (polysub p q) = Ipoly bs p - Ipoly bs q" by (simp add: polysub_def) -lemma polysub_normh: - "\<And>n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub p q) (min n0 n1)" + +lemma polysub_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polysub p q) (min n0 n1)" by (simp add: polysub_def polyneg_normh polyadd_normh) -lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub p q)" +lemma polysub_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polysub p q)" using polyadd_norm polyneg_norm by (simp add: polysub_def) + lemma polysub_same_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" shows "isnpolyh p n0 \<Longrightarrow> polysub p p = 0\<^sub>p" @@ -639,17 +744,18 @@ lemma polysub_0: assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" - shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)" + shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p -\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = q" unfolding polysub_def split_def fst_conv snd_conv by (induct p q arbitrary: n0 n1 rule:polyadd.induct) (auto simp: Nsub0[simplified Nsub_def] Let_def) text{* polypow is a power function and preserves normal forms *} -lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0,field_inverse_zero})) ^ n" +lemma polypow[simp]: + "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field_inverse_zero}) ^ n" proof (induct n rule: polypow.induct) case 1 - thus ?case by simp + then show ?case by simp next case (2 n) let ?q = "polypow ((Suc n) div 2) p" @@ -756,7 +862,8 @@ (Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})" using np proof (induct p arbitrary: n rule: behead.induct) - case (1 c p n) hence pn: "isnpolyh p n" by simp + case (1 c p n) + then have pn: "isnpolyh p n" by simp from 1(1)[OF pn] have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . then show ?case using "1.hyps" @@ -776,9 +883,12 @@ lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p" proof (induct p arbitrary: n rule: poly.induct, auto) case (goal1 c n p n') - hence "n = Suc (n - 1)" by simp - hence "isnpolyh p (Suc (n - 1))" using `isnpolyh p n` by simp - with goal1(2) show ?case by simp + then have "n = Suc (n - 1)" + by simp + then have "isnpolyh p (Suc (n - 1))" + using `isnpolyh p n` by simp + with goal1(2) show ?case + by simp qed lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p" @@ -800,16 +910,16 @@ lemma polybound0_I: assumes nb: "polybound0 a" - shows "Ipoly (b#bs) a = Ipoly (b'#bs) a" + shows "Ipoly (b # bs) a = Ipoly (b' # bs) a" using nb by (induct a rule: poly.induct) auto -lemma polysubst0_I: "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t" +lemma polysubst0_I: "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b # bs) a) # bs) t" by (induct t) simp_all lemma polysubst0_I': assumes nb: "polybound0 a" - shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b'#bs) a)#bs) t" + shows "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b' # bs) a) # bs) t" by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"]) lemma decrpoly: @@ -843,19 +953,30 @@ case (1 c p) show ?case proof - fix x assume xc: "x \<in> set (coefficients (CN c 0 p))" - hence "x = c \<or> x \<in> set (coefficients p)" by simp - moreover - {assume "x = c" hence "wf_bs bs x" using "1.prems" unfolding wf_bs_def by simp} + fix x + assume xc: "x \<in> set (coefficients (CN c 0 p))" + then have "x = c \<or> x \<in> set (coefficients p)" + by simp moreover - {assume H: "x \<in> set (coefficients p)" - from "1.prems" have "wf_bs bs p" unfolding wf_bs_def by simp - with "1.hyps" H have "wf_bs bs x" by blast } - ultimately show "wf_bs bs x" by blast + { + assume "x = c" + then have "wf_bs bs x" + using "1.prems" unfolding wf_bs_def by simp + } + moreover + { + assume H: "x \<in> set (coefficients p)" + from "1.prems" have "wf_bs bs p" + unfolding wf_bs_def by simp + with "1.hyps" H have "wf_bs bs x" + by blast + } + ultimately show "wf_bs bs x" + by blast qed qed simp_all -lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p" +lemma maxindex_coefficients: "\<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p" by (induct p rule: coefficients.induct) auto lemma wf_bs_I: "wf_bs bs p \<Longrightarrow> Ipoly (bs @ bs') p = Ipoly bs p" @@ -864,13 +985,17 @@ lemma take_maxindex_wf: assumes wf: "wf_bs bs p" shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p" -proof- +proof - let ?ip = "maxindex p" let ?tbs = "take ?ip bs" - from wf have "length ?tbs = ?ip" unfolding wf_bs_def by simp - hence wf': "wf_bs ?tbs p" unfolding wf_bs_def by simp - have eq: "bs = ?tbs @ (drop ?ip bs)" by simp - from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis using eq by simp + from wf have "length ?tbs = ?ip" + unfolding wf_bs_def by simp + then have wf': "wf_bs ?tbs p" + unfolding wf_bs_def by simp + have eq: "bs = ?tbs @ (drop ?ip bs)" + by simp + from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis + using eq by simp qed lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1" @@ -939,10 +1064,12 @@ lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall> q \<in> set (coefficients p). isnpolyh q n0" proof (induct p arbitrary: n0 rule: coefficients.induct) case (1 c p n0) - have cp: "isnpolyh (CN c 0 p) n0" by fact - hence norm: "isnpolyh c 0" "isnpolyh p 0" "p \<noteq> 0\<^sub>p" "n0 = 0" + have cp: "isnpolyh (CN c 0 p) n0" + by fact + then have norm: "isnpolyh c 0" "isnpolyh p 0" "p \<noteq> 0\<^sub>p" "n0 = 0" by (auto simp add: isnpolyh_mono[where n'=0]) - from "1.hyps"[OF norm(2)] norm(1) norm(4) show ?case by simp + from "1.hyps"[OF norm(2)] norm(1) norm(4) show ?case + by simp qed auto lemma coefficients_isconst: @@ -960,12 +1087,11 @@ from q cn_norm have th: "isnpolyh q n0" by blast from coefficients_isconst[OF np] q have "isconstant q" by blast with isconstant_polybound0[OF th] have "polybound0 q" by blast} - hence "\<forall>q \<in> ?cf. polybound0 q" .. - hence "\<forall>q \<in> ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)" + then have "\<forall>q \<in> ?cf. polybound0 q" .. + then have "\<forall>q \<in> ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)" using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs] by auto - - thus ?thesis unfolding polypoly_def polypoly'_def by simp + then show ?thesis unfolding polypoly_def polypoly'_def by simp qed lemma polypoly_poly: @@ -1207,57 +1333,102 @@ using np nq h d proof (induct p q rule: polyadd.induct) case (1 c c') - thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) + then show ?case + by (simp add: Nsub_def Nsub0[simplified Nsub_def]) next case (2 c c' n' p') - from 2 have "degree (C c) = degree (CN c' n' p')" by simp - hence nz:"n' > 0" by (cases n') auto - hence "head (CN c' n' p') = CN c' n' p'" by (cases n') auto - with 2 show ?case by simp + from 2 have "degree (C c) = degree (CN c' n' p')" + by simp + then have nz: "n' > 0" + by (cases n') auto + then have "head (CN c' n' p') = CN c' n' p'" + by (cases n') auto + with 2 show ?case + by simp next case (3 c n p c') - hence "degree (C c') = degree (CN c n p)" by simp - hence nz:"n > 0" by (cases n) auto - hence "head (CN c n p) = CN c n p" by (cases n) auto + then have "degree (C c') = degree (CN c n p)" + by simp + then have nz: "n > 0" + by (cases n) auto + then have "head (CN c n p) = CN c n p" + by (cases n) auto with 3 show ?case by simp next case (4 c n p c' n' p') - hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1" - "head (CN c n p) = head (CN c' n' p')" "degree (CN c n p) = degree (CN c' n' p')" by simp+ - hence degc: "degree c = 0" and degc': "degree c' = 0" by simp_all - hence degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0" + then have H: + "isnpolyh (CN c n p) n0" + "isnpolyh (CN c' n' p') n1" + "head (CN c n p) = head (CN c' n' p')" + "degree (CN c n p) = degree (CN c' n' p')" + by simp_all + then have degc: "degree c = 0" and degc': "degree c' = 0" + by simp_all + then have degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0" using H(1-2) degree_polyneg by auto - from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')" by simp+ - from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' have degcmc': "degree (c +\<^sub>p ~\<^sub>pc') = 0" by simp - from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" by auto - have "n = n' \<or> n < n' \<or> n > n'" by arith + from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')" + by simp_all + from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' + have degcmc': "degree (c +\<^sub>p ~\<^sub>pc') = 0" + by simp + from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" + by auto + have "n = n' \<or> n < n' \<or> n > n'" + by arith moreover - {assume nn': "n = n'" - have "n = 0 \<or> n >0" by arith - moreover {assume nz: "n = 0" hence ?case using 4 nn' by (auto simp add: Let_def degcmc')} - moreover {assume nz: "n > 0" - with nn' H(3) have cc':"c = c'" and pp': "p = p'" by (cases n, auto)+ - hence ?case - using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] polysub_same_0[OF c'nh, simplified polysub_def] - using nn' 4 by (simp add: Let_def) } - ultimately have ?case by blast} + { + assume nn': "n = n'" + have "n = 0 \<or> n > 0" by arith + moreover { + assume nz: "n = 0" + then have ?case using 4 nn' + by (auto simp add: Let_def degcmc') + } + moreover { + assume nz: "n > 0" + with nn' H(3) have cc': "c = c'" and pp': "p = p'" + by (cases n, auto)+ + then have ?case + using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] + using polysub_same_0[OF c'nh, simplified polysub_def] + using nn' 4 by (simp add: Let_def) + } + ultimately have ?case by blast + } moreover - {assume nn': "n < n'" hence n'p: "n' > 0" by simp - hence headcnp':"head (CN c' n' p') = CN c' n' p'" by (cases n') simp_all - have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" + { + assume nn': "n < n'" + then have n'p: "n' > 0" + by simp + then have headcnp':"head (CN c' n' p') = CN c' n' p'" + by (cases n') simp_all + have degcnp': "degree (CN c' n' p') = 0" + and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" using 4 nn' by (cases n', simp_all) - hence "n > 0" by (cases n) simp_all - hence headcnp: "head (CN c n p) = CN c n p" by (cases n) auto - from H(3) headcnp headcnp' nn' have ?case by auto} + then have "n > 0" + by (cases n) simp_all + then have headcnp: "head (CN c n p) = CN c n p" + by (cases n) auto + from H(3) headcnp headcnp' nn' have ?case + by auto + } moreover - {assume nn': "n > n'" hence np: "n > 0" by simp - hence headcnp:"head (CN c n p) = CN c n p" by (cases n) simp_all - from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp - from np have degcnp: "degree (CN c n p) = 0" by (cases n) simp_all - with degcnpeq have "n' > 0" by (cases n') simp_all - hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n') auto - from H(3) headcnp headcnp' nn' have ?case by auto} - ultimately show ?case by blast + { + assume nn': "n > n'" + then have np: "n > 0" by simp + then have headcnp:"head (CN c n p) = CN c n p" + by (cases n) simp_all + from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" + by simp + from np have degcnp: "degree (CN c n p) = 0" + by (cases n) simp_all + with degcnpeq have "n' > 0" + by (cases n') simp_all + then have headcnp': "head (CN c' n' p') = CN c' n' p'" + by (cases n') auto + from H(3) headcnp headcnp' nn' have ?case by auto + } + ultimately show ?case by blast qed auto lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p" @@ -1266,17 +1437,18 @@ lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p" proof (induct k arbitrary: n0 p) case 0 - thus ?case by auto + then show ?case by auto next case (Suc k n0 p) - hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh) + then have "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh) with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)" and "head (shift1 p) = head p" by (simp_all add: shift1_head) - thus ?case by (simp add: funpow_swap1) + then show ?case by (simp add: funpow_swap1) qed lemma shift1_degree: "degree (shift1 p) = 1 + degree p" by (simp add: shift1_def) + lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p " by (induct k arbitrary: p) (auto simp add: shift1_degree) @@ -1319,12 +1491,16 @@ shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q" proof (induct p q arbitrary: n0 n1 rule: polymul.induct) case (2 c c' n' p' n0 n1) - hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum c" by (simp_all add: head_isnpolyh) - thus ?case using 2 by (cases n') auto + then have "isnpolyh (head (CN c' n' p')) n1" "isnormNum c" + by (simp_all add: head_isnpolyh) + then show ?case + using 2 by (cases n') auto next case (3 c n p c' n0 n1) - hence "isnpolyh (head (CN c n p)) n0" "isnormNum c'" by (simp_all add: head_isnpolyh) - thus ?case using 3 by (cases n) auto + then have "isnpolyh (head (CN c n p)) n0" "isnormNum c'" + by (simp_all add: head_isnpolyh) + then show ?case using 3 + by (cases n) auto next case (4 c n p c' n' p' n0 n1) hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')" @@ -1332,24 +1508,30 @@ by simp_all have "n < n' \<or> n' < n \<or> n = n'" by arith moreover - {assume nn': "n < n'" hence ?case + { + assume nn': "n < n'" + then have ?case using norm "4.hyps"(2)[OF norm(1,6)] "4.hyps"(1)[OF norm(2,6)] apply simp apply (cases n) apply simp apply (cases n') apply simp_all - done } - moreover {assume nn': "n'< n" - hence ?case + done + } + moreover { + assume nn': "n'< n" + then have ?case using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] apply simp apply (cases n') apply simp apply (cases n) apply auto - done } - moreover {assume nn': "n' = n" + done + } + moreover { + assume nn': "n' = n" from nn' polymul_normh[OF norm(5,4)] have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def) from nn' polymul_normh[OF norm(5,3)] norm @@ -1359,12 +1541,15 @@ from polyadd_normh[OF ncnpc' ncnpp0'] have nth: "isnpolyh ((CN c n p *\<^sub>p c') +\<^sub>p (CN 0\<^sub>p n (CN c n p *\<^sub>p p'))) n" by (simp add: min_def) - {assume np: "n > 0" + { + assume np: "n > 0" with nn' head_isnpolyh_Suc'[OF np nth] head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']] - have ?case by simp} + have ?case by simp + } moreover - { assume nz: "n = 0" + { + assume nz: "n = 0" from polymul_degreen[OF norm(5,4), where m="0"] polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0 norm(5,6) degree_npolyhCN[OF norm(6)] @@ -1372,8 +1557,10 @@ hence dth':"degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth have ?case using norm "4.hyps"(6)[OF norm(5,3)] - "4.hyps"(5)[OF norm(5,4)] nn' nz by simp } - ultimately have ?case by (cases n) auto} + "4.hyps"(5)[OF norm(5,4)] nn' nz by simp + } + ultimately have ?case by (cases n) auto + } ultimately show ?case by blast qed simp_all @@ -1744,10 +1931,16 @@ assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" from isnonconstant_pnormal_iff[OF inc, of bs] h have pn: "pnormal ?p" by blast - { fix x assume H: "?p = [x]" - from H have "length (coefficients p) = 1" unfolding polypoly_def by auto - with isnonconstant_coefficients_length[OF inc] have False by arith } - thus "nonconstant ?p" using pn unfolding nonconstant_def by blast + { + fix x + assume H: "?p = [x]" + from H have "length (coefficients p) = 1" + unfolding polypoly_def by auto + with isnonconstant_coefficients_length[OF inc] + have False by arith + } + then show "nonconstant ?p" + using pn unfolding nonconstant_def by blast qed lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p" @@ -1800,10 +1993,10 @@ shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" proof (induct t) case (Bound k) - thus ?case using nbs mbs by simp + then show ?case using nbs mbs by simp next case (CN c k p) - thus ?case using nbs mbs by simp + then show ?case using nbs mbs by simp qed simp_all lemma swap_swap_id [simp]: "swap n m (swap m n t) = t"