src/HOL/Hahn_Banach/Bounds.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 44887 7ca82df6e951
child 54263 c4159fe6fa46
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/Bounds.thy
7566
c5a3f980a7af accomodate refined facts handling;
wenzelm
parents: 7535
diff changeset
     2
    Author:     Gertrud Bauer, TU Munich
c5a3f980a7af accomodate refined facts handling;
wenzelm
parents: 7535
diff changeset
     3
*)
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     4
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 8659
diff changeset
     5
header {* Bounds *}
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7656
diff changeset
     6
25596
ad9e3594f3f3 tuned header
haftmann
parents: 21404
diff changeset
     7
theory Bounds
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 32960
diff changeset
     8
imports Main "~~/src/HOL/Library/ContNotDenum"
25596
ad9e3594f3f3 tuned header
haftmann
parents: 21404
diff changeset
     9
begin
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    10
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    11
locale lub =
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    12
  fixes A and x
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    13
  assumes least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<le> b) \<Longrightarrow> x \<le> b"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    14
    and upper [intro?]: "a \<in> A \<Longrightarrow> a \<le> x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    15
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    16
lemmas [elim?] = lub.least lub.upper
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    17
44887
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
    18
definition the_lub :: "'a::order set \<Rightarrow> 'a"
7ca82df6e951 misc tuning and clarification;
wenzelm
parents: 41413
diff changeset
    19
  where "the_lub A = The (lub A)"
14653
0848ab6fe5fc constdefs: proper order;
wenzelm
parents: 13515
diff changeset
    20
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 19736
diff changeset
    21
notation (xsymbols)
19736
wenzelm
parents: 16417
diff changeset
    22
  the_lub  ("\<Squnion>_" [90] 90)
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    23
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    24
lemma the_lub_equality [elim?]:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25596
diff changeset
    25
  assumes "lub A x"
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    26
  shows "\<Squnion>A = (x::'a::order)"
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25596
diff changeset
    27
proof -
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 29043
diff changeset
    28
  interpret lub A x by fact
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    29
  show ?thesis
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    30
  proof (unfold the_lub_def)
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25596
diff changeset
    31
    from `lub A x` show "The (lub A) = x"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25596
diff changeset
    32
    proof
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25596
diff changeset
    33
      fix x' assume lub': "lub A x'"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25596
diff changeset
    34
      show "x' = x"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25596
diff changeset
    35
      proof (rule order_antisym)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
    36
        from lub' show "x' \<le> x"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
    37
        proof
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25596
diff changeset
    38
          fix a assume "a \<in> A"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25596
diff changeset
    39
          then show "a \<le> x" ..
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
    40
        qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
    41
        show "x \<le> x'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
    42
        proof
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25596
diff changeset
    43
          fix a assume "a \<in> A"
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25596
diff changeset
    44
          with lub' show "a \<le> x'" ..
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31795
diff changeset
    45
        qed
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    46
      qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    47
    qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    48
  qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    49
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    50
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    51
lemma the_lubI_ex:
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    52
  assumes ex: "\<exists>x. lub A x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    53
  shows "lub A (\<Squnion>A)"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    54
proof -
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    55
  from ex obtain x where x: "lub A x" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    56
  also from x have [symmetric]: "\<Squnion>A = x" ..
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    57
  finally show ?thesis .
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    58
qed
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    59
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    60
lemma lub_compat: "lub A x = isLub UNIV A x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    61
proof -
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    62
  have "isUb UNIV A = (\<lambda>x. A *<= x \<and> x \<in> UNIV)"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    63
    by (rule ext) (simp only: isUb_def)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    64
  then show ?thesis
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    65
    by (simp only: lub_def isLub_def leastP_def setge_def setle_def) blast
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 8659
diff changeset
    66
qed
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    67
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    68
lemma real_complete:
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    69
  fixes A :: "real set"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    70
  assumes nonempty: "\<exists>a. a \<in> A"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    71
    and ex_upper: "\<exists>y. \<forall>a \<in> A. a \<le> y"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    72
  shows "\<exists>x. lub A x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    73
proof -
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    74
  from ex_upper have "\<exists>y. isUb UNIV A y"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    75
    unfolding isUb_def setle_def by blast
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    76
  with nonempty have "\<exists>x. isLub UNIV A x"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    77
    by (rule reals_complete)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    78
  then show ?thesis by (simp only: lub_compat)
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    79
qed
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 10687
diff changeset
    80
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9503
diff changeset
    81
end