1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 08 17:12:24 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 08 21:28:27 2010 +0100
     1.3 @@ -15,11 +15,8 @@
     1.4  datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly
     1.5    | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
     1.6  
     1.7 -ML{* @{term "Add"}*}
     1.8 -syntax "_poly0" :: "poly" ("0\<^sub>p")
     1.9 -translations "0\<^sub>p" \<rightleftharpoons> "C (0\<^sub>N)"
    1.10 -syntax "_poly" :: "int \<Rightarrow> poly" ("_\<^sub>p")
    1.11 -translations "i\<^sub>p" \<rightleftharpoons> "C (i\<^sub>N)"
    1.12 +abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
    1.13 +abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)"
    1.14  
    1.15  subsection{* Boundedness, substitution and all that *}
    1.16  consts polysize:: "poly \<Rightarrow> nat"
    1.17 @@ -117,14 +114,14 @@
    1.18    polysub :: "poly\<times>poly \<Rightarrow> poly"
    1.19    polymul :: "poly\<times>poly \<Rightarrow> poly"
    1.20    polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
    1.21 -syntax "_polyadd" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
    1.22 -translations "a +\<^sub>p b" \<rightleftharpoons> "polyadd (a,b)"  
    1.23 -syntax "_polymul" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
    1.24 -translations "a *\<^sub>p b" \<rightleftharpoons> "polymul (a,b)"  
    1.25 -syntax "_polysub" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
    1.26 -translations "a -\<^sub>p b" \<rightleftharpoons> "polysub (a,b)"  
    1.27 -syntax "_polypow" :: "nat \<Rightarrow> poly \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
    1.28 -translations "a ^\<^sub>p k" \<rightleftharpoons> "polypow k a" 
    1.29 +abbreviation poly_add :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
    1.30 +  where "a +\<^sub>p b \<equiv> polyadd (a,b)"
    1.31 +abbreviation poly_mul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
    1.32 +  where "a *\<^sub>p b \<equiv> polymul (a,b)"
    1.33 +abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
    1.34 +  where "a -\<^sub>p b \<equiv> polysub (a,b)"
    1.35 +abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
    1.36 +  where "a ^\<^sub>p k \<equiv> polypow k a"
    1.37  
    1.38  recdef polyadd "measure (\<lambda> (a,b). polysize a + polysize b)"
    1.39    "polyadd (C c, C c') = C (c+\<^sub>Nc')"
    1.40 @@ -243,8 +240,9 @@
    1.41    "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
    1.42    "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
    1.43    "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
    1.44 -syntax "_Ipoly" :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_by_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    1.45 -translations "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup>" \<rightleftharpoons> "Ipoly bs p"  
    1.46 +abbreviation
    1.47 +  Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_by_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    1.48 +  where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
    1.49  
    1.50  lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" 
    1.51    by (simp add: INum_def)