# HG changeset patch # User huffman # Date 1179811789 -7200 # Node ID cdfff0241c12c9ef37c713a06e48733627b15602 # Parent 88bfbe03182028227b99285772e21e678faf264d rename lemmas LIM_ident, isCont_ident, DERIV_ident diff -r 88bfbe031820 -r cdfff0241c12 src/HOL/Complex/CLim.thy --- a/src/HOL/Complex/CLim.thy Tue May 22 05:07:48 2007 +0200 +++ b/src/HOL/Complex/CLim.thy Tue May 22 07:29:49 2007 +0200 @@ -152,7 +152,7 @@ lemma CDERIV_pow [simp]: "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))" apply (induct_tac "n") -apply (drule_tac [2] DERIV_Id [THEN DERIV_mult]) +apply (drule_tac [2] DERIV_ident [THEN DERIV_mult]) apply (auto simp add: left_distrib real_of_nat_Suc) apply (case_tac "n") apply (auto simp add: mult_ac add_commute) diff -r 88bfbe031820 -r cdfff0241c12 src/HOL/Hyperreal/Deriv.thy --- a/src/HOL/Hyperreal/Deriv.thy Tue May 22 05:07:48 2007 +0200 +++ b/src/HOL/Hyperreal/Deriv.thy Tue May 22 07:29:49 2007 +0200 @@ -47,7 +47,7 @@ lemma DERIV_const [simp]: "DERIV (\x. k) x :> 0" by (simp add: deriv_def) -lemma DERIV_Id [simp]: "DERIV (\x. x) x :> 1" +lemma DERIV_ident [simp]: "DERIV (\x. x) x :> 1" by (simp add: deriv_def divide_self cong: LIM_cong) lemma add_diff_add: @@ -77,7 +77,7 @@ hence "(\h. (f(x+h) - f(x)) / h) -- 0 --> D" by (rule DERIV_D) hence "(\h. (f(x+h) - f(x)) / h * h) -- 0 --> D * 0" - by (intro LIM_mult LIM_self) + by (intro LIM_mult LIM_ident) hence "(\h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0" by simp hence "(\h. f(x+h) - f(x)) -- 0 --> 0" @@ -296,10 +296,10 @@ (*derivative of linear multiplication*) lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c" -by (cut_tac c = c and x = x in DERIV_Id [THEN DERIV_cmult], simp) +by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp) lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))" -apply (cut_tac DERIV_power [OF DERIV_Id]) +apply (cut_tac DERIV_power [OF DERIV_ident]) apply (simp add: real_scaleR_def real_of_nat_def) done @@ -308,7 +308,7 @@ lemma DERIV_inverse: fixes x :: "'a::{real_normed_field,recpower}" shows "x \ 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))" -by (drule DERIV_inverse' [OF DERIV_Id]) (simp add: power_Suc) +by (drule DERIV_inverse' [OF DERIV_ident]) (simp add: power_Suc) text{*Derivative of inverse*} lemma DERIV_inverse_fun: @@ -985,7 +985,7 @@ proof - let ?F = "%x. f x - ((f b - f a) / (b-a)) * x" have contF: "\x. a \ x \ x \ b \ isCont ?F x" using con - by (fast intro: isCont_diff isCont_const isCont_mult isCont_Id) + by (fast intro: isCont_diff isCont_const isCont_mult isCont_ident) have difF: "\x. a < x \ x < b \ ?F differentiable x" proof (clarify) fix x::real diff -r 88bfbe031820 -r cdfff0241c12 src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Tue May 22 05:07:48 2007 +0200 +++ b/src/HOL/Hyperreal/Lim.thy Tue May 22 07:29:49 2007 +0200 @@ -183,7 +183,7 @@ apply (auto dest!: LIM_const_eq) done -lemma LIM_self: "(%x. x) -- a --> a" +lemma LIM_ident [simp]: "(\x. x) -- a --> a" by (auto simp add: LIM_def) text{*Limits are equal for functions equal except at limit point*} @@ -435,7 +435,7 @@ apply (simp add: LIM_inverse_lemma) done have "(\x. inverse a * x) -- a --> inverse a * a" - by (intro LIM_mult LIM_self LIM_const) + by (intro LIM_mult LIM_ident LIM_const) hence "(\x. inverse a * x) -- a --> 1" by (simp add: a) with 1 have "(\x. inverse (inverse a * x)) -- a --> inverse 1" @@ -464,8 +464,8 @@ lemma isCont_iff: "isCont f x = (\h. f (x + h)) -- 0 --> f x" by (simp add: isCont_def LIM_isCont_iff) -lemma isCont_Id: "isCont (\x. x) a" - unfolding isCont_def by (rule LIM_self) +lemma isCont_ident [simp]: "isCont (\x. x) a" + unfolding isCont_def by (rule LIM_ident) lemma isCont_const [simp]: "isCont (\x. k) a" unfolding isCont_def by (rule LIM_const) @@ -531,7 +531,7 @@ unfolding isCont_def by (rule LIM_power) lemma isCont_abs [simp]: "isCont abs (a::real)" -by (rule isCont_rabs [OF isCont_Id]) +by (rule isCont_rabs [OF isCont_ident]) subsection {* Uniform Continuity *} diff -r 88bfbe031820 -r cdfff0241c12 src/HOL/Hyperreal/MacLaurin.thy --- a/src/HOL/Hyperreal/MacLaurin.thy Tue May 22 05:07:48 2007 +0200 +++ b/src/HOL/Hyperreal/MacLaurin.thy Tue May 22 07:29:49 2007 +0200 @@ -33,12 +33,12 @@ {* local val deriv_rulesI = - [thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult", + [thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult", thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow", thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus", thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow", thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos", - thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos"]; + thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos"]; val DERIV_chain2 = thm "DERIV_chain2"; @@ -251,7 +251,7 @@ apply (rule DERIV_cmult) apply (rule lemma_DERIV_subst) apply (rule DERIV_chain2 [where g=uminus]) -apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_Id) +apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_ident) prefer 2 apply force apply force apply (rule_tac x = "-t" in exI, auto) diff -r 88bfbe031820 -r cdfff0241c12 src/HOL/Hyperreal/NthRoot.thy --- a/src/HOL/Hyperreal/NthRoot.thy Tue May 22 05:07:48 2007 +0200 +++ b/src/HOL/Hyperreal/NthRoot.thy Tue May 22 07:29:49 2007 +0200 @@ -29,7 +29,7 @@ using n1 by (rule power_increasing, simp) finally show "a \ max 1 a ^ n" . show "\r. 0 \ r \ r \ max 1 a \ isCont (\x. x ^ n) r" - by (simp add: isCont_power isCont_Id) + by (simp add: isCont_power) qed then obtain r where r: "0 \ r \ r ^ n = a" by fast with n a have "r \ 0" by (auto simp add: power_0_left) @@ -253,7 +253,7 @@ show "\z. \z - root n x\ \ root n x \ root n (z ^ n) = z" by (simp add: abs_le_iff real_root_power_cancel n) show "\z. \z - root n x\ \ root n x \ isCont (\a. a ^ n) z" - by (simp add: isCont_power isCont_Id) + by (simp add: isCont_power) qed thus ?thesis using n x by simp qed @@ -262,7 +262,7 @@ "\0 < n; x < 0\ \ isCont (root n) x" apply (subgoal_tac "isCont (\x. - root n (- x)) x") apply (simp add: real_root_minus) -apply (rule isCont_o2 [OF isCont_minus [OF isCont_Id]]) +apply (rule isCont_o2 [OF isCont_minus [OF isCont_ident]]) apply (simp add: isCont_minus isCont_root_pos) done diff -r 88bfbe031820 -r cdfff0241c12 src/HOL/Hyperreal/Taylor.thy --- a/src/HOL/Hyperreal/Taylor.thy Tue May 22 05:07:48 2007 +0200 +++ b/src/HOL/Hyperreal/Taylor.thy Tue May 22 07:29:49 2007 +0200 @@ -32,7 +32,7 @@ assume "m < n & 0 <= t & t <= b - c" with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto moreover - from DERIV_Id and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add) + from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add) ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2) thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp @@ -74,7 +74,7 @@ assume "m < n & a-c <= t & t <= 0" with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto moreover - from DERIV_Id and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add) + from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add) ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2) thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp qed diff -r 88bfbe031820 -r cdfff0241c12 src/HOL/Hyperreal/Transcendental.thy --- a/src/HOL/Hyperreal/Transcendental.thy Tue May 22 05:07:48 2007 +0200 +++ b/src/HOL/Hyperreal/Transcendental.thy Tue May 22 07:29:49 2007 +0200 @@ -637,14 +637,14 @@ lemma DERIV_exp_add_const: "DERIV (%x. exp (x + y)) x :> exp(x + y)" proof - have "DERIV (exp \ (\x. x + y)) x :> exp (x + y) * (1+0)" - by (fast intro: DERIV_chain DERIV_add DERIV_exp DERIV_Id DERIV_const) + by (fast intro: DERIV_chain DERIV_add DERIV_exp DERIV_ident DERIV_const) thus ?thesis by (simp add: o_def) qed lemma DERIV_exp_minus [simp]: "DERIV (%x. exp (-x)) x :> - exp(-x)" proof - have "DERIV (exp \ uminus) x :> exp (- x) * - 1" - by (fast intro: DERIV_chain DERIV_minus DERIV_exp DERIV_Id) + by (fast intro: DERIV_chain DERIV_minus DERIV_exp DERIV_ident) thus ?thesis by (simp add: o_def) qed @@ -1065,7 +1065,7 @@ apply (rule DERIV_cos, auto) done -lemmas DERIV_intros = DERIV_Id DERIV_const DERIV_cos DERIV_cmult +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