rename lemmas LIM_ident, isCont_ident, DERIV_ident
authorhuffman
Tue May 22 07:29:49 2007 +0200 (2007-05-22)
changeset 23069cdfff0241c12
parent 23068 88bfbe031820
child 23070 c5b896d9788c
rename lemmas LIM_ident, isCont_ident, DERIV_ident
src/HOL/Complex/CLim.thy
src/HOL/Hyperreal/Deriv.thy
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/NthRoot.thy
src/HOL/Hyperreal/Taylor.thy
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Complex/CLim.thy	Tue May 22 05:07:48 2007 +0200
     1.2 +++ b/src/HOL/Complex/CLim.thy	Tue May 22 07:29:49 2007 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4  lemma CDERIV_pow [simp]:
     1.5       "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
     1.6  apply (induct_tac "n")
     1.7 -apply (drule_tac [2] DERIV_Id [THEN DERIV_mult])
     1.8 +apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
     1.9  apply (auto simp add: left_distrib real_of_nat_Suc)
    1.10  apply (case_tac "n")
    1.11  apply (auto simp add: mult_ac add_commute)
     2.1 --- a/src/HOL/Hyperreal/Deriv.thy	Tue May 22 05:07:48 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/Deriv.thy	Tue May 22 07:29:49 2007 +0200
     2.3 @@ -47,7 +47,7 @@
     2.4  lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x :> 0"
     2.5  by (simp add: deriv_def)
     2.6  
     2.7 -lemma DERIV_Id [simp]: "DERIV (\<lambda>x. x) x :> 1"
     2.8 +lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x :> 1"
     2.9  by (simp add: deriv_def divide_self cong: LIM_cong)
    2.10  
    2.11  lemma add_diff_add:
    2.12 @@ -77,7 +77,7 @@
    2.13    hence "(\<lambda>h. (f(x+h) - f(x)) / h) -- 0 --> D"
    2.14      by (rule DERIV_D)
    2.15    hence "(\<lambda>h. (f(x+h) - f(x)) / h * h) -- 0 --> D * 0"
    2.16 -    by (intro LIM_mult LIM_self)
    2.17 +    by (intro LIM_mult LIM_ident)
    2.18    hence "(\<lambda>h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0"
    2.19      by simp
    2.20    hence "(\<lambda>h. f(x+h) - f(x)) -- 0 --> 0"
    2.21 @@ -296,10 +296,10 @@
    2.22  
    2.23  (*derivative of linear multiplication*)
    2.24  lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c"
    2.25 -by (cut_tac c = c and x = x in DERIV_Id [THEN DERIV_cmult], simp)
    2.26 +by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp)
    2.27  
    2.28  lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
    2.29 -apply (cut_tac DERIV_power [OF DERIV_Id])
    2.30 +apply (cut_tac DERIV_power [OF DERIV_ident])
    2.31  apply (simp add: real_scaleR_def real_of_nat_def)
    2.32  done
    2.33  
    2.34 @@ -308,7 +308,7 @@
    2.35  lemma DERIV_inverse:
    2.36    fixes x :: "'a::{real_normed_field,recpower}"
    2.37    shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
    2.38 -by (drule DERIV_inverse' [OF DERIV_Id]) (simp add: power_Suc)
    2.39 +by (drule DERIV_inverse' [OF DERIV_ident]) (simp add: power_Suc)
    2.40  
    2.41  text{*Derivative of inverse*}
    2.42  lemma DERIV_inverse_fun:
    2.43 @@ -985,7 +985,7 @@
    2.44  proof -
    2.45    let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
    2.46    have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x" using con
    2.47 -    by (fast intro: isCont_diff isCont_const isCont_mult isCont_Id)
    2.48 +    by (fast intro: isCont_diff isCont_const isCont_mult isCont_ident)
    2.49    have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable x"
    2.50    proof (clarify)
    2.51      fix x::real
     3.1 --- a/src/HOL/Hyperreal/Lim.thy	Tue May 22 05:07:48 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/Lim.thy	Tue May 22 07:29:49 2007 +0200
     3.3 @@ -183,7 +183,7 @@
     3.4  apply (auto dest!: LIM_const_eq)
     3.5  done
     3.6  
     3.7 -lemma LIM_self: "(%x. x) -- a --> a"
     3.8 +lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
     3.9  by (auto simp add: LIM_def)
    3.10  
    3.11  text{*Limits are equal for functions equal except at limit point*}
    3.12 @@ -435,7 +435,7 @@
    3.13      apply (simp add: LIM_inverse_lemma)
    3.14      done
    3.15    have "(\<lambda>x. inverse a * x) -- a --> inverse a * a"
    3.16 -    by (intro LIM_mult LIM_self LIM_const)
    3.17 +    by (intro LIM_mult LIM_ident LIM_const)
    3.18    hence "(\<lambda>x. inverse a * x) -- a --> 1"
    3.19      by (simp add: a)
    3.20    with 1 have "(\<lambda>x. inverse (inverse a * x)) -- a --> inverse 1"
    3.21 @@ -464,8 +464,8 @@
    3.22  lemma isCont_iff: "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
    3.23  by (simp add: isCont_def LIM_isCont_iff)
    3.24  
    3.25 -lemma isCont_Id: "isCont (\<lambda>x. x) a"
    3.26 -  unfolding isCont_def by (rule LIM_self)
    3.27 +lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a"
    3.28 +  unfolding isCont_def by (rule LIM_ident)
    3.29  
    3.30  lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
    3.31    unfolding isCont_def by (rule LIM_const)
    3.32 @@ -531,7 +531,7 @@
    3.33    unfolding isCont_def by (rule LIM_power)
    3.34  
    3.35  lemma isCont_abs [simp]: "isCont abs (a::real)"
    3.36 -by (rule isCont_rabs [OF isCont_Id])
    3.37 +by (rule isCont_rabs [OF isCont_ident])
    3.38  
    3.39  
    3.40  subsection {* Uniform Continuity *}
     4.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Tue May 22 05:07:48 2007 +0200
     4.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue May 22 07:29:49 2007 +0200
     4.3 @@ -33,12 +33,12 @@
     4.4  {*
     4.5  local
     4.6  val deriv_rulesI =
     4.7 -  [thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
     4.8 +  [thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
     4.9    thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow",
    4.10    thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus",
    4.11    thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow",
    4.12    thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos",
    4.13 -  thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos"];
    4.14 +  thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos"];
    4.15  
    4.16  val DERIV_chain2 = thm "DERIV_chain2";
    4.17  
    4.18 @@ -251,7 +251,7 @@
    4.19  apply (rule DERIV_cmult)
    4.20  apply (rule lemma_DERIV_subst)
    4.21  apply (rule DERIV_chain2 [where g=uminus])
    4.22 -apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_Id)
    4.23 +apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_ident)
    4.24  prefer 2 apply force
    4.25  apply force
    4.26  apply (rule_tac x = "-t" in exI, auto)
     5.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Tue May 22 05:07:48 2007 +0200
     5.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Tue May 22 07:29:49 2007 +0200
     5.3 @@ -29,7 +29,7 @@
     5.4        using n1 by (rule power_increasing, simp)
     5.5      finally show "a \<le> max 1 a ^ n" .
     5.6      show "\<forall>r. 0 \<le> r \<and> r \<le> max 1 a \<longrightarrow> isCont (\<lambda>x. x ^ n) r"
     5.7 -      by (simp add: isCont_power isCont_Id)
     5.8 +      by (simp add: isCont_power)
     5.9    qed
    5.10    then obtain r where r: "0 \<le> r \<and> r ^ n = a" by fast
    5.11    with n a have "r \<noteq> 0" by (auto simp add: power_0_left)
    5.12 @@ -253,7 +253,7 @@
    5.13      show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> root n (z ^ n) = z"
    5.14        by (simp add: abs_le_iff real_root_power_cancel n)
    5.15      show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> isCont (\<lambda>a. a ^ n) z"
    5.16 -      by (simp add: isCont_power isCont_Id)
    5.17 +      by (simp add: isCont_power)
    5.18    qed
    5.19    thus ?thesis using n x by simp
    5.20  qed
    5.21 @@ -262,7 +262,7 @@
    5.22    "\<lbrakk>0 < n; x < 0\<rbrakk> \<Longrightarrow> isCont (root n) x"
    5.23  apply (subgoal_tac "isCont (\<lambda>x. - root n (- x)) x")
    5.24  apply (simp add: real_root_minus)
    5.25 -apply (rule isCont_o2 [OF isCont_minus [OF isCont_Id]])
    5.26 +apply (rule isCont_o2 [OF isCont_minus [OF isCont_ident]])
    5.27  apply (simp add: isCont_minus isCont_root_pos)
    5.28  done
    5.29  
     6.1 --- a/src/HOL/Hyperreal/Taylor.thy	Tue May 22 05:07:48 2007 +0200
     6.2 +++ b/src/HOL/Hyperreal/Taylor.thy	Tue May 22 07:29:49 2007 +0200
     6.3 @@ -32,7 +32,7 @@
     6.4      assume "m < n & 0 <= t & t <= b - c"
     6.5      with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
     6.6      moreover
     6.7 -    from DERIV_Id and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
     6.8 +    from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
     6.9      ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)"
    6.10        by (rule DERIV_chain2)
    6.11      thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
    6.12 @@ -74,7 +74,7 @@
    6.13      assume "m < n & a-c <= t & t <= 0"
    6.14      with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto 
    6.15      moreover
    6.16 -    from DERIV_Id and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
    6.17 +    from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
    6.18      ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)
    6.19      thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
    6.20    qed
     7.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Tue May 22 05:07:48 2007 +0200
     7.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Tue May 22 07:29:49 2007 +0200
     7.3 @@ -637,14 +637,14 @@
     7.4  lemma DERIV_exp_add_const: "DERIV (%x. exp (x + y)) x :> exp(x + y)"
     7.5  proof -
     7.6    have "DERIV (exp \<circ> (\<lambda>x. x + y)) x :> exp (x + y) * (1+0)"
     7.7 -    by (fast intro: DERIV_chain DERIV_add DERIV_exp DERIV_Id DERIV_const) 
     7.8 +    by (fast intro: DERIV_chain DERIV_add DERIV_exp DERIV_ident DERIV_const) 
     7.9    thus ?thesis by (simp add: o_def)
    7.10  qed
    7.11  
    7.12  lemma DERIV_exp_minus [simp]: "DERIV (%x. exp (-x)) x :> - exp(-x)"
    7.13  proof -
    7.14    have "DERIV (exp \<circ> uminus) x :> exp (- x) * - 1"
    7.15 -    by (fast intro: DERIV_chain DERIV_minus DERIV_exp DERIV_Id) 
    7.16 +    by (fast intro: DERIV_chain DERIV_minus DERIV_exp DERIV_ident)
    7.17    thus ?thesis by (simp add: o_def)
    7.18  qed
    7.19  
    7.20 @@ -1065,7 +1065,7 @@
    7.21  apply (rule DERIV_cos, auto)
    7.22  done
    7.23  
    7.24 -lemmas DERIV_intros = DERIV_Id DERIV_const DERIV_cos DERIV_cmult 
    7.25 +lemmas DERIV_intros = DERIV_ident DERIV_const DERIV_cos DERIV_cmult 
    7.26                      DERIV_sin  DERIV_exp  DERIV_inverse DERIV_pow 
    7.27                      DERIV_add  DERIV_diff  DERIV_mult  DERIV_minus 
    7.28                      DERIV_inverse_fun DERIV_quotient DERIV_fun_pow