src/HOL/Real/HahnBanach/Subspace.thy
author wenzelm
Fri, 10 Sep 1999 17:28:51 +0200
changeset 7535 599d3414b51d
child 7566 c5a3f980a7af
permissions -rw-r--r--
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) (by Gertrud Bauer, TU Munich);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     1
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     2
theory Subspace = LinearSpace:;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     3
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     4
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     5
section {* subspaces *};
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     6
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     7
constdefs
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     8
  is_subspace ::  "['a set, 'a set] => bool"
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     9
  "is_subspace U V ==  <0>:U  & U <= V 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    10
     &  (ALL x:U. ALL y:U. ALL a. x [+] y : U                          
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    11
                       & a [*] x : U)";                            
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    12
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    13
lemma subspace_I: 
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    15
  \ ==> is_subspace U V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    16
  by (unfold is_subspace_def) blast;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    17
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    18
lemma "is_subspace U V ==> U ~= {}";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    19
  by (unfold is_subspace_def) force;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    20
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    21
lemma zero_in_subspace: "is_subspace U V ==> <0>:U";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    22
  by (unfold is_subspace_def) force;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    23
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    24
lemma subspace_subset: "is_subspace U V ==> U <= V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    25
  by (unfold is_subspace_def) fast;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    26
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    28
  by (unfold is_subspace_def) fast;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    29
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    31
  by (unfold is_subspace_def) asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    32
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    34
  by (unfold is_subspace_def) asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    35
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    37
  by (unfold diff_def negate_def) asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    38
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    40
 by (unfold negate_def) asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    41
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    42
theorem subspace_vs [intro!!]:
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    43
  "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    44
proof -;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    45
  presume "U <= V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    46
  assume "is_vectorspace V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    47
  assume "is_subspace U V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    48
  show ?thesis;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    49
  proof (rule vs_I);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    50
    show "<0>:U"; by (rule zero_in_subspace);
599d3414b51d The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    54
next;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    55
  assume "is_subspace U V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    56
  show "U <= V"; by (rule subspace_subset);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    57
qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    58
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    59
lemma subspace_refl: "is_vectorspace V ==> is_subspace V V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    60
proof (unfold is_subspace_def, intro conjI); 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    61
  assume "is_vectorspace V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    62
  show "<0> : V"; by (rule zero_in_vs [of V], assumption);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    63
  show "V <= V"; by (simp);
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    65
qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    66
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    68
proof (rule subspace_I); 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    69
  assume "is_subspace U V" "is_subspace V W";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    70
  show "<0> : U"; by (rule zero_in_subspace);;
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    72
  show "ALL x:U. ALL y:U. x [+] y : U"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    73
  proof (intro ballI);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    74
    fix x y; assume "x:U" "y:U";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    75
    show "x [+] y : U"; by (rule subspace_add_closed);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    76
  qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    77
  show "ALL x:U. ALL a. a [*] x : U";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    78
  proof (intro ballI allI);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    79
    fix x a; assume "x:U";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    80
    show "a [*] x : U"; by (rule subspace_mult_closed);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    81
  qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    82
qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    83
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    84
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    85
section {* linear closure *};
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    86
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    87
constdefs
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    88
  lin :: "'a => 'a set"
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    89
  "lin x == {y. ? a. y = a [*] x}";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    90
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    91
lemma linD: "x : lin v = (? a::real. x = a [*] v)";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    92
  by (unfold lin_def) fast;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    93
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    95
proof (unfold lin_def, intro CollectI exI);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    96
  assume "is_vectorspace V" "x:V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    97
  show "x = 1r [*] x"; by (asm_simp);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    98
qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    99
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   101
proof (rule subspace_I);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   102
  assume "is_vectorspace V" "x:V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   103
  show "<0> : lin x"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   104
  proof (unfold lin_def, intro CollectI exI);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   105
    show "<0> = 0r [*] x"; by asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   106
  qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   107
  show "lin x <= V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   108
  proof (unfold lin_def, intro subsetI, elim CollectD [elimify] exE); 
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   110
  qed;
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   112
  proof (intro ballI);
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   114
    proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   115
      fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   117
    qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   118
  qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   119
  show "ALL xa:lin x. ALL a. a [*] xa : lin x"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   120
  proof (intro ballI allI);
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   122
    proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   123
      fix a1; assume "x1 = a1 [*] x";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   124
      show "a [*] x1 = (a * a1) [*] x"; by asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   125
    qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   126
  qed; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   127
qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   128
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   129
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   131
proof (rule subspace_vs);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   132
  assume "is_vectorspace V" "x:V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   133
  show "is_subspace (lin x) V"; by (rule lin_subspace);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   134
qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   135
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   136
section {* sum of two vectorspaces *};
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   137
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   138
constdefs 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   139
  vectorspace_sum :: "['a set, 'a set] => 'a set"
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   141
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   143
  by (unfold vectorspace_sum_def) fast;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   144
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   146
  by (unfold vectorspace_sum_def, intro CollectI bexI); 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   147
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   148
lemma subspace_vs_sum1 [intro!!]: 
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   150
proof (rule subspace_I);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   151
  assume "is_vectorspace U" "is_vectorspace V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   152
  show "<0> : U"; by (rule zero_in_vs);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   153
  show "U <= vectorspace_sum U V";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   154
  proof (intro subsetI vs_sum_I);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   155
  fix x; assume "x:U";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   156
    show "x = x [+] <0>"; by asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   157
    show "<0> : V"; by asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   158
  qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   159
  show "ALL x:U. ALL y:U. x [+] y : U"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   160
  proof (intro ballI);
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   162
  qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   163
  show "ALL x:U. ALL a. a [*] x : U"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   164
  proof (intro ballI allI);
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   166
  qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   167
qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   168
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   169
lemma vs_sum_subspace: 
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   171
proof (rule subspace_I);
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   173
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   174
  show "<0> : vectorspace_sum U V";
599d3414b51d The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   177
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   178
  show "vectorspace_sum U V <= E";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   179
  proof (intro subsetI, elim vs_sumD [RS iffD1, elimify] bexE);
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   181
    show "x:E"; by (asm_simp);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   182
  qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   183
  
599d3414b51d The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   187
    show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   188
  qed asm_simp+;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   189
599d3414b51d The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   194
  qed asm_simp+;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   195
qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   196
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   197
lemma vs_sum_vs: 
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   199
  by (rule subspace_vs [OF vs_sum_subspace]);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   200
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   201
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   203
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   204
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   206
  x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   207
  ==> y1 = y2 & a1 = a2";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   208
proof;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   209
  assume "is_vectorspace E" "is_subspace H E"
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   210
         "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   211
         "y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   212
  have h: "is_vectorspace H"; by (rule subspace_vs);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   213
  have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   214
    by (rule vs_add_diff_swap) asm_simp+;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   215
  also; have "... = (a2 - a1) [*] x0";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   216
    by (rule vs_diff_mult_distrib2 [RS sym]);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   217
  finally; have eq: "y1 [-] y2 = (a2 - a1) [*] x0"; .;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   218
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   219
  have y: "y1 [-] y2 : H"; by asm_simp;
599d3414b51d The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   223
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   224
  have int: "H Int (lin x0) = {<0>}"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   225
  proof;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   226
    show "H Int lin x0 <= {<0>}"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   227
    proof (intro subsetI, unfold lin_def, elim IntE CollectD[elimify] exE,
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   228
      rule singleton_iff[RS iffD2]);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   229
      fix x a; assume "x : H" and ax0: "x = a [*] x0";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   230
      show "x = <0>";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   231
      proof (rule case [of "a=0r"]);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   232
        assume "a = 0r"; show ?thesis; by asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   233
      next;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   234
        assume "a ~= 0r"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   235
        have "(rinv a) [*] a [*] x0 : H"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   236
          by (rule vs_mult_closed [OF h]) asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   237
        also; have "(rinv a) [*] a [*] x0 = x0"; by asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   238
        finally; have "x0 : H"; .;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   239
        thus ?thesis; by contradiction;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   240
      qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   241
    qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   242
    show "{<0>} <= H Int lin x0"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   243
    proof (intro subsetI, elim singletonD[elimify], intro IntI, asm_simp+);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   244
      show "<0> : H"; by (rule zero_in_vs [OF h]);
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   246
    qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   247
  qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   248
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   249
  from h; show "y1 = y2";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   250
  proof (rule vs_add_minus_eq);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   251
    show "y1 [-] y2 = <0>";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   252
      by (rule Int_singeltonD [OF int y y']); 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   253
  qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   254
 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   255
  show "a1 = a2";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   256
  proof (rule real_add_minus_eq [RS sym]);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   257
    show "a2 - a1 = 0r";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   258
    proof (rule vs_mult_zero_uniq);
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   260
    qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   261
  qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   262
qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   263
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   264
 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   265
lemma lemma1: 
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   267
  ==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   268
proof (rule, unfold split_paired_all);
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   270
  have h: "is_vectorspace H"; by (rule subspace_vs);
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   272
  have "y = t & a = 0r"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   273
    by (rule lemma4) (assumption+, asm_simp); 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   274
  thus "(y, a) = (t, 0r)"; by asm_simp;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   275
qed asm_simp+;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   276
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   277
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   279
                            in (h y) + a * xi);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   280
                  x = y [+] a [*] x0; 
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   282
  ==> h0 x = h y + a * xi";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   283
proof -;  
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   284
  fix x0 h xi x y a H;
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   286
                            in (h y) + a * xi)";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   287
  assume "x = y [+] a [*] x0";
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   289
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   290
  have "x : vectorspace_sum H (lin x0)"; 
599d3414b51d The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   293
  proof;
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   295
      by (asm_simp, rule exI, force);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   296
  next;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   297
    fix xa ya;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   298
    assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa"
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   299
           "(%(y,a). x = y [+] a [*] x0 & y : H) ya";
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   300
    show "xa = ya"; ;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   301
    proof -;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   302
      show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   303
        by(rule Pair_fst_snd_eq [RS iffD2]);
599d3414b51d The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   307
        by (elim conjE) (rule lemma4, asm_simp+);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   308
    qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   309
  qed;
599d3414b51d The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   311
    by (rule select1_equality, force);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   312
  thus "h0 x = h y + a * xi"; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   313
    by (asm_simp add: Let_def);
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   314
qed;  
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   315
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   316
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   317
end;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   318
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
   319