src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45605 a89b4bc311a5
child 52183 667961fa6a60
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
     1
(*  Title:      HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     2
    Author:     Gertrud Bauer, TU Munich
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     3
*)
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     4
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
     5
header {* The supremum w.r.t.~the function order *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     6
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
     7
theory Hahn_Banach_Sup_Lemmas
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
     8
imports Function_Norm Zorn_Lemma
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
     9
begin
9256
f9a6670427fb completed TYPES version of HahnBanach;
bauerg
parents: 9035
diff changeset
    10
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    11
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    12
  This section contains some lemmas that will be used in the proof of
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    13
  the Hahn-Banach Theorem.  In this section the following context is
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    14
  presumed.  Let @{text E} be a real vector space with a seminorm
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    15
  @{text p} on @{text E}.  @{text F} is a subspace of @{text E} and
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    16
  @{text f} a linear form on @{text F}. We consider a chain @{text c}
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    17
  of norm-preserving extensions of @{text f}, such that @{text "\<Union>c =
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    18
  graph H h"}.  We will show some properties about the limit function
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    19
  @{text h}, i.e.\ the supremum of the chain @{text c}.
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    20
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    21
  \medskip Let @{text c} be a chain of norm-preserving extensions of
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    22
  the function @{text f} and let @{text "graph H h"} be the supremum
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    23
  of @{text c}.  Every element in @{text H} is member of one of the
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    24
  elements of the chain.
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    25
*}
14710
247615bfffb8 replaced Aux.thy by RealLemmas.thy
bauerg
parents: 13547
diff changeset
    26
lemmas [dest?] = chainD
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 44887
diff changeset
    27
lemmas chainE2 [elim?] = chainD2 [elim_format]
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    28
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    29
lemma some_H'h't:
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    30
  assumes M: "M = norm_pres_extensions E p F f"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    31
    and cM: "c \<in> chain M"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    32
    and u: "graph H h = \<Union>c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    33
    and x: "x \<in> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    34
  shows "\<exists>H' h'. graph H' h' \<in> c
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    35
    \<and> (x, h x) \<in> graph H' h'
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    36
    \<and> linearform H' h' \<and> H' \<unlhd> E
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    37
    \<and> F \<unlhd> H' \<and> graph F f \<subseteq> graph H' h'
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    38
    \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
    39
proof -
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    40
  from x have "(x, h x) \<in> graph H h" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    41
  also from u have "\<dots> = \<Union>c" .
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    42
  finally obtain g where gc: "g \<in> c" and gh: "(x, h x) \<in> g" by blast
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    43
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    44
  from cM have "c \<subseteq> M" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    45
  with gc have "g \<in> M" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    46
  also from M have "\<dots> = norm_pres_extensions E p F f" .
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    47
  finally obtain H' and h' where g: "g = graph H' h'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    48
    and * : "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    49
      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    50
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    51
  from gc and g have "graph H' h' \<in> c" by (simp only:)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    52
  moreover from gh and g have "(x, h x) \<in> graph H' h'" by (simp only:)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    53
  ultimately show ?thesis using * by blast
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
    54
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    55
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    56
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    57
  \medskip Let @{text c} be a chain of norm-preserving extensions of
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    58
  the function @{text f} and let @{text "graph H h"} be the supremum
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    59
  of @{text c}.  Every element in the domain @{text H} of the supremum
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    60
  function is member of the domain @{text H'} of some function @{text
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    61
  h'}, such that @{text h} extends @{text h'}.
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
    62
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    63
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    64
lemma some_H'h':
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    65
  assumes M: "M = norm_pres_extensions E p F f"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    66
    and cM: "c \<in> chain M"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    67
    and u: "graph H h = \<Union>c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    68
    and x: "x \<in> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    69
  shows "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    70
    \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    71
    \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
    72
proof -
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    73
  from M cM u x obtain H' h' where
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    74
      x_hx: "(x, h x) \<in> graph H' h'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    75
    and c: "graph H' h' \<in> c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    76
    and * : "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    77
      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    78
    by (rule some_H'h't [elim_format]) blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    79
  from x_hx have "x \<in> H'" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    80
  moreover from cM u c have "graph H' h' \<subseteq> graph H h"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    81
    by (simp only: chain_ball_Union_upper)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    82
  ultimately show ?thesis using * by blast
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
    83
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    84
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    85
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    86
  \medskip Any two elements @{text x} and @{text y} in the domain
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    87
  @{text H} of the supremum function @{text h} are both in the domain
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    88
  @{text H'} of some function @{text h'}, such that @{text h} extends
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    89
  @{text h'}.
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    90
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    91
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
    92
lemma some_H'h'2:
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    93
  assumes M: "M = norm_pres_extensions E p F f"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    94
    and cM: "c \<in> chain M"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    95
    and u: "graph H h = \<Union>c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    96
    and x: "x \<in> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    97
    and y: "y \<in> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    98
  shows "\<exists>H' h'. x \<in> H' \<and> y \<in> H'
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    99
    \<and> graph H' h' \<subseteq> graph H h
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   100
    \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   101
    \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   102
proof -
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   103
  txt {* @{text y} is in the domain @{text H''} of some function @{text h''},
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   104
  such that @{text h} extends @{text h''}. *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   105
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   106
  from M cM u and y obtain H' h' where
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   107
      y_hy: "(y, h y) \<in> graph H' h'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   108
    and c': "graph H' h' \<in> c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   109
    and * :
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   110
      "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   111
      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   112
    by (rule some_H'h't [elim_format]) blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   113
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   114
  txt {* @{text x} is in the domain @{text H'} of some function @{text h'},
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   115
    such that @{text h} extends @{text h'}. *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   116
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   117
  from M cM u and x obtain H'' h'' where
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   118
      x_hx: "(x, h x) \<in> graph H'' h''"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   119
    and c'': "graph H'' h'' \<in> c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   120
    and ** :
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   121
      "linearform H'' h''"  "H'' \<unlhd> E"  "F \<unlhd> H''"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   122
      "graph F f \<subseteq> graph H'' h''"  "\<forall>x \<in> H''. h'' x \<le> p x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   123
    by (rule some_H'h't [elim_format]) blast
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   124
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   125
  txt {* Since both @{text h'} and @{text h''} are elements of the chain,
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   126
    @{text h''} is an extension of @{text h'} or vice versa. Thus both
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   127
    @{text x} and @{text y} are contained in the greater
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   128
    one. \label{cases1}*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   129
23378
1d138d6bb461 tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
   130
  from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   131
    (is "?case1 \<or> ?case2") ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   132
  then show ?thesis
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   133
  proof
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   134
    assume ?case1
23378
1d138d6bb461 tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
   135
    have "(x, h x) \<in> graph H'' h''" by fact
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   136
    also have "\<dots> \<subseteq> graph H' h'" by fact
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   137
    finally have xh:"(x, h x) \<in> graph H' h'" .
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   138
    then have "x \<in> H'" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   139
    moreover from y_hy have "y \<in> H'" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   140
    moreover from cM u and c' have "graph H' h' \<subseteq> graph H h"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   141
      by (simp only: chain_ball_Union_upper)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   142
    ultimately show ?thesis using * by blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   143
  next
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   144
    assume ?case2
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   145
    from x_hx have "x \<in> H''" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   146
    moreover {
23378
1d138d6bb461 tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
   147
      have "(y, h y) \<in> graph H' h'" by (rule y_hy)
1d138d6bb461 tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
   148
      also have "\<dots> \<subseteq> graph H'' h''" by fact
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   149
      finally have "(y, h y) \<in> graph H'' h''" .
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   150
    } then have "y \<in> H''" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   151
    moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   152
      by (simp only: chain_ball_Union_upper)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   153
    ultimately show ?thesis using ** by blast
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   154
  qed
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   155
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   156
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   157
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   158
  \medskip The relation induced by the graph of the supremum of a
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   159
  chain @{text c} is definite, i.~e.~t is the graph of a function.
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   160
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   161
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   162
lemma sup_definite:
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   163
  assumes M_def: "M \<equiv> norm_pres_extensions E p F f"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   164
    and cM: "c \<in> chain M"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   165
    and xy: "(x, y) \<in> \<Union>c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   166
    and xz: "(x, z) \<in> \<Union>c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   167
  shows "z = y"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   168
proof -
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   169
  from cM have c: "c \<subseteq> M" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   170
  from xy obtain G1 where xy': "(x, y) \<in> G1" and G1: "G1 \<in> c" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   171
  from xz obtain G2 where xz': "(x, z) \<in> G2" and G2: "G2 \<in> c" ..
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   172
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   173
  from G1 c have "G1 \<in> M" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   174
  then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   175
    unfolding M_def by blast
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   176
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   177
  from G2 c have "G2 \<in> M" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   178
  then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   179
    unfolding M_def by blast
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   180
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   181
  txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   182
    or vice versa, since both @{text "G\<^sub>1"} and @{text
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   183
    "G\<^sub>2"} are members of @{text c}. \label{cases2}*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   184
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   185
  from cM G1 G2 have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   186
  then show ?thesis
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   187
  proof
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   188
    assume ?case1
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   189
    with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   190
    then have "y = h2 x" ..
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   191
    also
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   192
    from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:)
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   193
    then have "z = h2 x" ..
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   194
    finally show ?thesis .
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   195
  next
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   196
    assume ?case2
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   197
    with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   198
    then have "z = h1 x" ..
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   199
    also
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   200
    from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:)
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
   201
    then have "y = h1 x" ..
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   202
    finally show ?thesis ..
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   203
  qed
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   204
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   205
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   206
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   207
  \medskip The limit function @{text h} is linear. Every element
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   208
  @{text x} in the domain of @{text h} is in the domain of a function
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   209
  @{text h'} in the chain of norm preserving extensions.  Furthermore,
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   210
  @{text h} is an extension of @{text h'} so the function values of
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   211
  @{text x} are identical for @{text h'} and @{text h}.  Finally, the
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   212
  function @{text h'} is linear by construction of @{text M}.
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   213
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   214
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   215
lemma sup_lf:
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   216
  assumes M: "M = norm_pres_extensions E p F f"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   217
    and cM: "c \<in> chain M"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   218
    and u: "graph H h = \<Union>c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   219
  shows "linearform H h"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   220
proof
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   221
  fix x y assume x: "x \<in> H" and y: "y \<in> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   222
  with M cM u obtain H' h' where
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   223
        x': "x \<in> H'" and y': "y \<in> H'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   224
      and b: "graph H' h' \<subseteq> graph H h"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   225
      and linearform: "linearform H' h'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   226
      and subspace: "H' \<unlhd> E"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   227
    by (rule some_H'h'2 [elim_format]) blast
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   228
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   229
  show "h (x + y) = h x + h y"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   230
  proof -
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   231
    from linearform x' y' have "h' (x + y) = h' x + h' y"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   232
      by (rule linearform.add)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   233
    also from b x' have "h' x = h x" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   234
    also from b y' have "h' y = h y" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   235
    also from subspace x' y' have "x + y \<in> H'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   236
      by (rule subspace.add_closed)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   237
    with b have "h' (x + y) = h (x + y)" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   238
    finally show ?thesis .
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   239
  qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   240
next
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   241
  fix x a assume x: "x \<in> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   242
  with M cM u obtain H' h' where
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   243
        x': "x \<in> H'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   244
      and b: "graph H' h' \<subseteq> graph H h"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   245
      and linearform: "linearform H' h'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   246
      and subspace: "H' \<unlhd> E"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   247
    by (rule some_H'h' [elim_format]) blast
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   248
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   249
  show "h (a \<cdot> x) = a * h x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   250
  proof -
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   251
    from linearform x' have "h' (a \<cdot> x) = a * h' x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   252
      by (rule linearform.mult)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   253
    also from b x' have "h' x = h x" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   254
    also from subspace x' have "a \<cdot> x \<in> H'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   255
      by (rule subspace.mult_closed)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   256
    with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   257
    finally show ?thesis .
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   258
  qed
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   259
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   260
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   261
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   262
  \medskip The limit of a non-empty chain of norm preserving
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   263
  extensions of @{text f} is an extension of @{text f}, since every
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   264
  element of the chain is an extension of @{text f} and the supremum
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   265
  is an extension for every element of the chain.
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   266
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   267
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   268
lemma sup_ext:
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   269
  assumes graph: "graph H h = \<Union>c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   270
    and M: "M = norm_pres_extensions E p F f"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   271
    and cM: "c \<in> chain M"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   272
    and ex: "\<exists>x. x \<in> c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   273
  shows "graph F f \<subseteq> graph H h"
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   274
proof -
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   275
  from ex obtain x where xc: "x \<in> c" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   276
  from cM have "c \<subseteq> M" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   277
  with xc have "x \<in> M" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   278
  with M have "x \<in> norm_pres_extensions E p F f"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   279
    by (simp only:)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   280
  then obtain G g where "x = graph G g" and "graph F f \<subseteq> graph G g" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   281
  then have "graph F f \<subseteq> x" by (simp only:)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   282
  also from xc have "\<dots> \<subseteq> \<Union>c" by blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   283
  also from graph have "\<dots> = graph H h" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   284
  finally show ?thesis .
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   285
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   286
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   287
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   288
  \medskip The domain @{text H} of the limit function is a superspace
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   289
  of @{text F}, since @{text F} is a subset of @{text H}. The
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   290
  existence of the @{text 0} element in @{text F} and the closure
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   291
  properties follow from the fact that @{text F} is a vector space.
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   292
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   293
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   294
lemma sup_supF:
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   295
  assumes graph: "graph H h = \<Union>c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   296
    and M: "M = norm_pres_extensions E p F f"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   297
    and cM: "c \<in> chain M"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   298
    and ex: "\<exists>x. x \<in> c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   299
    and FE: "F \<unlhd> E"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   300
  shows "F \<unlhd> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   301
proof
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   302
  from FE show "F \<noteq> {}" by (rule subspace.non_empty)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   303
  from graph M cM ex have "graph F f \<subseteq> graph H h" by (rule sup_ext)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   304
  then show "F \<subseteq> H" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   305
  fix x y assume "x \<in> F" and "y \<in> F"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   306
  with FE show "x + y \<in> F" by (rule subspace.add_closed)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   307
next
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   308
  fix x a assume "x \<in> F"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   309
  with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed)
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   310
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   311
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   312
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   313
  \medskip The domain @{text H} of the limit function is a subspace of
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   314
  @{text E}.
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   315
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   316
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   317
lemma sup_subE:
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   318
  assumes graph: "graph H h = \<Union>c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   319
    and M: "M = norm_pres_extensions E p F f"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   320
    and cM: "c \<in> chain M"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   321
    and ex: "\<exists>x. x \<in> c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   322
    and FE: "F \<unlhd> E"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   323
    and E: "vectorspace E"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   324
  shows "H \<unlhd> E"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   325
proof
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   326
  show "H \<noteq> {}"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   327
  proof -
13547
wenzelm
parents: 13515
diff changeset
   328
    from FE E have "0 \<in> F" by (rule subspace.zero)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   329
    also from graph M cM ex FE have "F \<unlhd> H" by (rule sup_supF)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   330
    then have "F \<subseteq> H" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   331
    finally show ?thesis by blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   332
  qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   333
  show "H \<subseteq> E"
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   334
  proof
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   335
    fix x assume "x \<in> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   336
    with M cM graph
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 32960
diff changeset
   337
    obtain H' where x: "x \<in> H'" and H'E: "H' \<unlhd> E"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   338
      by (rule some_H'h' [elim_format]) blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   339
    from H'E have "H' \<subseteq> E" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   340
    with x show "x \<in> E" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   341
  qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   342
  fix x y assume x: "x \<in> H" and y: "y \<in> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   343
  show "x + y \<in> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   344
  proof -
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   345
    from M cM graph x y obtain H' h' where
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   346
          x': "x \<in> H'" and y': "y \<in> H'" and H'E: "H' \<unlhd> E"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   347
        and graphs: "graph H' h' \<subseteq> graph H h"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   348
      by (rule some_H'h'2 [elim_format]) blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   349
    from H'E x' y' have "x + y \<in> H'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   350
      by (rule subspace.add_closed)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   351
    also from graphs have "H' \<subseteq> H" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   352
    finally show ?thesis .
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   353
  qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   354
next
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   355
  fix x a assume x: "x \<in> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   356
  show "a \<cdot> x \<in> H"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   357
  proof -
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   358
    from M cM graph x
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   359
    obtain H' h' where x': "x \<in> H'" and H'E: "H' \<unlhd> E"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   360
        and graphs: "graph H' h' \<subseteq> graph H h"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   361
      by (rule some_H'h' [elim_format]) blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   362
    from H'E x' have "a \<cdot> x \<in> H'" by (rule subspace.mult_closed)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   363
    also from graphs have "H' \<subseteq> H" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   364
    finally show ?thesis .
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   365
  qed
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   366
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   367
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   368
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   369
  \medskip The limit function is bounded by the norm @{text p} as
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   370
  well, since all elements in the chain are bounded by @{text p}.
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   371
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   372
9374
153853af318b - xsymbols for
bauerg
parents: 9262
diff changeset
   373
lemma sup_norm_pres:
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   374
  assumes graph: "graph H h = \<Union>c"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   375
    and M: "M = norm_pres_extensions E p F f"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   376
    and cM: "c \<in> chain M"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   377
  shows "\<forall>x \<in> H. h x \<le> p x"
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   378
proof
9503
wenzelm
parents: 9394
diff changeset
   379
  fix x assume "x \<in> H"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   380
  with M cM graph obtain H' h' where x': "x \<in> H'"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   381
      and graphs: "graph H' h' \<subseteq> graph H h"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   382
      and a: "\<forall>x \<in> H'. h' x \<le> p x"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   383
    by (rule some_H'h' [elim_format]) blast
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   384
  from graphs x' have [symmetric]: "h' x = h x" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   385
  also from a x' have "h' x \<le> p x " ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   386
  finally show "h x \<le> p x" .
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   387
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   388
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   389
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   390
  \medskip The following lemma is a property of linear forms on real
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
   391
  vector spaces. It will be used for the lemma @{text abs_Hahn_Banach}
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
   392
  (see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   393
  vector spaces the following inequations are equivalent:
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   394
  \begin{center}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   395
  \begin{tabular}{lll}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   396
  @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   397
  @{text "\<forall>x \<in> H. h x \<le> p x"} \\
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   398
  \end{tabular}
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   399
  \end{center}
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   400
*}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   401
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   402
lemma abs_ineq_iff:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   403
  assumes "subspace H E" and "vectorspace E" and "seminorm E p"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 23378
diff changeset
   404
    and "linearform H h"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   405
  shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   406
proof
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 27612
diff changeset
   407
  interpret subspace H E by fact
60f7fb56f8cd More porting to new locales.
ballarin
parents: 27612
diff changeset
   408
  interpret vectorspace E by fact
60f7fb56f8cd More porting to new locales.
ballarin
parents: 27612
diff changeset
   409
  interpret seminorm E p by fact
60f7fb56f8cd More porting to new locales.
ballarin
parents: 27612
diff changeset
   410
  interpret linearform H h by fact
23378
1d138d6bb461 tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
   411
  have H: "vectorspace H" using `vectorspace E` ..
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   412
  {
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   413
    assume l: ?L
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   414
    show ?R
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   415
    proof
9503
wenzelm
parents: 9394
diff changeset
   416
      fix x assume x: "x \<in> H"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   417
      have "h x \<le> \<bar>h x\<bar>" by arith
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   418
      also from l x have "\<dots> \<le> p x" ..
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   419
      finally show "h x \<le> p x" .
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   420
    qed
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   421
  next
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   422
    assume r: ?R
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   423
    show ?L
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   424
    proof
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   425
      fix x assume x: "x \<in> H"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   426
      show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   427
        by arith
23378
1d138d6bb461 tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
   428
      from `linearform H h` and H x
1d138d6bb461 tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
   429
      have "- h x = h (- x)" by (rule linearform.neg [symmetric])
14710
247615bfffb8 replaced Aux.thy by RealLemmas.thy
bauerg
parents: 13547
diff changeset
   430
      also
247615bfffb8 replaced Aux.thy by RealLemmas.thy
bauerg
parents: 13547
diff changeset
   431
      from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
247615bfffb8 replaced Aux.thy by RealLemmas.thy
bauerg
parents: 13547
diff changeset
   432
      with r have "h (- x) \<le> p (- x)" ..
247615bfffb8 replaced Aux.thy by RealLemmas.thy
bauerg
parents: 13547
diff changeset
   433
      also have "\<dots> = p x"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
   434
        using `seminorm E p` `vectorspace E`
14710
247615bfffb8 replaced Aux.thy by RealLemmas.thy
bauerg
parents: 13547
diff changeset
   435
      proof (rule seminorm.minus)
247615bfffb8 replaced Aux.thy by RealLemmas.thy
bauerg
parents: 13547
diff changeset
   436
        from x show "x \<in> E" ..
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   437
      qed
14710
247615bfffb8 replaced Aux.thy by RealLemmas.thy
bauerg
parents: 13547
diff changeset
   438
      finally have "- h x \<le> p x" .
247615bfffb8 replaced Aux.thy by RealLemmas.thy
bauerg
parents: 13547
diff changeset
   439
      then show "- p x \<le> h x" by simp
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   440
      from r x show "h x \<le> p x" ..
9261
879e0f0cd047 removed sorry;
bauerg
parents: 9256
diff changeset
   441
    qed
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
   442
  }
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   443
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents:
diff changeset
   444
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9623
diff changeset
   445
end