author  wenzelm 
Sun, 21 Mar 2010 15:57:40 +0100  
changeset 35847  19f1f7066917 
parent 33657  a4179bf442d1 
child 35848  5443079512ea 
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" 
33657  21 
and weak_le_antisym [intro]: 
27713
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 

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

29 
lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50) 
35847  30 
where "x \<sqsubset>\<^bsub>L\<^esub> y == x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y" 
27713
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 

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

106 
Upper :: "[_, 'a set] => 'a set" 
35847  107 
where "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L > x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

108 

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

110 
Lower :: "[_, 'a set] => 'a set" 
35847  111 
where "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L > l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L" 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

112 

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

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

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

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

118 
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

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

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

122 
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

123 
"[ 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

124 
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

125 
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

126 

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

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

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

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

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

132 
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

133 
"[ !! 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

134 
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

135 

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

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

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

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

140 
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

141 
"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

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

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

144 
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

145 
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

146 
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

147 
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

148 
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

149 
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

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

151 
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

152 
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

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

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

155 
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

156 
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

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

158 

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

159 
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

160 
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

161 
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

162 
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

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

164 
apply rule 
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 
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

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

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

169 
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

170 
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

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

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

173 
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

174 
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

175 
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

176 
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

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

178 
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

179 

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

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

181 
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

182 
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

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

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

185 
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

186 
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

187 
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

188 

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

189 
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

190 
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

191 
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

192 
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

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

194 
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

195 

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

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

197 
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

198 
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

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

200 

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

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

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

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

206 
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

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

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

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

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

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

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

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

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

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

219 
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

220 
"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

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

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

223 
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

224 
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

225 
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

226 
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

227 
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

228 
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

229 
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

230 

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

231 
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

232 
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

233 
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

234 
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

235 
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

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

237 
apply safe 
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 
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

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

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

242 
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

243 
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

244 
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

245 
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

246 

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

247 
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

248 
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

249 
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

250 
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

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

252 

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

253 
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

254 
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

255 
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

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

257 
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

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

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

260 
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

261 
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

262 
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

263 
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

264 

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

265 
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

266 
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

267 
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

268 
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

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

270 
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

271 
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

272 
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

273 
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

274 
qed 
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 

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

277 
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

278 

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

280 
least :: "[_, 'a, 'a set] => bool" 
35847  281 
where "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

282 

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

284 
greatest :: "[_, 'a, 'a set] => bool" 
35847  285 
where "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

286 

30363
9b8d9b6ef803
proper local context for text with antiquotations;
wenzelm
parents:
29242
diff
changeset

287 
text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l 
9b8d9b6ef803
proper local context for text with antiquotations;
wenzelm
parents:
29242
diff
changeset

288 
.\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *} 
14551  289 

27700  290 
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

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

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

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

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

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

298 
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

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

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

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

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

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

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

307 
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

308 
"[ 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

309 
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

310 

30363
9b8d9b6ef803
proper local context for text with antiquotations;
wenzelm
parents:
29242
diff
changeset

311 
text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for 
9b8d9b6ef803
proper local context for text with antiquotations;
wenzelm
parents:
29242
diff
changeset

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

313 

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

314 
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

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

316 
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

317 
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

318 
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

319 
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

320 

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

321 
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

322 
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

323 
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

324 
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

325 
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

326 
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

327 

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

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

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

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

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

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

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

336 
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

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

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

341 
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

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

343 
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

344 
by (unfold least_def) blast 
14551  345 

27700  346 
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

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

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

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

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

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

354 
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

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

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

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

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

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

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

363 
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

364 
"[ 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

365 
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

366 
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

367 

30363
9b8d9b6ef803
proper local context for text with antiquotations;
wenzelm
parents:
29242
diff
changeset

368 
text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for 
9b8d9b6ef803
proper local context for text with antiquotations;
wenzelm
parents:
29242
diff
changeset

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

370 

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

371 
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

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

373 
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

374 
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

375 
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

376 
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

377 

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

378 
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

379 
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

380 
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

381 
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

382 
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

383 
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

384 

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

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

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

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

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

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

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

393 
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

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

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

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

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

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

403 
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

404 

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

406 
sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90) 
35847  407 
where "\<Squnion>\<^bsub>L\<^esub>A == SOME x. least L x (Upper L A)" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

408 

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

410 
inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90) 
35847  411 
where "\<Sqinter>\<^bsub>L\<^esub>A == SOME x. greatest L x (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

412 

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

414 
join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65) 
35847  415 
where "x \<squnion>\<^bsub>L\<^esub> y == \<Squnion>\<^bsub>L\<^esub>{x, y}" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

416 

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

418 
meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70) 
35847  419 
where "x \<sqinter>\<^bsub>L\<^esub> y == \<Sqinter>\<^bsub>L\<^esub>{x, y}" 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

420 

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

421 

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

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

423 

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

424 
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

425 
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

426 
"[ 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

427 

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

428 
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

429 
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

430 
"[ 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

431 

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

432 
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

433 

14666  434 

14551  435 
subsubsection {* Supremum *} 
436 

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

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

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

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

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

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

443 
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

444 
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

445 
by (fast intro: someI2 P) 
14551  446 
qed 
447 

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

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

449 
"[ x \<in> carrier L; y \<in> carrier L ] ==> x \<squnion> y \<in> carrier L" 
27700  450 
by (rule joinI) (rule least_closed) 
14551  451 

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

452 
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

453 
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

454 
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

455 
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

456 
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

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

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

459 
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

460 

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

461 
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

462 
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

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

464 
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

465 
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

466 

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

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

468 
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

469 
qed (rule carr)+ 
14551  470 

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

471 
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

472 
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

473 
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

474 
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

475 
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

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

477 
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

478 
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

479 
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

480 
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

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

482 
have seq: "{x, y} {.=} {x, y'}" . 
14551  483 

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

484 
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

485 
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

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

487 
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

488 
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

489 

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

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

491 
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

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

493 

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

494 
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

495 
"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

496 
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

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) 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

499 
"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

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: 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

502 

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

503 
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

504 
"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

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

506 
by (rule someI2) (auto intro: sup_of_singletonI) 
14666  507 

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

14551  509 

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

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

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

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

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

516 
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

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

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

520 
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

521 
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

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

523 
show "least L s (Upper L (insert x A))" 
14551  524 
proof (rule least_UpperI) 
525 
fix z 

14693  526 
assume "z \<in> insert x A" 
527 
then show "z \<sqsubseteq> s" 

528 
proof 

529 
assume "z = x" then show ?thesis 

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

531 
next 

532 
assume "z \<in> A" 

533 
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

534 
by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above) 
14693  535 
qed 
536 
next 

537 
fix y 

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

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

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

541 
fix z 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

542 
assume z: "z \<in> {a, x}" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

543 
then show "z \<sqsubseteq> y" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

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

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

546 
apply (rule subsetD [where A = "Upper L (insert x A)"]) 
23463  547 
apply (rule Upper_antimono) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

548 
apply blast 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

549 
apply (rule y) 
14693  550 
done 
551 
assume "z = a" 

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

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

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

554 
assume "z \<in> {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *) 
14693  555 
with y L show ?thesis by blast 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

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

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

560 
from least_s show "s \<in> carrier L" by simp 
14551  561 
qed 
23350  562 
qed (rule P) 
14551  563 
qed 
564 

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

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

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

14551  570 
next 
15328  571 
case (insert x A) 
14551  572 
show ?case 
573 
proof (cases "A = {}") 

574 
case True 

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

575 
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

576 
by simp (simp add: least_cong [OF weak_sup_of_singleton] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

577 
sup_of_singleton_closed sup_of_singletonI) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

578 
(* The above step is hairy; least_cong can make simp loop. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

579 
Would want special version of simp to apply least_cong. *) 
14551  580 
next 
581 
case False 

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

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

14551  585 
qed 
586 
qed 

587 

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

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

589 
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

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

593 
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

594 
by (simp add: finite_sup_least) 
14551  595 
next 
596 
case False with P and xA show ?thesis 

597 
by (simp add: sup_insertI finite_sup_least) 

598 
qed 

599 

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

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

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

15328  605 
case insert then show ?case 
14693  606 
by  (rule finite_sup_insertI, simp_all) 
14551  607 
qed 
608 

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

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

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

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

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

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

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

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

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

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

621 
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

622 
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

623 
by (fast intro: someI2 weak_least_unique) (* blast fails *) 
14551  624 
qed 
625 

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

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

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

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

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

637 
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

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

642 
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

643 
show "x \<squnion> (y \<squnion> z) .= s" 
33657  644 
proof (rule weak_le_antisym) 
14551  645 
from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s" 
646 
by (fastsimp intro!: join_le elim: least_Upper_above) 

647 
next 

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

649 
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

650 
(blast intro!: Upper_memI intro: le_trans join_left join_right join_closed) 
27700  651 
qed (simp_all add: L least_closed [OF sup]) 
14551  652 
qed (simp_all add: L) 
653 

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

654 
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

655 

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

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

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

658 
shows "x \<squnion> y = y \<squnion> x" 
14551  659 
by (unfold join_def) (simp add: insert_commute) 
660 

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

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

662 
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

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

665 
(* 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

666 
omit [symmetric] in last step. *) 
14551  667 
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

668 
also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma) 
14693  669 
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

670 
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

671 
finally show ?thesis by (simp add: L) 
14551  672 
qed 
673 

14693  674 

14551  675 
subsubsection {* Infimum *} 
676 

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

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

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

679 
x \<in> carrier L; y \<in> carrier L ] 
14551  680 
==> P (x \<sqinter> y)" 
681 
proof (unfold meet_def inf_def) 

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

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

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

684 
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

685 
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

686 
by (fast intro: someI2 weak_greatest_unique P) 
14551  687 
qed 
688 

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

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

690 
"[ x \<in> carrier L; y \<in> carrier L ] ==> x \<sqinter> y \<in> carrier L" 
27700  691 
by (rule meetI) (rule greatest_closed) 
14551  692 

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

693 
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

694 
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

695 
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

696 
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

697 
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

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

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

700 
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

701 

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

702 
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

703 
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

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

705 
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

706 
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

707 

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

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

709 
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

710 
qed (rule carr)+ 
14551  711 

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

712 
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

713 
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

714 
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

715 
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

716 
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

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

718 
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

719 
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

720 
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

721 
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

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

723 
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

724 

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

725 
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

726 
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

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

728 
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

729 
by (simp add: greatest_Lower_cong_r[OF _ _ seq]) 
14551  730 

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

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

732 
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

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

734 

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

735 
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

736 
"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

737 
by (rule greatest_LowerI) auto 
14551  738 

27713
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) 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

740 
"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

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: 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

743 

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

744 
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

745 
"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

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

747 
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

748 

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

749 
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

750 

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

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

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

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

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

757 
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

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

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

761 
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

762 
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

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

764 
show "greatest L i (Lower L (insert x A))" 
14551  765 
proof (rule greatest_LowerI) 
766 
fix z 

14693  767 
assume "z \<in> insert x A" 
768 
then show "i \<sqsubseteq> z" 

769 
proof 

770 
assume "z = x" then show ?thesis 

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

774 
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

775 
by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below) 
14693  776 
qed 
777 
next 

778 
fix y 

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

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

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

782 
fix z 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

783 
assume z: "z \<in> {a, x}" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

784 
then show "y \<sqsubseteq> z" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

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

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

787 
apply (rule subsetD [where A = "Lower L (insert x A)"]) 
23463  788 
apply (rule Lower_antimono) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

789 
apply blast 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

790 
apply (rule y) 
14693  791 
done 
792 
assume "z = a" 

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

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

794 
next 
14693  795 
assume "z \<in> {x}" 
796 
with y L show ?thesis by blast 

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

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

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

801 
from greatest_i show "i \<in> carrier L" by simp 
14551  802 
qed 
23350  803 
qed (rule P) 
14551  804 
qed 
805 

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

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

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

15328  811 
case (insert x A) 
14551  812 
show ?case 
813 
proof (cases "A = {}") 

814 
case True 

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

815 
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

816 
by simp (simp add: greatest_cong [OF weak_inf_of_singleton] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30363
diff
changeset

817 
inf_of_singleton_closed inf_of_singletonI) 
14551  818 
next 
819 
case False 

820 
from insert show ?thesis 

821 
proof (rule_tac inf_insertI) 

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

822 
from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp 
14551  823 
qed simp_all 
824 
qed 

825 
qed 

826 

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

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

828 
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

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

832 
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

833 
by (simp add: finite_inf_greatest) 
14551  834 
next 
835 
case False with P and xA show ?thesis 

836 
by (simp add: inf_insertI finite_inf_greatest) 

837 
qed 

838 

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

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

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

15328  844 
case insert then show ?case 
14551  845 
by (rule_tac finite_inf_insertI) (simp_all) 
846 
qed 

847 

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

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

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

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

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

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

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

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

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

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

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

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

863 
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

864 
by (fast intro: someI2 weak_greatest_unique) (* blast fails *) 
14551  865 
qed 
866 

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

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

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

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

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

878 
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

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

882 
fix i 

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

883 
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

884 
show "x \<sqinter> (y \<sqinter> z) .= i" 
33657  885 
proof (rule weak_le_antisym) 
14551  886 
from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" 
27700  887 
by (fastsimp intro!: meet_le elim: greatest_Lower_below) 
14551  888 
next 
889 
from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i" 

890 
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

891 
(blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed) 
27700  892 
qed (simp_all add: L greatest_closed [OF inf]) 
14551  893 
qed (simp_all add: L) 
894 

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

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

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

897 
shows "x \<sqinter> y = y \<sqinter> x" 
14551  898 
by (unfold meet_def) (simp add: insert_commute) 
899 

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

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

901 
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

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

904 
(* FIXME: improved simp, see weak_join_assoc above *) 
14551  905 
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

906 
also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma) 
14551  907 
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

908 
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

909 
finally show ?thesis by (simp add: L) 
14551  910 
qed 
911 

14693  912 

14551  913 
subsection {* Total Orders *} 
914 

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

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

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

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

919 

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

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

921 
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

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

924 

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

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

926 

29242  927 
sublocale weak_total_order < weak: weak_lattice 
28823  928 
proof 
24087
eb025d149a34
Proper interpretation of total orders in lattices.
ballarin
parents:
23463
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

968 
qed 
14551  969 

14693  970 

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

971 
subsection {* Complete Lattices *} 
14551  972 

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

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

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

977 
"[ 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

978 

14551  979 
text {* Introduction rule: the usual definition of complete lattice *} 
980 

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

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

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

985 
"!!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

986 
shows "weak_complete_lattice L" 
28823  987 
proof qed (auto intro: sup_exists inf_exists) 
14551  988 

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

990 
top :: "_ => 'a" ("\<top>\<index>") 
35847  991 
where "\<top>\<^bsub>L\<^esub> == sup L (carrier L)" 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

992 

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

994 
bottom :: "_ => 'a" ("\<bottom>\<index>") 
35847  995 
where "\<bottom>\<^bsub>L\<^esub> == inf L (carrier L)" 
14551  996 

997 

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

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

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

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

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

1004 
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

1005 
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

1006 
by (fast intro: someI2 weak_least_unique P) 
14551  1007 
qed 
1008 

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

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

1010 
"A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L" 
14551  1011 
by (rule supI) simp_all 
1012 

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

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

1014 
"\<top> \<in> carrier L" 
14551  1015 
by (unfold top_def) simp 
1016 

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

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

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

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

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

1023 
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

1024 
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

1025 
by (fast intro: someI2 weak_greatest_unique P) 
14551  1026 
qed 
1027 

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

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

1029 
"A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L" 
14551  1030 
by (rule infI) simp_all 
1031 

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

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

1033 
"\<bottom> \<in> carrier L" 
14551  1034 
by (unfold bottom_def) simp 
1035 

1036 
text {* Jacobson: Theorem 8.1 *} 

1037 

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

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

1039 
"Lower L {} = carrier L" 
14551  1040 
by (unfold Lower_def) simp 
1041 

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

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

1043 
"Upper L {} = carrier L" 
14551  1044 
by (unfold Upper_def) simp 
1045 

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

1046 
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

1047 
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

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

1049 
"!!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

1050 
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

1051 
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

1052 
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

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

1054 
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

1055 
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

1056 
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

1057 
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

1058 
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

1059 
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

1060 
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

1061 
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

1062 
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

1063 
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

1064 
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

1065 
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

1066 
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

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

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

1069 
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

1070 
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

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

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

1073 
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

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

1075 
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

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

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

1078 
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

1079 
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

1080 
proof (cases "A = {}") 
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1081 
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

1082 
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

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

1084 
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

1085 
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

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

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

1088 

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

1089 
(* 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

1090 

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 
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

1093 

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

1094 
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

1095 
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

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

1097 

33657  1098 
declare weak_le_antisym [rule del] 
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27700
diff
changeset

1099 

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

1101 
"[ x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L ] ==> x = y" 
33657  1102 
using weak_le_antisym 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

1103 

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

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

1105 
"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

1106 
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

1107 

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

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

1109 
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

1110 
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

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

1112 
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

1113 

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

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

1115 

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

1116 

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

1117 
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

1118 

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

1119 
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

1120 
"[ 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

1121 
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

1122 

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

1123 
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

1124 
"[ 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

1125 
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

1126 

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

1127 

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

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

1129 

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

1130 
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

1131 
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

1132 
"[ 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

1133 

29242  1134 
sublocale upper_semilattice < weak: weak_upper_semilattice 
28823  1135 
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

1136 

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

1137 
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

1138 
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

1139 
"[ 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

1140 

29242  1141 
sublocale lower_semilattice < weak: weak_lower_semilattice 
28823  1142 
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

1143 

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

1144 
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

1145 

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

1146 

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

1147 
text {* Supremum *} 
27713
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 
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

1150 

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

1151 
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

1152 
"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

1153 
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

1154 

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

1155 
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

1156 
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

1157 
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

1158 
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

1159 

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

1160 
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

1161 
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

1162 
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

1163 
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

1164 

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

1165 

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

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

1167 

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

1168 
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

1169 

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

1170 
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

1171 
"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

1172 
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

1173 

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

1174 
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

1175 

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

1176 
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

1177 
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

1178 
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

1179 
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

1180 

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

1181 
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

1182 
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

1183 
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

1184 
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

1185 

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

1186 

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

1187 
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

1188 

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

1189 
locale total_order = partial_order + 
28823  1190 
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

1191 

29242  1192 
sublocale total_order < weak: weak_total_order 
28823  1193 
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

1194 

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

1195 
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

1196 

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

1197 
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

1198 
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

1199 
shows "total_order L" 
28823  1200 
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

1201 

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

1202 
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

1203 

29242  1204 
sublocale total_order < weak: lattice 
28823  1205 
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

1206 

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

1207 

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

1208 
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

1209 

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

1210 
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

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

1212 
"[ 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

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

1214 
"[ 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

1215 

29242  1216 
sublocale complete_lattice < weak: weak_complete_lattice 
28823  1217 
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

1218 

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

1219 
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

1220 

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

1221 
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

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

1223 
"!!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

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

1225 
"!!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

1226 
shows "complete_lattice L" 
28823  1227 
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

1228 

14551  1229 
theorem (in partial_order) complete_lattice_criterion1: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1230 
assumes top_exists: "EX g. greatest L g (carrier L)" 
14551  1231 
and inf_exists: 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1232 
"!!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

1233 
shows "complete_lattice L" 
14551  1234 
proof (rule complete_latticeI) 
22063
717425609192
Reverted to structure representation with records.
ballarin
parents:
21896
diff
changeset

1235 
from top_exists obtain top where top: "greatest L top (carrier L)" .. 
14551  1236 
fix 