# HG changeset patch # User wenzelm # Date 1354194353 -3600 # Node ID fe4d4bb9f4c2547f0a57a3348b5b13e11749eab1 # Parent cbba160847842a31e7bf17e3f4bdf7e630aea35b more robust syntax that survives collapse of \<^isub> and \<^sub>; diff -r cbba16084784 -r fe4d4bb9f4c2 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Nov 29 10:56:59 2012 +0100 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Nov 29 14:05:53 2012 +0100 @@ -297,7 +297,7 @@ fun simptm:: "tm \ tm" where "simptm (CP j) = CP (polynate j)" -| "simptm (Bound n) = CNP n 1\<^sub>p (CP 0\<^sub>p)" +| "simptm (Bound n) = CNP n (1)\<^sub>p (CP 0\<^sub>p)" | "simptm (Neg t) = tmneg (simptm t)" | "simptm (Add t s) = tmadd (simptm t,simptm s)" | "simptm (Sub t s) = tmsub (simptm t) (simptm s)" @@ -333,7 +333,7 @@ declare let_cong[fundef_cong del] fun split0 :: "tm \ (poly \ tm)" where - "split0 (Bound 0) = (1\<^sub>p, CP 0\<^sub>p)" + "split0 (Bound 0) = ((1)\<^sub>p, CP 0\<^sub>p)" | "split0 (CNP 0 c t) = (let (c',t') = split0 t in (c +\<^sub>p c',t'))" | "split0 (Neg t) = (let (c,t') = split0 t in (~\<^sub>p c,Neg t'))" | "split0 (CNP n c t) = (let (c',t') = split0 t in (c',CNP n c t'))" @@ -1892,17 +1892,17 @@ section{* First implementation : Naive by encoding all case splits locally *} definition "msubsteq c t d s a r = evaldjf (split conj) - [(let cd = c *\<^sub>p d in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul (2\<^sub>p *\<^sub>p cd) r)))), - (conj (Eq (CP c)) (NEq (CP d)) , Eq (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))), - (conj (NEq (CP c)) (Eq (CP d)) , Eq (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))), + [(let cd = c *\<^sub>p d in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (Eq (CP c)) (NEq (CP d)) , Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (NEq (CP c)) (Eq (CP d)) , Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), (conj (Eq (CP c)) (Eq (CP d)) , Eq r)]" lemma msubsteq_nb: assumes lp: "islin (Eq (CNP 0 a r))" and t: "tmbound0 t" and s: "tmbound0 s" shows "bound0 (msubsteq c t d s a r)" proof- - have th: "\x\ set [(let cd = c *\<^sub>p d in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul (2\<^sub>p *\<^sub>p cd) r)))), - (conj (Eq (CP c)) (NEq (CP d)) , Eq (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))), - (conj (NEq (CP c)) (Eq (CP d)) , Eq (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))), + have th: "\x\ set [(let cd = c *\<^sub>p d in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (Eq (CP c)) (NEq (CP d)) , Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (NEq (CP c)) (Eq (CP d)) , Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), (conj (Eq (CP c)) (Eq (CP d)) , Eq r)]. bound0 (split conj x)" using lp by (simp add: Let_def t s ) from evaldjf_bound0[OF th] show ?thesis by (simp add: msubsteq_def) @@ -1974,17 +1974,17 @@ definition "msubstneq c t d s a r = evaldjf (split conj) - [(let cd = c *\<^sub>p d in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul (2\<^sub>p *\<^sub>p cd) r)))), - (conj (Eq (CP c)) (NEq (CP d)) , NEq (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))), - (conj (NEq (CP c)) (Eq (CP d)) , NEq (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))), + [(let cd = c *\<^sub>p d in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (Eq (CP c)) (NEq (CP d)) , NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (NEq (CP c)) (Eq (CP d)) , NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), (conj (Eq (CP c)) (Eq (CP d)) , NEq r)]" lemma msubstneq_nb: assumes lp: "islin (NEq (CNP 0 a r))" and t: "tmbound0 t" and s: "tmbound0 s" shows "bound0 (msubstneq c t d s a r)" proof- - have th: "\x\ set [(let cd = c *\<^sub>p d in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul (2\<^sub>p *\<^sub>p cd) r)))), - (conj (Eq (CP c)) (NEq (CP d)) , NEq (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))), - (conj (NEq (CP c)) (Eq (CP d)) , NEq (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))), + have th: "\x\ set [(let cd = c *\<^sub>p d in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (Eq (CP c)) (NEq (CP d)) , NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (NEq (CP c)) (Eq (CP d)) , NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), (conj (Eq (CP c)) (Eq (CP d)) , NEq r)]. bound0 (split conj x)" using lp by (simp add: Let_def t s ) from evaldjf_bound0[OF th] show ?thesis by (simp add: msubstneq_def) @@ -2055,23 +2055,23 @@ definition "msubstlt c t d s a r = evaldjf (split conj) - [(let cd = c *\<^sub>p d in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul (2\<^sub>p *\<^sub>p cd) r)))), - (let cd = c *\<^sub>p d in (lt (CP cd), Lt (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul (2\<^sub>p *\<^sub>p cd) r)))), - (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Lt (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP c)) (Eq (CP d)) , Lt (Sub (Mul a t) (Mul (2\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Lt (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))), - (conj (lt (CP d)) (Eq (CP c)) , Lt (Sub (Mul a s) (Mul (2\<^sub>p *\<^sub>p d) r))), + [(let cd = c *\<^sub>p d in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (let cd = c *\<^sub>p d in (lt (CP cd), Lt (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Lt (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP c)) (Eq (CP d)) , Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (lt (CP d)) (Eq (CP c)) , Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), (conj (Eq (CP c)) (Eq (CP d)) , Lt r)]" lemma msubstlt_nb: assumes lp: "islin (Lt (CNP 0 a r))" and t: "tmbound0 t" and s: "tmbound0 s" shows "bound0 (msubstlt c t d s a r)" proof- - have th: "\x\ set [(let cd = c *\<^sub>p d in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul (2\<^sub>p *\<^sub>p cd) r)))), - (let cd = c *\<^sub>p d in (lt (CP cd), Lt (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul (2\<^sub>p *\<^sub>p cd) r)))), - (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Lt (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP c)) (Eq (CP d)) , Lt (Sub (Mul a t) (Mul (2\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Lt (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))), - (conj (lt (CP d)) (Eq (CP c)) , Lt (Sub (Mul a s) (Mul (2\<^sub>p *\<^sub>p d) r))), + have th: "\x\ set [(let cd = c *\<^sub>p d in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (let cd = c *\<^sub>p d in (lt (CP cd), Lt (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Lt (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP c)) (Eq (CP d)) , Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (lt (CP d)) (Eq (CP c)) , Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), (conj (Eq (CP c)) (Eq (CP d)) , Lt r)]. bound0 (split conj x)" using lp by (simp add: Let_def t s lt_nb ) from evaldjf_bound0[OF th] show ?thesis by (simp add: msubstlt_def) @@ -2202,23 +2202,23 @@ definition "msubstle c t d s a r = evaldjf (split conj) - [(let cd = c *\<^sub>p d in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul (2\<^sub>p *\<^sub>p cd) r)))), - (let cd = c *\<^sub>p d in (lt (CP cd), Le (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul (2\<^sub>p *\<^sub>p cd) r)))), - (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Le (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul (2\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))), - (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul (2\<^sub>p *\<^sub>p d) r))), + [(let cd = c *\<^sub>p d in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (let cd = c *\<^sub>p d in (lt (CP cd), Le (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Le (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), (conj (Eq (CP c)) (Eq (CP d)) , Le r)]" lemma msubstle_nb: assumes lp: "islin (Le (CNP 0 a r))" and t: "tmbound0 t" and s: "tmbound0 s" shows "bound0 (msubstle c t d s a r)" proof- - have th: "\x\ set [(let cd = c *\<^sub>p d in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul (2\<^sub>p *\<^sub>p cd) r)))), - (let cd = c *\<^sub>p d in (lt (CP cd), Le (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul (2\<^sub>p *\<^sub>p cd) r)))), - (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Le (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul (2\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))), - (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul (2\<^sub>p *\<^sub>p d) r))), + have th: "\x\ set [(let cd = c *\<^sub>p d in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (let cd = c *\<^sub>p d in (lt (CP cd), Le (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Le (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (split conj x)" using lp by (simp add: Let_def t s lt_nb ) from evaldjf_bound0[OF th] show ?thesis by (simp add: msubstle_def) diff -r cbba16084784 -r fe4d4bb9f4c2 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Nov 29 10:56:59 2012 +0100 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Nov 29 14:05:53 2012 +0100 @@ -16,7 +16,7 @@ | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \ C (0\<^sub>N)" -abbreviation poly_p :: "int \ poly" ("_\<^sub>p") where "i\<^sub>p \ C (i\<^sub>N)" +abbreviation poly_p :: "int \ poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \ C (i)\<^sub>N" subsection{* Boundedness, substitution and all that *} primrec polysize:: "poly \ nat" where @@ -153,7 +153,7 @@ fun polypow :: "nat \ poly \ poly" where - "polypow 0 = (\p. 1\<^sub>p)" + "polypow 0 = (\p. (1)\<^sub>p)" | "polypow n = (\p. let q = polypow (n div 2) p ; d = polymul q q in if even n then d else polymul p d)" @@ -162,7 +162,7 @@ function polynate :: "poly \ poly" where - "polynate (Bound n) = CN 0\<^sub>p n 1\<^sub>p" + "polynate (Bound n) = CN 0\<^sub>p n (1)\<^sub>p" | "polynate (Add p q) = (polynate p +\<^sub>p polynate q)" | "polynate (Sub p q) = (polynate p -\<^sub>p polynate q)" | "polynate (Mul p q) = (polynate p *\<^sub>p polynate q)" @@ -689,7 +689,7 @@ using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def) lemma funpow_shift1_1: - "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)" + "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)" by (simp add: funpow_shift1) lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)" @@ -994,7 +994,7 @@ using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp -lemma one_normh: "isnpolyh 1\<^sub>p n" by simp +lemma one_normh: "isnpolyh (1)\<^sub>p n" by simp lemma polyadd_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p" @@ -1003,7 +1003,7 @@ lemma polymul_1[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p" + and np: "isnpolyh p n0" shows "p *\<^sub>p (1)\<^sub>p = p" and "(1)\<^sub>p *\<^sub>p p = p" using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all lemma polymul_0[simp]: @@ -1262,14 +1262,14 @@ \ (\nr. isnpolyh r nr) \ ?qths" let ?b = "head s" let ?p' = "funpow (degree s - n) shift1 p" - let ?xdn = "funpow (degree s - n) shift1 1\<^sub>p" + let ?xdn = "funpow (degree s - n) shift1 (1)\<^sub>p" let ?akk' = "a ^\<^sub>p (k' - k)" note ns = `isnpolyh s n1` from np have np0: "isnpolyh p 0" using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by simp 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 have headp': "head ?p' = head p" using funpow_shift1_head[OF np pnz] by simp - from funpow_shift1_isnpoly[where p="1\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def) + from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def) from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap have nakk':"isnpolyh ?akk' 0" by blast {assume sz: "s = 0\<^sub>p" @@ -1312,19 +1312,19 @@ Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" by (simp add: field_simps) hence " \(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = - Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p) + Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) + Ipoly bs p * Ipoly bs q + Ipoly bs r" by (auto simp only: funpow_shift1_1) hence "\(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = - Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p) + Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) + Ipoly bs q) + Ipoly bs r" by (simp add: field_simps) hence "\(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = - 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 + 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 with isnpolyh_unique[OF nakks' nqr'] have "a ^\<^sub>p (k' - k) *\<^sub>p s = - 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 + 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 hence ?qths using nq' - apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q" in exI) + apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q" in exI) apply (rule_tac x="0" in exI) by simp with kk' nr dr have "k \ k' \ (degree r = 0 \ degree r < degree p) \ (\nr. isnpolyh r nr) \ ?qths" by blast } hence ?ths by blast } diff -r cbba16084784 -r fe4d4bb9f4c2 src/HOL/Library/Abstract_Rat.thy --- a/src/HOL/Library/Abstract_Rat.thy Thu Nov 29 10:56:59 2012 +0100 +++ b/src/HOL/Library/Abstract_Rat.thy Thu Nov 29 14:05:53 2012 +0100 @@ -13,8 +13,8 @@ abbreviation Num0_syn :: Num ("0\<^sub>N") where "0\<^sub>N \ (0, 0)" -abbreviation Numi_syn :: "int \ Num" ("_\<^sub>N") - where "i\<^sub>N \ (i, 1)" +abbreviation Numi_syn :: "int \ Num" ("'((_)')\<^sub>N") + where "(i)\<^sub>N \ (i, 1)" definition isnormNum :: "Num \ bool" where "isnormNum = (\(a,b). (if a = 0 then b = 0 else b > 0 \ gcd a b = 1))" @@ -125,7 +125,7 @@ (cases "fst x = 0", auto simp add: gcd_commute_int) lemma isnormNum_int[simp]: - "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \ 0 \ isnormNum (i\<^sub>N)" + "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \ 0 \ isnormNum (i)\<^sub>N" by (simp_all add: isnormNum_def) @@ -151,7 +151,7 @@ definition "INum = (\(a,b). of_int a / of_int b)" -lemma INum_int [simp]: "INum (i\<^sub>N) = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)" +lemma INum_int [simp]: "INum (i)\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)" by (simp_all add: INum_def) lemma isnormNum_unique[simp]: @@ -512,8 +512,8 @@ by (simp add: Nneg_def split_def) lemma Nmul1[simp]: - "isnormNum c \ 1\<^sub>N *\<^sub>N c = c" - "isnormNum c \ c *\<^sub>N (1\<^sub>N) = c" + "isnormNum c \ (1)\<^sub>N *\<^sub>N c = c" + "isnormNum c \ c *\<^sub>N (1)\<^sub>N = c" apply (simp_all add: Nmul_def Let_def split_def isnormNum_def) apply (cases "fst c = 0", simp_all, cases c, simp_all)+ done