diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/Subspace.thy --- a/src/HOL/Real/HahnBanach/Subspace.thy Fri Oct 08 16:18:51 1999 +0200 +++ b/src/HOL/Real/HahnBanach/Subspace.thy Fri Oct 08 16:40:27 1999 +0200 @@ -3,10 +3,13 @@ Author: Gertrud Bauer, TU Munich *) + +header {* Subspaces *}; + theory Subspace = LinearSpace:; -section {* subspaces *}; +subsection {* Subspaces *}; constdefs is_subspace :: "['a set, 'a set] => bool" @@ -15,8 +18,9 @@ & a [*] x : U)"; lemma subspaceI [intro]: - "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); ALL x:U. ALL a. a [*] x : U |] - \ ==> is_subspace U V"; + "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); + ALL x:U. ALL a. a [*] x : U |] + ==> is_subspace U V"; by (unfold is_subspace_def) simp; lemma "is_subspace U V ==> U ~= {}"; @@ -28,23 +32,27 @@ lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V"; by (unfold is_subspace_def) simp; -lemma subspace_subsetD [simp, intro!!]: "[| is_subspace U V; x:U |]==> x:V"; +lemma subspace_subsetD [simp, intro!!]: + "[| is_subspace U V; x:U |]==> x:V"; by (unfold is_subspace_def) force; -lemma subspace_add_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U"; - by (unfold is_subspace_def) simp; - -lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U"; +lemma subspace_add_closed [simp, intro!!]: + "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U"; by (unfold is_subspace_def) simp; -lemma subspace_diff_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U"; +lemma subspace_mult_closed [simp, intro!!]: + "[| is_subspace U V; x: U |] ==> a [*] x: U"; + by (unfold is_subspace_def) simp; + +lemma subspace_diff_closed [simp, intro!!]: + "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U"; by (unfold diff_def negate_def) simp; -lemma subspace_neg_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> [-] x: U"; - by (unfold negate_def) simp; +lemma subspace_neg_closed [simp, intro!!]: + "[| is_subspace U V; x: U |] ==> [-] x: U"; + by (unfold negate_def) simp; - -theorem subspace_vs [intro!!]: +lemma subspace_vs [intro!!]: "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U"; proof -; assume "is_subspace U V" "is_vectorspace V"; @@ -65,7 +73,8 @@ show "ALL x:V. ALL a. a [*] x : V"; by (simp!); qed; -lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W"; +lemma subspace_trans: + "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W"; proof; assume "is_subspace U V" "is_subspace V W"; show "<0> : U"; ..; @@ -88,7 +97,9 @@ qed; -section {* linear closure *}; + +subsection {* Linear closure *}; + constdefs lin :: "'a => 'a set" @@ -106,7 +117,8 @@ show "x = 1r [*] x"; by (simp!); qed; -lemma lin_subspace [intro!!]: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V"; +lemma lin_subspace [intro!!]: + "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V"; proof; assume "is_vectorspace V" "x:V"; show "<0> : lin x"; @@ -126,7 +138,8 @@ thus "x1 [+] x2 : lin x"; proof (unfold lin_def, elim CollectE exE, intro CollectI exI); fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x"; - show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2); + show "x1 [+] x2 = (a1 + a2) [*] x"; + by (simp! add: vs_add_mult_distrib2); qed; qed; @@ -141,14 +154,17 @@ qed; qed; - -lemma lin_vs [intro!!]: "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)"; +lemma lin_vs [intro!!]: + "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)"; proof (rule subspace_vs); assume "is_vectorspace V" "x:V"; show "is_subspace (lin x) V"; ..; qed; -section {* sum of two vectorspaces *}; + + +subsection {* Sum of two vectorspaces *}; + constdefs vectorspace_sum :: "['a set, 'a set] => 'a set" @@ -159,11 +175,14 @@ lemmas vs_sumE = vs_sumD [RS iffD1, elimify]; -lemma vs_sumI [intro!!]: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V"; +lemma vs_sumI [intro!!]: + "[| x: U; y:V; (t::'a) = x [+] y |] + ==> (t::'a) : vectorspace_sum U V"; by (unfold vectorspace_sum_def, intro CollectI bexI); lemma subspace_vs_sum1 [intro!!]: - "[| is_vectorspace U; is_vectorspace V |] ==> is_subspace U (vectorspace_sum U V)"; + "[| is_vectorspace U; is_vectorspace V |] + ==> is_subspace U (vectorspace_sum U V)"; proof; assume "is_vectorspace U" "is_vectorspace V"; show "<0> : U"; ..; @@ -188,7 +207,6 @@ ==> is_subspace (vectorspace_sum U V) E"; proof; assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E"; - show "<0> : vectorspace_sum U V"; proof (intro vs_sumI); show "<0> : U"; ..; @@ -202,24 +220,28 @@ show "x:E"; by (simp!); qed; - show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V"; + show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. + x [+] y : vectorspace_sum U V"; proof (intro ballI); fix x y; assume "x:vectorspace_sum U V" "y:vectorspace_sum U V"; thus "x [+] y : vectorspace_sum U V"; proof (elim vs_sumE bexE, intro vs_sumI); fix ux vx uy vy; - assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy"; + assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" + "y = uy [+] vy"; show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by (simp!); qed (simp!)+; qed; - show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V"; + show "ALL x:vectorspace_sum U V. ALL a. + a [*] x : vectorspace_sum U V"; proof (intro ballI allI); fix x a; assume "x:vectorspace_sum U V"; thus "a [*] x : vectorspace_sum U V"; proof (elim vs_sumE bexE, intro vs_sumI); fix a x u v; assume "u : U" "v : V" "x = u [+] v"; - show "a [*] x = (a [*] u) [+] (a [*] v)"; by (simp! add: vs_add_mult_distrib1); + show "a [*] x = (a [*] u) [+] (a [*] v)"; + by (simp! add: vs_add_mult_distrib1); qed (simp!)+; qed; qed; @@ -233,17 +255,25 @@ qed; -section {* special case: direct sum of a vectorspace and a linear closure of a vector *}; + +subsection {* A special case *} + -lemma decomp: "[| is_vectorspace E; is_subspace U E; is_subspace V E; U Int V = {<0>}; - u1:U; u2:U; v1:V; v2:V; u1 [+] v1 = u2 [+] v2 |] +text {* direct sum of a vectorspace and a linear closure of a vector +*}; + +lemma decomp: "[| is_vectorspace E; is_subspace U E; is_subspace V E; + U Int V = {<0>}; u1:U; u2:U; v1:V; v2:V; u1 [+] v1 = u2 [+] v2 |] ==> u1 = u2 & v1 = v2"; proof; - assume "is_vectorspace E" "is_subspace U E" "is_subspace V E" "U Int V = {<0>}" - "u1:U" "u2:U" "v1:V" "v2:V" "u1 [+] v1 = u2 [+] v2"; + assume "is_vectorspace E" "is_subspace U E" "is_subspace V E" + "U Int V = {<0>}" "u1:U" "u2:U" "v1:V" "v2:V" + "u1 [+] v1 = u2 [+] v2"; have eq: "u1 [-] u2 = v2 [-] v1"; by (simp! add: vs_add_diff_swap); - have u: "u1 [-] u2 : U"; by (simp!); with eq; have v': "v2 [-] v1 : U"; by simp; - have v: "v2 [-] v1 : V"; by (simp!); with eq; have u': "u1 [-] u2 : V"; by simp; + have u: "u1 [-] u2 : U"; by (simp!); + with eq; have v': "v2 [-] v1 : U"; by simp; + have v: "v2 [-] v1 : V"; by (simp!); + with eq; have u': "u1 [-] u2 : V"; by simp; show "u1 = u2"; proof (rule vs_add_minus_eq); @@ -256,8 +286,8 @@ qed (rule); qed; -lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; - x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |] +lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; + x0 ~: H; x0 :E; x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |] ==> y1 = y2 & a1 = a2"; proof; assume "is_vectorspace E" and h: "is_subspace H E" @@ -281,7 +311,8 @@ assume "a = 0r"; show ?thesis; by (simp!); next; assume "a ~= 0r"; - from h; have "(rinv a) [*] a [*] x0 : H"; by (rule subspace_mult_closed) (simp!); + from h; have "(rinv a) [*] a [*] x0 : H"; + by (rule subspace_mult_closed) (simp!); also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!); finally; have "x0 : H"; .; thus ?thesis; by contradiction; @@ -306,10 +337,11 @@ qed; lemma decomp1: - "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |] + "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |] ==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)"; proof (rule, unfold split_paired_all); - assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>"; + assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" + "x0 ~= <0>"; have h: "is_vectorspace H"; ..; fix y a; presume t1: "t = y [+] a [*] x0" and "y : H"; have "y = t & a = 0r"; @@ -320,17 +352,17 @@ lemma decomp3: "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi); - x = y [+] a [*] x0; - is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |] + x = y [+] a [*] x0; is_vectorspace E; is_subspace H E; + y:H; x0 ~: H; x0:E; x0 ~= <0> |] ==> h0 x = h y + a * xi"; proof -; assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) in (h y) + a * xi)" - "x = y [+] a [*] x0" - "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>"; - + "x = y [+] a [*] x0" "is_vectorspace E" "is_subspace H E" + "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>"; have "x : vectorspace_sum H (lin x0)"; - by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+; + by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) + force+; have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; proof%%; show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; @@ -343,15 +375,17 @@ proof -; show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; by (rule Pair_fst_snd_eq [RS iffD2]); - have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by (force!); - have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by (force!); - from x y; show "fst xa = fst ya & snd xa = snd ya"; by (elim conjE) (rule decomp4, (simp!)+); + have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; + by (force!); + have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; + by (force!); + from x y; show "fst xa = fst ya & snd xa = snd ya"; + by (elim conjE) (rule decomp4, (simp!)+); qed; qed; - hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; by (rule select1_equality) (force!); + hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; + by (rule select1_equality) (force!); thus "h0 x = h y + a * xi"; by (simp! add: Let_def); qed; -end; - - +end; \ No newline at end of file