# HG changeset patch # User hoelzl # Date 1258380203 -3600 # Node ID 8cce3a34c1222a22c921573108702b5d37c0f19f # Parent eb2574ac417369914543eb7f04e2226e146686e7 removed hassize predicate diff -r eb2574ac4173 -r 8cce3a34c122 src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Mon Nov 16 15:06:34 2009 +0100 +++ b/src/HOL/Library/Permutations.thy Mon Nov 16 15:03:23 2009 +0100 @@ -152,78 +152,66 @@ thus ?thesis by auto qed -lemma hassize_insert: "a \ F \ insert a F hassize n \ F hassize (n - 1)" - by (auto simp add: hassize_def) - -lemma hassize_permutations: assumes Sn: "S hassize n" - shows "{p. p permutes S} hassize (fact n)" -proof- - from Sn have fS:"finite S" by (simp add: hassize_def) - - have "\n. (S hassize n) \ ({p. p permutes S} hassize (fact n))" - proof(rule finite_induct[where F = S]) - from fS show "finite S" . - next - show "\n. ({} hassize n) \ ({p. p permutes {}} hassize fact n)" - by (simp add: hassize_def permutes_empty) - next - fix x F - assume fF: "finite F" and xF: "x \ F" - and H: "\n. (F hassize n) \ ({p. p permutes F} hassize fact n)" - {fix n assume H0: "insert x F hassize n" - let ?xF = "{p. p permutes insert x F}" - let ?pF = "{p. p permutes F}" - let ?pF' = "{(b, p). b \ insert x F \ p \ ?pF}" - let ?g = "(\(b, p). Fun.swap x b id \ p)" - from permutes_insert[of x F] - have xfgpF': "?xF = ?g ` ?pF'" . - from hassize_insert[OF xF H0] have Fs: "F hassize (n - 1)" . - from H Fs have pFs: "?pF hassize fact (n - 1)" by blast - hence pF'f: "finite ?pF'" using H0 unfolding hassize_def - apply (simp only: Collect_split Collect_mem_eq) - apply (rule finite_cartesian_product) - apply simp_all - done +lemma card_permutations: assumes Sn: "card S = n" and fS: "finite S" + shows "card {p. p permutes S} = fact n" +using fS Sn proof (induct arbitrary: n) + case empty thus ?case by (simp add: permutes_empty) +next + case (insert x F) + { fix n assume H0: "card (insert x F) = n" + let ?xF = "{p. p permutes insert x F}" + let ?pF = "{p. p permutes F}" + let ?pF' = "{(b, p). b \ insert x F \ p \ ?pF}" + let ?g = "(\(b, p). Fun.swap x b id \ p)" + from permutes_insert[of x F] + have xfgpF': "?xF = ?g ` ?pF'" . + have Fs: "card F = n - 1" using `x \ F` H0 `finite F` by auto + from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" using `finite F` by auto + moreover hence "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite) + ultimately have pF'f: "finite ?pF'" using H0 `finite F` + apply (simp only: Collect_split Collect_mem_eq) + apply (rule finite_cartesian_product) + apply simp_all + done - have ginj: "inj_on ?g ?pF'" - proof- - { - fix b p c q assume bp: "(b,p) \ ?pF'" and cq: "(c,q) \ ?pF'" - and eq: "?g (b,p) = ?g (c,q)" - from bp cq have ths: "b \ insert x F" "c \ insert x F" "x \ insert x F" "p permutes F" "q permutes F" by auto - from ths(4) xF eq have "b = ?g (b,p) x" unfolding permutes_def - by (auto simp add: swap_def fun_upd_def expand_fun_eq) - also have "\ = ?g (c,q) x" using ths(5) xF eq - by (auto simp add: swap_def fun_upd_def expand_fun_eq) - also have "\ = c"using ths(5) xF unfolding permutes_def - by (auto simp add: swap_def fun_upd_def expand_fun_eq) - finally have bc: "b = c" . - hence "Fun.swap x b id = Fun.swap x c id" by simp - with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp - hence "Fun.swap x b id o (Fun.swap x b id o p) = Fun.swap x b id o (Fun.swap x b id o q)" by simp - hence "p = q" by (simp add: o_assoc) - with bc have "(b,p) = (c,q)" by simp } - thus ?thesis unfolding inj_on_def by blast - qed - from xF H0 have n0: "n \ 0 " by (auto simp add: hassize_def) - hence "\m. n = Suc m" by arith - then obtain m where n[simp]: "n = Suc m" by blast - from pFs H0 have xFc: "card ?xF = fact n" - unfolding xfgpF' card_image[OF ginj] hassize_def - apply (simp only: Collect_split Collect_mem_eq card_cartesian_product) - by simp - from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp - have "?xF hassize fact n" - using xFf xFc - unfolding hassize_def xFf by blast } - thus "\n. (insert x F hassize n) \ ({p. p permutes insert x F} hassize fact n)" - by blast - qed - with Sn show ?thesis by blast + have ginj: "inj_on ?g ?pF'" + proof- + { + fix b p c q assume bp: "(b,p) \ ?pF'" and cq: "(c,q) \ ?pF'" + and eq: "?g (b,p) = ?g (c,q)" + from bp cq have ths: "b \ insert x F" "c \ insert x F" "x \ insert x F" "p permutes F" "q permutes F" by auto + from ths(4) `x \ F` eq have "b = ?g (b,p) x" unfolding permutes_def + by (auto simp add: swap_def fun_upd_def expand_fun_eq) + also have "\ = ?g (c,q) x" using ths(5) `x \ F` eq + by (auto simp add: swap_def fun_upd_def expand_fun_eq) + also have "\ = c"using ths(5) `x \ F` unfolding permutes_def + by (auto simp add: swap_def fun_upd_def expand_fun_eq) + finally have bc: "b = c" . + hence "Fun.swap x b id = Fun.swap x c id" by simp + with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp + hence "Fun.swap x b id o (Fun.swap x b id o p) = Fun.swap x b id o (Fun.swap x b id o q)" by simp + hence "p = q" by (simp add: o_assoc) + with bc have "(b,p) = (c,q)" by simp + } + thus ?thesis unfolding inj_on_def by blast + qed + from `x \ F` H0 have n0: "n \ 0 " using `finite F` by auto + hence "\m. n = Suc m" by arith + then obtain m where n[simp]: "n = Suc m" by blast + from pFs H0 have xFc: "card ?xF = fact n" + unfolding xfgpF' card_image[OF ginj] using `finite F` `finite ?pF` + apply (simp only: Collect_split Collect_mem_eq card_cartesian_product) + by simp + from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp + have "card ?xF = fact n" + using xFf xFc unfolding xFf by blast + } + thus ?case using insert by simp qed -lemma finite_permutations: "finite S ==> finite {p. p permutes S}" - using hassize_permutations[of S] unfolding hassize_def by blast +lemma finite_permutations: assumes fS: "finite S" shows "finite {p. p permutes S}" + using card_permutations[OF refl fS] fact_gt_zero_nat + by (auto intro: card_ge_0_finite) (* ------------------------------------------------------------------------- *) (* Permutations of index set for iterated operations. *) diff -r eb2574ac4173 -r 8cce3a34c122 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Nov 16 15:06:34 2009 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Nov 16 15:03:23 2009 +0100 @@ -1955,16 +1955,17 @@ subsection {* Helly's theorem. *} lemma helly_induct: fixes f::"(real^'n::finite) set set" - assumes "f hassize n" "n \ CARD('n) + 1" + assumes "card f = n" "n \ CARD('n) + 1" "\s\f. convex s" "\t\f. card t = CARD('n) + 1 \ \ t \ {}" shows "\ f \ {}" - using assms unfolding hassize_def apply(erule_tac conjE) proof(induct n arbitrary: f) +using assms proof(induct n arbitrary: f) case (Suc n) -show "\ f \ {}" apply(cases "n = CARD('n)") apply(rule Suc(4)[rule_format]) - unfolding card_Diff_singleton_if[OF Suc(5)] and Suc(6) proof- +have "finite f" using `card f = Suc n` by (auto intro: card_ge_0_finite) +show "\ f \ {}" apply(cases "n = CARD('n)") apply(rule Suc(5)[rule_format]) + unfolding `card f = Suc n` proof- assume ng:"n \ CARD('n)" hence "\X. \s\f. X s \ \(f - {s})" apply(rule_tac bchoice) unfolding ex_in_conv - apply(rule, rule Suc(1)[rule_format]) unfolding card_Diff_singleton_if[OF Suc(5)] and Suc(6) - defer apply(rule Suc(3)[rule_format]) defer apply(rule Suc(4)[rule_format]) using Suc(2,5) by auto + apply(rule, rule Suc(1)[rule_format]) unfolding card_Diff_singleton_if[OF `finite f`] `card f = Suc n` + defer defer apply(rule Suc(4)[rule_format]) defer apply(rule Suc(5)[rule_format]) using Suc(3) `finite f` by auto then obtain X where X:"\s\f. X s \ \(f - {s})" by auto show ?thesis proof(cases "inj_on X f") case False then obtain s t where st:"s\t" "s\f" "t\f" "X s = X t" unfolding inj_on_def by auto @@ -1973,7 +1974,7 @@ apply(rule, rule X[rule_format]) using X st by auto next case True then obtain m p where mp:"m \ p = {}" "m \ p = X ` f" "convex hull m \ convex hull p \ {}" using radon_partition[of "X ` f"] and affine_dependent_biggerset[of "X ` f"] - unfolding card_image[OF True] and Suc(6) using Suc(2,5) and ng by auto + unfolding card_image[OF True] and `card f = Suc n` using Suc(3) `finite f` and ng by auto have "m \ X ` f" "p \ X ` f" using mp(2) by auto then obtain g h where gh:"m = X ` g" "p = X ` h" "g \ f" "h \ f" unfolding subset_image_iff by auto hence "f \ (g \ h) = f" by auto @@ -1981,7 +1982,7 @@ unfolding mp(2)[unfolded image_Un[THEN sym] gh] by auto have *:"g \ h = {}" using mp(1) unfolding gh using inj_on_image_Int[OF True gh(3,4)] by auto have "convex hull (X ` h) \ \ g" "convex hull (X ` g) \ \ h" - apply(rule_tac [!] hull_minimal) using Suc(3) gh(3-4) unfolding mem_def unfolding subset_eq + apply(rule_tac [!] hull_minimal) using Suc gh(3-4) unfolding mem_def unfolding subset_eq apply(rule_tac [2] convex_Inter, rule_tac [4] convex_Inter) apply rule prefer 3 apply rule proof- fix x assume "x\X ` g" then guess y unfolding image_iff .. thus "x\\h" using X[THEN bspec[where x=y]] using * f by auto next @@ -1992,10 +1993,10 @@ qed(insert dimindex_ge_1, auto) qed(auto) lemma helly: fixes f::"(real^'n::finite) set set" - assumes "finite f" "card f \ CARD('n) + 1" "\s\f. convex s" + assumes "card f \ CARD('n) + 1" "\s\f. convex s" "\t\f. card t = CARD('n) + 1 \ \ t \ {}" shows "\ f \{}" - apply(rule helly_induct) unfolding hassize_def using assms by auto + apply(rule helly_induct) using assms by auto subsection {* Convex hull is "preserved" by a linear function. *} diff -r eb2574ac4173 -r 8cce3a34c122 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Nov 16 15:06:34 2009 +0100 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Nov 16 15:03:23 2009 +0100 @@ -3436,21 +3436,18 @@ apply (auto simp add: Collect_def mem_def) done -lemma has_size_stdbasis: "{basis i ::real ^'n::finite | i. i \ (UNIV :: 'n set)} hassize CARD('n)" (is "?S hassize ?n") +lemma finite_stdbasis: "finite {basis i ::real^'n::finite |i. i\ (UNIV:: 'n set)}" (is "finite ?S") proof- have eq: "?S = basis ` UNIV" by blast - show ?thesis unfolding eq - apply (rule hassize_image_inj[OF basis_inj]) - by (simp add: hassize_def) + show ?thesis unfolding eq by auto qed -lemma finite_stdbasis: "finite {basis i ::real^'n::finite |i. i\ (UNIV:: 'n set)}" - using has_size_stdbasis[unfolded hassize_def] - .. - -lemma card_stdbasis: "card {basis i ::real^'n::finite |i. i\ (UNIV :: 'n set)} = CARD('n)" - using has_size_stdbasis[unfolded hassize_def] - .. +lemma card_stdbasis: "card {basis i ::real^'n::finite |i. i\ (UNIV :: 'n set)} = CARD('n)" (is "card ?S = _") +proof- + have eq: "?S = basis ` UNIV" by blast + show ?thesis unfolding eq using card_image[OF basis_inj] by simp +qed + lemma independent_stdbasis_lemma: assumes x: "(x::'a::semiring_1 ^ 'n) \ span (basis ` S)" @@ -3571,7 +3568,7 @@ lemma exchange_lemma: assumes f:"finite (t:: ('a::field^'n) set)" and i: "independent s" and sp:"s \ span t" - shows "\t'. (t' hassize card t) \ s \ t' \ t' \ s \ t \ s \ span t'" + shows "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" using f i sp proof(induct c\"card(t - s)" arbitrary: s t rule: nat_less_induct) fix n:: nat and s t :: "('a ^'n) set" @@ -3580,21 +3577,21 @@ independent x \ x \ span xa \ m = card (xa - x) \ - (\t'. (t' hassize card xa) \ + (\t'. (card t' = card xa) \ finite t' \ x \ t' \ t' \ x \ xa \ x \ span t')" and ft: "finite t" and s: "independent s" and sp: "s \ span t" and n: "n = card (t - s)" - let ?P = "\t'. (t' hassize card t) \ s \ t' \ t' \ s \ t \ s \ span t'" + let ?P = "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ span t'" let ?ths = "\t'. ?P t'" {assume st: "s \ t" from st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t]) - by (auto simp add: hassize_def intro: span_superset)} + by (auto intro: span_superset)} moreover {assume st: "t \ s" from spanning_subset_independent[OF st s sp] st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t]) - by (auto simp add: hassize_def intro: span_superset)} + by (auto intro: span_superset)} moreover {assume st: "\ s \ t" "\ t \ s" from st(2) obtain b where b: "b \ t" "b \ s" by blast @@ -3605,20 +3602,20 @@ {assume stb: "s \ span(t -{b})" from ft have ftb: "finite (t -{b})" by auto from H[rule_format, OF cardlt ftb s stb] - obtain u where u: "u hassize card (t-{b})" "s \ u" "u \ s \ (t - {b})" "s \ span u" by blast + obtain u where u: "card u = card (t-{b})" "s \ u" "u \ s \ (t - {b})" "s \ span u" and fu: "finite u" by blast let ?w = "insert b u" have th0: "s \ insert b u" using u by blast from u(3) b have "u \ s \ t" by blast then have th1: "insert b u \ s \ t" using u b by blast have bu: "b \ u" using b u by blast - from u(1) have fu: "finite u" by (simp add: hassize_def) - from u(1) ft b have "u hassize (card t - 1)" by auto + from u(1) ft b have "card u = (card t - 1)" by auto then - have th2: "insert b u hassize card t" - using card_insert_disjoint[OF fu bu] ct0 by (auto simp add: hassize_def) + have th2: "card (insert b u) = card t" + using card_insert_disjoint[OF fu bu] ct0 by auto from u(4) have "s \ span u" . also have "\ \ span (insert b u)" apply (rule span_mono) by blast - finally have th3: "s \ span (insert b u)" . from th0 th1 th2 th3 have th: "?P ?w" by blast + finally have th3: "s \ span (insert b u)" . + from th0 th1 th2 th3 fu have th: "?P ?w" by blast from th have ?ths by blast} moreover {assume stb: "\ s \ span(t -{b})" @@ -3640,9 +3637,9 @@ then have sp': "s \ span (insert a (t - {b}))" by blast from H[rule_format, OF mlt ft' s sp' refl] obtain u where - u: "u hassize card (insert a (t -{b}))" "s \ u" "u \ s \ insert a (t -{b})" + u: "card u = card (insert a (t -{b}))" "finite u" "s \ u" "u \ s \ insert a (t -{b})" "s \ span u" by blast - from u a b ft at ct0 have "?P u" by (auto simp add: hassize_def) + from u a b ft at ct0 have "?P u" by auto then have ?ths by blast } ultimately have ?ths by blast } @@ -3655,7 +3652,7 @@ lemma independent_span_bound: assumes f: "finite t" and i: "independent (s::('a::field^'n) set)" and sp:"s \ span t" shows "finite s \ card s \ card t" - by (metis exchange_lemma[OF f i sp] hassize_def finite_subset card_mono) + by (metis exchange_lemma[OF f i sp] finite_subset card_mono) lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\ (UNIV::'a::finite set)}" @@ -3723,39 +3720,44 @@ (* Notion of dimension. *) -definition "dim V = (SOME n. \B. B \ V \ independent B \ V \ span B \ (B hassize n))" - -lemma basis_exists: "\B. (B :: (real ^'n::finite) set) \ V \ independent B \ V \ span B \ (B hassize dim V)" -unfolding dim_def some_eq_ex[of "\n. \B. B \ V \ independent B \ V \ span B \ (B hassize n)"] -unfolding hassize_def +definition "dim V = (SOME n. \B. B \ V \ independent B \ V \ span B \ (card B = n))" + +lemma basis_exists: "\B. (B :: (real ^'n::finite) set) \ V \ independent B \ V \ span B \ (card B = dim V)" +unfolding dim_def some_eq_ex[of "\n. \B. B \ V \ independent B \ V \ span B \ (card B = n)"] using maximal_independent_subset[of V] independent_bound by auto (* Consequences of independence or spanning for cardinality. *) -lemma independent_card_le_dim: "(B::(real ^'n::finite) set) \ V \ independent B \ finite B \ card B \ dim V" -by (metis basis_exists[of V] independent_span_bound[where ?'a=real] hassize_def subset_trans) +lemma independent_card_le_dim: + assumes "(B::(real ^'n::finite) set) \ V" and "independent B" shows "card B \ dim V" +proof - + from basis_exists[of V] `B \ V` + obtain B' where "independent B'" and "B \ span B'" and "card B' = dim V" by blast + with independent_span_bound[OF _ `independent B` `B \ span B'`] independent_bound[of B'] + show ?thesis by auto +qed lemma span_card_ge_dim: "(B::(real ^'n::finite) set) \ V \ V \ span B \ finite B \ dim V \ card B" - by (metis basis_exists[of V] independent_span_bound hassize_def subset_trans) + by (metis basis_exists[of V] independent_span_bound subset_trans) lemma basis_card_eq_dim: "B \ (V:: (real ^'n::finite) set) \ V \ span B \ independent B \ finite B \ card B = dim V" - by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_mono) - -lemma dim_unique: "(B::(real ^'n::finite) set) \ V \ V \ span B \ independent B \ B hassize n \ dim V = n" - by (metis basis_card_eq_dim hassize_def) + by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_mono independent_bound) + +lemma dim_unique: "(B::(real ^'n::finite) set) \ V \ V \ span B \ independent B \ card B = n \ dim V = n" + by (metis basis_card_eq_dim) (* More lemmas about dimension. *) lemma dim_univ: "dim (UNIV :: (real^'n::finite) set) = CARD('n)" apply (rule dim_unique[of "{basis i |i. i\ (UNIV :: 'n set)}"]) - by (auto simp only: span_stdbasis has_size_stdbasis independent_stdbasis) + by (auto simp only: span_stdbasis card_stdbasis finite_stdbasis independent_stdbasis) lemma dim_subset: "(S:: (real ^'n::finite) set) \ T \ dim S \ dim T" using basis_exists[of T] basis_exists[of S] - by (metis independent_span_bound[where ?'a = real and ?'n = 'n] subset_eq hassize_def) + by (metis independent_card_le_dim subset_trans) lemma dim_subset_univ: "dim (S:: (real^'n::finite) set) \ CARD('n)" by (metis dim_subset subset_UNIV dim_univ) @@ -3771,7 +3773,7 @@ then have iaB: "independent (insert a B)" using iB aV BV by (simp add: independent_insert) from aV BV have th0: "insert a B \ V" by blast from aB have "a \B" by (auto simp add: span_superset) - with independent_card_le_dim[OF th0 iaB] dVB have False by auto} + with independent_card_le_dim[OF th0 iaB] dVB independent_bound[OF iB] have False by auto } then have "a \ span B" by blast} then show ?thesis by blast qed @@ -3798,8 +3800,8 @@ then show ?thesis unfolding dependent_def by blast qed -lemma card_eq_dim: "(B:: (real ^'n::finite) set) \ V \ B hassize dim V \ independent B \ V \ span B" - by (metis hassize_def order_eq_iff card_le_dim_spanning +lemma card_eq_dim: "(B:: (real ^'n::finite) set) \ V \ card B = dim V \ finite B \ independent B \ V \ span B" + by (metis order_eq_iff card_le_dim_spanning card_ge_dim_independent) (* ------------------------------------------------------------------------- *) @@ -3818,8 +3820,8 @@ have th0: "dim S \ dim (span S)" by (auto simp add: subset_eq intro: dim_subset span_superset) from basis_exists[of S] - obtain B where B: "B \ S" "independent B" "S \ span B" "B hassize dim S" by blast - from B have fB: "finite B" "card B = dim S" unfolding hassize_def by blast+ + obtain B where B: "B \ S" "independent B" "S \ span B" "card B = dim S" by blast + from B have fB: "finite B" "card B = dim S" using independent_bound by blast+ have bSS: "B \ span S" using B(1) by (metis subset_eq span_inc) have sssB: "span S \ span B" using span_mono[OF B(3)] by (simp add: span_span) from span_card_ge_dim[OF bSS sssB fB(1)] th0 show ?thesis @@ -3843,8 +3845,8 @@ assumes lf: "linear f" shows "dim (f ` S) \ dim (S:: (real ^'n::finite) set)" proof- from basis_exists[of S] obtain B where - B: "B \ S" "independent B" "S \ span B" "B hassize dim S" by blast - from B have fB: "finite B" "card B = dim S" unfolding hassize_def by blast+ + B: "B \ S" "independent B" "S \ span B" "card B = dim S" by blast + from B have fB: "finite B" "card B = dim S" using independent_bound by blast+ have "dim (f ` S) \ card (f ` B)" apply (rule span_card_ge_dim) using lf B fB by (auto simp add: span_linear_image spans_image subset_image_iff) @@ -3968,10 +3970,10 @@ lemma orthogonal_basis_exists: fixes V :: "(real ^'n::finite) set" - shows "\B. independent B \ B \ span V \ V \ span B \ (B hassize dim V) \ pairwise orthogonal B" + shows "\B. independent B \ B \ span V \ V \ span B \ (card B = dim V) \ pairwise orthogonal B" proof- - from basis_exists[of V] obtain B where B: "B \ V" "independent B" "V \ span B" "B hassize dim V" by blast - from B have fB: "finite B" "card B = dim V" by (simp_all add: hassize_def) + from basis_exists[of V] obtain B where B: "B \ V" "independent B" "V \ span B" "card B = dim V" by blast + from B have fB: "finite B" "card B = dim V" using independent_bound by auto from basis_orthogonal[OF fB(1)] obtain C where C: "finite C" "card C \ card B" "span C = span B" "pairwise orthogonal C" by blast from C B @@ -3982,7 +3984,7 @@ from C fB have "card C \ dim V" by simp moreover have "dim V \ card C" using span_card_ge_dim[OF CSV SVC C(1)] by (simp add: dim_span) - ultimately have CdV: "C hassize dim V" unfolding hassize_def using C(1) by simp + ultimately have CdV: "card C = dim V" using C(1) by simp from C B CSV CdV iC show ?thesis by auto qed @@ -3999,9 +4001,9 @@ proof- from sU obtain a where a: "a \ span S" by blast from orthogonal_basis_exists obtain B where - B: "independent B" "B \ span S" "S \ span B" "B hassize dim S" "pairwise orthogonal B" + B: "independent B" "B \ span S" "S \ span B" "card B = dim S" "pairwise orthogonal B" by blast - from B have fB: "finite B" "card B = dim S" by (simp_all add: hassize_def) + from B have fB: "finite B" "card B = dim S" using independent_bound by auto from span_mono[OF B(2)] span_mono[OF B(3)] have sSB: "span S = span B" by (simp add: span_span) let ?a = "a - setsum (\b. (a\b / (b\b)) *s b) B" @@ -4249,20 +4251,18 @@ and d: "dim S = dim T" shows "\f. linear f \ f ` S = T \ inj_on f S" proof- - from basis_exists[of S] obtain B where - B: "B \ S" "independent B" "S \ span B" "B hassize dim S" by blast - from basis_exists[of T] obtain C where - C: "C \ T" "independent C" "T \ span C" "C hassize dim T" by blast + from basis_exists[of S] independent_bound obtain B where + B: "B \ S" "independent B" "S \ span B" "card B = dim S" and fB: "finite B" by blast + from basis_exists[of T] independent_bound obtain C where + C: "C \ T" "independent C" "T \ span C" "card C = dim T" and fC: "finite C" by blast from B(4) C(4) card_le_inj[of B C] d obtain f where - f: "f ` B \ C" "inj_on f B" unfolding hassize_def by auto + f: "f ` B \ C" "inj_on f B" using `finite B` `finite C` by auto from linear_independent_extend[OF B(2)] obtain g where g: "linear g" "\x\ B. g x = f x" by blast - from B(4) have fB: "finite B" by (simp add: hassize_def) - from C(4) have fC: "finite C" by (simp add: hassize_def) from inj_on_iff_eq_card[OF fB, of f] f(2) have "card (f ` B) = card B" by simp with B(4) C(4) have ceq: "card (f ` B) = card C" using d - by (simp add: hassize_def) + by simp have "g ` B = f ` B" using g(2) by (auto simp add: image_iff) also have "\ = C" using card_subset_eq[OF fC f(1) ceq] . @@ -4578,9 +4578,9 @@ proof- let ?U = "UNIV :: (real ^'n) set" from basis_exists[of ?U] obtain B - where B: "B \ ?U" "independent B" "?U \ span B" "B hassize dim ?U" + where B: "B \ ?U" "independent B" "?U \ span B" "card B = dim ?U" by blast - from B(4) have d: "dim ?U = card B" by (simp add: hassize_def) + from B(4) have d: "dim ?U = card B" by simp have th: "?U \ span (f ` B)" apply (rule card_ge_dim_independent) apply blast @@ -4640,11 +4640,10 @@ proof- let ?U = "UNIV :: (real ^'n) set" from basis_exists[of ?U] obtain B - where B: "B \ ?U" "independent B" "?U \ span B" "B hassize dim ?U" + where B: "B \ ?U" "independent B" "?U \ span B" and d: "card B = dim ?U" by blast {fix x assume x: "x \ span B" and fx: "f x = 0" - from B(4) have fB: "finite B" by (simp add: hassize_def) - from B(4) have d: "dim ?U = card B" by (simp add: hassize_def) + from B(2) have fB: "finite B" using independent_bound by auto have fBi: "independent (f ` B)" apply (rule card_le_dim_spanning[of "f ` B" ?U]) apply blast @@ -4652,7 +4651,7 @@ unfolding span_linear_image[OF lf] surj_def subset_eq image_iff apply blast using fB apply (blast intro: finite_imageI) - unfolding d + unfolding d[symmetric] apply (rule card_image_le) apply (rule fB) done diff -r eb2574ac4173 -r 8cce3a34c122 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Nov 16 15:06:34 2009 +0100 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Nov 16 15:03:23 2009 +0100 @@ -8,15 +8,6 @@ imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*) begin -definition hassize (infixr "hassize" 12) where - "(S hassize n) = (finite S \ card S = n)" - -lemma hassize_image_inj: assumes f: "inj_on f S" and S: "S hassize n" - shows "f ` S hassize n" - using f S card_image[OF f] - by (simp add: hassize_def inj_on_def) - - subsection {* Finite Cartesian products, with indexing and lambdas. *} typedef (open Cart) diff -r eb2574ac4173 -r 8cce3a34c122 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Nov 16 15:06:34 2009 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Nov 16 15:03:23 2009 +0100 @@ -5629,7 +5629,7 @@ moreover have "d \ ?D" unfolding subset_eq using assms by auto hence *:"inj_on (basis::'n\real^'n) d" using subset_inj_on[OF basis_inj, of "d"] by auto - have "?B hassize (card d)" unfolding hassize_def and card_image[OF *] by auto + have "card ?B = card d" unfolding card_image[OF *] by auto ultimately show ?thesis using dim_unique[of "basis ` d" ?A] by auto qed