# HG changeset patch # User wenzelm # Date 1375123865 -7200 # Node ID 4b6b71fb00d55bf6eb097b99701d7c8742e590cb # Parent 7ffcd6f2890dce47a745ef5d1c7b0e58715fc7ec# Parent 82707f95a7839abda0eade9198216e5f36a5ffdb merged diff -r 7ffcd6f2890d -r 4b6b71fb00d5 NEWS --- 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. diff -r 7ffcd6f2890d -r 4b6b71fb00d5 etc/options --- 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" diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/HOL/Decision_Procs/Polynomial_List.thy --- 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 \ (\x. p \ [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 = (\q. poly p2 = poly(p1 *** q))" +definition divides :: "[('a::comm_ring_1) list, 'a list] => bool" (infixl "divides" 70) + where "p1 divides p2 = (\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 \ poly [] & (\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 "\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 "\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]: "\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]: - "\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]: "\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 "\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 "\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 "\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 "\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: "\h. \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: "\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 = []) | (\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: "\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]: "\h k a. length (k %* p +++ (h # (a %* p))) = Suc (length p)" + by (induct p) auto -lemma lemma_poly_length_mult2: "\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]: "\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]: - "\p2. length (p1 +++ p2) = - (if (length p1 < length p2) then length p2 else length p1)" -apply (induct "p1", simp_all) -apply arith -done + "\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 \ poly [] x) = - (poly p x \ poly [] x & poly q x \ 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 \ poly [] x) = + (poly p x \ poly [] x & poly q x \ 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]: "\p x. poly p x \ poly [] x & length p = n --> (\i. \x. (poly p x = (0::'a::idom)) --> (\m. (m \ n & x = i m)))" -apply (induct "n", safe) -apply (rule ccontr) -apply (subgoal_tac "\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 "\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) \ poly [] x ==> - \i. \x. (poly p x = 0) --> (\n. n \ length p & x = i n)" -by (blast intro: poly_roots_index_lemma1) +lemma poly_roots_index_length0: + "poly p (x::'a::idom) \ poly [] x \ + \i. \x. (poly p x = 0) \ (\n. n \ length p & x = i n)" + by (blast intro: poly_roots_index_lemma1) -lemma poly_roots_finite_lemma: "poly p (x::'a::idom) \ poly [] x ==> - \N i. \x. (poly p x = 0) --> (\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) \ poly [] x \ + \N i. \x. (poly p x = 0) \ (\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: "\x. P x --> (\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 \ ?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]: - "\p x. poly p x \ poly [] x & length p = n - --> (\i. \x. (poly p x = (0::'a::{idom})) --> x \ set i)" -apply (induct "n", safe) -apply (rule ccontr) -apply (subgoal_tac "\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 + "\p x. poly p x \ poly [] x & length p = n + \ (\i. \x. (poly p x = (0::'a::{idom})) \ x \ set i)" + apply (induct "n", safe) + apply (rule ccontr) + apply (subgoal_tac "\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) \ poly [] x ==> - \i. \x. (poly p x = 0) --> x \ set i" -by (blast intro: poly_roots_index_lemma2) +lemma poly_roots_index_length: + "poly p (x::'a::idom) \ poly [] x \ + \i. \x. (poly p x = 0) --> x \ set i" + by (blast intro: poly_roots_index_lemma2) -lemma poly_roots_finite_lemma': "poly p (x::'a::idom) \ poly [] x ==> - \i. \x. (poly p x = 0) --> x \ set i" -by (drule poly_roots_index_length, safe) +lemma poly_roots_finite_lemma': + "poly p (x::'a::idom) \ poly [] x \ + \i. \x. (poly p x = 0) --> x \ set i" + apply (drule poly_roots_index_length) + apply auto + done lemma UNIV_nat_infinite: "\ 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 \ 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 "\x. \xa f xa" by auto} + { assume "n =0" hence "\x. \xa f xa" by auto } moreover - {assume nz: "n \ 0" - hence thne: "?fN \ {}" by (auto simp add: neq0_conv) + { assume nz: "n \ 0" + hence thne: "?fN \ {}" by auto have "\x\ ?fN. Max ?fN \ x" using nz Max_ge_iff[OF thfN thne] by auto hence "\x\ ?fN. ?y > x" by (auto simp add: less_Suc_eq_le) hence "?y \ ?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 \ '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 \ poly []) = - finite {x. poly p x = (0::'a::{idom, ring_char_0})}" +lemma poly_roots_finite: "(poly p \ poly []) = finite {x. poly p x = (0::'a::{idom, ring_char_0})}" proof assume H: "poly p \ 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: "\ finite {x. poly p x = (0\'a)}" + assume F: "\ finite {x. poly p x = (0\'a)}" and P: "\x. poly p x = (0\'a) \ x \ set i" let ?M= "{x. poly p x = (0\'a)}" from P have "?M \ set i" by auto with finite_subset F show False by auto qed next - assume F: "finite {x. poly p x = (0\'a)}" - show "poly p \ poly []" using F UNIV_ring_char_0_infinte by auto + assume "finite {x. poly p x = (0\'a)}" + then show "poly p \ 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) \ poly [] ; poly q \ poly [] |] - ==> poly (p *** q) \ 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) \ poly [] \ poly q \ poly [] \ + poly (p *** q) \ 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) \ poly ([]::('a::{idom,ring_char_0}) list)) = ((poly p \ poly []) & (poly q \ poly []))" -by (simp add: poly_entire) +lemma poly_entire_neg: + "(poly (p *** q) \ poly ([]::('a::{idom,ring_char_0}) list)) = + ((poly p \ poly []) & (poly q \ poly []))" + by (simp add: poly_entire) -lemma fun_eq: " (f = g) = (\x. f x = g x)" -by (auto intro!: ext) +lemma fun_eq: "f = g \ (\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 \ 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 \ 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)] \ 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)] \ 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) \ poly [])" -by auto -declare poly_exp_prime_eq_zero [simp] +lemma poly_exp_prime_eq_zero [simp]: "(poly ([a, (1::'a::idom)] %^ n) \ 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 [] \ 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: "\x. x = (0\'a) \ poly t x = (0\'a)" and pnz: "poly t \ 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\'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 \ 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_exp: "m \ 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 \ 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_exp_divides: "[| (p %^ n) divides q; m\n |] ==> (p %^ m) divides q" -by (blast intro: poly_divides_exp poly_divides_trans) +lemma poly_exp_divides: "(p %^ n) divides q \ m \ n \ (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 \ 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_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 \ 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 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]: - "\p. length p = d --> poly p \ poly [] - --> (\n q. p = mulexp n [-a, (1::'a::{idom,ring_char_0})] q & poly q a \ 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 + "\p. length p = d \ poly p \ poly [] \ + (\n q. p = mulexp n [-a, (1::'a::{idom,ring_char_0})] q & poly q a \ 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 \ poly [] |] ==> \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) \ 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) \ 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 \ 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 \ 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 \ 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 order_unique: "[| poly p \ 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 \ 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]: - "\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 + "\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 \ 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 \ 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 \ poly [] - ==> \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 \ poly [] \ + \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) \ 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) \ 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_root2: "poly p \ poly [] ==> (poly p a = 0) = (order (a::'a::{idom,ring_char_0}) p \ 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}) |] - ==> \q. (poly p = poly ([-a, 1] *** q)) & poly q a \ 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}) |] + ==> \q. (poly p = poly ([-a, 1] *** q)) & poly q a \ 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 \ pnormalize p = []" -by (induct "p", auto) +lemma lemma_degree_zero: "list_all (%c. c = 0) p \ pnormalize p = []" + by (induct p) auto lemma degree_zero: "(poly p = poly ([]:: (('a::{idom,ring_char_0}) list))) \ (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]) \ x \ 0" by simp + lemma pnormalize_pair: "y \ 0 \ (pnormalize [x, y] = [x, y])" by simp -lemma pnormal_cons: "pnormal p \ pnormal (c#p)" + +lemma pnormal_cons: "pnormal p \ pnormal (c#p)" unfolding pnormal_def by simp + lemma pnormal_tail: "p\[] \ pnormal (c#p) \ 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 \ 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 \ 0 < length p" unfolding pnormal_def length_greater_0_conv by blast + lemma pnormal_last_length: "\0 < length p ; last p \ 0\ \ 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 \ (0 < length p \ last p \ 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 \ poly [] ==> finite {x::'a::{idom,ring_char_0}. poly p x = 0}" -unfolding poly_roots_finite . +lemma poly_roots_finite_set: + "poly p \ poly [] \ finite {x::'a::{idom,ring_char_0}. poly p x = 0}" + unfolding poly_roots_finite . text{*bound for polynomial.*} lemma poly_mono: "abs(x) \ k ==> abs(poly p (x::'a::{linordered_idom})) \ 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 diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Pure/Concurrent/future.ML --- 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" diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Pure/PIDE/command.ML --- 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; diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Pure/PIDE/document.ML --- 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'; diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Pure/PIDE/execution.ML --- 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; diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Pure/PIDE/protocol.ML --- 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; diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Pure/PIDE/protocol.scala --- 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]) { diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Pure/System/isabelle_process.ML --- 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; diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Pure/System/session.scala --- 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) } diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Pure/goal.ML --- 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 (); diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Tools/jEdit/src/actions.xml --- 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"); - + - isabelle.jedit.PIDE.check_buffer(buffer); + isabelle.jedit.PIDE.execution_range_none(); - + - isabelle.jedit.PIDE.cancel_execution(); + isabelle.jedit.PIDE.execution_range_visible(); diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Tools/jEdit/src/document_model.scala --- 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 */ diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Tools/jEdit/src/document_view.scala diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Tools/jEdit/src/jEdit.props --- 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 diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Tools/jEdit/src/plugin.scala --- 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) } diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Tools/jEdit/src/raw_output_dockable.scala --- 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) } diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Tools/jEdit/src/theories_dockable.scala --- 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)) diff -r 7ffcd6f2890d -r 4b6b71fb00d5 src/Tools/try.ML --- 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 =>