1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -1440,12 +1440,12 @@
     1.4  lemma interval_cart: fixes a :: "'a::ord^'n" shows
     1.5    "{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
     1.6    "{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
     1.7 -  by (auto simp add: expand_set_eq vector_less_def vector_le_def)
     1.8 +  by (auto simp add: set_ext_iff vector_less_def vector_le_def)
     1.9  
    1.10  lemma mem_interval_cart: fixes a :: "'a::ord^'n" shows
    1.11    "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
    1.12    "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
    1.13 -  using interval_cart[of a b] by(auto simp add: expand_set_eq vector_less_def vector_le_def)
    1.14 +  using interval_cart[of a b] by(auto simp add: set_ext_iff vector_less_def vector_le_def)
    1.15  
    1.16  lemma interval_eq_empty_cart: fixes a :: "real^'n" shows
    1.17   "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
    1.18 @@ -1498,7 +1498,7 @@
    1.19  
    1.20  lemma interval_sing: fixes a :: "'a::linorder^'n" shows
    1.21   "{a .. a} = {a} \<and> {a<..<a} = {}"
    1.22 -apply(auto simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
    1.23 +apply(auto simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
    1.24  apply (simp add: order_eq_iff)
    1.25  apply (auto simp add: not_less less_imp_le)
    1.26  done
    1.27 @@ -1511,17 +1511,17 @@
    1.28    { fix i
    1.29      have "a $ i \<le> x $ i"
    1.30        using x order_less_imp_le[of "a$i" "x$i"]
    1.31 -      by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
    1.32 +      by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
    1.33    }
    1.34    moreover
    1.35    { fix i
    1.36      have "x $ i \<le> b $ i"
    1.37        using x order_less_imp_le[of "x$i" "b$i"]
    1.38 -      by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
    1.39 +      by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
    1.40    }
    1.41    ultimately
    1.42    show "a \<le> x \<and> x \<le> b"
    1.43 -    by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
    1.44 +    by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
    1.45  qed
    1.46  
    1.47  lemma subset_interval_cart: fixes a :: "real^'n" shows
    1.48 @@ -1540,7 +1540,7 @@
    1.49  
    1.50  lemma inter_interval_cart: fixes a :: "'a::linorder^'n" shows
    1.51   "{a .. b} \<inter> {c .. d} =  {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
    1.52 -  unfolding expand_set_eq and Int_iff and mem_interval_cart
    1.53 +  unfolding set_ext_iff and Int_iff and mem_interval_cart
    1.54    by auto
    1.55  
    1.56  lemma closed_interval_left_cart: fixes b::"real^'n"
    1.57 @@ -1656,7 +1656,7 @@
    1.58    shows "(\<lambda>x. m *s x + c) o (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
    1.59    "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) o (\<lambda>x. m *s x + c) = id"
    1.60    using m0
    1.61 -apply (auto simp add: expand_fun_eq vector_add_ldistrib)
    1.62 +apply (auto simp add: ext_iff vector_add_ldistrib)
    1.63  by (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric])
    1.64  
    1.65  lemma vector_affinity_eq:
    1.66 @@ -2119,10 +2119,10 @@
    1.67  
    1.68  lemma open_closed_interval_1: fixes a :: "real^1" shows
    1.69   "{a<..<b} = {a .. b} - {a, b}"
    1.70 -  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
    1.71 +  unfolding set_ext_iff apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
    1.72  
    1.73  lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
    1.74 -  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
    1.75 +  unfolding set_ext_iff apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
    1.76  
    1.77  lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
    1.78    "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"