1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Sep 13 08:43:48 2010 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Sep 13 11:13:15 2010 +0200
1.3 @@ -880,7 +880,7 @@
1.4 by (simp add: row_def column_def transpose_def Cart_eq)
1.5
1.6 lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
1.7 -by (auto simp add: rows_def columns_def row_transpose intro: set_ext)
1.8 +by (auto simp add: rows_def columns_def row_transpose intro: set_eqI)
1.9
1.10 lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" by (metis transpose_transpose rows_transpose)
1.11
1.12 @@ -986,7 +986,7 @@
1.13 subsection {* Standard bases are a spanning set, and obviously finite. *}
1.14
1.15 lemma span_stdbasis:"span {cart_basis i :: real^'n | i. i \<in> (UNIV :: 'n set)} = UNIV"
1.16 -apply (rule set_ext)
1.17 +apply (rule set_eqI)
1.18 apply auto
1.19 apply (subst basis_expansion'[symmetric])
1.20 apply (rule span_setsum)
1.21 @@ -1440,12 +1440,12 @@
1.22 lemma interval_cart: fixes a :: "'a::ord^'n" shows
1.23 "{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
1.24 "{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
1.25 - by (auto simp add: set_ext_iff vector_less_def vector_le_def)
1.26 + by (auto simp add: set_eq_iff vector_less_def vector_le_def)
1.27
1.28 lemma mem_interval_cart: fixes a :: "'a::ord^'n" shows
1.29 "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
1.30 "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
1.31 - using interval_cart[of a b] by(auto simp add: set_ext_iff vector_less_def vector_le_def)
1.32 + using interval_cart[of a b] by(auto simp add: set_eq_iff vector_less_def vector_le_def)
1.33
1.34 lemma interval_eq_empty_cart: fixes a :: "real^'n" shows
1.35 "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
1.36 @@ -1498,7 +1498,7 @@
1.37
1.38 lemma interval_sing: fixes a :: "'a::linorder^'n" shows
1.39 "{a .. a} = {a} \<and> {a<..<a} = {}"
1.40 -apply(auto simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
1.41 +apply(auto simp add: set_eq_iff vector_less_def vector_le_def Cart_eq)
1.42 apply (simp add: order_eq_iff)
1.43 apply (auto simp add: not_less less_imp_le)
1.44 done
1.45 @@ -1511,17 +1511,17 @@
1.46 { fix i
1.47 have "a $ i \<le> x $ i"
1.48 using x order_less_imp_le[of "a$i" "x$i"]
1.49 - by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
1.50 + by(simp add: set_eq_iff vector_less_def vector_le_def Cart_eq)
1.51 }
1.52 moreover
1.53 { fix i
1.54 have "x $ i \<le> b $ i"
1.55 using x order_less_imp_le[of "x$i" "b$i"]
1.56 - by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
1.57 + by(simp add: set_eq_iff vector_less_def vector_le_def Cart_eq)
1.58 }
1.59 ultimately
1.60 show "a \<le> x \<and> x \<le> b"
1.61 - by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
1.62 + by(simp add: set_eq_iff vector_less_def vector_le_def Cart_eq)
1.63 qed
1.64
1.65 lemma subset_interval_cart: fixes a :: "real^'n" shows
1.66 @@ -1540,7 +1540,7 @@
1.67
1.68 lemma inter_interval_cart: fixes a :: "'a::linorder^'n" shows
1.69 "{a .. b} \<inter> {c .. d} = {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
1.70 - unfolding set_ext_iff and Int_iff and mem_interval_cart
1.71 + unfolding set_eq_iff and Int_iff and mem_interval_cart
1.72 by auto
1.73
1.74 lemma closed_interval_left_cart: fixes b::"real^'n"
1.75 @@ -1656,7 +1656,7 @@
1.76 shows "(\<lambda>x. m *s x + c) o (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
1.77 "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) o (\<lambda>x. m *s x + c) = id"
1.78 using m0
1.79 -apply (auto simp add: ext_iff vector_add_ldistrib)
1.80 +apply (auto simp add: fun_eq_iff vector_add_ldistrib)
1.81 by (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric])
1.82
1.83 lemma vector_affinity_eq:
1.84 @@ -1712,7 +1712,7 @@
1.85 lemma unit_interval_convex_hull_cart:
1.86 "{0::real^'n .. 1} = convex hull {x. \<forall>i. (x$i = 0) \<or> (x$i = 1)}" (is "?int = convex hull ?points")
1.87 unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"]
1.88 - apply(rule arg_cong[where f="\<lambda>x. convex hull x"]) apply(rule set_ext) unfolding mem_Collect_eq
1.89 + apply(rule arg_cong[where f="\<lambda>x. convex hull x"]) apply(rule set_eqI) unfolding mem_Collect_eq
1.90 apply safe apply(erule_tac x="\<pi>' i" in allE) unfolding nth_conv_component defer
1.91 apply(erule_tac x="\<pi> i" in allE) by auto
1.92
1.93 @@ -1974,7 +1974,7 @@
1.94 apply (simp add: forall_3)
1.95 done
1.96
1.97 -lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
1.98 +lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_eqI,rule) unfolding image_iff defer
1.99 apply(rule_tac x="dest_vec1 x" in bexI) by auto
1.100
1.101 lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
1.102 @@ -2069,7 +2069,7 @@
1.103 lemma vec1_interval:fixes a::"real" shows
1.104 "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
1.105 "vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
1.106 - apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval_cart
1.107 + apply(rule_tac[!] set_eqI) unfolding image_iff vector_less_def unfolding mem_interval_cart
1.108 unfolding forall_1 unfolding vec1_dest_vec1_simps
1.109 apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
1.110 apply(rule_tac x="dest_vec1 x" in bexI) by auto
1.111 @@ -2119,10 +2119,10 @@
1.112
1.113 lemma open_closed_interval_1: fixes a :: "real^1" shows
1.114 "{a<..<b} = {a .. b} - {a, b}"
1.115 - 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.116 + unfolding set_eq_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.117
1.118 lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
1.119 - 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.120 + unfolding set_eq_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.121
1.122 lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
1.123 "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
1.124 @@ -2284,7 +2284,7 @@
1.125 lemma interval_split_cart:
1.126 "{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
1.127 "{a..b} \<inter> {x. x$k \<ge> c} = {(\<chi> i. if i = k then max (a$k) c else a$i) .. b}"
1.128 - apply(rule_tac[!] set_ext) unfolding Int_iff mem_interval_cart mem_Collect_eq
1.129 + apply(rule_tac[!] set_eqI) unfolding Int_iff mem_interval_cart mem_Collect_eq
1.130 unfolding Cart_lambda_beta by auto
1.131
1.132 (*lemma content_split_cart: