author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44887  7ca82df6e951 
child 54263  c4159fe6fa46 
permissions  rwrr 
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

1 
(* Title: HOL/Hahn_Banach/Bounds.thy 
7566  2 
Author: Gertrud Bauer, TU Munich 
3 
*) 

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

4 

9035  5 
header {* Bounds *} 
7808  6 

25596  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  9 
begin 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

10 

13515  11 
locale lub = 
12 
fixes A and x 

13 
assumes least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<le> b) \<Longrightarrow> x \<le> b" 

14 
and upper [intro?]: "a \<in> A \<Longrightarrow> a \<le> x" 

15 

16 
lemmas [elim?] = lub.least lub.upper 

17 

44887  18 
definition the_lub :: "'a::order set \<Rightarrow> 'a" 
19 
where "the_lub A = The (lub A)" 

14653  20 

21210  21 
notation (xsymbols) 
19736  22 
the_lub ("\<Squnion>_" [90] 90) 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

23 

13515  24 
lemma the_lub_equality [elim?]: 
27611  25 
assumes "lub A x" 
13515  26 
shows "\<Squnion>A = (x::'a::order)" 
27611  27 
proof  
29234  28 
interpret lub A x by fact 
27612  29 
show ?thesis 
30 
proof (unfold the_lub_def) 

27611  31 
from `lub A x` show "The (lub A) = x" 
32 
proof 

33 
fix x' assume lub': "lub A x'" 

34 
show "x' = x" 

35 
proof (rule order_antisym) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

36 
from lub' show "x' \<le> x" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

37 
proof 
27611  38 
fix a assume "a \<in> A" 
39 
then show "a \<le> x" .. 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

40 
qed 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

41 
show "x \<le> x'" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

42 
proof 
27611  43 
fix a assume "a \<in> A" 
44 
with lub' show "a \<le> x'" .. 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

45 
qed 
13515  46 
qed 
47 
qed 

48 
qed 

49 
qed 

7917  50 

13515  51 
lemma the_lubI_ex: 
52 
assumes ex: "\<exists>x. lub A x" 

53 
shows "lub A (\<Squnion>A)" 

54 
proof  

55 
from ex obtain x where x: "lub A x" .. 

56 
also from x have [symmetric]: "\<Squnion>A = x" .. 

57 
finally show ?thesis . 

58 
qed 

7917  59 

13515  60 
lemma lub_compat: "lub A x = isLub UNIV A x" 
61 
proof  

62 
have "isUb UNIV A = (\<lambda>x. A *<= x \<and> x \<in> UNIV)" 

63 
by (rule ext) (simp only: isUb_def) 

64 
then show ?thesis 

65 
by (simp only: lub_def isLub_def leastP_def setge_def setle_def) blast 

9035  66 
qed 
13515  67 

68 
lemma real_complete: 

69 
fixes A :: "real set" 

70 
assumes nonempty: "\<exists>a. a \<in> A" 

71 
and ex_upper: "\<exists>y. \<forall>a \<in> A. a \<le> y" 

72 
shows "\<exists>x. lub A x" 

73 
proof  

74 
from ex_upper have "\<exists>y. isUb UNIV A y" 

27612  75 
unfolding isUb_def setle_def by blast 
13515  76 
with nonempty have "\<exists>x. isLub UNIV A x" 
77 
by (rule reals_complete) 

78 
then show ?thesis by (simp only: lub_compat) 

79 
qed 

80 

10687  81 
end 