diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Sep 13 11:13:15 2010 +0200 @@ -191,7 +191,7 @@ lemma affine_hull_finite: assumes "finite s" shows "affine hull s = {y. \u. setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" - unfolding affine_hull_explicit and set_ext_iff and mem_Collect_eq apply (rule,rule) + unfolding affine_hull_explicit and set_eq_iff and mem_Collect_eq apply (rule,rule) apply(erule exE)+ apply(erule conjE)+ defer apply(erule exE) apply(erule conjE) proof- fix x u assume "setsum u s = 1" "(\v\s. u v *\<^sub>R v) = x" thus "\sa u. finite sa \ \ (\x. (x \ sa) = (x \ {})) \ sa \ s \ setsum u sa = 1 \ (\v\sa. u v *\<^sub>R v) = x" @@ -709,7 +709,7 @@ ultimately have "\k u x. (\i\{1..k}. 0 \ u i \ x i \ p) \ setsum u {1..k} = 1 \ (\i::nat = 1..k. u i *\<^sub>R x i) = y" apply(rule_tac x="card s" in exI) apply(rule_tac x="u \ f" in exI) apply(rule_tac x=f in exI) by fastsimp hence "y \ ?lhs" unfolding convex_hull_indexed by auto } - ultimately show ?thesis unfolding set_ext_iff by blast + ultimately show ?thesis unfolding set_eq_iff by blast qed subsection {* A stepping theorem for that expansion. *} @@ -882,7 +882,7 @@ lemma convex_hull_caratheodory: fixes p::"('a::euclidean_space) set" shows "convex hull p = {y. \s u. finite s \ s \ p \ card s \ DIM('a) + 1 \ (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" - unfolding convex_hull_explicit set_ext_iff mem_Collect_eq + unfolding convex_hull_explicit set_eq_iff mem_Collect_eq proof(rule,rule) fix y let ?P = "\n. \s u. finite s \ card s = n \ s \ p \ (\x\s. 0 \ u x) \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" assume "\s u. finite s \ s \ p \ (\x\s. 0 \ u x) \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" @@ -939,7 +939,7 @@ lemma caratheodory: "convex hull p = {x::'a::euclidean_space. \s. finite s \ s \ p \ card s \ DIM('a) + 1 \ x \ convex hull s}" - unfolding set_ext_iff apply(rule, rule) unfolding mem_Collect_eq proof- + unfolding set_eq_iff apply(rule, rule) unfolding mem_Collect_eq proof- fix x assume "x \ convex hull p" then obtain s u where "finite s" "s \ p" "card s \ DIM('a) + 1" "\x\s. 0 \ u x" "setsum u s = 1" "(\v\s. u v *\<^sub>R v) = x"unfolding convex_hull_caratheodory by auto @@ -1000,7 +1000,7 @@ let ?X = "{0..1} \ s \ t" let ?h = "(\z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))" have *:"{ (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \ u \ u \ 1 \ x \ s \ y \ t} = ?h ` ?X" - apply(rule set_ext) unfolding image_iff mem_Collect_eq + apply(rule set_eqI) unfolding image_iff mem_Collect_eq apply rule apply auto apply (rule_tac x=u in rev_bexI, simp) apply (erule rev_bexI, erule rev_bexI, simp) @@ -1029,7 +1029,7 @@ case (Suc n) show ?case proof(cases "n=0") case True have "{x. \t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t} = s" - unfolding set_ext_iff and mem_Collect_eq proof(rule, rule) + unfolding set_eq_iff and mem_Collect_eq proof(rule, rule) fix x assume "\t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t" then obtain t where t:"finite t" "t \ s" "card t \ Suc n" "x \ convex hull t" by auto show "x\s" proof(cases "card t = 0") @@ -1048,7 +1048,7 @@ case False have "{x. \t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t} = { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \ u \ u \ 1 \ x \ s \ y \ {x. \t. finite t \ t \ s \ card t \ n \ x \ convex hull t}}" - unfolding set_ext_iff and mem_Collect_eq proof(rule,rule) + unfolding set_eq_iff and mem_Collect_eq proof(rule,rule) fix x assume "\u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \ 0 \ c \ c \ 1 \ u \ s \ (\t. finite t \ t \ s \ card t \ n \ v \ convex hull t)" then obtain u v c t where obt:"x = (1 - c) *\<^sub>R u + c *\<^sub>R v" @@ -1531,7 +1531,7 @@ fixes s :: "('a::euclidean_space) set" assumes "closed s" "convex s" shows "s = \ {h. s \ h \ (\a b. h = {x. inner a x \ b})}" - apply(rule set_ext, rule) unfolding Inter_iff Ball_def mem_Collect_eq apply(rule,rule,erule conjE) proof- + apply(rule set_eqI, rule) unfolding Inter_iff Ball_def mem_Collect_eq apply(rule,rule,erule conjE) proof- fix x assume "\xa. s \ xa \ (\a b. xa = {x. inner a x \ b}) \ x \ xa" hence "\a b. s \ {x. inner a x \ b} \ x \ {x. inner a x \ b}" by blast thus "x\s" apply(rule_tac ccontr) apply(drule separating_hyperplane_closed_point[OF assms(2,1)]) @@ -1752,7 +1752,7 @@ have "\surf. homeomorphism (frontier s) sphere pi surf" apply(rule homeomorphism_compact) apply(rule compact_frontier[OF assms(1)]) - apply(rule continuous_on_subset[OF contpi]) defer apply(rule set_ext,rule) + apply(rule continuous_on_subset[OF contpi]) defer apply(rule set_eqI,rule) unfolding inj_on_def prefer 3 apply(rule,rule,rule) proof- fix x assume "x\pi ` frontier s" then obtain y where "y\frontier s" "x = pi y" by auto thus "x \ sphere" using pi(1)[of y] and `0 \ frontier s` by auto @@ -1813,7 +1813,7 @@ qed } note hom2 = this show ?thesis apply(subst homeomorphic_sym) apply(rule homeomorphic_compact[where f="\x. norm x *\<^sub>R surf (pi x)"]) - apply(rule compact_cball) defer apply(rule set_ext, rule, erule imageE, drule hom) + apply(rule compact_cball) defer apply(rule set_eqI, rule, erule imageE, drule hom) prefer 4 apply(rule continuous_at_imp_continuous_on, rule) apply(rule_tac [3] hom2) proof- fix x::"'a" assume as:"x \ cball 0 1" thus "continuous (at x) (\x. norm x *\<^sub>R surf (pi x))" proof(cases "x=0") @@ -2119,7 +2119,7 @@ assumes "0 < d" obtains s::"('a::ordered_euclidean_space) set" where "finite s" "{x - (\\ i. d) .. x + (\\ i. d)} = convex hull s" proof- let ?d = "(\\ i. d)::'a" - have *:"{x - ?d .. x + ?d} = (\y. x - ?d + (2 * d) *\<^sub>R y) ` {0 .. \\ i. 1}" apply(rule set_ext, rule) + have *:"{x - ?d .. x + ?d} = (\y. x - ?d + (2 * d) *\<^sub>R y) ` {0 .. \\ i. 1}" apply(rule set_eqI, rule) unfolding image_iff defer apply(erule bexE) proof- fix y assume as:"y\{x - ?d .. x + ?d}" { fix i assume i:"i d + y $$ i" "y $$ i \ d + x $$ i" @@ -2329,7 +2329,7 @@ "closed_segment a b = convex hull {a,b}" proof- have *:"\x. {x} \ {}" by auto have **:"\u v. u + v = 1 \ u = 1 - (v::real)" by auto - show ?thesis unfolding segment convex_hull_insert[OF *] convex_hull_singleton apply(rule set_ext) + show ?thesis unfolding segment convex_hull_insert[OF *] convex_hull_singleton apply(rule set_eqI) unfolding mem_Collect_eq apply(rule,erule exE) apply(rule_tac x="1 - u" in exI) apply rule defer apply(rule_tac x=u in exI) defer apply(erule exE, (erule conjE)?)+ apply(rule_tac x="1 - u" in exI) unfolding ** by auto qed @@ -2454,7 +2454,7 @@ lemma simplex: assumes "finite s" "0 \ s" shows "convex hull (insert 0 s) = { y. (\u. (\x\s. 0 \ u x) \ setsum u s \ 1 \ setsum (\x. u x *\<^sub>R x) s = y)}" - unfolding convex_hull_finite[OF finite.insertI[OF assms(1)]] apply(rule set_ext, rule) unfolding mem_Collect_eq + unfolding convex_hull_finite[OF finite.insertI[OF assms(1)]] apply(rule set_eqI, rule) unfolding mem_Collect_eq apply(erule_tac[!] exE) apply(erule_tac[!] conjE)+ unfolding setsum_clauses(2)[OF assms(1)] apply(rule_tac x=u in exI) defer apply(rule_tac x="\x. if x = 0 then 1 - setsum u s else u x" in exI) using assms(2) unfolding if_smult and setsum_delta_notmem[OF assms(2)] by auto @@ -2467,7 +2467,7 @@ have *:"finite ?p" "0\?p" by auto have "{(basis i)::'a |i. ix\{basis i |i. i u x" "setsum u {basis i |i. i 1" "(\x\{basis i |i. iR x) = x" @@ -2500,7 +2500,7 @@ lemma interior_std_simplex: "interior (convex hull (insert 0 { basis i| i. ii setsum (\i. x$$i) {..xa. dist x xa < e \ (\x xa $$ x) \ setsum (op $$ xa) {.. 1" show "(\xa setsum (op $$ x) {..