src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 35416 d8d7d1b785af
parent 35054 a5db9779b026
child 36349 39be26d1bc28
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -188,12 +188,12 @@
     1.4  | "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)"
     1.5  | "poly_cmul y p = C y *\<^sub>p p"
     1.6  
     1.7 -constdefs monic:: "poly \<Rightarrow> (poly \<times> bool)"
     1.8 +definition monic :: "poly \<Rightarrow> (poly \<times> bool)" where
     1.9    "monic p \<equiv> (let h = headconst p in if h = 0\<^sub>N then (p,False) else ((C (Ninv h)) *\<^sub>p p, 0>\<^sub>N h))"
    1.10  
    1.11  subsection{* Pseudo-division *}
    1.12  
    1.13 -constdefs shift1:: "poly \<Rightarrow> poly"
    1.14 +definition shift1 :: "poly \<Rightarrow> poly" where
    1.15    "shift1 p \<equiv> CN 0\<^sub>p 0 p"
    1.16  consts funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
    1.17  
    1.18 @@ -212,7 +212,7 @@
    1.19    by pat_completeness auto
    1.20  
    1.21  
    1.22 -constdefs polydivide:: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)"
    1.23 +definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where
    1.24    "polydivide s p \<equiv> polydivide_aux (head p,degree p,p,0, s)"
    1.25  
    1.26  fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" where
    1.27 @@ -262,7 +262,7 @@
    1.28  lemma isnpolyh_mono: "\<lbrakk>n' \<le> n ; isnpolyh p n\<rbrakk> \<Longrightarrow> isnpolyh p n'"
    1.29  by (induct p rule: isnpolyh.induct, auto)
    1.30  
    1.31 -constdefs isnpoly:: "poly \<Rightarrow> bool"
    1.32 +definition isnpoly :: "poly \<Rightarrow> bool" where
    1.33    "isnpoly p \<equiv> isnpolyh p 0"
    1.34  
    1.35  text{* polyadd preserves normal forms *}