--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Sep 07 10:05:19 2010 +0200
@@ -665,7 +665,7 @@
have "\<forall>i<DIM('a). f' (basis i) = 0"
by (simp add: euclidean_eq[of _ "0::'a"])
with derivative_is_linear[OF deriv, THEN linear_componentwise, of _ 0]
- show ?thesis by (simp add: expand_fun_eq)
+ show ?thesis by (simp add: ext_iff)
qed
lemma rolle: fixes f::"real\<Rightarrow>real"
@@ -948,13 +948,13 @@
assumes lf: "linear f" and gf: "f o g = id"
shows "linear g"
proof-
- from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def expand_fun_eq)
+ from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def ext_iff)
by metis
from linear_surjective_isomorphism[OF lf fi]
obtain h:: "'a => 'a" where
h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x" by blast
have "h = g" apply (rule ext) using gf h(2,3)
- apply (simp add: o_def id_def expand_fun_eq)
+ apply (simp add: o_def id_def ext_iff)
by metis
with h(1) show ?thesis by blast
qed
@@ -1268,7 +1268,7 @@
have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
using assms [unfolded has_vector_derivative_def]
by (rule frechet_derivative_unique_at)
- thus ?thesis unfolding expand_fun_eq by auto
+ thus ?thesis unfolding ext_iff by auto
qed
lemma vector_derivative_unique_within_closed_interval: fixes f::"real \<Rightarrow> 'n::ordered_euclidean_space"
@@ -1279,7 +1279,7 @@
apply(rule frechet_derivative_unique_within_closed_interval[of "a" "b"])
using assms(3-)[unfolded has_vector_derivative_def] using assms(1-2) by auto
show ?thesis proof(rule ccontr) assume "f' \<noteq> f''" moreover
- hence "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1" using * by (auto simp: expand_fun_eq)
+ hence "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1" using * by (auto simp: ext_iff)
ultimately show False unfolding o_def by auto qed qed
lemma vector_derivative_at: