--- a/NEWS Mon Jul 29 18:06:39 2013 +0200
+++ b/NEWS Mon Jul 29 20:51:05 2013 +0200
@@ -43,6 +43,12 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
+* Execution range of continuous document processing may be set to
+"all", "none", "visible". See also dockable window "Theories" or
+keyboard shortcuts "C-e BACK_SPACE" for "none", and "C-e SPACE" for
+"visible". These declarative options supersede the old-style action
+buttons "Cancel" and "Check".
+
* Strictly monotonic document update, without premature cancelation of
running transactions that are still needed: avoid reset/restart of
such command executions while editing.
--- a/etc/options Mon Jul 29 18:06:39 2013 +0200
+++ b/etc/options Mon Jul 29 20:51:05 2013 +0200
@@ -123,9 +123,12 @@
public option editor_chart_delay : real = 3.0
-- "delay for chart repainting"
-public option editor_execution_priority : int = -2
+option editor_execution_priority : int = -1
-- "execution priority of main document structure (e.g. 0, -1, -2)"
+option editor_execution_range : string = "visible"
+ -- "execution range of continuous document processing: all, none, visible"
+
section "Miscellaneous Tools"
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Mon Jul 29 18:06:39 2013 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Mon Jul 29 20:51:05 2013 +0200
@@ -10,7 +10,8 @@
text{* Application of polynomial as a real function. *}
-primrec poly :: "'a list => 'a => ('a::{comm_ring})" where
+primrec poly :: "'a list => 'a => ('a::{comm_ring})"
+where
poly_Nil: "poly [] x = 0"
| poly_Cons: "poly (h#t) x = h + x * poly t x"
@@ -18,42 +19,49 @@
subsection{*Arithmetic Operations on Polynomials*}
text{*addition*}
-primrec padd :: "['a list, 'a list] => ('a::comm_ring_1) list" (infixl "+++" 65) where
+primrec padd :: "['a list, 'a list] => ('a::comm_ring_1) list" (infixl "+++" 65)
+where
padd_Nil: "[] +++ l2 = l2"
| padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
else (h + hd l2)#(t +++ tl l2))"
text{*Multiplication by a constant*}
-primrec cmult :: "['a :: comm_ring_1, 'a list] => 'a list" (infixl "%*" 70) where
+primrec cmult :: "['a :: comm_ring_1, 'a list] => 'a list" (infixl "%*" 70)
+where
cmult_Nil: "c %* [] = []"
| cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
text{*Multiplication by a polynomial*}
-primrec pmult :: "['a list, 'a list] => ('a::comm_ring_1) list" (infixl "***" 70) where
+primrec pmult :: "['a list, 'a list] => ('a::comm_ring_1) list" (infixl "***" 70)
+where
pmult_Nil: "[] *** l2 = []"
| pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
else (h %* l2) +++ ((0) # (t *** l2)))"
text{*Repeated multiplication by a polynomial*}
-primrec mulexp :: "[nat, 'a list, 'a list] => ('a ::comm_ring_1) list" where
+primrec mulexp :: "[nat, 'a list, 'a list] => ('a ::comm_ring_1) list"
+where
mulexp_zero: "mulexp 0 p q = q"
| mulexp_Suc: "mulexp (Suc n) p q = p *** mulexp n p q"
text{*Exponential*}
-primrec pexp :: "['a list, nat] => ('a::comm_ring_1) list" (infixl "%^" 80) where
+primrec pexp :: "['a list, nat] => ('a::comm_ring_1) list" (infixl "%^" 80)
+where
pexp_0: "p %^ 0 = [1]"
| pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
text{*Quotient related value of dividing a polynomial by x + a*}
(* Useful for divisor properties in inductive proofs *)
-primrec pquot :: "['a list, 'a::field] => 'a list" where
- pquot_Nil: "pquot [] a= []"
-| pquot_Cons: "pquot (h#t) a = (if t = [] then [h]
- else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))"
+primrec pquot :: "['a list, 'a::field] => 'a list"
+where
+ pquot_Nil: "pquot [] a= []"
+| pquot_Cons:
+ "pquot (h#t) a = (if t = [] then [h] else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))"
text{*normalization of polynomials (remove extra 0 coeff)*}
-primrec pnormalize :: "('a::comm_ring_1) list => 'a list" where
+primrec pnormalize :: "('a::comm_ring_1) list => 'a list"
+where
pnormalize_Nil: "pnormalize [] = []"
| pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = [])
then (if (h = 0) then [] else [h])
@@ -63,24 +71,17 @@
definition "nonconstant p = (pnormal p \<and> (\<forall>x. p \<noteq> [x]))"
text{*Other definitions*}
-definition
- poly_minus :: "'a list => ('a :: comm_ring_1) list" ("-- _" [80] 80) where
- "-- p = (- 1) %* p"
+definition poly_minus :: "'a list => ('a :: comm_ring_1) list" ("-- _" [80] 80)
+ where "-- p = (- 1) %* p"
-definition
- divides :: "[('a::comm_ring_1) list, 'a list] => bool" (infixl "divides" 70) where
- "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
+definition divides :: "[('a::comm_ring_1) list, 'a list] => bool" (infixl "divides" 70)
+ where "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
-definition
- order :: "('a::comm_ring_1) => 'a list => nat" where
- --{*order of a polynomial*}
- "order a p = (SOME n. ([-a, 1] %^ n) divides p &
- ~ (([-a, 1] %^ (Suc n)) divides p))"
+definition order :: "('a::comm_ring_1) => 'a list => nat" --{*order of a polynomial*}
+ where "order a p = (SOME n. ([-a, 1] %^ n) divides p & ~ (([-a, 1] %^ (Suc n)) divides p))"
-definition
- degree :: "('a::comm_ring_1) list => nat" where
- --{*degree of a polynomial*}
- "degree p = length (pnormalize p) - 1"
+definition degree :: "('a::comm_ring_1) list => nat" --{*degree of a polynomial*}
+ where "degree p = length (pnormalize p) - 1"
definition
rsquarefree :: "('a::comm_ring_1) list => bool" where
@@ -88,263 +89,255 @@
"rsquarefree p = (poly p \<noteq> poly [] &
(\<forall>a. (order a p = 0) | (order a p = 1)))"
-lemma padd_Nil2: "p +++ [] = p"
-by (induct p) auto
-declare padd_Nil2 [simp]
+lemma padd_Nil2 [simp]: "p +++ [] = p"
+ by (induct p) auto
lemma padd_Cons_Cons: "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)"
-by auto
+ by auto
-lemma pminus_Nil: "-- [] = []"
-by (simp add: poly_minus_def)
-declare pminus_Nil [simp]
+lemma pminus_Nil [simp]: "-- [] = []"
+ by (simp add: poly_minus_def)
lemma pmult_singleton: "[h1] *** p1 = h1 %* p1"
-by simp
+ by simp
-lemma poly_ident_mult: "1 %* t = t"
-by (induct "t", auto)
-declare poly_ident_mult [simp]
+lemma poly_ident_mult [simp]: "1 %* t = t"
+ by (induct t) auto
-lemma poly_simple_add_Cons: "[a] +++ ((0)#t) = (a#t)"
-by simp
-declare poly_simple_add_Cons [simp]
+lemma poly_simple_add_Cons [simp]: "[a] +++ ((0)#t) = (a#t)"
+ by simp
text{*Handy general properties*}
lemma padd_commut: "b +++ a = a +++ b"
-apply (subgoal_tac "\<forall>a. b +++ a = a +++ b")
-apply (induct_tac [2] "b", auto)
-apply (rule padd_Cons [THEN ssubst])
-apply (case_tac "aa", auto)
-done
+ apply (subgoal_tac "\<forall>a. b +++ a = a +++ b")
+ apply (induct_tac [2] "b", auto)
+ apply (rule padd_Cons [THEN ssubst])
+ apply (case_tac "aa", auto)
+ done
lemma padd_assoc [rule_format]: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
-apply (induct "a", simp, clarify)
-apply (case_tac b, simp_all)
-done
+ apply (induct "a", simp, clarify)
+ apply (case_tac b, simp_all)
+ done
-lemma poly_cmult_distr [rule_format]:
- "\<forall>q. a %* ( p +++ q) = (a %* p +++ a %* q)"
-apply (induct "p", simp, clarify)
-apply (case_tac "q")
-apply (simp_all add: distrib_left)
-done
+lemma poly_cmult_distr [rule_format]: "\<forall>q. a %* ( p +++ q) = (a %* p +++ a %* q)"
+ apply (induct p)
+ apply simp
+ apply clarify
+ apply (case_tac q)
+ apply (simp_all add: distrib_left)
+ done
lemma pmult_by_x[simp]: "[0, 1] *** t = ((0)#t)"
-apply (induct "t", simp)
-by (auto simp add: mult_zero_left poly_ident_mult padd_commut)
+ apply (induct t)
+ apply simp
+ apply (auto simp add: padd_commut)
+ done
text{*properties of evaluation of polynomials.*}
lemma poly_add: "poly (p1 +++ p2) x = poly p1 x + poly p2 x"
-apply (subgoal_tac "\<forall>p2. poly (p1 +++ p2) x = poly (p1) x + poly (p2) x")
-apply (induct_tac [2] "p1", auto)
-apply (case_tac "p2")
-apply (auto simp add: distrib_left)
-done
+ apply (subgoal_tac "\<forall>p2. poly (p1 +++ p2) x = poly (p1) x + poly (p2) x")
+ apply (induct_tac [2] "p1", auto)
+ apply (case_tac "p2")
+ apply (auto simp add: distrib_left)
+ done
lemma poly_cmult: "poly (c %* p) x = c * poly p x"
-apply (induct "p")
-apply (case_tac [2] "x=0")
-apply (auto simp add: distrib_left mult_ac)
-done
+ apply (induct "p")
+ apply (case_tac [2] "x=0")
+ apply (auto simp add: distrib_left mult_ac)
+ done
lemma poly_minus: "poly (-- p) x = - (poly p x)"
-apply (simp add: poly_minus_def)
-apply (auto simp add: poly_cmult)
-done
+ apply (simp add: poly_minus_def)
+ apply (auto simp add: poly_cmult)
+ done
lemma poly_mult: "poly (p1 *** p2) x = poly p1 x * poly p2 x"
-apply (subgoal_tac "\<forall>p2. poly (p1 *** p2) x = poly p1 x * poly p2 x")
-apply (simp (no_asm_simp))
-apply (induct "p1")
-apply (auto simp add: poly_cmult)
-apply (case_tac p1)
-apply (auto simp add: poly_cmult poly_add distrib_right distrib_left mult_ac)
-done
+ apply (subgoal_tac "\<forall>p2. poly (p1 *** p2) x = poly p1 x * poly p2 x")
+ apply (simp (no_asm_simp))
+ apply (induct "p1")
+ apply (auto simp add: poly_cmult)
+ apply (case_tac p1)
+ apply (auto simp add: poly_cmult poly_add distrib_right distrib_left mult_ac)
+ done
lemma poly_exp: "poly (p %^ n) (x::'a::comm_ring_1) = (poly p x) ^ n"
-apply (induct "n")
-apply (auto simp add: poly_cmult poly_mult power_Suc)
-done
+ by (induct "n") (auto simp add: poly_cmult poly_mult)
text{*More Polynomial Evaluation Lemmas*}
-lemma poly_add_rzero: "poly (a +++ []) x = poly a x"
-by simp
-declare poly_add_rzero [simp]
+lemma poly_add_rzero [simp]: "poly (a +++ []) x = poly a x"
+ by simp
lemma poly_mult_assoc: "poly ((a *** b) *** c) x = poly (a *** (b *** c)) x"
by (simp add: poly_mult mult_assoc)
-lemma poly_mult_Nil2: "poly (p *** []) x = 0"
-by (induct "p", auto)
-declare poly_mult_Nil2 [simp]
+lemma poly_mult_Nil2 [simp]: "poly (p *** []) x = 0"
+ by (induct "p") auto
lemma poly_exp_add: "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d) x"
-apply (induct "n")
-apply (auto simp add: poly_mult mult_assoc)
-done
+ by (induct "n") (auto simp add: poly_mult mult_assoc)
subsection{*Key Property: if @{term "f(a) = 0"} then @{term "(x - a)"} divides
@{term "p(x)"} *}
lemma lemma_poly_linear_rem: "\<forall>h. \<exists>q r. h#t = [r] +++ [-a, 1] *** q"
-apply (induct "t", safe)
-apply (rule_tac x = "[]" in exI)
-apply (rule_tac x = h in exI, simp)
-apply (drule_tac x = aa in spec, safe)
-apply (rule_tac x = "r#q" in exI)
-apply (rule_tac x = "a*r + h" in exI)
-apply (case_tac "q", auto)
-done
+ apply (induct "t", safe)
+ apply (rule_tac x = "[]" in exI)
+ apply (rule_tac x = h in exI, simp)
+ apply (drule_tac x = aa in spec, safe)
+ apply (rule_tac x = "r#q" in exI)
+ apply (rule_tac x = "a*r + h" in exI)
+ apply (case_tac "q", auto)
+ done
lemma poly_linear_rem: "\<exists>q r. h#t = [r] +++ [-a, 1] *** q"
-by (cut_tac t = t and a = a in lemma_poly_linear_rem, auto)
+ using lemma_poly_linear_rem [where t = t and a = a] by auto
lemma poly_linear_divides: "(poly p a = 0) = ((p = []) | (\<exists>q. p = [-a, 1] *** q))"
-apply (auto simp add: poly_add poly_cmult distrib_left)
-apply (case_tac "p", simp)
-apply (cut_tac h = aa and t = list and a = a in poly_linear_rem, safe)
-apply (case_tac "q", auto)
-apply (drule_tac x = "[]" in spec, simp)
-apply (auto simp add: poly_add poly_cmult add_assoc)
-apply (drule_tac x = "aa#lista" in spec, auto)
-done
+ apply (auto simp add: poly_add poly_cmult distrib_left)
+ apply (case_tac "p", simp)
+ apply (cut_tac h = aa and t = list and a = a in poly_linear_rem, safe)
+ apply (case_tac "q", auto)
+ apply (drule_tac x = "[]" in spec, simp)
+ apply (auto simp add: poly_add poly_cmult add_assoc)
+ apply (drule_tac x = "aa#lista" in spec, auto)
+ done
-lemma lemma_poly_length_mult: "\<forall>h k a. length (k %* p +++ (h # (a %* p))) = Suc (length p)"
-by (induct "p", auto)
-declare lemma_poly_length_mult [simp]
+lemma lemma_poly_length_mult [simp]: "\<forall>h k a. length (k %* p +++ (h # (a %* p))) = Suc (length p)"
+ by (induct p) auto
-lemma lemma_poly_length_mult2: "\<forall>h k. length (k %* p +++ (h # p)) = Suc (length p)"
-by (induct "p", auto)
-declare lemma_poly_length_mult2 [simp]
+lemma lemma_poly_length_mult2 [simp]: "\<forall>h k. length (k %* p +++ (h # p)) = Suc (length p)"
+ by (induct p) auto
-lemma poly_length_mult: "length([-a,1] *** q) = Suc (length q)"
-by auto
-declare poly_length_mult [simp]
+lemma poly_length_mult [simp]: "length([-a,1] *** q) = Suc (length q)"
+ by auto
subsection{*Polynomial length*}
-lemma poly_cmult_length: "length (a %* p) = length p"
-by (induct "p", auto)
-declare poly_cmult_length [simp]
+lemma poly_cmult_length [simp]: "length (a %* p) = length p"
+ by (induct p) auto
lemma poly_add_length [rule_format]:
- "\<forall>p2. length (p1 +++ p2) =
- (if (length p1 < length p2) then length p2 else length p1)"
-apply (induct "p1", simp_all)
-apply arith
-done
+ "\<forall>p2. length (p1 +++ p2) = (if (length p1 < length p2) then length p2 else length p1)"
+ apply (induct p1)
+ apply simp_all
+ apply arith
+ done
-lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)"
-by (simp add: poly_cmult_length poly_add_length)
-declare poly_root_mult_length [simp]
+lemma poly_root_mult_length [simp]: "length([a,b] *** p) = Suc (length p)"
+ by simp
-lemma poly_mult_not_eq_poly_Nil: "(poly (p *** q) x \<noteq> poly [] x) =
- (poly p x \<noteq> poly [] x & poly q x \<noteq> poly [] (x::'a::idom))"
-apply (auto simp add: poly_mult)
-done
-declare poly_mult_not_eq_poly_Nil [simp]
+lemma poly_mult_not_eq_poly_Nil [simp]: "(poly (p *** q) x \<noteq> poly [] x) =
+ (poly p x \<noteq> poly [] x & poly q x \<noteq> poly [] (x::'a::idom))"
+ by (auto simp add: poly_mult)
lemma poly_mult_eq_zero_disj: "(poly (p *** q) (x::'a::idom) = 0) = (poly p x = 0 | poly q x = 0)"
-by (auto simp add: poly_mult)
+ by (auto simp add: poly_mult)
text{*Normalisation Properties*}
lemma poly_normalized_nil: "(pnormalize p = []) --> (poly p x = 0)"
-by (induct "p", auto)
+ by (induct p) auto
text{*A nontrivial polynomial of degree n has no more than n roots*}
lemma poly_roots_index_lemma0 [rule_format]:
"\<forall>p x. poly p x \<noteq> poly [] x & length p = n
--> (\<exists>i. \<forall>x. (poly p x = (0::'a::idom)) --> (\<exists>m. (m \<le> n & x = i m)))"
-apply (induct "n", safe)
-apply (rule ccontr)
-apply (subgoal_tac "\<exists>a. poly p a = 0", safe)
-apply (drule poly_linear_divides [THEN iffD1], safe)
-apply (drule_tac x = q in spec)
-apply (drule_tac x = x in spec)
-apply (simp del: poly_Nil pmult_Cons)
-apply (erule exE)
-apply (drule_tac x = "%m. if m = Suc n then a else i m" in spec, safe)
-apply (drule poly_mult_eq_zero_disj [THEN iffD1], safe)
-apply (drule_tac x = "Suc (length q)" in spec)
-apply (auto simp add: field_simps)
-apply (drule_tac x = xa in spec)
-apply (clarsimp simp add: field_simps)
-apply (drule_tac x = m in spec)
-apply (auto simp add:field_simps)
-done
+ apply (induct "n", safe)
+ apply (rule ccontr)
+ apply (subgoal_tac "\<exists>a. poly p a = 0", safe)
+ apply (drule poly_linear_divides [THEN iffD1], safe)
+ apply (drule_tac x = q in spec)
+ apply (drule_tac x = x in spec)
+ apply (simp del: poly_Nil pmult_Cons)
+ apply (erule exE)
+ apply (drule_tac x = "%m. if m = Suc n then a else i m" in spec, safe)
+ apply (drule poly_mult_eq_zero_disj [THEN iffD1], safe)
+ apply (drule_tac x = "Suc (length q)" in spec)
+ apply (auto simp add: field_simps)
+ apply (drule_tac x = xa in spec)
+ apply (clarsimp simp add: field_simps)
+ apply (drule_tac x = m in spec)
+ apply (auto simp add:field_simps)
+ done
lemmas poly_roots_index_lemma1 = conjI [THEN poly_roots_index_lemma0]
-lemma poly_roots_index_length0: "poly p (x::'a::idom) \<noteq> poly [] x ==>
- \<exists>i. \<forall>x. (poly p x = 0) --> (\<exists>n. n \<le> length p & x = i n)"
-by (blast intro: poly_roots_index_lemma1)
+lemma poly_roots_index_length0:
+ "poly p (x::'a::idom) \<noteq> poly [] x \<Longrightarrow>
+ \<exists>i. \<forall>x. (poly p x = 0) \<longrightarrow> (\<exists>n. n \<le> length p & x = i n)"
+ by (blast intro: poly_roots_index_lemma1)
-lemma poly_roots_finite_lemma: "poly p (x::'a::idom) \<noteq> poly [] x ==>
- \<exists>N i. \<forall>x. (poly p x = 0) --> (\<exists>n. (n::nat) < N & x = i n)"
-apply (drule poly_roots_index_length0, safe)
-apply (rule_tac x = "Suc (length p)" in exI)
-apply (rule_tac x = i in exI)
-apply (simp add: less_Suc_eq_le)
-done
+lemma poly_roots_finite_lemma:
+ "poly p (x::'a::idom) \<noteq> poly [] x \<Longrightarrow>
+ \<exists>N i. \<forall>x. (poly p x = 0) \<longrightarrow> (\<exists>n. (n::nat) < N & x = i n)"
+ apply (drule poly_roots_index_length0, safe)
+ apply (rule_tac x = "Suc (length p)" in exI)
+ apply (rule_tac x = i in exI)
+ apply (simp add: less_Suc_eq_le)
+ done
lemma real_finite_lemma:
assumes P: "\<forall>x. P x --> (\<exists>n. n < length j & x = j!n)"
shows "finite {(x::'a::idom). P x}"
-proof-
+proof -
let ?M = "{x. P x}"
let ?N = "set j"
have "?M \<subseteq> ?N" using P by auto
- thus ?thesis using finite_subset by auto
+ then show ?thesis using finite_subset by auto
qed
lemma poly_roots_index_lemma [rule_format]:
- "\<forall>p x. poly p x \<noteq> poly [] x & length p = n
- --> (\<exists>i. \<forall>x. (poly p x = (0::'a::{idom})) --> x \<in> set i)"
-apply (induct "n", safe)
-apply (rule ccontr)
-apply (subgoal_tac "\<exists>a. poly p a = 0", safe)
-apply (drule poly_linear_divides [THEN iffD1], safe)
-apply (drule_tac x = q in spec)
-apply (drule_tac x = x in spec)
-apply (auto simp del: poly_Nil pmult_Cons)
-apply (drule_tac x = "a#i" in spec)
-apply (auto simp only: poly_mult List.list.size)
-apply (drule_tac x = xa in spec)
-apply (clarsimp simp add: field_simps)
-done
+ "\<forall>p x. poly p x \<noteq> poly [] x & length p = n
+ \<longrightarrow> (\<exists>i. \<forall>x. (poly p x = (0::'a::{idom})) \<longrightarrow> x \<in> set i)"
+ apply (induct "n", safe)
+ apply (rule ccontr)
+ apply (subgoal_tac "\<exists>a. poly p a = 0", safe)
+ apply (drule poly_linear_divides [THEN iffD1], safe)
+ apply (drule_tac x = q in spec)
+ apply (drule_tac x = x in spec)
+ apply (auto simp del: poly_Nil pmult_Cons)
+ apply (drule_tac x = "a#i" in spec)
+ apply (auto simp only: poly_mult List.list.size)
+ apply (drule_tac x = xa in spec)
+ apply (clarsimp simp add: field_simps)
+ done
lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma]
-lemma poly_roots_index_length: "poly p (x::'a::idom) \<noteq> poly [] x ==>
- \<exists>i. \<forall>x. (poly p x = 0) --> x \<in> set i"
-by (blast intro: poly_roots_index_lemma2)
+lemma poly_roots_index_length:
+ "poly p (x::'a::idom) \<noteq> poly [] x \<Longrightarrow>
+ \<exists>i. \<forall>x. (poly p x = 0) --> x \<in> set i"
+ by (blast intro: poly_roots_index_lemma2)
-lemma poly_roots_finite_lemma': "poly p (x::'a::idom) \<noteq> poly [] x ==>
- \<exists>i. \<forall>x. (poly p x = 0) --> x \<in> set i"
-by (drule poly_roots_index_length, safe)
+lemma poly_roots_finite_lemma':
+ "poly p (x::'a::idom) \<noteq> poly [] x \<Longrightarrow>
+ \<exists>i. \<forall>x. (poly p x = 0) --> x \<in> set i"
+ apply (drule poly_roots_index_length)
+ apply auto
+ done
lemma UNIV_nat_infinite: "\<not> finite (UNIV :: nat set)"
unfolding finite_conv_nat_seg_image
-proof(auto simp add: set_eq_iff image_iff)
+proof (auto simp add: set_eq_iff image_iff)
fix n::nat and f:: "nat \<Rightarrow> nat"
let ?N = "{i. i < n}"
let ?fN = "f ` ?N"
let ?y = "Max ?fN + 1"
- from nat_seg_image_imp_finite[of "?fN" "f" n]
+ from nat_seg_image_imp_finite[of "?fN" "f" n]
have thfN: "finite ?fN" by simp
- {assume "n =0" hence "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by auto}
+ { assume "n =0" hence "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by auto }
moreover
- {assume nz: "n \<noteq> 0"
- hence thne: "?fN \<noteq> {}" by (auto simp add: neq0_conv)
+ { assume nz: "n \<noteq> 0"
+ hence thne: "?fN \<noteq> {}" by auto
have "\<forall>x\<in> ?fN. Max ?fN \<ge> x" using nz Max_ge_iff[OF thfN thne] by auto
hence "\<forall>x\<in> ?fN. ?y > x" by (auto simp add: less_Suc_eq_le)
hence "?y \<notin> ?fN" by auto
@@ -359,12 +352,11 @@
from finite_subset[OF th0 F] have th: "finite (of_nat ` UNIV :: 'a set)" .
have th': "inj_on (of_nat::nat \<Rightarrow> 'a) (UNIV)"
unfolding inj_on_def by auto
- from finite_imageD[OF th th'] UNIV_nat_infinite
+ from finite_imageD[OF th th'] UNIV_nat_infinite
show False by blast
qed
-lemma poly_roots_finite: "(poly p \<noteq> poly []) =
- finite {x. poly p x = (0::'a::{idom, ring_char_0})}"
+lemma poly_roots_finite: "(poly p \<noteq> poly []) = finite {x. poly p x = (0::'a::{idom, ring_char_0})}"
proof
assume H: "poly p \<noteq> poly []"
show "finite {x. poly p x = (0::'a)}"
@@ -374,75 +366,80 @@
apply (rule ccontr)
apply (clarify dest!: poly_roots_finite_lemma')
using finite_subset
- proof-
+ proof -
fix x i
- assume F: "\<not> finite {x. poly p x = (0\<Colon>'a)}"
+ assume F: "\<not> finite {x. poly p x = (0\<Colon>'a)}"
and P: "\<forall>x. poly p x = (0\<Colon>'a) \<longrightarrow> x \<in> set i"
let ?M= "{x. poly p x = (0\<Colon>'a)}"
from P have "?M \<subseteq> set i" by auto
with finite_subset F show False by auto
qed
next
- assume F: "finite {x. poly p x = (0\<Colon>'a)}"
- show "poly p \<noteq> poly []" using F UNIV_ring_char_0_infinte by auto
+ assume "finite {x. poly p x = (0\<Colon>'a)}"
+ then show "poly p \<noteq> poly []" using UNIV_ring_char_0_infinte by auto
qed
text{*Entirety and Cancellation for polynomials*}
-lemma poly_entire_lemma: "[| poly (p:: ('a::{idom,ring_char_0}) list) \<noteq> poly [] ; poly q \<noteq> poly [] |]
- ==> poly (p *** q) \<noteq> poly []"
-by (auto simp add: poly_roots_finite poly_mult Collect_disj_eq)
+lemma poly_entire_lemma:
+ "poly (p:: ('a::{idom,ring_char_0}) list) \<noteq> poly [] \<Longrightarrow> poly q \<noteq> poly [] \<Longrightarrow>
+ poly (p *** q) \<noteq> poly []"
+ by (auto simp add: poly_roots_finite poly_mult Collect_disj_eq)
-lemma poly_entire: "(poly (p *** q) = poly ([]::('a::{idom,ring_char_0}) list)) = ((poly p = poly []) | (poly q = poly []))"
-apply (auto intro: ext dest: fun_cong simp add: poly_entire_lemma poly_mult)
-apply (blast intro: ccontr dest: poly_entire_lemma poly_mult [THEN subst])
-done
+lemma poly_entire:
+ "(poly (p *** q) =
+ poly ([]::('a::{idom,ring_char_0}) list)) = ((poly p = poly []) | (poly q = poly []))"
+ apply (auto dest: fun_cong simp add: poly_entire_lemma poly_mult)
+ apply (blast intro: ccontr dest: poly_entire_lemma poly_mult [THEN subst])
+ done
-lemma poly_entire_neg: "(poly (p *** q) \<noteq> poly ([]::('a::{idom,ring_char_0}) list)) = ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))"
-by (simp add: poly_entire)
+lemma poly_entire_neg:
+ "(poly (p *** q) \<noteq> poly ([]::('a::{idom,ring_char_0}) list)) =
+ ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))"
+ by (simp add: poly_entire)
-lemma fun_eq: " (f = g) = (\<forall>x. f x = g x)"
-by (auto intro!: ext)
+lemma fun_eq: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
+ by auto
lemma poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)"
-by (auto simp add: field_simps poly_add poly_minus_def fun_eq poly_cmult)
+ by (auto simp add: field_simps poly_add poly_minus_def fun_eq poly_cmult)
lemma poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
-by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult distrib_left)
+ by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult distrib_left)
-lemma poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly ([]::('a::{idom, ring_char_0}) list) | poly q = poly r)"
-apply (rule_tac p1 = "p *** q" in poly_add_minus_zero_iff [THEN subst])
-apply (auto intro: ext simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff)
-done
+lemma poly_mult_left_cancel:
+ "(poly (p *** q) = poly (p *** r)) =
+ (poly p = poly ([]::('a::{idom, ring_char_0}) list) | poly q = poly r)"
+ apply (rule_tac p1 = "p *** q" in poly_add_minus_zero_iff [THEN subst])
+ apply (auto simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff)
+ done
-lemma poly_exp_eq_zero:
- "(poly (p %^ n) = poly ([]::('a::idom) list)) = (poly p = poly [] & n \<noteq> 0)"
-apply (simp only: fun_eq add: HOL.all_simps [symmetric])
-apply (rule arg_cong [where f = All])
-apply (rule ext)
-apply (induct_tac "n")
-apply (auto simp add: poly_mult)
-done
-declare poly_exp_eq_zero [simp]
+lemma poly_exp_eq_zero [simp]:
+ "(poly (p %^ n) = poly ([]::('a::idom) list)) = (poly p = poly [] & n \<noteq> 0)"
+ apply (simp only: fun_eq add: HOL.all_simps [symmetric])
+ apply (rule arg_cong [where f = All])
+ apply (rule ext)
+ apply (induct_tac "n")
+ apply (auto simp add: poly_mult)
+ done
-lemma poly_prime_eq_zero: "poly [a,(1::'a::comm_ring_1)] \<noteq> poly []"
-apply (simp add: fun_eq)
-apply (rule_tac x = "1 - a" in exI, simp)
-done
-declare poly_prime_eq_zero [simp]
+lemma poly_prime_eq_zero [simp]: "poly [a,(1::'a::comm_ring_1)] \<noteq> poly []"
+ apply (simp add: fun_eq)
+ apply (rule_tac x = "1 - a" in exI, simp)
+ done
-lemma poly_exp_prime_eq_zero: "(poly ([a, (1::'a::idom)] %^ n) \<noteq> poly [])"
-by auto
-declare poly_exp_prime_eq_zero [simp]
+lemma poly_exp_prime_eq_zero [simp]: "(poly ([a, (1::'a::idom)] %^ n) \<noteq> poly [])"
+ by auto
text{*A more constructive notion of polynomials being trivial*}
-lemma poly_zero_lemma': "poly (h # t) = poly [] ==> h = (0::'a::{idom,ring_char_0}) & poly t = poly []"
-apply(simp add: fun_eq)
-apply (case_tac "h = 0")
-apply (drule_tac [2] x = 0 in spec, auto)
-apply (case_tac "poly t = poly []", simp)
-proof-
+lemma poly_zero_lemma':
+ "poly (h # t) = poly [] \<Longrightarrow> h = (0::'a::{idom,ring_char_0}) & poly t = poly []"
+ apply (simp add: fun_eq)
+ apply (case_tac "h = 0")
+ apply (drule_tac [2] x = 0 in spec, auto)
+ apply (case_tac "poly t = poly []", simp)
+proof -
fix x
assume H: "\<forall>x. x = (0\<Colon>'a) \<or> poly t x = (0\<Colon>'a)" and pnz: "poly t \<noteq> poly []"
let ?S = "{x. poly t x = 0}"
@@ -451,325 +448,323 @@
from poly_roots_finite pnz have th': "finite ?S" by blast
from finite_subset[OF th th'] UNIV_ring_char_0_infinte[where ?'a = 'a]
show "poly t x = (0\<Colon>'a)" by simp
- qed
+qed
lemma poly_zero: "(poly p = poly []) = list_all (%c. c = (0::'a::{idom,ring_char_0})) p"
-apply (induct "p", simp)
-apply (rule iffI)
-apply (drule poly_zero_lemma', auto)
-done
-
+ apply (induct p)
+ apply simp
+ apply (rule iffI)
+ apply (drule poly_zero_lemma')
+ apply auto
+ done
text{*Basics of divisibility.*}
lemma poly_primes: "([a, (1::'a::idom)] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)"
-apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult distrib_right [symmetric])
-apply (drule_tac x = "-a" in spec)
-apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
-apply (rule_tac x = "qa *** q" in exI)
-apply (rule_tac [2] x = "p *** qa" in exI)
-apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
-done
+ apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult distrib_right [symmetric])
+ apply (drule_tac x = "-a" in spec)
+ apply (auto simp add: poly_linear_divides poly_add poly_cmult distrib_right [symmetric])
+ apply (rule_tac x = "qa *** q" in exI)
+ apply (rule_tac [2] x = "p *** qa" in exI)
+ apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
+ done
-lemma poly_divides_refl: "p divides p"
-apply (simp add: divides_def)
-apply (rule_tac x = "[1]" in exI)
-apply (auto simp add: poly_mult fun_eq)
-done
-declare poly_divides_refl [simp]
+lemma poly_divides_refl [simp]: "p divides p"
+ apply (simp add: divides_def)
+ apply (rule_tac x = "[1]" in exI)
+ apply (auto simp add: poly_mult fun_eq)
+ done
-lemma poly_divides_trans: "[| p divides q; q divides r |] ==> p divides r"
-apply (simp add: divides_def, safe)
-apply (rule_tac x = "qa *** qaa" in exI)
-apply (auto simp add: poly_mult fun_eq mult_assoc)
-done
+lemma poly_divides_trans: "p divides q \<Longrightarrow> q divides r \<Longrightarrow> p divides r"
+ apply (simp add: divides_def, safe)
+ apply (rule_tac x = "qa *** qaa" in exI)
+ apply (auto simp add: poly_mult fun_eq mult_assoc)
+ done
-lemma poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
-apply (auto simp add: le_iff_add)
-apply (induct_tac k)
-apply (rule_tac [2] poly_divides_trans)
-apply (auto simp add: divides_def)
-apply (rule_tac x = p in exI)
-apply (auto simp add: poly_mult fun_eq mult_ac)
-done
+lemma poly_divides_exp: "m \<le> n \<Longrightarrow> (p %^ m) divides (p %^ n)"
+ apply (auto simp add: le_iff_add)
+ apply (induct_tac k)
+ apply (rule_tac [2] poly_divides_trans)
+ apply (auto simp add: divides_def)
+ apply (rule_tac x = p in exI)
+ apply (auto simp add: poly_mult fun_eq mult_ac)
+ done
-lemma poly_exp_divides: "[| (p %^ n) divides q; m\<le>n |] ==> (p %^ m) divides q"
-by (blast intro: poly_divides_exp poly_divides_trans)
+lemma poly_exp_divides: "(p %^ n) divides q \<Longrightarrow> m \<le> n \<Longrightarrow> (p %^ m) divides q"
+ by (blast intro: poly_divides_exp poly_divides_trans)
-lemma poly_divides_add:
- "[| p divides q; p divides r |] ==> p divides (q +++ r)"
-apply (simp add: divides_def, auto)
-apply (rule_tac x = "qa +++ qaa" in exI)
-apply (auto simp add: poly_add fun_eq poly_mult distrib_left)
-done
+lemma poly_divides_add: "p divides q \<Longrightarrow> p divides r \<Longrightarrow> p divides (q +++ r)"
+ apply (simp add: divides_def, auto)
+ apply (rule_tac x = "qa +++ qaa" in exI)
+ apply (auto simp add: poly_add fun_eq poly_mult distrib_left)
+ done
-lemma poly_divides_diff:
- "[| p divides q; p divides (q +++ r) |] ==> p divides r"
-apply (simp add: divides_def, auto)
-apply (rule_tac x = "qaa +++ -- qa" in exI)
-apply (auto simp add: poly_add fun_eq poly_mult poly_minus right_diff_distrib algebra_simps)
-done
+lemma poly_divides_diff: "p divides q \<Longrightarrow> p divides (q +++ r) \<Longrightarrow> p divides r"
+ apply (simp add: divides_def, auto)
+ apply (rule_tac x = "qaa +++ -- qa" in exI)
+ apply (auto simp add: poly_add fun_eq poly_mult poly_minus algebra_simps)
+ done
lemma poly_divides_diff2: "[| p divides r; p divides (q +++ r) |] ==> p divides q"
-apply (erule poly_divides_diff)
-apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac)
-done
+ apply (erule poly_divides_diff)
+ apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac)
+ done
lemma poly_divides_zero: "poly p = poly [] ==> q divides p"
-apply (simp add: divides_def)
-apply (rule exI[where x="[]"])
-apply (auto simp add: fun_eq poly_mult)
-done
+ apply (simp add: divides_def)
+ apply (rule exI[where x="[]"])
+ apply (auto simp add: fun_eq poly_mult)
+ done
-lemma poly_divides_zero2: "q divides []"
-apply (simp add: divides_def)
-apply (rule_tac x = "[]" in exI)
-apply (auto simp add: fun_eq)
-done
-declare poly_divides_zero2 [simp]
+lemma poly_divides_zero2 [simp]: "q divides []"
+ apply (simp add: divides_def)
+ apply (rule_tac x = "[]" in exI)
+ apply (auto simp add: fun_eq)
+ done
text{*At last, we can consider the order of a root.*}
lemma poly_order_exists_lemma [rule_format]:
- "\<forall>p. length p = d --> poly p \<noteq> poly []
- --> (\<exists>n q. p = mulexp n [-a, (1::'a::{idom,ring_char_0})] q & poly q a \<noteq> 0)"
-apply (induct "d")
-apply (simp add: fun_eq, safe)
-apply (case_tac "poly p a = 0")
-apply (drule_tac poly_linear_divides [THEN iffD1], safe)
-apply (drule_tac x = q in spec)
-apply (drule_tac poly_entire_neg [THEN iffD1], safe, force)
-apply (rule_tac x = "Suc n" in exI)
-apply (rule_tac x = qa in exI)
-apply (simp del: pmult_Cons)
-apply (rule_tac x = 0 in exI, force)
-done
+ "\<forall>p. length p = d \<longrightarrow> poly p \<noteq> poly [] \<longrightarrow>
+ (\<exists>n q. p = mulexp n [-a, (1::'a::{idom,ring_char_0})] q & poly q a \<noteq> 0)"
+ apply (induct "d")
+ apply (simp add: fun_eq, safe)
+ apply (case_tac "poly p a = 0")
+ apply (drule_tac poly_linear_divides [THEN iffD1], safe)
+ apply (drule_tac x = q in spec)
+ apply (drule_tac poly_entire_neg [THEN iffD1], safe, force)
+ apply (rule_tac x = "Suc n" in exI)
+ apply (rule_tac x = qa in exI)
+ apply (simp del: pmult_Cons)
+ apply (rule_tac x = 0 in exI, force)
+ done
(* FIXME: Tidy up *)
lemma poly_order_exists:
"[| length p = d; poly p \<noteq> poly [] |]
==> \<exists>n. ([-a, 1] %^ n) divides p &
~(([-a, (1::'a::{idom,ring_char_0})] %^ (Suc n)) divides p)"
-apply (drule poly_order_exists_lemma [where a=a], assumption, clarify)
-apply (rule_tac x = n in exI, safe)
-apply (unfold divides_def)
-apply (rule_tac x = q in exI)
-apply (induct_tac "n", simp)
-apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult distrib_left mult_ac)
-apply safe
-apply (subgoal_tac "poly (mulexp n [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc n *** qa)")
-apply simp
-apply (induct_tac "n")
-apply (simp del: pmult_Cons pexp_Suc)
-apply (erule_tac Q = "poly q a = 0" in contrapos_np)
-apply (simp add: poly_add poly_cmult)
-apply (rule pexp_Suc [THEN ssubst])
-apply (rule ccontr)
-apply (simp add: poly_mult_left_cancel poly_mult_assoc del: pmult_Cons pexp_Suc)
-done
+ apply (drule poly_order_exists_lemma [where a=a], assumption, clarify)
+ apply (rule_tac x = n in exI, safe)
+ apply (unfold divides_def)
+ apply (rule_tac x = q in exI)
+ apply (induct_tac n, simp)
+ apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult distrib_left mult_ac)
+ apply safe
+ apply (subgoal_tac "poly (mulexp n [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc n *** qa)")
+ apply simp
+ apply (induct_tac n)
+ apply (simp del: pmult_Cons pexp_Suc)
+ apply (erule_tac Q = "poly q a = 0" in contrapos_np)
+ apply (simp add: poly_add poly_cmult)
+ apply (rule pexp_Suc [THEN ssubst])
+ apply (rule ccontr)
+ apply (simp add: poly_mult_left_cancel poly_mult_assoc del: pmult_Cons pexp_Suc)
+ done
-lemma poly_one_divides: "[1] divides p"
-by (simp add: divides_def, auto)
-declare poly_one_divides [simp]
+lemma poly_one_divides [simp]: "[1] divides p"
+ by (auto simp: divides_def)
lemma poly_order: "poly p \<noteq> poly []
==> EX! n. ([-a, (1::'a::{idom,ring_char_0})] %^ n) divides p &
~(([-a, 1] %^ (Suc n)) divides p)"
-apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
-apply (cut_tac x = y and y = n in less_linear)
-apply (drule_tac m = n in poly_exp_divides)
-apply (auto dest: Suc_le_eq [THEN iffD2, THEN [2] poly_exp_divides]
- simp del: pmult_Cons pexp_Suc)
-done
+ apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
+ apply (cut_tac x = y and y = n in less_linear)
+ apply (drule_tac m = n in poly_exp_divides)
+ apply (auto dest: Suc_le_eq [THEN iffD2, THEN [2] poly_exp_divides]
+ simp del: pmult_Cons pexp_Suc)
+ done
text{*Order*}
lemma some1_equalityD: "[| n = (@n. P n); EX! n. P n |] ==> P n"
-by (blast intro: someI2)
+ by (blast intro: someI2)
lemma order:
- "(([-a, (1::'a::{idom,ring_char_0})] %^ n) divides p &
- ~(([-a, 1] %^ (Suc n)) divides p)) =
- ((n = order a p) & ~(poly p = poly []))"
-apply (unfold order_def)
-apply (rule iffI)
-apply (blast dest: poly_divides_zero intro!: some1_equality [symmetric] poly_order)
-apply (blast intro!: poly_order [THEN [2] some1_equalityD])
-done
+ "(([-a, (1::'a::{idom,ring_char_0})] %^ n) divides p &
+ ~(([-a, 1] %^ (Suc n)) divides p)) =
+ ((n = order a p) & ~(poly p = poly []))"
+ apply (unfold order_def)
+ apply (rule iffI)
+ apply (blast dest: poly_divides_zero intro!: some1_equality [symmetric] poly_order)
+ apply (blast intro!: poly_order [THEN [2] some1_equalityD])
+ done
-lemma order2: "[| poly p \<noteq> poly [] |]
- ==> ([-a, (1::'a::{idom,ring_char_0})] %^ (order a p)) divides p &
- ~(([-a, 1] %^ (Suc(order a p))) divides p)"
-by (simp add: order del: pexp_Suc)
+lemma order2: "poly p \<noteq> poly [] \<Longrightarrow>
+ ([-a, (1::'a::{idom,ring_char_0})] %^ (order a p)) divides p &
+ ~(([-a, 1] %^ (Suc(order a p))) divides p)"
+ by (simp add: order del: pexp_Suc)
lemma order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p;
- ~(([-a, (1::'a::{idom,ring_char_0})] %^ (Suc n)) divides p)
+ ~(([-a, (1::'a::{idom,ring_char_0})] %^ (Suc n)) divides p)
|] ==> (n = order a p)"
-by (insert order [of a n p], auto)
+ using order [of a n p] by auto
lemma order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p &
~(([-a, (1::'a::{idom,ring_char_0})] %^ (Suc n)) divides p))
==> (n = order a p)"
-by (blast intro: order_unique)
+ by (blast intro: order_unique)
lemma order_poly: "poly p = poly q ==> order a p = order a q"
-by (auto simp add: fun_eq divides_def poly_mult order_def)
+ by (auto simp add: fun_eq divides_def poly_mult order_def)
-lemma pexp_one: "p %^ (Suc 0) = p"
-apply (induct "p")
-apply (auto simp add: numeral_1_eq_1)
-done
-declare pexp_one [simp]
+lemma pexp_one [simp]: "p %^ (Suc 0) = p"
+ by (induct p) simp_all
lemma lemma_order_root [rule_format]:
- "\<forall>p a. 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
- --> poly p a = 0"
-apply (induct "n", blast)
-apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
-done
+ "\<forall>p a. 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
+ --> poly p a = 0"
+ apply (induct n)
+ apply blast
+ apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
+ done
lemma order_root: "(poly p a = (0::'a::{idom,ring_char_0})) = ((poly p = poly []) | order a p \<noteq> 0)"
-apply (case_tac "poly p = poly []", auto)
-apply (simp add: poly_linear_divides del: pmult_Cons, safe)
-apply (drule_tac [!] a = a in order2)
-apply (rule ccontr)
-apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
-using neq0_conv
-apply (blast intro: lemma_order_root)
-done
+ apply (case_tac "poly p = poly []", auto)
+ apply (simp add: poly_linear_divides del: pmult_Cons, safe)
+ apply (drule_tac [!] a = a in order2)
+ apply (rule ccontr)
+ apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
+ using neq0_conv
+ apply (blast intro: lemma_order_root)
+ done
lemma order_divides: "(([-a, 1::'a::{idom,ring_char_0}] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
-apply (case_tac "poly p = poly []", auto)
-apply (simp add: divides_def fun_eq poly_mult)
-apply (rule_tac x = "[]" in exI)
-apply (auto dest!: order2 [where a=a]
- intro: poly_exp_divides simp del: pexp_Suc)
-done
+ apply (case_tac "poly p = poly []", auto)
+ apply (simp add: divides_def fun_eq poly_mult)
+ apply (rule_tac x = "[]" in exI)
+ apply (auto dest!: order2 [where a=a]
+ intro: poly_exp_divides simp del: pexp_Suc)
+ done
lemma order_decomp:
- "poly p \<noteq> poly []
- ==> \<exists>q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) &
- ~([-a, 1::'a::{idom,ring_char_0}] divides q)"
-apply (unfold divides_def)
-apply (drule order2 [where a = a])
-apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe)
-apply (rule_tac x = q in exI, safe)
-apply (drule_tac x = qa in spec)
-apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons)
-done
+ "poly p \<noteq> poly [] \<Longrightarrow>
+ \<exists>q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) &
+ ~([-a, 1::'a::{idom,ring_char_0}] divides q)"
+ apply (unfold divides_def)
+ apply (drule order2 [where a = a])
+ apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe)
+ apply (rule_tac x = q in exI, safe)
+ apply (drule_tac x = qa in spec)
+ apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons)
+ done
text{*Important composition properties of orders.*}
-lemma order_mult: "poly (p *** q) \<noteq> poly []
- ==> order a (p *** q) = order a p + order (a::'a::{idom,ring_char_0}) q"
-apply (cut_tac a = a and p = "p***q" and n = "order a p + order a q" in order)
-apply (auto simp add: poly_entire simp del: pmult_Cons)
-apply (drule_tac a = a in order2)+
-apply safe
-apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
-apply (rule_tac x = "qa *** qaa" in exI)
-apply (simp add: poly_mult mult_ac del: pmult_Cons)
-apply (drule_tac a = a in order_decomp)+
-apply safe
-apply (subgoal_tac "[-a,1] divides (qa *** qaa) ")
-apply (simp add: poly_primes del: pmult_Cons)
-apply (auto simp add: divides_def simp del: pmult_Cons)
-apply (rule_tac x = qb in exI)
-apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))")
-apply (drule poly_mult_left_cancel [THEN iffD1], force)
-apply (subgoal_tac "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (qa *** qaa))) = poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))) ")
-apply (drule poly_mult_left_cancel [THEN iffD1], force)
-apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
-done
-
-
+lemma order_mult: "poly (p *** q) \<noteq> poly [] \<Longrightarrow>
+ order a (p *** q) = order a p + order (a::'a::{idom,ring_char_0}) q"
+ apply (cut_tac a = a and p = "p***q" and n = "order a p + order a q" in order)
+ apply (auto simp add: poly_entire simp del: pmult_Cons)
+ apply (drule_tac a = a in order2)+
+ apply safe
+ apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
+ apply (rule_tac x = "qa *** qaa" in exI)
+ apply (simp add: poly_mult mult_ac del: pmult_Cons)
+ apply (drule_tac a = a in order_decomp)+
+ apply safe
+ apply (subgoal_tac "[-a,1] divides (qa *** qaa) ")
+ apply (simp add: poly_primes del: pmult_Cons)
+ apply (auto simp add: divides_def simp del: pmult_Cons)
+ apply (rule_tac x = qb in exI)
+ apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))")
+ apply (drule poly_mult_left_cancel [THEN iffD1], force)
+ apply (subgoal_tac "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (qa *** qaa))) = poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))) ")
+ apply (drule poly_mult_left_cancel [THEN iffD1], force)
+ apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
+ done
lemma order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order (a::'a::{idom,ring_char_0}) p \<noteq> 0)"
-by (rule order_root [THEN ssubst], auto)
+ by (rule order_root [THEN ssubst], auto)
-lemma pmult_one: "[1] *** p = p"
-by auto
-declare pmult_one [simp]
+lemma pmult_one [simp]: "[1] *** p = p"
+ by auto
lemma poly_Nil_zero: "poly [] = poly [0]"
-by (simp add: fun_eq)
+ by (simp add: fun_eq)
lemma rsquarefree_decomp:
- "[| rsquarefree p; poly p a = (0::'a::{idom,ring_char_0}) |]
- ==> \<exists>q. (poly p = poly ([-a, 1] *** q)) & poly q a \<noteq> 0"
-apply (simp add: rsquarefree_def, safe)
-apply (frule_tac a = a in order_decomp)
-apply (drule_tac x = a in spec)
-apply (drule_tac a = a in order_root2 [symmetric])
-apply (auto simp del: pmult_Cons)
-apply (rule_tac x = q in exI, safe)
-apply (simp add: poly_mult fun_eq)
-apply (drule_tac p1 = q in poly_linear_divides [THEN iffD1])
-apply (simp add: divides_def del: pmult_Cons, safe)
-apply (drule_tac x = "[]" in spec)
-apply (auto simp add: fun_eq)
-done
+ "[| rsquarefree p; poly p a = (0::'a::{idom,ring_char_0}) |]
+ ==> \<exists>q. (poly p = poly ([-a, 1] *** q)) & poly q a \<noteq> 0"
+ apply (simp add: rsquarefree_def, safe)
+ apply (frule_tac a = a in order_decomp)
+ apply (drule_tac x = a in spec)
+ apply (drule_tac a = a in order_root2 [symmetric])
+ apply (auto simp del: pmult_Cons)
+ apply (rule_tac x = q in exI, safe)
+ apply (simp add: poly_mult fun_eq)
+ apply (drule_tac p1 = q in poly_linear_divides [THEN iffD1])
+ apply (simp add: divides_def del: pmult_Cons, safe)
+ apply (drule_tac x = "[]" in spec)
+ apply (auto simp add: fun_eq)
+ done
text{*Normalization of a polynomial.*}
-lemma poly_normalize: "poly (pnormalize p) = poly p"
-apply (induct "p")
-apply (auto simp add: fun_eq)
-done
-declare poly_normalize [simp]
+lemma poly_normalize [simp]: "poly (pnormalize p) = poly p"
+ by (induct p) (auto simp add: fun_eq)
text{*The degree of a polynomial.*}
-lemma lemma_degree_zero:
- "list_all (%c. c = 0) p \<longleftrightarrow> pnormalize p = []"
-by (induct "p", auto)
+lemma lemma_degree_zero: "list_all (%c. c = 0) p \<longleftrightarrow> pnormalize p = []"
+ by (induct p) auto
lemma degree_zero: "(poly p = poly ([]:: (('a::{idom,ring_char_0}) list))) \<Longrightarrow> (degree p = 0)"
-apply (simp add: degree_def)
-apply (case_tac "pnormalize p = []")
-apply (auto simp add: poly_zero lemma_degree_zero )
-done
+ apply (simp add: degree_def)
+ apply (case_tac "pnormalize p = []")
+ apply (auto simp add: poly_zero lemma_degree_zero )
+ done
lemma pnormalize_sing: "(pnormalize [x] = [x]) \<longleftrightarrow> x \<noteq> 0" by simp
+
lemma pnormalize_pair: "y \<noteq> 0 \<longleftrightarrow> (pnormalize [x, y] = [x, y])" by simp
-lemma pnormal_cons: "pnormal p \<Longrightarrow> pnormal (c#p)"
+
+lemma pnormal_cons: "pnormal p \<Longrightarrow> pnormal (c#p)"
unfolding pnormal_def by simp
+
lemma pnormal_tail: "p\<noteq>[] \<Longrightarrow> pnormal (c#p) \<Longrightarrow> pnormal p"
- unfolding pnormal_def
+ unfolding pnormal_def
apply (cases "pnormalize p = []", auto)
- by (cases "c = 0", auto)
+ apply (cases "c = 0", auto)
+ done
+
lemma pnormal_last_nonzero: "pnormal p ==> last p \<noteq> 0"
apply (induct p, auto simp add: pnormal_def)
apply (case_tac "pnormalize p = []", auto)
- by (case_tac "a=0", auto)
+ apply (case_tac "a=0", auto)
+ done
+
lemma pnormal_length: "pnormal p \<Longrightarrow> 0 < length p"
unfolding pnormal_def length_greater_0_conv by blast
+
lemma pnormal_last_length: "\<lbrakk>0 < length p ; last p \<noteq> 0\<rbrakk> \<Longrightarrow> pnormal p"
apply (induct p, auto)
apply (case_tac "p = []", auto)
apply (simp add: pnormal_def)
- by (rule pnormal_cons, auto)
+ apply (rule pnormal_cons, auto)
+ done
+
lemma pnormal_id: "pnormal p \<longleftrightarrow> (0 < length p \<and> last p \<noteq> 0)"
using pnormal_last_length pnormal_length pnormal_last_nonzero by blast
text{*Tidier versions of finiteness of roots.*}
-lemma poly_roots_finite_set: "poly p \<noteq> poly [] ==> finite {x::'a::{idom,ring_char_0}. poly p x = 0}"
-unfolding poly_roots_finite .
+lemma poly_roots_finite_set:
+ "poly p \<noteq> poly [] \<Longrightarrow> finite {x::'a::{idom,ring_char_0}. poly p x = 0}"
+ unfolding poly_roots_finite .
text{*bound for polynomial.*}
lemma poly_mono: "abs(x) \<le> k ==> abs(poly p (x::'a::{linordered_idom})) \<le> poly (map abs p) k"
-apply (induct "p", auto)
-apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans)
-apply (rule abs_triangle_ineq)
-apply (auto intro!: mult_mono simp add: abs_mult)
-done
+ apply (induct "p", auto)
+ apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans)
+ apply (rule abs_triangle_ineq)
+ apply (auto intro!: mult_mono simp add: abs_mult)
+ done
lemma poly_Sing: "poly [c] x = c" by simp
--- a/src/Pure/Concurrent/future.ML Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Jul 29 20:51:05 2013 +0200
@@ -48,6 +48,7 @@
val worker_group: unit -> group option
val the_worker_group: unit -> group
val worker_subgroup: unit -> group
+ val worker_nest: string -> ('a -> 'b) -> 'a -> 'b
val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b
type 'a future
val task_of: 'a future -> task
@@ -108,6 +109,9 @@
fun worker_subgroup () = new_group (worker_group ());
+fun worker_nest name f x =
+ setmp_worker_task (Task_Queue.new_task (the_worker_group ()) name NONE) f x;
+
fun worker_guest name group f x =
if is_some (worker_task ()) then
raise Fail "Already running as worker thread"
--- a/src/Pure/PIDE/command.ML Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Pure/PIDE/command.ML Mon Jul 29 20:51:05 2013 +0200
@@ -9,15 +9,15 @@
val read: (unit -> theory) -> Token.T list -> Toplevel.transition
type eval
val eval_eq: eval * eval -> bool
+ val eval_finished: eval -> bool
val eval_result_state: eval -> Toplevel.state
- val eval_stable: eval -> bool
val eval: (unit -> theory) -> Token.T list -> eval -> eval
type print
val print: bool -> string -> eval -> print list -> print list option
type print_fn = Toplevel.transition -> Toplevel.state -> unit
val print_function: string ->
({command_name: string} ->
- {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
+ {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
val no_print_function: string -> unit
type exec = eval * print list
val no_exec: exec
@@ -28,7 +28,7 @@
structure Command: COMMAND =
struct
-(** memo results -- including physical interrupts! **)
+(** memo results **)
datatype 'a expr =
Expr of Document_ID.exec * (unit -> 'a) |
@@ -45,30 +45,28 @@
Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
| Result res => Exn.release res);
-fun memo_stable (Memo v) =
- (case Synchronized.value v of
- Expr _ => true
- | Result res => not (Exn.is_interrupt_exn res));
-
fun memo_finished (Memo v) =
(case Synchronized.value v of
Expr _ => false
- | Result res => not (Exn.is_interrupt_exn res));
+ | Result _ => true);
fun memo_exec execution_id (Memo v) =
- Synchronized.guarded_access v
+ Synchronized.timed_access v (K (SOME Time.zeroTime))
(fn expr =>
(case expr of
- Expr (exec_id, e) =>
+ Expr (exec_id, body) =>
uninterruptible (fn restore_attributes => fn () =>
if Execution.running execution_id exec_id then
let
- val res = Exn.capture (restore_attributes e) ();
- val _ = Execution.finished exec_id;
- in SOME (Exn.is_interrupt_exn res, Result res) end
- else SOME (true, expr)) ()
- | Result _ => SOME (false, expr)))
- |> (fn true => Exn.interrupt () | false => ());
+ val res =
+ (body
+ |> restore_attributes
+ |> Future.worker_nest "Command.memo_exec"
+ |> Exn.interruptible_capture) ();
+ in SOME ((), Result res) end
+ else SOME ((), expr)) ()
+ | Result _ => SOME ((), expr)))
+ |> (fn NONE => error "Conflicting command execution" | _ => ());
fun memo_fork params execution_id (Memo v) =
(case Synchronized.value v of
@@ -122,12 +120,11 @@
fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
+fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
+
fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
val eval_result_state = #state o eval_result;
-fun eval_stable (Eval {exec_id, eval_process}) =
- Goal.stable_futures exec_id andalso memo_stable eval_process;
-
local
fun run int tr st =
@@ -198,14 +195,14 @@
(* print *)
datatype print = Print of
- {name: string, delay: Time.time, pri: int, persistent: bool,
+ {name: string, delay: Time.time option, pri: int, persistent: bool,
exec_id: Document_ID.exec, print_process: unit memo};
type print_fn = Toplevel.transition -> Toplevel.state -> unit;
type print_function =
{command_name: string} ->
- {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option;
+ {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
local
@@ -220,11 +217,7 @@
fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
-fun print_stable (Print {exec_id, print_process, ...}) =
- Goal.stable_futures exec_id andalso memo_stable print_process;
-
-fun print_finished (Print {exec_id, print_process, ...}) =
- Goal.stable_futures exec_id andalso memo_finished print_process;
+fun print_finished (Print {print_process, ...}) = memo_finished print_process;
fun print_persistent (Print {persistent, ...}) = persistent;
@@ -256,16 +249,15 @@
| Exn.Res (SOME pr) => SOME (make_print false pr)
| Exn.Exn exn =>
SOME (make_print true
- {delay = Time.zeroTime, pri = 0, persistent = false,
- print_fn = fn _ => fn _ => reraise exn}))
+ {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
end;
val new_prints =
if command_visible then
rev (Synchronized.value print_functions) |> map_filter (fn pr =>
(case find_first (fn Print {name, ...} => name = fst pr) old_prints of
- SOME print => if print_stable print then SOME print else new_print pr
- | NONE => new_print pr))
+ NONE => new_print pr
+ | some => some))
else filter (fn print => print_finished print andalso print_persistent print) old_prints;
in
if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
@@ -285,7 +277,7 @@
val _ =
print_function "print_state"
(fn {command_name} =>
- SOME {delay = Time.zeroTime, pri = 1, persistent = true,
+ SOME {delay = NONE, pri = 1, persistent = true,
print_fn = fn tr => fn st' =>
let
val is_init = Keyword.is_theory_begin command_name;
@@ -316,8 +308,9 @@
memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
execution_id print_process;
in
- if delay = Time.zeroTime then fork ()
- else ignore (Event_Timer.request (Time.+ (Time.now (), delay)) fork)
+ (case delay of
+ NONE => fork ()
+ | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork))
end
else memo_exec execution_id print_process;
--- a/src/Pure/PIDE/document.ML Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Pure/PIDE/document.ML Mon Jul 29 20:51:05 2013 +0200
@@ -18,7 +18,7 @@
val init_state: state
val define_command: Document_ID.command -> string -> string -> state -> state
val remove_versions: Document_ID.version list -> state -> state
- val start_execution: state -> unit
+ val start_execution: state -> state
val timing: bool Unsynchronized.ref
val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
@@ -41,7 +41,7 @@
abstype node = Node of
{header: node_header, (*master directory, theory header, errors*)
perspective: perspective, (*visible commands, last visible command*)
- entries: Command.exec option Entries.T * bool, (*command entries with excecutions, stable*)
+ entries: Command.exec option Entries.T, (*command entries with excecutions*)
result: Command.eval option} (*result of last execution*)
and version = Version of node String_Graph.T (*development graph wrt. static imports*)
with
@@ -58,9 +58,8 @@
val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
val no_perspective = make_perspective [];
-val empty_node = make_node (no_header, no_perspective, (Entries.empty, true), NONE);
-val clear_node =
- map_node (fn (header, _, _, _) => (header, no_perspective, (Entries.empty, true), NONE));
+val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
+val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
(* basic components *)
@@ -87,17 +86,11 @@
val visible_node = is_some o visible_last
fun map_entries f =
- map_node (fn (header, perspective, (entries, stable), result) =>
- (header, perspective, (f entries, stable), result));
-fun get_entries (Node {entries = (entries, _), ...}) = entries;
-
-fun entries_stable stable =
- map_node (fn (header, perspective, (entries, _), result) =>
- (header, perspective, (entries, stable), result));
-fun stable_entries (Node {entries = (_, stable), ...}) = stable;
+ map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
+fun get_entries (Node {entries, ...}) = entries;
fun iterate_entries f = Entries.iterate NONE f o get_entries;
-fun iterate_entries_after start f (Node {entries = (entries, _), ...}) =
+fun iterate_entries_after start f (Node {entries, ...}) =
(case Entries.get_after entries start of
NONE => I
| SOME id => Entries.iterate (SOME id) f entries);
@@ -112,10 +105,10 @@
| (NONE, NONE) => false
| _ => true);
-fun finished_theory node =
- (case Exn.capture (Command.eval_result_state o the) (get_result node) of
- Exn.Res st => can (Toplevel.end_theory Position.none) st
- | _ => false);
+fun pending_result node =
+ (case get_result node of
+ SOME eval => not (Command.eval_finished eval)
+ | NONE => false);
fun get_node nodes name = String_Graph.get_node nodes name
handle String_Graph.UNDEF _ => empty_node;
@@ -203,10 +196,16 @@
(** main state -- document structure and execution process **)
-type execution = {version_id: Document_ID.version, execution_id: Document_ID.execution};
+type execution =
+ {version_id: Document_ID.version, (*static version id*)
+ execution_id: Document_ID.execution, (*dynamic execution id*)
+ frontier: Future.task Symtab.table}; (*node name -> running execution task*)
-val no_execution = {version_id = Document_ID.none, execution_id = Document_ID.none};
-fun next_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
+val no_execution: execution =
+ {version_id = Document_ID.none, execution_id = Document_ID.none, frontier = Symtab.empty};
+
+fun new_execution version_id frontier : execution =
+ {version_id = version_id, execution_id = Execution.start (), frontier = frontier};
abstype state = State of
{versions: version Inttab.table, (*version id -> document content*)
@@ -223,17 +222,15 @@
val init_state =
make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution);
-fun execution_of (State {execution, ...}) = execution;
-
(* document versions *)
fun define_version version_id version =
- map_state (fn (versions, commands, _) =>
+ map_state (fn (versions, commands, {frontier, ...}) =>
let
val versions' = Inttab.update_new (version_id, version) versions
handle Inttab.DUP dup => err_dup "document version" dup;
- val execution' = next_execution version_id;
+ val execution' = new_execution version_id frontier;
in (versions', commands, execution') end);
fun the_version (State {versions, ...}) version_id =
@@ -294,30 +291,38 @@
(* document execution *)
-fun start_execution state =
+fun start_execution state = state |> map_state (fn (versions, commands, execution) =>
let
- val {version_id, execution_id} = execution_of state;
+ val {version_id, execution_id, frontier} = execution;
val pri = Options.default_int "editor_execution_priority";
- val _ =
+
+ val new_tasks =
if Execution.is_running execution_id then
nodes_of (the_version state version_id) |> String_Graph.schedule
(fn deps => fn (name, node) =>
- if not (visible_node node) andalso finished_theory node then
- Future.value ()
- else
- (singleton o Future.forks)
- {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
- deps = map (Future.task_of o #2) deps, pri = pri, interrupts = false}
- (fn () =>
+ if visible_node node orelse pending_result node then
+ let
+ val former_task = Symtab.lookup frontier name;
+ fun body () =
iterate_entries (fn (_, opt_exec) => fn () =>
(case opt_exec of
SOME exec =>
if Execution.is_running execution_id
then SOME (Command.exec execution_id exec)
else NONE
- | NONE => NONE)) node ()))
+ | NONE => NONE)) node ()
+ handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn;
+ val future =
+ (singleton o Future.forks)
+ {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
+ deps = the_list former_task @ map #2 (maps #2 deps),
+ pri = pri, interrupts = false} body;
+ in [(name, Future.task_of future)] end
+ else [])
else [];
- in () end;
+ val frontier' = (fold o fold) Symtab.update new_tasks frontier;
+ val execution' = {version_id = version_id, execution_id = execution_id, frontier = frontier'};
+ in (versions, commands, execution') end);
@@ -328,7 +333,6 @@
type assign_update = Command.exec option Inttab.table; (*command id -> exec*)
val assign_update_empty: assign_update = Inttab.empty;
-fun assign_update_null (tab: assign_update) = Inttab.is_empty tab;
fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id;
fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node;
@@ -358,7 +362,7 @@
Symtab.fold (fn (a, ()) =>
exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
Symtab.update (a, ())) all_visible Symtab.empty;
- in Symtab.defined required end;
+ in required end;
fun init_theory deps node span =
let
@@ -402,8 +406,7 @@
val flags' = update_flags prev flags;
val same' =
(case (lookup_entry node0 command_id, opt_exec) of
- (SOME (eval0, _), SOME (eval, _)) =>
- Command.eval_eq (eval0, eval) andalso Command.eval_stable eval
+ (SOME (eval0, _), SOME (eval, _)) => Command.eval_eq (eval0, eval)
| _ => false);
val assign_update' = assign_update |> same' ?
(case opt_exec of
@@ -456,7 +459,9 @@
val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
val nodes = nodes_of new_version;
- val is_required = make_required nodes;
+ val required = make_required nodes;
+ val required0 = make_required (nodes_of old_version);
+ val edited = fold (fn (name, _) => Symtab.update (name, ())) edits Symtab.empty;
val updated = timeit "Document.update" (fn () =>
nodes |> String_Graph.schedule
@@ -467,11 +472,11 @@
(fn () =>
let
val imports = map (apsnd Future.join) deps;
- val imports_changed = exists (#4 o #1 o #2) imports;
- val node_required = is_required name;
+ val imports_result_changed = exists (#4 o #1 o #2) imports;
+ val node_required = Symtab.defined required name;
in
- if imports_changed orelse AList.defined (op =) edits name orelse
- not (stable_entries node) orelse not (finished_theory node)
+ if Symtab.defined edited name orelse visible_node node orelse
+ imports_result_changed orelse Symtab.defined required0 name <> node_required
then
let
val node0 = node_of old_version name;
@@ -481,7 +486,7 @@
forall (fn (name, (_, node)) => check_theory true name node) imports;
val (print_execs, common, (still_visible, initial)) =
- if imports_changed then (assign_update_empty, NONE, (true, true))
+ if imports_result_changed then (assign_update_empty, NONE, (true, true))
else last_common state node0 node;
val common_command_exec = the_default_entry node common;
@@ -512,7 +517,6 @@
val node' = node
|> assign_update_apply assigned_execs
- |> entries_stable (assign_update_null updated_execs)
|> set_result result;
val assigned_node = SOME (name, node');
val result_changed = changed_result node0 node';
--- a/src/Pure/PIDE/execution.ML Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Pure/PIDE/execution.ML Mon Jul 29 20:51:05 2013 +0200
@@ -11,10 +11,8 @@
val discontinue: unit -> unit
val is_running: Document_ID.execution -> bool
val running: Document_ID.execution -> Document_ID.exec -> bool
- val finished: Document_ID.exec -> unit
val cancel: Document_ID.exec -> unit
val terminate: Document_ID.exec -> unit
- val snapshot: unit -> Future.group list
end;
structure Execution: EXECUTION =
@@ -53,20 +51,11 @@
else execs;
in SOME (continue, (execution_id', execs')) end);
-fun finished exec_id =
- Synchronized.change state
- (apsnd (fn execs =>
- Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
- error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
-
fun peek_list exec_id =
the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);
fun cancel exec_id = List.app Future.cancel_group (peek_list exec_id);
fun terminate exec_id = List.app Future.terminate (peek_list exec_id);
-fun snapshot () =
- Inttab.fold (cons o #2) (snd (Synchronized.value state)) [];
-
end;
--- a/src/Pure/PIDE/protocol.ML Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Mon Jul 29 20:51:05 2013 +0200
@@ -20,16 +20,6 @@
(fn [] => Execution.discontinue ());
val _ =
- Isabelle_Process.protocol_command "Document.cancel_execution"
- (fn [] =>
- let
- val _ = Execution.discontinue ();
- val groups = Execution.snapshot ();
- val _ = List.app Future.cancel_group groups;
- val _ = List.app Future.terminate groups;
- in () end);
-
-val _ =
Isabelle_Process.protocol_command "Document.update"
(fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
let
@@ -59,6 +49,7 @@
val (removed, assign_update, state') = Document.update old_id new_id edits state;
val _ = List.app Execution.terminate removed;
+ val _ = Goal.purge_futures removed;
val _ = List.app Isabelle_Process.reset_tracing removed;
val _ =
@@ -67,10 +58,7 @@
let open XML.Encode
in pair int (list (pair int (list int))) end
|> YXML.string_of_body);
- val _ =
- Event_Timer.request (Time.+ (Time.now (), seconds 0.02))
- (fn () => Document.start_execution state');
- in state' end));
+ in Document.start_execution state' end));
val _ =
Isabelle_Process.protocol_command "Document.remove_versions"
@@ -87,7 +75,7 @@
Isabelle_Process.protocol_command "Document.dialog_result"
(fn [serial, result] =>
Active.dialog_result (Markup.parse_int serial) result
- handle exn => if Exn.is_interrupt exn then () else reraise exn);
+ handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
end;
--- a/src/Pure/PIDE/protocol.scala Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala Mon Jul 29 20:51:05 2013 +0200
@@ -319,8 +319,6 @@
def discontinue_execution() { protocol_command("Document.discontinue_execution") }
- def cancel_execution() { protocol_command("Document.cancel_execution") }
-
def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
edits: List[Document.Edit_Command])
{
--- a/src/Pure/System/isabelle_process.ML Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML Mon Jul 29 20:51:05 2013 +0200
@@ -188,7 +188,10 @@
| name :: args => (worker_guest (fn () => run_command name args); true))
handle Runtime.TERMINATE => false
| exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
- in if continue then loop channel else Future.shutdown () end;
+ in
+ if continue then loop channel
+ else (Future.shutdown (); Goal.reset_futures (); ())
+ end;
end;
--- a/src/Pure/System/session.scala Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Pure/System/session.scala Mon Jul 29 20:51:05 2013 +0200
@@ -238,7 +238,6 @@
/* actor messages */
private case class Start(args: List[String])
- private case object Cancel_Execution
private case class Change(
doc_edits: List[Document.Edit_Command],
previous: Document.Version,
@@ -462,7 +461,7 @@
if (rc == 0) phase = Session.Inactive
else phase = Session.Failed
- case _ => bad_output()
+ case _ => raw_output_messages.event(output)
}
}
}
@@ -504,9 +503,6 @@
global_options.event(Session.Global_Options(options))
reply(())
- case Cancel_Execution if prover.isDefined =>
- prover.get.cancel_execution()
-
case Session.Raw_Edits(edits) if prover.isDefined =>
handle_raw_edits(edits)
reply(())
@@ -553,8 +549,6 @@
session_actor !? Stop
}
- def cancel_execution() { session_actor ! Cancel_Execution }
-
def update(edits: List[Document.Edit_Text])
{ if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }
--- a/src/Pure/goal.ML Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Pure/goal.ML Mon Jul 29 20:51:05 2013 +0200
@@ -27,7 +27,7 @@
val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
val fork: int -> (unit -> 'a) -> 'a future
val peek_futures: int -> unit future list
- val stable_futures: int-> bool
+ val purge_futures: int list -> unit
val reset_futures: unit -> Future.group list
val shutdown_futures: unit -> unit
val skip_proofs_enabled: unit -> bool
@@ -119,21 +119,21 @@
val forked_proofs =
Synchronized.var "forked_proofs"
- (0, []: Future.group list, Inttab.empty: unit future list Inttab.table);
+ (0, Inttab.empty: (Future.group * unit future) list Inttab.table);
fun count_forked i =
- Synchronized.change forked_proofs (fn (m, groups, tab) =>
+ Synchronized.change forked_proofs (fn (m, tab) =>
let
val n = m + i;
val _ = Future.forked_proofs := n;
- in (n, groups, tab) end);
+ in (n, tab) end);
fun register_forked id future =
- Synchronized.change forked_proofs (fn (m, groups, tab) =>
+ Synchronized.change forked_proofs (fn (m, tab) =>
let
- val groups' = Task_Queue.group_of_task (Future.task_of future) :: groups;
- val tab' = Inttab.cons_list (id, Future.map (K ()) future) tab;
- in (m, groups', tab') end);
+ val group = Task_Queue.group_of_task (Future.task_of future);
+ val tab' = Inttab.cons_list (id, (group, Future.map (K ()) future)) tab;
+ in (m, tab') end);
fun status task markups =
let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
@@ -179,14 +179,29 @@
fun forked_count () = #1 (Synchronized.value forked_proofs);
fun peek_futures id =
- Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
+ map #2 (Inttab.lookup_list (#2 (Synchronized.value forked_proofs)) id);
+
+fun check_canceled id group =
+ if Task_Queue.is_canceled group then ()
+ else raise Fail ("Attempt to purge valid execution " ^ string_of_int id);
-fun stable_futures id =
- not (Par_Exn.is_interrupted (map_filter Future.peek (peek_futures id)));
+fun purge_futures ids =
+ Synchronized.change forked_proofs (fn (_, tab) =>
+ let
+ val tab' = fold Inttab.delete_safe ids tab;
+ val n' =
+ Inttab.fold (fn (id, futures) => fn m =>
+ if Inttab.defined tab' id then m + length futures
+ else (List.app (check_canceled id o #1) futures; m)) tab 0;
+ val _ = Future.forked_proofs := n';
+ in (n', tab') end);
fun reset_futures () =
- Synchronized.change_result forked_proofs (fn (_, groups, _) =>
- (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
+ Synchronized.change_result forked_proofs (fn (_, tab) =>
+ let
+ val groups = Inttab.fold (fold (cons o #1) o #2) tab [];
+ val _ = Future.forked_proofs := 0;
+ in (groups, (0, Inttab.empty)) end);
fun shutdown_futures () =
(Future.shutdown ();
--- a/src/Tools/jEdit/src/actions.xml Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml Mon Jul 29 20:51:05 2013 +0200
@@ -52,14 +52,14 @@
wm.addDockableWindow("isabelle-symbols");
</CODE>
</ACTION>
- <ACTION NAME="isabelle.check-buffer">
+ <ACTION NAME="isabelle.execution-range-none">
<CODE>
- isabelle.jedit.PIDE.check_buffer(buffer);
+ isabelle.jedit.PIDE.execution_range_none();
</CODE>
</ACTION>
- <ACTION NAME="isabelle.cancel-execution">
+ <ACTION NAME="isabelle.execution-range-visible">
<CODE>
- isabelle.jedit.PIDE.cancel_execution();
+ isabelle.jedit.PIDE.execution_range_visible();
</CODE>
</ACTION>
<ACTION NAME="isabelle.increase-font-size">
--- a/src/Tools/jEdit/src/document_model.scala Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Mon Jul 29 20:51:05 2013 +0200
@@ -82,11 +82,17 @@
def node_perspective(): Text.Perspective =
{
Swing_Thread.require()
- Text.Perspective(
- for {
- doc_view <- PIDE.document_views(buffer)
- range <- doc_view.perspective().ranges
- } yield range)
+
+ PIDE.execution_range() match {
+ case PIDE.Execution_Range.ALL => Text.Perspective.full
+ case PIDE.Execution_Range.NONE => Text.Perspective.empty
+ case PIDE.Execution_Range.VISIBLE =>
+ Text.Perspective(
+ for {
+ doc_view <- PIDE.document_views(buffer)
+ range <- doc_view.perspective().ranges
+ } yield range)
+ }
}
@@ -126,7 +132,7 @@
def snapshot(): List[Text.Edit] = pending.toList
- def flush()
+ def flushed_edits(): List[Document.Edit_Text] =
{
Swing_Thread.require()
@@ -135,11 +141,14 @@
if (!edits.isEmpty || last_perspective != new_perspective) {
pending.clear
last_perspective = new_perspective
- session.update(node_edits(new_perspective, edits))
+ node_edits(new_perspective, edits)
}
+ else Nil
}
- private val delay_flush =
+ def flush(): Unit = session.update(flushed_edits())
+
+ val delay_flush =
Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
def +=(edit: Text.Edit)
@@ -149,11 +158,6 @@
delay_flush.invoke()
}
- def update_perspective()
- {
- delay_flush.invoke()
- }
-
def init()
{
flush()
@@ -167,17 +171,9 @@
}
}
- def update_perspective()
- {
- Swing_Thread.require()
- pending_edits.update_perspective()
- }
+ def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits()
- def full_perspective()
- {
- pending_edits.flush()
- session.update(node_edits(Text.Perspective(List(JEdit_Lib.buffer_range(buffer))), Nil))
- }
+ def update_perspective(): Unit = pending_edits.delay_flush.invoke()
/* snapshot */
--- a/src/Tools/jEdit/src/jEdit.props Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Mon Jul 29 20:51:05 2013 +0200
@@ -185,10 +185,10 @@
isabelle-readme.dock-position=bottom
isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=right
-isabelle.cancel-execution.label=Cancel execution
-isabelle.cancel-execution.shortcut=C+e BACK_SPACE
-isabelle.check-buffer.label=Commence full checking
-isabelle.check-buffer.shortcut=C+e SPACE
+isabelle.execution-range-none.label=Check nothing
+isabelle.execution-range-none.shortcut=C+e BACK_SPACE
+isabelle.execution-range-visible=Check visible parts of theories
+isabelle.execution-range-visible.shortcut=C+e SPACE
isabelle.control-bold.label=Control bold
isabelle.control-bold.shortcut=C+e RIGHT
isabelle.control-isub.label=Control subscript
--- a/src/Tools/jEdit/src/plugin.scala Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Mon Jul 29 20:51:05 2013 +0200
@@ -117,17 +117,46 @@
}
- /* full checking */
+ /* execution range */
+
+ object Execution_Range extends Enumeration {
+ val ALL = Value("all")
+ val NONE = Value("none")
+ val VISIBLE = Value("visible")
+ }
- def check_buffer(buffer: Buffer)
+ def execution_range(): Execution_Range.Value =
+ options.string("editor_execution_range") match {
+ case "all" => Execution_Range.ALL
+ case "none" => Execution_Range.NONE
+ case "visible" => Execution_Range.VISIBLE
+ case s => error("Bad value for option \"editor_execution_range\": " + quote(s))
+ }
+
+ def update_execution_range(range: Execution_Range.Value)
{
- document_model(buffer) match {
- case Some(model) => model.full_perspective()
- case None =>
+ Swing_Thread.require()
+
+ if (options.string("editor_execution_range") != range.toString) {
+ options.string("editor_execution_range") = range.toString
+ PIDE.session.global_options.event(Session.Global_Options(options.value))
+
+ PIDE.session.update(
+ (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
+ case (edits, buffer) =>
+ JEdit_Lib.buffer_lock(buffer) {
+ document_model(buffer) match {
+ case Some(model) => model.flushed_edits() ::: edits
+ case None => edits
+ }
+ }
+ }
+ )
}
}
- def cancel_execution() { PIDE.session.cancel_execution() }
+ def execution_range_none(): Unit = update_execution_range(Execution_Range.NONE)
+ def execution_range_visible(): Unit = update_execution_range(Execution_Range.VISIBLE)
}
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Mon Jul 29 20:51:05 2013 +0200
@@ -29,8 +29,10 @@
loop {
react {
case output: Isabelle_Process.Output =>
- if (output.is_stdout || output.is_stderr)
- Swing_Thread.later { text_area.append(XML.content(output.message)) }
+ Swing_Thread.later {
+ text_area.append(XML.content(output.message))
+ if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
+ }
case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
}
--- a/src/Tools/jEdit/src/theories_dockable.scala Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Jul 29 20:51:05 2013 +0200
@@ -10,13 +10,14 @@
import isabelle._
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component,
+ BoxPanel, Orientation, RadioButton, ButtonGroup}
import scala.swing.event.{ButtonClicked, MouseClicked}
import java.lang.System
-import java.awt.{BorderLayout, Graphics2D, Insets}
+import java.awt.{BorderLayout, Graphics2D, Insets, Color}
import javax.swing.{JList, BorderFactory}
-import javax.swing.border.{BevelBorder, SoftBevelBorder}
+import javax.swing.border.{BevelBorder, SoftBevelBorder, LineBorder}
import org.gjt.sp.jedit.{View, jEdit}
@@ -54,20 +55,36 @@
Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
}
- private val cancel = new Button("Cancel") {
- reactions += { case ButtonClicked(_) => PIDE.cancel_execution() }
- }
- cancel.tooltip = "Cancel current checking process"
+ private val execution_range = new BoxPanel(Orientation.Horizontal) {
+ private def button(range: PIDE.Execution_Range.Value, tip: String): RadioButton =
+ new RadioButton(range.toString) {
+ tooltip = tip
+ reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) }
+ }
+ private val label =
+ new Label("Range:") { tooltip = "Execution range of continuous document processing" }
+ private val b1 = button(PIDE.Execution_Range.ALL, "Check all theories (potentially slow)")
+ private val b2 = button(PIDE.Execution_Range.NONE, "Check nothing")
+ private val b3 = button(PIDE.Execution_Range.VISIBLE, "Check visible parts of theories")
+ private val group = new ButtonGroup(b1, b2, b3)
+ contents ++= List(label, b1, b2, b3)
+ border = new LineBorder(Color.GRAY)
- private val check = new Button("Check") {
- reactions += { case ButtonClicked(_) => PIDE.check_buffer(view.getBuffer) }
+ def load()
+ {
+ PIDE.execution_range() match {
+ case PIDE.Execution_Range.ALL => group.select(b1)
+ case PIDE.Execution_Range.NONE => group.select(b2)
+ case PIDE.Execution_Range.VISIBLE => group.select(b3)
+ }
+ }
+ load()
}
- check.tooltip = "Commence full checking of current buffer"
private val logic = Isabelle_Logic.logic_selector(true)
private val controls =
- new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
+ new FlowPanel(FlowPanel.Alignment.Right)(execution_range, session_phase, logic)
add(controls.peer, BorderLayout.NORTH)
@@ -156,7 +173,11 @@
react {
case phase: Session.Phase => handle_phase(phase)
- case _: Session.Global_Options => Swing_Thread.later { logic.load () }
+ case _: Session.Global_Options =>
+ Swing_Thread.later {
+ execution_range.load()
+ logic.load ()
+ }
case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
--- a/src/Tools/try.ML Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Tools/try.ML Mon Jul 29 20:51:05 2013 +0200
@@ -120,7 +120,7 @@
(fn {command_name} =>
if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
SOME
- {delay = seconds (Options.default_real @{option auto_time_start}),
+ {delay = SOME (seconds (Options.default_real @{option auto_time_start})),
pri = ~ weight,
persistent = true,
print_fn = fn _ => fn st =>