# HG changeset patch # User wenzelm # Date 1354195769 -3600 # Node ID cb4bdcbfdb8d557475c44a76c9339ffee405fcac # Parent e79a8341dd6b7ca017633c6cf27d4b90b06c4f4c# Parent fe4d4bb9f4c2547f0a57a3348b5b13e11749eab1 merged diff -r e79a8341dd6b -r cb4bdcbfdb8d README_REPOSITORY --- a/README_REPOSITORY Thu Nov 29 09:59:20 2012 +0100 +++ b/README_REPOSITORY Thu Nov 29 14:29:29 2012 +0100 @@ -22,6 +22,12 @@ ./isabelle/bin/isabelle jedit +4. For later update replace "hg clone ..." above by: + + cd isabelle + + hg pull -u + Introduction ------------ @@ -189,11 +195,18 @@ * Start publishing again by pull or fetch, which normally produces local merges. - * Test the merged result as usual and push back in real time. + * Test the merged result, e.g. like this: + + isabelle build -a + + * Push back in real time. Piling private changes and public merges longer than 0.5-2 hours is apt to produce some mess when pushing eventually! +The pull-test-push cycle should not be repeated too fast, to avoid +delaying others from doing the same concurrently. + Content discipline ------------------ diff -r e79a8341dd6b -r cb4bdcbfdb8d src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Nov 29 09:59:20 2012 +0100 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Nov 29 14:29:29 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 e79a8341dd6b -r cb4bdcbfdb8d src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Nov 29 09:59:20 2012 +0100 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Nov 29 14:29:29 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 e79a8341dd6b -r cb4bdcbfdb8d src/HOL/Library/Abstract_Rat.thy --- a/src/HOL/Library/Abstract_Rat.thy Thu Nov 29 09:59:20 2012 +0100 +++ b/src/HOL/Library/Abstract_Rat.thy Thu Nov 29 14:29:29 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 diff -r e79a8341dd6b -r cb4bdcbfdb8d src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Thu Nov 29 09:59:20 2012 +0100 +++ b/src/Pure/Concurrent/future.ML Thu Nov 29 14:29:29 2012 +0100 @@ -51,6 +51,7 @@ val task_of: 'a future -> task val peek: 'a future -> 'a Exn.result option val is_finished: 'a future -> bool + val ML_statistics: bool Unsynchronized.ref val interruptible_task: ('a -> 'b) -> 'a -> 'b val cancel_group: group -> unit val cancel: 'a future -> unit @@ -169,6 +170,10 @@ val max_active = Unsynchronized.ref 0; val worker_trend = Unsynchronized.ref 0; +val status_ticks = Unsynchronized.ref 0; +val last_round = Unsynchronized.ref Time.zeroTime; +val next_round = seconds 0.05; + datatype worker_state = Working | Waiting | Sleeping; val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list); @@ -176,6 +181,32 @@ fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0; + +(* status *) + +val ML_statistics = Unsynchronized.ref false; + +fun report_status () = (*requires SYNCHRONIZED*) + if ! ML_statistics then + let + val {ready, pending, running, passive} = Task_Queue.status (! queue); + val total = length (! workers); + val active = count_workers Working; + val waiting = count_workers Waiting; + val stats = + [("now", signed_string_of_real (Time.toReal (Time.now ()))), + ("tasks_ready", Markup.print_int ready), + ("tasks_pending", Markup.print_int pending), + ("tasks_running", Markup.print_int running), + ("tasks_passive", Markup.print_int passive), + ("workers_total", Markup.print_int total), + ("workers_active", Markup.print_int active), + ("workers_waiting", Markup.print_int waiting)] @ + ML_Statistics.get (); + in Output.protocol_message (Markup.ML_statistics @ stats) "" end + else (); + + (* cancellation primitives *) fun cancel_now group = (*requires SYNCHRONIZED*) @@ -271,18 +302,6 @@ (* scheduler *) -fun ML_statistics () = - if ! ML_Statistics.enabled then - (case ML_Statistics.get () of - [] => () - | stats => Output.protocol_message (Markup.ML_statistics @ stats) "") - else (); - -val status_ticks = Unsynchronized.ref 0; - -val last_round = Unsynchronized.ref Time.zeroTime; -val next_round = seconds 0.05; - fun scheduler_next () = (*requires SYNCHRONIZED*) let val now = Time.now (); @@ -290,30 +309,12 @@ val _ = if tick then last_round := now else (); - (* queue and worker status *) + (* runtime status *) val _ = if tick then Unsynchronized.change status_ticks (fn i => (i + 1) mod 10) else (); val _ = - if tick andalso ! status_ticks = 0 then - (ML_statistics (); - Multithreading.tracing 1 (fn () => - let - val {ready, pending, running, passive} = Task_Queue.status (! queue); - val total = length (! workers); - val active = count_workers Working; - val waiting = count_workers Waiting; - in - "SCHEDULE " ^ Time.toString now ^ ": " ^ - string_of_int ready ^ " ready, " ^ - string_of_int pending ^ " pending, " ^ - string_of_int running ^ " running, " ^ - string_of_int passive ^ " passive; " ^ - string_of_int total ^ " workers, " ^ - string_of_int active ^ " active, " ^ - string_of_int waiting ^ " waiting " - end)) - else (); + if tick andalso ! status_ticks = 0 then report_status () else (); val _ = if forall (Thread.isActive o #1) (! workers) then () @@ -400,7 +401,7 @@ Multithreading.with_attributes (Multithreading.sync_interrupts Multithreading.public_interrupts) (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ())) - do (); last_round := Time.zeroTime; ML_statistics ()); + do (); last_round := Time.zeroTime; report_status ()); fun scheduler_active () = (*requires SYNCHRONIZED*) (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread); @@ -665,11 +666,6 @@ else (); -(* queue status *) - -fun queue_status () = Task_Queue.status (! queue); - - (*final declarations of this structure!*) val map = map_future; diff -r e79a8341dd6b -r cb4bdcbfdb8d src/Pure/ML/ml_statistics_dummy.ML --- a/src/Pure/ML/ml_statistics_dummy.ML Thu Nov 29 09:59:20 2012 +0100 +++ b/src/Pure/ML/ml_statistics_dummy.ML Thu Nov 29 14:29:29 2012 +0100 @@ -6,14 +6,12 @@ signature ML_STATISTICS = sig - val enabled: bool Unsynchronized.ref val get: unit -> Properties.T end; structure ML_Statistics: ML_STATISTICS = struct -val enabled = Unsynchronized.ref false; fun get () = []; end; diff -r e79a8341dd6b -r cb4bdcbfdb8d src/Pure/ML/ml_statistics_polyml-5.5.0.ML --- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML Thu Nov 29 09:59:20 2012 +0100 +++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML Thu Nov 29 14:29:29 2012 +0100 @@ -6,15 +6,12 @@ signature ML_STATISTICS = sig - val enabled: bool Unsynchronized.ref val get: unit -> Properties.T end; structure ML_Statistics: ML_STATISTICS = struct -val enabled = Unsynchronized.ref false; - fun get () = let val @@ -37,8 +34,7 @@ timeNonGCUser, userCounters = _} = PolyML.Statistics.getLocalStats () in - [("now", signed_string_of_real (Time.toReal (Time.now ()))), - ("full_GCs", Markup.print_int gcFullGCs), + [("full_GCs", Markup.print_int gcFullGCs), ("partial_GCs", Markup.print_int gcPartialGCs), ("size_allocation", Markup.print_int sizeAllocation), ("size_allocation_free", Markup.print_int sizeAllocationFree), diff -r e79a8341dd6b -r cb4bdcbfdb8d src/Pure/System/build.ML --- a/src/Pure/System/build.ML Thu Nov 29 09:59:20 2012 +0100 +++ b/src/Pure/System/build.ML Thu Nov 29 14:29:29 2012 +0100 @@ -27,7 +27,7 @@ (Options.int options "parallel_proofs_threshold") |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace") |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads") - |> Unsynchronized.setmp ML_Statistics.enabled (Options.bool options "ML_statistics") + |> Unsynchronized.setmp Future.ML_statistics (Options.bool options "ML_statistics") |> no_document options ? Present.no_document |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty") |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs") diff -r e79a8341dd6b -r cb4bdcbfdb8d src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Thu Nov 29 09:59:20 2012 +0100 +++ b/src/Pure/System/isabelle_process.ML Thu Nov 29 14:29:29 2012 +0100 @@ -217,7 +217,7 @@ protocol_command "Isabelle_Process.options" (fn [options_yxml] => let val options = Options.decode (YXML.parse_body options_yxml) in - ML_Statistics.enabled := Options.bool options "ML_statistics"; + Future.ML_statistics := Options.bool options "ML_statistics"; Multithreading.trace := Options.int options "threads_trace"; Multithreading.max_threads := Options.int options "threads"; if Multithreading.max_threads_value () < 2