1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Nov 29 10:56:59 2012 +0100
1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Nov 29 14:05:53 2012 +0100
1.3 @@ -297,7 +297,7 @@
1.4
1.5 fun simptm:: "tm \<Rightarrow> tm" where
1.6 "simptm (CP j) = CP (polynate j)"
1.7 -| "simptm (Bound n) = CNP n 1\<^sub>p (CP 0\<^sub>p)"
1.8 +| "simptm (Bound n) = CNP n (1)\<^sub>p (CP 0\<^sub>p)"
1.9 | "simptm (Neg t) = tmneg (simptm t)"
1.10 | "simptm (Add t s) = tmadd (simptm t,simptm s)"
1.11 | "simptm (Sub t s) = tmsub (simptm t) (simptm s)"
1.12 @@ -333,7 +333,7 @@
1.13 declare let_cong[fundef_cong del]
1.14
1.15 fun split0 :: "tm \<Rightarrow> (poly \<times> tm)" where
1.16 - "split0 (Bound 0) = (1\<^sub>p, CP 0\<^sub>p)"
1.17 + "split0 (Bound 0) = ((1)\<^sub>p, CP 0\<^sub>p)"
1.18 | "split0 (CNP 0 c t) = (let (c',t') = split0 t in (c +\<^sub>p c',t'))"
1.19 | "split0 (Neg t) = (let (c,t') = split0 t in (~\<^sub>p c,Neg t'))"
1.20 | "split0 (CNP n c t) = (let (c',t') = split0 t in (c',CNP n c t'))"
1.21 @@ -1892,17 +1892,17 @@
1.22 section{* First implementation : Naive by encoding all case splits locally *}
1.23 definition "msubsteq c t d s a r =
1.24 evaldjf (split conj)
1.25 - [(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)))),
1.26 - (conj (Eq (CP c)) (NEq (CP d)) , Eq (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))),
1.27 - (conj (NEq (CP c)) (Eq (CP d)) , Eq (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))),
1.28 + [(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)))),
1.29 + (conj (Eq (CP c)) (NEq (CP d)) , Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
1.30 + (conj (NEq (CP c)) (Eq (CP d)) , Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
1.31 (conj (Eq (CP c)) (Eq (CP d)) , Eq r)]"
1.32
1.33 lemma msubsteq_nb: assumes lp: "islin (Eq (CNP 0 a r))" and t: "tmbound0 t" and s: "tmbound0 s"
1.34 shows "bound0 (msubsteq c t d s a r)"
1.35 proof-
1.36 - have th: "\<forall>x\<in> 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)))),
1.37 - (conj (Eq (CP c)) (NEq (CP d)) , Eq (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))),
1.38 - (conj (NEq (CP c)) (Eq (CP d)) , Eq (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))),
1.39 + have th: "\<forall>x\<in> 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)))),
1.40 + (conj (Eq (CP c)) (NEq (CP d)) , Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
1.41 + (conj (NEq (CP c)) (Eq (CP d)) , Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
1.42 (conj (Eq (CP c)) (Eq (CP d)) , Eq r)]. bound0 (split conj x)"
1.43 using lp by (simp add: Let_def t s )
1.44 from evaldjf_bound0[OF th] show ?thesis by (simp add: msubsteq_def)
1.45 @@ -1974,17 +1974,17 @@
1.46
1.47 definition "msubstneq c t d s a r =
1.48 evaldjf (split conj)
1.49 - [(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)))),
1.50 - (conj (Eq (CP c)) (NEq (CP d)) , NEq (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))),
1.51 - (conj (NEq (CP c)) (Eq (CP d)) , NEq (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))),
1.52 + [(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)))),
1.53 + (conj (Eq (CP c)) (NEq (CP d)) , NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
1.54 + (conj (NEq (CP c)) (Eq (CP d)) , NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
1.55 (conj (Eq (CP c)) (Eq (CP d)) , NEq r)]"
1.56
1.57 lemma msubstneq_nb: assumes lp: "islin (NEq (CNP 0 a r))" and t: "tmbound0 t" and s: "tmbound0 s"
1.58 shows "bound0 (msubstneq c t d s a r)"
1.59 proof-
1.60 - have th: "\<forall>x\<in> 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)))),
1.61 - (conj (Eq (CP c)) (NEq (CP d)) , NEq (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))),
1.62 - (conj (NEq (CP c)) (Eq (CP d)) , NEq (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))),
1.63 + have th: "\<forall>x\<in> 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)))),
1.64 + (conj (Eq (CP c)) (NEq (CP d)) , NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
1.65 + (conj (NEq (CP c)) (Eq (CP d)) , NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
1.66 (conj (Eq (CP c)) (Eq (CP d)) , NEq r)]. bound0 (split conj x)"
1.67 using lp by (simp add: Let_def t s )
1.68 from evaldjf_bound0[OF th] show ?thesis by (simp add: msubstneq_def)
1.69 @@ -2055,23 +2055,23 @@
1.70
1.71 definition "msubstlt c t d s a r =
1.72 evaldjf (split conj)
1.73 - [(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)))),
1.74 - (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)))),
1.75 - (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Lt (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))),
1.76 - (conj (lt (CP c)) (Eq (CP d)) , Lt (Sub (Mul a t) (Mul (2\<^sub>p *\<^sub>p c) r))),
1.77 - (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Lt (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))),
1.78 - (conj (lt (CP d)) (Eq (CP c)) , Lt (Sub (Mul a s) (Mul (2\<^sub>p *\<^sub>p d) r))),
1.79 + [(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)))),
1.80 + (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)))),
1.81 + (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Lt (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
1.82 + (conj (lt (CP c)) (Eq (CP d)) , Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
1.83 + (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
1.84 + (conj (lt (CP d)) (Eq (CP c)) , Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
1.85 (conj (Eq (CP c)) (Eq (CP d)) , Lt r)]"
1.86
1.87 lemma msubstlt_nb: assumes lp: "islin (Lt (CNP 0 a r))" and t: "tmbound0 t" and s: "tmbound0 s"
1.88 shows "bound0 (msubstlt c t d s a r)"
1.89 proof-
1.90 - have th: "\<forall>x\<in> 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)))),
1.91 - (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)))),
1.92 - (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Lt (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))),
1.93 - (conj (lt (CP c)) (Eq (CP d)) , Lt (Sub (Mul a t) (Mul (2\<^sub>p *\<^sub>p c) r))),
1.94 - (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Lt (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))),
1.95 - (conj (lt (CP d)) (Eq (CP c)) , Lt (Sub (Mul a s) (Mul (2\<^sub>p *\<^sub>p d) r))),
1.96 + have th: "\<forall>x\<in> 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)))),
1.97 + (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)))),
1.98 + (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Lt (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
1.99 + (conj (lt (CP c)) (Eq (CP d)) , Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
1.100 + (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
1.101 + (conj (lt (CP d)) (Eq (CP c)) , Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
1.102 (conj (Eq (CP c)) (Eq (CP d)) , Lt r)]. bound0 (split conj x)"
1.103 using lp by (simp add: Let_def t s lt_nb )
1.104 from evaldjf_bound0[OF th] show ?thesis by (simp add: msubstlt_def)
1.105 @@ -2202,23 +2202,23 @@
1.106
1.107 definition "msubstle c t d s a r =
1.108 evaldjf (split conj)
1.109 - [(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)))),
1.110 - (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)))),
1.111 - (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Le (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))),
1.112 - (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul (2\<^sub>p *\<^sub>p c) r))),
1.113 - (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))),
1.114 - (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul (2\<^sub>p *\<^sub>p d) r))),
1.115 + [(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)))),
1.116 + (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)))),
1.117 + (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Le (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
1.118 + (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
1.119 + (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
1.120 + (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
1.121 (conj (Eq (CP c)) (Eq (CP d)) , Le r)]"
1.122
1.123 lemma msubstle_nb: assumes lp: "islin (Le (CNP 0 a r))" and t: "tmbound0 t" and s: "tmbound0 s"
1.124 shows "bound0 (msubstle c t d s a r)"
1.125 proof-
1.126 - have th: "\<forall>x\<in> 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)))),
1.127 - (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)))),
1.128 - (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Le (Add (Mul (~\<^sub>p a) t) (Mul (2\<^sub>p *\<^sub>p c) r))),
1.129 - (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul (2\<^sub>p *\<^sub>p c) r))),
1.130 - (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul (2\<^sub>p *\<^sub>p d) r))),
1.131 - (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul (2\<^sub>p *\<^sub>p d) r))),
1.132 + have th: "\<forall>x\<in> 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)))),
1.133 + (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)))),
1.134 + (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Le (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
1.135 + (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))),
1.136 + (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
1.137 + (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))),
1.138 (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (split conj x)"
1.139 using lp by (simp add: Let_def t s lt_nb )
1.140 from evaldjf_bound0[OF th] show ?thesis by (simp add: msubstle_def)
2.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Nov 29 10:56:59 2012 +0100
2.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Nov 29 14:05:53 2012 +0100
2.3 @@ -16,7 +16,7 @@
2.4 | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
2.5
2.6 abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
2.7 -abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)"
2.8 +abbreviation poly_p :: "int \<Rightarrow> poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \<equiv> C (i)\<^sub>N"
2.9
2.10 subsection{* Boundedness, substitution and all that *}
2.11 primrec polysize:: "poly \<Rightarrow> nat" where
2.12 @@ -153,7 +153,7 @@
2.13
2.14 fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
2.15 where
2.16 - "polypow 0 = (\<lambda>p. 1\<^sub>p)"
2.17 + "polypow 0 = (\<lambda>p. (1)\<^sub>p)"
2.18 | "polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul q q in
2.19 if even n then d else polymul p d)"
2.20
2.21 @@ -162,7 +162,7 @@
2.22
2.23 function polynate :: "poly \<Rightarrow> poly"
2.24 where
2.25 - "polynate (Bound n) = CN 0\<^sub>p n 1\<^sub>p"
2.26 + "polynate (Bound n) = CN 0\<^sub>p n (1)\<^sub>p"
2.27 | "polynate (Add p q) = (polynate p +\<^sub>p polynate q)"
2.28 | "polynate (Sub p q) = (polynate p -\<^sub>p polynate q)"
2.29 | "polynate (Mul p q) = (polynate p *\<^sub>p polynate q)"
2.30 @@ -689,7 +689,7 @@
2.31 using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
2.32
2.33 lemma funpow_shift1_1:
2.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)"
2.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)"
2.36 by (simp add: funpow_shift1)
2.37
2.38 lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
2.39 @@ -994,7 +994,7 @@
2.40 using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
2.41
2.42 lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
2.43 -lemma one_normh: "isnpolyh 1\<^sub>p n" by simp
2.44 +lemma one_normh: "isnpolyh (1)\<^sub>p n" by simp
2.45 lemma polyadd_0[simp]:
2.46 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
2.47 and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
2.48 @@ -1003,7 +1003,7 @@
2.49
2.50 lemma polymul_1[simp]:
2.51 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
2.52 - and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
2.53 + and np: "isnpolyh p n0" shows "p *\<^sub>p (1)\<^sub>p = p" and "(1)\<^sub>p *\<^sub>p p = p"
2.54 using isnpolyh_unique[OF polymul_normh[OF np one_normh] np]
2.55 isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
2.56 lemma polymul_0[simp]:
2.57 @@ -1262,14 +1262,14 @@
2.58 \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
2.59 let ?b = "head s"
2.60 let ?p' = "funpow (degree s - n) shift1 p"
2.61 - let ?xdn = "funpow (degree s - n) shift1 1\<^sub>p"
2.62 + let ?xdn = "funpow (degree s - n) shift1 (1)\<^sub>p"
2.63 let ?akk' = "a ^\<^sub>p (k' - k)"
2.64 note ns = `isnpolyh s n1`
2.65 from np have np0: "isnpolyh p 0"
2.66 using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by simp
2.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
2.68 have headp': "head ?p' = head p" using funpow_shift1_head[OF np pnz] by simp
2.69 - from funpow_shift1_isnpoly[where p="1\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def)
2.70 + from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def)
2.71 from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap
2.72 have nakk':"isnpolyh ?akk' 0" by blast
2.73 {assume sz: "s = 0\<^sub>p"
2.74 @@ -1312,19 +1312,19 @@
2.75 Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r"
2.76 by (simp add: field_simps)
2.77 hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
2.78 - Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p)
2.79 + Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p)
2.80 + Ipoly bs p * Ipoly bs q + Ipoly bs r"
2.81 by (auto simp only: funpow_shift1_1)
2.82 hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
2.83 - Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p)
2.84 + Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p)
2.85 + Ipoly bs q) + Ipoly bs r" by (simp add: field_simps)
2.86 hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) =
2.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
2.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
2.89 with isnpolyh_unique[OF nakks' nqr']
2.90 have "a ^\<^sub>p (k' - k) *\<^sub>p s =
2.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
2.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
2.93 hence ?qths using nq'
2.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)
2.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)
2.96 apply (rule_tac x="0" in exI) by simp
2.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"
2.98 by blast } hence ?ths by blast }
3.1 --- a/src/HOL/Library/Abstract_Rat.thy Thu Nov 29 10:56:59 2012 +0100
3.2 +++ b/src/HOL/Library/Abstract_Rat.thy Thu Nov 29 14:05:53 2012 +0100
3.3 @@ -13,8 +13,8 @@
3.4 abbreviation Num0_syn :: Num ("0\<^sub>N")
3.5 where "0\<^sub>N \<equiv> (0, 0)"
3.6
3.7 -abbreviation Numi_syn :: "int \<Rightarrow> Num" ("_\<^sub>N")
3.8 - where "i\<^sub>N \<equiv> (i, 1)"
3.9 +abbreviation Numi_syn :: "int \<Rightarrow> Num" ("'((_)')\<^sub>N")
3.10 + where "(i)\<^sub>N \<equiv> (i, 1)"
3.11
3.12 definition isnormNum :: "Num \<Rightarrow> bool" where
3.13 "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> gcd a b = 1))"
3.14 @@ -125,7 +125,7 @@
3.15 (cases "fst x = 0", auto simp add: gcd_commute_int)
3.16
3.17 lemma isnormNum_int[simp]:
3.18 - "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i\<^sub>N)"
3.19 + "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i)\<^sub>N"
3.20 by (simp_all add: isnormNum_def)
3.21
3.22
3.23 @@ -151,7 +151,7 @@
3.24
3.25 definition "INum = (\<lambda>(a,b). of_int a / of_int b)"
3.26
3.27 -lemma INum_int [simp]: "INum (i\<^sub>N) = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
3.28 +lemma INum_int [simp]: "INum (i)\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
3.29 by (simp_all add: INum_def)
3.30
3.31 lemma isnormNum_unique[simp]:
3.32 @@ -512,8 +512,8 @@
3.33 by (simp add: Nneg_def split_def)
3.34
3.35 lemma Nmul1[simp]:
3.36 - "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c"
3.37 - "isnormNum c \<Longrightarrow> c *\<^sub>N (1\<^sub>N) = c"
3.38 + "isnormNum c \<Longrightarrow> (1)\<^sub>N *\<^sub>N c = c"
3.39 + "isnormNum c \<Longrightarrow> c *\<^sub>N (1)\<^sub>N = c"
3.40 apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
3.41 apply (cases "fst c = 0", simp_all, cases c, simp_all)+
3.42 done