--- a/src/HOL/Decision_Procs/Approximation.thy Fri Aug 19 19:33:31 2011 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Sat Aug 20 01:21:22 2011 +0200
@@ -839,7 +839,8 @@
cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
+ (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
(is "_ = ?SUM + ?rest / ?fact * ?pow")
- using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`] by auto
+ using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`]
+ unfolding cos_coeff_def by auto
have "cos t * -1^n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
also have "\<dots> = cos (t + n * pi)" using cos_add by auto
@@ -951,7 +952,8 @@
sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
+ (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
(is "_ = ?SUM + ?rest / ?fact * ?pow")
- using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`] by auto
+ using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
+ unfolding sin_coeff_def by auto
have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add left_distrib right_distrib by auto
moreover
@@ -959,7 +961,7 @@
hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
ultimately have even: "even n \<Longrightarrow> 0 \<le> ?rest" and odd: "odd n \<Longrightarrow> 0 \<le> - ?rest " by auto
- have "0 < ?fact" by (rule real_of_nat_fact_gt_zero)
+ have "0 < ?fact" by (simp del: fact_Suc)
have "0 < ?pow" using `0 < real x` by (rule zero_less_power)
{
--- a/src/HOL/Ln.thy Fri Aug 19 19:33:31 2011 +0200
+++ b/src/HOL/Ln.thy Sat Aug 20 01:21:22 2011 +0200
@@ -65,7 +65,7 @@
apply (rule mult_right_mono)
apply (subst inverse_eq_divide)
apply simp
- apply (rule inv_real_of_nat_fact_ge_zero)
+ apply (simp del: fact_Suc)
done
finally show ?thesis .
qed
--- a/src/HOL/MacLaurin.thy Fri Aug 19 19:33:31 2011 +0200
+++ b/src/HOL/MacLaurin.thy Sat Aug 20 01:21:22 2011 +0200
@@ -417,32 +417,33 @@
cos (x + real (m) * pi / 2)"
by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
+lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
+ unfolding sin_coeff_def by simp (* TODO: move *)
+
lemma Maclaurin_sin_expansion2:
"\<exists>t. abs t \<le> abs x &
sin x =
- (\<Sum>m=0..<n. (if even m then 0
- else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
- x ^ m)
+ (\<Sum>m=0..<n. sin_coeff m * x ^ m)
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and x = x
and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
apply safe
apply (simp (no_asm))
apply (simp (no_asm) add: sin_expansion_lemma)
-apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
+apply (force intro!: DERIV_intros)
+apply (subst (asm) setsum_0', clarify, case_tac "a", simp, simp)
+apply (cases n, simp, simp)
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
+apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
done
lemma Maclaurin_sin_expansion:
"\<exists>t. sin x =
- (\<Sum>m=0..<n. (if even m then 0
- else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
- x ^ m)
+ (\<Sum>m=0..<n. sin_coeff m * x ^ m)
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (insert Maclaurin_sin_expansion2 [of x n])
apply (blast intro: elim:)
@@ -452,44 +453,44 @@
"[| n > 0; 0 < x |] ==>
\<exists>t. 0 < t & t < x &
sin x =
- (\<Sum>m=0..<n. (if even m then 0
- else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
- x ^ m)
+ (\<Sum>m=0..<n. sin_coeff m * x ^ m)
+ ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
apply simp
apply (simp (no_asm) add: sin_expansion_lemma)
+apply (force intro!: DERIV_intros)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
+apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
done
lemma Maclaurin_sin_expansion4:
"0 < x ==>
\<exists>t. 0 < t & t \<le> x &
sin x =
- (\<Sum>m=0..<n. (if even m then 0
- else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
- x ^ m)
+ (\<Sum>m=0..<n. sin_coeff m * x ^ m)
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
apply safe
apply simp
apply (simp (no_asm) add: sin_expansion_lemma)
+apply (force intro!: DERIV_intros)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
+apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
done
subsection{*Maclaurin Expansion for Cosine Function*}
+lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
+ unfolding cos_coeff_def by simp (* TODO: move *)
+
lemma sumr_cos_zero_one [simp]:
- "(\<Sum>m=0..<(Suc n).
- (if even m then -1 ^ (m div 2)/(real (fact m)) else 0) * 0 ^ m) = 1"
+ "(\<Sum>m=0..<(Suc n). cos_coeff m * 0 ^ m) = 1"
by (induct "n", auto)
lemma cos_expansion_lemma:
@@ -499,10 +500,7 @@
lemma Maclaurin_cos_expansion:
"\<exists>t. abs t \<le> abs x &
cos x =
- (\<Sum>m=0..<n. (if even m
- then -1 ^ (m div 2)/(real (fact m))
- else 0) *
- x ^ m)
+ (\<Sum>m=0..<n. cos_coeff m * x ^ m)
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
apply safe
@@ -515,17 +513,14 @@
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: cos_zero_iff even_mult_two_ex)
+apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
done
lemma Maclaurin_cos_expansion2:
"[| 0 < x; n > 0 |] ==>
\<exists>t. 0 < t & t < x &
cos x =
- (\<Sum>m=0..<n. (if even m
- then -1 ^ (m div 2)/(real (fact m))
- else 0) *
- x ^ m)
+ (\<Sum>m=0..<n. cos_coeff m * x ^ m)
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
@@ -534,17 +529,14 @@
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: cos_zero_iff even_mult_two_ex)
+apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
done
lemma Maclaurin_minus_cos_expansion:
"[| x < 0; n > 0 |] ==>
\<exists>t. x < t & t < 0 &
cos x =
- (\<Sum>m=0..<n. (if even m
- then -1 ^ (m div 2)/(real (fact m))
- else 0) *
- x ^ m)
+ (\<Sum>m=0..<n. cos_coeff m * x ^ m)
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
apply safe
@@ -553,7 +545,7 @@
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: cos_zero_iff even_mult_two_ex)
+apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
done
(* ------------------------------------------------------------------------- *)
@@ -565,8 +557,8 @@
by auto
lemma Maclaurin_sin_bound:
- "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
- x ^ m)) \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
+ "abs(sin x - (\<Sum>m=0..<n. sin_coeff m * x ^ m))
+ \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
proof -
have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
by (rule_tac mult_right_mono,simp_all)
@@ -592,6 +584,7 @@
apply (safe dest!: mod_eqD, simp_all)
done
show ?thesis
+ unfolding sin_coeff_def
apply (subst t2)
apply (rule sin_bound_lemma)
apply (rule setsum_cong[OF refl])
--- a/src/HOL/Transcendental.thy Fri Aug 19 19:33:31 2011 +0200
+++ b/src/HOL/Transcendental.thy Sat Aug 20 01:21:22 2011 +0200
@@ -618,23 +618,6 @@
qed
-subsection{* Some properties of factorials *}
-
-lemma real_of_nat_fact_not_zero [simp]: "real (fact (n::nat)) \<noteq> 0"
-by auto
-
-lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact (n::nat))"
-by auto
-
-lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact (n::nat))"
-by simp
-
-lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact (n::nat)))"
-by (auto simp add: positive_imp_inverse_positive)
-
-lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact (n::nat)))"
-by (auto intro: order_less_imp_le)
-
subsection {* Derivability of power series *}
lemma DERIV_series': fixes f :: "real \<Rightarrow> nat \<Rightarrow> real"
@@ -820,9 +803,8 @@
subsection {* Exponential Function *}
-definition
- exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
- "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
+definition exp :: "'a \<Rightarrow> 'a::{real_normed_field,banach}" where
+ "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
lemma summable_exp_generic:
fixes x :: "'a::{real_normed_algebra_1,banach}"
@@ -880,14 +862,10 @@
lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
by (simp add: diffs_def)
-lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
-by (auto simp add: exp_def)
-
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
-apply (simp add: exp_def)
-apply (subst lemma_exp_ext)
-apply (subgoal_tac "DERIV (\<lambda>u. \<Sum>n. of_real (inverse (real (fact n))) * u ^ n) x :> (\<Sum>n. diffs (\<lambda>n. of_real (inverse (real (fact n)))) n * x ^ n)")
-apply (rule_tac [2] K = "of_real (1 + norm x)" in termdiffs)
+unfolding exp_def scaleR_conv_of_real
+apply (rule DERIV_cong)
+apply (rule termdiffs [where K="of_real (1 + norm x)"])
apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
apply (simp del: of_real_add)
@@ -1100,120 +1078,93 @@
subsection {* Natural Logarithm *}
-definition
- ln :: "real => real" where
+definition ln :: "real \<Rightarrow> real" where
"ln x = (THE u. exp u = x)"
lemma ln_exp [simp]: "ln (exp x) = x"
-by (simp add: ln_def)
+ by (simp add: ln_def)
lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
-by (auto dest: exp_total)
+ by (auto dest: exp_total)
lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
-apply (rule iffI)
-apply (erule subst, rule exp_gt_zero)
-apply (erule exp_ln)
-done
+ by (metis exp_gt_zero exp_ln)
lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
-by (erule subst, rule ln_exp)
+ by (erule subst, rule ln_exp)
lemma ln_one [simp]: "ln 1 = 0"
-by (rule ln_unique, simp)
+ by (rule ln_unique, simp)
lemma ln_mult: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x * y) = ln x + ln y"
-by (rule ln_unique, simp add: exp_add)
+ by (rule ln_unique, simp add: exp_add)
lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
-by (rule ln_unique, simp add: exp_minus)
+ by (rule ln_unique, simp add: exp_minus)
lemma ln_div: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln (x / y) = ln x - ln y"
-by (rule ln_unique, simp add: exp_diff)
+ by (rule ln_unique, simp add: exp_diff)
lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
-by (rule ln_unique, simp add: exp_real_of_nat_mult)
+ by (rule ln_unique, simp add: exp_real_of_nat_mult)
lemma ln_less_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
-by (subst exp_less_cancel_iff [symmetric], simp)
+ by (subst exp_less_cancel_iff [symmetric], simp)
lemma ln_le_cancel_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
-by (simp add: linorder_not_less [symmetric])
+ by (simp add: linorder_not_less [symmetric])
lemma ln_inj_iff [simp]: "\<lbrakk>0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
-by (simp add: order_eq_iff)
+ by (simp add: order_eq_iff)
lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
-apply (rule exp_le_cancel_iff [THEN iffD1])
-apply (simp add: exp_ge_add_one_self_aux)
-done
+ apply (rule exp_le_cancel_iff [THEN iffD1])
+ apply (simp add: exp_ge_add_one_self_aux)
+ done
lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
-by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
-
-lemma ln_ge_zero [simp]:
- assumes x: "1 \<le> x" shows "0 \<le> ln x"
-proof -
- have "0 < x" using x by arith
- hence "exp 0 \<le> exp (ln x)"
- by (simp add: x)
- thus ?thesis by (simp only: exp_le_cancel_iff)
-qed
-
-lemma ln_ge_zero_imp_ge_one:
- assumes ln: "0 \<le> ln x"
- and x: "0 < x"
- shows "1 \<le> x"
-proof -
- from ln have "ln 1 \<le> ln x" by simp
- thus ?thesis by (simp add: x del: ln_one)
-qed
-
-lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)"
-by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one)
-
-lemma ln_less_zero_iff [simp]: "0 < x ==> (ln x < 0) = (x < 1)"
-by (insert ln_ge_zero_iff [of x], arith)
-
-lemma ln_gt_zero:
- assumes x: "1 < x" shows "0 < ln x"
-proof -
- have "0 < x" using x by arith
- hence "exp 0 < exp (ln x)" by (simp add: x)
- thus ?thesis by (simp only: exp_less_cancel_iff)
-qed
-
-lemma ln_gt_zero_imp_gt_one:
- assumes ln: "0 < ln x"
- and x: "0 < x"
- shows "1 < x"
-proof -
- from ln have "ln 1 < ln x" by simp
- thus ?thesis by (simp add: x del: ln_one)
-qed
-
-lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)"
-by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one)
-
-lemma ln_eq_zero_iff [simp]: "0 < x ==> (ln x = 0) = (x = 1)"
-by (insert ln_less_zero_iff [of x] ln_gt_zero_iff [of x], arith)
-
-lemma ln_less_zero: "[| 0 < x; x < 1 |] ==> ln x < 0"
-by simp
+ by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
+
+lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
+ using ln_le_cancel_iff [of 1 x] by simp
+
+lemma ln_ge_zero_imp_ge_one: "\<lbrakk>0 \<le> ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 \<le> x"
+ using ln_le_cancel_iff [of 1 x] by simp
+
+lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> (0 \<le> ln x) = (1 \<le> x)"
+ using ln_le_cancel_iff [of 1 x] by simp
+
+lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x < 0) = (x < 1)"
+ using ln_less_cancel_iff [of x 1] by simp
+
+lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
+ using ln_less_cancel_iff [of 1 x] by simp
+
+lemma ln_gt_zero_imp_gt_one: "\<lbrakk>0 < ln x; 0 < x\<rbrakk> \<Longrightarrow> 1 < x"
+ using ln_less_cancel_iff [of 1 x] by simp
+
+lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> (0 < ln x) = (1 < x)"
+ using ln_less_cancel_iff [of 1 x] by simp
+
+lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> (ln x = 0) = (x = 1)"
+ using ln_inj_iff [of x 1] by simp
+
+lemma ln_less_zero: "\<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ln x < 0"
+ by simp
lemma exp_ln_eq: "exp u = x ==> ln x = u"
-by auto
+ by (rule ln_unique) (* TODO: delete *)
lemma isCont_ln: "0 < x \<Longrightarrow> isCont ln x"
-apply (subgoal_tac "isCont ln (exp (ln x))", simp)
-apply (rule isCont_inverse_function [where f=exp], simp_all)
-done
+ apply (subgoal_tac "isCont ln (exp (ln x))", simp)
+ apply (rule isCont_inverse_function [where f=exp], simp_all)
+ done
lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
-apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
-apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
-apply (simp_all add: abs_if isCont_ln)
-done
+ apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
+ apply (erule lemma_DERIV_subst [OF DERIV_exp exp_ln])
+ apply (simp_all add: abs_if isCont_ln)
+ done
lemma DERIV_ln_divide: "0 < x ==> DERIV ln x :> 1 / x"
by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
@@ -1253,60 +1204,30 @@
subsection {* Sine and Cosine *}
-definition
- sin_coeff :: "nat \<Rightarrow> real" where
+definition sin_coeff :: "nat \<Rightarrow> real" where
"sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))"
-definition
- cos_coeff :: "nat \<Rightarrow> real" where
+definition cos_coeff :: "nat \<Rightarrow> real" where
"cos_coeff = (\<lambda>n. if even n then (-1 ^ (n div 2)) / real (fact n) else 0)"
-definition
- sin :: "real => real" where
- "sin x = (\<Sum>n. sin_coeff n * x ^ n)"
-
-definition
- cos :: "real => real" where
- "cos x = (\<Sum>n. cos_coeff n * x ^ n)"
+definition sin :: "real \<Rightarrow> real" where
+ "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
+
+definition cos :: "real \<Rightarrow> real" where
+ "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
unfolding sin_coeff_def
-apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
-apply (rule_tac [2] summable_exp)
-apply (rule_tac x = 0 in exI)
+apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
done
lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
unfolding cos_coeff_def
-apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
-apply (rule_tac [2] summable_exp)
-apply (rule_tac x = 0 in exI)
+apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
done
-lemma lemma_STAR_sin:
- "(if even n then 0
- else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos:
- "0 < n -->
- -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos1:
- "0 < n -->
- (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos2:
- "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) * 0 ^ n
- else 0) = 0"
-apply (induct "n")
-apply (case_tac [2] "n", auto)
-done
-
lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
unfolding sin_def by (rule summable_sin [THEN summable_sums])
@@ -1336,22 +1257,15 @@
lemma lemma_sin_minus: "- sin x = (\<Sum>n. - (sin_coeff n * x ^ n))"
by (auto intro!: sums_unique sums_minus sin_converges)
-lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
- by (auto simp add: sin_def)
-
-lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
- by (auto simp add: cos_def)
-
lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
-apply (simp add: cos_def)
-apply (subst lemma_sin_ext)
+unfolding sin_def cos_def
apply (auto simp add: sin_fdiffs2 [symmetric])
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
done
lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
-apply (subst lemma_cos_ext)
+unfolding cos_def
apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
@@ -1378,196 +1292,122 @@
lemma cos_zero [simp]: "cos 0 = 1"
unfolding cos_def cos_coeff_def by (simp add: powser_zero)
-lemma DERIV_sin_sin_mult [simp]:
- "DERIV (%x. sin(x)*sin(x)) x :> cos(x) * sin(x) + cos(x) * sin(x)"
-by (rule DERIV_mult, auto)
-
-lemma DERIV_sin_sin_mult2 [simp]:
- "DERIV (%x. sin(x)*sin(x)) x :> 2 * cos(x) * sin(x)"
-apply (cut_tac x = x in DERIV_sin_sin_mult)
-apply (auto simp add: mult_assoc)
-done
-
-lemma DERIV_sin_realpow2 [simp]:
- "DERIV (%x. (sin x)\<twosuperior>) x :> cos(x) * sin(x) + cos(x) * sin(x)"
-by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
-
-lemma DERIV_sin_realpow2a [simp]:
- "DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)"
-by (auto simp add: numeral_2_eq_2)
-
-lemma DERIV_cos_cos_mult [simp]:
- "DERIV (%x. cos(x)*cos(x)) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
-by (rule DERIV_mult, auto)
-
-lemma DERIV_cos_cos_mult2 [simp]:
- "DERIV (%x. cos(x)*cos(x)) x :> -2 * cos(x) * sin(x)"
-apply (cut_tac x = x in DERIV_cos_cos_mult)
-apply (auto simp add: mult_ac)
-done
-
-lemma DERIV_cos_realpow2 [simp]:
- "DERIV (%x. (cos x)\<twosuperior>) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
-by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
-
-lemma DERIV_cos_realpow2a [simp]:
- "DERIV (%x. (cos x)\<twosuperior>) x :> -2 * cos(x) * sin(x)"
-by (auto simp add: numeral_2_eq_2)
-
lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
-by auto
-
-lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
- by (auto intro!: DERIV_intros)
-
-(* most useful *)
-lemma DERIV_cos_cos_mult3 [simp]:
- "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
- by (auto intro!: DERIV_intros)
-
-lemma DERIV_sin_circle_all:
- "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>
- (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
- by (auto intro!: DERIV_intros)
-
-lemma DERIV_sin_circle_all_zero [simp]:
- "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
-by (cut_tac DERIV_sin_circle_all, auto)
-
-lemma sin_cos_squared_add [simp]: "((sin x)\<twosuperior>) + ((cos x)\<twosuperior>) = 1"
-apply (cut_tac x = x and y = 0 in DERIV_sin_circle_all_zero [THEN DERIV_isconst_all])
-apply (auto simp add: numeral_2_eq_2)
-done
-
-lemma sin_cos_squared_add2 [simp]: "((cos x)\<twosuperior>) + ((sin x)\<twosuperior>) = 1"
-apply (subst add_commute)
-apply (rule sin_cos_squared_add)
-done
+ by (rule DERIV_cong) (* TODO: delete *)
+
+lemma sin_cos_squared_add [simp]: "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1"
+proof -
+ have "\<forall>x. DERIV (\<lambda>x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
+ by (auto intro!: DERIV_intros)
+ hence "(sin x)\<twosuperior> + (cos x)\<twosuperior> = (sin 0)\<twosuperior> + (cos 0)\<twosuperior>"
+ by (rule DERIV_isconst_all)
+ thus "(sin x)\<twosuperior> + (cos x)\<twosuperior> = 1" by simp
+qed
+
+lemma sin_cos_squared_add2 [simp]: "(cos x)\<twosuperior> + (sin x)\<twosuperior> = 1"
+ by (subst add_commute, rule sin_cos_squared_add)
lemma sin_cos_squared_add3 [simp]: "cos x * cos x + sin x * sin x = 1"
-apply (cut_tac x = x in sin_cos_squared_add2)
-apply (simp add: power2_eq_square)
-done
+ using sin_cos_squared_add2 [unfolded power2_eq_square] .
lemma sin_squared_eq: "(sin x)\<twosuperior> = 1 - (cos x)\<twosuperior>"
-apply (rule_tac a1 = "(cos x)\<twosuperior>" in add_right_cancel [THEN iffD1])
-apply simp
-done
+ unfolding eq_diff_eq by (rule sin_cos_squared_add)
lemma cos_squared_eq: "(cos x)\<twosuperior> = 1 - (sin x)\<twosuperior>"
-apply (rule_tac a1 = "(sin x)\<twosuperior>" in add_right_cancel [THEN iffD1])
-apply simp
-done
+ unfolding eq_diff_eq by (rule sin_cos_squared_add2)
lemma abs_sin_le_one [simp]: "\<bar>sin x\<bar> \<le> 1"
-by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
+ by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
lemma sin_ge_minus_one [simp]: "-1 \<le> sin x"
-apply (insert abs_sin_le_one [of x])
-apply (simp add: abs_le_iff del: abs_sin_le_one)
-done
+ using abs_sin_le_one [of x] unfolding abs_le_iff by simp
lemma sin_le_one [simp]: "sin x \<le> 1"
-apply (insert abs_sin_le_one [of x])
-apply (simp add: abs_le_iff del: abs_sin_le_one)
-done
+ using abs_sin_le_one [of x] unfolding abs_le_iff by simp
lemma abs_cos_le_one [simp]: "\<bar>cos x\<bar> \<le> 1"
-by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
+ by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
lemma cos_ge_minus_one [simp]: "-1 \<le> cos x"
-apply (insert abs_cos_le_one [of x])
-apply (simp add: abs_le_iff del: abs_cos_le_one)
-done
+ using abs_cos_le_one [of x] unfolding abs_le_iff by simp
lemma cos_le_one [simp]: "cos x \<le> 1"
-apply (insert abs_cos_le_one [of x])
-apply (simp add: abs_le_iff del: abs_cos_le_one)
-done
+ using abs_cos_le_one [of x] unfolding abs_le_iff by simp
lemma DERIV_fun_pow: "DERIV g x :> m ==>
DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
unfolding One_nat_def
-apply (rule lemma_DERIV_subst)
+apply (rule DERIV_cong)
apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
apply (rule DERIV_pow, auto)
done
lemma DERIV_fun_exp:
"DERIV g x :> m ==> DERIV (%x. exp(g x)) x :> exp(g x) * m"
-apply (rule lemma_DERIV_subst)
+apply (rule DERIV_cong)
apply (rule_tac f = exp in DERIV_chain2)
apply (rule DERIV_exp, auto)
done
lemma DERIV_fun_sin:
"DERIV g x :> m ==> DERIV (%x. sin(g x)) x :> cos(g x) * m"
-apply (rule lemma_DERIV_subst)
+apply (rule DERIV_cong)
apply (rule_tac f = sin in DERIV_chain2)
apply (rule DERIV_sin, auto)
done
lemma DERIV_fun_cos:
"DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m"
-apply (rule lemma_DERIV_subst)
+apply (rule DERIV_cong)
apply (rule_tac f = cos in DERIV_chain2)
apply (rule DERIV_cos, auto)
done
-(* lemma *)
-lemma lemma_DERIV_sin_cos_add:
- "\<forall>x.
- DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
- (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
- by (auto intro!: DERIV_intros simp add: algebra_simps)
-
-lemma sin_cos_add [simp]:
+lemma sin_cos_add_lemma:
"(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
(cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0"
-apply (cut_tac y = 0 and x = x and y7 = y
- in lemma_DERIV_sin_cos_add [THEN DERIV_isconst_all])
-apply (auto simp add: numeral_2_eq_2)
-done
+ (is "?f x = 0")
+proof -
+ have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
+ by (auto intro!: DERIV_intros simp add: algebra_simps)
+ hence "?f x = ?f 0"
+ by (rule DERIV_isconst_all)
+ thus ?thesis by simp
+qed
lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
-apply (cut_tac x = x and y = y in sin_cos_add)
-apply (simp del: sin_cos_add)
-done
+ using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
-apply (cut_tac x = x and y = y in sin_cos_add)
-apply (simp del: sin_cos_add)
-done
-
-lemma lemma_DERIV_sin_cos_minus:
- "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
- by (auto intro!: DERIV_intros simp add: algebra_simps)
-
-
-lemma sin_cos_minus:
- "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
-apply (cut_tac y = 0 and x = x
- in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
-apply simp
-done
+ using sin_cos_add_lemma unfolding realpow_two_sum_zero_iff by simp
+
+lemma sin_cos_minus_lemma:
+ "(sin(-x) + sin(x))\<twosuperior> + (cos(-x) - cos(x))\<twosuperior> = 0" (is "?f x = 0")
+proof -
+ have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
+ by (auto intro!: DERIV_intros simp add: algebra_simps)
+ hence "?f x = ?f 0"
+ by (rule DERIV_isconst_all)
+ thus ?thesis by simp
+qed
lemma sin_minus [simp]: "sin (-x) = -sin(x)"
- using sin_cos_minus [where x=x] by simp
+ using sin_cos_minus_lemma [where x=x] by simp
lemma cos_minus [simp]: "cos (-x) = cos(x)"
- using sin_cos_minus [where x=x] by simp
+ using sin_cos_minus_lemma [where x=x] by simp
lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
-by (simp add: diff_minus sin_add)
+ by (simp add: diff_minus sin_add)
lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
-by (simp add: sin_diff mult_commute)
+ by (simp add: sin_diff mult_commute)
lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
-by (simp add: diff_minus cos_add)
+ by (simp add: diff_minus cos_add)
lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
-by (simp add: cos_diff mult_commute)
+ by (simp add: cos_diff mult_commute)
lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x"
using sin_add [where x=x and y=x] by simp
@@ -1579,8 +1419,7 @@
subsection {* The Constant Pi *}
-definition
- pi :: "real" where
+definition pi :: "real" where
"pi = 2 * (THE x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"};
@@ -1701,7 +1540,8 @@
apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
del: fact_Suc)
apply (rule real_mult_inverse_cancel2)
-apply (rule real_of_nat_fact_gt_zero)+
+apply (simp del: fact_Suc)
+apply (simp del: fact_Suc)
apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
apply (subst fact_lemma)
apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
@@ -2467,7 +2307,7 @@
lemma DERIV_arcsin:
"\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<twosuperior>))"
apply (rule DERIV_inverse_function [where f=sin and a="-1" and b="1"])
-apply (rule lemma_DERIV_subst [OF DERIV_sin])
+apply (rule DERIV_cong [OF DERIV_sin])
apply (simp add: cos_arcsin)
apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
apply (rule power_strict_mono, simp, simp, simp)
@@ -2480,7 +2320,7 @@
lemma DERIV_arccos:
"\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<twosuperior>))"
apply (rule DERIV_inverse_function [where f=cos and a="-1" and b="1"])
-apply (rule lemma_DERIV_subst [OF DERIV_cos])
+apply (rule DERIV_cong [OF DERIV_cos])
apply (simp add: sin_arccos)
apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> < 1\<twosuperior>", simp)
apply (rule power_strict_mono, simp, simp, simp)
@@ -2492,7 +2332,7 @@
lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<twosuperior>)"
apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
-apply (rule lemma_DERIV_subst [OF DERIV_tan])
+apply (rule DERIV_cong [OF DERIV_tan])
apply (rule cos_arctan_not_zero)
apply (simp add: power_inverse tan_sec [symmetric])
apply (subgoal_tac "0 < 1 + x\<twosuperior>", simp)
@@ -2581,8 +2421,8 @@
lemma tan_60: "tan (pi / 3) = sqrt 3"
unfolding tan_def by (simp add: sin_60 cos_60)
-lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
- by (auto intro!: DERIV_intros)
+lemma DERIV_sin_add: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
+ by (auto intro!: DERIV_intros) (* TODO: delete *)
lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
proof -
--- a/src/Pure/Concurrent/future.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Concurrent/future.ML Sat Aug 20 01:21:22 2011 +0200
@@ -31,6 +31,9 @@
that lack regular result information, will pick up parallel
exceptions from the cumulative group context (as Par_Exn).
+ * Future task groups may be canceled: present and future group
+ members will be interrupted eventually.
+
* Promised "passive" futures are fulfilled by external means. There
is no associated evaluation task, but other futures can depend on
them via regular join operations.
@@ -38,31 +41,35 @@
signature FUTURE =
sig
- val worker_task: unit -> Task_Queue.task option
- val worker_group: unit -> Task_Queue.group option
- val worker_subgroup: unit -> Task_Queue.group
+ type task = Task_Queue.task
+ type group = Task_Queue.group
+ val new_group: group option -> group
+ val worker_task: unit -> task option
+ val worker_group: unit -> group option
+ val worker_subgroup: unit -> group
type 'a future
- val task_of: 'a future -> Task_Queue.task
+ val task_of: 'a future -> task
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
val get_finished: 'a future -> 'a
val interruptible_task: ('a -> 'b) -> 'a -> 'b
- val cancel_group: Task_Queue.group -> unit
- val cancel: 'a future -> unit
+ val cancel_group: group -> task list
+ val cancel: 'a future -> task list
type fork_params =
- {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
- pri: int, interrupts: bool}
+ {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
val forks: fork_params -> (unit -> 'a) list -> 'a future list
val fork_pri: int -> (unit -> 'a) -> 'a future
val fork: (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
val join_result: 'a future -> 'a Exn.result
val join: 'a future -> 'a
+ val join_tasks: task list -> unit
+ val value_result: 'a Exn.result -> 'a future
val value: 'a -> 'a future
val map: ('a -> 'b) -> 'a future -> 'b future
val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
- val promise_group: Task_Queue.group -> 'a future
- val promise: unit -> 'a future
+ val promise_group: group -> (unit -> unit) -> 'a future
+ val promise: (unit -> unit) -> 'a future
val fulfill_result: 'a future -> 'a Exn.result -> unit
val fulfill: 'a future -> 'a -> unit
val shutdown: unit -> unit
@@ -74,17 +81,22 @@
(** future values **)
+type task = Task_Queue.task;
+type group = Task_Queue.group;
+val new_group = Task_Queue.new_group;
+
+
(* identifiers *)
local
- val tag = Universal.tag () : Task_Queue.task option Universal.tag;
+ val tag = Universal.tag () : task option Universal.tag;
in
fun worker_task () = the_default NONE (Thread.getLocal tag);
fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x;
end;
val worker_group = Option.map Task_Queue.group_of_task o worker_task;
-fun worker_subgroup () = Task_Queue.new_group (worker_group ());
+fun worker_subgroup () = new_group (worker_group ());
fun worker_joining e =
(case worker_task () of
@@ -103,7 +115,7 @@
datatype 'a future = Future of
{promised: bool,
- task: Task_Queue.task,
+ task: task,
result: 'a result};
fun task_of (Future {task, ...}) = task;
@@ -157,7 +169,7 @@
val queue = Unsynchronized.ref Task_Queue.empty;
val next = Unsynchronized.ref 0;
val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
-val canceled = Unsynchronized.ref ([]: Task_Queue.group list);
+val canceled = Unsynchronized.ref ([]: group list);
val do_shutdown = Unsynchronized.ref false;
val max_workers = Unsynchronized.ref 0;
val max_active = Unsynchronized.ref 0;
@@ -172,15 +184,6 @@
(* cancellation primitives *)
-fun interruptible_task f x =
- if Multithreading.available then
- Multithreading.with_attributes
- (if is_some (worker_task ())
- then Multithreading.private_interrupts
- else Multithreading.public_interrupts)
- (fn _ => f x)
- else interruptible f x;
-
fun cancel_now group = (*requires SYNCHRONIZED*)
Task_Queue.cancel (! queue) group;
@@ -189,6 +192,17 @@
broadcast scheduler_event);
+fun interruptible_task f x =
+ (if Multithreading.available then
+ Multithreading.with_attributes
+ (if is_some (worker_task ())
+ then Multithreading.private_interrupts
+ else Multithreading.public_interrupts)
+ (fn _ => f x)
+ else interruptible f x)
+ before Multithreading.interrupted ();
+
+
(* worker threads *)
fun worker_exec (task, jobs) =
@@ -208,10 +222,10 @@
val _ = SYNCHRONIZED "finish" (fn () =>
let
val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
- val _ = Exn.capture Multithreading.interrupted ();
+ val test = Exn.capture Multithreading.interrupted ();
val _ =
- if ok then ()
- else if cancel_now group then ()
+ if ok andalso not (Exn.is_interrupt_exn test) then ()
+ else if null (cancel_now group) then ()
else cancel_later group;
val _ = broadcast work_finished;
val _ = if maximal then () else signal work_available;
@@ -244,7 +258,7 @@
fun worker_loop name =
(case SYNCHRONIZED name (fn () => worker_next ()) of
NONE => ()
- | SOME work => (Exn.capture Multithreading.interrupted (); worker_exec work; worker_loop name));
+ | SOME work => (worker_exec work; worker_loop name));
fun worker_start name = (*requires SYNCHRONIZED*)
Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
@@ -345,7 +359,7 @@
else
(Multithreading.tracing 1 (fn () =>
string_of_int (length (! canceled)) ^ " canceled groups");
- Unsynchronized.change canceled (filter_out cancel_now);
+ Unsynchronized.change canceled (filter_out (null o cancel_now));
broadcast_work ());
@@ -388,12 +402,15 @@
(** futures **)
-(* cancellation *)
+(* cancel *)
-(*cancel: present and future group members will be interrupted eventually*)
-fun cancel_group group = SYNCHRONIZED "cancel" (fn () =>
- (if cancel_now group then () else cancel_later group;
- signal work_available; scheduler_check ()));
+fun cancel_group group = SYNCHRONIZED "cancel_group" (fn () =>
+ let
+ val running = cancel_now group;
+ val _ =
+ if null running then ()
+ else (cancel_later group; signal work_available; scheduler_check ());
+ in running end);
fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
@@ -430,8 +447,7 @@
Multithreading.with_attributes
(if interrupts
then Multithreading.private_interrupts else Multithreading.no_interrupts)
- (fn _ => Position.setmp_thread_data pos e ()) before
- Multithreading.interrupted ()) ()
+ (fn _ => Position.setmp_thread_data pos e ())) ()
else Exn.interrupt_exn;
in assign_result group result res end;
in (result, job) end;
@@ -440,8 +456,7 @@
(* fork *)
type fork_params =
- {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
- pri: int, interrupts: bool};
+ {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
if null es then []
@@ -469,7 +484,7 @@
end;
fun fork_pri pri e =
- singleton (forks {name = "", group = NONE, deps = [], pri = pri, interrupts = true}) e;
+ (singleton o forks) {name = "fork", group = NONE, deps = [], pri = pri, interrupts = true} e;
fun fork e = fork_pri 0 e;
@@ -521,21 +536,30 @@
fun join_result x = singleton join_results x;
fun join x = Exn.release (join_result x);
+fun join_tasks [] = ()
+ | join_tasks tasks =
+ (singleton o forks)
+ {name = "join_tasks", group = SOME (new_group NONE),
+ deps = tasks, pri = 0, interrupts = false} I
+ |> join;
+
(* fast-path versions -- bypassing task queue *)
-fun value (x: 'a) =
+fun value_result (res: 'a Exn.result) =
let
val task = Task_Queue.dummy_task ();
val group = Task_Queue.group_of_task task;
val result = Single_Assignment.var "value" : 'a result;
- val _ = assign_result group result (Exn.Res x);
+ val _ = assign_result group result res;
in Future {promised = false, task = task, result = result} end;
+fun value x = value_result (Exn.Res x);
+
fun map_future f x =
let
val task = task_of x;
- val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task));
+ val group = new_group (SOME (Task_Queue.group_of_task task));
val (result, job) = future_job group true (fn () => f (join x));
val extended = SYNCHRONIZED "extend" (fn () =>
@@ -545,32 +569,36 @@
in
if extended then Future {promised = false, task = task, result = result}
else
- singleton
- (forks {name = "Future.map", group = SOME group, deps = [task],
- pri = Task_Queue.pri_of_task task, interrupts = true})
+ (singleton o forks)
+ {name = "map_future", group = SOME group, deps = [task],
+ pri = Task_Queue.pri_of_task task, interrupts = true}
(fn () => f (join x))
end;
fun cond_forks args es =
if Multithreading.enabled () then forks args es
- else map (fn e => value (e ())) es;
+ else map (fn e => value_result (Exn.interruptible_capture e ())) es;
(* promised futures -- fulfilled by external means *)
-fun promise_group group : 'a future =
+fun promise_group group abort : 'a future =
let
val result = Single_Assignment.var "promise" : 'a result;
- fun abort () = assign_result group result Exn.interrupt_exn
+ fun assign () = assign_result group result Exn.interrupt_exn
handle Fail _ => true
| exn =>
- if Exn.is_interrupt exn then raise Fail "Concurrent attempt to fulfill promise"
+ if Exn.is_interrupt exn
+ then raise Fail "Concurrent attempt to fulfill promise"
else reraise exn;
+ fun job () =
+ Multithreading.with_attributes Multithreading.no_interrupts
+ (fn _ => assign () before abort ());
val task = SYNCHRONIZED "enqueue_passive" (fn () =>
- Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
+ Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job));
in Future {promised = true, task = task, result = result} end;
-fun promise () = promise_group (worker_subgroup ());
+fun promise abort = promise_group (worker_subgroup ()) abort;
fun fulfill_result (Future {promised, task, result}) res =
if not promised then raise Fail "Not a promised future"
--- a/src/Pure/Concurrent/lazy.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Concurrent/lazy.ML Sat Aug 20 01:21:22 2011 +0200
@@ -57,7 +57,7 @@
val (expr, x) =
Synchronized.change_result var
(fn Expr e =>
- let val x = Future.promise ()
+ let val x = Future.promise I
in ((SOME e, x), Result x) end
| Result x => ((NONE, x), Result x));
in
--- a/src/Pure/Concurrent/par_exn.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Concurrent/par_exn.ML Sat Aug 20 01:21:22 2011 +0200
@@ -22,7 +22,11 @@
fun serial exn =
(case get_exn_serial exn of
SOME i => (i, exn)
- | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
+ | NONE =>
+ let
+ val i = Library.serial ();
+ val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
+ in (i, exn') end);
val the_serial = the o get_exn_serial;
--- a/src/Pure/Concurrent/par_list.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Concurrent/par_list.ML Sat Aug 20 01:21:22 2011 +0200
@@ -34,12 +34,13 @@
then map (Exn.capture f) xs
else
let
- val group = Task_Queue.new_group (Future.worker_group ());
+ val group = Future.new_group (Future.worker_group ());
val futures =
Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
(map (fn x => fn () => f x) xs);
val results = Future.join_results futures
- handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
+ handle exn =>
+ (if Exn.is_interrupt exn then ignore (Future.cancel_group group) else (); reraise exn);
in results end;
fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
--- a/src/Pure/Concurrent/task_queue.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Sat Aug 20 01:21:22 2011 +0200
@@ -31,7 +31,7 @@
val known_task: queue -> task -> bool
val all_passive: queue -> bool
val status: queue -> {ready: int, pending: int, running: int, passive: int}
- val cancel: queue -> group -> bool
+ val cancel: queue -> group -> task list
val cancel_all: queue -> group list
val finish: task -> queue -> bool * queue
val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
@@ -248,10 +248,12 @@
let
val _ = cancel_group group Exn.Interrupt;
val running =
- Tasks.fold (#1 #> get_job jobs #> (fn Running t => insert Thread.equal t | _ => I))
+ Tasks.fold (fn (task, _) =>
+ (case get_job jobs task of Running thread => cons (task, thread) | _ => I))
(get_tasks groups (group_id group)) [];
- val _ = List.app Simple_Thread.interrupt_unsynchronized running;
- in null running end;
+ val threads = fold (insert Thread.equal o #2) running [];
+ val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
+ in map #1 running end;
fun cancel_all (Queue {jobs, ...}) =
let
--- a/src/Pure/General/markup.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/General/markup.ML Sat Aug 20 01:21:22 2011 +0200
@@ -119,6 +119,7 @@
val badN: string val bad: T
val functionN: string
val invoke_scala: string -> string -> Properties.T
+ val cancel_scala: string -> Properties.T
val no_output: Output.output * Output.output
val default_output: T -> Output.output * Output.output
val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -377,6 +378,7 @@
val functionN = "function"
fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
+fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
--- a/src/Pure/General/markup.scala Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/General/markup.scala Sat Aug 20 01:21:22 2011 +0200
@@ -283,6 +283,16 @@
}
}
+ val CANCEL_SCALA = "cancel_scala"
+ object Cancel_Scala
+ {
+ def unapply(props: Properties.T): Option[String] =
+ props match {
+ case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
+ case _ => None
+ }
+ }
+
/* system data */
--- a/src/Pure/Isar/runtime.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Isar/runtime.ML Sat Aug 20 01:21:22 2011 +0200
@@ -119,7 +119,7 @@
else f x;
fun controlled_execution f x =
- ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
+ (f |> debugging |> Future.interruptible_task) x;
fun toplevel_error output_exn f x = f x
handle exn =>
--- a/src/Pure/Isar/toplevel.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML Sat Aug 20 01:21:22 2011 +0200
@@ -419,6 +419,14 @@
(* theory transitions *)
+val global_theory_group =
+ Sign.new_group #>
+ Global_Theory.begin_recent_proofs #> Theory.checkpoint;
+
+val local_theory_group =
+ Local_Theory.new_group #>
+ Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
+
fun generic_theory f = transaction (fn _ =>
(fn Theory (gthy, _) => Theory (f gthy, NONE)
| _ => raise UNDEF));
@@ -426,8 +434,7 @@
fun theory' f = transaction (fn int =>
(fn Theory (Context.Theory thy, _) =>
let val thy' = thy
- |> Sign.new_group
- |> Theory.checkpoint
+ |> global_theory_group
|> f int
|> Sign.reset_group;
in Theory (Context.Theory thy', NONE) end
@@ -454,7 +461,7 @@
let
val finish = loc_finish loc gthy;
val lthy' = loc_begin loc gthy
- |> Local_Theory.new_group
+ |> local_theory_group
|> f int
|> Local_Theory.reset_group;
in Theory (finish lthy', SOME lthy') end
@@ -506,13 +513,13 @@
in
fun local_theory_to_proof' loc f = begin_proof
- (fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy)))
+ (fn int => fn gthy => f int (local_theory_group (loc_begin loc gthy)))
(fn gthy => loc_finish loc gthy o Local_Theory.reset_group);
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
fun theory_to_proof f = begin_proof
- (K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
+ (K (fn Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF))
(K (Context.Theory o Sign.reset_group o Proof_Context.theory_of));
end;
--- a/src/Pure/PIDE/document.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/PIDE/document.ML Sat Aug 20 01:21:22 2011 +0200
@@ -24,7 +24,7 @@
type state
val init_state: state
val join_commands: state -> unit
- val cancel_execution: state -> unit -> unit
+ val cancel_execution: state -> Future.task list
val define_command: command_id -> string -> state -> state
val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
val execute: version_id -> state -> state
@@ -164,7 +164,7 @@
{versions: version Inttab.table, (*version_id -> document content*)
commands: Toplevel.transition future Inttab.table, (*command_id -> transition (future parsing)*)
execs: Toplevel.state lazy Inttab.table, (*exec_id -> execution process*)
- execution: unit future list} (*global execution process*)
+ execution: Future.group} (*global execution process*)
with
fun make_state (versions, commands, execs, execution) =
@@ -177,7 +177,7 @@
make_state (Inttab.make [(no_id, empty_version)],
Inttab.make [(no_id, Future.value Toplevel.empty)],
Inttab.make [(no_id, empty_exec)],
- []);
+ Future.new_group NONE);
(* document versions *)
@@ -200,9 +200,10 @@
map_state (fn (versions, commands, execs, execution) =>
let
val id_string = print_id id;
- val tr = Future.fork_pri 2 (fn () =>
- Position.setmp_thread_data (Position.id_only id_string)
- (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
+ val tr =
+ Future.fork_pri 2 (fn () =>
+ Position.setmp_thread_data (Position.id_only id_string)
+ (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
val commands' =
Inttab.update_new (id, tr) commands
handle Inttab.DUP dup => err_dup "command" dup;
@@ -233,9 +234,7 @@
(* document execution *)
-fun cancel_execution (State {execution, ...}) =
- (List.app Future.cancel execution;
- fn () => ignore (Future.join_results execution));
+fun cancel_execution (State {execution, ...}) = Future.cancel_group execution;
end;
@@ -253,13 +252,13 @@
| NONE => ());
fun async_state tr st =
- ignore
- (singleton
- (Future.forks {name = "Document.async_state",
- group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true})
- (fn () =>
- Toplevel.setmp_thread_position tr
- (fn () => Toplevel.print_state false st) ()));
+ (singleton o Future.forks)
+ {name = "Document.async_state", group = SOME (Future.new_group NONE),
+ deps = [], pri = 0, interrupts = true}
+ (fn () =>
+ Toplevel.setmp_thread_position tr
+ (fn () => Toplevel.print_state false st) ())
+ |> ignore;
fun run int tr st =
(case Toplevel.transition int tr st of
@@ -355,9 +354,9 @@
fun get_command id =
(id, the_command state id |> Future.map (Toplevel.modify_init init));
in
- singleton
- (Future.forks {name = "Document.edit", group = NONE,
- deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false})
+ (singleton o Future.forks)
+ {name = "Document.edit", group = NONE,
+ deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
(fn () =>
let
val prev_exec =
@@ -393,17 +392,16 @@
fun force_exec NONE = ()
| force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
- val execution' =
+ val execution = Future.new_group NONE;
+ val _ =
nodes_of version |> Graph.schedule
(fn deps => fn (name, node) =>
- singleton
- (Future.forks
- {name = "theory:" ^ name, group = NONE,
- deps = map (Future.task_of o #2) deps,
- pri = 1, interrupts = true})
+ (singleton o Future.forks)
+ {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
+ deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
(fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
- in (versions, commands, execs, execution') end);
+ in (versions, commands, execs, execution) end);
--- a/src/Pure/PIDE/isar_document.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML Sat Aug 20 01:21:22 2011 +0200
@@ -30,9 +30,9 @@
fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
end;
- val await_cancellation = Document.cancel_execution state;
+ val running = Document.cancel_execution state;
val (updates, state') = Document.edit old_id new_id edits state;
- val _ = await_cancellation ();
+ val _ = Future.join_tasks running;
val _ = Document.join_commands state';
val _ =
Output.status (Markup.markup (Markup.assign new_id)
--- a/src/Pure/System/invoke_scala.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/System/invoke_scala.ML Sat Aug 20 01:21:22 2011 +0200
@@ -33,7 +33,8 @@
fun promise_method name arg =
let
val id = new_id ();
- val promise = Future.promise () : string future;
+ fun abort () = Output.raw_message (Markup.cancel_scala id) "";
+ val promise = Future.promise abort : string future;
val _ = Synchronized.change promises (Symtab.update (id, promise));
val _ = Output.raw_message (Markup.invoke_scala name id) arg;
in promise end;
--- a/src/Pure/System/session.scala Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/System/session.scala Sat Aug 20 01:21:22 2011 +0200
@@ -275,6 +275,8 @@
val (tag, res) = Invoke_Scala.method(name, arg)
prover.get.invoke_scala(id, tag, res)
}
+ case Markup.Cancel_Scala(id) =>
+ System.err.println("cancel_scala " + id) // FIXME cancel JVM task
case _ =>
if (result.is_syslog) {
reverse_syslog ::= result.message
--- a/src/Pure/Thy/thy_info.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML Sat Aug 20 01:21:22 2011 +0200
@@ -194,11 +194,9 @@
Graph.schedule (fn deps => fn (name, task) =>
(case task of
Task (parents, body) =>
- singleton
- (Future.forks
- {name = "theory:" ^ name, group = NONE,
- deps = map (Future.task_of o #2) deps,
- pri = 0, interrupts = true})
+ (singleton o Future.forks)
+ {name = "theory:" ^ name, group = NONE,
+ deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
(fn () =>
(case filter (not o can Future.join o #2) deps of
[] => body (map (#1 o Future.join) (task_parents deps parents))
--- a/src/Pure/global_theory.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/global_theory.ML Sat Aug 20 01:21:22 2011 +0200
@@ -10,6 +10,8 @@
val intern_fact: theory -> xstring -> string
val defined_fact: theory -> string -> bool
val hide_fact: bool -> string -> theory -> theory
+ val begin_recent_proofs: theory -> theory
+ val join_recent_proofs: theory -> unit
val join_proofs: theory -> unit
val get_fact: Context.generic -> theory -> Facts.ref -> thm list
val get_thms: theory -> xstring -> thm list
@@ -49,10 +51,10 @@
structure Data = Theory_Data
(
- type T = Facts.T * thm list;
- val empty = (Facts.empty, []);
- fun extend (facts, _) = (facts, []);
- fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
+ type T = Facts.T * (thm list * thm list);
+ val empty = (Facts.empty, ([], []));
+ fun extend (facts, _) = (facts, ([], []));
+ fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
);
@@ -68,10 +70,11 @@
(* proofs *)
-fun register_proofs (thy, thms) = (Data.map (apsnd (append thms)) thy, thms);
+fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (append thms))) thy, thms);
-fun join_proofs thy = Thm.join_proofs (rev (#2 (Data.get thy)));
-
+val begin_recent_proofs = Data.map (apsnd (fn (_, thms) => ([], thms)));
+val join_recent_proofs = Thm.join_proofs o rev o #1 o #2 o Data.get;
+val join_proofs = Thm.join_proofs o rev o #2 o #2 o Data.get;
(** retrieve theorems **)
--- a/src/Pure/goal.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/goal.ML Sat Aug 20 01:21:22 2011 +0200
@@ -124,8 +124,8 @@
let
val _ = forked 1;
val future =
- singleton
- (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = false})
+ (singleton o Future.forks)
+ {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
(fn () =>
Exn.release
(Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
--- a/src/Pure/proofterm.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/proofterm.ML Sat Aug 20 01:21:22 2011 +0200
@@ -37,11 +37,11 @@
type oracle = string * term
type pthm = serial * (string * term * proof_body future)
+ val join_body: proof_body -> unit
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
- val join_bodies: proof_body list -> unit
val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
val oracle_ord: oracle * oracle -> order
@@ -171,6 +171,10 @@
type oracle = string * term;
type pthm = serial * (string * term * proof_body future);
+fun join_thm (pthm: pthm) = ignore (Future.join (#3 (#2 pthm)));
+fun join_thms thms = (Future.join_results (map (#3 o #2) thms); List.app join_thm thms);
+fun join_body (PBody {thms, ...}) = join_thms thms;
+
fun proof_of (PBody {proof, ...}) = proof;
val join_proof = Future.join #> proof_of;
@@ -195,18 +199,15 @@
fun fold_body_thms f =
let
fun app (PBody {thms, ...}) =
- (Future.join_results (map (#3 o #2) thms);
- thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
+ tap join_thms thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
if Inttab.defined seen i then (x, seen)
else
let
val body' = Future.join body;
val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
- in (f (name, prop, body') x', seen') end));
+ in (f (name, prop, body') x', seen') end);
in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
-fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
-
fun status_of bodies =
let
fun status (PBody {oracles, thms, ...}) x =
@@ -242,14 +243,13 @@
val all_oracles_of =
let
fun collect (PBody {oracles, thms, ...}) =
- (Future.join_results (map (#3 o #2) thms);
- thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
+ tap join_thms thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
if Inttab.defined seen i then (x, seen)
else
let
val body' = Future.join body;
val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
- in (merge_oracles oracles x', seen') end));
+ in (merge_oracles oracles x', seen') end);
in fn body => #1 (collect body ([], Inttab.empty)) end;
fun approximate_proof_body prf =
@@ -1396,16 +1396,17 @@
| fill _ = NONE;
val (rules, procs) = get_data thy;
val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
+ val _ = join_thms thms;
in PBody {oracles = oracles, thms = thms, proof = proof} end;
fun fulfill_proof_future _ [] postproc body =
if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
else Future.map postproc body
| fulfill_proof_future thy promises postproc body =
- singleton
- (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
- deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
- interrupts = true})
+ (singleton o Future.forks)
+ {name = "Proofterm.fulfill_proof_future", group = NONE,
+ deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
+ interrupts = true}
(fn () =>
postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
@@ -1461,10 +1462,9 @@
if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
else
- singleton
- (Future.forks
- {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1,
- interrupts = true})
+ (singleton o Future.forks)
+ {name = "Proofterm.prepare_thm_proof", group = NONE,
+ deps = [], pri = ~1, interrupts = true}
(make_body0 o full_proof0);
fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
--- a/src/Pure/thm.ML Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Pure/thm.ML Sat Aug 20 01:21:22 2011 +0200
@@ -517,9 +517,9 @@
(map #1 promises ~~ fulfill_bodies (map #2 promises)) body
and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
-val join_proofs = Proofterm.join_bodies o map fulfill_body;
+fun join_proofs thms = ignore (map fulfill_body thms);
-fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm);
+fun proof_body_of thm = (Proofterm.join_body (raw_body thm); fulfill_body thm);
val proof_of = Proofterm.proof_of o proof_body_of;
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Sat Aug 20 01:21:22 2011 +0200
@@ -21,7 +21,6 @@
extends Dockable(view: View, position: String)
{
private val text_area = new TextArea
- text_area.editable = false
set_content(new ScrollPane(text_area))
--- a/src/Tools/jEdit/src/session_dockable.scala Fri Aug 19 19:33:31 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Sat Aug 20 01:21:22 2011 +0200
@@ -28,7 +28,6 @@
readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
private val syslog = new TextArea(Isabelle.session.syslog())
- syslog.editable = false
private val tabs = new TabbedPane {
pages += new TabbedPane.Page("README", Component.wrap(readme))