author  hoelzl 
Tue, 26 Mar 2013 12:20:52 +0100  
changeset 51518  6a56b7088a6a 
parent 51475  src/HOL/SupInf.thy@ebf9d4fd00ba 
child 51643  b6675f4549d8 
permissions  rwrr 
51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

1 
(* Title: HOL/Conditional_Complete_Lattices.thy 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

2 
Author: Amine Chaieb and L C Paulson, University of Cambridge 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

3 
Author: Johanens Hölzl, TU München 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

4 
*) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

5 

51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

6 
header {* Conditional Complete Lattices *} 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

7 

51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

8 
theory Conditional_Complete_Lattices 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

9 
imports Main Lubs 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

10 
begin 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

11 

51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

12 
lemma Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

13 
by (induct X rule: finite_ne_induct) (simp_all add: sup_max) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

14 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

15 
lemma Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

16 
by (induct X rule: finite_ne_induct) (simp_all add: inf_min) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

17 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

18 
text {* 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

19 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

20 
To avoid name classes with the @{class complete_lattice}class we prefix @{const Sup} and 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

21 
@{const Inf} in theorem names with c. 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

22 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

23 
*} 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

24 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

25 
class conditional_complete_lattice = lattice + Sup + Inf + 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

26 
assumes cInf_lower: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> z \<le> a) \<Longrightarrow> Inf X \<le> x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

27 
and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

28 
assumes cSup_upper: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> a \<le> z) \<Longrightarrow> x \<le> Sup X" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

29 
and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z" 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

30 
begin 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

31 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

32 
lemma cSup_eq_maximum: (*REAL_SUP_MAX in HOL4*) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

33 
"z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

34 
by (blast intro: antisym cSup_upper cSup_least) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

35 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

36 
lemma cInf_eq_minimum: (*REAL_INF_MIN in HOL4*) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

37 
"z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

38 
by (intro antisym cInf_lower[of z X z] cInf_greatest[of X z]) auto 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

39 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

40 
lemma cSup_le_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> a \<le> z) \<Longrightarrow> Sup S \<le> a \<longleftrightarrow> (\<forall>x\<in>S. x \<le> a)" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

41 
by (metis order_trans cSup_upper cSup_least) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

42 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

43 
lemma le_cInf_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> z \<le> a) \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

44 
by (metis order_trans cInf_lower cInf_greatest) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

45 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

46 
lemma cSup_singleton [simp]: "Sup {x} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

47 
by (intro cSup_eq_maximum) auto 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

48 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

49 
lemma cInf_singleton [simp]: "Inf {x} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

50 
by (intro cInf_eq_minimum) auto 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

51 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

52 
lemma cSup_upper2: (*REAL_IMP_LE_SUP in HOL4*) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

53 
"x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

54 
by (metis cSup_upper order_trans) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

55 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

56 
lemma cInf_lower2: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

57 
"x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

58 
by (metis cInf_lower order_trans) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

59 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

60 
lemma cSup_upper_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

61 
by (blast intro: cSup_upper) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

62 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

63 
lemma cInf_lower_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

64 
by (blast intro: cInf_lower) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

65 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

66 
lemma cSup_eq_non_empty: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

67 
assumes 1: "X \<noteq> {}" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

68 
assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

69 
assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

70 
shows "Sup X = a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

71 
by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

72 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

73 
lemma cInf_eq_non_empty: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

74 
assumes 1: "X \<noteq> {}" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

75 
assumes 2: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

76 
assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

77 
shows "Inf X = a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

78 
by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

79 

51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

80 
lemma cInf_cSup: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf S = Sup {x. \<forall>s\<in>S. x \<le> s}" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

81 
by (rule cInf_eq_non_empty) (auto intro: cSup_upper cSup_least) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

82 

6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

83 
lemma cSup_cInf: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup S = Inf {x. \<forall>s\<in>S. s \<le> x}" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

84 
by (rule cSup_eq_non_empty) (auto intro: cInf_lower cInf_greatest) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

85 

51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

86 
lemma cSup_insert: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

87 
assumes x: "X \<noteq> {}" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

88 
and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

89 
shows "Sup (insert a X) = sup a (Sup X)" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

90 
proof (intro cSup_eq_non_empty) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

91 
fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> x \<le> y" with x show "sup a (Sup X) \<le> y" by (auto intro: cSup_least) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

92 
qed (auto intro: le_supI2 z cSup_upper) 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

93 

51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

94 
lemma cInf_insert: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

95 
assumes x: "X \<noteq> {}" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

96 
and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

97 
shows "Inf (insert a X) = inf a (Inf X)" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

98 
proof (intro cInf_eq_non_empty) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

99 
fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> y \<le> x" with x show "y \<le> inf a (Inf X)" by (auto intro: cInf_greatest) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

100 
qed (auto intro: le_infI2 z cInf_lower) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

101 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

102 
lemma cSup_insert_If: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

103 
"(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

104 
using cSup_insert[of X z] by simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

105 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

106 
lemma cInf_insert_if: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

107 
"(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

108 
using cInf_insert[of X z] by simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

109 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

110 
lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

111 
proof (induct X arbitrary: x rule: finite_induct) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

112 
case (insert x X y) then show ?case 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

113 
apply (cases "X = {}") 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

114 
apply simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

115 
apply (subst cSup_insert[of _ "Sup X"]) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

116 
apply (auto intro: le_supI2) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

117 
done 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

118 
qed simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

119 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

120 
lemma cInf_le_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> Inf X \<le> x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

121 
proof (induct X arbitrary: x rule: finite_induct) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

122 
case (insert x X y) then show ?case 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

123 
apply (cases "X = {}") 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

124 
apply simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

125 
apply (subst cInf_insert[of _ "Inf X"]) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

126 
apply (auto intro: le_infI2) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

127 
done 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

128 
qed simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

129 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

130 
lemma cSup_eq_Sup_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Sup_fin X" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

131 
proof (induct X rule: finite_ne_induct) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

132 
case (insert x X) then show ?case 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

133 
using cSup_insert[of X "Sup_fin X" x] le_cSup_finite[of X] by simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

134 
qed simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

135 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

136 
lemma cInf_eq_Inf_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Inf_fin X" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

137 
proof (induct X rule: finite_ne_induct) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

138 
case (insert x X) then show ?case 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

139 
using cInf_insert[of X "Inf_fin X" x] cInf_le_finite[of X] by simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

140 
qed simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

141 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

142 
lemma cSup_atMost[simp]: "Sup {..x} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

143 
by (auto intro!: cSup_eq_maximum) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

144 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

145 
lemma cSup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

146 
by (auto intro!: cSup_eq_maximum) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

147 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

148 
lemma cSup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

149 
by (auto intro!: cSup_eq_maximum) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

150 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

151 
lemma cInf_atLeast[simp]: "Inf {x..} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

152 
by (auto intro!: cInf_eq_minimum) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

153 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

154 
lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

155 
by (auto intro!: cInf_eq_minimum) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

156 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

157 
lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

158 
by (auto intro!: cInf_eq_minimum) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

159 

33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

160 
end 
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

161 

51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

162 
instance complete_lattice \<subseteq> conditional_complete_lattice 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

163 
by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

164 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

165 
lemma isLub_cSup: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

166 
"(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

167 
by (auto simp add: isLub_def setle_def leastP_def isUb_def 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

168 
intro!: setgeI intro: cSup_upper cSup_least) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

169 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

170 
lemma cSup_eq: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

171 
fixes a :: "'a :: {conditional_complete_lattice, no_bot}" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

172 
assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

173 
assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

174 
shows "Sup X = a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

175 
proof cases 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

176 
assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

177 
qed (intro cSup_eq_non_empty assms) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

178 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

179 
lemma cInf_eq: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

180 
fixes a :: "'a :: {conditional_complete_lattice, no_top}" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

181 
assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

182 
assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

183 
shows "Inf X = a" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

184 
proof cases 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

185 
assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

186 
qed (intro cInf_eq_non_empty assms) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

187 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

188 
lemma cSup_le: "(S::'a::conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

189 
by (metis cSup_least setle_def) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

190 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

191 
lemma cInf_ge: "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

192 
by (metis cInf_greatest setge_def) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

193 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

194 
class conditional_complete_linorder = conditional_complete_lattice + linorder 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

195 
begin 
51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

196 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

197 
lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

198 
"X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

199 
by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

200 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

201 
lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

202 
by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

203 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

204 
lemma less_cSupE: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

205 
assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

206 
by (metis cSup_least assms not_le that) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

207 

51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

208 
lemma less_cSupD: 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

209 
"X \<noteq> {} \<Longrightarrow> z < Sup X \<Longrightarrow> \<exists>x\<in>X. z < x" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

210 
by (metis less_cSup_iff not_leE) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

211 

6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

212 
lemma cInf_lessD: 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

213 
"X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

214 
by (metis cInf_less_iff not_leE) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

215 

51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

216 
lemma complete_interval: 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

217 
assumes "a < b" and "P a" and "\<not> P b" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

218 
shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and> 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

219 
(\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

220 
proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d > P x}"], auto) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

221 
show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

222 
by (rule cSup_upper [where z=b], auto) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

223 
(metis `a < b` `\<not> P b` linear less_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

224 
next 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

225 
show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

226 
apply (rule cSup_least) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

227 
apply auto 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

228 
apply (metis less_le_not_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

229 
apply (metis `a<b` `~ P b` linear less_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

230 
done 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

231 
next 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

232 
fix x 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

233 
assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

234 
show "P x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

235 
apply (rule less_cSupE [OF lt], auto) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

236 
apply (metis less_le_not_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

237 
apply (metis x) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

238 
done 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

239 
next 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

240 
fix d 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

241 
assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

242 
thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

243 
by (rule_tac z="b" in cSup_upper, auto) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

244 
(metis `a<b` `~ P b` linear less_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

245 
qed 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

246 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

247 
end 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

248 

51518
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

249 
lemma cSup_bounds: 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

250 
fixes S :: "'a :: conditional_complete_lattice set" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

251 
assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

252 
shows "a \<le> Sup S \<and> Sup S \<le> b" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

253 
proof 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

254 
from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

255 
hence b: "Sup S \<le> b" using u 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

256 
by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

257 
from Se obtain y where y: "y \<in> S" by blast 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

258 
from lub l have "a \<le> Sup S" 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

259 
by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

260 
(metis le_iff_sup le_sup_iff y) 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

261 
with b show ?thesis by blast 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

262 
qed 
6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

263 

6a56b7088a6a
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
hoelzl
parents:
51475
diff
changeset

264 

51475
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

265 
lemma cSup_unique: "(S::'a :: {conditional_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

266 
by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

267 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

268 
lemma cInf_unique: "b <=* (S::'a :: {conditional_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

269 
by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

270 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

271 
lemma cSup_eq_Max: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

272 
using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

273 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

274 
lemma cInf_eq_Min: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

275 
using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

276 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

277 
lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditional_complete_linorder, dense_linorder}} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

278 
by (auto intro!: cSup_eq_non_empty intro: dense_le) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

279 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

280 
lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

281 
by (auto intro!: cSup_eq intro: dense_le_bounded) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

282 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

283 
lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditional_complete_linorder, dense_linorder}} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

284 
by (auto intro!: cSup_eq intro: dense_le_bounded) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

285 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

286 
lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditional_complete_linorder, dense_linorder} <..} = x" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

287 
by (auto intro!: cInf_eq intro: dense_ge) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

288 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

289 
lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditional_complete_linorder, dense_linorder}} = y" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

290 
by (auto intro!: cInf_eq intro: dense_ge_bounded) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

291 

ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

292 
lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = y" 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

293 
by (auto intro!: cInf_eq intro: dense_ge_bounded) 
ebf9d4fd00ba
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
hoelzl
parents:
46757
diff
changeset

294 

33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
diff
changeset

295 
end 