author  wenzelm 
Tue, 21 Sep 1999 17:31:20 +0200  
changeset 7566  c5a3f980a7af 
parent 7535  599d3414b51d 
child 7567  62384a807775 
permissions  rwrr 
7566  1 
(* Title: HOL/Real/HahnBanach/Subspace.thy 
2 
ID: $Id$ 

3 
Author: Gertrud Bauer, TU Munich 

4 
*) 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

5 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

6 
theory Subspace = LinearSpace:; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

7 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

8 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

9 
section {* subspaces *}; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

10 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

11 
constdefs 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

12 
is_subspace :: "['a set, 'a set] => bool" 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

13 
"is_subspace U V == <0>:U & U <= V 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

14 
& (ALL x:U. ALL y:U. ALL a. x [+] y : U 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

15 
& a [*] x : U)"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

16 

7566  17 
lemma subspaceI [intro]: 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

18 
"[ <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); ALL x:U. ALL a. a [*] x : U ] 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

19 
\ ==> is_subspace U V"; 
7566  20 
by (unfold is_subspace_def) (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

21 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

22 
lemma "is_subspace U V ==> U ~= {}"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

23 
by (unfold is_subspace_def) force; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

24 

7566  25 
lemma zero_in_subspace [intro !!]: "is_subspace U V ==> <0>:U"; 
26 
by (unfold is_subspace_def) (simp!);; 

27 

28 
lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V"; 

29 
by (unfold is_subspace_def) (simp!); 

30 

31 
lemma subspace_subsetD [simp, intro!!]: "[ is_subspace U V; x:U ]==> x:V"; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

32 
by (unfold is_subspace_def) force; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

33 

7566  34 
lemma subspace_add_closed [simp, intro!!]: "[ is_subspace U V; x: U; y: U ] ==> x [+] y: U"; 
35 
by (unfold is_subspace_def) (simp!); 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

36 

7566  37 
lemma subspace_mult_closed [simp, intro!!]: "[ is_subspace U V; x: U ] ==> a [*] x: U"; 
38 
by (unfold is_subspace_def) (simp!); 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

39 

7566  40 
lemma subspace_diff_closed [simp, intro!!]: "[ is_subspace U V; x: U; y: U ] ==> x [] y: U"; 
41 
by (unfold diff_def negate_def) (simp!); 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

42 

7566  43 
lemma subspace_neg_closed [simp, intro!!]: "[ is_subspace U V; x: U ] ==> [] x: U"; 
44 
by (unfold negate_def) (simp!); 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

45 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

46 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

47 
theorem subspace_vs [intro!!]: 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

48 
"[ is_subspace U V; is_vectorspace V ] ==> is_vectorspace U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

49 
proof ; 
7566  50 
assume "is_subspace U V"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

51 
assume "is_vectorspace V"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

52 
assume "is_subspace U V"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

53 
show ?thesis; 
7566  54 
proof; 
55 
show "<0>:U"; ..; 

56 
show "ALL x:U. ALL a. a [*] x : U"; by (simp!); 

57 
show "ALL x:U. ALL y:U. x [+] y : U"; by (simp!); 

58 
qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

59 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

60 

7566  61 
lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V"; 
62 
proof; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

63 
assume "is_vectorspace V"; 
7566  64 
show "<0> : V"; ..; 
65 
show "V <= V"; ..; 

66 
show "ALL x:V. ALL y:V. x [+] y : V"; by (simp!); 

67 
show "ALL x:V. ALL a. a [*] x : V"; by (simp!); 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

68 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

69 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

70 
lemma subspace_trans: "[ is_subspace U V; is_subspace V W ] ==> is_subspace U W"; 
7566  71 
proof; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

72 
assume "is_subspace U V" "is_subspace V W"; 
7566  73 
show "<0> : U"; ..; 
74 
have "U <= V"; ..; 

75 
also; have "V <= W"; ..; 

76 
finally; show "U <= W"; .; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

77 
show "ALL x:U. ALL y:U. x [+] y : U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

78 
proof (intro ballI); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

79 
fix x y; assume "x:U" "y:U"; 
7566  80 
show "x [+] y : U"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

81 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

82 
show "ALL x:U. ALL a. a [*] x : U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

83 
proof (intro ballI allI); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

84 
fix x a; assume "x:U"; 
7566  85 
show "a [*] x : U"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

86 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

87 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

88 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

89 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

90 
section {* linear closure *}; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

91 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

92 
constdefs 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

93 
lin :: "'a => 'a set" 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

94 
"lin x == {y. ? a. y = a [*] x}"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

95 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

96 
lemma linD: "x : lin v = (? a::real. x = a [*] v)"; 
7566  97 
by (unfold lin_def) force; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

98 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

99 
lemma x_lin_x: "[ is_vectorspace V; x:V ] ==> x:lin x"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

100 
proof (unfold lin_def, intro CollectI exI); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

101 
assume "is_vectorspace V" "x:V"; 
7566  102 
show "x = 1r [*] x"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

103 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

104 

7566  105 
lemma lin_subspace [intro!!]: "[ is_vectorspace V; x:V ] ==> is_subspace (lin x) V"; 
106 
proof; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

107 
assume "is_vectorspace V" "x:V"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

108 
show "<0> : lin x"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

109 
proof (unfold lin_def, intro CollectI exI); 
7566  110 
show "<0> = 0r [*] x"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

111 
qed; 
7566  112 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

113 
show "lin x <= V"; 
7566  114 
proof (unfold lin_def, intro subsetI, elim CollectE exE); 
115 
fix xa a; assume "xa = a [*] x"; 

116 
show "xa:V"; by (simp!); 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

117 
qed; 
7566  118 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

119 
show "ALL x1 : lin x. ALL x2 : lin x. x1 [+] x2 : lin x"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

120 
proof (intro ballI); 
7566  121 
fix x1 x2; assume "x1 : lin x" "x2 : lin x"; 
122 
thus "x1 [+] x2 : lin x"; 

123 
proof (, unfold lin_def, elim CollectE exE, intro CollectI exI); (* FIXME !? *) 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

124 
fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x"; 
7566  125 
show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

126 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

127 
qed; 
7566  128 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

129 
show "ALL xa:lin x. ALL a. a [*] xa : lin x"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

130 
proof (intro ballI allI); 
7566  131 
fix x1 a; assume "x1 : lin x"; 
132 
thus "a [*] x1 : lin x"; 

133 
proof (, unfold lin_def, elim CollectE exE, intro CollectI exI); 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

134 
fix a1; assume "x1 = a1 [*] x"; 
7566  135 
show "a [*] x1 = (a * a1) [*] x"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

136 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

137 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

138 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

139 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

140 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

141 
lemma lin_vs [intro!!]: "[ is_vectorspace V; x:V ] ==> is_vectorspace (lin x)"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

142 
proof (rule subspace_vs); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

143 
assume "is_vectorspace V" "x:V"; 
7566  144 
show "is_subspace (lin x) V"; ..; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

145 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

146 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

147 
section {* sum of two vectorspaces *}; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

148 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

149 
constdefs 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

150 
vectorspace_sum :: "['a set, 'a set] => 'a set" 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

151 
"vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

152 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

153 
lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)"; 
7566  154 
by (unfold vectorspace_sum_def) (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

155 

7566  156 
lemmas vs_sumE = vs_sumD [RS iffD1, elimify]; 
157 

158 
lemma vs_sumI [intro!!]: "[ x: U; y:V; (t::'a) = x [+] y ] ==> (t::'a) : vectorspace_sum U V"; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

159 
by (unfold vectorspace_sum_def, intro CollectI bexI); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

160 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

161 
lemma subspace_vs_sum1 [intro!!]: 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

162 
"[ is_vectorspace U; is_vectorspace V ] ==> is_subspace U (vectorspace_sum U V)"; 
7566  163 
proof; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

164 
assume "is_vectorspace U" "is_vectorspace V"; 
7566  165 
show "<0> : U"; ..; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

166 
show "U <= vectorspace_sum U V"; 
7566  167 
proof (intro subsetI vs_sumI); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

168 
fix x; assume "x:U"; 
7566  169 
show "x = x [+] <0>"; by (simp!); 
170 
show "<0> : V"; by (simp!); 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

171 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

172 
show "ALL x:U. ALL y:U. x [+] y : U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

173 
proof (intro ballI); 
7566  174 
fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

175 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

176 
show "ALL x:U. ALL a. a [*] x : U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

177 
proof (intro ballI allI); 
7566  178 
fix x a; assume "x:U"; show "a [*] x : U"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

179 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

180 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

181 

7566  182 
lemma vs_sum_subspace [intro!!]: 
183 
"[ is_subspace U E; is_subspace V E; is_vectorspace E ] 

184 
==> is_subspace (vectorspace_sum U V) E"; 

185 
proof; 

186 
assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E"; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

187 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

188 
show "<0> : vectorspace_sum U V"; 
7566  189 
proof (intro vs_sumI); 
190 
show "<0> : U"; ..; 

191 
show "<0> : V"; ..; 

192 
show "(<0>::'a) = <0> [+] <0>"; 

193 
by (simp!); 

194 
qed; 

195 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

196 
show "vectorspace_sum U V <= E"; 
7566  197 
proof (intro subsetI, elim vs_sumE bexE); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

198 
fix x u v; assume "u : U" "v : V" "x = u [+] v"; 
7566  199 
show "x:E"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

200 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

201 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

202 
show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V"; 
7566  203 
proof (intro ballI); 
204 
fix x y; assume "x:vectorspace_sum U V" "y:vectorspace_sum U V"; 

205 
thus "x [+] y : vectorspace_sum U V"; 

206 
proof (elim vs_sumE bexE, intro vs_sumI); 

207 
fix ux vx uy vy; 

208 
assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy"; 

209 
show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by (simp!); 

210 
qed (simp!)+; 

211 
qed; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

212 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

213 
show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V"; 
7566  214 
proof (intro ballI allI); 
215 
fix x a; assume "x:vectorspace_sum U V"; 

216 
thus "a [*] x : vectorspace_sum U V"; 

217 
proof (elim vs_sumE bexE, intro vs_sumI); 

218 
fix a x u v; assume "u : U" "v : V" "x = u [+] v"; 

219 
show "a [*] x = (a [*] u) [+] (a [*] v)"; by (simp! add: vs_add_mult_distrib1); 

220 
qed (simp!)+; 

221 
qed; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

222 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

223 

7566  224 
lemma vs_sum_vs [intro!!]: 
225 
"[ is_subspace U E; is_subspace V E; is_vectorspace E ] 

226 
==> is_vectorspace (vectorspace_sum U V)"; 

227 
proof (rule subspace_vs); 

228 
assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"; 

229 
show "is_subspace (vectorspace_sum U V) E"; ..; 

230 
qed; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

231 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

232 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

233 
section {* special case: direct sum of a vectorspace and a linear closure of a vector *}; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

234 

7566  235 
lemma decomp4: "[ is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

236 
x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 ] 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

237 
==> y1 = y2 & a1 = a2"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

238 
proof; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

239 
assume "is_vectorspace E" "is_subspace H E" 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

240 
"y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

241 
"y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0"; 
7566  242 
have h: "is_vectorspace H"; ..; 
243 
have "y1 [] y2 = a2 [*] x0 [] a1 [*] x0"; 

244 
by (simp! add: vs_add_diff_swap); 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

245 
also; have "... = (a2  a1) [*] x0"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

246 
by (rule vs_diff_mult_distrib2 [RS sym]); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

247 
finally; have eq: "y1 [] y2 = (a2  a1) [*] x0"; .; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

248 

7566  249 
have y: "y1 [] y2 : H"; by (simp!); 
250 
have x: "(a2  a1) [*] x0 : lin x0"; by (simp! add: lin_def) force; 

251 
from eq y x; have y': "y1 [] y2 : lin x0"; by simp; 

252 
from eq y x; have x': "(a2  a1) [*] x0 : H"; by simp; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

253 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

254 
have int: "H Int (lin x0) = {<0>}"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

255 
proof; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

256 
show "H Int lin x0 <= {<0>}"; 
7566  257 
proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]); 
258 
fix x; assume "x:H" "x:lin x0"; 

259 
thus "x = <0>"; 

260 
proof (, unfold lin_def, elim CollectE exE); 

261 
fix a; assume "x = a [*] x0"; 

262 
show ?thesis; 

263 
proof (rule case [of "a = 0r"]); 

264 
assume "a = 0r"; show ?thesis; by (simp!); 

265 
next; 

266 
assume "a ~= 0r"; 

267 
have "(rinv a) [*] a [*] x0 : H"; 

268 
by (rule vs_mult_closed [OF h]) (simp!); 

269 
also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!); 

270 
finally; have "x0 : H"; .; 

271 
thus ?thesis; by contradiction; 

272 
qed; 

273 
qed; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

274 
qed; 
7566  275 
show "{<0>} <= H Int lin x0"; 
276 
proof (intro subsetI, elim singletonE, intro IntI, simp+); 

277 
show "<0> : H"; ..; 

278 
from lin_vs; show "<0> : lin x0"; ..; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

279 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

280 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

281 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

282 
from h; show "y1 = y2"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

283 
proof (rule vs_add_minus_eq); 
7566  284 
show "y1 [] y2 = <0>"; 
285 
by (rule Int_singletonD [OF int y y']); 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

286 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

287 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

288 
show "a1 = a2"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

289 
proof (rule real_add_minus_eq [RS sym]); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

290 
show "a2  a1 = 0r"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

291 
proof (rule vs_mult_zero_uniq); 
7566  292 
show "(a2  a1) [*] x0 = <0>"; by (rule Int_singletonD [OF int x' x]); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

293 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

294 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

295 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

296 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

297 

7566  298 
lemma decomp1: 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

299 
"[ is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> ] 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

300 
==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

301 
proof (rule, unfold split_paired_all); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

302 
assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>"; 
7566  303 
have h: "is_vectorspace H"; ..; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

304 
fix y a; presume t1: "t = y [+] a [*] x0" and "y : H"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

305 
have "y = t & a = 0r"; 
7566  306 
by (rule decomp4) (assumption+, (simp!)); 
307 
thus "(y, a) = (t, 0r)"; by (simp!); 

308 
qed (simp!)+; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

309 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

310 

7566  311 
lemma decomp3: 
312 
"[ h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 

313 
in (h y) + a * xi); 

314 
x = y [+] a [*] x0; 

315 
is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> ] 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

316 
==> h0 x = h y + a * xi"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

317 
proof ; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

318 
assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
7566  319 
in (h y) + a * xi)"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

320 
assume "x = y [+] a [*] x0"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

321 
assume "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

322 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

323 
have "x : vectorspace_sum H (lin x0)"; 
7566  324 
by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

325 
have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

326 
proof; 
7566  327 
show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
328 
by (force!); 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

329 
next; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

330 
fix xa ya; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

331 
assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa" 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

332 
"(%(y,a). x = y [+] a [*] x0 & y : H) ya"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

333 
show "xa = ya"; ; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

334 
proof ; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

335 
show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
7566  336 
by (rule Pair_fst_snd_eq [RS iffD2]); 
337 
have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by (force!); 

338 
have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by (force!); 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

339 
from x y; show "fst xa = fst ya & snd xa = snd ya"; 
7566  340 
by (elim conjE) (rule decomp4, (simp!)+); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

341 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

342 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

343 
hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; 
7566  344 
by (rule select1_equality) (force!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

345 
thus "h0 x = h y + a * xi"; 
7566  346 
by (simp! add: Let_def); 
347 
qed; 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

348 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

349 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

350 
end; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

351 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

352 