# HG changeset patch
# User krauss
# Date 1293311935 -3600
# Node ID 7eba049f7310b148ec1da3584c85406dbd3f25ec
# Parent  b647212cee032ec0fda8c7d605ad71bd320f08f7
partial_function (tailrec) replaces function (tailrec);
dropped unnecessary domain reasoning;
curried polydivide_aux

diff -r b647212cee03 -r 7eba049f7310 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Dec 24 14:26:10 2010 -0800
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Dec 25 22:18:55 2010 +0100
@@ -196,19 +196,18 @@
 abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" where
   "funpow \<equiv> compow"
 
-function (tailrec) polydivide_aux :: "(poly \<times> nat \<times> poly \<times> nat \<times> poly) \<Rightarrow> (nat \<times> poly)"
+partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<times> poly"
   where
-  "polydivide_aux (a,n,p,k,s) = 
+  "polydivide_aux a n p k s = 
   (if s = 0\<^sub>p then (k,s)
   else (let b = head s; m = degree s in
   (if m < n then (k,s) else 
   (let p'= funpow (m - n) shift1 p in 
-  (if a = b then polydivide_aux (a,n,p,k,s -\<^sub>p p') 
-  else polydivide_aux (a,n,p,Suc k, (a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
-  by pat_completeness auto
+  (if a = b then polydivide_aux a n p k (s -\<^sub>p p') 
+  else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
 
 definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where
-  "polydivide s p \<equiv> polydivide_aux (head p,degree p,p,0, s)"
+  "polydivide s p \<equiv> polydivide_aux (head p) (degree p) p 0 s"
 
 fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" where
   "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)"
@@ -1308,52 +1307,18 @@
 
 subsection {* Correctness of polynomial pseudo division *}
 
-lemma polydivide_aux_real_domintros:
-  assumes call1: "\<lbrakk>s \<noteq> 0\<^sub>p; \<not> degree s < n; a = head s\<rbrakk> 
-  \<Longrightarrow> polydivide_aux_dom (a, n, p, k, s -\<^sub>p funpow (degree s - n) shift1 p)"
-  and call2 : "\<lbrakk>s \<noteq> 0\<^sub>p; \<not> degree s < n; a \<noteq> head s\<rbrakk> 
-  \<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))"
-  shows "polydivide_aux_dom (a, n, p, k, s)"
-proof (rule accpI, erule polydivide_aux_rel.cases)
-  fix y aa ka na pa sa x xa xb
-  assume eqs: "y = (aa, na, pa, ka, sa -\<^sub>p xb)" "(a, n, p, k, s) = (aa, na, pa, ka, sa)"
-     and \<Gamma>1': "sa \<noteq> 0\<^sub>p" "x = head sa" "xa = degree sa" "\<not> xa < na" 
-    "xb = funpow (xa - na) shift1 pa" "aa = x"
-
-  hence \<Gamma>1: "s \<noteq> 0\<^sub>p" "a = head s" "xa = degree s" "\<not> degree s < n" "\<not> xa < na" 
-    "xb = funpow (xa - na) shift1 pa" "aa = x" by auto
-
-  with call1 have "polydivide_aux_dom (a, n, p, k, s -\<^sub>p funpow (degree s - n) shift1 p)"
-    by auto
-  with eqs \<Gamma>1 show "polydivide_aux_dom y" by auto
-next
-  fix y aa ka na pa sa x xa xb
-  assume eqs: "y = (aa, na, pa, Suc ka, aa *\<^sub>p sa -\<^sub>p (x *\<^sub>p xb))" 
-    "(a, n, p, k, s) =(aa, na, pa, ka, sa)"
-    and \<Gamma>2': "sa \<noteq> 0\<^sub>p" "x = head sa" "xa = degree sa" "\<not> xa < na"
-    "xb = funpow (xa - na) shift1 pa" "aa \<noteq> x"
-  hence \<Gamma>2: "s \<noteq> 0\<^sub>p" "a \<noteq> head s" "xa = degree s" "\<not> degree s < n"
-    "xb = funpow (xa - na) shift1 pa" "aa \<noteq> x" by auto
-  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
-  with eqs \<Gamma>2'  show "polydivide_aux_dom y" by auto
-qed
-
 lemma polydivide_aux_properties:
   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   and np: "isnpolyh p n0" and ns: "isnpolyh s n1"
   and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
-  shows "polydivide_aux_dom (a,n,p,k,s) \<and> 
-  (polydivide_aux (a,n,p,k,s) = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p) 
+  shows "(polydivide_aux a n p k s = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p) 
           \<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)))"
   using ns
 proof(induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
   case less
-  let ?D = "polydivide_aux_dom"
-  let ?dths = "?D (a, n, p, k, s)"
   let ?qths = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
-  let ?qrths = "polydivide_aux (a, n, p, k, s) = (k', r) \<longrightarrow>  k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) 
+  let ?ths = "polydivide_aux a n p k s = (k', r) \<longrightarrow>  k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) 
     \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
-  let ?ths = "?dths \<and> ?qrths"
   let ?b = "head s"
   let ?p' = "funpow (degree s - n) shift1 p"
   let ?xdn = "funpow (degree s - n) shift1 1\<^sub>p"
@@ -1367,17 +1332,11 @@
   from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap 
   have nakk':"isnpolyh ?akk' 0" by blast
   {assume sz: "s = 0\<^sub>p"
-    hence dom: ?dths apply - apply (rule polydivide_aux_real_domintros) apply simp_all done
-    from polydivide_aux.psimps[OF dom] sz
-    have ?qrths using np apply clarsimp by (rule exI[where x="0\<^sub>p"], simp)
-    hence ?ths using dom by blast}
+   hence ?ths using np polydivide_aux.simps apply clarsimp by (rule exI[where x="0\<^sub>p"], simp) }
   moreover
   {assume sz: "s \<noteq> 0\<^sub>p"
     {assume dn: "degree s < n"
-      with sz have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all) 
-      from polydivide_aux.psimps[OF dom] sz dn
-      have "?qrths" using ns ndp np by auto (rule exI[where x="0\<^sub>p"],simp)
-      with dom have ?ths by blast}
+      hence "?ths" using ns ndp np polydivide_aux.simps by auto (rule exI[where x="0\<^sub>p"],simp) }
     moreover 
     {assume dn': "\<not> degree s < n" hence dn: "degree s \<ge> n" by arith
       have degsp': "degree s = degree ?p'" 
@@ -1389,14 +1348,10 @@
         have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
         moreover 
         {assume deglt:"degree (s -\<^sub>p ?p') < degree s"
-          from  less(1)[OF deglt nr] 
-          have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast 
-          have dom: ?dths apply (rule polydivide_aux_real_domintros) 
-            using ba dn' domsp by simp_all
-          from polydivide_aux.psimps[OF dom] sz dn' ba
-          have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
+          from polydivide_aux.simps sz dn' ba
+          have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
             by (simp add: Let_def)
-          {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
+          {assume h1: "polydivide_aux a n p k s = (k', r)"
             from less(1)[OF deglt nr, of k k' r]
               trans[OF eq[symmetric] h1]
             have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
@@ -1431,32 +1386,26 @@
               apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
               apply (rule_tac x="0" in exI) by simp
             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"
-              by blast } hence ?qrths by blast
-          with dom have ?ths by blast} 
+              by blast } hence ?ths by blast }
         moreover 
         {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
-          hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" 
-            apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
-          have dom: ?dths apply (rule polydivide_aux_real_domintros) 
-            using ba dn' domsp by simp_all
           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}"]
           have " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" by simp
           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
             by (simp only: funpow_shift1_1) simp
           hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
-          {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
-            from polydivide_aux.psimps[OF dom] sz dn' ba
-            have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
+          {assume h1: "polydivide_aux a n p k s = (k',r)"
+            from polydivide_aux.simps sz dn' ba
+            have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
               by (simp add: Let_def)
-            also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
+            also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.simps spz by simp
             finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
             with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
-              polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
+              polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?ths
               apply auto
               apply (rule exI[where x="?xdn"])        
               apply (auto simp add: polymul_commute[of p])
-              done}
-          with dom have ?ths by blast}
+              done} }
         ultimately have ?ths by blast }
       moreover
       {assume ba: "?b \<noteq> a"
@@ -1481,15 +1430,11 @@
         have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
           by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
         {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s"
-          have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
-            using less(1)[OF dth nth] by blast 
-          have dom: ?dths using ba dn' th
-            by - (rule polydivide_aux_real_domintros, simp_all)
           from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
           ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
-          {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
-            from h1  polydivide_aux.psimps[OF dom] sz dn' ba
-            have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
+          {assume h1:"polydivide_aux a n p k s = (k', r)"
+            from h1 polydivide_aux.simps sz dn' ba
+            have eq:"polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
               by (simp add: Let_def)
             with less(1)[OF dth nasbp', of "Suc k" k' r]
             obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" 
@@ -1513,20 +1458,15 @@
             have nqw: "isnpolyh ?q 0" by simp
             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]]
             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
-            from dr kk' nr h1 asth nqw have ?qrths apply simp
+            from dr kk' nr h1 asth nqw have ?ths apply simp
               apply (rule conjI)
               apply (rule exI[where x="nr"], simp)
               apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
               apply (rule exI[where x="0"], simp)
               done}
-          hence ?qrths by blast
-          with dom have ?ths by blast}
+          hence ?ths by blast }
         moreover 
         {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
-          hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))" 
-            apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
-          have dom: ?dths using sz ba dn' domsp 
-            by - (rule polydivide_aux_real_domintros, simp_all)
           {fix bs :: "'a::{field_char_0, field_inverse_zero} list"
             from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
           have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
@@ -1540,17 +1480,16 @@
             using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
                     polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
               simplified ap] by simp
-          {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
-          from h1 sz ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] 
+          {assume h1: "polydivide_aux a n p k s = (k', r)"
+          from h1 sz ba dn' spz polydivide_aux.simps polydivide_aux.simps
           have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
           with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
             polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
-          have ?qrths apply (clarsimp simp add: Let_def)
+          have ?ths apply (clarsimp simp add: Let_def)
             apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
             apply (rule exI[where x="0"], simp)
             done}
-        hence ?qrths by blast
-        with dom have ?ths by blast}
+        hence ?ths by blast}
         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"]
           head_nz[OF np] pnz sz ap[symmetric]
           by (simp add: degree_eq_degreen0[symmetric]) blast }
@@ -1567,12 +1506,10 @@
   \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
 proof-
   have trv: "head p = head p" "degree p = degree p" by simp_all
-  from polydivide_aux_properties[OF np ns trv pnz, where k="0"] 
-  have d: "polydivide_aux_dom (head p, degree p, p, 0, s)" by blast
-  from polydivide_def[where s="s" and p="p"] polydivide_aux.psimps[OF d]
+  from polydivide_def[where s="s" and p="p"] 
   have ex: "\<exists> k r. polydivide s p = (k,r)" by auto
   then obtain k r where kr: "polydivide s p = (k,r)" by blast
-  from trans[OF meta_eq_to_obj_eq[OF polydivide_def[where s="s" and p="p"], symmetric] kr]
+  from trans[OF meta_eq_to_obj_eq[OF polydivide_def[where s="s"and p="p"], symmetric] kr]
     polydivide_aux_properties[OF np ns trv pnz, where k="0" and k'="k" and r="r"]
   have "(degree r = 0 \<or> degree r < degree p) \<and>
    (\<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