--- 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)
--- 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 (\<lambda>x. k) x :> 0"
by (simp add: deriv_def)
-lemma DERIV_Id [simp]: "DERIV (\<lambda>x. x) x :> 1"
+lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x :> 1"
by (simp add: deriv_def divide_self cong: LIM_cong)
lemma add_diff_add:
@@ -77,7 +77,7 @@
hence "(\<lambda>h. (f(x+h) - f(x)) / h) -- 0 --> D"
by (rule DERIV_D)
hence "(\<lambda>h. (f(x+h) - f(x)) / h * h) -- 0 --> D * 0"
- by (intro LIM_mult LIM_self)
+ by (intro LIM_mult LIM_ident)
hence "(\<lambda>h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0"
by simp
hence "(\<lambda>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 \<noteq> 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: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> 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: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable x"
proof (clarify)
fix x::real
--- 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]: "(\<lambda>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 "(\<lambda>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 "(\<lambda>x. inverse a * x) -- a --> 1"
by (simp add: a)
with 1 have "(\<lambda>x. inverse (inverse a * x)) -- a --> inverse 1"
@@ -464,8 +464,8 @@
lemma isCont_iff: "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
by (simp add: isCont_def LIM_isCont_iff)
-lemma isCont_Id: "isCont (\<lambda>x. x) a"
- unfolding isCont_def by (rule LIM_self)
+lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a"
+ unfolding isCont_def by (rule LIM_ident)
lemma isCont_const [simp]: "isCont (\<lambda>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 *}
--- 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)
--- 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 \<le> max 1 a ^ n" .
show "\<forall>r. 0 \<le> r \<and> r \<le> max 1 a \<longrightarrow> isCont (\<lambda>x. x ^ n) r"
- by (simp add: isCont_power isCont_Id)
+ by (simp add: isCont_power)
qed
then obtain r where r: "0 \<le> r \<and> r ^ n = a" by fast
with n a have "r \<noteq> 0" by (auto simp add: power_0_left)
@@ -253,7 +253,7 @@
show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> root n (z ^ n) = z"
by (simp add: abs_le_iff real_root_power_cancel n)
show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> isCont (\<lambda>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 @@
"\<lbrakk>0 < n; x < 0\<rbrakk> \<Longrightarrow> isCont (root n) x"
apply (subgoal_tac "isCont (\<lambda>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
--- 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
--- 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 \<circ> (\<lambda>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 \<circ> 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