partial_function (tailrec) replaces function (tailrec);
authorkrauss
Sat Dec 25 22:18:55 2010 +0100 (2010-12-25)
changeset 414037eba049f7310
parent 41402 b647212cee03
child 41404 aae9f912cca8
partial_function (tailrec) replaces function (tailrec);
dropped unnecessary domain reasoning;
curried polydivide_aux
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
     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.115              by (simp add: Let_def)
   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.145                by (simp add: Let_def)
   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.169            from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
   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.177                by (simp add: Let_def)
   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