--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Sep 07 10:05:19 2010 +0200
@@ -2363,7 +2363,7 @@
apply (rule span_mul)
by (rule span_superset)}
then have SC: "span ?C = span (insert a B)"
- unfolding expand_set_eq span_breakdown_eq C(3)[symmetric] by auto
+ unfolding set_ext_iff span_breakdown_eq C(3)[symmetric] by auto
thm pairwise_def
{fix x y assume xC: "x \<in> ?C" and yC: "y \<in> ?C" and xy: "x \<noteq> y"
{assume xa: "x = ?a" and ya: "y = ?a"
@@ -2826,7 +2826,7 @@
" \<forall>x \<in> f ` basis ` {..<DIM('a)}. h x = inv f x" by blast
from h(2)
have th: "\<forall>i<DIM('a). (h \<circ> f) (basis i) = id (basis i)"
- using inv_o_cancel[OF fi, unfolded expand_fun_eq id_def o_def]
+ using inv_o_cancel[OF fi, unfolded ext_iff id_def o_def]
by auto
from linear_eq_stdbasis[OF linear_compose[OF lf h(1)] linear_id th]
@@ -2843,7 +2843,7 @@
h: "linear h" "\<forall> x\<in> basis ` {..<DIM('b)}. h x = inv f x" by blast
from h(2)
have th: "\<forall>i<DIM('b). (f o h) (basis i) = id (basis i)"
- using sf by(auto simp add: surj_iff o_def expand_fun_eq)
+ using sf by(auto simp add: surj_iff o_def ext_iff)
from linear_eq_stdbasis[OF linear_compose[OF h(1) lf] linear_id th]
have "f o h = id" .
then show ?thesis using h(1) by blast
@@ -2970,7 +2970,7 @@
lemma isomorphism_expand:
"f o g = id \<and> g o f = id \<longleftrightarrow> (\<forall>x. f(g x) = x) \<and> (\<forall>x. g(f x) = x)"
- by (simp add: expand_fun_eq o_def id_def)
+ by (simp add: ext_iff o_def id_def)
lemma linear_injective_isomorphism: fixes f::"'a::euclidean_space => 'a::euclidean_space"
assumes lf: "linear f" and fi: "inj f"
@@ -2995,10 +2995,10 @@
{fix f f':: "'a => 'a"
assume lf: "linear f" "linear f'" and f: "f o f' = id"
from f have sf: "surj f"
- apply (auto simp add: o_def expand_fun_eq id_def surj_def)
+ apply (auto simp add: o_def ext_iff id_def surj_def)
by metis
from linear_surjective_isomorphism[OF lf(1) sf] lf f
- have "f' o f = id" unfolding expand_fun_eq o_def id_def
+ have "f' o f = id" unfolding ext_iff o_def id_def
by metis}
then show ?thesis using lf lf' by metis
qed
@@ -3009,13 +3009,13 @@
assumes lf: "linear f" and gf: "g o f = id"
shows "linear g"
proof-
- from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def expand_fun_eq)
+ from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def ext_iff)
by metis
from linear_injective_isomorphism[OF lf fi]
obtain h:: "'a \<Rightarrow> '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