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.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.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"
```