recdef -> function
authorkrauss
Mon Feb 21 23:14:36 2011 +0100 (2011-02-21)
changeset 418089f436d00248f
parent 41806 173e1b50d5c5
child 41809 6799f95479e2
recdef -> function
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
     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 -
    1.55 -consts headn:: "poly \<Rightarrow> nat \<Rightarrow> poly"
    1.56 -recdef headn "measure size"
    1.57 -  "headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)"
    1.58 -  "headn p = (\<lambda>m. p)"
    1.59 + |"degreen p = (\<lambda>m. 0)"
    1.60  
    1.61 -consts coefficients:: "poly \<Rightarrow> poly list"
    1.62 -recdef coefficients "measure size"
    1.63 -  "coefficients (CN c 0 p) = c#(coefficients p)"
    1.64 -  "coefficients p = [p]"
    1.65 +fun headn:: "poly \<Rightarrow> nat \<Rightarrow> poly"
    1.66 +where
    1.67 +  "headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)"
    1.68 +| "headn p = (\<lambda>m. p)"
    1.69  
    1.70 -consts isconstant:: "poly \<Rightarrow> bool"
    1.71 -recdef isconstant "measure size"
    1.72 -  "isconstant (CN c 0 p) = False"
    1.73 -  "isconstant p = True"
    1.74 +fun coefficients:: "poly \<Rightarrow> poly list"
    1.75 +where
    1.76 +  "coefficients (CN c 0 p) = c#(coefficients p)"
    1.77 +| "coefficients p = [p]"
    1.78  
    1.79 -consts behead:: "poly \<Rightarrow> poly"
    1.80 -recdef behead "measure size"
    1.81 -  "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
    1.82 -  "behead p = 0\<^sub>p"
    1.83 +fun isconstant:: "poly \<Rightarrow> bool"
    1.84 +where
    1.85 +  "isconstant (CN c 0 p) = False"
    1.86 +| "isconstant p = True"
    1.87  
    1.88 -consts headconst:: "poly \<Rightarrow> Num"
    1.89 -recdef headconst "measure size"
    1.90 +fun behead:: "poly \<Rightarrow> poly"
    1.91 +where
    1.92 +  "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
    1.93 +| "behead p = 0\<^sub>p"
    1.94 +
    1.95 +fun headconst:: "poly \<Rightarrow> Num"
    1.96 +where
    1.97    "headconst (CN c n p) = headconst p"
    1.98 -  "headconst (C n) = n"
    1.99 +| "headconst (C n) = n"
   1.100  
   1.101  subsection{* Operations for normalization *}
   1.102  consts 
   1.103    polyadd :: "poly\<times>poly \<Rightarrow> poly"
   1.104 -  polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p")
   1.105    polysub :: "poly\<times>poly \<Rightarrow> poly"
   1.106    polymul :: "poly\<times>poly \<Rightarrow> poly"
   1.107 -  polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
   1.108 +
   1.109  abbreviation poly_add :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
   1.110    where "a +\<^sub>p b \<equiv> polyadd (a,b)"
   1.111  abbreviation poly_mul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
   1.112    where "a *\<^sub>p b \<equiv> polymul (a,b)"
   1.113  abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
   1.114    where "a -\<^sub>p b \<equiv> polysub (a,b)"
   1.115 -abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
   1.116 -  where "a ^\<^sub>p k \<equiv> polypow k a"
   1.117  
   1.118  recdef polyadd "measure (\<lambda> (a,b). polysize a + polysize b)"
   1.119    "polyadd (C c, C c') = C (c+\<^sub>Nc')"
   1.120 @@ -133,10 +130,11 @@
   1.121    "polyadd (a, b) = Add a b"
   1.122  (hints recdef_simp add: Let_def measure_def split_def inv_image_def recdef_cong del: if_cong)
   1.123  
   1.124 -recdef polyneg "measure size"
   1.125 +fun polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p")
   1.126 +where
   1.127    "polyneg (C c) = C (~\<^sub>N c)"
   1.128 -  "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
   1.129 -  "polyneg a = Neg a"
   1.130 +| "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
   1.131 +| "polyneg a = Neg a"
   1.132  
   1.133  defs polysub_def[code]: "polysub \<equiv> \<lambda> (p,q). polyadd (p,polyneg q)"
   1.134  
   1.135 @@ -152,21 +150,28 @@
   1.136    then CN (polymul(CN c n p,c')) n' (polymul(CN c n p,p'))
   1.137    else polyadd(polymul(CN c n p, c'),CN 0\<^sub>p n' (polymul(CN c n p, p'))))"
   1.138    "polymul (a,b) = Mul a b"
   1.139 -recdef polypow "measure id"
   1.140 +
   1.141 +fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
   1.142 +where
   1.143    "polypow 0 = (\<lambda>p. 1\<^sub>p)"
   1.144 -  "polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul(q,q) in 
   1.145 +| "polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul(q,q) in 
   1.146                      if even n then d else polymul(p,d))"
   1.147  
   1.148 -consts polynate :: "poly \<Rightarrow> poly"
   1.149 -recdef polynate "measure polysize"
   1.150 +abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
   1.151 +  where "a ^\<^sub>p k \<equiv> polypow k a"
   1.152 +
   1.153 +function polynate :: "poly \<Rightarrow> poly"
   1.154 +where
   1.155    "polynate (Bound n) = CN 0\<^sub>p n 1\<^sub>p"
   1.156 -  "polynate (Add p q) = (polynate p +\<^sub>p polynate q)"
   1.157 -  "polynate (Sub p q) = (polynate p -\<^sub>p polynate q)"
   1.158 -  "polynate (Mul p q) = (polynate p *\<^sub>p polynate q)"
   1.159 -  "polynate (Neg p) = (~\<^sub>p (polynate p))"
   1.160 -  "polynate (Pw p n) = ((polynate p) ^\<^sub>p n)"
   1.161 -  "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
   1.162 -  "polynate (C c) = C (normNum c)"
   1.163 +| "polynate (Add p q) = (polynate p +\<^sub>p polynate q)"
   1.164 +| "polynate (Sub p q) = (polynate p -\<^sub>p polynate q)"
   1.165 +| "polynate (Mul p q) = (polynate p *\<^sub>p polynate q)"
   1.166 +| "polynate (Neg p) = (~\<^sub>p (polynate p))"
   1.167 +| "polynate (Pw p n) = ((polynate p) ^\<^sub>p n)"
   1.168 +| "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
   1.169 +| "polynate (C c) = C (normNum c)"
   1.170 +by pat_completeness auto
   1.171 +termination by (relation "measure polysize") auto
   1.172  
   1.173  fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly" where
   1.174    "poly_cmul y (C x) = C (y *\<^sub>N x)"
   1.175 @@ -235,11 +240,11 @@
   1.176  
   1.177  subsection {* Normal form and normalization *}
   1.178  
   1.179 -consts isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
   1.180 -recdef isnpolyh "measure size"
   1.181 +fun isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
   1.182 +where
   1.183    "isnpolyh (C c) = (\<lambda>k. isnormNum c)"
   1.184 -  "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.185 -  "isnpolyh p = (\<lambda>k. False)"
   1.186 +| "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.187 +| "isnpolyh p = (\<lambda>k. False)"
   1.188  
   1.189  lemma isnpolyh_mono: "\<lbrakk>n' \<le> n ; isnpolyh p n\<rbrakk> \<Longrightarrow> isnpolyh p n'"
   1.190  by (induct p rule: isnpolyh.induct, auto)
   1.191 @@ -1618,11 +1623,11 @@
   1.192  
   1.193  lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)" by (induct p, simp_all)
   1.194  
   1.195 -consts isweaknpoly :: "poly \<Rightarrow> bool"
   1.196 -recdef isweaknpoly "measure size"
   1.197 +fun isweaknpoly :: "poly \<Rightarrow> bool"
   1.198 +where
   1.199    "isweaknpoly (C c) = True"
   1.200 -  "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
   1.201 -  "isweaknpoly p = False"       
   1.202 +| "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
   1.203 +| "isweaknpoly p = False"
   1.204  
   1.205  lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p" 
   1.206    by (induct p arbitrary: n0, auto)