author  ballarin 
Tue, 16 Dec 2008 21:10:53 +0100  
changeset 29237  e90d9d51106b 
parent 28823  dcbef866c9e2 
child 29242  e190bc2a5399 
permissions  rwrr 
14551  1 
(* 
27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

2 
Title: HOL/Algebra/Lattice.thy 
14551  3 
Author: Clemens Ballarin, started 7 November 2003 
4 
Copyright: Clemens Ballarin 

27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

5 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

6 
Most congruence rules by Stephan Hohe. 
14551  7 
*) 
8 

27700  9 
theory Lattice imports Congruence begin 
14551  10 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

11 
section {* Orders and Lattices *} 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

12 

14551  13 
subsection {* Partial Orders *} 
14 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

15 
record 'a gorder = "'a eq_object" + 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

16 
le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50) 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

17 

29237  18 
locale weak_partial_order = equivalence L for L (structure) + 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

19 
assumes le_refl [intro, simp]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

20 
"x \<in> carrier L ==> x \<sqsubseteq> x" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

21 
and weak_le_anti_sym [intro]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

22 
"[ x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L ] ==> x .= y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

23 
and le_trans [trans]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

24 
"[ x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L ] ==> x \<sqsubseteq> z" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

25 
and le_cong: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

26 
"\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

27 

717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

28 
constdefs (structure L) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

29 
lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

30 
"x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

31 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

32 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

33 
subsubsection {* The order relation *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

34 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

35 
context weak_partial_order begin 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

36 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

37 
lemma le_cong_l [intro, trans]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

38 
"\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

39 
by (auto intro: le_cong [THEN iffD2]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

40 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

41 
lemma le_cong_r [intro, trans]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

42 
"\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

43 
by (auto intro: le_cong [THEN iffD1]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

44 

27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

45 
lemma weak_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

46 
by (simp add: le_cong_l) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

47 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

48 
end 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

49 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

50 
lemma weak_llessI: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

51 
fixes R (structure) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

52 
assumes "x \<sqsubseteq> y" and "~(x .= y)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

53 
shows "x \<sqsubset> y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

54 
using assms unfolding lless_def by simp 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

55 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

56 
lemma lless_imp_le: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

57 
fixes R (structure) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

58 
assumes "x \<sqsubset> y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

59 
shows "x \<sqsubseteq> y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

60 
using assms unfolding lless_def by simp 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

61 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

62 
lemma weak_lless_imp_not_eq: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

63 
fixes R (structure) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

64 
assumes "x \<sqsubset> y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

65 
shows "\<not> (x .= y)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

66 
using assms unfolding lless_def by simp 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

67 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

68 
lemma weak_llessE: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

69 
fixes R (structure) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

70 
assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

71 
shows "P" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

72 
using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

73 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

74 
lemma (in weak_partial_order) lless_cong_l [trans]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

75 
assumes xx': "x .= x'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

76 
and xy: "x' \<sqsubset> y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

77 
and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

78 
shows "x \<sqsubset> y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

79 
using assms unfolding lless_def by (auto intro: trans sym) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

80 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

81 
lemma (in weak_partial_order) lless_cong_r [trans]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

82 
assumes xy: "x \<sqsubset> y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

83 
and yy': "y .= y'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

84 
and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

85 
shows "x \<sqsubset> y'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

86 
using assms unfolding lless_def by (auto intro: trans sym) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

87 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

88 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

89 
lemma (in weak_partial_order) lless_antisym: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

90 
assumes "a \<in> carrier L" "b \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

91 
and "a \<sqsubset> b" "b \<sqsubset> a" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

92 
shows "P" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

93 
using assms 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

94 
by (elim weak_llessE) auto 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

95 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

96 
lemma (in weak_partial_order) lless_trans [trans]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

97 
assumes "a \<sqsubset> b" "b \<sqsubset> c" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

98 
and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

99 
shows "a \<sqsubset> c" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

100 
using assms unfolding lless_def by (blast dest: le_trans intro: sym) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

101 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

102 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

103 
subsubsection {* Upper and lower bounds of a set *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

104 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

105 
constdefs (structure L) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

106 
Upper :: "[_, 'a set] => 'a set" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

107 
"Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L > x \<sqsubseteq> u)} \<inter> carrier L" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

108 

717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

109 
Lower :: "[_, 'a set] => 'a set" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

110 
"Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L > l \<sqsubseteq> x)} \<inter> carrier L" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

111 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

112 
lemma Upper_closed [intro!, simp]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

113 
"Upper L A \<subseteq> carrier L" 
14551  114 
by (unfold Upper_def) clarify 
115 

27700  116 
lemma Upper_memD [dest]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

117 
fixes L (structure) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

118 
shows "[ u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L ] ==> x \<sqsubseteq> u \<and> u \<in> carrier L" 
14693  119 
by (unfold Upper_def) blast 
14551  120 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

121 
lemma (in weak_partial_order) Upper_elemD [dest]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

122 
"[ u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L ] ==> x \<sqsubseteq> u" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

123 
unfolding Upper_def elem_def 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

124 
by (blast dest: sym) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

125 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

126 
lemma Upper_memI: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

127 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

128 
shows "[ !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L ] ==> x \<in> Upper L A" 
14693  129 
by (unfold Upper_def) blast 
14551  130 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

131 
lemma (in weak_partial_order) Upper_elemI: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

132 
"[ !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L ] ==> x .\<in> Upper L A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

133 
unfolding Upper_def by blast 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

134 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

135 
lemma Upper_antimono: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

136 
"A \<subseteq> B ==> Upper L B \<subseteq> Upper L A" 
14551  137 
by (unfold Upper_def) blast 
138 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

139 
lemma (in weak_partial_order) Upper_is_closed [simp]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

140 
"A \<subseteq> carrier L ==> is_closed (Upper L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

141 
by (rule is_closedI) (blast intro: Upper_memI)+ 
14651  142 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

143 
lemma (in weak_partial_order) Upper_mem_cong: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

144 
assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

145 
and aa': "a .= a'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

146 
and aelem: "a \<in> Upper L A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

147 
shows "a' \<in> Upper L A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

148 
proof (rule Upper_memI[OF _ a'carr]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

149 
fix y 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

150 
assume yA: "y \<in> A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

151 
hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

152 
also note aa' 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

153 
finally 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

154 
show "y \<sqsubseteq> a'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

155 
by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

156 
qed 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

157 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

158 
lemma (in weak_partial_order) Upper_cong: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

159 
assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

160 
and AA': "A {.=} A'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

161 
shows "Upper L A = Upper L A'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

162 
unfolding Upper_def 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

163 
apply rule 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

164 
apply (rule, clarsimp) defer 1 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

165 
apply (rule, clarsimp) defer 1 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

166 
proof  
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

167 
fix x a' 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

168 
assume carr: "x \<in> carrier L" "a' \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

169 
and a'A': "a' \<in> A'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

170 
assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x" 
14551  171 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

172 
from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

173 
from this obtain a 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

174 
where aA: "a \<in> A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

175 
and a'a: "a' .= a" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

176 
by auto 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

177 
note [simp] = subsetD[OF Acarr aA] carr 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

178 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

179 
note a'a 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

180 
also have "a \<sqsubseteq> x" by (simp add: aLxCond aA) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

181 
finally show "a' \<sqsubseteq> x" by simp 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

182 
next 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

183 
fix x a 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

184 
assume carr: "x \<in> carrier L" "a \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

185 
and aA: "a \<in> A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

186 
assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

187 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

188 
from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

189 
from this obtain a' 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

190 
where a'A': "a' \<in> A'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

191 
and aa': "a .= a'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

192 
by auto 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

193 
note [simp] = subsetD[OF A'carr a'A'] carr 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

194 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

195 
note aa' 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

196 
also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A') 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

197 
finally show "a \<sqsubseteq> x" by simp 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

198 
qed 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

199 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

200 
lemma Lower_closed [intro!, simp]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

201 
"Lower L A \<subseteq> carrier L" 
14551  202 
by (unfold Lower_def) clarify 
203 

27700  204 
lemma Lower_memD [dest]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

205 
fixes L (structure) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

206 
shows "[ l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L ] ==> l \<sqsubseteq> x \<and> l \<in> carrier L" 
14693  207 
by (unfold Lower_def) blast 
14551  208 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

209 
lemma Lower_memI: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

210 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

211 
shows "[ !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L ] ==> x \<in> Lower L A" 
14693  212 
by (unfold Lower_def) blast 
14551  213 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

214 
lemma Lower_antimono: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

215 
"A \<subseteq> B ==> Lower L B \<subseteq> Lower L A" 
14551  216 
by (unfold Lower_def) blast 
217 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

218 
lemma (in weak_partial_order) Lower_is_closed [simp]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

219 
"A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

220 
by (rule is_closedI) (blast intro: Lower_memI dest: sym)+ 
14651  221 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

222 
lemma (in weak_partial_order) Lower_mem_cong: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

223 
assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

224 
and aa': "a .= a'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

225 
and aelem: "a \<in> Lower L A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

226 
shows "a' \<in> Lower L A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

227 
using assms Lower_closed[of L A] 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

228 
by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

229 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

230 
lemma (in weak_partial_order) Lower_cong: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

231 
assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

232 
and AA': "A {.=} A'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

233 
shows "Lower L A = Lower L A'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

234 
using Lower_memD[of y] 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

235 
unfolding Lower_def 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

236 
apply safe 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

237 
apply clarsimp defer 1 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

238 
apply clarsimp defer 1 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

239 
proof  
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

240 
fix x a' 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

241 
assume carr: "x \<in> carrier L" "a' \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

242 
and a'A': "a' \<in> A'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

243 
assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

244 
hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

245 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

246 
from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

247 
from this obtain a 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

248 
where aA: "a \<in> A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

249 
and a'a: "a' .= a" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

250 
by auto 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

251 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

252 
from aA and subsetD[OF Acarr aA] 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

253 
have "x \<sqsubseteq> a" by (rule aLxCond) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

254 
also note a'a[symmetric] 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

255 
finally 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

256 
show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

257 
next 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

258 
fix x a 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

259 
assume carr: "x \<in> carrier L" "a \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

260 
and aA: "a \<in> A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

261 
assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

262 
hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+ 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

263 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

264 
from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

265 
from this obtain a' 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

266 
where a'A': "a' \<in> A'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

267 
and aa': "a .= a'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

268 
by auto 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

269 
from a'A' and subsetD[OF A'carr a'A'] 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

270 
have "x \<sqsubseteq> a'" by (rule a'LxCond) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

271 
also note aa'[symmetric] 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

272 
finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A']) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

273 
qed 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

274 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

275 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

276 
subsubsection {* Least and greatest, as predicate *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

277 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

278 
constdefs (structure L) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

279 
least :: "[_, 'a, 'a set] => bool" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

280 
"least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

281 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

282 
greatest :: "[_, 'a, 'a set] => bool" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

283 
"greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

284 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

285 
text {* Could weaken these to @{term [locale=weak_partial_order] "l \<in> carrier L \<and> l 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

286 
.\<in> A"} and @{term [locale=weak_partial_order] "g \<in> carrier L \<and> g .\<in> A"}. *} 
14551  287 

27700  288 
lemma least_closed [intro, simp]: 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

289 
"least L l A ==> l \<in> carrier L" 
14551  290 
by (unfold least_def) fast 
291 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

292 
lemma least_mem: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

293 
"least L l A ==> l \<in> A" 
14551  294 
by (unfold least_def) fast 
295 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

296 
lemma (in weak_partial_order) weak_least_unique: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

297 
"[ least L x A; least L y A ] ==> x .= y" 
14551  298 
by (unfold least_def) blast 
299 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

300 
lemma least_le: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

301 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

302 
shows "[ least L x A; a \<in> A ] ==> x \<sqsubseteq> a" 
14551  303 
by (unfold least_def) fast 
304 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

305 
lemma (in weak_partial_order) least_cong: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

306 
"[ x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A ] ==> least L x A = least L x' A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

307 
by (unfold least_def) (auto dest: sym) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

308 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

309 
text {* @{const least} is not congruent in the second parameter for 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

310 
@{term [locale=weak_partial_order] "A {.=} A'"} *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

311 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

312 
lemma (in weak_partial_order) least_Upper_cong_l: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

313 
assumes "x .= x'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

314 
and "x \<in> carrier L" "x' \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

315 
and "A \<subseteq> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

316 
shows "least L x (Upper L A) = least L x' (Upper L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

317 
apply (rule least_cong) using assms by auto 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

318 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

319 
lemma (in weak_partial_order) least_Upper_cong_r: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

320 
assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

321 
and AA': "A {.=} A'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

322 
shows "least L x (Upper L A) = least L x (Upper L A')" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

323 
apply (subgoal_tac "Upper L A = Upper L A'", simp) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

324 
by (rule Upper_cong) fact+ 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

325 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

326 
lemma least_UpperI: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

327 
fixes L (structure) 
14551  328 
assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

329 
and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

330 
and L: "A \<subseteq> carrier L" "s \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

331 
shows "least L s (Upper L A)" 
14693  332 
proof  
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

333 
have "Upper L A \<subseteq> carrier L" by simp 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

334 
moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

335 
moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast 
14693  336 
ultimately show ?thesis by (simp add: least_def) 
14551  337 
qed 
338 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

339 
lemma least_Upper_above: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

340 
fixes L (structure) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

341 
shows "[ least L s (Upper L A); x \<in> A; A \<subseteq> carrier L ] ==> x \<sqsubseteq> s" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

342 
by (unfold least_def) blast 
14551  343 

27700  344 
lemma greatest_closed [intro, simp]: 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

345 
"greatest L l A ==> l \<in> carrier L" 
14551  346 
by (unfold greatest_def) fast 
347 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

348 
lemma greatest_mem: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

349 
"greatest L l A ==> l \<in> A" 
14551  350 
by (unfold greatest_def) fast 
351 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

352 
lemma (in weak_partial_order) weak_greatest_unique: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

353 
"[ greatest L x A; greatest L y A ] ==> x .= y" 
14551  354 
by (unfold greatest_def) blast 
355 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

356 
lemma greatest_le: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

357 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

358 
shows "[ greatest L x A; a \<in> A ] ==> a \<sqsubseteq> x" 
14551  359 
by (unfold greatest_def) fast 
360 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

361 
lemma (in weak_partial_order) greatest_cong: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

362 
"[ x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A ] ==> 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

363 
greatest L x A = greatest L x' A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

364 
by (unfold greatest_def) (auto dest: sym) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

365 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

366 
text {* @{const greatest} is not congruent in the second parameter for 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

367 
@{term [locale=weak_partial_order] "A {.=} A'"} *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

368 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

369 
lemma (in weak_partial_order) greatest_Lower_cong_l: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

370 
assumes "x .= x'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

371 
and "x \<in> carrier L" "x' \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

372 
and "A \<subseteq> carrier L" (* unneccessary with current Lower *) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

373 
shows "greatest L x (Lower L A) = greatest L x' (Lower L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

374 
apply (rule greatest_cong) using assms by auto 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

375 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

376 
lemma (in weak_partial_order) greatest_Lower_cong_r: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

377 
assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

378 
and AA': "A {.=} A'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

379 
shows "greatest L x (Lower L A) = greatest L x (Lower L A')" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

380 
apply (subgoal_tac "Lower L A = Lower L A'", simp) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

381 
by (rule Lower_cong) fact+ 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

382 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

383 
lemma greatest_LowerI: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

384 
fixes L (structure) 
14551  385 
assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

386 
and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

387 
and L: "A \<subseteq> carrier L" "i \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

388 
shows "greatest L i (Lower L A)" 
14693  389 
proof  
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

390 
have "Lower L A \<subseteq> carrier L" by simp 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

391 
moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

392 
moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast 
14693  393 
ultimately show ?thesis by (simp add: greatest_def) 
14551  394 
qed 
395 

27700  396 
lemma greatest_Lower_below: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

397 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

398 
shows "[ greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L ] ==> i \<sqsubseteq> x" 
14551  399 
by (unfold greatest_def) blast 
400 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

401 
text {* Supremum and infimum *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

402 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

403 
constdefs (structure L) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

404 
sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

405 
"\<Squnion>A == SOME x. least L x (Upper L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

406 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

407 
inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

408 
"\<Sqinter>A == SOME x. greatest L x (Lower L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

409 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

410 
join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

411 
"x \<squnion> y == \<Squnion> {x, y}" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

412 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

413 
meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

414 
"x \<sqinter> y == \<Sqinter> {x, y}" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

415 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

416 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

417 
subsection {* Lattices *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

418 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

419 
locale weak_upper_semilattice = weak_partial_order + 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

420 
assumes sup_of_two_exists: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

421 
"[ x \<in> carrier L; y \<in> carrier L ] ==> EX s. least L s (Upper L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

422 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

423 
locale weak_lower_semilattice = weak_partial_order + 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

424 
assumes inf_of_two_exists: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

425 
"[ x \<in> carrier L; y \<in> carrier L ] ==> EX s. greatest L s (Lower L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

426 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

427 
locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

428 

14666  429 

14551  430 
subsubsection {* Supremum *} 
431 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

432 
lemma (in weak_upper_semilattice) joinI: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

433 
"[ !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L ] 
14551  434 
==> P (x \<squnion> y)" 
435 
proof (unfold join_def sup_def) 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

436 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

437 
and P: "!!l. least L l (Upper L {x, y}) ==> P l" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

438 
with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

439 
with L show "P (SOME l. least L l (Upper L {x, y}))" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

440 
by (fast intro: someI2 P) 
14551  441 
qed 
442 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

443 
lemma (in weak_upper_semilattice) join_closed [simp]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

444 
"[ x \<in> carrier L; y \<in> carrier L ] ==> x \<squnion> y \<in> carrier L" 
27700  445 
by (rule joinI) (rule least_closed) 
14551  446 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

447 
lemma (in weak_upper_semilattice) join_cong_l: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

448 
assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

449 
and xx': "x .= x'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

450 
shows "x \<squnion> y .= x' \<squnion> y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

451 
proof (rule joinI, rule joinI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

452 
fix a b 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

453 
from xx' carr 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

454 
have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

455 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

456 
assume leasta: "least L a (Upper L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

457 
assume "least L b (Upper L {x', y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

458 
with carr 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

459 
have leastb: "least L b (Upper L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

460 
by (simp add: least_Upper_cong_r[OF _ _ seq]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

461 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

462 
from leasta leastb 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

463 
show "a .= b" by (rule weak_least_unique) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

464 
qed (rule carr)+ 
14551  465 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

466 
lemma (in weak_upper_semilattice) join_cong_r: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

467 
assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

468 
and yy': "y .= y'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

469 
shows "x \<squnion> y .= x \<squnion> y'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

470 
proof (rule joinI, rule joinI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

471 
fix a b 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

472 
have "{x, y} = {y, x}" by fast 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

473 
also from carr yy' 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

474 
have "{y, x} {.=} {y', x}" by (intro set_eq_pairI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

475 
also have "{y', x} = {x, y'}" by fast 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

476 
finally 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

477 
have seq: "{x, y} {.=} {x, y'}" . 
14551  478 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

479 
assume leasta: "least L a (Upper L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

480 
assume "least L b (Upper L {x, y'})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

481 
with carr 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

482 
have leastb: "least L b (Upper L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

483 
by (simp add: least_Upper_cong_r[OF _ _ seq]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

484 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

485 
from leasta leastb 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

486 
show "a .= b" by (rule weak_least_unique) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

487 
qed (rule carr)+ 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

488 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

489 
lemma (in weak_partial_order) sup_of_singletonI: (* only reflexivity needed ? *) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

490 
"x \<in> carrier L ==> least L x (Upper L {x})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

491 
by (rule least_UpperI) auto 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

492 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

493 
lemma (in weak_partial_order) weak_sup_of_singleton [simp]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

494 
"x \<in> carrier L ==> \<Squnion>{x} .= x" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

495 
unfolding sup_def 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

496 
by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

497 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

498 
lemma (in weak_partial_order) sup_of_singleton_closed [simp]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

499 
"x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

500 
unfolding sup_def 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

501 
by (rule someI2) (auto intro: sup_of_singletonI) 
14666  502 

503 
text {* Condition on @{text A}: supremum exists. *} 

14551  504 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

505 
lemma (in weak_upper_semilattice) sup_insertI: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

506 
"[ !!s. least L s (Upper L (insert x A)) ==> P s; 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

507 
least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L ] 
14693  508 
==> P (\<Squnion>(insert x A))" 
14551  509 
proof (unfold sup_def) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

510 
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

511 
and P: "!!l. least L l (Upper L (insert x A)) ==> P l" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

512 
and least_a: "least L a (Upper L A)" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

513 
from L least_a have La: "a \<in> carrier L" by simp 
14551  514 
from L sup_of_two_exists least_a 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

515 
obtain s where least_s: "least L s (Upper L {a, x})" by blast 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

516 
show "P (SOME l. least L l (Upper L (insert x A)))" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

517 
proof (rule someI2) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

518 
show "least L s (Upper L (insert x A))" 
14551  519 
proof (rule least_UpperI) 
520 
fix z 

14693  521 
assume "z \<in> insert x A" 
522 
then show "z \<sqsubseteq> s" 

523 
proof 

524 
assume "z = x" then show ?thesis 

525 
by (simp add: least_Upper_above [OF least_s] L La) 

526 
next 

527 
assume "z \<in> A" 

528 
with L least_s least_a show ?thesis 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

529 
by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above) 
14693  530 
qed 
531 
next 

532 
fix y 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

533 
assume y: "y \<in> Upper L (insert x A)" 
14693  534 
show "s \<sqsubseteq> y" 
535 
proof (rule least_le [OF least_s], rule Upper_memI) 

536 
fix z 

537 
assume z: "z \<in> {a, x}" 

538 
then show "z \<sqsubseteq> y" 

539 
proof 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

540 
have y': "y \<in> Upper L A" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

541 
apply (rule subsetD [where A = "Upper L (insert x A)"]) 
23463  542 
apply (rule Upper_antimono) 
543 
apply blast 

544 
apply (rule y) 

14693  545 
done 
546 
assume "z = a" 

547 
with y' least_a show ?thesis by (fast dest: least_le) 

548 
next 

549 
assume "z \<in> {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *) 

550 
with y L show ?thesis by blast 

551 
qed 

23350  552 
qed (rule Upper_closed [THEN subsetD, OF y]) 
14693  553 
next 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

554 
from L show "insert x A \<subseteq> carrier L" by simp 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

555 
from least_s show "s \<in> carrier L" by simp 
14551  556 
qed 
23350  557 
qed (rule P) 
14551  558 
qed 
559 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

560 
lemma (in weak_upper_semilattice) finite_sup_least: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

561 
"[ finite A; A \<subseteq> carrier L; A ~= {} ] ==> least L (\<Squnion>A) (Upper L A)" 
22265  562 
proof (induct set: finite) 
14693  563 
case empty 
564 
then show ?case by simp 

14551  565 
next 
15328  566 
case (insert x A) 
14551  567 
show ?case 
568 
proof (cases "A = {}") 

569 
case True 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

570 
with insert show ?thesis 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

571 
by simp (simp add: least_cong [OF weak_sup_of_singleton] 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

572 
sup_of_singleton_closed sup_of_singletonI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

573 
(* The above step is hairy; least_cong can make simp loop. 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

574 
Would want special version of simp to apply least_cong. *) 
14551  575 
next 
576 
case False 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

577 
with insert have "least L (\<Squnion>A) (Upper L A)" by simp 
14693  578 
with _ show ?thesis 
579 
by (rule sup_insertI) (simp_all add: insert [simplified]) 

14551  580 
qed 
581 
qed 

582 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

583 
lemma (in weak_upper_semilattice) finite_sup_insertI: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

584 
assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

585 
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" 
14551  586 
shows "P (\<Squnion> (insert x A))" 
587 
proof (cases "A = {}") 

588 
case True with P and xA show ?thesis 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

589 
by (simp add: finite_sup_least) 
14551  590 
next 
591 
case False with P and xA show ?thesis 

592 
by (simp add: sup_insertI finite_sup_least) 

593 
qed 

594 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

595 
lemma (in weak_upper_semilattice) finite_sup_closed [simp]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

596 
"[ finite A; A \<subseteq> carrier L; A ~= {} ] ==> \<Squnion>A \<in> carrier L" 
22265  597 
proof (induct set: finite) 
14551  598 
case empty then show ?case by simp 
599 
next 

15328  600 
case insert then show ?case 
14693  601 
by  (rule finite_sup_insertI, simp_all) 
14551  602 
qed 
603 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

604 
lemma (in weak_upper_semilattice) join_left: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

605 
"[ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqsubseteq> x \<squnion> y" 
14693  606 
by (rule joinI [folded join_def]) (blast dest: least_mem) 
14551  607 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

608 
lemma (in weak_upper_semilattice) join_right: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

609 
"[ x \<in> carrier L; y \<in> carrier L ] ==> y \<sqsubseteq> x \<squnion> y" 
14693  610 
by (rule joinI [folded join_def]) (blast dest: least_mem) 
14551  611 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

612 
lemma (in weak_upper_semilattice) sup_of_two_least: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

613 
"[ x \<in> carrier L; y \<in> carrier L ] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})" 
14551  614 
proof (unfold sup_def) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

615 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

616 
with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

617 
with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

618 
by (fast intro: someI2 weak_least_unique) (* blast fails *) 
14551  619 
qed 
620 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

621 
lemma (in weak_upper_semilattice) join_le: 
14693  622 
assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" 
23350  623 
and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L" 
14551  624 
shows "x \<squnion> y \<sqsubseteq> z" 
23350  625 
proof (rule joinI [OF _ x y]) 
14551  626 
fix s 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

627 
assume "least L s (Upper L {x, y})" 
23350  628 
with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI) 
14551  629 
qed 
14693  630 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

631 
lemma (in weak_upper_semilattice) weak_join_assoc_lemma: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

632 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

633 
shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}" 
14551  634 
proof (rule finite_sup_insertI) 
14651  635 
 {* The textbook argument in Jacobson I, p 457 *} 
14551  636 
fix s 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

637 
assume sup: "least L s (Upper L {x, y, z})" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

638 
show "x \<squnion> (y \<squnion> z) .= s" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

639 
proof (rule weak_le_anti_sym) 
14551  640 
from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s" 
641 
by (fastsimp intro!: join_le elim: least_Upper_above) 

642 
next 

643 
from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)" 

644 
by (erule_tac least_le) 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

645 
(blast intro!: Upper_memI intro: le_trans join_left join_right join_closed) 
27700  646 
qed (simp_all add: L least_closed [OF sup]) 
14551  647 
qed (simp_all add: L) 
648 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

649 
text {* Commutativity holds for @{text "="}. *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

650 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

651 
lemma join_comm: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

652 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

653 
shows "x \<squnion> y = y \<squnion> x" 
14551  654 
by (unfold join_def) (simp add: insert_commute) 
655 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

656 
lemma (in weak_upper_semilattice) weak_join_assoc: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

657 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

658 
shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)" 
14551  659 
proof  
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

660 
(* FIXME: could be simplified by improved simp: uniform use of .=, 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

661 
omit [symmetric] in last step. *) 
14551  662 
have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

663 
also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma) 
14693  664 
also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

665 
also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

666 
finally show ?thesis by (simp add: L) 
14551  667 
qed 
668 

14693  669 

14551  670 
subsubsection {* Infimum *} 
671 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

672 
lemma (in weak_lower_semilattice) meetI: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

673 
"[ !!i. greatest L i (Lower L {x, y}) ==> P i; 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

674 
x \<in> carrier L; y \<in> carrier L ] 
14551  675 
==> P (x \<sqinter> y)" 
676 
proof (unfold meet_def inf_def) 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

677 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

678 
and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

679 
with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

680 
with L show "P (SOME g. greatest L g (Lower L {x, y}))" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

681 
by (fast intro: someI2 weak_greatest_unique P) 
14551  682 
qed 
683 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

684 
lemma (in weak_lower_semilattice) meet_closed [simp]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

685 
"[ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqinter> y \<in> carrier L" 
27700  686 
by (rule meetI) (rule greatest_closed) 
14551  687 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

688 
lemma (in weak_lower_semilattice) meet_cong_l: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

689 
assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

690 
and xx': "x .= x'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

691 
shows "x \<sqinter> y .= x' \<sqinter> y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

692 
proof (rule meetI, rule meetI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

693 
fix a b 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

694 
from xx' carr 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

695 
have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

696 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

697 
assume greatesta: "greatest L a (Lower L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

698 
assume "greatest L b (Lower L {x', y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

699 
with carr 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

700 
have greatestb: "greatest L b (Lower L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

701 
by (simp add: greatest_Lower_cong_r[OF _ _ seq]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

702 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

703 
from greatesta greatestb 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

704 
show "a .= b" by (rule weak_greatest_unique) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

705 
qed (rule carr)+ 
14551  706 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

707 
lemma (in weak_lower_semilattice) meet_cong_r: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

708 
assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

709 
and yy': "y .= y'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

710 
shows "x \<sqinter> y .= x \<sqinter> y'" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

711 
proof (rule meetI, rule meetI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

712 
fix a b 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

713 
have "{x, y} = {y, x}" by fast 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

714 
also from carr yy' 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

715 
have "{y, x} {.=} {y', x}" by (intro set_eq_pairI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

716 
also have "{y', x} = {x, y'}" by fast 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

717 
finally 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

718 
have seq: "{x, y} {.=} {x, y'}" . 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

719 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

720 
assume greatesta: "greatest L a (Lower L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

721 
assume "greatest L b (Lower L {x, y'})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

722 
with carr 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

723 
have greatestb: "greatest L b (Lower L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

724 
by (simp add: greatest_Lower_cong_r[OF _ _ seq]) 
14551  725 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

726 
from greatesta greatestb 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

727 
show "a .= b" by (rule weak_greatest_unique) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

728 
qed (rule carr)+ 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

729 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

730 
lemma (in weak_partial_order) inf_of_singletonI: (* only reflexivity needed ? *) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

731 
"x \<in> carrier L ==> greatest L x (Lower L {x})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

732 
by (rule greatest_LowerI) auto 
14551  733 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

734 
lemma (in weak_partial_order) weak_inf_of_singleton [simp]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

735 
"x \<in> carrier L ==> \<Sqinter>{x} .= x" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

736 
unfolding inf_def 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

737 
by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

738 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

739 
lemma (in weak_partial_order) inf_of_singleton_closed: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

740 
"x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

741 
unfolding inf_def 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

742 
by (rule someI2) (auto intro: inf_of_singletonI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

743 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

744 
text {* Condition on @{text A}: infimum exists. *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

745 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

746 
lemma (in weak_lower_semilattice) inf_insertI: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

747 
"[ !!i. greatest L i (Lower L (insert x A)) ==> P i; 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

748 
greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L ] 
14693  749 
==> P (\<Sqinter>(insert x A))" 
14551  750 
proof (unfold inf_def) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

751 
assume L: "x \<in> carrier L" "A \<subseteq> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

752 
and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

753 
and greatest_a: "greatest L a (Lower L A)" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

754 
from L greatest_a have La: "a \<in> carrier L" by simp 
14551  755 
from L inf_of_two_exists greatest_a 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

756 
obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

757 
show "P (SOME g. greatest L g (Lower L (insert x A)))" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

758 
proof (rule someI2) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

759 
show "greatest L i (Lower L (insert x A))" 
14551  760 
proof (rule greatest_LowerI) 
761 
fix z 

14693  762 
assume "z \<in> insert x A" 
763 
then show "i \<sqsubseteq> z" 

764 
proof 

765 
assume "z = x" then show ?thesis 

27700  766 
by (simp add: greatest_Lower_below [OF greatest_i] L La) 
14693  767 
next 
768 
assume "z \<in> A" 

769 
with L greatest_i greatest_a show ?thesis 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

770 
by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below) 
14693  771 
qed 
772 
next 

773 
fix y 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

774 
assume y: "y \<in> Lower L (insert x A)" 
14693  775 
show "y \<sqsubseteq> i" 
776 
proof (rule greatest_le [OF greatest_i], rule Lower_memI) 

777 
fix z 

778 
assume z: "z \<in> {a, x}" 

779 
then show "y \<sqsubseteq> z" 

780 
proof 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

781 
have y': "y \<in> Lower L A" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

782 
apply (rule subsetD [where A = "Lower L (insert x A)"]) 
23463  783 
apply (rule Lower_antimono) 
784 
apply blast 

785 
apply (rule y) 

14693  786 
done 
787 
assume "z = a" 

788 
with y' greatest_a show ?thesis by (fast dest: greatest_le) 

789 
next 

790 
assume "z \<in> {x}" 

791 
with y L show ?thesis by blast 

792 
qed 

23350  793 
qed (rule Lower_closed [THEN subsetD, OF y]) 
14693  794 
next 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

795 
from L show "insert x A \<subseteq> carrier L" by simp 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

796 
from greatest_i show "i \<in> carrier L" by simp 
14551  797 
qed 
23350  798 
qed (rule P) 
14551  799 
qed 
800 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

801 
lemma (in weak_lower_semilattice) finite_inf_greatest: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

802 
"[ finite A; A \<subseteq> carrier L; A ~= {} ] ==> greatest L (\<Sqinter>A) (Lower L A)" 
22265  803 
proof (induct set: finite) 
14551  804 
case empty then show ?case by simp 
805 
next 

15328  806 
case (insert x A) 
14551  807 
show ?case 
808 
proof (cases "A = {}") 

809 
case True 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

810 
with insert show ?thesis 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

811 
by simp (simp add: greatest_cong [OF weak_inf_of_singleton] 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

812 
inf_of_singleton_closed inf_of_singletonI) 
14551  813 
next 
814 
case False 

815 
from insert show ?thesis 

816 
proof (rule_tac inf_insertI) 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

817 
from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp 
14551  818 
qed simp_all 
819 
qed 

820 
qed 

821 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

822 
lemma (in weak_lower_semilattice) finite_inf_insertI: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

823 
assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

824 
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" 
14551  825 
shows "P (\<Sqinter> (insert x A))" 
826 
proof (cases "A = {}") 

827 
case True with P and xA show ?thesis 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

828 
by (simp add: finite_inf_greatest) 
14551  829 
next 
830 
case False with P and xA show ?thesis 

831 
by (simp add: inf_insertI finite_inf_greatest) 

832 
qed 

833 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

834 
lemma (in weak_lower_semilattice) finite_inf_closed [simp]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

835 
"[ finite A; A \<subseteq> carrier L; A ~= {} ] ==> \<Sqinter>A \<in> carrier L" 
22265  836 
proof (induct set: finite) 
14551  837 
case empty then show ?case by simp 
838 
next 

15328  839 
case insert then show ?case 
14551  840 
by (rule_tac finite_inf_insertI) (simp_all) 
841 
qed 

842 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

843 
lemma (in weak_lower_semilattice) meet_left: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

844 
"[ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqinter> y \<sqsubseteq> x" 
14693  845 
by (rule meetI [folded meet_def]) (blast dest: greatest_mem) 
14551  846 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

847 
lemma (in weak_lower_semilattice) meet_right: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

848 
"[ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqinter> y \<sqsubseteq> y" 
14693  849 
by (rule meetI [folded meet_def]) (blast dest: greatest_mem) 
14551  850 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

851 
lemma (in weak_lower_semilattice) inf_of_two_greatest: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

852 
"[ x \<in> carrier L; y \<in> carrier L ] ==> 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

853 
greatest L (\<Sqinter> {x, y}) (Lower L {x, y})" 
14551  854 
proof (unfold inf_def) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

855 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

856 
with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast 
14551  857 
with L 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

858 
show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

859 
by (fast intro: someI2 weak_greatest_unique) (* blast fails *) 
14551  860 
qed 
861 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

862 
lemma (in weak_lower_semilattice) meet_le: 
14693  863 
assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" 
23350  864 
and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L" 
14551  865 
shows "z \<sqsubseteq> x \<sqinter> y" 
23350  866 
proof (rule meetI [OF _ x y]) 
14551  867 
fix i 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

868 
assume "greatest L i (Lower L {x, y})" 
23350  869 
with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI) 
14551  870 
qed 
14693  871 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

872 
lemma (in weak_lower_semilattice) weak_meet_assoc_lemma: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

873 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

874 
shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}" 
14551  875 
proof (rule finite_inf_insertI) 
876 
txt {* The textbook argument in Jacobson I, p 457 *} 

877 
fix i 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

878 
assume inf: "greatest L i (Lower L {x, y, z})" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

879 
show "x \<sqinter> (y \<sqinter> z) .= i" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

880 
proof (rule weak_le_anti_sym) 
14551  881 
from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" 
27700  882 
by (fastsimp intro!: meet_le elim: greatest_Lower_below) 
14551  883 
next 
884 
from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i" 

885 
by (erule_tac greatest_le) 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

886 
(blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed) 
27700  887 
qed (simp_all add: L greatest_closed [OF inf]) 
14551  888 
qed (simp_all add: L) 
889 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

890 
lemma meet_comm: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

891 
fixes L (structure) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

892 
shows "x \<sqinter> y = y \<sqinter> x" 
14551  893 
by (unfold meet_def) (simp add: insert_commute) 
894 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

895 
lemma (in weak_lower_semilattice) weak_meet_assoc: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

896 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

897 
shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)" 
14551  898 
proof  
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

899 
(* FIXME: improved simp, see weak_join_assoc above *) 
14551  900 
have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

901 
also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma) 
14551  902 
also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

903 
also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

904 
finally show ?thesis by (simp add: L) 
14551  905 
qed 
906 

14693  907 

14551  908 
subsection {* Total Orders *} 
909 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

910 
locale weak_total_order = weak_partial_order + 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

911 
assumes total: "[ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqsubseteq> y  y \<sqsubseteq> x" 
14551  912 

913 
text {* Introduction rule: the usual definition of total order *} 

914 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

915 
lemma (in weak_partial_order) weak_total_orderI: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

916 
assumes total: "!!x y. [ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqsubseteq> y  y \<sqsubseteq> x" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

917 
shows "weak_total_order L" 
28823  918 
proof qed (rule total) 
24087
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

919 

eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

920 
text {* Total orders are lattices. *} 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

921 

29237  922 
sublocale weak_total_order < weak_lattice 
28823  923 
proof 
24087
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

924 
fix x y 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

925 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

926 
show "EX s. least L s (Upper L {x, y})" 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

927 
proof  
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

928 
note total L 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

929 
moreover 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

930 
{ 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

931 
assume "x \<sqsubseteq> y" 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

932 
with L have "least L y (Upper L {x, y})" 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

933 
by (rule_tac least_UpperI) auto 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

934 
} 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

935 
moreover 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

936 
{ 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

937 
assume "y \<sqsubseteq> x" 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

938 
with L have "least L x (Upper L {x, y})" 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

939 
by (rule_tac least_UpperI) auto 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

940 
} 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

941 
ultimately show ?thesis by blast 
14551  942 
qed 
24087
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

943 
next 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

944 
fix x y 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

945 
assume L: "x \<in> carrier L" "y \<in> carrier L" 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

946 
show "EX i. greatest L i (Lower L {x, y})" 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

947 
proof  
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

948 
note total L 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

949 
moreover 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

950 
{ 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

951 
assume "y \<sqsubseteq> x" 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

952 
with L have "greatest L y (Lower L {x, y})" 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

953 
by (rule_tac greatest_LowerI) auto 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

954 
} 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

955 
moreover 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

956 
{ 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

957 
assume "x \<sqsubseteq> y" 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

958 
with L have "greatest L x (Lower L {x, y})" 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

959 
by (rule_tac greatest_LowerI) auto 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

960 
} 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

961 
ultimately show ?thesis by blast 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

962 
qed 
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

963 
qed 
14551  964 

14693  965 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

966 
subsection {* Complete Lattices *} 
14551  967 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

968 
locale weak_complete_lattice = weak_lattice + 
14551  969 
assumes sup_exists: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

970 
"[ A \<subseteq> carrier L ] ==> EX s. least L s (Upper L A)" 
14551  971 
and inf_exists: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

972 
"[ A \<subseteq> carrier L ] ==> EX i. greatest L i (Lower L A)" 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

973 

14551  974 
text {* Introduction rule: the usual definition of complete lattice *} 
975 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

976 
lemma (in weak_partial_order) weak_complete_latticeI: 
14551  977 
assumes sup_exists: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

978 
"!!A. [ A \<subseteq> carrier L ] ==> EX s. least L s (Upper L A)" 
14551  979 
and inf_exists: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

980 
"!!A. [ A \<subseteq> carrier L ] ==> EX i. greatest L i (Lower L A)" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

981 
shows "weak_complete_lattice L" 
28823  982 
proof qed (auto intro: sup_exists inf_exists) 
14551  983 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

984 
constdefs (structure L) 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

985 
top :: "_ => 'a" ("\<top>\<index>") 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

986 
"\<top> == sup L (carrier L)" 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

987 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

988 
bottom :: "_ => 'a" ("\<bottom>\<index>") 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

989 
"\<bottom> == inf L (carrier L)" 
14551  990 

991 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

992 
lemma (in weak_complete_lattice) supI: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

993 
"[ !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L ] 
14651  994 
==> P (\<Squnion>A)" 
14551  995 
proof (unfold sup_def) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

996 
assume L: "A \<subseteq> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

997 
and P: "!!l. least L l (Upper L A) ==> P l" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

998 
with sup_exists obtain s where "least L s (Upper L A)" by blast 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

999 
with L show "P (SOME l. least L l (Upper L A))" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1000 
by (fast intro: someI2 weak_least_unique P) 
14551  1001 
qed 
1002 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1003 
lemma (in weak_complete_lattice) sup_closed [simp]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1004 
"A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L" 
14551  1005 
by (rule supI) simp_all 
1006 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1007 
lemma (in weak_complete_lattice) top_closed [simp, intro]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1008 
"\<top> \<in> carrier L" 
14551  1009 
by (unfold top_def) simp 
1010 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1011 
lemma (in weak_complete_lattice) infI: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1012 
"[ !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L ] 
14693  1013 
==> P (\<Sqinter>A)" 
14551  1014 
proof (unfold inf_def) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1015 
assume L: "A \<subseteq> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1016 
and P: "!!l. greatest L l (Lower L A) ==> P l" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1017 
with inf_exists obtain s where "greatest L s (Lower L A)" by blast 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1018 
with L show "P (SOME l. greatest L l (Lower L A))" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1019 
by (fast intro: someI2 weak_greatest_unique P) 
14551  1020 
qed 
1021 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1022 
lemma (in weak_complete_lattice) inf_closed [simp]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1023 
"A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L" 
14551  1024 
by (rule infI) simp_all 
1025 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1026 
lemma (in weak_complete_lattice) bottom_closed [simp, intro]: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1027 
"\<bottom> \<in> carrier L" 
14551  1028 
by (unfold bottom_def) simp 
1029 

1030 
text {* Jacobson: Theorem 8.1 *} 

1031 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1032 
lemma Lower_empty [simp]: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1033 
"Lower L {} = carrier L" 
14551  1034 
by (unfold Lower_def) simp 
1035 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1036 
lemma Upper_empty [simp]: 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1037 
"Upper L {} = carrier L" 
14551  1038 
by (unfold Upper_def) simp 
1039 

27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1040 
theorem (in weak_partial_order) weak_complete_lattice_criterion1: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1041 
assumes top_exists: "EX g. greatest L g (carrier L)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1042 
and inf_exists: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1043 
"!!A. [ A \<subseteq> carrier L; A ~= {} ] ==> EX i. greatest L i (Lower L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1044 
shows "weak_complete_lattice L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1045 
proof (rule weak_complete_latticeI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1046 
from top_exists obtain top where top: "greatest L top (carrier L)" .. 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1047 
fix A 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1048 
assume L: "A \<subseteq> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1049 
let ?B = "Upper L A" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1050 
from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1051 
then have B_non_empty: "?B ~= {}" by fast 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1052 
have B_L: "?B \<subseteq> carrier L" by simp 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1053 
from inf_exists [OF B_L B_non_empty] 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1054 
obtain b where b_inf_B: "greatest L b (Lower L ?B)" .. 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1055 
have "least L b (Upper L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1056 
apply (rule least_UpperI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1057 
apply (rule greatest_le [where A = "Lower L ?B"]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1058 
apply (rule b_inf_B) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1059 
apply (rule Lower_memI) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1060 
apply (erule Upper_memD [THEN conjunct1]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1061 
apply assumption 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1062 
apply (rule L) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1063 
apply (fast intro: L [THEN subsetD]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1064 
apply (erule greatest_Lower_below [OF b_inf_B]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1065 
apply simp 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1066 
apply (rule L) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1067 
apply (rule greatest_closed [OF b_inf_B]) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1068 
done 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1069 
then show "EX s. least L s (Upper L A)" .. 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1070 
next 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1071 
fix A 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1072 
assume L: "A \<subseteq> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1073 
show "EX i. greatest L i (Lower L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1074 
proof (cases "A = {}") 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1075 
case True then show ?thesis 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1076 
by (simp add: top_exists) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1077 
next 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1078 
case False with L show ?thesis 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1079 
by (rule inf_exists) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1080 
qed 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1081 
qed 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1082 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1083 
(* TODO: prove dual version *) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1084 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1085 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1086 
subsection {* Orders and Lattices where @{text eq} is the Equality *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1087 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1088 
locale partial_order = weak_partial_order + 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1089 
assumes eq_is_equal: "op .= = op =" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1090 
begin 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1091 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1092 
declare weak_le_anti_sym [rule del] 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1093 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1094 
lemma le_anti_sym [intro]: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1095 
"[ x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L ] ==> x = y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1096 
using weak_le_anti_sym unfolding eq_is_equal . 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1097 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1098 
lemma lless_eq: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1099 
"x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1100 
unfolding lless_def by (simp add: eq_is_equal) 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1101 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1102 
lemma lless_asym: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1103 
assumes "a \<in> carrier L" "b \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1104 
and "a \<sqsubset> b" "b \<sqsubset> a" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1105 
shows "P" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1106 
using assms unfolding lless_eq by auto 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1107 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1108 
end 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1109 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1110 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1111 
text {* Least and greatest, as predicate *} 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1112 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1113 
lemma (in partial_order) least_unique: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1114 
"[ least L x A; least L y A ] ==> x = y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1115 
using weak_least_unique unfolding eq_is_equal . 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1116 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1117 
lemma (in partial_order) greatest_unique: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1118 
"[ greatest L x A; greatest L y A ] ==> x = y" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1119 
using weak_greatest_unique unfolding eq_is_equal . 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1120 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1121 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1122 
text {* Lattices *} 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1123 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1124 
locale upper_semilattice = partial_order + 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1125 
assumes sup_of_two_exists: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1126 
"[ x \<in> carrier L; y \<in> carrier L ] ==> EX s. least L s (Upper L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1127 

29237  1128 
sublocale upper_semilattice < weak_upper_semilattice 
28823  1129 
proof qed (rule sup_of_two_exists) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1130 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1131 
locale lower_semilattice = partial_order + 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1132 
assumes inf_of_two_exists: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1133 
"[ x \<in> carrier L; y \<in> carrier L ] ==> EX s. greatest L s (Lower L {x, y})" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1134 

29237  1135 
sublocale lower_semilattice < weak_lower_semilattice 
28823  1136 
proof qed (rule inf_of_two_exists) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1137 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1138 
locale lattice = upper_semilattice + lower_semilattice 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1139 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1140 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1141 
text {* Supremum *} 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1142 

27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

1143 
declare (in partial_order) weak_sup_of_singleton [simp del] 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1144 

27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

1145 
lemma (in partial_order) sup_of_singleton [simp]: 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1146 
"x \<in> carrier L ==> \<Squnion>{x} = x" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1147 
using weak_sup_of_singleton unfolding eq_is_equal . 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1148 

27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

1149 
lemma (in upper_semilattice) join_assoc_lemma: 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1150 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1151 
shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}" 
27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

1152 
using weak_join_assoc_lemma L unfolding eq_is_equal . 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1153 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1154 
lemma (in upper_semilattice) join_assoc: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1155 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1156 
shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" 
27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

1157 
using weak_join_assoc L unfolding eq_is_equal . 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1158 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1159 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1160 
text {* Infimum *} 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1161 

27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

1162 
declare (in partial_order) weak_inf_of_singleton [simp del] 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1163 

27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

1164 
lemma (in partial_order) inf_of_singleton [simp]: 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1165 
"x \<in> carrier L ==> \<Sqinter>{x} = x" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1166 
using weak_inf_of_singleton unfolding eq_is_equal . 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1167 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1168 
text {* Condition on @{text A}: infimum exists. *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1169 

27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

1170 
lemma (in lower_semilattice) meet_assoc_lemma: 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1171 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1172 
shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}" 
27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

1173 
using weak_meet_assoc_lemma L unfolding eq_is_equal . 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1174 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1175 
lemma (in lower_semilattice) meet_assoc: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1176 
assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1177 
shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" 
27714
27b4d7c01f8b
Tuned (for the sake of a meaningless log entry).
ballarin
parents:
27713
diff
changeset

1178 
using weak_meet_assoc L unfolding eq_is_equal . 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1179 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1180 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1181 
text {* Total Orders *} 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1182 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1183 
locale total_order = partial_order + 
28823  1184 
assumes total_order_total: "[ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqsubseteq> y  y \<sqsubseteq> x" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1185 

29237  1186 
sublocale total_order < weak_total_order 
28823  1187 
proof qed (rule total_order_total) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1188 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1189 
text {* Introduction rule: the usual definition of total order *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1190 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1191 
lemma (in partial_order) total_orderI: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1192 
assumes total: "!!x y. [ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqsubseteq> y  y \<sqsubseteq> x" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1193 
shows "total_order L" 
28823  1194 
proof qed (rule total) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1195 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1196 
text {* Total orders are lattices. *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1197 

29237  1198 
sublocale total_order < lattice 
28823  1199 
proof qed (auto intro: sup_of_two_exists inf_of_two_exists) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1200 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1201 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27714
diff
changeset

1202 
text {* Complete lattices *} 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1203 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1204 
locale complete_lattice = lattice + 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1205 
assumes sup_exists: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1206 
"[ A \<subseteq> carrier L ] ==> EX s. least L s (Upper L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1207 
and inf_exists: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1208 
"[ A \<subseteq> carrier L ] ==> EX i. greatest L i (Lower L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1209 

29237  1210 
sublocale complete_lattice < weak_complete_lattice 
28823  1211 
proof qed (auto intro: sup_exists inf_exists) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1212 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1213 
text {* Introduction rule: the usual definition of complete lattice *} 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1214 

95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1215 
lemma (in partial_order) complete_latticeI: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1216 
assumes sup_exists: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1217 
"!!A. [ A \<subseteq> carrier L ] ==> EX s. least L s (Upper L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1218 
and inf_exists: 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1219 
"!!A. [ A \<subseteq> carrier L ] ==> EX i. greatest L i (Lower L A)" 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1220 
shows "complete_lattice L" 
28823  1221 
proof qed (auto intro: sup_exists inf_exists) 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1222 

14551  1223 
theorem (in partial_order) complete_lattice_criterion1: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1224 
assumes top_exists: "EX g. greatest L g (carrier L)" 
14551  1225 
and inf_exists: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1226 
"!!A. [ A \<subseteq> carrier L; A ~= {} ] ==> EX i. greatest L i (Lower L A)" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1227 
shows "complete_lattice L" 
14551  1228 
proof (rule complete_latticeI) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1229 
from top_exists obtain top where top: "greatest L top (carrier L)" .. 
14551  1230 
fix A 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1231 
assume L: "A \<subseteq> carrier L" 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1232 
let ?B = "Upper L A" 
14551  1233 
from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le) 
1234 
then have B_non_empty: "?B ~= {}" by fast 

22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1235 
have B_L: "?B \<subseteq> carrier L" by simp 
14551  1236 
from inf_exists [OF B_L B_non_empty] 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1237 
obtain b where b_inf_B: "greatest L b (Lower L ?B)" .. 
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1238 
have "least L b (Upper L A)" 
14551  1239 
apply (rule least_UpperI) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1240 
apply (rule greatest_le [where A = "Lower L ?B"]) 
14551  1241 
apply (rule b_inf_B) 
1242 
apply (rule Lower_memI) 
