author krauss Sat Dec 25 22:18:55 2010 +0100 (2010-12-25) changeset 41403 7eba049f7310 parent 41402 b647212cee03 child 41404 aae9f912cca8
partial_function (tailrec) replaces function (tailrec);
dropped unnecessary domain reasoning;
curried polydivide_aux
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Dec 24 14:26:10 2010 -0800
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Dec 25 22:18:55 2010 +0100
1.3 @@ -196,19 +196,18 @@
1.4  abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" where
1.5    "funpow \<equiv> compow"
1.6
1.7 -function (tailrec) polydivide_aux :: "(poly \<times> nat \<times> poly \<times> nat \<times> poly) \<Rightarrow> (nat \<times> poly)"
1.8 +partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<times> poly"
1.9    where
1.10 -  "polydivide_aux (a,n,p,k,s) =
1.11 +  "polydivide_aux a n p k s =
1.12    (if s = 0\<^sub>p then (k,s)
1.13    else (let b = head s; m = degree s in
1.14    (if m < n then (k,s) else
1.15    (let p'= funpow (m - n) shift1 p in
1.16 -  (if a = b then polydivide_aux (a,n,p,k,s -\<^sub>p p')
1.17 -  else polydivide_aux (a,n,p,Suc k, (a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
1.18 -  by pat_completeness auto
1.19 +  (if a = b then polydivide_aux a n p k (s -\<^sub>p p')
1.20 +  else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
1.21
1.22  definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where
1.23 -  "polydivide s p \<equiv> polydivide_aux (head p,degree p,p,0, s)"
1.24 +  "polydivide s p \<equiv> polydivide_aux (head p) (degree p) p 0 s"
1.25
1.26  fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" where
1.27    "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)"
1.28 @@ -1308,52 +1307,18 @@
1.29
1.30  subsection {* Correctness of polynomial pseudo division *}
1.31
1.32 -lemma polydivide_aux_real_domintros:
1.33 -  assumes call1: "\<lbrakk>s \<noteq> 0\<^sub>p; \<not> degree s < n; a = head s\<rbrakk>
1.34 -  \<Longrightarrow> polydivide_aux_dom (a, n, p, k, s -\<^sub>p funpow (degree s - n) shift1 p)"
1.35 -  and call2 : "\<lbrakk>s \<noteq> 0\<^sub>p; \<not> degree s < n; a \<noteq> head s\<rbrakk>
1.36 -  \<Longrightarrow> polydivide_aux_dom(a, n, p,Suc k, a *\<^sub>p s -\<^sub>p (head s *\<^sub>p funpow (degree s - n) shift1 p))"
1.37 -  shows "polydivide_aux_dom (a, n, p, k, s)"
1.38 -proof (rule accpI, erule polydivide_aux_rel.cases)
1.39 -  fix y aa ka na pa sa x xa xb
1.40 -  assume eqs: "y = (aa, na, pa, ka, sa -\<^sub>p xb)" "(a, n, p, k, s) = (aa, na, pa, ka, sa)"
1.41 -     and \<Gamma>1': "sa \<noteq> 0\<^sub>p" "x = head sa" "xa = degree sa" "\<not> xa < na"
1.42 -    "xb = funpow (xa - na) shift1 pa" "aa = x"
1.43 -
1.44 -  hence \<Gamma>1: "s \<noteq> 0\<^sub>p" "a = head s" "xa = degree s" "\<not> degree s < n" "\<not> xa < na"
1.45 -    "xb = funpow (xa - na) shift1 pa" "aa = x" by auto
1.46 -
1.47 -  with call1 have "polydivide_aux_dom (a, n, p, k, s -\<^sub>p funpow (degree s - n) shift1 p)"
1.48 -    by auto
1.49 -  with eqs \<Gamma>1 show "polydivide_aux_dom y" by auto
1.50 -next
1.51 -  fix y aa ka na pa sa x xa xb
1.52 -  assume eqs: "y = (aa, na, pa, Suc ka, aa *\<^sub>p sa -\<^sub>p (x *\<^sub>p xb))"
1.53 -    "(a, n, p, k, s) =(aa, na, pa, ka, sa)"
1.54 -    and \<Gamma>2': "sa \<noteq> 0\<^sub>p" "x = head sa" "xa = degree sa" "\<not> xa < na"
1.55 -    "xb = funpow (xa - na) shift1 pa" "aa \<noteq> x"
1.56 -  hence \<Gamma>2: "s \<noteq> 0\<^sub>p" "a \<noteq> head s" "xa = degree s" "\<not> degree s < n"
1.57 -    "xb = funpow (xa - na) shift1 pa" "aa \<noteq> x" by auto
1.58 -  with call2 have "polydivide_aux_dom (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (head s *\<^sub>p funpow (degree s - n) shift1 p))" by auto
1.59 -  with eqs \<Gamma>2'  show "polydivide_aux_dom y" by auto
1.60 -qed
1.61 -
1.62  lemma polydivide_aux_properties:
1.63    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.64    and np: "isnpolyh p n0" and ns: "isnpolyh s n1"
1.65    and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
1.66 -  shows "polydivide_aux_dom (a,n,p,k,s) \<and>
1.67 -  (polydivide_aux (a,n,p,k,s) = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p)
1.68 +  shows "(polydivide_aux a n p k s = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p)
1.69            \<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)))"
1.70    using ns
1.71  proof(induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
1.72    case less
1.73 -  let ?D = "polydivide_aux_dom"
1.74 -  let ?dths = "?D (a, n, p, k, s)"
1.75    let ?qths = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
1.76 -  let ?qrths = "polydivide_aux (a, n, p, k, s) = (k', r) \<longrightarrow>  k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p)
1.77 +  let ?ths = "polydivide_aux a n p k s = (k', r) \<longrightarrow>  k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p)
1.78      \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
1.79 -  let ?ths = "?dths \<and> ?qrths"
1.80    let ?b = "head s"
1.81    let ?p' = "funpow (degree s - n) shift1 p"
1.82    let ?xdn = "funpow (degree s - n) shift1 1\<^sub>p"
1.83 @@ -1367,17 +1332,11 @@
1.84    from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap
1.85    have nakk':"isnpolyh ?akk' 0" by blast
1.86    {assume sz: "s = 0\<^sub>p"
1.87 -    hence dom: ?dths apply - apply (rule polydivide_aux_real_domintros) apply simp_all done
1.88 -    from polydivide_aux.psimps[OF dom] sz
1.89 -    have ?qrths using np apply clarsimp by (rule exI[where x="0\<^sub>p"], simp)
1.90 -    hence ?ths using dom by blast}
1.91 +   hence ?ths using np polydivide_aux.simps apply clarsimp by (rule exI[where x="0\<^sub>p"], simp) }
1.92    moreover
1.93    {assume sz: "s \<noteq> 0\<^sub>p"
1.94      {assume dn: "degree s < n"
1.95 -      with sz have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all)
1.96 -      from polydivide_aux.psimps[OF dom] sz dn
1.97 -      have "?qrths" using ns ndp np by auto (rule exI[where x="0\<^sub>p"],simp)
1.98 -      with dom have ?ths by blast}
1.99 +      hence "?ths" using ns ndp np polydivide_aux.simps by auto (rule exI[where x="0\<^sub>p"],simp) }
1.100      moreover
1.101      {assume dn': "\<not> degree s < n" hence dn: "degree s \<ge> n" by arith
1.102        have degsp': "degree s = degree ?p'"
1.103 @@ -1389,14 +1348,10 @@
1.104          have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
1.105          moreover
1.106          {assume deglt:"degree (s -\<^sub>p ?p') < degree s"
1.107 -          from  less(1)[OF deglt nr]
1.108 -          have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast
1.109 -          have dom: ?dths apply (rule polydivide_aux_real_domintros)
1.110 -            using ba dn' domsp by simp_all
1.111 -          from polydivide_aux.psimps[OF dom] sz dn' ba
1.112 -          have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
1.113 +          from polydivide_aux.simps sz dn' ba
1.114 +          have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
1.116 -          {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
1.117 +          {assume h1: "polydivide_aux a n p k s = (k', r)"
1.118              from less(1)[OF deglt nr, of k k' r]
1.119                trans[OF eq[symmetric] h1]
1.120              have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
1.121 @@ -1431,32 +1386,26 @@
1.122                apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
1.123                apply (rule_tac x="0" in exI) by simp
1.124              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"
1.125 -              by blast } hence ?qrths by blast
1.126 -          with dom have ?ths by blast}
1.127 +              by blast } hence ?ths by blast }
1.128          moreover
1.129          {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
1.130 -          hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')"
1.131 -            apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
1.132 -          have dom: ?dths apply (rule polydivide_aux_real_domintros)
1.133 -            using ba dn' domsp by simp_all
1.134            from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0, field_inverse_zero}"]
1.135            have " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" by simp
1.136            hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp
1.137              by (simp only: funpow_shift1_1) simp
1.138            hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
1.139 -          {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
1.140 -            from polydivide_aux.psimps[OF dom] sz dn' ba
1.141 -            have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
1.142 +          {assume h1: "polydivide_aux a n p k s = (k',r)"
1.143 +            from polydivide_aux.simps sz dn' ba
1.144 +            have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
1.146 -            also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
1.147 +            also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.simps spz by simp
1.148              finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
1.149              with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
1.150 -              polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
1.151 +              polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?ths
1.152                apply auto
1.153                apply (rule exI[where x="?xdn"])
1.154                apply (auto simp add: polymul_commute[of p])
1.155 -              done}
1.156 -          with dom have ?ths by blast}
1.157 +              done} }
1.158          ultimately have ?ths by blast }
1.159        moreover
1.160        {assume ba: "?b \<noteq> a"
1.161 @@ -1481,15 +1430,11 @@
1.162          have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
1.163            by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
1.164          {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s"
1.165 -          have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
1.166 -            using less(1)[OF dth nth] by blast
1.167 -          have dom: ?dths using ba dn' th
1.168 -            by - (rule polydivide_aux_real_domintros, simp_all)
1.170            ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
1.171 -          {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
1.172 -            from h1  polydivide_aux.psimps[OF dom] sz dn' ba
1.173 -            have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
1.174 +          {assume h1:"polydivide_aux a n p k s = (k', r)"
1.175 +            from h1 polydivide_aux.simps sz dn' ba
1.176 +            have eq:"polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
1.178              with less(1)[OF dth nasbp', of "Suc k" k' r]
1.179              obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq"
1.180 @@ -1513,20 +1458,15 @@
1.181              have nqw: "isnpolyh ?q 0" by simp
1.182              from ieq isnpolyh_unique[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - k"] ns, simplified ap] polyadd_normh[OF polymul_normh[OF np nqw] nr]]
1.183              have asth: "(a ^\<^sub>p (k' - k) *\<^sub>p s) = p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r" by blast
1.184 -            from dr kk' nr h1 asth nqw have ?qrths apply simp
1.185 +            from dr kk' nr h1 asth nqw have ?ths apply simp
1.186                apply (rule conjI)
1.187                apply (rule exI[where x="nr"], simp)
1.188                apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
1.189                apply (rule exI[where x="0"], simp)
1.190                done}
1.191 -          hence ?qrths by blast
1.192 -          with dom have ?ths by blast}
1.193 +          hence ?ths by blast }
1.194          moreover
1.195          {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
1.196 -          hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))"
1.197 -            apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
1.198 -          have dom: ?dths using sz ba dn' domsp
1.199 -            by - (rule polydivide_aux_real_domintros, simp_all)
1.200            {fix bs :: "'a::{field_char_0, field_inverse_zero} list"
1.201              from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
1.202            have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
1.203 @@ -1540,17 +1480,16 @@
1.204              using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns]
1.205                      polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
1.206                simplified ap] by simp
1.207 -          {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
1.208 -          from h1 sz ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp]
1.209 +          {assume h1: "polydivide_aux a n p k s = (k', r)"
1.210 +          from h1 sz ba dn' spz polydivide_aux.simps polydivide_aux.simps
1.211            have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
1.212            with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
1.213              polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
1.214 -          have ?qrths apply (clarsimp simp add: Let_def)
1.215 +          have ?ths apply (clarsimp simp add: Let_def)
1.216              apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
1.217              apply (rule exI[where x="0"], simp)
1.218              done}
1.219 -        hence ?qrths by blast
1.220 -        with dom have ?ths by blast}
1.221 +        hence ?ths by blast}
1.222          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"]
1.223            head_nz[OF np] pnz sz ap[symmetric]
1.224            by (simp add: degree_eq_degreen0[symmetric]) blast }
1.225 @@ -1567,12 +1506,10 @@
1.226    \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
1.227  proof-
1.228    have trv: "head p = head p" "degree p = degree p" by simp_all
1.229 -  from polydivide_aux_properties[OF np ns trv pnz, where k="0"]
1.230 -  have d: "polydivide_aux_dom (head p, degree p, p, 0, s)" by blast
1.231 -  from polydivide_def[where s="s" and p="p"] polydivide_aux.psimps[OF d]
1.232 +  from polydivide_def[where s="s" and p="p"]
1.233    have ex: "\<exists> k r. polydivide s p = (k,r)" by auto
1.234    then obtain k r where kr: "polydivide s p = (k,r)" by blast
1.235 -  from trans[OF meta_eq_to_obj_eq[OF polydivide_def[where s="s" and p="p"], symmetric] kr]
1.236 +  from trans[OF meta_eq_to_obj_eq[OF polydivide_def[where s="s"and p="p"], symmetric] kr]
1.237      polydivide_aux_properties[OF np ns trv pnz, where k="0" and k'="k" and r="r"]
1.238    have "(degree r = 0 \<or> degree r < degree p) \<and>
1.239     (\<exists>nr. isnpolyh r nr) \<and> (\<exists>q n1. isnpolyh q n1 \<and> head p ^\<^sub>p k - 0 *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" by blast
```