--- 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
------------------
--- 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 \<Rightarrow> 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 \<Rightarrow> (poly \<times> 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: "\<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)))),
- (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: "\<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)))),
+ (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: "\<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)))),
- (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: "\<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)))),
+ (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: "\<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)))),
- (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: "\<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)))),
+ (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: "\<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)))),
- (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: "\<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)))),
+ (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)
--- 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 \<equiv> C (0\<^sub>N)"
-abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)"
+abbreviation poly_p :: "int \<Rightarrow> poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \<equiv> C (i)\<^sub>N"
subsection{* Boundedness, substitution and all that *}
primrec polysize:: "poly \<Rightarrow> nat" where
@@ -153,7 +153,7 @@
fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
where
- "polypow 0 = (\<lambda>p. 1\<^sub>p)"
+ "polypow 0 = (\<lambda>p. (1)\<^sub>p)"
| "polypow n = (\<lambda>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 \<Rightarrow> 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 @@
\<and> (\<exists>nr. isnpolyh r nr) \<and> ?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 " \<forall>(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 "\<forall>(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 "\<forall>(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 \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
by blast } hence ?ths by blast }
--- 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 \<equiv> (0, 0)"
-abbreviation Numi_syn :: "int \<Rightarrow> Num" ("_\<^sub>N")
- where "i\<^sub>N \<equiv> (i, 1)"
+abbreviation Numi_syn :: "int \<Rightarrow> Num" ("'((_)')\<^sub>N")
+ where "(i)\<^sub>N \<equiv> (i, 1)"
definition isnormNum :: "Num \<Rightarrow> bool" where
"isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> 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 \<noteq> 0 \<Longrightarrow> isnormNum (i\<^sub>N)"
+ "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i)\<^sub>N"
by (simp_all add: isnormNum_def)
@@ -151,7 +151,7 @@
definition "INum = (\<lambda>(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 \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c"
- "isnormNum c \<Longrightarrow> c *\<^sub>N (1\<^sub>N) = c"
+ "isnormNum c \<Longrightarrow> (1)\<^sub>N *\<^sub>N c = c"
+ "isnormNum c \<Longrightarrow> 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
--- 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;
--- 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;
--- 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),
--- 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")
--- 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