--- a/Admin/isatest/isatest-makedist Tue Jun 30 19:45:52 2009 +0200
+++ b/Admin/isatest/isatest-makedist Tue Jun 30 22:03:40 2009 +0200
@@ -106,7 +106,7 @@
sleep 15
$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly"
sleep 15
-$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8"
+$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8; $MAKEALL $HOME/settings/mac-poly64-M4"
sleep 15
$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly"
sleep 15
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/settings/mac-poly64-M4 Tue Jun 30 22:03:40 2009 +0200
@@ -0,0 +1,28 @@
+# -*- shell-script -*- :mode=shellscript:
+
+ POLYML_HOME="/home/polyml/polyml-svn"
+ ML_SYSTEM="polyml-experimental"
+ ML_PLATFORM="x86_64-darwin"
+ ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ ML_OPTIONS="--mutable 2000 --immutable 2000"
+
+
+ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
+
+# Where to look for isabelle tools (multiple dirs separated by ':').
+ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
+
+# Location for temporary files (should be on a local file system).
+ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
+
+
+# Heap input locations. ML system identifier is included in lookup.
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
+
+# Heap output location. ML system identifier is appended automatically later on.
+ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
+ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
+
+ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
+
+HOL_USEDIR_OPTIONS="-p 2 -Q false"
--- a/NEWS Tue Jun 30 19:45:52 2009 +0200
+++ b/NEWS Tue Jun 30 22:03:40 2009 +0200
@@ -75,6 +75,14 @@
* "approximate" supports now arithmetic expressions as boundaries of intervals and implements
interval splitting and taylor series expansion.
+* Changed DERIV_intros to a NamedThmsFun. Each of the theorems in DERIV_intros
+assumes composition with an additional function and matches a variable to the
+derivative, which has to be solved by the simplifier. Hence
+(auto intro!: DERIV_intros) computes the derivative of most elementary terms.
+
+* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are replaced by:
+(auto intro!: DERIV_intros)
+INCOMPATIBILITY.
*** ML ***
--- a/src/HOL/Decision_Procs/Approximation.thy Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue Jun 30 22:03:40 2009 +0200
@@ -2670,11 +2670,6 @@
"DERIV_floatarith x (Num f) = Num 0" |
"DERIV_floatarith x (Atom n) = (if x = n then Num 1 else Num 0)"
-lemma DERIV_chain'': "\<lbrakk>DERIV g (f x) :> E ; DERIV f x :> D; x' = E * D \<rbrakk> \<Longrightarrow>
- DERIV (\<lambda>x. g (f x)) x :> x'" using DERIV_chain' by auto
-
-lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = X' \<rbrakk> \<Longrightarrow> DERIV f x :> X'" by simp
-
lemma DERIV_floatarith:
assumes "n < length vs"
assumes isDERIV: "isDERIV n f (vs[n := x])"
@@ -2682,31 +2677,20 @@
interpret_floatarith (DERIV_floatarith n f) (vs[n := x])"
(is "DERIV (?i f) x :> _")
using isDERIV proof (induct f arbitrary: x)
- case (Add a b) thus ?case by (auto intro: DERIV_add)
-next case (Mult a b) thus ?case by (auto intro!: DERIV_mult[THEN DERIV_cong])
-next case (Minus a) thus ?case by (auto intro!: DERIV_minus[THEN DERIV_cong])
-next case (Inverse a) thus ?case
- by (auto intro!: DERIV_inverse_fun[THEN DERIV_cong] DERIV_inverse[THEN DERIV_cong]
+ case (Inverse a) thus ?case
+ by (auto intro!: DERIV_intros
simp add: algebra_simps power2_eq_square)
next case (Cos a) thus ?case
- by (auto intro!: DERIV_chain''[of cos "?i a"]
- DERIV_cos[THEN DERIV_cong]
+ by (auto intro!: DERIV_intros
simp del: interpret_floatarith.simps(5)
simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a])
-next case (Arctan a) thus ?case
- by (auto intro!: DERIV_chain''[of arctan "?i a"] DERIV_arctan[THEN DERIV_cong])
-next case (Exp a) thus ?case
- by (auto intro!: DERIV_chain''[of exp "?i a"] DERIV_exp[THEN DERIV_cong])
next case (Power a n) thus ?case
- by (cases n, auto intro!: DERIV_power_Suc[THEN DERIV_cong]
+ by (cases n, auto intro!: DERIV_intros
simp del: power_Suc simp add: real_eq_of_nat)
-next case (Sqrt a) thus ?case
- by (auto intro!: DERIV_chain''[of sqrt "?i a"] DERIV_real_sqrt[THEN DERIV_cong])
next case (Ln a) thus ?case
- by (auto intro!: DERIV_chain''[of ln "?i a"] DERIV_ln[THEN DERIV_cong]
- simp add: divide_inverse)
+ by (auto intro!: DERIV_intros simp add: divide_inverse)
next case (Atom i) thus ?case using `n < length vs` by auto
-qed auto
+qed (auto intro!: DERIV_intros)
declare approx.simps[simp del]
--- a/src/HOL/Deriv.thy Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/Deriv.thy Tue Jun 30 22:03:40 2009 +0200
@@ -115,12 +115,16 @@
text{*Differentiation of finite sum*}
+lemma DERIV_setsum:
+ assumes "finite S"
+ and "\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x :> (f' x n)"
+ shows "DERIV (%x. setsum (f x) S) x :> setsum (f' x) S"
+ using assms by induct (auto intro!: DERIV_add)
+
lemma DERIV_sumr [rule_format (no_asm)]:
"(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
--> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
-apply (induct "n")
-apply (auto intro: DERIV_add)
-done
+ by (auto intro: DERIV_setsum)
text{*Alternative definition for differentiability*}
@@ -216,7 +220,6 @@
shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
-
text {* Caratheodory formulation of derivative at a point *}
lemma CARAT_DERIV:
@@ -308,6 +311,30 @@
lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
by auto
+text {* DERIV_intros *}
+
+ML{*
+structure DerivIntros =
+ NamedThmsFun(val name = "DERIV_intros"
+ val description = "DERIV introduction rules");
+*}
+setup DerivIntros.setup
+
+lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
+ by simp
+
+declare
+ DERIV_const[THEN DERIV_cong, DERIV_intros]
+ DERIV_ident[THEN DERIV_cong, DERIV_intros]
+ DERIV_add[THEN DERIV_cong, DERIV_intros]
+ DERIV_minus[THEN DERIV_cong, DERIV_intros]
+ DERIV_mult[THEN DERIV_cong, DERIV_intros]
+ DERIV_diff[THEN DERIV_cong, DERIV_intros]
+ DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
+ DERIV_divide[THEN DERIV_cong, DERIV_intros]
+ DERIV_power[where 'a=real, THEN DERIV_cong,
+ unfolded real_of_nat_def[symmetric], DERIV_intros]
+ DERIV_setsum[THEN DERIV_cong, DERIV_intros]
subsection {* Differentiability predicate *}
--- a/src/HOL/Library/Poly_Deriv.thy Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/Library/Poly_Deriv.thy Tue Jun 30 22:03:40 2009 +0200
@@ -85,13 +85,7 @@
by (rule lemma_DERIV_subst, rule DERIV_add, auto)
lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
-apply (induct p)
-apply simp
-apply (simp add: pderiv_pCons)
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_add DERIV_mult DERIV_const DERIV_ident | assumption)+
-apply simp
-done
+ by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons)
text{* Consequences of the derivative theorem above*}
--- a/src/HOL/Ln.thy Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/Ln.thy Tue Jun 30 22:03:40 2009 +0200
@@ -343,43 +343,7 @@
done
lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
- apply (unfold deriv_def, unfold LIM_eq, clarsimp)
- apply (rule exI)
- apply (rule conjI)
- prefer 2
- apply clarsimp
- apply (subgoal_tac "(ln (x + xa) - ln x) / xa - (1 / x) =
- (ln (1 + xa / x) - xa / x) / xa")
- apply (erule ssubst)
- apply (subst abs_divide)
- apply (rule mult_imp_div_pos_less)
- apply force
- apply (rule order_le_less_trans)
- apply (rule abs_ln_one_plus_x_minus_x_bound)
- apply (subst abs_divide)
- apply (subst abs_of_pos, assumption)
- apply (erule mult_imp_div_pos_le)
- apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
- apply force
- apply assumption
- apply (simp add: power2_eq_square mult_compare_simps)
- apply (rule mult_imp_div_pos_less)
- apply (rule mult_pos_pos, assumption, assumption)
- apply (subgoal_tac "xa * xa = abs xa * abs xa")
- apply (erule ssubst)
- apply (subgoal_tac "abs xa * (abs xa * 2) < abs xa * (r * (x * x))")
- apply (simp only: mult_ac)
- apply (rule mult_strict_left_mono)
- apply (erule conjE, assumption)
- apply force
- apply simp
- apply (subst ln_div [THEN sym])
- apply arith
- apply (auto simp add: algebra_simps add_frac_eq frac_eq_eq
- add_divide_distrib power2_eq_square)
- apply (rule mult_pos_pos, assumption)+
- apply assumption
-done
+ by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"
proof -
--- a/src/HOL/MacLaurin.thy Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/MacLaurin.thy Tue Jun 30 22:03:40 2009 +0200
@@ -27,36 +27,6 @@
lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
by arith
-text{*A crude tactic to differentiate by proof.*}
-
-lemmas deriv_rulesI =
- DERIV_ident DERIV_const DERIV_cos DERIV_cmult
- DERIV_sin DERIV_exp DERIV_inverse DERIV_pow
- DERIV_add DERIV_diff DERIV_mult DERIV_minus
- DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
- DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
- DERIV_ident DERIV_const DERIV_cos
-
-ML
-{*
-local
-exception DERIV_name;
-fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
-| get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
-| get_fun_name _ = raise DERIV_name;
-
-in
-
-fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
- resolve_tac @{thms deriv_rulesI} i ORELSE
- ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)]
- @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
-
-fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
-
-end
-*}
-
lemma Maclaurin_lemma2:
assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
assumes n: "n = Suc k"
@@ -91,13 +61,12 @@
apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
apply (rule DERIV_cmult)
apply (rule lemma_DERIV_subst)
- apply (best intro: DERIV_chain2 intro!: DERIV_intros)
+ apply (best intro!: DERIV_intros)
apply (subst fact_Suc)
apply (subst real_of_nat_mult)
apply (simp add: mult_ac)
done
-
lemma Maclaurin:
assumes h: "0 < h"
assumes n: "0 < n"
@@ -565,9 +534,7 @@
apply (clarify)
apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
apply (cut_tac m=m in mod_exhaust_less_4)
- apply (safe, simp_all)
- apply (rule DERIV_minus, simp)
- apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
+ apply (safe, auto intro!: DERIV_intros)
done
from Maclaurin_all_le [OF diff_0 DERIV_diff]
obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
--- a/src/HOL/NthRoot.thy Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/NthRoot.thy Tue Jun 30 22:03:40 2009 +0200
@@ -372,6 +372,41 @@
using odd_pos [OF n] by (rule isCont_real_root)
qed
+lemma DERIV_even_real_root:
+ assumes n: "0 < n" and "even n"
+ assumes x: "x < 0"
+ shows "DERIV (root n) x :> inverse (- real n * root n x ^ (n - Suc 0))"
+proof (rule DERIV_inverse_function)
+ show "x - 1 < x" by simp
+ show "x < 0" using x .
+next
+ show "\<forall>y. x - 1 < y \<and> y < 0 \<longrightarrow> - (root n y ^ n) = y"
+ proof (rule allI, rule impI, erule conjE)
+ fix y assume "x - 1 < y" and "y < 0"
+ hence "root n (-y) ^ n = -y" using `0 < n` by simp
+ with real_root_minus[OF `0 < n`] and `even n`
+ show "- (root n y ^ n) = y" by simp
+ qed
+next
+ show "DERIV (\<lambda>x. - (x ^ n)) (root n x) :> - real n * root n x ^ (n - Suc 0)"
+ by (auto intro!: DERIV_intros)
+ show "- real n * root n x ^ (n - Suc 0) \<noteq> 0"
+ using n x by simp
+ show "isCont (root n) x"
+ using n by (rule isCont_real_root)
+qed
+
+lemma DERIV_real_root_generic:
+ assumes "0 < n" and "x \<noteq> 0"
+ and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+ and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
+ and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+ shows "DERIV (root n) x :> D"
+using assms by (cases "even n", cases "0 < x",
+ auto intro: DERIV_real_root[THEN DERIV_cong]
+ DERIV_odd_real_root[THEN DERIV_cong]
+ DERIV_even_real_root[THEN DERIV_cong])
+
subsection {* Square Root *}
definition
@@ -456,9 +491,21 @@
lemma isCont_real_sqrt: "isCont sqrt x"
unfolding sqrt_def by (rule isCont_real_root [OF pos2])
+lemma DERIV_real_sqrt_generic:
+ assumes "x \<noteq> 0"
+ assumes "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2"
+ assumes "x < 0 \<Longrightarrow> D = - inverse (sqrt x) / 2"
+ shows "DERIV sqrt x :> D"
+ using assms unfolding sqrt_def
+ by (auto intro!: DERIV_real_root_generic)
+
lemma DERIV_real_sqrt:
"0 < x \<Longrightarrow> DERIV sqrt x :> inverse (sqrt x) / 2"
-unfolding sqrt_def by (rule DERIV_real_root [OF pos2, simplified])
+ using DERIV_real_sqrt_generic by simp
+
+declare
+ DERIV_real_sqrt_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_real_root_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
apply auto
--- a/src/HOL/Transcendental.thy Tue Jun 30 19:45:52 2009 +0200
+++ b/src/HOL/Transcendental.thy Tue Jun 30 22:03:40 2009 +0200
@@ -784,9 +784,8 @@
also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult real_mult_assoc[symmetric] by algebra
finally show ?thesis .
qed }
- { fix n
- from DERIV_pow[of "Suc n" x0, THEN DERIV_cmult[where c="f n"]]
- show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)" unfolding real_mult_assoc by auto }
+ { fix n show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
+ by (auto intro!: DERIV_intros simp del: power_Suc) }
{ fix x assume "x \<in> {-R' <..< R'}" hence "R' \<in> {-R <..< R}" and "norm x < norm R'" using assms `R' < R` by auto
have "summable (\<lambda> n. f n * x^n)"
proof (rule summable_le2[THEN conjunct1, OF _ powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`]], rule allI)
@@ -1362,6 +1361,12 @@
by (rule DERIV_cos [THEN DERIV_isCont])
+declare
+ DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_ln[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+
subsection {* Properties of Sine and Cosine *}
lemma sin_zero [simp]: "sin 0 = 0"
@@ -1410,24 +1415,17 @@
by auto
lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_cos_realpow2a, auto)
-done
+ 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))"
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_cos_cos_mult2, auto)
-done
+ 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))"
-apply (simp only: diff_minus, safe)
-apply (rule DERIV_add)
-apply (auto simp add: numeral_2_eq_2)
-done
+ by (auto intro!: DERIV_intros)
lemma DERIV_sin_circle_all_zero [simp]:
"\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
@@ -1513,22 +1511,12 @@
apply (rule DERIV_cos, auto)
done
-lemmas DERIV_intros = DERIV_ident DERIV_const DERIV_cos DERIV_cmult
- DERIV_sin DERIV_exp DERIV_inverse DERIV_pow
- DERIV_add DERIV_diff DERIV_mult DERIV_minus
- DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
- DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
-
(* 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"
-apply (safe, rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)
- --{*replaces the old @{text DERIV_tac}*}
-apply (auto simp add: algebra_simps)
-done
+ by (auto intro!: DERIV_intros simp add: algebra_simps)
lemma sin_cos_add [simp]:
"(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
@@ -1550,10 +1538,8 @@
lemma lemma_DERIV_sin_cos_minus:
"\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
-apply (safe, rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)
-apply (simp add: algebra_simps)
-done
+ by (auto intro!: DERIV_intros simp add: algebra_simps)
+
lemma sin_cos_minus:
"(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
@@ -1722,7 +1708,7 @@
apply (assumption, rule_tac y=y in order_less_le_trans, simp_all)
apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all)
done
-
+
lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
by (simp add: pi_def)
@@ -2121,10 +2107,7 @@
lemma lemma_DERIV_tan:
"cos x \<noteq> 0 ==> DERIV (%x. sin(x)/cos(x)) x :> inverse((cos x)\<twosuperior>)"
-apply (rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)
-apply (auto simp add: divide_inverse numeral_2_eq_2)
-done
+ by (auto intro!: DERIV_intros simp add: field_simps numeral_2_eq_2)
lemma DERIV_tan [simp]: "cos x \<noteq> 0 ==> DERIV tan x :> inverse((cos x)\<twosuperior>)"
by (auto dest: lemma_DERIV_tan simp add: tan_def [symmetric])
@@ -2500,6 +2483,11 @@
apply (simp, simp, simp, rule isCont_arctan)
done
+declare
+ DERIV_arcsin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_arccos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+ DERIV_arctan[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+
subsection {* More Theorems about Sin and Cos *}
lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
@@ -2589,11 +2577,7 @@
by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
-apply (rule lemma_DERIV_subst)
-apply (rule_tac f = sin and g = "%x. x + k" in DERIV_chain2)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)+
-apply (simp (no_asm))
-done
+ by (auto intro!: DERIV_intros)
lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
proof -
@@ -2634,11 +2618,7 @@
by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
-apply (rule lemma_DERIV_subst)
-apply (rule_tac f = cos and g = "%x. x + k" in DERIV_chain2)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)+
-apply (simp (no_asm))
-done
+ by (auto intro!: DERIV_intros)
lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
by (auto simp add: sin_zero_iff even_mult_two_ex)
--- a/src/Pure/General/swing.scala Tue Jun 30 19:45:52 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-/* Title: Pure/General/swing.scala
- Author: Makarius
-
-Swing utilities.
-*/
-
-package isabelle
-
-import javax.swing.SwingUtilities
-
-object Swing
-{
- def now[A](body: => A): A = {
- var result: Option[A] = None
- if (SwingUtilities.isEventDispatchThread) { result = Some(body) }
- else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
- result.get
- }
-
- def later(body: => Unit) {
- if (SwingUtilities.isEventDispatchThread) body
- else SwingUtilities.invokeLater(new Runnable { def run = body })
- }
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/swing_thread.scala Tue Jun 30 22:03:40 2009 +0200
@@ -0,0 +1,24 @@
+/* Title: Pure/General/swing_thread.scala
+ Author: Makarius
+
+Evaluation within the AWT/Swing thread.
+*/
+
+package isabelle
+
+import javax.swing.SwingUtilities
+
+object Swing_Thread
+{
+ def now[A](body: => A): A = {
+ var result: Option[A] = None
+ if (SwingUtilities.isEventDispatchThread) { result = Some(body) }
+ else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
+ result.get
+ }
+
+ def later(body: => Unit) {
+ if (SwingUtilities.isEventDispatchThread) body
+ else SwingUtilities.invokeLater(new Runnable { def run = body })
+ }
+}
--- a/src/Pure/IsaMakefile Tue Jun 30 19:45:52 2009 +0200
+++ b/src/Pure/IsaMakefile Tue Jun 30 22:03:40 2009 +0200
@@ -118,7 +118,7 @@
## Scala material
SCALA_FILES = General/event_bus.scala General/markup.scala \
- General/position.scala General/scan.scala General/swing.scala \
+ General/position.scala General/scan.scala General/swing_thread.scala \
General/symbol.scala General/xml.scala General/yxml.scala \
Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala \
System/cygwin.scala System/gui_setup.scala \
--- a/src/Pure/System/gui_setup.scala Tue Jun 30 19:45:52 2009 +0200
+++ b/src/Pure/System/gui_setup.scala Tue Jun 30 22:03:40 2009 +0200
@@ -16,7 +16,7 @@
{
def main(args: Array[String]) =
{
- Swing.later {
+ Swing_Thread.later {
UIManager.setLookAndFeel(Platform.look_and_feel)
top.pack()
top.visible = true