src/HOL/Real/HahnBanach/Subspace.thy
author wenzelm
Tue Sep 21 17:31:20 1999 +0200 (1999-09-21)
changeset 7566 c5a3f980a7af
parent 7535 599d3414b51d
child 7567 62384a807775
permissions -rw-r--r--
accomodate refined facts handling;
wenzelm@7566
     1
(*  Title:      HOL/Real/HahnBanach/Subspace.thy
wenzelm@7566
     2
    ID:         $Id$
wenzelm@7566
     3
    Author:     Gertrud Bauer, TU Munich
wenzelm@7566
     4
*)
wenzelm@7535
     5
wenzelm@7535
     6
theory Subspace = LinearSpace:;
wenzelm@7535
     7
wenzelm@7535
     8
wenzelm@7535
     9
section {* subspaces *};
wenzelm@7535
    10
wenzelm@7535
    11
constdefs
wenzelm@7535
    12
  is_subspace ::  "['a set, 'a set] => bool"
wenzelm@7535
    13
  "is_subspace U V ==  <0>:U  & U <= V 
wenzelm@7535
    14
     &  (ALL x:U. ALL y:U. ALL a. x [+] y : U                          
wenzelm@7535
    15
                       & a [*] x : U)";                            
wenzelm@7535
    16
wenzelm@7566
    17
lemma subspaceI [intro]: 
wenzelm@7535
    18
  "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); ALL x:U. ALL a. a [*] x : U |]
wenzelm@7535
    19
  \ ==> is_subspace U V";
wenzelm@7566
    20
  by (unfold is_subspace_def) (simp!);
wenzelm@7535
    21
wenzelm@7535
    22
lemma "is_subspace U V ==> U ~= {}";
wenzelm@7535
    23
  by (unfold is_subspace_def) force;
wenzelm@7535
    24
wenzelm@7566
    25
lemma zero_in_subspace [intro !!]: "is_subspace U V ==> <0>:U";
wenzelm@7566
    26
  by (unfold is_subspace_def) (simp!);;
wenzelm@7566
    27
wenzelm@7566
    28
lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
wenzelm@7566
    29
  by (unfold is_subspace_def) (simp!);
wenzelm@7566
    30
wenzelm@7566
    31
lemma subspace_subsetD [simp, intro!!]: "[| is_subspace U V; x:U |]==> x:V";
wenzelm@7535
    32
  by (unfold is_subspace_def) force;
wenzelm@7535
    33
wenzelm@7566
    34
lemma subspace_add_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
wenzelm@7566
    35
  by (unfold is_subspace_def) (simp!);
wenzelm@7535
    36
wenzelm@7566
    37
lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
wenzelm@7566
    38
  by (unfold is_subspace_def) (simp!);
wenzelm@7535
    39
wenzelm@7566
    40
lemma subspace_diff_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
wenzelm@7566
    41
  by (unfold diff_def negate_def) (simp!);
wenzelm@7535
    42
wenzelm@7566
    43
lemma subspace_neg_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> [-] x: U";
wenzelm@7566
    44
 by (unfold negate_def) (simp!);
wenzelm@7535
    45
wenzelm@7535
    46
wenzelm@7535
    47
theorem subspace_vs [intro!!]:
wenzelm@7535
    48
  "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
wenzelm@7535
    49
proof -;
wenzelm@7566
    50
  assume "is_subspace U V";
wenzelm@7535
    51
  assume "is_vectorspace V";
wenzelm@7535
    52
  assume "is_subspace U V";
wenzelm@7535
    53
  show ?thesis;
wenzelm@7566
    54
  proof; 
wenzelm@7566
    55
    show "<0>:U"; ..;
wenzelm@7566
    56
    show "ALL x:U. ALL a. a [*] x : U"; by (simp!);
wenzelm@7566
    57
    show "ALL x:U. ALL y:U. x [+] y : U"; by (simp!);
wenzelm@7566
    58
  qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
wenzelm@7535
    59
qed;
wenzelm@7535
    60
wenzelm@7566
    61
lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V";
wenzelm@7566
    62
proof; 
wenzelm@7535
    63
  assume "is_vectorspace V";
wenzelm@7566
    64
  show "<0> : V"; ..;
wenzelm@7566
    65
  show "V <= V"; ..;
wenzelm@7566
    66
  show "ALL x:V. ALL y:V. x [+] y : V"; by (simp!);
wenzelm@7566
    67
  show "ALL x:V. ALL a. a [*] x : V"; by (simp!);
wenzelm@7535
    68
qed;
wenzelm@7535
    69
wenzelm@7535
    70
lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
wenzelm@7566
    71
proof; 
wenzelm@7535
    72
  assume "is_subspace U V" "is_subspace V W";
wenzelm@7566
    73
  show "<0> : U"; ..;
wenzelm@7566
    74
  have "U <= V"; ..;
wenzelm@7566
    75
  also; have "V <= W"; ..;
wenzelm@7566
    76
  finally; show "U <= W"; .;
wenzelm@7535
    77
  show "ALL x:U. ALL y:U. x [+] y : U"; 
wenzelm@7535
    78
  proof (intro ballI);
wenzelm@7535
    79
    fix x y; assume "x:U" "y:U";
wenzelm@7566
    80
    show "x [+] y : U"; by (simp!);
wenzelm@7535
    81
  qed;
wenzelm@7535
    82
  show "ALL x:U. ALL a. a [*] x : U";
wenzelm@7535
    83
  proof (intro ballI allI);
wenzelm@7535
    84
    fix x a; assume "x:U";
wenzelm@7566
    85
    show "a [*] x : U"; by (simp!);
wenzelm@7535
    86
  qed;
wenzelm@7535
    87
qed;
wenzelm@7535
    88
wenzelm@7535
    89
wenzelm@7535
    90
section {* linear closure *};
wenzelm@7535
    91
wenzelm@7535
    92
constdefs
wenzelm@7535
    93
  lin :: "'a => 'a set"
wenzelm@7535
    94
  "lin x == {y. ? a. y = a [*] x}";
wenzelm@7535
    95
wenzelm@7535
    96
lemma linD: "x : lin v = (? a::real. x = a [*] v)";
wenzelm@7566
    97
  by (unfold lin_def) force;
wenzelm@7535
    98
wenzelm@7535
    99
lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
wenzelm@7535
   100
proof (unfold lin_def, intro CollectI exI);
wenzelm@7535
   101
  assume "is_vectorspace V" "x:V";
wenzelm@7566
   102
  show "x = 1r [*] x"; by (simp!);
wenzelm@7535
   103
qed;
wenzelm@7535
   104
wenzelm@7566
   105
lemma lin_subspace [intro!!]: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
wenzelm@7566
   106
proof;
wenzelm@7535
   107
  assume "is_vectorspace V" "x:V";
wenzelm@7535
   108
  show "<0> : lin x"; 
wenzelm@7535
   109
  proof (unfold lin_def, intro CollectI exI);
wenzelm@7566
   110
    show "<0> = 0r [*] x"; by (simp!);
wenzelm@7535
   111
  qed;
wenzelm@7566
   112
wenzelm@7535
   113
  show "lin x <= V";
wenzelm@7566
   114
  proof (unfold lin_def, intro subsetI, elim CollectE exE); 
wenzelm@7566
   115
    fix xa a; assume "xa = a [*] x"; 
wenzelm@7566
   116
    show "xa:V"; by (simp!);
wenzelm@7535
   117
  qed;
wenzelm@7566
   118
wenzelm@7535
   119
  show "ALL x1 : lin x. ALL x2 : lin x. x1 [+] x2 : lin x"; 
wenzelm@7535
   120
  proof (intro ballI);
wenzelm@7566
   121
    fix x1 x2; assume "x1 : lin x" "x2 : lin x"; 
wenzelm@7566
   122
    thus "x1 [+] x2 : lin x";
wenzelm@7566
   123
    proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);   (* FIXME !? *)
wenzelm@7535
   124
      fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
wenzelm@7566
   125
      show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2);
wenzelm@7535
   126
    qed;
wenzelm@7535
   127
  qed;
wenzelm@7566
   128
wenzelm@7535
   129
  show "ALL xa:lin x. ALL a. a [*] xa : lin x"; 
wenzelm@7535
   130
  proof (intro ballI allI);
wenzelm@7566
   131
    fix x1 a; assume "x1 : lin x"; 
wenzelm@7566
   132
    thus "a [*] x1 : lin x";
wenzelm@7566
   133
    proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);
wenzelm@7535
   134
      fix a1; assume "x1 = a1 [*] x";
wenzelm@7566
   135
      show "a [*] x1 = (a * a1) [*] x"; by (simp!);
wenzelm@7535
   136
    qed;
wenzelm@7535
   137
  qed; 
wenzelm@7535
   138
qed;
wenzelm@7535
   139
wenzelm@7535
   140
wenzelm@7535
   141
lemma lin_vs [intro!!]: "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
wenzelm@7535
   142
proof (rule subspace_vs);
wenzelm@7535
   143
  assume "is_vectorspace V" "x:V";
wenzelm@7566
   144
  show "is_subspace (lin x) V"; ..;
wenzelm@7535
   145
qed;
wenzelm@7535
   146
wenzelm@7535
   147
section {* sum of two vectorspaces *};
wenzelm@7535
   148
wenzelm@7535
   149
constdefs 
wenzelm@7535
   150
  vectorspace_sum :: "['a set, 'a set] => 'a set"
wenzelm@7535
   151
  "vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}";
wenzelm@7535
   152
wenzelm@7535
   153
lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)";
wenzelm@7566
   154
  by (unfold vectorspace_sum_def) (simp!);
wenzelm@7535
   155
wenzelm@7566
   156
lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
wenzelm@7566
   157
wenzelm@7566
   158
lemma vs_sumI [intro!!]: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V";
wenzelm@7535
   159
  by (unfold vectorspace_sum_def, intro CollectI bexI); 
wenzelm@7535
   160
wenzelm@7535
   161
lemma subspace_vs_sum1 [intro!!]: 
wenzelm@7535
   162
  "[| is_vectorspace U; is_vectorspace V |] ==> is_subspace U (vectorspace_sum U V)";
wenzelm@7566
   163
proof; 
wenzelm@7535
   164
  assume "is_vectorspace U" "is_vectorspace V";
wenzelm@7566
   165
  show "<0> : U"; ..;
wenzelm@7535
   166
  show "U <= vectorspace_sum U V";
wenzelm@7566
   167
  proof (intro subsetI vs_sumI);
wenzelm@7535
   168
  fix x; assume "x:U";
wenzelm@7566
   169
    show "x = x [+] <0>"; by (simp!);
wenzelm@7566
   170
    show "<0> : V"; by (simp!);
wenzelm@7535
   171
  qed;
wenzelm@7535
   172
  show "ALL x:U. ALL y:U. x [+] y : U"; 
wenzelm@7535
   173
  proof (intro ballI);
wenzelm@7566
   174
    fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by (simp!);
wenzelm@7535
   175
  qed;
wenzelm@7535
   176
  show "ALL x:U. ALL a. a [*] x : U"; 
wenzelm@7535
   177
  proof (intro ballI allI);
wenzelm@7566
   178
    fix x a; assume "x:U"; show "a [*] x : U"; by (simp!);
wenzelm@7535
   179
  qed;
wenzelm@7535
   180
qed;
wenzelm@7535
   181
wenzelm@7566
   182
lemma vs_sum_subspace [intro!!]: 
wenzelm@7566
   183
  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
wenzelm@7566
   184
  ==> is_subspace (vectorspace_sum U V) E";
wenzelm@7566
   185
proof; 
wenzelm@7566
   186
  assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E";
wenzelm@7535
   187
wenzelm@7535
   188
  show "<0> : vectorspace_sum U V";
wenzelm@7566
   189
  proof (intro vs_sumI);
wenzelm@7566
   190
    show "<0> : U"; ..;
wenzelm@7566
   191
    show "<0> : V"; ..;
wenzelm@7566
   192
    show "(<0>::'a) = <0> [+] <0>"; 
wenzelm@7566
   193
      by (simp!);
wenzelm@7566
   194
  qed;
wenzelm@7566
   195
  
wenzelm@7535
   196
  show "vectorspace_sum U V <= E";
wenzelm@7566
   197
  proof (intro subsetI, elim vs_sumE bexE);
wenzelm@7535
   198
    fix x u v; assume "u : U" "v : V" "x = u [+] v";
wenzelm@7566
   199
    show "x:E"; by (simp!);
wenzelm@7535
   200
  qed;
wenzelm@7535
   201
  
wenzelm@7535
   202
  show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V";
wenzelm@7566
   203
  proof (intro ballI);
wenzelm@7566
   204
    fix x y; assume "x:vectorspace_sum U V" "y:vectorspace_sum U V";
wenzelm@7566
   205
    thus "x [+] y : vectorspace_sum U V";
wenzelm@7566
   206
    proof (elim vs_sumE bexE, intro vs_sumI);
wenzelm@7566
   207
      fix ux vx uy vy; 
wenzelm@7566
   208
      assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy";
wenzelm@7566
   209
      show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by (simp!);
wenzelm@7566
   210
    qed (simp!)+;
wenzelm@7566
   211
  qed;
wenzelm@7535
   212
wenzelm@7535
   213
  show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V";
wenzelm@7566
   214
  proof (intro ballI allI);
wenzelm@7566
   215
    fix x a; assume "x:vectorspace_sum U V";
wenzelm@7566
   216
    thus "a [*] x : vectorspace_sum U V";
wenzelm@7566
   217
    proof (elim vs_sumE bexE, intro vs_sumI);
wenzelm@7566
   218
      fix a x u v; assume "u : U" "v : V" "x = u [+] v";
wenzelm@7566
   219
      show "a [*] x = (a [*] u) [+] (a [*] v)"; by (simp! add: vs_add_mult_distrib1);
wenzelm@7566
   220
    qed (simp!)+;
wenzelm@7566
   221
  qed;
wenzelm@7535
   222
qed;
wenzelm@7535
   223
wenzelm@7566
   224
lemma vs_sum_vs [intro!!]: 
wenzelm@7566
   225
  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
wenzelm@7566
   226
  ==> is_vectorspace (vectorspace_sum U V)";
wenzelm@7566
   227
proof (rule subspace_vs);
wenzelm@7566
   228
  assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
wenzelm@7566
   229
  show "is_subspace (vectorspace_sum U V) E"; ..;
wenzelm@7566
   230
qed;
wenzelm@7535
   231
wenzelm@7535
   232
wenzelm@7535
   233
section {* special case: direct sum of a vectorspace and a linear closure of a vector *};
wenzelm@7535
   234
wenzelm@7566
   235
lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; 
wenzelm@7535
   236
  x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
wenzelm@7535
   237
  ==> y1 = y2 & a1 = a2";
wenzelm@7535
   238
proof;
wenzelm@7535
   239
  assume "is_vectorspace E" "is_subspace H E"
wenzelm@7535
   240
         "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
wenzelm@7535
   241
         "y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0";
wenzelm@7566
   242
  have h: "is_vectorspace H"; ..;
wenzelm@7566
   243
  have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0";
wenzelm@7566
   244
    by (simp! add: vs_add_diff_swap);
wenzelm@7535
   245
  also; have "... = (a2 - a1) [*] x0";
wenzelm@7535
   246
    by (rule vs_diff_mult_distrib2 [RS sym]);
wenzelm@7535
   247
  finally; have eq: "y1 [-] y2 = (a2 - a1) [*] x0"; .;
wenzelm@7535
   248
wenzelm@7566
   249
  have y: "y1 [-] y2 : H"; by (simp!);
wenzelm@7566
   250
  have x: "(a2 - a1) [*] x0 : lin x0"; by (simp! add: lin_def) force; 
wenzelm@7566
   251
  from eq y x; have y': "y1 [-] y2 : lin x0"; by simp;
wenzelm@7566
   252
  from eq y x; have x': "(a2 - a1) [*] x0 : H"; by simp;
wenzelm@7535
   253
wenzelm@7535
   254
  have int: "H Int (lin x0) = {<0>}"; 
wenzelm@7535
   255
  proof;
wenzelm@7535
   256
    show "H Int lin x0 <= {<0>}"; 
wenzelm@7566
   257
    proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
wenzelm@7566
   258
      fix x; assume "x:H" "x:lin x0"; 
wenzelm@7566
   259
      thus "x = <0>";
wenzelm@7566
   260
      proof (-, unfold lin_def, elim CollectE exE);
wenzelm@7566
   261
        fix a; assume "x = a [*] x0";
wenzelm@7566
   262
        show ?thesis;
wenzelm@7566
   263
        proof (rule case [of "a = 0r"]);
wenzelm@7566
   264
          assume "a = 0r"; show ?thesis; by (simp!);
wenzelm@7566
   265
        next;
wenzelm@7566
   266
          assume "a ~= 0r"; 
wenzelm@7566
   267
          have "(rinv a) [*] a [*] x0 : H"; 
wenzelm@7566
   268
            by (rule vs_mult_closed [OF h]) (simp!);
wenzelm@7566
   269
          also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
wenzelm@7566
   270
          finally; have "x0 : H"; .;
wenzelm@7566
   271
          thus ?thesis; by contradiction;
wenzelm@7566
   272
        qed;
wenzelm@7566
   273
     qed;
wenzelm@7535
   274
    qed;
wenzelm@7566
   275
    show "{<0>} <= H Int lin x0";
wenzelm@7566
   276
    proof (intro subsetI, elim singletonE, intro IntI, simp+);
wenzelm@7566
   277
      show "<0> : H"; ..;
wenzelm@7566
   278
      from lin_vs; show "<0> : lin x0"; ..;
wenzelm@7535
   279
    qed;
wenzelm@7535
   280
  qed;
wenzelm@7535
   281
wenzelm@7535
   282
  from h; show "y1 = y2";
wenzelm@7535
   283
  proof (rule vs_add_minus_eq);
wenzelm@7566
   284
    show "y1 [-] y2 = <0>"; 
wenzelm@7566
   285
      by (rule Int_singletonD [OF int y y']); 
wenzelm@7535
   286
  qed;
wenzelm@7535
   287
 
wenzelm@7535
   288
  show "a1 = a2";
wenzelm@7535
   289
  proof (rule real_add_minus_eq [RS sym]);
wenzelm@7535
   290
    show "a2 - a1 = 0r";
wenzelm@7535
   291
    proof (rule vs_mult_zero_uniq);
wenzelm@7566
   292
      show "(a2 - a1) [*] x0 = <0>";  by (rule Int_singletonD [OF int x' x]);
wenzelm@7535
   293
    qed;
wenzelm@7535
   294
  qed;
wenzelm@7535
   295
qed;
wenzelm@7535
   296
wenzelm@7535
   297
 
wenzelm@7566
   298
lemma decomp1: 
wenzelm@7535
   299
  "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |] 
wenzelm@7535
   300
  ==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
wenzelm@7535
   301
proof (rule, unfold split_paired_all);
wenzelm@7535
   302
  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>";
wenzelm@7566
   303
  have h: "is_vectorspace H"; ..;
wenzelm@7535
   304
  fix y a; presume t1: "t = y [+] a [*] x0" and "y : H";
wenzelm@7535
   305
  have "y = t & a = 0r"; 
wenzelm@7566
   306
    by (rule decomp4) (assumption+, (simp!)); 
wenzelm@7566
   307
  thus "(y, a) = (t, 0r)"; by (simp!);
wenzelm@7566
   308
qed (simp!)+;
wenzelm@7535
   309
wenzelm@7535
   310
wenzelm@7566
   311
lemma decomp3:
wenzelm@7566
   312
  "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
wenzelm@7566
   313
                in (h y) + a * xi);
wenzelm@7566
   314
      x = y [+] a [*] x0; 
wenzelm@7566
   315
      is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |]
wenzelm@7535
   316
  ==> h0 x = h y + a * xi";
wenzelm@7535
   317
proof -;  
wenzelm@7535
   318
  assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
wenzelm@7566
   319
                    in (h y) + a * xi)";
wenzelm@7535
   320
  assume "x = y [+] a [*] x0";
wenzelm@7535
   321
  assume "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
wenzelm@7535
   322
wenzelm@7535
   323
  have "x : vectorspace_sum H (lin x0)"; 
wenzelm@7566
   324
    by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+;
wenzelm@7535
   325
  have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
wenzelm@7535
   326
  proof;
wenzelm@7566
   327
    show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
wenzelm@7566
   328
      by (force!);
wenzelm@7535
   329
  next;
wenzelm@7535
   330
    fix xa ya;
wenzelm@7535
   331
    assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa"
wenzelm@7535
   332
           "(%(y,a). x = y [+] a [*] x0 & y : H) ya";
wenzelm@7535
   333
    show "xa = ya"; ;
wenzelm@7535
   334
    proof -;
wenzelm@7535
   335
      show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
wenzelm@7566
   336
        by (rule Pair_fst_snd_eq [RS iffD2]);
wenzelm@7566
   337
      have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by (force!);
wenzelm@7566
   338
      have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by (force!);
wenzelm@7535
   339
      from x y; show "fst xa = fst ya & snd xa = snd ya"; 
wenzelm@7566
   340
        by (elim conjE) (rule decomp4, (simp!)+);
wenzelm@7535
   341
    qed;
wenzelm@7535
   342
  qed;
wenzelm@7535
   343
  hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; 
wenzelm@7566
   344
    by (rule select1_equality) (force!);
wenzelm@7535
   345
  thus "h0 x = h y + a * xi"; 
wenzelm@7566
   346
    by (simp! add: Let_def);
wenzelm@7566
   347
qed;
wenzelm@7535
   348
wenzelm@7535
   349
wenzelm@7535
   350
end;
wenzelm@7535
   351
wenzelm@7535
   352