src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 changeset 50282 fe4d4bb9f4c2 parent 49962 a8cc904a6820 child 52658 1e7896c7f781
```     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Nov 29 10:56:59 2012 +0100
1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Nov 29 14:05:53 2012 +0100
1.3 @@ -16,7 +16,7 @@
1.4    | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
1.5
1.6  abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
1.7 -abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)"
1.8 +abbreviation poly_p :: "int \<Rightarrow> poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \<equiv> C (i)\<^sub>N"
1.9
1.10  subsection{* Boundedness, substitution and all that *}
1.11  primrec polysize:: "poly \<Rightarrow> nat" where
1.12 @@ -153,7 +153,7 @@
1.13
1.14  fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
1.15  where
1.16 -  "polypow 0 = (\<lambda>p. 1\<^sub>p)"
1.17 +  "polypow 0 = (\<lambda>p. (1)\<^sub>p)"
1.18  | "polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul q q in
1.19                      if even n then d else polymul p d)"
1.20
1.21 @@ -162,7 +162,7 @@
1.22
1.23  function polynate :: "poly \<Rightarrow> poly"
1.24  where
1.25 -  "polynate (Bound n) = CN 0\<^sub>p n 1\<^sub>p"
1.26 +  "polynate (Bound n) = CN 0\<^sub>p n (1)\<^sub>p"
1.27  | "polynate (Add p q) = (polynate p +\<^sub>p polynate q)"
1.28  | "polynate (Sub p q) = (polynate p -\<^sub>p polynate q)"
1.29  | "polynate (Mul p q) = (polynate p *\<^sub>p polynate q)"
1.30 @@ -689,7 +689,7 @@
1.31    using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
1.32
1.33  lemma funpow_shift1_1:
1.34 -  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)"
1.35 +  "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)"
1.36    by (simp add: funpow_shift1)
1.37
1.38  lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
1.39 @@ -994,7 +994,7 @@
1.40    using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
1.41
1.42  lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
1.43 -lemma one_normh: "isnpolyh 1\<^sub>p n" by simp
1.44 +lemma one_normh: "isnpolyh (1)\<^sub>p n" by simp
1.46    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.47    and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
1.48 @@ -1003,7 +1003,7 @@
1.49
1.50  lemma polymul_1[simp]:
1.51      assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
1.52 -  and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
1.53 +  and np: "isnpolyh p n0" shows "p *\<^sub>p (1)\<^sub>p = p" and "(1)\<^sub>p *\<^sub>p p = p"
1.54    using isnpolyh_unique[OF polymul_normh[OF np one_normh] np]
1.55      isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
1.56  lemma polymul_0[simp]:
1.57 @@ -1262,14 +1262,14 @@
1.58      \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
1.59    let ?b = "head s"
1.60    let ?p' = "funpow (degree s - n) shift1 p"
1.61 -  let ?xdn = "funpow (degree s - n) shift1 1\<^sub>p"
1.62 +  let ?xdn = "funpow (degree s - n) shift1 (1)\<^sub>p"
1.63    let ?akk' = "a ^\<^sub>p (k' - k)"
1.64    note ns = `isnpolyh s n1`
1.65    from np have np0: "isnpolyh p 0"
1.66      using isnpolyh_mono[where n="n0" and n'="0" and p="p"]  by simp
1.67    have np': "isnpolyh ?p' 0" using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="degree s - n"] isnpoly_def by simp
1.68    have headp': "head ?p' = head p" using funpow_shift1_head[OF np pnz] by simp
1.69 -  from funpow_shift1_isnpoly[where p="1\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def)
1.70 +  from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def)
1.71    from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap
1.72    have nakk':"isnpolyh ?akk' 0" by blast
1.73    {assume sz: "s = 0\<^sub>p"
1.74 @@ -1312,19 +1312,19 @@
1.75                Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.76                by (simp add: field_simps)
1.77              hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.78 -              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p)
1.79 +              Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p)
1.80                + Ipoly bs p * Ipoly bs q + Ipoly bs r"
1.81                by (auto simp only: funpow_shift1_1)
1.82              hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.83 -              Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p)
1.84 +              Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p)
1.85                + Ipoly bs q) + Ipoly bs r" by (simp add: field_simps)
1.86              hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
1.87 -              Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp
1.88 +              Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp
1.89              with isnpolyh_unique[OF nakks' nqr']
1.90              have "a ^\<^sub>p (k' - k) *\<^sub>p s =
1.91 -              p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast
1.92 +              p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast
1.93              hence ?qths using nq'
1.94 -              apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
1.95 +              apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q" in exI)
1.96                apply (rule_tac x="0" in exI) by simp
1.97              with kk' nr dr have "k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
1.98                by blast } hence ?ths by blast }
```