more robust syntax that survives collapse of \<^isub> and \<^sub>;
authorwenzelm
Thu Nov 29 14:05:53 2012 +0100 (2012-11-29)
changeset 50282fe4d4bb9f4c2
parent 50281 cbba16084784
child 50284 cb4bdcbfdb8d
more robust syntax that survives collapse of \<^isub> and \<^sub>;
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Library/Abstract_Rat.thy
     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