author  wenzelm 
Fri, 10 Sep 1999 17:28:51 +0200  
changeset 7535  599d3414b51d 
child 7566  c5a3f980a7af 
permissions  rwrr 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

1 

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

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

3 

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

4 

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

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

6 

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

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

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

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

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

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

12 

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

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

14 
"[ <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

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

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

17 

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

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

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

20 

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

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

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

23 

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

24 
lemma subspace_subset: "is_subspace U V ==> U <= V"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

26 

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

27 
lemma subspace_subset2 [simp]: "[ is_subspace U V; x:U ]==> x:V"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

29 

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

30 
lemma subspace_add_closed [simp]: "[ is_subspace U V; x: U; y: U ] ==> x [+] y: U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

32 

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

33 
lemma subspace_mult_closed [simp]: "[ is_subspace U V; x: U ] ==> a [*] x: U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

35 

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

36 
lemma subspace_diff_closed [simp]: "[ is_subspace U V; x: U; y: U ] ==> x [] y: U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

37 
by (unfold diff_def negate_def) asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

38 

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

39 
lemma subspace_neg_closed [simp]: "[ is_subspace U V; x: U ] ==> [] x: U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

40 
by (unfold negate_def) asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

41 

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

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

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

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

45 
presume "U <= V"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

48 
show ?thesis; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

50 
show "<0>:U"; by (rule zero_in_subspace); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

53 
qed (asm_simp add: vs_add_mult_distrib1 vs_add_mult_distrib2)+; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

56 
show "U <= V"; by (rule subspace_subset); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

58 

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

59 
lemma subspace_refl: "is_vectorspace V ==> is_subspace V V"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

60 
proof (unfold is_subspace_def, intro conjI); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

62 
show "<0> : V"; by (rule zero_in_vs [of V], assumption); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

63 
show "V <= V"; by (simp); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

64 
show "ALL x::'a:V. ALL y::'a:V. ALL a::real. x [+] y : V & a [*] x : V"; by (asm_simp); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

66 

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

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

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

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

70 
show "<0> : U"; by (rule zero_in_subspace);; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

71 
from subspace_subset [of U] subspace_subset [of V]; show uw: "U <= W"; by force; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

74 
fix x y; assume "x:U" "y:U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

75 
show "x [+] y : U"; by (rule subspace_add_closed); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

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

79 
fix x a; assume "x:U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

80 
show "a [*] x : U"; by (rule subspace_mult_closed); 
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 
qed; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

83 

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

84 

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

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

86 

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

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

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

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

90 

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

91 
lemma linD: "x : lin v = (? a::real. x = a [*] v)"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

92 
by (unfold lin_def) fast; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

93 

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

94 
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

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

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

97 
show "x = 1r [*] x"; by (asm_simp); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

99 

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

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

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

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

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

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

105 
show "<0> = 0r [*] x"; by asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

108 
proof (unfold lin_def, intro subsetI, elim CollectD [elimify] exE); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

109 
fix xa a; assume "xa = a [*] x"; show "xa:V"; by asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

111 
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

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

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

114 
proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

115 
fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

116 
show "x1 [+] x2 = (a1 + a2) [*] x"; by (asm_simp add: vs_add_mult_distrib2); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

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

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

121 
fix x1 a; assume "x1 : lin x"; show "a [*] x1 : lin x"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

122 
proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

123 
fix a1; assume "x1 = a1 [*] x"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

124 
show "a [*] x1 = (a * a1) [*] x"; by asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

125 
qed; 
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; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

128 

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

129 

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

130 
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

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

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

133 
show "is_subspace (lin x) V"; by (rule lin_subspace); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

135 

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

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

137 

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

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

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

140 
"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

141 

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

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

143 
by (unfold vectorspace_sum_def) fast; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

144 

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

145 
lemma vs_sum_I: "[ x: U; y:V; (t::'a) = x [+] y ] ==> (t::'a) : vectorspace_sum U V"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

147 

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

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

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

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

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

152 
show "<0> : U"; by (rule zero_in_vs); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

153 
show "U <= vectorspace_sum U V"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

155 
fix x; assume "x:U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

156 
show "x = x [+] <0>"; by asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

157 
show "<0> : V"; by asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

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

161 
fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

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

165 
fix x a; assume "x:U"; show "a [*] x : U"; by asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

168 

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

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

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

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

172 
assume u: "is_subspace U E" and v: "is_subspace V E" and e: "is_vectorspace E"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

173 

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

174 
show "<0> : vectorspace_sum U V"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

175 
by (intro vs_sum_I, rule vs_add_zero_left [RS sym], 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

176 
rule zero_in_subspace, rule zero_in_subspace, rule zero_in_vs); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

177 

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

178 
show "vectorspace_sum U V <= E"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

179 
proof (intro subsetI, elim vs_sumD [RS iffD1, elimify] bexE); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

180 
fix x u v; assume "u : U" "v : V" "x = u [+] v"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

181 
show "x:E"; by (asm_simp); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

183 

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

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

185 
proof (intro ballI, elim vs_sumD [RS iffD1, elimify] bexE, intro vs_sum_I); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

186 
fix x y ux vx uy vy; assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

187 
show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

189 

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

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

191 
proof (intro ballI allI, elim vs_sumD [RS iffD1, elimify] bexE, intro vs_sum_I); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

192 
fix a x u v; assume "u : U" "v : V" "x = u [+] v"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

193 
show "a [*] x = (a [*] u) [+] (a [*] v)"; by (asm_simp add: vs_add_mult_distrib1 [OF e]); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

196 

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

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

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

199 
by (rule subspace_vs [OF vs_sum_subspace]); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

200 

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 
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

203 

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

204 

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

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

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

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

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

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

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

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

212 
have h: "is_vectorspace H"; by (rule subspace_vs); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

214 
by (rule vs_add_diff_swap) asm_simp+; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

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

218 

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

219 
have y: "y1 [] y2 : H"; by asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

220 
have x: "(a2  a1) [*] x0 : lin x0"; by (asm_simp add: lin_def) force; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

221 
from y; have y': "y1 [] y2 : lin x0"; by (simp only: eq x); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

222 
from x; have x': "(a2  a1) [*] x0 : H"; by (simp only: eq [RS sym] y); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

223 

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

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

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

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

227 
proof (intro subsetI, unfold lin_def, elim IntE CollectD[elimify] exE, 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

228 
rule singleton_iff[RS iffD2]); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

229 
fix x a; assume "x : H" and ax0: "x = a [*] x0"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

231 
proof (rule case [of "a=0r"]); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

232 
assume "a = 0r"; show ?thesis; by asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

234 
assume "a ~= 0r"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

235 
have "(rinv a) [*] a [*] x0 : H"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

236 
by (rule vs_mult_closed [OF h]) asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

237 
also; have "(rinv a) [*] a [*] x0 = x0"; by asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

238 
finally; have "x0 : H"; .; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

239 
thus ?thesis; by contradiction; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

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

243 
proof (intro subsetI, elim singletonD[elimify], intro IntI, asm_simp+); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

244 
show "<0> : H"; by (rule zero_in_vs [OF h]); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

245 
show "<0> : lin x0"; by (rule zero_in_vs [OF lin_vs]); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

248 

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

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

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

251 
show "y1 [] y2 = <0>"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

252 
by (rule Int_singeltonD [OF int y y']); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

254 

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

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

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

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

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

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

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

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

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

263 

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

264 

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

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

266 
"[ 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

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

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

269 
assume "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

270 
have h: "is_vectorspace H"; by (rule subspace_vs); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

271 
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

272 
have "y = t & a = 0r"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

273 
by (rule lemma4) (assumption+, asm_simp); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

274 
thus "(y, a) = (t, 0r)"; by asm_simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

276 

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

277 

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

278 
lemma lemma3: "!! x0 h xi x y a H. [ h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

279 
in (h y) + a * xi); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

281 
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

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

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

284 
fix x0 h xi x y a H; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

286 
in (h y) + a * xi)"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

288 
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

289 

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

290 
have "x : vectorspace_sum H (lin x0)"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

291 
by (asm_simp add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

292 
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

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

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

295 
by (asm_simp, rule exI, force); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

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

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

304 
have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by force; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

305 
have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by force; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

306 
from x y; show "fst xa = fst ya & snd xa = snd ya"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

307 
by (elim conjE) (rule lemma4, asm_simp+); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

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

311 
by (rule select1_equality, force); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

313 
by (asm_simp add: Let_def); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

315 

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

316 

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

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

318 

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

319 