1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Feb 21 18:29:47 2011 +0100
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Feb 21 23:14:36 2011 +0100
1.3 @@ -50,75 +50,72 @@
1.4 | "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
1.5 else CN (polysubst0 t c) n (polysubst0 t p))"
1.6
1.7 -consts
1.8 - decrpoly:: "poly \<Rightarrow> poly"
1.9 -recdef decrpoly "measure polysize"
1.10 +fun decrpoly:: "poly \<Rightarrow> poly"
1.11 +where
1.12 "decrpoly (Bound n) = Bound (n - 1)"
1.13 - "decrpoly (Neg a) = Neg (decrpoly a)"
1.14 - "decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)"
1.15 - "decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)"
1.16 - "decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)"
1.17 - "decrpoly (Pw p n) = Pw (decrpoly p) n"
1.18 - "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)"
1.19 - "decrpoly a = a"
1.20 +| "decrpoly (Neg a) = Neg (decrpoly a)"
1.21 +| "decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)"
1.22 +| "decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)"
1.23 +| "decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)"
1.24 +| "decrpoly (Pw p n) = Pw (decrpoly p) n"
1.25 +| "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)"
1.26 +| "decrpoly a = a"
1.27
1.28 subsection{* Degrees and heads and coefficients *}
1.29
1.30 -consts degree:: "poly \<Rightarrow> nat"
1.31 -recdef degree "measure size"
1.32 +fun degree:: "poly \<Rightarrow> nat"
1.33 +where
1.34 "degree (CN c 0 p) = 1 + degree p"
1.35 - "degree p = 0"
1.36 -consts head:: "poly \<Rightarrow> poly"
1.37 +| "degree p = 0"
1.38
1.39 -recdef head "measure size"
1.40 +fun head:: "poly \<Rightarrow> poly"
1.41 +where
1.42 "head (CN c 0 p) = head p"
1.43 - "head p = p"
1.44 - (* More general notions of degree and head *)
1.45 -consts degreen:: "poly \<Rightarrow> nat \<Rightarrow> nat"
1.46 -recdef degreen "measure size"
1.47 +| "head p = p"
1.48 +
1.49 +(* More general notions of degree and head *)
1.50 +fun degreen:: "poly \<Rightarrow> nat \<Rightarrow> nat"
1.51 +where
1.52 "degreen (CN c n p) = (\<lambda>m. if n=m then 1 + degreen p n else 0)"
1.53 - "degreen p = (\<lambda>m. 0)"
1.54 + |"degreen p = (\<lambda>m. 0)"
1.55
1.56 -consts headn:: "poly \<Rightarrow> nat \<Rightarrow> poly"
1.57 -recdef headn "measure size"
1.58 +fun headn:: "poly \<Rightarrow> nat \<Rightarrow> poly"
1.59 +where
1.60 "headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)"
1.61 - "headn p = (\<lambda>m. p)"
1.62 +| "headn p = (\<lambda>m. p)"
1.63
1.64 -consts coefficients:: "poly \<Rightarrow> poly list"
1.65 -recdef coefficients "measure size"
1.66 +fun coefficients:: "poly \<Rightarrow> poly list"
1.67 +where
1.68 "coefficients (CN c 0 p) = c#(coefficients p)"
1.69 - "coefficients p = [p]"
1.70 +| "coefficients p = [p]"
1.71
1.72 -consts isconstant:: "poly \<Rightarrow> bool"
1.73 -recdef isconstant "measure size"
1.74 +fun isconstant:: "poly \<Rightarrow> bool"
1.75 +where
1.76 "isconstant (CN c 0 p) = False"
1.77 - "isconstant p = True"
1.78 +| "isconstant p = True"
1.79
1.80 -consts behead:: "poly \<Rightarrow> poly"
1.81 -recdef behead "measure size"
1.82 +fun behead:: "poly \<Rightarrow> poly"
1.83 +where
1.84 "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
1.85 - "behead p = 0\<^sub>p"
1.86 +| "behead p = 0\<^sub>p"
1.87
1.88 -consts headconst:: "poly \<Rightarrow> Num"
1.89 -recdef headconst "measure size"
1.90 +fun headconst:: "poly \<Rightarrow> Num"
1.91 +where
1.92 "headconst (CN c n p) = headconst p"
1.93 - "headconst (C n) = n"
1.94 +| "headconst (C n) = n"
1.95
1.96 subsection{* Operations for normalization *}
1.97 consts
1.98 polyadd :: "poly\<times>poly \<Rightarrow> poly"
1.99 - polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p")
1.100 polysub :: "poly\<times>poly \<Rightarrow> poly"
1.101 polymul :: "poly\<times>poly \<Rightarrow> poly"
1.102 - polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
1.103 +
1.104 abbreviation poly_add :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
1.105 where "a +\<^sub>p b \<equiv> polyadd (a,b)"
1.106 abbreviation poly_mul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
1.107 where "a *\<^sub>p b \<equiv> polymul (a,b)"
1.108 abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
1.109 where "a -\<^sub>p b \<equiv> polysub (a,b)"
1.110 -abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
1.111 - where "a ^\<^sub>p k \<equiv> polypow k a"
1.112
1.113 recdef polyadd "measure (\<lambda> (a,b). polysize a + polysize b)"
1.114 "polyadd (C c, C c') = C (c+\<^sub>Nc')"
1.115 @@ -133,10 +130,11 @@
1.116 "polyadd (a, b) = Add a b"
1.117 (hints recdef_simp add: Let_def measure_def split_def inv_image_def recdef_cong del: if_cong)
1.118
1.119 -recdef polyneg "measure size"
1.120 +fun polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p")
1.121 +where
1.122 "polyneg (C c) = C (~\<^sub>N c)"
1.123 - "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
1.124 - "polyneg a = Neg a"
1.125 +| "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
1.126 +| "polyneg a = Neg a"
1.127
1.128 defs polysub_def[code]: "polysub \<equiv> \<lambda> (p,q). polyadd (p,polyneg q)"
1.129
1.130 @@ -152,21 +150,28 @@
1.131 then CN (polymul(CN c n p,c')) n' (polymul(CN c n p,p'))
1.132 else polyadd(polymul(CN c n p, c'),CN 0\<^sub>p n' (polymul(CN c n p, p'))))"
1.133 "polymul (a,b) = Mul a b"
1.134 -recdef polypow "measure id"
1.135 +
1.136 +fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
1.137 +where
1.138 "polypow 0 = (\<lambda>p. 1\<^sub>p)"
1.139 - "polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul(q,q) in
1.140 +| "polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul(q,q) in
1.141 if even n then d else polymul(p,d))"
1.142
1.143 -consts polynate :: "poly \<Rightarrow> poly"
1.144 -recdef polynate "measure polysize"
1.145 +abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
1.146 + where "a ^\<^sub>p k \<equiv> polypow k a"
1.147 +
1.148 +function polynate :: "poly \<Rightarrow> poly"
1.149 +where
1.150 "polynate (Bound n) = CN 0\<^sub>p n 1\<^sub>p"
1.151 - "polynate (Add p q) = (polynate p +\<^sub>p polynate q)"
1.152 - "polynate (Sub p q) = (polynate p -\<^sub>p polynate q)"
1.153 - "polynate (Mul p q) = (polynate p *\<^sub>p polynate q)"
1.154 - "polynate (Neg p) = (~\<^sub>p (polynate p))"
1.155 - "polynate (Pw p n) = ((polynate p) ^\<^sub>p n)"
1.156 - "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
1.157 - "polynate (C c) = C (normNum c)"
1.158 +| "polynate (Add p q) = (polynate p +\<^sub>p polynate q)"
1.159 +| "polynate (Sub p q) = (polynate p -\<^sub>p polynate q)"
1.160 +| "polynate (Mul p q) = (polynate p *\<^sub>p polynate q)"
1.161 +| "polynate (Neg p) = (~\<^sub>p (polynate p))"
1.162 +| "polynate (Pw p n) = ((polynate p) ^\<^sub>p n)"
1.163 +| "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
1.164 +| "polynate (C c) = C (normNum c)"
1.165 +by pat_completeness auto
1.166 +termination by (relation "measure polysize") auto
1.167
1.168 fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly" where
1.169 "poly_cmul y (C x) = C (y *\<^sub>N x)"
1.170 @@ -235,11 +240,11 @@
1.171
1.172 subsection {* Normal form and normalization *}
1.173
1.174 -consts isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
1.175 -recdef isnpolyh "measure size"
1.176 +fun isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
1.177 +where
1.178 "isnpolyh (C c) = (\<lambda>k. isnormNum c)"
1.179 - "isnpolyh (CN c n p) = (\<lambda>k. n\<ge> k \<and> (isnpolyh c (Suc n)) \<and> (isnpolyh p n) \<and> (p \<noteq> 0\<^sub>p))"
1.180 - "isnpolyh p = (\<lambda>k. False)"
1.181 +| "isnpolyh (CN c n p) = (\<lambda>k. n \<ge> k \<and> (isnpolyh c (Suc n)) \<and> (isnpolyh p n) \<and> (p \<noteq> 0\<^sub>p))"
1.182 +| "isnpolyh p = (\<lambda>k. False)"
1.183
1.184 lemma isnpolyh_mono: "\<lbrakk>n' \<le> n ; isnpolyh p n\<rbrakk> \<Longrightarrow> isnpolyh p n'"
1.185 by (induct p rule: isnpolyh.induct, auto)
1.186 @@ -1618,11 +1623,11 @@
1.187
1.188 lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)" by (induct p, simp_all)
1.189
1.190 -consts isweaknpoly :: "poly \<Rightarrow> bool"
1.191 -recdef isweaknpoly "measure size"
1.192 +fun isweaknpoly :: "poly \<Rightarrow> bool"
1.193 +where
1.194 "isweaknpoly (C c) = True"
1.195 - "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
1.196 - "isweaknpoly p = False"
1.197 +| "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
1.198 +| "isweaknpoly p = False"
1.199
1.200 lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p"
1.201 by (induct p arbitrary: n0, auto)