src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 39246 9e58f0499f57
parent 36409 d323e7773aa8
child 41403 7eba049f7310
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Sep 08 13:25:22 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Sep 08 19:21:46 2010 +0200
     1.3 @@ -19,38 +19,35 @@
     1.4  abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)"
     1.5  
     1.6  subsection{* Boundedness, substitution and all that *}
     1.7 -consts polysize:: "poly \<Rightarrow> nat"
     1.8 -primrec
     1.9 +primrec polysize:: "poly \<Rightarrow> nat" where
    1.10    "polysize (C c) = 1"
    1.11 -  "polysize (Bound n) = 1"
    1.12 -  "polysize (Neg p) = 1 + polysize p"
    1.13 -  "polysize (Add p q) = 1 + polysize p + polysize q"
    1.14 -  "polysize (Sub p q) = 1 + polysize p + polysize q"
    1.15 -  "polysize (Mul p q) = 1 + polysize p + polysize q"
    1.16 -  "polysize (Pw p n) = 1 + polysize p"
    1.17 -  "polysize (CN c n p) = 4 + polysize c + polysize p"
    1.18 +| "polysize (Bound n) = 1"
    1.19 +| "polysize (Neg p) = 1 + polysize p"
    1.20 +| "polysize (Add p q) = 1 + polysize p + polysize q"
    1.21 +| "polysize (Sub p q) = 1 + polysize p + polysize q"
    1.22 +| "polysize (Mul p q) = 1 + polysize p + polysize q"
    1.23 +| "polysize (Pw p n) = 1 + polysize p"
    1.24 +| "polysize (CN c n p) = 4 + polysize c + polysize p"
    1.25  
    1.26 -consts 
    1.27 -  polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *)
    1.28 -  polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *)
    1.29 -primrec
    1.30 +primrec polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *) where
    1.31    "polybound0 (C c) = True"
    1.32 -  "polybound0 (Bound n) = (n>0)"
    1.33 -  "polybound0 (Neg a) = polybound0 a"
    1.34 -  "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)"
    1.35 -  "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)" 
    1.36 -  "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)"
    1.37 -  "polybound0 (Pw p n) = (polybound0 p)"
    1.38 -  "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
    1.39 -primrec
    1.40 +| "polybound0 (Bound n) = (n>0)"
    1.41 +| "polybound0 (Neg a) = polybound0 a"
    1.42 +| "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)"
    1.43 +| "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)" 
    1.44 +| "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)"
    1.45 +| "polybound0 (Pw p n) = (polybound0 p)"
    1.46 +| "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
    1.47 +
    1.48 +primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *) where
    1.49    "polysubst0 t (C c) = (C c)"
    1.50 -  "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
    1.51 -  "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
    1.52 -  "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
    1.53 -  "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" 
    1.54 -  "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
    1.55 -  "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
    1.56 -  "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
    1.57 +| "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
    1.58 +| "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
    1.59 +| "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
    1.60 +| "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" 
    1.61 +| "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
    1.62 +| "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
    1.63 +| "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
    1.64                               else CN (polysubst0 t c) n (polysubst0 t p))"
    1.65  
    1.66  consts 
    1.67 @@ -195,11 +192,10 @@
    1.68  
    1.69  definition shift1 :: "poly \<Rightarrow> poly" where
    1.70    "shift1 p \<equiv> CN 0\<^sub>p 0 p"
    1.71 -consts funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
    1.72  
    1.73 -primrec
    1.74 -  "funpow 0 f x = x"
    1.75 -  "funpow (Suc n) f x = funpow n f (f x)"
    1.76 +abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" where
    1.77 +  "funpow \<equiv> compow"
    1.78 +
    1.79  function (tailrec) polydivide_aux :: "(poly \<times> nat \<times> poly \<times> nat \<times> poly) \<Rightarrow> (nat \<times> poly)"
    1.80    where
    1.81    "polydivide_aux (a,n,p,k,s) = 
    1.82 @@ -211,7 +207,6 @@
    1.83    else polydivide_aux (a,n,p,Suc k, (a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
    1.84    by pat_completeness auto
    1.85  
    1.86 -
    1.87  definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where
    1.88    "polydivide s p \<equiv> polydivide_aux (head p,degree p,p,0, s)"
    1.89  
    1.90 @@ -230,16 +225,16 @@
    1.91  
    1.92  subsection{* Semantics of the polynomial representation *}
    1.93  
    1.94 -consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}"
    1.95 -primrec
    1.96 +primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
    1.97    "Ipoly bs (C c) = INum c"
    1.98 -  "Ipoly bs (Bound n) = bs!n"
    1.99 -  "Ipoly bs (Neg a) = - Ipoly bs a"
   1.100 -  "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
   1.101 -  "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
   1.102 -  "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
   1.103 -  "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
   1.104 -  "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
   1.105 +| "Ipoly bs (Bound n) = bs!n"
   1.106 +| "Ipoly bs (Neg a) = - Ipoly bs a"
   1.107 +| "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
   1.108 +| "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
   1.109 +| "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
   1.110 +| "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
   1.111 +| "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
   1.112 +
   1.113  abbreviation
   1.114    Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
   1.115    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
   1.116 @@ -729,7 +724,7 @@
   1.117    by (simp add: shift1_def)
   1.118  lemma funpow_shift1_isnpoly: 
   1.119    "\<lbrakk> isnpoly p ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> isnpoly (funpow n shift1 p)"
   1.120 -  by (induct n arbitrary: p, auto simp add: shift1_isnpoly)
   1.121 +  by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
   1.122  
   1.123  lemma funpow_isnpolyh: 
   1.124    assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n "and np: "isnpolyh p n"
   1.125 @@ -767,7 +762,7 @@
   1.126  
   1.127  subsection{* Miscilanious lemmas about indexes, decrementation, substitution  etc ... *}
   1.128  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
   1.129 -proof(induct p arbitrary: n rule: polybound0.induct, auto)
   1.130 +proof(induct p arbitrary: n rule: poly.induct, auto)
   1.131    case (goal1 c n p n')
   1.132    hence "n = Suc (n - 1)" by simp
   1.133    hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp
   1.134 @@ -793,7 +788,7 @@
   1.135    assumes nb: "polybound0 a"
   1.136    shows "Ipoly (b#bs) a = Ipoly (b'#bs) a"
   1.137  using nb
   1.138 -by (induct a rule: polybound0.induct) auto 
   1.139 +by (induct a rule: poly.induct) auto 
   1.140  lemma polysubst0_I:
   1.141    shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"
   1.142    by (induct t) simp_all
   1.143 @@ -809,12 +804,12 @@
   1.144  
   1.145  lemma polysubst0_polybound0: assumes nb: "polybound0 t"
   1.146    shows "polybound0 (polysubst0 t a)"
   1.147 -using nb by (induct a rule: polysubst0.induct, auto)
   1.148 +using nb by (induct a rule: poly.induct, auto)
   1.149  
   1.150  lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
   1.151    by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0)
   1.152  
   1.153 -fun maxindex :: "poly \<Rightarrow> nat" where
   1.154 +primrec maxindex :: "poly \<Rightarrow> nat" where
   1.155    "maxindex (Bound n) = n + 1"
   1.156  | "maxindex (CN c n p) = max  (n + 1) (max (maxindex c) (maxindex p))"
   1.157  | "maxindex (Add p q) = max (maxindex p) (maxindex q)"
   1.158 @@ -1183,7 +1178,7 @@
   1.159    case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
   1.160    with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
   1.161      and "head (shift1 p) = head p" by (simp_all add: shift1_head) 
   1.162 -  thus ?case by simp
   1.163 +  thus ?case by (simp add: funpow_swap1)
   1.164  qed auto  
   1.165  
   1.166  lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
   1.167 @@ -1641,8 +1636,8 @@
   1.168  
   1.169  lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
   1.170    unfolding pnormal_def
   1.171 - apply (induct p rule: pnormalize.induct, simp_all)
   1.172 - apply (case_tac "p=[]", simp_all)
   1.173 + apply (induct p)
   1.174 + apply (simp_all, case_tac "p=[]", simp_all)
   1.175   done
   1.176  
   1.177  lemma degree_degree: assumes inc: "isnonconstant p"
   1.178 @@ -1668,16 +1663,15 @@
   1.179  qed
   1.180  
   1.181  section{* Swaps ; Division by a certain variable *}
   1.182 -consts swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly"
   1.183 -primrec
   1.184 +primrec swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" where
   1.185    "swap n m (C x) = C x"
   1.186 -  "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
   1.187 -  "swap n m (Neg t) = Neg (swap n m t)"
   1.188 -  "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
   1.189 -  "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
   1.190 -  "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
   1.191 -  "swap n m (Pw t k) = Pw (swap n m t) k"
   1.192 -  "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k)
   1.193 +| "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
   1.194 +| "swap n m (Neg t) = Neg (swap n m t)"
   1.195 +| "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
   1.196 +| "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
   1.197 +| "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
   1.198 +| "swap n m (Pw t k) = Pw (swap n m t) k"
   1.199 +| "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k)
   1.200    (swap n m p)"
   1.201  
   1.202  lemma swap: assumes nbs: "n < length bs" and mbs: "m < length bs"